Tracking memory misallocation by trying to improve sharing.

4 files changed, 36 insertions, 21 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 105eb7da1b..93677e5a9f 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -97,9 +97,16 @@ let named_vals_of_val = snd
    each declarations.
    *** /!\ ***   [f t] should be convertible with t *)
 let map_named_val f (ctxt,ctxtv) =
-  let ctxt =
-    List.map (fun (id,body,typ) -> (id, Option.map f body, f typ)) ctxt in
-  (ctxt,ctxtv)
+  let rec map ctx = match ctx with
+  | [] -> []
+  | (id, body, typ) :: rem ->
+    let body' = Option.smartmap f body in
+    let typ' = f typ in
+    let rem' = map rem in
+    if body' == body && typ' == typ && rem' == rem then ctx
+    else (id, body', typ') :: rem'
+  in
+  (map ctxt, ctxtv)
 
 let empty_named_context = empty_named_context
 
@@ -373,18 +380,22 @@ let insert_after_hyp (ctxt,vals) id d check =
 
 (* To be used in Logic.clear_hyps *)
 let remove_hyps ids check_context check_value (ctxt, vals) =
-  List.fold_right2 (fun (id,_,_ as d) (id',v) (ctxt,vals) ->
-      if Id.Set.mem id ids then
-	(ctxt,vals)
-      else
-	let nd = check_context d in
-	let nv = check_value v in
-	  (nd::ctxt,(id',nv)::vals))
-		     ctxt vals ([],[])
-
-
-
-
+  let rec remove_hyps ctxt vals = match ctxt, vals with
+  | [], [] -> [], []
+  | d :: rctxt, (nid, v) :: rvals ->
+    let (id, _, _) = d in
+    let ans = remove_hyps rctxt rvals in
+    if Id.Set.mem id ids then ans
+    else
+      let (rctxt', rvals') = ans in
+      let d' = check_context d in
+      let v' = check_value v in
+      if d == d' && v == v' && rctxt == rctxt' && rvals == rvals' then
+        ctxt, vals
+      else (d' :: rctxt', (nid, v') :: rvals')
+  | _ -> assert false
+  in
+  remove_hyps ctxt vals
 
 (*spiwack: the following functions assemble the pieces of the retroknowledge
    note that the "consistent" register function is available in the module
diff --git a/lib/pp.ml b/lib/pp.ml
index 4477d16567..bbd5c35207 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -371,7 +371,7 @@ let std_logger level msg = match level with
 | Debug _ -> msgnl (debugbody msg) (* cyan *)
 | Info -> msgnl (print_color "37" (hov 0 msg)) (* gray *)
 | Notice -> msgnl msg
-| Warning -> Flags.if_warn (msgnl_with !err_ft) (warnbody msg) (* bright yellow *)
+| Warning -> Flags.if_warn (fun () -> msgnl_with !err_ft (warnbody msg)) () (* bright yellow *)
 | Error -> msgnl_with !err_ft (errorbody msg) (* bright red *)
 
 let logger = ref std_logger
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 93d9552c0d..264172d0c9 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -487,10 +487,11 @@ let clear_hyps_in_evi evdref hyps concl ids =
   let nconcl =
     check_and_clear_in_constr evdref (OccurHypInSimpleClause None) ids concl in
   let nhyps =
-    let check_context (id,ob,c) =
+    let check_context ((id,ob,c) as decl) =
       let err = OccurHypInSimpleClause (Some id) in
-      (id, Option.map (check_and_clear_in_constr evdref err ids) ob,
-	check_and_clear_in_constr evdref err ids c)
+      let ob' = Option.smartmap (fun c -> check_and_clear_in_constr evdref err ids c) ob in
+      let c' = check_and_clear_in_constr evdref err ids c in
+      if ob == ob' && c == c' then decl else (id, ob', c')
     in
     let check_value vk =
       match !vk with
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 60548ef7da..4eb2785eeb 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -381,7 +381,8 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 	in
 	let ((acc'',conclty',sigma), args) = mk_arggoals sigma goal acc' hdty l in
 	check_conv_leq_goal env sigma trm conclty' conclty;
-        (acc'',conclty',sigma, Term.mkApp (applicand, args))
+        let ans = if applicand == f && args == l then trm else Term.mkApp (applicand, args) in
+        (acc'',conclty',sigma, ans)
 
     | Case (ci,p,c,lf) ->
 	let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals sigma goal goalacc p c in
@@ -429,7 +430,8 @@ and mk_hdgoals sigma goal goalacc trm =
 	  else mk_hdgoals sigma goal goalacc f
 	in
 	let ((acc'',conclty',sigma), args) = mk_arggoals sigma goal acc' hdty l in
-	(acc'',conclty',sigma, Term.mkApp (applicand, args))
+        let ans = if applicand == f && args == l then trm else Term.mkApp (applicand, args) in
+	(acc'',conclty',sigma, ans)
 
     | Case (ci,p,c,lf) ->
 	let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals sigma goal goalacc p c in
@@ -464,6 +466,7 @@ and mk_arggoals sigma goal goalacc funty allargs =
         fill sigma goalacc (subst1 c1 b) i
       | _ -> raise (RefinerError (CannotApply (t,harg)))
   in
+  let ans = if Array.equal (==) ans allargs then allargs else ans in
   (fill sigma goalacc funty 0, ans)
 
 and mk_casegoals sigma goal goalacc p c =