module Language.ATS.Types
( ATS (..)
, Declaration (..)
, Type (..)
, Name (..)
, Pattern (..)
, PatternF (..)
, Arg (..)
, Universal (..)
, Function (..)
, Expression (..)
, ExpressionF (..)
, Implementation (..)
, BinOp (..)
, UnOp (..)
, TypeF (..)
, Existential (..)
, LambdaType (..)
, Addendum (..)
, DataPropLeaf (..)
, PreFunction (..)
) where
import Control.DeepSeq (NFData)
import Data.Functor.Foldable.TH (makeBaseFunctor)
import GHC.Generics (Generic)
import Language.ATS.Lexer (Addendum (..), AlexPosn)
newtype ATS = ATS { unATS :: [Declaration] }
deriving (Show, Eq, Generic, NFData)
data Declaration = Func AlexPosn Function
| Impl Implementation
| ProofImpl Implementation
| Val Addendum (Maybe Type) Pattern Expression
| PrVal Pattern Expression
| Var (Maybe Type) Pattern Expression
| AndDecl (Maybe Type) Pattern Expression
| Include String
| Staload (Maybe String) String
| Stadef String Name
| CBlock String
| RecordType String [(String, Type)]
| RecordViewType String Type
| SumType String [(String, Maybe Type)]
| SumViewType String [(String, Maybe Type)]
| AbsViewType AlexPosn String [Arg] Type
| OverloadOp AlexPosn BinOp Name
| Comment String
| DataProp AlexPosn String [Arg] [DataPropLeaf]
| Extern AlexPosn Declaration
| Define String
deriving (Show, Eq, Generic, NFData)
data DataPropLeaf = DataPropLeaf [Universal] Expression
deriving (Show, Eq, Generic, NFData)
data Type = Bool
| Void
| String
| Char
| Int
| Nat
| DependentInt Expression
| DependentBool Expression
| DepString Expression
| Double
| Float
| Tuple AlexPosn [Type]
| Named String
| Ex Existential Type
| ForA Universal Type
| Dependent Name [Type]
| Unconsumed Type
| AsProof Type (Maybe Type)
| FromVT Type
| MaybeVal Type
| T0p Addendum
| Vt0p Addendum
| At AlexPosn Type Type
| ProofType AlexPosn Type Type
| ConcreteType Expression
| RefType Type
| AbsProp AlexPosn String [Arg]
deriving (Show, Eq, Generic, NFData)
data LambdaType = Plain AlexPosn
| Full AlexPosn String
deriving (Show, Eq, Generic, NFData)
data Name = Unqualified String
| Qualified AlexPosn String String
deriving (Show, Eq, Generic, NFData)
data Pattern = Wildcard AlexPosn
| PName String [Pattern]
| PSum String Pattern
| PLiteral Expression
| Guarded AlexPosn Expression Pattern
| Free Pattern
| Proof AlexPosn Pattern Pattern
| NullPattern AlexPosn
| TuplePattern [Pattern]
deriving (Show, Eq, Generic, NFData)
data Arg = Arg String (Maybe Type)
deriving (Show, Eq, Generic, NFData)
data Universal = Universal { bound :: [Arg], typeU :: Maybe Type, prop :: Maybe Expression }
deriving (Show, Eq, Generic, NFData)
data Existential = Existential { boundE :: [Arg], typeE :: Maybe Type, propE :: Maybe Expression }
deriving (Show, Eq, Generic, NFData)
data UnOp = Negate
deriving (Show, Eq, Generic, NFData)
data BinOp = Add
| Mult
| Div
| Sub
| GreaterThan
| GreaterThanEq
| LessThan
| LessThanEq
| Equal
| NotEqual
| LogicalAnd
| LogicalOr
deriving (Show, Eq, Generic, NFData)
data Expression = Let AlexPosn ATS Expression
| Begin ATS
| Local ATS
| VoidLiteral
AlexPosn
| Call Name [Expression] [Type] [Expression]
| NamedVal Name
| If { cond :: Expression
, whenTrue :: Expression
, elseExpr :: Expression
}
| Sif { cond :: Expression, whenTrue :: Expression, elseExpr :: Expression }
| BoolLit Bool
| TimeLit String
| FloatLit Float
| IntLit Int
| Lambda AlexPosn LambdaType Pattern Expression
| LinearLambda AlexPosn LambdaType Pattern Expression
| Index AlexPosn Name Expression
| Access AlexPosn Expression Name
| StringLit String
| CharLit Char
| Binary BinOp Expression Expression
| Unary UnOp Expression
| Case { posE :: AlexPosn
, kind :: Addendum
, val :: Expression
, arms :: [(Pattern, Expression)]
}
| RecordValue AlexPosn [(String, Expression)] (Maybe Type)
| Precede Expression Expression
| FieldMutate { posE :: AlexPosn
, old :: Expression
, field :: String
, new :: Expression
}
| Deref AlexPosn Expression
| Ref AlexPosn Type Expression
| ProofExpr AlexPosn Expression Expression
| TypeSignature Expression Type
| WhereExp Expression Declaration
| TupleEx AlexPosn [Expression]
| While AlexPosn Expression Expression
| Actions ATS
deriving (Show, Eq, Generic, NFData)
data Implementation = Implement { pos :: AlexPosn
, preUniversalsI :: [Universal]
, universalsI :: [Universal]
, nameI :: Name
, iArgs :: [Arg]
, iExpression :: Expression
}
deriving (Show, Eq, Generic, NFData)
data Function = Fun PreFunction
| Fnx PreFunction
| And PreFunction
| PrFun PreFunction
| PrFn PreFunction
| Praxi PreFunction
deriving (Show, Eq, Generic, NFData)
data PreFunction = PreF { fname :: String
, preUniversals :: [Universal]
, universals :: [Universal]
, args :: [Arg]
, returnType :: Type
, termetric :: Maybe Expression
, expression :: Maybe Expression
}
deriving (Show, Eq, Generic, NFData)
makeBaseFunctor ''Pattern
makeBaseFunctor ''Expression
makeBaseFunctor ''Type