Stefan pushed to branch master at Stefan / Typer
Commits: 108275af by Stefan Monnier at 2016-11-14T19:37:13-05:00 Switch metavars to use ?<name> instead of _
* DESIGN: Use org-mode to highlight URLs.
* src/builtin.ml: Don't open `Debruijn`. Hash-cons predefined sorts.
* src/debruijn.ml (level0): Move from src/builtin.ml. (type0): Hash-cons it.
* src/eval.ml (print_eval_result): Remove unused `lexp-trace` var.
* src/inverse_subst.ml (impossible): Silence compiler warning.
* src/lexp.ml (push_susp): Fix SortLevel induction. Fix missing hash-cons of `Let`. (clean): New function. (lexp_unparse): Print metavars with their substitution. (subst_string): Print shifts more like we used in the article.
* src/lparse.ml (elab_check_sort, elab_check_def): Use `clean` to replace instantiated metavars in error message. (newMetavar): Add `l` and `name` args. (newMetalevel, newMetatype): Update accordingly. (infer_type): Try to unify with `Sort` before signaling an error. (infer_call): Remove redundant `nosusp`.
* src/opslexp.ml (conv_p'): Minor simplification.
* src/pexp.ml (pexp_parse): Don't treat `_` as metavar. Treat any var starting with `?` as a metavar instead.
* tests/eval_test.ml ("Metavars"): New test.
- - - - -
11 changed files:
- DESIGN - src/builtin.ml - src/debruijn.ml - src/eval.ml - src/inverse_subst.ml - src/lexp.ml - src/lparse.ml - src/opslexp.ml - src/pexp.ml - tests/eval_test.ml - tests/inverse_test.ml
Changes:
===================================== DESIGN ===================================== --- a/DESIGN +++ b/DESIGN @@ -1,4 +1,4 @@ --*- outline -*- +-*- org -*-
New: - extend the stt table to give precedence for "inner op chars" to use within
===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -36,7 +36,7 @@ open Sexp (* Integer/Float *) open Pexp (* arg_kind *) open Lexp
-open Debruijn +module DB = Debruijn open Env (* get_rte_variable *)
let error loc msg = msg_error "BUILT-IN" loc msg; raise (internal_error msg) @@ -69,13 +69,13 @@ let get_predef_raw (name: string) : lexp = | None -> error dloc ("""^ name ^ "" was not predefined")
let get_predef_option (name: string) ctx = - let r = (get_size ctx) - !builtin_size - 0 in + let r = (DB.get_size ctx) - !builtin_size - 0 in match !(SMap.find name (!predef_map)) with | Some exp -> Some (mkSusp exp (S.shift r)) | None -> None
let get_predef (name: string) ctx = - let r = (get_size ctx) - !builtin_size - 0 in + let r = (DB.get_size ctx) - !builtin_size - 0 in let p = get_predef_raw name in (mkSusp p (S.shift r))
@@ -91,15 +91,15 @@ let dump_predef () = print_string "\n") !predef_map in ()
(* Builtin types *) -let dloc = dummy_location -let level0 = SortLevel SLz -let level1 = SortLevel (SLsucc level0) -let level2 = SortLevel (SLsucc level1) -let type0 = Sort (dloc, Stype level0) -let type1 = Sort (dloc, Stype level1) -let type2 = Sort (dloc, Stype level2) -let type_omega = Sort (dloc, StypeOmega) -let type_level = Sort (dloc, StypeLevel) +let dloc = DB.dloc +let level0 = DB.level0 +let level1 = mkSortLevel (SLsucc level0) +let level2 = mkSortLevel (SLsucc level1) +let type0 = DB.type0 +let type1 = mkSort (dloc, Stype level1) +let type2 = mkSort (dloc, Stype level2) +let type_omega = mkSort (dloc, StypeOmega) +let type_level = mkSort (dloc, StypeLevel)
let op_binary t = Arrow (Aexplicit, None, t, dloc, Arrow (Aexplicit, None, t, dloc, t)) @@ -148,7 +148,7 @@ let rec tlist2olist acc expr =
let is_lbuiltin idx ctx = let bsize = 1 in - let csize = get_size ctx in + let csize = DB.get_size ctx in
if idx >= csize - bsize then true @@ -167,8 +167,8 @@ let get_attribute_impl loc largs ctx ftype = | [Var((_, vn), vi); Var((_, an), ai)] -> (vi, vn), (ai, an) | _ -> error loc "get-attribute expects two arguments" in
- let lxp = get_property ctx (vi, vn) (ai, an) in - let ltype = match env_lookup_expr ctx ((loc, an), ai) with + let lxp = DB.get_property ctx (vi, vn) (ai, an) in + let ltype = match DB.env_lookup_expr ctx ((loc, an), ai) with | Some ltp -> ltp | None -> error loc "not expression available" in
@@ -188,7 +188,7 @@ let has_attribute_impl loc largs ctx ftype = | [Var((_, vn), vi); Var((_, an), ai)] -> (vi, vn), (ai, an) | _ -> error loc "has-attribute expects two arguments" in
- let b = has_property ctx (vi, vn) (ai, an) in + let b = DB.has_property ctx (vi, vn) (ai, an) in
let rvar = if b then get_predef "True" ctx else get_predef "False" ctx in rvar, (get_predef "Bool" ctx) @@ -199,7 +199,7 @@ let declexpr_impl loc largs ctx ftype = | [Var((_, vn), vi)] -> (vi, vn) | _ -> error loc "declexpr expects one argument" in
- let lxp = match env_lookup_expr ctx ((loc, vn), vi) with + let lxp = match DB.env_lookup_expr ctx ((loc, vn), vi) with | Some lxp -> lxp | None -> error loc "no expr available" in (* ltp and ftype should be the same @@ -213,7 +213,7 @@ let decltype_impl loc largs ctx ftype = | [Var((_, vn), vi)] -> (vi, vn) | _ -> error loc "decltype expects one argument" in
- let ltype = env_lookup_type ctx ((loc, vn), vi) in + let ltype = DB.env_lookup_type ctx ((loc, vn), vi) in (* mkSusp prop (S.shift (var_i + 1)) *) ltype, type0
@@ -229,7 +229,7 @@ let builtin_macro = [ ]
type macromap = - (location -> lexp list -> elab_context -> lexp -> (lexp * lexp)) SMap.t + (location -> lexp list -> DB.elab_context -> lexp -> (lexp * lexp)) SMap.t
let macro_impl_map : macromap = List.fold_left (fun map (name, funct) ->
===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -79,7 +79,8 @@ let warning = msg_warning "DEBRUIJN" * ---------------------------------- *)
let dloc = dummy_location -let type0 = Sort (dloc, Stype (SortLevel SLz)) +let level0 = mkSortLevel SLz +let type0 = mkSort (dloc, Stype level0) let dltype = type0
type property_key = (int * string) (* rev_dbi * Var name *)
===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -566,7 +566,6 @@ and print_trace title trace default = print_string ((type_name expr) ^ ": " ^ (type_string expr) ^ "\n") ) in
- let lexp_trace = print_trace pexp_name pexp_string pexp_location in let elexp_trace = print_trace elexp_name elexp_string elexp_location in
(* Print the trace*)
===================================== src/inverse_subst.ml ===================================== --- a/src/inverse_subst.ml +++ b/src/inverse_subst.ml @@ -19,6 +19,18 @@ 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/. *)
+(* During unification, we often have problems of the form + * + * X[σ] = e + * + * Where X is a metavariable and `e` can be any term. We can solve this + * problem by computing the inverse of the substitution, σ⁻¹, and use: + * + * X = e[σ⁻¹] + * + * where σ⁻¹ is such that e[σ⁻¹][σ] = e[σ⁻¹ ∘ σ] = e + *) + open Lexp open Util module S = Subst @@ -72,7 +84,7 @@ let counter = ref 0 let mkVar (idx: int) : lexp = counter := !counter + 1; Var((U.dummy_location, "<anon" ^ string_of_int idx ^ ">"), idx) -let impossible = Imm Epsilon +let impossible = Imm Sexp.Epsilon
(** Fill the gap between e_i in the list of couple (e_i, i) by adding dummy variables.
===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -201,7 +201,8 @@ let maybev mv = match mv with None -> vdummy | Some v -> v let rec push_susp e s = (* Push a suspension one level down. *) match e with | Imm _ -> e - | SortLevel _ -> e + | SortLevel (SLz) -> e + | SortLevel (SLsucc e') -> mkSortLevel (SLsucc (mkSusp e' s)) | Sort (l, Stype e) -> mkSort (l, Stype (mkSusp e s)) | Sort (l, _) -> e | Builtin _ -> e @@ -211,7 +212,7 @@ let rec push_susp e s = (* Push a suspension one level down. *) -> (ssink v s, (v, mkSusp e s', mkSusp ty s) :: ndefs)) (s, []) defs in - Let (l, ndefs, mkSusp e s') + mkLet (l, ndefs, mkSusp e s') | Arrow (ak, v, t1, l, t2) -> 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)) @@ -254,11 +255,70 @@ let rec push_susp e s = (* Push a suspension one level down. *) | Susp (e,s') -> push_susp e (scompose s' s) | (Var _ | Metavar _) -> nosusp (mkSusp e s)
-and nosusp e = (* Return `e` without `Susp`. *) +and nosusp e = (* Return `e` with no outermost `Susp`. *) match e with | Susp(e, s) -> push_susp e s | _ -> e
+ +(* Get rid of `Susp`ensions and instantiated `Maetavar`s. *) +let clean meta_ctx e = + let rec clean s e = match e with + | Imm _ -> e + | SortLevel (SLz) -> e + | SortLevel (SLsucc e) -> mkSortLevel (SLsucc (clean s e)) + | Sort (l, Stype e) -> mkSort (l, Stype (clean s e)) + | Sort (l, _) -> e + | Builtin _ -> e + | Let (l, defs, e) + -> let s' = L.fold_left (fun s (v, _, _) -> ssink v s) s defs in + let (_,ndefs) = L.fold_left (fun (s,ndefs) (v, def, ty) + -> (ssink v s, + (v, clean s' e, clean s ty) :: ndefs)) + (s, []) defs in + mkLet (l, ndefs, clean s' e) + | Arrow (ak, v, t1, l, t2) + -> mkArrow (ak, v, clean s t1, l, clean (ssink (maybev v) s) t2) + | Lambda (ak, v, t, e) -> mkLambda (ak, v, clean s t, clean (ssink v s) e) + | Call (f, args) -> mkCall (clean s f, + L.map (fun (ak, arg) -> (ak, clean s arg)) args) + | Inductive (l, label, args, cases) + -> let (s, nargs) = L.fold_left (fun (s, nargs) (ak, v, t) + -> (ssink v s, (ak, v, clean s t) :: nargs)) + (s, []) args in + let ncases = SMap.map (fun args + -> let (_, ncase) + = L.fold_left (fun (s, nargs) (ak, v, t) + -> (ssink (maybev v) s, + (ak, v, clean s t) + :: nargs)) + (s, []) args in + L.rev ncase) + cases in + mkInductive (l, label, nargs, ncases) + | Cons (it, name) -> Cons (clean s it, name) + | Case (l, e, ret, cases, default) + -> mkCase (l, clean s e, clean s ret, + 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, clean s' e)) + cases, + match default with + | None -> default + | Some (v,e) -> Some (v, clean (ssink (maybev v) s) 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 (VMap.find idx meta_ctx) + with Not_found -> mkMetavar (idx, s, l, t) + in clean S.identity e + let lexp_name e = match e with | Imm _ -> "Imm" @@ -274,77 +334,6 @@ let lexp_name e = | Susp _ -> "Susp" | _ -> "lexp_to_string: not implemented"
-(* -(* In non-recursion calls, `s' is always empty. *) -let lexp_conv_p env = lexp_conv_p env VMap.empty - -let lexp_unparse_v (l,v) - (* FIXME: This only works for bound vars, free vars will need - * a different treatment! *) - = let name = varname v in (l,name ^ (string_of_int v)) -let rec lexp_unparse_decls decls = - List.map (fun (v,_,t) - -> (lexp_unparse_v v, lexp_unparse t, true)) - decls - @ List.map (fun (v,e,_) - -> (lexp_unparse_v v, lexp_unparse e, false)) - decls -and lexp_unparse e : pexp = - match e with - | Sort (l, StypeLevel) -> Pvar (l, "TypeLevel") - | Sort (l, StypeOmega) -> Pvar (l, "TypeΩ") - | Sort (l, Stype e) - -> Pcall (Pvar (l, "Type"), [pexp_unparse (lexp_unparse e)]) - | SortLevel (SLn n) -> Pimm (Integer (U.dummy_location, n)) - | SortLevel (SLsucc e) -> Pcall (Pvar (lexp_location e, "S"), - [pexp_unparse (lexp_unparse e)]) - | Imm s -> Pimm s - | Builtin (b,name,t) -> Pvar (U.dummy_location, name) - | Var v -> Pvar (lexp_unparse_v v) - | Let (l,decls,e) - -> Plet (l, lexp_unparse_decls decls, - lexp_unparse e) - | Arrow (ak,v,t1,l,t2) - -> Parrow (ak, - (match v with Some v -> Some (lexp_unparse_v v) | None -> None), - lexp_unparse t1, - l, lexp_unparse t2) - | Lambda (ak, v, t, e) (* FIXME: losing `ak'. *) - -> Plambda (ak, lexp_unparse_v v, Some (lexp_unparse t), lexp_unparse e) - | Call (f, args) (* FIXME: losing `ak'. *) - -> Pcall (lexp_unparse f, List.map (fun (_,arg) - -> pexp_unparse (lexp_unparse arg)) - args) - | Inductive (_,t,cases) (* FIXME: losing `id'. *) - -> Pinductive (lexp_unparse t, - SMap.fold (fun name t ps - -> ((lexp_location t, name), lexp_unparse t)::ps) - cases []) - | Cons (Var v, tag) - -> Pcons (lexp_unparse_v v, tag) - | Cons (_,_) - -> (U.internal_error "Can't print a non-Var-typed Constructor") - | Case (l, e, t, branches, default) - -> Pcase (l, lexp_unparse e, - (* FIXME!! *) - SMap.fold (fun name (l, args, e) cases - -> ((l,name), - List.map (fun (ak,v) -> (ak, lexp_unparse_v v)) args, - lexp_unparse e) :: cases) - branches [], - opt_map lexp_unparse default) - (* | Metavar (v,_,r) -> - * (match !r with - * | MetaSet e -> lexp_unparse e - * | _ -> Pmetavar v) (* FIXME: losing the ref. *) - * | Susp (s,e) -> lexp_unparse (lexp_whnf s e) *) - (* (U.internal_error "Can't print a Susp") *) - -let lexp_print e = sexp_print (pexp_unparse (lexp_unparse e)) - -*) - - (* ugly printing (sexp_print (pexp_unparse (lexp_unparse e))) *) let rec lexp_unparse lxp = match lxp with @@ -416,23 +405,25 @@ let rec lexp_unparse lxp =
(* FIXME: The cases below are all broken! *) | Metavar (idx, subst, (loc, name), _) - -> Pimm (Symbol (loc, "?<" ^ name ^ "-" ^ string_of_int idx ^ ">")) + -> Pimm (Symbol (loc, "?<" ^ name ^ "-" ^ string_of_int idx + ^ "[" ^ subst_string subst ^ "]>"))
| SortLevel (SLz) -> Pimm (Integer (U.dummy_location, 0)) | SortLevel (SLsucc sl) -> Pcall (Pimm (Symbol (U.dummy_location, "<S>")), [pexp_unparse (lexp_unparse sl)]) - | Sort (l, StypeOmega) -> Pimm (Symbol (l, "<SortOmega>")) - | Sort (l, StypeLevel) -> Pimm (Symbol (l, "<SortLevel>")) + | Sort (l, StypeOmega) -> Pimm (Symbol (l, "<TypeOmega>")) + | Sort (l, StypeLevel) -> Pimm (Symbol (l, "<TypeLevel>")) | Sort (l, Stype sl) -> Pcall (Pimm (Symbol (l, "<Type>")), [pexp_unparse (lexp_unparse sl)])
(* FIXME: ¡Unify lexp_print and lexp_string! *) -let lexp_string lxp = sexp_string (pexp_unparse (lexp_unparse lxp)) +and lexp_string lxp = sexp_string (pexp_unparse (lexp_unparse lxp))
-let rec subst_string s = match s with +and subst_string s = match s with | S.Identity -> "Id" - | S.Shift (s, n) -> "(" ^ subst_string s ^ "↑" ^ string_of_int n ^ ")" + | S.Shift (s, n) -> "(↑"^ string_of_int n ^ " " ^ subst_string s ^ ")" | S.Cons (l, s) -> lexp_string l ^ " · " ^ subst_string s + (* * Printing * --------------------- *)
===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -96,7 +96,8 @@ let elab_check_sort (ctx : elab_context) lsort var ltp = let meta_ctx, _ = !global_substitution in match OL.lexp_whnf lsort (ectx_to_lctx ctx) meta_ctx with | Sort (_, _) -> () (* All clear! *) - | _ -> let typestr = lexp_string ltp ^ " : " ^ lexp_string lsort in + | _ -> let lexp_string e = lexp_string (L.clean meta_ctx e) in + let typestr = lexp_string ltp ^ " : " ^ lexp_string lsort in match var with | None -> lexp_error (lexp_location ltp) ltp ("`" ^ typestr ^ "` is not a proper type") @@ -122,6 +123,7 @@ let elab_check_def (ctx : elab_context) var lxp ltype = 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 with e -> lexp_error loc lxp "Error while type-checking"; @@ -131,9 +133,9 @@ let elab_check_def (ctx : elab_context) var lxp ltype = elab_check_proper_type ctx ltype (Some var) else (debug_messages fatal loc "Type check error: ¡¡ctx_define error!!" [ - (lexp_string lxp) ^ "!: " ^ (lexp_string ltype); - " because"; - (lexp_string (OL.check meta_ctx lctx lxp)) ^ "!= " ^ (lexp_string ltype);]) + lexp_string lxp ^ " !: " ^ lexp_string ltype; + " because"; + lexp_string (OL.check meta_ctx lctx lxp) ^ " != " ^ lexp_string ltype])
let ctx_extend (ctx: elab_context) (var : vdef option) def ltype = elab_check_proper_type ctx ltype var; @@ -197,18 +199,14 @@ let ctx_define_rec (ctx: elab_context) decls = *)
-let newMetavar t = +let newMetavar l name t = let meta = Unif.create_metavar () in - let name = "__metavar" (* ^ (string_of_int meta) *) in - mkMetavar (meta, S.Identity, (Util.dummy_location, name), t) + mkMetavar (meta, S.Identity, (l, name), t)
let newMetalevel () = - let meta = Unif.create_metavar () in - let name = "__metalevel" (* ^ (string_of_int meta) *) in - mkMetavar (meta, S.Identity, (Util.dummy_location, name), - Sort (dummy_location, StypeLevel)) + newMetavar Util.dummy_location "l" (Sort (dummy_location, StypeLevel))
-let newMetatype () = newMetavar (newMetalevel ()) +let newMetatype () = newMetavar Util.dummy_location "t" (newMetalevel ())
let rec infer (p : pexp) (ctx : elab_context): lexp * ltype =
@@ -357,7 +355,9 @@ and instantiate_implicit e t ctx = let rec instantiate t args = match OL.lexp_whnf t (ectx_to_lctx ctx) meta_ctx with | Arrow ((Aerasable | Aimplicit) as ak, v, t1, _, t2) - -> let arg = newMetavar t1 in (* FIXME: Use `v` to make matevar name. *) + -> let arg = newMetavar (lexp_location e) + (match v with Some (_, name) -> name | _ -> "v") + t1 in instantiate (mkSusp t2 (S.substitute arg)) ((ak, arg)::args) | _ -> (mkCall (e, List.rev args), t) in instantiate t [] @@ -367,7 +367,24 @@ 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 - elab_check_sort ectx s var t; + (let meta_ctx, _ = !global_substitution in + match OL.lexp_whnf s (ectx_to_lctx ectx) meta_ctx with + | Sort (_, _) -> () (* All clear! *) + | _ -> + (* 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 + let typestr = lexp_string t ^ " : " ^ lexp_string s in + match var with + | None -> lexp_error (lexp_location t) t + ("`" ^ typestr ^ "` is not a proper type") + | Some (l, name) + -> lexp_error l t + ("Type of `" ^ name ^ "` is not a proper type: " + ^ typestr)) + | Some subst -> global_substitution := subst); t
and lexp_let_decls declss (body: lexp) ctx = @@ -442,7 +459,10 @@ and check (p : pexp) (t : ltype) (ctx : elab_context): lexp = (* FIXME: Handle *macro* pcalls here! *) (* | Pcall (fname, _args) -> *)
- | Pmetavar _ -> newMetavar t + | Pmetavar (l,"") -> newMetavar l "v" t + | Pmetavar (l, name) + -> pexp_error l p "Named metavars not supported (yet)"; + newMetavar l name t
| _ -> infer_and_check p ctx t
@@ -598,7 +618,6 @@ and infer_call (func: pexp) (sargs: sexp list) ctx =
(* retrieve function's body (sqr 3) sqr is a Pvar() *) let body, ltp = infer func ctx in - let ltp = nosusp ltp in
let rec handle_fun_args largs sargs pending ltp = let ltp' = OL.lexp_whnf ltp (ectx_to_lctx ctx) meta_ctx in @@ -651,16 +670,18 @@ and infer_call (func: pexp) (sargs: sexp list) ctx = let larg = check parg arg_type ctx in handle_fun_args ((Aexplicit, larg) :: largs) sargs pending (L.mkSusp ret_type (S.substitute larg)) - | sarg :: sargs, Arrow (kind, _, arg_type, _, ret_type) - -> let larg = newMetavar arg_type in + | sarg :: sargs, Arrow (kind, v, arg_type, _, ret_type) + -> let larg = newMetavar (sexp_location sarg) + (match v with Some (_, name) -> name | _ -> "v") + arg_type in handle_fun_args ((kind, larg) :: largs) (sarg::sargs) pending (L.mkSusp ret_type (S.substitute larg))
| sarg :: sargs, t -> print_lexp_ctx (ectx_to_lctx ctx); lexp_fatal (sexp_location sarg) t - ("Explicit arg `" ^ sexp_string sarg ^ - "` to non-function (type = " ^ lexp_string ltp ^ ")") in + ("Explicit arg `" ^ sexp_string sarg + ^ "` to non-function (type = " ^ lexp_string ltp ^ ")") in
let handle_funcall () = (* Here we use lexp_whnf on actual code, but it's OK
===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -170,69 +170,67 @@ 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' + e1' == e2' || + 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 + match if stop1 || stop2 then (e1, e2) else (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_erase || 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_erase && ak1 = P.Aerasable || 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
let conv_p meta_ctx (ctx : DB.lexp_context) e1 e2 = if e1 == e2 then true
===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -95,7 +95,8 @@ let rec pexp_parse (s : sexp) : pexp = | Epsilon -> (internal_error "Epsilon in pexp_parse") | (Block _ | Integer _ | Float _ | String _) -> Pimm s (* | Symbol (l, "Type") -> Psort (l, Type) *) - | Symbol ((_, "_") as s) -> Pmetavar s + | Symbol (l, name) when String.length name > 0 && String.get name 0 == '?' + -> Pmetavar (l, String.sub name 1 (String.length name - 1)) | Symbol s -> Pvar s | Node (Symbol (start, "_:_"), [e; t]) -> Phastype (start, pexp_parse e, pexp_parse t)
===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -332,6 +332,11 @@ let _ = test_eval_eqv_named
"7; 13; 5; 7; 7"
+let _ = test_eval_eqv_named "Metavars" + "f : ?; + f x = 2 + f (1 + x);" + + "1" "1"
let _ = test_eval_eqv_named "Implicit Arguments"
===================================== tests/inverse_test.ml ===================================== --- a/tests/inverse_test.ml +++ b/tests/inverse_test.ml @@ -150,7 +150,7 @@ let _ = generate_tests "INVERSION" fmt_res (fun (s, b) -> ( match inverse s with | Some (s') -> (let comp = scompose s s' in - let ret = (is_identity comp) in + let ret = is_identity comp in let str = (subst_string s, subst_string s', subst_string comp) in (str, ret)) @@ -169,7 +169,7 @@ let _ = generate_tests "INVERSION-RAND" fmt_res (fun (s) -> ( match inverse s with | Some (s') -> (let comp = scompose s s' in - let ret = (is_identity comp) in + let ret = is_identity comp in let str = (subst_string s, subst_string s', subst_string comp) in
View it on GitLab: https://gitlab.com/monnier/typer/commit/108275af4dfe8ce4a85616e4e7ca8f1ed1b2...
Afficher les réponses par date