logger added

[helm.git] / helm / software / components / ng_kernel / nCicTypeChecker.ml

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 920a2078e214b8dbc11936140d6fecd33876df9d..96b2f9186fcc7ebfcec7714e9a35f6d1fe66df0a 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -11,6 +11,14 @@
 
 (* $Id: nCicReduction.ml 8250 2008-03-25 17:56:20Z tassi $ *)
 
+(* web interface stuff *)
+
+let logger = 
+  ref (function (`Start_type_checking _|`Type_checking_completed _) -> ())
+;;
+
+let set_logger f = logger := f;;
+
 exception TypeCheckerFailure of string Lazy.t
 exception AssertFailure of string Lazy.t
 
@@ -517,40 +525,6 @@ and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI =
              args coInductiveTypeURI
          ) fl true
 
- and returns_a_coinductive ~subst context ty =
-  let module C = Cic in
-   match CicReduction.whd ~subst context ty with
-      C.MutInd (uri,i,_) ->
-       (*CSC: definire una funzioncina per questo codice sempre replicato *)
-        let obj,_ =
-          try
-            CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
-          with Not_found -> assert false
-        in
-        (match obj with
-           C.InductiveDefinition (itl,_,_,_) ->
-            let (_,is_inductive,_,_) = List.nth itl i in
-             if is_inductive then None else (Some uri)
-         | _ ->
-            raise (TypeCheckerFailure
-              (lazy ("Unknown mutual inductive definition:" ^
-              UriManager.string_of_uri uri)))
-        )
-    | C.Appl ((C.MutInd (uri,i,_))::_) ->
-       (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
-         match o with
-           C.InductiveDefinition (itl,_,_,_) ->
-            let (_,is_inductive,_,_) = List.nth itl i in
-             if is_inductive then None else (Some uri)
-         | _ ->
-            raise (TypeCheckerFailure
-              (lazy ("Unknown mutual inductive definition:" ^
-              UriManager.string_of_uri uri)))
-        )
-    | C.Prod (n,so,de) ->
-       returns_a_coinductive ~subst ((Some (n,C.Decl so))::context) de
-    | _ -> None
-
  in
   type_of_aux ~logger context t ugraph
 
@@ -921,10 +895,10 @@ let rec typeof ~subst ~metasenv context term =
               let type_t = typeof_aux context t in
               if not (R.are_convertible ~subst ~metasenv context type_t ct) then
                 raise (TypeCheckerFailure 
-                  (lazy (Printf.sprintf 
-                   ("Not well typed metavariable local context: "^^
-                    "expected a term of type %s, found %s of type %s") 
-                    (NCicPp.ppterm ct) (NCicPp.ppterm t) (NCicPp.ppterm type_t))))
+                 (lazy (Printf.sprintf 
+                  ("Not well typed metavariable local context: "^^
+                  "expected a term of type %s, found %s of type %s") 
+                  (NCicPp.ppterm ct) (NCicPp.ppterm t) (NCicPp.ppterm type_t))))
         ) l lifted_canonical_context 
        with
         Invalid_argument _ ->
@@ -1148,15 +1122,22 @@ and is_really_smaller ~subst (context, recfuns, x, safes as k) te =
            pl cl
     | _ -> List.for_all (is_really_smaller ~subst k) pl)
 
-and returns_a_coinductive ~subst _ _ = assert false
+and returns_a_coinductive ~subst context ty =
+  match R.whd ~subst context ty with
+  | C.Const (Ref.Ref (_,uri,Ref.Ind _) as ref) 
+  | C.Appl (C.Const (Ref.Ref (_,uri,Ref.Ind _) as ref)::_) ->
+     let isinductive, _, _, _, _ = E.get_checked_indtys ref in
+     if isinductive then None else (Some uri)
+  | C.Prod (n,so,de) ->
+     returns_a_coinductive ~subst ((n,C.Decl so)::context) de
+  | _ -> None
 
-and type_of_constant ref = assert false (* USARE typecheck_obj0 *)
-(* ALIAS typecheck *)
-(*
-  let cobj,ugraph1 =
-   match CicEnvironment.is_type_checked ~trust:true ugraph uri with
-       CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
-     | CicEnvironment.UncheckedObj uobj ->
+and type_of_constant ref = 
+assert false        (*
+  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