type of constant ported

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 96b2f9186fcc7ebfcec7714e9a35f6d1fe66df0a..7ba5ab15219d435aa3be7011fd3086c0086f15ff 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -1132,55 +1132,33 @@ and returns_a_coinductive ~subst context ty =
      returns_a_coinductive ~subst ((n,C.Decl so)::context) de
   | _ -> None
 
-and type_of_constant ref = 
-assert false        (*
+and type_of_constant ((Ref.Ref (_,uri,_)) as ref) = 
   let cobj =
-   match E.get_obj uri with
-   | true, cobj -> cobj
-   | false, uobj ->
-         logger#log (`Start_type_checking uri) ;
-         let ugraph1_dust =
-          typecheck_obj0 ~logger uri CicUniv.empty_ugraph uobj in
-           try 
-             CicEnvironment.set_type_checking_info uri ;
-             logger#log (`Type_checking_completed uri) ;
-             (match CicEnvironment.is_type_checked ~trust:false ugraph uri with
-                  CicEnvironment.CheckedObj (cobj,ugraph') -> (cobj,ugraph')
-                | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
-             )
-           with
-            (*
-              this is raised if set_type_checking_info is called on an object
-              that has no associated universe file. If we are in univ_maker 
-              phase this is OK since univ_maker will properly commit the 
-              object.
-            *)
-               Invalid_argument s ->
-                 (*debug_print (lazy s);*)
-                 uobj,ugraph1_dust
+    match E.get_obj uri with
+    | true, cobj -> cobj
+    | false, uobj ->
+       !logger (`Start_type_checking uri);
+       check_obj_well_typed uobj;
+       E.add_obj uobj;
+       !logger (`Type_checking_completed uri);
+       if not (fst (E.get_obj uri)) then
+         raise (AssertFailure (lazy "environment error"));
+       uobj
   in
-CASO COSTRUTTORE
-    match cobj with
-        C.InductiveDefinition (dl,_,_,_) ->
-          let (_,_,arity,_) = List.nth dl i in
-            arity,ugraph1
-      | _ ->
-          raise (TypeCheckerFailure
-           (lazy ("Unknown mutual inductive definition:" ^ U.string_of_uri uri)))
-CASO TIPO INDUTTIVO
-    match cobj with
-        C.InductiveDefinition (dl,_,_,_) ->
-          let (_,_,_,cl) = List.nth dl i in
-          let (_,ty) = List.nth cl (j-1) in
-            ty,ugraph1
-      | _ ->
-          raise (TypeCheckerFailure
-           (lazy ("Unknown mutual inductive definition:" ^ UriManager.string_of_uri uri)))
-CASO COSTANTE
-CASO FIX/COFIX
-*)
+  match cobj, ref with
+  | (_,_,_,_,C.Inductive (_,_,tl,_)), Ref.Ref (_,_,Ref.Ind i)  ->
+      let _,_,arity,_ = List.nth tl i in arity
+  | (_,_,_,_,C.Inductive (_,_,tl,_)), Ref.Ref (_,_,Ref.Con (i,j))  ->
+      let _,_,_,cl = List.nth tl i in 
+      let _,_,arity = List.nth cl j in 
+      arity
+  | (_,_,_,_,C.Fixpoint (_,fl,_)), Ref.Ref (_,_,(Ref.Fix (i,_)|Ref.CoFix i)) ->
+      let _,_,_,arity,_ = List.nth fl i in
+      arity
+  | (_,_,_,_,C.Constant (_,_,_,ty,_)), Ref.Ref (_,_,(Ref.Def |Ref.Decl)) -> ty
+  | _ -> raise (AssertFailure (lazy "type_of_constant: environment/reference"))
 
-and typecheck_obj0 (uri,height,metasenv,subst,kind) =
+and check_obj_well_typed (uri,height,metasenv,subst,kind) =
  (* CSC: here we should typecheck the metasenv and the subst *)
  assert (metasenv = [] && subst = []);
  match kind with
@@ -1229,9 +1207,6 @@ and typecheck_obj0 (uri,height,metasenv,subst,kind) =
                    (lazy "CoFix: not guarded by constructors"))
           ) fl
 
-let typecheck_obj (*uri*) obj = assert false (*
- let ugraph = typecheck_obj0 ~logger uri CicUniv.empty_ugraph obj in
- let ugraph, univlist, obj = CicUnivUtils.clean_and_fill uri obj ugraph in
-  CicEnvironment.add_type_checked_obj uri (obj,ugraph,univlist)
-*)
-;;
+let typecheck_obj = check_obj_well_typed;;
+
+(* EOF *)