Stefan pushed to branch master at Stefan / Typer

Commits: 17853dd7 by Stefan Monnier at 2017-09-26T09:08:22-04:00 Finally implement the occurs check (and scope_level propagation)

* src/lexp.ml (ctx_length): Rename from scope_length.

* src/unification.ml (occurs_in): New function. (_unify_metavar.unif): Use it to avoid circular types and inconsistent generalization!

- - - - -

3 changed files:

- src/lexp.ml - src/opslexp.ml - src/unification.ml

Changes:

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -141,10 +141,10 @@ type varbind =

(* Scope level is used to detect "out of scope" metavars. * See http://okmij.org/ftp/ML/generalization.html - * The lctx_length keeps track of the lctx's length when that scope level was - * entered in order to know by how much to shift metavars. *) + * The ctx_length keeps track of the length of the lctx in which the + * metavar is meant to be defined. *) type scope_level = int -type scope_length = int +type ctx_length = int

type metavar_info = | MVal of lexp (* Exp to which the var is instantiated. *) @@ -153,7 +153,7 @@ type metavar_info = (* We'd like to keep the lexp_content in which the type is to be * understood, but lexp_context is not yet defined here, * so we just keep the length of the lexp_context. *) - * scope_length + * ctx_length type meta_subst = metavar_info U.IMap.t type constraints = (lexp * lexp) list

===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -624,7 +624,7 @@ let rec list_union l1 l2 = match l1 with | [] -> l2 | (x::l1) -> list_union l1 (if List.mem x l2 then l2 else (x::l2))

-type mv_set = (scope_level * ltype * scope_length * vname) IMap.t +type mv_set = (scope_level * ltype * ctx_length * vname) IMap.t (* Metavars that appear in non-erasable positions. *) * unit IMap.t let mv_set_empty : mv_set = (IMap.empty, IMap.empty)

===================================== src/unification.ml ===================================== --- a/src/unification.ml +++ b/src/unification.ml @@ -19,12 +19,6 @@ more details. You should have received a copy of the GNU General Public License along with this program. If not, see http://www.gnu.org/licenses/. *)

-(* FIXME: Needs occurs-check. - * Also needs to add a notion of scope-level, as described in - * http://okmij.org/ftp/ML/generalization.html (aka ranks in - * ftp://ftp.inria.fr/INRIA/Projects/cristal/Didier.Remy/eq-theory-on-types.ps.gz) - *) - open Lexp (* open Sexp *) (* open Inverse_subst *) @@ -47,9 +41,66 @@ let create_metavar (ctx : DB.lexp_context) (sl : scope_level) (t : ltype) type return_type = constraints option

(** Alias for VMap.add*) -let associate (meta: int) (lxp: lexp) (subst: meta_subst) : meta_subst - = U.IMap.add meta (MVal lxp) subst - +let associate (id: meta_id) (lxp: lexp) (subst: meta_subst) : meta_subst + = U.IMap.add id (MVal lxp) subst + +let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with + | MVal _ -> U.internal_error + "Checking occurrence of an instantiated metavar!!" + | MVar (sl, _, _) + -> let rec oi e = match e with + | Imm _ -> false + | SortLevel SLz -> false + | SortLevel (SLsucc e) -> oi e + | SortLevel (SLlub (e1, e2)) -> oi e1 || oi e2 + | Sort (_, Stype e) -> oi e + | Sort (_, (StypeOmega | StypeLevel)) -> false + | Builtin _ -> false + | Var (_, i) -> false + | Susp (e, s) -> U.internal_error "`e` should be "clean" here!?" + (* ; oi (push_susp e s) *) + | Let (_, defs, e) + -> List.fold_left (fun o (_, e, t) -> o || oi e || oi t) (oi e) defs + | Arrow (_, _, t1, _, t2) -> oi t1 || oi t2 + | Lambda (_, _, t, e) -> oi t || oi e + | Call (f, args) + -> List.fold_left (fun o (_, arg) -> o || oi arg) (oi f) args + | Inductive (_, _, args, cases) + -> SMap.fold + (fun _ fields o + -> List.fold_left (fun o (_, _, t) -> o || oi t) + o fields) + cases + (List.fold_left (fun o (_, _, t) -> o || oi t) false args) + | Cons (t, _) -> oi t + | Case (_, e, t, cases, def) + -> let o = oi e || oi t in + let o = match def with | None -> o | Some (_, e) -> o || oi e in + SMap.fold (fun _ (_, _, e) o -> o || oi e) + cases o + | Metavar (id', _, name) when id' = id -> true + | Metavar (id', _, _) + -> (match metavar_lookup id' with + | MVal e -> U.internal_error "`e` should be "clean" here!?" + (* ; oi e *) + | MVar (sl', t, cl) + -> if sl' > sl then + (* id' will now appear in id's scope, so if id's scope is + * higher than id', we need to make sure id' won't be + * generalized in sl' but only in sl! + * This is the trick mentioned in + * http://okmij.org/ftp/ML/generalization.html + * to avoid computing `fv lctx` when generalizing! *) + metavar_table := U.IMap.add id' (MVar (sl, t, cl)) + (!metavar_table); + false) in + let old_mvt = (!metavar_table) in + if oi e then + (* Undo the side-effects since we're not going to instantiate the + var after all! *) + (metavar_table := old_mvt; true) + else false + (** lexp is equivalent to _ in ocaml (Let , lexp) == (lexp , Let) @@ -175,6 +226,7 @@ and _unify_metavar ctx idx s (lxp1: lexp) (lxp2: lexp) lexp_print lxp; print_string "\n"; None + | lxp' when occurs_in idx lxp' -> None | lxp' -> metavar_table := associate idx lxp' (!metavar_table); match unify t (OL.get_type ctx lxp) ctx with

View it on GitLab: https://gitlab.com/monnier/typer/commit/17853dd7385dc60938a31aeee474bc28f637...

--- View it on GitLab: https://gitlab.com/monnier/typer/commit/17853dd7385dc60938a31aeee474bc28f637... You're receiving this email because of your account on gitlab.com.