{-# LANGUAGE GADTs #-}
{-# LANGUAGE RoleAnnotations #-}

-- | Reusable theorem and clause structure, independent of registry actions.
module Conformance.Story.Specification
    ( Story
    , Step (..)
    , Theorem
    , bindTheorem
    , theoremBinding
    , TheoremStory
    , Clause (..)
    , clauses
    , LeanCheck
    , bindCheck
    , checkTheorem
    , checkAction
    , action
    , theorem
    , clause
    ) where

import Conformance.Story.Binding (Binding)
import Control.Monad.Operational (Program, singleton)

-- | A bound declaration. Its nominal index identifies the theorem's checks.
type role Theorem nominal

newtype Theorem thm = BoundTheorem Binding

-- | Bind a domain-specific theorem marker to its checked declaration identity.
bindTheorem :: Binding -> Theorem thm
bindTheorem :: forall {k} (thm :: k). Binding -> Theorem thm
bindTheorem = Binding -> Theorem thm
forall {k} (thm :: k). Binding -> Theorem thm
BoundTheorem

-- | The declaration resolved by execution and named by rendering.
theoremBinding :: Theorem thm -> Binding
theoremBinding :: forall {k} (thm :: k). Theorem thm -> Binding
theoremBinding (BoundTheorem Binding
binding) = Binding
binding

-- | A check retains its theorem and supplies an interpreter action for the observation.
type role LeanCheck nominal nominal nominal

data LeanCheck act thm obs = BoundCheck (Theorem thm) (obs -> Story act ())

-- | Domain bindings supply the executable check of an observed result.
bindCheck
    :: Theorem thm -> (obs -> Story act ()) -> LeanCheck act thm obs
bindCheck :: forall {k} (thm :: k) obs (act :: * -> *).
Theorem thm -> (obs -> Story act ()) -> LeanCheck act thm obs
bindCheck = Theorem thm -> (obs -> Story act ()) -> LeanCheck act thm obs
forall {k} (act :: * -> *) (thm :: k) obs.
Theorem thm -> (obs -> Story act ()) -> LeanCheck act thm obs
BoundCheck

-- | Resolve the same declaration for the enclosing theorem and its check.
checkTheorem :: LeanCheck act thm obs -> Theorem thm
checkTheorem :: forall {k} (act :: * -> *) (thm :: k) obs.
LeanCheck act thm obs -> Theorem thm
checkTheorem (BoundCheck Theorem thm
binding obs -> Story act ()
_) = Theorem thm
binding

-- | Run the domain's check through the same interpreter as its actions.
checkAction :: LeanCheck act thm obs -> obs -> Story act ()
checkAction :: forall {k} (act :: * -> *) (thm :: k) obs.
LeanCheck act thm obs -> obs -> Story act ()
checkAction (BoundCheck Theorem thm
_ obs -> Story act ()
check) = obs -> Story act ()
check

-- | A reusable action program with nested theorem-scoped clauses.
type Story act = Program (Step act)

-- | The structure interpreted by both execution and presentation.
data Step act res where
    Action :: act res -> Step act res
    Theorem :: Theorem thm -> TheoremStory thm act res -> Step act res

-- | Clauses belonging to one theorem. The index cannot be changed by coercion.
newtype TheoremStory thm act res = TheoremStory (Program (Clause thm act) res)
    deriving newtype ((forall a b.
 (a -> b) -> TheoremStory thm act a -> TheoremStory thm act b)
-> (forall a b.
    a -> TheoremStory thm act b -> TheoremStory thm act a)
-> Functor (TheoremStory thm act)
forall k (thm :: k) (act :: * -> *) a b.
a -> TheoremStory thm act b -> TheoremStory thm act a
forall k (thm :: k) (act :: * -> *) a b.
(a -> b) -> TheoremStory thm act a -> TheoremStory thm act b
forall a b. a -> TheoremStory thm act b -> TheoremStory thm act a
forall a b.
(a -> b) -> TheoremStory thm act a -> TheoremStory thm act b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall k (thm :: k) (act :: * -> *) a b.
(a -> b) -> TheoremStory thm act a -> TheoremStory thm act b
fmap :: forall a b.
(a -> b) -> TheoremStory thm act a -> TheoremStory thm act b
$c<$ :: forall k (thm :: k) (act :: * -> *) a b.
a -> TheoremStory thm act b -> TheoremStory thm act a
<$ :: forall a b. a -> TheoremStory thm act b -> TheoremStory thm act a
Functor, Functor (TheoremStory thm act)
Functor (TheoremStory thm act) =>
(forall a. a -> TheoremStory thm act a)
-> (forall a b.
    TheoremStory thm act (a -> b)
    -> TheoremStory thm act a -> TheoremStory thm act b)
-> (forall a b c.
    (a -> b -> c)
    -> TheoremStory thm act a
    -> TheoremStory thm act b
    -> TheoremStory thm act c)
-> (forall a b.
    TheoremStory thm act a
    -> TheoremStory thm act b -> TheoremStory thm act b)
-> (forall a b.
    TheoremStory thm act a
    -> TheoremStory thm act b -> TheoremStory thm act a)
-> Applicative (TheoremStory thm act)
forall a. a -> TheoremStory thm act a
forall k (thm :: k) (act :: * -> *). Functor (TheoremStory thm act)
forall k (thm :: k) (act :: * -> *) a. a -> TheoremStory thm act a
forall k (thm :: k) (act :: * -> *) a b.
TheoremStory thm act a
-> TheoremStory thm act b -> TheoremStory thm act a
forall k (thm :: k) (act :: * -> *) a b.
TheoremStory thm act a
-> TheoremStory thm act b -> TheoremStory thm act b
forall k (thm :: k) (act :: * -> *) a b.
TheoremStory thm act (a -> b)
-> TheoremStory thm act a -> TheoremStory thm act b
forall k (thm :: k) (act :: * -> *) a b c.
(a -> b -> c)
-> TheoremStory thm act a
-> TheoremStory thm act b
-> TheoremStory thm act c
forall a b.
TheoremStory thm act a
-> TheoremStory thm act b -> TheoremStory thm act a
forall a b.
TheoremStory thm act a
-> TheoremStory thm act b -> TheoremStory thm act b
forall a b.
TheoremStory thm act (a -> b)
-> TheoremStory thm act a -> TheoremStory thm act b
forall a b c.
(a -> b -> c)
-> TheoremStory thm act a
-> TheoremStory thm act b
-> TheoremStory thm act c
forall (f :: * -> *).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
$cpure :: forall k (thm :: k) (act :: * -> *) a. a -> TheoremStory thm act a
pure :: forall a. a -> TheoremStory thm act a
$c<*> :: forall k (thm :: k) (act :: * -> *) a b.
TheoremStory thm act (a -> b)
-> TheoremStory thm act a -> TheoremStory thm act b
<*> :: forall a b.
TheoremStory thm act (a -> b)
-> TheoremStory thm act a -> TheoremStory thm act b
$cliftA2 :: forall k (thm :: k) (act :: * -> *) a b c.
(a -> b -> c)
-> TheoremStory thm act a
-> TheoremStory thm act b
-> TheoremStory thm act c
liftA2 :: forall a b c.
(a -> b -> c)
-> TheoremStory thm act a
-> TheoremStory thm act b
-> TheoremStory thm act c
$c*> :: forall k (thm :: k) (act :: * -> *) a b.
TheoremStory thm act a
-> TheoremStory thm act b -> TheoremStory thm act b
*> :: forall a b.
TheoremStory thm act a
-> TheoremStory thm act b -> TheoremStory thm act b
$c<* :: forall k (thm :: k) (act :: * -> *) a b.
TheoremStory thm act a
-> TheoremStory thm act b -> TheoremStory thm act a
<* :: forall a b.
TheoremStory thm act a
-> TheoremStory thm act b -> TheoremStory thm act a
Applicative, Applicative (TheoremStory thm act)
Applicative (TheoremStory thm act) =>
(forall a b.
 TheoremStory thm act a
 -> (a -> TheoremStory thm act b) -> TheoremStory thm act b)
-> (forall a b.
    TheoremStory thm act a
    -> TheoremStory thm act b -> TheoremStory thm act b)
-> (forall a. a -> TheoremStory thm act a)
-> Monad (TheoremStory thm act)
forall a. a -> TheoremStory thm act a
forall k (thm :: k) (act :: * -> *).
Applicative (TheoremStory thm act)
forall k (thm :: k) (act :: * -> *) a. a -> TheoremStory thm act a
forall k (thm :: k) (act :: * -> *) a b.
TheoremStory thm act a
-> TheoremStory thm act b -> TheoremStory thm act b
forall k (thm :: k) (act :: * -> *) a b.
TheoremStory thm act a
-> (a -> TheoremStory thm act b) -> TheoremStory thm act b
forall a b.
TheoremStory thm act a
-> TheoremStory thm act b -> TheoremStory thm act b
forall a b.
TheoremStory thm act a
-> (a -> TheoremStory thm act b) -> TheoremStory thm act b
forall (m :: * -> *).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
$c>>= :: forall k (thm :: k) (act :: * -> *) a b.
TheoremStory thm act a
-> (a -> TheoremStory thm act b) -> TheoremStory thm act b
>>= :: forall a b.
TheoremStory thm act a
-> (a -> TheoremStory thm act b) -> TheoremStory thm act b
$c>> :: forall k (thm :: k) (act :: * -> *) a b.
TheoremStory thm act a
-> TheoremStory thm act b -> TheoremStory thm act b
>> :: forall a b.
TheoremStory thm act a
-> TheoremStory thm act b -> TheoremStory thm act b
$creturn :: forall k (thm :: k) (act :: * -> *) a. a -> TheoremStory thm act a
return :: forall a. a -> TheoremStory thm act a
Monad)

-- | An action's result is checked before it is returned to the surrounding story.
data Clause thm act obs where
    Clause
        :: String -> LeanCheck act thm obs -> Story act obs -> Clause thm act obs

-- | Expose the clause program to interpreters without permitting reindexing.
clauses :: TheoremStory thm act res -> Program (Clause thm act) res
clauses :: forall {k} (thm :: k) (act :: * -> *) res.
TheoremStory thm act res -> Program (Clause thm act) res
clauses (TheoremStory Program (Clause thm act) res
program) = Program (Clause thm act) res
program

-- | Lift one domain action into the shared story language.
action :: act res -> Story act res
action :: forall (act :: * -> *) res. act res -> Story act res
action = Step act res -> ProgramT (Step act) Identity res
forall (instr :: * -> *) a (m :: * -> *).
instr a -> ProgramT instr m a
singleton (Step act res -> ProgramT (Step act) Identity res)
-> (act res -> Step act res)
-> act res
-> ProgramT (Step act) Identity res
forall b c a. (b -> c) -> (a -> b) -> a -> c
. act res -> Step act res
forall (act :: * -> *) res. act res -> Step act res
Action

-- | Execute clauses under their governing theorem.
theorem
    :: Theorem thm
    -> TheoremStory thm act res
    -> Story act res
theorem :: forall {k} (thm :: k) (act :: * -> *) res.
Theorem thm -> TheoremStory thm act res -> Story act res
theorem Theorem thm
binding TheoremStory thm act res
body = Step act res -> ProgramT (Step act) Identity res
forall (instr :: * -> *) a (m :: * -> *).
instr a -> ProgramT instr m a
singleton (Theorem thm -> TheoremStory thm act res -> Step act res
forall {k} (thm :: k) (act :: * -> *) res.
Theorem thm -> TheoremStory thm act res -> Step act res
Theorem Theorem thm
binding TheoremStory thm act res
body)

-- | Name an observation and associate its action with a check of the same theorem.
clause
    :: String
    -> LeanCheck act thm obs
    -> Story act obs
    -> TheoremStory thm act obs
clause :: forall {k} (act :: * -> *) (thm :: k) obs.
String
-> LeanCheck act thm obs
-> Story act obs
-> TheoremStory thm act obs
clause String
title LeanCheck act thm obs
check Story act obs
body = Program (Clause thm act) obs -> TheoremStory thm act obs
forall {k} (thm :: k) (act :: * -> *) res.
Program (Clause thm act) res -> TheoremStory thm act res
TheoremStory (Clause thm act obs -> Program (Clause thm act) obs
forall (instr :: * -> *) a (m :: * -> *).
instr a -> ProgramT instr m a
singleton (String
-> LeanCheck act thm obs -> Story act obs -> Clause thm act obs
forall {k} (act :: * -> *) (thm :: k) obs.
String
-> LeanCheck act thm obs -> Story act obs -> Clause thm act obs
Clause String
title LeanCheck act thm obs
check Story act obs
body))