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


-- | A dependently typed core language
--   
--   PiSigma is a small dependently typed language with only very few
--   constructs: Type:Type, Pi-types, Sigma-types, enumerations and a
--   general meachanism for mutual recursion for types and values
--   controlled by lifted types. It is intended as a core language for
--   dependently typed languages like Agda. It has been described in the
--   paper <a>em</a>PiSigma: Dependent Types Without the Sugar<a>/em</a>
--   which has appeared in the proceedings of FLOPS 2010.
@package pisigma
@version 0.2

module Language.PiSigma.Util.String.Parser
type String = ByteString
append :: String -> String -> String
fromString :: String -> String
isPrefixOf :: String -> String -> Bool
lines :: String -> [String]
null :: String -> Bool
readFile :: FilePath -> IO String
span :: (Char -> Bool) -> String -> (String, String)
toString :: String -> String
uncons :: String -> Maybe (Char, String)
unlines :: [String] -> String
instance IsString String

module Language.PiSigma.Util.String.Internal
type String = Text
append :: String -> String -> String
concat :: [String] -> String
fromString :: String -> String
isPrefixOf :: String -> String -> Bool
null :: String -> Bool
putStrLn :: String -> IO ()
toString :: String -> String

module Language.PiSigma.Syntax

-- | The use of Bind indicates the scope of the bound identifier.
type Bind a = (Name, a)
newtype Boxed
Boxed :: (Clos Term) -> Boxed
type Clos a = (a, Scope)
class Closure a
getScope :: (Closure a) => a -> Scope
putScope :: (Closure a) => a -> Scope -> a
data Entry
Decl :: Loc -> Name -> Type -> Entry
Defn :: Loc -> Name -> Term -> Entry

-- | Class <a>Enum</a> defines operations on sequentially ordered types.
--   
--   The <tt>enumFrom</tt>... methods are used in Haskell's translation of
--   arithmetic sequences.
--   
--   Instances of <a>Enum</a> may be derived for any enumeration type
--   (types whose constructors have no fields). The nullary constructors
--   are assumed to be numbered left-to-right by <a>fromEnum</a> from
--   <tt>0</tt> through <tt>n-1</tt>. See Chapter 10 of the <i>Haskell
--   Report</i> for more details.
--   
--   For any type that is an instance of class <a>Bounded</a> as well as
--   <a>Enum</a>, the following should hold:
--   
--   <ul>
--   <li>The calls <tt><a>succ</a> <a>maxBound</a></tt> and <tt><a>pred</a>
--   <a>minBound</a></tt> should result in a runtime error.</li>
--   <li><a>fromEnum</a> and <a>toEnum</a> should give a runtime error if
--   the result value is not representable in the result type. For example,
--   <tt><a>toEnum</a> 7 :: <a>Bool</a></tt> is an error.</li>
--   <li><a>enumFrom</a> and <a>enumFromThen</a> should be defined with an
--   implicit bound, thus:</li>
--   </ul>
--   
--   <tt> enumFrom x = enumFromTo x maxBound enumFromThen x y =
--   enumFromThenTo x y bound where bound | fromEnum y &gt;= fromEnum x =
--   maxBound | otherwise = minBound </tt>
class Enum a
class Env e
emptyE :: (Env e) => e
extE :: (Env e) => e -> PrtInfo -> (Id, e)
setE :: (Env e) => e -> Id -> EnvEntry -> e
getE :: (Env e) => e -> Id -> EnvEntry
prtE :: (Env e) => e -> Id -> PrtInfo
data EnvEntry
Id :: Id -> EnvEntry
Closure :: (Clos Term) -> EnvEntry
type EnvEntries = [(EnvEntry, PrtInfo)]
class GetLoc a
getLoc :: (GetLoc a) => a -> Loc
type Id = Int
type Label = String
data Loc
Unknown :: Loc
Loc :: !String -> !Int -> !Int -> Loc
filename :: Loc -> !String
line :: Loc -> !Int
column :: Loc -> !Int
type Name = String

-- | Neutral terms.
data Ne
NVar :: Id -> Ne
(:..) :: Ne -> (Clos Term) -> Ne
NSplit :: Ne -> (Bind (Bind (Clos Term))) -> Ne
NCase :: Ne -> (Clos [(Label, Term)]) -> Ne
NForce :: Ne -> Ne
NUnfold :: Ne -> (Bind (Clos Term)) -> Ne
data Phrase
Prog :: Prog -> Phrase
Term :: Term -> Phrase

-- | For treating quantifiers in a uniform way.
data PiSigma
Pi :: PiSigma
Sigma :: PiSigma
type Prog = [Entry]
data PrtInfo
PrtInfo :: Name -> Bool -> PrtInfo
name :: PrtInfo -> Name
expand :: PrtInfo -> Bool
newtype Scope
Scope :: [(Name, (Id, Maybe (Clos Type)))] -> Scope
data Term
Var :: Loc -> Name -> Term
Let :: Loc -> Prog -> Term -> Term
Type :: Loc -> Term
Q :: Loc -> PiSigma -> (Type, Bind Type) -> Term
Lam :: Loc -> (Bind Term) -> Term
App :: Term -> Term -> Term
Pair :: Loc -> Term -> Term -> Term
Split :: Loc -> Term -> (Bind (Bind Term)) -> Term
Enum :: Loc -> [Name] -> Term
Label :: Loc -> Label -> Term
Case :: Loc -> Term -> [(Label, Term)] -> Term
Lift :: Loc -> Term -> Term
Box :: Loc -> Term -> Term
Force :: Loc -> Term -> Term
Rec :: Loc -> Term -> Term
Fold :: Loc -> Term -> Term
Unfold :: Loc -> Term -> (Bind Term) -> Term
type Type = Term
data Val
Ne :: Ne -> Val
VType :: Val
VQ :: PiSigma -> (Clos (Type, Bind Type)) -> Val
VLift :: (Clos Type) -> Val
VLam :: (Bind (Clos Term)) -> Val
VPair :: (Clos (Term, Term)) -> Val
VEnum :: [Label] -> Val
VLabel :: Label -> Val
VBox :: Boxed -> Val
VRec :: (Clos Type) -> Val
VFold :: (Clos Term) -> Val

-- | Smart constructor for product.
(-*-) :: Type -> Type -> Type

-- | Smart constructor for function space.
(->-) :: Type -> Type -> Type
emptyScope :: Scope
extendScope :: Scope -> Name -> (Id, Maybe (Clos Type)) -> Scope
label :: Label -> Clos Term

-- | Smart constructor for lambda abstractions.
lam :: [(Loc, Name)] -> Term -> Term
locMessage :: Loc -> String
decls :: Prog -> [Name]
lookupCon :: Scope -> Name -> Maybe (Clos Type)
lookupScope :: Scope -> Name -> Maybe Id

-- | Smart constructor for multiple Pi applications.
pis :: [(Loc, Name)] -> Type -> Type -> Type

-- | Smart constructor for multiple Sigma applications.
sigmas :: [(Loc, Name)] -> Type -> Type -> Type

-- | Smart constructor for split.
split :: Loc -> Term -> (Name, Name) -> Term -> Term
ty :: Clos Type
lty :: Clos Type
tforce :: Clos Type -> Clos Type
tlift :: Clos Type -> Clos Type
instance Show EnvEntry
instance Show Ne
instance Eq Ne
instance Show Val
instance Eq Val
instance Show Boxed
instance Eq Boxed
instance Show Scope
instance Eq Scope
instance Show Term
instance Eq Term
instance Show PiSigma
instance Eq PiSigma
instance Show Entry
instance Eq Entry
instance Show Phrase
instance Eq Phrase
instance Show Loc
instance Env EnvEntries
instance Closure Boxed
instance (Closure a) => Closure (Bind a)
instance Closure (Clos a)
instance (GetLoc a) => GetLoc (Clos a)
instance GetLoc Term
instance GetLoc Entry
instance Eq Loc

module Language.PiSigma.Lexer
type Parser = Parsec String ()
angles :: Parser a -> Parser a
braces :: Parser a -> Parser a
brackets :: Parser a -> Parser a
charLiteral :: Parser Char
colon :: Parser String
comma :: Parser String
commaSep :: Parser a -> Parser [a]
commaSep1 :: Parser a -> Parser [a]
decimal :: Parser Integer
dot :: Parser String
float :: Parser Double
hexadecimal :: Parser Integer
identifier :: Parser String
integer :: Parser Integer
locate :: Parser a -> Parser Loc
location :: Parser Loc
locReserved :: String -> Parser Loc
locReservedOp :: String -> Parser Loc
locSymbol :: String -> Parser Loc
lexeme :: Parser a -> Parser a
natural :: Parser Integer
naturalOrFloat :: Parser (Either Integer Double)
octal :: Parser Integer
operator :: Parser String
parens :: Parser a -> Parser a
reserved :: String -> Parser ()
reservedOp :: String -> Parser ()
semi :: Parser String
semiSep :: Parser a -> Parser [a]
semiSep1 :: Parser a -> Parser [a]
squares :: Parser a -> Parser a
stringLiteral :: Parser String
symbol :: String -> Parser String
tokArr :: Parser Loc
tokForce :: Parser Loc
tokLam :: Parser Loc
tokLift :: Parser Loc
whiteSpace :: Parser ()
instance (Monad m) => Stream String m Char

module Language.PiSigma.Parser
parse :: Parser a -> SourceName -> String -> Either ParseError a
sPhrase :: Parser Phrase
sProg :: Parser Prog
s2Terms :: Parser (Term, Term)
sTerm :: Parser Term

module Language.PiSigma.Evaluate
newtype Eval e a
Eval :: StateT e (ErrorT EvalErr Identity) a -> Eval e a
unEval :: Eval e a -> StateT e (ErrorT EvalErr Identity) a
catchE :: Eval e a -> (EvalErr -> Eval e a) -> Eval e a

-- | Takes a name, a scope, and potentially a type. It extends the
--   environment and the scope with that name.
decl :: (Env e) => Name -> PrtInfo -> Scope -> Maybe (Clos Type) -> Eval e (Id, Scope)
decl' :: (Env e) => Name -> Scope -> Eval e (Id, Scope)
defn' :: (Env e) => Id -> Clos Type -> Eval e ()
force :: (Env e) => Val -> Eval e Val
eval :: (Env e) => (Clos Term) -> Eval e Val
evalProg :: (Env e) => Clos Prog -> Eval e Scope
getEnv :: Eval e e
getId :: Loc -> Name -> Scope -> Eval e Id

-- | Locally updates the environment.
letn :: (Env e) => Id -> EnvEntry -> Eval e a -> Eval e a
letn' :: (Env e) => Id -> Clos Type -> Eval e a -> Eval e a
lookupId :: (Env e) => Id -> Eval e EnvEntry
run :: e -> Eval e a -> Either EvalErr (a, e)
subst :: (Env e) => Bind (Clos Term) -> (Clos Term) -> Eval e (Clos Term)
tdecl :: (Env e) => Name -> Scope -> (Clos Type) -> Eval e (Id, Scope)
instance Monad (Eval e)
instance MonadError EvalErr (Eval e)
instance MonadState e (Eval e)
instance Error EvalErr

module Language.PiSigma.Normalise
quote :: (Nf a b, Env e) => Vars -> a -> Eval e b
nf :: (Nf a b, Env e) => Vars -> a -> Eval e b
instance Nf Ne Term
instance Nf Val Term
instance (Closure a, Nf a b) => Nf (Bind a) (Bind b)
instance Nf Id Term
instance Nf (Clos Term) Term

module Language.PiSigma.Pretty
type Pretty = Pretty (Seq String Char) (Tok String Char)
class Print a
evalPrint :: (Print a, Env e) => a -> Eval e Pretty
fromPretty :: Pretty -> String
instance Print Msg
instance Print Term
instance Print Ne
instance Print (Clos Term)
instance Print Val
instance Print Pretty
instance Print String

module Language.PiSigma.Equality
eq :: (Equal a, Env e) => a -> a -> Eval e ()
instance Equal Ne
instance Equal Id
instance Equal Boxed
instance Equal Val
instance (Equal a, Closure a) => Equal (Bind a)
instance Equal (Clos Term)

module Language.PiSigma.Check
checkProg :: (Env e) => Clos Prog -> Eval e Scope
infer :: (Env e) => Clos Term -> Eval e (Clos Type)