From 03c7963bf4d4262bb3f955e9e33e180fa4dbaca2 Mon Sep 17 00:00:00 2001 From: hinarid Date: Mon, 11 Nov 2024 18:54:39 +0900 Subject: [PATCH 1/5] add searchProofWithIncrementalDepth --- src/DTS/Prover/Wani/Prove.hs | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/src/DTS/Prover/Wani/Prove.hs b/src/DTS/Prover/Wani/Prove.hs index 89512131..0099a2c9 100644 --- a/src/DTS/Prover/Wani/Prove.hs +++ b/src/DTS/Prover/Wani/Prove.hs @@ -17,6 +17,7 @@ import qualified DTS.QueryTypes as QT import qualified Data.Text.Lazy as T import qualified Data.List as L +import qualified Data.Maybe as M import qualified Debug.Trace as D import qualified ListT as ListT @@ -42,7 +43,7 @@ hojo varEnv sigEnv pre_type setting = let sigEnv' = map (Data.Bifunctor.second A.fromDT2A) sigEnv varEnv' = map A.fromDT2A varEnv arrowType = A.fromDT2A pre_type - result = searchProof' sigEnv' varEnv' arrowType 1 setting + result = searchProofWithIncrementalDepth sigEnv' varEnv' arrowType 1 setting 1 (M.Just 20) in WB.debugLog (sigEnv',varEnv') arrowType 0 setting "goal" result searchProof' :: WB.DeduceRule @@ -50,6 +51,11 @@ searchProof' a b c d setting= let result = B.deduce a b c d setting in result{WB.trees = L.nub (WB.trees result)} +searchProofWithIncrementalDepth :: A.SAEnv -> A.AEnv -> WB.AType -> WB.Depth -> WB.Setting -> Int -> M.Maybe Int-> WB.Result +searchProofWithIncrementalDepth a b c d setting currentDepth maybeLim = + let result = searchProof' a b c d setting{WB.maxdepth = currentDepth} + in D.trace ("d=" ++ (show currentDepth)) $ if (null (WB.trees result) && maybe True (currentDepth <) maybeLim) then searchProofWithIncrementalDepth a b c d setting (currentDepth+1) maybeLim else result + -- | Prover for lightblue: prove' :: QT.ProverBuilder prove' QT.ProofSearchSetting{..} (DdB.ProofSearchQuery sig ctx typ) = -- LiftT IO (Tree (U.Judgment U.DTT) UDTTrule) @@ -61,12 +67,12 @@ prove' QT.ProofSearchSetting{..} (DdB.ProofSearchQuery sig ctx typ) = -- LiftT WB.falsum = True, WB.maxdepth = case maxDepth of Just n -> n - Nothing -> 9, + Nothing -> 4, WB.maxtime = case maxTime of Just t -> t Nothing -> 100000, WB.debug = False, WB.sStatus = WB.statusDef }; - result = hojo ctx sig typ setting + result = hojo ctx sig typ setting in ListT.fromFoldable $ map A.aTreeTojTree' $ WB.trees result From 5772c5e4c13bbe48c3bc8d39c8d3f14f4440d057 Mon Sep 17 00:00:00 2001 From: hinarid Date: Mon, 11 Nov 2024 18:57:22 +0900 Subject: [PATCH 2/5] minor fix --- src/DTS/Prover/Wani/Prove.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/DTS/Prover/Wani/Prove.hs b/src/DTS/Prover/Wani/Prove.hs index 0099a2c9..47c61e23 100644 --- a/src/DTS/Prover/Wani/Prove.hs +++ b/src/DTS/Prover/Wani/Prove.hs @@ -43,7 +43,7 @@ hojo varEnv sigEnv pre_type setting = let sigEnv' = map (Data.Bifunctor.second A.fromDT2A) sigEnv varEnv' = map A.fromDT2A varEnv arrowType = A.fromDT2A pre_type - result = searchProofWithIncrementalDepth sigEnv' varEnv' arrowType 1 setting 1 (M.Just 20) + result = searchProofWithIncrementalDepth sigEnv' varEnv' arrowType 1 setting 1 (M.Just $ WB.maxdepth setting) in WB.debugLog (sigEnv',varEnv') arrowType 0 setting "goal" result searchProof' :: WB.DeduceRule From 849d61481b9385804eb9bb7ca1fd7d0baae24063 Mon Sep 17 00:00:00 2001 From: hinarid Date: Mon, 11 Nov 2024 19:09:26 +0900 Subject: [PATCH 3/5] minor fix --- src/DTS/Prover/Wani/Prove.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/DTS/Prover/Wani/Prove.hs b/src/DTS/Prover/Wani/Prove.hs index 47c61e23..ab8f6052 100644 --- a/src/DTS/Prover/Wani/Prove.hs +++ b/src/DTS/Prover/Wani/Prove.hs @@ -43,7 +43,7 @@ hojo varEnv sigEnv pre_type setting = let sigEnv' = map (Data.Bifunctor.second A.fromDT2A) sigEnv varEnv' = map A.fromDT2A varEnv arrowType = A.fromDT2A pre_type - result = searchProofWithIncrementalDepth sigEnv' varEnv' arrowType 1 setting 1 (M.Just $ WB.maxdepth setting) + result = searchProofWithIncrementalDepth sigEnv' varEnv' arrowType 1 setting 1 (let num = WB.maxdepth setting in if num < 0 then M.Nothing else M.Just num) in WB.debugLog (sigEnv',varEnv') arrowType 0 setting "goal" result searchProof' :: WB.DeduceRule @@ -67,7 +67,7 @@ prove' QT.ProofSearchSetting{..} (DdB.ProofSearchQuery sig ctx typ) = -- LiftT WB.falsum = True, WB.maxdepth = case maxDepth of Just n -> n - Nothing -> 4, + Nothing -> 9, WB.maxtime = case maxTime of Just t -> t Nothing -> 100000, From 907faf94312056674bc57ed3615ad593799c70b4 Mon Sep 17 00:00:00 2001 From: Daisuke Bekki Date: Mon, 11 Nov 2024 23:07:14 +0900 Subject: [PATCH 4/5] Added --maxdepth global option --- README.md | 1 + app/lightblueMain.hs | 16 +++++++++++----- src/DTS/Prover/Wani/Prove.hs | 5 ++++- 3 files changed, 16 insertions(+), 6 deletions(-) diff --git a/README.md b/README.md index 808aced3..a1a1faa5 100644 --- a/README.md +++ b/README.md @@ -105,6 +105,7 @@ The global options are common to all commands. |```--nparse ``` |```-1``` |Search only N-best parse trees for each sentence (A negative value means all trees) | | |```--ntypecheck ``` |```-1``` |Search only N-best diagrams for each type checking of a logical form (A negative value means all diagrams) | |```--nproof ``` |```-1``` |Search only N-best diagrams for each proof search (A negative value means all diagrams) | +|```--maxdepth ``` |```9``` |Set the maximum search depth in proof search (default: 9) | |```--noTypeCheck``` | |If specified, show no type checking diagram for each sentence.| |```--noInference``` | |If specified, execute no inference for each discourse.| |```--time``` | |Show the execution time in stderr.| diff --git a/app/lightblueMain.hs b/app/lightblueMain.hs index 7dce3c55..bdef293e 100644 --- a/app/lightblueMain.hs +++ b/app/lightblueMain.hs @@ -2,7 +2,7 @@ {-# LANGUAGE OverloadedStrings, RecordWildCards #-} import Options.Applicative hiding (style) --optparse-applicative ---import Data.Semigroup ((<>)) --semigroup +import Control.Applicative (optional) --base import Control.Monad (forM) --base import ListT (toList) --list-t import qualified Data.Text.Lazy as T --text @@ -38,7 +38,7 @@ data Options = -- Version -- | Stat -- | Test - Options Command I.Style FilePath Juman.MorphAnalyzerName Int Int Int Int Bool Bool Bool Bool + Options Command I.Style FilePath Juman.MorphAnalyzerName Int Int Int Int Int Bool Bool Bool Bool deriving (Show, Eq) data Command = @@ -178,6 +178,12 @@ optionParser = <> showDefault <> value (-1) <> metavar "INT" ) + <*> option auto + ( long "maxdepth" + <> help "Set the maximum search depth in proof search" + <> showDefault + <> value 9 + <> metavar "INT" ) <*> switch ( long "noTypeCheck" <> help "If True, execute no type checking for LFs" ) @@ -239,7 +245,7 @@ lightblueMain :: Options -> IO() -- lightblueMain Version = showVersion -- lightblueMain Stat = showStat -- lightblueMain Test = test -lightblueMain (Options commands style filepath morphaName beamW nParse nTypeCheck nProof noTypeCheck noInference iftime verbose) = do +lightblueMain (Options commands style filepath morphaName beamW nParse nTypeCheck nProof maxDepth noTypeCheck noInference iftime verbose) = do start <- Time.getCurrentTime contents <- case filepath of "-" -> T.getContents @@ -260,7 +266,7 @@ lightblueMain (Options commands style filepath morphaName beamW nParse nTypeChec lightblueMainLocal (Parse output proverName) lr contents = do let handle = S.stdout parseSetting = CP.ParseSetting jpOptions lr beamW nParse nTypeCheck nProof True Nothing Nothing noInference verbose - prover = NLI.getProver proverName $ QT.ProofSearchSetting Nothing Nothing (Just QT.Classical) + prover = NLI.getProver proverName $ QT.ProofSearchSetting (Just maxDepth) Nothing (Just QT.Classical) parseResult = NLI.parseWithTypeCheck parseSetting prover [("dummy",DTT.Entity)] [] $ T.lines contents posTagOnly = case output of I.TREE -> False @@ -281,7 +287,7 @@ lightblueMain (Options commands style filepath morphaName beamW nParse nTypeChec | otherwise = take nSample parsedJSeM' handle = S.stdout parseSetting = CP.ParseSetting jpOptions lr beamW nParse nTypeCheck nProof True Nothing Nothing noInference verbose - prover = NLI.getProver proverName $ QT.ProofSearchSetting Nothing Nothing (Just QT.Classical) + prover = NLI.getProver proverName $ QT.ProofSearchSetting (Just maxDepth) Nothing (Just QT.Classical) S.hPutStrLn handle $ I.headerOf style pairs <- forM parsedJSeM'' $ \j -> do let title = "JSeM-ID " ++ (StrictT.unpack $ J.jsem_id j) diff --git a/src/DTS/Prover/Wani/Prove.hs b/src/DTS/Prover/Wani/Prove.hs index ab8f6052..c452035e 100644 --- a/src/DTS/Prover/Wani/Prove.hs +++ b/src/DTS/Prover/Wani/Prove.hs @@ -54,7 +54,10 @@ searchProof' a b c d setting= searchProofWithIncrementalDepth :: A.SAEnv -> A.AEnv -> WB.AType -> WB.Depth -> WB.Setting -> Int -> M.Maybe Int-> WB.Result searchProofWithIncrementalDepth a b c d setting currentDepth maybeLim = let result = searchProof' a b c d setting{WB.maxdepth = currentDepth} - in D.trace ("d=" ++ (show currentDepth)) $ if (null (WB.trees result) && maybe True (currentDepth <) maybeLim) then searchProofWithIncrementalDepth a b c d setting (currentDepth+1) maybeLim else result + in D.trace ("d=" ++ (show currentDepth)) $ + if (null (WB.trees result) && maybe True (currentDepth <) maybeLim) + then searchProofWithIncrementalDepth a b c d setting (currentDepth+1) maybeLim + else result -- | Prover for lightblue: prove' :: QT.ProverBuilder From 675a9d0e5d4dc548ea20743b8b22edbf3e79ed58 Mon Sep 17 00:00:00 2001 From: Daisuke Bekki Date: Mon, 11 Nov 2024 23:18:35 +0900 Subject: [PATCH 5/5] Added verbose field to DTS.QueryTypes.ProofSearchSetting --- app/lightblueMain.hs | 6 +++--- src/DTS/Prover/Wani/Prove.hs | 2 +- src/DTS/QueryTypes.hs | 1 + 3 files changed, 5 insertions(+), 4 deletions(-) diff --git a/app/lightblueMain.hs b/app/lightblueMain.hs index bdef293e..695890a5 100644 --- a/app/lightblueMain.hs +++ b/app/lightblueMain.hs @@ -266,7 +266,7 @@ lightblueMain (Options commands style filepath morphaName beamW nParse nTypeChec lightblueMainLocal (Parse output proverName) lr contents = do let handle = S.stdout parseSetting = CP.ParseSetting jpOptions lr beamW nParse nTypeCheck nProof True Nothing Nothing noInference verbose - prover = NLI.getProver proverName $ QT.ProofSearchSetting (Just maxDepth) Nothing (Just QT.Classical) + prover = NLI.getProver proverName $ QT.ProofSearchSetting (Just maxDepth) Nothing (Just QT.Classical) verbose parseResult = NLI.parseWithTypeCheck parseSetting prover [("dummy",DTT.Entity)] [] $ T.lines contents posTagOnly = case output of I.TREE -> False @@ -287,7 +287,7 @@ lightblueMain (Options commands style filepath morphaName beamW nParse nTypeChec | otherwise = take nSample parsedJSeM' handle = S.stdout parseSetting = CP.ParseSetting jpOptions lr beamW nParse nTypeCheck nProof True Nothing Nothing noInference verbose - prover = NLI.getProver proverName $ QT.ProofSearchSetting (Just maxDepth) Nothing (Just QT.Classical) + prover = NLI.getProver proverName $ QT.ProofSearchSetting (Just maxDepth) Nothing (Just QT.Classical) verbose S.hPutStrLn handle $ I.headerOf style pairs <- forM parsedJSeM'' $ \j -> do let title = "JSeM-ID " ++ (StrictT.unpack $ J.jsem_id j) @@ -392,7 +392,7 @@ test = do termA = UDTT.Sigma (UDTT.Con "entity") (UDTT.App (UDTT.Con "f") (UDTT.Var 0)) -- typeA = DTS.Kind tcq = UDTT.TypeInferQuery signature context termA - pss = QT.ProofSearchSetting Nothing Nothing (Just QT.Classical) + pss = QT.ProofSearchSetting Nothing Nothing (Just QT.Classical) False typeCheckResults <- toList $ typeInfer (nullProver pss) False tcq T.putStrLn $ T.toText $ head typeCheckResults --T.hPutStrLn S.stderr $ T.toText $ DTS.Judgment context (DTS.Var 0) DTS.Type diff --git a/src/DTS/Prover/Wani/Prove.hs b/src/DTS/Prover/Wani/Prove.hs index c452035e..efcf5dfd 100644 --- a/src/DTS/Prover/Wani/Prove.hs +++ b/src/DTS/Prover/Wani/Prove.hs @@ -74,7 +74,7 @@ prove' QT.ProofSearchSetting{..} (DdB.ProofSearchQuery sig ctx typ) = -- LiftT WB.maxtime = case maxTime of Just t -> t Nothing -> 100000, - WB.debug = False, + WB.debug = verbose, WB.sStatus = WB.statusDef }; result = hojo ctx sig typ setting diff --git a/src/DTS/QueryTypes.hs b/src/DTS/QueryTypes.hs index c37c0e7f..b1f1a3a0 100644 --- a/src/DTS/QueryTypes.hs +++ b/src/DTS/QueryTypes.hs @@ -78,6 +78,7 @@ data ProofSearchSetting = ProofSearchSetting { maxDepth :: Maybe Int , maxTime :: Maybe Int , logicSystem :: Maybe LogicSystem + , verbose :: Bool } deriving (Eq, Show) type Prover = DTTdB.ProofSearchQuery -> ListT IO DTTProofDiagram