Language.ATS

Main module for the library

Functions

lexATS :: String -> [Token]

This function turns a string into a stream of tokens for the parser.

parseATS :: [Token] -> Either (ATSError String) ATS

printATS :: ATS -> String

Types

newtype ATS

Newtype wrapper containing a list of declarations

Constructors

ATS

Fields

• unATS :: [Declaration]

Instances

Eq ATS

Methods

(==) :: ATS -> ATS -> Bool

(/=) :: ATS -> ATS -> Bool

Show ATS

Methods

showsPrec :: Int -> ATS -> ShowS

show :: ATS -> String

showList :: [ATS] -> ShowS

Generic ATS

Associated Types

type Rep ATS :: * -> *

Methods

from :: ATS -> Rep ATS x

to :: Rep ATS x -> ATS

NFData ATS

Methods

rnf :: ATS -> ()

type Rep ATS

type Rep ATS = D1 * (MetaData "ATS" "Language.ATS.Types" "ats-format-0.1.0.4-8XxiRaaxvYz91MPkPCFYvZ" True) (C1 * (MetaCons "ATS" PrefixI True) (S1 * (MetaSel (Just Symbol "unATS") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [Declaration])))

data Declaration

Declare something in a scope (a function, value, action, etc.)

Constructors

Func AlexPosn Function

Impl [Arg] Implementation

ProofImpl Implementation

Val Addendum (Maybe Type) Pattern Expression

PrVal Pattern Expression

Var (Maybe Type) Pattern (Maybe Expression)

AndDecl (Maybe Type) Pattern Expression

Include String

Staload (Maybe String) String

Stadef String Name

CBlock String

RecordType String [Arg] [(String, Type)]

RecordViewType String [Arg] [(String, Type)]

TypeDef AlexPosn String [Arg] Type

ViewTypeDef AlexPosn String [Arg] Type

SumType String [Arg] [(String, Maybe Type)]

SumViewType String [Arg] [(String, Maybe Type)]

AbsType AlexPosn String [Arg] Type

AbsViewType AlexPosn String [Arg] Type

OverloadOp AlexPosn BinOp Name

Comment String

DataProp AlexPosn String [Arg] [DataPropLeaf]

Extern AlexPosn Declaration

Define String

SortDef AlexPosn String Type

AndD Declaration Declaration

Local AlexPosn [Declaration] [Declaration]

AbsProp AlexPosn String [Arg]

Assume Name [Arg] Expression

Instances

Eq Declaration

Methods

(==) :: Declaration -> Declaration -> Bool

(/=) :: Declaration -> Declaration -> Bool

Show Declaration

Methods

showsPrec :: Int -> Declaration -> ShowS

show :: Declaration -> String

showList :: [Declaration] -> ShowS

Generic Declaration

Associated Types

type Rep Declaration :: * -> *

Methods

from :: Declaration -> Rep Declaration x

to :: Rep Declaration x -> Declaration

NFData Declaration

Methods

rnf :: Declaration -> ()

type Rep Declaration

type Rep Declaration

data Expression

A (possibly effectful) expression.

Constructors

Let AlexPosn ATS (Maybe Expression)

VoidLiteral AlexPosn

Call Name [Expression] [Type] (Maybe Expression) [Expression]

NamedVal Name

If

Fields

• cond :: Expression

  Expression evaluating to a boolean value

• whenTrue :: Expression

  Expression to be returned when true

• elseExpr :: Maybe Expression

  Expression to be returned when false

Sif

Fields

• cond :: Expression

  Expression evaluating to a boolean value

• whenTrue :: Expression

  Expression to be returned when true

• selseExpr :: 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

Binary BinOp Expression Expression

BinList

Fields

• _op :: BinOp
• _exprs :: [Expression]

Unary UnOp Expression

Case

Fields

• posE :: AlexPosn
• kind :: Addendum
• val :: Expression
• arms :: [(Pattern, Expression)]

  Each `(Pattern, Expression)` pair corresponds to a branch of the 'case' statement

RecordValue AlexPosn [(String, Expression)] (Maybe Type)

Precede Expression Expression

FieldMutate

Fields

• posE :: AlexPosn
• old :: Expression

  Record to modify

• field :: String

  Field being modified

• new :: Expression

  New value of the field

Mutate Expression 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

TKind AlexPosn Name String

ViewExpr AlexPosn Type

Begin AlexPosn Expression

Instances

Eq Expression

Methods

(==) :: Expression -> Expression -> Bool

(/=) :: Expression -> Expression -> Bool

Show Expression

Methods

showsPrec :: Int -> Expression -> ShowS

show :: Expression -> String

showList :: [Expression] -> ShowS

Generic Expression

Associated Types

type Rep Expression :: * -> *

Methods

from :: Expression -> Rep Expression x

to :: Rep Expression x -> Expression

NFData Expression

Methods

rnf :: Expression -> ()

Plated Expression

Methods

plate :: Traversal' Expression Expression

Recursive Expression

Methods

project :: Expression -> Base Expression Expression

cata :: (Base Expression a -> a) -> Expression -> a

para :: (Base Expression (Expression, a) -> a) -> Expression -> a

gpara :: (Corecursive Expression, Comonad w) => (forall b. Base Expression (w b) -> w (Base Expression b)) -> (Base Expression (EnvT Expression w a) -> a) -> Expression -> a

prepro :: Corecursive Expression => (forall b. Base Expression b -> Base Expression b) -> (Base Expression a -> a) -> Expression -> a

gprepro :: (Corecursive Expression, Comonad w) => (forall b. Base Expression (w b) -> w (Base Expression b)) -> (forall c. Base Expression c -> Base Expression c) -> (Base Expression (w a) -> a) -> Expression -> a

Corecursive Expression

Methods

embed :: Base Expression Expression -> Expression

ana :: (a -> Base Expression a) -> a -> Expression

apo :: (a -> Base Expression (Either Expression a)) -> a -> Expression

postpro :: Recursive Expression => (forall b. Base Expression b -> Base Expression b) -> (a -> Base Expression a) -> a -> Expression

gpostpro :: (Recursive Expression, Monad m) => (forall b. m (Base Expression b) -> Base Expression (m b)) -> (forall c. Base Expression c -> Base Expression c) -> (a -> Base Expression (m a)) -> a -> Expression

type Rep Expression

type Rep Expression

type Base Expression

type Base Expression

data Type

A type for parsed ATS types

Constructors

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

ViewType AlexPosn Type

FunctionType String Type Type

Instances

Eq Type

Methods

(==) :: Type -> Type -> Bool

(/=) :: Type -> Type -> Bool

Show Type

Methods

showsPrec :: Int -> Type -> ShowS

show :: Type -> String

showList :: [Type] -> ShowS

Generic Type

Associated Types

type Rep Type :: * -> *

Methods

from :: Type -> Rep Type x

to :: Rep Type x -> Type

NFData Type

Methods

rnf :: Type -> ()

Recursive Type

Methods

project :: Type -> Base Type Type

cata :: (Base Type a -> a) -> Type -> a

para :: (Base Type (Type, a) -> a) -> Type -> a

gpara :: (Corecursive Type, Comonad w) => (forall b. Base Type (w b) -> w (Base Type b)) -> (Base Type (EnvT Type w a) -> a) -> Type -> a

prepro :: Corecursive Type => (forall b. Base Type b -> Base Type b) -> (Base Type a -> a) -> Type -> a

gprepro :: (Corecursive Type, Comonad w) => (forall b. Base Type (w b) -> w (Base Type b)) -> (forall c. Base Type c -> Base Type c) -> (Base Type (w a) -> a) -> Type -> a

Corecursive Type

Methods

embed :: Base Type Type -> Type

ana :: (a -> Base Type a) -> a -> Type

apo :: (a -> Base Type (Either Type a)) -> a -> Type

postpro :: Recursive Type => (forall b. Base Type b -> Base Type b) -> (a -> Base Type a) -> a -> Type

gpostpro :: (Recursive Type, Monad m) => (forall b. m (Base Type b) -> Base Type (m b)) -> (forall c. Base Type c -> Base Type c) -> (a -> Base Type (m a)) -> a -> Type

type Rep Type

type Rep Type

type Base Type

type Base Type

Executable

exec :: IO ()