From 15271270eecc6ebe1f042049e13e2c21c550660a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 2 Feb 2009 13:28:08 +0000 Subject: [PATCH] CicTypeChecker.typecheck now takes an additional parameter: - trust:bool, set to false only by the proofChecker daemon, while the refiner (for example) passes true --- .../components/cic_proof_checking/cicTypeChecker.ml | 6 +++--- .../components/cic_proof_checking/cicTypeChecker.mli | 4 +++- helm/software/daemons/proofChecker/Makefile | 2 +- helm/software/daemons/proofChecker/proofChecker.ml | 3 ++- 4 files changed, 9 insertions(+), 6 deletions(-) diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml index ca7682706..c38c15b93 100644 --- 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 98cb72ad7..a3361fc7b 100644 --- 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 4be11212f..0afd0a7a5 100644 --- 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 1b3661e34..2928cf648 100644 --- 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'); -- 2.39.2