module Language.ATS.Types
( ATS (..)
, Declaration (..)
, Type (..)
, Name (..)
, Pattern (..)
, PatternF (..)
, Arg (..)
, Universal (..)
, Function (..)
, Expression (..)
, ExpressionF (..)
, Implementation (..)
, BinOp (..)
, UnOp (..)
, TypeF (..)
, Existential (..)
, LambdaType (..)
, Addendum (..)
, DataPropLeaf (..)
, PreFunction (..)
, Paired (..)
, Bifurcated (..)
, rewriteATS
) where
import Control.DeepSeq (NFData)
import Data.Functor.Foldable (cata, embed)
import Data.Functor.Foldable.TH (makeBaseFunctor)
import GHC.Generics (Generic)
import Language.ATS.Lexer (Addendum (..), AlexPosn)
data Bifurcated a = Nil
| Comma a (Bifurcated a)
| Bar a (Bifurcated a)
newtype ATS = ATS { unATS :: [Declaration] }
deriving (Show, Eq, Generic, NFData)
data Declaration = Func AlexPosn Function
| Impl [Arg] Implementation
| ProofImpl Implementation
| Val Addendum (Maybe Type) Pattern Expression
| PrVal Pattern Expression
| Var (Maybe Type) Pattern (Maybe Expression) (Maybe Expression)
| AndDecl (Maybe Type) Pattern Expression
| Include String
| Staload (Maybe String) String
| Stadef String Name [Type]
| CBlock String
| RecordType String [Arg] [Universal] [(String, Type)]
| RecordViewType String [Arg] [Universal] [(String, Type)]
| TypeDef AlexPosn String [Arg] Type
| ViewTypeDef AlexPosn String [Arg] Type
| SumType String [Arg] [(String, Maybe Type)]
| SumViewType String [Arg] [(String, Maybe Type)]
| AbsType AlexPosn String [Arg] Type
| AbsViewType AlexPosn String [Arg] Type
| OverloadOp AlexPosn BinOp Name
| Comment String
| DataProp AlexPosn String [Arg] [DataPropLeaf]
| Extern AlexPosn Declaration
| Define String
| SortDef AlexPosn String Type
| AndD Declaration Declaration
| Local AlexPosn [Declaration] [Declaration]
| AbsProp AlexPosn String [Arg]
| Assume Name [Arg] Expression
| TKind AlexPosn Name 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
| ViewType AlexPosn Type
| FunctionType String Type Type
| NoneType AlexPosn
| ImplicitType AlexPosn
deriving (Show, Eq, Generic, NFData)
data LambdaType = Plain AlexPosn
| Full AlexPosn String
| Spear AlexPosn
deriving (Show, Eq, Generic, NFData)
data Name = Unqualified String
| Qualified AlexPosn String String
| SpecialName AlexPosn String
| Functorial 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]
| TuplePattern [Pattern]
deriving (Show, Eq, Generic, NFData)
data Paired a b = Both a b
| First a
| Second b
deriving (Show, Eq, Generic, NFData)
data Arg = Arg (Paired String Type)
| PrfArg Arg Arg
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
| StaticEq
deriving (Show, Eq, Generic, NFData)
data Expression = Let AlexPosn ATS (Maybe Expression)
| VoidLiteral
AlexPosn
| Call Name [Type] [Type] (Maybe Expression) [Expression]
| NamedVal Name
| If { cond :: Expression
, whenTrue :: Expression
, elseExpr :: Maybe Expression
}
| Sif { cond :: Expression, whenTrue :: Expression, selseExpr :: Expression }
| BoolLit Bool
| TimeLit String
| FloatLit Float
| IntLit Int
| UnderscoreLit AlexPosn
| Lambda AlexPosn LambdaType Pattern Expression
| LinearLambda AlexPosn LambdaType Pattern Expression
| Index AlexPosn Name Expression
| Access AlexPosn Expression Name
| StringLit String
| CharLit Char
| AtExpr Expression Expression
| 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
}
| Mutate Expression Expression
| Deref AlexPosn Expression
| ProofExpr AlexPosn Expression Expression
| TypeSignature Expression Type
| WhereExp Expression [Declaration]
| TupleEx AlexPosn [Expression]
| While AlexPosn Expression Expression
| Actions ATS
| Begin AlexPosn Expression
| BinList { _op :: BinOp, _exprs :: [Expression] }
| PrecedeList { _exprs :: [Expression] }
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 :: Name
, sig :: 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
rewriteATS :: Expression -> Expression
rewriteATS = cata a where
a (PrecedeF e e'@PrecedeList{}) = PrecedeList (e : _exprs e')
a (PrecedeF e e') = PrecedeList [e, e']
a x = embed x