| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Language.ATS
Contents
Description
Main module for the library
- lexATS :: String -> Either String [Token]
- parse :: String -> Either ATSError (ATS AlexPosn)
- parseWithCtx :: FixityState AlexPosn -> ([Token] -> [Token]) -> String -> Either ATSError (ATS AlexPosn)
- parseM :: String -> Either ATSError (ATS AlexPosn)
- printATS :: Eq a => ATS a -> String
- printATSCustom :: Eq a => Float -> Int -> ATS a -> String
- printATSFast :: Eq a => ATS a -> String
- printErr :: MonadIO m => ATSError -> m ()
- warnErr :: MonadIO m => FilePath -> ATSError -> m ()
- defaultFixityState :: FixityState a
- getDependencies :: ATS a -> [FilePath]
- newtype ATS a = ATS {
- unATS :: [Declaration a]
- data Declaration a
- = Func { }
- | Impl {
- implArgs :: [Arg a]
- _impl :: Implementation a
- | ProofImpl {
- implArgs :: [Arg a]
- _impl :: Implementation a
- | Val {
- add :: Addendum
- valT :: Maybe (Type a)
- valPat :: Pattern a
- _valExpression :: Expression a
- | StaVal [Universal a] String (Type a)
- | PrVal {
- prvalPat :: Pattern a
- _prValExpr :: Maybe (Expression a)
- prValType :: Maybe (Type a)
- | Var { }
- | AndDecl { }
- | Include String
- | Load { }
- | Stadef String (SortArgs a) (Either (StaticExpression a) (Type a))
- | CBlock String
- | TypeDef a String (SortArgs a) (Type a)
- | ViewTypeDef a String (SortArgs a) (Type a)
- | SumType { }
- | SumViewType { }
- | AbsType a String (SortArgs a) (Maybe (Type a))
- | AbsViewType a String (SortArgs a) (Maybe (Type a))
- | AbsView a String (SortArgs a) (Maybe (Type a))
- | AbsVT0p a String (SortArgs a) (Maybe (Type a))
- | AbsT0p a String (SortArgs a) (Maybe (Type a))
- | ViewDef a String (SortArgs a) (Type a)
- | OverloadOp a (BinOp a) (Name a) (Maybe Int)
- | OverloadIdent a String (Name a) (Maybe Int)
- | Comment { }
- | DataProp {
- pos :: a
- propName :: String
- propArgs :: SortArgs a
- _propLeaves :: [DataPropLeaf a]
- | DataView a String (SortArgs a) [Leaf a]
- | Extern a (Declaration a)
- | Define String
- | SortDef a String (Either (Sort a) (Universal a))
- | AndD (Declaration a) (Declaration a)
- | Local a (ATS a) (ATS a)
- | AbsProp a String [Arg a]
- | Assume (Name a) [Arg a] (Type a)
- | TKind a (Name a) String
- | SymIntr a [Name a]
- | Stacst a (Name a) (Type a) (Maybe (Expression a))
- | PropDef a String [Arg a] (Type a)
- | FixityDecl (Fixity a) [String]
- | MacDecl a String [String] (Expression a)
- | DataSort a String [DataSortLeaf a]
- | Exception String (Type a)
- | ExtVar a String (Expression a)
- data Expression a
- = Let a (ATS a) (Maybe (Expression a))
- | VoidLiteral a
- | Call {
- callName :: Name a
- callImplicits :: [[Type a]]
- callUniversals :: [Type a]
- callProofs :: Maybe [Expression a]
- callArgs :: [Expression a]
- | NamedVal (Name a)
- | ListLiteral a String (Type a) [Expression a]
- | If {
- cond :: Expression a
- whenTrue :: Expression a
- elseExpr :: Maybe (Expression a)
- | UintLit Word
- | FloatLit Float
- | IntLit Int
- | UnderscoreLit a
- | Lambda a (LambdaType a) (Pattern a) (Expression a)
- | LinearLambda a (LambdaType a) (Pattern a) (Expression a)
- | Index a (Name a) (Expression a)
- | Access a (Expression a) (Name a)
- | StringLit String
- | CharLit Char
- | AddrAt a (Expression a)
- | ViewAt a (Expression a)
- | Binary (BinOp a) (Expression a) (Expression a)
- | Unary (UnOp a) (Expression a)
- | IfCase {
- posE :: a
- ifArms :: [(Expression a, LambdaType a, Expression a)]
- | Case {
- posE :: a
- kind :: Addendum
- val :: Expression a
- _arms :: [(Pattern a, LambdaType a, Expression a)]
- | RecordValue a [(String, Expression a)] (Maybe (Type a))
- | Precede (Expression a) (Expression a)
- | ProofExpr a (Expression a) (Expression a)
- | TypeSignature (Expression a) (Type a)
- | WhereExp (Expression a) (ATS a)
- | TupleEx a [Expression a]
- | While a (Expression a) (Expression a)
- | Actions (ATS a)
- | Begin a (Expression a)
- | BinList {
- _op :: BinOp a
- _exprs :: [Expression a]
- | PrecedeList {
- _exprs :: [Expression a]
- | FixAt a String (StackFunction a)
- | LambdaAt a (StackFunction a)
- | ParenExpr a (Expression a)
- | CommentExpr String (Expression a)
- | MacroVar a String
- data Type a
- = Tuple a [Type a]
- | Named (Name a)
- | Ex (Existential a) (Maybe (Type a))
- | ForA (Universal a) (Type a)
- | Dependent {
- _typeCall :: Name a
- _typeCallArgs :: [Type a]
- | Unconsumed (Type a)
- | AsProof (Type a) (Maybe (Type a))
- | FromVT (Type a)
- | MaybeVal (Type a)
- | AtExpr a (Type a) (StaticExpression a)
- | AtType a (Type a)
- | ProofType a [Type a] (Type a)
- | ConcreteType (StaticExpression a)
- | RefType (Type a)
- | ViewType a (Type a)
- | FunctionType String (Type a) (Type a)
- | NoneType a
- | ImplicitType a
- | ViewLiteral Addendum
- | AnonymousRecord a [(String, Type a)]
- | ParenType a (Type a)
- | WhereType a (Type a) String (SortArgs a) (Type a)
- data Function a
- = Fun {
- _preF :: PreFunction a
- | Fn {
- _preF :: PreFunction a
- | Fnx {
- _preF :: PreFunction a
- | And {
- _preF :: PreFunction a
- | PrFun {
- _preF :: PreFunction a
- | PrFn {
- _preF :: PreFunction a
- | Praxi {
- _preF :: PreFunction a
- | CastFn {
- _preF :: PreFunction a
- = Fun {
- data Implementation a = Implement {
- pos :: a
- preUniversalsI :: [Universal a]
- implicits :: [[Type a]]
- universalsI :: [Universal a]
- nameI :: Name a
- iArgs :: [Arg a]
- _iExpression :: Either (StaticExpression a) (Expression a)
- data Pattern a
- = Wildcard a
- | PName (Name a) [Pattern a]
- | PSum String (Pattern a)
- | PLiteral (Expression a)
- | Guarded a (Expression a) (Pattern a)
- | Free (Pattern a)
- | Proof a [Pattern a] [Pattern a]
- | TuplePattern [Pattern a]
- | AtPattern a (Pattern a)
- | UniversalPattern a String [Universal a] (Pattern a)
- | ExistentialPattern (Existential a) (Pattern a)
- data Name a
- data UnOp a
- data BinOp a
- = Add
- | Mult
- | Div
- | Sub
- | GreaterThan
- | GreaterThanEq
- | LessThan
- | LessThanEq
- | Equal
- | LogicalAnd
- | LogicalOr
- | StaticEq
- | Mod
- | NotEq
- | Mutate
- | At
- | SpearOp
- | SpecialInfix a String
- data DataPropLeaf a = DataPropLeaf {
- propU :: [Universal a]
- _propExpr1 :: Expression a
- _propExpr2 :: Maybe (Expression a)
- data Leaf a = Leaf {
- _constructorUniversals :: [Universal a]
- name :: String
- constructorArgs :: [StaticExpression a]
- maybeType :: Maybe (Type a)
- data DataSortLeaf a = DataSortLeaf [Universal a] (Sort a) (Maybe (Sort a))
- data Arg a
- data Addendum
- data LambdaType a
- data Universal a = Universal {}
- data Existential a = Existential {}
- data PreFunction a = PreF {
- fname :: Name a
- sig :: Maybe String
- preUniversals :: [Universal a]
- universals :: [Universal a]
- args :: [Arg a]
- returnType :: Maybe (Type a)
- termetric :: Maybe (StaticExpression a)
- _expression :: Maybe (Expression a)
- data StaticExpression a
- = StaticVal (Name a)
- | StaticBinary (BinOp a) (StaticExpression a) (StaticExpression a)
- | StaticInt Int
- | SPrecede (StaticExpression a) (StaticExpression a)
- | StaticVoid a
- | Sif {
- scond :: StaticExpression a
- wwhenTrue :: StaticExpression a
- selseExpr :: StaticExpression a
- | SCall (Name a) [StaticExpression a]
- | SUnary (UnOp a) (StaticExpression a)
- | SLet a [Declaration a] (Maybe (StaticExpression a))
- data StackFunction a = StackF {
- stSig :: String
- stArgs :: [Arg a]
- stReturnType :: Type a
- stExpression :: Expression a
- data Paired a b
- data Fixity a
- data SortArg a
- data Sort a
- type SortArgs a = Maybe [SortArg a]
- type FixityState a = Map String (Fixity a)
- data Token
- = Identifier AlexPosn String
- | SpecialIdentifier AlexPosn String
- | Keyword AlexPosn Keyword
- | IntTok AlexPosn Int
- | FloatTok AlexPosn Float
- | CharTok AlexPosn Char
- | StringTok AlexPosn String
- | Special AlexPosn String
- | CBlockLex AlexPosn String
- | IdentifierSpace AlexPosn String
- | Operator AlexPosn String
- | Arrow AlexPosn String
- | FuncType AlexPosn String
- | CommentLex AlexPosn String
- | CommentBegin AlexPosn
- | CommentEnd AlexPosn
- | CommentContents AlexPosn String
- | MacroBlock AlexPosn String
- | UintTok AlexPosn Word
- | SignatureTok AlexPosn String
- | DoubleParenTok AlexPosn
- | DoubleBracesTok AlexPosn
- | DoubleBracketTok AlexPosn
- | SpecialBracket AlexPosn
- | FixityTok AlexPosn String
- | End
- data AlexPosn = AlexPn !Int !Int !Int
- data Keyword
- = KwFun
- | KwFnx
- | KwAnd
- | KwDatatype
- | KwDatavtype
- | KwAssume
- | KwTypedef
- | KwVtypedef
- | KwVtype Addendum
- | KwStaload Bool
- | KwDynload Bool
- | KwLet
- | KwIn
- | KwLocal
- | KwEnd
- | KwImplement
- | KwCase Addendum
- | KwIf
- | KwSif
- | KwThen
- | KwElse
- | KwVal Addendum
- | KwVar
- | KwLambda
- | KwLinearLambda
- | KwInclude
- | KwWhen
- | KwOf
- | KwAbsprop
- | KwPrval
- | KwStadef
- | KwPraxi
- | KwWhile
- | KwWhere
- | KwBegin
- | KwOverload
- | KwWith
- | KwIfCase
- | KwDataview
- | KwDataprop
- | KwView Addendum
- | KwAbstype
- | KwType
- | KwAbst0p Addendum
- | KwAbsvt0p Addendum
- | KwT0p Addendum
- | KwVt0p Addendum
- | KwPrfun
- | KwPrfn
- | KwCastfn
- | KwExtern
- | KwAbsvtype
- | KwProofImplement
- | KwSortdef
- | KwExtVar
- | KwPropdef
- | KwRaise
- | KwTKind
- | KwMod
- | KwFixAt
- | KwLambdaAt
- | KwAddrAt
- | KwAddr
- | KwSta
- | KwViewAt
- | KwViewdef
- | KwSymintr
- | KwAbsview
- | KwFn
- | KwInfix
- | KwInfixr
- | KwInfixl
- | KwStacst
- | KwListLit String
- | KwMacdef
- | KwDatasort
- | KwException
- data ATSError
- preF :: forall a a. Lens (Function a) (Function a) (PreFunction a) (PreFunction a)
- expression :: forall a. Lens' (PreFunction a) (Maybe (Expression a))
- fun :: forall a. Traversal' (Declaration a) (Function a)
- leaves :: forall a. Traversal' (Declaration a) [Leaf a]
- constructorUniversals :: forall a. Lens' (Leaf a) [Universal a]
- typeCall :: forall a. Traversal' (Type a) (Name a)
- typeCallArgs :: forall a. Traversal' (Type a) [Type a]
Functions for working with syntax
lexATS :: String -> Either String [Token] Source #
This function turns a string into a stream of tokens for the parser.
parseWithCtx :: FixityState AlexPosn -> ([Token] -> [Token]) -> String -> Either ATSError (ATS AlexPosn) Source #
Parse with some fixity declarations already in scope.
parseM :: String -> Either ATSError (ATS AlexPosn) Source #
Parse a string containing ATS source, disregarding comments.
printATSFast :: Eq a => ATS a -> String Source #
Slightly faster pretty-printer without indendation (for code generation).
warnErr :: MonadIO m => FilePath -> ATSError -> m () Source #
Same as printErr, but print a yellow warning message instead.
Library functions
getDependencies :: ATS a -> [FilePath] Source #
Extract a list of files that some code depends on.
Syntax Tree
Newtype wrapper containing a list of declarations
Constructors
| ATS | |
Fields
| |
data Declaration a Source #
Declare something in a scope (a function, value, action, etc.)
Constructors
Instances
| Eq a => Eq (Declaration a) Source # | |
| Show a => Show (Declaration a) Source # | |
| Generic (Declaration a) Source # | |
| NFData a => NFData (Declaration a) Source # | |
| type Rep (Declaration a) Source # | |
data Expression a Source #
A (possibly effectful) expression.
Constructors
Instances
| Eq a => Eq (Expression a) Source # | |
| Show a => Show (Expression a) Source # | |
| Generic (Expression a) Source # | |
| NFData a => NFData (Expression a) Source # | |
| Recursive (Expression a) Source # | |
| Corecursive (Expression a) Source # | |
| type Rep (Expression a) Source # | |
| type Base (Expression a) Source # | |
A type for parsed ATS types
Constructors
| Tuple a [Type a] | |
| Named (Name a) | |
| Ex (Existential a) (Maybe (Type a)) | |
| ForA (Universal a) (Type a) | |
| Dependent | |
Fields
| |
| Unconsumed (Type a) | |
| AsProof (Type a) (Maybe (Type a)) | |
| FromVT (Type a) | |
| MaybeVal (Type a) | a?! |
| AtExpr a (Type a) (StaticExpression a) | a? |
| AtType a (Type a) | |
| ProofType a [Type a] (Type a) | |
| ConcreteType (StaticExpression a) | |
| RefType (Type a) | |
| ViewType a (Type a) | |
| FunctionType String (Type a) (Type a) | |
| NoneType a | |
| ImplicitType a | |
| ViewLiteral Addendum | |
| AnonymousRecord a [(String, Type a)] | |
| ParenType a (Type a) | |
| WhereType a (Type a) String (SortArgs a) (Type a) | |
A function declaration accounting for all keywords ATS uses to define them.
Constructors
| Fun | |
Fields
| |
| Fn | |
Fields
| |
| Fnx | |
Fields
| |
| And | |
Fields
| |
| PrFun | |
Fields
| |
| PrFn | |
Fields
| |
| Praxi | |
Fields
| |
| CastFn | |
Fields
| |
data Implementation a Source #
An implement or primplmnt declaration
Constructors
| Implement | |
Fields
| |
Instances
| Eq a => Eq (Implementation a) Source # | |
| Show a => Show (Implementation a) Source # | |
| Generic (Implementation a) Source # | |
| NFData a => NFData (Implementation a) Source # | |
| type Rep (Implementation a) Source # | |
A data type for patterns.
Constructors
| Wildcard a | |
| PName (Name a) [Pattern a] | |
| PSum String (Pattern a) | |
| PLiteral (Expression a) | |
| Guarded a (Expression a) (Pattern a) | |
| Free (Pattern a) | |
| Proof a [Pattern a] [Pattern a] | |
| TuplePattern [Pattern a] | |
| AtPattern a (Pattern a) | |
| UniversalPattern a String [Universal a] (Pattern a) | |
| ExistentialPattern (Existential a) (Pattern a) |
Constructors
| Unqualified String | |
| Qualified a String String | A name can be qualified e.g. |
| SpecialName a String | A name for builtin functions such as |
| Functorial String String | |
| FieldName a String String |
~ is used to negate numbers in ATS
Binary operators on expressions
Constructors
| Add | |
| Mult | |
| Div | |
| Sub | |
| GreaterThan | |
| GreaterThanEq | |
| LessThan | |
| LessThanEq | |
| Equal | |
| LogicalAnd | |
| LogicalOr | |
| StaticEq | |
| Mod | |
| NotEq | |
| Mutate | := |
| At | |
| SpearOp | -> |
| SpecialInfix a String |
data DataPropLeaf a Source #
Constructors
| DataPropLeaf | |
Fields
| |
Instances
| Eq a => Eq (DataPropLeaf a) Source # | |
| Show a => Show (DataPropLeaf a) Source # | |
| Generic (DataPropLeaf a) Source # | |
| NFData a => NFData (DataPropLeaf a) Source # | |
| type Rep (DataPropLeaf a) Source # | |
Constructors
| Leaf | |
Fields
| |
data DataSortLeaf a Source #
Constructors
| DataSortLeaf [Universal a] (Sort a) (Maybe (Sort a)) |
Instances
| Eq a => Eq (DataSortLeaf a) Source # | |
| Show a => Show (DataSortLeaf a) Source # | |
| Generic (DataSortLeaf a) Source # | |
| NFData a => NFData (DataSortLeaf a) Source # | |
| type Rep (DataSortLeaf a) Source # | |
An argument to a function.
Determines the default behavior for incomplete pattern matches
data LambdaType a Source #
A type for =>, =<cloref1>, etc.
Instances
| Eq a => Eq (LambdaType a) Source # | |
| Show a => Show (LambdaType a) Source # | |
| Generic (LambdaType a) Source # | |
| NFData a => NFData (LambdaType a) Source # | |
| type Rep (LambdaType a) Source # | |
Wrapper for universal quantifiers (refinement types)
data Existential a Source #
Wrapper for existential quantifiers/types
Constructors
| Existential | |
Instances
| Eq a => Eq (Existential a) Source # | |
| Show a => Show (Existential a) Source # | |
| Generic (Existential a) Source # | |
| NFData a => NFData (Existential a) Source # | |
| type Rep (Existential a) Source # | |
data PreFunction a Source #
Constructors
| PreF | |
Fields
| |
Instances
| Eq a => Eq (PreFunction a) Source # | |
| Show a => Show (PreFunction a) Source # | |
| Generic (PreFunction a) Source # | |
| NFData a => NFData (PreFunction a) Source # | |
| type Rep (PreFunction a) Source # | |
data StaticExpression a Source #
Constructors
| StaticVal (Name a) | |
| StaticBinary (BinOp a) (StaticExpression a) (StaticExpression a) | |
| StaticInt Int | |
| SPrecede (StaticExpression a) (StaticExpression a) | |
| StaticVoid a | |
| Sif | |
Fields
| |
| SCall (Name a) [StaticExpression a] | |
| SUnary (UnOp a) (StaticExpression a) | |
| SLet a [Declaration a] (Maybe (StaticExpression a)) | |
Instances
| Eq a => Eq (StaticExpression a) Source # | |
| Show a => Show (StaticExpression a) Source # | |
| Generic (StaticExpression a) Source # | |
| NFData a => NFData (StaticExpression a) Source # | |
| Recursive (StaticExpression a) Source # | |
| Corecursive (StaticExpression a) Source # | |
| type Rep (StaticExpression a) Source # | |
| type Base (StaticExpression a) Source # | |
data StackFunction a Source #
A type for stack-allocated functions. See here for more.
Constructors
| StackF | |
Fields
| |
Instances
| Eq a => Eq (StackFunction a) Source # | |
| Show a => Show (StackFunction a) Source # | |
| Generic (StackFunction a) Source # | |
| NFData a => NFData (StackFunction a) Source # | |
| type Rep (StackFunction a) Source # | |
A datatype for sorts.
Parser State
Lexical types
Constructors
Constructors
Error types
Lenses
preF :: forall a a. Lens (Function a) (Function a) (PreFunction a) (PreFunction a) Source #
expression :: forall a. Lens' (PreFunction a) (Maybe (Expression a)) Source #
fun :: forall a. Traversal' (Declaration a) (Function a) Source #
leaves :: forall a. Traversal' (Declaration a) [Leaf a] Source #
typeCallArgs :: forall a. Traversal' (Type a) [Type a] Source #