7 files changed, 285 insertions, 9 deletions

diff --git a/proofs/logic_monad.ml b/proofs/logic_monad.ml
index ac9fea772..30af03cd9 100644
--- a/proofs/logic_monad.ml
+++ b/proofs/logic_monad.ml
@@ -154,6 +154,12 @@ module type Param = sig
   (** Read-write *)
   type s
 
+  (** Update-only. Essentially a writer on [u->u]. *)
+  type u
+
+  (** [u] must be pointed. *)
+  val uunit : u
+
 end
 
 
@@ -164,6 +170,7 @@ struct
       state-passing-style monad.*)
   type state = {
     rstate : P.e;
+    ustate : P.u;
     wstate : P.w;
     sstate : P.s;
   }
@@ -256,6 +263,9 @@ struct
   let put (w : P.w) : unit t = (); fun s ->
     { iolist = fun nil cons -> cons ((), { s with wstate = P.wprod s.wstate w }) nil }
 
+  let update (f : P.u -> P.u) : unit t = (); fun s ->
+    { iolist = fun nil cons -> cons ((), { s with ustate = f s.ustate }) nil }
+
   (** List observation *)
 
   let once (m : 'a t) : 'a t = (); fun s ->
@@ -295,10 +305,10 @@ struct
       end }
 
   let run m r s =
-    let s = { wstate = P.wunit; rstate = r; sstate = s } in
+    let s = { wstate = P.wunit; ustate = P.uunit; rstate = r; sstate = s } in
     let m = m s in
     let nil e = NonLogical.raise (TacticFailure e) in
-    let cons (x, s) _ = NonLogical.return (x, s.sstate, s.wstate) in
+    let cons (x, s) _ = NonLogical.return (x, s.sstate, s.wstate, s.ustate) in
     m.iolist nil cons
 
  end
diff --git a/proofs/logic_monad.mli b/proofs/logic_monad.mli
index 3d6866514..8006873ad 100644
--- a/proofs/logic_monad.mli
+++ b/proofs/logic_monad.mli
@@ -118,6 +118,12 @@ module type Param = sig
   (** Read-write *)
   type s
 
+  (** Update-only. Essentially a writer on [u->u]. *)
+  type u
+
+  (** [u] must be pointed. *)
+  val uunit : u
+
 end
 
 module Logical (P:Param) : sig
@@ -131,6 +137,7 @@ module Logical (P:Param) : sig
   val modify : (P.s -> P.s) -> unit t
   val put : P.w -> unit t
   val current : P.e t
+  val update : (P.u -> P.u) -> unit t
 
   val zero : exn -> 'a t
   val plus : 'a t -> (exn -> 'a t) -> 'a t
@@ -140,5 +147,5 @@ module Logical (P:Param) : sig
 
   val lift : 'a NonLogical.t -> 'a t
 
-  val run : 'a t -> P.e -> P.s -> ('a * P.s * P.w) NonLogical.t
+  val run : 'a t -> P.e -> P.s -> ('a * P.s * P.w * P.u) NonLogical.t
 end
diff --git a/proofs/proof.ml b/proofs/proof.ml
index d00618be0..1dc89ca2c 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -318,7 +318,7 @@ let initial_goals p = Proofview.initial_goals p.entry
 
 let run_tactic env tac pr =
   let sp = pr.proofview in
-  let (_,tacticced_proofview,(status,to_shelve,give_up)) = Proofview.apply env tac sp in
+  let (_,tacticced_proofview,(status,to_shelve,give_up),_) = Proofview.apply env tac sp in
   let shelf =
     let sigma = Proofview.return tacticced_proofview in
     let pre_shelf = pr.shelf@(List.rev (Evd.future_goals sigma))@to_shelve in
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index d69ee0260..bf4a1e5a6 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -209,10 +209,10 @@ type +'a tactic = 'a Proof.t
 
 (** Applies a tactic to the current proofview. *)
 let apply env t sp =
-  let (next_r,(next_state,_),status) =
+  let (next_r,(next_state,_),status,info) =
     Logic_monad.NonLogical.run (Proof.run t () (sp,env))
   in
-  next_r,next_state,status
+  next_r,next_state,status,Trace.to_tree info
 
 
 
@@ -712,9 +712,10 @@ let tclTIMEOUT n t =
         | e -> Logic_monad.NonLogical.raise e
       end
   end >>= function
-    | Util.Inl (res,s,m) ->
+    | Util.Inl (res,s,m,i) ->
         Proof.set s >>
         Proof.put m >>
+        Proof.update (fun _ -> i) >>
         return res
     | Util.Inr e -> tclZERO e
 
@@ -959,6 +960,19 @@ end
 
 
 
+(** {6 Trace} *)
+
+module Trace = struct
+
+  let log m = InfoL.leaf (Info.Msg m)
+  let name_tactic m t = InfoL.tag (Info.Tactic m) t
+
+  let pr_info = Info.print
+
+end
+
+
+
 (** {6 Non-logical state} *)
 
 module NonLogical = Logic_monad.NonLogical
@@ -1054,7 +1068,7 @@ module V82 = struct
   let of_tactic t gls =
     try
       let init = { solution = gls.Evd.sigma ; comb = [gls.Evd.it] } in
-      let (_,final,_) = apply (GoalV82.env gls.Evd.sigma gls.Evd.it) t init in
+      let (_,final,_,_) = apply (GoalV82.env gls.Evd.sigma gls.Evd.it) t init in
       { Evd.sigma = final.solution ; it = final.comb }
     with Logic_monad.TacticFailure e as src ->
       let src = Errors.push src in
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 293d99fdc..934a44574 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -145,6 +145,7 @@ type +'a tactic
 val apply : Environ.env -> 'a tactic -> proofview -> 'a
                                                    * proofview
                                                    * (bool*Goal.goal list*Goal.goal list)
+                                                   * Proofview_monad.Info.tree
 
 (** {7 Monadic primitives} *)
 
@@ -474,6 +475,18 @@ module Refine : sig
 end
 
 
+(** {6 Trace} *)
+
+module Trace : sig
+
+  val log : Proofview_monad.lazy_msg -> unit tactic
+  val name_tactic : Proofview_monad.lazy_msg -> 'a tactic -> 'a tactic
+
+  val pr_info : Proofview_monad.Info.tree -> Pp.std_ppcmds
+
+end
+
+
 (** {6 Non-logical state} *)
 
 (** The [NonLogical] module allows the execution of effects (including
diff --git a/proofs/proofview_monad.ml b/proofs/proofview_monad.ml
index b04d053f5..8f494c309 100644
--- a/proofs/proofview_monad.ml
+++ b/proofs/proofview_monad.ml
@@ -9,8 +9,152 @@
 (** This file defines the datatypes used as internal states by the
     tactic monad, and specialises the [Logic_monad] to these type. *)
 
+(** {6 Trees/forest for traces} *)
+
+module Trace = struct
+
+  (** The intent is that an ['a forest] is a list of messages of type
+      ['a]. But messages can stand for a list of more precise
+      messages, hence the structure is organised as a tree. *)
+  type 'a forest = 'a tree list
+  and  'a tree   = Seq of 'a * 'a forest
+
+  (** To build a trace incrementally, we use an intermediary data
+      structure on which we can define an S-expression like language
+      (like a simplified xml except the closing tags do not carry a
+      name). Note that nodes are built from right to left in ['a
+      incr], the result is mirrored when returning so that in the
+      exposed interface, the forest is read from left to right.
+
+      Concretely, we want to add a new tree to a forest: and we are
+      building it by adding new trees to the left of its left-most
+      subtrees which is built the same way. *)
+  type 'a incr = { head:'a forest ; opened: 'a tree list }
+
+  (** S-expression like language as ['a incr] transformers. It is the
+      responsibility of the library builder not to use [close] when no
+      tag is open. *)
+  let empty_incr = { head=[] ; opened=[] }
+  let opn a { head ; opened } = { head ; opened = Seq(a,[])::opened }
+  let close { head ; opened } =
+    match opened with
+    | [a] -> { head = a::head ; opened=[] }
+    | a::Seq(b,f)::opened -> { head ; opened=Seq(b,a::f)::opened }
+    | [] -> assert false
+  let leaf a s = close (opn a s)
+
+  (** Returning a forest. It is the responsibility of the library
+      builder to close all the tags. *)
+  (* spiwack: I may want to close the tags instead, to deal with
+     interruptions. *)
+  let rec mirror f = List.rev_map mirror_tree f
+  and mirror_tree (Seq(a,f)) = Seq(a,mirror f)
+
+  let to_tree = function
+    | { head ; opened=[] } -> mirror head
+    | { head ; opened=_::_} -> assert false
+
+end
+
+
+
 (** {6 State types} *)
 
+(** We typically label nodes of [Trace.tree] with messages to
+    print. But we don't want to compute the result. *)
+type lazy_msg = unit -> Pp.std_ppcmds
+let pr_lazy_msg msg = msg ()
+
+(** Info trace. *)
+module Info = struct
+
+  (** The type of the tags for [info]. *)
+  type tag =
+    | Msg of lazy_msg (** A simple message *)
+    | Tactic of lazy_msg (** A tactic call *)
+    | Dispatch  (** A call to [tclDISPATCH]/[tclEXTEND] *)
+    | DBranch  (** A special marker to delimit individual branch of a dispatch. *)
+
+  type state = tag Trace.incr
+  type tree = tag Trace.forest
+
+
+
+  let pr_in_comments m = Pp.(str"(* "++pr_lazy_msg m++str" *)")
+
+  let unbranch = function
+    | Trace.Seq (DBranch,brs) -> brs
+    | _ -> assert false
+
+
+  let is_empty_branch = let open Trace in function
+    | Seq(DBranch,[]) -> true
+    | _ -> false
+
+  (** Dispatch with empty branches are (supposed to be) equivalent to
+      [idtac] which need not appear, so they are removed from the
+      trace. *)
+  let dispatch brs =
+    let open Trace in
+    if CList.for_all is_empty_branch brs then None
+    else Some (Seq(Dispatch,brs))
+
+  let constr = let open Trace in function
+    | Dispatch -> dispatch
+    | t -> fun br -> Some (Seq(t,br))
+
+  let rec compress_tree = let open Trace in function
+    | Seq(t,f) -> constr t (compress f)
+  and compress f =
+    CList.map_filter compress_tree f
+
+  let rec is_empty = let open Trace in function
+    | Seq(Dispatch,brs) -> List.for_all is_empty brs
+    | Seq(DBranch,br) -> List.for_all is_empty br
+    | _ -> false
+
+  (** [with_sep] is [true] when [Tactic m] must be printed with a
+      trailing semi-colon. *)
+  let rec pr_tree with_sep = let open Trace in function
+    | Seq (Msg m,[]) -> pr_in_comments m
+    | Seq (Tactic m,_) ->
+        let tail = if with_sep then Pp.str";" else Pp.mt () in
+        Pp.(pr_lazy_msg m ++ tail)
+    | Seq (Dispatch,brs) ->
+        let tail = if with_sep then Pp.str";" else Pp.mt () in
+        Pp.(pr_dispatch brs++tail)
+    | Seq (Msg _,_::_) | Seq (DBranch,_) -> assert false
+  and pr_dispatch brs =
+    let open Pp in
+    let brs = List.map unbranch brs in
+    match brs with
+    | [br] -> pr_forest br
+    | _ ->
+        let sep () = spc()++str"|"++spc() in
+        let branches = prlist_with_sep sep pr_forest brs in
+        str"[>"++spc()++branches++spc()++str"]"
+  and pr_forest = function
+    | [] -> Pp.mt ()
+    | [tr] -> pr_tree false tr
+    | tr::l -> Pp.(pr_tree true tr ++ pr_forest l)
+
+  let print f =
+    pr_forest (compress f)
+
+  let rec collapse_tree n t =
+    let open Trace in
+    match n , t with
+    | 0 , t -> [t]
+    | _ , (Seq(Tactic _,[]) as t) -> [t]
+    | n , Seq(Tactic _,f) -> collapse (pred n) f
+    | n , Seq(Dispatch,brs) -> [Seq(Dispatch, (collapse n brs))]
+    | n , Seq(DBranch,br) -> [Seq(DBranch, (collapse n br))]
+    | _ , (Seq(Msg _,_) as t) -> [t]
+  and collapse n f =
+    CList.map_append (collapse_tree n) f
+end
+
+
 (** Type of proof views: current [evar_map] together with the list of
     focused goals. *)
 type proofview = { solution : Evd.evar_map; comb : Goal.goal list }
@@ -32,6 +176,10 @@ module P = struct
   let wunit = true , [] , []
   let wprod (b1,s1,g1) (b2,s2,g2) = b1 && b2 , s1@s2 , g1@g2
 
+  type u = Info.state
+
+  let uunit = Trace.empty_incr
+
 end
 
 module Logical = Logic_monad.Logical(P)
@@ -92,3 +240,18 @@ module Giveup : Writer with type t = Evar.t list = struct
   type t = Evar.t list
   let put gs = Logical.put (true,[],gs)
 end
+
+(** Lens and utilies pertaining to the info trace *)
+module InfoL = struct
+  let update = Logical.update
+  let opn a = update (Trace.opn a)
+  let close = update Trace.close
+  let leaf a = update (Trace.leaf a)
+
+  let tag a t =
+    let open Logical in
+    opn a >>
+    t >>= fun a ->
+    close >>
+    return a
+end
diff --git a/proofs/proofview_monad.mli b/proofs/proofview_monad.mli
index 43d1f6d80..ef20415ce 100644
--- a/proofs/proofview_monad.mli
+++ b/proofs/proofview_monad.mli
@@ -9,13 +9,67 @@
 (** This file defines the datatypes used as internal states by the
     tactic monad, and specialises the [Logic_monad] to these type. *)
 
+(** {6 Traces} *)
+
+module Trace : sig
+
+  (** The intent is that an ['a forest] is a list of messages of type
+      ['a]. But messages can stand for a list of more precise
+      messages, hence the structure is organised as a tree. *)
+  type 'a forest = 'a tree list
+  and  'a tree   = Seq of 'a * 'a forest
+
+  (** To build a trace incrementally, we use an intermediary data
+      structure on which we can define an S-expression like language
+      (like a simplified xml except the closing tags do not carry a
+      name). *)
+  type 'a incr
+  val to_tree : 'a incr -> 'a forest
+
+  (** [open a] opens a tag with name [a]. *)
+  val opn : 'a -> 'a incr -> 'a incr
+
+  (** [close] closes the last open tag. It is the responsibility of
+      the user to close all the tags. *)
+  val close : 'a incr -> 'a incr
+
+  (** [leaf] creates an empty tag with name [a]. *)
+  val leaf : 'a -> 'a incr -> 'a incr
+
+end
+
 (** {6 State types} *)
 
+(** We typically label nodes of [Trace.tree] with messages to
+    print. But we don't want to compute the result. *)
+type lazy_msg = unit -> Pp.std_ppcmds
+
+(** Info trace. *)
+module Info : sig
+
+  (** The type of the tags for [info]. *)
+  type tag =
+    | Msg of lazy_msg (** A simple message *)
+    | Tactic of lazy_msg (** A tactic call *)
+    | Dispatch  (** A call to [tclDISPATCH]/[tclEXTEND] *)
+    | DBranch  (** A special marker to delimit individual branch of a dispatch. *)
+
+  type state = tag Trace.incr
+  type tree = tag Trace.forest
+
+  val print : tree -> Pp.std_ppcmds
+
+  (** [collapse n t] flattens the first [n] levels of [Tactic] in an
+      info trace, effectively forgetting about the [n] top level of
+      names (if there are fewer, the last name is kept). *)
+  val collapse : int -> tree -> tree
+
+end
+
 (** Type of proof views: current [evar_map] together with the list of
     focused goals. *)
 type proofview = { solution : Evd.evar_map; comb : Goal.goal list }
 
-
 (** {6 Instantiation of the logic monad} *)
 
 module P : sig
@@ -28,6 +82,10 @@ module P : sig
   val wprod : w -> w -> w
 
   type e = unit
+
+  type u = Info.state
+
+  val uunit : u
 end
 
 module Logical : module type of Logic_monad.Logical(P)
@@ -69,3 +127,14 @@ module Shelf : Writer with type t = Evar.t list
 (** Lens to the list of goals which were given up during the execution
     of the tactic. *)
 module Giveup : Writer with type t = Evar.t list
+
+(** Lens and utilies pertaining to the info trace *)
+module InfoL : sig
+  val update : (Info.state -> Info.state) -> unit Logical.t
+  val opn : Info.tag -> unit Logical.t
+  val close : unit Logical.t
+  val leaf : Info.tag -> unit Logical.t
+
+  (** [tag a t] opens tag [a] runs [t] then closes the tag. *)
+  val tag : Info.tag -> 'a Logical.t -> 'a Logical.t
+end