{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PatternSynonyms #-}

{-|
Module      : Theory.Signature
Description : Theory-level signatures
Copyright   : (c) Julian Grove and Aaron Steven White, 2025
License     : MIT
Maintainer  : julian.grove@gmail.com

Theory-level signatures.
-}

module Theory.Signature ( tauStates
                        ) where

import Framework.Lambda.Convenience
import Framework.Lambda.Signature
import Framework.Lambda.Terms
import Framework.Lambda.Types

tauStates :: Sig
tauStates :: Sig
tauStates = Type -> [(String, Type)] -> Sig
mkStateSig Type
σ                    [ ( String
"CG"  , Type -> Type
P Type
ι ) ]         Sig -> Sig -> Sig
forall (m :: * -> *) a b.
Alternative m =>
(a -> m b) -> (a -> m b) -> a -> m b
<||>
            Type -> (Type -> Type) -> (Type -> Type) -> [(String, Type)] -> Sig
mkStackSig Type
σ (Type -> Type -> Type -> Type
q Type
ι Type
α) (Type -> Type -> Type -> Type
popQ Type
ι Type
α) [ ( String
"QUD" , Type
α Type -> Type -> Type
:→ Type
ι Type -> Type -> Type
:→ Type
t ) ]