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 (..)
, Leaf (..)
, StaticExpression (..)
, StaticExpressionF (..)
, Fixity (..)
, StackFunction (..)
, 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 Data.Semigroup (Semigroup)
import GHC.Generics (Generic)
import Language.ATS.Lexer (Addendum (..), AlexPosn)
data Fixity = RightFix AlexPosn
| LeftFix AlexPosn
| Pre AlexPosn
| Post AlexPosn
deriving (Show, Eq, Generic, NFData)
newtype ATS = ATS { unATS :: [Declaration] }
deriving (Show, Eq, Generic)
deriving newtype (NFData, Semigroup, Monoid)
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
| StaVal [Universal] String Type
| PrVal Pattern Expression
| Var (Maybe Type) Pattern (Maybe Expression) (Maybe Expression)
| AndDecl (Maybe Type) Pattern Expression
| Include String
| Staload Bool (Maybe String) String
| Stadef String Name [Type]
| CBlock String
| 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 (Maybe Int)
| Comment String
| DataProp AlexPosn String [Arg] [DataPropLeaf]
| Extern AlexPosn Declaration
| Define String
| SortDef AlexPosn String Type
| AndD Declaration Declaration
| Local AlexPosn ATS ATS
| 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
| FixityDecl Fixity (Maybe Int) [String]
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 (Maybe Type) Type
| ProofType AlexPosn Type Type
| ConcreteType StaticExpression
| RefType Type
| ViewType AlexPosn Type
| FunctionType String Type Type
| NoneType AlexPosn
| ImplicitType AlexPosn
| ViewLiteral Addendum
| AnonymousRecord AlexPosn [(String, Type)]
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
| FieldName 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]
| TuplePattern [Pattern]
| AtPattern AlexPosn Pattern
| UniversalPattern AlexPosn String [Universal] Pattern
| ExistentialPattern Existential 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], isOpen :: Bool, typeE :: Maybe Type, propE :: Maybe StaticExpression }
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 String StackFunction
| LambdaAt StackFunction
| 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 StackFunction = StackF { stSig :: String
, stArgs :: [Arg]
, stReturnType :: Type
, stExpression :: Expression
}
deriving (Show, Eq, Generic, NFData)
data PreFunction = PreF { fname :: Name
, sig :: String
, preUniversals :: [Universal]
, universals :: [Universal]
, args :: [Arg]
, returnType :: Maybe 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 (CallF n ts ts' me [ParenExpr _ e@NamedVal{}]) = Call n ts ts' me [e]
a (CallF n ts ts' me [ParenExpr _ e@Call{}]) = Call n ts ts' me [e]
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 (BinaryF Add e (BinList Add es)) = BinList Add (e : es)
a (BinaryF Add e e') = BinList Add [e, e']
a (ParenExprF _ e@Precede{}) = e
a (ParenExprF _ e@PrecedeList{}) = e
a x = embed x