CicTypeChecker.typecheck now takes an additional parameter:

- trust:bool, set to false only by the proofChecker daemon, while
  the refiner (for example) passes true

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index ca76827068c7b893326369800910c27676ebf1e0..c38c15b931cdea943fda830e4097790503ef5501 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -2087,12 +2087,12 @@ let typecheck_obj0 ~logger uri (obj,unchecked_ugraph) =
    check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri obj
 ;;
 
-let typecheck uri =
+let typecheck ?(trust=true) uri =
  let module C = Cic in
  let module R = CicReduction in
  let module U = UriManager in
  let logger = new CicLogger.logger in
-   match CicEnvironment.is_type_checked ~trust:false CicUniv.empty_ugraph uri with
+   match CicEnvironment.is_type_checked ~trust CicUniv.empty_ugraph uri with
    | CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
    | CicEnvironment.UncheckedObj (uobj,unchecked_ugraph) ->
       (* let's typecheck the uncooked object *)
@@ -2100,7 +2100,7 @@ let typecheck uri =
       let ugraph, ul, obj = typecheck_obj0 ~logger uri (uobj,unchecked_ugraph) in
       CicEnvironment.set_type_checking_info uri (obj,ugraph,ul);
       logger#log (`Type_checking_completed uri);
-      match CicEnvironment.is_type_checked ~trust:false CicUniv.empty_ugraph uri with
+      match CicEnvironment.is_type_checked ~trust CicUniv.empty_ugraph uri with
       | CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
       | _ -> raise CicEnvironmentError
 ;;

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.mli b/helm/software/components/cic_proof_checking/cicTypeChecker.mli
index 98cb72ad773577cd9d2b2e5dc3952dbdf57bc657..a3361fc7be609f6c860cd5788de5662bb59fd148 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.mli
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.mli
@@ -37,7 +37,9 @@ val debrujin_constructor :
  ?check_exp_named_subst: bool ->
   UriManager.uri -> int -> Cic.context -> Cic.term -> Cic.term
 
-val typecheck : UriManager.uri -> Cic.obj * CicUniv.universe_graph
+  (* defaults to true *)
+val typecheck : 
+  ?trust:bool -> UriManager.uri -> Cic.obj * CicUniv.universe_graph
 
 (* FUNCTIONS USED ONLY IN THE TOPLEVEL *)
 

diff --git a/helm/software/daemons/proofChecker/Makefile b/helm/software/daemons/proofChecker/Makefile
index 4be11212f2609333a94bb3c493513d443b375e94..0afd0a7a50f940c3db7c3b11c9952336905a03cf 100644 (file)
--- a/helm/software/daemons/proofChecker/Makefile
+++ b/helm/software/daemons/proofChecker/Makefile
@@ -1,7 +1,7 @@
 BIN_DIR = /usr/local/bin
 REQUIRES = helm-cic_proof_checking http
 PREDICATES =
-OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -thread
+OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -thread -rectypes
 ifeq ($(origin OCAMLPATH), undefined)
 OCAMLFIND = OCAMLPATH=../../components/METAS ocamlfind
 else

diff --git a/helm/software/daemons/proofChecker/proofChecker.ml b/helm/software/daemons/proofChecker/proofChecker.ml
index 1b3661e3471dcdb262f4da1dd19fe5f82bb3c125..2928cf6484b4a85ea0daefe48d36aab6261fa305 100644 (file)
--- a/helm/software/daemons/proofChecker/proofChecker.ml
+++ b/helm/software/daemons/proofChecker/proofChecker.ml
@@ -107,7 +107,8 @@ let callback (req : Http_types.request) outchan' =
           fprintf outchan' "%s" (html_preamble uri);
           flush outchan';
           (try
-            ignore (CicTypeChecker.typecheck (UriManager.uri_of_string uri));
+            ignore (CicTypeChecker.typecheck ~trust:false 
+              (UriManager.uri_of_string uri));
            with e ->
             fprintf outchan' "%s\n" (Printexc.to_string e);
             flush outchan');