From 218c0062f93dd3221b0266cfbc26fd9cf787ad18 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 17 Jan 2005 16:24:17 +0000 Subject: [PATCH] new cicEnvironment implementation --- helm/gTopLevel/gTopLevel.ml | 6 +- helm/gTopLevel/testlibrary.ml | 27 +- helm/ocaml/cic_disambiguation/disambiguate.ml | 8 +- helm/ocaml/cic_omdoc/cic2content.ml | 6 +- helm/ocaml/cic_omdoc/doubleTypeInference.ml | 14 +- helm/ocaml/cic_omdoc/eta_fixing.ml | 4 +- helm/ocaml/cic_proof_checking/cicElim.ml | 2 +- .../cic_proof_checking/cicEnvironment.ml | 864 ++++++++++-------- .../cic_proof_checking/cicEnvironment.mli | 65 +- helm/ocaml/cic_proof_checking/cicPp.ml | 6 +- .../cic_proof_checking/cicReductionMachine.ml | 14 +- .../cic_proof_checking/cicReductionNaif.ml | 6 +- .../cic_proof_checking/cicSubstitution.ml | 8 +- .../cic_proof_checking/cicTypeChecker.ml | 53 +- helm/ocaml/cic_proof_checking/cicUnivUtils.ml | 27 +- helm/ocaml/cic_transformations/acic2Ast.ml | 2 +- helm/ocaml/cic_unification/cicRefine.ml | 10 +- helm/ocaml/tactics/discriminationTactics.ml | 8 +- helm/ocaml/tactics/primitiveTactics.ml | 6 +- helm/ocaml/tactics/proofEngineReduction.ml | 12 +- 20 files changed, 603 insertions(+), 545 deletions(-) diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 2276fdac4..e06c02297 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -460,7 +460,7 @@ let qed () = pathname_of_annuri (UriManager.buri_of_uri uri) in let list_of_universes = - CicUnivUtils.universes_of_obj (Cic.Constant ("",None,ty,[])) + CicUnivUtils.universes_of_obj uri (Cic.Constant ("",None,ty,[])) in let u1_clean = CicUniv.clean_ugraph u1 list_of_universes in let u2 = CicUniv.fill_empty_nodes_with_uri u1_clean uri in @@ -880,7 +880,7 @@ let (`Error (`T (Printexc.to_string e))) in let show_in_show_window_uri uri = - let obj,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in + let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in show_in_show_window_obj uri obj in let show_in_show_window_callback mmlwidget ((n : Gdome.element option),_,_,_) = @@ -1593,7 +1593,7 @@ let open_ () = ignore(CicTypeChecker.typecheck uri CicUniv.empty_ugraph); (* TASSI: typecheck mette la uri nell'env... cosa fa la open_ ?*) let metasenv,bo,ty = - match fst(CicEnvironment.get_cooked_obj uri CicUniv.empty_ugraph) with + match fst(CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri ) with Cic.Constant (_,Some bo,ty,_) -> [],bo,ty | Cic.CurrentProof (_,metasenv,bo,ty,_) -> metasenv,bo,ty | Cic.Constant _ diff --git a/helm/gTopLevel/testlibrary.ml b/helm/gTopLevel/testlibrary.ml index f35ee096a..34f71d412 100644 --- a/helm/gTopLevel/testlibrary.ml +++ b/helm/gTopLevel/testlibrary.ml @@ -8,7 +8,15 @@ Helm_registry.load_from "gTopLevel.conf.xml";; let mqi_debug_fun s = HelmLogger.log ~append_NL:true (`Msg (`T s)) let mqi_flags = [] + +let dbd = Mysql.quick_connect + ~host:(Helm_registry.get "db.host") + ~user:(Helm_registry.get "db.user") + ~database:(Helm_registry.get "db.database") + () +(* let mqi_handle = MQIConn.init ~flags:mqi_flags ~log:mqi_debug_fun () +*) let verbose = false @@ -40,11 +48,11 @@ let debug_print s = prerr_endline ("^^^^^^ " ^ s) let test_uri typecheck uri = if typecheck then - try ignore(CicTypeChecker.typecheck uri);1 + try ignore(CicTypeChecker.typecheck uri CicUniv.empty_ugraph);1 with CicTypeChecker.TypeCheckerFailure s | CicTypeChecker.AssertFailure s -> 0 else - let obj = CicEnvironment.get_obj uri in + let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in let (annobj, _, _, ids_to_inner_sorts, _, _, _) = Cic2acic.acic_object_of_cic_object ~eta_fix:false obj in @@ -52,17 +60,19 @@ let test_uri typecheck uri = let round_trip annterm = debug_print "(1) acic -> ast"; let (ast, _) = - Acic2Ast.ast_of_acic ids_to_inner_sorts ids_to_uris annterm + Acic2Ast.ast_of_acic ids_to_inner_sorts (*ids_to_uris*) annterm in let new_pp = BoxPp.pp_term ast in debug_print ("ast:\n" ^ new_pp); let new_ast = CicTextualParser2.parse_term (Stream.of_string new_pp) in debug_print ("new_ast:\n" ^ CicAstPp.pp_term ast); let res = - Disambiguate'.disambiguate_term mqi_handle [] [] new_ast - DisambiguateTypes.Environment.empty in + Disambiguate'.disambiguate_term ~dbd [] [] new_ast + ~aliases:DisambiguateTypes.Environment.empty + ~initial_ugraph:CicUniv.empty_ugraph + in List.iter - (fun (domain, _, term) -> + (fun (domain, _, term, _) -> debug_print ("domain: " ^ CicTextualParser2.EnvironmentP3.to_string domain) ; debug_print ("term: " ^ CicPp.ppterm term) @@ -153,10 +163,7 @@ let do_uri typecheck (ok, nok, maybe, timeout) uri = maybe := uri_str :: !maybe | `TimeOut -> print_endline "[TIMEOUT!]"; - timeout := uri_str :: !timeout); - print_endline "--"; - print_endline (CicUniv.print_stats ()); - print_endline "--" + timeout := uri_str :: !timeout) let do_file typecheck status fname = try diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index 2eafc81f3..b39d35f07 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -235,7 +235,7 @@ let interpretate ~context ~env ast = match cic with | Cic.Const (uri, []) -> let uris = - let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with (*match CicTypeChecker.typecheck uri with*) | Cic.Constant (_, _, _, uris) -> uris @@ -244,7 +244,7 @@ let interpretate ~context ~env ast = Cic.Const (uri, mk_subst uris) | Cic.Var (uri, []) -> let uris = - let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with (*match CicTypeChecker.typecheck uri with*) | Cic.Variable (_, _, _, uris) -> uris @@ -253,7 +253,7 @@ let interpretate ~context ~env ast = Cic.Var (uri, mk_subst uris) | Cic.MutInd (uri, i, []) -> let uris = - let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with (*match CicTypeChecker.typecheck uri with*) | Cic.InductiveDefinition (_, uris, _) -> uris @@ -262,7 +262,7 @@ let interpretate ~context ~env ast = Cic.MutInd (uri, i, mk_subst uris) | Cic.MutConstruct (uri, i, j, []) -> let uris = - let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with (*match CicTypeChecker.typecheck uri with*) | Cic.InductiveDefinition (_, uris, _) -> uris diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml index 56459d197..c91eb200b 100644 --- a/helm/ocaml/cic_omdoc/cic2content.ml +++ b/helm/ocaml/cic_omdoc/cic2content.ml @@ -369,7 +369,7 @@ let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts if sort ="Prop" then let inductive_types = (let o,_ = - CicEnvironment.get_obj uri CicUniv.empty_ugraph + CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with Cic.Constant _ -> assert false @@ -541,7 +541,7 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t = else raise Not_a_proof | C.AMutCase (id,uri,typeno,ty,te,patterns) -> let inductive_types,noparams = - (let o, _ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in + (let o, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with Cic.Constant _ -> assert false | Cic.Variable _ -> assert false @@ -690,7 +690,7 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts = let ind_str = (prefix ^ ".ind") in let ind_uri = UriManager.uri_of_string ind_str in let inductive_types,noparams = - (let o,_ = CicEnvironment.get_obj ind_uri CicUniv.empty_ugraph in + (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph ind_uri in match o with Cic.Constant _ -> assert false | Cic.Variable _ -> assert false diff --git a/helm/ocaml/cic_omdoc/doubleTypeInference.ml b/helm/ocaml/cic_omdoc/doubleTypeInference.ml index 235d8d835..e16aa789f 100644 --- a/helm/ocaml/cic_omdoc/doubleTypeInference.ml +++ b/helm/ocaml/cic_omdoc/doubleTypeInference.ml @@ -266,7 +266,7 @@ let type_of_constant uri = let module R = CicReduction in let module U = UriManager in let cobj = - match CicEnvironment.is_type_checked uri CicUniv.empty_ugraph with + match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with CicEnvironment.CheckedObj (cobj,_) -> cobj | CicEnvironment.UncheckedObj uobj -> raise (NotWellTyped "Reference to an unchecked constant") @@ -281,7 +281,7 @@ let type_of_variable uri = let module C = Cic in let module R = CicReduction in let module U = UriManager in - match CicEnvironment.is_type_checked uri CicUniv.empty_ugraph with + match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_)),_) -> ty | CicEnvironment.UncheckedObj (C.Variable _) -> raise (NotWellTyped "Reference to an unchecked variable") @@ -293,7 +293,7 @@ let 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 CicUniv.empty_ugraph with + match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with CicEnvironment.CheckedObj (cobj,_) -> cobj | CicEnvironment.UncheckedObj uobj -> raise (NotWellTyped "Reference to an unchecked inductive type") @@ -310,7 +310,7 @@ let 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 CicUniv.empty_ugraph with + match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with CicEnvironment.CheckedObj (cobj,_) -> cobj | CicEnvironment.UncheckedObj uobj -> raise (NotWellTyped "Reference to an unchecked constructor") @@ -539,7 +539,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = let (cl,parsno) = let obj,_ = try - CicEnvironment.get_cooked_obj uri CicUniv.empty_ugraph + CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri with Not_found -> assert false in match obj with @@ -642,7 +642,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = let uris_and_types = let obj,_ = try - CicEnvironment.get_cooked_obj uri CicUniv.empty_ugraph + CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri with Not_found -> assert false in match obj with @@ -654,7 +654,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = (function uri -> let obj,_ = try - CicEnvironment.get_cooked_obj uri CicUniv.empty_ugraph + CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri with Not_found -> assert false in match obj with diff --git a/helm/ocaml/cic_omdoc/eta_fixing.ml b/helm/ocaml/cic_omdoc/eta_fixing.ml index b86779337..41cc72738 100644 --- a/helm/ocaml/cic_omdoc/eta_fixing.ml +++ b/helm/ocaml/cic_omdoc/eta_fixing.ml @@ -237,7 +237,7 @@ let eta_fix metasenv context t = let term' = eta_fix' context term in let patterns' = List.map (eta_fix' context) patterns in let inductive_types,noparams = - let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in (match o with Cic.Constant _ -> assert false | Cic.Variable _ -> assert false @@ -297,7 +297,7 @@ let eta_fix metasenv context t = (fun newsubst (uri,t) -> let t' = eta_fix' context t in let ty = - let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with Cic.Variable (_,_,ty,_) -> CicSubstitution.subst_vars newsubst ty diff --git a/helm/ocaml/cic_proof_checking/cicElim.ml b/helm/ocaml/cic_proof_checking/cicElim.ml index b46aa0b22..1864e89b0 100644 --- a/helm/ocaml/cic_proof_checking/cicElim.ml +++ b/helm/ocaml/cic_proof_checking/cicElim.ml @@ -247,7 +247,7 @@ let branch (uri, typeno) insource liftno paramsno t fix head args = branch (uri, typeno) insource paramsno t fix head args let elim_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno = - let (obj, univ) = (CicEnvironment.get_obj uri CicUniv.empty_ugraph) in + let (obj, univ) = (CicEnvironment.get_obj CicUniv.empty_ugraph uri) in match obj with | Cic.InductiveDefinition (indTypes, params, leftno) -> let (name, inductive, ty, constructors) = diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml index 0f01a0a55..62e733522 100644 --- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml +++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml @@ -36,32 +36,45 @@ (*****************************************************************************) -let cleanup_tmp = true;; +(* ************************************************************************** * + CicEnvironment SETTINGS (trust and clean_tmp) + * ************************************************************************** *) +let cleanup_tmp = true;; let trust = ref (fun _ -> true);; let set_trust f = trust := f let trust_obj uri = !trust uri + +(* ************************************************************************** * + TYPES + * ************************************************************************** *) + type type_checked_obj = CheckedObj of (Cic.obj * CicUniv.universe_graph) (* cooked obj *) | UncheckedObj of Cic.obj (* uncooked obj to proof-check *) ;; - exception AlreadyCooked of string;; exception CircularDependency of string;; exception CouldNotFreeze of string;; exception CouldNotUnfreeze of string;; exception Term_not_found of UriManager.uri;; + +(* ************************************************************************** * + HERE STARTS THE CACHE MODULE + * ************************************************************************** *) + (* Cache that uses == instead of = for testing equality *) (* Invariant: an object is always in at most one of the *) (* following states: unchecked, frozen and cooked. *) module Cache : sig - val find_or_add_unchecked : + val find_or_add_to_unchecked : UriManager.uri -> - get_object_to_add:(unit -> Cic.obj * CicUniv.universe_graph option) -> + get_object_to_add: + (UriManager.uri -> Cic.obj * CicUniv.universe_graph option) -> Cic.obj * CicUniv.universe_graph val can_be_cooked: UriManager.uri -> bool @@ -75,310 +88,331 @@ module Cache : key:UriManager.uri -> Cic.obj * CicUniv.universe_graph val add_cooked : key:UriManager.uri -> (Cic.obj * CicUniv.universe_graph) -> unit - val not_jet_cooked: - UriManager.uri -> Cic.obj * CicUniv.universe_graph val remove: UriManager.uri -> unit - val dump_to_channel : ?callback:(string -> unit) -> out_channel -> unit val restore_from_channel : ?callback:(string -> unit) -> in_channel -> unit val empty : unit -> unit val is_in_frozen: UriManager.uri -> bool val is_in_unchecked: UriManager.uri -> bool + val is_in_cooked: UriManager.uri -> bool end = struct (************************************************************************* TASSI: invariant - The CacheOfCookedObjects will contain only objects with a valid universe - graph. valid means that non None (used if there is no universe file + The cacheOfCookedObjects will contain only objects with a valid universe + graph. valid means that not None (used if there is no universe file in the universe generation phase). **************************************************************************) - module CacheOfCookedObjects : - sig - val mem : UriManager.uri -> bool - val find : UriManager.uri -> Cic.obj * CicUniv.universe_graph - val add : UriManager.uri -> (Cic.obj * CicUniv.universe_graph) -> unit - val remove : UriManager.uri -> unit - - (** (de)serialization of type checker cache *) - val dump_to_channel : ?callback:(string -> unit) -> out_channel -> unit - val restore_from_channel : ?callback:(string -> unit) -> in_channel -> unit - val empty : unit -> unit - end - = + + (* DATA: the data structure that implements the CACHE *) + module HashedType = struct - module HashedType = - struct - type t = UriManager.uri - let equal = UriManager.eq - let hash = Hashtbl.hash - end - ;; - module HT = Hashtbl.Make(HashedType);; - let hashtable = HT.create 1009;; - let mem uri = - try - HT.mem hashtable uri - with - Not_found -> false - ;; - let find uri = HT.find hashtable uri ;; - let add uri (obj,ugraph) = - HT.add hashtable uri (obj,ugraph) - ;; - let remove uri = - if mem uri then - HT.remove hashtable uri - else - raise (Term_not_found uri); - ;; + type t = UriManager.uri + let equal = UriManager.eq + let hash = Hashtbl.hash + end + ;; + + module HT = Hashtbl.Make(HashedType);; + let cacheOfCookedObjects = HT.create 1009;; + + (* DATA: The parking lists + * the lists elements are (uri * (obj * universe_graph option)) + * ( u, ( o, None )) means that the object has no universes file, this + * should happen only in the universe generation phase. + * FIXME: if the universe generation is integrated in the library + * exportation phase, the 'option' MUST be removed. + * ( u, ( o, Some g)) means that the object has a universes file, + * the usual case. + *) + + (* frozen is used to detect circular dependency. *) + let frozen_list = ref [];; + (* unchecked is used to store objects just fetched, nothing more. *) + let unchecked_list = ref [];; + + (* FIXED: should be ok even if not touched *) (* used to hash cons uris on restore to grant URI structure unicity *) - let restore_uris = - let module C = Cic in - let recons uri = - UriManager.uri_of_string (UriManager.string_of_uri uri) - in - let rec restore_in_term = - function - (C.Rel _) as t -> t - | C.Var (uri,exp_named_subst) -> - let uri' = recons uri in - let exp_named_subst' = - List.map - (function (uri,t) ->(recons uri,restore_in_term t)) - exp_named_subst - in - C.Var (uri',exp_named_subst') - | C.Meta (i,l) -> - let l' = - List.map - (function - None -> None - | Some t -> Some (restore_in_term t) - ) l - in - C.Meta(i,l') - | C.Sort _ as t -> t - | C.Implicit _ as t -> t - | C.Cast (te,ty) -> C.Cast (restore_in_term te, restore_in_term ty) - | C.Prod (n,s,t) -> C.Prod (n, restore_in_term s, restore_in_term t) - | C.Lambda (n,s,t) -> C.Lambda (n, restore_in_term s, restore_in_term t) - | C.LetIn (n,s,t) -> C.LetIn (n, restore_in_term s, restore_in_term t) - | C.Appl l -> C.Appl (List.map restore_in_term l) - | C.Const (uri,exp_named_subst) -> - let uri' = recons uri in - let exp_named_subst' = - List.map - (function (uri,t) -> (recons uri,restore_in_term t)) exp_named_subst - in - C.Const (uri',exp_named_subst') - | C.MutInd (uri,tyno,exp_named_subst) -> - let uri' = recons uri in - let exp_named_subst' = - List.map - (function (uri,t) -> (recons uri,restore_in_term t)) exp_named_subst - in - C.MutInd (uri',tyno,exp_named_subst') - | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> - let uri' = recons uri in - let exp_named_subst' = - List.map - (function (uri,t) -> (recons uri,restore_in_term t)) exp_named_subst - in - C.MutConstruct (uri',tyno,consno,exp_named_subst') - | C.MutCase (uri,i,outty,t,pl) -> - C.MutCase (recons uri, i, restore_in_term outty, restore_in_term t, - List.map restore_in_term pl) - | C.Fix (i, fl) -> - let len = List.length fl in - let liftedfl = - List.map - (fun (name, i, ty, bo) -> - (name, i, restore_in_term ty, restore_in_term bo)) - fl - in - C.Fix (i, liftedfl) - | C.CoFix (i, fl) -> - let len = List.length fl in - let liftedfl = - List.map - (fun (name, ty, bo) -> (name, restore_in_term ty, restore_in_term bo)) - fl - in - C.CoFix (i, liftedfl) - in - function - C.Constant (name,bo,ty,params) -> - let bo' = - match bo with - None -> None - | Some bo -> Some (restore_in_term bo) + let restore_uris = + let module C = Cic in + let recons uri = + UriManager.uri_of_string (UriManager.string_of_uri uri) + in + let rec restore_in_term = + function + (C.Rel _) as t -> t + | C.Var (uri,exp_named_subst) -> + let uri' = recons uri in + let exp_named_subst' = + List.map + (function (uri,t) ->(recons uri,restore_in_term t)) + exp_named_subst + in + C.Var (uri',exp_named_subst') + | C.Meta (i,l) -> + let l' = + List.map + (function + None -> None + | Some t -> Some (restore_in_term t) + ) l in - let ty' = restore_in_term ty in - let params' = List.map recons params in - C.Constant (name, bo', ty', params') - | C.CurrentProof (name,conjs,bo,ty,params) -> - let conjs' = - List.map - (function (i,hyps,ty) -> - (i, - List.map (function - None -> None - | Some (name,C.Decl t) -> - Some (name,C.Decl (restore_in_term t)) - | Some (name,C.Def (bo,ty)) -> - let ty' = - match ty with - None -> None - | Some ty'' -> Some (restore_in_term ty'') - in - Some (name,C.Def (restore_in_term bo, ty'))) hyps, - restore_in_term ty)) - conjs + C.Meta(i,l') + | C.Sort _ as t -> t + | C.Implicit _ as t -> t + | C.Cast (te,ty) -> C.Cast (restore_in_term te, restore_in_term ty) + | C.Prod (n,s,t) -> C.Prod (n, restore_in_term s, restore_in_term t) + | C.Lambda (n,s,t) -> C.Lambda (n, restore_in_term s, restore_in_term t) + | C.LetIn (n,s,t) -> C.LetIn (n, restore_in_term s, restore_in_term t) + | C.Appl l -> C.Appl (List.map restore_in_term l) + | C.Const (uri,exp_named_subst) -> + let uri' = recons uri in + let exp_named_subst' = + List.map + (function (uri,t) -> (recons uri,restore_in_term t)) exp_named_subst in - let bo' = restore_in_term bo in - let ty' = restore_in_term ty in - let params' = List.map recons params in - C.CurrentProof (name, conjs', bo', ty', params') - | C.Variable (name,bo,ty,params) -> - let bo' = - match bo with - None -> None - | Some bo -> Some (restore_in_term bo) + C.Const (uri',exp_named_subst') + | C.MutInd (uri,tyno,exp_named_subst) -> + let uri' = recons uri in + let exp_named_subst' = + List.map + (function (uri,t) -> (recons uri,restore_in_term t)) exp_named_subst in - let ty' = restore_in_term ty in - let params' = List.map recons params in - C.Variable (name, bo', ty', params') - | C.InductiveDefinition (tl,params,paramsno) -> - let params' = List.map recons params in - let tl' = - List.map (function (name, inductive, ty, constructors) -> - name, - inductive, - restore_in_term ty, - (List.map - (function (name, ty) -> name, restore_in_term ty) - constructors)) - tl + C.MutInd (uri',tyno,exp_named_subst') + | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> + let uri' = recons uri in + let exp_named_subst' = + List.map + (function (uri,t) -> (recons uri,restore_in_term t)) exp_named_subst in - C.InductiveDefinition (tl', params', paramsno) - - let dump_to_channel ?(callback = ignore) oc = - HT.iter (fun uri _ -> callback (UriManager.string_of_uri uri)) hashtable; - Marshal.to_channel oc hashtable [] ;; - let empty () = HT.clear hashtable ;; - let restore_from_channel ?(callback = ignore) ic = - let restored = Marshal.from_channel ic in - empty (); - HT.iter - (fun k v -> - callback (UriManager.string_of_uri k); - HT.add hashtable - (UriManager.uri_of_string (UriManager.string_of_uri k)) - -(************************************************ - TASSI: FIXME add channel stuff for universes -*************************************************) - - ((restore_uris v),CicUniv.empty_ugraph)) - restored - ;; + C.MutConstruct (uri',tyno,consno,exp_named_subst') + | C.MutCase (uri,i,outty,t,pl) -> + C.MutCase (recons uri, i, restore_in_term outty, restore_in_term t, + List.map restore_in_term pl) + | C.Fix (i, fl) -> + let len = List.length fl in + let liftedfl = + List.map + (fun (name, i, ty, bo) -> + (name, i, restore_in_term ty, restore_in_term bo)) + fl + in + C.Fix (i, liftedfl) + | C.CoFix (i, fl) -> + let len = List.length fl in + let liftedfl = + List.map + (fun (name, ty, bo) -> (name, restore_in_term ty, restore_in_term bo)) + fl + in + C.CoFix (i, liftedfl) + in + function + C.Constant (name,bo,ty,params) -> + let bo' = + match bo with + None -> None + | Some bo -> Some (restore_in_term bo) + in + let ty' = restore_in_term ty in + let params' = List.map recons params in + C.Constant (name, bo', ty', params') + | C.CurrentProof (name,conjs,bo,ty,params) -> + let conjs' = + List.map + (function (i,hyps,ty) -> + (i, + List.map (function + None -> None + | Some (name,C.Decl t) -> + Some (name,C.Decl (restore_in_term t)) + | Some (name,C.Def (bo,ty)) -> + let ty' = + match ty with + None -> None + | Some ty'' -> Some (restore_in_term ty'') + in + Some (name,C.Def (restore_in_term bo, ty'))) hyps, + restore_in_term ty)) + conjs + in + let bo' = restore_in_term bo in + let ty' = restore_in_term ty in + let params' = List.map recons params in + C.CurrentProof (name, conjs', bo', ty', params') + | C.Variable (name,bo,ty,params) -> + let bo' = + match bo with + None -> None + | Some bo -> Some (restore_in_term bo) + in + let ty' = restore_in_term ty in + let params' = List.map recons params in + C.Variable (name, bo', ty', params') + | C.InductiveDefinition (tl,params,paramsno) -> + let params' = List.map recons params in + let tl' = + List.map (function (name, inductive, ty, constructors) -> + name, + inductive, + restore_in_term ty, + (List.map + (function (name, ty) -> name, restore_in_term ty) + constructors)) + tl + in + C.InductiveDefinition (tl', params', paramsno) + ;; - end - ;; - let frozen_list = ref [];; - let unchecked_list = ref [];; + let empty () = + HT.clear cacheOfCookedObjects; + unchecked_list := [] ; + frozen_list := [] + ;; - let is_in_frozen uri = - List.mem_assoc uri !frozen_list - ;; - - let is_in_unchecked uri = - List.mem_assoc uri !unchecked_list - ;; - (******************************************************************* - TASSI: invariant - we need, in the universe generation phase, to traverse objects - that are not jet committed, so we search them in the frozen list. - Only uncommitted objects without a universe file (see the assertion) - can be searched with method - *******************************************************************) - let not_jet_cooked uri = - try - let o,u = List.assoc uri !frozen_list in - match u with - None -> o, CicUniv.empty_ugraph - | Some _ -> assert false (* only univ_maker ca use this *) - with Not_found -> - CacheOfCookedObjects.find uri - ;; - let find_or_add_unchecked uri ~get_object_to_add = + (* FIX: universe stuff?? *) + let dump_to_channel ?(callback = ignore) oc = + HT.iter (fun uri _ -> callback (UriManager.string_of_uri uri)) + cacheOfCookedObjects; + Marshal.to_channel oc cacheOfCookedObjects [] + ;; + + (* FIX: universes stuff?? *) + let restore_from_channel ?(callback = ignore) ic = + let restored = Marshal.from_channel ic in + (* FIXME: should this empty clean the frozen and unchecked? + * if not, the only-one-empty-end-not-3 patch is wrong + *) + empty (); + HT.iter + (fun k v -> + callback (UriManager.string_of_uri k); + HT.add cacheOfCookedObjects + (UriManager.uri_of_string (UriManager.string_of_uri k)) + (*********************************************** + TSSI: FIXME add channel stuff for universes + ************************************************) + ((restore_uris v),CicUniv.empty_ugraph)) + restored + ;; + + + let is_in_frozen uri = + List.mem_assoc uri !frozen_list + ;; + + let is_in_unchecked uri = + List.mem_assoc uri !unchecked_list + ;; + + let is_in_cooked uri = + HT.mem cacheOfCookedObjects uri + ;; + + + (******************************************************************* + TASSI: invariant + we need, in the universe generation phase, to traverse objects + that are not jet committed, so we search them in the frozen list. + Only uncommitted objects without a universe file (see the assertion) + can be searched with method + *******************************************************************) + + let find_or_add_to_unchecked uri ~get_object_to_add = try let o,g = List.assq uri !unchecked_list in - match g with - None -> o,CicUniv.empty_ugraph - | Some g' -> o,g' + match g with + (* FIXME: we accept both cases, as at the end of this function + * maybe the None universe outside the cache module should be + * avoided elsewhere. + * + * another thing that should be removed if univ generation phase + * and lib exportation are unified. + *) + None -> o,CicUniv.empty_ugraph + | Some g' -> o,g' with - Not_found -> - if List.mem_assq uri !frozen_list then - begin - print_endline "\nCircularDependency!\nfrozen list: \n"; - List.iter ( - fun (u,(_,o)) -> - let su = UriManager.string_of_uri u in - let univ = if o = None then "NO_UNIV" else "" in - print_endline (su^" "^univ)) - !frozen_list; - raise (CircularDependency (UriManager.string_of_uri uri)) - end - else - if CacheOfCookedObjects.mem uri then + Not_found -> + if List.mem_assq uri !frozen_list then + (* CIRCULAR DEPENDENCY DETECTED, print the error and raise *) + begin + print_endline "\nCircularDependency!\nfrozen list: \n"; + List.iter ( + fun (u,(_,o)) -> + let su = UriManager.string_of_uri u in + let univ = if o = None then "NO_UNIV" else "" in + print_endline (su^" "^univ)) + !frozen_list; + raise (CircularDependency (UriManager.string_of_uri uri)) + end + else + if HT.mem cacheOfCookedObjects uri then + (* DOUBLE COOK DETECTED, raise the exception *) raise (AlreadyCooked (UriManager.string_of_uri uri)) - else + else (* OK, it is not already frozen nor cooked *) - let obj,ugraph = get_object_to_add () in - let ugraph_real = - match ugraph with - None -> CicUniv.empty_ugraph - | Some g -> g - in - unchecked_list := (uri,(obj,ugraph))::!unchecked_list ; - obj,ugraph_real - ;; - let unchecked_to_frozen uri = - try - let obj,ugraph = List.assq uri !unchecked_list in - unchecked_list := List.remove_assq uri !unchecked_list ; - frozen_list := (uri,(obj,ugraph))::!frozen_list - with - Not_found -> raise (CouldNotFreeze (UriManager.string_of_uri uri)) - ;; + let obj,ugraph = get_object_to_add uri in + let ugraph_real = + match ugraph with + (* FIXME: not sure it is OK*) + None -> CicUniv.empty_ugraph + | Some g -> g + in + unchecked_list := (uri,(obj,ugraph))::!unchecked_list ; + obj,ugraph_real + ;; + + let unchecked_to_frozen uri = + try + let obj,ugraph = List.assq uri !unchecked_list in + unchecked_list := List.remove_assq uri !unchecked_list ; + frozen_list := (uri,(obj,ugraph))::!frozen_list + with + Not_found -> raise (CouldNotFreeze (UriManager.string_of_uri uri)) + ;; + + (************************************************************ TASSI: invariant only object with a valid universe graph can be committed + + this should disappear if the universe generation phase and the + library exportation are unified. *************************************************************) let frozen_to_cooked ~uri = try let obj,ugraph = List.assq uri !frozen_list in match ugraph with None -> - assert false (* only non dummy universes can be committed *) + assert false (* only NON dummy universes can be committed *) | Some g -> frozen_list := List.remove_assq uri !frozen_list ; - CacheOfCookedObjects.add uri (obj,g) + HT.add cacheOfCookedObjects uri (obj,g) with Not_found -> raise (CouldNotUnfreeze (UriManager.string_of_uri uri)) ;; + let can_be_cooked uri = try let obj,ugraph = List.assq uri !frozen_list in + (* FIXME: another thing to remove if univ generation phase and lib + * exportation are unified. + *) match ugraph with None -> false | Some _ -> true with Not_found -> false ;; + + (* this function injects a real universe graph in a (uri, (obj, None)) + * element of the frozen list. + * + * FIXME: another thing to remove if univ generation phase and lib + * exportation are unified. + *) let hack_univ uri real_ugraph = try let o,g = List.assq uri !frozen_list in @@ -390,109 +424,130 @@ module Cache : prerr_endline ( "You are probably hacking an object already hacked or an"^ " object that has the universe file but is not"^ - " jet committed"); + " yet committed."); assert false with Not_found -> prerr_endline ( "You are hacking an object that is not in the"^ " frozen_list, this means you are probably generating an"^ - " universe file for an object that already as an universe file"); + " universe file for an object that already"^ + " as an universe file"); assert false ;; - let find_cooked ~key:uri = CacheOfCookedObjects.find uri;; + + let find_cooked ~key:uri = HT.find cacheOfCookedObjects uri ;; + let add_cooked ~key:uri (obj,ugraph) = - CacheOfCookedObjects.add uri (obj,ugraph);; + HT.add cacheOfCookedObjects uri (obj,ugraph) + ;; + + (* invariant + * + * an object can be romeved from the cache only if we are not typechecking + * something. this means check and frozen must be empty. + *) let remove uri = if (!unchecked_list <> []) || (!frozen_list <> []) then failwith "CicEnvironment.remove while type checking" else - CacheOfCookedObjects.remove uri - ;; - let dump_to_channel = CacheOfCookedObjects.dump_to_channel;; - let restore_from_channel = CacheOfCookedObjects.restore_from_channel;; - let empty () = - CacheOfCookedObjects.empty (); - unchecked_list := [] ; - frozen_list := [] + HT.remove cacheOfCookedObjects uri ;; + end ;; +(* ************************************************************************ + HERE ENDS THE CACHE MODULE + * ************************************************************************ *) + +(* exported cache functions *) let dump_to_channel = Cache.dump_to_channel;; let restore_from_channel = Cache.restore_from_channel;; let empty = Cache.empty;; -let find_or_add_unchecked_to_cache uri = - Cache.find_or_add_unchecked uri - ~get_object_to_add: - (function () -> - let filename = Http_getter.getxml' uri in - let bodyfilename = - match UriManager.bodyuri_of_uri uri with - None -> None - | Some bodyuri -> - try - ignore (Http_getter.resolve' bodyuri) ; - (* The body exists ==> it is not an axiom *) - Some (Http_getter.getxml' bodyuri) - with - Http_getter_types.Key_not_found _ -> - (* The body does not exist ==> we consider it an axiom *) - None - in - - (* - maybe this is not the right place to do this.. but I think - obj_of_xml is called only here - *) - (* this brakes something : let _ = CicUniv.restart_numbering () in *) - let obj = CicParser.obj_of_xml filename bodyfilename in - let ugraph,filename_univ = - (* - try - let filename_univ = - Http_getter.getxml' ( - UriManager.uri_of_string ( - (UriManager.string_of_uri uri) ^ ".univ")) - in - (Some (CicUniv.ugraph_of_xml filename_univ),Some filename_univ) - with Failure s -> - - prerr_endline ( - "WE HAVE NO UNIVERSE FILE FOR " ^ (UriManager.string_of_uri uri)); - None,None - *) - (********************************************** - TASSI: should fail when universes will be ON - ***********************************************) - (Some CicUniv.empty_ugraph,None) - in - let cleanup () = - Unix.unlink filename ; - begin - match filename_univ with - Some f -> Unix.unlink f - | None -> () - end; - begin - match bodyfilename with - Some f -> Unix.unlink f - | None -> () - end +let get_object_to_add uri = + let filename = Http_getter.getxml' uri in + let bodyfilename = + match UriManager.bodyuri_of_uri uri with + None -> None + | Some bodyuri -> + try + ignore (Http_getter.resolve' bodyuri) ; + (* The body exists ==> it is not an axiom *) + Some (Http_getter.getxml' bodyuri) + with + Http_getter_types.Key_not_found _ -> + (* The body does not exist ==> we consider it an axiom *) + None + in + let cleanup () = + Unix.unlink filename ; + (* + begin + match filename_univ with + Some f -> Unix.unlink f + | None -> () + end; + *) + begin + match bodyfilename with + Some f -> Unix.unlink f + | None -> () + end + in + (* this brakes something : + * let _ = CicUniv.restart_numbering () in + *) + let obj = + try + CicParser.obj_of_xml filename bodyfilename + with exn -> + cleanup (); + raise exn + in + let ugraph,filename_univ = + (* FIXME: decomment this when the universes will be part of the library + try + let filename_univ = + Http_getter.getxml' ( + UriManager.uri_of_string ( + (UriManager.string_of_uri uri) ^ ".univ")) in - cleanup(); - obj,ugraph) + (Some (CicUniv.ugraph_of_xml filename_univ),Some filename_univ) + with Failure s -> + + prerr_endline ( + "WE HAVE NO UNIVERSE FILE FOR " ^ (UriManager.string_of_uri uri)); + Inix.unlink + None,None + *) + (********************************************** + TASSI: should fail when universes will be ON + ***********************************************) + (Some CicUniv.empty_ugraph,None) + in + cleanup(); + obj,ugraph ;; + +(* this is the function to fetch the object in the unchecked list and + * nothing more (except returning it) + *) +let find_or_add_to_unchecked uri = + Cache.find_or_add_to_unchecked uri ~get_object_to_add -(* set_type_checking_info uri *) -(* must be called once the type-checking of uri is finished *) -(* The object whose uri is uri is unfreezed *) +(* set_type_checking_info uri *) +(* must be called once the type-checking of uri is finished *) +(* The object whose uri is uri is unfreezed *) +(* *) +(* the replacement ugraph must be the one returned by the *) +(* typechecker, restricted with the CicUnivUtils.clean_and_fill *) let set_type_checking_info ?(replace_ugraph=None) uri = if Cache.can_be_cooked uri && replace_ugraph <> None then invalid_arg ( "?replace_ugraph must be None if you are not committing an "^ - "object that has an no universe graph associated "^ + "object that has a universe graph associated "^ "(can happen only in the fase of universes graphs generation)."); if not (Cache.can_be_cooked uri) && replace_ugraph = None then invalid_arg ( @@ -508,76 +563,82 @@ let set_type_checking_info ?(replace_ugraph=None) uri = Cache.frozen_to_cooked uri ;; - -(* is_type_checked uri *) -(* CSC: commento falso ed obsoleto *) -(* returns a CheckedObj if the term has been type-checked *) -(* 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 ?(trust=true) uri base_univ = - try - let o,u = Cache.find_cooked uri in - CheckedObj (o,CicUniv.merge_ugraphs u base_univ) - with - Not_found -> - let obj,ugraph = find_or_add_unchecked_to_cache uri in - Cache.unchecked_to_frozen uri ; - if trust && trust_obj uri then - begin - CicLogger.log (`Trusting uri) ; - set_type_checking_info uri ; - let o,u = Cache.find_cooked uri in - let u' = CicUniv.merge_ugraphs base_univ ugraph in - CheckedObj (o,u') - end - else - begin - UncheckedObj obj - end +(* fetch, unfreeze and commit an uri to the cacheOfCookedObjects and + * return the object,ugraph + *) +let add_trusted_uri_to_cache uri = + let o,u = find_or_add_to_unchecked uri in + Cache.unchecked_to_frozen uri; + set_type_checking_info uri; + try + Cache.find_cooked uri + with Not_found -> assert false ;; -(* 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 base_univ = - try - let o,u = Cache.find_cooked uri in - o,(CicUniv.merge_ugraphs base_univ u) - with Not_found -> - if trust && trust_obj uri then - begin - match is_type_checked uri base_univ with - CheckedObj (obj,ugraph) -> obj,(CicUniv.merge_ugraphs ugraph base_univ) - | _ -> assert false - end - else - 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 the uri, if we trust it will be added to the cacheOfCookedObjects *) +let get_cooked_obj ?(trust=true) base_univ uri = + try + (* the object should be in the cacheOfCookedObjects *) + let o,u = Cache.find_cooked uri in + o,(CicUniv.merge_ugraphs base_univ u) + with Not_found -> + (* this should be an error case, but if we trust the uri... *) + if trust && trust_obj uri then + (* trusting means that we will fetch cook it on the fly *) + let o,u = add_trusted_uri_to_cache uri in + o,(CicUniv.merge_ugraphs base_univ u) + else + (* we don't trust the uri, so we fail *) + begin + prerr_endline ("CACHE MISS: " ^ (UriManager.string_of_uri uri)); + raise Not_found + end + +(* This has not the old semantic :( but is what the name suggests + * + * let is_type_checked ?(trust=true) uri = + * try + * let _ = Cache.find_cooked uri in + * true + * with + * Not_found -> + * trust && trust_obj uri + * ;; + * + * as the get_cooked_obj but returns a type_checked_obj + * + *) +let is_type_checked ?(trust=true) base_univ uri = + try + let o,u = Cache.find_cooked uri in + CheckedObj (o,(CicUniv.merge_ugraphs base_univ u)) + with Not_found -> + (* this should return UncheckedObj *) + if trust && trust_obj uri then + (* trusting means that we will fetch cook it on the fly *) + let o,u = add_trusted_uri_to_cache uri in + CheckedObj ( o, CicUniv.merge_ugraphs u base_univ ) + else + let o,u = find_or_add_to_unchecked uri in + UncheckedObj o ;; -(* get_obj uri *) -(* returns the cic object whose uri is uri. If the term is not just in cache,*) -(* then it is parsed via CicParser.term_of_xml from the file whose name is *) -(* the result of Getter.getxml uri *) -let get_obj ?(not_jet_cooked=false) uri base_univ = - if not_jet_cooked then - let o,u = Cache.not_jet_cooked uri in +(* as the get cooked, but if not present the object is only fetched, + * not unfreezed and committed + *) +let get_obj base_univ uri = + try + (* the object should be in the cacheOfCookedObjects *) + let o,u = Cache.find_cooked uri in o,(CicUniv.merge_ugraphs base_univ u) - else - try - get_cooked_obj uri base_univ - with - Not_found -> - let s = ( UriManager.string_of_uri uri) in - let o,u = find_or_add_unchecked_to_cache uri in - o,(CicUniv.merge_ugraphs base_univ u) + with Not_found -> + (* this should be an error case, but if we trust the uri... *) + if trust_obj uri then + (* trusting we add it to the unchecked list *) + let o,u = find_or_add_to_unchecked uri in + o,(CicUniv.merge_ugraphs base_univ u) + else + raise Not_found ;; exception OnlyPutOfInductiveDefinitionsIsAllowed @@ -589,10 +650,9 @@ let put_inductive_definition uri (obj,ugraph) = ;; let in_cache uri = - try - ignore (Cache.find_cooked uri); - prerr_endline "TROVATO NELLA CHECKED";true - with Not_found -> + if Cache.is_in_cooked uri then + (prerr_endline "TROVATO NELLA CHECKED";true) + else if Cache.is_in_frozen uri then (prerr_endline "TROVATO NELLA FROZEN";true) else diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.mli b/helm/ocaml/cic_proof_checking/cicEnvironment.mli index c3ca6ef95..9875f52ac 100644 --- a/helm/ocaml/cic_proof_checking/cicEnvironment.mli +++ b/helm/ocaml/cic_proof_checking/cicEnvironment.mli @@ -23,47 +23,45 @@ * http://cs.unibo.it/helm/. *) -(*****************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 24/01/2000 *) -(* *) -(* This module implements a trival cache system (an hash-table) for cic *) -(* objects. Uses the getter (getter.ml) and the parser (cicParser.ml) *) -(* *) -(*****************************************************************************) +(****************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 24/01/2000 *) +(* *) +(* This module implements a trival cache system (an hash-table) for cic *) +(* ^^^^^^ *) +(* objects. Uses the getter (getter.ml) and the parser (cicParser.ml) *) +(* *) +(****************************************************************************) exception CircularDependency of string;; exception Term_not_found of UriManager.uri;; -(* get_obj uri *) -(* returns the cic object whose uri is uri. If the term is not just in cache,*) -(* then it is parsed via CicParser.term_of_xml from the file whose name is *) -(* the result of Getter.get uri *) -(* *) -(* ~not_jet_cooked returns the object even if it is not in the *) -(* CacheOfCookedObjects searching it in the frozen list. *) -(* This is necessary in cicUnivUtils.ml since (in the univ_maker phase *) -(* it has to traverse object before they are committed. *) -(* see the .ml file for some reassuring invariants on this. *) +(* as the get cooked, but if not present the object is only fetched, + * not unfreezed and committed + *) val get_obj : - ?not_jet_cooked:bool -> UriManager.uri -> CicUniv.universe_graph -> - Cic.obj * CicUniv.universe_graph + CicUniv.universe_graph -> UriManager.uri -> + Cic.obj * CicUniv.universe_graph type type_checked_obj = CheckedObj of (Cic.obj * CicUniv.universe_graph) (* cooked obj *) | UncheckedObj of Cic.obj (* uncooked obj *) -(* is_type_checked uri cookingsno *) -(*CSC commento falso ed obsoleto *) -(* returns (true,object) if the object has been type-checked *) -(* otherwise it returns (false,object) and freeze the object for *) -(* type-checking *) -(* set_type_checking_info must be called to unfreeze the object *) +(* + * I think this should be the real semantic: + * + * val is_type_checked: + * ?trust:bool -> UriManager.uri -> bool + * + * but the old semantic is similar to get_cooked_obj, but + * returns an unchecked object intead of a Not_found + *) val is_type_checked : - ?trust:bool -> UriManager.uri -> CicUniv.universe_graph -> type_checked_obj + ?trust:bool -> CicUniv.universe_graph -> UriManager.uri -> + type_checked_obj (* set_type_checking_info uri *) (* must be called once the type-checking of uri is finished *) @@ -94,8 +92,8 @@ val remove_term: UriManager.uri -> unit (* trusted (if [trust] = true and the trusting function accepts it) *) (* Otherwise it raises Not_found *) val get_cooked_obj : - ?trust:bool -> UriManager.uri -> - CicUniv.universe_graph -> Cic.obj * CicUniv.universe_graph + ?trust:bool -> CicUniv.universe_graph -> UriManager.uri -> + Cic.obj * CicUniv.universe_graph (* FUNCTIONS USED ONLY IN THE TOPLEVEL/PROOF-ENGINE *) @@ -118,5 +116,6 @@ val empty : unit -> unit val set_trust: (UriManager.uri -> bool) -> unit (* for filtering in tacticChaser *) -(* NEW *) val in_cache : UriManager.uri -> bool + +(* EOF *) diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml index 49d004ee0..d2cf1a623 100644 --- a/helm/ocaml/cic_proof_checking/cicPp.ml +++ b/helm/ocaml/cic_proof_checking/cicPp.ml @@ -109,7 +109,7 @@ let rec pp t l = UriManager.name_of_uri uri ^ pp_exp_named_subst exp_named_subst l | C.MutInd (uri,n,exp_named_subst) -> (try - match fst(CicEnvironment.get_obj uri CicUniv.empty_ugraph) with + match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with C.InductiveDefinition (dl,_,_) -> let (name,_,_,_) = get_nth dl (n+1) in name ^ pp_exp_named_subst exp_named_subst l @@ -119,7 +119,7 @@ let rec pp t l = ) | C.MutConstruct (uri,n1,n2,exp_named_subst) -> (try - match fst(CicEnvironment.get_obj uri CicUniv.empty_ugraph) with + match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with C.InductiveDefinition (dl,_,_) -> let (_,_,_,cons) = get_nth dl (n1+1) in let (id,_) = get_nth cons n2 in @@ -132,7 +132,7 @@ let rec pp t l = ) | C.MutCase (uri,n1,ty,te,patterns) -> let connames = - (match fst(CicEnvironment.get_obj uri CicUniv.empty_ugraph) with + (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with C.InductiveDefinition (dl,_,_) -> let (_,_,_,cons) = get_nth dl (n1+1) in List.map (fun (id,_) -> id) cons diff --git a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml index e0fd252a6..e456a1731 100644 --- a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml +++ b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml @@ -354,7 +354,7 @@ prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) - else let params = let o,_ = - CicEnvironment.get_cooked_obj uri CicUniv.empty_ugraph + CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri in (match o with C.Constant _ -> raise ReferenceToConstant @@ -386,7 +386,7 @@ prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) - | C.Const (uri,exp_named_subst) -> let params = let o,_ = - CicEnvironment.get_cooked_obj uri CicUniv.empty_ugraph + CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri in (match o with C.Constant (_,_,_,params) -> params @@ -402,7 +402,7 @@ prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) - | C.MutInd (uri,i,exp_named_subst) -> let params = let o,_ = - CicEnvironment.get_cooked_obj uri CicUniv.empty_ugraph + CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri in (match o with C.Constant _ -> raise ReferenceToConstant @@ -418,7 +418,7 @@ prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) - | C.MutConstruct (uri,i,j,exp_named_subst) -> let params = let o,_ = - CicEnvironment.get_cooked_obj uri CicUniv.empty_ugraph + CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri in (match o with C.Constant _ -> raise ReferenceToConstant @@ -543,7 +543,7 @@ if List.mem uri params then prerr_endline "---- OK2" ; reduce (0, [], [], RS.from_ens (List.assq uri ens), s) else ( let o,_ = - CicEnvironment.get_cooked_obj uri CicUniv.empty_ugraph + CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri in match o with C.Constant _ -> raise ReferenceToConstant @@ -601,7 +601,7 @@ if List.mem uri params then prerr_endline "---- OK2" ; *) | (k, e, ens, (C.Const (uri,exp_named_subst) as t), s) -> (let o,_ = - CicEnvironment.get_cooked_obj uri CicUniv.empty_ugraph + CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri in match o with C.Constant (_,Some body,_,_) -> @@ -659,7 +659,7 @@ if List.mem uri params then prerr_endline "---- OK2" ; | C.Appl (C.MutConstruct (_,_,j,_) :: tl) -> let (arity, r) = let o,_ = - CicEnvironment.get_cooked_obj mutind CicUniv.empty_ugraph + CicEnvironment.get_cooked_obj CicUniv.empty_ugraph mutind in match o with C.InductiveDefinition (tl,ingredients,r) -> diff --git a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml index 6a4b07aab..4df3a5bd4 100644 --- a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml +++ b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml @@ -58,7 +58,7 @@ let whd context = ) | C.Var (uri,exp_named_subst) as t -> let o,_ = - CicEnvironment.get_cooked_obj ~trust:false uri CicUniv.empty_ugraph + CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri in (match o with C.Constant _ -> raise ReferenceToConstant @@ -84,7 +84,7 @@ let whd context = | C.Appl [] -> raise (Impossible 1) | C.Const (uri,exp_named_subst) as t -> let o,_ = - CicEnvironment.get_cooked_obj ~trust:false uri CicUniv.empty_ugraph + CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri in (match o with C.Constant (_,Some body,_,_) -> @@ -126,7 +126,7 @@ let whd context = C.MutConstruct (_,_,j,_) -> whdaux l (List.nth pl (j-1)) | C.Appl (C.MutConstruct (_,_,j,_) :: tl) -> let (arity, r) = - let o,_ = CicEnvironment.get_obj mutind CicUniv.empty_ugraph in + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in match o with C.InductiveDefinition (tl,ingredients,r) -> let (_,_,arity,_) = List.nth tl i in diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.ml b/helm/ocaml/cic_proof_checking/cicSubstitution.ml index aff943757..a7124d4a3 100644 --- a/helm/ocaml/cic_proof_checking/cicSubstitution.ml +++ b/helm/ocaml/cic_proof_checking/cicSubstitution.ml @@ -205,7 +205,7 @@ prerr_endline ("@@@POSSIBLE BUG: SUBSTITUTION IS NOT SIMULTANEOUS") ; with Not_found -> let params = - let obj,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in + let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in (match obj with C.Constant _ -> raise ReferenceToConstant | C.Variable (_,_,_,params) -> params @@ -254,7 +254,7 @@ prerr_endline "---- END\n\n " ; | C.Appl _ -> assert false | C.Const (uri,exp_named_subst') -> let params = - let obj,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in + let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in (match obj with C.Constant (_,_,_,params) -> params | C.Variable _ -> raise ReferenceToVariable @@ -268,7 +268,7 @@ prerr_endline "---- END\n\n " ; C.Const (uri,exp_named_subst'') | C.MutInd (uri,typeno,exp_named_subst') -> let params = - let obj,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in + let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in (match obj with C.Constant _ -> raise ReferenceToConstant | C.Variable _ -> raise ReferenceToVariable @@ -282,7 +282,7 @@ prerr_endline "---- END\n\n " ; C.MutInd (uri,typeno,exp_named_subst'') | C.MutConstruct (uri,typeno,consno,exp_named_subst') -> let params = - let obj,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in + let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in (match obj with C.Constant _ -> raise ReferenceToConstant | C.Variable _ -> raise ReferenceToVariable diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index 4035b3217..cab4640c8 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -123,7 +123,7 @@ let rec type_of_constant ~logger uri ugraph = let module R = CicReduction in let module U = UriManager in let cobj,ugraph = - match CicEnvironment.is_type_checked ~trust:true uri ugraph with + match CicEnvironment.is_type_checked ~trust:true ugraph uri with CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph' | CicEnvironment.UncheckedObj uobj -> logger#log (`Start_type_checking uri) ; @@ -180,7 +180,7 @@ let rec type_of_constant ~logger uri ugraph = try CicEnvironment.set_type_checking_info uri; logger#log (`Type_checking_completed uri) ; - match CicEnvironment.is_type_checked ~trust:false uri ugraph with + match CicEnvironment.is_type_checked ~trust:false ugraph uri with CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph' | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError with Invalid_argument s -> @@ -198,7 +198,7 @@ and type_of_variable ~logger uri ugraph = 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 ~trust:true uri ugraph with + match CicEnvironment.is_type_checked ~trust:true ugraph uri with CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_)),ugraph') -> ty,ugraph' | CicEnvironment.UncheckedObj (C.Variable (_,bo,ty,_)) -> logger#log (`Start_type_checking uri) ; @@ -219,7 +219,7 @@ and type_of_variable ~logger uri ugraph = (try CicEnvironment.set_type_checking_info uri ; logger#log (`Type_checking_completed uri) ; - match CicEnvironment.is_type_checked ~trust:false uri ugraph with + match CicEnvironment.is_type_checked ~trust:false ugraph uri with CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_)),ugraph') -> ty,ugraph' | CicEnvironment.CheckedObj _ @@ -404,7 +404,7 @@ and strictly_positive context n nn te = List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true | C.Appl ((C.MutInd (uri,i,exp_named_subst))::tl) -> let (ok,paramsno,ity,cl,name) = - let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with C.InductiveDefinition (tl,_,paramsno) -> let (name,_,ity,cl) = List.nth tl i in @@ -557,7 +557,7 @@ and type_of_mutual_inductive_defs ~logger uri i ugraph = let module R = CicReduction in let module U = UriManager in let cobj,ugraph1 = - match CicEnvironment.is_type_checked ~trust:true uri ugraph with + match CicEnvironment.is_type_checked ~trust:true ugraph uri with CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph' | CicEnvironment.UncheckedObj uobj -> logger#log (`Start_type_checking uri) ; @@ -568,7 +568,7 @@ and type_of_mutual_inductive_defs ~logger uri i ugraph = try CicEnvironment.set_type_checking_info uri ; logger#log (`Type_checking_completed uri) ; - (match CicEnvironment.is_type_checked ~trust:false uri ugraph with + (match CicEnvironment.is_type_checked ~trust:false ugraph uri with CicEnvironment.CheckedObj (cobj,ugraph') -> (cobj,ugraph') | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError ) @@ -590,7 +590,7 @@ and type_of_mutual_inductive_constr ~logger uri i j ugraph = let module R = CicReduction in let module U = UriManager in let cobj,ugraph1 = - match CicEnvironment.is_type_checked ~trust:true uri ugraph with + match CicEnvironment.is_type_checked ~trust:true ugraph uri with CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph' | CicEnvironment.UncheckedObj uobj -> logger#log (`Start_type_checking uri) ; @@ -601,10 +601,11 @@ and type_of_mutual_inductive_constr ~logger uri i j ugraph = try CicEnvironment.set_type_checking_info uri ; logger#log (`Type_checking_completed uri) ; - (match CicEnvironment.is_type_checked - ~trust:false uri ugraph with - CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph' - | CicEnvironment.UncheckedObj _ -> + (match + CicEnvironment.is_type_checked ~trust:false ugraph uri + with + CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph' + | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError) with Invalid_argument s -> @@ -739,7 +740,7 @@ and check_is_really_smaller_arg ?(subst = []) context n nn kl x safes te = (match term with C.Rel m when List.mem m safes || m = x -> let (tys,len,isinductive,paramsno,cl) = - let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with C.InductiveDefinition (tl,_,paramsno) -> let tys = @@ -778,7 +779,7 @@ and check_is_really_smaller_arg ?(subst = []) context n nn kl x safes te = ) (List.combine pl cl) true | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x -> let (tys,len,isinductive,paramsno,cl) = - let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with C.InductiveDefinition (tl,_,paramsno) -> let (_,isinductive,_,cl) = List.nth tl i in @@ -905,7 +906,7 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes = (match term with C.Rel m when List.mem m safes || m = x -> let (tys,len,isinductive,paramsno,cl) = - let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with C.InductiveDefinition (tl,_,paramsno) -> let len = List.length tl in @@ -950,7 +951,7 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes = ) (List.combine pl cl) true | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x -> let (tys,len,isinductive,paramsno,cl) = - let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with C.InductiveDefinition (tl,_,paramsno) -> let (_,isinductive,_,cl) = List.nth tl i in @@ -1063,7 +1064,7 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI = let consty = let obj,_ = try - CicEnvironment.get_cooked_obj ~trust:false uri CicUniv.empty_ugraph + CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri with Not_found -> assert false in match obj with @@ -1250,7 +1251,7 @@ and check_allowed_sort_elimination ~logger context uri i need_dummy ind | (C.Sort C.Prop, C.Sort (C.Type _) ) when need_dummy -> (* TASSI: da verificare *) (*CSC: WRONG. MISSING CONDITIONS ON THE ARGUMENTS OF THE CONSTRUTOR *) - (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in + (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with C.InductiveDefinition (itl,_,_) -> let (_,_,_,cl) = List.nth itl i in @@ -1270,7 +1271,7 @@ and check_allowed_sort_elimination ~logger context uri i need_dummy ind | ((C.Sort C.Set, C.Sort (C.Type _)) | (C.Sort C.CProp, C.Sort (C.Type _))) (* TASSI: da verificare *) when need_dummy -> - (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in + (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with C.InductiveDefinition (itl,_,paramsno) -> let tys = @@ -1298,7 +1299,7 @@ and check_allowed_sort_elimination ~logger context uri i need_dummy ind (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with C.Sort C.Prop -> true,ugraph1 | (C.Sort C.Set | C.Sort C.CProp) -> - (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in + (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with C.InductiveDefinition (itl,_,_) -> let (_,_,_,cl) = List.nth itl i in @@ -1324,7 +1325,7 @@ and check_allowed_sort_elimination ~logger context uri i need_dummy ind | C.Sort C.CProp -> true,ugraph1 | C.Sort (C.Type _) -> (* TASSI: da verificare *) - (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in + (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with C.InductiveDefinition (itl,_,paramsno) -> let (_,_,_,cl) = List.nth itl i in @@ -1722,7 +1723,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = let parsno = let obj,_ = try - CicEnvironment.get_cooked_obj ~trust:false uri CicUniv.empty_ugraph + CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri with Not_found -> assert false in match obj with @@ -1961,7 +1962,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = (*CSC: definire una funzioncina per questo codice sempre replicato *) let obj,_ = try - CicEnvironment.get_cooked_obj ~trust:false uri CicUniv.empty_ugraph + CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri with Not_found -> assert false in (match obj with @@ -1974,7 +1975,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = UriManager.string_of_uri uri)) ) | C.Appl ((C.MutInd (uri,i,_))::_) -> - (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in + (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with C.InductiveDefinition (itl,_,_) -> let (_,is_inductive,_,_) = List.nth itl i in @@ -2034,7 +2035,7 @@ let typecheck uri ugraph = let module U = UriManager in let logger = new CicLogger.logger in (* ??? match CicEnvironment.is_type_checked ~trust:true uri with ???? *) - match CicEnvironment.is_type_checked ~trust:false uri ugraph with + match CicEnvironment.is_type_checked ~trust:false ugraph uri with CicEnvironment.CheckedObj (cobj,ugraph') -> (* prerr_endline ("NON-INIZIO A TYPECHECKARE " ^ U.string_of_uri uri);*) cobj,ugraph' @@ -2099,7 +2100,7 @@ let typecheck uri ugraph = try CicEnvironment.set_type_checking_info uri; logger#log (`Type_checking_completed uri); - match CicEnvironment.is_type_checked ~trust:false uri ugraph with + match CicEnvironment.is_type_checked ~trust:false ugraph uri with CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph' | _ -> raise CicEnvironmentError with diff --git a/helm/ocaml/cic_proof_checking/cicUnivUtils.ml b/helm/ocaml/cic_proof_checking/cicUnivUtils.ml index 1897772a8..c02719454 100644 --- a/helm/ocaml/cic_proof_checking/cicUnivUtils.ml +++ b/helm/ocaml/cic_proof_checking/cicUnivUtils.ml @@ -45,16 +45,14 @@ let universes_of_obj uri t = | C.Var (u,exp_named_subst) -> if List.mem u !don then [] else (don := u::!don; - aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u - CicUniv.empty_ugraph)) + aux_obj (CicEnvironment.get_obj CicUniv.empty_ugraph u)) | C.MutInd (u,_,exp_named_subst) -> if List.mem u !don || eq u uri then [] else begin don := u::!don; - (match fst(CicEnvironment.get_obj ~not_jet_cooked:true u - CicUniv.empty_ugraph) + (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph u) with | C.InductiveDefinition (l,_,_) -> List.fold_left ( @@ -73,8 +71,7 @@ let universes_of_obj uri t = else begin don := u::!don; - (match fst(CicEnvironment.get_obj ~not_jet_cooked:true u - CicUniv.empty_ugraph) with + (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph u) with | C.InductiveDefinition (l,_,_) -> List.fold_left ( fun x (_,_,_t,l') -> @@ -120,36 +117,31 @@ let universes_of_obj uri t = List.fold_left ( fun l u -> l @ if eq u uri then [] else - (aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u - CicUniv.empty_ugraph))) + (aux_obj (CicEnvironment.get_obj CicUniv.empty_ugraph u))) [] v | C.Constant (_,None,ty,v) -> aux ty @ List.fold_left ( fun l u -> l @ if eq u uri then [] else - (aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u - CicUniv.empty_ugraph))) + (aux_obj (CicEnvironment.get_obj CicUniv.empty_ugraph u))) [] v | C.CurrentProof (_,conjs,te,ty,v) -> aux te @ aux ty @ List.fold_left ( fun l u -> l @ if eq u uri then [] else - (aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u - CicUniv.empty_ugraph))) + (aux_obj (CicEnvironment.get_obj CicUniv.empty_ugraph u))) [] v | C.Variable (_,Some bo,ty,v) -> aux bo @ aux ty @ List.fold_left ( fun l u -> l @ if eq u uri then [] else - (aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u - CicUniv.empty_ugraph))) + (aux_obj (CicEnvironment.get_obj CicUniv.empty_ugraph u))) [] v | C.Variable (_,None ,ty,v) -> aux ty @ List.fold_left ( fun l u -> l @ if eq u uri then [] else - (aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u - CicUniv.empty_ugraph))) + (aux_obj (CicEnvironment.get_obj CicUniv.empty_ugraph u))) [] v | C.InductiveDefinition (l,v,_) -> (List.fold_left ( @@ -161,8 +153,7 @@ let universes_of_obj uri t = (List.fold_left (fun l u -> l @ if eq u uri then [] else - (aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u - CicUniv.empty_ugraph))) + (aux_obj (CicEnvironment.get_obj CicUniv.empty_ugraph u))) [] v) ) in diff --git a/helm/ocaml/cic_transformations/acic2Ast.ml b/helm/ocaml/cic_transformations/acic2Ast.ml index d8ded0356..752dd3216 100644 --- a/helm/ocaml/cic_transformations/acic2Ast.ml +++ b/helm/ocaml/cic_transformations/acic2Ast.ml @@ -37,7 +37,7 @@ let sort_of_string = function | _ -> assert false let get_types uri = - let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with | Cic.Constant _ -> assert false | Cic.Variable _ -> assert false diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 82b472fa0..566a531cc 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -57,7 +57,7 @@ let rec type_of_constant uri ugraph = with Not_found -> assert false in *) - let obj,u= CicEnvironment.get_obj uri ugraph in + let obj,u= CicEnvironment.get_obj ugraph uri in match obj with C.Constant (_,_,ty,_) -> ty,u | C.CurrentProof (_,_,_,ty,_) -> ty,u @@ -76,7 +76,7 @@ and type_of_variable uri ugraph = with Not_found -> assert false in *) - let obj,u = CicEnvironment.get_obj uri ugraph in + let obj,u = CicEnvironment.get_obj ugraph uri in match obj with C.Variable (_,_,ty,_) -> ty,u | _ -> @@ -95,7 +95,7 @@ and type_of_mutual_inductive_defs uri i ugraph = with Not_found -> assert false in *) - let obj,u = CicEnvironment.get_obj uri ugraph in + let obj,u = CicEnvironment.get_obj ugraph uri in match obj with C.InductiveDefinition (dl,_,_) -> let (_,_,arity,_) = List.nth dl i in @@ -116,7 +116,7 @@ and type_of_mutual_inductive_constr uri i j ugraph = with Not_found -> assert false in *) - let obj,u = CicEnvironment.get_obj uri ugraph in + let obj,u = CicEnvironment.get_obj ugraph uri in match obj with C.InductiveDefinition (dl,_,_) -> let (_,_,_,cl) = List.nth dl i in @@ -313,7 +313,7 @@ and type_of_aux' metasenv context t ugraph = with Not_found -> assert false in *) - let obj,u = CicEnvironment.get_obj uri ugraph in + let obj,u = CicEnvironment.get_obj ugraph uri in match obj with C.InductiveDefinition (l,expl_params,parsno) -> List.nth l i , expl_params, parsno, u diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml index 66a860a45..781e6f5c8 100644 --- a/helm/ocaml/tactics/discriminationTactics.ml +++ b/helm/ocaml/tactics/discriminationTactics.ml @@ -120,8 +120,8 @@ and injection1_tac ~term ~i = prerr_endline ("XXXX t2' " ^ CicPp.ppterm t2') ; prerr_endline ("XXXX consno " ^ string_of_int consno) ; let pattern = - match fst(CicEnvironment.get_obj turi - CicUniv.empty_ugraph ) with + match fst(CicEnvironment.get_obj + CicUniv.empty_ugraph turi ) with C.InductiveDefinition (ind_type_list,_,nr_ind_params_dx) -> let _,_,_,constructor_list = (List.nth ind_type_list typeno) in let i_constr_id,_ = List.nth constructor_list (consno - 1) in @@ -275,8 +275,8 @@ prerr_endline ("XXXX consno2 " ^ (string_of_int consno2)) ; let pattern = (* a list of "True" except for the element in position consno2 which is "False" *) - match fst(CicEnvironment.get_obj turi - CicUniv.empty_ugraph) with + match fst(CicEnvironment.get_obj + CicUniv.empty_ugraph turi) with C.InductiveDefinition (ind_type_list,_,nr_ind_params) -> prerr_endline ("XXXX nth " ^ (string_of_int (List.length ind_type_list)) ^ " " ^ (string_of_int typeno)) ; let _,_,_,constructor_list = (List.nth ind_type_list typeno) in diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml index 0cb8acead..92b89a679 100644 --- a/helm/ocaml/tactics/primitiveTactics.ml +++ b/helm/ocaml/tactics/primitiveTactics.ml @@ -204,7 +204,7 @@ let = let module C = Cic in let params = - let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with C.Constant (_,_,_,params) | C.CurrentProof (_,_,_,_,params) @@ -220,7 +220,7 @@ let [],[] -> [] | uri::tl,[] -> let ty = - let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with C.Variable (_,_,ty,_) -> CicSubstitution.subst_vars !exp_named_subst_diff ty @@ -492,7 +492,7 @@ let elim_tac ~term = let eliminator_uri = let buri = U.buri_of_uri uri in let name = - let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with C.InductiveDefinition (tys,_,_) -> let (name,_,_,_) = List.nth tys typeno in diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml index e7975793f..e53d69048 100644 --- a/helm/ocaml/tactics/proofEngineReduction.ml +++ b/helm/ocaml/tactics/proofEngineReduction.ml @@ -389,7 +389,7 @@ let reduce context = let exp_named_subst' = reduceaux_exp_named_subst context l exp_named_subst in - (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in + (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with C.Constant _ -> raise ReferenceToConstant | C.CurrentProof _ -> raise ReferenceToCurrentProof @@ -430,7 +430,7 @@ let reduce context = let exp_named_subst' = reduceaux_exp_named_subst context l exp_named_subst in - (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in + (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with C.Constant (_,Some body,_,_) -> (reduceaux context l @@ -492,7 +492,7 @@ let reduce context = C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1)) | C.Appl (C.MutConstruct (_,_,j,_) :: tl) -> let (arity, r) = - let o,_ = CicEnvironment.get_obj mutind CicUniv.empty_ugraph in + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in match o with C.InductiveDefinition (tl,_,r) -> let (_,_,arity,_) = List.nth tl i in @@ -615,7 +615,7 @@ let simpl context = let exp_named_subst' = reduceaux_exp_named_subst context l exp_named_subst in - (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in + (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with C.Constant _ -> raise ReferenceToConstant | C.CurrentProof _ -> raise ReferenceToCurrentProof @@ -656,7 +656,7 @@ let simpl context = let exp_named_subst' = reduceaux_exp_named_subst context l exp_named_subst in - (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in + (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with C.Constant (_,Some body,_,_) -> try_delta_expansion l @@ -715,7 +715,7 @@ let simpl context = C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1)) | C.Appl (C.MutConstruct (_,_,j,_) :: tl) -> let (arity, r) = - let o,_ = CicEnvironment.get_obj mutind CicUniv.empty_ugraph in + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in match o with C.InductiveDefinition (tl,ingredients,r) -> let (_,_,arity,_) = List.nth tl i in -- 2.39.2