From 16e2e2496f35a96c59e909133ff69767d37298aa Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 22 Oct 2004 12:16:22 +0000
Subject: [PATCH] - ported to typed explicit subst - beta expansion in the case
 of Appl commented, waiting for a better   solution

---
 helm/ocaml/cic_unification/cicUnification.ml  | 17 ++++++++++++-----
 helm/ocaml/cic_unification/cicUnification.mli |  6 +++---
 2 files changed, 15 insertions(+), 8 deletions(-)

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index cebbb9e8f..63abdfb01 100644
--- 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 9956b3043..9d26fd3df 100644
--- 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
 
-- 
2.39.2