Stefan pushed to branch master at Stefan / Typer

Commits: 7b789287 by Stefan Monnier at 2017-07-27T14:43:23-04:00 Merge VMap and IntMap into IMap

- - - - - 5f814ec5 by Stefan Monnier at 2017-07-27T14:47:31-04:00 * opslexp.ml (level_canon): CSE

- - - - - 632d0b65 by Stefan Monnier at 2017-07-27T14:57:23-04:00 Provide scope_level to create_metavar

* src/debruijn.ml (get_size): Check that the two lengths are in sync. (ectx_to_scope_level, ectx_local_scope_size): New functions.

* src/elab.ml (newMetavar, newMetalevel, newMetatype): Take current scope_level as argument. (check): Use ectx_local_scope_size.

* src/lexp.ml (scope_level): Move from deruijn.ml. (dummy_scope_level): New var.

* src/unification.ml (create_metavar): Take current scope_level as argument.

- - - - - 73e53794 by Stefan Monnier at 2017-07-27T15:09:15-04:00 (metavar_info): Keep track of scope_level

* src/lexp.ml (metavar_info): Keep track of scope_level. (empty_meta_subst, empty_constraint): Remove. (metavar_lookup): Lookups should never fail now.

* src/unification.ml (create_metavar): Record the scope_level.

- - - - -

7 changed files:

- src/debruijn.ml - src/elab.ml - src/eval.ml - src/lexp.ml - src/opslexp.ml - src/unification.ml - src/util.ml

Changes:

===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -104,21 +104,24 @@ type scope = db_ridx SMap.t (* Map<String, db_ridx>*) type senv_length = int (* it is not the map true length *) type senv_type = senv_length * scope

-(* 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. *) -type scope_level = int type lctx_length = db_ridx

(* This is the *elaboration context* (i.e. a context that holds * a lexp context plus some side info. *) type elab_context = senv_type * lexp_context * (scope_level * lctx_length)

+let get_size ctx = let ((n, _), lctx, _) = ctx in + assert (n = M.length lctx); n + (* Extract the lexp context from the context used during elaboration. *) let ectx_to_lctx (ectx : elab_context) : lexp_context = let (_, lctx, _) = ectx in lctx

+let ectx_to_scope_level ((_, _, (sl, _)) : elab_context) : scope_level = sl + +let ectx_local_scope_size (((n, _), _, (_, slen)) as ectx: elab_context) : int + = get_size ectx - slen + (* internal definitions * ---------------------------------- *)

@@ -131,8 +134,6 @@ let _make_myers = M.nil

let empty_elab_context : elab_context = (_make_senv_type, _make_myers, (0, 0))

-let get_size ctx = let ((n, _), _, _) = ctx in n - (* return its current DeBruijn index *) let rec senv_lookup (name: string) (ctx: elab_context): int = let ((n, map), _, _) = ctx in @@ -342,16 +343,16 @@ let rec lctx_view lctx =

(** Sets of DeBruijn indices **)

-type set = db_offset * unit VMap.t +type set = db_offset * unit IMap.t

-let set_empty = (0, VMap.empty) +let set_empty = (0, IMap.empty)

-let set_mem i (o, m) = VMap.mem (i - o) m +let set_mem i (o, m) = IMap.mem (i - o) m

-let set_set i (o, m) = (o, VMap.add (i - o) () m) -let set_reset i (o, m) = (o, VMap.remove (i - o) m) +let set_set i (o, m) = (o, IMap.add (i - o) () m) +let set_reset i (o, m) = (o, IMap.remove (i - o) m)

-let set_singleton i = (0, VMap.singleton i ()) +let set_singleton i = (0, IMap.singleton i ())

(* Adjust a set for use in a deeper scope with `o` additional bindings. *) let set_sink o (o', m) = (o + o', m) @@ -359,14 +360,14 @@ let set_sink o (o', m) = (o + o', m) (* Adjust a set for use in a higher scope with `o` fewer bindings. *) let set_hoist o (o', m) = let newo = o' - o in - let (_, _, newm) = VMap.split (-1 - newo) m + let (_, _, newm) = IMap.split (-1 - newo) m in (newo, newm)

let set_union (o1, m1) (o2, m2) : set = if o1 = o2 then - (o1, VMap.merge (fun k _ _ -> Some ()) m1 m2) + (o1, IMap.merge (fun k _ _ -> Some ()) m1 m2) else let o = o2 - o1 in - (o1, VMap.fold (fun i2 () m1 - -> VMap.add (i2 + o) () m1) + (o1, IMap.fold (fun i2 () m1 + -> IMap.add (i2 + o) () m1) m2 m1)

===================================== src/elab.ml ===================================== --- a/src/elab.ml +++ b/src/elab.ml @@ -232,22 +232,22 @@ let ctx_define_rec (ctx: elab_context) decls = * definitions. *)

- -let newMetavar l name t = - let meta = Unif.create_metavar () in +let newMetavar sl l name t = + let meta = Unif.create_metavar sl in mkMetavar (meta, S.Identity, (l, name), t)

-let newMetalevel () = - newMetavar Util.dummy_location "l" type_level +let newMetalevel sl = + newMetavar sl Util.dummy_location "l" type_level

-let newMetatype loc = newMetavar loc "t" (mkSort (loc, Stype (newMetalevel ()))) +let newMetatype sl loc + = newMetavar sl loc "t" (mkSort (loc, Stype (newMetalevel sl)))

(* Functions used when we need to return some lexp/ltype but * an error makes it impossible to return "the right one". *) -let mkDummy_type loc = newMetatype loc -let mkDummy_check loc t = newMetavar loc "dummy" t +let mkDummy_type loc = newMetatype dummy_scope_level loc +let mkDummy_check loc t = newMetavar dummy_scope_level loc "dummy" t let mkDummy_infer loc = - let t = newMetatype loc in (mkDummy_check loc t, t) + let t = newMetatype dummy_scope_level loc in (mkDummy_check loc t, t)

let rec infer (p : sexp) (ctx : elab_context): lexp * ltype =

@@ -288,7 +288,7 @@ let rec infer (p : sexp) (ctx : elab_context): lexp * ltype = parse_special_form ctx f args None else if (OL.conv_p (ectx_to_lctx ctx) t (BI.get_predef "Macro" ctx)) then - let t = newMetatype (sexp_location func) in + let t = newMetatype (ectx_to_scope_level ctx) (sexp_location func) in let lxp = handle_macro_call ctx f args t in (lxp, t) else @@ -296,7 +296,7 @@ let rec infer (p : sexp) (ctx : elab_context): lexp * ltype =

| Symbol (_, name) -> assert (String.length name >= 1 || String.get name 0 = '?'); - let t = newMetatype (sexp_location p) in + let t = newMetatype (ectx_to_scope_level ctx) (sexp_location p) in let lxp = check p t ctx in (lxp, t)

@@ -362,7 +362,7 @@ and get_implicit_arg ctx loc name t =

(* Elaborate the argument *) check lsarg t ctx - | None -> newMetavar loc name t + | None -> newMetavar (ectx_to_scope_level ctx) loc name t

(* Build the list of implicit arguments to instantiate. *) and instantiate_implicit e t ctx = @@ -390,7 +390,9 @@ and infer_type pexp ectx var = | _ -> (* FIXME: Here we rule out TypeLevel/TypeOmega. *) match - Unif.unify (mkSort (lexp_location s, Stype (newMetalevel ()))) s + Unif.unify (mkSort (lexp_location s, + Stype (newMetalevel (ectx_to_scope_level ectx)))) + s (ectx_to_lctx ectx) with | (None | Some (_::_)) -> (let lexp_string e = lexp_string (L.clean e) in @@ -410,9 +412,9 @@ and lexp_let_decls declss (body: lexp) ctx = declss body

and unify_with_arrow ctx tloc lxp kind var aty = - let body = newMetatype tloc in + let body = newMetatype (ectx_to_scope_level ctx) tloc in let arg = match aty with - | None -> newMetatype tloc + | None -> newMetatype (ectx_to_scope_level ctx) tloc | Some laty -> laty in let l, _ = var in let arrow = mkArrow (kind, Some var, arg, l, body) in @@ -451,13 +453,13 @@ and check (p : sexp) (t : ltype) (ctx : elab_context): lexp = -> let name = if name = "?" then "v" else (sexp_error l "Named metavars not supported (yet)"; String.sub name 1 (String.length name)) in - let (_, slen) = ectx_get_scope ctx in (* Shift the var so it can't refer to the local vars. * This is used so that in cases like "lambda t (y : ?) ... " * type inference can guess ? without having to wonder whether it * can refer `t` or not. If the user wants ? to be able to refer to * `t`, then she should explicitly write (y : ? t). *) - mkSusp (newMetavar l name t) (S.shift ((get_size ctx) - slen)) + mkSusp (newMetavar (ectx_to_scope_level ctx) l name t) + (S.shift (ectx_local_scope_size ctx))

| _ -> infer_and_check p ctx t

@@ -754,7 +756,7 @@ and lexp_parse_inductive ctors ctx = and track_fv rctx lctx e = let (fvs, mvs) = OL.fv e in let nc = EV.not_closed rctx fvs in - if nc = [] && not (VMap.is_empty mvs) then + if nc = [] && not (IMap.is_empty mvs) then "metavars" else if nc = [] then "a bug" @@ -839,11 +841,11 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) -> let adjusted_t = push_susp t (S.shift (i + 1)) in let e = check pexp adjusted_t nctx in let (ec, lc, sl) = nctx in - (IntMap.add i (v, e, t) map, + (IMap.add i (v, e, t) map, (ec, Myers.set_nth i (o, v', LetDef e, t) lc, sl)) | _ -> U.internal_error "Defining same slot!") - defs (IntMap.empty, nctx) in - let decls = List.rev (List.map (fun (_, d) -> d) (IntMap.bindings declmap)) in + defs (IMap.empty, nctx) in + let decls = List.rev (List.map (fun (_, d) -> d) (IMap.bindings declmap)) in decls, ctx_define_rec ectx decls

@@ -1012,8 +1014,8 @@ and get_attribute ctx loc largs = with Not_found -> None

and sform_dummy_ret loc = - let t = newMetatype loc in - (newMetavar loc "special-form-error" t, Inferred t) + let t = newMetatype dummy_scope_level loc in + (newMetavar dummy_scope_level loc "special-form-error" t, Inferred t)

and sform_get_attribute ctx loc (sargs : sexp list) ot = match get_attribute ctx loc (List.map (lexp_parse_sexp ctx) sargs) with @@ -1100,7 +1102,8 @@ let sform_typecons ctx loc sargs ot = -> let (kind, var, opxp) = pexp_p_formal_arg sformal in let ltp = match opxp with | Some pxp -> let (l,_) = infer pxp ctx in l - | None -> let (l,_) = var in newMetatype l in + | None -> let (l,_) = var in + newMetatype (ectx_to_scope_level ctx) l in

parse_formals sformals ((kind, var, ltp) :: rformals) (env_extend ctx var Variable ltp) in @@ -1184,7 +1187,7 @@ let rec sform_lambda kind ctx loc sargs ot = (match ot with | None -> mklam (match olt1 with | Some lt1 -> lt1 - | None -> newMetatype loc) + | None -> newMetatype (ectx_to_scope_level ctx) loc) None (* Read var type from the provided type *) | Some t @@ -1233,7 +1236,8 @@ let rec sform_case ctx loc sargs ot = match sargs with sexp_error l "Unrecognized simple case branch"; (Ppatany l, Symbol (l, "?")) in let pcases = List.map parse_case scases in - let t = match ot with Some t -> t | None -> newMetatype loc in + let t = match ot with Some t -> t + | None -> newMetatype (ectx_to_scope_level ctx) loc in let le = check_case t (loc, se, pcases) ctx in (le, match ot with Some _ -> Checked | None -> Inferred t)

===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -664,7 +664,7 @@ module CMap let ctx_memo = CMap.create 1000

let not_closed rctx ((o, vm) : DB.set) = - VMap.fold (fun i () nc -> let i = i + o in + IMap.fold (fun i () nc -> let i = i + o in let (_, rc) = Myers.nth i rctx in match !rc with Vundefined -> i::nc | _ -> nc) vm [] @@ -672,7 +672,7 @@ let not_closed rctx ((o, vm) : DB.set) = let closed_p rctx (fvs, mvs) = not_closed rctx fvs = [] (* FIXME: Handle metavars! *) - && VMap.is_empty mvs + && IMap.is_empty mvs

let from_lctx (lctx: lexp_context): runtime_env = (* FIXME: `eval` with a disabled IO.run. *)

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -121,8 +121,6 @@ type varbind = | ForwardRef | LetDef of lexp

-module VMap = Map.Make (struct type t = int let compare = compare end) - (* For metavariables, we give each metavar a (hopefully) unique integer * and then we store its corresponding info into the `metavar_table` * global map. @@ -139,20 +137,29 @@ module VMap = Map.Make (struct type t = int let compare = compare end) * integer in order to procude a hash anyway (and we'd have to write the hash * function by hand, tho that might be a good idea anyway). *) -type metavar_info = lexp -type meta_subst = metavar_info VMap.t -type constraints = (lexp * lexp) list

-let empty_meta_subst : meta_subst = VMap.empty +(* 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. *) +type scope_level = int

-let empty_constraint : constraints = [] +type metavar_info = + | MVal of lexp (* Exp to which the var is instantiated. *) + | MLevel of scope_level (* Outermost scope in which the var appears. *) +type meta_subst = metavar_info U.IMap.t +type constraints = (lexp * lexp) list

+let dummy_scope_level = 0 let impossible = Imm Sexp.dummy_epsilon

let builtin_size = ref 0

-let metavar_table = ref (VMap.empty : meta_subst) -let metavar_lookup idx : metavar_info = VMap.find idx (!metavar_table) +let metavar_table = ref (U.IMap.empty : meta_subst) +let metavar_lookup idx : metavar_info + = try U.IMap.find idx (!metavar_table) + with Not_found + -> U.msg_fatal "LEXP" U.dummy_location "metavar lookup failure!"

(********************** Hash-consing **********************)

@@ -358,10 +365,11 @@ let clean e = | Susp (e, s') -> clean (scompose s' s) e | Var _ -> if S.identity_p s then e else clean S.identity (mkSusp e s) - | Metavar (idx, s', l, t) - -> let s = (scompose s' s) in - try clean s (metavar_lookup idx) - with Not_found -> mkMetavar (idx, s, l, t) + | Metavar (idx, s', name, t) + -> let s = scompose s' s in + match metavar_lookup idx with + | MVal e -> clean s e + | _ -> mkMetavar (idx, s, name, t) in clean S.identity e

let sdatacons = Symbol (U.dummy_location, "##datacons")

===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -22,6 +22,7 @@ this program. If not, see http://www.gnu.org/licenses/. *)

module U = Util module SMap = U.SMap +module IMap = U.IMap (* open Lexer *) open Sexp module P = Pexp @@ -173,8 +174,9 @@ let lexp_whnf e (ctx : DB.lexp_context) : lexp = | Call (Cons (_, (_, name)), aargs) -> reduce name aargs | _ -> mkCase (l, e, rt, branches, default)) | Metavar (idx, s, _, _) - -> (try lexp_whnf (mkSusp (metavar_lookup idx) s) ctx - with Not_found -> e) + -> (match metavar_lookup idx with + | MVal e -> lexp_whnf (push_susp e s) ctx + | _ -> e)

(* FIXME: I'd really prefer to use "native" recursive substitutions, using * ideally a trick similar to the db_offsets in lexp_context! *) @@ -297,24 +299,27 @@ let conv_p (ctx : DB.lexp_context) e1 e2 * and `m` maps variable indices to the maxmimum depth at which they were * found. *) let level_canon e = + let add_var_depth v d ((c,m) as acc) = + let o = try IMap.find v m with Not_found -> -1 in + if o < d then (c, IMap.add v d m) else acc in + let rec canon e d ((c,m) as acc) = match e with | SortLevel SLz -> if c < d then (d, m) else acc | SortLevel (SLsucc e) -> canon e (d + 1) acc | SortLevel (SLlub (e1, e2)) -> canon e1 d (canon e2 d acc) - | Var (_, i) -> let o = try VMap.find i m with Not_found -> -1 in - if o < d then (c, VMap.add i d m) else acc - | Metavar (i, _, _, _) - -> (try canon (metavar_lookup i) d acc - with Not_found - -> let o = try VMap.find (- i) m with Not_found -> -1 in - if o < d then (c, VMap.add (- i) d m) else acc) + | Var (_, i) -> add_var_depth i d acc + | Metavar (i, s, _, _) + -> (match metavar_lookup i with + | MVal e -> canon (push_susp e s) d acc + | _ -> add_var_depth (- i) d acc) + | Susp (e, s) -> canon (push_susp e s) d acc | _ -> (max_int, m) - in canon e 0 (0,VMap.empty) + in canon e 0 (0,IMap.empty)

let level_leq (c1, m1) (c2, m2) = c1 <= c2 && c1 != max_int - && VMap.for_all (fun i d -> try d <= VMap.find i m2 with Not_found -> false) + && IMap.for_all (fun i d -> try d <= IMap.find i m2 with Not_found -> false) m1

let rec mkSLlub ctx e1 e2 = @@ -604,10 +609,11 @@ let rec check' erased ctx e = ^ lexp_string t); DB.type_int)) | Metavar (idx, s, _, t) - -> (try let e = push_susp (metavar_lookup idx) s in - let t' = check erased ctx e in - assert_type ctx e t' t - with Not_found -> ()); + -> (match metavar_lookup idx with + | MVal e -> let e = push_susp e s in + let t' = check erased ctx e in + assert_type ctx e t' t + | _ -> ()); t

let check = check' DB.set_empty @@ -618,14 +624,14 @@ 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 = subst list VMap.t -let mv_set_empty = VMap.empty +type mv_set = subst list IMap.t +let mv_set_empty = IMap.empty let mv_set_add ms m s - = let ss = try VMap.find m ms with Not_found -> [] in + = let ss = try IMap.find m ms with Not_found -> [] in if List.mem s ss then ms - else VMap.add m (s::ss) ms + else IMap.add m (s::ss) ms let mv_set_union : mv_set -> mv_set -> mv_set - = VMap.merge (fun m oss1 oss2 + = IMap.merge (fun m oss1 oss2 -> match (oss1, oss2) with | (None, _) -> oss2 | (_, None) -> oss1

===================================== src/unification.ml ===================================== --- a/src/unification.ml +++ b/src/unification.ml @@ -36,16 +36,18 @@ module DB = Debruijn (* :-( *) let global_last_metavar = ref (-1) (*The first metavar is 0*)

-let create_metavar () = global_last_metavar := !global_last_metavar + 1; - !global_last_metavar +let create_metavar (sl : scope_level) + = let idx = !global_last_metavar + 1 in + global_last_metavar := idx; + metavar_table := U.IMap.add idx (MLevel sl) (!metavar_table); + idx

(* For convenience *) type return_type = constraints option

(** Alias for VMap.add*) -let associate (meta: int) (lxp: lexp) (subst: meta_subst) - : meta_subst = - (VMap.add meta lxp subst) +let associate (meta: int) (lxp: lexp) (subst: meta_subst) : meta_subst + = U.IMap.add meta (MVal lxp) subst

(** lexp is equivalent to _ in ocaml

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

module SMap = Map.Make (String) -module IntMap = Map.Make (struct type t = int let compare = compare end) +module IMap = Map.Make (struct type t = int let compare = compare end)

type charpos = int type bytepos = int

View it on GitLab: https://gitlab.com/monnier/typer/compare/fd03306646d4e6b60bcd59407bc55353746...

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