[Git][monnier/typer][alice] correction physical equality of lexp - Typer

5 Jui 2020


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





    