| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Language.ATS.Types
Description
This is a module containing types to model the ATS syntax tree. As it is collapsed by the pretty printer, you may see that in some places it is focused on the lexical side of things.
- newtype ATS = ATS {
- unATS :: [Declaration]
- 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
- 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]
- data Name
- data Pattern
- data PatternF r
- = WildcardF AlexPosn
- | PNameF String [r]
- | PSumF String r
- | PLiteralF Expression
- | GuardedF AlexPosn Expression r
- | FreeF r
- | ProofF AlexPosn r r
- | NullPatternF AlexPosn
- | TuplePatternF [r]
- data Arg = Arg String (Maybe Type)
- data Universal = Universal {}
- data Function
- data Expression
- = Let AlexPosn ATS Expression
- | Begin ATS
- | Local ATS
- | VoidLiteral AlexPosn
- | Call Name [Expression] [Type] [Expression]
- | NamedVal Name
- | If { }
- | Sif { }
- | 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
- data ExpressionF r
- = LetF AlexPosn ATS r
- | BeginF ATS
- | LocalF ATS
- | VoidLiteralF AlexPosn
- | CallF Name [r] [Type] [r]
- | NamedValF Name
- | IfF { }
- | SifF { }
- | BoolLitF Bool
- | TimeLitF String
- | FloatLitF Float
- | IntLitF Int
- | LambdaF AlexPosn LambdaType Pattern r
- | LinearLambdaF AlexPosn LambdaType Pattern r
- | IndexF AlexPosn Name r
- | AccessF AlexPosn r Name
- | StringLitF String
- | CharLitF Char
- | BinaryF BinOp r r
- | UnaryF UnOp r
- | CaseF { }
- | RecordValueF AlexPosn [(String, r)] (Maybe Type)
- | PrecedeF r r
- | FieldMutateF { }
- | DerefF AlexPosn r
- | RefF AlexPosn Type r
- | ProofExprF AlexPosn r r
- | TypeSignatureF r Type
- | WhereExpF r Declaration
- | TupleExF AlexPosn [r]
- | WhileF AlexPosn r r
- | ActionsF ATS
- data Implementation = Implement {
- pos :: AlexPosn
- preUniversalsI :: [Universal]
- universalsI :: [Universal]
- nameI :: Name
- iArgs :: [Arg]
- iExpression :: Expression
- data BinOp
- = Add
- | Mult
- | Div
- | Sub
- | GreaterThan
- | GreaterThanEq
- | LessThan
- | LessThanEq
- | Equal
- | NotEqual
- | LogicalAnd
- | LogicalOr
- data UnOp = Negate
- data TypeF r
- = BoolF
- | VoidF
- | StringF
- | CharF
- | IntF
- | NatF
- | DependentIntF Expression
- | DependentBoolF Expression
- | DepStringF Expression
- | DoubleF
- | FloatF
- | TupleF AlexPosn [r]
- | NamedF String
- | ExF Existential r
- | ForAF Universal r
- | DependentF Name [r]
- | UnconsumedF r
- | AsProofF r (Maybe r)
- | FromVTF r
- | MaybeValF r
- | T0pF Addendum
- | Vt0pF Addendum
- | AtF AlexPosn r r
- | ProofTypeF AlexPosn r r
- | ConcreteTypeF Expression
- | RefTypeF r
- | AbsPropF AlexPosn String [Arg]
- data Existential = Existential {}
- data LambdaType
- data Addendum
- data DataPropLeaf = DataPropLeaf [Universal] Expression
- data PreFunction = PreF {
- fname :: String
- preUniversals :: [Universal]
- universals :: [Universal]
- args :: [Arg]
- returnType :: Type
- termetric :: Maybe Expression
- expression :: Maybe Expression
Documentation
Newtype wrapper containing a list of declarations
Constructors
| ATS | |
Fields
| |
data Declaration Source #
Declare something in a scope (a function, value, action, etc.)
Constructors
Instances
A type for parsed ATS types
Constructors
A name can be qualified (`$UN.unsafefn`) or not
A data type for patterns.
Constructors
| WildcardF AlexPosn | |
| PNameF String [r] | |
| PSumF String r | |
| PLiteralF Expression | |
| GuardedF AlexPosn Expression r | |
| FreeF r | |
| ProofF AlexPosn r r | |
| NullPatternF AlexPosn | |
| TuplePatternF [r] |
An argument to a function.
Wrapper for universal quantifiers (refinement types)
A function declaration accounting for all three keywords (???) ATS uses to define them.
Constructors
| Fun PreFunction | |
| Fnx PreFunction | |
| And PreFunction | |
| PrFun PreFunction | |
| PrFn PreFunction | |
| Praxi PreFunction |
data Expression Source #
A (possibly effectful) expression.
Constructors
Instances
data ExpressionF r Source #
Constructors
| LetF AlexPosn ATS r | |
| BeginF ATS | |
| LocalF ATS | |
| VoidLiteralF AlexPosn | |
| CallF Name [r] [Type] [r] | |
| NamedValF Name | |
| IfF | |
| SifF | |
| BoolLitF Bool | |
| TimeLitF String | |
| FloatLitF Float | |
| IntLitF Int | |
| LambdaF AlexPosn LambdaType Pattern r | |
| LinearLambdaF AlexPosn LambdaType Pattern r | |
| IndexF AlexPosn Name r | |
| AccessF AlexPosn r Name | |
| StringLitF String | |
| CharLitF Char | |
| BinaryF BinOp r r | |
| UnaryF UnOp r | |
| CaseF | |
| RecordValueF AlexPosn [(String, r)] (Maybe Type) | |
| PrecedeF r r | |
| FieldMutateF | |
| DerefF AlexPosn r | |
| RefF AlexPosn Type r | |
| ProofExprF AlexPosn r r | |
| TypeSignatureF r Type | |
| WhereExpF r Declaration | |
| TupleExF AlexPosn [r] | |
| WhileF AlexPosn r r | |
| ActionsF ATS | |
Instances
data Implementation Source #
An implement declaration
Constructors
| Implement | |
Fields
| |
Instances
Binary operators on expressions
Constructors
| Add | |
| Mult | |
| Div | |
| Sub | |
| GreaterThan | |
| GreaterThanEq | |
| LessThan | |
| LessThanEq | |
| Equal | |
| NotEqual | |
| LogicalAnd | |
| LogicalOr |
`~` is used to negate numbers in ATS
Constructors
| Negate |
Constructors
data PreFunction Source #
Constructors
| PreF | |
Fields
| |
Instances