# 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 that`catch`

blocks of the IO monad would only catch exceptions raised by the`raise`

function of the IO monad, and not for instance, by system interrupts. Also used in`Proofview`

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 * 'e -> 'b`

A view type for the logical monad, which is a form of list, hence we can decompose it with as a list.

`module BackState : sig ... end`

`module type Param = sig ... end`

The monad is parametrised in the types of state, environment and writer.