Stefan pushed to branch master at Stefan / Typer

Commits: 8396dc22 by Stefan Monnier at 2016-11-29T13:31:20-05:00 Make `Builtin`s be closed and available via ##... syntax

* src/builtin.ml (type_eq, olist2tlist_lexp): Add missing hashconsing.

* src/lexp.ml (mkSusp): Don't make a susp for Builtins. (push_susp): Builtins are closed, so there's nothing to push anything. (eq, subst_eq): New functions.

* src/lparse.ml (newMetalevel): Add missing hashconsing. (sform_built_in, sform_new_attribute): Close type of builtin. (sform_built_in): Add to BI.lmap so it's available via the ##... syntax. (sform_add_attribute): Close attr before adding it to table.

* src/opslexp.ml (lctx_to_subst, lexp_close): New functions. (set_plexp): Rename from set_lexp, change it to hold pairs. (set_member_p, set_add): Rewrite. (conv_p'): Use a set of hypothetical equalities to break inf-loops. Add missing hashconsing. * src/unification.ml (unify'): Mirror change in OL.conv_p'.

- - - - -

6 changed files:

- DESIGN - src/builtin.ml - src/lexp.ml - src/lparse.ml - src/opslexp.ml - src/unification.ml

Changes:

===================================== DESIGN ===================================== --- a/DESIGN +++ b/DESIGN @@ -998,26 +998,6 @@ the recursive calls. (e.g. that need to know the set of freevars in one of its arguments) are "impossible" unless Typer provides extra support for them. * Syntax -** Lexical rules -Tokens will be made of any sequence of letters other than blanks/comments. - - blanks = LF, CR, TAB, SPC - comments = %...\n - strings = "...?..." - numbers = as standard as possible - maybe handle \ specially not only in strings but anywhere else as well - special token = sequence of chars which is always treated as a single - token even if it's not surrounded by blanks. The set of special tokens - can be extended by the programmer. - magic token = the _ char is magical in that it forcefully connects even - special tokens: a(b are 3 tokens if ( is special, but a_(_b is a single - (magic) token. - -** Structured identifiers -We want to support identifiers with inner structure, such as "foo.bar.baz". - -This could be lexed into a Node identical to that of ( __.__ foo bar baz) - ** Provide syntax for backquote&unquote Since "," is to be used as separator, maybe (,e) and (`e) could be used? ** Macros

===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -118,17 +118,19 @@ let dump_predef () = (* Builtin types *) let dloc = DB.dloc

-let op_binary t = Arrow (Aexplicit, None, t, dloc, - Arrow (Aexplicit, None, t, dloc, t)) +let op_binary t = mkArrow (Aexplicit, None, t, dloc, + mkArrow (Aexplicit, None, t, dloc, t))

let type_eq = let lv = (dloc, "l") in let tv = (dloc, "t") in - Arrow (Aerasable, Some lv, DB.type_level, dloc, - Arrow (Aerasable, Some tv, - Sort (dloc, Stype (Var (lv, 0))), dloc, - Arrow (Aexplicit, None, Var (tv, 0), dloc, - Arrow (Aexplicit, None, Var (tv, 1), dloc, - DB.type0)))) + mkArrow (Aerasable, Some lv, + DB.type_level, dloc, + mkArrow (Aerasable, Some tv, + mkSort (dloc, Stype (Var (lv, 0))), dloc, + mkArrow (Aexplicit, None, Var (tv, 0), dloc, + mkArrow (Aexplicit, None, + mkVar (tv, 1), dloc, + DB.type0))))

(* lexp Imm list *) @@ -138,8 +140,8 @@ let olist2tlist_lexp lst ctx =

let rlst = List.rev lst in List.fold_left (fun tail elem -> - Call(tcons, [(Aexplicit, (Imm(elem))); - (Aexplicit, tail)])) tnil rlst + mkCall(tcons, [(Aexplicit, (Imm(elem))); + (Aexplicit, tail)])) tnil rlst

(* typer list as seen during runtime *) let olist2tlist_rte lst = @@ -193,5 +195,5 @@ let builtins =

let _ = new_builtin_type "Sexp" DB.type0 let _ = new_builtin_type - "IO" (Arrow (Aexplicit, None, DB.type0, dloc, DB.type0)) + "IO" (mkArrow (Aexplicit, None, DB.type0, dloc, DB.type0)) let _ = new_builtin_type "FileHandle" DB.type0

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -168,6 +168,7 @@ let rec mkSusp e s = match e with (* FIXME: `Builtin` shouuld be treated like `Imm`. *) | Imm _ -> e + | 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) @@ -211,11 +212,7 @@ let rec push_susp e s = (* Push a suspension one level down. *) | SortLevel (SLsucc e') -> mkSortLevel (SLsucc (mkSusp e' s)) | Sort (l, Stype e) -> mkSort (l, Stype (mkSusp e s)) | Sort (l, _) -> e - | Builtin (l, ltp, otable) - -> let otable' = match otable with - | Some table -> Some (AttributeMap.map (fun lxp -> mkSusp lxp s) table) - | _ -> None in - mkBuiltin (l, (mkSusp ltp s), otable') + | Builtin _ -> e

| Let (l, defs, e) -> let s' = L.fold_left (fun s (v, _, _) -> ssink v s) s defs in @@ -693,3 +690,73 @@ and _lexp_str_decls ctx decls = (name ^ " = " ^ (lexp_to_str lxp) ^ ";" ^ sepdecl)::str) [] decls in List.rev ret + +(** Syntactic equality (i.e. without β). *******) + +let rec eq meta_ctx 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 + | (Imm (String (_, s1)), Imm (String (_, s2))) -> s1 = s2 + | (Imm s1, Imm s2) -> s1 = s2 + | (SortLevel SLz, SortLevel SLz) -> true + | (SortLevel (SLsucc e1), SortLevel (SLsucc e2)) -> eq e1 e2 + | (Sort (_, StypeOmega), Sort (_, StypeOmega)) -> true + | (Sort (_, StypeLevel), Sort (_, StypeLevel)) -> true + | (Sort (_, Stype e1), Sort (_, Stype e2)) -> eq e1 e2 + | (Builtin ((_, name1), _, _), Builtin ((_, name2), _, _)) -> name1 = name2 + | (Var (_, i1), Var (_, i2)) -> i1 = i2 + | (Susp (e1, s1), e2) -> eq (push_susp e1 s1) e2 + | (e1, Susp (e2, s2)) -> eq e1 (push_susp e2 s2) + | (Let (_, defs1, e1), Let (_, defs2, e2)) + -> eq e1 e2 && List.for_all2 (fun (_, e1, t1) (_, e2, t2) + -> eq t1 t2 && eq e1 e2) + defs1 defs2 + | (Arrow (ak1, _, t11, _, t21), Arrow (ak2, _, t12, _, t22)) + -> ak1 = ak2 && eq t11 t12 && eq t21 t22 + | (Lambda (ak1, _, t1, e1), Lambda (ak2, _, t2, e2)) + -> ak1 = ak2 && eq t1 t2 && eq e1 e2 + | (Call (e1, as1), Call (e2, as2)) + -> eq e1 e2 && List.for_all2 (fun (ak1, e1) (ak2, e2) -> ak1 = ak2 && eq e1 e2) + as1 as2 + | (Inductive (_, l1, as1, cases1), Inductive (_, l2, as2, cases2)) + -> l1 = l2 + && List.for_all2 (fun (ak1, _, e1) (ak2, _, e2) -> ak1 = ak2 && eq e1 e2) + as1 as2 + && SMap.equal (List.for_all2 (fun (ak1, _, e1) (ak2, _, e2) + -> ak1 = ak2 && eq e1 e2)) + cases1 cases2 + | (Cons (t1, (_, l1)), Cons (t2, (_, l2))) -> eq t1 t2 && l1 = l2 + | (Case (_, e1, r1, cases1, def1), Case (_, e2, r2, cases2, def2)) + -> eq e1 e2 && eq r1 r2 + && SMap.equal (fun (_, fields1, e1) (_, fields2, e2) + -> eq e1 e2 && List.for_all2 (fun (ak1, _) (ak2, _) + -> ak1 = ak2) + fields1 fields2) + cases1 cases2 + && (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 meta_ctx s1 s2 + | _ -> false + +and subst_eq meta_ctx 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 + | (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)) + | (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 + | (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) + | _ -> false +

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -237,7 +237,7 @@ let newMetavar l name t = mkMetavar (meta, S.Identity, (l, name), t)

let newMetalevel () = - newMetavar Util.dummy_location "l" (Sort (dummy_location, StypeLevel)) + newMetavar Util.dummy_location "l" (mkSort (dummy_location, StypeLevel))

let newMetatype () = newMetavar Util.dummy_location "t" (newMetalevel ())

@@ -770,21 +770,21 @@ and infer_call (func: pexp) (sargs: sexp list) ctx = let parg = pexp_parse lsarg in let larg = check parg arg_type ctx in

- handle_fun_args ((Aimplicit, larg) :: largs) (sarg::sargs) pending - (L.mkSusp ret_type (S.substitute larg))) + handle_fun_args ((Aimplicit, larg) :: largs) (sarg::sargs) pending + (L.mkSusp ret_type (S.substitute larg))) (* Aerasable *) | sarg :: sargs, Arrow (Aerasable, v, arg_type, _, ret_type) -> let larg = newMetavar (sexp_location sarg) - (match v with Some (_, name) -> name | _ -> "v") - arg_type in - handle_fun_args ((Aerasable, larg) :: largs) (sarg::sargs) pending - (L.mkSusp ret_type (S.substitute larg)) + (match v with Some (_, name) -> name | _ -> "v") + arg_type in + handle_fun_args ((Aerasable, 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 + | 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

let handle_funcall () = let largs, ret_type = handle_fun_args [] sargs SMap.empty ltp in @@ -1002,14 +1002,17 @@ and lexp_parse_sexp (ctx: elab_context) (e : sexp) : lexp = * -------------------------------------------------------------------------- *)

and sform_new_attribute ctx loc sargs = - let ltp = match sargs with - | [t] -> lexp_parse_sexp ctx t - | _ -> fatal loc "new-attribute expects a single Type argument" 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. *) - Builtin ((loc, "new-attribute"), ltp, Some AttributeMap.empty) + match sargs with + | [t] -> let ptp = pexp_parse t in + let ltp = infer_type ptp 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, + Some AttributeMap.empty) + | _ -> fatal loc "new-attribute expects a single Type argument"

and sform_add_attribute ctx loc (sargs : sexp list) = let n = get_size ctx in @@ -1018,13 +1021,14 @@ and sform_add_attribute ctx loc (sargs : sexp list) = | _ -> 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 - | Builtin (_, attr_type, Some map)-> map, attr_type + let map, attr_type = match OL.lexp_whnf table (ectx_to_lctx ctx) meta_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 table = AttributeMap.add var attr map in - Builtin ((loc, "add-attribute"), attr_type, Some table) + (* FIXME: Type check (attr: type == attr_type) *) + let attr' = OL.lexp_close meta_ctx (ectx_to_lctx ctx) attr in + let table = AttributeMap.add var attr' map in + mkBuiltin ((loc, "add-attribute"), attr_type, Some table)

and get_attribute ctx loc largs = let ctx_n = get_size ctx in @@ -1079,10 +1083,14 @@ let sform_decltype ctx loc sargs =

let sform_built_in ctx loc sargs = match !_parsing_internals, sargs with - | true, [String (_, str); stp] -> - let ptp = pexp_parse stp in - let ltp, _ = infer ptp ctx in - mkBuiltin((loc, str), ltp, None) + | true, [String (_, name); stp] + -> let ptp = pexp_parse stp in + let ltp = infer_type ptp ctx None in + let meta_ctx, _ = !global_substitution in + let ltp' = OL.lexp_close meta_ctx (ectx_to_lctx ctx) ltp in + let bi = mkBuiltin ((loc, name), ltp', None) in + BI.add_builtin_cst name bi; + bi

| true, _ -> error loc "Wrong Usage of `Built-in`"; dlxp

===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -69,7 +69,49 @@ let rec lexp_defs_subst l s defs = match defs with | (_, lexp, _) :: defs' -> lexp_defs_subst l (S.cons (mkLet (l, defs, lexp)) s) defs'

-(* Reduce to weak head normal form. +(** Convert a lexp_context into a substitution. *) + +let rec lctx_to_subst lctx = + match lctx with + | Myers.Mnil -> Subst.identity + | Myers.Mcons ((0, _, LetDef e, _), lctx, _, _) + -> let s = lctx_to_subst lctx in + L.scompose (S.substitute e) s + | Myers.Mcons ((0, ov, _, _), lctx, _, _) + -> let s = lctx_to_subst lctx in + (* Here we decide to keep those vars in the target domain. + * Another option would be to map them to `L.impossible`, + * hence making the target domain be empty (i.e. making the substitution + * generate closed results). *) + L.ssink (maybev ov) s + | Myers.Mcons ((1, ov, LetDef e, t), lctx, _, _) + -> let rec getdefs i lctx rdefs = + match lctx with + | Myers.Mcons ((o, ov, LetDef e, t), lctx, _, _) + when o = i + -> getdefs (i + 1) lctx ((maybev ov, e, t) :: rdefs) + | _ -> (lctx, List.rev rdefs) in + let (lctx, defs) = getdefs 2 lctx [(maybev ov, e, t)] in + let s1 = lctx_to_subst lctx in + let s2 = lexp_defs_subst DB.dloc S.identity defs in + L.scompose s2 s1 + | _ -> U.internal_error "Unexpected lexp_context shape!" + +(* Take an expression `e` that is "closed" relatively to context 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 = + (* 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)) + + +(** Reduce to weak head normal form. * WHNF implies: * - Not a Let. * - Not a let-bound variable. @@ -146,38 +188,39 @@ let lexp_whnf e (ctx : DB.lexp_context) meta_ctx : lexp = 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 +(** 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 + = 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') + 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)); *) + ((e1, e2) :: s) +let set_shift_n (s : set_plexp) (n : U.db_offset) + = List.map (let s = S.shift n in + fun (e1, e2) -> (Lexp.push_susp e1 s, Lexp.push_susp e2 s)) + s +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_lexp) e1 e2 : bool = +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 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 changed = not (e1 == e1' && e2 == e2') in + if changed && set_member_p meta_ctx 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 if stop1 || stop2 then (e1, e2) else (e1', e2') with + 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 @@ -301,14 +344,15 @@ let rec check' meta_ctx erased ctx e = | Sort (l, Stype e) -> let t = check erased ctx e in assert_type ctx e t DB.type_level; - Sort (l, Stype (SortLevel (SLsucc e))) + mkSort (l, Stype (mkSortLevel (SLsucc e))) | Sort (_, StypeLevel) -> DB.sort_omega | Sort (_, StypeOmega) -> (U.msg_error "TC" (lexp_location e) "Reached unreachable sort!"; (* U.internal_error "Reached unreachable sort!"; *) DB.sort_omega) | Builtin (_, t, _) - -> check_type DB.set_empty ctx t; (* FIXME: Use an empty ctx? *) + -> let _ = check_type DB.set_empty Myers.nil t in + (* FIXME: Check the attributemap as well! *) t (* FIXME: Check recursive references. *) | Var (((_, name), idx) as v) @@ -347,22 +391,22 @@ let rec check' meta_ctx erased ctx e = (* FIXME: fix scoping of `k2` and `s2`. *) -> if ak == P.Aerasable && impredicative_erase && s1 != StypeLevel then k2 - else Sort (l, sort_compose l s1 s2) + else mkSort (l, sort_compose l s1 s2) | (Sort (_, _), _) -> (U.msg_error "TC" (lexp_location t2) "Not a proper type"; - Sort (l, StypeOmega)) + mkSort (l, StypeOmega)) | (_, _) -> (U.msg_error "TC" (lexp_location t1) "Not a proper type"; - Sort (l, StypeOmega))) + mkSort (l, StypeOmega))) | Lambda (ak, ((l,_) as v), t, e) -> ((match lexp_whnf (check_type DB.set_empty ctx t) ctx meta_ctx with | Sort _ -> () | _ -> (U.msg_error "TC" (lexp_location t) "Formal arg type is not a type!"; ())); - Arrow (ak, Some v, t, l, - check (dbset_push ak erased) - (DB.lctx_extend ctx (Some v) Variable t) - e)) + mkArrow (ak, Some v, t, l, + check (dbset_push ak erased) + (DB.lctx_extend ctx (Some v) Variable t) + e)) | Call (f, args) -> let ft = check erased ctx f in List.fold_left @@ -414,10 +458,10 @@ let rec check' meta_ctx erased ctx e = case in level) cases (mkSortLevel SLz) in - Sort (l, Stype level) + mkSort (l, Stype level) | (ak, v, t)::args - -> Arrow (ak, Some v, t, lexp_location t, - arg_loop args (DB.lctx_extend ctx (Some v) Variable t)) in + -> mkArrow (ak, Some v, t, lexp_location t, + arg_loop args (DB.lctx_extend ctx (Some v) Variable t)) in let tct = arg_loop args ctx in tct | Case (l, e, ret, branches, default) @@ -489,15 +533,15 @@ let rec check' meta_ctx erased ctx e = let rec fieldargs ftypes = match ftypes with | [] -> let nargs = List.length fieldtypes + List.length fargs in - Call (mkSusp t (S.shift nargs), indtype fargs (nargs - 1)) + mkCall (mkSusp t (S.shift nargs), indtype fargs (nargs - 1)) | (ak, vd, ftype) :: ftypes - -> Arrow (ak, vd, ftype, lexp_location ftype, - fieldargs ftypes) in + -> mkArrow (ak, vd, ftype, lexp_location ftype, + fieldargs ftypes) in let rec buildtype fargs = match fargs with | [] -> fieldargs fieldtypes | (ak, ((l,_) as vd), atype) :: fargs - -> Arrow (P.Aerasable, Some vd, atype, l, + -> mkArrow (P.Aerasable, Some vd, atype, l, buildtype fargs) in buildtype fargs | _ -> (U.msg_error "TC" (lexp_location e)

===================================== src/unification.ml ===================================== --- a/src/unification.ml +++ b/src/unification.ml @@ -87,16 +87,14 @@ let rec unify (e1: lexp) (e2: lexp) unify' e1 e2 ctx OL.set_empty subst

and unify' (e1: lexp) (e2: lexp) - (ctx : DB.lexp_context) (vs : OL.set_lexp) (subst: meta_subst) + (ctx : DB.lexp_context) (vs : OL.set_plexp) (subst: meta_subst) : return_type = let e1' = OL.lexp_whnf e1 ctx subst in let e2' = OL.lexp_whnf e2 ctx subst in - let stop1 = not (e1 == e1') && OL.set_member_p vs e1' in - let stop2 = not (e2 == e2') && OL.set_member_p vs e2' in - let vs' = if not (e1 == e1') && not stop1 then OL.set_add vs e1' - else if not (e2 == e2') && not stop2 then OL.set_add vs e2' - else vs in - match if stop1 || stop2 then (e1, e2) else (e1', e2') with + let changed = not (e1 == e1' && e2 == e2') in + if changed && OL.set_member_p subst vs e1' e2' then Some (subst, []) 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

View it on GitLab: https://gitlab.com/monnier/typer/commit/8396dc22616f8cb9b6aa501a5a5d6ebfaa4a...