An API for info traces.

1 files changed, 163 insertions, 0 deletions

diff --git a/proofs/proofview_monad.ml b/proofs/proofview_monad.ml
index b04d053f5b..8f494c3098 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