Better implementation of the trusting machinery: some CicEnvironment functions

now have a trust optional attribute (that defaults to true). The TypeChecker
uses the false value only when type-checking the topmost object.

Every other operation of the kernel uses the true value (i.e. it trusts).
Is this really a safe behaviour? Hmmmmm. We need a proof here.

diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
index 329615bb3b5692740033c57c1f3d2f0cf2aebc39..e9050cd8c1867ac6f0686abc2094facedfabcd9f 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml
+++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
@@ -37,9 +37,7 @@
 
 let cleanup_tmp = true;;
 
-let never_trust = function uri -> false;;
-let always_trust = function uri -> true;;
-let trust_obj = ref never_trust;;
+let trust_obj = function uri -> true;;
 
 type type_checked_obj =
    CheckedObj of Cic.obj     (* cooked obj *)
@@ -169,7 +167,6 @@ let find_or_add_unchecked_to_cache uri =
 (* must be called once the type-checking of uri is finished *)
 (* The object whose uri is uri is unfreezed                 *)
 let set_type_checking_info uri =
- trust_obj := never_trust ;
  Cache.frozen_to_cooked uri
 ;;
 
@@ -179,43 +176,42 @@ let set_type_checking_info uri =
 (* otherwise it freezes the term for type-checking and returns
  it *)
 (* set_type_checking_info must be called to unfreeze the term         *)
-let is_type_checked uri =
+let is_type_checked ?(trust=true) uri =
  try
   CheckedObj (Cache.find_cooked uri)
  with
   Not_found ->
    let obj = find_or_add_unchecked_to_cache uri in
     Cache.unchecked_to_frozen uri ;
-    if !trust_obj uri then
+    if trust && trust_obj uri then
      begin
       Logger.log (`Trusting uri) ;
       set_type_checking_info uri ;
-      trust_obj := always_trust ;
       CheckedObj (Cache.find_cooked uri)
      end
     else
-     begin
-      trust_obj := always_trust ;
-      UncheckedObj obj
-     end
+     UncheckedObj obj
 ;;
 
-(* get_cooked_obj uri                                                        *)
-(* returns the cooked cic object whose uri is uri. The term must be present  *)
-(* and cooked in cache                                                       *)
-let get_cooked_obj uri =
+(* get_cooked_obj ~trust uri *)
+(* returns the object if it is already type-checked or if it can be *)
+(* trusted (if [trust] = true and the trusting function accepts it) *)
+(* Otherwise it raises Not_found                                    *)
+let get_cooked_obj ?(trust=true) uri =
  try
   Cache.find_cooked uri
  with Not_found ->
-  if not (!trust_obj uri) then
+  if trust && trust_obj uri then
    begin
-    prerr_endline ("@@@ OOOOOOOPS: WE DO NOT TRUST " ^ UriManager.string_of_uri uri ^ " EVEN IF WE ARE REQUIRED TO DO THAT! THAT MAY MEAN LOOKING FOR TROUBLES ;-(") ;
-    raise Not_found
+    match is_type_checked uri with
+       CheckedObj obj -> obj
+     | _ -> assert false
    end
   else
-   match is_type_checked uri with
-      CheckedObj obj -> obj
-    | _ -> assert false
+   begin
+    prerr_endline ("@@@ OOOOOOOPS: get_cooked_obj(" ^ UriManager.string_of_uri uri ^ ") raises Not_found since the object is not type-checked nor trusted.") ;
+    raise Not_found
+   end
 ;;
 
 (* get_obj uri                                                                *)

diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.mli b/helm/ocaml/cic_proof_checking/cicEnvironment.mli
index c54df77e2ef2f0dec7516b326c3c17695f6ddb90..fbc53955ba80483c15311d4206cb144fe8e367d3 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicEnvironment.mli
+++ b/helm/ocaml/cic_proof_checking/cicEnvironment.mli
@@ -53,7 +53,7 @@ type type_checked_obj =
 (* otherwise it returns (false,object) and freeze the object for    *)
 (* type-checking                                                    *)
 (* set_type_checking_info must be called to unfreeze the object     *)
-val is_type_checked : UriManager.uri -> type_checked_obj
+val is_type_checked : ?trust:bool -> UriManager.uri -> type_checked_obj
 
 (* set_type_checking_info uri                                         *)
 (* must be called once the type-checking of uri is finished           *)
@@ -61,5 +61,8 @@ val is_type_checked : UriManager.uri -> type_checked_obj
 (* again in the future (is_type_checked will return true)             *)
 val set_type_checking_info : UriManager.uri -> unit
 
-(* get_cooked_obj uri *)
-val get_cooked_obj : UriManager.uri -> Cic.obj
+(* get_cooked_obj ~trust uri *)
+(* returns the object if it is already type-checked or if it can be *)
+(* trusted (if [trust] = true and the trusting function accepts it) *)
+(* Otherwise it raises Not_found                                    *)
+val get_cooked_obj : ?trust:bool -> UriManager.uri -> Cic.obj

diff --git a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
index e45702077691e3f9053d6af5d715c3f243dec13f..3b769b5bcec98db1a51ca07c7d7ea8c1a9bce386 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
+++ b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
@@ -82,7 +82,7 @@ prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -
         CicSubstitution.lift m (List.assq uri ens)
        else
         let params =
-         (match CicEnvironment.get_cooked_obj uri with
+         (match CicEnvironment.get_obj uri with
              C.Constant _ -> raise ReferenceToConstant
            | C.Variable (_,_,_,params) -> params
            | C.CurrentProof _ -> raise ReferenceToCurrentProof
@@ -111,7 +111,7 @@ prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -
      | C.Appl l -> C.Appl (List.map (unwind_aux m) l)
      | C.Const (uri,exp_named_subst) ->
         let params =
-         (match CicEnvironment.get_cooked_obj uri with
+         (match CicEnvironment.get_obj uri with
              C.Constant (_,_,_,params) -> params
            | C.Variable _ -> raise ReferenceToVariable
            | C.CurrentProof (_,_,_,_,params) -> params
@@ -124,7 +124,7 @@ prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -
           C.Const (uri,exp_named_subst')
      | C.MutInd (uri,i,exp_named_subst) ->
         let params =
-         (match CicEnvironment.get_cooked_obj uri with
+         (match CicEnvironment.get_obj uri with
              C.Constant _ -> raise ReferenceToConstant
            | C.Variable _ -> raise ReferenceToVariable
            | C.CurrentProof _ -> raise ReferenceToCurrentProof
@@ -137,7 +137,7 @@ prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -
           C.MutInd (uri,i,exp_named_subst')
      | C.MutConstruct (uri,i,j,exp_named_subst) ->
         let params =
-         (match CicEnvironment.get_cooked_obj uri with
+         (match CicEnvironment.get_obj uri with
              C.Constant _ -> raise ReferenceToConstant
            | C.Variable _ -> raise ReferenceToVariable
            | C.CurrentProof _ -> raise ReferenceToCurrentProof
@@ -259,7 +259,7 @@ let reduce context : config -> Cic.term =
        if List.exists (function (uri',_) -> UriManager.eq uri' uri) ens then
         reduce (0, [], [], List.assq uri ens, s)
        else
-        (match CicEnvironment.get_cooked_obj uri with
+        (match CicEnvironment.get_obj uri with
             C.Constant _ -> raise ReferenceToConstant
           | C.CurrentProof _ -> raise ReferenceToCurrentProof
           | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
@@ -319,7 +319,7 @@ let reduce context : config -> Cic.term =
        C.Appl (List.append (List.map (unwind k e ens) l) s)
 *)
    | (k, e, ens, (C.Const (uri,exp_named_subst) as t), s) ->
-      (match CicEnvironment.get_cooked_obj uri with
+      (match CicEnvironment.get_obj uri with
           C.Constant (_,Some body,_,_) ->
            let ens' = push_exp_named_subst k e ens exp_named_subst in
             (* constants are closed *)
@@ -598,8 +598,8 @@ let are_convertible =
    else
     begin
      debug t1 [t2] "PREWHD";
-     let t1' = whd context t1 
-     and t2' = whd context t2 in
+     let t1' = whd context t1 in
+     let t2' = whd context t2 in
       debug t1' [t2'] "POSTWHD";
       aux2 t1' t2'
     end

diff --git a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
index f7ddd1968047db0a87abba9954140be3762cbd10..581c5918f4c78c301c1ba65009cc48aa2fc222da 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
+++ b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
@@ -57,7 +57,7 @@ let whd context =
         | None -> raise RelToHiddenHypothesis
        )
     | C.Var (uri,exp_named_subst) as t ->
-       (match CicEnvironment.get_cooked_obj uri with
+       (match CicEnvironment.get_cooked_obj ~trust:false uri with
            C.Constant _ -> raise ReferenceToConstant
          | C.CurrentProof _ -> raise ReferenceToCurrentProof
          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
@@ -80,7 +80,7 @@ let whd context =
     | C.Appl (he::tl) -> whdaux (tl@l) he
     | C.Appl [] -> raise (Impossible 1)
     | C.Const (uri,exp_named_subst) as t ->
-       (match CicEnvironment.get_cooked_obj uri with
+       (match CicEnvironment.get_cooked_obj ~trust:false uri with
            C.Constant (_,Some body,_,_) ->
             whdaux l (CicSubstitution.subst_vars exp_named_subst body)
          | C.Constant _ -> if l = [] then t else C.Appl (t::l)

diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.ml b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
index 002ea28df102ecf9c849306017d20d4ef19a37fb..4a938acb9c209be1cbbab3e338f35c6bbf19538e 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicSubstitution.ml
+++ b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
@@ -202,7 +202,7 @@ prerr_endline ("@@@POSSIBLE BUG: SUBSTITUTION IS NOT SIMULTANEOUS") ;
         with
          Not_found ->
           let params =
-           (match CicEnvironment.get_cooked_obj uri with
+           (match CicEnvironment.get_cooked_obj ~trust:true uri with
                C.Constant _ -> raise ReferenceToConstant
              | C.Variable (_,_,_,params) -> params
              | C.CurrentProof _ -> raise ReferenceToCurrentProof
@@ -250,7 +250,7 @@ prerr_endline "---- END\n\n " ;
     | C.Appl _ -> assert false
     | C.Const (uri,exp_named_subst')  ->
        let params =
-        (match CicEnvironment.get_cooked_obj uri with
+        (match CicEnvironment.get_cooked_obj ~trust:true uri with
             C.Constant (_,_,_,params) -> params
           | C.Variable _ -> raise ReferenceToVariable
           | C.CurrentProof (_,_,_,_,params) -> params
@@ -263,7 +263,7 @@ prerr_endline "---- END\n\n " ;
          C.Const (uri,exp_named_subst'')
     | C.MutInd (uri,typeno,exp_named_subst') ->
        let params =
-        (match CicEnvironment.get_cooked_obj uri with
+        (match CicEnvironment.get_cooked_obj ~trust:true uri with
             C.Constant _ -> raise ReferenceToConstant
           | C.Variable _ -> raise ReferenceToVariable
           | C.CurrentProof _ -> raise ReferenceToCurrentProof
@@ -276,7 +276,7 @@ prerr_endline "---- END\n\n " ;
          C.MutInd (uri,typeno,exp_named_subst'')
     | C.MutConstruct (uri,typeno,consno,exp_named_subst') ->
        let params =
-        (match CicEnvironment.get_cooked_obj uri with
+        (match CicEnvironment.get_cooked_obj ~trust:true uri with
             C.Constant _ -> raise ReferenceToConstant
           | C.Variable _ -> raise ReferenceToVariable
           | C.CurrentProof _ -> raise ReferenceToCurrentProof

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 57bc5e2ad3698be43ae6a93e77d45b0273d100bb..7e96de2a42aca82b8acdc7e7d57ebba1d949840a 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 *)