Stefan pushed to branch unification at Stefan / Typer

Commits: 876a022d by Stefan Monnier at 2016-11-04T13:24:13-04:00 Fix conv_p to unfold variable's definitions

* src/lexp.ml (hc_table, hc): Hash_consing function for lexp. (mkImm, mkSortLevel, mkSort, mkBuiltin, mkVar, mkLet, mkArrow) (mkLambda, mkCall, mkInductive, mkCons, mkCase): New "smart constructor" functions, which perform hash-consing. Use them everywhere. (mkSusp): Make it hash-consing.

* src/lparse.ml (elab_check_def): Do call conv_p now. (lexp_case): Adjust call to conv_p. (lexp_call): Don't bother calling lexp_whnf before conv_p any more.

* src/opslexp.ml (lexp_whnf): Move before conv_p. <Call>: Return e itself instead of reconstructing the same lexp node. <Let>: Handle it. (set_lexp): New type. (set_empty, set_member_p, set_add, set_shift): New functions. (conv_p, conv_p'): Rewrite.

* src/debruijn.ml (env_elem): Use Util.db_offset. (db_idx): Remove, unused.

- - - - - f762ac7e by Stefan Monnier at 2016-11-04T14:29:10-04:00 Merge branch 'trunk' into unification

- - - - -

6 changed files:

- DESIGN - src/debruijn.ml - src/lexp.ml - src/lparse.ml - src/myers.ml - src/opslexp.ml

Changes:

===================================== DESIGN ===================================== --- a/DESIGN +++ b/DESIGN @@ -444,7 +444,21 @@ datatypes where one of the elements can be meaningfully treated as the "false"/"null" value (e.g. the empty list, the "none" of the option type, ...).

-* K axiom +* Equality + +** Heterogenous equality + +*** One suggestion from Agda list ("telescopic equlity"): + + [_]_≅_ : ∀ {X : Set} {x y} → (Z : X → Set) → Z x → Z y → Set + [_]_≅_ {x = x} {y} Z a b = (x , a) ≡ (y , b) + +*** Definition in Agda + + data _≅_ {i} {A : Set i} (x : A) : {B : Set i} → B → Set i where + refl : x ≅ x + +** K axiom

[ See article by Jesper Cockx et al. http://dl.acm.org/citation.cfm?id=2628139&CFID=459245005&CFTOKEN=469... ]

===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -43,6 +43,38 @@ module S = Subst let error l m = msg_error "DEBRUIJN" l m; internal_error m let warning = msg_warning "DEBRUIJN"

+(* Handling scoping/bindings is always tricky. So it's always important + * to keep in mind for *every* expression which is its context. + * + * In particular, this holds true as well for those expressions that appear + * in the context. Traditionally for dependently typed languages we expect + * the context's rules to say something like: + * + * ⊢ Γ Γ ⊢ τ:Type + * ————————————————— + * ⊢ Γ,x:τ + * + * Which means that we expect (τ) expressions in the context to be typed + * within the *rest* of that context. + * + * This also means that when we look up a binding in the context, we need to + * adjust the result, since we need to use it in the context where we looked + * it up, which is different from the context where it was defined. + * + * More concretely, this means that lookup(Γ, i) should return an expression + * where debruijn indices have been shifted by "i". + * + * This is nice for "normal bindings", but there's a complication in the + * case of recursive definitions. Typically, this is handled by using + * something like a μx.e construct, which works OK for the theory but tends + * to become rather inconvenient in practice for mutually recursive + * definitions. So instead, we annotate the recursive binding with + * a "recursion_offset" (of type `db_offset`) to say that rather than being + * defined in "the rest of the context", they're defined in a slightly larger + * context that includes "younger" bindings. + *) + + (* Type definitions * ---------------------------------- *)

@@ -59,10 +91,9 @@ type property_elem = lexp PropertyMap.t type property_env = property_elem PropertyMap.t

(* easier to debug with type annotations *) -type env_elem = (int * vdef option * varbind * ltype) +type env_elem = (db_offset * vdef option * varbind * ltype) type lexp_context = env_elem M.myers

-type db_idx = int (* DeBruijn index. *) type db_ridx = int (* DeBruijn reverse index (i.e. counting from the root). *)

(* Map matching variable name and its distance in the current scope *)

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -112,7 +112,6 @@ type ltype = lexp | SLz | SLsucc of lexp

- type varbind = | Variable | ForwardRef @@ -125,6 +124,29 @@ let empty_subst = (VMap.empty)

let builtin_size = ref 0

+(********************** Hash-consing **********************) + +(* FIXME: We'd want this hash-table to be weak in its values: as soon + * as one of its values can be GC'd, the entry should be removed. *) +let hc_table : (lexp, lexp) Hashtbl.t = Hashtbl.create 1000 +let hc (e : lexp) : lexp = + try Hashtbl.find hc_table e + with Not_found -> Hashtbl.add hc_table e e; + e +let mkImm s = hc (Imm s) +let mkSortLevel l = hc (SortLevel l) +let mkSort (l, s) = hc (Sort (l, s)) +let mkBuiltin (v, t) = hc (Builtin (v, t)) +let mkVar v = hc (Var v) +let mkLet (l, ds, e) = hc (Let (l, ds, e)) +let mkArrow (k, v, t1, l, t2) = hc (Arrow (k, v, t1, l, t2)) +let mkLambda (k, v, t, e) = hc (Lambda (k, v, t, e)) +let mkCall (f, es) = hc (Call (f, es)) +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)) + (********* Helper functions to use the Subst operations *********) (* This basically "ties the knot" between Subst and Lexp. * Maybe it would be cleaner to just move subst.ml into lexp.ml @@ -138,142 +160,15 @@ let rec mkSusp e s = match e with | Susp (e, s') -> mkSusp e (scompose s' s) | Var (l,v) -> slookup s l v - | Metavar (vn, s', vd, t) -> Metavar (vn, scompose s' s, vd, mkSusp t s) - | _ -> Susp (e, s) + | Metavar (vn, s', vd, t) -> mkMetavar (vn, scompose s' s, vd, mkSusp t s) + | _ -> hc (Susp (e, s)) and scompose s1 s2 = S.compose mkSusp s1 s2 -and slookup s l v = S.lookup (fun l i -> Var (l, i)) +and slookup s l v = S.lookup (fun l i -> mkVar (l, i)) (fun e o -> mkSusp e (S.shift o)) s l v -let ssink = S.sink (fun l i -> Var (l, i)) +let ssink = S.sink (fun l i -> mkVar (l, i))

-(**** The builtin elements ****) -(* -let builtins = - (* let l = dloc in *) - [ (* (0,"%type1%", Some (type1), Lsort (l, 2)) *) - ("Type", Some (type0), type1) - ; ("Type@", Some (let lv = (dloc, "ℓ") in - Lambda (Aexplicit, lv, type_level, - Sort (dloc, Stype (Var (lv, 0))))), - let lv = (dloc, "ℓ") in - Arrow (Aexplicit, Some lv, type_level, dloc, - Sort (dloc, Stype (SortLevel (SLsucc (Var (lv,0))))))) - (* ;(var_macro, "%Macro%", None, type0) *) - ] @ - List.map (fun bi -> match bi with - | Builtin (_, name, t) -> (name, Some bi, t) - | _ -> U.internal_error "Registering a non-builtin") - [type_level; type_int; type_float; type_eq] -(* let var_bottom = Var (dloc, -1) *) - - * let (senv_builtin,venv_builtin) - * = List.fold_left (fun (senv,venv) (name,e,t) -> - * let v = name in - * (SMap.add name v senv, - * VMap.add v (e, t) venv)) - * (SMap.empty, VMap.empty) - * builtins *) - -(* Handling scoping/bindings is always tricky. So it's always important - * to keep in mind for *every* expression which is its context. - * - * In particular, this holds true as well for those expressions that appear - * in the context. Traditionally for dependently typed languages we expect - * the context's rules to say something like: - * - * ⊢ Γ Γ ⊢ τ:Type - * ————————————————— - * ⊢ Γ,x:τ - * - * Which means that we expect (τ) expressions in the context to be typed - * within the *rest* of that context. - * - * This also means that when we look up a binding in the context, we need to - * adjust the result, since we need to use it in the context where we looked - * it up, which is different from the context where it was defined. - * - * More concretely, this means that lookup(Γ, i) should return an expression - * where debruijn indices have been shifted by "i". - * - * This is nice for "normal bindings", but there's a complication in the - * case of recursive definitions. Typically, this is handled by using - * something like a μx.e construct, which works OK for the theory but tends - * to become rather inconvenient in practice for mutually recursive - * definitions. So instead, we annotate the recursive binding with - * a "recursion_offset" to say that rather than being defined in "the rest - * of the context", they're defined in a slightly larger context that - * includes "younger" bindings. - *) - - -(***** SMap fold2 helper *****) - -let smap_fold2 c f m1 m2 init - = let chunks = SMap.merge f m1 m2 in - SMap.fold (fun _ x y -> c x y) chunks init - -(** Elaboration. **) - -(* let mk_meta2 sl venv l - * = let mk = MetaGraft VMap.empty in - * let t = Metavar ((l, "_"), mk, ref (MetaUnset (venv, None, sl))) - * in (Metavar ((l, "_"), mk, ref (MetaUnset (venv, Some t, sl))), t) - * let mk_meta sl venv l - * = let mk = MetaGraft VMap.empty in - * let t = Metavar ((l, "_"), mk, ref (MetaUnset (venv, None, sl))) - * in Metavar ((l, "_"), mk, ref (MetaUnset (venv, Some t, sl))) - * let mk_meta_dummy = mk_meta (ScopeLevel(-1)) - * let mk_metat sl venv l t - * = let mk = MetaGraft VMap.empty in - * Metavar ((l, "_"), mk, ref (MetaUnset (venv, Some t, sl))) *) -type value = lexp - -(* Free vars (with type) we need to generalize. *) -(* type fvars = lexp SMap.t *) -(* Each element of a unification constraint is a pair of expresions that - * need to be unified together with a boolean indicating whether this might be - * algorithmically unifiable. I.e. if the boolean is false, then there's no - * point calling lexp_unify on it because we know it will just re-add the same - * constraint. *) -(* type unify_cond = - * | UnifyNever (* Can't be resolved by unification. *) - * | UnifyWhenInst of metavar ref (* Needs ref to be instantiated. *) - * | UnifyMaybe (* Not clear when. *) - * type unify_csts = (lexp * lexp * unify_cond) list - * type constraints = unify_csts - * - * type pending = constraints *) -let id x = x - -(* Combine two substitutions. I.e. e = s(s'(e))). *) -(* let lexp_subst_subst s s' = - * let s' = VMap.map (fun e -> mk_susp s e) s' in - * VMap.fold (fun v e s -> if VMap.mem v s - * then (U.internal_error "Overlapping substs") - * else VMap.add v e s) - * s s' *) - -let lexp_max_sort (k1, k2) = - match k1,k2 with - | Sort (_,l1), Sort (_, l2) -> max l1 l2 - | _ -> U.internal_error "finding the max of non-sorts!" - -(* Invert a substitution. I.e. return s' such that s'(s(e))=e. - * It is allowed to presume that e is closed in `venv'. *) -(* exception Lexp_subst_inv - * let lexp_subst_inv venv s = - * VMap.fold (fun v e s -> - * try let _ = VMap.find v venv in - * match e with - * (* | Var _ when e = var_bottom -> s *) - * | Var (l,v') -> if VMap.mem v' s then raise Lexp_subst_inv - * else VMap.add v' (Var (l,v)) s - * | _ -> raise Lexp_subst_inv - * (* `v' is not in `venv' so it won't appear in `e'. *) - * with Not_found -> s) - * s VMap.empty *) - let rec lexp_location e = match e with | Sort (l,_) -> l @@ -303,7 +198,7 @@ let rec push_susp e s = (* Push a suspension one level down. *) match e with | Imm _ -> e | SortLevel _ -> e - | Sort (l, Stype e) -> Sort (l, Stype (mkSusp e s)) + | Sort (l, Stype e) -> mkSort (l, Stype (mkSusp e s)) | Sort (l, _) -> e | Builtin _ -> e | Let (l, defs, e) @@ -314,10 +209,10 @@ let rec push_susp e s = (* Push a suspension one level down. *) (s, []) defs in Let (l, ndefs, mkSusp e s') | Arrow (ak, v, t1, l, t2) - -> Arrow (ak, v, mkSusp t1 s, l, mkSusp t2 (ssink (maybev v) s)) - | Lambda (ak, v, t, e) -> Lambda (ak, v, mkSusp t s, mkSusp e (ssink v s)) - | Call (f, args) -> Call (mkSusp f s, - L.map (fun (ak, arg) -> (ak, mkSusp arg s)) args) + -> mkArrow (ak, v, mkSusp t1 s, l, mkSusp t2 (ssink (maybev v) s)) + | Lambda (ak, v, t, e) -> mkLambda (ak, v, mkSusp t s, mkSusp e (ssink v s)) + | Call (f, args) -> mkCall (mkSusp f s, + L.map (fun (ak, arg) -> (ak, mkSusp arg s)) args) | Inductive (l, label, args, cases) -> let (s, nargs) = L.fold_left (fun (s, nargs) (ak, v, t) -> (ssink v s, (ak, v, mkSusp t s) :: nargs)) @@ -331,21 +226,21 @@ let rec push_susp e s = (* Push a suspension one level down. *) (s, []) args in L.rev ncase) cases in - Inductive (l, label, nargs, ncases) + mkInductive (l, label, nargs, ncases) | Cons (it, name) -> Cons (mkSusp it s, name) | Case (l, e, ret, cases, default) - -> Case (l, mkSusp e s, mkSusp ret s, - SMap.map (fun (l, cargs, e) - -> let s' = L.fold_left (fun s carg - -> match carg with - | (_,None) -> s - | (_,Some v) -> ssink v s) - s cargs in - (l, cargs, mkSusp e s')) - cases, - match default with - | None -> default - | Some (v,e) -> Some (v, mkSusp e (ssink (maybev v) s))) + -> mkCase (l, mkSusp e s, mkSusp ret s, + SMap.map (fun (l, cargs, e) + -> let s' = L.fold_left (fun s carg + -> match carg with + | (_,None) -> s + | (_,Some v) -> ssink v s) + s cargs in + (l, cargs, mkSusp e s')) + cases, + match default with + | None -> default + | Some (v,e) -> Some (v, mkSusp e (ssink (maybev v) s))) (* Susp should never appear around Var/Susp/Metavar because mkSusp * pushes the subst into them eagerly. IOW if there's a Susp(Var..) * or Susp(Metavar..) it's because some chunk of code should use mkSusp @@ -442,82 +337,6 @@ and lexp_unparse e : pexp =

let lexp_print e = sexp_print (pexp_unparse (lexp_unparse e))

-(* let rec lexp_type (env: (lexp option * lexp) VMap.t) e : lexp = - * let rec follow e = - * match e with - * | Var (_,v) -> vmap_getval v - * | Metavar (_,_,r) -> (match !r with MetaSet e -> follow e | _ -> e) - * | _ -> e - * and vmap_getval (v : var) = - * match VMap.find v env with (Some e, _) -> follow e - * | _ -> Var (U.dummy_location, v) in - * match e with - * | Sort (l, Stype e) -> Sort (l, Stype (SortLevel (SLsucc e))) - * | Sort (l, StypeOmega) - * -> msg_error l "TypeΩ doesn't have a type"; mk_meta_dummy env l - * | Sort (l, StypeLevel) - * -> msg_error l "TypeLevel doesn't have a type"; mk_meta_dummy env l - * | SortLevel _ -> Sort (lexp_location e, StypeLevel) - * | Imm (Integer _) -> type_int - * | Imm (Float _) -> type_float - * | Builtin (_,_,t) -> t - * (* | Imm (String _) -> Var (U.dummy_location, var_string) *) - * | Imm s -> let l = sexp_location s in - * msg_error l "Unrecognized sexp in lexp"; mk_meta_dummy env l - * | Var (_,name) -> snd (VMap.find name env) - * | Let (l, decls, body) -> - * lexp_type (List.fold_left (fun env ((_,v),e,t) -> - * VMap.add v (Some (Let (l, decls, e)), t) env) - * env decls) - * body - * | Arrow _ -> type0 (* FIXME! *) - * | Lambda (ak, ((l,v) as var),t,e) -> - * Arrow (ak, Some var, t, U.dummy_location, - * lexp_type (VMap.add v (None, t) env) e) - * | Call (f, args) -> - * let ft = lexp_type env f in - * let rec one_arg t (_,arg) = - * match lexp_whnf VMap.empty t with - * | Arrow (_, None, t1, _, t2) -> t2 - * | Arrow (_, Some (_,v), t1, _, t2) -> - * Susp (VMap.add v arg VMap.empty, t2) - * | _ -> msg_error (lexp_location arg) "Too many arguments"; t - * in List.fold_left one_arg ft args - * | Inductive (_,t,_) -> t - * | Cons (e,(l,name)) -> - * (match lexp_whnf VMap.empty e with - * | Inductive (_,_,branches) -> - * (try SMap.find name branches - * with Not_found -> msg_error l ("No such constructor name `"^name^"'"); - * mk_meta_dummy env l) - * | _ -> msg_error l "The constructor refers to a non-inductive type"; - * mk_meta_dummy env l) - * | Case (_,_,_,_,Some default) -> lexp_type env default - * (* | Case (_,_,(_,i, args, branch) :: _,_) -> - * * let ct = lexp_type env (vmap_getval cv) in - * * let rec one_arg (t,env) argo = - * * match t with - * * | Arrow (_, None, t1, _, t2) -> - * * (t2, VMap.add (snd argo) (None, t1) env) - * * | Arrow (_, Some (l,v), t1, _, t2) -> - * * (Susp (VMap.add v (mk_meta_dummy l) VMap.empty, t2), - * * VMap.add (snd argo) (None, t1) env) - * * | Susp (s, Arrow (ak,v,t1,l,t2)) -> - * * one_arg (Arrow (ak, v, Susp (s, t1), l, Susp (s, t2)), env) argo - * * | _ -> msg_error (fst argo) "Too many arguments"; - * * (t, VMap.add (snd argo) - * * (None, mk_meta_dummy (fst argo)) - * * env) - * * in let (_,env') = List.fold_left one_arg (ct,env) args - * * in lexp_type env' branch *) - * | Case (l,_,_,_,None) -> mk_meta_dummy env l (* Dead code? *) - * | Susp (s, e) -> lexp_type env (lexp_whnf s e) - * | Metavar ((l,_),_,r) - * -> match !r with MetaSet e -> lexp_type env e - * | MetaUnset (_, Some t, _) -> t - * | _ -> msg_error l "Uninstantiated metavar of unknown type"; - * mk_meta_dummy env l *) - *)

@@ -534,11 +353,14 @@ let rec lexp_unparse lxp = | Arrow (arg_kind, vdef, ltp1, loc, ltp2) -> Parrow(arg_kind, vdef, lexp_unparse ltp1, loc, lexp_unparse ltp2)

- | Let (loc, ldecls, body) -> - (* (vdef * lexp * ltype) list *) - let pdecls = List.fold_left (fun acc (vdef, lxp, ltp) -> - Ptype(vdef, lexp_unparse ltp)::Pexpr(vdef, lexp_unparse lxp)::acc) [] ldecls in - Plet (loc, pdecls, lexp_unparse body) + | Let (loc, ldecls, body) + -> (* (vdef * lexp * ltype) list *) + let pdecls = List.fold_left + (fun acc (vdef, lxp, ltp) + -> Ptype (vdef, lexp_unparse ltp) + :: Pexpr(vdef, lexp_unparse lxp)::acc) + [] ldecls in + Plet (loc, pdecls, lexp_unparse body)

| Call(lxp, largs) -> (* (arg_kind * lexp) list *) let pargs = List.map (fun (kind, elem) -> lexp_unparse elem) largs in @@ -721,9 +543,9 @@ and _lexp_to_str ctx exp = | h1::decls -> h1, decls, 2 | _ -> "", [], 1 in

- let decls = List.fold_left (fun str elem -> - str ^ (make_indent 1) ^ elem ^ nl) - (h1 ^ nl) decls in + let decls = List.fold_left (fun str elem + -> str ^ (make_indent 1) ^ elem ^ nl) + (h1 ^ nl) decls in

let n = String.length decls - 2 in (* remove last newline *) @@ -778,8 +600,9 @@ and _lexp_to_str ctx exp = (* not an operator *) | _ -> let args = List.fold_left - (fun str (_, lxp) -> str ^ " " ^ (lexp_to_str lxp)) - "" args in + (fun str (_, lxp) + -> str ^ " " ^ (lexp_to_str lxp)) + "" args in

let str = fun_call (lexp_to_str fname) in let str = add_parens inner_parens str in @@ -790,26 +613,28 @@ and _lexp_to_str ctx exp = (keyword "inductive_") ^ " (" ^ name ^") " ^ (lexp_str_ctor ctx ctors)

- | Inductive (_, (_, name), args, ctors) -> - let args_str = List.fold_left (fun str (arg_kind, (_, name), ltype) -> - str ^ " (" ^ name ^ " " ^ (kindp_str arg_kind) ^ " " - ^ (lexp_to_str ltype) ^ ")") - "" args in + | Inductive (_, (_, name), args, ctors) + -> let args_str + = List.fold_left + (fun str (arg_kind, (_, name), ltype) + -> str ^ " (" ^ name ^ " " ^ (kindp_str arg_kind) ^ " " + ^ (lexp_to_str ltype) ^ ")") + "" args in

- (keyword "inductive_") ^ " (" ^ name ^ args_str ^") " ^ - (lexp_str_ctor ctx ctors) + (keyword "inductive_") ^ " (" ^ name ^ args_str ^") " + ^ (lexp_str_ctor ctx ctors)

| Case (_, target, _ret, map, dflt) ->( let str = (keyword "case ") ^ (lexp_to_str target) (* FIXME: `tpe' is the *base* type of `target`. E.g. if `target` * is a `List Int`, then `tpe` will be `List`. ^ * " : " ^ (lexp_to_str tpe) *) in - let arg_str arg = - List.fold_left (fun str v -> - match v with - | (_,None) -> str ^ " _" - | (_, Some (_, n)) -> str ^ " " ^ n) "" arg in - + let arg_str arg + = List.fold_left (fun str v + -> match v with + | (_,None) -> str ^ " _" + | (_, Some (_, n)) -> str ^ " " ^ n) + "" arg in

let str = SMap.fold (fun k (_, arg, exp) str -> str ^ nl ^ (make_indent 1) ^ @@ -834,13 +659,13 @@ and _lexp_to_str ctx exp = | SortLevel (SLsucc e) -> "<LevelS?>"

and lexp_str_ctor ctx ctors = - SMap.fold (fun key value str -> - let str = str ^ " (" ^ key in - let str = List.fold_left (fun str (k, _, arg) -> - str ^ " " ^ (_lexp_to_str ctx arg)) str value in - - str ^ ")") - ctors "" + SMap.fold (fun key value str + -> let str = str ^ " (" ^ key in + let str = List.fold_left (fun str (k, _, arg) + -> str ^ " " ^ (_lexp_to_str ctx arg)) + str value in + str ^ ")") + ctors ""

and _lexp_str_decls ctx decls =

@@ -855,9 +680,9 @@ and _lexp_str_decls ctx decls = let type_str name lxp = (if ptype then ( name ^ " : " ^ (lexp_to_str lxp) ^ ";") else "") in

- let ret = List.fold_left (fun str ((_, name), lxp, ltp) -> - let str = if ptype then (type_str name ltp)::str else str in - (name ^ " = " ^ (lexp_to_str lxp) ^ ";" ^ sepdecl)::str) - - [] decls in - List.rev ret + let ret = List.fold_left + (fun str ((_, name), lxp, ltp) + -> let str = if ptype then (type_str name ltp)::str else str in + (name ^ " = " ^ (lexp_to_str lxp) ^ ";" ^ sepdecl)::str) + [] decls in + List.rev ret

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -56,7 +56,7 @@ module SU = Subst

(* Shortcut => Create a Var *) let make_var name index loc = - Var(((loc, name), index)) + mkVar (((loc, name), index))

(* dummies *) let dlxp = type0 @@ -128,9 +128,8 @@ let elab_check_def (ctx : elab_context) var lxp ltype = lexp_error loc lxp "Error while type-checking"; print_lexp_ctx (ectx_to_lctx ctx); raise e in - (* FIXME: conv_p fails too often, e.g. it fails to see that `Type` is - * convertible to `Type_0`, because it doesn't have access to lctx. *) - if true (* OL.conv_p ltype ltype' *) then + let meta_ctx, _ = !global_substitution in + if OL.conv_p meta_ctx (ectx_to_lctx ctx) ltype ltype' then elab_check_proper_type ctx ltype (Some var) else (debug_messages fatal loc "Type check error: ¡¡ctx_define error!!" [ @@ -234,7 +233,7 @@ let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype = match p with (* Block/String/Integer/Float. *) | Pimm v - -> (Imm(v), + -> (mkImm (v), match v with | Integer _ -> type_int | Float _ -> type_float @@ -272,7 +271,7 @@ let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype =

let lxp = lexp_type_infer expr nctx None trace in

- let v = Arrow(kind, ovar, ltp, tloc, lxp) in + let v = mkArrow(kind, ovar, ltp, tloc, lxp) in v, type0

| Pinductive (label, formal_args, ctors) @@ -289,14 +288,14 @@ let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype =

let nctx = !nctx in let ltp = List.fold_left (fun tp (kind, v, ltp) - -> (Arrow (kind, Some v, ltp, tloc, tp))) + -> (mkArrow (kind, Some v, ltp, tloc, tp))) (* FIXME: See OL.check for how to * compute the real target sort * (not always type0). *) type0 (List.rev formal) in

let map_ctor = lexp_parse_inductive ctors nctx trace in - let v = Inductive(tloc, label, formal, map_ctor) in + let v = mkInductive(tloc, label, formal, map_ctor) in v, ltp

(* This case can be inferred *) @@ -310,8 +309,8 @@ let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype = * let nctx = env_extend ctx var Variable ltp in * let lbody, lbtp = lexp_infer body nctx in * - * let lambda_type = Arrow(kind, None, ltp, tloc, lbtp) in - * Lambda(kind, var, ltp, lbody), lambda_type *) + * let lambda_type = mkArrow(kind, None, ltp, tloc, lbtp) in + * mkLambda(kind, var, ltp, lbody), lambda_type *)

| Pcall (fname, _args) -> lexp_call fname _args ctx trace

@@ -345,22 +344,22 @@ let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype = i - 1)) formal ([], List.length formal + List.length args - 1) in - Call (push_susp idt (S.shift (List.length formal - + List.length args)), - targs) in + mkCall (push_susp idt (S.shift (List.length formal + + List.length args)), + targs) in let cons_type = List.fold_left (fun ltp (kind, v, tp) - -> Arrow (kind, v, tp, loc, ltp)) + -> mkArrow (kind, v, tp, loc, ltp)) target (List.rev args) in

(* Add Aerasable arguments. *) let cons_type = List.fold_left (fun ltp (kind, v, tp) - -> Arrow (Aerasable, Some v, tp, loc, ltp)) + -> mkArrow (Aerasable, Some v, tp, loc, ltp)) cons_type (List.rev formal) in

- Cons(idt, sym), cons_type + mkCons(idt, sym), cons_type

| Phastype (_, pxp, ptp) -> let ltp = lexp_type_infer ptp ctx None trace in @@ -379,7 +378,7 @@ and lexp_type_infer pexp ectx var trace = t

and lexp_let_decls declss (body: lexp) ctx i = - List.fold_right (fun decls lxp -> Let (dloc, decls, lxp)) + List.fold_right (fun decls lxp -> mkLet (dloc, decls, lxp)) declss body

and _lexp_p_check (p : pexp) (t : ltype) (ctx : elab_context) trace: lexp = @@ -412,7 +411,7 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : elab_context) trace: lexp = -> let laty, lasort = lexp_infer paty ctx in elab_check_sort ctx lasort (Some var) laty; laty in - let arrow = Arrow (kind, None, arg, Util.dummy_location, body) in + let arrow = mkArrow (kind, None, arg, Util.dummy_location, body) in match Unif.unify arrow lxp subst with | Some subst -> global_substitution := subst; arg, body | None -> lexp_error tloc lxp ("Type " ^ lexp_string lxp @@ -433,7 +432,7 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : elab_context) trace: lexp =

let nctx = env_extend ctx var Variable ltp in let lbody = lexp_check body lbtp nctx in - Lambda(kind, var, ltp, lbody) + mkLambda (kind, var, ltp, lbody)

in let subst, _ = !global_substitution in @@ -528,7 +527,7 @@ and lexp_case rtype (loc, target, ppatterns) ctx i = let meta_ctx, _ = !global_substitution in match OL.lexp_whnf lctor (ectx_to_lctx ctx) meta_ctx with | Cons (it', (_, cons_name)) - -> let _ = if OL.conv_p it' it then () + -> let _ = if OL.conv_p meta_ctx (ectx_to_lctx ctx) it' it then () else lexp_error loc lctor ("Expected pattern of type `" ^ lexp_string it ^ "` but got `" @@ -582,7 +581,7 @@ and lexp_case rtype (loc, target, ppatterns) ctx i = | Ppatsym ((_, name) as var) -> (try let idx = senv_lookup name ctx in let meta_ctx, _ = !global_substitution in - match OL.lexp_whnf (Var (var, idx)) + match OL.lexp_whnf (mkVar (var, idx)) (ectx_to_lctx ctx) meta_ctx with | Cons _ (* It's indeed a constructor! *) -> add_branch (Pvar var) [] @@ -594,7 +593,7 @@ and lexp_case rtype (loc, target, ppatterns) ctx i = let (lpattern, dflt) = List.fold_left fold_fun (SMap.empty, None) ppatterns in

- Case (loc, tlxp, rtype, lpattern, dflt) + mkCase (loc, tlxp, rtype, lpattern, dflt)

(* Identify Call Type and return processed call *) and lexp_call (func: pexp) (sargs: sexp list) ctx i = @@ -692,7 +691,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = print_endline (">>>" ^ lexp_string ltp); raise (Internal_error m) in - Call (body, List.rev largs), ret_type in + mkCall (body, List.rev largs), ret_type in

let handle_macro_call () = let sxp = match lexp_expand_macro body sargs ctx i with @@ -716,10 +715,8 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = (* determine function type *) match func, ltp with | macro, _ when (macro_disp - (* FIXME: This call to lexp_whnf shouldn't be needed! *) - && OL.conv_p (OL.lexp_whnf ltp (ectx_to_lctx ctx) - meta_ctx) - macro_type) -> ( + && OL.conv_p meta_ctx (ectx_to_lctx ctx) + ltp macro_type) -> ( match macro with | Pvar(l, name) when is_builtin_macro name -> let pargs = List.map pexp_parse sargs in @@ -727,8 +724,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = (get_macro_impl loc name) loc largs ctx ltp

(* true macro *) - | _ -> - handle_macro_call ()) + | _ -> handle_macro_call ())

(* FIXME: Handle special-forms here as well! *) | _ -> handle_funcall () @@ -772,7 +768,7 @@ and lexp_expand_macro macro_funct sargs ctx trace = let macro_expand = get_predef "expand_macro_" ctx in let args = [(Aexplicit, macro_funct); (Aexplicit, (olist2tlist_lexp sargs ctx))] in

- let macro = Call(macro_expand, args) in + let macro = mkCall (macro_expand, args) in let emacro = OL.erase_type macro in let rctx = from_lctx ctx in

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

type 'a myers = | Mnil + (* | Mcons1 of 'a * 'a myers *) | Mcons of 'a * 'a myers * int * 'a myers

(* Contrary to Myers's presentation, we index from the top of the stack, @@ -44,7 +45,7 @@ let nil = Mnil

let cons x l = match l with - | Mcons (_, _, s1, Mcons (_, _, s2, l2)) when s1 = s2 + | Mcons (_, _, s1, Mcons (_, _, s2, l2)) when s1 >= s2 -> Mcons (x, l, s1 + s2 + 1, l2) | _ -> Mcons (x, l, 1, l)

===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -48,72 +48,7 @@ let impredicative_erase = true (* Allows erasable args to be impredicative. *) let lookup_type = DB.lctx_lookup_type let lookup_value = DB.lctx_lookup_value

-(********* Testing if two types are "convertible" aka "equivalent" *********) - -let get_vardef lv = match lv with - | Some lv -> lv - | None -> (U.dummy_location, "<anon>") - -let rec conv_arglist_p s1 s2 args1 args2 : bool = - List.fold_left2 - (fun eqp (ak1,t1) (ak2,t2) -> - eqp && ak1 = ak2 && conv_p' s1 s2 t1 t2) - true args1 args2 - -(* Returns true if e₁ and e₂ are equal (upto alpha/beta/...). *) -and conv_p' (s1:lexp S.subst) (s2:lexp S.subst) e1 e2 : bool = - let conv_p = conv_p' s1 s2 in - (* e1 == e2 !! Looks obvious, but can fail because of s1 and s2 !! *) - match (e1, e2) with - | (Imm (Integer (_, i1)), Imm (Integer (_, i2))) -> i1 = i2 - | (Imm (Float (_, i1)), Imm (Float (_, i2))) -> i1 = i2 - | (Imm (String (_, i1)), Imm (String (_, i2))) -> i1 = i2 - | (SortLevel (sl1), SortLevel (sl2)) -> sl1 == sl2 - | (Sort (_, s1), Sort (_, s2)) -> s1 = s2 - | (Builtin ((_, s1), _), Builtin ((_, s2), _)) -> s1 == s2 - (* BEWARE: When we'll make expand let-defined vars here, we'll have to - * be careful not to introduce infinite-recursion. *) - | (Var (l1, v1), e2) when not (S.identity_p s1) -> - conv_p' S.identity s2 (slookup s1 l1 v1) e2 - | (e1, Var (l2, v2)) when not (S.identity_p s2) -> - conv_p' s1 S.identity e1 (slookup s2 l2 v2) - | (Var (_, v1), Var (_, v2)) -> v1 == v2 - | (Susp (e1, s1'), e2) -> conv_p' (scompose s1' s1) s2 e1 e2 - | (e1, Susp (e2, s2')) -> conv_p' s1 (scompose s2' s2) e1 e2 - | (Arrow (ak1, vd1, t11, _, t12), Arrow (ak2, vd2, t21, _, t22)) - -> ak1 == ak2 && conv_p t11 t21 - && conv_p' (ssink (get_vardef vd1) s1) (ssink (get_vardef vd2) s2) - t12 t22 - | (Lambda (ak1, l1, t1, e1), Lambda (ak2, l2, t2, e2)) - -> ak1 == ak2 && conv_p t1 t2 && conv_p' (ssink l1 s1) (ssink l2 s2) e1 e2 - | (Call (f1, args1), Call (f2, args2)) - -> conv_p f1 f2 && conv_arglist_p s1 s2 args1 args2 - | (Inductive (_, l1, args1, cases1), Inductive (_, l2, args2, cases2)) - -> let rec conv_args s1 s2 args1 args2 = - match args1, args2 with - | ([], []) -> true - | ((ak1,l1,t1)::args1, (ak2,l2,t2)::args2) - -> ak1 == ak2 && conv_p' s1 s2 t1 t2 - && conv_args (ssink l1 s1) (ssink l2 s2) args1 args2 - | _,_ -> false in - let rec conv_fields s1 s2 fields1 fields2 = - match fields1, fields2 with - | ([], []) -> true - | ((ak1,vd1,t1)::fields1, (ak2,vd2,t2)::fields2) - -> ak1 == ak2 && conv_p' s1 s2 t1 t2 - && conv_fields (match vd1 with None -> s1 | Some l1 -> ssink l1 s1) - (match vd2 with None -> s2 | Some l2 -> ssink l2 s2) - fields1 fields2 - | _,_ -> false in - l1 == l2 && conv_args s1 s2 args1 args2 - && SMap.equal (conv_fields s1 s2) cases1 cases2 - | (Cons (t1, l1), Cons (t2, l2)) -> l1 == l2 && conv_p t1 t2 - (* FIXME: Various missing cases, such as Let, Case, and beta-reduction. *) - | (_, _) -> false - -and conv_p e1 e2 = conv_p' S.identity S.identity e1 e2 - -(* Extend a substitution S with a (mutually recursive) set +(** Extend a substitution S with a (mutually recursive) set * of definitions DEFS. * This is rather tricky. E.g. for * @@ -132,7 +67,7 @@ and conv_p e1 e2 = conv_p' S.identity S.identity e1 e2 let rec lexp_defs_subst l s defs = match defs with | [] -> s | (_, lexp, _) :: defs' - -> lexp_defs_subst l (S.cons (Let (l, defs, lexp)) s) defs' + -> lexp_defs_subst l (S.cons (mkLet (l, defs, lexp)) s) defs'

(* Reduce to weak head normal form. * WHNF implies: @@ -169,17 +104,17 @@ let lexp_whnf e (ctx : DB.lexp_context) meta_ctx : lexp = | Some e' -> lexp_whnf e' ctx) | Susp (e, s) -> lexp_whnf (push_susp e s) ctx | Call (e, []) -> lexp_whnf e ctx - | Call (e, (((_, arg)::args) as xs)) -> - (match lexp_whnf e ctx with + | Call (f, (((_, arg)::args) as xs)) -> + (match lexp_whnf f ctx with | Lambda (_, _, _, body) -> (* Here we apply whnf to the arg eagerly to kind of stay closer * to the idea of call-by-value, although in this context * we can't really make sure we always reduce the arg to a value. *) - lexp_whnf (Call (push_susp body (S.substitute (lexp_whnf arg ctx)), - args)) + lexp_whnf (mkCall (push_susp body (S.substitute (lexp_whnf arg ctx)), + args)) ctx - | Call (e', xs1) -> Call (e', List.append xs1 xs) - | e' -> Call (e, xs)) (* Keep `e`, assuming it's more readable! *) + | Call (f', xs1) -> mkCall (f', List.append xs1 xs) + | _ -> e) (* Keep `e`, assuming it's more readable! *) | Case (l, e, rt, branches, default) -> let e' = lexp_whnf e ctx in let reduce name aargs = @@ -200,29 +135,117 @@ let lexp_whnf e (ctx : DB.lexp_context) meta_ctx : lexp = | _ -> U.msg_error "WHNF" l ("Unhandled constructor " ^ name ^ "in case expression"); - Case (l, e, rt, branches, default) in + mkCase (l, e, rt, branches, default) in (match e' with | Cons (_, (_, name)) -> reduce name [] | Call (Cons (_, (_, name)), aargs) -> reduce name aargs - | _ -> Case (l, e, rt, branches, default)) + | _ -> mkCase (l, e, rt, branches, default)) | Metavar (idx, s, _, _) -> (try lexp_whnf (mkSusp (L.VMap.find idx meta_ctx) s) ctx - with Not_found -> e) + with Not_found -> e)

- (* FIXME: - * - This should be correct, but requires improvements in conv_p - * to avoid inf-looping! - * - I'd really prefer to use "native" recursive substitutions, using - * ideally a trick similar to the db_offsets in lexp_context! - * - * | Let (l, defs, body) - * -> push_susp body (lexp_defs_subst l S.identity defs) *) + (* FIXME: I'd really prefer to use "native" recursive substitutions, using + * ideally a trick similar to the db_offsets in lexp_context! *) + | Let (l, defs, body) + -> push_susp body (lexp_defs_subst l S.identity defs)

| e -> e

in lexp_whnf e ctx

+(** A very naive implementation of sets of lexps. *) +type set_lexp = lexp list +let set_empty : set_lexp = [] +let set_member_p (s : set_lexp) (e : lexp) : bool + = if not (e == Lexp.hc e) then + (print_string "Not hashcons'd: "; + lexp_print e; + print_string "\n"); + assert (e == Lexp.hc e); + List.mem e s +let set_add (s : set_lexp) (e : lexp) : set_lexp + = assert (not (set_member_p s e)); + e :: s +let set_shift_n (s : set_lexp) (n : U.db_offset) + = List.map (fun e -> Lexp.push_susp e (S.shift n)) s +let set_shift s : set_lexp = 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_lexp) 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 stop1 = not (e1 == e1') && set_member_p vs e1' in + let stop2 = not (e2 == e2') && set_member_p vs e2' in + let vs' = if not (e1 == e1') && not stop1 then set_add vs e1' + else if not (e2 == e2') && not stop2 then set_add vs e2' + else vs in + let conv_p = conv_p' ctx vs' in + let conv_p'' e1 e2 = + e1 == e2 || + (match (e1, e2) with + | (Imm (Integer (_, i1)), Imm (Integer (_, i2))) -> i1 = i2 + | (Imm (Float (_, i1)), Imm (Float (_, i2))) -> i1 = i2 + | (Imm (String (_, i1)), Imm (String (_, i2))) -> i1 = i2 + | (SortLevel (sl1), SortLevel (sl2)) -> sl1 = sl2 + | (Sort (_, s1), Sort (_, s2)) + -> s1 == s2 + || (match (s1, s2) with + | (Stype e1, Stype e2) -> conv_p e1 e2 + | _ -> false) + | (Builtin ((_, s1), _), Builtin ((_, s2), _)) -> s1 = s2 + | (Var (_, v1), Var (_, v2)) -> v1 = v2 + | (Arrow (ak1, vd1, t11, _, t12), Arrow (ak2, vd2, t21, _, t22)) + -> ak1 == ak2 + && conv_p t11 t21 + && conv_p' (DB.lexp_ctx_cons ctx 0 vd1 Variable t11) (set_shift vs') + t12 t22 + | (Lambda (ak1, l1, t1, e1), Lambda (ak2, l2, t2, e2)) + -> ak1 == ak2 && conv_p t1 t2 + && conv_p' (DB.lexp_ctx_cons ctx 0 (Some l1) Variable t1) + (set_shift vs') + e1 e2 + | (Call (f1, args1), Call (f2, args2)) + -> let rec conv_arglist_p args1 args2 : bool = + List.fold_left2 + (fun eqp (ak1,t1) (ak2,t2) -> eqp && ak1 = ak2 && conv_p t1 t2) + true args1 args2 in + conv_p f1 f2 && conv_arglist_p args1 args2 + | (Inductive (_, l1, args1, cases1), Inductive (_, l2, args2, cases2)) + -> let rec conv_args ctx vs args1 args2 = + match args1, args2 with + | ([], []) -> true + | ((ak1,l1,t1)::args1, (ak2,l2,t2)::args2) + -> ak1 == ak2 && conv_p' ctx vs t1 t2 + && conv_args (DB.lexp_ctx_cons ctx 0 (Some l1) Variable t1) + (set_shift vs) + args1 args2 + | _,_ -> false in + let rec conv_fields ctx vs fields1 fields2 = + match fields1, fields2 with + | ([], []) -> true + | ((ak1,vd1,t1)::fields1, (ak2,vd2,t2)::fields2) + -> ak1 == ak2 && conv_p' ctx vs t1 t2 + && conv_fields (DB.lexp_ctx_cons ctx 0 vd1 Variable t1) + (set_shift vs) + fields1 fields2 + | _,_ -> false in + l1 == l2 && conv_args ctx vs' args1 args2 + && SMap.equal (conv_fields ctx vs') cases1 cases2 + | (Cons (t1, (_, l1)), Cons (t2, (_, l2))) -> l1 = l2 && conv_p t1 t2 + (* FIXME: Various missing cases, such as Case. *) + | (_, _) -> false) + in if stop1 || stop2 + then conv_p'' e1 e2 + else conv_p'' e1' e2' + +let conv_p meta_ctx (ctx : DB.lexp_context) e1 e2 + = if e1 == e2 then true + else conv_p' meta_ctx ctx set_empty e1 e2 + (********* Testing if a lexp is properly typed *********)

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