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.
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.
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 :: forall j d e. Tactic j d e -> j -> Eff (err :: Exception | e) (ProofState j d e)
idT :: forall j d e. Tactic j d e
The identity tactic has no effect on the proof state.
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 :: 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 :: 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 :: 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
.
instance semigroupTactic :: Semigroup (Tactic j d e)
Tactics form a semigroup via the thenT
tactical.
instance monoidTactic :: Monoid (Tactic j d e)
Tactics form a monoid via the idT
tactic, which is the unit of thenT
.
lazyOrElseT :: forall j d e. Tactic j d e -> Lazy (Tactic j d e) -> Tactic j d e
lazyOrElseT
t1 t2first tries
t1, and if it fails, then tries
t2`.
orElseT :: forall j d e. Tactic j d e -> Tactic j d e -> Tactic j d e
orElseT
t1 t2first tries
t1, and if it fails, then tries
t2`.
failT :: forall j d e. Tactic j d e
failT
always fails.
tryT :: forall j d e. Tactic j d e -> Tactic j d e
tryT
either succeeds, or does nothing.
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 :: forall j d e. Tactic j d e -> Tactic j d e
Succeeds if the tactic fails; fails if the tactic succeeds.
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.
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 :: forall j d e. AdditiveTactic j d e -> Tactic j d e
instance semigroupAdditiveTactic :: Semigroup (AdditiveTactic j d e)
The semigroup operation is given by orElseT
.
instance monoidAdditiveTactic :: Monoid (AdditiveTactic j d e)
The monoid arises from the failT
tactic, which is the unit of orElseT
.
(/\) :: 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
.