1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(** 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.t
(** 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"(* "++ 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
(** [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.(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 _env _sigma 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
module StateStore = Store.Make()
(* let (set_state, get_state) = StateDyn.Easy.make_dyn "goal_state" *)
type goal = Evar.t
type goal_with_state = Evar.t * StateStore.t
let drop_state = fst
let get_state = snd
let goal_with_state g s = (g, s)
let with_empty_state g = (g, StateStore.empty)
let map_goal_with_state f (g, s) = (f g, s)
(** Type of proof views: current [evar_map] together with the list of
focused goals. *)
type proofview = {
solution : Evd.evar_map;
comb : goal_with_state list;
}
(** {6 Instantiation of the logic monad} *)
(** Parameters of the logic monads *)
module P = struct
type s = proofview * Environ.env
(** Recording info trace (true) or not. *)
type e = { trace: bool; name : Names.Id.t; poly : bool }
(** Status (safe/unsafe) * shelved goals * given up *)
type w = bool
let wunit = true
let wprod b1 b2 = b1 && b2
type u = Info.state
let uunit = Trace.empty_incr
end
module Logical = Logic_monad.Logical(P)
(** {6 Lenses to access to components of the states} *)
module type State = sig
type t
val get : t Logical.t
val set : t -> unit Logical.t
val modify : (t->t) -> unit Logical.t
end
module type Reader = sig
type t
val get : t Logical.t
end
module type Writer = sig
type t
val put : t -> unit Logical.t
end
module Pv : State with type t := proofview = struct
let get = Logical.(map fst get)
let set p = Logical.modify (fun (_,e) -> (p,e))
let modify f= Logical.modify (fun (p,e) -> (f p,e))
end
module Solution : State with type t := Evd.evar_map = struct
let get = Logical.map (fun {solution} -> solution) Pv.get
let set s = Pv.modify (fun pv -> { pv with solution = s })
let modify f = Pv.modify (fun pv -> { pv with solution = f pv.solution })
end
module Comb : State with type t = goal_with_state list = struct
(* spiwack: I don't know why I cannot substitute ([:=]) [t] with a type expression. *)
type t = goal_with_state list
let get = Logical.map (fun {comb} -> comb) Pv.get
let set c = Pv.modify (fun pv -> { pv with comb = c })
let modify f = Pv.modify (fun pv -> { pv with comb = f pv.comb })
end
module Env : State with type t := Environ.env = struct
let get = Logical.(map snd get)
let set e = Logical.modify (fun (p,_) -> (p,e))
let modify f = Logical.modify (fun (p,e) -> (p,f e))
end
module Status : Writer with type t := bool = struct
let put s = Logical.put s
end
(** Lens and utilities pertaining to the info trace *)
module InfoL = struct
let recording = Logical.(map (fun {P.trace} -> trace) current)
let if_recording t =
let open Logical in
recording >>= fun r ->
if r then t else return ()
let record_trace t =
Logical.(
current >>= fun s ->
local {s with P.trace = true} t)
let raw_update = Logical.update
let update f = if_recording (raw_update f)
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
recording >>= fun r ->
if r then begin
raw_update (Trace.opn a) >>
t >>= fun a ->
raw_update Trace.close >>
return a
end else
t
end
|