language-ats-1.7.0.5: Parser and pretty-printer for ATS.

Safe HaskellNone
LanguageHaskell2010

Language.ATS

Contents

Description

Main module for the library

Synopsis

Functions for working with syntax

lexATS :: String -> Either String [Token] Source #

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

parse :: String -> Either ATSError (ATS AlexPosn) Source #

Parse a string containing ATS source.

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.

printATS :: Eq a => ATS a -> String Source #

Pretty-print with sensible defaults.

printATSCustom Source #

Arguments

:: Eq a 
=> Float

Ribbon fraction

-> Int

Ribbon width

-> ATS a 
-> String 

printATSFast :: Eq a => ATS a -> String Source #

Slightly faster pretty-printer without indendation (for code generation).

printErr :: MonadIO m => ATSError -> m () Source #

Print an error message to standard error.

warnErr :: MonadIO m => FilePath -> ATSError -> m () Source #

Same as printErr, but print a yellow warning message instead.

defaultFixityState :: FixityState a Source #

Fixities for operators in the ATS prelude.

Library functions

getDependencies :: ATS a -> [FilePath] Source #

Extract a list of files that some code depends on.

Syntax Tree

newtype ATS a Source #

An ATS file, containing a list of declarations

Constructors

ATS 

Fields

Instances
Eq a => Eq (ATS a) Source # 
Instance details

Defined in Language.ATS.Types

Methods

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

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

Generic (ATS a) Source # 
Instance details

Defined in Language.ATS.Types

Associated Types

type Rep (ATS a) :: Type -> Type #

Methods

from :: ATS a -> Rep (ATS a) x #

to :: Rep (ATS a) x -> ATS a #

Semigroup (ATS a) Source # 
Instance details

Defined in Language.ATS.Types

Methods

(<>) :: ATS a -> ATS a -> ATS a #

sconcat :: NonEmpty (ATS a) -> ATS a #

stimes :: Integral b => b -> ATS a -> ATS a #

Monoid (ATS a) Source # 
Instance details

Defined in Language.ATS.Types

Methods

mempty :: ATS a #

mappend :: ATS a -> ATS a -> ATS a #

mconcat :: [ATS a] -> ATS a #

Eq a => Pretty (ATS a) Source # 
Instance details

Defined in Language.ATS.PrettyPrint

Methods

pretty :: ATS a -> Doc #

prettyList :: [ATS a] -> Doc #

NFData a => NFData (ATS a) Source # 
Instance details

Defined in Language.ATS.Types

Methods

rnf :: ATS a -> () #

type Rep (ATS a) Source # 
Instance details

Defined in Language.ATS.Types

type Rep (ATS a) = D1 (MetaData "ATS" "Language.ATS.Types" "language-ats-1.7.0.5-CkYPsygOmJ2JVyp1DMPQY" True) (C1 (MetaCons "ATS" PrefixI True) (S1 (MetaSel (Just "unATS") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Declaration a])))

data Declaration a Source #

Declarations for functions, values, actions, etc.

Constructors

Func 

Fields

Impl 

Fields

ProofImpl 

Fields

Val 
StaVal [Universal a] String (Type a) 
PrVal 
PrVar 
Var 
AndDecl 

Fields

Include String 
Load 
Stadef String (SortArgs a) (Either (StaticExpression a, Maybe (Sort a)) (Maybe (Type a), Type a)) 
CBlock String 
TypeDef a String (SortArgs a) (Type a) (Maybe (Sort 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 

Fields

DataProp 
DataView a String (SortArgs a) (NonEmpty (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) (SortArgs a) (Type a) 
TKind a (Name a) String 
SymIntr a [Name a] 
Stacst a (Name a) (Type a) (Maybe (StaticExpression a)) 
PropDef a String (Args a) (Type a) 
FixityDecl (Fixity a) [String] 
MacDecl a String (Maybe [String]) (Expression a) 
DataSort a String (NonEmpty (DataSortLeaf a)) 
Exception String (Type a) 
ExtVar a String (Expression a) 
AbsImpl a (Name a) (SortArgs a) (Type a) 
Instances
Eq a => Eq (Declaration a) Source # 
Instance details

Defined in Language.ATS.Types

Generic (Declaration a) Source # 
Instance details

Defined in Language.ATS.Types

Associated Types

type Rep (Declaration a) :: Type -> Type #

Methods

from :: Declaration a -> Rep (Declaration a) x #

to :: Rep (Declaration a) x -> Declaration a #

Eq a => Pretty (Declaration a) Source # 
Instance details

Defined in Language.ATS.PrettyPrint

Methods

pretty :: Declaration a -> Doc #

prettyList :: [Declaration a] -> Doc #

NFData a => NFData (Declaration a) Source # 
Instance details

Defined in Language.ATS.Types

Methods

rnf :: Declaration a -> () #

type Rep (Declaration a) Source # 
Instance details

Defined in Language.ATS.Types

type Rep (Declaration a) = D1 (MetaData "Declaration" "Language.ATS.Types" "language-ats-1.7.0.5-CkYPsygOmJ2JVyp1DMPQY" False) (((((C1 (MetaCons "Func" PrefixI True) (S1 (MetaSel (Just "pos") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Just "_fun") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Function a))) :+: C1 (MetaCons "Impl" PrefixI True) (S1 (MetaSel (Just "implArgs") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Args a)) :*: S1 (MetaSel (Just "_impl") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Implementation a)))) :+: (C1 (MetaCons "ProofImpl" PrefixI True) (S1 (MetaSel (Just "implArgs") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Args a)) :*: S1 (MetaSel (Just "_impl") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Implementation a))) :+: (C1 (MetaCons "Val" PrefixI True) ((S1 (MetaSel (Just "add") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Addendum) :*: S1 (MetaSel (Just "valT") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe (Type a)))) :*: (S1 (MetaSel (Just "valPat") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Pattern a)) :*: S1 (MetaSel (Just "_valExpression") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expression a)))) :+: C1 (MetaCons "StaVal" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Universal a]) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type a))))))) :+: ((C1 (MetaCons "PrVal" PrefixI True) (S1 (MetaSel (Just "prvalPat") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Pattern a)) :*: (S1 (MetaSel (Just "_prValExpr") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe (StaticExpression a))) :*: S1 (MetaSel (Just "prValType") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe (Type a))))) :+: (C1 (MetaCons "PrVar" PrefixI True) (S1 (MetaSel (Just "prvarPat") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Pattern a)) :*: (S1 (MetaSel (Just "_prVarExpr") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe (StaticExpression a))) :*: S1 (MetaSel (Just "prVarType") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe (Type a))))) :+: C1 (MetaCons "Var" PrefixI True) ((S1 (MetaSel (Just "varT") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe (Type a))) :*: S1 (MetaSel (Just "varPat") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Pattern a))) :*: (S1 (MetaSel (Just "_varExpr1") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe (Expression a))) :*: S1 (MetaSel (Just "_varExpr2") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe (Expression a))))))) :+: (C1 (MetaCons "AndDecl" PrefixI True) (S1 (MetaSel (Just "andT") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe (Type a))) :*: (S1 (MetaSel (Just "andPat") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Pattern a)) :*: S1 (MetaSel (Just "_andExpr") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expression a)))) :+: (C1 (MetaCons "Include" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :+: C1 (MetaCons "Load" PrefixI True) ((S1 (MetaSel (Just "static") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool) :*: S1 (MetaSel (Just "withOctothorpe") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool)) :*: (S1 (MetaSel (Just "qualName") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe String)) :*: S1 (MetaSel (Just "fileName") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String))))))) :+: (((C1 (MetaCons "Stadef" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (SortArgs a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Either (StaticExpression a, Maybe (Sort a)) (Maybe (Type a), Type a))))) :+: C1 (MetaCons "CBlock" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String))) :+: (C1 (MetaCons "TypeDef" PrefixI False) ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (SortArgs a)) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe (Sort a)))))) :+: (C1 (MetaCons "ViewTypeDef" PrefixI False) ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (SortArgs a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type a)))) :+: C1 (MetaCons "SumType" PrefixI True) (S1 (MetaSel (Just "typeName") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String) :*: (S1 (MetaSel (Just "typeArgs") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (SortArgs a)) :*: S1 (MetaSel (Just "_leaves") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (NonEmpty (Leaf a)))))))) :+: ((C1 (MetaCons "SumViewType" PrefixI True) (S1 (MetaSel (Just "typeName") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String) :*: (S1 (MetaSel (Just "typeArgs") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (SortArgs a)) :*: S1 (MetaSel (Just "_leaves") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (NonEmpty (Leaf a))))) :+: (C1 (MetaCons "AbsType" PrefixI False) ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (SortArgs a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe (Type a))))) :+: C1 (MetaCons "AbsViewType" PrefixI False) ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (SortArgs a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe (Type a))))))) :+: (C1 (MetaCons "AbsView" PrefixI False) ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (SortArgs a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe (Type a))))) :+: (C1 (MetaCons "AbsVT0p" PrefixI False) ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (SortArgs a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe (Type a))))) :+: C1 (MetaCons "AbsT0p" PrefixI False) ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (SortArgs a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe (Type a)))))))))) :+: ((((C1 (MetaCons "ViewDef" PrefixI False) ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (SortArgs a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type a)))) :+: C1 (MetaCons "OverloadOp" PrefixI False) ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (BinOp a))) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Name a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe Int))))) :+: (C1 (MetaCons "OverloadIdent" PrefixI False) ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Name a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe Int)))) :+: (C1 (MetaCons "Comment" PrefixI True) (S1 (MetaSel (Just "_comment") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :+: C1 (MetaCons "DataProp" PrefixI True) ((S1 (MetaSel (Just "pos") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Just "propName") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :*: (S1 (MetaSel (Just "propArgs") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (SortArgs a)) :*: S1 (MetaSel (Just "_propLeaves") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [DataPropLeaf a])))))) :+: ((C1 (MetaCons "DataView" PrefixI False) ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (SortArgs a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (NonEmpty (Leaf a))))) :+: (C1 (MetaCons "Extern" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Declaration a))) :+: C1 (MetaCons "Define" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)))) :+: (C1 (MetaCons "SortDef" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Either (Sort a) (Universal a))))) :+: (C1 (MetaCons "AndD" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Declaration a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Declaration a))) :+: C1 (MetaCons "Local" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (ATS a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (ATS a)))))))) :+: (((C1 (MetaCons "AbsProp" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Arg a]))) :+: (C1 (MetaCons "Assume" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Name a)) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (SortArgs a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type a)))) :+: C1 (MetaCons "TKind" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Name a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String))))) :+: (C1 (MetaCons "SymIntr" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Name a])) :+: (C1 (MetaCons "Stacst" PrefixI False) ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Name a))) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe (StaticExpression a))))) :+: C1 (MetaCons "PropDef" PrefixI False) ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Args a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type a))))))) :+: ((C1 (MetaCons "FixityDecl" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Fixity a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [String])) :+: (C1 (MetaCons "MacDecl" PrefixI False) ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe [String])) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expression a)))) :+: C1 (MetaCons "DataSort" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (NonEmpty (DataSortLeaf a))))))) :+: (C1 (MetaCons "Exception" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type a))) :+: (C1 (MetaCons "ExtVar" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expression a)))) :+: C1 (MetaCons "AbsImpl" PrefixI False) ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Name a))) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (SortArgs a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type a))))))))))

data Expression a Source #

A (possibly effectful) expression.

Constructors

Let a (ATS a) (Maybe (Expression a)) 
VoidLiteral a

The '()' literal representing inaction.

Call 

Fields

NamedVal (Name a) 
ListLiteral a String (Type a) [Expression a] 
If 

Fields

UintLit Word

E.g. 1000u

FloatLit Float 
IntLit Int 
HexLit String 
UnderscoreLit a 
Lambda a (LambdaType a) (Pattern a) (Expression a) 
LinearLambda a (LambdaType a) (Pattern a) (Expression a) 
Index a (Name a) (Expression a)

E.g. array[0].

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 

Fields

Case 

Fields

RecordValue a (NonEmpty (String, Expression a)) 
BoxRecordValue a (NonEmpty (String, Expression a)) 
Precede (Expression a) (Expression a) 
ProofExpr a (NonEmpty (Expression a)) (Expression a) 
TypeSignature (Expression a) (Type a) 
WhereExp (Expression a) (ATS a) 
TupleEx a (NonEmpty (Expression a)) 
BoxTupleEx a (NonEmpty (Expression a)) 
While a (Expression a) (Expression a) 
WhileStar a [Universal a] (StaticExpression a) [Arg a] (Expression a) (Expression a) (Args a)

A while loop that is guaranteed to terminate.

For a (Expression a) (Expression a) 
ForStar a [Universal a] (StaticExpression a) [Arg a] (Expression a) (Expression a)

A for loop that is guaranteed to terminate.

Actions (ATS a) 
Begin a (Expression a) 
BinList 

Fields

PrecedeList 

Fields

FixAt a String (StackFunction a) 
LambdaAt a (StackFunction a) 
LinearLambdaAt a (StackFunction a) 
ParenExpr a (Expression a) 
CommentExpr String (Expression a) 
MacroVar a String 
Instances
Eq a => Eq (Expression a) Source # 
Instance details

Defined in Language.ATS.Types

Methods

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

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

Generic (Expression a) Source # 
Instance details

Defined in Language.ATS.Types

Associated Types

type Rep (Expression a) :: Type -> Type #

Methods

from :: Expression a -> Rep (Expression a) x #

to :: Rep (Expression a) x -> Expression a #

Eq a => Pretty (Expression a) Source # 
Instance details

Defined in Language.ATS.PrettyPrint

Methods

pretty :: Expression a -> Doc #

prettyList :: [Expression a] -> Doc #

NFData a => NFData (Expression a) Source # 
Instance details

Defined in Language.ATS.Types

Methods

rnf :: Expression a -> () #

Recursive (Expression a) Source # 
Instance details

Defined in Language.ATS.Types

Methods

project :: Expression a -> Base (Expression a) (Expression a) #

Corecursive (Expression a) Source # 
Instance details

Defined in Language.ATS.Types

Methods

embed :: Base (Expression a) (Expression a) -> Expression a #

type Rep (Expression a) Source # 
Instance details

Defined in Language.ATS.Types

type Rep (Expression a) = D1 (MetaData "Expression" "Language.ATS.Types" "language-ats-1.7.0.5-CkYPsygOmJ2JVyp1DMPQY" False) (((((C1 (MetaCons "Let" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (ATS a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe (Expression a))))) :+: C1 (MetaCons "VoidLiteral" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a))) :+: (C1 (MetaCons "Call" PrefixI True) ((S1 (MetaSel (Just "callName") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Name a)) :*: S1 (MetaSel (Just "callImplicits") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [[Type a]])) :*: (S1 (MetaSel (Just "callUniversals") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [[Type a]]) :*: (S1 (MetaSel (Just "callProofs") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe [Expression a])) :*: S1 (MetaSel (Just "callArgs") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Expression a])))) :+: (C1 (MetaCons "NamedVal" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Name a))) :+: C1 (MetaCons "ListLiteral" PrefixI False) ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Expression a])))))) :+: ((C1 (MetaCons "If" PrefixI True) (S1 (MetaSel (Just "cond") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expression a)) :*: (S1 (MetaSel (Just "whenTrue") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expression a)) :*: S1 (MetaSel (Just "elseExpr") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe (Expression a))))) :+: (C1 (MetaCons "UintLit" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Word)) :+: C1 (MetaCons "FloatLit" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Float)))) :+: (C1 (MetaCons "IntLit" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int)) :+: (C1 (MetaCons "HexLit" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :+: C1 (MetaCons "UnderscoreLit" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a)))))) :+: (((C1 (MetaCons "Lambda" PrefixI False) ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (LambdaType a))) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Pattern a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expression a)))) :+: C1 (MetaCons "LinearLambda" PrefixI False) ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (LambdaType a))) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Pattern a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expression a))))) :+: (C1 (MetaCons "Index" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Name a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expression a)))) :+: (C1 (MetaCons "Access" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expression a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Name a)))) :+: C1 (MetaCons "StringLit" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String))))) :+: ((C1 (MetaCons "CharLit" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Char)) :+: (C1 (MetaCons "AddrAt" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expression a))) :+: C1 (MetaCons "ViewAt" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expression a))))) :+: (C1 (MetaCons "Binary" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (BinOp a)) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expression a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expression a)))) :+: (C1 (MetaCons "Unary" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (UnOp a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expression a))) :+: C1 (MetaCons "IfCase" PrefixI True) (S1 (MetaSel (Just "posE") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Just "ifArms") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [(Expression a, LambdaType a, Expression a)]))))))) :+: ((((C1 (MetaCons "Case" PrefixI True) ((S1 (MetaSel (Just "posE") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Just "kind") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Addendum)) :*: (S1 (MetaSel (Just "val") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expression a)) :*: S1 (MetaSel (Just "_arms") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [(Pattern a, LambdaType a, Expression a)]))) :+: C1 (MetaCons "RecordValue" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (NonEmpty (String, Expression a))))) :+: (C1 (MetaCons "BoxRecordValue" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (NonEmpty (String, Expression a)))) :+: (C1 (MetaCons "Precede" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expression a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expression a))) :+: C1 (MetaCons "ProofExpr" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (NonEmpty (Expression a))) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expression a))))))) :+: ((C1 (MetaCons "TypeSignature" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expression a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type a))) :+: (C1 (MetaCons "WhereExp" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expression a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (ATS a))) :+: C1 (MetaCons "TupleEx" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (NonEmpty (Expression a)))))) :+: (C1 (MetaCons "BoxTupleEx" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (NonEmpty (Expression a)))) :+: (C1 (MetaCons "While" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expression a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expression a)))) :+: C1 (MetaCons "WhileStar" PrefixI False) ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Universal a]) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (StaticExpression a)))) :*: ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Arg a]) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expression a))) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expression a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Args a))))))))) :+: (((C1 (MetaCons "For" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expression a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expression a)))) :+: (C1 (MetaCons "ForStar" PrefixI False) ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Universal a]) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (StaticExpression a)))) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Arg a]) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expression a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expression a))))) :+: C1 (MetaCons "Actions" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (ATS a))))) :+: (C1 (MetaCons "Begin" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expression a))) :+: (C1 (MetaCons "BinList" PrefixI True) (S1 (MetaSel (Just "_op") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (BinOp a)) :*: S1 (MetaSel (Just "_exprs") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Expression a])) :+: C1 (MetaCons "PrecedeList" PrefixI True) (S1 (MetaSel (Just "_exprs") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Expression a]))))) :+: ((C1 (MetaCons "FixAt" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (StackFunction a)))) :+: (C1 (MetaCons "LambdaAt" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (StackFunction a))) :+: C1 (MetaCons "LinearLambdaAt" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (StackFunction a))))) :+: (C1 (MetaCons "ParenExpr" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expression a))) :+: (C1 (MetaCons "CommentExpr" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expression a))) :+: C1 (MetaCons "MacroVar" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String))))))))
type Base (Expression a) Source # 
Instance details

Defined in Language.ATS.Types

type Base (Expression a)

data Type a Source #

A type for parsed ATS types

Instances
Eq a => Eq (Type a) Source # 
Instance details

Defined in Language.ATS.Types

Methods

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

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

Generic (Type a) Source # 
Instance details

Defined in Language.ATS.Types

Associated Types

type Rep (Type a) :: Type -> Type #

Methods

from :: Type a -> Rep (Type a) x #

to :: Rep (Type a) x -> Type a #

Eq a => Pretty (Type a) Source # 
Instance details

Defined in Language.ATS.PrettyPrint

Methods

pretty :: Type a -> Doc #

prettyList :: [Type a] -> Doc #

NFData a => NFData (Type a) Source # 
Instance details

Defined in Language.ATS.Types

Methods

rnf :: Type a -> () #

Recursive (Type a) Source # 
Instance details

Defined in Language.ATS.Types

Methods

project :: Type a -> Base (Type a) (Type a) #

type Rep (Type a) Source # 
Instance details

Defined in Language.ATS.Types

type Rep (Type a) = D1 (MetaData "Type" "Language.ATS.Types" "language-ats-1.7.0.5-CkYPsygOmJ2JVyp1DMPQY" False) ((((C1 (MetaCons "Tuple" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Type a])) :+: C1 (MetaCons "BoxTuple" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (NonEmpty (Type a))))) :+: (C1 (MetaCons "Named" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Name a))) :+: (C1 (MetaCons "Ex" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Existential a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe (Type a)))) :+: C1 (MetaCons "ForA" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Universal a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type a)))))) :+: ((C1 (MetaCons "Dependent" PrefixI True) (S1 (MetaSel (Just "_typeCall") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Name a)) :*: S1 (MetaSel (Just "_typeCallArgs") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Type a])) :+: (C1 (MetaCons "Unconsumed" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type a))) :+: C1 (MetaCons "AsProof" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe (Type a)))))) :+: (C1 (MetaCons "FromVT" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type a))) :+: (C1 (MetaCons "MaybeVal" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type a))) :+: C1 (MetaCons "AtExpr" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (StaticExpression a)))))))) :+: (((C1 (MetaCons "ArrayType" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (StaticExpression a)))) :+: C1 (MetaCons "ProofType" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (NonEmpty (Type a))) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (NonEmpty (Type a)))))) :+: (C1 (MetaCons "ConcreteType" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (StaticExpression a))) :+: (C1 (MetaCons "RefType" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type a))) :+: C1 (MetaCons "ViewType" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type a)))))) :+: ((C1 (MetaCons "FunctionType" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type a)))) :+: (C1 (MetaCons "ImplicitType" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a)) :+: C1 (MetaCons "ViewLiteral" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Addendum)))) :+: (C1 (MetaCons "AnonymousRecord" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (NonEmpty (String, Type a)))) :+: (C1 (MetaCons "WhereType" PrefixI False) ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type a))) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (SortArgs a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type a))))) :+: C1 (MetaCons "AddrType" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a)))))))
type Base (Type a) Source # 
Instance details

Defined in Language.ATS.Types

type Base (Type a)

data Function a Source #

A function declaration accounting for all keywords ATS uses to define them.

Instances
Eq a => Eq (Function a) Source # 
Instance details

Defined in Language.ATS.Types

Methods

(==) :: Function a -> Function a -> Bool #

(/=) :: Function a -> Function a -> Bool #

Generic (Function a) Source # 
Instance details

Defined in Language.ATS.Types

Associated Types

type Rep (Function a) :: Type -> Type #

Methods

from :: Function a -> Rep (Function a) x #

to :: Rep (Function a) x -> Function a #

NFData a => NFData (Function a) Source # 
Instance details

Defined in Language.ATS.Types

Methods

rnf :: Function a -> () #

type Rep (Function a) Source # 
Instance details

Defined in Language.ATS.Types

data Implementation a Source #

An implement or primplmnt declaration

Constructors

Implement 

Fields

Instances
Eq a => Eq (Implementation a) Source # 
Instance details

Defined in Language.ATS.Types

Generic (Implementation a) Source # 
Instance details

Defined in Language.ATS.Types

Associated Types

type Rep (Implementation a) :: Type -> Type #

Eq a => Pretty (Implementation a) Source # 
Instance details

Defined in Language.ATS.PrettyPrint

NFData a => NFData (Implementation a) Source # 
Instance details

Defined in Language.ATS.Types

Methods

rnf :: Implementation a -> () #

type Rep (Implementation a) Source # 
Instance details

Defined in Language.ATS.Types

data Pattern a Source #

A data type for patterns.

Instances
Eq a => Eq (Pattern a) Source # 
Instance details

Defined in Language.ATS.Types

Methods

(==) :: Pattern a -> Pattern a -> Bool #

(/=) :: Pattern a -> Pattern a -> Bool #

Generic (Pattern a) Source # 
Instance details

Defined in Language.ATS.Types

Associated Types

type Rep (Pattern a) :: Type -> Type #

Methods

from :: Pattern a -> Rep (Pattern a) x #

to :: Rep (Pattern a) x -> Pattern a #

Eq a => Pretty (Pattern a) Source # 
Instance details

Defined in Language.ATS.PrettyPrint

Methods

pretty :: Pattern a -> Doc #

prettyList :: [Pattern a] -> Doc #

NFData a => NFData (Pattern a) Source # 
Instance details

Defined in Language.ATS.Types

Methods

rnf :: Pattern a -> () #

Recursive (Pattern a) Source # 
Instance details

Defined in Language.ATS.Types

Methods

project :: Pattern a -> Base (Pattern a) (Pattern a) #

type Rep (Pattern a) Source # 
Instance details

Defined in Language.ATS.Types

type Rep (Pattern a) = D1 (MetaData "Pattern" "Language.ATS.Types" "language-ats-1.7.0.5-CkYPsygOmJ2JVyp1DMPQY" False) (((C1 (MetaCons "PName" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Name a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Pattern a])) :+: (C1 (MetaCons "PSum" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Pattern a))) :+: C1 (MetaCons "PLiteral" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expression a))))) :+: (C1 (MetaCons "Guarded" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expression a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Pattern a)))) :+: (C1 (MetaCons "Free" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Pattern a))) :+: C1 (MetaCons "Proof" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Pattern a]) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Pattern a])))))) :+: ((C1 (MetaCons "TuplePattern" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Pattern a])) :+: (C1 (MetaCons "BoxTuplePattern" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Pattern a])) :+: C1 (MetaCons "AtPattern" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Pattern a))))) :+: ((C1 (MetaCons "UniversalPattern" PrefixI False) ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Universal a]) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Pattern a)))) :+: C1 (MetaCons "ExistentialPattern" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Existential a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Pattern a)))) :+: (C1 (MetaCons "As" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Pattern a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Pattern a)))) :+: C1 (MetaCons "BinPattern" PrefixI False) ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (BinOp a))) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Pattern a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Pattern a))))))))
type Base (Pattern a) Source # 
Instance details

Defined in Language.ATS.Types

type Base (Pattern a)

data Name a Source #

Constructors

Unqualified String 
Qualified a String String

A name can be qualified e.g. $UN.unsafefn

SpecialName a String

A name for builtin functions such as $showtype.

Functorial String String 
FieldName a String String 
Instances
Eq a => Eq (Name a) Source # 
Instance details

Defined in Language.ATS.Types

Methods

(==) :: Name a -> Name a -> Bool #

(/=) :: Name a -> Name a -> Bool #

Generic (Name a) Source # 
Instance details

Defined in Language.ATS.Types

Associated Types

type Rep (Name a) :: Type -> Type #

Methods

from :: Name a -> Rep (Name a) x #

to :: Rep (Name a) x -> Name a #

Pretty (Name a) Source # 
Instance details

Defined in Language.ATS.PrettyPrint

Methods

pretty :: Name a -> Doc #

prettyList :: [Name a] -> Doc #

NFData a => NFData (Name a) Source # 
Instance details

Defined in Language.ATS.Types

Methods

rnf :: Name a -> () #

type Rep (Name a) Source # 
Instance details

Defined in Language.ATS.Types

type Rep (Name a) = D1 (MetaData "Name" "Language.ATS.Types" "language-ats-1.7.0.5-CkYPsygOmJ2JVyp1DMPQY" False) ((C1 (MetaCons "Unqualified" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :+: C1 (MetaCons "Qualified" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)))) :+: (C1 (MetaCons "SpecialName" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :+: (C1 (MetaCons "Functorial" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :+: C1 (MetaCons "FieldName" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String))))))

data UnOp a Source #

Unary operators

Constructors

Negate 
Deref
~
SpecialOp a String
!
Instances
Eq a => Eq (UnOp a) Source # 
Instance details

Defined in Language.ATS.Types

Methods

(==) :: UnOp a -> UnOp a -> Bool #

(/=) :: UnOp a -> UnOp a -> Bool #

Generic (UnOp a) Source # 
Instance details

Defined in Language.ATS.Types

Associated Types

type Rep (UnOp a) :: Type -> Type #

Methods

from :: UnOp a -> Rep (UnOp a) x #

to :: Rep (UnOp a) x -> UnOp a #

Pretty (UnOp a) Source # 
Instance details

Defined in Language.ATS.PrettyPrint

Methods

pretty :: UnOp a -> Doc #

prettyList :: [UnOp a] -> Doc #

NFData a => NFData (UnOp a) Source # 
Instance details

Defined in Language.ATS.Types

Methods

rnf :: UnOp a -> () #

type Rep (UnOp a) Source # 
Instance details

Defined in Language.ATS.Types

type Rep (UnOp a) = D1 (MetaData "UnOp" "Language.ATS.Types" "language-ats-1.7.0.5-CkYPsygOmJ2JVyp1DMPQY" False) (C1 (MetaCons "Negate" PrefixI False) (U1 :: Type -> Type) :+: (C1 (MetaCons "Deref" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "SpecialOp" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String))))

data BinOp a Source #

Binary operators on expressions

Bundled Patterns

pattern Con :: a -> BinOp a 
Instances
Eq a => Eq (BinOp a) Source # 
Instance details

Defined in Language.ATS.Types

Methods

(==) :: BinOp a -> BinOp a -> Bool #

(/=) :: BinOp a -> BinOp a -> Bool #

Generic (BinOp a) Source # 
Instance details

Defined in Language.ATS.Types

Associated Types

type Rep (BinOp a) :: Type -> Type #

Methods

from :: BinOp a -> Rep (BinOp a) x #

to :: Rep (BinOp a) x -> BinOp a #

Pretty (BinOp a) Source # 
Instance details

Defined in Language.ATS.PrettyPrint

Methods

pretty :: BinOp a -> Doc #

prettyList :: [BinOp a] -> Doc #

NFData a => NFData (BinOp a) Source # 
Instance details

Defined in Language.ATS.Types

Methods

rnf :: BinOp a -> () #

type Rep (BinOp a) Source # 
Instance details

Defined in Language.ATS.Types

type Rep (BinOp a) = D1 (MetaData "BinOp" "Language.ATS.Types" "language-ats-1.7.0.5-CkYPsygOmJ2JVyp1DMPQY" False) ((((C1 (MetaCons "Add" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "Mult" PrefixI False) (U1 :: Type -> Type)) :+: (C1 (MetaCons "Div" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "Sub" PrefixI False) (U1 :: Type -> Type))) :+: ((C1 (MetaCons "GreaterThan" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "GreaterThanEq" PrefixI False) (U1 :: Type -> Type)) :+: (C1 (MetaCons "LessThan" PrefixI False) (U1 :: Type -> Type) :+: (C1 (MetaCons "LessThanEq" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "Equal" PrefixI False) (U1 :: Type -> Type))))) :+: (((C1 (MetaCons "LogicalAnd" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "LogicalOr" PrefixI False) (U1 :: Type -> Type)) :+: (C1 (MetaCons "StaticEq" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "Mod" PrefixI False) (U1 :: Type -> Type))) :+: ((C1 (MetaCons "NotEq" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "Mutate" PrefixI False) (U1 :: Type -> Type)) :+: (C1 (MetaCons "At" PrefixI False) (U1 :: Type -> Type) :+: (C1 (MetaCons "SpearOp" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "SpecialInfix" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)))))))

data DataPropLeaf a Source #

Constructors

DataPropLeaf 
Instances
Eq a => Eq (DataPropLeaf a) Source # 
Instance details

Defined in Language.ATS.Types

Generic (DataPropLeaf a) Source # 
Instance details

Defined in Language.ATS.Types

Associated Types

type Rep (DataPropLeaf a) :: Type -> Type #

Methods

from :: DataPropLeaf a -> Rep (DataPropLeaf a) x #

to :: Rep (DataPropLeaf a) x -> DataPropLeaf a #

NFData a => NFData (DataPropLeaf a) Source # 
Instance details

Defined in Language.ATS.Types

Methods

rnf :: DataPropLeaf a -> () #

type Rep (DataPropLeaf a) Source # 
Instance details

Defined in Language.ATS.Types

type Rep (DataPropLeaf a) = D1 (MetaData "DataPropLeaf" "Language.ATS.Types" "language-ats-1.7.0.5-CkYPsygOmJ2JVyp1DMPQY" False) (C1 (MetaCons "DataPropLeaf" PrefixI True) (S1 (MetaSel (Just "propU") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Universal a]) :*: (S1 (MetaSel (Just "_propExpr1") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expression a)) :*: S1 (MetaSel (Just "_propExpr2") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe (Expression a))))))

data Leaf a Source #

Instances
Eq a => Eq (Leaf a) Source # 
Instance details

Defined in Language.ATS.Types

Methods

(==) :: Leaf a -> Leaf a -> Bool #

(/=) :: Leaf a -> Leaf a -> Bool #

Generic (Leaf a) Source # 
Instance details

Defined in Language.ATS.Types

Associated Types

type Rep (Leaf a) :: Type -> Type #

Methods

from :: Leaf a -> Rep (Leaf a) x #

to :: Rep (Leaf a) x -> Leaf a #

NFData a => NFData (Leaf a) Source # 
Instance details

Defined in Language.ATS.Types

Methods

rnf :: Leaf a -> () #

type Rep (Leaf a) Source # 
Instance details

Defined in Language.ATS.Types

type Rep (Leaf a) = D1 (MetaData "Leaf" "Language.ATS.Types" "language-ats-1.7.0.5-CkYPsygOmJ2JVyp1DMPQY" False) (C1 (MetaCons "Leaf" PrefixI True) ((S1 (MetaSel (Just "_constructorUniversals") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Universal a]) :*: S1 (MetaSel (Just "name") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :*: (S1 (MetaSel (Just "constructorArgs") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [StaticExpression a]) :*: S1 (MetaSel (Just "maybeType") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe (Type a))))))

data DataSortLeaf a Source #

Constructors

DataSortLeaf [Universal a] (Sort a) (Maybe (Sort a)) 
Instances
Eq a => Eq (DataSortLeaf a) Source # 
Instance details

Defined in Language.ATS.Types

Generic (DataSortLeaf a) Source # 
Instance details

Defined in Language.ATS.Types

Associated Types

type Rep (DataSortLeaf a) :: Type -> Type #

Methods

from :: DataSortLeaf a -> Rep (DataSortLeaf a) x #

to :: Rep (DataSortLeaf a) x -> DataSortLeaf a #

NFData a => NFData (DataSortLeaf a) Source # 
Instance details

Defined in Language.ATS.Types

Methods

rnf :: DataSortLeaf a -> () #

type Rep (DataSortLeaf a) Source # 
Instance details

Defined in Language.ATS.Types

data Arg a Source #

An argument to a function.

Constructors

Arg (Paired String (Type a)) 
PrfArg [Arg a] (Arg a) 
Instances
Eq a => Eq (Arg a) Source # 
Instance details

Defined in Language.ATS.Types

Methods

(==) :: Arg a -> Arg a -> Bool #

(/=) :: Arg a -> Arg a -> Bool #

Generic (Arg a) Source # 
Instance details

Defined in Language.ATS.Types

Associated Types

type Rep (Arg a) :: Type -> Type #

Methods

from :: Arg a -> Rep (Arg a) x #

to :: Rep (Arg a) x -> Arg a #

Eq a => Pretty (Arg a) Source # 
Instance details

Defined in Language.ATS.PrettyPrint

Methods

pretty :: Arg a -> Doc #

prettyList :: [Arg a] -> Doc #

NFData a => NFData (Arg a) Source # 
Instance details

Defined in Language.ATS.Types

Methods

rnf :: Arg a -> () #

type Rep (Arg a) Source # 
Instance details

Defined in Language.ATS.Types

data Addendum Source #

Determines the default behavior for incomplete pattern matches

Constructors

None 
Plus 
Minus 
Instances
Eq Addendum Source # 
Instance details

Defined in Language.ATS.Lexer

Show Addendum Source # 
Instance details

Defined in Language.ATS.Lexer

Generic Addendum Source # 
Instance details

Defined in Language.ATS.Lexer

Associated Types

type Rep Addendum :: Type -> Type #

Methods

from :: Addendum -> Rep Addendum x #

to :: Rep Addendum x -> Addendum #

Pretty Addendum Source # 
Instance details

Defined in Language.ATS.Lexer

Methods

pretty :: Addendum -> Doc #

prettyList :: [Addendum] -> Doc #

NFData Addendum Source # 
Instance details

Defined in Language.ATS.Lexer

Methods

rnf :: Addendum -> () #

type Rep Addendum Source # 
Instance details

Defined in Language.ATS.Lexer

type Rep Addendum = D1 (MetaData "Addendum" "Language.ATS.Lexer" "language-ats-1.7.0.5-CkYPsygOmJ2JVyp1DMPQY" False) (C1 (MetaCons "None" PrefixI False) (U1 :: Type -> Type) :+: (C1 (MetaCons "Plus" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "Minus" PrefixI False) (U1 :: Type -> Type)))

data LambdaType a Source #

A type for =>, =<cloref1>, etc.

Constructors

Plain a 
Spear a 
ProofArrow a
=>>
ProofSpear a
=/=>
Full a String
=/=>>
Instances
Eq a => Eq (LambdaType a) Source # 
Instance details

Defined in Language.ATS.Types

Methods

(==) :: LambdaType a -> LambdaType a -> Bool #

(/=) :: LambdaType a -> LambdaType a -> Bool #

Generic (LambdaType a) Source # 
Instance details

Defined in Language.ATS.Types

Associated Types

type Rep (LambdaType a) :: Type -> Type #

Methods

from :: LambdaType a -> Rep (LambdaType a) x #

to :: Rep (LambdaType a) x -> LambdaType a #

Pretty (LambdaType a) Source # 
Instance details

Defined in Language.ATS.PrettyPrint

Methods

pretty :: LambdaType a -> Doc #

prettyList :: [LambdaType a] -> Doc #

NFData a => NFData (LambdaType a) Source # 
Instance details

Defined in Language.ATS.Types

Methods

rnf :: LambdaType a -> () #

type Rep (LambdaType a) Source # 
Instance details

Defined in Language.ATS.Types

data Universal a Source #

Wrapper for universal quantifiers (refinement types)

Constructors

Universal 

Fields

Instances
Eq a => Eq (Universal a) Source # 
Instance details

Defined in Language.ATS.Types

Methods

(==) :: Universal a -> Universal a -> Bool #

(/=) :: Universal a -> Universal a -> Bool #

Generic (Universal a) Source # 
Instance details

Defined in Language.ATS.Types

Associated Types

type Rep (Universal a) :: Type -> Type #

Methods

from :: Universal a -> Rep (Universal a) x #

to :: Rep (Universal a) x -> Universal a #

Eq a => Pretty (Universal a) Source # 
Instance details

Defined in Language.ATS.PrettyPrint

Methods

pretty :: Universal a -> Doc #

prettyList :: [Universal a] -> Doc #

NFData a => NFData (Universal a) Source # 
Instance details

Defined in Language.ATS.Types

Methods

rnf :: Universal a -> () #

type Rep (Universal a) Source # 
Instance details

Defined in Language.ATS.Types

type Rep (Universal a) = D1 (MetaData "Universal" "Language.ATS.Types" "language-ats-1.7.0.5-CkYPsygOmJ2JVyp1DMPQY" False) (C1 (MetaCons "Universal" PrefixI True) (S1 (MetaSel (Just "bound") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [String]) :*: (S1 (MetaSel (Just "typeU") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe (Sort a))) :*: S1 (MetaSel (Just "prop") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [StaticExpression a]))))

data Existential a Source #

Wrapper for existential quantifiers/types

Constructors

Existential 

Fields

Instances
Eq a => Eq (Existential a) Source # 
Instance details

Defined in Language.ATS.Types

Generic (Existential a) Source # 
Instance details

Defined in Language.ATS.Types

Associated Types

type Rep (Existential a) :: Type -> Type #

Methods

from :: Existential a -> Rep (Existential a) x #

to :: Rep (Existential a) x -> Existential a #

Eq a => Pretty (Existential a) Source # 
Instance details

Defined in Language.ATS.PrettyPrint

Methods

pretty :: Existential a -> Doc #

prettyList :: [Existential a] -> Doc #

NFData a => NFData (Existential a) Source # 
Instance details

Defined in Language.ATS.Types

Methods

rnf :: Existential a -> () #

type Rep (Existential a) Source # 
Instance details

Defined in Language.ATS.Types

data PreFunction ek a Source #

Constructors

PreF 

Fields

Instances
(Eq a, Eq (ek a)) => Eq (PreFunction ek a) Source # 
Instance details

Defined in Language.ATS.Types

Methods

(==) :: PreFunction ek a -> PreFunction ek a -> Bool #

(/=) :: PreFunction ek a -> PreFunction ek a -> Bool #

Generic (PreFunction ek a) Source # 
Instance details

Defined in Language.ATS.Types

Associated Types

type Rep (PreFunction ek a) :: Type -> Type #

Methods

from :: PreFunction ek a -> Rep (PreFunction ek a) x #

to :: Rep (PreFunction ek a) x -> PreFunction ek a #

(Eq a, Pretty (ek a)) => Pretty (PreFunction ek a) Source # 
Instance details

Defined in Language.ATS.PrettyPrint

Methods

pretty :: PreFunction ek a -> Doc #

prettyList :: [PreFunction ek a] -> Doc #

(NFData a, NFData (ek a)) => NFData (PreFunction ek a) Source # 
Instance details

Defined in Language.ATS.Types

Methods

rnf :: PreFunction ek a -> () #

type Rep (PreFunction ek a) Source # 
Instance details

Defined in Language.ATS.Types

data StaticExpression a Source #

Instances
Eq a => Eq (StaticExpression a) Source # 
Instance details

Defined in Language.ATS.Types

Generic (StaticExpression a) Source # 
Instance details

Defined in Language.ATS.Types

Associated Types

type Rep (StaticExpression a) :: Type -> Type #

Eq a => Pretty (StaticExpression a) Source # 
Instance details

Defined in Language.ATS.PrettyPrint

NFData a => NFData (StaticExpression a) Source # 
Instance details

Defined in Language.ATS.Types

Methods

rnf :: StaticExpression a -> () #

Recursive (StaticExpression a) Source # 
Instance details

Defined in Language.ATS.Types

Corecursive (StaticExpression a) Source # 
Instance details

Defined in Language.ATS.Types

type Rep (StaticExpression a) Source # 
Instance details

Defined in Language.ATS.Types

type Rep (StaticExpression a) = D1 (MetaData "StaticExpression" "Language.ATS.Types" "language-ats-1.7.0.5-CkYPsygOmJ2JVyp1DMPQY" False) ((((C1 (MetaCons "StaticVal" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Name a))) :+: C1 (MetaCons "StaticBinary" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (BinOp a)) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (StaticExpression a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (StaticExpression a))))) :+: (C1 (MetaCons "StaticInt" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int)) :+: C1 (MetaCons "StaticHex" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)))) :+: ((C1 (MetaCons "SPrecede" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (StaticExpression a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (StaticExpression a))) :+: C1 (MetaCons "SPrecedeList" PrefixI True) (S1 (MetaSel (Just "_sExprs") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [StaticExpression a]))) :+: (C1 (MetaCons "StaticVoid" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a)) :+: (C1 (MetaCons "Sif" PrefixI True) (S1 (MetaSel (Just "scond") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (StaticExpression a)) :*: (S1 (MetaSel (Just "whenTrue") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (StaticExpression a)) :*: S1 (MetaSel (Just "selseExpr") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (StaticExpression a)))) :+: C1 (MetaCons "SCall" PrefixI False) ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Name a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [[Type a]])) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [[Type a]]) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [StaticExpression a]))))))) :+: (((C1 (MetaCons "SUnary" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (UnOp a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (StaticExpression a))) :+: C1 (MetaCons "SLet" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Declaration a]) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe (StaticExpression a)))))) :+: (C1 (MetaCons "SCase" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Addendum) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (StaticExpression a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [(Pattern a, LambdaType a, StaticExpression a)]))) :+: C1 (MetaCons "SString" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)))) :+: ((C1 (MetaCons "Witness" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (StaticExpression a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (StaticExpression a)))) :+: C1 (MetaCons "ProofLambda" PrefixI False) ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (LambdaType a))) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Pattern a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (StaticExpression a))))) :+: (C1 (MetaCons "ProofLinearLambda" PrefixI False) ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (LambdaType a))) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Pattern a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (StaticExpression a)))) :+: (C1 (MetaCons "WhereStaExp" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (StaticExpression a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (ATS a))) :+: C1 (MetaCons "SParens" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (StaticExpression a))))))))
type Base (StaticExpression a) Source # 
Instance details

Defined in Language.ATS.Types

data StackFunction a Source #

A type for stack-allocated functions. See here for more.

Constructors

StackF 
Instances
Eq a => Eq (StackFunction a) Source # 
Instance details

Defined in Language.ATS.Types

Generic (StackFunction a) Source # 
Instance details

Defined in Language.ATS.Types

Associated Types

type Rep (StackFunction a) :: Type -> Type #

NFData a => NFData (StackFunction a) Source # 
Instance details

Defined in Language.ATS.Types

Methods

rnf :: StackFunction a -> () #

type Rep (StackFunction a) Source # 
Instance details

Defined in Language.ATS.Types

type Rep (StackFunction a) = D1 (MetaData "StackFunction" "Language.ATS.Types" "language-ats-1.7.0.5-CkYPsygOmJ2JVyp1DMPQY" False) (C1 (MetaCons "StackF" PrefixI True) ((S1 (MetaSel (Just "stSig") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String) :*: S1 (MetaSel (Just "stArgs") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Arg a])) :*: (S1 (MetaSel (Just "stReturnType") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type a)) :*: S1 (MetaSel (Just "stExpression") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expression a)))))

data Paired a b Source #

Constructors

Both a b 
First a 
Second b 
Instances
(Eq a, Eq b) => Eq (Paired a b) Source # 
Instance details

Defined in Language.ATS.Types

Methods

(==) :: Paired a b -> Paired a b -> Bool #

(/=) :: Paired a b -> Paired a b -> Bool #

Generic (Paired a b) Source # 
Instance details

Defined in Language.ATS.Types

Associated Types

type Rep (Paired a b) :: Type -> Type #

Methods

from :: Paired a b -> Rep (Paired a b) x #

to :: Rep (Paired a b) x -> Paired a b #

(NFData a, NFData b) => NFData (Paired a b) Source # 
Instance details

Defined in Language.ATS.Types

Methods

rnf :: Paired a b -> () #

type Rep (Paired a b) Source # 
Instance details

Defined in Language.ATS.Types

data Fixity a Source #

Constructors

RightFix 

Fields

LeftFix 

Fields

Pre 

Fields

Post 

Fields

Infix 

Fields

Instances
Eq a => Eq (Fixity a) Source # 
Instance details

Defined in Language.ATS.Types

Methods

(==) :: Fixity a -> Fixity a -> Bool #

(/=) :: Fixity a -> Fixity a -> Bool #

Eq a => Ord (Fixity a) Source # 
Instance details

Defined in Language.ATS.Types

Methods

compare :: Fixity a -> Fixity a -> Ordering #

(<) :: Fixity a -> Fixity a -> Bool #

(<=) :: Fixity a -> Fixity a -> Bool #

(>) :: Fixity a -> Fixity a -> Bool #

(>=) :: Fixity a -> Fixity a -> Bool #

max :: Fixity a -> Fixity a -> Fixity a #

min :: Fixity a -> Fixity a -> Fixity a #

Generic (Fixity a) Source # 
Instance details

Defined in Language.ATS.Types

Associated Types

type Rep (Fixity a) :: Type -> Type #

Methods

from :: Fixity a -> Rep (Fixity a) x #

to :: Rep (Fixity a) x -> Fixity a #

Eq a => Pretty (Fixity a) Source # 
Instance details

Defined in Language.ATS.PrettyPrint

Methods

pretty :: Fixity a -> Doc #

prettyList :: [Fixity a] -> Doc #

NFData a => NFData (Fixity a) Source # 
Instance details

Defined in Language.ATS.Types

Methods

rnf :: Fixity a -> () #

type Rep (Fixity a) Source # 
Instance details

Defined in Language.ATS.Types

data SortArg a Source #

Constructors

SortArg String (Sort a) 
Anonymous (Sort a) 
Instances
Eq a => Eq (SortArg a) Source # 
Instance details

Defined in Language.ATS.Types

Methods

(==) :: SortArg a -> SortArg a -> Bool #

(/=) :: SortArg a -> SortArg a -> Bool #

Generic (SortArg a) Source # 
Instance details

Defined in Language.ATS.Types

Associated Types

type Rep (SortArg a) :: Type -> Type #

Methods

from :: SortArg a -> Rep (SortArg a) x #

to :: Rep (SortArg a) x -> SortArg a #

Eq a => Pretty (SortArg a) Source # 
Instance details

Defined in Language.ATS.PrettyPrint

Methods

pretty :: SortArg a -> Doc #

prettyList :: [SortArg a] -> Doc #

NFData a => NFData (SortArg a) Source # 
Instance details

Defined in Language.ATS.Types

Methods

rnf :: SortArg a -> () #

type Rep (SortArg a) Source # 
Instance details

Defined in Language.ATS.Types

data Sort a Source #

A datatype for sorts.

Constructors

NamedSort 

Fields

T0p Addendum
t@ype
Vt0p Addendum
vt@ype
Addr 
VType a Addendum

viewtype or vtype

View a Addendum
view
TupleSort a (Sort a) (Sort a) 
ArrowSort a (Sort a) (Sort a) 
Instances
Eq a => Eq (Sort a) Source # 
Instance details

Defined in Language.ATS.Types

Methods

(==) :: Sort a -> Sort a -> Bool #

(/=) :: Sort a -> Sort a -> Bool #

Generic (Sort a) Source # 
Instance details

Defined in Language.ATS.Types

Associated Types

type Rep (Sort a) :: Type -> Type #

Methods

from :: Sort a -> Rep (Sort a) x #

to :: Rep (Sort a) x -> Sort a #

Eq a => Pretty (Sort a) Source # 
Instance details

Defined in Language.ATS.PrettyPrint

Methods

pretty :: Sort a -> Doc #

prettyList :: [Sort a] -> Doc #

NFData a => NFData (Sort a) Source # 
Instance details

Defined in Language.ATS.Types

Methods

rnf :: Sort a -> () #

Recursive (Sort a) Source # 
Instance details

Defined in Language.ATS.Types

Methods

project :: Sort a -> Base (Sort a) (Sort a) #

type Rep (Sort a) Source # 
Instance details

Defined in Language.ATS.Types

type Rep (Sort a) = D1 (MetaData "Sort" "Language.ATS.Types" "language-ats-1.7.0.5-CkYPsygOmJ2JVyp1DMPQY" False) (((C1 (MetaCons "NamedSort" PrefixI True) (S1 (MetaSel (Just "_sortName") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :+: C1 (MetaCons "T0p" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Addendum))) :+: (C1 (MetaCons "Vt0p" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Addendum)) :+: C1 (MetaCons "Addr" PrefixI False) (U1 :: Type -> Type))) :+: ((C1 (MetaCons "VType" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Addendum)) :+: C1 (MetaCons "View" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Addendum))) :+: (C1 (MetaCons "TupleSort" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Sort a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Sort a)))) :+: C1 (MetaCons "ArrowSort" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Sort a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Sort a)))))))
type Base (Sort a) Source # 
Instance details

Defined in Language.ATS.Types

type Base (Sort a)

type Args a = Maybe [Arg a] Source #

Parser State

Lexical types

data Token Source #

Instances
Eq Token Source # 
Instance details

Defined in Language.ATS.Lexer

Methods

(==) :: Token -> Token -> Bool #

(/=) :: Token -> Token -> Bool #

Show Token Source # 
Instance details

Defined in Language.ATS.Lexer

Methods

showsPrec :: Int -> Token -> ShowS #

show :: Token -> String #

showList :: [Token] -> ShowS #

Generic Token Source # 
Instance details

Defined in Language.ATS.Lexer

Associated Types

type Rep Token :: Type -> Type #

Methods

from :: Token -> Rep Token x #

to :: Rep Token x -> Token #

Pretty Token Source # 
Instance details

Defined in Language.ATS.Lexer

Methods

pretty :: Token -> Doc #

prettyList :: [Token] -> Doc #

NFData Token Source # 
Instance details

Defined in Language.ATS.Lexer

Methods

rnf :: Token -> () #

type Rep Token Source # 
Instance details

Defined in Language.ATS.Lexer

type Rep Token = D1 (MetaData "Token" "Language.ATS.Lexer" "language-ats-1.7.0.5-CkYPsygOmJ2JVyp1DMPQY" False) ((((C1 (MetaCons "Identifier" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 AlexPosn) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :+: (C1 (MetaCons "SpecialIdentifier" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 AlexPosn) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :+: C1 (MetaCons "Keyword" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 AlexPosn) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Keyword)))) :+: (C1 (MetaCons "IntTok" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 AlexPosn) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int)) :+: (C1 (MetaCons "HexIntTok" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 AlexPosn) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :+: C1 (MetaCons "FloatTok" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 AlexPosn) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Float))))) :+: ((C1 (MetaCons "CharTok" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 AlexPosn) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Char)) :+: (C1 (MetaCons "StringTok" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 AlexPosn) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :+: C1 (MetaCons "Special" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 AlexPosn) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)))) :+: ((C1 (MetaCons "CBlockLex" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 AlexPosn) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :+: C1 (MetaCons "IdentifierSpace" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 AlexPosn) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String))) :+: (C1 (MetaCons "Operator" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 AlexPosn) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :+: C1 (MetaCons "Arrow" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 AlexPosn) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)))))) :+: (((C1 (MetaCons "FuncType" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 AlexPosn) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :+: (C1 (MetaCons "CommentLex" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 AlexPosn) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :+: C1 (MetaCons "CommentBegin" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 AlexPosn)))) :+: ((C1 (MetaCons "CommentEnd" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 AlexPosn)) :+: C1 (MetaCons "CommentContents" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 AlexPosn) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String))) :+: (C1 (MetaCons "MacroBlock" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 AlexPosn) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :+: C1 (MetaCons "UintTok" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 AlexPosn) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Word))))) :+: ((C1 (MetaCons "SignatureTok" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 AlexPosn) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :+: (C1 (MetaCons "DoubleParenTok" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 AlexPosn)) :+: C1 (MetaCons "DoubleBracesTok" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 AlexPosn)))) :+: ((C1 (MetaCons "DoubleBracketTok" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 AlexPosn)) :+: C1 (MetaCons "SpecialBracket" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 AlexPosn))) :+: (C1 (MetaCons "FixityTok" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 AlexPosn) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :+: C1 (MetaCons "End" PrefixI False) (U1 :: Type -> Type))))))

data AlexPosn Source #

Constructors

AlexPn !Int !Int !Int 
Instances
Eq AlexPosn Source # 
Instance details

Defined in Language.ATS.Lexer

Show AlexPosn Source # 
Instance details

Defined in Language.ATS.Lexer

Generic AlexPosn Source # 
Instance details

Defined in Language.ATS.Lexer

Associated Types

type Rep AlexPosn :: Type -> Type #

Methods

from :: AlexPosn -> Rep AlexPosn x #

to :: Rep AlexPosn x -> AlexPosn #

Pretty AlexPosn Source # 
Instance details

Defined in Language.ATS.Lexer

Methods

pretty :: AlexPosn -> Doc #

prettyList :: [AlexPosn] -> Doc #

NFData AlexPosn Source # 
Instance details

Defined in Language.ATS.Lexer

Methods

rnf :: AlexPosn -> () #

type Rep AlexPosn Source # 
Instance details

Defined in Language.ATS.Lexer