PTQ 0.0.4 → 0.0.5
raw patch · 13 files changed
+653/−422 lines, 13 filesdep +xml
Dependencies added: xml
Files
- PTQ.cabal +7/−7
- README +2/−3
- src/CGIMain.hs +4/−2
- src/Expr.hs +0/−246
- src/IL.hs +319/−0
- src/MP.hs +26/−10
- src/Main.hs +22/−14
- src/P.hs +45/−38
- src/Parser.hs +49/−48
- src/Report.hs +8/−2
- src/ReportHTML.hs +76/−0
- src/Translation.hs +91/−52
- src/Version.hs +4/−0
PTQ.cabal view
@@ -1,5 +1,5 @@ Name: PTQ-Version: 0.0.4+Version: 0.0.5 License: LGPL License-File: COPYING Author: Masahiro Sakai@@ -29,18 +29,18 @@ Main-Is: Main.hs Hs-Source-Dirs: src Other-Modules:- Expr+ IL P Translation Parser Report+ Version Extensions: EmptyDataDecls GADTs MultiParamTypeClasses TypeOperators TypeSynonymInstances- GeneralizedNewtypeDeriving Build-Depends: base >=4 && <5, haskell98, mtl, containers if flag(UTF8Terminal) CPP-Options: "-DUSE_UTF8"@@ -50,11 +50,12 @@ Main-Is: CGIMain.hs Hs-Source-Dirs: src Other-Modules:- Expr+ IL P Translation Parser- Report+ Version+ ReportHTML CGI URLEncoding Extensions:@@ -63,9 +64,8 @@ MultiParamTypeClasses TypeOperators TypeSynonymInstances- GeneralizedNewtypeDeriving CPP- Build-Depends: base >=4 && <5, haskell98, mtl, containers, network+ Build-Depends: base >=4 && <5, haskell98, mtl, containers, network, xml if flag(UTF8CGI) CPP-Options: "-DUSE_UTF8" Build-Depends: utf8-string
README view
@@ -34,9 +34,8 @@ PTQ> quit % -== Simple CGI interface+== CGI interface By locating ptq.cgi, cgi/index.html and cgi/main.html to the place where CGI is executable, you can try it on the web.--Currenly it also runs at ((<URL:http://www.tom.sfc.keio.ac.jp/~sakai/hsPTQ/>)).+Demo site runs at <http://www.tom.sfc.keio.ac.jp/~sakai/hsPTQ/>.
src/CGIMain.hs view
@@ -9,7 +9,8 @@ -- Portability : portable module Main where-import Report++import ReportHTML import CGI import Control.Concurrent @@ -26,4 +27,5 @@ Nothing -> HTTPResponse (textContentType "text/plain" "us-ascii") "(no input)\n" Just s ->- HTTPResponse (textContentType "text/plain" "utf-8") (report s)+ --HTTPResponse (textContentType "text/plain" "utf-8") (report s)+ HTTPResponse (textContentType "text/html" "utf-8") (report s)
− src/Expr.hs
@@ -1,246 +0,0 @@--------------------------------------------------------------------------------- |--- Module : Expr--- Copyright : (c) Masahiro Sakai 2007-2009--- License : BSD3-style (see LICENSE)--- --- Maintainer: masahiro.sakai@gmail.com--- Stability : experimental--- Portability : non-portable--{-# LANGUAGE CPP, GeneralizedNewtypeDeriving #-}-module Expr- ( Op1 (..)- , Op2 (..)- , Binder (..)- , Expr (..)- , Scope (..)- , Name- , lambda- , forall- , exists- , int- , ext- , (<@>)- , abstract- , instantiate- , normalize- , RenderM- , runRenderM- , renderExpr- , renderExprU- ) where--import Control.Monad.RWS-import Data.List---------------------------------------------------------------------------------data Op1 = Not | Box | F | H | Int | Ext deriving (Eq,Show)-data Op2 = And | Or | Imply | Equiv | Id deriving (Eq,Show)-data Binder = Lambda | Forall | Exists deriving (Eq,Show)--infixl 9 :@--data Expr- = FVar Name -- 自由変数- | BVar !Int -- 束縛変数- | Expr :@ Expr -- 関数適用- | Const String -- 定数 (≒自由変数)- | Op1 !Op1 Expr -- 前置演算子- | Op2 !Op2 Expr Expr -- 中置演算子- | Bind !Binder Scope -- 変数束縛--instance Show Expr where-#ifdef USE_UTF8- showsPrec d x = runRenderM (renderExprU d x)-#else- showsPrec d x = runRenderM (renderExpr d x)-#endif--newtype Scope = Sc Expr deriving Show-type Name = String---------------------------------------------------------------------------------lambda :: Name -> Expr -> Expr-lambda name expr = Bind Lambda (abstract name expr)--forall :: Name -> Expr -> Expr-forall name expr = Bind Forall (abstract name expr)--exists :: Name -> Expr -> Expr-exists name expr = Bind Exists (abstract name expr)--int :: Expr -> Expr-int = Op1 Int--ext :: Expr -> Expr-ext = Op1 Ext---- 「a{b}」を「a <@> b」と表記-infixl 9 <@>-(<@>) :: Expr -> Expr -> Expr-fun <@> arg = ext fun :@ arg---------------------------------------------------------------------------------varChange :: (Int -> Name -> Expr) -> (Int -> Int -> Expr) -> Expr -> Expr-varChange f g = h 0- where- h :: Int -> Expr -> Expr- h outer (FVar name) = f outer name- h outer (BVar index) = g outer index- h outer (Bind q (Sc body)) = Bind q (Sc (h (outer+1) body))- h outer (fun :@ arg) = h outer fun :@ h outer arg- h _ (Const s) = Const s- h outer (Op1 op a) = Op1 op (h outer a)- h outer (Op2 op a b) = Op2 op (h outer a) (h outer b)--abstract :: Name -> Expr -> Scope-abstract name expr = Sc (varChange f g expr)- where- f outer name' | name==name' = BVar outer- | otherwise = FVar name'- g outer index | index>=outer = BVar (index+1)- | otherwise = BVar index--instantiate :: Expr -> Scope -> Expr-instantiate image (Sc body) = varChange f g body- where- f _ name = FVar name- g outer index | index==outer = varShift outer image- | index>outer = BVar (index-1)- | otherwise = BVar index---- 外を指している変数のインデックスをずらす-varShift :: Int -> Expr -> Expr-varShift 0 = id-varShift n = varChange f g - where- f _ name = FVar name- g outer index | index>=outer = BVar (index+n)- | otherwise = BVar index--normalize :: Expr -> Expr-normalize (Bind Lambda (Sc body)) =- case normalize body of- f :@ BVar 0 | not (0 `elem` bvs f) -> varShift (-1) f -- η-conversion- body -> Bind Lambda (Sc body)-normalize (Bind q (Sc body)) = Bind q (Sc (normalize body))-normalize (fun :@ arg) =- case normalize fun of- Bind Lambda body -> normalize (instantiate arg' body) -- β-reduction- fun -> fun :@ arg'- where arg' = normalize arg-normalize (Op1 Ext a) =- case normalize a of- Op1 Int b -> b- a' -> Op1 Ext a'-normalize (Op1 op a) = Op1 op (normalize a)-normalize (Op2 op a b) = Op2 op (normalize a) (normalize b)-normalize x = x--bvs :: Expr -> [Int]-bvs (FVar _) = []-bvs (BVar n) = [n]-bvs (f :@ x) = bvs f ++ bvs x-bvs (Const _) = []-bvs (Op1 _ e) = bvs e-bvs (Op2 _ e1 e2) = bvs e1 ++ bvs e2-bvs (Bind b (Sc e)) = [n - 1 | n <- bvs e, n /= 0]---------------------------------------------------------------------------------newtype RenderM a = RenderM (RWS [Name] () Int a)- deriving (Monad, MonadReader [Name])--runRenderM :: RenderM a -> a-runRenderM (RenderM m) = - case runRWS m [] 0 of- (a, _, _) -> a--render :: Bool -> Int -> Expr -> RenderM ShowS-render u = h- where- h d e = case e of- FVar name -> return $ showString name- BVar index -> do- vs <- ask- return $ showString (vs !! index)- Bind q _ -> f d q e- Op1 Ext a :@ b -> do- a' <- h (app_prec+1) a- b' <- h 0 b- return $ showParen (d > app_prec)- $ a' . showString " {" . b' . showChar '}'- a :@ b -> do - a' <- h app_prec a- b' <- h (app_prec+1) b- return $ showParen (d > app_prec) $ a' . showChar ' ' . b'- Const s -> return $ showString s- Op1 op a -> do- t <- h (prec+1) a- return $ showParen (d > prec)- $ showString s . t- where- s = case op of- Not -> if u then "¬" else "not " -- ¬ (U+00AC)- Box -> if u then "◻" else "[]" -- ◻ (U+25FB) が正しそうだが □ (U+25A1) を使うのが無難か?- F -> "F "- H -> "H "- Int -> if u then "˄" else "Int " -- ˄ (U+02C4)- Ext -> if u then "˅" else "Ext " -- ˅ (U+02C5)- prec = case op of- Int | u -> app_prec + 1- Ext | u -> app_prec + 1- _ -> app_prec- Op2 op a b -> do- a' <- h (l prec) a- b' <- h (r prec) b- return $ showParen (d > prec)- $ a' . showChar ' ' . showString s . showChar ' ' . b'- where- (s,prec,l,r) =- case op of- And -> (if u then "∧" else "&&", 4, id, id) -- ∧ (U+2227)- Or -> (if u then "∨" else "||", 3, id, id) -- ∨ (U+2228)- Imply -> (if u then "→" else "->", 1, (+1), id) -- → (U+2192)- Equiv -> (if u then "↔" else "<->", 1, (+1), (+1)) -- ↔ (U+2194)- Id -> ("=", 2, (+1), (+1))-- f :: Int -> Binder -> Expr -> RenderM ShowS- f d b e = do- (xs, s) <- go e- return $ showParen (d > 0) $- showString (g b) . showString (intercalate " " xs) . showString ". " . s- where- go :: Expr -> RenderM ([Name], ShowS)- go (Bind b' (Sc body)) | b==b' = do- x <- gensym - (xs, s) <- local (x:) $ go body- return (x:xs, s)- go e = do- s <- h 0 e- return ([], s)-- g :: Binder -> String- g Lambda = if u then "λ" else "\\" -- λ (U+03BB)- g Forall = if u then "∀" else "forall " -- ∀ (U+2200)- g Exists = if u then "∃" else "exists " -- ∃ (U+2203)---renderExpr :: Int -> Expr -> RenderM ShowS-renderExpr = render False--renderExprU :: Int -> Expr -> RenderM ShowS-renderExprU = render True--app_prec :: Int-app_prec = 10--gensym :: RenderM Name-gensym = RenderM $ do - i <- get- put (i+1)- return ("x"++show i)
+ src/IL.hs view
@@ -0,0 +1,319 @@+-----------------------------------------------------------------------------+-- |+-- Module : IL+-- Copyright : (c) Masahiro Sakai 2007-2009+-- License : BSD3-style (see LICENSE)+-- +-- Maintainer: masahiro.sakai@gmail.com+-- Stability : experimental+-- Portability : non-portable++{-# LANGUAGE CPP #-}+module IL+ ( Type (..)+ , renderType+ , Op1 (..)+ , Op2 (..)+ , Binder (..)+ , Expr (..)+ , Scope (..)+ , Name+ , lambda+ , forall+ , exists+ , int+ , ext+ , (<@>)+ , abstract+ , instantiate+ , normalize+ , renderExpr+ , typeCheck+ ) where++import Control.Monad.RWS+import Data.List+import Data.Monoid+import Data.Function++-- --------------------------------------------------------------------------++infixr 0 :->++data Type+ = Prop+ | E+ | S Type+ | (:->) Type Type+ deriving (Eq, Ord)++instance Show Type where+#ifdef USE_UTF8+ showsPrec = renderType True+#else+ showsPrec = renderType False+#endif++renderType :: Bool -> Int -> Type -> ShowS+renderType unicode = f+ where+ f _ Prop = showString "t"+ f _ E = showString "e"+ f d (S t) = showParen (d > 0) $ showString "s" . arr . f 0 t+ f d (t1 :-> t2) = showParen (d > 0) $ f 1 t1 . arr . f 0 t2+ arr = if unicode then showString "→" else showString "->"++-- --------------------------------------------------------------------------++infixl 9 :@++data Expr+ = FVar Name -- 自由変数+ | BVar !Int -- 束縛変数+ | Expr :@ Expr -- 関数適用+ | Const Name -- 定数 (≒自由変数)+ | Op1 !Op1 Expr -- 前置演算子+ | Op2 !Op2 Expr Expr -- 中置演算子+ | Bind !Binder Type Scope -- 変数束縛++data Op1 = Not | Box | F | H | Int | Ext deriving (Eq,Ord,Show)+data Op2 = And | Or | Imply | Equiv | Id deriving (Eq,Ord,Show)+data Binder = Lambda | Forall | Exists deriving (Eq,Ord,Show)++newtype Scope = Sc Expr deriving Show+type Name = (String, Type)++instance Show Expr where+#ifdef USE_UTF8+ showsPrec = renderExpr True False+#else+ showsPrec = renderExpr False False+#endif++lambda :: Name -> Expr -> Expr+lambda name expr = Bind Lambda (snd name) (abstract name expr)++forall :: Name -> Expr -> Expr+forall name expr = Bind Forall (snd name) (abstract name expr)++exists :: Name -> Expr -> Expr+exists name expr = Bind Exists (snd name) (abstract name expr)++int :: Expr -> Expr+int = Op1 Int++ext :: Expr -> Expr+ext = Op1 Ext++-- 「a{b}」を「a <@> b」と表記+infixl 9 <@>+(<@>) :: Expr -> Expr -> Expr+fun <@> arg = ext fun :@ arg++varChange :: (Int -> Name -> Expr) -> (Int -> Int -> Expr) -> Expr -> Expr+varChange f g = h 0+ where+ h :: Int -> Expr -> Expr+ h outer (FVar name) = f outer name+ h outer (BVar index) = g outer index+ h outer (Bind q t (Sc body)) = Bind q t (Sc (h (outer+1) body))+ h outer (fun :@ arg) = h outer fun :@ h outer arg+ h _ (Const s) = Const s+ h outer (Op1 op a) = Op1 op (h outer a)+ h outer (Op2 op a b) = Op2 op (h outer a) (h outer b)++abstract :: Name -> Expr -> Scope+abstract name expr = Sc (varChange f g expr)+ where+ f outer name' | name==name' = BVar outer+ | otherwise = FVar name'+ g outer index | index>=outer = BVar (index+1)+ | otherwise = BVar index++instantiate :: Expr -> Scope -> Expr+instantiate image (Sc body) = varChange f g body+ where+ f _ name = FVar name+ g outer index | index==outer = varShift outer image+ | index>outer = BVar (index-1)+ | otherwise = BVar index++-- 外を指している変数のインデックスをずらす+varShift :: Int -> Expr -> Expr+varShift 0 = id+varShift n = varChange f g + where+ f _ name = FVar name+ g outer index | index>=outer = BVar (index+n)+ | otherwise = BVar index++normalize :: Expr -> Expr+normalize (Bind Lambda t (Sc body)) =+ case normalize body of+ f :@ BVar 0 | not (0 `elem` bvs f) -> varShift (-1) f -- η-conversion+ body' -> Bind Lambda t (Sc body')+normalize (Bind q t (Sc body)) = Bind q t (Sc (normalize body))+normalize (fun :@ arg) =+ case normalize fun of+ Bind Lambda t body -> normalize (instantiate arg' body) -- β-reduction+ fun' -> fun' :@ arg'+ where arg' = normalize arg+normalize (Op1 Ext a) =+ case normalize a of+ Op1 Int b -> b+ a' -> Op1 Ext a'+normalize (Op1 op a) = Op1 op (normalize a)+normalize (Op2 op a b) = Op2 op (normalize a) (normalize b)+normalize x = x++bvs :: Expr -> [Int]+bvs (FVar _) = []+bvs (BVar n) = [n]+bvs (f :@ x) = bvs f ++ bvs x+bvs (Const _) = []+bvs (Op1 _ e) = bvs e+bvs (Op2 _ e1 e2) = bvs e1 ++ bvs e2+bvs (Bind _ _ (Sc e)) = [n - 1 | n <- bvs e, n /= 0]++-- --------------------------------------------------------------------------++type RenderM = RWS [Name] () Int++renderExpr :: Bool -> Bool -> Int -> Expr -> ShowS+renderExpr unicode uncurrying d e =+ case runRWS (h d e) [] 0 of+ (a, _, _) -> a+ where+ h d e = case e of+ FVar name -> return $ showString (fst name)+ BVar index -> do+ vs <- ask+ return $ showString $ fst (vs !! index)+ Bind q _ _ -> f d q e+ a :@ b | uncurrying -> f a [b]+ where+ f (e1 :@ e2) xs = f e1 (e2:xs)+ f e xs = uncurriedApp e xs+ Op1 Ext a :@ b -> do+ a' <- h (app_prec+1) a+ b' <- h 0 b+ return $ showParen (d > app_prec)+ $ a' . showString " {" . b' . showChar '}'+ a :@ b -> do + a' <- h app_prec a+ b' <- h (app_prec+1) b+ return $ showParen (d > app_prec) $ a' . showChar ' ' . b'+ Const s -> return $ showString (fst s)+ Op1 op a -> do+ t <- h (prec+1) a+ return $ showParen (d > prec)+ $ showString s . t+ where+ s = case op of+ Not -> if unicode then "¬" else "not " -- ¬ (U+00AC)+ Box -> if unicode then "◻" else "[]" -- ◻ (U+25FB) が正しそうだが □ (U+25A1) を使うのが無難か?+ F -> "F "+ H -> "H "+ Int -> if unicode then "˄" else "Int " -- ˄ (U+02C4)+ Ext -> if unicode then "˅" else "Ext " -- ˅ (U+02C5)+ prec = case op of+ Int | unicode -> app_prec + 1+ Ext | unicode -> app_prec + 1+ _ -> app_prec+ Op2 op a b -> do+ a' <- h (l prec) a+ b' <- h (r prec) b+ return $ showParen (d > prec)+ $ a' . showChar ' ' . showString s . showChar ' ' . b'+ where+ (s,prec,l,r) =+ case op of+ And -> (if unicode then "∧" else "&&", 4, id, id) -- ∧ (U+2227)+ Or -> (if unicode then "∨" else "||", 3, id, id) -- ∨ (U+2228)+ Imply -> (if unicode then "→" else "->", 1, (+1), id) -- → (U+2192)+ Equiv -> (if unicode then "↔" else "<->", 1, (+1), (+1)) -- ↔ (U+2194)+ Id -> ("=", 5, (+1), (+1))++ f :: Int -> Binder -> Expr -> RenderM ShowS+ f d b e = do+ (xs, s) <- go e+ let b' = case b of+ Lambda -> if unicode then "λ" else "\\" -- λ (U+03BB)+ Forall -> if unicode then "∀" else "forall " -- ∀ (U+2200)+ Exists -> if unicode then "∃" else "exists " -- ∃ (U+2203)+ ys :: [(Type, [String])]+ ys = [(snd (head ys), map fst ys) | ys <- groupBy ((==) `on` snd) xs]+ ws :: [String]+ ws = [intercalate ", " zs ++ " : "++ renderType unicode 0 t "" | (t, zs) <- ys]+ return $ showParen (d > 0) $+ showString b' . showString (intercalate ", " ws) . showString ". " . s+ where+ go :: Expr -> RenderM ([Name], ShowS)+ go (Bind b' t (Sc body)) | b==b' = do+ x <- gensym t+ (xs, s) <- local (x:) $ go body+ return (x:xs, s)+ go e = do+ s <- h 0 e+ return ([], s)++ uncurriedApp :: Expr -> [Expr] -> RenderM ShowS+ uncurriedApp e xs = do+ bs <- mapM (liftM Endo . h 0) $ reverse xs+ let cs = appEndo $ mconcat $ intersperse (Endo (showString ", ")) bs+ case e of+ Op1 Ext e2 -> do+ a <- h (app_prec+1) e2+ return $ showParen (d > app_prec)+ $ a . showString "{" . cs . showChar '}'+ _ -> do+ a <- h (app_prec+1) e+ return $ showParen (d > app_prec)+ $ a . showString "(" . cs . showChar ')'++app_prec :: Int+app_prec = 10++gensym :: Type -> RenderM Name+gensym t = do + i <- get+ put (i+1)+ return ("x"++show i, t)++-- ---------------------------------------------------------------------------++typeCheck ::[Type] -> Expr -> Maybe Type+typeCheck = f+ where+ f _ (FVar (_,t)) = return t+ f env (BVar n) = return (env !! n)+ f env (e1 :@ e2) = do+ (t1 :-> t2) <- f env e1+ t3 <- f env e2+ guard $ t1 == t3+ return t2+ f env (Const (_,t)) = return t+ f env (Op1 Ext e) = do+ S t <- f env e+ return t+ f env (Op1 Int e) = do+ t <- f env e+ return (S t)+ f env (Op1 op e) = do+ Prop <- f env e+ return Prop+ f env (Op2 Id e1 e2) = do+ t1 <- f env e1+ t2 <- f env e2+ guard $ t1 == t2+ return Prop+ f env (Op2 op e1 e2) = do+ Prop <- f env e1+ Prop <- f env e2+ return Prop+ f env (Bind Lambda t (Sc e)) = do+ t2 <- f (t:env) e+ return (t :-> t2)+ f env (Bind b t (Sc e)) = do+ Prop <- f (t:env) e+ return Prop
src/MP.hs view
@@ -12,22 +12,38 @@ ( applyMP ) where-import Expr+import P+import IL+import Translation (catToType) applyMP :: Expr -> Expr -- MP1 -- MP4-applyMP (Const tv) | tv `elem` ["find","lose","eat","love"] =- lambda "p" $ lambda "x" $- FVar "p" <@> (int $ lambda "y" $ Const tv :@ int (lambda "P" $ FVar "P" <@> FVar "y") :@ FVar "x")+applyMP (Const tv) | fst tv `elem` ["find","lose","eat","love"] =+ lambda p $ lambda x $+ FVar p <@> (int $ lambda y $ int (Const tv') <@> FVar y :@ FVar x)+ where+ tv' = (fst tv ++ "*", E :-> E :-> Prop)+ p = ("p", S ((S (E :-> Prop)) :-> Prop))+ x = ("x", E)+ y = ("y", E) -- MP8-applyMP (Const "in") =- lambda "p" $ lambda "P" $ lambda "x" $- FVar "p" <@> (int $ lambda "y" $ Const "in" :@ int (lambda "z" $ FVar "z" <@> FVar "y") :@ FVar "P" :@ FVar "x")+applyMP (Const ("in",_)) =+ lambda p $ lambda pp $ lambda x $+ FVar p <@> (int $ lambda y $ int (Const in') <@> FVar y :@ FVar pp :@ FVar x)+ where+ in' = ("in*", E :-> (S (E :-> Prop)) :-> E :-> Prop)+ p = ("p", S ((S (E :-> Prop)) :-> Prop))+ pp = ("P", S (E :-> Prop))+ x = ("x", E)+ y = ("y", E) -- MP9-applyMP (Const "seek") = lambda "P" $ Const "try" :@ int (find' :@ FVar "P")- where find' = applyMP (Const "find")-applyMP (Bind q (Sc body)) = Bind q (Sc (applyMP body))+applyMP (Const ("seek",_)) = lambda p $ Const try' :@ int (find' :@ FVar p)+ where+ try' = ("try", catToType (IV :// IV))+ find' = applyMP (Const ("find", catToType (cat :: Cat TV)))+ p = ("P", S ((S (E :-> Prop)) :-> Prop))+applyMP (Bind q t (Sc body)) = Bind q t (Sc (applyMP body)) applyMP (fun :@ arg) = applyMP fun :@ applyMP arg applyMP (Op1 op a) = Op1 op (applyMP a) applyMP (Op2 op a b) = Op2 op (applyMP a) (applyMP b)
src/Main.hs view
@@ -11,26 +11,34 @@ {-# LANGUAGE CPP #-} module Main where import Report+import Version #ifdef USE_UTF8-import Prelude hiding (putStr, getLine)-import System.IO hiding (putStr, getLine)+import Prelude hiding (putStr, putStrLn, getLine)+import System.IO (stdout, hSetBuffering, BufferMode (..)) import System.IO.UTF8 #else import System.IO #endif main :: IO ()-main =- do -- FIXME: バナーを表示- hSetBuffering stdout NoBuffering- loop+main = do+ putStrLn banner+ hSetBuffering stdout NoBuffering+ loop +banner :: String+banner = unlines+ [ "PTQ version " ++ versionStr+ , ""+ , "Type :quit to quit"+ ]+ loop :: IO ()-loop = - do putStr "PTQ> "- s <- getLine- case s of- "quit" -> return ()- _ -> do - putStr (report s)- loop+loop = do+ putStr "PTQ> "+ s <- getLine+ case s of+ ":quit" -> return ()+ _ -> do+ putStr (report s)+ loop
src/P.hs view
@@ -19,33 +19,24 @@ , (:/) , (://) , Cat (..)- , cat_Sen- , cat_IV- , cat_CN- , cat_Adj+ , CatType (..) , T , TV , IAV- , cat_T- , cat_TV- , cat_IAV , Det , DTV , TTV , PP- , cat_Det- , cat_DTV- , cat_PP , PronounNo , P (..) , PAny (..) , F5 , F6- , F8 (..)- , F9 (..)- , F10 (..)+ , F8+ , F9+ , F10+ , catOf ) where-import Expr ----------------------------------------------------------------------------- @@ -68,26 +59,39 @@ Adj :: Cat Adj (:/) :: Cat a -> Cat b -> Cat (a :/ b) (://) :: Cat a -> Cat b -> Cat (a :// b)-cat_Sen = Sen-cat_IV = IV-cat_CN = CN-cat_Adj = Adj +class CatType a where+ cat :: Cat a+instance CatType Sen where+ cat = Sen+instance CatType IV where+ cat = IV+instance CatType CN where+ cat = CN+instance CatType Adj where+ cat = Adj+instance (CatType a, CatType b) => CatType (a :/ b) where+ cat = cat :/ cat+instance (CatType a, CatType b) => CatType (a :// b) where+ cat = cat :// cat++instance Show (Cat a) where+ showsPrec _ Sen = showString "t"+ showsPrec _ IV = showString "IV"+ showsPrec _ CN = showString "CN"+ showsPrec _ Adj = showString "Adj"+ showsPrec d (a :/ b) = showParen (d > 0) $ showsPrec 1 a . showString " / " . showsPrec 1 b+ showsPrec d (a :// b) = showParen (d > 0) $ showsPrec 1 a . showString " // " . showsPrec 1 b+ type T = Sen :/ IV -- 名詞句, 固有名詞: John, he type TV = IV :/ T -- 他動詞(句): find type IAV = IV :/ IV -- 動詞句修飾の副詞(句): slowly-cat_T = cat_Sen :/ cat_IV-cat_TV = cat_IV :/ cat_T-cat_IAV = cat_IV :/ cat_IV -- FIXME: 定義が載っていなかった範疇 type Det = T :/ CN -- 冠詞 type DTV = TV :/ T -- ditransitive verb : 名詞句を２つ取る他動詞 type TTV = TV :/ T -- to transitive verb : DTVと名詞句の順序が逆? type PP = IV :/ TV -- prepositional phrase?: by John-cat_Det = cat_T :/ cat_CN-cat_DTV = cat_TV :/ cat_T-cat_PP = cat_IV :/ cat_TV ----------------------------------------------------------------------------- @@ -127,29 +131,32 @@ F25 :: P TV -> P Adj data PAny where- PAny :: P a -> PAny+ PAny :: CatType c => P c -> PAny -class F5 c +class CatType c => F5 c instance F5 IV -- T5 instance F5 IAV -- T6 -class F6 c a+class (CatType c, CatType a) => F6 c a instance F6 Sen Sen -- T9 instance F6 IV Adj -- T18 -class F8 c where f8 :: Cat c-instance F8 Sen where f8 = cat_Sen-instance F8 IV where f8 = cat_IV+class CatType c => F8 c+instance F8 Sen+instance F8 IV -class F9 c where f9 :: Cat c-instance F9 Sen where f9 = cat_Sen-instance F9 IV where f9 = cat_IV-instance F9 T where f9 = cat_T+class CatType c => F9 c+instance F9 Sen+instance F9 IV+instance F9 T -class F10 c where f10 :: Cat c-instance F10 Sen where f10 = cat_Sen-instance F10 CN where f10 = cat_CN-instance F10 IV where f10 = cat_IV+class CatType c => F10 c+instance F10 Sen+instance F10 CN+instance F10 IV++catOf :: CatType c => P c -> Cat c+catOf _ = cat -----------------------------------------------------------------------------
src/Parser.hs view
@@ -15,7 +15,7 @@ import Control.Monad import qualified Data.IntSet as IS -import P hiding (f8,f9,f10)+import P ----------------------------------------------------------------------------- -- パーサのコア部分@@ -146,10 +146,10 @@ do s <- getF10State putF10State [] (x,a) <- localS3 ([(n,g) | (n,g,_,_)<-s]++) p- x <- introF10s x+ x' <- introF10s x s' <- getF10State putF10State (s'++s)- return (x,a)+ return (x',a) introF10 :: F10 c => P c -> Parser (P c) introF10 x =@@ -209,12 +209,11 @@ parseAny :: String -> [PAny] parseAny s = concat $ [ f p_Det, f (liftM fst p_CN), f p_IAV_T, f p_t_t, f p_t, f p_Adj, f p_PP- , f p_IAV, f p_PP_T ] ++- [ f (p_T x) | x <- [Subject, Object] ] +++ , f p_IAV, f p_PP_T, f (p_T [Subject, Object]) ] ++ [ concat [ f (p_IV x), f (p_TV x), f (p_IV__IV x), f (p_DTV x), f (p_IV_t x) , f (p_IV_Adj x)] | x <- vfs ] where- f :: Parser (P a) -> [PAny]+ f :: CatType a => Parser (P a) -> [PAny] f p = map PAny (parse' p s) vfs :: [VerbForm] vfs = [VFOrig, VFPastParticiple] ++ [f True | f <- [VFPresent, VFFuture, VFPerfect]]@@ -241,7 +240,7 @@ p_Det :: Parser (P Det) p_Det = do x@(B _ s) <- s1_Det- let x' = if s=="an" then B cat_Det "a" else x -- XXX+ let x' = if s=="an" then B (cat :: Cat Det) "a" else x -- XXX -- FIXME: anの場合には次の語が母音で始まるかチェック return $ x' @@ -252,25 +251,27 @@ return (zeta,g) -- FIXME: 全ての組み合わせを網羅している?-p_T :: Case -> Parser (P T)-p_T c = chainr1 (p <|> he_n c) f9 -- S13+p_T :: [Case] -> Parser (P T)+p_T cs = chainr1 (p <|> he_n cs) f9 -- S13 where p = do (x,g) <- s1_T <|> s2 return x <|> asPronoun g x -- He_n-he_n :: Case -> Parser (P T)-he_n c =- do g <- case c of- Subject -> - msum [ token "he" >> return Masculine- , token "she" >> return Feminine- , token "it" >> return Neuter- ]- Object ->- msum [ token "him" >> return Masculine- , token "her" >> return Feminine- , token "it" >> return Neuter- ]+he_n :: [Case] -> Parser (P T)+he_n cs =+ do g <- mplus+ (if Subject `elem` cs+ then msum [ token "he" >> return Masculine+ , token "she" >> return Feminine+ , token "it" >> return Neuter+ ]+ else mzero)+ (if Object `elem` cs+ then msum [ token "him" >> return Masculine+ , token "her" >> return Feminine+ , token "it" >> return Neuter+ ]+ else mzero) xs <- getF10State ys <- askS3 let ns = [(n,g') | (n, g', _, _) <- xs] ++ ys@@ -409,8 +410,8 @@ | VFPerfect !Bool -- 三人称単数現在完了系とその否定形 {-# INLINE verbParser #-}-verbParser :: Cat c -> [VerbEntry] -> VerbForm -> Parser (P c)-verbParser cat dict vf =+verbParser :: CatType c => [VerbEntry] -> VerbForm -> Parser (P c)+verbParser dict vf = do s <- verbParser' dict vf return (B cat s) @@ -475,12 +476,12 @@ ] {-# INLINE nounParser #-}-nounParser :: Cat c -> [NounEntry] -> Parser (P c, Gender)-nounParser c dict =+nounParser :: CatType c => [NounEntry] -> Parser (P c, Gender)+nounParser dict = do x <- anyToken case lookup x dict of Nothing -> mzero- Just g -> return (B c x, g)+ Just g -> return (B cat x, g) ----------------------------------------------------------------------------- -- それ以外の基本表現の辞書とパーサ@@ -509,8 +510,8 @@ dict_PP_T = ["by"] {-# INLINE dictParser #-}-dictParser :: Cat c -> [String] -> Parser (P c)-dictParser cat dict =+dictParser :: CatType c => [String] -> Parser (P c)+dictParser dict = do x <- anyToken guard $ x `elem` dict return $ B cat x@@ -519,43 +520,43 @@ -- 各統語規則のパーサ s1_IV :: VerbForm -> Parser (P IV)-s1_IV = verbParser cat_IV dict_IV+s1_IV = verbParser dict_IV s1_TV :: VerbForm -> Parser (P TV)-s1_TV = verbParser cat_TV dict_TV+s1_TV = verbParser dict_TV s1_IV_t :: VerbForm -> Parser (P (IV :/ Sen))-s1_IV_t = verbParser (cat_IV :/ cat_Sen) dict_IV_t+s1_IV_t = verbParser dict_IV_t s1_IV__IV :: VerbForm -> Parser (P (IV :// IV))-s1_IV__IV = verbParser (cat_IV :// cat_IV) dict_IV__IV+s1_IV__IV = verbParser dict_IV__IV s1_IV_Adj :: VerbForm -> Parser (P (IV :/ Adj))-s1_IV_Adj = verbParser (cat_IV :/ cat_Adj) dict_IV_Adj+s1_IV_Adj = verbParser dict_IV_Adj s1_T :: Parser (P T, Gender)-s1_T = nounParser cat_T dict_T+s1_T = nounParser dict_T s1_CN :: Parser (P CN, Gender)-s1_CN = nounParser cat_CN dict_CN+s1_CN = nounParser dict_CN s1_IAV :: Parser (P IAV)-s1_IAV = dictParser cat_IAV dict_IAV+s1_IAV = dictParser dict_IAV s1_t_t :: Parser (P (Sen :/ Sen)) -s1_t_t = dictParser (cat_Sen :/ cat_Sen) dict_t_t+s1_t_t = dictParser dict_t_t s1_IAV_T :: Parser (P (IAV :/ T))-s1_IAV_T = dictParser (cat_IAV :/ cat_T) dict_IAV_T+s1_IAV_T = dictParser dict_IAV_T s1_Adj :: Parser (P Adj)-s1_Adj = dictParser cat_Adj dict_Adj+s1_Adj = dictParser dict_Adj s1_Det :: Parser (P Det)-s1_Det = dictParser cat_Det dict_Det+s1_Det = dictParser dict_Det s1_PP_T :: Parser (P (PP :/ T))-s1_PP_T = dictParser (cat_PP :/ cat_T) dict_PP_T+s1_PP_T = dictParser dict_PP_T s2 :: Parser (P T, Gender) s2 =@@ -579,7 +580,7 @@ s4_or_s17 :: Parser (P Sen) s4_or_s17 =- do alpha <- p_T Subject+ do alpha <- p_T [Subject] msum [ do delta <- p_IV (VFPresent True) return (F4 alpha delta) -- 三人称単数現在形 (S4) , do delta <- p_IV (VFPresent False) @@ -597,13 +598,13 @@ s5 :: VerbForm -> Parser (P IV) s5 vf = do delta <- p_TV vf- beta <- p_T Object+ beta <- p_T [Object] return (F5 delta beta) s6 :: Parser (P IAV) s6 = do delta <- p_IAV_T- beta <- p_T Object+ beta <- p_T [Object] return (F5 delta beta) s7 :: VerbForm -> Parser (P IV)@@ -656,13 +657,13 @@ s20 vf = do delta <- p_DTV vf token "to"- beta <- p_T Object+ beta <- p_T [Object] return (F20 delta beta) s21 :: VerbForm -> Parser (P TV) s21 vf = do delta <- p_DTV vf- beta <- p_T Object+ beta <- p_T [Object] return (F21 delta beta) -- FIXME: この規則はどこからも使われていないけど良いのだろうか?@@ -683,7 +684,7 @@ s24 :: Parser (P PP) s24 = do alpha <- p_PP_T- beta <- p_T Object+ beta <- p_T [Object] return (F24 alpha beta) s25 :: Parser (P Adj)
src/Report.hs view
@@ -9,12 +9,12 @@ -- Portability : portable module Report (report) where-import Expr+import IL import P import Parser import MP import Translation-import List (intersperse)+import Data.List (intersperse) report :: String -> String report s = unlines $@@ -26,20 +26,26 @@ f (PAny p) = [ "Parsed:" , " " ++ show p+ , " : " ++ show c , "" , "Translation:" , " " ++ show e+ , " : " ++ show t , "" , "Translation (simplified):" , " " ++ show e'+ , " : " ++ show t , "" , "Translation (MP applied):" , " " ++ show e''+ , " : " ++ show t ] where e = translate p e' = normalize e e'' = normalize $ applyMP $ e'+ c = catOf p+ t = catToType c sep :: String sep = "------------------------------------------------------"
+ src/ReportHTML.hs view
@@ -0,0 +1,76 @@+-----------------------------------------------------------------------------+-- |+-- Module : ReportHTML+-- Copyright : (c) Masahiro Sakai 2009+-- License : BSD3-style (see LICENSE)+-- +-- Maintainer: masahiro.sakai@gmail.com+-- Stability : experimental+-- Portability : portable++module ReportHTML (report) where+import IL+import P+import Parser+import MP+import Translation+import Data.List (intersperse)+import Text.XML.Light++report :: String -> String+report s = showTopElement $ html [hd (title ("Result of \"" ++ s ++ "\"")), body b]+ where+ b = case parseAny s of+ [] -> [p "(parse error)"]+ ps -> intersperse sep (map f ps)++f :: PAny -> Element+f (PAny p) = dl+ [ dt "Parsed"+ , dd (show p ++ " : " ++ show c)+ , dt "Translation"+ , dd (show e ++ " : " ++ show t)+ , dt "Translation (simplified)"+ , dd (show e' ++ " : " ++ show t)+ , dt "Translation (MP applied)"+ , dd (show e'' ++ " : " ++ show t)+ ]+ where+ e = translate p+ e' = normalize e+ e'' = normalize $ applyMP $ e'+ c = catOf p+ t = catToType c++html :: Node t => t -> Element+html c = add_attr (Attr xmlns ns) $ node QName{ qName = "html", qURI = Just ns, qPrefix = Nothing } c++xmlns :: QName+xmlns = QName{ qName = "xmlns", qURI = Nothing, qPrefix = Nothing}++ns :: String+ns = "http://www.w3.org/1999/xhtml"++hd :: Node t => t -> Element+hd = node QName{ qName = "head", qURI = Just ns, qPrefix = Nothing }++title :: Node t => t -> Element+title = node QName{ qName = "title", qURI = Just ns, qPrefix = Nothing }++body :: Node t => t -> Element+body = node QName{ qName = "body", qURI = Just ns, qPrefix = Nothing }++p :: Node t => t -> Element+p = node QName{ qName = "p", qURI = Just ns, qPrefix = Nothing }++dl :: Node t => t -> Element+dl = node QName{ qName = "dl", qURI = Just ns, qPrefix = Nothing }++dt :: Node t => t -> Element+dt = node QName{ qName = "dt", qURI = Just ns, qPrefix = Nothing }++dd :: Node t => t -> Element+dd = node QName{ qName = "dd", qURI = Just ns, qPrefix = Nothing }++sep :: Element+sep = node QName{ qName = "hr", qURI = Just ns, qPrefix = Nothing } ()
src/Translation.hs view
@@ -10,29 +10,32 @@ {-# LANGUAGE TypeOperators, GADTs, TypeSynonymInstances, ScopedTypeVariables #-} -module Translation (translate) where+module Translation (translate, catToType) where -import Expr+import IL import P -------------------------------------------------------------------------------- Exprも型付きにしたいなぁ {--data E -- e-data S -- s-data Prop -- t--- 関数型はHaskellの -> をそのまま使う- -- 範疇から型への対応 type family Translate x type instance Translate Sen = Prop type instance Translate IV = E -> Prop type instance Translate CN = E -> Prop+type instance Translate Adj = E -> Prop type instance Translate (a :/ b) = ((S -> Translate b) -> Translate a) type instance Translate (a :// b) = ((S -> Translate b) -> Translate a) -} +catToType :: Cat c -> Type+catToType Sen = Prop+catToType IV = E :-> Prop+catToType CN = E :-> Prop+catToType Adj = E :-> Prop -- これで本当にあっている?+catToType (a :/ b) = (S (catToType b)) :-> catToType a+catToType (a :// b) = (S (catToType b)) :-> catToType a+ ----------------------------------------------------------------------------- translate :: forall c. P c -> Expr@@ -41,16 +44,24 @@ --- 2. be → λp.λx. p{f^λy.[x = y]}. --- ここで，変数pのタイプは<s, <<s, <e, t>>, t>>. translate (B (IV :/ (Sen :/ IV)){- TV -} "be") =- lambda "p" $ lambda "x" $ - FVar "p" <@>- int (lambda "y" $ Op2 Id (FVar "x") (FVar "y"))+ lambda p $ lambda x $ + FVar p <@> int (lambda y $ Op2 Id (FVar x) (FVar y))+ where+ p = ("p", S (S (E :-> Prop) :-> Prop))+ x = ("x", E)+ y = ("y", E) --- 3. necessarily → λp[□ext p]. ここで，p のタイプは<s, t>とする．-translate (B (Sen :/ Sen) "necessarily") = lambda "p" $ Op1 Box (ext (FVar "p"))+translate (B (Sen :/ Sen) "necessarily") = lambda p $ Op1 Box (ext (FVar p))+ where+ p = ("p", S Prop) --- 4. j, m, b はタイプがe の定数記号，変数P のタイプは<s, <e, t>>とする．-translate (B (Sen :/ IV){- T -} x) = lambda "p" $ FVar "p" <@> Const x+translate (B (Sen :/ IV){- T -} x) = lambda p $ FVar p <@> Const (x, E)+ where+ p = ("p", S (catToType IV)) --- 5. he_n → λP. P {x_n}．x_ はタイプe の変数．-translate (He n) = lambda "p" $ FVar "p" <@> FVar (xn n)-+translate (He n) = lambda p $ FVar p <@> FVar (xn n)+ where+ p = ("p", S (E :-> Prop)) translate (F2 delta zeta) = trApp delta zeta -- T2 translate (F3 n zeta phi) = -- T3 lambda (xn n) $ Op2 And (translate zeta :@ FVar (xn n)) (translate phi)@@ -62,20 +73,26 @@ translate (F6 delta beta) = trApp delta beta -- T9 translate (F7 delta beta) = trApp delta beta -- T10 translate (F8 phi psi) =- case f8 :: Cat c of+ case cat :: Cat c of Sen -> Op2 And (translate phi) (translate psi) -- T11a- IV -> lambda "x" $ Op2 And (translate phi :@ FVar "x") (translate psi :@ FVar "x") -- T12a+ IV -> lambda x $ Op2 And (translate phi :@ FVar x) (translate psi :@ FVar x) -- T12a+ where+ x = ("x", E) translate (F9 phi psi) =- case f9 :: Cat c of+ case cat :: Cat c of Sen -> Op2 Or (translate phi) (translate psi) -- T11b- IV -> lambda "x" $ Op2 Or (translate phi :@ FVar "x") (translate psi :@ FVar "x") -- T12b- Sen :/ IV -> lambda "P" $ Op2 Or (translate phi :@ FVar "P") (translate psi :@ FVar "P") -- T13+ IV -> lambda x $ Op2 Or (translate phi :@ FVar x) (translate psi :@ FVar x) -- T12b+ where x = ("x", E)+ Sen :/ IV -> lambda p $ Op2 Or (translate phi :@ FVar p) (translate psi :@ FVar p) -- T13+ where p = ("P", S (E :-> Prop)) -- T14 (講義資料はx_nになるべきところがxになっている) translate (F10 n alpha phi) =- case f10 :: Cat c of+ case cat :: Cat c of Sen -> translate alpha :@ (int $ lambda (xn n) (translate phi)) -- T14- CN -> lambda "y" $ translate alpha :@ int (lambda (xn n) (translate phi :@ FVar "y")) -- T15- IV -> lambda "y" $ translate alpha :@ int (lambda (xn n) (translate phi :@ FVar "y")) -- T16+ CN -> lambda y $ translate alpha :@ int (lambda (xn n) (translate phi :@ FVar y)) -- T15+ IV -> lambda y $ translate alpha :@ int (lambda (xn n) (translate phi :@ FVar y)) -- T16+ where+ y = ("y", E) -- T17 translate (F11 alpha delta) = Op1 Not $ trApp alpha delta translate (F12 alpha delta) = Op1 F $ trApp alpha delta@@ -83,56 +100,78 @@ translate (F14 alpha delta) = Op1 H $ trApp alpha delta translate (F15 alpha delta) = Op1 Not $ Op1 H $ trApp alpha delta -- T18 (beの扱い以外はT9と同じ)-translate (B (IV :/ Adj) "be") =- lambda "P" $ lambda "x" $ FVar "P" <@> FVar "x"+translate (B (IV :/ Adj) "be") = lambda p $ lambda x $ FVar p <@> FVar x+ where+ p = ("P", S (E :-> Prop))+ x = ("x", E) -- T19 translate (F19 delta) =- lambda "x" $ exists "y" $- translate delta :@- int (lambda "P" (FVar "P" <@> FVar "y")) :@- FVar "x"+ lambda x $ exists y $+ translate delta :@ int (lambda p (FVar p <@> FVar y)) :@ FVar x+ where+ x = ("x", E)+ p = ("P", S (E :-> Prop))+ y = ("y", E) translate (F20 delta beta) = trApp delta beta -- T20 translate (F21 delta beta) = trApp delta beta -- T21 (講義資料ではF20を誤って使っている) -- T22 translate (F22 delta) =- lambda "P" $ lambda "Q" $ lambda "x" $- translate delta :@ FVar "Q" :@ FVar "P" :@ FVar "x"+ lambda p $ lambda q $ lambda x $+ translate delta :@ FVar q :@ FVar p :@ FVar x+ where+ p = ("P", S (catToType (cat :: Cat T)))+ q = ("Q", S (catToType (cat :: Cat T)))+ x = ("x", E) translate (F23 alpha delta) = trApp alpha delta -- T23 translate (F24 alpha beta) = trApp alpha beta -- T24 -- 講義資料のByの解釈は誤り? (型が一致しない) translate (B (IV :/ (IV :/ (Sen :/ IV)) :/ (Sen :/ IV)){- PP/T -} "by") = - lambda "P" $ lambda "R" $ lambda "x" $- FVar "P" <@>- (int $ lambda "y" $- FVar "R" <@> int (lambda "Q" $ FVar "Q" <@> FVar "x") :@ FVar "y")+ lambda p $ lambda r $ lambda x $+ FVar p <@>+ (int $ lambda y $ FVar r <@> int (lambda q $ FVar q <@> FVar x) :@ FVar y)+ where+ p = ("P", S (catToType (Sen :/ IV)))+ r = ("R", S (catToType (IV :/ (Sen :/ IV))))+ x = ("x", E)+ y = ("y", E)+ q = ("Q", S (catToType IV)) -- T25 translate (F25 delta) =- lambda "x" $ exists "y" $ Op1 H $- translate delta :@- int (lambda "P" $ FVar "P" <@> FVar "x") :@- (FVar "y")+ lambda x $ exists y $ Op1 H $+ translate delta :@+ int (lambda p $ FVar p <@> FVar x) :@+ (FVar y)+ where+ x = ("x", E)+ y = ("y", E)+ p = ("P", S (catToType IV)) -- Det translate (B (Sen :/ IV :/ CN) s) =- case s of+ case s of "a" ->- lambda "p" $ lambda "q" $ exists "x" $- Op2 And (FVar "p" <@> FVar "x") (FVar "q" <@> FVar "x")+ lambda p $ lambda q $ exists x $+ Op2 And (FVar p <@> FVar x) (FVar q <@> FVar x) "the" ->- lambda "p" $ lambda "q" $ exists "y" $ forall "x" $+ lambda p $ lambda q $ exists y $ Op2 And- (Op2 Equiv (FVar "p" <@> FVar "x") (Op2 Id (FVar "x") (FVar "y")))- (FVar "q" <@> FVar "x")+ (forall x $ Op2 Equiv (FVar p <@> FVar x) (Op2 Id (FVar x) (FVar y)))+ (FVar q <@> FVar y) "every" ->- lambda "p" $ lambda "q" $ forall "x" $- Op2 Imply (FVar "p" <@> FVar "x") (FVar "q" <@> FVar "x")+ lambda p $ lambda q $ forall x $+ Op2 Imply (FVar p <@> FVar x) (FVar q <@> FVar x) "no" ->- lambda "p" $ lambda "q" $ forall "x" $- Op1 Not (Op2 And (FVar "p" <@> FVar "x") (FVar "q" <@> FVar "x"))- _ -> Const s+ lambda p $ lambda q $ forall x $+ Op1 Not (Op2 And (FVar p <@> FVar x) (FVar q <@> FVar x))+ _ -> Const (s, catToType (cat :: Cat Det))+ where+ p = ("p", S (E :-> Prop))+ q = ("q", S (E :-> Prop))+ x = ("x", E)+ y = ("y", E) -- それ以外-translate (B _ x) = Const x+translate (B c x) = Const (x, catToType c) -- ユーティリティ trApp :: P (b :/ a) -> P a -> Expr@@ -141,5 +180,5 @@ trApp' f a = translate f :@ (int (translate a)) xn :: Int -> Name-xn n = "he_"++show n+xn n = ("he_"++show n, E)
+ src/Version.hs view
@@ -0,0 +1,4 @@+module Version where++versionStr :: String+versionStr = "0.0.5"