Module Logic_monad
This file implements the low-level monadic operations used by the tactic monad. The monad is divided into two layers: a non-logical layer which consists in operations which will not (or cannot) be backtracked in case of failure (input/output or persistent state) and a logical layer which handles backtracking, proof manipulation, and any other effect which needs to backtrack.
Exceptions
exception
Exception of exn
To help distinguish between exceptions raised by the IO monad from the one used natively by Coq, the former are wrapped in
Exception
. It is only used internally so thatcatch
blocks of the IO monad would only catch exceptions raised by theraise
function of the IO monad, and not for instance, by system interrupts. Also used inProofview
to avoid capturing exception from the IO monad (Proofview
catches errors in its compatibility layer, and when lifting goal-level expressions).
Non-logical layer
module NonLogical : sig ... end
The non-logical monad is a simple
unit -> 'a
(i/o) monad. The operations are simple wrappers around corresponding usual operations and require little documentation.
Logical layer
type ('a, 'b, 'e) list_view_
=
|
Nil of 'e
|
Cons of 'a * 'b
A view type for the logical monad, which is a form of list, hence we can decompose it with as a list.
type ('a, 'b, 'e) list_view
= ('a, 'e -> 'b, 'e) list_view_
module BackState : sig ... end
module type Param = sig ... end
The monad is parametrised in the types of state, environment and writer.