From 45a9e84c12f57e5473eccc6f611cdbb343998d5d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 26 Sep 2008 08:03:47 +0000 Subject: [PATCH] lazy proof term to increase sharing and decrease memory consumption. I hope nobody was comparing grafite-statuses with ocaml polymorphic = --- .../components/grafite_engine/grafiteEngine.ml | 6 +++--- helm/software/components/tactics/auto.ml | 12 ++++++------ helm/software/components/tactics/auto.mli | 4 ++-- helm/software/components/tactics/equalityTactics.ml | 4 ++-- .../components/tactics/inversion_principle.ml | 5 +++-- helm/software/components/tactics/primitiveTactics.ml | 2 +- .../components/tactics/proofEngineHelpers.ml | 4 ++-- helm/software/components/tactics/proofEngineTypes.ml | 6 ++++-- .../software/components/tactics/proofEngineTypes.mli | 2 +- .../components/tactics/statefulProofEngine.mli | 6 +++--- helm/software/matita/matita.ml | 10 ++++++---- helm/software/matita/matitaAutoGui.ml | 12 ++++++------ helm/software/matita/matitaAutoGui.mli | 4 ++-- helm/software/matita/matitaMathView.ml | 4 ++-- helm/software/matita/matitaScript.ml | 2 +- 15 files changed, 44 insertions(+), 39 deletions(-) diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 10cf1b8cb..888ad55ff 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -689,7 +689,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status status,[] | GrafiteAst.Print (_,"proofterm") -> let _,_,_,p,_, _ = GrafiteTypes.get_current_proof status in - prerr_endline (Auto.pp_proofterm p); + prerr_endline (Auto.pp_proofterm (Lazy.force p)); status,[] | GrafiteAst.Print (_,_) -> status,[] | GrafiteAst.Qed loc -> @@ -710,7 +710,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status (GrafiteTypes.Command_error "Proof not completed! metasenv is not empty!"); let name = UriManager.name_of_uri uri in - let obj = Cic.Constant (name,Some bo,ty,[],attrs) in + let obj = Cic.Constant (name,Some (Lazy.force bo),ty,[],attrs) in let status, lemmas = add_obj uri obj status in {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof}, @@ -768,7 +768,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status "\nPlease use a variant.")); end; let _subst = [] in - let initial_proof = (Some uri, metasenv', _subst, bo, ty, attrs) in + let initial_proof = (Some uri, metasenv', _subst, lazy bo, ty, attrs) in let initial_stack = Continuationals.Stack.of_metasenv metasenv' in { status with GrafiteTypes.proof_status = GrafiteTypes.Incomplete_proof diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml index c3e2b6b48..3c8c89468 100644 --- a/helm/software/components/tactics/auto.ml +++ b/helm/software/components/tactics/auto.ml @@ -807,7 +807,7 @@ type menv = Cic.metasenv type subst = Cic.substitution type goal = ProofEngineTypes.goal * int * AutoTypes.sort let candidate_no = ref 0;; -type candidate = int * Cic.term +type candidate = int * Cic.term Lazy.t type cache = AutoCache.cache type tables = Saturation.active_table * Saturation.passive_table * Equality.equality_bag @@ -837,8 +837,8 @@ type auto_result = (* the status exported to the external observer *) type auto_status = (* context, (goal,candidate) list, and_list, history *) - Cic.context * (int * Cic.term * bool * int * (int * Cic.term) list) list * - (int * Cic.term * int) list * Cic.term list + Cic.context * (int * Cic.term * bool * int * (int * Cic.term Lazy.t) list) list * + (int * Cic.term * int) list * Cic.term Lazy.t list let d_prefix l = let rec aux acc = function @@ -890,7 +890,7 @@ let pp_status ctx status = | None -> Printf.sprintf "D(%d, _, %d)" gi d in let string_of_s m su k (ci,ct) gi = - Printf.sprintf "S(%d, %s, %s, %d)" gi (pp k) (pp ct) ci + Printf.sprintf "S(%d, %s, %s, %d)" gi (pp k) (pp (Lazy.force ct)) ci in let string_of_ol m su l = String.concat " | " @@ -1129,7 +1129,7 @@ let put_in_subst subst metasenv (goalno,_,_) canonical_ctx t ty = subst, metasenv ;; let mk_fake_proof metasenv subst (goalno,_,_) goalty context = - None,metasenv,subst ,Cic.Meta(goalno,mk_irl context),goalty, [] + None,metasenv,subst ,(lazy (Cic.Meta(goalno,mk_irl context))),goalty, [] ;; let equational_case tables maxm cache depth fake_proof goalno goalty subst context @@ -1208,7 +1208,7 @@ let try_candidate let open_goals = order_new_goals metasenv subst open_goals ppterm in let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in incr candidate_no; - Some ((!candidate_no,cand),metasenv,subst,open_goals), tables , maxmeta + Some ((!candidate_no,lazy cand),metasenv,subst,open_goals), tables , maxmeta with | ProofEngineTypes.Fail s -> None,tables, maxm | CicUnification.Uncertain s -> None,tables, maxm diff --git a/helm/software/components/tactics/auto.mli b/helm/software/components/tactics/auto.mli index a300a3132..31a801b1d 100644 --- a/helm/software/components/tactics/auto.mli +++ b/helm/software/components/tactics/auto.mli @@ -52,11 +52,11 @@ val solve_rewrite_tac: type auto_status = Cic.context * (* or list: goalno, goaltype, grey, depth, candidates: (goalno, c) *) - (int * Cic.term * bool * int * (int * Cic.term) list) list * + (int * Cic.term * bool * int * (int * Cic.term Lazy.t) list) list * (* and list *) (int * Cic.term * int) list * (* last moves *) - Cic.term list + Cic.term Lazy.t list val get_auto_status : unit -> auto_status val pause: bool -> unit diff --git a/helm/software/components/tactics/equalityTactics.ml b/helm/software/components/tactics/equalityTactics.ml index 16aa6d3b2..6eae44531 100644 --- a/helm/software/components/tactics/equalityTactics.ml +++ b/helm/software/components/tactics/equalityTactics.ml @@ -160,7 +160,7 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality = let t1 = CicMetaSubst.apply_subst subst t1 in let t2 = CicMetaSubst.apply_subst subst t2 in let ty = CicMetaSubst.apply_subst subst ty in - let pbo = CicMetaSubst.apply_subst subst pbo in + let pbo = lazy (CicMetaSubst.apply_subst subst (Lazy.force pbo)) in let pty = CicMetaSubst.apply_subst subst pty in let equality = CicMetaSubst.apply_subst subst equality in let abstr_gty = @@ -238,7 +238,7 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what = let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in let with_what, metasenv, u = with_what context metasenv u in let with_what = CicMetaSubst.apply_subst subst with_what in - let pbo = CicMetaSubst.apply_subst subst pbo in + let pbo = lazy (CicMetaSubst.apply_subst subst (Lazy.force pbo)) in let pty = CicMetaSubst.apply_subst subst pty in let status = (uri,metasenv,_subst,pbo,pty, attrs),goal in let ty_of_with_what,u = diff --git a/helm/software/components/tactics/inversion_principle.ml b/helm/software/components/tactics/inversion_principle.ml index 2b6e14b37..0f50116cb 100644 --- a/helm/software/components/tactics/inversion_principle.ml +++ b/helm/software/components/tactics/inversion_principle.ml @@ -156,7 +156,8 @@ let build_inversion uri obj = let attrs = [`Class (`InversionPrinciple); `Generated] in let _subst = [] in let proof= - (Some inversor_uri,metasenv',_subst,Cic.Meta(goal,[]),ref_theorem, attrs) in + (Some inversor_uri,metasenv',_subst, + lazy (Cic.Meta(goal,[])),ref_theorem, attrs) in let _,applies = List.fold_right (fun _ (i,applies) -> @@ -193,7 +194,7 @@ let build_inversion uri obj = Some (inversor_uri, Cic.Constant - (UriManager.name_of_uri inversor_uri,Some bo,ty,[],[])) + (UriManager.name_of_uri inversor_uri,Some (Lazy.force bo),ty,[],[])) with Inversion.EqualityNotDefinedYet -> None | CicRefine.RefineFailure ls -> diff --git a/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml index 0fa4ebaec..d6a6c91b9 100644 --- a/helm/software/components/tactics/primitiveTactics.ml +++ b/helm/software/components/tactics/primitiveTactics.ml @@ -637,7 +637,7 @@ let generalize_tac ~conjecture ~pattern in let context = CicMetaSubst.apply_subst_context subst context in let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in - let pbo = CicMetaSubst.apply_subst subst pbo in + let pbo = lazy (CicMetaSubst.apply_subst subst (Lazy.force pbo)) in let pty = CicMetaSubst.apply_subst subst pty in let term = match term with diff --git a/helm/software/components/tactics/proofEngineHelpers.ml b/helm/software/components/tactics/proofEngineHelpers.ml index e45c13257..fc508f0c1 100644 --- a/helm/software/components/tactics/proofEngineHelpers.ml +++ b/helm/software/components/tactics/proofEngineHelpers.ml @@ -56,7 +56,7 @@ let subst_meta_in_proof proof meta term newmetasenv = i,canonical_context',(subst_in ty) ) metasenv' in - let bo' = subst_in bo in + let bo' = lazy (subst_in (Lazy.force bo)) in (* Metavariables can appear also in the *statement* of the theorem * since the parser does not reject as statements terms with * metavariable therein *) @@ -79,7 +79,7 @@ let subst_meta_in_proof proof meta term newmetasenv = let subst_meta_and_metasenv_in_proof proof meta subst newmetasenv = let (uri,_,initial_subst,bo,ty, attrs) = proof in let subst_in = CicMetaSubst.apply_subst subst in - let bo' = subst_in bo in + let bo' = lazy (subst_in (Lazy.force bo)) in (* Metavariables can appear also in the *statement* of the theorem * since the parser does not reject as statements terms with * metavariable therein *) diff --git a/helm/software/components/tactics/proofEngineTypes.ml b/helm/software/components/tactics/proofEngineTypes.ml index 93436e799..c60b6fdc0 100644 --- a/helm/software/components/tactics/proofEngineTypes.ml +++ b/helm/software/components/tactics/proofEngineTypes.ml @@ -28,7 +28,8 @@ (** current proof (proof uri * metas * (in)complete proof * term to be prooved) *) -type proof = UriManager.uri option * Cic.metasenv * Cic.substitution * Cic.term * Cic.term * Cic.attribute list +type proof = + UriManager.uri option * Cic.metasenv * Cic.substitution * Cic.term Lazy.t * Cic.term * Cic.attribute list (** current goal, integer index *) type goal = int type status = proof * goal @@ -45,7 +46,8 @@ let initial_status ty metasenv attrs = let newmeta_idx = aux 0 metasenv in let _subst = [] in let proof = - None, (newmeta_idx, [], ty) :: metasenv, _subst, Cic.Meta (newmeta_idx, []), ty, attrs + None, (newmeta_idx, [], ty) :: metasenv, _subst, + lazy (Cic.Meta (newmeta_idx, [])), ty, attrs in (proof, newmeta_idx) diff --git a/helm/software/components/tactics/proofEngineTypes.mli b/helm/software/components/tactics/proofEngineTypes.mli index 7c7b8330e..7e6f571e4 100644 --- a/helm/software/components/tactics/proofEngineTypes.mli +++ b/helm/software/components/tactics/proofEngineTypes.mli @@ -27,7 +27,7 @@ current proof (proof uri * metas * (in)complete proof * term to be prooved) *) type proof = - UriManager.uri option * Cic.metasenv * Cic.substitution * Cic.term * Cic.term * Cic.attribute list + UriManager.uri option * Cic.metasenv * Cic.substitution * Cic.term Lazy.t * Cic.term * Cic.attribute list (** current goal, integer index *) type goal = int type status = proof * goal diff --git a/helm/software/components/tactics/statefulProofEngine.mli b/helm/software/components/tactics/statefulProofEngine.mli index 64a394d74..06defd79f 100644 --- a/helm/software/components/tactics/statefulProofEngine.mli +++ b/helm/software/components/tactics/statefulProofEngine.mli @@ -62,7 +62,7 @@ exception Data_failure of exn class ['a] status: ?history_size:int -> (** default 20 *) ?uri:UriManager.uri -> - typ:Cic.term -> body:Cic.term -> metasenv:Cic.metasenv -> + typ:Cic.term -> body:Cic.term Lazy.t -> metasenv:Cic.metasenv -> attrs:Cic.attribute list -> (proof_status -> 'a) -> (* init data *) (proof_status * 'a -> proof_status -> 'a) -> (* update data *) @@ -71,7 +71,7 @@ class ['a] status: method proof: ProofEngineTypes.proof method metasenv: Cic.metasenv - method body: Cic.term + method body: Cic.term Lazy.t method typ: Cic.term method attrs: Cic.attribute list @@ -116,7 +116,7 @@ class ['a] status: val trivial_status: ?uri:UriManager.uri -> - typ:Cic.term -> body:Cic.term -> metasenv:Cic.metasenv -> + typ:Cic.term -> body:Cic.term Lazy.t -> metasenv:Cic.metasenv -> attrs:Cic.attribute list -> unit -> unit status diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml index 64d1a4513..d63e327f0 100644 --- a/helm/software/matita/matita.ml +++ b/helm/software/matita/matita.ml @@ -171,8 +171,10 @@ let _ = (MatitaScript.current ())#grafite_status.GrafiteTypes.proof_status with | GrafiteTypes.No_proof -> (Cic.Implicit None) - | Incomplete_proof i -> let _,_,_subst,p,_, _ = i.GrafiteTypes.proof in p - | Proof p -> let _,_,_subst,p,_, _ = p in p + | Incomplete_proof i -> + let _,_,_subst,p,_, _ = i.GrafiteTypes.proof in + Lazy.force p + | Proof p -> let _,_,_subst,p,_, _ = p in Lazy.force p | Intermediate _ -> assert false))); addDebugItem "Print current proof (natural language) to stderr" (fun _ -> @@ -186,9 +188,9 @@ let _ = | GrafiteTypes.No_proof -> assert false | Incomplete_proof i -> let _,m,_subst,p,ty, attrs = i.GrafiteTypes.proof in - Cic.CurrentProof ("current (incomplete) proof",m,p,ty,[],attrs) + Cic.CurrentProof ("current (incomplete) proof",m,Lazy.force p,ty,[],attrs) | Proof (_,m,_subst,p,ty, attrs) -> - Cic.CurrentProof ("current proof",m,p,ty,[],attrs) + Cic.CurrentProof ("current proof",m,Lazy.force p,ty,[],attrs) | Intermediate _ -> assert false))); (* addDebugItem "ask record choice" (fun _ -> diff --git a/helm/software/matita/matitaAutoGui.ml b/helm/software/matita/matitaAutoGui.ml index d01cac5d1..588dc5fec 100644 --- a/helm/software/matita/matitaAutoGui.ml +++ b/helm/software/matita/matitaAutoGui.ml @@ -25,9 +25,9 @@ *) type status = - Cic.context * (int * Cic.term * bool * int * (int * Cic.term) list) list * + Cic.context * (int * Cic.term * bool * int * (int * Cic.term Lazy.t) list) list * (int * Cic.term * int) list * - Cic.term list + Cic.term Lazy.t list let fake_goal = Cic.Implicit None;; let fake_candidates = [];; @@ -57,16 +57,16 @@ let pp ?(size=(!font_size)) c t = let pp_goal context x = if x == fake_goal then "" else pp context x ;; -let pp_candidate context x = pp context x -let pp_candidate_tip context x = pp ~size:0 context x +let pp_candidate context x = pp context (Lazy.force x) +let pp_candidate_tip context x = pp ~size:0 context (Lazy.force x) let pp_candidate_type context x = try let ty, _ = CicTypeChecker.type_of_aux' [] ~subst:[] - context x CicUniv.oblivion_ugraph + context (Lazy.force x) CicUniv.oblivion_ugraph in pp ~size:0 context ty - with CicUtil.Meta_not_found _ -> pp ~size:0 context x + with CicUtil.Meta_not_found _ -> pp ~size:0 context (Lazy.force x) ;; let sublist start len l = diff --git a/helm/software/matita/matitaAutoGui.mli b/helm/software/matita/matitaAutoGui.mli index 896886a02..eabf24aab 100644 --- a/helm/software/matita/matitaAutoGui.mli +++ b/helm/software/matita/matitaAutoGui.mli @@ -27,7 +27,7 @@ type status = Cic.context * - (int * Cic.term * bool * int * (int * Cic.term) list) list * - (int * Cic.term * int) list * Cic.term list + (int * Cic.term * bool * int * (int * Cic.term Lazy.t) list) list * + (int * Cic.term * int) list * Cic.term Lazy.t list val auto_dialog : (unit -> status) -> unit val set_font_size: int -> unit diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml index e6c261791..63cf77a16 100644 --- a/helm/software/matita/matitaMathView.ml +++ b/helm/software/matita/matitaMathView.ml @@ -1154,11 +1154,11 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) match self#script#grafite_status.proof_status with | Proof (uri, metasenv, _subst, bo, ty, attrs) -> let name = UriManager.name_of_uri (HExtlib.unopt uri) in - let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], attrs) in + let obj = Cic.CurrentProof (name, metasenv, Lazy.force bo, ty, [], attrs) in self#_loadObj obj | Incomplete_proof { proof = (uri, metasenv, _subst, bo, ty, attrs) } -> let name = UriManager.name_of_uri (HExtlib.unopt uri) in - let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], attrs) in + let obj = Cic.CurrentProof (name, metasenv, Lazy.force bo, ty, [], attrs) in self#_loadObj obj | _ -> self#blank () diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index f769484c8..a92b5b789 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/matita/matitaScript.ml @@ -440,7 +440,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status [], "", parsed_text_length | TA.WHint (loc, term) -> let _subst = [] in - let s = ((None,[0,[],term], _subst, Cic.Meta (0,[]) ,term, []),0) in + let s = ((None,[0,[],term], _subst, lazy (Cic.Meta (0,[])) ,term, []),0) in let l = List.map fst (MQ.experimental_hint ~dbd s) in let entry = `Whelp (pp_macro mac, l) in guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; -- 2.39.2