Partial environments

[zilinc]

Issue by lim060 Sat Jul 4 02:43:07 2015 Originally opened as https://github.csiro.au/ts-filesystems/Cogent/issues/89

---

The procedure environments Ξ (proc_ctx) and ξ (proc_env) are partial, since they are only meaningful for functions actually in the program. They are currently undefined for other keys.

The problem is, predicates like proc_ctx_wellformed or proc_env_matches are technically undefined on any concrete Ξ, ξ. This introduces unsoundness whenever such predicates appear in hypotheses. It's also hard to verify anything that transforms Ξ or ξ since parts of them are undefined.

[zilinc]

Comment by lim060 Sat Jul 4 02:49:32 2015

---

Possible solutions:

1. Use the map type which encodes partiality. Nones will pop up everywhere, so this implies messy changes to the semantics and proofs.
2. Use a dummy default value. Possibilities are Ξ _ = ([], TUnit, TUnit) and ξ _ _ _ = False. It's not known whether this hack will be compatible with proofs (present and future).