Module Logger added.

[helm.git] / helm / ocaml / cic_proof_checking / cicTypeChecker.ml

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 63366b4b9997f5897027117458c17a98a7627f05..ba72a37a2a6edbfe8300007f140358765a46e7cc 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -23,7 +23,6 @@
  * http://cs.unibo.it/helm/.
  *)
 
-exception NotImplemented;;
 exception Impossible of int;;
 exception NotWellTyped of string;;
 exception WrongUriToConstant of string;;
@@ -34,30 +33,6 @@ exception NotPositiveOccurrences of string;;
 exception NotWellFormedTypeOfInductiveConstructor of string;;
 exception WrongRequiredArgument of string;;
 
-let log =
- let module U = UriManager in
-  let indent = ref 0 in
-   function
-      `Start_type_checking uri ->
-        print_string (
-         (String.make !indent ' ') ^
-         "<div style=\"margin-left: " ^
-         string_of_float (float_of_int !indent *. 0.5) ^ "cm\">" ^
-         "Type-Checking of " ^ (U.string_of_uri uri) ^ " started</div>\n"
-        ) ;
-        flush stdout ;
-        incr indent
-    | `Type_checking_completed uri ->
-        decr indent ;
-        print_string (
-         (String.make !indent ' ') ^
-         "<div style=\"color: green ; margin-left: " ^
-         string_of_float (float_of_int !indent *. 0.5) ^ "cm\">" ^
-         "Type-Checking of " ^ (U.string_of_uri uri) ^ " completed.</div>\n"
-        ) ;
-        flush stdout
-;;
-
 let fdebug = ref 0;;
 let debug t env =
  let rec debug_aux t i =
@@ -87,7 +62,7 @@ let rec cooked_type_of_constant uri cookingsno =
    match CicEnvironment.is_type_checked uri cookingsno with
       CicEnvironment.CheckedObj cobj -> cobj
     | CicEnvironment.UncheckedObj uobj ->
-       log (`Start_type_checking uri) ;
+       Logger.log (`Start_type_checking uri) ;
        (* let's typecheck the uncooked obj *)
        (match uobj with
            C.Definition (_,te,ty,_) ->
@@ -97,14 +72,14 @@ let rec cooked_type_of_constant uri cookingsno =
          | C.Axiom (_,ty,_) ->
            (* only to check that ty is well-typed *)
            let _ = type_of ty in ()
-         | C.CurrentProof (_,_,te,ty) ->
-             let _ = type_of ty in
-              if not (R.are_convertible (type_of te) ty) then
+         | C.CurrentProof (_,conjs,te,ty) ->
+             let _ = type_of_aux' conjs [] ty in
+              if not (R.are_convertible (type_of_aux' conjs [] te) ty) then
                raise (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri)))
          | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
        ) ;
        CicEnvironment.set_type_checking_info uri ;
-       log (`Type_checking_completed uri) ;
+       Logger.log (`Type_checking_completed uri) ;
        match CicEnvironment.is_type_checked uri cookingsno with
           CicEnvironment.CheckedObj cobj -> cobj
         | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
@@ -123,7 +98,7 @@ and type_of_variable uri =
   match CicEnvironment.is_type_checked uri 0 with
      CicEnvironment.CheckedObj (C.Variable (_,_,ty)) -> ty
    | CicEnvironment.UncheckedObj (C.Variable (_,bo,ty)) ->
-       log (`Start_type_checking uri) ;
+      Logger.log (`Start_type_checking uri) ;
       (* only to check that ty is well-typed *)
       let _ = type_of ty in
        (match bo with
@@ -133,7 +108,7 @@ and type_of_variable uri =
              raise (NotWellTyped ("Variable " ^ (U.string_of_uri uri)))
        ) ;
        CicEnvironment.set_type_checking_info uri ;
-       log (`Type_checking_completed uri) ;
+       Logger.log (`Type_checking_completed uri) ;
        ty
    |  _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
 
@@ -377,10 +352,10 @@ and cooked_type_of_mutual_inductive_defs uri cookingsno i =
    match CicEnvironment.is_type_checked uri cookingsno with
       CicEnvironment.CheckedObj cobj -> cobj
     | CicEnvironment.UncheckedObj uobj ->
-       log (`Start_type_checking uri) ;
+       Logger.log (`Start_type_checking uri) ;
        cooked_mutual_inductive_defs uri uobj ;
        CicEnvironment.set_type_checking_info uri ;
-       log (`Type_checking_completed uri) ;
+       Logger.log (`Type_checking_completed uri) ;
        (match CicEnvironment.is_type_checked uri cookingsno with
           CicEnvironment.CheckedObj cobj -> cobj
         | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
@@ -400,10 +375,10 @@ and cooked_type_of_mutual_inductive_constr uri cookingsno i j =
    match CicEnvironment.is_type_checked uri cookingsno with
       CicEnvironment.CheckedObj cobj -> cobj
     | CicEnvironment.UncheckedObj uobj ->
-       log (`Start_type_checking uri) ;
+       Logger.log (`Start_type_checking uri) ;
        cooked_mutual_inductive_defs uri uobj ;
        CicEnvironment.set_type_checking_info uri ;
-       log (`Type_checking_completed uri) ;
+       Logger.log (`Type_checking_completed uri) ;
        (match CicEnvironment.is_type_checked uri cookingsno with
           CicEnvironment.CheckedObj cobj -> cobj
         | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
@@ -1048,7 +1023,7 @@ and type_of_branch argsno need_dummy outtype term constype =
        
  
 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
-and type_of_aux' env t =
+and type_of_aux' metasenv env t =
  let rec type_of_aux env =
   let module C = Cic in
   let module R = CicReduction in
@@ -1068,7 +1043,7 @@ and type_of_aux' env t =
       let ty = type_of_variable uri in
        decr fdebug ;
        ty
-    | C.Meta n -> raise NotImplemented
+    | C.Meta n -> List.assoc n metasenv
     | C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
     | C.Implicit -> raise (Impossible 21)
     | C.Cast (te,ty) ->
@@ -1320,7 +1295,8 @@ and is_small paramsno c =
   let module C = Cic in
    match CicReduction.whd c with
       C.Prod (_,so,de) ->
-       let s = type_of_aux' env so in
+       (*CSC: [] is an empty metasenv. Is it correct? *)
+       let s = type_of_aux' [] env so in
         (s = C.Sort C.Prop || s = C.Sort C.Set) &&
         is_small_aux (so::env) de
     | _ -> true (*CSC: we trust the type-checker *)
@@ -1329,7 +1305,7 @@ and is_small paramsno c =
    is_small_aux (List.rev sx) dx
 
 and type_of t =
- type_of_aux' [] t
+ type_of_aux' [] [] t
 ;;
 
 let typecheck uri =
@@ -1340,7 +1316,7 @@ let typecheck uri =
      CicEnvironment.CheckedObj _ -> ()
    | CicEnvironment.UncheckedObj uobj ->
       (* let's typecheck the uncooked object *)
-      log (`Start_type_checking uri) ;
+      Logger.log (`Start_type_checking uri) ;
       (match uobj with
           C.Definition (_,te,ty,_) ->
            let _ = type_of ty in
@@ -1349,12 +1325,12 @@ let typecheck uri =
         | C.Axiom (_,ty,_) ->
           (* only to check that ty is well-typed *)
           let _ = type_of ty in ()
-        | C.CurrentProof (_,_,te,ty) ->
-           (*CSC [] wrong *)
-           let _ = type_of ty in
-            debug (type_of te) [] ;
-            if not (R.are_convertible (type_of te) ty) then
-             raise (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri)))
+        | C.CurrentProof (_,conjs,te,ty) ->
+           (*CSC [] wrong *)
+            let _ = type_of_aux' conjs [] ty in
+             debug (type_of_aux' conjs [] te) [] ;
+             if not (R.are_convertible (type_of_aux' conjs [] te) ty) then
+              raise (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri)))
         | C.Variable (_,bo,ty) ->
            (* only to check that ty is well-typed *)
            let _ = type_of ty in
@@ -1368,5 +1344,6 @@ let typecheck uri =
            cooked_mutual_inductive_defs uri uobj
       ) ;
       CicEnvironment.set_type_checking_info uri ;
-      log (`Type_checking_completed uri)
+      Logger.log (`Type_checking_completed uri)
 ;;
+