notation support fixed to parentesize in a more sane way and

[helm.git] / helm / software / components / cic_unification / cicUnification.ml

diff --git a/helm/software/components/cic_unification/cicUnification.ml b/helm/software/components/cic_unification/cicUnification.ml
index fb6a66d4fc5c8cb6969353d90b49c1409635cf91..517c013d42b2ac4ffcb6fe7973725561d0fa01da 100644 (file)
--- a/helm/software/components/cic_unification/cicUnification.ml
+++ b/helm/software/components/cic_unification/cicUnification.ml
@@ -197,15 +197,17 @@ let foo () =
            in
            (* TASSI: sure this is in serial? *)
             subst,metasenv,(C.Lambda (nn, s', t')),ugraph2
-        | C.LetIn (nn,s,t) ->
+        | C.LetIn (nn,s,ty,t) ->
            let subst,metasenv,s',ugraph1 = 
              aux metasenv subst n context s ugraph in
+           let subst,metasenv,ty',ugraph1 = 
+             aux metasenv subst n context ty ugraph in
            let subst,metasenv,t',ugraph2 =
-            aux metasenv subst (n+1) ((Some (nn, C.Def (s,None)))::context) t
+            aux metasenv subst (n+1) ((Some (nn, C.Def (s,ty)))::context) t
               ugraph1
            in
            (* TASSI: sure this is in serial? *)
-            subst,metasenv,(C.LetIn (nn, s', t')),ugraph2
+            subst,metasenv,(C.LetIn (nn, s', ty', t')),ugraph2
         | C.Appl l ->
            let subst,metasenv,revl',ugraph1 =
             List.fold_left
@@ -316,11 +318,18 @@ and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph =
  let module S = CicSubstitution in
  let t1 = deref subst t1 in
  let t2 = deref subst t2 in
- let b,ugraph  = 
+ let (&&&) a b = (a && b) || ((not a) && (not b)) in
+(* let bef = Sys.time () in *)
+ let b,ugraph =
+  if not (CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t1) &&& CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t2)) then
+   false,ugraph
+  else
 let foo () =
    R.are_convertible ~subst ~metasenv context t1 t2 ugraph 
 in profiler_are_convertible.HExtlib.profile foo ()
  in
+(* let aft = Sys.time () in
+if (aft -. bef > 2.0) then prerr_endline ("LEEEENTO: " ^ CicMetaSubst.ppterm_in_context subst ~metasenv t1 context ^ " <===> " ^ CicMetaSubst.ppterm_in_context subst ~metasenv t2 context); *)
    if b then
      subst, metasenv, ugraph 
    else
@@ -496,20 +505,14 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
                               subst context metasenv te t2 ugraph
    | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only 
                               subst context metasenv t1 te ugraph
-   | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) -> 
-       let subst',metasenv',ugraph1 = 
-         fo_unif_subst true subst context metasenv s1 s2 ugraph 
-       in
-         fo_unif_subst test_equality_only 
-           subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
    | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) -> 
        let subst',metasenv',ugraph1 = 
          fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph 
        in
          fo_unif_subst test_equality_only 
            subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
-   | (C.LetIn (_,s1,t1), t2)  
-   | (t2, C.LetIn (_,s1,t1)) -> 
+   | (C.LetIn (_,s1,ty1,t1), t2)  
+   | (t2, C.LetIn (_,s1,ty1,t1)) -> 
        fo_unif_subst 
         test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
    | (C.Appl l1, C.Appl l2) -> 
@@ -758,28 +761,22 @@ res
                 subst context metasenv t1' t2 ugraph         
           | _ -> raise (UnificationFailure (lazy "8")))
 *)
-(* The following idea could be exploited again; right now we have no
-   longer any example requiring it
-   | (C.Prod _, t2) ->
-       let t2' = R.whd ~subst context t2 in
-       (match t2' with
-            C.Prod _ -> 
-              fo_unif_subst test_equality_only 
-                subst context metasenv t1 t2' ugraph         
-          | _ -> raise (UnificationFailure (lazy "8")))
-   | (t1, C.Prod _) ->
-       let t1' = R.whd ~subst context t1 in
-       (match t1' with
-            C.Prod _ -> 
-              fo_unif_subst test_equality_only 
-                subst context metasenv t1' t2 ugraph         
-          | _ -> (* raise (UnificationFailure "9")) *)
-             raise 
-                (UnificationFailure (lazy (sprintf
-                   "Can't unify %s with %s because they are not convertible"
-                   (CicMetaSubst.ppterm ~metasenv subst t1) 
-                   (CicMetaSubst.ppterm ~metasenv subst t2)))))
-*)
+   | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) -> 
+       let subst',metasenv',ugraph1 = 
+         fo_unif_subst true subst context metasenv s1 s2 ugraph 
+       in
+         fo_unif_subst test_equality_only 
+           subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
+   | (C.Prod _, _) ->
+       (match CicReduction.whd ~subst context t2 with
+        | C.Prod _ as t2 -> 
+            fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
+        | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t2^"Not a product"))))
+   | (_, C.Prod _) ->
+       (match CicReduction.whd ~subst context t1 with
+        | C.Prod _ as t1 -> 
+            fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
+        | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t1^"Not a product"))))
    | (_,_) ->
      (* delta-beta reduction should almost never be a problem for
         unification since: