Safe Haskell	None
Language	GHC2021

Conformance.Story.Specification

Description

Reusable theorem and clause structure, independent of registry actions.

Synopsis

type Story (act :: Type -> Type) = Program (Step act)
data Step (act :: Type -> Type) res where
- Action :: forall (act :: Type -> Type) res. act res -> Step act res
- Theorem :: forall {k} (thm :: k) (act :: Type -> Type) res. Theorem thm -> TheoremStory thm act res -> Step act res
data Theorem (thm :: k)
bindTheorem :: forall {k} (thm :: k). Binding -> Theorem thm
theoremBinding :: forall {k} (thm :: k). Theorem thm -> Binding
data TheoremStory (thm :: k) (act :: Type -> Type) res
data Clause (thm :: k) (act :: Type -> Type) obs where
- Clause :: forall {k} (act :: Type -> Type) (thm :: k) obs. String -> LeanCheck act thm obs -> Story act obs -> Clause thm act obs
clauses :: forall {k} (thm :: k) (act :: Type -> Type) res. TheoremStory thm act res -> Program (Clause thm act) res
data LeanCheck (act :: Type -> Type) (thm :: k) obs
bindCheck :: forall {k} (thm :: k) obs (act :: Type -> Type). Theorem thm -> (obs -> Story act ()) -> LeanCheck act thm obs
checkTheorem :: forall {k} (act :: Type -> Type) (thm :: k) obs. LeanCheck act thm obs -> Theorem thm
checkAction :: forall {k} (act :: Type -> Type) (thm :: k) obs. LeanCheck act thm obs -> obs -> Story act ()
action :: act res -> Story act res
theorem :: forall {k} (thm :: k) (act :: Type -> Type) res. Theorem thm -> TheoremStory thm act res -> Story act res
clause :: forall {k} (act :: Type -> Type) (thm :: k) obs. String -> LeanCheck act thm obs -> Story act obs -> TheoremStory thm act obs

Documentation

type Story (act :: Type -> Type) = Program (Step act) Source #

A reusable action program with nested theorem-scoped clauses.

data Step (act :: Type -> Type) res where Source #

The structure interpreted by both execution and presentation.

Constructors

Action :: forall (act :: Type -> Type) res. act res -> Step act res
Theorem :: forall {k} (thm :: k) (act :: Type -> Type) res. Theorem thm -> TheoremStory thm act res -> Step act res

data Theorem (thm :: k) Source #

A bound declaration. Its nominal index identifies the theorem's checks.

bindTheorem :: forall {k} (thm :: k). Binding -> Theorem thm Source #

Bind a domain-specific theorem marker to its checked declaration identity.

theoremBinding :: forall {k} (thm :: k). Theorem thm -> Binding Source #

The declaration resolved by execution and named by rendering.

data TheoremStory (thm :: k) (act :: Type -> Type) res Source #

Clauses belonging to one theorem. The index cannot be changed by coercion.

Instances details

Applicative (TheoremStory thm act) Source #
Instance details Defined in Conformance.Story.Specification Methods pure :: a -> TheoremStory thm act a Source # (<>) :: TheoremStory thm act (a -> b) -> TheoremStory thm act a -> TheoremStory thm act b Source # liftA2 :: (a -> b -> c) -> TheoremStory thm act a -> TheoremStory thm act b -> TheoremStory thm act c Source # (>) :: TheoremStory thm act a -> TheoremStory thm act b -> TheoremStory thm act b Source # (<*) :: TheoremStory thm act a -> TheoremStory thm act b -> TheoremStory thm act a Source #
Functor (TheoremStory thm act) Source #
Instance details Defined in Conformance.Story.Specification Methods fmap :: (a -> b) -> TheoremStory thm act a -> TheoremStory thm act b Source # (<$) :: a -> TheoremStory thm act b -> TheoremStory thm act a Source #
Monad (TheoremStory thm act) Source #
Instance details Defined in Conformance.Story.Specification Methods (>>=) :: TheoremStory thm act a -> (a -> TheoremStory thm act b) -> TheoremStory thm act b Source # (>>) :: TheoremStory thm act a -> TheoremStory thm act b -> TheoremStory thm act b Source # return :: a -> TheoremStory thm act a Source #

data Clause (thm :: k) (act :: Type -> Type) obs where Source #

An action's result is checked before it is returned to the surrounding story.

Constructors

Clause :: forall {k} (act :: Type -> Type) (thm :: k) obs. String -> LeanCheck act thm obs -> Story act obs -> Clause thm act obs

clauses :: forall {k} (thm :: k) (act :: Type -> Type) res. TheoremStory thm act res -> Program (Clause thm act) res Source #

Expose the clause program to interpreters without permitting reindexing.

data LeanCheck (act :: Type -> Type) (thm :: k) obs Source #

A check retains its theorem and supplies an interpreter action for the observation.

bindCheck :: forall {k} (thm :: k) obs (act :: Type -> Type). Theorem thm -> (obs -> Story act ()) -> LeanCheck act thm obs Source #

Domain bindings supply the executable check of an observed result.

checkTheorem :: forall {k} (act :: Type -> Type) (thm :: k) obs. LeanCheck act thm obs -> Theorem thm Source #

Resolve the same declaration for the enclosing theorem and its check.

checkAction :: forall {k} (act :: Type -> Type) (thm :: k) obs. LeanCheck act thm obs -> obs -> Story act () Source #

Run the domain's check through the same interpreter as its actions.

action :: act res -> Story act res Source #

Lift one domain action into the shared story language.

theorem :: forall {k} (thm :: k) (act :: Type -> Type) res. Theorem thm -> TheoremStory thm act res -> Story act res Source #

Execute clauses under their governing theorem.

clause :: forall {k} (act :: Type -> Type) (thm :: k) obs. String -> LeanCheck act thm obs -> Story act obs -> TheoremStory thm act obs Source #

Name an observation and associate its action with a check of the same theorem.