- ported to typed explicit subst

- beta expansion in the case of Appl commented, waiting for a better
  solution

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index cebbb9e8f68d2bc1fadc45f2fbca438fad2bf617..63abdfb012a2dca27af1e9eaa11d022aca63c0a9 100644 (file)
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -59,6 +59,7 @@ let type_of_aux' metasenv subst context term =
         (CicMetaSubst.ppmetasenv metasenv subst) msg))) *)
 
 let rec deref subst =
+  let snd (_,a,_) = a in
   function
       Cic.Meta(n,l) as t -> 
        (try 
@@ -241,6 +242,9 @@ and fo_unif_subst test_equality_only subst context metasenv t1 t2 =
  let module S = CicSubstitution in
  let t1 = deref subst t1 in
  let t2 = deref subst t2 in
+ if R.are_convertible ~subst ~metasenv context t1 t2 then
+   subst, metasenv
+ else
   match (t1, t2) with
      (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
        let _,subst,metasenv =
@@ -346,14 +350,14 @@ prerr_endline ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (str
         in
         (* Unifying the types may have already instantiated n. Let's check *)
         try
-          let (_, oldt) = CicUtil.lookup_subst n subst in
+          let (_, oldt,_) = CicUtil.lookup_subst n subst in
           let lifted_oldt = S.lift_meta l oldt in
             fo_unif_subst_ordered 
               test_equality_only subst context metasenv t lifted_oldt
         with
             CicUtil.Subst_not_found _ -> 
-              let (_, context, _) = CicUtil.lookup_meta n metasenv in
-              let subst = (n, (context, t'')) :: subst in
+              let (_, context, ty) = CicUtil.lookup_meta n metasenv in
+              let subst = (n, (context, t'',ty)) :: subst in
               let metasenv =
                 List.filter (fun (m,_,_) -> not (n = m)) metasenv in
               subst, metasenv
@@ -421,6 +425,8 @@ prerr_endline ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (str
                    beta_reduce (Cic.Appl(he''::tl'))
            | t -> t in
         (match l1,l2 with
+(* andrea : this was too powerful. It works very bad with f_equal and
+   similar terms, try and see 
            C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
              (try 
                List.fold_left2 
@@ -430,7 +436,7 @@ prerr_endline ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (str
              with (Invalid_argument msg) -> raise (UnificationFailure msg)) 
          | C.Meta (i,l)::args, _ ->
             (try 
-              let (_,t) = CicUtil.lookup_subst i subst in
+              let (_,t,_) = CicUtil.lookup_subst i subst in
               let lifted = S.lift_meta l t in
                let reduced = beta_reduce (Cic.Appl (lifted::args)) in
               fo_unif_subst 
@@ -444,7 +450,7 @@ prerr_endline ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (str
                 (C.Meta (i,l)) beta_expanded) 
          | _, C.Meta (i,l)::args ->
             (try 
-              let (_,t) = CicUtil.lookup_subst i subst in
+              let (_,t,_) = CicUtil.lookup_subst i subst in
               let lifted = S.lift_meta l t in
                let reduced = beta_reduce (Cic.Appl (lifted::args)) in
               fo_unif_subst 
@@ -456,6 +462,7 @@ prerr_endline ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (str
                   test_equality_only metasenv subst context t1 args in
                fo_unif_subst test_equality_only subst context metasenv 
                 (C.Meta (i,l)) beta_expanded)
+*)
          | _,_ ->
             let lr1 = List.rev l1 in
              let lr2 = List.rev l2 in

diff --git a/helm/ocaml/cic_unification/cicUnification.mli b/helm/ocaml/cic_unification/cicUnification.mli
index 9956b304378c40d7769378fafd5ffbf344de6855..9d26fd3dfc4e7151cec571e0b13d7401e0a05b89 100644 (file)
--- a/helm/ocaml/cic_unification/cicUnification.mli
+++ b/helm/ocaml/cic_unification/cicUnification.mli
@@ -35,7 +35,7 @@ exception AssertFailure of string;;
 (* withouth first unwinding it.                  *)
 val fo_unif :
   Cic.metasenv -> Cic.context -> Cic.term -> Cic.term ->
-   CicMetaSubst.substitution * Cic.metasenv
+   Cic.substitution * Cic.metasenv
 
 (* fo_unif_subst metasenv subst context t1 t2    *)
 (* unifies [t1] and [t2] in a context [context]  *)
@@ -51,7 +51,7 @@ val fo_unif :
 (*CSC: fare un tipo unione Unwinded o ToUnwind e fare gestire la
  cosa all'apply_subst!!!*)
 val fo_unif_subst :
-  CicMetaSubst.substitution ->
+  Cic.substitution ->
   Cic.context -> Cic.metasenv -> Cic.term -> Cic.term ->
-   CicMetaSubst.substitution * Cic.metasenv
+   Cic.substitution * Cic.metasenv