lazy proof term to increase sharing and decrease memory consumption.

I hope nobody was comparing grafite-statuses with ocaml polymorphic =

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 10cf1b8cbc41e3171f83a6e01300f6822ff2c91f..888ad55ff0b773df640cca516314f6e69749c797 100644 (file)
--- 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 c3e2b6b4894929dc84648e5549a3c7be412bf6f2..3c8c89468e0f46d9334eb95e4819ca32ff2c2ebe 100644 (file)
--- 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 a300a3132d421e0946610bc1d7debcdbbf77c36b..31a801b1da1f4ab37fb7166639a3213a803fd472 100644 (file)
--- 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 16aa6d3b2d5925a10b1ab3bf7e47583885365c2f..6eae445313304922677231b3aa0f518f108fb9d4 100644 (file)
--- 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 2b6e14b37e28e5ccc3a515ce0f5a1d86c727b685..0f50116cb5ed7be0ce46d09178e8317a8dc1f8fe 100644 (file)
--- 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 0fa4ebaec60a335ee0be727e741e42fac035cf83..d6a6c91b9d8e60ad78d5b95fea237865869a37af 100644 (file)
--- 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 e45c13257d54003e2dbee36171e84463417127e1..fc508f0c11a33b85df8795ab5c63e487b3214dcb 100644 (file)
--- 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 93436e799586b899ecd4ffe6a7ebb098e8e3f5b0..c60b6fdc0080ae6fbbecfa238a2c215267d31c83 100644 (file)
--- 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 7c7b8330ee13d7cf075c6247dd4a293dc9520d16..7e6f571e42387c63902fba2db884c8ebc31ceeaa 100644 (file)
--- 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 64a394d744bc23dbad51af14c1f8111171eb4ef4..06defd79fcead87272be0850c48ad067679c5de1 100644 (file)
--- 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 64d1a4513ebed04a6c7fa8427aa8094a9f4b3da3..d63e327f03b89e8d68a58b7ce2a80e68e945ff78 100644 (file)
--- 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 d01cac5d14a698166a25637fcd379f0aadc4c9f7..588dc5fecd09363f7de821a80eecb261ed083624 100644 (file)
--- 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 896886a02ee6231f1cac61026536a5b72c008969..eabf24aab70ef2ecec3b6f2c96f5114fe35bca42 100644 (file)
--- 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 e6c26179132205f9028779dc0a8d7868b9271f43..63cf77a16e356352294078aa27e5651e7213e54c 100644 (file)
--- 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 f769484c87706e9d615a7f9aa508b5ba1d9430db..a92b5b789707020df7c05b9de48ed906693cfe66 100644 (file)
--- 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;