Relation patched, property 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 57bc5e2ad3698be43ae6a93e77d45b0273d100bb..a494c4a690f519638efacbe63738446e9f100245 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -124,7 +124,7 @@ let rec type_of_constant uri =
  let module R = CicReduction in
  let module U = UriManager in
   let cobj =
-   match CicEnvironment.is_type_checked uri with
+   match CicEnvironment.is_type_checked ~trust:true uri with
       CicEnvironment.CheckedObj cobj -> cobj
     | CicEnvironment.UncheckedObj uobj ->
        Logger.log (`Start_type_checking uri) ;
@@ -153,7 +153,7 @@ let rec type_of_constant uri =
        ) ;
        CicEnvironment.set_type_checking_info uri ;
        Logger.log (`Type_checking_completed uri) ;
-       match CicEnvironment.is_type_checked uri with
+       match CicEnvironment.is_type_checked ~trust:false uri with
           CicEnvironment.CheckedObj cobj -> cobj
         | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
   in
@@ -167,7 +167,7 @@ and type_of_variable uri =
  let module R = CicReduction in
  let module U = UriManager in
   (* 0 because a variable is never cooked => no partial cooking at one level *)
-  match CicEnvironment.is_type_checked uri with
+  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) ;
@@ -477,14 +477,14 @@ and type_of_mutual_inductive_defs uri i =
  let module R = CicReduction in
  let module U = UriManager in
   let cobj =
-   match CicEnvironment.is_type_checked uri with
+   match CicEnvironment.is_type_checked ~trust:true uri with
       CicEnvironment.CheckedObj cobj -> cobj
     | CicEnvironment.UncheckedObj uobj ->
        Logger.log (`Start_type_checking uri) ;
        check_mutual_inductive_defs uri uobj ;
        CicEnvironment.set_type_checking_info uri ;
        Logger.log (`Type_checking_completed uri) ;
-       (match CicEnvironment.is_type_checked uri with
+       (match CicEnvironment.is_type_checked ~trust:false uri with
           CicEnvironment.CheckedObj cobj -> cobj
         | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
        )
@@ -500,14 +500,14 @@ and type_of_mutual_inductive_constr uri i j =
  let module R = CicReduction in
  let module U = UriManager in
   let cobj =
-   match CicEnvironment.is_type_checked uri with
+   match CicEnvironment.is_type_checked ~trust:true uri with
       CicEnvironment.CheckedObj cobj -> cobj
     | CicEnvironment.UncheckedObj uobj ->
        Logger.log (`Start_type_checking uri) ;
        check_mutual_inductive_defs uri uobj ;
        CicEnvironment.set_type_checking_info uri ;
        Logger.log (`Type_checking_completed uri) ;
-       (match CicEnvironment.is_type_checked uri with
+       (match CicEnvironment.is_type_checked ~trust:false uri with
           CicEnvironment.CheckedObj cobj -> cobj
         | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
        )
@@ -934,7 +934,7 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI =
        List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
    | C.Appl ((C.MutConstruct (uri,i,j,exp_named_subst))::tl) ->
       let consty =
-       match CicEnvironment.get_cooked_obj uri with
+       match CicEnvironment.get_cooked_obj ~trust:false uri with
           C.InductiveDefinition (itl,_,_) ->
            let (_,_,_,cl) = List.nth itl i in
             let (_,cons) = List.nth cl (j - 1) in
@@ -1393,7 +1393,7 @@ and type_of_aux' metasenv context t =
 
         (* let's check if the type of branches are right *)
         let parsno =
-         match CicEnvironment.get_cooked_obj uri with
+         match CicEnvironment.get_cooked_obj ~trust:false uri with
             C.InductiveDefinition (_,_,parsno) -> parsno
           | _ ->
             raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
@@ -1504,7 +1504,7 @@ in if not res then prerr_endline ("#### " ^ CicPp.ppterm (type_of_aux context p)
     | ((uri,t) as subst)::tl ->
        let typeofvar =
         CicSubstitution.subst_vars substs (type_of_variable uri) in
-       (match CicEnvironment.get_cooked_obj uri with
+       (match CicEnvironment.get_cooked_obj ~trust:false uri with
            Cic.Variable (_,Some bo,_,_) ->
             raise
              (NotWellTyped
@@ -1568,7 +1568,7 @@ in if not res then prerr_endline ("#### " ^ CicPp.ppterm (type_of_aux context p)
    match CicReduction.whd context ty with
       C.MutInd (uri,i,_) ->
        (*CSC: definire una funzioncina per questo codice sempre replicato *)
-       (match CicEnvironment.get_cooked_obj uri with
+       (match CicEnvironment.get_cooked_obj ~trust:false uri with
            C.InductiveDefinition (itl,_,_) ->
             let (_,is_inductive,_,_) = List.nth itl i in
              if is_inductive then None else (Some uri)
@@ -1630,7 +1630,7 @@ let typecheck uri =
  let module C = Cic in
  let module R = CicReduction in
  let module U = UriManager in
-  match CicEnvironment.is_type_checked uri with
+  match CicEnvironment.is_type_checked ~trust:false uri with
      CicEnvironment.CheckedObj _ -> ()
    | CicEnvironment.UncheckedObj uobj ->
       (* let's typecheck the uncooked object *)
@@ -1644,10 +1644,16 @@ let typecheck uri =
           (* only to check that ty is well-typed *)
           let _ = type_of ty in ()
         | C.CurrentProof (_,conjs,te,ty,_) ->
-            (*CSC: bisogna controllare anche il metasenv!!! *)
+           let _ =
+            List.fold_left
+             (fun metasenv ((_,context,ty) as conj) ->
+               ignore (type_of_aux' metasenv context ty) ;
+               metasenv @ [conj]
+             ) [] conjs
+           in
             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
+             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 *)