s/Callbacks/DisambiguateCallbacks/

[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 e3086c80126011c9a8be1bdb32a187e45c355296..979c9637ede5591125cf64dfa4786d08299a2648 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -34,8 +34,6 @@ exception ListTooShort;;
 exception WrongUriToMutualInductiveDefinitions of string;;
 exception RelToHiddenHypothesis;;
 exception MetasenvInconsistency;;
-exception MutCaseFixAndCofixRefineNotImplemented;;
-exception FreeMetaFound of int;;
 exception WrongArgumentNumber;;
 
 let fdebug = ref 0;;
@@ -111,7 +109,7 @@ and check_branch n context metasenv subst left_args_no actualtype term expectedt
   let module C = Cic in
   let module R = CicMetaSubst in
   let module Un = CicUnification in 
-  match R.whd subst context expectedtype with
+  match R.whd metasenv subst context expectedtype with
      C.MutInd (_,_,_) ->
        (n,context,actualtype, [term]), subst, metasenv
    | C.Appl (C.MutInd (_,_,_)::tl) ->
@@ -120,7 +118,7 @@ and check_branch n context metasenv subst left_args_no actualtype term expectedt
    | C.Prod (name,so,de) ->
       (* we expect that the actual type of the branch has the due 
          number of Prod *)
-      (match R.whd subst context actualtype with
+      (match R.whd metasenv subst context actualtype with
            C.Prod (name',so',de') ->
              let subst, metasenv = 
                 Un.fo_unif_subst subst context metasenv so so' in
@@ -162,12 +160,7 @@ and type_of_aux' metasenv context t =
        decr fdebug ;
        ty,subst',metasenv'
     | C.Meta (n,l) -> 
-       let (_,canonical_context,ty) =
-        try
-         List.find (function (m,_,_) -> n = m) metasenv
-        with
-         Not_found -> raise (FreeMetaFound n)
-       in
+       let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
         let subst',metasenv' =
          check_metasenv_consistency subst metasenv context canonical_context l
         in
@@ -180,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''' =
@@ -267,7 +260,7 @@ and type_of_aux' metasenv context t =
             raise
              (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) in
        let rec count_prod t =
-         match CicMetaSubst.whd subst context t with
+         match CicMetaSubst.whd metasenv subst context t with
              C.Prod (_, _, t) -> 1 + (count_prod t)
            | _ -> 0 in 
        let no_args = count_prod arity in
@@ -292,7 +285,7 @@ and type_of_aux' metasenv context t =
        let _, subst, metasenv =
          type_of_aux subst metasenv context expected_type
        in
-       let actual_type = CicMetaSubst.whd subst context actual_type in
+       let actual_type = CicMetaSubst.whd metasenv subst context actual_type in
        let subst,metasenv =
          Un.fo_unif_subst subst context metasenv expected_type actual_type
        in
@@ -342,14 +335,56 @@ and type_of_aux' metasenv context t =
                   type_of_aux subst metasenv context appl
                 in
 *)
-                CicMetaSubst.whd subst context appl
+                CicMetaSubst.whd metasenv subst context appl
               in
                Un.fo_unif_subst subst context metasenv instance instance')
              (subst,metasenv) outtypeinstances in
-        CicMetaSubst.whd subst
+        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 -
@@ -427,8 +462,10 @@ and type_of_aux' metasenv context t =
    let subst',metasenv' = CicMetaSubst.unwind_subst metasenv subst in
    let t1' = CicMetaSubst.apply_subst subst' t1 in
    let t2' = CicMetaSubst.apply_subst subst' t2 in
-    let t1'' = CicMetaSubst.whd subst' context t1' in
-    let t2'' = CicMetaSubst.whd subst' ((Some (name,C.Decl s))::context) t2' in
+    let t1'' = CicMetaSubst.whd metasenv subst' context t1' in
+    let t2'' =
+      CicMetaSubst.whd metasenv subst' ((Some (name,C.Decl s))::context) t2'
+    in
     match (t1'', t2'') with
        (C.Sort s1, C.Sort s2)
          when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different from Coq manual!!! *)
@@ -452,7 +489,7 @@ and type_of_aux' metasenv context t =
   function
      [] -> hetype,subst,metasenv
    | (hete, hety)::tl ->
-    (match (CicMetaSubst.whd subst context hetype) with
+    (match (CicMetaSubst.whd metasenv subst context hetype) with
         Cic.Prod (n,s,t) ->
          let subst',metasenv' =
            CicUnification.fo_unif_subst subst context metasenv s hety