Safe Haskell | None |
---|---|
Language | Haskell2010 |
Main module for the library
- lexATS :: String -> [Token]
- parseATS :: [Token] -> Either (ATSError String) ATS
- printATS :: ATS -> String
- printATSCustom :: Float -> Int -> ATS -> String
- printATSFast :: ATS -> String
- getDependencies :: ATS -> [FilePath]
- newtype ATS = ATS {
- unATS :: [Declaration]
- 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 { }
- | SumViewType { }
- | 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]
- data Expression
- = Let AlexPosn ATS (Maybe Expression)
- | VoidLiteral AlexPosn
- | Call Name [Type] [Type] (Maybe Expression) [Expression]
- | NamedVal Name
- | ListLiteral AlexPosn String Type [Expression]
- | If { }
- | 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
- 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)]
- data Function
- data Implementation = Implement {
- pos :: AlexPosn
- preUniversalsI :: [Universal]
- universalsI :: [Universal]
- nameI :: Name
- iArgs :: [Arg]
- iExpression :: Expression
- 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
- data Name
- data UnOp = Negate
- data BinOp
- = Add
- | Mult
- | Div
- | Sub
- | GreaterThan
- | GreaterThanEq
- | LessThan
- | LessThanEq
- | Equal
- | NotEqual
- | LogicalAnd
- | LogicalOr
- | StaticEq
- | Mod
- data DataPropLeaf = DataPropLeaf [Universal] Expression (Maybe Expression)
- data Leaf = Leaf {
- _constructorUniversals :: [Universal]
- name :: String
- constructorArgs :: [String]
- maybeType :: Maybe Type
- data Arg
- data Addendum
- data LambdaType
- data Universal = Universal {}
- data Existential = Existential {}
- data PreFunction = PreF {
- fname :: Name
- sig :: String
- preUniversals :: [Universal]
- universals :: [Universal]
- args :: [Arg]
- returnType :: Maybe Type
- termetric :: Maybe StaticExpression
- expression :: Maybe Expression
- data StaticExpression
- data Paired a b
- data Fixity
- data Token
- = Identifier AlexPosn String
- | Keyword AlexPosn Keyword
- | BoolTok AlexPosn Bool
- | 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
- | MacroBlock AlexPosn String
- | TimeTok AlexPosn String
- | SignatureTok AlexPosn String
- | DoubleParenTok AlexPosn
- | DoubleBracesTok AlexPosn
- | DoubleBracketTok AlexPosn
- | SpecialBracket AlexPosn
- | FixityTok AlexPosn String
- data AlexPosn = AlexPn !Int !Int !Int
- data Keyword
- = KwFun
- | KwFnx
- | KwAnd
- | KwDatatype
- | KwDatavtype
- | KwAssume
- | KwTypedef
- | KwVtypedef
- | KwStaload Bool
- | KwLet
- | KwIn
- | KwLocal
- | KwEnd
- | KwImplement
- | KwCase Addendum
- | KwIf
- | KwSif
- | KwThen
- | KwElse
- | KwString
- | KwBool
- | KwInt
- | KwVoid
- | KwNat
- | KwVal Addendum
- | KwVar
- | KwLambda
- | KwLinearLambda
- | KwInclude
- | KwWhen
- | KwOf
- | KwAbsprop
- | KwPrval
- | KwStadef
- | KwPraxi
- | KwWhile
- | KwWhere
- | KwBegin
- | KwOverload
- | KwWith
- | KwChar
- | KwDataview
- | KwDataprop
- | KwView Addendum
- | KwAbstype
- | KwType
- | KwAbst0p Addendum
- | KwAbsvt0p Addendum
- | KwT0p Addendum
- | KwVt0p Addendum
- | KwPrfun
- | KwPrfn
- | KwCastfn
- | KwExtern
- | KwAbsvtype
- | KwProofImplement
- | KwSortdef
- | KwPropdef
- | KwRaise
- | KwTKind
- | KwMod
- | KwFixAt
- | KwLambdaAt
- | KwAddrAt
- | KwAddr
- | KwSta
- | KwViewAt
- | KwViewdef
- | KwSymintr
- | KwAbsview
- | KwFn
- | KwInfix
- | KwInfixr
- | KwInfixl
- | KwStacst
- | KwListLit String
- data ATSError a
- leaves :: Traversal' Declaration [Leaf]
- constructorUniversals :: Lens' Leaf [Universal]
Functions for working with syntax
lexATS :: String -> [Token] Source #
This function turns a string into a stream of tokens for the parser.
printATSFast :: ATS -> String Source #
Fast pretty-printer without indendation. Useful for generating code.
Library functions
getDependencies :: ATS -> [FilePath] Source #
Syntax Tree
Newtype wrapper containing a list of declarations
ATS | |
|
data Declaration Source #
Declare something in a scope (a function, value, action, etc.)
data Expression Source #
A (possibly effectful) expression.
A type for parsed ATS types
A function declaration accounting for all three keywords (???) ATS uses to define them.
data Implementation Source #
An implement
declaration
Implement | |
|
A data type for patterns.
A name can be qualified ($UN.unsafefn
) or not
~
is used to negate numbers in ATS
Binary operators on expressions
data DataPropLeaf Source #
Leaf | |
|
An argument to a function.
Determines the default behavior for incomplete pattern matches
data LambdaType Source #
A type for the various lambda arrows (=>
, =<cloref1>
, etc.)
Wrapper for universal quantifiers (refinement types)
data Existential Source #
Wrapper for existential quantifiers/types
data PreFunction Source #
PreF | |
|
data StaticExpression Source #
Lexical types
Error types
Lenses
leaves :: Traversal' Declaration [Leaf] Source #