Branch V7_3_new_exportation closed.

[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 62dc951aaa54deb58cc3fe0dc36dfa5e142a4fac..0d171604d74beed6e5ce8c1ce3a6f000d457f772 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -136,7 +136,7 @@ let rec type_of_constant uri =
    match CicEnvironment.is_type_checked ~trust:true uri with
       CicEnvironment.CheckedObj cobj -> cobj
     | CicEnvironment.UncheckedObj uobj ->
-       Logger.log (`Start_type_checking uri) ;
+       CicLogger.log (`Start_type_checking uri) ;
        (* let's typecheck the uncooked obj *)
        (match uobj with
            C.Constant (_,Some te,ty,_) ->
@@ -166,7 +166,7 @@ let rec type_of_constant uri =
            raise (TypeCheckerFailure (WrongUriToConstant (U.string_of_uri uri)))
        ) ;
        CicEnvironment.set_type_checking_info uri ;
-       Logger.log (`Type_checking_completed uri) ;
+       CicLogger.log (`Type_checking_completed uri) ;
        match CicEnvironment.is_type_checked ~trust:false uri with
           CicEnvironment.CheckedObj cobj -> cobj
         | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
@@ -184,7 +184,7 @@ and type_of_variable uri =
   match CicEnvironment.is_type_checked ~trust:true uri with
      CicEnvironment.CheckedObj (C.Variable (_,_,ty,_)) -> ty
    | CicEnvironment.UncheckedObj (C.Variable (_,bo,ty,_)) ->
-      Logger.log (`Start_type_checking uri) ;
+      CicLogger.log (`Start_type_checking uri) ;
       (* only to check that ty is well-typed *)
       let _ = type_of ty in
        (match bo with
@@ -196,7 +196,7 @@ and type_of_variable uri =
                 (NotWellTyped ("Variable " ^ (U.string_of_uri uri))))
        ) ;
        CicEnvironment.set_type_checking_info uri ;
-       Logger.log (`Type_checking_completed uri) ;
+       CicLogger.log (`Type_checking_completed uri) ;
        ty
    |  _ ->
        raise
@@ -529,10 +529,10 @@ and type_of_mutual_inductive_defs uri i =
    match CicEnvironment.is_type_checked ~trust:true uri with
       CicEnvironment.CheckedObj cobj -> cobj
     | CicEnvironment.UncheckedObj uobj ->
-       Logger.log (`Start_type_checking uri) ;
+       CicLogger.log (`Start_type_checking uri) ;
        check_mutual_inductive_defs uri uobj ;
        CicEnvironment.set_type_checking_info uri ;
-       Logger.log (`Type_checking_completed uri) ;
+       CicLogger.log (`Type_checking_completed uri) ;
        (match CicEnvironment.is_type_checked ~trust:false uri with
           CicEnvironment.CheckedObj cobj -> cobj
         | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
@@ -555,10 +555,10 @@ and type_of_mutual_inductive_constr uri i j =
    match CicEnvironment.is_type_checked ~trust:true uri with
       CicEnvironment.CheckedObj cobj -> cobj
     | CicEnvironment.UncheckedObj uobj ->
-       Logger.log (`Start_type_checking uri) ;
+       CicLogger.log (`Start_type_checking uri) ;
        check_mutual_inductive_defs uri uobj ;
        CicEnvironment.set_type_checking_info uri ;
-       Logger.log (`Type_checking_completed uri) ;
+       CicLogger.log (`Type_checking_completed uri) ;
        (match CicEnvironment.is_type_checked ~trust:false uri with
           CicEnvironment.CheckedObj cobj -> cobj
         | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
@@ -1185,6 +1185,7 @@ and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 =
         (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2
    | (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true
    | (C.Sort C.Prop, C.Sort C.Set)
+   | (C.Sort C.Prop, C.Sort C.CProp)
    | (C.Sort C.Prop, C.Sort C.Type) when need_dummy ->
 (*CSC: WRONG. MISSING CONDITIONS ON THE ARGUMENTS OF THE CONSTRUTOR *)
        (match CicEnvironment.get_obj uri with
@@ -1198,8 +1199,13 @@ and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 =
               (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)))
        )
    | (C.Sort C.Set, C.Sort C.Prop) when need_dummy -> true
+   | (C.Sort C.CProp, C.Sort C.Prop) when need_dummy -> true
    | (C.Sort C.Set, C.Sort C.Set) when need_dummy -> true
-   | (C.Sort C.Set, C.Sort C.Type) when need_dummy ->
+   | (C.Sort C.Set, C.Sort C.CProp) when need_dummy -> true
+   | (C.Sort C.CProp, C.Sort C.Set) when need_dummy -> true
+   | (C.Sort C.CProp, C.Sort C.CProp) when need_dummy -> true
+   | ((C.Sort C.Set, C.Sort C.Type) | (C.Sort C.CProp, C.Sort C.Type))
+      when need_dummy ->
        (match CicEnvironment.get_obj uri with
            C.InductiveDefinition (itl,_,paramsno) ->
             let tys =
@@ -1220,7 +1226,7 @@ and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 =
         res &&
         (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
             C.Sort C.Prop -> true
-          | C.Sort C.Set ->
+          | (C.Sort C.Set | C.Sort C.CProp) ->
              (match CicEnvironment.get_obj uri with
                  C.InductiveDefinition (itl,_,_) ->
                   let (_,_,_,cl) = List.nth itl i in
@@ -1233,13 +1239,15 @@ and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 =
              )
           | _ -> false
         )
-   | (C.Sort C.Set, C.Prod (name,so,ta)) when not need_dummy ->
+   | ((C.Sort C.Set, C.Prod (name,so,ta)) | (C.Sort C.CProp, C.Prod (name,so,ta)))
+      when not need_dummy ->
        let res = CicReduction.are_convertible context so ind
        in
         res &&
         (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
             C.Sort C.Prop
           | C.Sort C.Set  -> true
+         | C.Sort C.CProp -> true
           | C.Sort C.Type ->
              (match CicEnvironment.get_obj uri with
                  C.InductiveDefinition (itl,_,paramsno) ->
@@ -1647,7 +1655,7 @@ in if not res then prerr_endline ("#### " ^ CicPp.ppterm (type_of_aux context p)
    let t2' = CicReduction.whd ((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) -> (* different from Coq manual!!! *)
+        when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different from Coq manual!!! *)
          C.Sort s2
     | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
     | (_,_) ->
@@ -1728,7 +1736,7 @@ and is_small context paramsno c =
       C.Prod (n,so,de) ->
        (*CSC: [] is an empty metasenv. Is it correct? *)
        let s = type_of_aux' [] context so in
-        (s = C.Sort C.Prop || s = C.Sort C.Set) &&
+        (s = C.Sort C.Prop || s = C.Sort C.Set || s = C.Sort C.CProp) &&
         is_small_aux ((Some (n,(C.Decl so)))::context) de
     | _ -> true (*CSC: we trust the type-checker *)
  in
@@ -1754,7 +1762,7 @@ let typecheck uri =
      CicEnvironment.CheckedObj _ -> ()
    | CicEnvironment.UncheckedObj uobj ->
       (* let's typecheck the uncooked object *)
-      Logger.log (`Start_type_checking uri) ;
+      CicLogger.log (`Start_type_checking uri) ;
       (match uobj with
           C.Constant (_,Some te,ty,_) ->
            let _ = type_of ty in
@@ -1794,5 +1802,5 @@ let typecheck uri =
            check_mutual_inductive_defs uri uobj
       ) ;
       CicEnvironment.set_type_checking_info uri ;
-      Logger.log (`Type_checking_completed uri)
+      CicLogger.log (`Type_checking_completed uri)
 ;;