Alice de Berny pushed to branch alice at Stefan / Typer
Commits: 3376edac by irradiee at 2020-06-05T10:14:41-04:00 correction physical equality of lexp
- - - - -
4 changed files:
- src/elab.ml - src/lexp.ml - src/opslexp.ml - src/unification.ml
Changes:
===================================== src/elab.ml ===================================== @@ -1009,7 +1009,7 @@ and lexp_parse_inductive ctors ctx = -> hc (Arrow (Aerasable, vname, t, l, e))) altacc in - if lexp_lexp' altacc' == lexp_lexp' altacc + if altacc' == altacc then acc (* No generalization! *) else (* Convert the Lexp back into a list of fields. *)
===================================== src/lexp.ml ===================================== @@ -188,6 +188,15 @@ let metavar_lookup (id : meta_id) : metavar_info | e :: l -> e lxor (apply_lxor l)
let combine_hash e1 e2 = e1 lxor e2 + +let smap_hash e smap = + (combine_hash + (apply_lxor + (List.map (fun e -> let (ak, n, lt) = e in + (combine_hash (Hashtbl.hash ak) + (combine_hash (Hashtbl.hash n) (lexp_hash lt)))) + e)) (Hashtbl.hash smap)) + (* Hashtbl.hash for not lexp types * TODO: - find something else * - extract the first arg of 2 arg types ? (SMap)*) @@ -238,14 +247,11 @@ let combine_hash e1 e2 = e1 lxor e2 (combine_hash (Hashtbl.hash ak) (lexp_hash lp))) args)) | Susp (lp, subst) -> combine_hash (lexp_hash lp) (Hashtbl.hash subst)
-let impossible = (let imp = Imm Sexp.dummy_epsilon in (imp, dummy_hash)) - let compare_hash x y = let (x', h1) = x in let (y', h2) = y in compare h1 h2 = 0
-(* May be a tree ? *) module WHC = Weak.Make (struct type t = lexp (* Using (=) instead of `compare` results * in an *enormous* slowdown. Apparently @@ -259,6 +265,8 @@ let hc_table : WHC.t = WHC.create 1000 let hc (e : lexp') : lexp = let lp = (e, lexp'_hash e) in WHC.merge hc_table lp
+let impossible = hc (Imm Sexp.dummy_epsilon) + let mkImm s = hc (Imm s) let mkSortLevel l = hc (SortLevel l) let mkSort (l, s) = hc (Sort (l, s)) @@ -1040,10 +1048,8 @@ and lexp_str_decls ctx decls = (** Syntactic equality (i.e. without β). *******)
let rec eq e1 e2 = - let e1' = lexp_lexp' e1 in - let e2' = lexp_lexp' e2 in - e1' == e2' || - match (e1', e2') with + e1 == e2 || + match (lexp_lexp' e1, lexp_lexp' 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
===================================== src/opslexp.ml ===================================== @@ -211,8 +211,8 @@ let lexp_whnf e (ctx : DB.lexp_context) : lexp = type set_plexp = (lexp * lexp) list let set_empty : set_plexp = [] let set_member_p (s : set_plexp) (e1 : lexp) (e2 : lexp) : bool - = assert (lexp_lexp' e1 == lexp_lexp' (Lexp.hc (lexp_lexp' e1))); - assert (lexp_lexp' e2 == lexp_lexp' (Lexp.hc (lexp_lexp' e2))); + = assert (e1 == Lexp.hc (lexp_lexp' e1)); + assert (e2 == Lexp.hc (lexp_lexp' e2)); try let _ = List.find (fun (e1', e2') -> L.eq e1 e1' && L.eq e2 e2') s @@ -266,14 +266,12 @@ let level_leq (c1, m1) (c2, m2) = 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 - let e1'' = lexp'_whnf e1 ctx in - let e2'' = lexp'_whnf e2 ctx in - e1'' == e2'' || - let changed = not (lexp_lexp' e1 == e1'' && lexp_lexp' e2 == e2'') in + e1' == e2' || + let changed = not (e1 == e1' && e2 == e2') in 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 + match (lexp_lexp' e1', lexp_lexp' 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 @@ -331,7 +329,7 @@ let rec conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = (set_shift vs) args1 args2 | _,_ -> false in - lexp_lexp' l1 == lexp_lexp' l2 && conv_args ctx vs' args1 args2 + l1 == l2 && conv_args ctx vs' args1 args2 | (Cons (t1, (_, l1)), Cons (t2, (_, l2))) -> l1 = l2 && conv_p t1 t2 (* I'm not sure to understand how to compare two Metavar * * Should I do a `lookup`? Or is it that simple: *) @@ -340,7 +338,7 @@ let rec conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = | (_, _) -> false
let conv_p (ctx : DB.lexp_context) e1 e2 - = if lexp_lexp' e1 == lexp_lexp' e2 then true + = if e1 == e2 then true else conv_p' ctx set_empty e1 e2
(********* Testing if a lexp is properly typed *********)
===================================== src/unification.ml ===================================== @@ -184,30 +184,28 @@ let rec unify (e1: lexp) (e2: lexp) and unify' (e1: lexp) (e2: lexp) (ctx : DB.lexp_context) (vs : OL.set_plexp) : return_type = - if lexp_lexp' e1 == lexp_lexp' e2 then [] else + if e1 == e2 then [] else let e1' = OL.lexp_whnf e1 ctx in let e2' = OL.lexp_whnf e2 ctx in - let e1'' = lexp_lexp' e1' in - let e2'' = lexp_lexp' e2' in - if e1'' == e2'' then [] else + if e1' == e2' then [] else let changed = true (* not (e1 == e1' && e2 == e2') *) in if changed && OL.set_member_p vs e1' e2' then [] else let vs' = if changed then OL.set_add vs e1' e2' else vs in - match (e1'', e2'') with + match (lexp_lexp' e1', lexp_lexp' e2') with | ((Imm _, Imm _) | (Cons _, Cons _) | (Builtin _, Builtin _) | (Var _, Var _)) -> if OL.conv_p ctx e1' e2' then [] else [(CKimpossible, ctx, e1, e2)] - | (l, (Metavar (idx, s, _) as r)) -> unify_metavar ctx idx s e2' e1' - | ((Metavar (idx, s, _) as l), r) -> unify_metavar ctx idx s e1' e2' - | (l, (Call _ as r)) -> unify_call e2' e1' ctx vs' + | (_, Metavar (idx, s, _)) -> unify_metavar ctx idx s e2' e1' + | (Metavar (idx, s, _), _) -> unify_metavar ctx idx s e1' e2' + | (_, Call _) -> unify_call e2' e1' ctx vs' (* | (l, (Case _ as r)) -> unify_case r l subst *) - | (Arrow _ as l, r) -> unify_arrow e1' e2' ctx vs' - | (Lambda _ as l, r) -> unify_lambda e1' e2' ctx vs' - | (Call _ as l, r) -> unify_call e1' e2' ctx vs' + | (Arrow _ , _) -> unify_arrow e1' e2' ctx vs' + | (Lambda _, _) -> unify_lambda e1' e2' ctx vs' + | (Call _, _) -> unify_call e1' e2' 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 e1' e2' ctx vs' - | (SortLevel _ as l, r) -> unify_sortlvl e1' e2' ctx vs' + | (Sort _, _) -> unify_sort e1' e2' ctx vs' + | (SortLevel _, _) -> unify_sortlvl e1' e2' ctx vs' | (Inductive (_loc1, label1, args1, consts1), Inductive (_loc2, label2, args2, consts2)) -> (* print_string ("Unifying inductives "
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/3376edace9286d4aff35fb4f87be0628e8...