theoremquest (empty) → 0.0.0

raw patch · 6 files changed

+319/−0 lines, 6 filesdep +HTTPdep +basedep +jsonsetup-changed

Dependencies added: HTTP, base, json, utf8-string

Files

• LICENSE +27/−0
• Setup.lhs +8/−0
• TheoremQuest.hs +8/−0
• TheoremQuest/Logic.hs +161/−0
• TheoremQuest/Transactions.hs +81/−0
• theoremquest.cabal +34/−0

@@ -0,0 +1,27 @@+Copyright (c) Tom Hawkins 2011++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions+are met:+1. Redistributions of source code must retain the above copyright+   notice, this list of conditions and the following disclaimer.+2. Redistributions in binary form must reproduce the above copyright+   notice, this list of conditions and the following disclaimer in the+   documentation and/or other materials provided with the distribution.+3. Neither the name of the author nor the names of his contributors+   may be used to endorse or promote products derived from this software+   without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE+ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS+OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)+HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT+LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY+OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF+SUCH DAMAGE.

@@ -0,0 +1,8 @@+#! /usr/bin/env runhaskell++> module Main (main) where+>+> import Distribution.Simple (defaultMain)+>+> main :: IO ()+> main = defaultMain

@@ -0,0 +1,8 @@+module TheoremQuest+  ( module TheoremQuest.Logic+  , module TheoremQuest.Transactions+  ) where++import TheoremQuest.Logic+import TheoremQuest.Transactions+

@@ -0,0 +1,161 @@+module TheoremQuest.Logic+  ( Term          (..)+  , Proposition+  , Variable      (..)+  , Theorem+  , Type          (..)+  , Inference     (..)+  , Axiom         (..)+  , TypeOf        (..)+  , (=.)+  , assumptions+  , conclusion+  , inference+  , wellTyped+  , freeIn+  , freeVariables+  ) where++import Data.List++infix  4 =.+infixr 1 :->++data Term+  = Const String Type+  | Var   Variable+  | Abs   Variable Term+  | Comb  Term Term+  deriving (Show, Read, Eq)++-- | A boolean term.+type Proposition = Term++data Variable = Variable String Type+  deriving (Show, Read)++instance Eq Variable where+  Variable a _ == Variable b _ = a == b++data Theorem = Theorem [Proposition] Proposition++-- | Assumptions of a 'Theorem'.+assumptions :: Theorem -> [Proposition]+assumptions (Theorem a _) = a++-- | Conclusion of a 'Theorem'.+conclusion :: Theorem -> Proposition+conclusion (Theorem _ a) = a++data Type+  = Bool+  | Type :-> Type+  deriving (Show, Read)++instance Eq Type where+  Bool == Bool = True+  (a :-> b) == (x :-> y) = a == x && b == y+  _ == _ = False+++data Inference a+  = REFL           Term+  | TRANS          a a+  | MK_COMB        a a+  | ABS            Term a+  | BETA           Term+  | ASSUME         Term+  | EQ_MP          a a+  | DEDUCT_ANTISYM a a+  | INST           [(Variable, Term)] a+  | INST_TYPE      [(Type, Type)] a+  | AXIOM          Axiom+  deriving (Show, Read)++data Axiom+  = Axiom+  deriving (Show, Read)++class    TypeOf a        where typeOf :: a -> Type+instance TypeOf Type     where typeOf = id+instance TypeOf Variable where typeOf (Variable _ t) = t+instance TypeOf Term where+  typeOf a = case a of+    Const _ t -> t+    Var v -> typeOf v+    Comb f _ -> case typeOf f of+      _ :-> a -> a+      _ -> error "invalid type for Comb"+    Abs (Variable _ t) b -> t :-> typeOf b++(=.) :: Term -> Term -> Term+a =. b = Comb (Comb (Const "=" $ typeOf a :-> typeOf a :-> Bool) a) b+-- XXX Need to better understand mk_eq.++-- | Creates a 'Theorem' from an 'Inference' rule application.+inference :: Inference Theorem -> Maybe Theorem+inference rule = case rule of+  REFL a -> validateTheorem [] (a =. a)+  TRANS (Theorem a1 (Comb (Comb (Const "=" _) a2) a3)) (Theorem b1 (Comb (Comb (Const "=" _) b2) b3)) | a3 == b2 -> validateTheorem (union a1 b1) (a2 =. b3)+  MK_COMB (Theorem a1 (Comb (Comb (Const "=" _) a2) a3)) (Theorem b1 (Comb (Comb (Const "=" _) b2) b3)) -> validateTheorem (union a1 b1) (Comb a2 b2 =. Comb a3 b3)+  ABS (Var x) (Theorem a1 (Comb (Comb (Const "=" _) a2) a3)) | not $ any (freeIn x) a1 -> validateTheorem a1 (Abs x a2 =. Abs x a3)+  BETA a@(Comb (Abs x1 t)(Var x2)) | x1 == x2 -> validateTheorem [] $ a =. t+  ASSUME p -> validateTheorem [p] p+  EQ_MP (Theorem a1 (Comb (Comb (Const "=" _) a2) a3)) (Theorem b1 b2) | a2 == b2 -> validateTheorem (union a1 b1) a3+  DEDUCT_ANTISYM (Theorem a1 a2) (Theorem b1 b2) -> validateTheorem (union (delete b2 a1) (delete a2 b1)) $ a2 =. b2+  INST subs (Theorem assumes prop) -> validateTheorem (map (replace subs) assumes) (replace subs prop)+    where+    replace subs a = case a of+      Const _ _ -> a+      Var v -> case lookup v subs of+        Nothing -> a+	Just t  -> t+      Abs v a -> Abs v $ replace [ (v', t) | (v', t) <- subs, v /= v' ] a+      Comb a b -> Comb (replace subs a) (replace subs b)+  -- INST_TYPE           Theorem [(Type, Type)]+  -- AXIOM               Axiom+  _ -> Nothing++-- | Validates (type checks) a theorem.+validateTheorem :: [Term] -> Term -> Maybe Theorem+validateTheorem assumptions conclusion+  | all (\ t -> wellTyped t && typeOf t == Bool) (conclusion : assumptions) = Just $ Theorem assumptions conclusion+  | otherwise = Nothing++-- | Checks if a term is well-typed.+wellTyped :: Term -> Bool+wellTyped a = wellTyped (freeVariables a) a+  where+  wellTyped :: [Variable] -> Term -> Bool+  wellTyped env a = case a of+    Const _ (_ :-> _) -> False+    Const _ _ -> True+    Var v -> wellTypedVar env v+    Comb fun arg -> case typeOf fun of+      argType :-> _ -> typeOf arg == argType && wellTyped env fun && wellTyped env arg+      _ -> False+    Abs x t -> wellTyped (x : env) t++  wellTypedVar :: [Variable] -> Variable -> Bool+  wellTypedVar [] _ = False+  wellTypedVar (Variable name t : rest) v@(Variable name' t')+    | name == name' = t == t'+    | otherwise = wellTypedVar rest v++-- | Checks if a variable is free in a term.+freeIn :: Variable -> Term -> Bool+freeIn (Variable name _) t = elem name [ n | Variable n _ <- freeVariables t ]++-- | All free variables in a term.+freeVariables :: Term -> [Variable]+freeVariables = nub . variables []+  where+  variables :: [Variable] -> Term -> [Variable]+  variables env a = case a of+    Const _ _ -> []+    Var v+      | elem v env -> []+      | otherwise -> [v]+    Comb a b -> variables env a ++ variables env b+    Abs x a -> variables (x : env) a+

@@ -0,0 +1,81 @@+module TheoremQuest.Transactions+  ( Req (..)+  , Rsp (..)+  , User+  , Email+  , TheoremId+  , formatJSON+  , formatText+  , formatHaskell+  , maybeRead+  ) where++import Codec.Binary.UTF8.String (encodeString)+import Network.HTTP+import Text.JSON++import TheoremQuest.Logic++type User = String+type Email = String+type TheoremId = Int++-- | Requests from client to server.+data Req+  = Ping                                   -- ^ Ping server.+  | NewUser User Email                     -- ^ New user: username, email.+  | RspInJSON Req                          -- ^ Send response in JSON.+  | Inference User (Inference TheoremId)   -- ^ Submit an inference.  Server will validate the inference and return a theorem.+  | TheoremAssumptions TheoremId           -- ^ Request a theorem's assumptions.+  | TheoremConclusion  TheoremId           -- ^ Request a theorem's conclusion.+  | TheoremSearch Term Int                 -- ^ Search for a theorem similar to a term.  Return a list of ids starting at the given index.+  deriving (Show, Read)++-- | Responses to client requests.+data Rsp+  = DeprecatedReq Rsp   -- ^ A warning to clients that the associated 'Req' will soon be obsolete.+  | UnknownReq          -- ^ Server did not recognize 'Req'.+  | Ack                 -- ^ Acknowledge.+  | Nack String         -- ^ No acknowledge with reason.+  | Id Int              -- ^ A unique id.  Usually a 'TheoremId'.+  | Ids [Int]           -- ^ A list of unique ids.+  | Term Term           -- ^ A term.+  | Terms [Term]        -- ^ A list of terms.+  deriving (Show, Read)++instance JSON Rsp where+  readJSON = undefined+  showJSON = undefined+  {-+  showJSON a = case a of+    DeprecatedReq a -> JSArray [JSString $ toJSString "DeprecatedReq", showJSON a]+    UnknownReq      -> JSArray [JSString $ toJSString "UnknownReq"]+    Ack             -> JSArray [JSString $ toJSString "Ack"]+    Nack a          -> JSArray $ map (JSString . toJSString) ["Nack", a]+    -}++instance JSON Term where+  readJSON = undefined+  showJSON = undefined++-- | HTTP headers and body for JSON transfer.+formatJSON :: JSON a => a -> ([Header], String)+formatJSON a = ([Header HdrContentLength $ show $ length msg, Header HdrContentEncoding "UTF-8", Header HdrContentType "application/json"], msg)+  where+  msg = encodeString $ encode a++-- | HTTP headers and body for text transfer.+formatText :: String -> ([Header], String)+formatText a = ([Header HdrContentLength $ show $ length msg, Header HdrContentEncoding "UTF-8", Header HdrContentType "text/plain"], msg)+  where+  msg = encodeString a++-- | HTTP headers and body for shown Haskell type transfer.+formatHaskell :: Show a => a -> ([Header], String)+formatHaskell = formatText . show++-- | Maybe read, on parse errors return Nothing.+maybeRead :: Read a => String -> Maybe a+maybeRead s = case [x | (x,t) <- reads s, ("","") <- lex t] of+  [x] -> Just x+  _ -> Nothing

@@ -0,0 +1,34 @@+name:    theoremquest+version: 0.0.0++category: Game, Formal Methods, Theorem Provers++synopsis: A common library for TheoremQuest, a theorem proving game.++description:+  TODO++author:     Tom Hawkins <tomahawkins@gmail.com>+maintainer: Tom Hawkins <tomahawkins@gmail.com>++build-type:    Simple+cabal-version: >= 1.6++license:      BSD3+license-file: LICENSE++library+  build-depends:     base         >= 4.0    && < 5,+                     HTTP         >= 4000.1 && < 4000.2,+                     utf8-string  >= 0.3   && < 0.4,+                     json         >= 0.4.4  && < 0.5+  exposed-modules:+    TheoremQuest+    TheoremQuest.Logic+    TheoremQuest.Transactions+  ghc-options: -W++source-repository head+  type:     git+  location: git://github.com/tomahawkins/theoremquest.git+