-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | A source-code formatter for ATS
--   
--   An opinionated source-code formatter for <a>ATS</a>.
@package ats-format
@version 0.1.0.21


-- | Main module for the library
module Language.ATS

-- | This function turns a string into a stream of tokens for the parser.
lexATS :: String -> [Token]
parseATS :: [Token] -> Either ATSError String ATS
printATS :: ATS -> String

-- | Newtype wrapper containing a list of declarations
newtype ATS
ATS :: [Declaration] -> ATS
[unATS] :: ATS -> [Declaration]

-- | Declare something in a scope (a function, value, action, etc.)
data Declaration
Func :: AlexPosn -> Function -> Declaration
Impl :: [Arg] -> Implementation -> Declaration
ProofImpl :: Implementation -> Declaration
Val :: Addendum -> (Maybe Type) -> Pattern -> Expression -> Declaration
PrVal :: Pattern -> Expression -> Declaration
Var :: (Maybe Type) -> Pattern -> (Maybe Expression) -> (Maybe Expression) -> Declaration
AndDecl :: (Maybe Type) -> Pattern -> Expression -> Declaration
Include :: String -> Declaration
Staload :: (Maybe String) -> String -> Declaration
Stadef :: String -> Name -> [Type] -> Declaration
CBlock :: String -> Declaration
RecordType :: String -> [Arg] -> [Universal] -> [(String, Type)] -> Declaration
RecordViewType :: String -> [Arg] -> [Universal] -> [(String, Type)] -> Declaration
TypeDef :: AlexPosn -> String -> [Arg] -> Type -> Declaration
ViewTypeDef :: AlexPosn -> String -> [Arg] -> Type -> Declaration
SumType :: String -> [Arg] -> [Leaf] -> Declaration
[typeName] :: Declaration -> String
[typeArgs] :: Declaration -> [Arg]
[_leaves] :: Declaration -> [Leaf]
SumViewType :: String -> [Arg] -> [Leaf] -> Declaration
[typeName] :: Declaration -> String
[typeArgs] :: Declaration -> [Arg]
[_leaves] :: Declaration -> [Leaf]
AbsType :: AlexPosn -> String -> [Arg] -> (Maybe Type) -> Declaration
AbsViewType :: AlexPosn -> String -> [Arg] -> (Maybe Type) -> Declaration
AbsView :: AlexPosn -> String -> [Arg] -> (Maybe Type) -> Declaration
AbsVT0p :: AlexPosn -> String -> [Arg] -> (Maybe Type) -> Declaration
AbsT0p :: AlexPosn -> String -> Type -> Declaration
ViewDef :: AlexPosn -> String -> [Arg] -> Type -> Declaration
OverloadOp :: AlexPosn -> BinOp -> Name -> Declaration
OverloadIdent :: AlexPosn -> String -> Name -> Declaration
Comment :: String -> Declaration
DataProp :: AlexPosn -> String -> [Arg] -> [DataPropLeaf] -> Declaration
Extern :: AlexPosn -> Declaration -> Declaration
Define :: String -> Declaration
SortDef :: AlexPosn -> String -> Type -> Declaration
AndD :: Declaration -> Declaration -> Declaration
Local :: AlexPosn -> [Declaration] -> [Declaration] -> Declaration
AbsProp :: AlexPosn -> String -> [Arg] -> Declaration
Assume :: Name -> [Arg] -> Expression -> Declaration
TKind :: AlexPosn -> Name -> String -> Declaration
SymIntr :: AlexPosn -> Name -> Declaration
Stacst :: AlexPosn -> Name -> Type -> (Maybe Expression) -> Declaration
PropDef :: AlexPosn -> String -> [Arg] -> Type -> Declaration

-- | A (possibly effectful) expression.
data Expression
Let :: AlexPosn -> ATS -> (Maybe Expression) -> Expression
VoidLiteral :: AlexPosn -> Expression
Call :: Name -> [Type] -> [Type] -> (Maybe Expression) -> [Expression] -> Expression
NamedVal :: Name -> Expression
ListLiteral :: AlexPosn -> String -> Type -> [Expression] -> Expression
If :: Expression -> Expression -> Maybe Expression -> Expression

-- | Expression evaluating to a boolean value
[cond] :: Expression -> Expression

-- | Expression to be returned when true
[whenTrue] :: Expression -> Expression

-- | Expression to be returned when false
[elseExpr] :: Expression -> Maybe Expression
BoolLit :: Bool -> Expression
TimeLit :: String -> Expression
FloatLit :: Float -> Expression
IntLit :: Int -> Expression
UnderscoreLit :: AlexPosn -> Expression
Lambda :: AlexPosn -> LambdaType -> Pattern -> Expression -> Expression
LinearLambda :: AlexPosn -> LambdaType -> Pattern -> Expression -> Expression
Index :: AlexPosn -> Name -> Expression -> Expression
Access :: AlexPosn -> Expression -> Name -> Expression
StringLit :: String -> Expression
CharLit :: Char -> Expression
AtExpr :: Expression -> Expression -> Expression
AddrAt :: AlexPosn -> Expression -> Expression
ViewAt :: AlexPosn -> Expression -> Expression
Binary :: BinOp -> Expression -> Expression -> Expression
Unary :: UnOp -> Expression -> Expression
Case :: AlexPosn -> Addendum -> Expression -> [(Pattern, LambdaType, Expression)] -> Expression
[posE] :: Expression -> AlexPosn
[kind] :: Expression -> Addendum
[val] :: Expression -> Expression

-- | Each <tt>(Pattern, Expression)</tt> pair corresponds to a branch of
--   the 'case' statement
[arms] :: Expression -> [(Pattern, LambdaType, Expression)]
RecordValue :: AlexPosn -> [(String, Expression)] -> (Maybe Type) -> Expression
Precede :: Expression -> Expression -> Expression
FieldMutate :: AlexPosn -> Expression -> String -> Expression -> Expression
[posE] :: Expression -> AlexPosn

-- | Record to modify
[old] :: Expression -> Expression

-- | Field being modified
[field] :: Expression -> String

-- | New value of the field
[new] :: Expression -> Expression
Mutate :: Expression -> Expression -> Expression
Deref :: AlexPosn -> Expression -> Expression
ProofExpr :: AlexPosn -> Expression -> Expression -> Expression
TypeSignature :: Expression -> Type -> Expression
WhereExp :: Expression -> [Declaration] -> Expression
TupleEx :: AlexPosn -> [Expression] -> Expression
While :: AlexPosn -> Expression -> Expression -> Expression
Actions :: ATS -> Expression
Begin :: AlexPosn -> Expression -> Expression
BinList :: BinOp -> [Expression] -> Expression
[_op] :: Expression -> BinOp
[_exprs] :: Expression -> [Expression]
PrecedeList :: [Expression] -> Expression
[_exprs] :: Expression -> [Expression]
FixAt :: PreFunction -> Expression
LambdaAt :: PreFunction -> Expression
ParenExpr :: AlexPosn -> Expression -> Expression

-- | A type for parsed ATS types
data Type
Bool :: Type
Void :: Type
String :: Type
Char :: Type
Int :: Type
Nat :: Type
Addr :: Type
DependentInt :: StaticExpression -> Type
DependentBool :: StaticExpression -> Type
DepString :: StaticExpression -> Type
Double :: Type
Float :: Type
Tuple :: AlexPosn -> [Type] -> Type
Named :: String -> Type
Ex :: Existential -> Type -> Type
ForA :: Universal -> Type -> Type
Dependent :: Name -> [Type] -> Type
Unconsumed :: Type -> Type
AsProof :: Type -> (Maybe Type) -> Type
FromVT :: Type -> Type
MaybeVal :: Type -> Type
T0p :: Addendum -> Type
Vt0p :: Addendum -> Type
At :: AlexPosn -> Type -> Type -> Type
ProofType :: AlexPosn -> Type -> Type -> Type
ConcreteType :: Expression -> Type
RefType :: Type -> Type
ViewType :: AlexPosn -> Type -> Type
FunctionType :: String -> Type -> Type -> Type
NoneType :: AlexPosn -> Type
ImplicitType :: AlexPosn -> Type
ViewLiteral :: Addendum -> Type

-- | A function declaration accounting for all three keywords (???) ATS
--   uses to define them.
data Function
Fun :: PreFunction -> Function
Fn :: PreFunction -> Function
Fnx :: PreFunction -> Function
And :: PreFunction -> Function
PrFun :: PreFunction -> Function
PrFn :: PreFunction -> Function
Praxi :: PreFunction -> Function
CastFn :: PreFunction -> Function

-- | An <tt>implement</tt> declaration
data Implementation
Implement :: AlexPosn -> [Universal] -> [Universal] -> Name -> [Arg] -> Expression -> Implementation
[pos] :: Implementation -> AlexPosn
[preUniversalsI] :: Implementation -> [Universal]

-- | Universal quantifiers
[universalsI] :: Implementation -> [Universal]

-- | Name of the template being implemented
[nameI] :: Implementation -> Name

-- | Arguments
[iArgs] :: Implementation -> [Arg]

-- | Expression holding the function body.
[iExpression] :: Implementation -> Expression

-- | A data type for patterns.
data Pattern
Wildcard :: AlexPosn -> Pattern
PName :: String -> [Pattern] -> Pattern
PSum :: String -> Pattern -> Pattern
PLiteral :: Expression -> Pattern
Guarded :: AlexPosn -> Expression -> Pattern -> Pattern
Free :: Pattern -> Pattern
Proof :: AlexPosn -> [Pattern] -> [Pattern] -> Pattern
TuplePattern :: [Pattern] -> Pattern
AtPattern :: AlexPosn -> Pattern -> Pattern

-- | A name can be qualified (<tt>$UN.unsafefn</tt>) or not
data Name
Unqualified :: String -> Name
Qualified :: AlexPosn -> String -> String -> Name
SpecialName :: AlexPosn -> String -> Name
Functorial :: String -> String -> Name
Unnamed :: AlexPosn -> Name

-- | <tt>~</tt> is used to negate numbers in ATS
data UnOp
Negate :: UnOp

-- | Binary operators on expressions
data BinOp
Add :: BinOp
Mult :: BinOp
Div :: BinOp
Sub :: BinOp
GreaterThan :: BinOp
GreaterThanEq :: BinOp
LessThan :: BinOp
LessThanEq :: BinOp
Equal :: BinOp
NotEqual :: BinOp
LogicalAnd :: BinOp
LogicalOr :: BinOp
StaticEq :: BinOp
Mod :: BinOp
data DataPropLeaf
DataPropLeaf :: [Universal] -> Expression -> (Maybe Expression) -> DataPropLeaf
data Leaf
Leaf :: [Universal] -> String -> [String] -> Maybe Type -> Leaf
[_constructorUniversals] :: Leaf -> [Universal]
[name] :: Leaf -> String
[constructorArgs] :: Leaf -> [String]
[maybeType] :: Leaf -> Maybe Type

-- | An argument to a function.
data Arg
Arg :: (Paired String Type) -> Arg
PrfArg :: Arg -> Arg -> Arg
NoArgs :: Arg

-- | Determines the default behavior for incomplete pattern matches
data Addendum
None :: Addendum
Plus :: Addendum
Minus :: Addendum

-- | A type for the various lambda arrows (<tt>=&gt;</tt>,
--   <tt>=<a>cloref1</a></tt>, etc.)
data LambdaType
Plain :: AlexPosn -> LambdaType
Full :: AlexPosn -> String -> LambdaType
Spear :: AlexPosn -> LambdaType

-- | Wrapper for universal quantifiers (refinement types)
data Universal
Universal :: [Arg] -> Maybe Type -> Maybe StaticExpression -> Universal
[bound] :: Universal -> [Arg]
[typeU] :: Universal -> Maybe Type
[prop] :: Universal -> Maybe StaticExpression

-- | Wrapper for existential quantifiers/types
data Existential
Existential :: [Arg] -> Maybe Type -> Maybe Expression -> Existential
[boundE] :: Existential -> [Arg]
[typeE] :: Existential -> Maybe Type
[propE] :: Existential -> Maybe Expression
data PreFunction
PreF :: Name -> String -> [Universal] -> [Universal] -> [Arg] -> Type -> Maybe StaticExpression -> Maybe Expression -> PreFunction

-- | Function name
[fname] :: PreFunction -> Name

-- | e.g. &lt;&gt; or <a>!wrt</a>
[sig] :: PreFunction -> String

-- | Universal quantifiers making a function generic
[preUniversals] :: PreFunction -> [Universal]

-- | Universal quantifiers/refinement type
[universals] :: PreFunction -> [Universal]

-- | Actual function arguments
[args] :: PreFunction -> [Arg]

-- | Return type
[returnType] :: PreFunction -> Type

-- | Optional termination metric
[termetric] :: PreFunction -> Maybe StaticExpression

-- | Expression holding the actual function body (not present in static
--   templates)
[expression] :: PreFunction -> Maybe Expression
data StaticExpression
StaticVal :: Name -> StaticExpression
StaticBinary :: BinOp -> StaticExpression -> StaticExpression -> StaticExpression
StaticInt :: Int -> StaticExpression
SPrecede :: StaticExpression -> StaticExpression -> StaticExpression
StaticBool :: Bool -> StaticExpression
StaticVoid :: AlexPosn -> StaticExpression
Sif :: StaticExpression -> StaticExpression -> StaticExpression -> StaticExpression
[scond] :: StaticExpression -> StaticExpression
[wwhenTrue] :: StaticExpression -> StaticExpression
[selseExpr] :: StaticExpression -> StaticExpression
SCall :: Name -> [StaticExpression] -> StaticExpression
data Paired a b
Both :: a -> b -> Paired a b
First :: a -> Paired a b
Second :: b -> Paired a b
data Token
Identifier :: AlexPosn -> String -> Token
Keyword :: AlexPosn -> Keyword -> Token
BoolTok :: AlexPosn -> Bool -> Token
IntTok :: AlexPosn -> Int -> Token
FloatTok :: AlexPosn -> Float -> Token
CharTok :: AlexPosn -> Char -> Token
StringTok :: AlexPosn -> String -> Token
Special :: AlexPosn -> String -> Token
CBlockLex :: AlexPosn -> String -> Token
IdentifierSpace :: AlexPosn -> String -> Token
Operator :: AlexPosn -> String -> Token
Arrow :: AlexPosn -> String -> Token
FuncType :: AlexPosn -> String -> Token
CommentLex :: AlexPosn -> String -> Token
MacroBlock :: AlexPosn -> String -> Token
TimeTok :: AlexPosn -> String -> Token
SignatureTok :: AlexPosn -> String -> Token
DoubleParenTok :: AlexPosn -> Token
DoubleBracesTok :: AlexPosn -> Token
DoubleBracketTok :: AlexPosn -> Token
SpecialBracket :: AlexPosn -> Token
data AlexPosn
AlexPn :: !Int -> !Int -> !Int -> AlexPosn
data Keyword
KwFun :: Keyword
KwFnx :: Keyword
KwAnd :: Keyword
KwDatatype :: Keyword
KwDatavtype :: Keyword
KwAssume :: Keyword
KwTypedef :: Keyword
KwVtypedef :: Keyword
KwStaload :: Keyword
KwLet :: Keyword
KwIn :: Keyword
KwLocal :: Keyword
KwEnd :: Keyword
KwImplement :: Keyword
KwCase :: Addendum -> Keyword
KwIf :: Keyword
KwSif :: Keyword
KwThen :: Keyword
KwElse :: Keyword
KwString :: Keyword
KwBool :: Keyword
KwInt :: Keyword
KwVoid :: Keyword
KwNat :: Keyword
KwVal :: Addendum -> Keyword
KwVar :: Keyword
KwLambda :: Keyword
KwLinearLambda :: Keyword
KwInclude :: Keyword
KwWhen :: Keyword
KwOf :: Keyword
KwAbsprop :: Keyword
KwPrval :: Keyword
KwStadef :: Keyword
KwPraxi :: Keyword
KwWhile :: Keyword
KwWhere :: Keyword
KwBegin :: Keyword
KwOverload :: Keyword
KwWith :: Keyword
KwChar :: Keyword
KwDataview :: Keyword
KwDataprop :: Keyword
KwView :: Addendum -> Keyword
KwAbstype :: Keyword
KwType :: Keyword
KwAbst0p :: Addendum -> Keyword
KwAbsvt0p :: Addendum -> Keyword
KwT0p :: Addendum -> Keyword
KwVt0p :: Addendum -> Keyword
KwPrfun :: Keyword
KwPrfn :: Keyword
KwCastfn :: Keyword
KwExtern :: Keyword
KwAbsvtype :: Keyword
KwProofImplement :: Keyword
KwSortdef :: Keyword
KwPropdef :: Keyword
KwRaise :: Keyword
KwTKind :: Keyword
KwMod :: Keyword
KwFixAt :: Keyword
KwLambdaAt :: Keyword
KwAddrAt :: Keyword
KwAddr :: Keyword
KwSta :: Keyword
KwViewAt :: Keyword
KwViewdef :: Keyword
KwSymintr :: Keyword
KwAbsview :: Keyword
KwFn :: Keyword
KwInfix :: Keyword
KwInfixr :: Keyword
KwInfixl :: Keyword
KwStacst :: Keyword
KwListLit :: String -> Keyword
data ATSError a
leaves :: Traversal' Declaration [Leaf]
constructorUniversals :: Lens' Leaf [Universal]
exec :: IO ()