Module Documentation

Module LCF

Validation

type Validation d e = List d -> Eff (err :: Exception | e) d

A Validation d e constructs a proof/derivation d from the proofs of its subgoals.

ProofState

type ProofState j d e = { validation :: Validation d e, subgoals :: List j }

A ProofState j d e is a list of subgoals (judgements j) and a validation.

Tactic

newtype Tactic j d e
  = Tactic (j -> Eff (err :: Exception | e) (ProofState j d e))

A Tactic j d e is a strategy for constructing a proof in d of a judgement in j by transforming the proof state.

runTactic

runTactic :: forall j d e. Tactic j d e -> j -> Eff (err :: Exception | e) (ProofState j d e)

idT

idT :: forall j d e. Tactic j d e

The identity tactic has no effect on the proof state.

lazyThenLT

lazyThenLT :: forall j d e. Tactic j d e -> Lazy [Tactic j d e] -> Tactic j d e

lazyThenLT t ts applies the tactics ts pointwise to the subgoals generated by the tactic t.

lazyThenT

lazyThenT :: forall j d e. Tactic j d e -> Lazy (Tactic j d e) -> Tactic j d e

lazyThenT t1 t2 applies the tactic t2 to each of the subgoals generated by the tactic t.

thenLT

thenLT :: forall j d e. Tactic j d e -> [Tactic j d e] -> Tactic j d e

thenLT t ts applies the tactics ts pointwise to the subgoals generated by the tactic t.

thenT

thenT :: forall j d e. Tactic j d e -> Tactic j d e -> Tactic j d e

thenT t1 t2 applies the tactic t2 to each of the subgoals generated by the tactic t.

semigroupTactic

instance semigroupTactic :: Semigroup (Tactic j d e)

Tactics form a semigroup via the thenT tactical.

monoidTactic

instance monoidTactic :: Monoid (Tactic j d e)

Tactics form a monoid via the idT tactic, which is the unit of thenT.

lazyOrElseT

lazyOrElseT :: forall j d e. Tactic j d e -> Lazy (Tactic j d e) -> Tactic j d e

lazyOrElseT t1 t2first triest1, and if it fails, then tries t2`.

orElseT

orElseT :: forall j d e. Tactic j d e -> Tactic j d e -> Tactic j d e

orElseT t1 t2first triest1, and if it fails, then tries t2`.

failT

failT :: forall j d e. Tactic j d e

failT always fails.

tryT

tryT :: forall j d e. Tactic j d e -> Tactic j d e

tryT either succeeds, or does nothing.

repeatT

repeatT :: forall j d e. Tactic j d e -> Tactic j d e

repeatT repeats a tactic for as long as it succeeds. repeatT never fails.

notT

notT :: forall j d e. Tactic j d e -> Tactic j d e

Succeeds if the tactic fails; fails if the tactic succeeds.

impliesT

impliesT :: forall j d e. Tactic j d e -> Tactic j d e -> Tactic j d e

Classical "implication" of tactics: either the left tactic fails, or the right tactic succeeds. Note: I am not sure if this is useful at all, but it seemed interesting it was definable.

AdditiveTactic

newtype AdditiveTactic j d e
  = AdditiveTactic (Tactic j d e)

The tactics also give rise to another semigroup and monoid structure, given by disjunction and failure.

getAdditiveTactic

getAdditiveTactic :: forall j d e. AdditiveTactic j d e -> Tactic j d e

semigroupAdditiveTactic

instance semigroupAdditiveTactic :: Semigroup (AdditiveTactic j d e)

The semigroup operation is given by orElseT.

monoidAdditiveTactic

instance monoidAdditiveTactic :: Monoid (AdditiveTactic j d e)

The monoid arises from the failT tactic, which is the unit of orElseT.

Module LCF.Notation

(/\)

(/\) :: forall j d e. Tactic j d e -> Tactic j d e -> Tactic j d e

An abbreviation for thenT.

(\/)

(\/) :: forall j d e. Tactic j d e -> Tactic j d e -> Tactic j d e

An abbreviation for orElseT.

(/\*)

(/\*) :: forall j d e. Tactic j d e -> [Tactic j d e] -> Tactic j d e

An abbreviation for thenLT.

(~>)

(~>) :: forall j d e. Tactic j d e -> Tactic j d e -> Tactic j d e

An abbreviation for impliesT.