{-# OPTIONS_GHC -fno-warn-duplicate-exports #-}
{-# LANGUAGE DeriveAnyClass             #-}
{-# LANGUAGE DeriveFunctor              #-}
{-# LANGUAGE DeriveGeneric              #-}
{-# LANGUAGE DerivingStrategies         #-}
{-# LANGUAGE DuplicateRecordFields      #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE PatternSynonyms            #-}
{-# LANGUAGE TypeFamilies               #-}

-- | This is a module containing types to model the ATS syntax tree. As it is
-- collapsed by the pretty printer, you may see that in some places it is
-- focused on the lexical side of things.
module Language.ATS.Types
    ( ATS (..)
    , Declaration (..)
    , Type (..)
    , Name (..)
    , Pattern (..)
    , PatternF (..)
    , Arg (..)
    , Universal (..)
    , Function (..)
    , Expression (..)
    , ExpressionF (..)
    , Implementation (..)
    , BinOp (..)
    , BinOp (Con)
    , UnOp (..)
    , TypeF (..)
    , Existential (..)
    , LambdaType (..)
    , Addendum (..)
    , DataPropLeaf (..)
    , PreFunction (..)
    , Leaf (..)
    , StaticExpression (..)
    , StaticExpressionF (..)
    , Fixity (..)
    , StackFunction (..)
    , Sort (..)
    , SortF (..)
    , SortArg (..)
    , SortArgs
    , Args
    , DataSortLeaf (..)
    , Fix
    , FixityState
    ) where

import           Control.DeepSeq    (NFData)
import           Control.Recursion  hiding (Fix (..))
import           Data.Function      (on)
import           Data.List.NonEmpty (NonEmpty)
import qualified Data.Map           as M
import           Data.These         (These)
import           GHC.Generics       (Generic)
import           GHC.Natural        (Natural)
import           Language.ATS.Lexer (Addendum (..))

type Fix = Either Int String

data Fixity a = RightFix { Fixity a -> a
pos :: a, Fixity a -> Fix
ifix :: Fix }
              | LeftFix { pos :: a, ifix :: Fix }
              | Pre { pos :: a, ifix :: Fix }
              | Post { pos :: a, ifix :: Fix }
              | Infix { pos :: a, ifix :: Fix }
              deriving (Int -> Fixity a -> ShowS
[Fixity a] -> ShowS
Fixity a -> String
(Int -> Fixity a -> ShowS)
-> (Fixity a -> String) -> ([Fixity a] -> ShowS) -> Show (Fixity a)
forall a. Show a => Int -> Fixity a -> ShowS
forall a. Show a => [Fixity a] -> ShowS
forall a. Show a => Fixity a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Fixity a] -> ShowS
$cshowList :: forall a. Show a => [Fixity a] -> ShowS
show :: Fixity a -> String
$cshow :: forall a. Show a => Fixity a -> String
showsPrec :: Int -> Fixity a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Fixity a -> ShowS
Show, Fixity a -> Fixity a -> Bool
(Fixity a -> Fixity a -> Bool)
-> (Fixity a -> Fixity a -> Bool) -> Eq (Fixity a)
forall a. Eq a => Fixity a -> Fixity a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Fixity a -> Fixity a -> Bool
$c/= :: forall a. Eq a => Fixity a -> Fixity a -> Bool
== :: Fixity a -> Fixity a -> Bool
$c== :: forall a. Eq a => Fixity a -> Fixity a -> Bool
Eq, (forall x. Fixity a -> Rep (Fixity a) x)
-> (forall x. Rep (Fixity a) x -> Fixity a) -> Generic (Fixity a)
forall x. Rep (Fixity a) x -> Fixity a
forall x. Fixity a -> Rep (Fixity a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Fixity a) x -> Fixity a
forall a x. Fixity a -> Rep (Fixity a) x
$cto :: forall a x. Rep (Fixity a) x -> Fixity a
$cfrom :: forall a x. Fixity a -> Rep (Fixity a) x
Generic, Fixity a -> ()
(Fixity a -> ()) -> NFData (Fixity a)
forall a. NFData a => Fixity a -> ()
forall a. (a -> ()) -> NFData a
rnf :: Fixity a -> ()
$crnf :: forall a. NFData a => Fixity a -> ()
NFData)

-- | An ATS file, containing a list of declarations
newtype ATS a = ATS { ATS a -> [Declaration a]
unATS :: [Declaration a] }
    deriving (Int -> ATS a -> ShowS
[ATS a] -> ShowS
ATS a -> String
(Int -> ATS a -> ShowS)
-> (ATS a -> String) -> ([ATS a] -> ShowS) -> Show (ATS a)
forall a. Show a => Int -> ATS a -> ShowS
forall a. Show a => [ATS a] -> ShowS
forall a. Show a => ATS a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ATS a] -> ShowS
$cshowList :: forall a. Show a => [ATS a] -> ShowS
show :: ATS a -> String
$cshow :: forall a. Show a => ATS a -> String
showsPrec :: Int -> ATS a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> ATS a -> ShowS
Show, ATS a -> ATS a -> Bool
(ATS a -> ATS a -> Bool) -> (ATS a -> ATS a -> Bool) -> Eq (ATS a)
forall a. Eq a => ATS a -> ATS a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ATS a -> ATS a -> Bool
$c/= :: forall a. Eq a => ATS a -> ATS a -> Bool
== :: ATS a -> ATS a -> Bool
$c== :: forall a. Eq a => ATS a -> ATS a -> Bool
Eq, (forall x. ATS a -> Rep (ATS a) x)
-> (forall x. Rep (ATS a) x -> ATS a) -> Generic (ATS a)
forall x. Rep (ATS a) x -> ATS a
forall x. ATS a -> Rep (ATS a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (ATS a) x -> ATS a
forall a x. ATS a -> Rep (ATS a) x
$cto :: forall a x. Rep (ATS a) x -> ATS a
$cfrom :: forall a x. ATS a -> Rep (ATS a) x
Generic)
    deriving newtype (ATS a -> ()
(ATS a -> ()) -> NFData (ATS a)
forall a. NFData a => ATS a -> ()
forall a. (a -> ()) -> NFData a
rnf :: ATS a -> ()
$crnf :: forall a. NFData a => ATS a -> ()
NFData, b -> ATS a -> ATS a
NonEmpty (ATS a) -> ATS a
ATS a -> ATS a -> ATS a
(ATS a -> ATS a -> ATS a)
-> (NonEmpty (ATS a) -> ATS a)
-> (forall b. Integral b => b -> ATS a -> ATS a)
-> Semigroup (ATS a)
forall b. Integral b => b -> ATS a -> ATS a
forall a. NonEmpty (ATS a) -> ATS a
forall a. ATS a -> ATS a -> ATS a
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
forall a b. Integral b => b -> ATS a -> ATS a
stimes :: b -> ATS a -> ATS a
$cstimes :: forall a b. Integral b => b -> ATS a -> ATS a
sconcat :: NonEmpty (ATS a) -> ATS a
$csconcat :: forall a. NonEmpty (ATS a) -> ATS a
<> :: ATS a -> ATS a -> ATS a
$c<> :: forall a. ATS a -> ATS a -> ATS a
Semigroup, Semigroup (ATS a)
ATS a
Semigroup (ATS a)
-> ATS a
-> (ATS a -> ATS a -> ATS a)
-> ([ATS a] -> ATS a)
-> Monoid (ATS a)
[ATS a] -> ATS a
ATS a -> ATS a -> ATS a
forall a. Semigroup (ATS a)
forall a. ATS a
forall a.
Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
forall a. [ATS a] -> ATS a
forall a. ATS a -> ATS a -> ATS a
mconcat :: [ATS a] -> ATS a
$cmconcat :: forall a. [ATS a] -> ATS a
mappend :: ATS a -> ATS a -> ATS a
$cmappend :: forall a. ATS a -> ATS a -> ATS a
mempty :: ATS a
$cmempty :: forall a. ATS a
$cp1Monoid :: forall a. Semigroup (ATS a)
Monoid)

data Leaf a = Leaf { Leaf a -> [Universal a]
_constructorUniversals :: [Universal a], Leaf a -> String
name :: String, Leaf a -> [StaticExpression a]
constructorArgs :: [StaticExpression a], Leaf a -> Maybe (Type a)
maybeType :: Maybe (Type a) }
    deriving (Int -> Leaf a -> ShowS
[Leaf a] -> ShowS
Leaf a -> String
(Int -> Leaf a -> ShowS)
-> (Leaf a -> String) -> ([Leaf a] -> ShowS) -> Show (Leaf a)
forall a. Show a => Int -> Leaf a -> ShowS
forall a. Show a => [Leaf a] -> ShowS
forall a. Show a => Leaf a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Leaf a] -> ShowS
$cshowList :: forall a. Show a => [Leaf a] -> ShowS
show :: Leaf a -> String
$cshow :: forall a. Show a => Leaf a -> String
showsPrec :: Int -> Leaf a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Leaf a -> ShowS
Show, Leaf a -> Leaf a -> Bool
(Leaf a -> Leaf a -> Bool)
-> (Leaf a -> Leaf a -> Bool) -> Eq (Leaf a)
forall a. Eq a => Leaf a -> Leaf a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Leaf a -> Leaf a -> Bool
$c/= :: forall a. Eq a => Leaf a -> Leaf a -> Bool
== :: Leaf a -> Leaf a -> Bool
$c== :: forall a. Eq a => Leaf a -> Leaf a -> Bool
Eq, (forall x. Leaf a -> Rep (Leaf a) x)
-> (forall x. Rep (Leaf a) x -> Leaf a) -> Generic (Leaf a)
forall x. Rep (Leaf a) x -> Leaf a
forall x. Leaf a -> Rep (Leaf a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Leaf a) x -> Leaf a
forall a x. Leaf a -> Rep (Leaf a) x
$cto :: forall a x. Rep (Leaf a) x -> Leaf a
$cfrom :: forall a x. Leaf a -> Rep (Leaf a) x
Generic, Leaf a -> ()
(Leaf a -> ()) -> NFData (Leaf a)
forall a. NFData a => Leaf a -> ()
forall a. (a -> ()) -> NFData a
rnf :: Leaf a -> ()
$crnf :: forall a. NFData a => Leaf a -> ()
NFData)

type SortArgs a = Maybe [SortArg a]
type Args a = Maybe [Arg a]

-- | Declarations for functions, values, actions, etc.
data Declaration a = Func { Declaration a -> a
pos :: a, Declaration a -> Function a
_fun :: Function a }
                   | Impl { Declaration a -> Args a
implArgs :: Args a, Declaration a -> Implementation a
_impl :: Implementation a } -- TODO do something better for implicit universals
                   | ProofImpl { implArgs :: Args a, _impl :: Implementation a }
                   | Val { Declaration a -> Addendum
add :: Addendum, Declaration a -> Maybe (Type a)
valT :: Maybe (Type a), Declaration a -> Maybe (Pattern a)
valPat :: Maybe (Pattern a), Declaration a -> Maybe (Expression a)
_valExpression :: Maybe (Expression a) }
                   | StaVal [Universal a] String (Type a)
                   | PrVal { Declaration a -> [Universal a]
valUniversals :: [Universal a], Declaration a -> Pattern a
prvalPat :: Pattern a, Declaration a -> Maybe (StaticExpression a)
_prValExpr :: Maybe (StaticExpression a), Declaration a -> Maybe (Type a)
prValType :: Maybe (Type a) }
                   | PrVar { Declaration a -> Pattern a
prvarPat :: Pattern a, Declaration a -> Maybe (StaticExpression a)
_prVarExpr :: Maybe (StaticExpression a), Declaration a -> Maybe (Type a)
prVarType :: Maybe (Type a) }
                   | Var { Declaration a -> Maybe (Type a)
varT :: Maybe (Type a), Declaration a -> Pattern a
varPat :: Pattern a, Declaration a -> Maybe (Expression a)
_varExpr1 :: Maybe (Expression a), Declaration a -> Maybe (Expression a)
_varExpr2 :: Maybe (Expression a) }
                   | AndDecl { Declaration a -> Maybe (Type a)
andT :: Maybe (Type a), Declaration a -> Pattern a
andPat :: Pattern a, Declaration a -> Expression a
_andExpr :: Expression a }
                   | Include String
                   | Load { Declaration a -> Bool
static :: Bool, Declaration a -> Bool
withOctothorpe :: Bool, Declaration a -> Maybe String
qualName :: Maybe String, Declaration a -> String
fileName :: String }
                   | Stadef String (SortArgs a) (Either (StaticExpression a, Maybe (Sort a)) (Maybe (Type a), Type a))
                   | CBlock String
                   | TypeDef a String (SortArgs a) (Type a) (Maybe (Sort a))
                   | ViewTypeDef a String (SortArgs a) (Type a)
                   | SumType { Declaration a -> String
typeName :: String, Declaration a -> SortArgs a
typeArgs :: SortArgs a, Declaration a -> NonEmpty (Leaf a)
_leaves :: NonEmpty (Leaf a) }
                   | SumViewType { typeName :: String, typeArgs :: SortArgs a, _leaves :: NonEmpty (Leaf a) }
                   | AbsType a String (SortArgs a) (Maybe (Type a))
                   | AbsViewType a String (SortArgs a) (Maybe (Type a))
                   | AbsView a String (SortArgs a) (Maybe (Type a))
                   | AbsVT0p a String (SortArgs a) (Maybe (Type a))
                   | AbsT0p a String (SortArgs a) (Maybe (Type a))
                   | ViewDef a String (SortArgs a) (Type a)
                   | OverloadOp a (BinOp a) (Name a) (Maybe Int)
                   | OverloadIdent a String (Name a) (Maybe Int)
                   | Comment { Declaration a -> String
_comment :: String }
                   | DataProp { pos :: a, Declaration a -> String
propName :: String, Declaration a -> SortArgs a
propArgs :: SortArgs a, Declaration a -> [DataPropLeaf a]
_propLeaves :: [DataPropLeaf a] }
                   | DataView a String (SortArgs a) (NonEmpty (Leaf a))
                   | Extern a (Declaration a)
                   | Define String
                   | SortDef a String (Either (Sort a) (Universal a))
                   | AndD (Declaration a) (Declaration a)
                   | Local a (ATS a) (ATS a)
                   | AbsProp a String [Arg a]
                   | Assume (Name a) (SortArgs a) (Type a)
                   | TKind a (Name a) String
                   | SymIntr a [Name a]
                   | Stacst a (Name a) (Type a) (Maybe (StaticExpression a))
                   | PropDef a String (Args a) (Type a)
                   | FixityDecl (Fixity a) [String]
                   | MacDecl a String (Maybe [String]) (Expression a)
                   | DataSort a String (NonEmpty (DataSortLeaf a))
                   | Exception String (Type a)
                   | ExtVar a String (Expression a)
                   | AbsImpl a (Name a) (SortArgs a) (Type a)
                   deriving (Int -> Declaration a -> ShowS
[Declaration a] -> ShowS
Declaration a -> String
(Int -> Declaration a -> ShowS)
-> (Declaration a -> String)
-> ([Declaration a] -> ShowS)
-> Show (Declaration a)
forall a. Show a => Int -> Declaration a -> ShowS
forall a. Show a => [Declaration a] -> ShowS
forall a. Show a => Declaration a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Declaration a] -> ShowS
$cshowList :: forall a. Show a => [Declaration a] -> ShowS
show :: Declaration a -> String
$cshow :: forall a. Show a => Declaration a -> String
showsPrec :: Int -> Declaration a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Declaration a -> ShowS
Show, Declaration a -> Declaration a -> Bool
(Declaration a -> Declaration a -> Bool)
-> (Declaration a -> Declaration a -> Bool) -> Eq (Declaration a)
forall a. Eq a => Declaration a -> Declaration a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Declaration a -> Declaration a -> Bool
$c/= :: forall a. Eq a => Declaration a -> Declaration a -> Bool
== :: Declaration a -> Declaration a -> Bool
$c== :: forall a. Eq a => Declaration a -> Declaration a -> Bool
Eq, (forall x. Declaration a -> Rep (Declaration a) x)
-> (forall x. Rep (Declaration a) x -> Declaration a)
-> Generic (Declaration a)
forall x. Rep (Declaration a) x -> Declaration a
forall x. Declaration a -> Rep (Declaration a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Declaration a) x -> Declaration a
forall a x. Declaration a -> Rep (Declaration a) x
$cto :: forall a x. Rep (Declaration a) x -> Declaration a
$cfrom :: forall a x. Declaration a -> Rep (Declaration a) x
Generic, Declaration a -> ()
(Declaration a -> ()) -> NFData (Declaration a)
forall a. NFData a => Declaration a -> ()
forall a. (a -> ()) -> NFData a
rnf :: Declaration a -> ()
$crnf :: forall a. NFData a => Declaration a -> ()
NFData)

data DataSortLeaf a = DataSortLeaf [Universal a] (Sort a) (Maybe (Sort a))
                    deriving (Int -> DataSortLeaf a -> ShowS
[DataSortLeaf a] -> ShowS
DataSortLeaf a -> String
(Int -> DataSortLeaf a -> ShowS)
-> (DataSortLeaf a -> String)
-> ([DataSortLeaf a] -> ShowS)
-> Show (DataSortLeaf a)
forall a. Show a => Int -> DataSortLeaf a -> ShowS
forall a. Show a => [DataSortLeaf a] -> ShowS
forall a. Show a => DataSortLeaf a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DataSortLeaf a] -> ShowS
$cshowList :: forall a. Show a => [DataSortLeaf a] -> ShowS
show :: DataSortLeaf a -> String
$cshow :: forall a. Show a => DataSortLeaf a -> String
showsPrec :: Int -> DataSortLeaf a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> DataSortLeaf a -> ShowS
Show, DataSortLeaf a -> DataSortLeaf a -> Bool
(DataSortLeaf a -> DataSortLeaf a -> Bool)
-> (DataSortLeaf a -> DataSortLeaf a -> Bool)
-> Eq (DataSortLeaf a)
forall a. Eq a => DataSortLeaf a -> DataSortLeaf a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DataSortLeaf a -> DataSortLeaf a -> Bool
$c/= :: forall a. Eq a => DataSortLeaf a -> DataSortLeaf a -> Bool
== :: DataSortLeaf a -> DataSortLeaf a -> Bool
$c== :: forall a. Eq a => DataSortLeaf a -> DataSortLeaf a -> Bool
Eq, (forall x. DataSortLeaf a -> Rep (DataSortLeaf a) x)
-> (forall x. Rep (DataSortLeaf a) x -> DataSortLeaf a)
-> Generic (DataSortLeaf a)
forall x. Rep (DataSortLeaf a) x -> DataSortLeaf a
forall x. DataSortLeaf a -> Rep (DataSortLeaf a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (DataSortLeaf a) x -> DataSortLeaf a
forall a x. DataSortLeaf a -> Rep (DataSortLeaf a) x
$cto :: forall a x. Rep (DataSortLeaf a) x -> DataSortLeaf a
$cfrom :: forall a x. DataSortLeaf a -> Rep (DataSortLeaf a) x
Generic, DataSortLeaf a -> ()
(DataSortLeaf a -> ()) -> NFData (DataSortLeaf a)
forall a. NFData a => DataSortLeaf a -> ()
forall a. (a -> ()) -> NFData a
rnf :: DataSortLeaf a -> ()
$crnf :: forall a. NFData a => DataSortLeaf a -> ()
NFData)

data DataPropLeaf a = DataPropLeaf { DataPropLeaf a -> [Universal a]
propU :: [Universal a], DataPropLeaf a -> Expression a
_propExpr1 :: Expression a, DataPropLeaf a -> Maybe (Expression a)
_propExpr2 :: Maybe (Expression a) }
                    deriving (Int -> DataPropLeaf a -> ShowS
[DataPropLeaf a] -> ShowS
DataPropLeaf a -> String
(Int -> DataPropLeaf a -> ShowS)
-> (DataPropLeaf a -> String)
-> ([DataPropLeaf a] -> ShowS)
-> Show (DataPropLeaf a)
forall a. Show a => Int -> DataPropLeaf a -> ShowS
forall a. Show a => [DataPropLeaf a] -> ShowS
forall a. Show a => DataPropLeaf a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DataPropLeaf a] -> ShowS
$cshowList :: forall a. Show a => [DataPropLeaf a] -> ShowS
show :: DataPropLeaf a -> String
$cshow :: forall a. Show a => DataPropLeaf a -> String
showsPrec :: Int -> DataPropLeaf a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> DataPropLeaf a -> ShowS
Show, DataPropLeaf a -> DataPropLeaf a -> Bool
(DataPropLeaf a -> DataPropLeaf a -> Bool)
-> (DataPropLeaf a -> DataPropLeaf a -> Bool)
-> Eq (DataPropLeaf a)
forall a. Eq a => DataPropLeaf a -> DataPropLeaf a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DataPropLeaf a -> DataPropLeaf a -> Bool
$c/= :: forall a. Eq a => DataPropLeaf a -> DataPropLeaf a -> Bool
== :: DataPropLeaf a -> DataPropLeaf a -> Bool
$c== :: forall a. Eq a => DataPropLeaf a -> DataPropLeaf a -> Bool
Eq, (forall x. DataPropLeaf a -> Rep (DataPropLeaf a) x)
-> (forall x. Rep (DataPropLeaf a) x -> DataPropLeaf a)
-> Generic (DataPropLeaf a)
forall x. Rep (DataPropLeaf a) x -> DataPropLeaf a
forall x. DataPropLeaf a -> Rep (DataPropLeaf a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (DataPropLeaf a) x -> DataPropLeaf a
forall a x. DataPropLeaf a -> Rep (DataPropLeaf a) x
$cto :: forall a x. Rep (DataPropLeaf a) x -> DataPropLeaf a
$cfrom :: forall a x. DataPropLeaf a -> Rep (DataPropLeaf a) x
Generic, DataPropLeaf a -> ()
(DataPropLeaf a -> ()) -> NFData (DataPropLeaf a)
forall a. NFData a => DataPropLeaf a -> ()
forall a. (a -> ()) -> NFData a
rnf :: DataPropLeaf a -> ()
$crnf :: forall a. NFData a => DataPropLeaf a -> ()
NFData)

-- | A type for parsed ATS types
data Type a = Tuple a [Type a]
            | BoxTuple a (NonEmpty (Type a))
            | Named (Name a)
            | Ex (Existential a) (Maybe (Type a))
            | ForA (Universal a) (Type a)
            | Dependent { Type a -> Name a
_typeCall :: Name a, Type a -> [Type a]
_typeCallArgs :: [Type a] }
            | Unconsumed (Type a) -- @!a@
            | AsProof (Type a) (Maybe (Type a)) -- @a >> b@ If the second field is 'Nothing' this will print as @a >> _@.
            | FromVT (Type a) -- | @a?!@
            | MaybeVal (Type a) -- | @a?@
            | AtExpr a (Type a) (StaticExpression a)
            | ArrayType a (Type a) (StaticExpression a)
            | ProofType a (NonEmpty (Type a)) (NonEmpty (Type a)) -- Aka (prf | val)
            | ConcreteType (StaticExpression a)
            | RefType (Type a)
            | ViewType a (Type a)
            | FunctionType String (Type a) (Type a)
            | ImplicitType a
            | ViewLiteral Addendum
            | AnonymousRecord a (NonEmpty (String, Type a))
            | WhereType a (Type a) String (SortArgs a) (Type a)
            | AddrType a -- ^ @addr@
            deriving (Int -> Type a -> ShowS
[Type a] -> ShowS
Type a -> String
(Int -> Type a -> ShowS)
-> (Type a -> String) -> ([Type a] -> ShowS) -> Show (Type a)
forall a. Show a => Int -> Type a -> ShowS
forall a. Show a => [Type a] -> ShowS
forall a. Show a => Type a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Type a] -> ShowS
$cshowList :: forall a. Show a => [Type a] -> ShowS
show :: Type a -> String
$cshow :: forall a. Show a => Type a -> String
showsPrec :: Int -> Type a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Type a -> ShowS
Show, Type a -> Type a -> Bool
(Type a -> Type a -> Bool)
-> (Type a -> Type a -> Bool) -> Eq (Type a)
forall a. Eq a => Type a -> Type a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Type a -> Type a -> Bool
$c/= :: forall a. Eq a => Type a -> Type a -> Bool
== :: Type a -> Type a -> Bool
$c== :: forall a. Eq a => Type a -> Type a -> Bool
Eq, (forall x. Type a -> Rep (Type a) x)
-> (forall x. Rep (Type a) x -> Type a) -> Generic (Type a)
forall x. Rep (Type a) x -> Type a
forall x. Type a -> Rep (Type a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Type a) x -> Type a
forall a x. Type a -> Rep (Type a) x
$cto :: forall a x. Rep (Type a) x -> Type a
$cfrom :: forall a x. Type a -> Rep (Type a) x
Generic, Type a -> ()
(Type a -> ()) -> NFData (Type a)
forall a. NFData a => Type a -> ()
forall a. (a -> ()) -> NFData a
rnf :: Type a -> ()
$crnf :: forall a. NFData a => Type a -> ()
NFData, Functor (Base (Type a))
Functor (Base (Type a))
-> (Type a -> Base (Type a) (Type a)) -> Recursive (Type a)
Type a -> Base (Type a) (Type a)
forall a. Functor (Base (Type a))
forall t. Functor (Base t) -> (t -> Base t t) -> Recursive t
forall a. Type a -> Base (Type a) (Type a)
project :: Type a -> Base (Type a) (Type a)
$cproject :: forall a. Type a -> Base (Type a) (Type a)
$cp1Recursive :: forall a. Functor (Base (Type a))
Recursive)

data TypeF a x = TupleF a [x]
               | BoxTupleF a (NonEmpty x)
               | NamedF (Name a)
               | ExF (Existential a) (Maybe x)
               | ForAF (Universal a) x
               | DependentF (Name a) [x]
               | UnconsumedF x
               | AsProofF x (Maybe x)
               | FromVTF x
               | MaybeValF x
               | AtExprF a x (StaticExpression a)
               | ArrayTypeF a x (StaticExpression a)
               | ProofTypeF a (NonEmpty x) (NonEmpty x)
               | ConcreteTypeF (StaticExpression a)
               | RefTypeF x
               | ViewTypeF a x
               | FunctionTypeF String x x
               | ImplicitTypeF a
               | ViewLiteralF Addendum
               | AnonymousRecordF a (NonEmpty (String, x))
               | WhereTypeF a x String (SortArgs a) x
               | AddrTypeF a
               deriving (a -> TypeF a b -> TypeF a a
(a -> b) -> TypeF a a -> TypeF a b
(forall a b. (a -> b) -> TypeF a a -> TypeF a b)
-> (forall a b. a -> TypeF a b -> TypeF a a) -> Functor (TypeF a)
forall a b. a -> TypeF a b -> TypeF a a
forall a b. (a -> b) -> TypeF a a -> TypeF a b
forall a a b. a -> TypeF a b -> TypeF a a
forall a a b. (a -> b) -> TypeF a a -> TypeF a b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> TypeF a b -> TypeF a a
$c<$ :: forall a a b. a -> TypeF a b -> TypeF a a
fmap :: (a -> b) -> TypeF a a -> TypeF a b
$cfmap :: forall a a b. (a -> b) -> TypeF a a -> TypeF a b
Functor, (forall x. TypeF a x -> Rep (TypeF a x) x)
-> (forall x. Rep (TypeF a x) x -> TypeF a x)
-> Generic (TypeF a x)
forall x. Rep (TypeF a x) x -> TypeF a x
forall x. TypeF a x -> Rep (TypeF a x) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x x. Rep (TypeF a x) x -> TypeF a x
forall a x x. TypeF a x -> Rep (TypeF a x) x
$cto :: forall a x x. Rep (TypeF a x) x -> TypeF a x
$cfrom :: forall a x x. TypeF a x -> Rep (TypeF a x) x
Generic)

type instance Base (Type a) = TypeF a

-- | A type for @=>@, @=\<cloref1>@, etc.
data LambdaType a = Plain a
                  | Spear a -- | @=>>@
                  | ProofArrow a -- | @=/=>@
                  | ProofSpear a -- | @=/=>>@
                  | Full a String
                  deriving (Int -> LambdaType a -> ShowS
[LambdaType a] -> ShowS
LambdaType a -> String
(Int -> LambdaType a -> ShowS)
-> (LambdaType a -> String)
-> ([LambdaType a] -> ShowS)
-> Show (LambdaType a)
forall a. Show a => Int -> LambdaType a -> ShowS
forall a. Show a => [LambdaType a] -> ShowS
forall a. Show a => LambdaType a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [LambdaType a] -> ShowS
$cshowList :: forall a. Show a => [LambdaType a] -> ShowS
show :: LambdaType a -> String
$cshow :: forall a. Show a => LambdaType a -> String
showsPrec :: Int -> LambdaType a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> LambdaType a -> ShowS
Show, LambdaType a -> LambdaType a -> Bool
(LambdaType a -> LambdaType a -> Bool)
-> (LambdaType a -> LambdaType a -> Bool) -> Eq (LambdaType a)
forall a. Eq a => LambdaType a -> LambdaType a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LambdaType a -> LambdaType a -> Bool
$c/= :: forall a. Eq a => LambdaType a -> LambdaType a -> Bool
== :: LambdaType a -> LambdaType a -> Bool
$c== :: forall a. Eq a => LambdaType a -> LambdaType a -> Bool
Eq, (forall x. LambdaType a -> Rep (LambdaType a) x)
-> (forall x. Rep (LambdaType a) x -> LambdaType a)
-> Generic (LambdaType a)
forall x. Rep (LambdaType a) x -> LambdaType a
forall x. LambdaType a -> Rep (LambdaType a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (LambdaType a) x -> LambdaType a
forall a x. LambdaType a -> Rep (LambdaType a) x
$cto :: forall a x. Rep (LambdaType a) x -> LambdaType a
$cfrom :: forall a x. LambdaType a -> Rep (LambdaType a) x
Generic, LambdaType a -> ()
(LambdaType a -> ()) -> NFData (LambdaType a)
forall a. NFData a => LambdaType a -> ()
forall a. (a -> ()) -> NFData a
rnf :: LambdaType a -> ()
$crnf :: forall a. NFData a => LambdaType a -> ()
NFData)

data Name a = Unqualified String
            | Qualified a String String -- ^ A name can be qualified e.g. @$UN.unsafefn@
            | SpecialName a String -- ^ A name for builtin functions such as @$showtype@.
            | Functorial String String
            | FieldName a String String
            deriving (Int -> Name a -> ShowS
[Name a] -> ShowS
Name a -> String
(Int -> Name a -> ShowS)
-> (Name a -> String) -> ([Name a] -> ShowS) -> Show (Name a)
forall a. Show a => Int -> Name a -> ShowS
forall a. Show a => [Name a] -> ShowS
forall a. Show a => Name a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Name a] -> ShowS
$cshowList :: forall a. Show a => [Name a] -> ShowS
show :: Name a -> String
$cshow :: forall a. Show a => Name a -> String
showsPrec :: Int -> Name a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Name a -> ShowS
Show, Name a -> Name a -> Bool
(Name a -> Name a -> Bool)
-> (Name a -> Name a -> Bool) -> Eq (Name a)
forall a. Eq a => Name a -> Name a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Name a -> Name a -> Bool
$c/= :: forall a. Eq a => Name a -> Name a -> Bool
== :: Name a -> Name a -> Bool
$c== :: forall a. Eq a => Name a -> Name a -> Bool
Eq, (forall x. Name a -> Rep (Name a) x)
-> (forall x. Rep (Name a) x -> Name a) -> Generic (Name a)
forall x. Rep (Name a) x -> Name a
forall x. Name a -> Rep (Name a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Name a) x -> Name a
forall a x. Name a -> Rep (Name a) x
$cto :: forall a x. Rep (Name a) x -> Name a
$cfrom :: forall a x. Name a -> Rep (Name a) x
Generic, Name a -> ()
(Name a -> ()) -> NFData (Name a)
forall a. NFData a => Name a -> ()
forall a. (a -> ()) -> NFData a
rnf :: Name a -> ()
$crnf :: forall a. NFData a => Name a -> ()
NFData)

-- | A data type for patterns.
data Pattern a = PName (Name a) [Pattern a]
               | PSum String (Pattern a)
               | PLiteral (Expression a)
               | Guarded a (Expression a) (Pattern a)
               | Free (Pattern a)
               | Proof a [Pattern a] [Pattern a]
               | TuplePattern [Pattern a]
               | BoxTuplePattern a [Pattern a]
               | AtPattern a (Pattern a)
               | UniversalPattern a String [Universal a] (Maybe (Pattern a))
               | ExistentialPattern (Existential a) (Pattern a)
               | As a (Pattern a) (Pattern a)
               | BinPattern a (BinOp a) (Pattern a) (Pattern a) -- ^ For use with e.g. @::@.
               deriving (Int -> Pattern a -> ShowS
[Pattern a] -> ShowS
Pattern a -> String
(Int -> Pattern a -> ShowS)
-> (Pattern a -> String)
-> ([Pattern a] -> ShowS)
-> Show (Pattern a)
forall a. Show a => Int -> Pattern a -> ShowS
forall a. Show a => [Pattern a] -> ShowS
forall a. Show a => Pattern a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Pattern a] -> ShowS
$cshowList :: forall a. Show a => [Pattern a] -> ShowS
show :: Pattern a -> String
$cshow :: forall a. Show a => Pattern a -> String
showsPrec :: Int -> Pattern a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Pattern a -> ShowS
Show, Pattern a -> Pattern a -> Bool
(Pattern a -> Pattern a -> Bool)
-> (Pattern a -> Pattern a -> Bool) -> Eq (Pattern a)
forall a. Eq a => Pattern a -> Pattern a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Pattern a -> Pattern a -> Bool
$c/= :: forall a. Eq a => Pattern a -> Pattern a -> Bool
== :: Pattern a -> Pattern a -> Bool
$c== :: forall a. Eq a => Pattern a -> Pattern a -> Bool
Eq, (forall x. Pattern a -> Rep (Pattern a) x)
-> (forall x. Rep (Pattern a) x -> Pattern a)
-> Generic (Pattern a)
forall x. Rep (Pattern a) x -> Pattern a
forall x. Pattern a -> Rep (Pattern a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Pattern a) x -> Pattern a
forall a x. Pattern a -> Rep (Pattern a) x
$cto :: forall a x. Rep (Pattern a) x -> Pattern a
$cfrom :: forall a x. Pattern a -> Rep (Pattern a) x
Generic, Pattern a -> ()
(Pattern a -> ()) -> NFData (Pattern a)
forall a. NFData a => Pattern a -> ()
forall a. (a -> ()) -> NFData a
rnf :: Pattern a -> ()
$crnf :: forall a. NFData a => Pattern a -> ()
NFData, Functor (Base (Pattern a))
Functor (Base (Pattern a))
-> (Pattern a -> Base (Pattern a) (Pattern a))
-> Recursive (Pattern a)
Pattern a -> Base (Pattern a) (Pattern a)
forall a. Functor (Base (Pattern a))
forall t. Functor (Base t) -> (t -> Base t t) -> Recursive t
forall a. Pattern a -> Base (Pattern a) (Pattern a)
project :: Pattern a -> Base (Pattern a) (Pattern a)
$cproject :: forall a. Pattern a -> Base (Pattern a) (Pattern a)
$cp1Recursive :: forall a. Functor (Base (Pattern a))
Recursive)

data PatternF a x = PNameF (Name a) [x]
                  | PSumF String x
                  | PLiteralF (Expression a)
                  | GuardedF a (Expression a) x
                  | FreeF x
                  | ProofF a [x] [x]
                  | TuplePatternF [x]
                  | BoxTuplePatternF a [x]
                  | AtPatternF a x
                  | UniversalPatternF a String [Universal a] (Maybe x)
                  | ExistentialPatternF (Existential a) x
                  | AsF a x x
                  | BinPatternF a (BinOp a) x x
                  deriving (a -> PatternF a b -> PatternF a a
(a -> b) -> PatternF a a -> PatternF a b
(forall a b. (a -> b) -> PatternF a a -> PatternF a b)
-> (forall a b. a -> PatternF a b -> PatternF a a)
-> Functor (PatternF a)
forall a b. a -> PatternF a b -> PatternF a a
forall a b. (a -> b) -> PatternF a a -> PatternF a b
forall a a b. a -> PatternF a b -> PatternF a a
forall a a b. (a -> b) -> PatternF a a -> PatternF a b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> PatternF a b -> PatternF a a
$c<$ :: forall a a b. a -> PatternF a b -> PatternF a a
fmap :: (a -> b) -> PatternF a a -> PatternF a b
$cfmap :: forall a a b. (a -> b) -> PatternF a a -> PatternF a b
Functor, (forall x. PatternF a x -> Rep (PatternF a x) x)
-> (forall x. Rep (PatternF a x) x -> PatternF a x)
-> Generic (PatternF a x)
forall x. Rep (PatternF a x) x -> PatternF a x
forall x. PatternF a x -> Rep (PatternF a x) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x x. Rep (PatternF a x) x -> PatternF a x
forall a x x. PatternF a x -> Rep (PatternF a x) x
$cto :: forall a x x. Rep (PatternF a x) x -> PatternF a x
$cfrom :: forall a x x. PatternF a x -> Rep (PatternF a x) x
Generic)

type instance Base (Pattern a) = PatternF a

data SortArg a = SortArg String (Sort a)
               | Anonymous (Sort a)
    deriving (Int -> SortArg a -> ShowS
[SortArg a] -> ShowS
SortArg a -> String
(Int -> SortArg a -> ShowS)
-> (SortArg a -> String)
-> ([SortArg a] -> ShowS)
-> Show (SortArg a)
forall a. Show a => Int -> SortArg a -> ShowS
forall a. Show a => [SortArg a] -> ShowS
forall a. Show a => SortArg a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SortArg a] -> ShowS
$cshowList :: forall a. Show a => [SortArg a] -> ShowS
show :: SortArg a -> String
$cshow :: forall a. Show a => SortArg a -> String
showsPrec :: Int -> SortArg a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> SortArg a -> ShowS
Show, SortArg a -> SortArg a -> Bool
(SortArg a -> SortArg a -> Bool)
-> (SortArg a -> SortArg a -> Bool) -> Eq (SortArg a)
forall a. Eq a => SortArg a -> SortArg a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SortArg a -> SortArg a -> Bool
$c/= :: forall a. Eq a => SortArg a -> SortArg a -> Bool
== :: SortArg a -> SortArg a -> Bool
$c== :: forall a. Eq a => SortArg a -> SortArg a -> Bool
Eq, (forall x. SortArg a -> Rep (SortArg a) x)
-> (forall x. Rep (SortArg a) x -> SortArg a)
-> Generic (SortArg a)
forall x. Rep (SortArg a) x -> SortArg a
forall x. SortArg a -> Rep (SortArg a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (SortArg a) x -> SortArg a
forall a x. SortArg a -> Rep (SortArg a) x
$cto :: forall a x. Rep (SortArg a) x -> SortArg a
$cfrom :: forall a x. SortArg a -> Rep (SortArg a) x
Generic, SortArg a -> ()
(SortArg a -> ()) -> NFData (SortArg a)
forall a. NFData a => SortArg a -> ()
forall a. (a -> ()) -> NFData a
rnf :: SortArg a -> ()
$crnf :: forall a. NFData a => SortArg a -> ()
NFData)

-- | An argument to a function.
data Arg a = Arg (These String (Type a))
           | PrfArg [Arg a] (Arg a)
           deriving (Int -> Arg a -> ShowS
[Arg a] -> ShowS
Arg a -> String
(Int -> Arg a -> ShowS)
-> (Arg a -> String) -> ([Arg a] -> ShowS) -> Show (Arg a)
forall a. Show a => Int -> Arg a -> ShowS
forall a. Show a => [Arg a] -> ShowS
forall a. Show a => Arg a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Arg a] -> ShowS
$cshowList :: forall a. Show a => [Arg a] -> ShowS
show :: Arg a -> String
$cshow :: forall a. Show a => Arg a -> String
showsPrec :: Int -> Arg a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Arg a -> ShowS
Show, Arg a -> Arg a -> Bool
(Arg a -> Arg a -> Bool) -> (Arg a -> Arg a -> Bool) -> Eq (Arg a)
forall a. Eq a => Arg a -> Arg a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Arg a -> Arg a -> Bool
$c/= :: forall a. Eq a => Arg a -> Arg a -> Bool
== :: Arg a -> Arg a -> Bool
$c== :: forall a. Eq a => Arg a -> Arg a -> Bool
Eq, (forall x. Arg a -> Rep (Arg a) x)
-> (forall x. Rep (Arg a) x -> Arg a) -> Generic (Arg a)
forall x. Rep (Arg a) x -> Arg a
forall x. Arg a -> Rep (Arg a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Arg a) x -> Arg a
forall a x. Arg a -> Rep (Arg a) x
$cto :: forall a x. Rep (Arg a) x -> Arg a
$cfrom :: forall a x. Arg a -> Rep (Arg a) x
Generic, Arg a -> ()
(Arg a -> ()) -> NFData (Arg a)
forall a. NFData a => Arg a -> ()
forall a. (a -> ()) -> NFData a
rnf :: Arg a -> ()
$crnf :: forall a. NFData a => Arg a -> ()
NFData)

-- | A datatype for sorts.
data Sort a = NamedSort { Sort a -> String
_sortName :: String }
            | T0p Addendum -- ^ @t\@ype@
            | Vt0p Addendum -- ^ @vt\@ype@
            | Addr
            | VType a Addendum -- ^ @viewtype@ or @vtype@
            | View a Addendum -- ^ @view@
            | TupleSort a (Sort a) (Sort a)
            | ArrowSort a (Sort a) (Sort a)
            deriving (Int -> Sort a -> ShowS
[Sort a] -> ShowS
Sort a -> String
(Int -> Sort a -> ShowS)
-> (Sort a -> String) -> ([Sort a] -> ShowS) -> Show (Sort a)
forall a. Show a => Int -> Sort a -> ShowS
forall a. Show a => [Sort a] -> ShowS
forall a. Show a => Sort a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Sort a] -> ShowS
$cshowList :: forall a. Show a => [Sort a] -> ShowS
show :: Sort a -> String
$cshow :: forall a. Show a => Sort a -> String
showsPrec :: Int -> Sort a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Sort a -> ShowS
Show, Sort a -> Sort a -> Bool
(Sort a -> Sort a -> Bool)
-> (Sort a -> Sort a -> Bool) -> Eq (Sort a)
forall a. Eq a => Sort a -> Sort a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Sort a -> Sort a -> Bool
$c/= :: forall a. Eq a => Sort a -> Sort a -> Bool
== :: Sort a -> Sort a -> Bool
$c== :: forall a. Eq a => Sort a -> Sort a -> Bool
Eq, (forall x. Sort a -> Rep (Sort a) x)
-> (forall x. Rep (Sort a) x -> Sort a) -> Generic (Sort a)
forall x. Rep (Sort a) x -> Sort a
forall x. Sort a -> Rep (Sort a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Sort a) x -> Sort a
forall a x. Sort a -> Rep (Sort a) x
$cto :: forall a x. Rep (Sort a) x -> Sort a
$cfrom :: forall a x. Sort a -> Rep (Sort a) x
Generic, Sort a -> ()
(Sort a -> ()) -> NFData (Sort a)
forall a. NFData a => Sort a -> ()
forall a. (a -> ()) -> NFData a
rnf :: Sort a -> ()
$crnf :: forall a. NFData a => Sort a -> ()
NFData, Functor (Base (Sort a))
Functor (Base (Sort a))
-> (Sort a -> Base (Sort a) (Sort a)) -> Recursive (Sort a)
Sort a -> Base (Sort a) (Sort a)
forall a. Functor (Base (Sort a))
forall t. Functor (Base t) -> (t -> Base t t) -> Recursive t
forall a. Sort a -> Base (Sort a) (Sort a)
project :: Sort a -> Base (Sort a) (Sort a)
$cproject :: forall a. Sort a -> Base (Sort a) (Sort a)
$cp1Recursive :: forall a. Functor (Base (Sort a))
Recursive)

data SortF a x = NamedSortF String
               | T0pF Addendum
               | Vt0pF Addendum
               | AddrF
               | VTypeF a Addendum
               | ViewF a Addendum
               | TupleSortF a x x
               | ArrowSortF a x x
               deriving (a -> SortF a b -> SortF a a
(a -> b) -> SortF a a -> SortF a b
(forall a b. (a -> b) -> SortF a a -> SortF a b)
-> (forall a b. a -> SortF a b -> SortF a a) -> Functor (SortF a)
forall a b. a -> SortF a b -> SortF a a
forall a b. (a -> b) -> SortF a a -> SortF a b
forall a a b. a -> SortF a b -> SortF a a
forall a a b. (a -> b) -> SortF a a -> SortF a b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> SortF a b -> SortF a a
$c<$ :: forall a a b. a -> SortF a b -> SortF a a
fmap :: (a -> b) -> SortF a a -> SortF a b
$cfmap :: forall a a b. (a -> b) -> SortF a a -> SortF a b
Functor, (forall x. SortF a x -> Rep (SortF a x) x)
-> (forall x. Rep (SortF a x) x -> SortF a x)
-> Generic (SortF a x)
forall x. Rep (SortF a x) x -> SortF a x
forall x. SortF a x -> Rep (SortF a x) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x x. Rep (SortF a x) x -> SortF a x
forall a x x. SortF a x -> Rep (SortF a x) x
$cto :: forall a x x. Rep (SortF a x) x -> SortF a x
$cfrom :: forall a x x. SortF a x -> Rep (SortF a x) x
Generic)

type instance Base (Sort a) = SortF a

-- | Wrapper for universal quantifiers (refinement types)
data Universal a = Universal { Universal a -> [String]
bound :: [String], Universal a -> Maybe (Sort a)
typeU :: Maybe (Sort a), Universal a -> [StaticExpression a]
prop :: [StaticExpression a] }
    deriving (Int -> Universal a -> ShowS
[Universal a] -> ShowS
Universal a -> String
(Int -> Universal a -> ShowS)
-> (Universal a -> String)
-> ([Universal a] -> ShowS)
-> Show (Universal a)
forall a. Show a => Int -> Universal a -> ShowS
forall a. Show a => [Universal a] -> ShowS
forall a. Show a => Universal a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Universal a] -> ShowS
$cshowList :: forall a. Show a => [Universal a] -> ShowS
show :: Universal a -> String
$cshow :: forall a. Show a => Universal a -> String
showsPrec :: Int -> Universal a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Universal a -> ShowS
Show, Universal a -> Universal a -> Bool
(Universal a -> Universal a -> Bool)
-> (Universal a -> Universal a -> Bool) -> Eq (Universal a)
forall a. Eq a => Universal a -> Universal a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Universal a -> Universal a -> Bool
$c/= :: forall a. Eq a => Universal a -> Universal a -> Bool
== :: Universal a -> Universal a -> Bool
$c== :: forall a. Eq a => Universal a -> Universal a -> Bool
Eq, (forall x. Universal a -> Rep (Universal a) x)
-> (forall x. Rep (Universal a) x -> Universal a)
-> Generic (Universal a)
forall x. Rep (Universal a) x -> Universal a
forall x. Universal a -> Rep (Universal a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Universal a) x -> Universal a
forall a x. Universal a -> Rep (Universal a) x
$cto :: forall a x. Rep (Universal a) x -> Universal a
$cfrom :: forall a x. Universal a -> Rep (Universal a) x
Generic, Universal a -> ()
(Universal a -> ()) -> NFData (Universal a)
forall a. NFData a => Universal a -> ()
forall a. (a -> ()) -> NFData a
rnf :: Universal a -> ()
$crnf :: forall a. NFData a => Universal a -> ()
NFData)

-- | Wrapper for existential quantifiers/types
data Existential a = Existential { Existential a -> [String]
boundE :: [String], Existential a -> Bool
isOpen :: Bool, Existential a -> Maybe (Sort a)
typeE :: Maybe (Sort a), Existential a -> Maybe (StaticExpression a)
propE :: Maybe (StaticExpression a) }
    deriving (Int -> Existential a -> ShowS
[Existential a] -> ShowS
Existential a -> String
(Int -> Existential a -> ShowS)
-> (Existential a -> String)
-> ([Existential a] -> ShowS)
-> Show (Existential a)
forall a. Show a => Int -> Existential a -> ShowS
forall a. Show a => [Existential a] -> ShowS
forall a. Show a => Existential a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Existential a] -> ShowS
$cshowList :: forall a. Show a => [Existential a] -> ShowS
show :: Existential a -> String
$cshow :: forall a. Show a => Existential a -> String
showsPrec :: Int -> Existential a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Existential a -> ShowS
Show, Existential a -> Existential a -> Bool
(Existential a -> Existential a -> Bool)
-> (Existential a -> Existential a -> Bool) -> Eq (Existential a)
forall a. Eq a => Existential a -> Existential a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Existential a -> Existential a -> Bool
$c/= :: forall a. Eq a => Existential a -> Existential a -> Bool
== :: Existential a -> Existential a -> Bool
$c== :: forall a. Eq a => Existential a -> Existential a -> Bool
Eq, (forall x. Existential a -> Rep (Existential a) x)
-> (forall x. Rep (Existential a) x -> Existential a)
-> Generic (Existential a)
forall x. Rep (Existential a) x -> Existential a
forall x. Existential a -> Rep (Existential a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Existential a) x -> Existential a
forall a x. Existential a -> Rep (Existential a) x
$cto :: forall a x. Rep (Existential a) x -> Existential a
$cfrom :: forall a x. Existential a -> Rep (Existential a) x
Generic, Existential a -> ()
(Existential a -> ()) -> NFData (Existential a)
forall a. NFData a => Existential a -> ()
forall a. (a -> ()) -> NFData a
rnf :: Existential a -> ()
$crnf :: forall a. NFData a => Existential a -> ()
NFData)

-- | Unary operators
data UnOp a = Negate -- | @~@
            | Deref -- | @!@
            | SpecialOp a String
    deriving (Int -> UnOp a -> ShowS
[UnOp a] -> ShowS
UnOp a -> String
(Int -> UnOp a -> ShowS)
-> (UnOp a -> String) -> ([UnOp a] -> ShowS) -> Show (UnOp a)
forall a. Show a => Int -> UnOp a -> ShowS
forall a. Show a => [UnOp a] -> ShowS
forall a. Show a => UnOp a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [UnOp a] -> ShowS
$cshowList :: forall a. Show a => [UnOp a] -> ShowS
show :: UnOp a -> String
$cshow :: forall a. Show a => UnOp a -> String
showsPrec :: Int -> UnOp a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> UnOp a -> ShowS
Show, UnOp a -> UnOp a -> Bool
(UnOp a -> UnOp a -> Bool)
-> (UnOp a -> UnOp a -> Bool) -> Eq (UnOp a)
forall a. Eq a => UnOp a -> UnOp a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: UnOp a -> UnOp a -> Bool
$c/= :: forall a. Eq a => UnOp a -> UnOp a -> Bool
== :: UnOp a -> UnOp a -> Bool
$c== :: forall a. Eq a => UnOp a -> UnOp a -> Bool
Eq, (forall x. UnOp a -> Rep (UnOp a) x)
-> (forall x. Rep (UnOp a) x -> UnOp a) -> Generic (UnOp a)
forall x. Rep (UnOp a) x -> UnOp a
forall x. UnOp a -> Rep (UnOp a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (UnOp a) x -> UnOp a
forall a x. UnOp a -> Rep (UnOp a) x
$cto :: forall a x. Rep (UnOp a) x -> UnOp a
$cfrom :: forall a x. UnOp a -> Rep (UnOp a) x
Generic, UnOp a -> ()
(UnOp a -> ()) -> NFData (UnOp a)
forall a. NFData a => UnOp a -> ()
forall a. (a -> ()) -> NFData a
rnf :: UnOp a -> ()
$crnf :: forall a. NFData a => UnOp a -> ()
NFData)

-- | Binary operators on expressions
data BinOp a = Add
             | Mult
             | Div
             | Sub
             | GreaterThan
             | GreaterThanEq
             | LessThan
             | LessThanEq
             | Equal
             | LogicalAnd
             | LogicalOr
             | StaticEq
             | Mod
             | NotEq
             | Mutate -- ^ @:=@
             | At
             | SpearOp -- ^ @->@
             | LShift
             | RShift
             | SpecialInfix a String
             deriving (Int -> BinOp a -> ShowS
[BinOp a] -> ShowS
BinOp a -> String
(Int -> BinOp a -> ShowS)
-> (BinOp a -> String) -> ([BinOp a] -> ShowS) -> Show (BinOp a)
forall a. Show a => Int -> BinOp a -> ShowS
forall a. Show a => [BinOp a] -> ShowS
forall a. Show a => BinOp a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [BinOp a] -> ShowS
$cshowList :: forall a. Show a => [BinOp a] -> ShowS
show :: BinOp a -> String
$cshow :: forall a. Show a => BinOp a -> String
showsPrec :: Int -> BinOp a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> BinOp a -> ShowS
Show, BinOp a -> BinOp a -> Bool
(BinOp a -> BinOp a -> Bool)
-> (BinOp a -> BinOp a -> Bool) -> Eq (BinOp a)
forall a. Eq a => BinOp a -> BinOp a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: BinOp a -> BinOp a -> Bool
$c/= :: forall a. Eq a => BinOp a -> BinOp a -> Bool
== :: BinOp a -> BinOp a -> Bool
$c== :: forall a. Eq a => BinOp a -> BinOp a -> Bool
Eq, (forall x. BinOp a -> Rep (BinOp a) x)
-> (forall x. Rep (BinOp a) x -> BinOp a) -> Generic (BinOp a)
forall x. Rep (BinOp a) x -> BinOp a
forall x. BinOp a -> Rep (BinOp a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (BinOp a) x -> BinOp a
forall a x. BinOp a -> Rep (BinOp a) x
$cto :: forall a x. Rep (BinOp a) x -> BinOp a
$cfrom :: forall a x. BinOp a -> Rep (BinOp a) x
Generic, BinOp a -> ()
(BinOp a -> ()) -> NFData (BinOp a)
forall a. NFData a => BinOp a -> ()
forall a. (a -> ()) -> NFData a
rnf :: BinOp a -> ()
$crnf :: forall a. NFData a => BinOp a -> ()
NFData)

pattern Con :: a -> BinOp a
pattern $bCon :: a -> BinOp a
$mCon :: forall r a. BinOp a -> (a -> r) -> (Void# -> r) -> r
Con l = SpecialInfix l "::"

data StaticExpression a = StaticVal (Name a)
                        | StaticBinary (BinOp a) (StaticExpression a) (StaticExpression a)
                        | StaticInt Integer
                        | StaticHex String
                        | SPrecede (StaticExpression a) (StaticExpression a)
                        | SPrecedeList { StaticExpression a -> [StaticExpression a]
_sExprs :: [StaticExpression a] }
                        | StaticVoid a
                        | Sif { StaticExpression a -> StaticExpression a
scond :: StaticExpression a, StaticExpression a -> StaticExpression a
whenTrue :: StaticExpression a, StaticExpression a -> StaticExpression a
selseExpr :: StaticExpression a } -- Static if (for proofs)
                        | SCall (Name a) [[Type a]] [[Type a]] [StaticExpression a] (Maybe [Expression a])
                        | SUnary (UnOp a) (StaticExpression a)
                        | SLet a [Declaration a] (Maybe (StaticExpression a))
                        | SCase Addendum (StaticExpression a) [(Pattern a, LambdaType a, StaticExpression a)]
                        | SString String -- ^ @ext#@
                        | Witness a (StaticExpression a) (StaticExpression a) -- ^ @#[ m | () ]@
                        | ProofLambda a (LambdaType a) (Pattern a) (StaticExpression a)
                        | ProofLinearLambda a (LambdaType a) (Pattern a) (StaticExpression a)
                        | WhereStaExp (StaticExpression a) (ATS a)
                        | SParens (StaticExpression a)
                        deriving (Int -> StaticExpression a -> ShowS
[StaticExpression a] -> ShowS
StaticExpression a -> String
(Int -> StaticExpression a -> ShowS)
-> (StaticExpression a -> String)
-> ([StaticExpression a] -> ShowS)
-> Show (StaticExpression a)
forall a. Show a => Int -> StaticExpression a -> ShowS
forall a. Show a => [StaticExpression a] -> ShowS
forall a. Show a => StaticExpression a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [StaticExpression a] -> ShowS
$cshowList :: forall a. Show a => [StaticExpression a] -> ShowS
show :: StaticExpression a -> String
$cshow :: forall a. Show a => StaticExpression a -> String
showsPrec :: Int -> StaticExpression a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> StaticExpression a -> ShowS
Show, StaticExpression a -> StaticExpression a -> Bool
(StaticExpression a -> StaticExpression a -> Bool)
-> (StaticExpression a -> StaticExpression a -> Bool)
-> Eq (StaticExpression a)
forall a. Eq a => StaticExpression a -> StaticExpression a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: StaticExpression a -> StaticExpression a -> Bool
$c/= :: forall a. Eq a => StaticExpression a -> StaticExpression a -> Bool
== :: StaticExpression a -> StaticExpression a -> Bool
$c== :: forall a. Eq a => StaticExpression a -> StaticExpression a -> Bool
Eq, (forall x. StaticExpression a -> Rep (StaticExpression a) x)
-> (forall x. Rep (StaticExpression a) x -> StaticExpression a)
-> Generic (StaticExpression a)
forall x. Rep (StaticExpression a) x -> StaticExpression a
forall x. StaticExpression a -> Rep (StaticExpression a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (StaticExpression a) x -> StaticExpression a
forall a x. StaticExpression a -> Rep (StaticExpression a) x
$cto :: forall a x. Rep (StaticExpression a) x -> StaticExpression a
$cfrom :: forall a x. StaticExpression a -> Rep (StaticExpression a) x
Generic, StaticExpression a -> ()
(StaticExpression a -> ()) -> NFData (StaticExpression a)
forall a. NFData a => StaticExpression a -> ()
forall a. (a -> ()) -> NFData a
rnf :: StaticExpression a -> ()
$crnf :: forall a. NFData a => StaticExpression a -> ()
NFData, Functor (Base (StaticExpression a))
Functor (Base (StaticExpression a))
-> (StaticExpression a
    -> Base (StaticExpression a) (StaticExpression a))
-> Recursive (StaticExpression a)
StaticExpression a
-> Base (StaticExpression a) (StaticExpression a)
forall a. Functor (Base (StaticExpression a))
forall t. Functor (Base t) -> (t -> Base t t) -> Recursive t
forall a.
StaticExpression a
-> Base (StaticExpression a) (StaticExpression a)
project :: StaticExpression a
-> Base (StaticExpression a) (StaticExpression a)
$cproject :: forall a.
StaticExpression a
-> Base (StaticExpression a) (StaticExpression a)
$cp1Recursive :: forall a. Functor (Base (StaticExpression a))
Recursive, Functor (Base (StaticExpression a))
Functor (Base (StaticExpression a))
-> (Base (StaticExpression a) (StaticExpression a)
    -> StaticExpression a)
-> Corecursive (StaticExpression a)
Base (StaticExpression a) (StaticExpression a)
-> StaticExpression a
forall a. Functor (Base (StaticExpression a))
forall t. Functor (Base t) -> (Base t t -> t) -> Corecursive t
forall a.
Base (StaticExpression a) (StaticExpression a)
-> StaticExpression a
embed :: Base (StaticExpression a) (StaticExpression a)
-> StaticExpression a
$cembed :: forall a.
Base (StaticExpression a) (StaticExpression a)
-> StaticExpression a
$cp1Corecursive :: forall a. Functor (Base (StaticExpression a))
Corecursive)

data StaticExpressionF a x = StaticValF (Name a)
                           | StaticBinaryF (BinOp a) x x
                           | StaticIntF Integer
                           | StaticHexF String
                           | SPrecedeF x x
                           | SPrecedeListF [x]
                           | StaticVoidF a
                           | SifF x x x
                           | SCallF (Name a) [[Type a]] [[Type a]] [x] (Maybe [Expression a])
                           | SUnaryF (UnOp a) x
                           | SLetF a [Declaration a] (Maybe x)
                           | SCaseF Addendum x [(Pattern a, LambdaType a, x)]
                           | SStringF String
                           | WitnessF a x x
                           | ProofLambdaF a (LambdaType a) (Pattern a) x
                           | ProofLinearLambdaF a (LambdaType a) (Pattern a) x
                           | WhereStaExpF x (ATS a)
                           | SParensF x
                           deriving (a -> StaticExpressionF a b -> StaticExpressionF a a
(a -> b) -> StaticExpressionF a a -> StaticExpressionF a b
(forall a b.
 (a -> b) -> StaticExpressionF a a -> StaticExpressionF a b)
-> (forall a b.
    a -> StaticExpressionF a b -> StaticExpressionF a a)
-> Functor (StaticExpressionF a)
forall a b. a -> StaticExpressionF a b -> StaticExpressionF a a
forall a b.
(a -> b) -> StaticExpressionF a a -> StaticExpressionF a b
forall a a b. a -> StaticExpressionF a b -> StaticExpressionF a a
forall a a b.
(a -> b) -> StaticExpressionF a a -> StaticExpressionF a b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> StaticExpressionF a b -> StaticExpressionF a a
$c<$ :: forall a a b. a -> StaticExpressionF a b -> StaticExpressionF a a
fmap :: (a -> b) -> StaticExpressionF a a -> StaticExpressionF a b
$cfmap :: forall a a b.
(a -> b) -> StaticExpressionF a a -> StaticExpressionF a b
Functor, (forall x. StaticExpressionF a x -> Rep (StaticExpressionF a x) x)
-> (forall x.
    Rep (StaticExpressionF a x) x -> StaticExpressionF a x)
-> Generic (StaticExpressionF a x)
forall x. Rep (StaticExpressionF a x) x -> StaticExpressionF a x
forall x. StaticExpressionF a x -> Rep (StaticExpressionF a x) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x x.
Rep (StaticExpressionF a x) x -> StaticExpressionF a x
forall a x x.
StaticExpressionF a x -> Rep (StaticExpressionF a x) x
$cto :: forall a x x.
Rep (StaticExpressionF a x) x -> StaticExpressionF a x
$cfrom :: forall a x x.
StaticExpressionF a x -> Rep (StaticExpressionF a x) x
Generic)

type instance Base (StaticExpression a) = StaticExpressionF a

-- | A (possibly effectful) expression.
data Expression a = Let a (ATS a) (Maybe (Expression a))
                  | VoidLiteral a -- ^ The '()' literal representing inaction.
                  | Call { Expression a -> Name a
callName       :: Name a
                         , Expression a -> [[Type a]]
callImplicits  :: [[Type a]] -- ^ E.g. @some_function<a>@
                         , Expression a -> [[Type a]]
callUniversals :: [[Type a]] -- ^ E.g. @some_function{a}@
                         , Expression a -> Maybe [Expression a]
callProofs     :: Maybe [Expression a] -- ^ E.g. @pf@ in @call(pf | str)@.
                         , Expression a -> [Expression a]
callArgs       :: [Expression a] -- ^ The actual call arguments.
                         }
                  | NamedVal (Name a)
                  | ListLiteral a String (Type a) [Expression a]
                  | If { Expression a -> Expression a
cond     :: Expression a -- ^ Expression evaluating to a boolean value
                       , Expression a -> Expression a
whenTrue :: Expression a -- ^ Expression to be returned when true
                       , Expression a -> Maybe (Expression a)
elseExpr :: Maybe (Expression a) -- ^ Expression to be returned when false
                       }
                  | UintLit Natural -- ^ E.g. @1000u@
                  | FloatLit Float
                  | DoubleLit Double
                  | IntLit Integer
                  | HexLit String
                  | HexUintLit String
                  | UnderscoreLit a
                  | Lambda a (LambdaType a) (Pattern a) (Expression a) -- TODO: Fix
                  | LinearLambda a (LambdaType a) (Pattern a) (Expression a)
                  | Index a (Name a) (Expression a) -- ^ E.g. @array[0]@.
                  | Access a (Expression a) (Name a)
                  | StringLit String
                  | CharLit Char
                  | AddrAt a (Expression a)
                  | ViewAt a (Expression a)
                  | Binary (BinOp a) (Expression a) (Expression a)
                  | Unary (UnOp a) (Expression a)
                  | IfCase { Expression a -> a
posE   :: a
                           , Expression a -> [(Expression a, LambdaType a, Expression a)]
ifArms :: [(Expression a, LambdaType a, Expression a)] -- TODO I'm not sure @ifcase@ needs 'LambdaType'?
                           }
                  | Case { posE  :: a
                         , Expression a -> Addendum
kind  :: Addendum
                         , Expression a -> Expression a
val   :: Expression a
                         , Expression a -> [(Pattern a, LambdaType a, Expression a)]
_arms :: [(Pattern a, LambdaType a, Expression a)] -- ^ Each (('Pattern' a), ('Expression' a)) pair corresponds to a branch of the 'case' statement
                         }
                  | RecordValue a (NonEmpty (String, Expression a))
                  | BoxRecordValue a (NonEmpty (String, Expression a))
                  | Precede (Expression a) (Expression a)
                  | ProofExpr a (NonEmpty (Expression a)) (Expression a)
                  | TypeSignature (Expression a) (Type a)
                  | WhereExp (Expression a) (ATS a)
                  | TupleEx a (NonEmpty (Expression a))
                  | BoxTupleEx a (NonEmpty (Expression a))
                  | While a (Expression a) (Expression a)
                  | WhileStar a [Universal a] (StaticExpression a) [Arg a] (Expression a) (Expression a) (Args a) -- ^ A @while@ loop that is guaranteed to terminate.
                  | For a (Expression a) (Expression a)
                  | ForStar a [Universal a] (StaticExpression a) [Arg a] (Expression a) (Expression a) -- ^ A @for@ loop that is guaranteed to terminate.
                  | Actions (ATS a)
                  | Begin a (Expression a)
                  | BinList { Expression a -> BinOp a
_op :: BinOp a, Expression a -> [Expression a]
_exprs :: [Expression a] }
                  | PrecedeList { _exprs :: [Expression a] }
                  | FixAt a String (StackFunction a)
                  | LambdaAt a (StackFunction a)
                  | LinearLambdaAt a (StackFunction a)
                  | ParenExpr a (Expression a)
                  | CommentExpr String (Expression a)
                  | MacroVar a String
                  | ArrayLit a (Type a) (Maybe (StaticExpression a)) [Expression a]
                  deriving (Int -> Expression a -> ShowS
[Expression a] -> ShowS
Expression a -> String
(Int -> Expression a -> ShowS)
-> (Expression a -> String)
-> ([Expression a] -> ShowS)
-> Show (Expression a)
forall a. Show a => Int -> Expression a -> ShowS
forall a. Show a => [Expression a] -> ShowS
forall a. Show a => Expression a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Expression a] -> ShowS
$cshowList :: forall a. Show a => [Expression a] -> ShowS
show :: Expression a -> String
$cshow :: forall a. Show a => Expression a -> String
showsPrec :: Int -> Expression a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Expression a -> ShowS
Show, Expression a -> Expression a -> Bool
(Expression a -> Expression a -> Bool)
-> (Expression a -> Expression a -> Bool) -> Eq (Expression a)
forall a. Eq a => Expression a -> Expression a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Expression a -> Expression a -> Bool
$c/= :: forall a. Eq a => Expression a -> Expression a -> Bool
== :: Expression a -> Expression a -> Bool
$c== :: forall a. Eq a => Expression a -> Expression a -> Bool
Eq, (forall x. Expression a -> Rep (Expression a) x)
-> (forall x. Rep (Expression a) x -> Expression a)
-> Generic (Expression a)
forall x. Rep (Expression a) x -> Expression a
forall x. Expression a -> Rep (Expression a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Expression a) x -> Expression a
forall a x. Expression a -> Rep (Expression a) x
$cto :: forall a x. Rep (Expression a) x -> Expression a
$cfrom :: forall a x. Expression a -> Rep (Expression a) x
Generic, Expression a -> ()
(Expression a -> ()) -> NFData (Expression a)
forall a. NFData a => Expression a -> ()
forall a. (a -> ()) -> NFData a
rnf :: Expression a -> ()
$crnf :: forall a. NFData a => Expression a -> ()
NFData, Functor (Base (Expression a))
Functor (Base (Expression a))
-> (Expression a -> Base (Expression a) (Expression a))
-> Recursive (Expression a)
Expression a -> Base (Expression a) (Expression a)
forall a. Functor (Base (Expression a))
forall t. Functor (Base t) -> (t -> Base t t) -> Recursive t
forall a. Expression a -> Base (Expression a) (Expression a)
project :: Expression a -> Base (Expression a) (Expression a)
$cproject :: forall a. Expression a -> Base (Expression a) (Expression a)
$cp1Recursive :: forall a. Functor (Base (Expression a))
Recursive, Functor (Base (Expression a))
Functor (Base (Expression a))
-> (Base (Expression a) (Expression a) -> Expression a)
-> Corecursive (Expression a)
Base (Expression a) (Expression a) -> Expression a
forall a. Functor (Base (Expression a))
forall t. Functor (Base t) -> (Base t t -> t) -> Corecursive t
forall a. Base (Expression a) (Expression a) -> Expression a
embed :: Base (Expression a) (Expression a) -> Expression a
$cembed :: forall a. Base (Expression a) (Expression a) -> Expression a
$cp1Corecursive :: forall a. Functor (Base (Expression a))
Corecursive)

data ExpressionF a x = LetF a (ATS a) (Maybe x)
                     | VoidLiteralF a
                     | CallF (Name a) [[Type a]] [[Type a]] (Maybe [x]) [x]
                     | NamedValF (Name a)
                     | ListLiteralF a String (Type a) [x]
                     | IfF x x (Maybe x)
                     | UintLitF Natural
                     | FloatLitF Float
                     | DoubleLitF Double
                     | IntLitF Integer
                     | HexLitF String
                     | HexUintLitF String
                     | UnderscoreLitF a
                     | LambdaF a (LambdaType a) (Pattern a) x
                     | LinearLambdaF a (LambdaType a) (Pattern a) x
                     | IndexF a (Name a) x
                     | AccessF a x (Name a)
                     | StringLitF String
                     | CharLitF Char
                     | AddrAtF a x
                     | ViewAtF a x
                     | BinaryF (BinOp a) x x
                     | UnaryF (UnOp a) x
                     | IfCaseF a [(x, LambdaType a, x)]
                     | CaseF a Addendum x [(Pattern a, LambdaType a, x)]
                     | RecordValueF a (NonEmpty (String, x))
                     | BoxRecordValueF a (NonEmpty (String, x))
                     | PrecedeF x x
                     | ProofExprF a (NonEmpty x) x
                     | TypeSignatureF x (Type a)
                     | WhereExpF x (ATS a)
                     | TupleExF a (NonEmpty x)
                     | BoxTupleExF a (NonEmpty x)
                     | WhileF a x x
                     | WhileStarF a [Universal a] (StaticExpression a) [Arg a] x x (Args a)
                     | ForF a x x
                     | ForStarF a [Universal a] (StaticExpression a) [Arg a] x x
                     | ActionsF (ATS a)
                     | BeginF a x
                     | BinListF (BinOp a) [x]
                     | PrecedeListF [x]
                     | FixAtF a String (StackFunction a)
                     | LambdaAtF a (StackFunction a)
                     | LinearLambdaAtF a (StackFunction a)
                     | ParenExprF a x
                     | CommentExprF String x
                     | MacroVarF a String
                     | ArrayLitF a (Type a) (Maybe (StaticExpression a)) [x]
                     deriving ((forall x. ExpressionF a x -> Rep (ExpressionF a x) x)
-> (forall x. Rep (ExpressionF a x) x -> ExpressionF a x)
-> Generic (ExpressionF a x)
forall x. Rep (ExpressionF a x) x -> ExpressionF a x
forall x. ExpressionF a x -> Rep (ExpressionF a x) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x x. Rep (ExpressionF a x) x -> ExpressionF a x
forall a x x. ExpressionF a x -> Rep (ExpressionF a x) x
$cto :: forall a x x. Rep (ExpressionF a x) x -> ExpressionF a x
$cfrom :: forall a x x. ExpressionF a x -> Rep (ExpressionF a x) x
Generic, a -> ExpressionF a b -> ExpressionF a a
(a -> b) -> ExpressionF a a -> ExpressionF a b
(forall a b. (a -> b) -> ExpressionF a a -> ExpressionF a b)
-> (forall a b. a -> ExpressionF a b -> ExpressionF a a)
-> Functor (ExpressionF a)
forall a b. a -> ExpressionF a b -> ExpressionF a a
forall a b. (a -> b) -> ExpressionF a a -> ExpressionF a b
forall a a b. a -> ExpressionF a b -> ExpressionF a a
forall a a b. (a -> b) -> ExpressionF a a -> ExpressionF a b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> ExpressionF a b -> ExpressionF a a
$c<$ :: forall a a b. a -> ExpressionF a b -> ExpressionF a a
fmap :: (a -> b) -> ExpressionF a a -> ExpressionF a b
$cfmap :: forall a a b. (a -> b) -> ExpressionF a a -> ExpressionF a b
Functor)

type instance Base (Expression a) = (ExpressionF a)

-- | An 'implement' or 'primplmnt' declaration
data Implementation a = Implement { Implementation a -> a
pos            :: a
                                  , Implementation a -> [Universal a]
preUniversalsI :: [Universal a]
                                  , Implementation a -> [[Type a]]
implicits      :: [[Type a]] -- ^ Implicit arguments
                                  , Implementation a -> [Universal a]
universalsI    :: [Universal a] -- ^ Universal quantifiers
                                  , Implementation a -> Name a
nameI          :: Name a -- ^ ('Name' a) of the template being implemented
                                  , Implementation a -> Args a
iArgs          :: Args a -- ^ Arguments
                                  , Implementation a -> Either (StaticExpression a) (Expression a)
_iExpression   :: Either (StaticExpression a) (Expression a) -- ^ Expression (or static expression) holding the function body.
                                  }
    deriving (Int -> Implementation a -> ShowS
[Implementation a] -> ShowS
Implementation a -> String
(Int -> Implementation a -> ShowS)
-> (Implementation a -> String)
-> ([Implementation a] -> ShowS)
-> Show (Implementation a)
forall a. Show a => Int -> Implementation a -> ShowS
forall a. Show a => [Implementation a] -> ShowS
forall a. Show a => Implementation a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Implementation a] -> ShowS
$cshowList :: forall a. Show a => [Implementation a] -> ShowS
show :: Implementation a -> String
$cshow :: forall a. Show a => Implementation a -> String
showsPrec :: Int -> Implementation a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Implementation a -> ShowS
Show, Implementation a -> Implementation a -> Bool
(Implementation a -> Implementation a -> Bool)
-> (Implementation a -> Implementation a -> Bool)
-> Eq (Implementation a)
forall a. Eq a => Implementation a -> Implementation a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Implementation a -> Implementation a -> Bool
$c/= :: forall a. Eq a => Implementation a -> Implementation a -> Bool
== :: Implementation a -> Implementation a -> Bool
$c== :: forall a. Eq a => Implementation a -> Implementation a -> Bool
Eq, (forall x. Implementation a -> Rep (Implementation a) x)
-> (forall x. Rep (Implementation a) x -> Implementation a)
-> Generic (Implementation a)
forall x. Rep (Implementation a) x -> Implementation a
forall x. Implementation a -> Rep (Implementation a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Implementation a) x -> Implementation a
forall a x. Implementation a -> Rep (Implementation a) x
$cto :: forall a x. Rep (Implementation a) x -> Implementation a
$cfrom :: forall a x. Implementation a -> Rep (Implementation a) x
Generic, Implementation a -> ()
(Implementation a -> ()) -> NFData (Implementation a)
forall a. NFData a => Implementation a -> ()
forall a. (a -> ()) -> NFData a
rnf :: Implementation a -> ()
$crnf :: forall a. NFData a => Implementation a -> ()
NFData)

-- | A function declaration accounting for all keywords ATS uses to
-- define them.
data Function a = Fun { Function a -> PreFunction Expression a
_preF :: PreFunction Expression a }
                | Fn { _preF :: PreFunction Expression a }
                | Fnx { _preF :: PreFunction Expression a }
                | And { _preF :: PreFunction Expression a }
                | PrFun { Function a -> PreFunction StaticExpression a
_preStaF :: PreFunction StaticExpression a }
                | PrFn { _preStaF :: PreFunction StaticExpression a }
                | Praxi { _preStaF :: PreFunction StaticExpression a }
                | CastFn { _preF :: PreFunction Expression a }
                deriving (Int -> Function a -> ShowS
[Function a] -> ShowS
Function a -> String
(Int -> Function a -> ShowS)
-> (Function a -> String)
-> ([Function a] -> ShowS)
-> Show (Function a)
forall a. Show a => Int -> Function a -> ShowS
forall a. Show a => [Function a] -> ShowS
forall a. Show a => Function a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Function a] -> ShowS
$cshowList :: forall a. Show a => [Function a] -> ShowS
show :: Function a -> String
$cshow :: forall a. Show a => Function a -> String
showsPrec :: Int -> Function a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Function a -> ShowS
Show, Function a -> Function a -> Bool
(Function a -> Function a -> Bool)
-> (Function a -> Function a -> Bool) -> Eq (Function a)
forall a. Eq a => Function a -> Function a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Function a -> Function a -> Bool
$c/= :: forall a. Eq a => Function a -> Function a -> Bool
== :: Function a -> Function a -> Bool
$c== :: forall a. Eq a => Function a -> Function a -> Bool
Eq, (forall x. Function a -> Rep (Function a) x)
-> (forall x. Rep (Function a) x -> Function a)
-> Generic (Function a)
forall x. Rep (Function a) x -> Function a
forall x. Function a -> Rep (Function a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Function a) x -> Function a
forall a x. Function a -> Rep (Function a) x
$cto :: forall a x. Rep (Function a) x -> Function a
$cfrom :: forall a x. Function a -> Rep (Function a) x
Generic, Function a -> ()
(Function a -> ()) -> NFData (Function a)
forall a. NFData a => Function a -> ()
forall a. (a -> ()) -> NFData a
rnf :: Function a -> ()
$crnf :: forall a. NFData a => Function a -> ()
NFData)

-- | A type for stack-allocated functions. See
-- [here](http://ats-lang.sourceforge.net/DOCUMENT/ATS2TUTORIAL/HTML/c1267.html)
-- for more.
data StackFunction a = StackF { StackFunction a -> String
stSig        :: String
                              , StackFunction a -> [Arg a]
stArgs       :: [Arg a]
                              , StackFunction a -> Type a
stReturnType :: Type a
                              , StackFunction a -> Expression a
stExpression :: Expression a
                              }
                              deriving (Int -> StackFunction a -> ShowS
[StackFunction a] -> ShowS
StackFunction a -> String
(Int -> StackFunction a -> ShowS)
-> (StackFunction a -> String)
-> ([StackFunction a] -> ShowS)
-> Show (StackFunction a)
forall a. Show a => Int -> StackFunction a -> ShowS
forall a. Show a => [StackFunction a] -> ShowS
forall a. Show a => StackFunction a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [StackFunction a] -> ShowS
$cshowList :: forall a. Show a => [StackFunction a] -> ShowS
show :: StackFunction a -> String
$cshow :: forall a. Show a => StackFunction a -> String
showsPrec :: Int -> StackFunction a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> StackFunction a -> ShowS
Show, StackFunction a -> StackFunction a -> Bool
(StackFunction a -> StackFunction a -> Bool)
-> (StackFunction a -> StackFunction a -> Bool)
-> Eq (StackFunction a)
forall a. Eq a => StackFunction a -> StackFunction a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: StackFunction a -> StackFunction a -> Bool
$c/= :: forall a. Eq a => StackFunction a -> StackFunction a -> Bool
== :: StackFunction a -> StackFunction a -> Bool
$c== :: forall a. Eq a => StackFunction a -> StackFunction a -> Bool
Eq, (forall x. StackFunction a -> Rep (StackFunction a) x)
-> (forall x. Rep (StackFunction a) x -> StackFunction a)
-> Generic (StackFunction a)
forall x. Rep (StackFunction a) x -> StackFunction a
forall x. StackFunction a -> Rep (StackFunction a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (StackFunction a) x -> StackFunction a
forall a x. StackFunction a -> Rep (StackFunction a) x
$cto :: forall a x. Rep (StackFunction a) x -> StackFunction a
$cfrom :: forall a x. StackFunction a -> Rep (StackFunction a) x
Generic, StackFunction a -> ()
(StackFunction a -> ()) -> NFData (StackFunction a)
forall a. NFData a => StackFunction a -> ()
forall a. (a -> ()) -> NFData a
rnf :: StackFunction a -> ()
$crnf :: forall a. NFData a => StackFunction a -> ()
NFData)

data PreFunction ek a = PreF { PreFunction ek a -> Name a
fname         :: Name a -- ^ Function name
                             , PreFunction ek a -> Maybe String
sig           :: Maybe String -- ^ e.g. <> or \<!wrt>
                             , PreFunction ek a -> [Universal a]
preUniversals :: [Universal a] -- ^ Universal quantifiers making a function generic
                             , PreFunction ek a -> [Universal a]
universals    :: [Universal a] -- ^ (Universal a) quantifiers/refinement type
                             , PreFunction ek a -> Args a
args          :: Args a -- ^ Actual function arguments
                             , PreFunction ek a -> Maybe (Type a)
returnType    :: Maybe (Type a) -- ^ Return type
                             , PreFunction ek a -> Maybe (Maybe (StaticExpression a))
termetric     :: Maybe (Maybe (StaticExpression a)) -- ^ Optional termination metric, which may be empty
                             , PreFunction ek a -> Maybe (ek a)
_expression   :: Maybe (ek a) -- ^ Expression holding the actual function body (not present in static templates)
                             }
                             deriving (Int -> PreFunction ek a -> ShowS
[PreFunction ek a] -> ShowS
PreFunction ek a -> String
(Int -> PreFunction ek a -> ShowS)
-> (PreFunction ek a -> String)
-> ([PreFunction ek a] -> ShowS)
-> Show (PreFunction ek a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (ek :: * -> *) a.
(Show a, Show (ek a)) =>
Int -> PreFunction ek a -> ShowS
forall (ek :: * -> *) a.
(Show a, Show (ek a)) =>
[PreFunction ek a] -> ShowS
forall (ek :: * -> *) a.
(Show a, Show (ek a)) =>
PreFunction ek a -> String
showList :: [PreFunction ek a] -> ShowS
$cshowList :: forall (ek :: * -> *) a.
(Show a, Show (ek a)) =>
[PreFunction ek a] -> ShowS
show :: PreFunction ek a -> String
$cshow :: forall (ek :: * -> *) a.
(Show a, Show (ek a)) =>
PreFunction ek a -> String
showsPrec :: Int -> PreFunction ek a -> ShowS
$cshowsPrec :: forall (ek :: * -> *) a.
(Show a, Show (ek a)) =>
Int -> PreFunction ek a -> ShowS
Show, PreFunction ek a -> PreFunction ek a -> Bool
(PreFunction ek a -> PreFunction ek a -> Bool)
-> (PreFunction ek a -> PreFunction ek a -> Bool)
-> Eq (PreFunction ek a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (ek :: * -> *) a.
(Eq a, Eq (ek a)) =>
PreFunction ek a -> PreFunction ek a -> Bool
/= :: PreFunction ek a -> PreFunction ek a -> Bool
$c/= :: forall (ek :: * -> *) a.
(Eq a, Eq (ek a)) =>
PreFunction ek a -> PreFunction ek a -> Bool
== :: PreFunction ek a -> PreFunction ek a -> Bool
$c== :: forall (ek :: * -> *) a.
(Eq a, Eq (ek a)) =>
PreFunction ek a -> PreFunction ek a -> Bool
Eq, (forall x. PreFunction ek a -> Rep (PreFunction ek a) x)
-> (forall x. Rep (PreFunction ek a) x -> PreFunction ek a)
-> Generic (PreFunction ek a)
forall x. Rep (PreFunction ek a) x -> PreFunction ek a
forall x. PreFunction ek a -> Rep (PreFunction ek a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (ek :: * -> *) a x.
Rep (PreFunction ek a) x -> PreFunction ek a
forall (ek :: * -> *) a x.
PreFunction ek a -> Rep (PreFunction ek a) x
$cto :: forall (ek :: * -> *) a x.
Rep (PreFunction ek a) x -> PreFunction ek a
$cfrom :: forall (ek :: * -> *) a x.
PreFunction ek a -> Rep (PreFunction ek a) x
Generic, PreFunction ek a -> ()
(PreFunction ek a -> ()) -> NFData (PreFunction ek a)
forall a. (a -> ()) -> NFData a
forall (ek :: * -> *) a.
(NFData a, NFData (ek a)) =>
PreFunction ek a -> ()
rnf :: PreFunction ek a -> ()
$crnf :: forall (ek :: * -> *) a.
(NFData a, NFData (ek a)) =>
PreFunction ek a -> ()
NFData)

-- FIXME left vs. right shouldn't be treated the same
instance (Eq a) => Ord (Fixity a) where
    compare :: Fixity a -> Fixity a -> Ordering
compare = (Fix -> Fix -> Ordering)
-> (Fixity a -> Fix) -> Fixity a -> Fixity a -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
on Fix -> Fix -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Fixity a -> Fix
forall a. Fixity a -> Fix
ifix

type FixityState a = M.Map String (Fixity a)