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 (..)
, Leaf (..)
, StaticExpression (..)
, StaticExpressionF (..)
, rewriteATS
, rewriteDecl
, leaves
, constructorUniversals
) where
import Control.DeepSeq (NFData)
import Control.Lens
import Data.Functor.Foldable (ListF (Cons), ana, cata, embed, project)
import Data.Functor.Foldable.TH (makeBaseFunctor)
import Data.Maybe (isJust)
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 Leaf = Leaf { _constructorUniversals :: [Universal], name :: String, constructorArgs :: [String], maybeType :: Maybe Type }
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 { typeName :: String, typeArgs :: [Arg], _leaves :: [Leaf] }
| SumViewType { typeName :: String, typeArgs :: [Arg], _leaves :: [Leaf] }
| AbsType AlexPosn String [Arg] (Maybe Type)
| AbsViewType AlexPosn String [Arg] (Maybe Type)
| AbsView AlexPosn String [Arg] (Maybe Type)
| AbsVT0p AlexPosn String [Arg] (Maybe Type)
| AbsT0p AlexPosn String Type
| ViewDef AlexPosn String [Arg] Type
| OverloadOp AlexPosn BinOp Name
| OverloadIdent AlexPosn String 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
| SymIntr AlexPosn Name
| Stacst AlexPosn Name Type (Maybe Expression)
| PropDef AlexPosn String [Arg] Type
deriving (Show, Eq, Generic, NFData)
data DataPropLeaf = DataPropLeaf [Universal] Expression (Maybe Expression)
deriving (Show, Eq, Generic, NFData)
data Type = Bool
| Void
| String
| Char
| Int
| Nat
| Addr
| DependentInt StaticExpression
| DependentBool StaticExpression
| DepString StaticExpression
| Double
| Float
| Tuple AlexPosn [Type]
| Named Name
| 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
| ViewLiteral Addendum
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
| Unnamed AlexPosn
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]
| AtPattern AlexPosn 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
| NoArgs
deriving (Show, Eq, Generic, NFData)
data Universal = Universal { bound :: [Arg], typeU :: Maybe Type, prop :: Maybe StaticExpression }
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
| Mod
deriving (Show, Eq, Generic, NFData)
data StaticExpression = StaticVal Name
| StaticBinary BinOp StaticExpression StaticExpression
| StaticInt Int
| SPrecede StaticExpression StaticExpression
| StaticBool Bool
| StaticVoid AlexPosn
| Sif { scond :: StaticExpression, wwhenTrue :: StaticExpression, selseExpr :: StaticExpression }
| SCall Name [StaticExpression]
deriving (Show, Eq, Generic, NFData)
data Expression = Let AlexPosn ATS (Maybe Expression)
| VoidLiteral
AlexPosn
| Call Name [Type] [Type] (Maybe Expression) [Expression]
| NamedVal Name
| ListLiteral AlexPosn String Type [Expression]
| If { cond :: Expression
, whenTrue :: Expression
, elseExpr :: Maybe 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
| AddrAt AlexPosn Expression
| ViewAt AlexPosn Expression
| Binary BinOp Expression Expression
| Unary UnOp Expression
| Case { posE :: AlexPosn
, kind :: Addendum
, val :: Expression
, arms :: [(Pattern, LambdaType, 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] }
| FixAt PreFunction
| LambdaAt PreFunction
| ParenExpr AlexPosn 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
| Fn PreFunction
| Fnx PreFunction
| And PreFunction
| PrFun PreFunction
| PrFn PreFunction
| Praxi PreFunction
| CastFn PreFunction
deriving (Show, Eq, Generic, NFData)
data PreFunction = PreF { fname :: Name
, sig :: String
, preUniversals :: [Universal]
, universals :: [Universal]
, args :: [Arg]
, returnType :: Type
, termetric :: Maybe StaticExpression
, expression :: Maybe Expression
}
deriving (Show, Eq, Generic, NFData)
makeBaseFunctor ''Pattern
makeBaseFunctor ''Expression
makeBaseFunctor ''StaticExpression
makeBaseFunctor ''Type
makeLenses ''Leaf
makeLenses ''Declaration
rewriteDecl :: Declaration -> Declaration
rewriteDecl x@SumViewType{} = g x
where g = over (leaves.mapped.constructorUniversals) h
h :: [Universal] -> [Universal]
h = ana c where
c (y:y':ys)
| typeU y == typeU y' && isJust (typeU y) =
Cons (Universal (bound y ++ bound y') (typeU y) (StaticBinary LogicalAnd <$> prop y <*> prop y')) ys
c y = project y
rewriteDecl x = x
rewriteATS :: Expression -> Expression
rewriteATS = cata a where
a (PrecedeF e e'@PrecedeList{}) = PrecedeList (e : _exprs e')
a (PrecedeF e e') = PrecedeList [e, e']
a (BinaryF Mult (Binary Add e e') e'') = Binary Add e (Binary Mult e' e'')
a (ParenExprF _ e@Precede{}) = e
a (ParenExprF _ e@PrecedeList{}) = e
a x = embed x