X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=f216b3c5c03429324561f49e8a89e770246063e1;hb=33dd8006a7e0eb9c6c2a93b4d98c8ef88d2d49d1;hp=f30e3c53c0314819a825f62310b3fd28cbc0ae2c;hpb=75a7e852a03cdaa788e7005dfce222c5d6359915;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index f30e3c53c..f216b3c5c 100644
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -47,76 +47,68 @@ let rec split l n =
 ;;
 
 let rec type_of_constant uri ugraph =
-  let module C = Cic in
-  let module R = CicReduction in
-  let module U = UriManager in
-    (*
-      let obj =
-      try
-      CicEnvironment.get_cooked_obj uri
-      with Not_found -> assert false
-      in
-    *)
-  let obj,u= CicEnvironment.get_obj ugraph uri in
-    match obj with
-	C.Constant (_,_,ty,_,_) -> ty,u
-      | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
-      | _ ->
-	  raise
-	    (RefineFailure ("Unknown constant definition " ^  U.string_of_uri uri))
+ let module C = Cic in
+ let module R = CicReduction in
+ let module U = UriManager in
+  let _ = CicTypeChecker.typecheck uri in
+  let obj,u =
+   try
+    CicEnvironment.get_cooked_obj ugraph uri
+   with Not_found -> assert false
+  in
+   match obj with
+      C.Constant (_,_,ty,_,_) -> ty,u
+    | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
+    | _ ->
+       raise
+        (RefineFailure ("Unknown constant definition " ^  U.string_of_uri uri))
 
 and type_of_variable uri ugraph =
   let module C = Cic in
   let module R = CicReduction in
   let module U = UriManager in
-    (*
-      let obj =
-      try
-      CicEnvironment.get_cooked_obj uri
-      with Not_found -> assert false
-      in
-    *)
-  let obj,u = CicEnvironment.get_obj ugraph uri in
-    match obj with
-	C.Variable (_,_,ty,_,_) -> ty,u
-      |  _ ->
-	   raise
-	    (RefineFailure
-               ("Unknown variable definition " ^ UriManager.string_of_uri uri))
+  let _ = CicTypeChecker.typecheck uri in
+  let obj,u =
+   try
+    CicEnvironment.get_cooked_obj ugraph uri
+    with Not_found -> assert false
+  in
+   match obj with
+      C.Variable (_,_,ty,_,_) -> ty,u
+    | _ ->
+        raise
+         (RefineFailure
+          ("Unknown variable definition " ^ UriManager.string_of_uri uri))
 
 and type_of_mutual_inductive_defs uri i ugraph =
   let module C = Cic in
   let module R = CicReduction in
   let module U = UriManager in
-    (*
-      let obj =
-      try
-      CicEnvironment.get_cooked_obj uri
-      with Not_found -> assert false
-      in
-    *)
-  let obj,u = CicEnvironment.get_obj ugraph uri in
-    match obj with
-	C.InductiveDefinition (dl,_,_,_) ->
-	  let (_,_,arity,_) = List.nth dl i in
-	    arity,u
-      | _ ->
-	  raise
-	    (RefineFailure
-               ("Unknown mutual inductive definition " ^ U.string_of_uri uri))
+  let _ = CicTypeChecker.typecheck uri in
+  let obj,u =
+   try
+    CicEnvironment.get_cooked_obj ugraph uri
+   with Not_found -> assert false
+  in
+   match obj with
+      C.InductiveDefinition (dl,_,_,_) ->
+        let (_,_,arity,_) = List.nth dl i in
+	 arity,u
+    | _ ->
+       raise
+        (RefineFailure
+         ("Unknown mutual inductive definition " ^ U.string_of_uri uri))
 
 and type_of_mutual_inductive_constr uri i j ugraph =
   let module C = Cic in
   let module R = CicReduction in
   let module U = UriManager in
-    (*
-      let obj =
-      try
-      CicEnvironment.get_cooked_obj uri
-      with Not_found -> assert false
-      in
-    *)
-  let obj,u = CicEnvironment.get_obj ugraph uri in
+  let _ = CicTypeChecker.typecheck uri in
+   let obj,u =
+    try
+     CicEnvironment.get_cooked_obj ugraph uri
+    with Not_found -> assert false
+   in
     match obj with
 	C.InductiveDefinition (dl,_,_,_) ->
 	  let (_,_,_,cl) = List.nth dl i in
@@ -182,7 +174,12 @@ and type_of_aux' metasenv context t ugraph =
 		 | Some (_,C.Def (_,Some ty)) -> 
                      t,S.lift n ty,subst,metasenv, ugraph
 		 | Some (_,C.Def (bo,None)) ->
-		     type_of_aux subst metasenv context (S.lift n bo) ugraph 
+                     let ty,ugraph =
+                      (* if it is in the context it must be already well-typed*)
+		      CicTypeChecker.type_of_aux' ~subst metasenv context
+                       (S.lift n bo) ugraph 
+                     in
+                      t,ty,subst,metasenv,ugraph
 		 | None -> raise (RefineFailure "Rel to hidden hypothesis")
              with
 		 _ -> raise (RefineFailure "Not a close term")
@@ -287,7 +284,7 @@ and type_of_aux' metasenv context t ugraph =
 	       * Moreover the inferred type is closer to the expected one. 
                *)
 	      C.LetIn (n,s',t'),CicSubstitution.subst s' inferredty,
-                subst',metasenv',ugraph2
+                subst'',metasenv'',ugraph2
 	| C.Appl (he::((_::_) as tl)) ->
 	    let he',hetype,subst',metasenv',ugraph1 = 
 	      type_of_aux subst metasenv context he ugraph 
@@ -342,7 +339,8 @@ and type_of_aux' metasenv context t ugraph =
 	    (* first, get the inductive type (and noparams) 
              * in the environment  *)
 	    let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
-	      let obj,u = CicEnvironment.get_obj ugraph uri in
+              let _ = CicTypeChecker.typecheck uri in
+	      let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
               match obj with
 		  C.InductiveDefinition (l,expl_params,parsno,_) -> 
 		    List.nth l i , expl_params, parsno, u
@@ -437,7 +435,7 @@ and type_of_aux' metasenv context t ugraph =
                (let candidate,ugraph5,metasenv,subst = 
                  let exp_name_subst, metasenv = 
                     let o,_ = 
-                      CicEnvironment.get_obj CicUniv.empty_ugraph uri 
+                      CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri 
                     in
                     let uris = CicUtil.params_of_obj o in
                     List.fold_right (