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 (..)
, Sort (..)
, SortArg (..)
, SortArgs
, DataSortLeaf (..)
, rewriteATS
, rewriteDecl
, preF
, expression
, fun
, leaves
, constructorUniversals
, typeCall
, typeCallArgs
, comment
) where
import Control.DeepSeq (NFData)
import Control.Lens
import Data.Function (on)
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 { pos :: AlexPosn, ifix :: Int }
| LeftFix { pos :: AlexPosn, ifix :: Int }
| Pre { pos :: AlexPosn, ifix :: Int }
| Post { pos :: AlexPosn, ifix :: Int }
| Infix { pos :: AlexPosn, ifix :: Int }
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 :: [StaticExpression], maybeType :: Maybe Type }
deriving (Show, Eq, Generic, NFData)
type SortArgs = Maybe [SortArg]
data Declaration = Func { pos :: AlexPosn, _fun :: Function }
| Impl [Arg] Implementation
| ProofImpl [Arg] 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 SortArgs Type
| CBlock String
| TypeDef AlexPosn String SortArgs Type
| ViewTypeDef AlexPosn String SortArgs Type
| SumType { typeName :: String, typeArgs :: SortArgs, _leaves :: [Leaf] }
| SumViewType { typeName :: String, typeArgs :: SortArgs, _leaves :: [Leaf] }
| AbsType AlexPosn String SortArgs (Maybe Type)
| AbsViewType AlexPosn String SortArgs (Maybe Type)
| AbsView AlexPosn String SortArgs (Maybe Type)
| AbsVT0p AlexPosn String SortArgs (Maybe Type)
| AbsT0p AlexPosn String SortArgs (Maybe Type)
| ViewDef AlexPosn String SortArgs Type
| OverloadOp AlexPosn BinOp Name (Maybe Int)
| OverloadIdent AlexPosn String Name (Maybe Int)
| Comment { _comment :: String }
| DataProp AlexPosn String SortArgs [DataPropLeaf]
| DataView AlexPosn String SortArgs [Leaf]
| Extern AlexPosn Declaration
| Define String
| SortDef AlexPosn String (Either Sort Universal)
| AndD Declaration Declaration
| Local AlexPosn ATS ATS
| AbsProp AlexPosn String [Arg]
| Assume Name [Arg] Type
| TKind AlexPosn Name String
| SymIntr AlexPosn Name
| Stacst AlexPosn Name Type (Maybe Expression)
| PropDef AlexPosn String [Arg] Type
| FixityDecl Fixity [String]
| MacDecl AlexPosn String [String] Expression
| DataSort AlexPosn String [DataSortLeaf]
| Exception String Type
| ExtVar AlexPosn String Expression
deriving (Show, Eq, Generic, NFData)
data DataSortLeaf = DataSortLeaf [Universal] Sort (Maybe Sort)
deriving (Show, Eq, Generic, NFData)
data DataPropLeaf = DataPropLeaf [Universal] Expression (Maybe Expression)
deriving (Show, Eq, Generic, NFData)
data Type = Tuple AlexPosn [Type]
| Named Name
| Ex Existential (Maybe Type)
| ForA Universal Type
| Dependent { _typeCall :: Name, _typeCallArgs :: [Type] }
| Unconsumed Type
| AsProof Type (Maybe Type)
| FromVT Type
| MaybeVal Type
| AtExpr AlexPosn Type StaticExpression
| AtType AlexPosn 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)]
| ParenType AlexPosn 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
| FieldName AlexPosn String String
| Unnamed AlexPosn
deriving (Show, Eq, Generic, NFData)
data Pattern = Wildcard AlexPosn
| PName Name [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 SortArg = SortArg String Sort
| Anonymous Sort
deriving (Show, Eq, Generic, NFData)
data Arg = Arg (Paired String Type)
| PrfArg Arg Arg
| NoArgs
deriving (Show, Eq, Generic, NFData)
data Sort = NamedSort { _sortName :: String }
| T0p Addendum
| Vt0p Addendum
| Addr
| VType AlexPosn Addendum
| View AlexPosn Addendum
deriving (Show, Eq, Generic, NFData)
data Universal = Universal { bound :: [String], typeU :: Maybe Sort, prop :: [StaticExpression] }
deriving (Show, Eq, Generic, NFData)
data Existential = Existential { boundE :: [String], isOpen :: Bool, typeE :: Maybe Sort, propE :: Maybe StaticExpression }
deriving (Show, Eq, Generic, NFData)
data UnOp = Negate
| Deref
| SpecialOp String
deriving (Show, Eq, Generic, NFData)
data BinOp = Add
| Mult
| Div
| Sub
| GreaterThan
| GreaterThanEq
| LessThan
| LessThanEq
| Equal
| NotEqual
| LogicalAnd
| LogicalOr
| StaticEq
| Mod
| NotEq
| Mutate
| At
| SpearOp
| SpecialInfix AlexPosn String
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]
| SUnary UnOp StaticExpression
| SLet AlexPosn [Declaration] (Maybe 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
| AddrAt AlexPosn Expression
| ViewAt AlexPosn Expression
| Binary BinOp Expression Expression
| Unary UnOp Expression
| IfCase { posE :: AlexPosn
, ifArms :: [(Expression, LambdaType, Expression)]
}
| Case { posE :: AlexPosn
, kind :: Addendum
, val :: Expression
, arms :: [(Pattern, LambdaType, Expression)]
}
| RecordValue AlexPosn [(String, Expression)] (Maybe Type)
| Precede Expression Expression
| ProofExpr AlexPosn Expression Expression
| TypeSignature Expression Type
| WhereExp Expression ATS
| 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
| CommentExpr String Expression
| MacroVar AlexPosn String
deriving (Show, Eq, Generic, NFData)
data Implementation = Implement { pos :: AlexPosn
, preUniversalsI :: [Universal]
, implicits :: [[Type]]
, universalsI :: [Universal]
, nameI :: Name
, iArgs :: [Arg]
, iExpression :: Either StaticExpression Expression
}
deriving (Show, Eq, Generic, NFData)
data Function = Fun { _preF :: PreFunction }
| Fn { _preF :: PreFunction }
| Fnx { _preF :: PreFunction }
| And { _preF :: PreFunction }
| PrFun { _preF :: PreFunction }
| PrFn { _preF :: PreFunction }
| Praxi { _preF :: PreFunction }
| CastFn { _preF :: 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
makeLenses ''PreFunction
makeLenses ''Function
makeLenses ''Type
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
instance Ord Fixity where
compare = on compare ifix
leftFix :: Int -> Fixity
leftFix = LeftFix undefined
rightFix :: Int -> Fixity
rightFix = RightFix undefined
infix_ :: Int -> Fixity
infix_ = Infix undefined
getFixity :: BinOp -> Fixity
getFixity Add = leftFix 50
getFixity Sub = leftFix 50
getFixity Mutate = infix_ 0
getFixity Mult = leftFix 60
getFixity Div = leftFix 60
getFixity SpearOp = rightFix 10
getFixity LogicalAnd = leftFix 21
getFixity LogicalOr = leftFix 20
getFixity At = rightFix 40
getFixity GreaterThan = infix_ 40
getFixity GreaterThanEq = infix_ 40
getFixity LessThanEq = infix_ 40
getFixity Equal = infix_ 30
getFixity NotEqual = infix_ 30
getFixity StaticEq = infix_ 30
getFixity Mod = leftFix 60
getFixity _ = leftFix 100
instance Ord BinOp where
compare = on compare getFixity
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 op' (Binary op'' e e') e'')
| op' > op'' = Binary op'' e (Binary op' 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