Juillet 2017 - Typer - mailman.iro.umontreal.ca

Datatypes and tuples
by Stefan Monnier 02 Oct '18

02 Oct '18

Hi guys, Wondering if you might have an idea: In Typer, the basic datastructure is the "algebraic datatype" (which combines a sum, product, and recursion), and the basic eliminator is the "pattern matching case". It works OK, but is unsatisfactory: 1- both of those are fairly large/complex. 2- it means that extracting a record field is a "case" operation that discards all but the required field, so it's an O(n) operation (where n is the size of the record), if not in the final code, at least in intermediate code. 3- it means the choice of representation of datatype tags is hardcoded in the blackbox compiler. While point n°2 might seem irrelevant, it is a pain with large records, such as those you might get when records are used to represent modules: the encoding of the simple "String.concat" reference ends up taking space proportional to the number of primitives exported from the "String" module, which can be rather large. I'd like to find another option and was thinking of something along the following lines: - provide a separate product primitive. - provide a "union" type, i.e. an *untagged* sum. - provide primitive discrimination operations, such as "dispatch on an Int". then the Either type could look like Either a b = union (Singleton(1), a) (Singleton(2), b) and case e | Left x => ... | Right y => ... would turn into switch (e.0 <withmagicproof>) | 1 => let e' = cast (Singleton(1), a) e; x = e'.1 in ... | 2 => let e' = cast (Singleton(2), b) e; y = e'.1 in ... Obviously, we'd still want to have "case", but written as a macro. The `magicproof` is needed to convince Typer that all union members have a field 0. And of course, each `cast` would also need to provide a proof (constructed from a proof provided by `switch`) that indeed we know that `e` is this specific member of the union. The way I presented it is fairly general, but pretty heavyweight to define and to use: every "case" will be compiled to that big switch-with-proofs and the definition of a "record selection out of a union" (such as the "e.0 <withmagicproof>") seems fairly complex as well. Does anyone here have another approach to suggest? Stefan

5 7

[Git][monnier/typer][master] * src/lexp.ml: Move the type info of metavars from lexp to metavar_info
by Stefan 29 Jul '17

29 Jul '17

Stefan pushed to branch master at Stefan / Typer Commits: c9eae130 by Stefan Monnier at 2017-07-29T22:43:16-04:00 * src/lexp.ml: Move the type info of metavars from lexp to metavar_info (lexp): Don't carry the type of metavars any more. (scope_length): New type. (metavar_info): Rename MLevel to MVar and add type and ctx information. - - - - - 5 changed files: - src/elab.ml - src/lexp.ml - src/opslexp.ml - src/unification.ml - tests/unify_test.ml Changes: ===================================== src/elab.ml ===================================== --- a/src/elab.ml +++ b/src/elab.ml @@ -232,22 +232,24 @@ let ctx_define_rec (ctx: elab_context) decls = * definitions. *) -let newMetavar sl l name t = - let meta = Unif.create_metavar sl in - mkMetavar (meta, S.Identity, (l, name), t) +let newMetavar (ctx : lexp_context) sl l name t= + let meta = Unif.create_metavar ctx sl t in + mkMetavar (meta, S.Identity, (l, name)) -let newMetalevel sl = - newMetavar sl Util.dummy_location "l" type_level +let newMetalevel (ctx : elab_context) sl = + newMetavar (ectx_to_lctx ctx) sl Util.dummy_location "l" type_level -let newMetatype sl loc - = newMetavar sl loc "t" (mkSort (loc, Stype (newMetalevel sl))) +let newMetatype (ctx : elab_context) sl loc + = newMetavar (ectx_to_lctx ctx) sl loc + "t" (mkSort (loc, Stype (newMetalevel ctx 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 dummy_scope_level loc -let mkDummy_check loc t = newMetavar dummy_scope_level loc "dummy" t -let mkDummy_infer loc = - let t = newMetatype dummy_scope_level loc in (mkDummy_check loc t, t) +let mkDummy_type ctx loc = newMetatype ctx dummy_scope_level loc +let mkDummy_check ctx loc t = newMetavar (ectx_to_lctx ctx) dummy_scope_level + loc "dummy" t +let mkDummy_infer ctx loc = + let t = newMetatype ctx dummy_scope_level loc in (mkDummy_check ctx loc t, t) let rec infer (p : sexp) (ctx : elab_context): lexp * ltype = @@ -261,9 +263,9 @@ let rec infer (p : sexp) (ctx : elab_context): lexp * ltype = try SMap.find name (! BI.lmap) with Not_found -> sexp_error l ("Unknown builtin `" ^ name ^ "`"); - mkDummy_infer l + mkDummy_infer ctx l else (sexp_error l ("Invalid special identifier `" ^ name ^ "`"); - mkDummy_infer l) + mkDummy_infer ctx l) (* Symbol i.e identifier. *) | Symbol (loc, name) @@ -278,7 +280,7 @@ let rec infer (p : sexp) (ctx : elab_context): lexp * ltype = with Not_found -> (sexp_error loc ("The variable: `" ^ name ^ "` was not declared"); - mkDummy_infer loc)) + mkDummy_infer ctx loc)) | Node (se, []) -> infer se ctx @@ -288,7 +290,8 @@ 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 (ectx_to_scope_level ctx) (sexp_location func) in + let t = newMetatype ctx (ectx_to_scope_level ctx) + (sexp_location func) in let lxp = handle_macro_call ctx f args t in (lxp, t) else @@ -296,7 +299,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 (ectx_to_scope_level ctx) (sexp_location p) in + let t = newMetatype ctx (ectx_to_scope_level ctx) (sexp_location p) in let lxp = check p t ctx in (lxp, t) @@ -308,7 +311,7 @@ let rec infer (p : sexp) (ctx : elab_context): lexp * ltype = | Float _ -> DB.type_float | String _ -> DB.type_string; | _ -> sexp_error tloc "Could not find type"; - mkDummy_type tloc) + mkDummy_type ctx tloc) and parse_special_form ctx f args ot = @@ -329,7 +332,7 @@ and parse_special_form ctx f args ot = (e, t)) | _ -> lexp_error loc f ("Unknown special-form: " ^ lexp_string f); - mkDummy_infer loc + mkDummy_infer ctx loc (* Make up an argument of type `t` when none is provided. *) and get_implicit_arg ctx loc name t = @@ -362,7 +365,7 @@ and get_implicit_arg ctx loc name t = (* Elaborate the argument *) check lsarg t ctx - | None -> newMetavar (ectx_to_scope_level ctx) loc name t + | None -> newMetavar (ectx_to_lctx ctx) (ectx_to_scope_level ctx) loc name t (* Build the list of implicit arguments to instantiate. *) and instantiate_implicit e t ctx = @@ -391,7 +394,8 @@ and infer_type pexp ectx var = (* FIXME: Here we rule out TypeLevel/TypeOmega. *) match Unif.unify (mkSort (lexp_location s, - Stype (newMetalevel (ectx_to_scope_level ectx)))) + Stype (newMetalevel + ectx (ectx_to_scope_level ectx)))) s (ectx_to_lctx ectx) with | (None | Some (_::_)) @@ -411,26 +415,27 @@ and lexp_let_decls declss (body: lexp) ctx = List.fold_right (fun decls lxp -> mkLet (dloc, decls, lxp)) declss body -and unify_with_arrow ctx tloc lxp kind var aty = - let body = newMetatype (ectx_to_scope_level ctx) tloc in - let arg = match aty with - | 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 - match Unif.unify arrow lxp (ectx_to_lctx ctx) with - | None -> lexp_error tloc lxp ("Type " ^ lexp_string lxp - ^ " and " - ^ lexp_string arrow - ^ " does not match"); - (mkDummy_type l, mkDummy_type l) - | Some ((t1,t2)::_) - -> lexp_error tloc lxp ("Types `" ^ lexp_string t1 - ^ " and " - ^ lexp_string t2 - ^ " do not match"); - (mkDummy_type l, mkDummy_type l) - | Some [] -> arg, body +and unify_with_arrow ctx tloc lxp kind var aty + = let arg = match aty with + | None -> newMetatype ctx (ectx_to_scope_level ctx) tloc + | Some laty -> laty in + let nctx = ectx_extend ctx (Some var) Variable arg in + let body = newMetatype nctx (ectx_to_scope_level ctx) tloc in + let (l, _) = var in + let arrow = mkArrow (kind, Some var, arg, l, body) in + match Unif.unify arrow lxp (ectx_to_lctx ctx) with + | None -> lexp_error tloc lxp ("Type " ^ lexp_string lxp + ^ " and " + ^ lexp_string arrow + ^ " does not match"); + (mkDummy_type ctx l, mkDummy_type nctx l) + | Some ((t1,t2)::_) + -> lexp_error tloc lxp ("Types `" ^ lexp_string t1 + ^ " and " + ^ lexp_string t2 + ^ " do not match"); + (mkDummy_type ctx l, mkDummy_type nctx l) + | Some [] -> arg, body and check (p : sexp) (t : ltype) (ctx : elab_context): lexp = @@ -456,10 +461,15 @@ and check (p : sexp) (t : ltype) (ctx : elab_context): lexp = (* 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 (ectx_to_scope_level ctx) l name t) - (S.shift (ectx_local_scope_size ctx)) + * can refer to `t` or not. If the user wants ? to be able to refer + * to `t`, then she should explicitly write (y : ? t). *) + let ctx_shift = ectx_local_scope_size ctx in + let octx = Myers.nthcdr ctx_shift (ectx_to_lctx ctx) in + (* FIXME: `t` is defined in ctx instead of octx. + * We need something like: + * let t = push_inv_subst t (S.shift ctx_shift) in *) + mkSusp (newMetavar octx (ectx_to_scope_level ctx) l name t) + (S.shift ctx_shift) | _ -> infer_and_check p ctx t @@ -1013,14 +1023,15 @@ and get_attribute ctx loc largs = try Some (AttributeMap.find var map) with Not_found -> None -and sform_dummy_ret loc = - let t = newMetatype dummy_scope_level loc in - (newMetavar dummy_scope_level loc "special-form-error" t, Inferred t) +and sform_dummy_ret ctx loc = + let t = newMetatype ctx dummy_scope_level loc in + (newMetavar (ectx_to_lctx ctx) 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 | Some e -> (e, Lazy) - | None -> sexp_error loc "No attribute found"; sform_dummy_ret loc + | None -> sexp_error loc "No attribute found"; sform_dummy_ret ctx loc and sform_has_attribute ctx loc (sargs : sexp list) ot = let n = get_size ctx in @@ -1041,9 +1052,9 @@ and sform_declexpr ctx loc sargs ot = -> (match DB.env_lookup_expr ctx ((loc, vn), vi) with | Some lxp -> (lxp, Lazy) | None -> error loc "no expr available"; - sform_dummy_ret loc) + sform_dummy_ret ctx loc) | _ -> error loc "declexpr expects one argument"; - sform_dummy_ret loc + sform_dummy_ret ctx loc let sform_decltype ctx loc sargs ot = @@ -1051,7 +1062,7 @@ let sform_decltype ctx loc sargs ot = | [Var((_, vn), vi)] -> (DB.env_lookup_type ctx ((loc, vn), vi), Lazy) | _ -> error loc "decltype expects one argument"; - sform_dummy_ret loc + sform_dummy_ret ctx loc let builtin_value_types : ltype option SMap.t ref = ref SMap.empty @@ -1067,10 +1078,10 @@ let sform_built_in ctx loc sargs ot = (bi, Inferred ltp') | true, _ -> error loc "Wrong Usage of `Built-in`"; - sform_dummy_ret loc + sform_dummy_ret ctx loc | false, _ -> error loc "Use of `Built-in` in user code"; - sform_dummy_ret loc + sform_dummy_ret ctx loc let sform_datacons ctx loc sargs ot = match sargs with @@ -1079,13 +1090,13 @@ let sform_datacons ctx loc sargs ot = (mkCons (idt, sym), Lazy) | [_;_] -> sexp_error loc "Second arg of ##constr should be a symbol"; - sform_dummy_ret loc + sform_dummy_ret ctx loc | _ -> sexp_error loc "##constr requires two arguments"; - sform_dummy_ret loc + sform_dummy_ret ctx loc let sform_typecons ctx loc sargs ot = match sargs with - | [] -> sexp_error loc "No arg to ##typecons!"; (mkDummy_type loc, Lazy) + | [] -> sexp_error loc "No arg to ##typecons!"; (mkDummy_type ctx loc, Lazy) | formals :: constrs -> let (label, formals) = match formals with | Node (label, formals) -> (label, formals) @@ -1103,7 +1114,7 @@ let sform_typecons ctx loc sargs ot = let ltp = match opxp with | Some pxp -> let (l,_) = infer pxp ctx in l | None -> let (l,_) = var in - newMetatype (ectx_to_scope_level ctx) l in + newMetatype ctx (ectx_to_scope_level ctx) l in parse_formals sformals ((kind, var, ltp) :: rformals) (env_extend ctx var Variable ltp) in @@ -1134,7 +1145,7 @@ let sform_hastype ctx loc sargs ot = let le = check se lt ctx in (le, Inferred lt) | _ -> sexp_error loc "##_:_ takes two arguments"; - sform_dummy_ret loc + sform_dummy_ret ctx loc let sform_arrow kind ctx loc sargs ot = match sargs with @@ -1147,7 +1158,7 @@ let sform_arrow kind ctx loc sargs ot = let lt2 = infer_type st2 nctx None in (mkArrow (kind, v, lt1, loc, lt2), Lazy) | _ -> sexp_error loc "##_->_ takes two arguments"; - sform_dummy_ret loc + sform_dummy_ret ctx loc (* Infer or check, as the case may be. *) let elaborate ctx pe ot = @@ -1187,7 +1198,7 @@ let rec sform_lambda kind ctx loc sargs ot = (match ot with | None -> mklam (match olt1 with | Some lt1 -> lt1 - | None -> newMetatype (ectx_to_scope_level ctx) loc) + | None -> newMetatype ctx (ectx_to_scope_level ctx) loc) None (* Read var type from the provided type *) | Some t @@ -1225,7 +1236,7 @@ let rec sform_lambda kind ctx loc sargs ot = | Aimplicit -> "=>" | Aerasable -> "≡>") ^"_ takes two arguments"); - sform_dummy_ret loc + sform_dummy_ret ctx loc let rec sform_case ctx loc sargs ot = match sargs with | [Node (Symbol (_, "_|_"), se :: scases)] @@ -1236,15 +1247,16 @@ 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 (ectx_to_scope_level ctx) loc in + let t = match ot with + | Some t -> t + | None -> newMetatype ctx (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) (* In case there are no branches, pretend there was a | anyway. *) | [e] -> sform_case ctx loc [Node (Symbol (loc, "_|_"), sargs)] ot | _ -> sexp_error loc "Unrecognized case expression"; - sform_dummy_ret loc + sform_dummy_ret ctx loc let sform_letin ctx loc sargs ot = match sargs with | [sdecls; sbody] @@ -1255,7 +1267,7 @@ let sform_letin ctx loc sargs ot = match sargs with (lexp_let_decls declss bdy nctx, Inferred (mkSusp ltp s)) | _ -> sexp_error loc "Unrecognized let_in_ expression"; - sform_dummy_ret loc + sform_dummy_ret ctx loc (* Actually `Type_` could also be defined as a plain constant * Lambda("l", TypeLevel, Sort (Stype (Var "l"))) @@ -1269,7 +1281,7 @@ let sform_type ctx loc sargs ot = (mkSort (loc, Stype l), Inferred (mkSort (loc, Stype (SortLevel (SLsucc l))))) | _ -> sexp_error loc "##Type_ expects one argument"; - sform_dummy_ret loc + sform_dummy_ret ctx loc (* Only print var info *) and lexp_print_var_info ctx = ===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -81,7 +81,7 @@ type ltype = lexp * (vname option * lexp) option (* Default. *) (* The `subst` only applies to the lexp associated * with the metavar's "value", not to the ltype. *) - | Metavar of int * subst * vname * ltype + | Metavar of int * subst * vname (* (\* For logical metavars, there's no substitution. *\) * | Metavar of (U.location * string) * metakind * metavar ref * and metavar = @@ -143,10 +143,16 @@ type varbind = * 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 scope_length = int type metavar_info = | MVal of lexp (* Exp to which the var is instantiated. *) - | MLevel of scope_level (* Outermost scope in which the var appears. *) + | MVar of scope_level (* Outermost scope in which the var appears. *) + * ltype (* Expected type. *) + (* 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 type meta_subst = metavar_info U.IMap.t type constraints = (lexp * lexp) list @@ -191,7 +197,7 @@ let mkLambda (k, v, t, e) = hc (Lambda (k, v, t, e)) let mkInductive (l, n, a, cs) = hc (Inductive (l, n, a, cs)) let mkCons (t, n) = hc (Cons (t, n)) let mkCase (l, e, rt, bs, d) = hc (Case (l, e, rt, bs, d)) -let mkMetavar (n, s, v, t) = hc (Metavar (n, s, v, t)) +let mkMetavar (n, s, v) = hc (Metavar (n, s, v)) let mkCall (f, es) = match f, es with | Call (f', es'), _ -> hc (Call (f', es' @ es)) @@ -214,7 +220,7 @@ let rec mkSusp e s = | Builtin _ -> e | Susp (e, s') -> mkSusp e (scompose s' s) | Var (l,v) -> slookup s l v - | Metavar (vn, s', vd, t) -> mkMetavar (vn, scompose s' s, vd, mkSusp t s) + | Metavar (vn, s', vd) -> mkMetavar (vn, scompose s' s, vd) | _ -> hc (Susp (e, s)) and scompose s1 s2 = S.compose mkSusp s1 s2 and slookup s l v = S.lookup (fun l i -> mkVar (l, i)) @@ -241,7 +247,7 @@ let rec lexp_location e = | Case (l,_,_,_,_) -> l | Susp (e, _) -> lexp_location e (* | Susp (_, e) -> lexp_location e *) - | Metavar (_,_,(l,_), _) -> l + | Metavar (_,_,(l,_)) -> l (********* Normalizing a term *********) @@ -365,11 +371,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', name, t) + | Metavar (idx, s', name) -> let s = scompose s' s in match metavar_lookup idx with | MVal e -> clean s e - | _ -> mkMetavar (idx, s, name, t) + | _ -> mkMetavar (idx, s, name) in clean S.identity e let sdatacons = Symbol (U.dummy_location, "##datacons") @@ -479,7 +485,7 @@ let rec lexp_unparse lxp = pbranch) (* FIXME: The cases below are all broken! *) - | Metavar (idx, subst, (loc, name), _) + | Metavar (idx, subst, (loc, name)) -> Symbol (loc, "?" ^ name ^ "-" ^ string_of_int idx ^ "[" ^ subst_string subst ^ "]") @@ -690,17 +696,17 @@ and _lexp_str ctx (exp : lexp) : string = | Var ((loc, name), idx) -> name ^ (index idx) ; - | Metavar (idx, subst, (loc, name), _) ->( + | Metavar (idx, subst, (loc, name)) (* print metavar result if any *) - let print_meta exp = - let ctx = set_meta exp ctx in - _lexp_str ctx (clean exp) in + -> (let print_meta exp = + let ctx = set_meta exp ctx in + _lexp_str ctx (clean exp) in - match pp_meta ctx with - | None -> print_meta exp - | Some e when e != exp -> print_meta exp - | _ -> - "?" ^ name ^ (subst_string subst) ^ (index idx)) + match pp_meta ctx with + | None -> print_meta exp + | Some e when e != exp -> print_meta exp + | _ -> + "?" ^ name ^ (subst_string subst) ^ (index idx)) | Let (_, decls, body) -> (* Print first decls without indent *) @@ -882,8 +888,8 @@ let rec eq e1 e2 = && (match (def1, def2) with | (Some (_, e1), Some (_, e2)) -> eq e1 e2 | _ -> def1 = def2) - | (Metavar (i1, s1, _, t1), Metavar (i2, s2, _, t2)) - -> i1 = i2 && eq t1 t2 && subst_eq s1 s2 + | (Metavar (i1, s1, _), Metavar (i2, s2, _)) + -> i1 = i2 && subst_eq s1 s2 | _ -> false and subst_eq s1 s2 = ===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -173,7 +173,7 @@ let lexp_whnf e (ctx : DB.lexp_context) : lexp = | Cons (_, (_, name)) -> reduce name [] | Call (Cons (_, (_, name)), aargs) -> reduce name aargs | _ -> mkCase (l, e, rt, branches, default)) - | Metavar (idx, s, _, _) + | Metavar (idx, s, _) -> (match metavar_lookup idx with | MVal e -> lexp_whnf (push_susp e s) ctx | _ -> e) @@ -308,7 +308,7 @@ let level_canon e = | SortLevel (SLsucc e) -> canon e (d + 1) acc | SortLevel (SLlub (e1, e2)) -> canon e1 d (canon e2 d acc) | Var (_, i) -> add_var_depth i d acc - | Metavar (i, s, _, _) + | Metavar (i, s, _) -> (match metavar_lookup i with | MVal e -> canon (push_susp e s) d acc | _ -> add_var_depth (- i) d acc) @@ -608,13 +608,11 @@ let rec check' erased ctx e = ("Cons of a non-inductive type: " ^ lexp_string t); DB.type_int)) - | Metavar (idx, s, _, t) + | Metavar (idx, s, _) -> (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 + check erased ctx e + | MVar (_, t, _) -> push_susp t s) let check = check' DB.set_empty @@ -703,9 +701,12 @@ let rec fv (e : lexp) : (DB.set * mv_set) = SMap.fold (fun _ (_, fields, e) s -> fv_union s (fv_hoist (List.length fields) (fv e))) cases s - | Metavar (m, s, _, t) - -> let (fvs, mvs) = fv t in - (fvs, mv_set_add mvs m s) + | Metavar (m, s, _) + -> (match metavar_lookup m with + | MVal e -> fv (push_susp e s) + | MVar (_, t, _) + -> let (fvs, mvs) = fv (push_susp t s) in + (fvs, mv_set_add mvs m s)) in try LMap.find fv_memo e with Not_found @@ -818,7 +819,10 @@ let rec get_type ctx e = buildtype fargs with Not_found -> DB.type_int) | _ -> DB.type_int) - | Metavar (idx, s, _, t) -> t + | Metavar (idx, s, _) + -> (match metavar_lookup idx with + | MVal e -> get_type ctx (push_susp e s) + | MVar (_, t, _) -> push_susp t s) (*********** Type erasure, before evaluation. *****************) ===================================== src/unification.ml ===================================== --- a/src/unification.ml +++ b/src/unification.ml @@ -36,10 +36,11 @@ module DB = Debruijn (* :-( *) let global_last_metavar = ref (-1) (*The first metavar is 0*) -let create_metavar (sl : scope_level) +let create_metavar (ctx : DB.lexp_context) (sl : scope_level) (t : ltype) = let idx = !global_last_metavar + 1 in global_last_metavar := idx; - metavar_table := U.IMap.add idx (MLevel sl) (!metavar_table); + metavar_table := U.IMap.add idx (MVar (sl, t, Myers.length ctx)) + (!metavar_table); idx (* For convenience *) @@ -89,8 +90,8 @@ and unify' (e1: lexp) (e2: lexp) | ((Imm _, Imm _) | (Cons _, Cons _) | (Builtin _, Builtin _) | (Var _, Var _) | (Inductive _, Inductive _)) -> if OL.conv_p ctx e1' e2' then Some [] else None - | (l, (Metavar (idx, s, _, t) as r)) -> _unify_metavar ctx idx s t r l - | ((Metavar (idx, s, _, t) as l), r) -> _unify_metavar ctx idx s t l r + | (l, (Metavar (idx, s, _) as r)) -> _unify_metavar ctx idx s r l + | ((Metavar (idx, s, _) as l), r) -> _unify_metavar ctx idx s l r | (l, (Call _ as r)) -> _unify_call r l ctx vs' (* | (l, (Case _ as r)) -> _unify_case r l subst *) | (Arrow _ as l, r) -> _unify_arrow l r ctx vs' @@ -159,12 +160,16 @@ and _unify_lambda (lambda: lexp) (lxp: lexp) ctx vs : return_type = - metavar , metavar -> if Metavar = Metavar then OK else ERROR - metavar , lexp -> OK *) -and _unify_metavar ctx idx s t (lxp1: lexp) (lxp2: lexp) +and _unify_metavar ctx idx s (lxp1: lexp) (lxp2: lexp) : return_type = - let unif idx s t lxp = match Inverse_subst.inverse s with + let unif idx s lxp = match Inverse_subst.inverse s with | None -> None | Some s' - -> metavar_table := associate idx (mkSusp lxp s') (!metavar_table); + -> let t = match metavar_lookup idx with + | MVal _ -> U.internal_error + "`lexp_whnf` returned an instantiated metavar!!" + | MVar (_, t, _) -> push_susp t s in + metavar_table := associate idx (mkSusp lxp s') (!metavar_table); match unify t (OL.get_type ctx lxp) ctx with | Some [] as r -> r (* FIXME: Let's ignore the error for now. *) @@ -175,20 +180,20 @@ and _unify_metavar ctx idx s t (lxp1: lexp) (lxp2: lexp) ^ "\n" ^ "for " ^ lexp_string lxp ^ "\n"); Some [] in match lxp2 with - | Metavar (idx2, s2, _, t2) + | Metavar (idx2, s2, _) -> if idx = idx2 then (* FIXME: handle the case where s1 != s2 !! *) Some [] else (* If one of the two subst can't be inverted, try the other. * FIXME: There's probably a more general solution. *) - (match unif idx s t lxp2 with + (match unif idx s lxp2 with | Some s -> Some s | None -> - match unif idx2 s2 t2 lxp1 with + match unif idx2 s2 lxp1 with | Some s -> Some s | None -> None) - | _ -> unif idx s t lxp2 + | _ -> unif idx s lxp2 (** Unify a Call (call) and a lexp (lxp) - Call , Call -> UNIFY ===================================== tests/unify_test.ml ===================================== --- a/tests/unify_test.ml +++ b/tests/unify_test.ml @@ -183,7 +183,7 @@ let generate_testable (_: lexp list) : ((lexp * lexp * result) list) = ::(input_type , input_type_t , Equivalent) (* 44 *) - ::(Metavar (0, S.Identity, (Util.dummy_location, "M"), DB.type0), + ::(Metavar (0, S.Identity, (Util.dummy_location, "M")), Var ((Util.dummy_location, "x"), 3), Unification) (* 45 *) ::[] View it on GitLab: https://gitlab.com/monnier/typer/commit/c9eae130af634a4513935752502a5176e1c… --- View it on GitLab: https://gitlab.com/monnier/typer/commit/c9eae130af634a4513935752502a5176e1c… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][master] 4 commits: Merge VMap and IntMap into IMap
by Stefan 27 Jul '17

27 Jul '17

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/fd03306646d4e6b60bcd59407bc5535374… --- View it on GitLab: https://gitlab.com/monnier/typer/compare/fd03306646d4e6b60bcd59407bc5535374… You're receiving this email because of your account on gitlab.com.

1 0

***SPAM*** [Git][monnier/typer][master] Don't pass meta_ctx as arg any more
by Stefan 27 Jul '17

27 Jul '17

Stefan pushed to branch master at Stefan / Typer Commits: fd033066 by Stefan Monnier at 2017-07-27T14:26:38-04:00 Don't pass meta_ctx as arg any more Push the rest of last change, missed in last commit! - - - - - 9 changed files: - src/REPL.ml - src/builtin.ml - src/debug_util.ml - src/elab.ml - src/eval.ml - src/lexp.ml - src/opslexp.ml - src/unification.ml - tests/unify_test.ml Changes: ===================================== src/REPL.ml ===================================== --- a/src/REPL.ml +++ b/src/REPL.ml @@ -132,8 +132,7 @@ let ilexp_parse pexps lctx: ((ldecl list list * lexpr list) * elab_context) = let pdecls, pexprs = pexps in let ldecls, lctx = Elab.lexp_p_decls pdecls lctx in let lexprs = Elab.lexp_parse_all pexprs lctx in - let meta_ctx, _ = !global_substitution in - List.iter (fun lxp -> ignore (OL.check meta_ctx (ectx_to_lctx lctx) lxp)) + List.iter (fun lxp -> ignore (OL.check (ectx_to_lctx lctx) lxp)) lexprs; (ldecls, lexprs), lctx ===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -140,7 +140,7 @@ let lmap = ref (SMap.empty : (lexp * ltype) SMap.t) let add_builtin_cst (name : string) (e : lexp) = let map = !lmap in assert (not (SMap.mem name map)); - let t = OL.check VMap.empty Myers.nil e in + let t = OL.check Myers.nil e in lmap := SMap.add name (e, t) map let new_builtin_type name kind = ===================================== src/debug_util.ml ===================================== --- a/src/debug_util.ml +++ b/src/debug_util.ml @@ -296,7 +296,7 @@ let main () = let cctx = ectx_to_lctx ctx in (* run type check *) List.iter (fun (_, lxp, _) - -> let _ = OL.check VMap.empty cctx lxp in ()) + -> let _ = OL.check cctx lxp in ()) flexps; print_string (" " ^ (make_line '-' 76)); ===================================== src/elab.ml ===================================== --- a/src/elab.ml +++ b/src/elab.ml @@ -114,15 +114,14 @@ let get_special_form name = * to errors in the user's code). *) let elab_check_sort (ctx : elab_context) lsort var ltp = - let meta_ctx, _ = !global_substitution in - match (try OL.lexp_whnf lsort (ectx_to_lctx ctx) meta_ctx + match (try OL.lexp_whnf lsort (ectx_to_lctx ctx) with e -> print_string "Exception during whnf of "; lexp_print lsort; print_string "\n"; raise e) with | Sort (_, _) -> () (* All clear! *) - | _ -> let lexp_string e = lexp_string (L.clean meta_ctx e) in + | _ -> let lexp_string e = lexp_string (L.clean e) in let typestr = lexp_string ltp ^ " : " ^ lexp_string lsort in match var with | None -> lexp_error (lexp_location ltp) ltp @@ -133,8 +132,7 @@ let elab_check_sort (ctx : elab_context) lsort var ltp = ^ typestr) let elab_check_proper_type (ctx : elab_context) ltp var = - let meta_ctx, _ = !global_substitution in - try elab_check_sort ctx (OL.check meta_ctx (ectx_to_lctx ctx) ltp) var ltp + try elab_check_sort ctx (OL.check (ectx_to_lctx ctx) ltp) var ltp with e -> print_string "Exception while checking type `"; lexp_print ltp; (match var with @@ -148,14 +146,13 @@ let elab_check_def (ctx : elab_context) var lxp ltype = let lctx = ectx_to_lctx ctx in let loc = lexp_location lxp in - let meta_ctx, _ = !global_substitution in - let lexp_string e = lexp_string (L.clean meta_ctx e) in - let ltype' = try OL.check meta_ctx lctx lxp + let lexp_string e = lexp_string (L.clean e) in + let ltype' = try OL.check lctx lxp with e -> lexp_error loc lxp "Error while type-checking"; print_lexp_ctx (ectx_to_lctx ctx); raise e in - if (try OL.conv_p meta_ctx (ectx_to_lctx ctx) ltype ltype' + if (try OL.conv_p (ectx_to_lctx ctx) ltype ltype' with e -> print_string ("Exception while conversion-checking types:\n"); lexp_print ltype; @@ -287,10 +284,9 @@ let rec infer (p : sexp) (ctx : elab_context): lexp * ltype = | Node (func, args) -> let (f, t) as ft = infer func ctx in - let meta_ctx, _ = !global_substitution in - if (OL.conv_p meta_ctx (ectx_to_lctx ctx) t type_special_form) then + if (OL.conv_p (ectx_to_lctx ctx) t type_special_form) then parse_special_form ctx f args None - else if (OL.conv_p meta_ctx (ectx_to_lctx ctx) t + else if (OL.conv_p (ectx_to_lctx ctx) t (BI.get_predef "Macro" ctx)) then let t = newMetatype (sexp_location func) in let lxp = handle_macro_call ctx f args t in @@ -317,8 +313,7 @@ let rec infer (p : sexp) (ctx : elab_context): lexp * ltype = and parse_special_form ctx f args ot = let loc = lexp_location f in - let meta_ctx, _ = !global_substitution in - match OL.lexp_whnf f (ectx_to_lctx ctx) meta_ctx with + match OL.lexp_whnf f (ectx_to_lctx ctx) with | Builtin ((_, name), _, _) -> (* Special form. *) let (e, ot') = (get_special_form name) ctx loc args ot in @@ -327,20 +322,21 @@ and parse_special_form ctx f args ot = | (Some t, Checked) -> (e, t) | _ -> let inferred_t = match ot' with | Inferred t -> t - | _ -> let meta_ctx, _ = !global_substitution in - OL.get_type meta_ctx (ectx_to_lctx ctx) e in + | _ -> OL.get_type (ectx_to_lctx ctx) e in match ot with | None -> (e, inferred_t) | Some t -> let e = check_inferred ctx e inferred_t t in (e, t)) | _ -> lexp_error loc f ("Unknown special-form: " ^ lexp_string f); - let t = newMetatype loc in - (newMetavar loc "<dummy>" t, t) + mkDummy_infer loc (* Make up an argument of type `t` when none is provided. *) and get_implicit_arg ctx loc name t = (* lookup default attribute of t. *) + (* FIXME: Don't lookup defaults/tactics here. Instead, just always + * generate a metavar at this point. The use of defaults/tactics should be + * postponed, probably to just before we do HM-style generalization. *) match try (* FIXME: We shouldn't hard code as popular a name as `default`. *) let pidx, pname = (senv_lookup "default" ctx), "default" in @@ -370,9 +366,8 @@ and get_implicit_arg ctx loc name t = (* Build the list of implicit arguments to instantiate. *) and instantiate_implicit e t ctx = - let (meta_ctx, _) = !global_substitution in let rec instantiate t args = - match OL.lexp_whnf t (ectx_to_lctx ctx) meta_ctx with + match OL.lexp_whnf t (ectx_to_lctx ctx) with | Arrow ((Aerasable | Aimplicit) as ak, v, t1, _, t2) -> let arg = get_implicit_arg ctx (lexp_location e) @@ -387,18 +382,18 @@ and infer_type pexp ectx var = * Sort (?s), but in most cases the metavar would be allocated * unnecessarily. *) let t, s = infer pexp ectx in - (let meta_ctx, _ = !global_substitution in - match OL.lexp_whnf s (ectx_to_lctx ectx) meta_ctx with + (match OL.lexp_whnf s (ectx_to_lctx ectx) with | Sort (_, _) -> () (* All clear! *) (* FIXME: We could automatically coerce Type levels to Sorts, so we * could write `(a : TypeLevel) -> a -> a` instead of * `(a : TypeLevel) -> Type_ a -> Type_ a` *) | _ -> (* FIXME: Here we rule out TypeLevel/TypeOmega. *) - match Unif.unify (mkSort (lexp_location s, Stype (newMetalevel ()))) s - (ectx_to_lctx ectx) meta_ctx with - | (None | Some (_, _::_)) - -> (let lexp_string e = lexp_string (L.clean meta_ctx e) in + match + Unif.unify (mkSort (lexp_location s, Stype (newMetalevel ()))) s + (ectx_to_lctx ectx) with + | (None | Some (_::_)) + -> (let lexp_string e = lexp_string (L.clean e) in let typestr = lexp_string t ^ " : " ^ lexp_string s in match var with | None -> lexp_error (lexp_location t) t @@ -407,7 +402,7 @@ and infer_type pexp ectx var = -> lexp_error l t ("Type of `" ^ name ^ "` is not a proper type: " ^ typestr)) - | Some subst -> global_substitution := subst); + | Some [] -> ()); t and lexp_let_decls declss (body: lexp) ctx = @@ -421,20 +416,19 @@ and unify_with_arrow ctx tloc lxp kind var aty = | Some laty -> laty in let l, _ = var in let arrow = mkArrow (kind, Some var, arg, l, body) in - let meta_ctx, _ = !global_substitution in - match Unif.unify arrow lxp (ectx_to_lctx ctx) meta_ctx with + match Unif.unify arrow lxp (ectx_to_lctx ctx) with | None -> lexp_error tloc lxp ("Type " ^ lexp_string lxp ^ " and " ^ lexp_string arrow ^ " does not match"); (mkDummy_type l, mkDummy_type l) - | Some (_, (t1,t2)::_) + | Some ((t1,t2)::_) -> lexp_error tloc lxp ("Types `" ^ lexp_string t1 ^ " and " ^ lexp_string t2 ^ " do not match"); (mkDummy_type l, mkDummy_type l) - | Some subst -> global_substitution := subst; arg, body + | Some [] -> arg, body and check (p : sexp) (t : ltype) (ctx : elab_context): lexp = @@ -443,10 +437,9 @@ and check (p : sexp) (t : ltype) (ctx : elab_context): lexp = | Node (func, args) -> let (f, ft) = infer func ctx in - let meta_ctx, _ = !global_substitution in - if (OL.conv_p meta_ctx (ectx_to_lctx ctx) ft type_special_form) then + if (OL.conv_p (ectx_to_lctx ctx) ft type_special_form) then let (e, _) = parse_special_form ctx f args (Some t) in e - else if (OL.conv_p meta_ctx (ectx_to_lctx ctx) ft + else if (OL.conv_p (ectx_to_lctx ctx) ft (BI.get_predef "Macro" ctx)) then handle_macro_call ctx f args t else @@ -477,23 +470,22 @@ and infer_and_check pexp ctx t = * we use is to instantiate implicit arguments when needed, but we could/should * do lots of other things. *) and check_inferred ctx e inferred_t t = - let subst, _ = !global_substitution in - let (e, inferred_t) = match OL.lexp_whnf t (ectx_to_lctx ctx) subst with + let (e, inferred_t) = match OL.lexp_whnf t (ectx_to_lctx ctx) with | Arrow ((Aerasable | Aimplicit), _, _, _, _) -> (e, inferred_t) | _ -> instantiate_implicit e inferred_t ctx in - (match Unif.unify inferred_t t (ectx_to_lctx ctx) subst with + (match Unif.unify inferred_t t (ectx_to_lctx ctx) with | None -> lexp_error (lexp_location e) e ("Type mismatch! Context expected `" ^ lexp_string t ^ "` but expression has type `" ^ lexp_string inferred_t ^ "`") - | Some (_, (t1,t2)::_) + | Some ((t1,t2)::_) -> lexp_error (lexp_location e) e ("Type mismatch! Context expected `" ^ lexp_string t2 ^ "` but expression has type `" ^ lexp_string t1 ^ "`") - | Some subst -> global_substitution := subst); + | Some [] -> ()); e (* Lexp.case can sometimes be inferred, but we prefer to always check. *) @@ -512,15 +504,14 @@ and check_case rtype (loc, target, ppatterns) ctx = (* get target and its type *) let tlxp, tltp = infer target ctx in - let meta_ctx, _ = !global_substitution in (* FIXME: We need to be careful with whnf: while the output is "equivalent" * to the input, it's not necessarily as readable/efficient. * So try to reuse the "non-whnf" form whenever possible. *) - let call_split e = match (OL.lexp_whnf e (ectx_to_lctx ctx) meta_ctx) with + let call_split e = match (OL.lexp_whnf e (ectx_to_lctx ctx)) with | Call (f, args) -> (f, args) | _ -> (e,[]) in let it, targs = call_split tltp in - let constructors = match OL.lexp_whnf it (ectx_to_lctx ctx) meta_ctx with + let constructors = match OL.lexp_whnf it (ectx_to_lctx ctx) with (* FIXME: Check that it's `Inductive' only after performing Unif.unify * with the various branches, so that we can infer the type * of the target from the type of the patterns. *) @@ -546,16 +537,15 @@ and check_case rtype (loc, target, ppatterns) ctx = let add_branch pctor pargs = let loc = sexp_location pctor in let lctor, ct = infer pctor ctx in - let meta_ctx, _ = !global_substitution in - match OL.lexp_whnf lctor (ectx_to_lctx ctx) meta_ctx with + match OL.lexp_whnf lctor (ectx_to_lctx ctx) with | Cons (it', (_, cons_name)) - -> let _ = match Unif.unify it' it (ectx_to_lctx ctx) meta_ctx with - | (None | Some (_, _::_)) + -> let _ = match Unif.unify it' it (ectx_to_lctx ctx) with + | (None | Some (_::_)) -> lexp_error loc lctor ("Expected pattern of type `" ^ lexp_string it ^ "` but got `" ^ lexp_string it' ^ "`") - | Some subst -> global_substitution := subst in + | Some [] -> () in let _ = check_uniqueness pat cons_name lbranches in let cargs = try SMap.find cons_name constructors @@ -637,9 +627,8 @@ and check_case rtype (loc, target, ppatterns) ctx = | Ppatany _ -> add_default None | Ppatsym ((_, name) as var) -> (try let idx = senv_lookup name ctx in - let meta_ctx, _ = !global_substitution in match OL.lexp_whnf (mkVar (var, idx)) - (ectx_to_lctx ctx) meta_ctx with + (ectx_to_lctx ctx) with | Cons _ (* It's indeed a constructor! *) -> add_branch (Symbol var) [] | _ -> add_default (Some var) (* A named default branch. *) @@ -671,8 +660,7 @@ and infer_call ctx (func, ltp) (sargs: sexp list) = * Anonymous : lambda *) let rec handle_fun_args largs sargs pending ltp = - let meta_ctx, _ = !global_substitution in - let ltp' = OL.lexp_whnf ltp (ectx_to_lctx ctx) meta_ctx in + let ltp' = OL.lexp_whnf ltp (ectx_to_lctx ctx) in match sargs, ltp' with | _, Arrow (ak, Some (_, aname), arg_type, _, ret_type) when SMap.mem aname pending @@ -763,7 +751,7 @@ and lexp_parse_inductive ctors ctx = SMap.add name (make_args args ctx) lctors) SMap.empty ctors -and track_fv meta_ctx rctx lctx e = +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 @@ -781,24 +769,22 @@ and track_fv meta_ctx rctx lctx e = "somevars[" ^ string_of_int i ^ "-" ^ string_of_int o ^ "]" else name ^ " (" - ^ track_fv meta_ctx - (Myers.nthcdr drop rctx) + ^ track_fv (Myers.nthcdr drop rctx) (Myers.nthcdr drop lctx) - (L.clean meta_ctx e) + (L.clean e) ^ ")" | _ -> name in String.concat " " (List.map tfv nc) -and lexp_eval meta_ctx ectx e = - (* FIXME: Make erase_type take meta_ctx directly! *) - let e = L.clean meta_ctx e in +and lexp_eval ectx e = + let e = L.clean e in let ee = OL.erase_type e in - let rctx = EV.from_ectx meta_ctx ectx in + let rctx = EV.from_ectx ectx in if not (EV.closed_p rctx (OL.fv e)) then lexp_error (lexp_location e) e ("Expression `" ^ lexp_string e ^ "` is not closed: " - ^ track_fv meta_ctx rctx (ectx_to_lctx ectx) e); + ^ track_fv rctx (ectx_to_lctx ectx) e); try EV.eval ee rctx with exc -> EV.print_eval_trace None; raise exc @@ -807,13 +793,12 @@ and lexp_expand_macro loc macro_funct sargs ctx (ot : ltype option) : value_type = (* Build the function to be called *) - let meta_ctx, _ = !global_substitution in let macro_expand = BI.get_predef "Macro_expand" ctx in (* FIXME: Rather than remember the lexp of "expand_macro" in predef, * we should remember its value so we don't have to re-eval it everytime. *) - let macro_expand = lexp_eval meta_ctx ctx macro_expand in + let macro_expand = lexp_eval ctx macro_expand in (* FIXME: provide `ot` (the optional expected type) for non-decl macros. *) - let macro = lexp_eval meta_ctx ctx macro_funct in + let macro = lexp_eval ctx macro_funct in let args = [macro; BI.o2v_list sargs] in (* FIXME: Don't `mkCall + eval` but use eval_call instead! *) @@ -898,14 +883,13 @@ and lexp_decls_1 | (_, _, ForwardRef, t) -> push_susp t (S.shift (pt_idx + 1)) | _ -> U.internal_error "Var not found at its index!" in (* Unify it with the new one. *) - let meta_ctx, _ = !global_substitution in - let _ = match Unif.unify ltp pt (ectx_to_lctx nctx) meta_ctx with - | (None | Some (_, _::_)) + let _ = match Unif.unify ltp pt (ectx_to_lctx nctx) with + | (None | Some (_::_)) -> lexp_error l ltp ("New type annotation `" ^ lexp_string ltp ^ "` incompatible with previous `" ^ lexp_string pt ^ "`") - | Some subst -> global_substitution := subst in + | Some [] -> () in lexp_decls_1 sdecls ectx nctx pending_decls pending_defs else if List.exists (fun ((_, vname'), _) -> vname = vname') pending_defs then @@ -989,12 +973,11 @@ and lexp_parse_sexp (ctx: elab_context) (e : sexp) : lexp = and sform_new_attribute ctx loc sargs ot = match sargs with | [t] -> let ltp = infer_type t ctx None in - let meta_ctx, _ = !global_substitution in (* FIXME: This creates new values for type `ltp` (very wrong if `ltp` * is False, for example): Should be a type like `AttributeMap t` * instead. *) (mkBuiltin ((loc, "new-attribute"), - OL.lexp_close meta_ctx (ectx_to_lctx ctx) ltp, + OL.lexp_close (ectx_to_lctx ctx) ltp, Some AttributeMap.empty), Lazy) | _ -> fatal loc "new-attribute expects a single Type argument" @@ -1005,13 +988,12 @@ and sform_add_attribute ctx loc (sargs : sexp list) ot = | [table; Var((_, name), idx); attr] -> table, (n - idx, name), attr | _ -> fatal loc "add-attribute expects 3 arguments (table; var; attr)" in - let meta_ctx, _ = !global_substitution in - let map, attr_type = match OL.lexp_whnf table (ectx_to_lctx ctx) meta_ctx with + let map, attr_type = match OL.lexp_whnf table (ectx_to_lctx ctx) with | Builtin (_, attr_type, Some map) -> map, attr_type | _ -> fatal loc "add-attribute expects a table as first argument" in (* FIXME: Type check (attr: type == attr_type) *) - let attr' = OL.lexp_close meta_ctx (ectx_to_lctx ctx) attr in + let attr' = OL.lexp_close (ectx_to_lctx ctx) attr in let table = AttributeMap.add var attr' map in (mkBuiltin ((loc, "add-attribute"), attr_type, Some table), Lazy) @@ -1022,8 +1004,7 @@ and get_attribute ctx loc largs = | [table; Var((_, name), idx)] -> table, (ctx_n - idx, name) | _ -> fatal loc "get-attribute expects 2 arguments (table; var)" in - let meta_ctx, _ = !global_substitution in - let map = match OL.lexp_whnf table (ectx_to_lctx ctx) meta_ctx with + let map = match OL.lexp_whnf table (ectx_to_lctx ctx) with | Builtin (_, attr_type, Some map) -> map | _ -> fatal loc "get-attribute expects a table as first argument" in @@ -1045,8 +1026,7 @@ and sform_has_attribute ctx loc (sargs : sexp list) ot = | [table; Var((_, name), idx)] -> table, (n - idx, name) | _ -> fatal loc "get-attribute expects 2 arguments (table; var)" in - let meta_ctx, _ = !global_substitution in - let map, attr_type = match OL.lexp_whnf table (ectx_to_lctx ctx) meta_ctx with + let map, attr_type = match OL.lexp_whnf table (ectx_to_lctx ctx) with | Builtin (_, attr_type, Some map) -> map, attr_type | lxp -> lexp_fatal loc lxp "get-attribute expects a table as first argument" in @@ -1077,8 +1057,7 @@ let sform_built_in ctx loc sargs ot = match !_parsing_internals, sargs with | true, [String (_, name); stp] -> let ltp = infer_type stp ctx None in - let meta_ctx, _ = !global_substitution in - let ltp' = OL.lexp_close meta_ctx (ectx_to_lctx ctx) ltp in + let ltp' = OL.lexp_close (ectx_to_lctx ctx) ltp in let bi = mkBuiltin ((loc, name), ltp', None) in if not (SMap.mem name (!EV.builtin_functions)) then sexp_error loc ("Unknown built-in `" ^ name ^ "`"); @@ -1209,13 +1188,12 @@ let rec sform_lambda kind ctx loc sargs ot = None (* Read var type from the provided type *) | Some t - -> let meta_ctx, _ = !global_substitution in - match OL.lexp_whnf t (ectx_to_lctx ctx) meta_ctx with + -> match OL.lexp_whnf t (ectx_to_lctx ctx) with | Arrow (ak2, _, lt1, _, lt2) when ak2 = kind -> (match olt1 with | None -> () | Some lt1' - -> if not (OL.conv_p meta_ctx (ectx_to_lctx ctx) lt1 lt1') + -> if not (OL.conv_p (ectx_to_lctx ctx) lt1 lt1') then lexp_error (lexp_location lt1') lt1' ("Type mismatch! Context expected `" ^ lexp_string lt1 ^ "`")); @@ -1390,9 +1368,7 @@ let default_ectx let lctx = read_file (btl_folder ^ "/pervasive.typer") lctx in lctx -let default_rctx = - let meta_ctx, _ = !global_substitution in - EV.from_ectx meta_ctx default_ectx +let default_rctx = EV.from_ectx default_ectx (* String Parsing * --------------------------------------------------------- *) @@ -1402,8 +1378,7 @@ let _lexp_expr_str (str: string) (tenv: token_env) (grm: grammar) (limit: string option) (ctx: elab_context) = let pxps = _pexp_expr_str str tenv grm limit in let lexps = lexp_parse_all pxps ctx in - let meta_ctx, _ = !global_substitution in - List.iter (fun lxp -> ignore (OL.check meta_ctx (ectx_to_lctx ctx) lxp)) + List.iter (fun lxp -> ignore (OL.check (ectx_to_lctx ctx) lxp)) lexps; lexps ===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -674,7 +674,7 @@ let closed_p rctx (fvs, mvs) = (* FIXME: Handle metavars! *) && VMap.is_empty mvs -let from_lctx meta_ctx (lctx: lexp_context): runtime_env = +let from_lctx (lctx: lexp_context): runtime_env = (* FIXME: `eval` with a disabled IO.run. *) let rec from_lctx' (lctx: lexp_context): runtime_env = match lctx_view lctx with @@ -684,7 +684,7 @@ let from_lctx meta_ctx (lctx: lexp_context): runtime_env = Myers.cons (roname loname, ref (match def with | LetDef e - -> let e = L.clean meta_ctx e in + -> let e = L.clean e in if closed_p rctx (OL.fv e) then eval (OL.erase_type e) rctx else Vundefined @@ -695,7 +695,7 @@ let from_lctx meta_ctx (lctx: lexp_context): runtime_env = (fun fvs (_, odef, _) -> match odef with | LetDef e - -> OL.fv_union fvs (OL.fv (L.clean meta_ctx e)) + -> OL.fv_union fvs (OL.fv (L.clean e)) | _ -> fvs) OL.fv_empty defs in @@ -724,5 +724,5 @@ let from_lctx meta_ctx (lctx: lexp_context): runtime_env = in from_lctx lctx (* build a rctx from a ectx. *) -let from_ectx meta_ctx (ctx: elab_context): runtime_env = - from_lctx meta_ctx (ectx_to_lctx ctx) +let from_ectx (ctx: elab_context): runtime_env = + from_lctx (ectx_to_lctx ctx) ===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -122,7 +122,25 @@ type varbind = | LetDef of lexp module VMap = Map.Make (struct type t = int let compare = compare end) -type meta_subst = lexp VMap.t + +(* For metavariables, we give each metavar a (hopefully) unique integer + * and then we store its corresponding info into the `metavar_table` + * global map. + * + * Instead of this single ref-cell holding an IntMap, we could use many + * ref-cells, and do away with the unique integer. The reasons why we + * do it this way are: + * - for printing purposes, we want to have a printable unique identifier + * for each metavar. OCaml does not offer any way to turn a ref-cell + * into some kind of printable identifier (can't get a hash of the address, + * no `eq` hash-tables, ...). + * - Hashtbl.hash as well as `compare` happily follow ref-cell indirections: + * `compare (ref 0) (ref 0)` tells us they're equal! So we need the unique + * 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 @@ -133,8 +151,8 @@ let impossible = Imm Sexp.dummy_epsilon let builtin_size = ref 0 -(* :-( *) -let global_substitution = ref (empty_meta_subst, empty_constraint) +let metavar_table = ref (VMap.empty : meta_subst) +let metavar_lookup idx : metavar_info = VMap.find idx (!metavar_table) (********************** Hash-consing **********************) @@ -342,8 +360,7 @@ let clean e = else clean S.identity (mkSusp e s) | Metavar (idx, s', l, t) -> let s = (scompose s' s) in - let meta_ctx, _ = !global_substitution in - try clean s (VMap.find idx meta_ctx) + try clean s (metavar_lookup idx) with Not_found -> mkMetavar (idx, s, l, t) in clean S.identity e ===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -173,8 +173,7 @@ 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, _, _) - -> (let meta_ctx, _ = !global_substitution in - try lexp_whnf (mkSusp (L.VMap.find idx meta_ctx) s) ctx + -> (try lexp_whnf (mkSusp (metavar_lookup idx) s) ctx with Not_found -> e) (* FIXME: I'd really prefer to use "native" recursive substitutions, using @@ -305,8 +304,7 @@ let level_canon e = | 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, _, _, _) - -> (let meta_ctx, _ = !global_substitution in - try canon (VMap.find i meta_ctx) d acc + -> (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) @@ -606,8 +604,7 @@ let rec check' erased ctx e = ^ lexp_string t); DB.type_int)) | Metavar (idx, s, _, t) - -> (try let meta_ctx, _ = !global_substitution in - let e = push_susp (L.VMap.find idx meta_ctx) s in + -> (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 -> ()); ===================================== src/unification.ml ===================================== --- a/src/unification.ml +++ b/src/unification.ml @@ -1,6 +1,6 @@ (* unification.ml --- Unification of Lexp terms -Copyright (C) 2016 Free Software Foundation, Inc. +Copyright (C) 2016-2017 Free Software Foundation, Inc. Author: Vincent Bonnevalle <tiv.crb(a)gmail.com> @@ -40,24 +40,13 @@ let create_metavar () = global_last_metavar := !global_last_metavar + 1; !global_last_metavar (* For convenience *) -type return_type = (meta_subst * constraints) option +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) -(** If key is in map returns the value associated - else returns <code>None</code> -*) -let find_or_none (value: lexp) (map: meta_subst) : lexp option = - match value with - | Metavar (idx, _, _, _) - -> if VMap.mem idx map - then Some (VMap.find idx map) - else None - | _ -> None - (** lexp is equivalent to _ in ocaml (Let , lexp) == (lexp , Let) @@ -68,10 +57,10 @@ let find_or_none (value: lexp) (map: meta_subst) : lexp option = let unify_and res op = match res with | None -> None - | Some (subst, constraints1) - -> match op subst with + | Some constraints1 + -> match op with | None -> None - | Some (subst, constraints2) -> Some (subst, constraints2@constraints1) + | Some constraints2 -> Some (constraints2@constraints1) (****************************** Top level unify *************************************) @@ -82,35 +71,34 @@ let unify_and res op = match res with The metavar unifyer is the end rule, it can't call unify with it's parameter (changing their order) *) let rec unify (e1: lexp) (e2: lexp) - (ctx : DB.lexp_context) (subst: meta_subst) + (ctx : DB.lexp_context) : return_type = - unify' e1 e2 ctx OL.set_empty subst + unify' e1 e2 ctx OL.set_empty and unify' (e1: lexp) (e2: lexp) - (ctx : DB.lexp_context) (vs : OL.set_plexp) (subst: meta_subst) + (ctx : DB.lexp_context) (vs : OL.set_plexp) : return_type = - let e1' = OL.lexp_whnf e1 ctx subst in - let e2' = OL.lexp_whnf e2 ctx subst in + let e1' = OL.lexp_whnf e1 ctx in + let e2' = OL.lexp_whnf e2 ctx in let changed = not (e1 == e1' && e2 == e2') in - if changed && OL.set_member_p subst vs e1' e2' then Some (subst, []) else + if changed && OL.set_member_p vs e1' e2' then Some [] else let vs' = if changed then OL.set_add vs e1' e2' else vs in match (e1', e2') with | ((Imm _, Imm _) | (Cons _, Cons _) | (Builtin _, Builtin _) | (Var _, Var _) | (Inductive _, Inductive _)) - -> if OL.conv_p subst ctx e1' e2' then Some (subst, []) else None - | (l, (Metavar (idx, s, _, t) as r)) -> _unify_metavar subst ctx idx s t r l - | ((Metavar (idx, s, _, t) as l), r) -> _unify_metavar subst ctx idx s t l r - | (l, (Call _ as r)) -> _unify_call r l ctx vs' subst + -> if OL.conv_p ctx e1' e2' then Some [] else None + | (l, (Metavar (idx, s, _, t) as r)) -> _unify_metavar ctx idx s t r l + | ((Metavar (idx, s, _, t) as l), r) -> _unify_metavar ctx idx s t l r + | (l, (Call _ as r)) -> _unify_call r l ctx vs' (* | (l, (Case _ as r)) -> _unify_case r l subst *) - | (Arrow _ as l, r) -> _unify_arrow l r ctx vs' subst - | (Lambda _ as l, r) -> _unify_lambda l r ctx vs' subst - | (Call _ as l, r) -> _unify_call l r ctx vs' subst + | (Arrow _ as l, r) -> _unify_arrow l r ctx vs' + | (Lambda _ as l, r) -> _unify_lambda l r ctx vs' + | (Call _ as l, r) -> _unify_call l r ctx vs' (* | (Case _ as l, r) -> _unify_case l r subst *) (* | (Inductive _ as l, r) -> _unify_induct l r subst *) - | (Sort _ as l, r) -> _unify_sort l r ctx vs' subst - | (SortLevel _ as l, r) -> _unify_sortlvl l r ctx vs' subst - | _ -> Some (subst, - if OL.conv_p subst ctx e1' e2' then [] else [(e1, e2)]) + | (Sort _ as l, r) -> _unify_sort l r ctx vs' + | (SortLevel _ as l, r) -> _unify_sortlvl l r ctx vs' + | _ -> Some (if OL.conv_p ctx e1' e2' then [] else [(e1, e2)]) (********************************* Type specific unify *******************************) @@ -121,20 +109,20 @@ and unify' (e1: lexp) (e2: lexp) - (Arrow, Var) -> Constraint - (_, _) -> None *) -and _unify_arrow (arrow: lexp) (lxp: lexp) ctx vs (subst: meta_subst) +and _unify_arrow (arrow: lexp) (lxp: lexp) ctx vs : return_type = match (arrow, lxp) with | (Arrow (var_kind1, v1, ltype1, _, lexp1), Arrow (var_kind2, _, ltype2, _, lexp2)) -> if var_kind1 = var_kind2 - then unify_and (unify' ltype1 ltype2 ctx vs subst) + then unify_and (unify' ltype1 ltype2 ctx vs) (unify' lexp1 lexp2 (DB.lexp_ctx_cons ctx 0 v1 Variable ltype1) (OL.set_shift vs)) else None | (Arrow _, Imm _) -> None - | (Arrow _, Var _) -> Some (subst, [(arrow, lxp)]) - | (Arrow _, _) -> unify' lxp arrow ctx vs subst + | (Arrow _, Var _) -> Some ([(arrow, lxp)]) + | (Arrow _, _) -> unify' lxp arrow ctx vs | (_, _) -> None (** Unify a Lambda and a lexp if possible @@ -145,22 +133,22 @@ and _unify_arrow (arrow: lexp) (lxp: lexp) ctx vs (subst: meta_subst) - Lambda , Let -> Constraint - Lambda , lexp -> unify lexp lambda subst *) -and _unify_lambda (lambda: lexp) (lxp: lexp) ctx vs (subst: meta_subst) : return_type = +and _unify_lambda (lambda: lexp) (lxp: lexp) ctx vs : return_type = match (lambda, lxp) with | (Lambda (var_kind1, v1, ltype1, lexp1), Lambda (var_kind2, _, ltype2, lexp2)) -> if var_kind1 = var_kind2 - then unify_and (unify' ltype1 ltype2 ctx vs subst) + then unify_and (unify' ltype1 ltype2 ctx vs) (unify' lexp1 lexp2 (DB.lexp_ctx_cons ctx 0 (Some v1) Variable ltype1) (OL.set_shift vs)) else None - | (Lambda _, Var _) -> Some ((subst, [(lambda, lxp)])) - | (Lambda _, Let _) -> Some ((subst, [(lambda, lxp)])) + | ((Lambda _, Var _) + | (Lambda _, Let _) + | (Lambda _, Call _)) -> Some [(lambda, lxp)] | (Lambda _, Arrow _) -> None - | (Lambda _, Call _) -> Some ((subst, [(lambda, lxp)])) | (Lambda _, Imm _) -> None - | (Lambda _, _) -> unify' lxp lambda ctx vs subst + | (Lambda _, _) -> unify' lxp lambda ctx vs | (_, _) -> None (** Unify a Metavar and a lexp if possible @@ -169,26 +157,26 @@ and _unify_lambda (lambda: lexp) (lxp: lexp) ctx vs (subst: meta_subst) : return - metavar , metavar -> if Metavar = Metavar then OK else ERROR - metavar , lexp -> OK *) -and _unify_metavar (subst: meta_subst) ctx idx s t (lxp1: lexp) (lxp2: lexp) +and _unify_metavar ctx idx s t (lxp1: lexp) (lxp2: lexp) : return_type = let unif idx s t lxp = match Inverse_subst.inverse s with | None -> None | Some s' - -> let subst = associate idx (mkSusp lxp s') subst in - match unify t (OL.get_type subst ctx lxp) ctx subst with - | Some (subst, []) as r -> r + -> metavar_table := associate idx (mkSusp lxp s') (!metavar_table); + match unify t (OL.get_type ctx lxp) ctx with + | Some [] as r -> r (* FIXME: Let's ignore the error for now. *) | _ -> print_string ("Unification of metavar type failed:\n " - ^ lexp_string (Lexp.clean subst t) ^ " != " - ^ lexp_string (Lexp.clean subst (OL.get_type subst ctx lxp)) ^ "\n" - ^ "for " ^ lexp_string lxp ^ "\n"); - Some (subst, []) in + ^ lexp_string (Lexp.clean t) ^ " != " + ^ lexp_string (Lexp.clean (OL.get_type ctx lxp)) + ^ "\n" ^ "for " ^ lexp_string lxp ^ "\n"); + Some [] in match lxp2 with | Metavar (idx2, s2, _, t2) -> if idx = idx2 then (* FIXME: handle the case where s1 != s2 !! *) - Some ((subst, [])) + Some [] else (* If one of the two subst can't be inverted, try the other. * FIXME: There's probably a more general solution. *) @@ -204,19 +192,18 @@ and _unify_metavar (subst: meta_subst) ctx idx s t (lxp1: lexp) (lxp2: lexp) - Call , Call -> UNIFY - Call , lexp -> CONSTRAINT *) -and _unify_call (call: lexp) (lxp: lexp) ctx vs (subst: meta_subst) +and _unify_call (call: lexp) (lxp: lexp) ctx vs : return_type = match (call, lxp) with | (Call (lxp_left, lxp_list1), Call (lxp_right, lxp_list2)) - when OL.conv_p subst ctx lxp_left lxp_right - -> List.fold_left (fun op ((ak1, e1), (ak2, e2)) subst + when OL.conv_p ctx lxp_left lxp_right + -> List.fold_left (fun op ((ak1, e1), (ak2, e2)) -> if ak1 == ak2 then - unify_and (unify' e1 e2 ctx vs subst) op + unify_and (unify' e1 e2 ctx vs) op else None) - (fun subst -> Some (subst, [])) + (Some []) (List.combine lxp_list1 lxp_list2) - subst - | (Call _, _) -> Some ((subst, [(call, lxp)])) + | (Call _, _) -> Some [(call, lxp)] | (_, _) -> None (** Unify a Case with a lexp @@ -276,11 +263,11 @@ and _unify_call (call: lexp) (lxp: lexp) ctx vs (subst: meta_subst) - SortLevel, SortLevel -> if SortLevel ~= SortLevel then OK else ERROR - SortLevel, _ -> ERROR *) -and _unify_sortlvl (sortlvl: lexp) (lxp: lexp) ctx vs (subst: meta_subst) : return_type = +and _unify_sortlvl (sortlvl: lexp) (lxp: lexp) ctx vs : return_type = match sortlvl, lxp with | (SortLevel s, SortLevel s2) -> (match s, s2 with - | SLz, SLz -> Some (subst, []) - | SLsucc l1, SLsucc l2 -> unify' l1 l2 ctx vs subst + | SLz, SLz -> Some [] + | SLsucc l1, SLsucc l2 -> unify' l1 l2 ctx vs (* FIXME: Handle SLsub! *) | _, _ -> None) | _, _ -> None @@ -290,14 +277,14 @@ and _unify_sortlvl (sortlvl: lexp) (lxp: lexp) ctx vs (subst: meta_subst) : retu - Sort, Var -> Constraint - Sort, lexp -> ERROR *) -and _unify_sort (sort_: lexp) (lxp: lexp) ctx vs (subst: meta_subst) : return_type = +and _unify_sort (sort_: lexp) (lxp: lexp) ctx vs : return_type = match sort_, lxp with | (Sort (_, srt), Sort (_, srt2)) -> (match srt, srt2 with - | Stype lxp1, Stype lxp2 -> unify' lxp1 lxp2 ctx vs subst - | StypeOmega, StypeOmega -> Some (subst, []) - | StypeLevel, StypeLevel -> Some (subst, []) + | Stype lxp1, Stype lxp2 -> unify' lxp1 lxp2 ctx vs + | StypeOmega, StypeOmega -> Some [] + | StypeLevel, StypeLevel -> Some [] | _, _ -> None) - | Sort _, Var _ -> Some (subst, [(sort_, lxp)]) + | Sort _, Var _ -> Some [(sort_, lxp)] | _, _ -> None (************************ Helper function **************************************) ===================================== tests/unify_test.ml ===================================== --- a/tests/unify_test.ml +++ b/tests/unify_test.ml @@ -43,7 +43,7 @@ type result = | Equivalent | Nothing -type unif_res = (result * (meta_subst * constraints) option * lexp * lexp) +type unif_res = (result * (constraints) option * lexp * lexp) type triplet = string * string * string @@ -188,29 +188,32 @@ let generate_testable (_: lexp list) : ((lexp * lexp * result) list) = ::[] -let test_input (lxp1: lexp) (lxp2: lexp) (subst: meta_subst): unif_res = - let res = unify lxp1 lxp2 Myers.nil subst in - let tmp = match res with - | Some (s, []) when s = empty_meta_subst -> (Equivalent, res, lxp1, lxp2) - | Some (_, []) -> (Unification, res, lxp1, lxp2) +let test_input (lxp1: lexp) (lxp2: lexp): unif_res = + let orig_subst = !metavar_table in + let res = unify lxp1 lxp2 Myers.nil in + match res with + | Some [] + -> let new_subst = !metavar_table in + if orig_subst == new_subst + then (Equivalent, res, lxp1, lxp2) + else (Unification, res, lxp1, lxp2) | Some _ -> (Constraint, res, lxp1, lxp2) | None -> (Nothing, res, lxp1, lxp2) - in tmp -let check (lxp1: lexp) (lxp2: lexp) (res: result) (subst: meta_subst): bool = - let r, _, _, _ = test_input lxp1 lxp2 subst +let check (lxp1: lexp) (lxp2: lexp) (res: result): bool = + let r, _, _, _ = test_input lxp1 lxp2 in if r = res then true else false let test_if (input: lexp list) sample_generator checker : bool = let rec test_if_ samples checker = match samples with - | (l1, l2, res)::t -> if checker l1 l2 res empty_meta_subst then test_if_ t checker else false + | (l1, l2, res)::t -> if checker l1 l2 res then test_if_ t checker else false | [] -> true in test_if_ (sample_generator input) checker let unifications = List.map (fun (l1, l2, res) -> - let r, _, _, _ = test_input l1 l2 empty_meta_subst + let r, _, _, _ = test_input l1 l2 in (l1, l2, res, r)) (* FIXME: Skip failure for now. *) [] (* (generate_testable []) *) View it on GitLab: https://gitlab.com/monnier/typer/commit/fd03306646d4e6b60bcd59407bc55353746… --- View it on GitLab: https://gitlab.com/monnier/typer/commit/fd03306646d4e6b60bcd59407bc55353746… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][master] Don't pass meta_ctx as arg any more
by Stefan 27 Jul '17

27 Jul '17

Stefan pushed to branch master at Stefan / Typer Commits: aaa414b2 by Stefan Monnier at 2017-07-27T10:29:18-04:00 Don't pass meta_ctx as arg any more Instead, assign to global_substitution directly from unification.ml. - - - - - 2 changed files: - src/lexp.ml - src/opslexp.ml Changes: ===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -80,7 +80,7 @@ type ltype = lexp * (U.location * (arg_kind * vname option) list * lexp) SMap.t * (vname option * lexp) option (* Default. *) (* The `subst` only applies to the lexp associated - * with the metavar's index (i.e. its "value"), not to the ltype. *) + * with the metavar's "value", not to the ltype. *) | Metavar of int * subst * vname * ltype (* (\* For logical metavars, there's no substitution. *\) * | Metavar of (U.location * string) * metakind * metavar ref @@ -289,7 +289,7 @@ and nosusp e = (* Return `e` with no outermost `Susp`. *) (* Get rid of `Susp`ensions and instantiated `Metavar`s. *) -let clean meta_ctx e = +let clean e = let rec clean s e = match e with | Imm _ -> e | SortLevel (SLz) -> e @@ -342,6 +342,7 @@ let clean meta_ctx e = else clean S.identity (mkSusp e s) | Metavar (idx, s', l, t) -> let s = (scompose s' s) in + let meta_ctx, _ = !global_substitution in try clean s (VMap.find idx meta_ctx) with Not_found -> mkMetavar (idx, s, l, t) in clean S.identity e @@ -667,9 +668,8 @@ and _lexp_str ctx (exp : lexp) : string = | Metavar (idx, subst, (loc, name), _) ->( (* print metavar result if any *) let print_meta exp = - let meta_ctx, _ = !global_substitution in let ctx = set_meta exp ctx in - _lexp_str ctx (clean meta_ctx exp) in + _lexp_str ctx (clean exp) in match pp_meta ctx with | None -> print_meta exp @@ -810,9 +810,8 @@ and _lexp_str_decls ctx decls = (** Syntactic equality (i.e. without β). *******) -let rec eq meta_ctx e1 e2 = +let rec eq e1 e2 = e1 == e2 || - let eq = eq meta_ctx in match (e1, e2) with | (Imm (Integer (_, i1)), Imm (Integer (_, i2))) -> i1 = i2 | (Imm (Float (_, x1)), Imm (Float (_, x2))) -> x1 = x2 @@ -859,23 +858,23 @@ let rec eq meta_ctx e1 e2 = | (Some (_, e1), Some (_, e2)) -> eq e1 e2 | _ -> def1 = def2) | (Metavar (i1, s1, _, t1), Metavar (i2, s2, _, t2)) - -> i1 = i2 && eq t1 t2 && subst_eq meta_ctx s1 s2 + -> i1 = i2 && eq t1 t2 && subst_eq s1 s2 | _ -> false -and subst_eq meta_ctx s1 s2 = +and subst_eq s1 s2 = s1 == s2 || match (s1, s2) with | (S.Identity, S.Identity) -> true | (S.Cons (e1, s1), S.Cons (e2, s2)) - -> eq meta_ctx e1 e2 && subst_eq meta_ctx s1 s2 + -> eq e1 e2 && subst_eq s1 s2 | (S.Shift (s1, o1), S.Shift (s2, o2)) -> let o = min o1 o2 in - subst_eq meta_ctx (S.mkShift s1 (o1 - o)) (S.mkShift s2 (o2 - o)) + subst_eq (S.mkShift s1 (o1 - o)) (S.mkShift s2 (o2 - o)) | (S.Shift (S.Cons (e1, s1), o1), S.Cons (e2, s2)) - -> eq meta_ctx (mkSusp e1 (S.shift o1)) e2 - && subst_eq meta_ctx (S.mkShift s1 o1) s2 + -> eq (mkSusp e1 (S.shift o1)) e2 + && subst_eq (S.mkShift s1 o1) s2 | (S.Cons (e1, s1), S.Shift (S.Cons (e2, s2), o2)) - -> eq meta_ctx e1 (mkSusp e2 (S.shift o2)) - && subst_eq meta_ctx s1 (S.mkShift s2 o2) + -> eq e1 (mkSusp e2 (S.shift o2)) + && subst_eq s1 (S.mkShift s2 o2) | _ -> false ===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -99,14 +99,14 @@ let rec lctx_to_subst lctx = * and return an equivalent expression valid in the empty context. * By "closed" I mean that it only refers to elements of the context which * are LetDef. *) -let lexp_close meta_ctx lctx e = +let lexp_close lctx e = (* There are many different ways to skin this cat. * This is definitely not the best one: * - it inlines all the definitions everywhere they're used * - It turns the lctx (of O(log N) access time) into a subst * (of O(N) access time) * Oh well! *) - L.clean meta_ctx (mkSusp e (lctx_to_subst lctx)) + L.clean (mkSusp e (lctx_to_subst lctx)) (** Reduce to weak head normal form. @@ -125,7 +125,7 @@ let lexp_close meta_ctx lctx e = * but only on *types*. If you must use it on code, be sure to use its * return value as little as possible since WHNF will inherently introduce * call-by-name behavior. *) -let lexp_whnf e (ctx : DB.lexp_context) meta_ctx : lexp = +let lexp_whnf e (ctx : DB.lexp_context) : lexp = let rec lexp_whnf e (ctx : DB.lexp_context) : lexp = match e with | Var v -> (match lookup_value ctx v with @@ -173,7 +173,8 @@ let lexp_whnf e (ctx : DB.lexp_context) meta_ctx : lexp = | Call (Cons (_, (_, name)), aargs) -> reduce name aargs | _ -> mkCase (l, e, rt, branches, default)) | Metavar (idx, s, _, _) - -> (try lexp_whnf (mkSusp (L.VMap.find idx meta_ctx) s) ctx + -> (let meta_ctx, _ = !global_substitution in + try lexp_whnf (mkSusp (L.VMap.find idx meta_ctx) s) ctx with Not_found -> e) (* FIXME: I'd really prefer to use "native" recursive substitutions, using @@ -189,16 +190,16 @@ let lexp_whnf e (ctx : DB.lexp_context) meta_ctx : lexp = (** A very naive implementation of sets of pairs of lexps. *) type set_plexp = (lexp * lexp) list let set_empty : set_plexp = [] -let set_member_p meta_ctx (s : set_plexp) (e1 : lexp) (e2 : lexp) : bool +let set_member_p (s : set_plexp) (e1 : lexp) (e2 : lexp) : bool = assert (e1 == Lexp.hc e1); assert (e2 == Lexp.hc e2); try let _ = List.find (fun (e1', e2') - -> L.eq meta_ctx e1 e1' && L.eq meta_ctx e2 e2') + -> L.eq e1 e1' && L.eq e2 e2') s in true with Not_found -> false let set_add (s : set_plexp) (e1 : lexp) (e2 : lexp) : set_plexp - = (* assert (not (set_member_p meta_ctx s e1 e2)); *) + = (* assert (not (set_member_p s e1 e2)); *) ((e1, e2) :: s) let set_shift_n (s : set_plexp) (n : U.db_offset) = List.map (let s = S.shift n in @@ -209,13 +210,12 @@ let set_shift s : set_plexp = set_shift_n s 1 (********* Testing if two types are "convertible" aka "equivalent" *********) (* Returns true if e₁ and e₂ are equal (upto alpha/beta/...). *) -let rec conv_p' meta_ctx (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = - let conv_p' = conv_p' meta_ctx in - let e1' = lexp_whnf e1 ctx meta_ctx in - let e2' = lexp_whnf e2 ctx meta_ctx in +let rec conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = + let e1' = lexp_whnf e1 ctx in + let e2' = lexp_whnf e2 ctx in e1' == e2' || let changed = not (e1 == e1' && e2 == e2') in - if changed && set_member_p meta_ctx vs e1' e2' then true else + if changed && set_member_p vs e1' e2' then true else let vs' = if changed then set_add vs e1' e2' else vs in let conv_p = conv_p' ctx vs' in match (e1', e2') with @@ -285,14 +285,15 @@ let rec conv_p' meta_ctx (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = (* FIXME: Various missing cases, such as Case. *) | (_, _) -> false -let conv_p meta_ctx (ctx : DB.lexp_context) e1 e2 +let conv_p (ctx : DB.lexp_context) e1 e2 = if e1 == e2 then true - else conv_p' meta_ctx ctx set_empty e1 e2 + else conv_p' ctx set_empty e1 e2 (********* Testing if a lexp is properly typed *********) -(* Turn e into its canonical representation, which is basically the set - * of vars it references along with the number of `succ` applied to them. +(* Turn e (presumably of type TypeLevel) into its canonical representation, + * which is basically the set of vars it references along with the number of + * `succ` applied to them. * `c` is the maximum "constant" level that occurs in `e` * and `m` maps variable indices to the maxmimum depth at which they were * found. *) @@ -304,8 +305,11 @@ let level_canon e = | 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, _, _, _) - -> let o = try VMap.find (- i) m with Not_found -> -1 in - if o < d then (c, VMap.add (- i) d m) else acc + -> (let meta_ctx, _ = !global_substitution in + try canon (VMap.find i meta_ctx) 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) | _ -> (max_int, m) in canon e 0 (0,VMap.empty) @@ -315,22 +319,22 @@ let level_leq (c1, m1) (c2, m2) = && VMap.for_all (fun i d -> try d <= VMap.find i m2 with Not_found -> false) m1 -let rec mkSLlub meta_ctx ctx e1 e2 = - match (lexp_whnf e1 ctx meta_ctx, lexp_whnf e2 ctx meta_ctx) with +let rec mkSLlub ctx e1 e2 = + match (lexp_whnf e1 ctx, lexp_whnf e2 ctx) with | (SortLevel SLz, e2) -> e2 | (e1, SortLevel SLz) -> e1 | (SortLevel (SLsucc e1), SortLevel (SLsucc e2)) - -> mkSortLevel (SLsucc (mkSLlub meta_ctx ctx e1 e2)) + -> mkSortLevel (SLsucc (mkSLlub ctx e1 e2)) | (e1', e2') - -> let ce1 = level_canon (L.clean meta_ctx e1') in - let ce2 = level_canon (L.clean meta_ctx e2') in + -> let ce1 = level_canon (L.clean e1') in + let ce2 = level_canon (L.clean e2') in if level_leq ce1 ce2 then e1 else if level_leq ce2 ce1 then e2 else mkSortLevel (SLlub (e1, e2)) -let sort_compose meta_ctx ctx l s1 s2 = +let sort_compose ctx l s1 s2 = match s1, s2 with - | (Stype l1, Stype l2) -> Stype (mkSLlub meta_ctx ctx l1 l2) + | (Stype l1, Stype l2) -> Stype (mkSLlub ctx l1 l2) | ( (StypeLevel, Stype _) | (StypeLevel, StypeOmega) (* This is probably safe, but I don't think it adds much power nor @@ -347,19 +351,19 @@ let dbset_push ak erased = if ak = P.Aerasable then DB.set_set 0 nerased else nerased (* "check ctx e" should return τ when "Δ ⊢ e : τ" *) -let rec check' meta_ctx erased ctx e = - let check = check' meta_ctx in +let rec check' erased ctx e = + let check = check' in let assert_type ctx e t t' = - if conv_p meta_ctx ctx t t' then () + if conv_p ctx t t' then () else (U.msg_error "TC" (lexp_location e) ("Type mismatch for " - ^ lexp_string (L.clean meta_ctx e) ^ " : " - ^ lexp_string (L.clean meta_ctx t) ^ " != " - ^ lexp_string (L.clean meta_ctx t')); + ^ lexp_string (L.clean e) ^ " : " + ^ lexp_string (L.clean t) ^ " != " + ^ lexp_string (L.clean t')); (* U.internal_error "Type mismatch" *)) in let check_type erased ctx t = let s = check erased ctx t in - (match lexp_whnf s ctx meta_ctx with + (match lexp_whnf s ctx with | Sort _ -> () | _ -> U.msg_error "TC" (lexp_location t) ("Not a proper type: " ^ lexp_string t)); @@ -432,12 +436,12 @@ let rec check' meta_ctx erased ctx e = * should ignore `k2` and return TypeOmega anyway. *) let k2 = check_type (DB.set_sink 1 erased) nctx t2 in let k2 = mkSusp k2 (S.substitute impossible) in - match lexp_whnf k1 ctx meta_ctx, lexp_whnf k2 ctx meta_ctx with + match lexp_whnf k1 ctx, lexp_whnf k2 ctx with | (Sort (_, s1), Sort (_, s2)) (* FIXME: fix scoping of `k2` and `s2`. *) -> if ak == P.Aerasable && impredicative_erase && s1 != StypeLevel then k2 - else mkSort (l, sort_compose meta_ctx ctx l s1 s2) + else mkSort (l, sort_compose ctx l s1 s2) | (Sort (_, _), _) -> (U.msg_error "TC" (lexp_location t2) "Not a proper type"; mkSort (l, StypeOmega)) @@ -445,7 +449,7 @@ let rec check' meta_ctx erased ctx e = "Not a proper type"; mkSort (l, StypeOmega))) | Lambda (ak, ((l,_) as v), t, e) - -> ((match lexp_whnf (check_type DB.set_empty ctx t) ctx meta_ctx with + -> ((match lexp_whnf (check_type DB.set_empty ctx t) ctx with | Sort _ -> () | _ -> (U.msg_error "TC" (lexp_location t) "Formal arg type is not a type!"; ())); @@ -459,7 +463,7 @@ let rec check' meta_ctx erased ctx e = (fun ft (ak,arg) -> let at = check (if ak = P.Aerasable then DB.set_empty else erased) ctx arg in - match lexp_whnf ft ctx meta_ctx with + match lexp_whnf ft ctx with | Arrow (ak', v, t1, l, t2) -> if not (ak == ak') then (U.msg_error "TC" (lexp_location arg) @@ -484,13 +488,13 @@ let rec check' meta_ctx erased ctx e = (fun (level, ctx) (ak, v, t) -> (* FIXME: DB.set_empty seems wrong! *) (match lexp_whnf (check_type DB.set_empty ctx t) - ctx meta_ctx with + ctx with | Sort (_, Stype _) when ak == P.Aerasable && impredicative_erase -> level | Sort (_, Stype level') (* FIXME: scoping of level vars! *) - -> mkSLlub meta_ctx ctx level level' + -> mkSLlub ctx level level' | tt -> U.msg_error "TC" (lexp_location t) ("Field type " ^ lexp_string t @@ -515,9 +519,9 @@ let rec check' meta_ctx erased ctx e = -> let call_split e = match e with | Call (f, args) -> (f, args) | _ -> (e,[]) in - let etype = lexp_whnf (check erased ctx e) ctx meta_ctx in + let etype = lexp_whnf (check erased ctx e) ctx in let it, aargs = call_split etype in - (match lexp_whnf it ctx meta_ctx, aargs with + (match lexp_whnf it ctx, aargs with | Inductive (_, _, fargs, constructors), aargs -> let rec mksubst s fargs aargs = match fargs, aargs with @@ -569,7 +573,7 @@ let rec check' meta_ctx erased ctx e = | _,_ -> U.msg_error "TC" l "Case on a non-inductive type!"); ret | Cons (t, (l, name)) - -> (match lexp_whnf t ctx meta_ctx with + -> (match lexp_whnf t ctx with | Inductive (l, _, fargs, constructors) -> (try let fieldtypes = SMap.find name constructors in @@ -602,13 +606,14 @@ let rec check' meta_ctx erased ctx e = ^ lexp_string t); DB.type_int)) | Metavar (idx, s, _, t) - -> (try let e = push_susp (L.VMap.find idx meta_ctx) s in + -> (try let meta_ctx, _ = !global_substitution in + let e = push_susp (L.VMap.find idx meta_ctx) s in let t' = check erased ctx e in assert_type ctx e t' t with Not_found -> ()); t -let check meta_ctx = check' meta_ctx DB.set_empty +let check = check' DB.set_empty (** Compute the set of free (meta)variables. **) @@ -708,8 +713,7 @@ let rec fv (e : lexp) : (DB.set * mv_set) = (** Finding the type of a expression. **) (* This should never signal any warning/error. *) -let rec get_type meta_ctx ctx e = - let get_type = get_type meta_ctx in +let rec get_type ctx e = match e with | Imm (Float (_, _)) -> DB.type_float | Imm (Integer (_, _)) -> DB.type_int @@ -734,11 +738,11 @@ let rec get_type meta_ctx ctx e = * should ignore `k2` and return TypeOmega anyway. *) let k2 = get_type nctx t2 in let k2 = mkSusp k2 (S.substitute impossible) in - match lexp_whnf k1 ctx meta_ctx, lexp_whnf k2 ctx meta_ctx with + match lexp_whnf k1 ctx, lexp_whnf k2 ctx with | (Sort (_, s1), Sort (_, s2)) -> if ak == P.Aerasable && impredicative_erase && s1 != StypeLevel then k2 - else mkSort (l, sort_compose meta_ctx ctx l s1 s2) + else mkSort (l, sort_compose ctx l s1 s2) | _ -> DB.type0) | Lambda (ak, ((l,_) as v), t, e) -> (mkArrow (ak, Some v, t, l, @@ -748,7 +752,7 @@ let rec get_type meta_ctx ctx e = -> let ft = get_type ctx f in List.fold_left (fun ft (ak,arg) - -> match lexp_whnf ft ctx meta_ctx with + -> match lexp_whnf ft ctx with | Arrow (ak', v, t1, l, t2) -> mkSusp t2 (S.substitute arg) | _ -> ft) @@ -764,14 +768,13 @@ let rec get_type meta_ctx ctx e = let level, _ = List.fold_left (fun (level, ctx) (ak, v, t) -> - (match lexp_whnf (get_type ctx t) - ctx meta_ctx with + (match lexp_whnf (get_type ctx t) ctx with | Sort (_, Stype _) when ak == P.Aerasable && impredicative_erase -> level | Sort (_, Stype level') (* FIXME: scoping of level vars! *) - -> mkSLlub meta_ctx ctx level level' + -> mkSLlub ctx level level' | tt -> level), DB.lctx_extend ctx v Variable t) (level, ctx) @@ -786,7 +789,7 @@ let rec get_type meta_ctx ctx e = tct | Case (l, e, ret, branches, default) -> ret | Cons (t, (l, name)) - -> (match lexp_whnf t ctx meta_ctx with + -> (match lexp_whnf t ctx with | Inductive (l, _, fargs, constructors) -> (try let fieldtypes = SMap.find name constructors in View it on GitLab: https://gitlab.com/monnier/typer/commit/aaa414b231a5f51452e45b4ea6e8a654601… --- View it on GitLab: https://gitlab.com/monnier/typer/commit/aaa414b231a5f51452e45b4ea6e8a654601… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][master] Force TypeLevel parameters to come first
by Stefan 19 Jul '17

19 Jul '17

Stefan pushed to branch master at Stefan / Typer Commits: ef053aac by Stefan Monnier at 2017-07-19T15:36:46-04:00 Force TypeLevel parameters to come first - - - - - 2 changed files: - doc/manual.texi - src/opslexp.ml Changes: ===================================== doc/manual.texi ===================================== --- a/doc/manual.texi +++ b/doc/manual.texi @@ -210,7 +210,6 @@ A = { TypeLevel : SortL, } R = { (SortL, Type l, Sortω), ∀ l : TypeLevel (SortL, Sortω, Sortω), - (Type l, Sortω, Sortω), ∀ l : TypeLevel (Type l₁, Type l₂, Type (TypeLevel.∪ l₁ l₂)) ∀ l₁,l₂ : TypeLevel } @end example ===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -332,8 +332,11 @@ let sort_compose meta_ctx ctx l s1 s2 = match s1, s2 with | (Stype l1, Stype l2) -> Stype (mkSLlub meta_ctx ctx l1 l2) | ( (StypeLevel, Stype _) - | (StypeLevel, StypeOmega) - | (Stype _, StypeOmega)) + | (StypeLevel, StypeOmega) + (* This is probably safe, but I don't think it adds much power nor + * flexibility, so let's not bother for now: it's easier to add it later + * than to remove it later. + * | (Stype _, StypeOmega) *)) -> StypeOmega | _,_ -> (U.msg_error "TC" l "Mismatch sorts for arg and result"; View it on GitLab: https://gitlab.com/monnier/typer/commit/ef053aac6a6b2ed613342213c5ed8ad1da2… --- View it on GitLab: https://gitlab.com/monnier/typer/commit/ef053aac6a6b2ed613342213c5ed8ad1da2… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][master] Try and document the universe hierarchy
by Stefan 18 Jul '17

18 Jul '17

Stefan pushed to branch master at Stefan / Typer Commits: 49ca7fdb by Stefan Monnier at 2017-07-18T18:09:10-04:00 Try and document the universe hierarchy - - - - - 3 changed files: - doc/manual.texi - src/elab.ml - src/opslexp.ml Changes: ===================================== doc/manual.texi ===================================== --- a/doc/manual.texi +++ b/doc/manual.texi @@ -6,7 +6,7 @@ @copying . -Copyright @copyright{} 2012-2016 Free Software Foundation, Inc. +Copyright @copyright{} 2012-2017 Free Software Foundation, Inc. @quotation Permission is granted to copy, distribute and/or modify this document @@ -195,6 +195,44 @@ type2)}. @c @c Get fdl.texi from http://www.gnu.org/licenses/fdl.html @c @include fdl.texi +@node Universe Hierarchy +@subsection Universe Hierarchy + +The PTS used in Typer looks as follows: + +@example +S = { SortL, Sortω, Type l } ∀ l : TypeLevel +A = { TypeLevel : SortL, + TypeLevel.z : TypeLevel + TypeLevel.s : TypeLevel → TypeLevel, + TypeLevel.∪ : TypeLevel → TypeLevel → TypeLevel. + Type l : Type (TypeLevel.s l), ∀ l : TypeLevel + } +R = { (SortL, Type l, Sortω), ∀ l : TypeLevel + (SortL, Sortω, Sortω), + (Type l, Sortω, Sortω), ∀ l : TypeLevel + (Type l₁, Type l₂, Type (TypeLevel.∪ l₁ l₂)) ∀ l₁,l₂ : TypeLevel + } +@end example + +@c Another way to look at it is: + +@c @example +@c S = { SortType, Sortω } ∪ { s | s : Sort } +@c A = { Sort : SortType, +@c TypeZ : Sort +@c TypeS : Sort → Sort, +@c Type∪ : Sort → Sort → Sort +@c } +@c R = { (Sort, s, Sortω), +@c (Sort, Sortω, Sortω), +@c (s, Sortω, Sortω), +@c (s₁, s₂, Type∪ s₁ s₂) +@c } +@c @end example +@c But now we have the problem that TypeZ has type Sort but Type0 should +@c have type Type1 so we can't have TypeZ = Type0. + @node Index @unnumbered Index ===================================== src/elab.ml ===================================== --- a/src/elab.ml +++ b/src/elab.ml @@ -30,6 +30,11 @@ * Elaborate Sexp expression into Lexp. * This includes type inference, and macro expansion. * + * While elaboration will discover most type errors, strictly speaking + * this phase does not need to perform any checks, and it can instead presume + * that the code is well-behaved. The real type checks (and totality + * checks) are performed later in OL.check. + * * -------------------------------------------------------------------------- *) open Util @@ -493,8 +498,7 @@ and check_inferred ctx e inferred_t t = (* Lexp.case can sometimes be inferred, but we prefer to always check. *) and check_case rtype (loc, target, ppatterns) ctx = - (* FIXME: check if case is exhaustive *) - (* Helpers *) + (* Helpers *) let pat_string p = sexp_string (pexp_u_pat p) in ===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -508,6 +508,7 @@ let rec check' meta_ctx erased ctx e = let tct = arg_loop args ctx in tct | Case (l, e, ret, branches, default) + (* FIXME: Check that the return type isn't TypeLevel. *) -> let call_split e = match e with | Call (f, args) -> (f, args) | _ -> (e,[]) in View it on GitLab: https://gitlab.com/monnier/typer/commit/49ca7fdbd3a79287a905e8201cd792f5fc3… --- View it on GitLab: https://gitlab.com/monnier/typer/commit/49ca7fdbd3a79287a905e8201cd792f5fc3… You're receiving this email because of your account on gitlab.com.

1 0

let-polymorphism generalization
by Stefan Monnier 15 Jul '17

15 Jul '17

I started to look at what let-polymorphism should look like and I have a bit of a problem. Hopefully someone here can give me some ideas or at least opinions. *** Case 1 (easy): we want to be able to write map f xs = case xs | nil => [] | cons x xs => cons (f x) (map f xs); and that should work fairly easily: after inference we get 2 uninstantiated metavars so we add the corresponding 2 lambdas around the whole definition and we're done. *** Case 2 (easy): map : (?a -> ?b) -> List ?a -> List ?b; Here, similarly, the ?a and ?b metavars are left uninstantiated, so we can add the corresponding 2 pis around the type and we're done. *** Case 3: We could also allow map : (a -> b) -> List a -> List b; and automatically treat a reference to an non-existing variable (in a type annotation) as a metavar. *** Case 4: now comes the tricky part. what about case 1 combined with a type annotation? map : (a : Type) ≡> (b : Type) ≡> (a -> b) -> List a -> List b; map f xs = case xs | nil => [] | cons x xs => cons (f x) (map f xs); [ Of course, the type annotation could be shortened as in case 2 and case 3 without making much difference to the situation. ] Option 1: We could do it by treating the map definition as in case 1 and then checking that the inferred type matches the annotation, but: - in general this will fail because the two types may be "equivalent" yet different (e.g. the order of a and b may be reversed). - it means that we elaborate the definition of `map` without taking much advantage of the type annotation. It would allow polymorphic recursion, but while elaborating map, we wouldn't yet know that there are args `a` and `b` in the environment. In the present case, this probably doesn't matter much, but for type-class arguments this could be more annoying. Option 2: we could instead automatically wrap the definition of map into 2 erasable lambdas based on the type annotation. This is more natural from a "bidirectional type checking" point of view, takes full advantage of the type annotation, and doesn't suffer from having to later check the type we inferred (with the risk that we didn't infer "quite right"). *** Case 5: sinking deeper. Now, what about map : (a : Type) ≡> (b : Type) ≡> (a -> b) -> List a -> List b; map = lambda a ≡> lambda b ≡> lambda f -> lambda xs -> case xs | nil => [] | cons x xs => cons (f x) (map f xs); This is currently the code we accept, and I think it'd be good to still accept it, but if we go with option 2 in case 4, what should we do here? Before we even look at the "lambda a ≡> lam..." code, we'd end up adding two lambdas around the whole thing, but these would be extraneous here. We could try to arrange so that the "automatic instantiation" (which adds implict args wherever we think they're needed) could save us, by basically auto-rewriting the above as: map : (a : Type) ≡> (b : Type) ≡> (a -> b) -> List a -> List b; map = (lambda a ≡> lambda b ≡> lambda f -> lambda xs -> case xs | nil => [] | cons x xs => cons (f x) (map f xs)) (a := a) (b := b)) but it feels brittle, and seems wrong: why uselessly add lambdas and then matching applications, when the code came already "written in full"? [ Side note: notice how in the definition above, we use `a` and `b` which look like free variables but are really bound by the auto-added lambdas. ] One could think: only auto-add the lambdas if the body doesn't already start with such lambdas, but the thing is that the lambdas need to be added before we elaborate the definition (because the lambdas influence the ctx in which the elaboration takes place), so we can't really look at the definition to make a decision: for all we know, the definition has at its top-level a macro-call which needs to look at the ctx to decide what to do. I think maybe a good solution is to try and provide two forms of `=` definitions: a basic one that doesn't do any magic, and another one that auto-adds erasable lambdas based on provided type annotations. Hopefully the fancier one can be defined as a declaration-macro. Still, this "auto-adding lambdas" is pretty intrusive. It means that definitions with a type annotations are handled very differently than those without. And that the type annotation already provides part of the definition. Another problem is that this only works for "prefix args". If you consider the definition of K: K : (a : Type) ≡> a -> (b : Type) ≡> b -> a; K = ... only the `a` argument can be easily auto-added as part of the declaration. To auto-add the `b` argument, we'd need to auto-add lambdas not just around definitions, but around arbitrary expressions: this wouldn't be just let-bound generalization any more but it would require some generic "add implicit lambdas wherever needed". We know from MLF and other type-inference systems that such things can be done in some cases, but - it's tricky - it's usually based on comparing the expression's inferred type with what the context expects, but that means the lambda can only be added after the fact (i.e. this corresponds again to option 1 rather than option 2). This becomes even more problematic for implicit args (rather than merely erasable args): erasable args typically correspond to System-F style polymorphism and can be usually fully inferred and to a large extent they don't matter, but implicit args are real arguments (think type-class dictionaries) so they have an impact on performance, which means that we don't want to risk adding spurious "lambdas + corresponding calls" since they may not always turn out to be easily optimizable via eta-reduction. Maybe the best option is to only do the auto-add-lambdas for the case where the definition is of the form "f <args> = <exp>" and in that case we can even auto-add intermediate implicit/erasable args, so we could accept: K : (a : Type) ≡> a -> (b : Type) ≡> b -> a; K x y = x; Hmm... Stefan

2 6

[Git][monnier/typer][master] * src/elab.ml (lexp_decls_1): Accept multiple decls for the same var
by Stefan 12 Jul '17

12 Jul '17

Stefan pushed to branch master at Stefan / Typer Commits: 31ee7094 by Stefan Monnier at 2017-07-12T00:07:13-04:00 * src/elab.ml (lexp_decls_1): Accept multiple decls for the same var - - - - - 3 changed files: - btl/builtins.typer - btl/pervasive.typer - src/elab.ml Changes: ===================================== btl/builtins.typer ===================================== --- a/btl/builtins.typer +++ b/btl/builtins.typer @@ -115,6 +115,10 @@ Sexp_eq = Built-in "Sexp.=" (Sexp -> Sexp -> Bool); %% List %% ----------------------------------------------------- +%% FIXME: "List : ?" should be sufficient but triggers +%% [!] Error ELAB `(List[2] a[1]) : ?ta · Id[18]` is not a proper type +%% > Call: (List[2] a[1]) +%% "Subst-inversion-bug: <anon> · (↑2 () · () · () · Id) ∘ <anon0> · () · (↑4 Id) == <anon> · () · (↑2 Id) !!" List : Type -> Type; %% List a = typecons List (nil) (cons a (List a)); %% nil = lambda a ≡> datacons (List a) nil; ===================================== btl/pervasive.typer ===================================== --- a/btl/pervasive.typer +++ b/btl/pervasive.typer @@ -327,9 +327,10 @@ Decidable = typecons (Decidable (prop : Type)) test1 : Option Int; test2 : Option Int; test3 : Option Int; -test4 : Option Int; test1 = test2; +test4 : Option ?; test2 = none; +test4 : Option Int; test4 = test1; test3 = test4; ===================================== src/elab.ml ===================================== --- a/src/elab.ml +++ b/src/elab.ml @@ -385,6 +385,9 @@ and infer_type pexp ectx var = (let meta_ctx, _ = !global_substitution in match OL.lexp_whnf s (ectx_to_lctx ectx) meta_ctx with | Sort (_, _) -> () (* All clear! *) + (* FIXME: We could automatically coerce Type levels to Sorts, so we + * could write `(a : TypeLevel) -> a -> a` instead of + * `(a : TypeLevel) -> Type_ a -> Type_ a` *) | _ -> (* FIXME: Here we rule out TypeLevel/TypeOmega. *) match Unif.unify (mkSort (lexp_location s, Stype (newMetalevel ()))) s @@ -885,8 +888,21 @@ and lexp_decls_1 -> let ltp = infer_type stp (ectx_new_scope nctx) (Some v) in if SMap.mem vname pending_decls then (* Don't burp: take'em all and unify! *) - (error l ("Variable `" ^ vname ^ "` declared twice!"); - lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) + let pt_idx = senv_lookup vname nctx in + (* Take the previous type annotation. *) + let pt = match Myers.nth pt_idx (ectx_to_lctx nctx) with + | (_, _, ForwardRef, t) -> push_susp t (S.shift (pt_idx + 1)) + | _ -> U.internal_error "Var not found at its index!" in + (* Unify it with the new one. *) + let meta_ctx, _ = !global_substitution in + let _ = match Unif.unify ltp pt (ectx_to_lctx nctx) meta_ctx with + | (None | Some (_, _::_)) + -> lexp_error l ltp + ("New type annotation `" + ^ lexp_string ltp ^ "` incompatible with previous `" + ^ lexp_string pt ^ "`") + | Some subst -> global_substitution := subst in + lexp_decls_1 sdecls ectx nctx pending_decls pending_defs else if List.exists (fun ((_, vname'), _) -> vname = vname') pending_defs then (error l ("Variable `" ^ vname ^ "` already defined!"); View it on GitLab: https://gitlab.com/monnier/typer/commit/31ee70949f6176f17872d8b1ce2cb044b13… --- View it on GitLab: https://gitlab.com/monnier/typer/commit/31ee70949f6176f17872d8b1ce2cb044b13… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][master] 2 commits: * src/elab.ml (lexp_check_decls): Drop unused `ltype` from `defs`
by Stefan 07 Jul '17

07 Jul '17

Stefan pushed to branch master at Stefan / Typer Commits: 09e86649 by Stefan Monnier at 2017-07-07T22:38:37-04:00 * src/elab.ml (lexp_check_decls): Drop unused `ltype` from `defs` (lexp_decls_1): Drop corresponding info from pending_defs and pending_decls. - - - - - 17f4f72a by Stefan Monnier at 2017-07-07T22:39:25-04:00 * btl/pervasive.typer: Move some defs to benefit from multiarg λ - - - - - 3 changed files: - btl/pervasive.typer - src/elab.ml - src/sexp.ml Changes: ===================================== btl/pervasive.typer ===================================== --- a/btl/pervasive.typer +++ b/btl/pervasive.typer @@ -36,14 +36,6 @@ Option = typecons (Option (a : Type)) (none) (some a); some = datacons Option some; none = datacons Option none; -%%% Good 'ol combinators - -I : (a : Type) ≡> a -> a; -I x = x; - -K : (a : Type) ≡> a -> (b : Type) ≡> b -> a; -K x = lambda y -> x; - %%%% List functions List_length : (a : Type) ≡> List a -> Int; @@ -52,14 +44,6 @@ List_length xs = case xs | cons hd tl => (1 + (List_length tl)); -List_reverse : (a : Type) ≡> List a -> List a -> List a; -List_reverse l = lambda t -> case l - | nil => t - | cons hd tl => List_reverse tl (cons hd t); - -List_concat : (a : Type) ≡> List a -> List a -> List a; -List_concat l = lambda t -> List_reverse (List_reverse l nil) t; - %% ML's typical `head` function is not total, so can't be defined %% as-is in Typer. There are several workarounds: %% - Provide a default value : (a : Type) ≡> a -> List a -> a; @@ -85,11 +69,6 @@ List_map f = lambda xs -> case xs | nil => nil | cons x xs => cons (f x) (List_map f xs); -List_foldl : (a : Type) ≡> (b : Type) ≡> (a -> b -> a) -> a -> List b -> a; -List_foldl f = lambda i -> lambda xs -> case xs - | nil => i - | cons x xs => List_foldl f (f i x) xs; - List_foldr : (a : Type) ≡> (b : Type) ≡> (b -> a -> a) -> List b -> a -> a; List_foldr f = lambda xs -> lambda i -> case xs | nil => i @@ -100,7 +79,7 @@ List_find f = lambda xs -> case xs | nil => none | cons x xs => case f x | true => some x | false => List_find f xs; -%%%% A more flexible `lambda`. +%%%% A more flexible `lambda` %% An Sexp which we use to represents an error. Sexp_error = Sexp_symbol "<error>"; @@ -121,34 +100,11 @@ Sexp_to_list s = lambda exceptions -> singleton singleton singleton singleton; multiarg_lambda = - %% let bodytail = cons body nil; - %% mklam = lambda (a : Type) ≡> lambda (_ : a) - %% -> Sexp_node (Sexp_symbol "##lambda_->_") - %% (cons arg bodytail) in - %% Sexp_dispatch - %% arg - %% (node := (lambda head -> lambda tail -> - %% Sexp_dispatch - %% head - %% (symbol := (lambda s -> case String_eq s "_:_" - %% | true -> mklam () - %% | false -> case String_eq s "_::_" - %% | true - %% -> Sexp_node (Sexp_symbol "##lambda_=>_") - %% (cons (Sexp_node - %% (Sexp_symbol "_:_") - %% tail) - %% bodytail) - %% | false -> case String_eq s "_:::_" - %% | true - %% -> Sexp_node (Sexp_symbol "##lambda_≡>_") - %% (cons (Sexp_node - %% (Sexp_symbol "_:_") - %% tail) - %% bodytail) - %% | false -> mklam ())) - %% mklam mklam mklam mklam mklam)) - %% mklam mklam mklam mklam mklam + %% This macro lets `lambda_->_` (and siblings) accept multiplke arguments. + %% TODO: We could additionally turn + %% `lambda (x :: t) y -> e` into `lambda (x : t) => lambda y -> e` + %% thus providing an alternate syntax for lambdas which doesn't use + %% => and ≡>. let exceptions = List_map Sexp_symbol (cons "_:_" (cons "_::_" (cons "_:::_" nil))) in lambda name -> @@ -171,6 +127,29 @@ lambda_->_ = macro (multiarg_lambda "##lambda_->_"); lambda_=>_ = macro (multiarg_lambda "##lambda_=>_"); lambda_≡>_ = macro (multiarg_lambda "##lambda_≡>_"); +%%%% More list functions + +List_reverse : (a : Type) ≡> List a -> List a -> List a; +List_reverse l t = case l + | nil => t + | cons hd tl => List_reverse tl (cons hd t); + +List_concat : (a : Type) ≡> List a -> List a -> List a; +List_concat l t = List_reverse (List_reverse l nil) t; + +List_foldl : (a : Type) ≡> (b : Type) ≡> (a -> b -> a) -> a -> List b -> a; +List_foldl f i xs = case xs + | nil => i + | cons x xs => List_foldl f (f i x) xs; + +%%% Good 'ol combinators + +I : (a : Type) ≡> a -> a; +I x = x; + +K : (a : Type) ≡> a -> (b : Type) ≡> b -> a; +K x y = x; + %%%% Quasi-Quote macro %% f = (quote (uquote x) * x) (node _*_ [(Sexp_node unquote "x") "x"]) @@ -344,4 +323,15 @@ Decidable = typecons (Decidable (prop : Type)) (true (p ::: prop)) (false (p ::: Not prop)); +%%%% Test +test1 : Option Int; +test2 : Option Int; +test3 : Option Int; +test4 : Option Int; +test1 = test2; +test2 = none; +test4 = test1; +test3 = test4; + + %%% pervasive.typer ends here. ===================================== src/elab.ml ===================================== --- a/src/elab.ml +++ b/src/elab.ml @@ -621,7 +621,7 @@ and check_case rtype (loc, target, ppatterns) ctx = let lexp = check pexp rtype' nctx in SMap.add cons_name (loc, fargs, lexp) lbranches, dflt - (* FIXME: is `ct` is Special-Form or Macro, pass pargs to it + (* FIXME: If `ct` is Special-Form or Macro, pass pargs to it * and try again with the result. *) | _ -> lexp_error loc lctor "Not a constructor"; lbranches, dflt in @@ -817,7 +817,7 @@ and lexp_expand_macro loc macro_funct sargs ctx (ot : ltype option) (* Print each generated decls *) and sexp_decls_macro_print sxp_decls = match sxp_decls with - | Node(Symbol (_, "_;_"), decls) -> + | Node (Symbol (_, "_;_"), decls) -> List.iter (fun sxp -> sexp_decls_macro_print sxp) decls | e -> sexp_print e; print_string "\n" @@ -835,20 +835,19 @@ and lexp_decls_macro (loc, mname) sargs ctx: sexp = and lexp_check_decls (ectx : elab_context) (* External context. *) (nctx : elab_context) (* Context with type declarations. *) - (defs : (vname * sexp * ltype) list) + (defs : (vname * sexp) list) : (vname * lexp * ltype) list * elab_context = let (declmap, nctx) = List.fold_right - (fun ((_, vname) as v, pexp, ltp) (map, nctx) -> + (fun ((_, vname) as v, pexp) (map, nctx) -> let i = senv_lookup vname nctx in assert (i < List.length defs); match Myers.nth i (ectx_to_lctx nctx) with | (o, v', ForwardRef, t) - -> let adjusted_ltp = push_susp ltp (S.shift (i + 1)) in - assert (t == ltp); - let e = check pexp adjusted_ltp nctx in + -> 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, ltp) map, + (IntMap.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 @@ -860,13 +859,13 @@ and lexp_decls_1 (sdecls : sexp list) (ectx : elab_context) (* External ctx. *) (nctx : elab_context) (* New context. *) - (pending_decls : (location * ltype) SMap.t) (* Pending type decls. *) - (pending_defs : (vname * sexp * ltype) list) (* Pending definitions. *) + (pending_decls : location SMap.t) (* Pending type decls. *) + (pending_defs : (vname * sexp) list) (* Pending definitions. *) : (vname * lexp * ltype) list * sexp list * elab_context = match sdecls with | [] -> (if not (SMap.is_empty pending_decls) then - let (s, (l, _)) = SMap.choose pending_decls in + let (s, l) = SMap.choose pending_decls in error l ("Variable `" ^ s ^ "` declared but not defined!") else assert (pending_defs == [])); @@ -885,15 +884,16 @@ and lexp_decls_1 | [Symbol ((l, vname) as v); stp] -> let ltp = infer_type stp (ectx_new_scope nctx) (Some v) in if SMap.mem vname pending_decls then + (* Don't burp: take'em all and unify! *) (error l ("Variable `" ^ vname ^ "` declared twice!"); lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) - else if List.exists (fun ((_, vname'), _, _) -> vname = vname') + else if List.exists (fun ((_, vname'), _) -> vname = vname') pending_defs then (error l ("Variable `" ^ vname ^ "` already defined!"); lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) else lexp_decls_1 sdecls ectx (env_extend nctx v ForwardRef ltp) - (SMap.add vname (l, ltp) pending_decls) + (SMap.add vname l pending_decls) pending_defs | _ -> error l "Invalid type declaration syntax"; lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) @@ -912,18 +912,18 @@ and lexp_decls_1 ctx_define nctx v lexp ltp | [Symbol ((l, vname) as v); sexp] - -> (try let (_, ltp) = SMap.find vname pending_decls in - let pending_decls = SMap.remove vname pending_decls in - let pending_defs = ((v, sexp, ltp) :: pending_defs) in - if SMap.is_empty pending_decls then - let nctx = ectx_new_scope nctx in - let decls, nctx = lexp_check_decls ectx nctx pending_defs in - decls, sdecls, nctx - else - lexp_decls_1 sdecls ectx nctx pending_decls pending_defs - - with Not_found -> - error l ("`" ^ vname ^ "` defined but not declared!"); + -> if SMap.mem vname pending_decls then + let pending_decls = SMap.remove vname pending_decls in + let pending_defs = ((v, sexp) :: pending_defs) in + if SMap.is_empty pending_decls then + let nctx = ectx_new_scope nctx in + let decls, nctx = lexp_check_decls ectx nctx pending_defs in + decls, sdecls, nctx + else + lexp_decls_1 sdecls ectx nctx pending_decls pending_defs + + else + (error l ("`" ^ vname ^ "` defined but not declared!"); lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) | [Node (Symbol s, args) as d; body] ===================================== src/sexp.ml ===================================== --- a/src/sexp.ml +++ b/src/sexp.ml @@ -20,15 +20,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/TODO: - * - Give more control over the way we strip parentheses. - * E.g. allow some infix operators to keep track whether their args where - * parenthesized or not. Some uses may also want to "not-strip" parentheses - * so as to distinguish "((a b))" from "(a b)". - * - Add another level of tokenizing/parsing: on the first level "M.a" - * can be parsed as one token, and then on the second level, it would - * turn into a call to "." with two arguments. *) - open Util open Prelexer open Grammar View it on GitLab: https://gitlab.com/monnier/typer/compare/fc6835a1c317e3bca4048fc19ee1525744… --- View it on GitLab: https://gitlab.com/monnier/typer/compare/fc6835a1c317e3bca4048fc19ee1525744… You're receiving this email because of your account on gitlab.com.

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

Typer Juillet 2017