New version of pattern open, separating local equations in Env.t#578
New version of pattern open, separating local equations in Env.t#578garrigue wants to merge 8 commits intoocaml:trunkfrom
Conversation
During type unification and pattern typing in presence of GADTs, it is useful to be able to share type equalities. Before this commit, this was done by using a environment reference to modify the environment when needed. However, that made impossible to locally update the environment without either losing the shared reference or propagating globally the changes. This is problematic for local opens in pattern that need to introduce new identifiers in the environment for the sake or name lookup but only within a limited scope. This commit introduces an `Env.mut` type to fix this limitation in preparation of local open in pattern.
This commits extends the pattern syntax to support local open in
patterns. Four new constructions mirroring the expression constructions
are added
* `M.(pattern)`
* `M.[pattern_list]` ⟺ M.([pattern_list])
* `M.{labeled_pattern_list}` ⟺ M.({label_pattern_list})
* `M.[| .. |] ⟺ M.( [| .. |] )
At the typing phase, the construction `M.(pattern)` brings all
identifiers defined within M inside the scope and then proceed with the
typing of `pattern`. All others constructions are desugared to the
`M.(..)` construction during parsing.
Questionable implementation details:
* Currently, the local pattern open use the `type_open` function like
the local expression pattern. However, this implies that values defined
inside `M` are also brought to the scope. A specialized
`type_open_for_pattern` would be more efficient.
This reverts commit 5d25446.
| type t = Ident.t | ||
| let compare = compare | ||
| end) | ||
| module IdentSet = Set.Make(Ident) |
There was a problem hiding this comment.
Ident.Set ? (added with all the Identifiable stuff with flambda)
There was a problem hiding this comment.
Fine, but this is completely orthogonal (the code was already there).
|
Currently, the constraints are only on simple identifiers, not qualified paths, right? I guess you directly introduced a PathMap to support gadt constraints on non-local abstract types (for http://caml.inria.fr/mantis/view.php?id=7233 ). Is that right? |
|
Yes, and this is also needed for modular implicits. |
|
I merged in trunk ( 2d33e16 ), thanks! |
…view (ocaml#578) Co-authored-by: Sabine Schmaltz <[email protected]> Co-authored-by: Christine Rose <[email protected]>
5 participants
This is a new branch of GPR #187, which reduces the amount of changes by putting local constrains in a specific field of Env.t rather than mixing them with types.
This should help for other extensions.
Note that a large part of the changes are due to commit 68fdc8a, adding a compare function to the Path module, which should have been done ages ago :)