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


-- | A common library for TheoremQuest, a theorem proving game.
--   
--   TODO
@package theoremquest
@version 0.0.0

module TheoremQuest.Logic
data Term
Const :: String -> Type -> Term
Var :: Variable -> Term
Abs :: Variable -> Term -> Term
Comb :: Term -> Term -> Term

-- | A boolean term.
type Proposition = Term
data Variable
Variable :: String -> Type -> Variable
data Theorem
data Type
Bool :: Type
(:->) :: Type -> Type -> Type
data Inference a
REFL :: Term -> Inference a
TRANS :: a -> a -> Inference a
MK_COMB :: a -> a -> Inference a
ABS :: Term -> a -> Inference a
BETA :: Term -> Inference a
ASSUME :: Term -> Inference a
EQ_MP :: a -> a -> Inference a
DEDUCT_ANTISYM :: a -> a -> Inference a
INST :: [(Variable, Term)] -> a -> Inference a
INST_TYPE :: [(Type, Type)] -> a -> Inference a
AXIOM :: Axiom -> Inference a
data Axiom
Axiom :: Axiom
class TypeOf a
typeOf :: TypeOf a => a -> Type
(=.) :: Term -> Term -> Term

-- | Assumptions of a <a>Theorem</a>.
assumptions :: Theorem -> [Proposition]

-- | Conclusion of a <a>Theorem</a>.
conclusion :: Theorem -> Proposition

-- | Creates a <a>Theorem</a> from an <a>Inference</a> rule application.
inference :: Inference Theorem -> Maybe Theorem

-- | Checks if a term is well-typed.
wellTyped :: Term -> Bool

-- | Checks if a variable is free in a term.
freeIn :: Variable -> Term -> Bool

-- | All free variables in a term.
freeVariables :: Term -> [Variable]
instance Show Axiom
instance Read Axiom
instance Show a => Show (Inference a)
instance Read a => Read (Inference a)
instance Show Type
instance Read Type
instance Show Variable
instance Read Variable
instance Show Term
instance Read Term
instance Eq Term
instance TypeOf Term
instance TypeOf Variable
instance TypeOf Type
instance Eq Type
instance Eq Variable

module TheoremQuest.Transactions

-- | Requests from client to server.
data Req

-- | Ping server.
Ping :: Req

-- | New user: username, email.
NewUser :: User -> Email -> Req

-- | Send response in JSON.
RspInJSON :: Req -> Req

-- | Submit an inference. Server will validate the inference and return a
--   theorem.
Inference :: User -> (Inference TheoremId) -> Req

-- | Request a theorem's assumptions.
TheoremAssumptions :: TheoremId -> Req

-- | Request a theorem's conclusion.
TheoremConclusion :: TheoremId -> Req

-- | Search for a theorem similar to a term. Return a list of ids starting
--   at the given index.
TheoremSearch :: Term -> Int -> Req

-- | Responses to client requests.
data Rsp

-- | A warning to clients that the associated <a>Req</a> will soon be
--   obsolete.
DeprecatedReq :: Rsp -> Rsp

-- | Server did not recognize <a>Req</a>.
UnknownReq :: Rsp

-- | Acknowledge.
Ack :: Rsp

-- | No acknowledge with reason.
Nack :: String -> Rsp

-- | A unique id. Usually a <a>TheoremId</a>.
Id :: Int -> Rsp

-- | A list of unique ids.
Ids :: [Int] -> Rsp

-- | A term.
Term :: Term -> Rsp

-- | A list of terms.
Terms :: [Term] -> Rsp
type User = String
type Email = String
type TheoremId = Int

-- | HTTP headers and body for JSON transfer.
formatJSON :: JSON a => a -> ([Header], String)

-- | HTTP headers and body for text transfer.
formatText :: String -> ([Header], String)

-- | HTTP headers and body for shown Haskell type transfer.
formatHaskell :: Show a => a -> ([Header], String)

-- | Maybe read, on parse errors return Nothing.
maybeRead :: Read a => String -> Maybe a
instance Show Rsp
instance Read Rsp
instance Show Req
instance Read Req
instance JSON Term
instance JSON Rsp

module TheoremQuest