From cf7fbeee5c21b86f70281f42cd09ee699e0c62b7 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 29 Jan 2004 18:35:14 +0000
Subject: [PATCH] - lift added to CicMetaSubst - refine of Fix and CoFix
 implemented - bug fixed in refine of Cast

---
 helm/ocaml/cic_unification/cicMetaSubst.ml  | 10 +++++
 helm/ocaml/cic_unification/cicMetaSubst.mli |  2 +
 helm/ocaml/cic_unification/cicRefine.ml     | 49 +++++++++++++++++++--
 helm/ocaml/cic_unification/cicRefine.mli    |  1 -
 4 files changed, 57 insertions(+), 5 deletions(-)

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index a3b27c3e7..6d8b03ddb 100644
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -481,6 +481,16 @@ let unwind_subst metasenv subst =
 (* From now on we recreate a kernel abstraction where substitutions are part of
  * the calculus *)
 
+let lift metasenv subst n term =
+  (* TODO unwind's result is thrown away :-( *)
+  let (subst, _) = unwind_subst metasenv subst in
+  let term = apply_subst subst term in
+  try
+    CicSubstitution.lift n term
+  with e ->
+    raise (MetaSubstFailure ("Lift failure: " ^
+      Printexc.to_string e))
+
 let whd metasenv subst context term =
   (* TODO unwind's result is thrown away :-( *)
   let (subst, _) = unwind_subst metasenv subst in
diff --git a/helm/ocaml/cic_unification/cicMetaSubst.mli b/helm/ocaml/cic_unification/cicMetaSubst.mli
index 986a595ce..a81f50c1d 100644
--- a/helm/ocaml/cic_unification/cicMetaSubst.mli
+++ b/helm/ocaml/cic_unification/cicMetaSubst.mli
@@ -69,6 +69,8 @@ val ppsubst: substitution -> string
  * From now on we recreate a kernel abstraction where substitutions are part of
  * the calculus *)
 
+val lift : Cic.metasenv -> substitution -> int -> Cic.term -> Cic.term
+
 val whd: Cic.metasenv -> substitution -> Cic.context -> Cic.term -> Cic.term
 
 val are_convertible:
diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 54fde9a45..979c9637e 100644
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -34,7 +34,6 @@ exception ListTooShort;;
 exception WrongUriToMutualInductiveDefinitions of string;;
 exception RelToHiddenHypothesis;;
 exception MetasenvInconsistency;;
-exception MutCaseFixAndCofixRefineNotImplemented;;
 exception WrongArgumentNumber;;
 
 let fdebug = ref 0;;
@@ -174,7 +173,7 @@ and type_of_aux' metasenv context t =
        let _,subst',metasenv' =
         type_of_aux subst metasenv context ty in
        let inferredty,subst'',metasenv'' =
-        type_of_aux subst' metasenv' context ty
+        type_of_aux subst' metasenv' context te
        in
         (try
           let subst''',metasenv''' =
@@ -342,8 +341,50 @@ and type_of_aux' metasenv context t =
              (subst,metasenv) outtypeinstances in
         CicMetaSubst.whd metasenv subst
           context (C.Appl(outtype::right_args@[term])),subst,metasenv
-   | C.Fix _
-   | C.CoFix _ -> raise MutCaseFixAndCofixRefineNotImplemented
+   | C.Fix (i,fl) ->
+      let subst,metasenv,types =
+       List.fold_left
+        (fun (subst,metasenv,types) (n,_,ty,_) ->
+          let _,subst',metasenv' = type_of_aux subst metasenv context ty in
+           subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types
+        ) (subst,metasenv,[]) fl
+      in
+       let len = List.length types in
+       let context' = types@context in
+       let subst,metasenv =
+        List.fold_left
+         (fun (subst,metasenv) (name,x,ty,bo) ->
+           let ty_of_bo,subst,metasenv =
+            type_of_aux subst metasenv context' bo
+           in
+            Un.fo_unif_subst subst context' metasenv
+              ty_of_bo (CicMetaSubst.lift metasenv subst len ty)
+         ) (subst,metasenv) fl in
+      
+        let (_,_,ty,_) = List.nth fl i in
+         ty,subst,metasenv
+   | C.CoFix (i,fl) ->
+      let subst,metasenv,types =
+       List.fold_left
+        (fun (subst,metasenv,types) (n,ty,_) ->
+          let _,subst',metasenv' = type_of_aux subst metasenv context ty in
+           subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types
+        ) (subst,metasenv,[]) fl
+      in
+       let len = List.length types in
+       let context' = types@context in
+       let subst,metasenv =
+        List.fold_left
+         (fun (subst,metasenv) (name,ty,bo) ->
+           let ty_of_bo,subst,metasenv =
+            type_of_aux subst metasenv context' bo
+           in
+            Un.fo_unif_subst subst context' metasenv
+              ty_of_bo (CicMetaSubst.lift metasenv subst len ty)
+         ) (subst,metasenv) fl in
+      
+        let (_,ty,_) = List.nth fl i in
+         ty,subst,metasenv
 
  (* check_metasenv_consistency checks that the "canonical" context of a
  metavariable is consitent - up to relocation via the relocation list l -
diff --git a/helm/ocaml/cic_unification/cicRefine.mli b/helm/ocaml/cic_unification/cicRefine.mli
index 12a4bb98b..ce97e8ab7 100644
--- a/helm/ocaml/cic_unification/cicRefine.mli
+++ b/helm/ocaml/cic_unification/cicRefine.mli
@@ -28,7 +28,6 @@ exception Uncertain of string
 exception WrongUriToConstant of string
 exception WrongUriToVariable of string
 exception WrongUriToMutualInductiveDefinitions of string
-exception MutCaseFixAndCofixRefineNotImplemented;;
 
 (* type_of_aux' metasenv context term                        *)
 (* refines [term] and returns the refined form of [term],    *)
-- 
2.39.2