- lift added to CicMetaSubst

- refine of Fix and CoFix implemented
- bug fixed in refine of Cast

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index a3b27c3e74548e86f2fd9dc712a979e3d9c23094..6d8b03ddb4c4d73832553ed172670b8ca2b00780 100644 (file)
--- 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 986a595ce78fdb2ebec9e5dc89ee401ae275e874..a81f50c1dd2c1527e662b0b49ff7e4ba9b416437 100644 (file)
--- 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 54fde9a45a6d49c4d8e8d33ce88e98af2282f552..979c9637ede5591125cf64dfa4786d08299a2648 100644 (file)
--- 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 12a4bb98b45c0c61d86a965249b7b679e4859cd2..ce97e8ab7ff178f4222b1c6acc5954139d12411e 100644 (file)
--- 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],    *)