added a duplicated implementation of replace lifting

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

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index a73313ebae5f6047de9f40d464493a39336b18fc..4c825c8a7313ac8385d85d8610520a0a1e84ba6a 100644 (file)
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -1359,6 +1359,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
   and coerce_to_something 
     allow_coercions localization_tbl t infty expty subst metasenv context ugraph
   =
+    let module CS = CicSubstitution in
     let coerce_atom_to_something t infty expty subst metasenv context ugraph =
       let coer = 
         CoercGraph.look_for_coercion metasenv subst context infty expty
@@ -1408,52 +1409,66 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
         if not allow_coercions || not !insert_coercions then
           enrich localization_tbl t exn
         else
-          let clean t subst context = 
-            CicReduction.whd 
-              ~delta:false context (CicMetaSubst.apply_subst subst t)
-          in
+          let whd = CicReduction.whd ~delta:false in
+          let clean t s c = whd c (CicMetaSubst.apply_subst s t) in
           let infty = clean infty subst context in
           let expty = clean expty subst context in
-          match infty, expty with
-          | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2) -> 
-              (* covariant part *)
+          match infty, expty, t with
+          | Cic.Prod (nameprod,src,ty), Cic.Prod (_,src2,ty2), Cic.Fix (n,fl) ->
+             (match fl with
+                 [name,i,_(* infty *),bo] ->
+                   let context_bo =
+                    Some (Cic.Name name,Cic.Decl expty)::context in
+                   let (rel1, _), subst, metasenv, ugraph =
+                    coerce_to_something_aux (Cic.Rel 1) expty infty subst
+                     metasenv context_bo ugraph in
+                   let bo =
+                    CS.subst ~avoid_beta_redexes:true rel1 (CS.lift_from 2 1 bo)
+                   in
+                   let (bo,_), subst, metasenv, ugraph =
+                    coerce_to_something_aux bo infty expty subst
+                     metasenv context_bo ugraph
+                   in
+                    (Cic.Fix (n,[name,i,expty,bo]),expty),subst,metasenv,ugraph
+               | _ -> assert false (* not implemented yet *)
+             )
+          | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2), _ -> 
               let name_con = Cic.Name "name_con" in
-              let name_t, ty_s_bo, bo = 
+              let context_src2 = (Some (name_con, Cic.Decl src2) :: context) in
+              (* contravariant part: the argument of f:src->ty *)
+              let (rel1, _), subst, metasenv, ugraph = 
+                coerce_to_something_aux
+                 (Cic.Rel 1) (CS.lift 1 src2) 
+                 (CS.lift 1 src) subst metasenv context_src2 ugraph
+              in
+              (* covariant part: the result of f(c x); x:src2; (c x):src *)
+              let name_t, bo = 
                 match t with
-                | Cic.Lambda (name, src, bo) -> name, src, bo
-                | _ -> name_con,src,Cic.Appl[CicSubstitution.lift 1 t;Cic.Rel 1]
+                | Cic.Lambda (n,_,bo) -> n, CS.subst rel1 (CS.lift_from 2 1 bo)
+                | _ -> name_con, Cic.Appl[CS.lift 1 t;rel1]
               in
-              let context_bo = (Some (name_t, Cic.Decl ty_s_bo)) :: context in
+              (* we fix the possible dependency problem in the source ty *)
+              let ty = CS.subst rel1 (CS.lift_from 2 1 ty) in
               let (bo, _), subst, metasenv, ugraph = 
                 coerce_to_something_aux
-                  bo ty ty2 subst metasenv context_bo ugraph
-              in
-              (* contravariant part *)
-              let context_rel1 = (Some (name_t, Cic.Decl src2) :: context) in
-              let (rel1, _), subst, metasenv, ugraph = 
-                coerce_to_something_aux
-                 (Cic.Rel 1) (CicSubstitution.lift 1 src2) 
-                 (CicSubstitution.lift 1 src) subst metasenv context_rel1 ugraph
-              in
-              let coerced = 
-                Cic.Lambda (name_t,src2,
-                  CicSubstitution.subst rel1 (CicSubstitution.lift_from 2 1 bo))
+                  bo ty ty2 subst metasenv context_src2 ugraph
               in
+              let coerced = Cic.Lambda (name_t,src2, bo) in
                 (coerced, expty), subst, metasenv, ugraph
           | _ -> 
             coerce_atom_to_something t infty expty subst metasenv context ugraph
     in
     try
       coerce_to_something_aux t infty expty subst metasenv context ugraph
-    with Uncertain _ | RefineFailure _ ->
-      let exn = 
-        RefineFailure (lazy ("The term " ^
+    with Uncertain _ | RefineFailure _ as exn ->
+      let f _ =
+        lazy ("The term " ^
           CicMetaSubst.ppterm_in_context metasenv subst t context ^ 
           " has type " ^ CicMetaSubst.ppterm_in_context metasenv subst
           infty context ^ " but is here used with type " ^ 
-          CicMetaSubst.ppterm_in_context metasenv subst expty context))
+          CicMetaSubst.ppterm_in_context metasenv subst expty context)
       in
-        enrich localization_tbl t exn
+        enrich localization_tbl ~f t exn
 
   and coerce_to_sort localization_tbl t infty subst context metasenv uragph =
     match CicReduction.whd ~subst:subst context infty with