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


-- | A simply typed lambda calculus interpreter, written with GADTs
--   
@package glambda
@version 1.0.1


-- | Utility exports (and re-exports) for glambda. This module is meant to
--   be internal -- do not import it if you are not part of the glambda
--   package!
module Language.Glambda.Util

-- | Convert a <a>Doc</a> to a <a>String</a>
render :: Doc -> String

-- | Convert a <a>Doc</a> to a <a>SimpleDoc</a> for further rendering
toSimpleDoc :: Doc -> SimpleDoc

-- | Enclose a <a>Doc</a> in parens if the flag is <a>True</a>
maybeParens :: Bool -> Doc -> Doc

-- | Synonym for <a>&lt;$&gt;</a>
($$) :: Doc -> Doc -> Doc

-- | More perspicuous synonym for operator precedence
type Prec = Rational

-- | Precedence for top-level printing
topPrec :: Prec

-- | (Inefficiently) strips whitespace from a string
stripWhitespace :: String -> String

-- | Pluck out the nth item from a list, or use a default if the list is
--   too short
nthDefault :: a -> Int -> [a] -> a

-- | Propositional equality. If <tt>a :~: b</tt> is inhabited by some
--   terminating value, then the type <tt>a</tt> is the same as the type
--   <tt>b</tt>. To use this equality in practice, pattern-match on the
--   <tt>a :~: b</tt> to get out the <tt>Refl</tt> constructor; in the body
--   of the pattern-match, the compiler knows that <tt>a ~ b</tt>.
--   
--   <i>Since: 4.7.0.0</i>
data (:~:) (a :: k) (b :: k) :: k -> k -> *
Refl :: (:~:) k a1 a1

-- | Like <a>void</a>
ignore :: Functor f => f a -> f ()
instance Pretty ParseError


-- | Defines types
module Language.Glambda.Type

-- | Representation of a glambda type
data Ty

-- | A function type
Arr :: Ty -> Ty -> Ty
IntTy :: Ty
BoolTy :: Ty

-- | Perhaps convert a string representation of a base type into a
--   <a>Ty</a>
readTyCon :: String -> Maybe Ty

-- | Singleton for a glambda type
data STy :: * -> *
SArr :: STy arg -> STy res -> STy (arg -> res)
SIntTy :: STy Int
SBoolTy :: STy Bool

-- | Singleton for a typing context
data SCtx :: [*] -> *
SNil :: SCtx []
SCons :: STy h -> SCtx t -> SCtx (h : t)

-- | An implicit <a>STy</a>, wrapped up in a class constraint
class ITy ty
sty :: ITy ty => STy ty

-- | The singleton for the empty context
emptyContext :: SCtx []

-- | Convert a <a>Ty</a> into an <a>STy</a>.
refineTy :: Ty -> (forall ty. STy ty -> r) -> r

-- | Convert an <a>STy</a> into a <a>Ty</a>
unrefineTy :: STy ty -> Ty

-- | Compare two <a>STy</a>s for equality.
eqSTy :: STy ty1 -> STy ty2 -> Maybe (ty1 :~: ty2)
instance Eq Ty
instance Pretty (STy ty)
instance Show Ty
instance Pretty Ty
instance ITy Bool
instance ITy Int
instance (ITy arg, ITy res) => ITy (arg -> res)


-- | Defines a lexical token
module Language.Glambda.Token

-- | An <tt>ArithOp ty</tt> is an operator on numbers that produces a
--   result of type <tt>ty</tt>
data ArithOp ty
Plus :: ArithOp Int
Minus :: ArithOp Int
Times :: ArithOp Int
Divide :: ArithOp Int
Mod :: ArithOp Int
Less :: ArithOp Bool
LessE :: ArithOp Bool
Greater :: ArithOp Bool
GreaterE :: ArithOp Bool
Equals :: ArithOp Bool

-- | <a>UArithOp</a> ("unchecked <a>ArithOp</a>") is an existential package
--   for an <a>ArithOp</a>
data UArithOp
UArithOp :: ArithOp ty -> UArithOp

-- | Compare two <a>ArithOp</a>s (potentially of different types) for
--   equality
eqArithOp :: ArithOp ty1 -> ArithOp ty2 -> Bool
uPlus :: UArithOp
uMinus :: UArithOp
uTimes :: UArithOp
uDivide :: UArithOp
uMod :: UArithOp
uLess :: UArithOp
uLessE :: UArithOp
uGreater :: UArithOp
uGreaterE :: UArithOp
uEquals :: UArithOp

-- | A lexed token
data Token
LParen :: Token
RParen :: Token
Lambda :: Token
Dot :: Token
Arrow :: Token
Colon :: Token
ArithOp :: UArithOp -> Token
Int :: Int -> Token
Bool :: Bool -> Token
If :: Token
Then :: Token
Else :: Token
FixT :: Token
Assign :: Token
Semi :: Token
Name :: String -> Token

-- | A lexed token with location information attached
data LToken
L :: SourcePos -> Token -> LToken

-- | Remove location information from an <a>LToken</a>
unLoc :: LToken -> Token

-- | Perhaps extract a <a>UArithOp</a>
unArithOp :: Token -> Maybe UArithOp

-- | Perhaps extract an <a>Int</a>
unInt :: Token -> Maybe Int

-- | Perhaps extract an <a>Bool</a>
unBool :: Token -> Maybe Bool

-- | Perhaps extract a <a>String</a>
unName :: Token -> Maybe String
instance Eq Token
instance Show LToken
instance Pretty LToken
instance Show Token
instance Pretty Token
instance Show UArithOp
instance Pretty UArithOp
instance Show (ArithOp ty)
instance Pretty (ArithOp ty)
instance Eq UArithOp
instance Eq (ArithOp ty)


-- | Pretty-printing expressions. This allows reduction of code duplication
--   between unchecked and checked expressions.
module Language.Glambda.Pretty

-- | A class for expressions that can be pretty-printed
class Pretty exp => PrettyExp exp
prettyExp :: PrettyExp exp => Coloring -> Prec -> exp -> Doc

-- | Convenient implementation of <a>pretty</a>
defaultPretty :: PrettyExp exp => exp -> Doc

-- | Information about coloring in de Bruijn indexes and binders
data Coloring

-- | A <a>Coloring</a> for an empty context
defaultColoring :: Coloring

-- | Print a variable
prettyVar :: Coloring -> Int -> Doc

-- | Print a lambda expression
prettyLam :: PrettyExp exp => Coloring -> Prec -> Maybe Ty -> exp -> Doc

-- | Print an application
prettyApp :: (PrettyExp exp1, PrettyExp exp2) => Coloring -> Prec -> exp1 -> exp2 -> Doc

-- | Print an arithemtic expression
prettyArith :: (PrettyExp exp1, PrettyExp exp2) => Coloring -> Prec -> exp1 -> ArithOp ty -> exp2 -> Doc

-- | Print a conditional
prettyIf :: (PrettyExp exp1, PrettyExp exp2, PrettyExp exp3) => Coloring -> Prec -> exp1 -> exp2 -> exp3 -> Doc

-- | Print a <tt>fix</tt>
prettyFix :: PrettyExp exp => Coloring -> Prec -> exp -> Doc


-- | The Exp GADT. Glambda expressions encoded in an <a>Exp</a> value are
--   *always* well-typed.
module Language.Glambda.Exp

-- | <tt>Exp ctx ty</tt> is a well-typed expression of type <tt>ty</tt> in
--   context <tt>ctx</tt>. Note that a context is a list of types, where a
--   type's index in the list indicates the de Bruijn index of the
--   associated term-level variable.
data Exp :: [*] -> * -> *
Var :: Elem ctx ty -> Exp ctx ty
Lam :: Exp (arg : ctx) res -> Exp ctx (arg -> res)
App :: Exp ctx (arg -> res) -> Exp ctx arg -> Exp ctx res
Arith :: Exp ctx Int -> ArithOp ty -> Exp ctx Int -> Exp ctx ty
Cond :: Exp ctx Bool -> Exp ctx ty -> Exp ctx ty -> Exp ctx ty
Fix :: Exp ctx (ty -> ty) -> Exp ctx ty
IntE :: Int -> Exp ctx Int
BoolE :: Bool -> Exp ctx Bool

-- | <tt>Elem xs x</tt> is evidence that <tt>x</tt> is in the list
--   <tt>xs</tt>. <tt>EZ :: Elem xs x</tt> is evidence that <tt>x</tt> is
--   the first element of <tt>xs</tt>. <tt>ES ev :: Elem xs x</tt> is
--   evidence that <tt>x</tt> is one position later in <tt>xs</tt> than is
--   indicated in <tt>ev</tt>
data Elem :: [a] -> a -> *
EZ :: Elem (x : xs) x
ES :: Elem xs x -> Elem (y : xs) x

-- | Classifies types that can be values of glambda expressions
class GlamVal t where data family Val t
val :: GlamVal t => Val t -> Exp [] t

-- | Pretty-prints a <a>Val</a>. This needs type information to know how to
--   print. Pattern matching gives GHC enough information to be able to
--   find the <a>GlamVal</a> instance needed to construct the
--   <a>PrettyExp</a> instance.
prettyVal :: Val t -> STy t -> Doc

-- | Equality on expressions, needed for testing
eqExp :: Exp ctx1 ty1 -> Exp ctx2 ty2 -> Bool
instance GlamVal ty => PrettyExp (Val ty)
instance GlamVal ty => Pretty (Val ty)
instance PrettyExp (Exp ctx ty)
instance Pretty (Exp ctx ty)
instance GlamVal (a -> b)
instance GlamVal Bool
instance GlamVal Int


-- | Manages the global variables in Glambda
module Language.Glambda.Globals

-- | The global variable environment maps variables to type-checked
--   expressions
data Globals

-- | An empty global variable environment
emptyGlobals :: Globals

-- | Extend a <a>Globals</a> with a new binding
extend :: String -> STy ty -> Exp [] ty -> Globals -> Globals

-- | Lookup a global variable. Fails with <a>throwError</a> if the variable
--   is not bound.
lookupGlobal :: MonadError Doc m => Globals -> String -> (forall ty. STy ty -> Exp [] ty -> m r) -> m r


-- | The Glam monad, allowing for pretty-printed output to the user,
--   failing with an error message, and tracking global variables.
module Language.Glambda.Monad

-- | A monad giving Haskeline-like interaction, access to <a>Globals</a>,
--   and the ability to abort with <a>mzero</a>.
data Glam a

-- | Run a <a>Glam</a> computation
runGlam :: Glam () -> InputT IO ()

-- | Prompt the user for input, returning a string if one is entered. Like
--   <a>getInputLine</a>.
prompt :: String -> Glam (Maybe String)

-- | Abort the <a>Glam</a> monad
quit :: Glam a

-- | Like the <a>Glam</a> monad, but also supporting error messages via
--   <a>Doc</a>s
data GlamE a

-- | Run a <a>GlamE</a> computation
runGlamE :: GlamE a -> Glam (Either Doc a)

-- | Abort the computation with an error
issueError :: Doc -> GlamE a

-- | Hoist an <a>Either</a> into <a>GlamE</a>
eitherToGlamE :: Either String a -> GlamE a

-- | Class for the two glamorous monads
class GlamM m
printDoc :: GlamM m => Doc -> m ()
printLine :: GlamM m => Doc -> m ()
instance Monad Glam
instance Functor Glam
instance Applicative Glam
instance MonadState Globals Glam
instance MonadIO Glam
instance Monad GlamE
instance Functor GlamE
instance Applicative GlamE
instance MonadError Doc GlamE
instance GlamM GlamE
instance GlamM Glam
instance MonadReader Globals GlamE


-- | de Bruijn shifting and substitution
module Language.Glambda.Shift

-- | Convert an expression typed in one context to one typed in a larger
--   context. Operationally, this amounts to de Bruijn index shifting. As a
--   proposition, this is the weakening lemma.
shift :: Exp ts2 ty -> Exp (t : ts2) ty

-- | Substitute the first expression into the second. As a proposition,
--   this is the substitution lemma.
subst :: Exp ts2 s -> Exp (s : ts2) t -> Exp ts2 t


-- | Defines the AST for un-type-checked expressions
module Language.Glambda.Unchecked

-- | Unchecked expression
data UExp

-- | de Bruijn index for a variable
UVar :: Int -> UExp
UGlobal :: String -> UExp
ULam :: Ty -> UExp -> UExp
UApp :: UExp -> UExp -> UExp
UArith :: UExp -> UArithOp -> UExp -> UExp
UCond :: UExp -> UExp -> UExp -> UExp
UFix :: UExp -> UExp
UIntE :: Int -> UExp
UBoolE :: Bool -> UExp
instance PrettyExp UExp
instance Pretty UExp


-- | Defines the Glambda Statement type, which can either be a bare
--   expression or a global variable assignment.
module Language.Glambda.Statement

-- | A statement can either be a bare expression, which will be evaluated,
--   or an assignment to a global variable.
data Statement
BareExp :: UExp -> Statement
NewGlobal :: String -> UExp -> Statement
instance Pretty Statement


-- | Parses tokens into the un-type-checked AST. <a>Parsing</a>, in
--   glambda, also includes name resolution. This all might conceivably be
--   done in a later pass, but there doesn't seem to be an incentive to do
--   so.
module Language.Glambda.Parse

-- | Parse a sequence of semicolon-separated statements, aborting with an
--   error upon failure
parseStmtsG :: [LToken] -> GlamE [Statement]

-- | Parse a sequence of semicolon-separated statements
parseStmts :: [LToken] -> Either String [Statement]

-- | Parse a <a>Statement</a>, aborting with an error upon failure
parseStmtG :: [LToken] -> GlamE Statement

-- | Parse a <a>UExp</a>, aborting with an error upon failure
parseExpG :: [LToken] -> GlamE UExp

-- | Parse a <a>Statement</a>
parseStmt :: [LToken] -> Either String Statement

-- | Parse a <a>UExp</a>
parseExp :: [LToken] -> Either String UExp


-- | Lexes a Glambda program string into a sequence of tokens
module Language.Glambda.Lex

-- | Lex some program text into a list of <a>LToken</a>s, aborting upon
--   failure
lexG :: String -> GlamE [LToken]

-- | Lex some program text into a list of <a>LToken</a>s
lex :: String -> Either String [LToken]


-- | Glambda expression evaluators for checked expressions.
module Language.Glambda.Eval

-- | Evaluate an expression, using big-step semantics.
eval :: Exp [] t -> Val t

-- | Step an expression, either to another expression or to a value.
step :: Exp [] t -> Either (Exp [] t) (Val t)


-- | The glambda typechecker.
module Language.Glambda.Check

-- | Check the given expression, aborting on type errors. The resulting
--   type and checked expression is given to the provided continuation.
--   This is parameterized over the choice of monad in order to support
--   pure operation during testing. <a>GlamE</a> is the canonical choice
--   for the monad.
check :: (MonadError Doc m, MonadReader Globals m) => UExp -> (forall t. STy t -> Exp [] t -> m r) -> m r


-- | Implements a REPL for glambda.
module Language.Glambda.Repl

-- | The glamorous Glambda interpreter
main :: IO ()
instance [overlap ok] Pretty a => Reportable a
instance [overlap ok] Reportable Globals
instance [overlap ok] Reportable ()
instance [overlap ok] Reportable Doc