package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type

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).

exception Tac_Timeout

This exception is used to signal abortion in timeout functions.

exception TacticFailure of exn

This exception is used by the tactics to signal failure by lack of successes, rather than some other exceptions (like system interrupts).

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

The logical monad is a backtracking monad on top of which is layered a state monad (which is used to implement all of read/write, read only, and write only effects). The state monad being layered on top of the backtracking monad makes it so that the state is backtracked on failure.

Backtracking differs from regular exception in that, writing (+) for exception catching and (>>=) for bind, we require the following extra distributivity laws:

x+(y+z) = (x+y)+z

zero+x = x

x+zero = x

(x+y)>>=k = (x>>=k)+(y>>=k)

type ('a, 'b, 'e) list_view_ =
  1. | Nil of 'e
  2. | 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.

module Logical (P : Param) : sig ... end
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct