Bugs fixed: unification were not really explicit-named-substitutions aware.

It just compiled.

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index 66c88e60f2e40f544cd077ae31c1fe1c17495b50..612931ed48d12f31d40e573330760d33df63644a 100644 (file)
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -79,7 +79,11 @@ let delift context metasenv l t =
              ignore (deliftaux k (S.lift m t)) ;
              C.Rel ((position (m-k) l) + k)
          | None -> raise RelToHiddenHypothesis)
-     | C.Var _  as t -> t
+     | C.Var (uri,exp_named_subst) ->
+        let exp_named_subst' =
+         List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
+        in
+         C.Var (uri,exp_named_subst')
      | C.Meta (i, l1) as t -> 
         let rec deliftl j =
          function
@@ -194,6 +198,26 @@ let rec fo_unif_subst subst context metasenv t1 t2 =
         List.find (function (m,_,_) -> m=n) metasenv' in
        let tyt = CicTypeChecker.type_of_aux' metasenv' context t in
         fo_unif_subst subst' context metasenv' (S.lift_meta l meta_type) tyt
+   | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
+   | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
+      if UriManager.eq uri1 uri2 then
+       fo_unif_subst_exp_named_subst subst context metasenv
+        exp_named_subst1 exp_named_subst2
+      else
+       raise UnificationFailed
+   | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
+      if UriManager.eq uri1 uri2 && i1 = i2 then
+       fo_unif_subst_exp_named_subst subst context metasenv
+        exp_named_subst1 exp_named_subst2
+      else
+       raise UnificationFailed
+   | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
+     C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
+      if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
+       fo_unif_subst_exp_named_subst subst context metasenv
+        exp_named_subst1 exp_named_subst2
+      else
+       raise UnificationFailed
    | (C.Rel _, _)
    | (_,  C.Rel _) 
    | (C.Var _, _)
@@ -264,6 +288,21 @@ let rec fo_unif_subst subst context metasenv t1 t2 =
        else
         raise UnificationFailed
    | (_,_) -> raise UnificationFailed
+
+and fo_unif_subst_exp_named_subst subst context metasenv
+ exp_named_subst1 exp_named_subst2
+=
+try
+ List.fold_left2
+  (fun (subst,metasenv) (uri1,t1) (uri2,t2) ->
+    assert (uri1=uri2) ;
+    fo_unif_subst subst context metasenv t1 t2
+  ) (subst,metasenv) exp_named_subst1 exp_named_subst2
+with
+e ->
+let uri = UriManager.uri_of_string "cic:/dummy.var" in
+prerr_endline ("@@@: " ^ CicPp.ppterm (Cic.Var (uri,exp_named_subst1)) ^
+" <==> " ^ CicPp.ppterm (Cic.Var (uri,exp_named_subst2))) ; raise e
 ;;
 
 (*CSC: ???????????????
@@ -399,9 +438,6 @@ let unwind metasenv subst unwinded t =
                let (_,canonical_context,_) = 
                 List.find (function (m,_,_) -> m=i) metasenv
                in
-prerr_endline ("DELIFT(" ^ CicPp.ppterm t' ^ ")") ; flush stderr ;
-List.iter (function (Some t) -> prerr_endline ("l: " ^ CicPp.ppterm t) | None -> prerr_endline " _ ") l ; flush stderr ;
-prerr_endline "<DELIFT" ; flush stderr ;
                 delift canonical_context metasenv' l t'
               in
                unwinded := (i,t')::!unwinded ;