- lift added to CicMetaSubst

[helm.git] / helm / ocaml / cic_unification / cicRefine.ml

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 -