From 27e0d8b5798dd0f84ccd8bdf7be1b4f8f70298d5 Mon Sep 17 00:00:00 2001 From: Edward Ayers Date: Tue, 29 Nov 2016 14:22:58 +0000 Subject: [PATCH] initial commit from zip file --- HLint.hs | 4 + README.txt | 24 ++ Setup.lhs | 6 + count.sh | 3 + eachcount.sh | 12 + open.sh | 4 + out.txt | 93 ++++++++ robotone.cabal | 28 +++ run.sh | 10 + runi.sh | 12 + screen.sh | 5 + src/ApplyingMoves.hs | 490 ++++++++++++++++++++++++++++++++++++++ src/DeletionMoves.hs | 553 +++++++++++++++++++++++++++++++++++++++++++ src/Expansion.hs | 82 +++++++ src/Library.hs | 20 ++ src/Main.hs | 170 +++++++++++++ src/Match.hs | 351 +++++++++++++++++++++++++++ src/Move.hs | 242 +++++++++++++++++++ src/Parser.hs | 163 +++++++++++++ src/Printing.hs | 24 ++ src/Rename.hs | 2 + src/RobotM.hs | 300 +++++++++++++++++++++++ src/Suspension.hs | 89 +++++++ src/TestData.hs | 224 ++++++++++++++++++ src/TestData2.hs | 267 +++++++++++++++++++++ src/Tex.hs | 208 ++++++++++++++++ src/TexBase.hs | 158 +++++++++++++ src/TidyingMoves.hs | 457 +++++++++++++++++++++++++++++++++++ src/Types.hs | 356 ++++++++++++++++++++++++++++ src/Writeup.hs | 413 ++++++++++++++++++++++++++++++++ texput.log | 16 ++ 31 files changed, 4786 insertions(+) create mode 100755 HLint.hs create mode 100755 README.txt create mode 100755 Setup.lhs create mode 100755 count.sh create mode 100755 eachcount.sh create mode 100755 open.sh create mode 100755 out.txt create mode 100755 robotone.cabal create mode 100755 run.sh create mode 100755 runi.sh create mode 100755 screen.sh create mode 100755 src/ApplyingMoves.hs create mode 100755 src/DeletionMoves.hs create mode 100755 src/Expansion.hs create mode 100755 src/Library.hs create mode 100755 src/Main.hs create mode 100755 src/Match.hs create mode 100755 src/Move.hs create mode 100755 src/Parser.hs create mode 100755 src/Printing.hs create mode 100755 src/Rename.hs create mode 100755 src/RobotM.hs create mode 100755 src/Suspension.hs create mode 100755 src/TestData.hs create mode 100755 src/TestData2.hs create mode 100755 src/Tex.hs create mode 100755 src/TexBase.hs create mode 100755 src/TidyingMoves.hs create mode 100755 src/Types.hs create mode 100755 src/Writeup.hs create mode 100755 texput.log diff --git a/HLint.hs b/HLint.hs new file mode 100755 index 0000000..21d29c8 --- /dev/null +++ b/HLint.hs @@ -0,0 +1,4 @@ +import "hint" HLint.Default +import "hint" HLint.Dollar +import "hint" HLint.Generalise +ignore "Use mappend" \ No newline at end of file diff --git a/README.txt b/README.txt new file mode 100755 index 0000000..113002b --- /dev/null +++ b/README.txt @@ -0,0 +1,24 @@ +General note +------------ + +As described in the accompanying paper, the prover relies heavily on data stored in its _library_. This library needs to be tailored to the problem(s) being solved. It is not possible to build a general, problem-independent library because the prover will use "more advanced" results to prove simpler ones -- for example, using the fact that a polynomial is differentiable to prove that it is continuous. As such, before trying the prover on fresh problems you will need to update the library. Roughly speaking, the library needs to contain domain-specific results and operations that would be obvious to an undergraduate who could be given the problem as an exercise, without containing "more advanced" facts. + +Compilation and Execution +------------------------- + +This software should be compiled with ghc 7.8.3 and Cabal 1.18.0.5 using v. 0.6.0.2 of the logict package. You will also need a TeX distribution to compile the generated proofs; the software was tested with MikTeX 2.9. + +After the source code has been compiled, run run.sh to generate and compile the TeX output; this will generate PDFs in the build/ subdirectory. robotoneshort.pdf contains the actual proofs + +Changelog +--------- + +1.1 + +Added TestData2 (problems supplied by a referee). +forwardsLibraryReasoning no longer creates new terms. +matchTargetWithHypothesis no longer displays debug text in writeup. + +1.0 + +Initial release. diff --git a/Setup.lhs b/Setup.lhs new file mode 100755 index 0000000..57ab288 --- /dev/null +++ b/Setup.lhs @@ -0,0 +1,6 @@ +#!/usr/bin/runhaskell +> module Main where +> import Distribution.Simple +> main :: IO () +> main = defaultMain + diff --git a/count.sh b/count.sh new file mode 100755 index 0000000..7f4cd16 --- /dev/null +++ b/count.sh @@ -0,0 +1,3 @@ +#!/usr/bin/bash +wd=$(dirname "$0") +cat src/*.hs | grep -v -E '^[[:space:]]*($|--( |$)|//)' | wc -l \ No newline at end of file diff --git a/eachcount.sh b/eachcount.sh new file mode 100755 index 0000000..189e5a8 --- /dev/null +++ b/eachcount.sh @@ -0,0 +1,12 @@ +#!/usr/bin/bash +wd=$(dirname "$0") +echo +pushd src > 0 +for f in *.hs +do + paste <(cat $f | grep -v -E '^[[:space:]]*($|--( |$)|//)' | wc -l) <(echo ${f%src.*}) +done +echo +cat *.hs | grep -v -E '^[[:space:]]*($|--( |$)|//)' | wc -l +popd > 0 +echo \ No newline at end of file diff --git a/open.sh b/open.sh new file mode 100755 index 0000000..29870f8 --- /dev/null +++ b/open.sh @@ -0,0 +1,4 @@ +#!/usr/bin/bash +wd=$(dirname "$0") + +open "$wd/build/robotone.pdf" \ No newline at end of file diff --git a/out.txt b/out.txt new file mode 100755 index 0000000..0c7a013 --- /dev/null +++ b/out.txt @@ -0,0 +1,93 @@ +1. Expand pre-universal target T1. +2. Peel and split universal-conditional target T2. +3. Elementary expansion of hypothesis H3. +4. Forwards reasoning using H1 with H4. +5. Deleted H4, as this unexpandable atomic statement is unmatchable. +6. Deleted H1, as the conclusion of this implicative statement is unmatchable. +7. Forwards reasoning using H2 with H5. +8. Deleted H5, as this unexpandable atomic statement is unmatchable. +9. Deleted H2, as the conclusion of this implicative statement is unmatchable. +10. Unlock existential-universal-conditional target T3. +11. Elementary expansion of target T4. +12. Backwards reasoning using H6 with T5. +13. Delete H6 as it contans a dangling variable $A$. +14. Backwards reasoning using H7 with T6. +15. Delete H7 as it contans a dangling variable $B$. +16. Replacing diamonds with bullets in L2$^\blacklozenge$. +17. Backwards reasoning using library result ``transitivity'' with (T7,H8). +18. Moved H8 down, as $x$ can only be utilised by T8. +19. Backwards reasoning using library result ``transitivity'' with (T8,H8). +20. Delete H8 as it contans a dangling variable $x$. +21. Collapsed subtableau L3 as it has no undeleted hypotheses. +22. Taking $\delta^\bullet [\overline{y}] = \min(\delta'[x],\delta''[x])$ matches all targets against a library solution, so L2 is done. +23. All targets of L1 are `Done', so L1 is itself done. + 23 moves made; problem solved. +1. Expand pre-universal target T1. +2. Peel and split universal-conditional target T2. +3. Elementary expansion of hypothesis H3. +4. Forwards reasoning using H2 with H4. +5. Deleted H4, as this unexpandable atomic statement is unmatchable. +6. Deleted H2, as the conclusion of this implicative statement is unmatchable. +7. Unlock existential-universal-conditional target T3. +8. Elementary expansion of target T4. +9. Backwards reasoning using H5 with T5. +10. Delete H5 as it contans a dangling variable $U$. +11. Backwards reasoning using H1 with T6. +12. Delete H1 as it contans a dangling variable $f$. +13. Hypothesis H6 matches target T7 after choosing $\delta^\blacklozenge [\overline{y}] = \delta''[x,\delta'[f(x)]]$, so L2$^\blacklozenge$ is done. +14. All targets of L1 are `Done', so L1 is itself done. + 14 moves made; problem solved. +1. Expand pre-universal target T1. +2. Peel bare universal target T2. +3. Unlock existential-universal-conditional target T3. +4. Backwards reasoning using H2 with T4. +5. Delete H2 as it contans a dangling variable $g$. +6. Backwards reasoning using H1 with T5. +7. Delete H1 as it contans a dangling variable $f$. +8. Hypothesis H3 matches target T6 after choosing $\delta^\blacklozenge [\overline{y}] = \delta''[x,\delta'[f(x),\epsilon]]$, so L2$^\blacklozenge$ is done. +9. All targets of L1 are `Done', so L1 is itself done. + 9 moves made; problem solved. +1. Expand pre-universal target T1. +2. Peel bare universal target T2. +3. Unlock existential-universal-conditional target T3. +4. Backwards reasoning using H1 with T4. +5. Delete H1 as it contans a dangling variable $f$. +6. Backwards reasoning using H2 with T5. +7. Delete H2 as it contans a dangling variable $a$. +8. Hypothesis H3 matches target T6 after choosing $N^\blacklozenge [\overline{n}] = N'[\delta[a,\epsilon]]$, so L2$^\blacklozenge$ is done. +9. All targets of L1 are `Done', so L1 is itself done. + 9 moves made; problem solved. +1. Expand pre-universal target T1. +2. Peel and split universal-conditional target T2. +3. Forwards reasoning using H1 with H3. +4. Deleted H3, as this unexpandable atomic statement is unmatchable. +5. Deleted H1, as the premise of this implicative statement is unmatchable. +6. Expand pre-existential hypothesis H5. +7. Forwards reasoning using library result ``a closed set contains its limit points'' with (H2,H4,H6). +8. Delete H2 as it contans a dangling variable $X$. +9. All conjuncts of T3 (after expansion) can be simultaneously matched against H7 and H6 or rendered trivial by choosing $a' = a$, so L1 is done. + 9 moves made; problem solved. +1. Expand pre-universal target T1. +2. Peel and split universal-conditional target T2. +3. Expand pre-existential hypothesis H1. +4. Elementary expansion of hypothesis H2. +5. Rewrite $x$ as $f(y)$ throughout the tableau using hypothesis H3. +6. Hypothesis H4 matches target T3, so L1 is done. + 6 moves made; problem solved. +1. Expand pre-universal target T1. +2. Peel and split universal-conditional target T2. +3. Elementary expansion of target T3. +4. All conjuncts of T4 (after expansion) can be simultaneously matched against H1 or rendered trivial by choosing $y = x$, so L1 is done. + 4 moves made; problem solved. +1. Expand pre-universal target T1. +2. Peel and split universal-conditional target T2. +3. Elementary expansion of hypothesis H2. +4. Expand pre-existential hypothesis H3. +5. Expand pre-existential hypothesis H4. +6. Forwards reasoning using H1 with (H6,H8). +7. Expand pre-existential target T3. +8. Unlock existential target T4. +9. Elementary expansion of target T5. +10. Rewrite $x$ as $f(y)$ throughout the tableau using hypothesis H6. +11. Rewrite $y$ as $y'$ throughout the tableau using hypothesis H9. + 11 moves made. diff --git a/robotone.cabal b/robotone.cabal new file mode 100755 index 0000000..84f19f1 --- /dev/null +++ b/robotone.cabal @@ -0,0 +1,28 @@ +name: robotone +version: 0.0.1 +cabal-version: >=1.2 +build-type: Simple +license: AllRightsReserved +license-file: "" +description: +data-dir: "" + +executable robotone + build-depends: QuickCheck -any, base -any, containers -any, + logict -any, mtl -any, parsec -any, transformers -any + main-is: Main.hs + buildable: True + hs-source-dirs: src + other-modules: Writeup Types TidyingMoves TexBase Tex TestData TestData2 + Suspension RobotM Rename Printing Parser Move Match Library + Expansion DeletionMoves ApplyingMoves + ghc-options: -fwarn-unused-binds + +test-suite test-robotone + build-depends: QuickCheck -any, base -any, containers -any, + logict -any, mtl -any, parsec -any, transformers -any + type: exitcode-stdio-1.0 + main-is: Main.hs + buildable: True + cpp-options: -DMAIN_FUNCTION=testMain + hs-source-dirs: src \ No newline at end of file diff --git a/run.sh b/run.sh new file mode 100755 index 0000000..5dd5a90 --- /dev/null +++ b/run.sh @@ -0,0 +1,10 @@ +#!/usr/bin/bash +wd=$(dirname "$0") +xelatex=$(which xelatex) + +"$wd/dist/build/robotone/robotone" > "$wd/build/robotone.tex" +echo "TeX" +pushd "$wd/build" +"$xelatex" "\input{robotone.tex}" -jobname=robotoneshort -quiet +"$xelatex" "\def\showsteps{1} \input{robotone.tex}" -jobname=robotone -quiet +popd \ No newline at end of file diff --git a/runi.sh b/runi.sh new file mode 100755 index 0000000..ff52f7f --- /dev/null +++ b/runi.sh @@ -0,0 +1,12 @@ +#!/usr/bin/bash +wd=$(dirname "$0") +xelatex=$(which xelatex) + +pushd "$wd/src" +runghc Main.hs > "../build/robotone.tex" +popd +echo "TeX" +pushd "$wd/build" +"$xelatex" robotone.tex --quiet +popd +open "$wd/build/robotone.pdf" \ No newline at end of file diff --git a/screen.sh b/screen.sh new file mode 100755 index 0000000..31de42e --- /dev/null +++ b/screen.sh @@ -0,0 +1,5 @@ +#!/usr/bin/bash +wd=$(dirname "$0") +xelatex=$(which xelatex) + +"$wd/dist/build/robotone/robotone" \ No newline at end of file diff --git a/src/ApplyingMoves.hs b/src/ApplyingMoves.hs new file mode 100755 index 0000000..3c6868d --- /dev/null +++ b/src/ApplyingMoves.hs @@ -0,0 +1,490 @@ +{-# LANGUAGE TupleSections #-} + +module ApplyingMoves ( + expandPreExistentialHypothesis, + expandPreUniversalTarget, + expandPreExistentialTarget, + elementaryExpansionOfHypothesis, + elementaryExpansionOfTarget, + forwardsReasoning, + forwardsLibraryReasoning, + backwardsReasoning, + backwardsLibraryReasoning, + solveBullets +) where + +import Prelude hiding ((/)) +import Control.Arrow +import Control.Monad +import Control.Applicative +import Data.Maybe +import Data.Either +import Data.List +import qualified Data.Map as Map +import Data.Map (Map, (!)) +import Debug.Trace + +import Types +import Move +import Match +import Expansion +import TexBase +import Tex +import RobotM +import Library +import Writeup + +--TODO: rename tID to tN in this and other files + +---------------------------------------------------------------------------------------------------- + +boundVars = boundVariablesInFormula + +---------------------------------------------------------------------------------------------------- + +--peelHypothesis: peels a hypothesis and also splits 'and's recursively to any depth. +-- also returns list of peeled variables. +peelHypothesis :: Formula -> ([Formula], [Variable]) +peelHypothesis f@(AtomicFormula _ _) = ([f], []) +peelHypothesis f@(Not _) = ([f], []) +peelHypothesis f@(And fs) = concat *** concat $ unzip (peelHypothesis <$> fs) +peelHypothesis f@(Or _) = ([f], []) +peelHypothesis f@(Forall _ _) = ([f], []) +peelHypothesis f@(UniversalImplies _ _ _) = ([f], []) +peelHypothesis f@(Exists vs f') = second (++ vs) $ peelHypothesis f' + +---------------------------------------------------------------------------------------------------- + +isExistential :: Formula -> Bool +isExistential f@(Exists _ _) = True +isExistential _ = False + +isUniversal :: Formula -> Bool +isUniversal (Forall _ _) = True +isUniversal (UniversalImplies _ _ _) = True +isUniversal _ = False + +expandPreUniversalTarget :: MoveType +expandPreUniversalTarget = tableauwise onTableau where + + {- TODO: make this affect more cases with more than one target?-} + onTableau :: [Statement] -> Surroundings -> Tableau -> RobotM (MoveDescription, Tableau) + onTableau _ s tableau@(Tableau tID tVs hs (Target [Left (Statement n f _)])) = do + --obtain the primary expansion of the target (if one exists) + expansion <- primaryExpansion f + + --make sure it's pre-uc + guard $ isUniversal expansion + + f'' <- createStatement STTarget expansion + return (MoveDescription [n] [] $ "Expand pre-universal target " ++ texSN n ++ ".", s $ Tableau tID tVs hs (Target [Left f''])) + + onTableau _ _ _ = mzero + + +expandPreExistentialTarget :: MoveType +expandPreExistentialTarget = tableauwise onTableau where + + onTableau :: [Statement] -> Surroundings -> Tableau -> RobotM (MoveDescription, Tableau) + onTableau _ s tableau@(Tableau tID tVs hs (Target ps)) = do + --pick a target + (Left (Statement n f _), context) <- oneOf $ eachUndeletedTargetPartWithContext ps + + --obtain the primary expansion of the target (if one exists) + expansion <- primaryExpansion f + + --make sure it's pre-existential + guard $ isExistential expansion + + f'' <- createStatement STTarget expansion + + return (MoveDescription [n] [TargetIs [f'']] $ "Expand pre-existential target " ++ texSN n ++ ".", + s . Tableau tID tVs hs . Target . context . return . Left $ f'') + + onTableau _ _ _ = mzero + + +expandPreExistentialHypothesis :: MoveType +expandPreExistentialHypothesis = tableauwise onTableau where + + onTableau :: [Statement] -> Surroundings -> Tableau -> RobotM (MoveDescription, Tableau) + onTableau _ s tableau@(Tableau tID tVs hs t) = do + --pick a hypothesis + (h@(Statement n f _), context) <- oneOf $ eachUndeletedHypothesisWithContext hs + + --obtain its primary expansion (if one exists) + expansion <- markDependencies <$> primaryExpansion f + + --make sure it's pre-existential + guard $ isExistential expansion + + let (newFormulae, vs) = peelHypothesis expansion + newHypotheses <- mapM (createStatement STHypothesis) newFormulae :: RobotM [Statement] + return (MoveDescription [n] [byDefSince [h] . existVars vs $ Assertion newHypotheses] $ "Expand pre-existential hypothesis " ++ texSN n ++ ".", + s $ Tableau tID (tVs ++ vs) (context newHypotheses) t) + onTableau _ _ _ = mzero + + +---------------------------------------------------------------------------------------------------- + + +partsOfElementary :: Formula -> [Formula] +partsOfElementary f@(AtomicFormula _ _) = [f] +partsOfElementary f@(Not _) = [f] +partsOfElementary (And fs) = fs +partsOfElementary f@(Or _) = [f] + + +elementaryExpansionOfHypothesis :: MoveType +elementaryExpansionOfHypothesis = tableauwise onTableau where + + onTableau :: [Statement] -> Surroundings -> Tableau -> RobotM (MoveDescription, Tableau) + onTableau _ s tableau@(Tableau tID tVs hs t) = do + --pick a hypothesis + (h@(Statement n f _), context) <- oneOf $ eachUndeletedHypothesisWithContext hs + + --obtain its primary expansion (if one exists) + expansion <- markDependencies <$> primaryExpansion f + + --make sure it's elementary + guard $ isAtomic expansion + + newHypotheses <- mapM (createStatement STHypothesis) (partsOfElementary expansion) :: RobotM [Statement] + return (MoveDescription [n] [since [h] $ Assertion newHypotheses] $ "Quantifier-free expansion of hypothesis " ++ texSN n ++ ".", + s $ Tableau tID tVs (context newHypotheses) t) + + onTableau _ _ _ = mzero + +elementaryExpansionOfTarget :: MoveType +elementaryExpansionOfTarget = tableauwise onTableau where + + onTableau :: [Statement] -> Surroundings -> Tableau -> RobotM (MoveDescription, Tableau) + onTableau _ s tableau@(Tableau tN@(TableauName isUnlocked _) tVs hs (Target ps)) = do + --pick a target + (Left t@(Statement n f _), context) <- oneOf $ eachUndeletedTargetPartWithContext ps + + --obtain its primary expansion (if one exists) + expansion <- primaryExpansion f + + --make sure it's elementary + guard $ isAtomic expansion + + newTargetStatements <- mapM (createStatement STTarget) (partsOfElementary expansion) :: RobotM [Statement] + + let proofClauses = if isUnlocked then [But $ [t] `Iff` newTargetStatements] + else [TargetIsIE [t] newTargetStatements] + + return (MoveDescription [n] proofClauses $ "Quantifier-free expansion of target " ++ texSN n ++ ".", + s . Tableau tN tVs hs . Target . context $ Left <$> newTargetStatements) + + onTableau _ _ _ = mzero + +---------------------------------------------------------------------------------------------------- + +--the heart of a formula is the part that remains when you remove all existential/bare-universal +-- quantifiers. So e.g. the heart of ∀x,ϵ.(∃δ.(∀y.(d(x,y) < δ ⇒ d(f(x),f(y)) < ϵ))) +-- is ∀y.(d(x,y) < δ ⇒ d(f(x),f(y)) < ϵ) +--Looking at this is useful when performing backwards reasoning. +--This function computes the heart, and also +-- a) which ∀ variables which were removed (x,ϵ,y in above) +-- b) which ∃ variables which were removed (δ in above) + +heartAndVariables :: Formula -> (Formula, [Variable], [Variable]) +heartAndVariables f@(AtomicFormula _ _) = (f,[],[]) +heartAndVariables f@(Not _) = (f,[],[]) +heartAndVariables f@(And fs) = (f,[],[]) +heartAndVariables f@(Or _) = (f,[],[]) +heartAndVariables (Forall vs f') = (g,us++vs,es) where (g,us,es) = heartAndVariables f' +heartAndVariables f@(UniversalImplies _ _ _) = (f,[],[]) +heartAndVariables (Exists vs f') = (g,us,es++vs) where (g,us,es) = heartAndVariables f' + +--peelAndFilterNotIn fs f': peel f', and return the parts if at least one of them is not in fs +-- also return any peeled variables +peelAndFilterNotIn :: [Formula] -> Formula -> Maybe ([Formula], [Variable]) +peelAndFilterNotIn fs f' = + let (f's, vs) = peelHypothesis f' + bound = boundVariablesInFormula f' + already_there :: Formula -> Bool + already_there g = any (isIsomorphic bound g) fs + + in guard (not (already_there f') && not (any already_there f's)) >> return (f's, vs) + +--TODO: in forwards/backwarsd reasoning, +-- at the moment we only handle the case where the implication has exactly one antecedent +-- although this should be easy to get around using recursion or currying + +areDistinct :: Ord a => [a] -> Bool +areDistinct as = length as == length (nub . sort $ as) + +statementsByName :: [StatementName] -> [Statement] -> [Statement] +statementsByName ns ss = [s | s@(Statement n _ _) <- ss, n `elem` ns] + +hasNoDiamondedVariables :: Statement -> Bool +hasNoDiamondedVariables (Statement _ f _) = null [v | v@(Variable _ _ _ VTDiamond _) <- allVariablesInFormula f] + +isUnlocked :: Tableau -> Bool +isUnlocked (Tableau (TableauName u _) _ _ _) = u + +--TODO: Other submoves of forward reasoning need to be implemented +forwardsReasoning :: MoveType +forwardsReasoning = tableauwise onTableau where + + onTableau :: [Statement] -> Surroundings -> Tableau -> RobotM (MoveDescription, Tableau) + onTableau inheritedHs s tableau@(Tableau tN tVs hs t) = do + -- Find a (possibly inherited) hypothesis with an implicative heart (possibly using expansion) + -- also obtain any variables lying outside the heart + (h@(Statement n f tags), context) <- oneOf $ eachUndeletedHypothesisWithContext hs ++ + [(h', const hs) | h' <- inheritedHs] + guard $ hasNoDiamondedVariables h + + (UniversalImplies vs as c, uvs, evs) <- + heartAndVariables <$> (return f <|> (markDependencies <$> speculative (allExpansions f))) + --NB 'speculative' expansion doesn't claim var. names for bound vars in expanded + -- implication, as such vars will not appear in the new statements generated + let otherHs = context [] + visibleHs = filter hasNoDiamondedVariables . filter undeleted $ otherHs ++ inheritedHs + + -- Try to match the antecedents + (matching, n's) <- matchFormulaeAmongStatements (uvs ++ vs) as visibleHs + guard $ areDistinct n's + + --make sure we have matched all the quantified variables + guard . all (`Map.member` matching) $ uvs ++ vs + + let sortedN's = sort n's + + allLocalHNames = [name | Statement name _ _ <- hs] + --local: names of used hypotheses from this tableau (i.e. not inherited) + local = filter (`elem` allLocalHNames) (n:sortedN's) + + --make sure at least one of implication, statements used is not inherited + guard . not $ null local + + --make sure the substitution hasn't been done before + guard . not $ UsedForwardsWith sortedN's `elem` tags + + --make the corresponding subsitutions in the consequent + let newH = transform matching c + + --obtain the fresh parts of the substituted consequent, aborting if there are none + (partsFormulae, vs') <- oneOf . maybeToList $ peelAndFilterNotIn [g | (Statement _ g _) <- hs] newH + parts <- mapM (createStatement STHypothesis) $ markDependencies <$> partsFormulae :: RobotM [Statement] + + return (MoveDescription (n:n's) [since (h:statementsByName n's visibleHs) . existVars (evs ++ vs') $ Assertion parts] $ + "Forwards reasoning using " ++ texSN n ++ " with " ++ texSNs n's ++ ".", + tagStatementInTableauAs (UsedForwardsWith sortedN's) n . + flip (foldr (tagStatementInTableauAs Vulnerable)) {-local-} (n:n's) . + s $ + Tableau tN (tVs ++ evs ++ vs') (hs ++ parts) t) + onTableau _ _ _ = mzero + + +forwardsLibraryReasoning :: MoveType +forwardsLibraryReasoning = tableauwise onTableau where + + onTableau :: [Statement] -> Surroundings -> Tableau -> RobotM (MoveDescription, Tableau) + onTableau inheritedHs s tableau@(Tableau tN tVs hs t) = do + -- Find a (possibly inherited) hypothesis with an implicative heart (possibly using expansion) + Result desc as c <- askLibraryResult + let vs = concatMap allDirectVariablesInFormula as + visibleHs = filter hasNoDiamondedVariables . filter undeleted $ hs ++ inheritedHs + + -- Try to match the antecedents (a.k.a. premises) + (matching, n's) <- matchFormulaeAmongStatements vs as $ visibleHs + guard $ areDistinct n's + + --make sure we have matched all the quantified variables + guard $ all (`Map.member` matching) vs + + let sortedN's = sort n's + + allLocalHNames = [name | Statement name _ _ <- hs] + --local: names of used hypotheses from this tableau (i.e. not inherited) + local = filter (`elem` allLocalHNames) sortedN's + + --make sure at least one of implication, statements used is not inherited + guard . not $ null local + + -- Make the corresponding subsitutions in the consequent + let newH = transform matching c + + --obtain the fresh parts of the substituted consequent, aborting if there are none + (partsFormulae, vs') <- oneOf . maybeToList $ peelAndFilterNotIn [g | (Statement _ g _) <- hs] newH + parts <- mapM (createStatement STHypothesis) $ markDependencies <$> partsFormulae :: RobotM [Statement] + + + let newTerms = concatMap (accumulateTermInFormula return) [f | Statement _ f _ <- parts] :: [Term] + let globalTerms = accumulateTermInTableau return $ s tableau :: [Term] + + --make sure there are no new terms + guard $ all (`elem` globalTerms) newTerms -- + + return (MoveDescription n's [since (statementsByName n's visibleHs) . existVars vs' $ Assertion parts] $ + "Forwards reasoning using library result ``" ++ desc ++ "'' with " ++ texSNs n's ++ ".", + flip (foldr (tagStatementInTableauAs Vulnerable)) {-local-} n's . + s $ + Tableau tN (tVs ++ vs') (hs ++ parts) t) + onTableau _ _ _ = mzero + +--TODO: Other submoves of backward reasoning need to be implemented +backwardsReasoning :: MoveType +backwardsReasoning = tableauwise onTableau where + + onTableau :: [Statement] -> Surroundings -> Tableau -> RobotM (MoveDescription, Tableau) + onTableau inheritedHs s tableau@(Tableau tN tVs hs t@(Target ps)) = do + -- Find a (possibly inherited) hypothesis with an implicative heart (possibly using expansion) + -- also obtain any variables lying outside the heart + (h@(Statement n f tags), context) <- oneOf $ eachUndeletedHypothesisWithContext hs ++ + [(h', const hs) | h' <- inheritedHs] + guard $ hasNoDiamondedVariables h +-- (UniversalImplies vs as c, uvs, evs) <- +-- heartAndVariables <$> (return f <|> +-- (markDependencies <$> speculative (allExpansions f))) + + ((UniversalImplies vs as c, uvs, evs), expanded) <- + first heartAndVariables <$> (return (f, False) <|> + ((, True) . markDependencies <$> speculative (allExpansions f))) + + + --NB 'speculative' expansion doesn't claim var. names for bound vars in expanded + -- implication, as such vars will not appear in the new statements generated + let otherHs = context [] + visibleHs = filter hasNoDiamondedVariables . filter undeleted $ otherHs ++ inheritedHs + + -- Take a target statement + (Left t@(Statement n' f' _), targetContext) <- oneOf $ eachUndeletedTargetPartWithContext ps + + -- Try to match the conclusion + matching <- oneOf . maybeToList $ match (c / uvs ++ vs ++ boundVars c) f' + -- Try to match all but one of the antecedents + (matching', n''s, leftoverA) <- extendMatchAllButOneOfFormulaeAmongStatements matching (uvs ++ vs) as visibleHs + guard $ areDistinct n''s + + --make sure we have matched all the quantified variables + guard . all (`Map.member` matching') $ uvs ++ vs + +-- let sortedN's = sort $ n' : n's + +-- allLocalNames = n':[name | Statement name _ _ <- hs] +-- --local: names of used hypotheses/target from this tableau (i.e. not inherited) +-- local = filter (`elem` allLocalNames) (n:sortedN's) + + --make the corresponding subsitutions in the leftover antecedent + let newT = transform matching' leftoverA + + --obtain the fresh parts of the substituted antecedent, aborting if there are none + (partsFormulae, vs') <- oneOf . maybeToList $ peelAndFilterNotIn [g | (Statement _ g _) <- lefts ps] newT + parts <- mapM (createStatement STTarget) partsFormulae :: RobotM [Statement] + + let ifOrWhenever = if isUnlocked tableau then Whenever else If + + writeupClauses = if expanded then [since (h:statementsByName n''s visibleHs) . existVars (evs ++ vs') $ parts `ifOrWhenever` t] + else [since (statementsByName n''s visibleHs) . weKnowThat . existVars (evs ++ vs') $ parts `ifOrWhenever` t] + + return (MoveDescription (n:n':n''s) writeupClauses $ + "Backwards reasoning using " ++ texSN n ++ " with " ++ texSNs (n':n''s) ++ ".", + flip (foldr (tagStatementInTableauAs Vulnerable)) {-local-}(n:n''s) . + s . Tableau tN (tVs ++ evs ++ vs') hs . Target . targetContext $ Left <$> parts) + + onTableau _ _ _ = mzero + + +--TODO: Other submoves of backward reasoning need to be implemented +backwardsLibraryReasoning :: MoveType +backwardsLibraryReasoning = tableauwise onTableau where + + onTableau :: [Statement] -> Surroundings -> Tableau -> RobotM (MoveDescription, Tableau) + onTableau inheritedHs s tableau@(Tableau tN tVs hs t@(Target ps)) = do + -- Take a library result + Result desc as c <- askLibraryResult + let vs = concatMap allDirectVariablesInFormula as + visibleHs = filter hasNoDiamondedVariables . filter undeleted $ hs ++ inheritedHs + + -- Take a target statement + (Left targetS@(Statement n' f' _), targetContext) <- oneOf $ eachUndeletedTargetPartWithContext ps + + -- Try to match the conclusion + matching <- oneOf . maybeToList $ match (c / vs ++ boundVars c) f' + -- Try to match all but one of the antecedents (a.k.a. premises) + (matching', n''s, leftoverA) <- extendMatchAllButOneOfFormulaeAmongStatements matching vs as visibleHs + guard $ areDistinct n''s + + --make sure we have matched all the quantified variables + guard $ all (`Map.member` matching') vs + +-- let sortedN's = sort $ n' : n's +-- +-- allLocalNames = n':[name | Statement name _ _ <- hs] +-- --local: names of used hypotheses/target from this tableau (i.e. not inherited) +-- local = filter (`elem` allLocalNames) sortedN's + + --make the corresponding subsitutions in the leftover antecedent + let newT = transform matching' leftoverA + + --obtain the fresh parts of the substituted antecedent, aborting if there are none + (partsFormulae, vs') <- oneOf . maybeToList $ peelAndFilterNotIn [g | (Statement _ g _) <- lefts ps] newT + parts <- mapM (createStatement STTarget) partsFormulae :: RobotM [Statement] + + let ifOrWhenever = if isUnlocked tableau then Whenever else If + + writeupClauses = [since (statementsByName n''s visibleHs) . existVars vs' $ parts `ifOrWhenever` targetS] + + return (MoveDescription (n':n''s) writeupClauses $ + "Backwards reasoning using library result ``" ++ desc ++ "'' with " ++ texSNs (n':n''s) ++ ".", + flip (foldr (tagStatementInTableauAs Vulnerable)) {-local-}n''s . + s . Tableau tN (tVs ++ vs') hs . Target . targetContext $ Left <$> parts) + + onTableau _ _ _ = mzero + +---------------------------------------------------------------------------------------------------- + +--TODO: check we want VTBullet here + +extractVarFromVarTerm :: Term -> Maybe Variable +extractVarFromVarTerm (VariableTerm v@(Variable _ _ _ VTBullet _)) = Just v +extractVarFromVarTerm _ = Nothing + +--TODO: tidy up variable names in this next function +solveBullets :: MoveType +solveBullets = tableauwise onTableau where + + onTableau :: [Statement] -> Surroundings -> Tableau -> RobotM (MoveDescription, Tableau) + onTableau inheritedHs s tableau@(Tableau tID tVs hs t@(Target ps)) = do + let bulletedVars = filter isBulletedOrDiamonded tVs -- [v | v@(Variable _ _ _ VTBullet _) <- tVs] + varsInHypotheses = nub . sort $ concatMap allVariablesInFormula [f | Statement _ f _ <- hs] + bulletedVarsBelowLine = bulletedVars \\ varsInHypotheses + + --need at one bulleted var which only occurs below the line + guard . not $ null bulletedVarsBelowLine + + --all targets must be statements, not subtableax. (Relax this constraint?) + guard $ all isLeft ps + let targets = lefts ps + + (Solution vs fs sols) <- askLibrarySolution + + (matching, targetsMatched) <- matchFormulaeAmongStatements (concatMap allVariablesInFormula fs) fs targets + + --make sure we have matched all the targets + guard $ length (nub . sort $ targetsMatched) == length targets + + --find the quantities each slot in the solution was matched against + let ts = [matching ! v | v <- vs] + + -- make sure that they are all single variables + v's <- oneOf . maybeToList $ mapM extractVarFromVarTerm ts + + -- make sure that they are all bulleted variables below the line + guard $ all (`elem` bulletedVarsBelowLine) v's + + let choices = zipWith VariableChoice v's (transformTerm matching <$> sols) + guard $ all isBulletedVariableChoiceLegal choices + + pd <- askPrintingData + return (MoveDescription [] [WeMayTake choices, ProofDone] $ + "Taking " ++ + texList (tex pd <$> choices) ++ " matches all targets against a library solution, so " ++ + texTN tID ++ " is done.", + s $ Done tID) + + onTableau _ _ _ = mzero diff --git a/src/DeletionMoves.hs b/src/DeletionMoves.hs new file mode 100755 index 0000000..120bb2c --- /dev/null +++ b/src/DeletionMoves.hs @@ -0,0 +1,553 @@ +module DeletionMoves ( + deleteDone, + deleteDoneDisjunct, + deleteRedundantHypothesis, + deleteDangling, + deleteUnmatchable +) where + +import Prelude hiding ((/)) +import Control.Arrow +import Control.Monad +import Control.Applicative +import Data.Maybe +import Data.Either +import Data.List +import qualified Data.Map as Map +import Data.Map (Map, (!)) + +import Types +import Move +import Match +import Expansion +import TexBase +import Tex +import RobotM + +import Debug.Trace + +---------------------------------------------------------------------------------------------------- + +boundVars = boundVariablesInFormula + +---------------------------------------------------------------------------------------------------- + +replaceTargetStatementWithTableau :: StatementName -> Tableau -> Tableau -> Tableau +replaceTargetStatementWithTableau n rep = mapTableau shallow where + shallow tableau@(Tableau tID tVs hs t@(Target ps)) = + case [c | (Left t@(Statement n' _ _), c) <- eachUndeletedTargetPartWithContext ps, n == n'] of + [context] -> Tableau tID tVs hs . Target $ context [Right [rep]] + [] -> tableau + shallow tableau = tableau + +---------------------------------------------------------------------------------------------------- + +--TODO: check whether these fns are exhaustive, i.e. kill all possible 'Done' configurations + +isDone :: Tableau -> Bool +isDone (Done _) = True +isDone _ = False +-- +--isSingleDone :: [Tableau] -> Bool +--isSingleDone [Done _] = True +--isSingleDone _ = False + +isSingleDoneTP :: Either Statement [Tableau] -> Bool +isSingleDoneTP (Right [Done _]) = True +isSingleDoneTP _ = False + +deleteDone :: MoveType +deleteDone = tableauwise onTableau where + + onTableau :: [Statement] -> Surroundings -> Tableau -> RobotM (MoveDescription, Tableau) + onTableau _ s tableau@(Tableau tID tVs hs (Target ps)) = do + guard $ any isSingleDoneTP ps --some target part consists of a single 'Done' + + let notDone = filter (not . isSingleDoneTP) ps + + case notDone of + [] -> return (MoveDescription [] [] $ + "All targets of " ++ texTN tID ++ " are `Done', so " ++ texTN tID ++ " is itself done.", + s $ Done tID) + + ps -> return (MoveDescription [] [] $ + "Remove `Done' targets of " ++ texTN tID ++ ".", + s . Tableau tID tVs hs . Target $ ps) + + onTableau _ _ _ = mzero + +deleteDoneDisjunct :: MoveType +deleteDoneDisjunct = tableauwise onTableau where + + onTableau :: [Statement] -> Surroundings -> Tableau -> RobotM (MoveDescription, Tableau) + onTableau _ s tableau@(Tableau tID tVs hs (Target ps)) = do + + (Right ts, targetContext) <- oneOf $ eachUndeletedTargetPartWithContext ps + + guard $ any isDone ts --some disjunct tableau is 'Done' + + case targetContext [] of + [] -> return (MoveDescription [] [] $ + "Some disjunct of the target of " ++ texTN tID ++ " is `Done', so " ++ texTN tID ++ " is itself `Done'.", + s $ Done tID) + + ps -> return (MoveDescription [] [] $ + "Some disjunct of a target line of " ++ texTN tID ++ " is `Done', so we will remove the line.", + s . Tableau tID tVs hs . Target $ ps) + + + onTableau _ _ _ = mzero + + +---------------------------------------------------------------------------------------------------- + +deleteRedundantHypothesis :: MoveType +deleteRedundantHypothesis = movetypeFromSubmovetypes [ + tagRedundantForwardsImplication, + tagRedundantBackwardsImplication + --TODO: add the submoves relating to conjunctions and disjunctions + ] + + +--removeExistentialQuantifiers: +removeExistentialQuantifiers :: Formula -> Formula +removeExistentialQuantifiers f@(AtomicFormula _ _) = f +removeExistentialQuantifiers f@(Not _) = f +removeExistentialQuantifiers f@(And _) = f +removeExistentialQuantifiers f@(Or _) = f +removeExistentialQuantifiers f@(Forall _ _) = f +removeExistentialQuantifiers f@(UniversalImplies _ _ _) = f +removeExistentialQuantifiers f@(Exists vs f') = removeExistentialQuantifiers f' + +tagRedundantForwardsImplication :: MoveType +tagRedundantForwardsImplication = tableauwise onTableau where + + onTableau :: [Statement] -> Surroundings -> Tableau -> RobotM (MoveDescription, Tableau) + onTableau inheritedHs s tableau@(Tableau tID tVs hs t) = do + -- Find a one-variable implicative hypothesis (possibly using expansion) + (Statement n f tags, context) <- oneOf $ eachElementWithContext hs + UniversalImplies vs [_] consequent <- return f <|> speculative (primaryExpansion f) + let otherHs = context [] + + -- Take another hypothesis + (Statement n' f' _) <- oneOf otherHs + + -- Try to match them + matching <- oneOf . maybeToList $ match (removeExistentialQuantifiers consequent / vs ++ boundVars consequent) f' + let matchedTerms = map (matching !) vs --NB. allow arbitrary term here, not variable + -- add a CannotSubstitute tag if none exists + tags' = if null [() | CannotSubstitute _ <- tags] + then tags ++ [CannotSubstitute []] + else tags + + --make sure the substitution is not forbidden + (CannotSubstitute tss, tagContext) <- oneOf $ eachElementWithContext tags' + guard . not $ matchedTerms `elem` tss + + -- construct the retagged statement (and forbid the substitution) + let h' = Statement n f . tagContext . return . CannotSubstitute $ tss ++ [matchedTerms] + + pd <- askPrintingData + return (MoveDescription [] [] $ + "Note that one should not substitute $" ++ texTuple pd matchedTerms ++ + "$ into " ++ texSN n ++ ", as this would recreate the existing hypothesis " ++ texSN n' ++ ".", + s $ Tableau tID tVs (context [h']) t) + + onTableau _ _ _ = mzero + +--TODO: extract 66-76 into a 'tryToSubstitute' fn + +tagRedundantBackwardsImplication :: MoveType +tagRedundantBackwardsImplication = tableauwise onTableau where + + onTableau :: [Statement] -> Surroundings -> Tableau -> RobotM (MoveDescription, Tableau) + onTableau inheritedHs s tableau@(Tableau tID tVs hs t@(Target [Left (Statement n' f' _)])) = do + -- Find a one-variable implicative hypothesis (possibly using expansion) + (Statement n f tags, context) <- oneOf $ eachElementWithContext hs + UniversalImplies vs [antecedent] consequent <- return f <|> speculative (primaryExpansion f) + let otherHs = context [] + + -- Try to match the antecedent of the hypothesis with the target + matching <- oneOf . maybeToList $ match (antecedent / vs ++ boundVars antecedent) f' + let matchedTerms = map (matching !) vs --NB. allow arbitrary term here, not variable + -- add a CannotSubstitute tag if none exists + tags' = if null [() | CannotSubstitute _ <- tags] + then tags ++ [CannotSubstitute []] + else tags + + --make sure the substitution is not forbidden + (CannotSubstitute tss, tagContext) <- oneOf $ eachElementWithContext tags' + guard . not $ matchedTerms `elem` tss + + -- construct the retagged statement (and forbid the substitution) + let h' = Statement n f . tagContext . return . CannotSubstitute $ tss ++ [matchedTerms] + + pd <- askPrintingData + return (MoveDescription [] [] $ + "Note that one will never substitute $" ++ texTuple pd matchedTerms ++ + "$ into " ++ texSN n ++ ", as this requires the use of the target " ++ texSN n' ++ " as a hypothesis.", + s $ Tableau tID tVs (context [h']) t) + onTableau _ _ _ = mzero + +---------------------------------------------------------------------------------------------------- + + +isSimpleConditional :: Formula -> Bool +isSimpleConditional (UniversalImplies _ as c) = all isAtomic as && isAtomic c +isSimpleConditional _ = False + +{- +hypothesisDemands :: Statement -> [Variable] +hypothesisDemands (Statement _ f _) = nub . sort $ + boundUniversalVariablesInFormula f ++ + [v | v@(Variable _ _ _ True _) <- allVariablesInFormula f] --all bulleted vars + +targetDemands :: Statement -> [Variable] +targetDemands (Statement _ f _) = nub . sort $ + boundExistentialVariablesInFormula f ++ + [v | v@(Variable _ _ _ True _) <- allVariablesInFormula f] --all bulleted vars +-} + +typeOfVar :: Variable -> Type_ +typeOfVar (Variable _ _ t _ _) = t + +isOnlyTargetInItsTableau :: StatementName -> Tableau -> Bool +isOnlyTargetInItsTableau n = head . accumulateTableau shallow where + shallow :: Tableau -> [Bool] + shallow (Tableau _ _ _ (Target ps)) + | n `elem` [n' | Left (Statement n' _ _) <- ps] = [length ps == 1] + shallow _ = [] + +--TODO: use memoisation to make this more efficient +deleteDangling :: MoveType +deleteDangling = tableauwise onTableau where + + onTableau :: [Statement] -> Surroundings -> Tableau -> RobotM (MoveDescription, Tableau) + onTableau inheritedHs s tableau@(Tableau tID tVs hs t@(Target ps)) = do + + let visibleHypotheses = filter undeleted $ inheritedHs ++ hypothesesAtAnyDepth tableau + visibleTargets = filter undeleted $ targetFormulaeAtAnyDepth tableau + + --Pick a vulnerable hypothesis h + (h@(Statement n f tags), context) <- oneOf $ eachUndeletedHypothesisWithContext hs + guard $ Vulnerable `elem` tags + + --Pick a (unbound, unbulleted) variable v used in h + v@(Variable _ _ vType VTNormal _) <- oneOf $ allVariablesInFormula f \\ boundVariablesInFormula f + + --Find all statements which meantion or could potentially use v + let statementsWantingV = nub . sort $ + -- statements mentioning v [NB. mentions of v inside dependencies don't count -- hence use of allDirectVariablesInFormula.] + [s | s@(Statement _ f' _) <- visibleHypotheses ++ visibleTargets, v `elem` allDirectVariablesInFormula f'] -- ++ +-- --The following rule doesn't quite seem right; we have commented it out for now. +-- -- statements which are neither unexpandable nor simple-conditional +-- [s | s@(Statement _ f' _) <- visibleHypotheses ++ visibleTargets, not (isUnexpandable f' || isSimpleConditional f')] ++ + -- hypotheses demanding a variable of the same type as h +-- [s | s@(Statement _ f' _) <- visibleHypotheses, vType `elem` map typeOfVar (hypothesisDemands s)] ++ + -- targets demanding a variable of the same type as h +-- [s | s@(Statement _ f' _) <- visibleTargets, vType `elem` map typeOfVar (targetDemands s)] + + --TODO: If all the actualMatches lie in one tableau, move the hypothesis into that tableau + pd <- askPrintingData + case statementsWantingV \\ [h] of + [] -> return (MoveDescription [] [] $ "Delete " ++ texSN n ++ " as no other statement mentions $" ++ tex pd v ++ "$.", + s $ Tableau tID tVs (context [tagAs Deleted h]) t) + + -- If h is only used by a single target statement t, and t is not the only target statement in its tableau + -- move h down to t (By forming a new tableau) + [targetStatement@(Statement n'@(StatementName STTarget _) _ _)] -> if isOnlyTargetInItsTableau n' tableau then mzero else do + newTableau <- createTableau' False [tagAs (MovedDownFrom tID) h] $ Target [Left targetStatement] + return (MoveDescription [] [] $ "Moved " ++ texSN n ++ " down, as $" ++ tex pd v ++ "$ can only be utilised by " ++ texSN n' ++ ".", + s . replaceTargetStatementWithTableau n' newTableau $ Tableau tID tVs (context []) t) + + _ -> mzero + + onTableau _ _ _ = mzero + + +---------------------------------------------------------------------------------------------------- + +deleteUnmatchable :: MoveType +deleteUnmatchable = movetypeFromSubmovetypes [ + deleteUnmatchableAtomicHypothesis, + deleteHypothesisWithUnmatchablePremise, + deleteHypothesisWithUnmatchableConclusion + --TODO: add other submoves + ] + + +--we want to define +-- +-- matchesPremiseOf :: Statement -> Statement -> Bool +-- matchesPremiseOf s s': does s match premise of s' possibly after s is expanded? +-- +--Unfortunately, we can't _expand_ unless we are in the RobotM monad +-- So instead we define +-- +-- matchesPremiseOfM :: RobotM (Statement -> Statement -> Bool) +-- +-- which returns the function we want. +-- (And similarly for other functions.) +-- Also note this ensures that this kind of speculative expansion can't affect the RobotM state + +matchesPremiseOfM :: RobotM (Statement -> Statement -> Bool) +matchesPremiseOfM = do + printingData <- askPrintingData + library <- askLibrary + robotState <- getRobotState + let --tryMatchM nondeterministically tries to find a match, and returns () if it succeeds + tryMatchM :: Statement -> Statement -> RobotM () + tryMatchM (Statement n f _) (Statement _ f' tags') = do + -- Make sure the substitution is legal + guard $ UsedForwardsWith [n] `notElem` tags' + -- Possibly expand f' + look for a universal implication + UniversalImplies v's as _ <- return f' <|> primaryExpansion f' + -- Choose an antecedent + a <- oneOf as + -- Try to match + m <- oneOf . maybeToList $ match (a / v's ++ boundVars a) f + + return () + + tryMatch :: Statement -> Statement -> Bool + tryMatch s = not . null . evalAllRobotM printingData library robotState . tryMatchM s + + return tryMatch + + +matchesPremiseOf'M :: RobotM (FormulaWithSlots -> Statement -> Bool) +matchesPremiseOf'M = do + printingData <- askPrintingData + library <- askLibrary + robotState <- getRobotState + let --tryMatchM nondeterministically tries to find a match, and returns () if it succeeds + tryMatchM :: FormulaWithSlots -> Statement -> RobotM () + tryMatchM (FormulaWithSlots f vs) (Statement _ f' tags') = do + -- Possibly expand f' + look for a universal implication + UniversalImplies v's as _ <- return f' <|> primaryExpansion f' + -- Choose an antecedent + a <- oneOf as + -- Try to match + guard $ twoWayMatchExists (f / vs ++ boundVars f) (a / boundVars a) + + return () + + tryMatch :: FormulaWithSlots -> Statement -> Bool + tryMatch f = not . null . evalAllRobotM printingData library robotState . tryMatchM f + + return tryMatch + + +matchesConclusionOf'M :: RobotM (FormulaWithSlots -> Statement -> Bool) +matchesConclusionOf'M = do + printingData <- askPrintingData + library <- askLibrary + robotState <- getRobotState + let --tryMatchM nondeterministically tries to find a match, and returns () if it succeeds + tryMatchM :: FormulaWithSlots -> Statement -> RobotM () + tryMatchM (FormulaWithSlots f vs) (Statement _ f' tags') = do + -- Possibly expand f' + look for a universal implication + UniversalImplies v's _ c <- return f' <|> primaryExpansion f' + -- Try to match + guard $ twoWayMatchExists (f / vs ++ boundVars f) (c / boundVars c) + + return () + + tryMatch :: FormulaWithSlots -> Statement -> Bool + tryMatch f = not . null . evalAllRobotM printingData library robotState . tryMatchM f + + return tryMatch + +--we want to define +-- +-- premiseMatchesFormula :: Formula -> [Variable] -> Statement -> Bool +-- premiseMatchesFormula f vs s: does a premise of s match f (with vs as wildcards in f), possibly after s is expanded? +-- +--Unfortunately, we can't _expand_ unless we are in the RobotM monad +-- So instead we define +-- +-- premiseMatchesFormulaM :: RobotM (Formula -> [Variable] -> Statement -> Bool) +-- +-- which returns the function we want. +-- Also note this ensures that this kind of speculative expansion can't affect the RobotM state + +--premiseMatchesFormulaM :: RobotM (Formula -> [Variable] -> Statement -> Bool) +--premiseMatchesFormulaM = do +-- robotState <- getRobotState +-- let --tryMatchM nondeterministically tries to find a match, and returns () if it succeeds +-- tryMatchM :: Formula -> [Variable] -> Statement -> RobotM () +-- tryMatchM f vs (Statement _ f' tags') = do +-- -- Possibly expand f' + look for a universal Implication +-- UniversalImplies v's as _ <- return f' <|> primaryExpansion f' +-- -- Choose an antecedent +-- a <- oneOf as +-- -- Try to match +-- m <- oneOf . maybeToList $ twoWayMatch (a / v's ++ boundVars a) (f / vs) +-- let substituted = map (m !) v's --the terms substituted into the UniversalImplies +-- -- Make sure the substitution is legal +-- guard $ null [() | CannotSubstitute tss <- tags', substituted `elem` tss] +-- return () +-- +-- tryMatch :: Formula -> [Variable] -> Statement -> Bool +-- tryMatch f vs s = not . null $ evalAllRobotM robotState (tryMatchM f vs s) +-- +-- return tryMatch + +{- +--matchesPremise tableau vs f s: does f (with vs as wildcards) match a premise of s, possibly after s is expanded? +matchesPremise :: Tableau -> [Variable] -> Formula -> Statement -> RobotM () +matchesPremise tableau vs f (Statement _ f' tags) = do + -- Possibly expand f' + look for a universal Implication + UniversalImplies v's as _ <- return f' <|> primaryExpansion f' + -- Choose an antecedent + a <- oneOf as + -- Try to match + m <- oneOf . maybeToList $ twoWayMatch (a / v's ++ boundVars a) (f / vs) + let substituted = map (m !) v's --the terms substituted into the UniversalImplies + -- Make sure the substitution is legal + guard $ null [() | CannotSubstitute tss <- tags, substituted `elem` tss] + +--matchesConclusion tableau vs f s: does f (with vs as wildcards) match a conclusion of s, possibly after s is expanded? +matchesConclusion :: Tableau -> [Variable] -> Formula -> Statement -> RobotM () +matchesConclusion tableau vs f (Statement _ f' tags) = do + -- Possibly expand f' + look for a universal Implication + UniversalImplies v's _ c <- return f' <|> primaryExpansion f' + -- Try to match + m <- oneOf . maybeToList $ twoWayMatch (c / v's ++ boundVars c) (f / vs) + let substituted = map (m !) v's --the terms substituted into the UniversalImplies + -- Make sure the substitution is legal + guard $ null [() | CannotSubstitute tss <- tags, substituted `elem` tss] + return () +-} + +--matches f s: does f match s +matches :: FormulaWithSlots -> Statement -> Bool +matches (FormulaWithSlots f vs) (Statement _ f' _) = + twoWayMatchExists (f / vs ++ boundVars f) (f' / boundVars f') + + +deleteUnmatchableAtomicHypothesis :: MoveType +deleteUnmatchableAtomicHypothesis = tableauwise onTableau where + + onTableau :: [Statement] -> Surroundings -> Tableau -> RobotM (MoveDescription, Tableau) + onTableau inheritedHs s tableau@(Tableau tID tVs hs t@(Target ps)) = do + + let visibleHypotheses = filter undeleted $ inheritedHs ++ hypothesesAtAnyDepth tableau + visibleTargets = filter undeleted $ targetFormulaeAtAnyDepth tableau + + --Pick a vulnerable unexpandable atomic hypothesis with no bulleted variables + (h@(Statement n f tags), context) <- oneOf $ eachUndeletedHypothesisWithContext hs + guard $ Vulnerable `elem` tags + guard $ isAtomic f + guard =<< isUnexpandable f + guard . null . filter isBulletedOrDiamonded $ allDirectVariablesInFormula f --no bulleted variable + + matchesPremiseOf <- matchesPremiseOfM + + let actualMatches = filter ((f/[]) `matches`) visibleTargets ++ + filter (h `matchesPremiseOf`) visibleHypotheses + +-- --TODO: If all the actualMatches lie in one tableau, move the hypothesis into that tableau + case actualMatches of + [] -> return (MoveDescription [] [] $ "Deleted " ++ texSN n ++ ", as this unexpandable atomic statement is unmatchable.", + s $ Tableau tID tVs (context [tagAs Deleted h]) t) + + [targetStatement@(Statement n'@(StatementName STTarget _) _ _)] -> if isOnlyTargetInItsTableau n' tableau then mzero else do + newTableau <- createTableau' False [tagAs (MovedDownFrom tID) h] $ Target [Left targetStatement] + return (MoveDescription [] [] $ "Moved " ++ texSN n ++ ", as this unexpandable atomic statement can only be used to prove " ++ texSN n' ++ ".", + s . replaceTargetStatementWithTableau n' newTableau $ Tableau tID tVs (context []) t) + + _ -> mzero + + onTableau _ _ _ = mzero + + +deleteHypothesisWithUnmatchablePremise :: MoveType +deleteHypothesisWithUnmatchablePremise = tableauwise onTableau where + + onTableau :: [Statement] -> Surroundings -> Tableau -> RobotM (MoveDescription, Tableau) + onTableau inheritedHs s tableau@(Tableau tID tVs hs t@(Target ps)) = do + + let visibleHypotheses = filter undeleted $ inheritedHs ++ hypothesesAtAnyDepth tableau + visibleTargets = filter undeleted $ targetFormulaeAtAnyDepth tableau + + --Pick a vulnerable hypothesis + (h@(Statement n f tags), context) <- oneOf $ eachUndeletedHypothesisWithContext hs + guard $ Vulnerable `elem` tags + + --save the state before performning any expansions + state <- getRobotState + + --make sure it's universal + UniversalImplies vs as _ <- return f <|> primaryExpansion f + -- Choose a premise/antecedent + a <- oneOf as + + matchesPremiseOf' <- matchesPremiseOf'M + matchesConclusionOf' <- matchesConclusionOf'M + + let actualMatches = filter ((a/vs) `matches`) [h | h@(Statement _ g _) <- visibleHypotheses, isAtomic g] ++ + filter ((a/vs) `matchesConclusionOf'`) visibleHypotheses ++ + filter ((a/vs) `matchesPremiseOf'`) visibleTargets + + --restore the state (so we don't use up any variable names) + putRobotState state + +-- --TODO: If all the actualMatches lie in one tableau, move the hypothesis into that tableau + case actualMatches of + [] -> return (MoveDescription [] [] $ "Deleted " ++ texSN n ++ ", as the premise of this implicative statement is unmatchable.", + s $ Tableau tID tVs (context [tagAs Deleted h]) t) + + [targetStatement@(Statement n'@(StatementName STTarget _) _ _)] -> if isOnlyTargetInItsTableau n' tableau then mzero else do + newTableau <- createTableau' False [tagAs (MovedDownFrom tID) h] $ Target [Left targetStatement] + return (MoveDescription [] [] $ "Moved " ++ texSN n ++ ", as the premise of this unexpandable atomic statement can only be used with " ++ texSN n' ++ ".", + s . replaceTargetStatementWithTableau n' newTableau $ Tableau tID tVs (context []) t) + + _ -> mzero + + onTableau _ _ _ = mzero + + + +deleteHypothesisWithUnmatchableConclusion :: MoveType +deleteHypothesisWithUnmatchableConclusion = tableauwise onTableau where + + onTableau :: [Statement] -> Surroundings -> Tableau -> RobotM (MoveDescription, Tableau) + onTableau inheritedHs s tableau@(Tableau tID tVs hs t@(Target ps)) = do + + let visibleHypotheses = filter undeleted $ inheritedHs ++ hypothesesAtAnyDepth tableau + visibleTargets = filter undeleted $ targetFormulaeAtAnyDepth tableau + + --Pick a vulnerable hypothesis + (h@(Statement n f tags), context) <- oneOf $ eachUndeletedHypothesisWithContext hs + guard $ Vulnerable `elem` tags + + --save the state before performning any expansions + state <- getRobotState + + --make sure it's universal + UniversalImplies vs _ c <- return f <|> primaryExpansion f + + matchesPremiseOf' <- matchesPremiseOf'M + matchesConclusionOf' <- matchesConclusionOf'M + + let actualMatches = filter ((c/vs) `matches`) visibleTargets ++ + filter ((c/vs) `matchesPremiseOf'`) visibleHypotheses ++ + filter ((c/vs) `matchesConclusionOf'`) visibleTargets + + --restore the state (so we don't use up any variable names) + putRobotState state + +-- --TODO: If all the actualMatches lie in one tableau, move the hypothesis into that tableau + case actualMatches of + [] -> return (MoveDescription [] [] $ "Deleted " ++ texSN n ++ ", as the conclusion of this implicative statement is unmatchable.", + s $ Tableau tID tVs (context [tagAs Deleted h]) t) + + [targetStatement@(Statement n'@(StatementName STTarget _) _ _)] -> if isOnlyTargetInItsTableau n' tableau then mzero else do + newTableau <- createTableau' False [tagAs (MovedDownFrom tID) h] $ Target [Left targetStatement] + return (MoveDescription [] [] $ "Moved " ++ texSN n ++ ", as the premise of this unexpandable atomic statement can only be used with " ++ texSN n' ++ ".", + s . replaceTargetStatementWithTableau n' newTableau $ Tableau tID tVs (context []) t) + + _ -> mzero + + onTableau _ _ _ = mzero diff --git a/src/Expansion.hs b/src/Expansion.hs new file mode 100755 index 0000000..8125f03 --- /dev/null +++ b/src/Expansion.hs @@ -0,0 +1,82 @@ +{-# LANGUAGE NoMonomorphismRestriction #-} +module Expansion ( + primaryExpansion, allExpansions, isUnexpandable, + rewriteTerm, rewriteFormula +) where + +import Prelude hiding ((/)) +import Control.Applicative +import Control.Arrow +import Control.Monad +import Control.Monad.Trans +import qualified Data.Map as Map +import Data.Map (Map) +import Data.Maybe +import Parser + +import Library +import RobotM +import Types +import Match +import Move + +---------------------------------------------------------------------------------------------------- + +--TODO: consider moving primaryExpansion', isUnexpandable into the RobotM monad + +primaryExpansion' :: Formula -> RobotM (Maybe (Matching, Formula)) +primaryExpansion' f = do + et <- askLibraryExpansionTable + return . listToMaybe $ do + (pattern, expansion) <- et + matching <- maybeToList $ match pattern f + return (matching, expansion) +-- return $ transform matching expansion + +isUnexpandable :: Formula -> RobotM Bool +isUnexpandable f = do + et <- askLibraryExpansionTable + pe <- primaryExpansion' f + return $ isNothing pe + +primaryExpansion :: Formula -> RobotM Formula +primaryExpansion f = do + et <- askLibraryExpansionTable + rt <- askLibraryRewriteTable + pe <- primaryExpansion' f + (matching, expansion) <- oneOf $ maybeToList pe + expansion' <- renameFormula expansion + --rewriteFormulaIfPossible <$> renameFormula f' + rewriteFormulaIfPossible $ transform matching expansion' + +allExpansions :: Formula -> RobotM Formula +allExpansions = primaryExpansion + +---------------------------------------------------------------------------------------------------- + +--NB: this term rewriting code does not use renameFormula -- so DO NOT ever put quantifiers on RHS +-- of the rewrite trable. +-- (This is only relevant if we introduce sets, etc., so that formulae can be inside terms.) + +rewriteTerm :: Term -> RobotM (Maybe Term) +rewriteTerm t = do + rt <- askLibraryRewriteTable + return . listToMaybe $ do + (pattern, vs, rewriteTo) <- rt + matching <- maybeToList $ matchTerm pattern vs t + return $ transformTerm matching rewriteTo + +rewriteTermIfPossible :: Term -> RobotM Term +rewriteTermIfPossible t = do + rewritten <- rewriteTerm t + return . fromMaybe t $ rewritten + +rewriteFormulaIfPossible :: Formula -> RobotM Formula +rewriteFormulaIfPossible = mapTermInFormulaM rewriteTermIfPossible + +rewriteFormula :: Formula -> RobotM (Maybe Formula) +rewriteFormula f = do f' <- mapTermInFormulaM rewriteTermIfPossible f + return $ if f == f' then Nothing else Just f' + +---------------------------------------------------------------------------------------------------- + diff --git a/src/Library.hs b/src/Library.hs new file mode 100755 index 0000000..cfcb83d --- /dev/null +++ b/src/Library.hs @@ -0,0 +1,20 @@ +module Library ( + Library(..), + Result(..), + Solution(..), + ExpansionTable(..), + RewriteTable(..) +) where + +import Types + +data Library = Library [Result] [Solution] ExpansionTable RewriteTable deriving Show + +data Result = Result {-description-} String {-premises-} [Formula] {-conclusion-} Formula + deriving Show + +data Solution = Solution [Variable] [Formula] [Term] {-solution to existence problem-} deriving Show + +type ExpansionTable = [(FormulaWithSlots, Formula)] + +type RewriteTable = [(Term, [Variable], Term)] diff --git a/src/Main.hs b/src/Main.hs new file mode 100755 index 0000000..2c71761 --- /dev/null +++ b/src/Main.hs @@ -0,0 +1,170 @@ +module Main ( + main +) where + +import Prelude hiding ((/)) + +import Control.Arrow +import Control.Monad +import Control.Applicative +import Data.Maybe +import Data.Either +import qualified Data.Map as Map +import Data.Map (Map) +import Data.List +import Control.Monad.Logic +import Control.Monad.Trans.List +import Control.Monad.Trans.State.Lazy +import Control.Monad.Identity hiding (msum) + +import Debug.Trace + +import Types +import Rename +import Expansion +import Match +import TexBase +import Move +import Parser +import Tex +import RobotM +import Library +import Writeup +import Printing + +import DeletionMoves +import TidyingMoves +import ApplyingMoves +import Suspension + +import qualified TestData + +---------------------------------------------------------------------------------------------------- + +moveTypesByPriority :: [MoveType] +moveTypesByPriority = [ + --Deletion + deleteDone, + deleteDoneDisjunct, +-- deleteRedundantHypothesis, --move 1 + deleteDangling, --move 2 + deleteUnmatchable, -- move 3 + --Tidying (4-9) + peelAndSplitUniversalConditionalTarget, --move 4 +-- flipNegativeTarget, --move 5 +-- flipNegativeHypothesis, --move 6 + splitDisjunctiveHypothesis, --move 7 +-- splitConjunctiveTarget, --move 8 + splitDisjunctiveTarget, + peelBareUniversalTarget, -- move 9 + removeTarget, --move 10 + collapseSubtableauTarget, + --Applying + forwardsReasoning, --move 11 + forwardsLibraryReasoning, --move 11 + expandPreExistentialHypothesis, --move 13 + elementaryExpansionOfHypothesis, --move 12 + backwardsReasoning, --move 14 + backwardsLibraryReasoning, --move 14 + elementaryExpansionOfTarget, --move 15 + expandPreUniversalTarget, --move 16 + solveBullets, + automaticRewrite, + --Suspension + unlockExistentialUniversalConditionalTarget, --move 17 + unlockExistentialTarget, + expandPreExistentialTarget, + convertDiamondToBullet, + rewriteVariableVariableEquality, + rewriteVariableTermEquality + ] + +allMovesByPriority :: Tableau -> [RobotM (MoveDescription, Tableau)] +allMovesByPriority t = [f t | (MoveType f) <- moveTypesByPriority] + +---------------------------------------------------------------------------------------------------- + +lengthAtLeast :: Int -> [a] -> Bool +lengthAtLeast 0 _ = True +lengthAtLeast _ [] = False +lengthAtLeast n (_:xs) = lengthAtLeast (n-1) xs + +---------------------------------------------------------------------------------------------------- + +printMax = 100 + +main = do + let pd = TestData.printingData + lib = TestData.library + + let movesFrom :: RobotState -> Tableau -> [(MoveDescription, Tableau)] + movesFrom s t = case mapMaybe (runRobotM pd lib s) (allMovesByPriority t) of + [] -> [] + (move@(MoveDescription _ _ _, t'), s'):_ -> move:movesFrom s' t' + + solve :: Problem -> (Tableau, [(MoveDescription, Tableau)]) + solve (Problem _ hs t) = + let initialTableauM = createTableau False (parse formula <$> hs) $ parse formula t + Just (initialTableau, s) = runRobotM pd lib initialRobotState initialTableauM + in (initialTableau, movesFrom s initialTableau) + + -- printMove: prints oldTableau + move text + printMove :: Int -> Tableau -> MoveDescription -> IO () + printMove n oldTableau (MoveDescription statementsUsed clauses text) = do + putStrLn . fit $ texTableauBolding pd statementsUsed oldTableau + putStrLn "\\smallskip" + putStrLn "" + putStrLn $ {-trace (show n ++ ". " ++ text) $-} "\\noindent" ++ show n ++ ". " ++ text ++ "\\nopagebreak[4] " + putStrLn $ "\\marginpar{" ++ unwords (asSentence . writeup pd <$> clauses) ++ "}" ++ "\\nopagebreak[4] " + putStrLn $ "\\smallskip" ++ "\\nopagebreak[4] " + putStrLn "" + + printSolution :: Int -> Problem -> IO () + printSolution max p = + let (initialTableau, moves) = solve p + (moveDescriptions, outputTableaux) = unzip moves + proof = compress . eliminate . fuse $ concat [cs | MoveDescription _ cs _ <- moveDescriptions] + + in if null moves + then putStrLn (fit $ tex pd initialTableau) >> putStrLn "No moves possible." + else do + -- putStrLn "\\begin{center}" + -- putStrLn "\\vspace{-3mm}" + -- putStrLn . fit $ tex initialTableau + -- putStrLn "\\end{center}" + when (not $ lengthAtLeast (max+1) moves) $ do + putStrLn "\\begin{center}" + putStrLn "\\begin{minipage}{120mm}" + putStrLn . unwords $ asSentence . writeup pd <$> proof + putStrLn "\\end{minipage}" + putStrLn "\\end{center}" + putStrLn "" + putStrLn "\\bigskip" + + putStrLn "\\begin{steps}" + sequence_ $ zipWith3 printMove [1..max] (initialTableau:outputTableaux) moveDescriptions + putStrLn . fit . tex pd . last . take max $ outputTableaux --print final tableau + putStrLn "" + if lengthAtLeast (max+1) moves + then putStrLn $ show max ++ " moves made; stopping as the Robot may be in an infinite loop." + else case last moves of + (_, Done _) -> trace ("\t" ++ show (length moves) ++ " moves made; problem solved.") $ + putStrLn "Problem solved." + _ -> trace ("\t" ++ show (length moves) ++ " moves made.") $ + putStrLn "No moves possible." + putStrLn "\\cleardoublepage\n" + putStrLn "\\end{steps}" --} + + attemptProblem :: Problem -> IO () + attemptProblem p@(Problem description _ _) = do + -- putStrLn "\\vspace{-3mm}" + putStrLn $ "{\\begin{center} \\large " ++ textbf description ++ "\\end{center}}\\nopagebreak[4]" + putStrLn "" + printSolution printMax p + + + putStrLn texHeader + mapM_ attemptProblem TestData.problems + putStrLn texFooter + +---------------------------------------------------------------------------------------------------- diff --git a/src/Match.hs b/src/Match.hs new file mode 100755 index 0000000..6a045a9 --- /dev/null +++ b/src/Match.hs @@ -0,0 +1,351 @@ +{-# LANGUAGE NoMonomorphismRestriction #-} + +module Match ( + FormulaWithSlots(..), (/), + Matching, + match, matchTerm, + emptyMatching, extendMatch, + transform, transformTerm, + twoWayMatchExists, + isIsomorphic, + matchFormulaeAmongStatements, matchFormulaeAmongFormulae, + matchSomeOfFormulaeAmongStatements, + extendMatchAllButOneOfFormulaeAmongStatements +) where + + +import Prelude hiding ((/)) +import qualified Data.Map as Map +import Data.Maybe +import Data.Map (Map) +import Control.Applicative +import Control.Monad +import Control.Monad.Trans +import Control.Monad.Trans.State.Lazy + +import Debug.Trace + +import Types +import Move +import RobotM + +---------------------------------------------------------------------------------------------------- + +type Matching = Map Variable Term + +type MatchingM = State (Maybe Matching) +emptyMatching = Map.empty +getMatching = get +putMatching = put +modifyMatching = modify + +execMatching :: Matching -> MatchingM () -> Maybe Matching +execMatching m = flip execState (Just m) + +--match vs f f' : try to instantiate vs in f to make it match f' +--NB: will not match 'a and b' with 'b and a' (same for 'or', 'forall', 'exists'). + +match :: FormulaWithSlots -> Formula -> Maybe Matching +match = extendMatch emptyMatching + +extendMatch :: Matching -> FormulaWithSlots -> Formula -> Maybe Matching +extendMatch matching (FormulaWithSlots f renamable) f' = execMatching matching $ onFormula f f' where + onFormula :: Formula -> Formula -> MatchingM () + onFormula (AtomicFormula pred args) (AtomicFormula pred' args') + | pred == pred' = zipWithM_ onTerm args args' + onFormula (Not f) (Not f') = onFormula f f' + onFormula (And fs) (And f's) + | length fs == length f's = zipWithM_ onFormula fs f's + onFormula (Or fs) (Or f's) + | length fs == length f's = zipWithM_ onFormula fs f's + onFormula (Forall vs f) (Forall v's f') + | length vs == length v's = + sequence_ $ zipWith variableWithTerm vs (map VariableTerm v's) ++ + [onFormula f f'] + onFormula (UniversalImplies vs ls r) (UniversalImplies v's l's r') + | length vs == length v's && length ls == length l's = + sequence_ $ zipWith variableWithTerm vs (map VariableTerm v's) ++ + zipWith onFormula ls l's ++ + [onFormula r r'] + onFormula (Exists vs f) (Exists v's f') + | length vs == length v's = + sequence_ $ zipWith variableWithTerm vs (map VariableTerm v's) ++ + [onFormula f f'] + onFormula _ _ = put Nothing + + onTerm :: Term -> Term -> MatchingM () + onTerm (ApplyFn fn args) (ApplyFn fn' args') + | fn == fn' && length args == length args' = zipWithM_ onTerm args args' + onTerm (VariableTerm v) t = variableWithTerm v t + onTerm _ _ = put Nothing + + variableWithTerm :: Variable -> Term -> MatchingM () + variableWithTerm v t + | v `elem` renamable = do + mMatching <- getMatching + case mMatching of + Nothing -> return () + Just matching -> case Map.lookup v matching of + Just t' -> unless (t == t') $ put Nothing + Nothing -> put . Just $ Map.insert v t matching + variableWithTerm v (VariableTerm v') + | v == v' = return () + variableWithTerm _ _ = put Nothing + + +matchTerm :: Term -> [Variable] -> Term -> Maybe Matching +matchTerm t renamable t' = execMatching emptyMatching $ onTerm t t' where + onTerm :: Term -> Term -> MatchingM () + onTerm (ApplyFn fn args) (ApplyFn fn' args') + | fn == fn' && length args == length args' = zipWithM_ onTerm args args' + onTerm (VariableTerm v) t = variableWithTerm v t + onTerm _ _ = put Nothing + + variableWithTerm :: Variable -> Term -> MatchingM () + variableWithTerm v t + | v `elem` renamable = do + mMatching <- getMatching + case mMatching of + Nothing -> return () + Just matching -> case Map.lookup v matching of + Just t' -> unless (t == t') $ put Nothing + Nothing -> put . Just $ Map.insert v t matching + variableWithTerm v (VariableTerm v') + | v == v' = return () + variableWithTerm _ _ = put Nothing + + + +transform :: Matching -> Formula -> Formula +transform = mapDirectTermInFormula . transformTerm + +transformTerm :: Matching -> Term -> Term +transformTerm matching = mapTerm shallow where + shallow :: Term -> Term + shallow t@(VariableTerm v) = fromMaybe t (Map.lookup v matching) + shallow t = t + + + +---------------------------------------------------------------------------------------------------- + +-- Code for matching two formulas, both of which have slots. ('Two-way matching') +--this requires us to set up some machinery for unification. + +--NB. Do not use this code with bulleted variables as 'slots', as it ignores all (in)dependencies. + +data Equation = Term :=: Term + +instance Pretty Equation where + pretty (t :=: t') = pretty t ++ " <---> " ++ pretty t' + +variableEquation :: Variable -> Variable -> Equation +variableEquation v v' = VariableTerm v :=: VariableTerm v' + +--extractEquations: Match up the corresponding terms inside two formulae and +-- return the resulting equations. If matching fails, return Nothing. +extractEquations :: Formula -> Formula -> Maybe [Equation] +extractEquations (AtomicFormula p ts) (AtomicFormula p' t's) = + guard (p == p') >> return (zipWith (:=:) ts t's) +extractEquations (Not f) (Not f') = extractEquations f f' +extractEquations (And fs) (And f's) = do + guard (length fs == length f's) + concat <$> zipWithM extractEquations fs f's +extractEquations (Or fs) (Or f's) = do + guard (length fs == length f's) + concat <$> zipWithM extractEquations fs f's +extractEquations (Forall vs f) (Forall v's f') = do + guard (length vs == length v's) + innerEs <- extractEquations f f' + return $ zipWith variableEquation vs v's ++ innerEs +extractEquations (UniversalImplies vs as c) (UniversalImplies v's a's c') = do + guard (length vs == length v's) + guard (length as == length a's) + innerAntecedentEs <- concat <$> zipWithM extractEquations as a's + innerConsequentEs <- extractEquations c c' + return $ zipWith variableEquation vs v's ++ innerAntecedentEs ++ innerConsequentEs +extractEquations (Exists vs f) (Exists v's f') = do + guard (length vs == length v's) + innerEs <- extractEquations f f' + return $ zipWith variableEquation vs v's ++ innerEs +extractEquations _ _ = Nothing + + +--TODO: rewrite occursIn using the Any monoid +occursIn :: Variable -> Term -> Bool +occursIn v = or . accumulateVariableInTerm (return . (== v)) + +--we don't want the matching algorithm to recurse into dependencies, so we will simply strip them out +removeDependencies :: Variable -> Variable +removeDependencies (Variable n id t b _) = Variable n id t b (Dependencies [] []) + +removeDependenciesFromFormula :: Formula -> Formula +removeDependenciesFromFormula = mapVariableInFormula removeDependencies + +--eliminate v r me = me[v := r] +eliminate :: Variable -> Term -> Equation -> Equation +eliminate v r (a :=: b) = onTerm a :=: onTerm b where + onTerm = mapTerm shallow + shallow (VariableTerm v') + | v == v' = r + shallow t = t + +--twoWayMatchExists (FormulaWithSlots f vs) (FormulaWithSlots f' v's) : +-- try to instantiate vs in f and v's in f' to make them match +--NB. Assumes there is no variable collision between f and f'. +twoWayMatchExists :: FormulaWithSlots -> FormulaWithSlots -> Bool +twoWayMatchExists (FormulaWithSlots f vs) (FormulaWithSlots f' v's) = + let renamableVs :: [Variable] + renamableVs = removeDependencies <$> (vs ++ v's) + + renamable :: Variable -> Bool + renamable = (`elem` renamableVs) + + --areSolvable es: is it possible to solve es by renaming vars? + -- method: repeatedly remove a variable in all equations + areSolvable :: [Equation] -> Bool + areSolvable (vt@(VariableTerm v) :=: vt'@(VariableTerm v') : es) + | v == v' = areSolvable es + | renamable v = areSolvable $ eliminate v vt' <$> es + | renamable v' = areSolvable $ eliminate v' vt <$> es + | otherwise = False + + areSolvable (vt@(VariableTerm v) :=: t' : es) + | v `occursIn` t' = False --can't match e.g. x and f(x) + | renamable v = areSolvable $ eliminate v t' <$> es + | otherwise = False + + areSolvable (t :=: vt'@(VariableTerm v') : es) + | v' `occursIn` t = False --can't match e.g. x and f(x) + | renamable v' = areSolvable $ eliminate v' t <$> es + | otherwise = False + + areSolvable (ApplyFn fn ts :=: ApplyFn fn' t's : es) + | fn == fn' && length ts == length t's = areSolvable $ zipWith (:=:) ts t's ++ es + | otherwise = False + + areSolvable [] = True + + in case extractEquations (removeDependenciesFromFormula f) (removeDependenciesFromFormula f') of + Nothing -> False --formulae didn't match up + Just es -> areSolvable es + +--twoWayMatch (FormulaWithSlots f vs) (FormulaWithSlots f' []) = match (FormulaWithSlots f vs) f' --TODO: ***STUB*** + +---------------------------------------------------------------------------------------------------- + +isVariableTerm :: Term -> Bool +isVariableTerm (VariableTerm _) = True +isVariableTerm _ = False + +isIsomorphic :: [Variable] -> Formula -> Formula -> Bool +isIsomorphic bound f f' = case match (FormulaWithSlots f bound) f' of + Nothing -> False + Just matching -> and [isVariableTerm t | t <- Map.elems matching] + +---------------------------------------------------------------------------------------------------- + +--pv = parse variable +--pvs = map (parse variable) . words +--pf = parse formula +-- +--a = pf "lessthan(d(x, y), delta)" / pvs "x y" +--b = pf "lessthan(d(applyfn(f,c), applyfn(f,d)), epsilon)" / pvs "epsilon" + +---------------------------------------------------------------------------------------------------- + +--TODO: have changed all 'context []' to ss/f's. They now no longer need to be local variables of the 'go' functions. + +--matchFormulaeAmongStatements vs fs ss: try to match all of fs (with vs as slots) against some of ss, +-- and if successful return match + names of ss used. +matchFormulaeAmongStatements :: [Variable] -> [Formula] -> [Statement] -> RobotM (Matching, [StatementName]) +matchFormulaeAmongStatements vs = go emptyMatching [] where + + go :: Matching -> [StatementName] -> [Formula] -> [Statement] -> RobotM (Matching, [StatementName]) + go m ns (f:fs) ss = do + --pick a given statement + (Statement n f' _, context) <- oneOf $ eachElementWithContext ss + + --try to match it with the first given formula + m' <- oneOf . maybeToList $ extendMatch m (f / boundVariablesInFormula f ++ vs) f' + + --move on to the next statement + go m' (ns ++ [n]) fs ss + + go m ns [] _ = return (m,ns) + + +--matchFormulaeAmongFormulae vs fs ss: try to match all of fs (with vs as slots) against some of f's, +-- and if successful return match . +matchFormulaeAmongFormulae :: [Variable] -> [Formula] -> [Formula] -> RobotM Matching +matchFormulaeAmongFormulae vs = go emptyMatching where + + go :: Matching -> [Formula] -> [Formula] -> RobotM Matching + go m (f:fs) f's = do + --pick one of the f's + (f', context) <- oneOf $ eachElementWithContext f's + + --try to match it with the first lhs formula + m' <- oneOf . maybeToList $ extendMatch m (f / boundVariablesInFormula f ++ vs) f' + + --move on to the next statement + go m' fs f's + + go m [] _ = return m + +----matchTermsAmongTerms vs ts ss: try to match all of ts (with vs as slots) against some of t's, +---- and if successful return match . +--matchTermsAmongTerms :: [Variable] -> [Term] -> [Term] -> RobotM Matching +--matchTermsAmongTerms vs = go emptyMatching where +-- +-- go :: Matching -> [Term] -> [Term] -> RobotM Matching +-- go m (t:ts) t's = do +-- --pick one of the t's +-- (t', context) <- oneOf $ eachElementWithContext t's +-- +-- --try to match it with the first lhs Term +-- m' <- oneOf . maybeToList $ extendMatchTerm m (t / boundVariablesInFormula t ++ vs) t' +-- +-- --move on to the next statement +-- go m' ts (context []) +-- +-- go m [] _ = return m + + +extendMatchAllButOneOfFormulaeAmongStatements :: Matching -> [Variable] -> [Formula] -> [Statement] -> RobotM (Matching, [StatementName], Formula) +extendMatchAllButOneOfFormulaeAmongStatements m vs = go m [] Nothing where + + go :: Matching -> [StatementName] -> Maybe Formula -> [Formula] -> [Statement] -> RobotM (Matching, [StatementName], Formula) + go m ns Nothing [] _ = error "matchAllButOneOfFormulaeAmongStatements called with no formulae." + go m ns Nothing [f] _ = return (m,ns,f) + go m ns mLeftoverF (f:fs) ss = do + --pick a given statement + (Statement n f' _, context) <- oneOf $ eachElementWithContext ss + + --try to match it with the first given formula + case extendMatch m (f / boundVariablesInFormula f ++ vs) f' of + Just m' -> go m' (ns ++ [n]) mLeftoverF fs ss --keep going + Nothing -> case mLeftoverF of + Just _ -> mzero --two leftover formulae + Nothing -> go m ns (Just f) fs ss --first unmatchable formula found + + go m ns (Just l) [] _ = return (m,ns,l) + + +matchSomeOfFormulaeAmongStatements :: [Variable] -> [Formula] -> [Statement] -> RobotM (Matching, [StatementName], [Formula]) +matchSomeOfFormulaeAmongStatements = extendMatchSomeOfFormulaeAmongStatements emptyMatching + +extendMatchSomeOfFormulaeAmongStatements :: Matching -> [Variable] -> [Formula] -> [Statement] -> RobotM (Matching, [StatementName], [Formula]) +extendMatchSomeOfFormulaeAmongStatements m vs = go m [] [] where + + go :: Matching -> [StatementName] -> [Formula] -> [Formula] -> [Statement] -> RobotM (Matching, [StatementName], [Formula]) + go m ns leftovers (f:fs) ss = do + --pick a given statement + (Statement n f' _, context) <- oneOf $ eachElementWithContext ss + + --try to match it with the first given formula + case extendMatch m (f / boundVariablesInFormula f ++ vs) f' of + Just m' -> go m' (ns ++ [n]) leftovers fs ss --keep going + Nothing -> go m ns (leftovers ++ [f]) fs ss --first unmatchable formula found + + go m ns leftovers [] _ = return (m,ns,leftovers) diff --git a/src/Move.hs b/src/Move.hs new file mode 100755 index 0000000..0312dfd --- /dev/null +++ b/src/Move.hs @@ -0,0 +1,242 @@ +module Move + + where + +import Control.Applicative +import Control.Arrow +--import Control.Monad.RWS hiding (msum) +import Control.Monad.Logic hiding (msum) +import Control.Monad.Trans.List +import Control.Monad.Trans.State.Lazy +import Control.Monad.Identity hiding (msum) +--import Control.Monad +import Data.Either +import Data.List (nub, sort, intersect) +import Data.Maybe +import Data.Map hiding (map, filter, null) +import Data.Foldable (msum) + +import Types +import RobotM +import Writeup + + +---------------------------------------------------------------------------------------------------- + +--renameFormula :: NextFreeIDState -> Formula -> (Formula, NextFreeIDState) + + + +data MoveDescription = MoveDescription [StatementName] [Clause] String +data MoveType = MoveType (Tableau -> RobotM (MoveDescription, Tableau)) + +movetypeFromSubmovetypes :: [MoveType] -> MoveType +movetypeFromSubmovetypes ms = MoveType $ \t -> msum [f t | MoveType f <- ms] +---------------------------------------------------------------------------------------------------- + +type Surroundings = Tableau -> Tableau + +-- tableauwise: construct a type of move that operates on each subtableau, +-- using knowledge of a) inherited hypotheses and +-- b) the 'Surroundings', i.e. an embedding of subtableau into main tableau +tableauwise :: ([Statement] -> Surroundings -> Tableau -> RobotM (MoveDescription, Tableau)) -> MoveType +tableauwise = MoveType . tableauwise' + +--z :: TableauName -> TableauName +--z (TableauName n) = TableauName $ n + 100 + +tableauwise' :: ([Statement] -> Surroundings -> Tableau -> RobotM (MoveDescription, Tableau)) + -> Tableau + -> RobotM (MoveDescription, Tableau) +tableauwise' f t@(Tableau tID vs hs (Target ps)) = f [] id t <|> do + (p, context) <- oneOf $ eachElementWithContext ps + case p of + Left _ -> mzero + Right t's -> do + (t', disjunctContext) <- oneOf $ eachElementWithContext t's + let f' :: [Statement] -> Surroundings -> Tableau -> RobotM (MoveDescription, Tableau) + f' is s = f (is ++ hs) (Tableau tID vs hs . Target . context . return . Right . disjunctContext . return . s) + + tableauwise' f' t' + +tableauwise' f t@(Tableau _ _ _ Contradiction) = f [] id t +tableauwise' f t@(Done _) = f [] id t + +--eltBeforeAfter [1,2,3,4] = [(1,([],[2,3,4])),(2,([1],[3,4])),(3,([1,2],[4])),(4,([1,2,3],[]))] +eltBeforeAfter :: [a] -> [(a, ([a], [a]))] +eltBeforeAfter [] = [] +eltBeforeAfter (a:as) = (a, ([], as)) : map (second (first (a:))) (eltBeforeAfter as) + +--eachElementWithContext [1,2,3,4] = +-- [(1,\as->[]++as++[2,3,4]), +-- (2,\as->[1]++as++[3,4]), +-- (3,\as->[1,2]++as++[4]), +-- (4,\as->[1,2,3]++as++[])] +eachElementWithContext :: [a] -> [(a, [a] -> [a])] +eachElementWithContext = map (second glueBeforeAfter) . eltBeforeAfter where + --glueBeforeAfter ([10,11], [20, 21]) [90, 91] = [10,11,90,91,20,21] + glueBeforeAfter :: ([a], [a]) -> [a] -> [a] + glueBeforeAfter (before, after) as = before ++ as ++ after + +eachElementWithContextPair :: [a] -> [(a, a, [a] -> [a] -> [a])] +eachElementWithContextPair = concatMap f . eachElementWithContextPair' where + f (a, a', context) = [(a, a', context), (a', a, flip context)] + +eachElementWithContextPair' :: [a] -> [(a, a, [a] -> [a] -> [a])] +eachElementWithContextPair' as = do + (a, (beforeA, afterA)) <- eltBeforeAfter as + (a', (mid, afterA')) <- eltBeforeAfter afterA + let f x y = beforeA ++ x ++ mid ++ y ++ afterA' + return (a, a', f) + +---------------------------------------------------------------------------------------------------- +-- +--allVariablesInFormula :: Formula -> [Variable] +--allVariablesInFormula = nub . sort . accumulateVariableInFormula return + +boundVariablesInFormula :: Formula -> [Variable] +boundVariablesInFormula = nub . sort . accumulateFormula immediate where + immediate :: Formula -> [Variable] + immediate (AtomicFormula _ _) = [] + immediate (Not _) = [] + immediate (And _) = [] + immediate (Or _) = [] + immediate (Forall vs _) = vs + immediate (UniversalImplies vs _ _) = vs + immediate (Exists vs _) = vs + + +boundExistentialVariablesInFormula :: Formula -> [Variable] +boundExistentialVariablesInFormula = nub . sort . accumulateFormula immediate where + immediate :: Formula -> [Variable] + immediate (AtomicFormula _ _) = [] + immediate (Not _) = [] + immediate (And _) = [] + immediate (Or _) = [] + immediate (Forall vs _) = [] + immediate (UniversalImplies vs _ _) = [] + immediate (Exists vs _) = vs + +boundUniversalVariablesInFormula :: Formula -> [Variable] +boundUniversalVariablesInFormula = nub . sort . accumulateFormula immediate where + immediate :: Formula -> [Variable] + immediate (AtomicFormula _ _) = [] + immediate (Not _) = [] + immediate (And _) = [] + immediate (Or _) = [] + immediate (Forall vs _) = vs + immediate (UniversalImplies vs _ _) = vs + immediate (Exists vs _) = [] + +---------------------------------------------------------------------------------------------------- + +hypothesesAtAnyDepth = accumulateTableau extractHypotheses where + extractHypotheses (Tableau _ _ h's _) = h's + +targetFormulaeAtAnyDepth = accumulateTableau extractTargetFormulae where + extractTargetFormulae (Tableau _ _ _ (Target ps)) = lefts ps + +---------------------------------------------------------------------------------------------------- + +tagAs :: Tag -> Statement -> Statement +tagAs t s@(Statement n f ts) + | t `elem` ts = s + | otherwise = Statement n f $ ts ++ [t] + +tagStatementInTableauAs :: Tag -> StatementName -> Tableau -> Tableau +tagStatementInTableauAs tag n = mapTableau shallow where + shallow (Tableau id vs hs (Target ps)) = Tableau id vs (onStatement <$> hs) . Target $ either (Left . onStatement) Right <$> ps + shallow (Tableau id vs hs Contradiction) = Tableau id vs (onStatement <$> hs) Contradiction + shallow d@(Done _) = d + onStatement s'@(Statement n' _ _) + | n == n' = tagAs tag s' + | otherwise = s' + + +deleted :: Statement -> Bool +deleted (Statement _ _ tags) = Deleted `elem` tags + +undeleted :: Statement -> Bool +undeleted = not . deleted + +eachUndeletedHypothesisWithContext :: [Statement] -> [(Statement, [Statement] -> [Statement])] +eachUndeletedHypothesisWithContext = filter (undeleted . fst) . eachElementWithContext + +eachUndeletedHypothesisPairWithContext :: [Statement] -> [(Statement, Statement, [Statement] -> [Statement] -> [Statement])] +eachUndeletedHypothesisPairWithContext ss = [(s, s', c) | (s, s', c) <- eachElementWithContextPair ss, undeleted s, undeleted s'] + +type TP = Either Statement [Tableau] + +undeletedTP :: TP -> Bool +undeletedTP (Left s) = undeleted s +undeletedTP (Right _) = True + +eachUndeletedTargetPartWithContext :: [TP] -> [(TP, [TP] -> [TP])] +eachUndeletedTargetPartWithContext = filter (undeletedTP . fst) . eachElementWithContext + + +---------------------------------------------------------------------------------------------------- + + +addDependencies :: [Variable] -> Variable -> Variable +addDependencies vs (Variable n id t b (Dependencies ds is)) = Variable n id t b (Dependencies (map VariableTerm vs ++ ds) is) + +--markDependencies:: Every time you see a \exists, That the dependency of its variable on all +-- Previous universally quantified variables +-- e.g. Aa Eb Ac Ed P(a,b,c,d) --> Aa Eb[a] Ac Ed[a,c] P(a,b[a],c,d[a,c]) +markDependencies :: Formula -> Formula +markDependencies = mapFormula shallow where + shallow f@(AtomicFormula _ _) = f + shallow f@(Not _) = f + shallow f@(And fs) = f + shallow f@(Or _) = f + shallow (Forall vs c) = Forall vs (addD c) where + addD = mapFormula (addDependencyToExistential vs) + shallow (UniversalImplies vs as c) = UniversalImplies vs (map addD as) (addD c) where + addD = mapFormula (addDependencyToExistential vs) + shallow f@(Exists _ _) = f + + addDependencyToExistential :: [Variable] -> Formula -> Formula + addDependencyToExistential vs f@(AtomicFormula _ _) = f + addDependencyToExistential vs f@(Not _) = f + addDependencyToExistential vs f@(And fs) = f + addDependencyToExistential vs f@(Or _) = f + addDependencyToExistential vs f@(Forall _ _) = f + addDependencyToExistential vs f@(UniversalImplies _ _ _) = f + addDependencyToExistential vs f@(Exists v's _) = mapVariableInFormula mark f where + mark v + | v `elem` v's = addDependencies vs v + | otherwise = v + + +---------------------------------------------------------------------------------------------------- + +isBulletedVariableChoiceLegal :: VariableChoice -> Bool +isBulletedVariableChoiceLegal (VariableChoice (Variable _ _ _ _ (Dependencies _ is)) t) = + let ivs, dvs :: [Variable] + ivs = nub . sort $ concatMap (accumulateVariableInTerm return) is + dvs = accumulateVariableInTerm return t + in null $ intersect ivs dvs --TODO: loglinear comparison + +---------------------------------------------------------------------------------------------------- + +-- markBulletedIndependencies vs tableau: mark every bulleted variable in tableau as being independent of vs +markBulletedIndependencies :: [Variable] -> Tableau -> Tableau +markBulletedIndependencies vs = mapVariableInTableau shallow where + shallow (Variable n id t VTDiamond (Dependencies ds is)) = Variable n id t VTDiamond $ Dependencies ds (is ++ map VariableTerm vs) + shallow (Variable n id t VTBullet (Dependencies ds is)) = Variable n id t VTBullet $ Dependencies ds (is ++ map VariableTerm vs) + shallow v = v + +---------------------------------------------------------------------------------------------------- + + + +conjuncts :: Formula -> [Formula] +conjuncts f@(AtomicFormula _ _) = [f] +conjuncts f@(Not _) = [f] +conjuncts f@(And fs) = concatMap conjuncts fs +conjuncts f@(Or _) = [f] +conjuncts f@(Forall _ _) = [f] +conjuncts f@(UniversalImplies _ _ _) = [f] +conjuncts f@(Exists _ f') = [f] + diff --git a/src/Parser.hs b/src/Parser.hs new file mode 100755 index 0000000..680d151 --- /dev/null +++ b/src/Parser.hs @@ -0,0 +1,163 @@ +module Parser ( + Parser.parse, + variable, + term, + formula +) where + + +import Control.Applicative hiding (many, (<|>)) +import qualified Data.Map as Map +import Data.Map (Map, (!)) + +--import Text.Parsec.Text.Lazy +import Text.Parsec.String +import Text.Parsec.Char +import Text.Parsec.Combinator +import Text.Parsec.Prim +import Text.Parsec.Error + +import Types + + +---------------------------------------------------------------------------------------------------- + +parse :: Parser a -> String -> a +parse p = either (error . show) id . Text.Parsec.Prim.parse p "" + +tryInTurn :: [Parser a] -> Parser a +tryInTurn = foldl1 (<|>) . map try + +---------------------------------------------------------------------------------------------------- + +bracketed :: Parser a -> Parser a +bracketed p = string "(" *> spaces *> p <* spaces <* string ")" + +punct :: String -> Parser String +punct s = spaces *> string s <* spaces + +spaces1 = many1 space + +---------------------------------------------------------------------------------------------------- + +conventionalTypes = Map.fromList [ + ("a", TPoint), + ("b", TPoint), + ("f", TFunction), + ("g", TFunction), + ("h", TFunction), + ("n", TNaturalNumber), + ("x", TPoint), + ("y", TPoint), + ("z", TPoint), + ("u", TPoint), + ("v", TPoint), + ("w", TPoint), + ("p", TPoint), + ("q", TPoint), + ("r", TPoint), + ("s", TPoint), + ("t", TPoint), + ("A", TSet), + ("B", TSet), + ("C", TSet), + ("D", TSet), + ("F", TSet), + ("H", TGroup), + ("K", TGroup), + ("N", TNaturalNumber), + ("U", TSet), + ("V", TSet), + ("X", TSet), + ("alpha", TPositiveRealNumber), + ("beta", TPositiveRealNumber), + ("gamma", TPositiveRealNumber), + ("delta", TPositiveRealNumber), + ("epsilon", TPositiveRealNumber), + ("eta", TPositiveRealNumber), + ("theta", TPositiveRealNumber), + ("an", TSequence) + ] + +---------------------------------------------------------------------------------------------------- + +function :: Parser Function +function = Function <$> many1 alphaNum + +predicate :: Parser Predicate +predicate = Predicate <$> many1 alphaNum + +variable :: Parser Variable +variable = do + n <- many1 letter + ps <- many $ char '\'' + let t = Map.findWithDefault (error $ "Variable " ++ n ++ " does not have a conventional type.") n conventionalTypes + return $ Variable n (length ps + 1) t VTNormal (Dependencies [] []) + +term :: Parser Term +term = tryInTurn [ + ApplyFn <$> function <*> bracketed (sepBy term (try $ punct ",")), + VariableTerm <$> variable + ] + + +--rule_exp :: Parser RuleExp +--rule_exp = foldl (flip ($)) <$> rule_exp'' +-- <*> many (try_in_turn modifiers) "Semantic expression" +-- +--modifiers :: [Parser (RuleExp -> RuleExp)] +--modifiers = +-- [flip Apply <$> (whites *> bracketed rule_exp), +-- flip DRSMerge <$> space_then_oplus_exp, +-- flip PluralSum <$> (punct "&" *> rule_exp)] +-- +--space_then_oplus_exp :: Parser RuleExp +--space_then_oplus_exp = whites *> (string "⊕" <|> string "++") *> whites *> rule_exp + +--TODO: parse negated formulae + +formula :: Parser Formula --a conjunction of formula''s +formula = do + ps <- sepBy1 formula' (try $ punct "|") + case ps of + [p] -> return p + _ -> return $ Or ps + +formula' :: Parser Formula --a conjunction of formula''s +formula' = do + ps <- sepBy1 formula'' (try $ punct "&") + case ps of + [p] -> return p + _ -> return $ And ps + +formula'' :: Parser Formula +formula'' = tryInTurn [ + bracketed formula, + Not <$> (string "¬" *> formula''), + forall_, + univCond, + exists, + AtomicFormula <$> predicate <*> bracketed (sepBy term (try $ punct ",")) + ] + + +forall_ :: Parser Formula +forall_ = Forall <$> (string "forall " *> spaces *> sepBy variable spaces1) + <*> (punct ".(" *> formula <* spaces <* string ")") + +univCond :: Parser Formula +univCond = UniversalImplies <$> (string "forall " *> spaces *> sepBy variable spaces1) + <*> (punct ".(" *> sepBy1 formula'' (try $ punct "&")) + <*> (punct "=>" *> formula <* spaces <* string ")") + + +exists :: Parser Formula +exists = Exists <$> (string "exists " *> spaces *> sepBy variable spaces1) + <*> (punct ".(" *> formula <* spaces <* string ")") + +testF = "forall x.(in(x, intersect(A, B)) => exists delta.(forall y.(lessthan(d(x, y), delta) => in(y, intersect(A, B)))))" +testF2 = "forall y.(lessthan(d(x, y), delta) => in(y, intersect(A, B)))" +testF3 = "exists delta.(in(y, intersect(A, B)) & lessthan(d(x, y), delta))" +pu = Parser.parse univCond +pe = Parser.parse exists + diff --git a/src/Printing.hs b/src/Printing.hs new file mode 100755 index 0000000..2fdc228 --- /dev/null +++ b/src/Printing.hs @@ -0,0 +1,24 @@ +module Printing ( + Pattern, instantiatePattern, + PrintingData(..) +) where + +import Data.Map (Map, (!)) +import qualified Data.Map as Map + +---------------------------------------------------------------------------------------------------- + +type Pattern = String + +instantiatePattern :: Pattern -> [String] -> String +instantiatePattern ('%':cs) (s:ss) = s ++ instantiatePattern cs ss +instantiatePattern (c:cs) ss = c : instantiatePattern cs ss +instantiatePattern [] [] = "" + +data PrintingData = PrintingData { + termPatterns :: Map String Pattern, + formulaPatterns :: Map String Pattern, + nounPatterns :: Map String Pattern, + adjectivePatterns :: Map String Pattern + } deriving Show + diff --git a/src/Rename.hs b/src/Rename.hs new file mode 100755 index 0000000..bb89622 --- /dev/null +++ b/src/Rename.hs @@ -0,0 +1,2 @@ +{-# LANGUAGE NoMonomorphismRestriction #-} +module Rename ( ) where diff --git a/src/RobotM.hs b/src/RobotM.hs new file mode 100755 index 0000000..a1aa1af --- /dev/null +++ b/src/RobotM.hs @@ -0,0 +1,300 @@ +module RobotM ( + oneOf, + RobotM(..), + askPrintingData, + askLibrary, + askLibraryResult, askLibrarySolution, askLibraryExpansionTable, askLibraryRewriteTable, + RobotState(..), initialRobotState, getRobotState, putRobotState, + runRobotM, runAllRobotM, evalAllRobotM, + speculative, + renameFormula, + createStatement, createTableau, createTableau', + copyStatement, copyTableau, copyTarget +) where + +import Control.Applicative +import Control.Arrow +import Control.Monad.Logic hiding (msum) +import Control.Monad.Trans.List +import Control.Monad.Trans.State.Lazy +import Control.Monad.Trans.Reader +import Control.Monad.Identity hiding (msum) +import Data.Either +import Data.List (nub, sort) +import Data.Maybe +import qualified Data.Map as Map +import Data.Map (Map, (!), member, notMember) +import Data.Foldable (msum) + + +import Types +import Library +import Printing + +---------------------------------------------------------------------------------------------------- + +-- in a do-block in the [] monad, one can write +-- x <- [a,b,c] +-- in a more general nondeterministic monad (made with LogicT M), +-- one wants to be able to write something similar, as in +-- x <- oneOf [a,b,c] + +oneOf :: MonadPlus m => [a] -> m a +oneOf = msum . map return + +---------------------------------------------------------------------------------------------------- + +type VarNameCount = Map String Int + +type NextTableauID = Int +initialNextTableauID = 1 +type NextStatementIDs = Map StatementType Int +initialNextStatementIDs = Map.empty + +data RobotState = RobotState NextTableauID NextStatementIDs VarNameCount +initialRobotState = RobotState initialNextTableauID initialNextStatementIDs Map.empty + +type RobotM = StateT RobotState (LogicT (ReaderT (PrintingData, Library) Identity)) + +runRobotM :: PrintingData -> Library -> RobotState -> RobotM a -> Maybe (a, RobotState) +runRobotM p l s ma = listToMaybe . runIdentity . flip runReaderT (p,l) . observeManyT 1 $ runStateT ma s + +runAllRobotM :: PrintingData -> Library -> RobotState -> RobotM a -> [(a, RobotState)] +runAllRobotM p l s ma = runIdentity . flip runReaderT (p,l) . observeAllT $ runStateT ma s + +evalAllRobotM :: PrintingData -> Library -> RobotState -> RobotM a -> [a] +evalAllRobotM p l s = map fst . runAllRobotM p l s + +getRobotState :: RobotM RobotState +getRobotState = get + +putRobotState :: RobotState -> RobotM () +putRobotState = put + + +askPrintingData :: RobotM PrintingData +askPrintingData = fst `liftM` (lift $ lift ask) + +askLibrary :: RobotM Library +askLibrary = snd `liftM` (lift $ lift ask) + +askLibraryResult :: RobotM Result +askLibraryResult = do + Library rs _ _ _ <- askLibrary + r <- oneOf rs + renameResult r --variables bound by explicit quantifiers inside results need to be rebound + -- (and renaming implicitly bound variables is harmless) + +--NB: Solutions are not renamed as they should not contain bound variables. +askLibrarySolution :: RobotM Solution +askLibrarySolution = do + Library _ ss _ _ <- askLibrary + oneOf ss + +askLibraryExpansionTable :: RobotM ExpansionTable +askLibraryExpansionTable = do + Library _ _ et _ <- askLibrary + return et + +askLibraryRewriteTable :: RobotM RewriteTable +askLibraryRewriteTable = do + Library _ _ _ rt <- askLibrary + return rt + + +--speculative ma: Find out what the effect of running ma would be, but don't modify the state. +--Typically used when we want to rename but not claim variables from the stock. + +-- NB: if you have a renamed formula produced in this way, DO NOT use it with +-- any other expanded statement, as this may cause variable collision. +-- In such cases (speculative expansion of many formulae), use getRobotState/putRobotState + +speculative :: RobotM a -> RobotM a +speculative ma = do + s <- get + a <- ma + put s + return a + +--VarNameCount functions: +getVarNameCount :: RobotM VarNameCount +getVarNameCount = do + RobotState _ _ v <- get + return v + +putVarNameCount :: VarNameCount -> RobotM () +putVarNameCount v = do + RobotState t s _ <- get + put $ RobotState t s v + +--Sometimes variables can be given in the problem, rather than produced by renaming. +--When we see such variables we need to update the VarNameCount +-- to make sure we don't generate Variables with the same names when renaming. +registerVariables :: [Variable] -> RobotM () +registerVariables vs = do + vnc <- getVarNameCount + putVarNameCount $ foldr register vnc [(n, id) | Variable n id _ _ _ <- vs] + +register :: (String, ID) -> VarNameCount -> VarNameCount +register (n,id) = Map.insertWith max n (id + 1) + +---------------------------------------------------------------------------------------------------- + +-- RenameM renumbers *bound* variables in any number of formulae (e.g. from the Library), +-- avoiding numbers that are already used (and updating the underlying RobotM) +-- Note that each time we pull a fresh formula out of a library, we need a new RenameM +-- so that any "colliding" variables used in different formulae are renamed to different things. +-- Conversely if (for whatever reason) we want to rename two formulae in a consistent manner, +-- we must use one RenameM. + +boundNamesInFormula :: Formula -> [(String, ID)] +boundNamesInFormula = accumulateFormula immediate where + immediate :: Formula -> [(String, ID)] + immediate (AtomicFormula _ _) = [] + immediate (Not _) = [] + immediate (And _) = [] + immediate (Or _) = [] + immediate (Forall vs _) = [(n,id) | Variable n id _ _ _ <- vs] + immediate (UniversalImplies vs _ _) = [(n,id) | Variable n id _ _ _ <- vs] + immediate (Exists vs _) = [(n,id) | Variable n id _ _ _ <- vs] + +type VarNameMap = Map (String, ID) (String, ID) +type RenameM = StateT VarNameMap RobotM + +getVarNameMap :: RenameM VarNameMap +getVarNameMap = get + +putVarNameMap :: VarNameMap -> RenameM () +putVarNameMap = put + +modifyVarNameMap = modify + +getVarNameCount' = lift getVarNameCount +putVarNameCount' = lift . putVarNameCount + +renameNameid :: [(String, ID)] -> (String, ID) -> Type_ -> RenameM (String, ID) +renameNameid bounds n' t + | n' `elem` bounds = maybe (renameUnfamiliarNameid n' t) return + . Map.lookup n' + =<< getVarNameMap + | otherwise = return n' --don't rename free variables + +renameUnfamiliarNameid :: (String, ID) -> Type_ -> RenameM (String, ID) +renameUnfamiliarNameid n@(name, _) t = do + nc <- getVarNameCount' :: RenameM (Map String Int) + let unusedNames = filter (`notMember` nc) $ name:fallbacks t + n'@(name', id') = + head $ [(u,1) | u <- unusedNames] ++ --take an unused name if possible, + [(name, nc!name)] -- else add primes to original name + modifyVarNameMap $ Map.insert n n' + putVarNameCount' $ Map.insert name' (id'+1) nc + return n' + +fallbacks :: Type_ -> [String] +fallbacks TPositiveRealNumber = ["eta", "theta", "alpha", "beta", "gamma"] +fallbacks TPoint = ["z", "u", "v", "w", "p", "q", "r", "s", "t"] +fallbacks _ = [] + + + +renameFormula' :: Formula -> RenameM Formula +renameFormula' f = mapFormulaM shallow f where + bounds = boundNamesInFormula f + + shallow :: Formula -> RenameM Formula + shallow (AtomicFormula pred args) = AtomicFormula pred <$> mapM (mapTermM onTermShallow) args + shallow f@(Not _) = return f + shallow f@(And _) = return f + shallow f@(Or _) = return f + shallow (Forall vs f's) = liftM2 Forall (mapM onVariable vs) (return f's) + shallow (UniversalImplies vs f's f'') = liftM3 UniversalImplies (mapM onVariable vs) (return f's) (return f'') + shallow (Exists vs f's) = liftM2 Exists (mapM onVariable vs) (return f's) + + onTermShallow :: Term -> RenameM Term + onTermShallow (VariableTerm var) = VariableTerm <$> onVariable var + onTermShallow t = return t + + onVariable :: Variable -> RenameM Variable + onVariable = mapVariableM onVariableShallow + + onVariableShallow :: Variable -> RenameM Variable + onVariableShallow (Variable name id t hasBullet dependencies) = do + (name', id') <- renameNameid bounds (name, id) t + return $ Variable name' id' t hasBullet dependencies + +renameFormula :: Formula -> RobotM Formula +renameFormula f = evalStateT (renameFormula' f) Map.empty + +renameResult' :: Result -> RenameM Result +renameResult' (Result d ps c) = do + ps' <- mapM renameFormula' ps + c' <- renameFormula' c + return $ Result d ps' c' + +renameResult :: Result -> RobotM Result +renameResult f = evalStateT (renameResult' f) Map.empty + + +---------------------------------------------------------------------------------------------------- +--All of the following functions are in the RobotM monad +-- because they need to uniquely number Statements or Tableaux +--Some also affect variables (see below). + +getNewTableauID :: RobotM ID +getNewTableauID = do + RobotState t s v <- get + put $ RobotState (t+1) s v + return t + +getNewStatementID :: StatementType -> RobotM ID +getNewStatementID t = do + RobotState tab s v <- get + let n = Map.findWithDefault 1 t s + put $ RobotState tab (Map.insert t (n+1) s) v + return n + +--createStatement, createTableau do not rename any variables in the formulae they are given, +-- but they do register the names of these variables (to avoid collision during renaming) +createStatement :: StatementType -> Formula -> RobotM Statement +createStatement t f = do + let vs = accumulateVariableInFormula return f + registerVariables vs + id <- getNewStatementID t + return $ Statement (StatementName t id) f [] + +createTableau :: Bool -> [Formula] -> Formula -> RobotM Tableau +createTableau d hs t = do + id' <- getNewTableauID + hs' <- mapM (createStatement STHypothesis) hs + t' <- createStatement STTarget t + return $ Tableau (TableauName d id') [] hs' (Target [Left t']) + + +createTableau' :: Bool -> [Statement] -> Target -> RobotM Tableau +createTableau' d hs t = do + id' <- getNewTableauID + return $ Tableau (TableauName d id') [] hs t + +--copyStatement, copyTableau, copyTarget rename bound variables in their arguments. + +copyStatement :: Statement -> RobotM Statement +copyStatement (Statement (StatementName t _) f tags) = do + id <- getNewStatementID t + f' <- renameFormula f + return $ Statement (StatementName t id) f' tags + +copyTableau :: Tableau -> RobotM Tableau +copyTableau (Tableau (TableauName d _) vs hs t) = liftM4 Tableau (TableauName d `liftM ` getNewTableauID) + (return vs) + (mapM copyStatement hs) + (copyTarget t) + +copyTarget :: Target -> RobotM Target +copyTarget (Target ps) = Target <$> mapM onPart ps where + onPart = eitherM copyStatement (mapM copyTableau) + +--eitherM :: Monad m => (a -> m a) -> (b -> m b) -> Either a b -> m (Either a b) +--eitherM f g = either (liftM Left . f) (liftM Right . g) + +---------------------------------------------------------------------------------------------------- + diff --git a/src/Suspension.hs b/src/Suspension.hs new file mode 100755 index 0000000..d9a118a --- /dev/null +++ b/src/Suspension.hs @@ -0,0 +1,89 @@ +module Suspension ( + unlockExistentialUniversalConditionalTarget, + unlockExistentialTarget, + convertDiamondToBullet +) where + +import Control.Applicative +import Control.Monad + +import TexBase +import Types +import Move +import Tex +import RobotM +import Writeup + +---------------------------------------------------------------------------------------------------- + +addDiamond :: Variable -> Variable +addDiamond (Variable n id t VTNormal ds) = Variable n id t VTDiamond ds +addDiamond _ = error "Attempt to add a diamond to a variable that already has a diamond." + +addDiamondsInTableau :: [Variable] -> Tableau -> Tableau +addDiamondsInTableau vs = mapVariableInTableau shallow where + shallow v@(Variable n id t VTNormal ds) | v `elem` vs = Variable n id t VTDiamond ds + shallow v = v + + +-- If the target is existential-universal-conditional, then unlock it to create a diamonded tableau. +unlockExistentialUniversalConditionalTarget :: MoveType +unlockExistentialUniversalConditionalTarget = tableauwise onTableau where + + {- TODO: make this affect more cases with more than one target?-} + onTableau :: [Statement] -> Surroundings -> Tableau -> RobotM (MoveDescription, Tableau) + onTableau _ s tableau@(Tableau tID tVs hs (Target [Left t@(Statement n ( + Exists evs (ui@(UniversalImplies uvs as c)) + ) _)])) = do + as' <- mapM (createStatement STHypothesis) $ markDependencies <$> as + cs' <- mapM (createStatement STTarget) $ conjuncts c + newTableau@(Tableau tID' tVs' hs' t') <- createTableau' True (tagAs (MovedDownFrom tID) <$> as') $ Target (Left <$> cs') + let newTableau' = Tableau tID' (tVs' ++ evs ++ uvs) hs' t' +-- ui' <- createStatement STTarget ui + return (MoveDescription [n] [TargetIs [t] {-,Let [Suspended $ addDiamond <$> vs]-}] $ + "Unlock existential-universal-conditional target " ++ texSN n ++ ".", + markBulletedIndependencies uvs . s . addDiamondsInTableau evs $ Tableau tID tVs hs (Target [Right [newTableau']])) + onTableau _ _ _ = mzero + +-- If the target is existential, then unlock it to create a diamonded tableau. +unlockExistentialTarget :: MoveType +unlockExistentialTarget = tableauwise onTableau where + + {- TODO: make this affect more cases with more than one target?-} + onTableau :: [Statement] -> Surroundings -> Tableau -> RobotM (MoveDescription, Tableau) + onTableau _ s tableau@(Tableau tID tVs hs (Target [Left t@(Statement n ( + Exists evs inner + ) _)])) = do + inner's <- mapM (createStatement STTarget) $ conjuncts inner + newTableau@(Tableau tID' tVs' hs' t') <- createTableau' True [] $ Target (Left <$> inner's) + let newTableau' = Tableau tID' (tVs' ++ evs) hs' t' +-- ui' <- createStatement STTarget ui + return (MoveDescription [n] [TargetIs [t] {-,Let [Suspended $ addDiamond <$> vs]-}] $ + "Unlock existential target " ++ texSN n ++ ".", + s . addDiamondsInTableau evs $ Tableau tID tVs hs (Target [Right [newTableau']])) + onTableau _ _ _ = mzero + + + +convertDiamondToBullet :: MoveType +convertDiamondToBullet = tableauwise onTableau where + + onTableau :: [Statement] -> Surroundings -> Tableau -> RobotM (MoveDescription, Tableau) + onTableau inheritedHs s (Tableau tN@(TableauName True tID) tVs hs t) = do + -- find all diamonded variables owned by this tableau + let diamonded = [v | v@(Variable _ _ _ VTDiamond _) <- tVs] + + guard . not $ null diamonded + guard . not $ null hs + + let convert :: Variable -> Variable + convert v@(Variable n id t VTDiamond ds) + | v `elem` diamonded = Variable n id t VTBullet ds + convert v = v + + tableau' = mapVariableInTableau convert $ Tableau (TableauName False tID) tVs hs t + + return (MoveDescription [] [AssumeNow hs] $ + "Replacing diamonds with bullets in " ++ texTN tN ++ ".", + s $ tableau') + onTableau _ _ _ = mzero diff --git a/src/TestData.hs b/src/TestData.hs new file mode 100755 index 0000000..08bc0fc --- /dev/null +++ b/src/TestData.hs @@ -0,0 +1,224 @@ +module TestData ( + problems, library, printingData +) where + +import Prelude hiding ((/)) + +import Control.Arrow +import Control.Applicative +import qualified Data.Map as Map +import Data.Map (Map) + +import Types +import Expansion +import TexBase +import Parser +import Tex +import RobotM +import Library +import Writeup +import Printing + +intersectionOpenSets = Problem + "If $A$ and $B$ are open sets, then $A \\cap B$ is also open." --"The intersection of two open sets is open." + ["open(A)", + "open(B)"] + "open(intersect(A,B))" + +continuousPreimageOpen = Problem + "The pre-image of an open set $U$ under a continuous function $f$ is open." + ["continuous(f)", + "open(U)"] + "open(preimage(f,U))" + +compositionContinuousFunctions = Problem + "If $f$ and $g$ are continuous functions, then $g \\circ f$ is continuous." --"A composition of continuous functions is continuous." + ["continuous(f)", + "continuous(g)"] + "continuous(compose(g,f))" + +continuousFunctionsPreserveLimits = Problem + "If $f$ is a continuous function and $(a_n) \\to a$, then $(f(a_n)) \\to f(a)$"-- "A continuous function preserves limits." + ["continuous(f)", + "tendsto(an,a)"] + "tendsto(applyfnpointwise(f,an),applyfn(f,a))" + +closedSubsetCompleteIsComplete = Problem + "A closed subset $A$ of a complete metric space $X$ is complete." + ["completespace(X)", + "closedin(A,X)"] + "complete(A)" + +ffminusoneAsubsetA = Problem "$f(f^{-1}(A))\\subset A$" [] "subsetof(image(f,preimage(f,A)),A)" + +asubsetfminusonefA = Problem "$A \\subset f^{-1}(f(A))$" [] "subsetof(A, preimage(f,image(f,A)))" + + +iffInjectionThenfAcapfBsubsetfAcapB = Problem + "If $f$ is an injection then $f(A)\\cap f(B)\\subset f(A\\cap B)$" + ["injection(f)"] + "subsetof(intersect(image(f,A),image(f,B)),image(f,intersect(A,B)))" + +intersectionSubgroupsClosed = Problem + "The intersection of two subgroups is a subgroup" + ["subgroup(H)","subgroup(K)"] + "forall x y.(in(x,intersect(H,K)) & in(y,intersect(H,K)) => in(product(x,y),intersect(H,K)))" + +problems = [intersectionOpenSets, + continuousPreimageOpen, + compositionContinuousFunctions, + continuousFunctionsPreserveLimits, + closedSubsetCompleteIsComplete, + ffminusoneAsubsetA, asubsetfminusonefA, + iffInjectionThenfAcapfBsubsetfAcapB, + intersectionSubgroupsClosed] +---------------------------------------------------------------------------------------------------- + + +expansionTableSource :: [(String, String)] +expansionTableSource = [ + ("in(x,intersect(A,B))", "in(x,A) & in(x,B)"), + ("in(x,union(A,B))", "in(x,A) | in(x,B)"), + ("subsetof(A,intersect(B,C))","subsetof(A,B) & subsetof(A,C)"), + ("subsetof(A,B)", "forall x.(in(x,A) => in(x,B))"), + ("in(x,preimage(f,U))", "in(applyfn(f,x),U)"), + ("in(x,image(f,A))", "exists y.(in(y,A) & equals(applyfn(f,y),x))"), + ("in(x,complement(A))", "notin(x,A)"), + ("notin(x,A)","¬in(x,A)"), + ("injection(f)", "forall x y z.(equals(applyfn(f,x),z) & equals(applyfn(f,y),z) => equals(x,y))"), + ("sequencein(an,A)", "forall n.(in(kthterm(an,n),A))"), + ("open(A)", "forall x.(in(x, A) => exists delta.(forall y.(lessthan(d(x, y), delta) => in(y, A))))"), + ("continuous(f)", "forall x epsilon.(exists delta.(forall y.(lessthan(d(x, y), delta) => lessthan(d(applyfn(f,x), applyfn(f,y)), epsilon))))"), + ("tendsto(an,a)", "forall epsilon.(exists N.(forall n.(atleast(n,N) => lessthan(d(a,kthterm(an,n)),epsilon))))"), + ("completespace(X)", "forall an.(cauchy(an) => converges(an))"), + ("complete(A)", "forall an.(cauchy(an) & sequencein(an,A) => convergesin(an,A))"), + ("converges(an)", "exists a.(tendsto(an,a))"), + ("convergesin(an,A)", "exists a.(in(a,A) & tendsto(an,a))"), + ("closed(A)", "forall an a.(sequencein(an,A) & tendsto(an,a) => in(a,A))"), + ("denseon(A,B)", "forall x epsilon.(in(x,B) => exists y.(in(y,A) & lessthan(d(x,y), epsilon)))"), + ("cauchy(an)", "forall epsilon.(exists N.(forall m n.(atleast(m,N) & atleast(n,N) => lessthan(d(kthterm(an,m),kthterm(an,n)),epsilon))))"), + ("subgroup(H)", "closedunderinverse(H) & in(e(),H) & closedundermultiplication(H)") + ] + +expansionTable :: [(FormulaWithSlots, Formula)] +expansionTable = [(f / allVariablesInFormula f, f') | + (f, f') <- (parse formula *** parse formula) <$> expansionTableSource] + + +--NB: the term rewriting code does not use renameFormula -- so DO NOT ever put quantifiers on RHS +-- of the rewrite table. +-- (This is only relevant if we introduce sets, etc., so that formulae can be inside terms.) + +rewriteTableSource = [ + ("applyfn(compose(f,g),x)", "applyfn(f,applyfn(g,x))"), + ("kthterm(applyfnpointwise(f,an),n)", "applyfn(f,kthterm(an,n))") + ] + + +rewriteTable :: [(Term, [Variable], Term)] +rewriteTable = [(t, allVariablesInTerm t, t') | + (t, t') <- (parse term *** parse term) <$> rewriteTableSource ] + +---------------------------------------------------------------------------------------------------- + + +termPatterns' :: Map String Pattern +termPatterns' = Map.fromList [ + ("intersect", "%\\cap %"), + ("union", "%\\cup %"), + ("compose", "%\\circ %"), + ("applyfn", "%(%)"), + ("image", "%(%)"), + ("preimage", "%^{-1}(%)"), + ("complement", "%^c"), + ("product", "%%"), + ("inverse", "%^{-1}"), + ("e", "e"), + ("ball", "B_{%}(%)") + ] + +formulaPatterns' :: Map String Pattern +formulaPatterns' = Map.fromList [ + ("in", "$%\\in %$"), + ("notin", "$%\\notin %$"), + ("subsetof", "$%\\subset %$"), + ("equals", "$% = %$"), + ("lessthan", "$% < %$"), + ("atleast", "$%\\geqslant %$"), + ("atmost", "$%\\leqslant %$"), + ("open", "$%$ is open"), + ("closed", "$%$ is closed"), + ("complete", "$%$ is a complete space"), + ("completespace", "$%$ is complete"), + ("closedin", "$%$ is closed in $%$"), + ("sequencein", "$%$ is a sequence in $%$"), + ("injection", "$%$ is an injection"), + ("continuous", "$%$ is continuous"), + ("cauchy", "$%$ is Cauchy"), + ("converges", "$%$ converges"), + ("convergesin", "$%$ converges in $%$"), + ("mapsto", "$%:%\\mapsto %$"), + ("subgroup", "$%$ is a subgroup"), + ("closedunderinverse", "$%$ is closed under taking inverses"), + ("closedundermultiplication", "$%$ is closed under multiplication") + ] + +nounPatterns' :: Map String Pattern +nounPatterns' = Map.fromList [ + ("in", "element of $%$"), + ("subsetof", "subset of $%$"), + ("sequencein", "sequence in $%$"), + ("injection", "injection") + ] + +adjectivePatterns' :: Map String Pattern +adjectivePatterns' = Map.fromList [ + ("open", "open"), + ("closed", "closed"), + ("complete", "complete"), + ("continuous", "continuous"), + ("cauchy", "Cauchy") + ] + +printingData = PrintingData termPatterns' formulaPatterns' nounPatterns' adjectivePatterns' + +library = Library [ + Result "transitivity" [ + parse formula "lessthan(alpha,beta)", + parse formula "atmost(beta,gamma)"] + (parse formula "lessthan(alpha,gamma)"), + Result "" [ + parse formula "subset(A,ball(x,beta))", + parse formula "atmost(beta,gamma)"] + (parse formula "subset(A,ball(x,gamma))"), + Result "transitivity" [ + parse formula "atmost(alpha,beta)"] + (parse formula "subsetof(ball(x,alpha),ball(x,beta))"), + Result "" [ + parse formula "subsetof(A,B)", + parse formula "subsetof(B,C)"] + (parse formula "subsetof(A,C)"), + Result "" [ + parse formula "closedunderinverse(H)", + parse formula "in(x,H)"] + (parse formula "in(inverse(x),H)"), + Result "" [ + parse formula "closedundermultiplication(H)", + parse formula "in(x,H)", + parse formula "in(y,H)"] + (parse formula "in(product(x,y),H)"), + Result "a closed set contains its limit points" [ + parse formula "closedin(F,X)", + parse formula "sequencein(an,F)", + parse formula "tendsto(an,a)"] + (parse formula "in(a,F)"), + Result "" [parse formula "issameas(A,complement(B))"] (parse formula "equals(twoBack(f,A),complement(preimage(f,B)))") + ][ + Solution [parse variable "eta"] [ + parse formula "atmost(eta, alpha)", + parse formula "atmost(eta, beta)"] + [parse term "min(alpha, beta)"] + ] + expansionTable + rewriteTable + diff --git a/src/TestData2.hs b/src/TestData2.hs new file mode 100755 index 0000000..87b4cc2 --- /dev/null +++ b/src/TestData2.hs @@ -0,0 +1,267 @@ +module TestData2 ( + problems, library, printingData +) where + +import Prelude hiding ((/)) + +import Control.Arrow +import Control.Applicative +import qualified Data.Map as Map +import Data.Map (Map) + +import Types +import Expansion +import TexBase +import Parser +import Tex +import RobotM +import Library +import Writeup +import Printing + +union3OpenSets = Problem + "If $A$, $B$,and $C$ are open sets, then $A \\cup (B \\cup C)$ is also open." --"The union of three open sets is open." + ["open(A)", + "open(B)", + "open(C)"] + "open(union(A,union(B,C)))" + +intersection3OpenSets = Problem + "If $A$, $B$,and $C$ are open sets, then $A \\cap (B \\cap C)$ is also open." --"The intersection of three open sets is open." + ["open(A)", + "open(B)", + "open(C)"] + "open(intersect(A,intersect(B,C)))" + +unionOpenSets = Problem + "If $A$ and $B$ are open sets, then $A \\cup B$ is also open." --"The union of two open sets is open." + ["open(A)", + "open(B)"] + "open(union(A,B))" + +intersectionOpenSets = Problem + "If $A$ and $B$ are open sets, then $A \\cap B$ is also open." --"The intersection of two open sets is open." + ["open(A)", + "open(B)"] + "open(intersect(A,B))" + +unionClosedSets = Problem + "If $A$ and $B$ are closed sets, then $A \\cup B$ is also closed." --"The union of two closed sets is closed." + ["closed(A)", + "closed(B)"] + "closed(union(A,B))" + +intersectionClosedSets = Problem + "If $A$ and $B$ are closed sets, then $A \\cap B$ is also closed." --"The intersection of two closed sets is closed." + ["closed(A)", + "closed(B)"] + "closed(intersect(A,B))" + +continuousPreimageClosed = Problem + "The pre-image of a closed set $U$ under a continuous function $f$ is closed." + ["continuous(f)", + "closed(U)"] + "closed(preimage(f,U))" + +continuousPreimageOpen = Problem + "The pre-image of an open set $U$ under a continuous function $f$ is open." + ["continuous(f)", + "open(U)"] + "open(preimage(f,U))" + +compositionContinuousFunctions = Problem + "If $f$ and $g$ are continuous functions, then $g \\circ f$ is continuous." --"A composition of continuous functions is continuous." + ["continuous(f)", + "continuous(g)"] + "continuous(compose(g,f))" + +continuousFunctionsPreserveLimits = Problem + "If $f$ is a continuous function and $(a_n) \\to a$, then $(f(a_n)) \\to f(a)$"-- "A continuous function preserves limits." + ["continuous(f)", + "tendsto(an,a)"] + "tendsto(applyfnpointwise(f,an),applyfn(f,a))" + +closedSubsetCompleteIsComplete = Problem + "A closed subset $A$ of a complete metric space $X$ is complete." + ["completespace(X)", + "closedin(A,X)"] + "complete(A)" + +ffminusoneAsubsetA = Problem "$f(f^{-1}(A))\\subset A$" [] "subsetof(image(f,preimage(f,A)),A)" + +asubsetfminusonefA = Problem "$A \\subset f^{-1}(f(A))$" [] "subsetof(A, preimage(f,image(f,A)))" + + +iffInjectionThenfAcapfBsubsetfAcapB = Problem + "If $f$ is an injection then $f(A)\\cap f(B)\\subset f(A\\cap B)$" + ["injection(f)"] + "subsetof(intersect(image(f,A),image(f,B)),image(f,intersect(A,B)))" + +problems = [union3OpenSets, + intersection3OpenSets, + unionOpenSets, + unionClosedSets, + intersectionClosedSets, + continuousPreimageClosed] + +problems' = [intersectionOpenSets, + continuousPreimageOpen, + compositionContinuousFunctions, + continuousFunctionsPreserveLimits, + closedSubsetCompleteIsComplete, + ffminusoneAsubsetA, asubsetfminusonefA, + iffInjectionThenfAcapfBsubsetfAcapB + ] +---------------------------------------------------------------------------------------------------- + + +expansionTableSource :: [(String, String)] +expansionTableSource = [ + ("sequencein(an,intersect(A,B))", "sequencein(an,A) & sequencein(an,B)"), + ("in(x,intersect(A,B))", "in(x,A) & in(x,B)"), + ("in(x,union(A,B))", "in(x,A) | in(x,B)"), + ("subsetof(A,intersect(B,C))","subsetof(A,B) & subsetof(A,C)"), + ("subsetof(A,B)", "forall x.(in(x,A) => in(x,B))"), + ("in(x,preimage(f,U))", "in(applyfn(f,x),U)"), + ("sequencein(x,preimage(f,U))", "sequencein(applyfnpointwise(f,x),U)"), --NEW + ("in(x,image(f,A))", "exists y.(in(y,A) & equals(applyfn(f,y),x))"), + ("in(x,complement(A))", "notin(x,A)"), + ("notin(x,A)","¬in(x,A)"), + ("injection(f)", "forall x y z.(equals(applyfn(f,x),z) & equals(applyfn(f,y),z) => equals(x,y))"), + ("sequencein(an,A)", "forall n.(in(kthterm(an,n),A))"), + ("open(A)", "forall x.(in(x, A) => exists delta.(forall y.(lessthan(d(x, y), delta) => in(y, A))))"), + ("continuous(f)", "forall x epsilon.(exists delta.(forall y.(lessthan(d(x, y), delta) => lessthan(d(applyfn(f,x), applyfn(f,y)), epsilon))))"), + ("tendsto(an,a)", "forall epsilon.(exists N.(forall n.(atleast(n,N) => lessthan(d(a,kthterm(an,n)),epsilon))))"), + ("completespace(X)", "forall an.(cauchy(an) => converges(an))"), + ("complete(A)", "forall an.(cauchy(an) & sequencein(an,A) => convergesin(an,A))"), + ("converges(an)", "exists a.(tendsto(an,a))"), + ("convergesin(an,A)", "exists a.(in(a,A) & tendsto(an,a))"), + ("closed(A)", "forall an a.(sequencein(an,A) & tendsto(an,a) => in(a,A))"), + ("denseon(A,B)", "forall x epsilon.(in(x,B) => exists y.(in(y,A) & lessthan(d(x,y), epsilon)))"), + ("cauchy(an)", "forall epsilon.(exists N.(forall m n.(atleast(m,N) & atleast(n,N) => lessthan(d(kthterm(an,m),kthterm(an,n)),epsilon))))"), + ("subgroup(H)", "(forall x y.(in(x,H) & in(y,H) => in(product(x,y),H))) & in(e(),H) & (forall x.(in(x,H) => in(inverse(x),H)))") + ] + +expansionTable :: [(FormulaWithSlots, Formula)] +expansionTable = [(f / allVariablesInFormula f, f') | + (f, f') <- (parse formula *** parse formula) <$> expansionTableSource] + + +--NB: the term rewriting code does not use renameFormula -- so DO NOT ever put quantifiers on RHS +-- of the rewrite table. +-- (This is only relevant if we introduce sets, etc., so that formulae can be inside terms.) + +rewriteTableSource = [ + ("applyfn(compose(f,g),x)", "applyfn(f,applyfn(g,x))"), + ("kthterm(applyfnpointwise(f,an),n)", "applyfn(f,kthterm(an,n))") + ] + + +rewriteTable :: [(Term, [Variable], Term)] +rewriteTable = [(t, allVariablesInTerm t, t') | + (t, t') <- (parse term *** parse term) <$> rewriteTableSource ] + +---------------------------------------------------------------------------------------------------- + + +termPatterns' :: Map String Pattern +termPatterns' = Map.fromList [ + ("intersect", "%\\cap %"), + ("union", "%\\cup %"), + ("compose", "%\\circ %"), + ("applyfn", "%(%)"), + ("image", "%(%)"), + ("preimage", "%^{-1}(%)"), + ("complement", "%^c"), + ("product", "%%"), + ("inverse", "%^{-1}"), + ("e", "e"), + ("ball", "B_{%}(%)") + ] + +formulaPatterns' :: Map String Pattern +formulaPatterns' = Map.fromList [ + ("in", "$%\\in %$"), + ("notin", "$%\\notin %$"), + ("subsetof", "$%\\subset %$"), + ("equals", "$% = %$"), + ("lessthan", "$% < %$"), + ("atleast", "$%\\geqslant %$"), + ("atmost", "$%\\leqslant %$"), + ("open", "$%$ is open"), + ("closed", "$%$ is closed"), + ("complete", "$%$ is a complete space"), + ("completespace", "$%$ is complete"), + ("closedin", "$%$ is closed in $%$"), + ("sequencein", "$%$ is a sequence in $%$"), + ("injection", "$%$ is an injection"), + ("continuous", "$%$ is continuous"), + ("cauchy", "$%$ is Cauchy"), + ("converges", "$%$ converges"), + ("convergesin", "$%$ converges in $%$"), + ("mapsto", "$%:%\\mapsto %$"), + ("subgroup", "$%$ is a subgroup") + ] + +nounPatterns' :: Map String Pattern +nounPatterns' = Map.fromList [ + ("in", "element of $%$"), + ("subsetof", "subset of $%$"), + ("sequencein", "sequence in $%$"), + ("injection", "injection") + ] + +adjectivePatterns' :: Map String Pattern +adjectivePatterns' = Map.fromList [ + ("open", "open"), + ("closed", "closed"), + ("complete", "complete"), + ("continuous", "continuous"), + ("cauchy", "Cauchy") + ] + +printingData = PrintingData termPatterns' formulaPatterns' nounPatterns' adjectivePatterns' + +library = Library [ + Result "transitivity" [ + parse formula "lessthan(alpha,beta)", + parse formula "atmost(beta,gamma)"] + (parse formula "lessthan(alpha,gamma)"), + Result "" [ + parse formula "open(A)", + parse formula "open(B)"] + (parse formula "open(union(A,B))"), + Result "" [ + parse formula "open(A)", + parse formula "open(B)"] + (parse formula "open(intersect(A,B))"), +-- Result "continuous functions preserve limits" [ +-- parse formula "continuous(f)", +-- parse formula "tendsto(an,a)"] +-- (parse formula "tendsto(applyfnpointwise(f,an),applyfn(f,a))"), + Result "" [ + parse formula "subset(A,ball(x,beta))", + parse formula "atmost(beta,gamma)"] + (parse formula "subset(A,ball(x,gamma))"), + Result "transitivity" [ + parse formula "atmost(alpha,beta)"] + (parse formula "subsetof(ball(x,alpha),ball(x,beta))"), + Result "" [ + parse formula "subsetof(A,B)", + parse formula "subsetof(B,C)"] + (parse formula "subsetof(A,C)"), + Result "a closed set contains its limit points" [ + parse formula "closedin(F,X)", + parse formula "sequencein(an,F)", + parse formula "tendsto(an,a)"] + (parse formula "in(a,F)"), + Result "" [parse formula "issameas(A,complement(B))"] (parse formula "equals(twoBack(f,A),complement(preimage(f,B)))") + ][ + Solution [parse variable "eta"] [ + parse formula "atmost(eta, alpha)", + parse formula "atmost(eta, beta)"] + [parse term "min(alpha, beta)"] + ] + expansionTable + rewriteTable + diff --git a/src/Tex.hs b/src/Tex.hs new file mode 100755 index 0000000..57038f2 --- /dev/null +++ b/src/Tex.hs @@ -0,0 +1,208 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE ScopedTypeVariables #-} + +module Tex ( + Tex, tex, + texTuple, + texList, texOrList, + texSN, texSNs, texTN, + texTableauBolding +) where + + +import Prelude hiding (repeat) +import Control.Applicative +import Data.Functor.Identity +import Control.Monad +import Control.Monad.Writer.Lazy (Writer, tell, runWriter) +import Data.Monoid +import Data.List +import Data.Set (member) +import Data.Map (Map, (!)) +import qualified Data.Map as Map + +import Printing +import TexBase +import Types + +---------------------------------------------------------------------------------------------------- + +class Tex a where + tex :: PrintingData -> a -> String + +---------------------------------------------------------------------------------------------------- + + +instance Tex Function where + tex pd (Function "min") = "\\min" + tex pd (Function s) = textit s +instance Tex Predicate where + tex pd (Predicate s) = textit s + +texID :: ID -> String +texID n = replicate (n-1) '\'' + +texVariableNameID :: String -> ID -> String +texVariableNameID "an" id = "(a_n" ++ texID id ++ ")" +texVariableNameID s id + | s `member` texableGreekLetters = "\\" ++ s ++ texID id + | otherwise = s ++ texID id + +texSequenceShort :: PrintingData -> Term -> String +texSequenceShort pd (VariableTerm (Variable "an" id _ _ _)) = "a_n" ++ texID id +texSequenceShort pd t = tex pd t + +texSequenceElement :: Variable -> String -> String +texSequenceElement (Variable "an" id _ _ _) s = "a_{" ++ s ++ "}" ++ texID id + +instance Tex Dependencies where + tex pd (Dependencies [] []) = "" + tex pd (Dependencies ds is) = "[" ++ intercalate "," (map (tex pd) ds ++ (overline . tex pd <$> is)) ++ "]" + +instance Tex VariableType where + tex pd VTNormal = "" + tex pd VTDiamond = {--"^\\bullet " TEMP-} "^\\blacklozenge " + tex pd VTBullet = "^\\bullet " + +instance Tex Variable where + tex pd (Variable s id _ vtype d) = + texVariableNameID s id ++ tex pd vtype ++ tex pd d + +texList :: [String] -> String +texList [] = error "texList called with empty list" +texList [s] = s +texList ss = intercalate ", " (init ss) ++ " and " ++ last ss + +texOrList :: [String] -> String +texOrList [] = error "texOrList called with empty list" +texOrList [s] = s +texOrList ss = intercalate ", " (init ss) ++ " or " ++ last ss + +--texVariableList :: [Variable] -> String +--texVariableList [] = error "texVariableList called with empty variable list" +--texVariableList [v] = "$" ++ tex v ++ "$" +--texVariableList vs = intercalate "," (math . tex <$> init vs) ++ " and " ++ math (tex $ last vs) +-- where math s = "$" ++ s ++ "$" + +instance Tex Term where + tex pd (ApplyFn (Function "applyfnpointwise") [f,an]) = tex pd f ++ "(" ++ texSequenceShort pd an ++ ")" + tex pd (ApplyFn (Function "kthterm") [VariableTerm an,k]) = texSequenceElement an (tex pd k) + + tex pd (VariableTerm v) = tex pd v + tex pd (ApplyFn fn@(Function name) args) = case Map.lookup name (termPatterns pd) of + Just p -> instantiatePattern p $ tex pd <$> args + Nothing -> tex pd fn ++ "(" ++ intercalate "," (tex pd <$> args) ++ ")" + +instance Tex Formula where + tex pd (AtomicFormula (Predicate "tendsto") [an,b]) = texSequenceShort pd an ++ "\\to " ++ tex pd b + + tex pd (AtomicFormula pred@(Predicate name) args) = case Map.lookup name (formulaPatterns pd) of + Just p -> textrm . instantiatePattern p $ tex pd <$> args + Nothing -> tex pd pred ++ "(" ++ intercalate "," (tex pd <$> args) ++ ")" + + tex pd (Not f) = "\\neg " ++ tex pd f + tex pd (And fs) = intercalate "\\wedge " $ tex pd <$> fs + tex pd (Or fs) = intercalate "\\vee " $ tex pd <$> fs + tex pd (Forall vs f) = "\\forall " ++ intercalate ", " (tex pd <$> vs) ++ ".(" ++ tex pd f ++ ")" +-- tex pd (UniversalImplies _ [f@(AtomicFormula _ _)] f'@(AtomicFormula _ _)) = +-- tex f' ++ textrm " whenever " ++ tex f +-- tex pd (UniversalImplies _ [f] f') = textrm "if " ++ tex f ++ textrm ", then " ++ tex f' + tex pd (UniversalImplies vs fs f') = "\\forall " ++ intercalate ", " (tex pd <$> vs) ++ + ".(" ++ tex pd (And fs) ++ "\\Rightarrow " ++ tex pd f' ++ ")" +-- tex pd (Exists [v] f) = textrm "there is a " ++ tex v ++ textrm " s.t. " ++ tex f + tex pd (Exists vs f) = "\\exists " ++ intercalate ", " (tex pd <$> vs) ++ ".(" ++ tex pd f ++ ")" + + +texST :: StatementType -> String +texST STHypothesis = "H" +texST STTarget = "T" + +texSN :: StatementName -> String +texSN (StatementName t id) = texST t ++ show id + +texSNs :: [StatementName] -> String +texSNs [n] = texSN n +texSNs ns = "(" ++ intercalate "," (texSN <$> ns) ++ ")" + +texTuple :: Tex a => PrintingData -> [a] -> String +texTuple pd [a] = tex pd a +texTuple pd as = "(" ++ intercalate "," (tex pd <$> as) ++ ")" + +instance Tex Tag where + tex pd Vulnerable = "Vuln." + tex pd Deleted = error "A 'Deleted' tag should never be printed." + tex pd (MovedDownFrom n) = "From " ++ tex pd n ++ "." + tex pd (UsedForwardsWith ns) = "Used with " ++ texSNs ns ++ "." + tex pd (UsedBackwardsWith ns) = "Used with " ++ texSNs ns ++ "." + tex pd (CannotSubstitute ts) = "Cannot subst. " ++ intercalate "," (texTuple pd <$> ts) + +instance Tex Statement where + tex pd s@(Statement n f ts) + | Deleted `elem` ts = grey (texStatementCore pd s) {--TEMP-} ++ "&" ++ texTagsGrey pd ts + | otherwise = texStatementCore pd s {--TEMP-} ++ "&" ++ texTags pd ts + + +texStatementBold :: PrintingData -> Statement -> String +texStatementBold pd s@(Statement n f ts) + | Deleted `elem` ts = grey (textbf . boldmath $ texStatementCore pd s) {--TEMP-} ++ "&" ++ (textbf . boldmath $ texTagsGrey pd ts) + | otherwise = (textbf . boldmath $ texStatementCore pd s) {--TEMP-} ++ "&" ++ (textbf . boldmath $ texTags pd ts) + +texStatementCore :: PrintingData -> Statement -> String +texStatementCore pd (Statement n f ts) = texSN n ++ ".\\ " ++ math (tex pd f) + +texTags :: PrintingData -> [Tag] -> String +texTags pd [] = "" +texTags pd ts = "[" ++ intercalate "; " (tex pd <$> filter (/= Deleted) ts) ++ "]" + +texTagsGrey :: PrintingData -> [Tag] -> String +texTagsGrey pd [] = "" +texTagsGrey pd ts = grey ("[" ++ intercalate "; " (tex pd <$> filter (/= Deleted) ts) ++ "]") + +instance Tex TableauName where + tex pd (TableauName hasDagger id) = "L" ++ show id ++ (guard hasDagger >> "$^\\blacklozenge$") + +texTN :: TableauName -> String +texTN (TableauName hasDagger id) = "L" ++ show id ++ (guard hasDagger >> "$^\\blacklozenge$") + +instance Tex Tableau where + tex pd = texTableauBolding pd [] + +texTableauBolding :: PrintingData -> [StatementName] -> Tableau -> String +texTableauBolding pd ns (Tableau (TableauName hasDagger id) vs ss t) = unlines + ["\\begin{tikzpicture}[baseline=(main.base)]%", + "\\node[tableau] (main) {%", +{--TEMP-} intercalate "\\hspace{1.5mm}" (math . tex pd <$> vs) ++ "\\\\\n", + "\\begin{tabular}{ll}%", + intercalate "\\\\\n" + [if n `elem` ns then texStatementBold pd s else tex pd s | s@(Statement n _ _) <- ss], + "\\Bstrut\\\\\\hline\\Tstrut", + texTargetBolding pd ns t, + "\\end{tabular}%", + "};%", + "\\node[tableaulabel] at (main.north west) [xshift=4mm, yshift=-5.5mm] {L" ++ show id ++ (guard hasDagger >> "$^\\blacklozenge$") ++ "};", +-- "\\node[tableaulabel] at (main.north west) [xshift=4mm, yshift=-5.5mm] {L" ++ show id ++ {-TEMP (guard hasDagger >> "$^\\blacklozenge$") ++ -}"};", + "\\end{tikzpicture}%"] +texTableauBolding _ _ (Done (TableauName hasDagger id)) = unlines + ["\\begin{tikzpicture}%", + "\\node[tableau] (main) {%", + "\\ \\ \\,Done", + "};%", + "\\node[tableaulabel] at (main.north west) [xshift=4mm, yshift=-5.5mm] {L" ++ show id ++ (guard hasDagger >> "$^\\blacklozenge$") ++ "};", +-- "\\node[tableaulabel] at (main.north west) [xshift=4mm, yshift=-5.5mm] {L" ++ show id ++ {-TEMP (guard hasDagger >> "$^\\blacklozenge$") ++ -}"};", + "\\end{tikzpicture}%"] + +-- "\\node[tableaulabel] at (main.north west) [xshift=4mm, yshift=-5.5mm] {L" ++ show id ++ "};", + +instance Tex Target where --output goes inside an array env. +-- tex (Target ps) = intercalate "\\\\\n" [either tex tex p | p <- ps] +-- tex Contradiction = "Contradiction" + tex pd = texTargetBolding pd [] + +texTargetBolding :: PrintingData -> [StatementName] -> Target -> String +texTargetBolding pd ns (Target ps) = intercalate "\\\\\n" $ either f (intercalate "\\hspace{2mm}$\\vee$" . map (texTableauBolding pd ns)) <$> ps where + f s@(Statement n _ _) | n `elem` ns = texStatementBold pd s + | otherwise = tex pd s +texTargetBolding _ ns Contradiction = "Contradiction" + +instance Tex VariableChoice where + tex pd (VariableChoice v t) = math $ tex pd v ++ " = " ++ tex pd t diff --git a/src/TexBase.hs b/src/TexBase.hs new file mode 100755 index 0000000..d31ebc8 --- /dev/null +++ b/src/TexBase.hs @@ -0,0 +1,158 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE ScopedTypeVariables #-} + +module TexBase ( +-- Tex, tex, + texHeader, texFooter, + math, + escape, + operator, + scriptsize, footnotesize, small, + textbf, textrm, textsc, textit, + smalltextrm, smalltextit, + boldmath, + overline, + ensuremath, texableGreekLetters, + grey, + texSubscript, texIntSubscript, + texVerbatim, + fit, +) where + +import qualified Data.Set as Set + +--import GHC.Unicode (isAlphaNum, isDigit) + +--import Common + +---------------------------------------------------------------------------------------------------- +-- +--class Tex a where +-- tex :: a -> String + +--instance Tex Int where +-- tex = show + +---------------------------------------------------------------------------------------------------- + +math :: String -> String +math s = "$" ++ s ++ "$" + +escape :: String -> String +escape = concatMap escape' + +escape' :: Char -> String +escape' '\\' = "\\ensuremath{\\backslash}" +escape' '%' = "\\%" +escape' '^' = "\\^{}" +escape' '_' = "\\_" +escape' '<' = "\\ensuremath{<}" +escape' '>' = "\\ensuremath{>}" +escape' '\'' = "\\textquotesingle{}" +escape' c = [c] + +operator :: String -> String +operator s = "\\operatorname{" ++ s ++ "}" + +scriptsize, footnotesize, small :: String -> String +scriptsize s = "{\\scriptsize " ++ s ++ "}" +footnotesize s = "{\\footnotesize " ++ s ++ "}" +small s = "{\\small " ++ s ++ "}" + +textbf, textrm, textsc, textit :: String -> String +textbf s = "\\textbf{" ++ s ++ "}" +textrm s = "\\textrm{" ++ s ++ "}" +textsc s = "\\textsc{" ++ s ++ "}" +textit s = "\\textit{" ++ s ++ "}" + +smalltextrm, smalltextit :: String -> String +smalltextrm = textrm . small +smalltextit = textit . small + +boldmath s = "\\boldmath " ++ s ++ "\\unboldmath " + +overline s = "\\overline{" ++ s ++ "}" + +ensuremath :: String -> String +ensuremath s = "\\ensuremath{" ++ s ++ "}" + +texableGreekLetters = Set.fromList + ["alpha", "beta", "gamma", "delta", "epsilon", "zeta", "eta", "theta", "iota", "kappa", + "lambda", "mu", "nu", "xi", "pi", "rho", "sigma", "tau", "upsilon", "phi", "chi", "psi", + "Gamma", "Delta", "Theta", "Lambda", "Xi", "Pi", "Sigma", "Upsilon", "Phi", "Psi"] + +grey :: String -> String +grey s = "\\grey{" ++ s ++ "}" + +---------------------------------------------------------------------------------------------------- + +texSubscript :: String -> String +texSubscript s = "_{" ++ s ++ "}" + +texIntSubscript :: Int -> String +texIntSubscript = texSubscript . show + +---------------------------------------------------------------------------------------------------- + +texVerbatim :: String -> String +texVerbatim = textbf . escape + +fit :: String -> String +fit s = "\\begin{fit}" ++ s ++ "\\end{fit}" + +texHeader = + "\\documentclass[a4paper,twoside,12pt]{article}\n\ + \\\usepackage[hmargin={12mm,55mm},vmargin=10mm,footskip=7mm,asymmetric]{geometry}\n\ + \\\usepackage{amsmath}\n\ + \\\usepackage{amssymb}\n\ + \\\usepackage{tikz}\n\ + \\\usepackage{xcolor}\n\ + \\\usepackage{comment}\n\ + \\\usepackage{adjustbox}\n\ + \\\usepackage{iftex}\n\ + \\\ifPDFTeX\n\ + \\\usepackage[T1]{fontenc}\n\ + \\\usepackage[utf8]{inputenc}\n\ + \\\else\n\ + \\\usepackage[no-math]{fontspec}\n\ + \\\fi\n\ + \\\usepackage{libertine}\n\ + \\n\ + \\\makeatletter\n\ + \\\let\\_\\relax\n\ + \\\DeclareRobustCommand{\\_}{%\n\ + \ \\leavevmode\\vbox{%\n\ + \ \\hrule\\@width.4em\n\ + \ \\@height-.16ex\n\ + \ \\@depth\\dimexpr.16ex+.28pt\\relax}}\n\ + \\\makeatother\n\ + \\n\ + \\\newcommand\\Tstrut{\\rule{0pt}{2.4ex}}\n\ + \\\newcommand\\Bstrut{\\rule[-1.1ex]{0pt}{0pt}}\n\ + \\n\ + \\\tikzset{\n\ + \ tableaulabel/.style={draw=black!30, fill=gray!4, inner sep = 0.5mm, outer sep = 3mm, circle},\n\ + \ tableau/.style={draw=black!30, fill=gray!4, inner sep = 3mm, outer sep = 3mm, rounded corners=3mm, align=center},\n\ + \}\n\ + \\n\ + \\\definecolor{greycolour}{rgb}{0.6, 0.6, 0.6}\n\ + \\\newcommand\\grey[1]{{\\color{greycolour}{#1}}}\n\ + \\n\ + \\\setlength\\marginparwidth{45mm}\n\ + \\n\ + \\\newenvironment{fit}{\\begin{adjustbox}{max width=\\textwidth,max totalheight=\\textheight,keepaspectratio}}{\\end{adjustbox}}\n\ + \\n\ + \\n\ + \\\ifdefined\\showsteps\n\ + \ \\includecomment{steps}\n\ + \\\else\n\ + \ \\excludecomment{steps}\n\ + \\\fi\n\ + \\n\ + \\\raggedbottom\n\ + \\n\ + \\\begin{document}\ + \\n" + +texFooter = "\n\\end{document}" + diff --git a/src/TidyingMoves.hs b/src/TidyingMoves.hs new file mode 100755 index 0000000..d5b1855 --- /dev/null +++ b/src/TidyingMoves.hs @@ -0,0 +1,457 @@ +{-# LANGUAGE TupleSections #-} + +module TidyingMoves ( + peelAndSplitUniversalConditionalTarget, + peelBareUniversalTarget, + flipNegativeTarget, + flipNegativeHypothesis, + splitConjunctiveTarget, + splitDisjunctiveHypothesis, + splitDisjunctiveTarget, + removeTarget, + collapseSubtableauTarget, + automaticRewrite, + rewriteVariableTermEquality, + rewriteVariableVariableEquality +) where + +import Control.Applicative +import Control.Monad +import Data.Maybe +import Data.List +import Data.Map ((!)) +import Debug.Trace + +import Prelude hiding ((/)) +import Types +import Match +import Move +import TexBase +import Tex +import RobotM +import Expansion +import Writeup + +---------------------------------------------------------------------------------------------------- + +-- If you peel a target that contains a bulleted variable, +-- note that the variable is independent of the Variables that were peeled + +peelAndSplitUniversalConditionalTarget :: MoveType +peelAndSplitUniversalConditionalTarget = tableauwise onTableau where + + {- TODO: make this affect more cases with more than one target?-} + onTableau :: [Statement] -> Surroundings -> Tableau -> RobotM (MoveDescription, Tableau) + onTableau _ s tableau@(Tableau tID tVs hs (Target [Left (Statement n (UniversalImplies vs as c) _)])) = do + as' <- mapM (createStatement STHypothesis) $ markDependencies <$> as + cs' <- mapM (createStatement STTarget) $ conjuncts c + return (MoveDescription [n] [Let [vs `BeSuchThat` as']] $ "Apply `let' trick and move premise of universal-conditional target " ++ texSN n ++ " above the line.", + markBulletedIndependencies vs . s $ Tableau tID (tVs ++ vs) (hs ++ as') (Target $ Left <$> cs')) + onTableau _ _ _ = mzero + +peelBareUniversalTarget :: MoveType +peelBareUniversalTarget = tableauwise onTableau where + + onTableau :: [Statement] -> Surroundings -> Tableau -> RobotM (MoveDescription, Tableau) + onTableau _ s tableau@(Tableau tID tVs hs (Target [Left (Statement n (Forall vs c) _)])) = do + c' <- createStatement STTarget c + return (MoveDescription [n] [Take vs] $ "pply `let' trick and move premise of universal target " ++ texSN n ++ " above the line.", + markBulletedIndependencies vs . s $ Tableau tID (tVs ++ vs) hs (Target [Left c'])) + onTableau _ _ _ = mzero + +---------------------------------------------------------------------------------------------------- + +flipNegativeTarget :: MoveType +flipNegativeTarget = tableauwise onTableau where + + onTableau :: [Statement] -> Surroundings -> Tableau -> RobotM (MoveDescription, Tableau) + onTableau _ s tableau@(Tableau tID tVs hs (Target [Left (Statement n (Not f) _)])) = do + h' <- createStatement STHypothesis f + return (MoveDescription [n] [StubClause "Move negative target"] $ + "Move negative target " ++ texSN n ++ " above the line and make it positive.", + s $ Tableau tID tVs (hs ++ [h']) Contradiction) + onTableau _ _ _ = mzero + + + +flipNegativeHypothesis :: MoveType +flipNegativeHypothesis = tableauwise onTableau where + + onTableau :: [Statement] -> Surroundings -> Tableau -> RobotM (MoveDescription, Tableau) + onTableau _ s tableau@(Tableau tID tVs hs Contradiction) = do + (Statement n (Not f) _, context) <- oneOf $ eachUndeletedHypothesisWithContext hs + + t <- createStatement STTarget f + + return (MoveDescription [n] [StubClause "Move negative hypothesis"] $ + "Move negative hypothesis " ++ texSN n ++ " below the line and make it positive.", + s $ Tableau tID tVs (context []) (Target [Left t])) + + onTableau _ _ _ = mzero + +---------------------------------------------------------------------------------------------------- + +splitConjunctiveTarget :: MoveType +splitConjunctiveTarget = tableauwise onTableau where + + onTableau :: [Statement] -> Surroundings -> Tableau -> RobotM (MoveDescription, Tableau) + onTableau _ s tableau@(Tableau tID tVs hs t@(Target ps)) = do + --pick a conjunctive target + (Left (Statement n (And fs) _), context) <- oneOf $ eachUndeletedTargetPartWithContext ps + + --turn the conjuncts into new statements + newTs <- mapM (createStatement STTarget) fs + + return (MoveDescription [n] [] $ "Split up conjunctive target " ++ texSN n ++ ".", + s . Tableau tID tVs hs . Target . context $ Left <$> newTs) + + onTableau _ _ _ = mzero + + + +splitDisjunctiveHypothesis :: MoveType +splitDisjunctiveHypothesis = tableauwise onTableau where + + onTableau :: [Statement] -> Surroundings -> Tableau -> RobotM (MoveDescription, Tableau) + onTableau _ s tableau@(Tableau tID tVs hs t) = do + --pick a disjunctive hypothesis + (h@(Statement n (Or fs) _), context) <- oneOf $ eachUndeletedHypothesisWithContext hs + + --turn the disjuncts into new tableaux + disjunctHs <- mapM (createStatement STHypothesis) fs + copiedTs <- mapM copyTarget [t | _ <- disjunctHs] + newTableaux <- zipWithM (createTableau' False) (return <$> disjunctHs) copiedTs + + return (MoveDescription [n] [StubClause "Split disjunctive hypothesis"] $ "Split into cases to handle disjunctive hypothesis " ++ texSN n ++ ".", + s . Tableau tID tVs (context []) . Target $ Right . return <$> newTableaux) + + onTableau _ _ _ = mzero + + +splitDisjunctiveTarget :: MoveType +splitDisjunctiveTarget = tableauwise onTableau where + + onTableau :: [Statement] -> Surroundings -> Tableau -> RobotM (MoveDescription, Tableau) + onTableau _ s tableau@(Tableau tID tVs hs (Target ps)) = do + --pick a target part which is a single disjunctive statement + (Left (Statement n (Or fs) _), context) <- oneOf $ eachUndeletedTargetPartWithContext ps + + --Create a new tableau for each disjunct: + + disjuncts <- mapM (createStatement STTarget) fs + + newTableaux <- mapM (createTableau' False []) (Target . return . Left <$> disjuncts) :: RobotM [Tableau] + newTableaux' <- mapM copyTableau newTableaux --rename all targets (inc. the disjuncts) + + + return (MoveDescription [n] [StubClause "Split disjunctive target"] $ "Split up disjunctive target " ++ texSN n ++ ".", + s . Tableau tID tVs hs . Target . context . return . Right $ newTableaux') + + onTableau _ _ _ = mzero + +--splitDisjunctiveTarget :: MoveType +--splitDisjunctiveTarget = tableauwise onTableau where +-- +-- onTableau :: [Statement] -> Surroundings -> Tableau -> RobotM (MoveDescription, Tableau) +-- onTableau _ s tableau@(Tableau tID tVs hs (Target ps)) = do +-- --pick a target part which is a single disjunctive statement +-- (Left (Statement n (Or fs) _), context) <- oneOf $ eachUndeletedTargetPartWithContext ps +-- +-- --Create a new tableau for each disjunct: +-- +-- let disjuncts = [Statement n {-<--sic-} f [] | f <- fs] +-- -- note that we reuse the name n of the original statement here, because we will copy the _entirety_ +-- -- of the new tableaux, so that targets other than n are renamed too. +-- +-- newTableaux <- mapM (createTableau' []) (Target . context . return . Left <$> disjuncts) :: RobotM [Tableau] +-- newTableaux' <- mapM copyTableau newTableaux --rename all targets (inc. the disjuncts) +-- +-- +-- return (MoveDescription [n] $ "Split disjunctive target " ++ texSN n ++ ".", +-- s . Tableau tID tVs hs . Target . return . Right $ newTableaux') +-- +-- onTableau _ _ _ = mzero +---------------------------------------------------------------------------------------------------- + +removeTarget :: MoveType +removeTarget = movetypeFromSubmovetypes [ + matchTargetWithHypothesis, + matchExistentialConjunctiveTargetWithHypotheses, + matchSingleTargetWithBulletedHypothesis, + matchBulletedTargets + ] + +matchTargetWithHypothesis :: MoveType +matchTargetWithHypothesis = tableauwise onTableau where + + onTableau :: [Statement] -> Surroundings -> Tableau -> RobotM (MoveDescription, Tableau) + onTableau inheritedHs s tableau@(Tableau tID tVs hs (Target ps)) = do + --pick a hypothesis + (Statement n f _, context) <- oneOf . eachUndeletedHypothesisWithContext $ hs ++ inheritedHs + + --and a target + (Left (Statement n' f' _), targetContext) <- oneOf $ eachUndeletedTargetPartWithContext ps + + -- Try to match hypothesis and target + matching <- oneOf . maybeToList $ match (f / boundVariablesInFormula f) f' + + case targetContext [] of + [] -> return (MoveDescription [n, n'] [ProofDone] $ + "Hypothesis " ++ texSN n ++ " matches target " ++ texSN n' ++ "," ++ + " so " ++ texTN tID ++ " is done.", + s $ Done tID) + + ps' -> return (MoveDescription [n, n'] [] $ + "Hypothesis " ++ texSN n ++ " matches target " ++ texSN n' ++ "," ++ + " so we can remove " ++ texSN n' ++ ".", + s . Tableau tID tVs hs $ Target ps') + + onTableau _ _ _ = mzero + +isTrivialEquality :: Formula -> Bool +isTrivialEquality (AtomicFormula (Predicate "equals") [t,t']) = t == t' +isTrivialEquality _ = False + +matchExistentialConjunctiveTargetWithHypotheses :: MoveType +matchExistentialConjunctiveTargetWithHypotheses = tableauwise onTableau where + + onTableau :: [Statement] -> Surroundings -> Tableau -> RobotM (MoveDescription, Tableau) + onTableau inheritedHs s (Tableau tID tVs hs (Target ps)) = do + --find a target + (Left t@(Statement n' f' _), targetContext) <- oneOf $ eachUndeletedTargetPartWithContext ps + + --which is existential + (Exists vs g', expanded) <- return (f', False) <|> ((,True) <$> speculative (primaryExpansion f')) + + --match some of the conjuncts against the undeleted hypotheses + (matching, ns, leftovers) <- matchSomeOfFormulaeAmongStatements vs (conjuncts g') . filter undeleted $ hs ++ inheritedHs + + --substitute into the leftover conjuncts + let leftovers' = transform matching <$> leftovers + + --make sure the (substituted) leftover conjuncts are all trivial equalities + guard $ all isTrivialEquality leftovers' + + pd <- askPrintingData + let choices = [VariableChoice v (matching ! v) | v <- vs] + message = "All conjuncts of " ++ texSN n' ++ (guard expanded >> " (after expansion)") ++ + " can be simultaneously matched against " ++ texList (texSN <$> ns) ++ + " or rendered trivial by choosing " ++ texList (tex pd <$> choices) + + proofClauses = if expanded then [TargetIs [t], ClearlyTheCaseDone] + else [ThereforeSettingDone choices] + + case targetContext [] of + [] -> return (MoveDescription (ns ++ [n']) proofClauses $ + message ++ ", so " ++ texTN tID ++ " is done.", + s $ Done tID) + + ps' -> return (MoveDescription (ns ++ [n']) [StubClause "remove one existential target"] $ + message ++ ", so we can remove " ++ texSN n' ++ ".", + s . Tableau tID tVs hs $ Target ps') + + onTableau _ _ _ = mzero + +--disjunctivePartsOfTargetOf tableau: +--find the (possibly nested) disjunctive targets of the tableau, +-- failing if you ever see conjunctive targets +disjunctivePartsOfTargetOf :: Tableau -> Maybe [Statement] +disjunctivePartsOfTargetOf (Tableau _ _ _ (Target [p])) = onPart p where + onPart :: Either Statement [Tableau] -> Maybe [Statement] + onPart (Left s) = Just [s] + onPart (Right ts) = concat <$> mapM disjunctivePartsOfTargetOf ts where +disjunctivePartsOfTargetOf t = Nothing + +matchSingleTargetWithBulletedHypothesis :: MoveType +matchSingleTargetWithBulletedHypothesis = tableauwise onTableau where + + onTableau :: [Statement] -> Surroundings -> Tableau -> RobotM (MoveDescription, Tableau) + onTableau inheritedHs s tableau@(Tableau tID tVs hs t) = do + let bulletedVars = filter isBulletedOrDiamonded tVs + + --pick a hypothesis + (Statement n f _, context) <- oneOf $ eachUndeletedHypothesisWithContext hs + + -- if the targets of the tableau are morally a simple disjunction, extract them. + disjunctiveTargets <- oneOf . maybeToList $ disjunctivePartsOfTargetOf tableau + + --pick any one of these targets + Statement n' f' _ <- oneOf disjunctiveTargets + + -- Try to match hypothesis and target + matching <- oneOf . maybeToList $ match (f / boundVariablesInFormula f ++ bulletedVars) f' + + let choices = [VariableChoice v (matching ! v) | v <- bulletedVars] + guard $ all isBulletedVariableChoiceLegal choices + + pd <- askPrintingData + return (MoveDescription [n, n'] [ThereforeSettingDone choices] $ + "Hypothesis " ++ texSN n ++ " matches target " ++ texSN n' ++ " after choosing " ++ + texList (tex pd <$> choices) ++ ", so " ++ + texTN tID ++ " is done.", + s $ Done tID) + + onTableau _ _ _ = mzero + +--foldM :: Monad m => (Matching -> b -> m Matching) -> Matching -> [b] -> m Matching + +matchBulletedTargets :: MoveType +matchBulletedTargets = tableauwise onTableau where + + onTableau :: [Statement] -> Surroundings -> Tableau -> RobotM (MoveDescription, Tableau) + onTableau inheritedHs s tableau@(Tableau tID tVs hs (Target ps)) = do + let bulletedVars = filter isBulletedOrDiamonded tVs + visibleHs = filter undeleted $ hs ++ inheritedHs + + extend :: [Statement] -> Matching -> Either Statement [Tableau] -> RobotM Matching + extend hs m (Left (Statement _ f' _)) = do + --pick a hypothesis + (Statement n f _, context) <- oneOf $ eachUndeletedHypothesisWithContext hs + + -- Try to match hypothesis and target + oneOf . maybeToList $ extendMatch m (f' / boundVariablesInFormula f' ++ bulletedVars) f + + extend hs m (Right tableau's) = do + --pick a disjunct + (Tableau _ _ h's (Target p's)) <- oneOf tableau's + + --match against its target parts (using its extra hypotheses) + foldM (extend $ hs ++ h's) m p's + + matching <- foldM (extend visibleHs) emptyMatching ps + + let choices = [VariableChoice v (matching ! v) | v <- bulletedVars] + guard $ all isBulletedVariableChoiceLegal choices + + pd <- askPrintingData + return (MoveDescription [] [ThereforeSettingDone choices] $ + "Choosing " ++ texList (tex pd <$> choices) ++ + " matches all targets inside " ++ texTN tID ++ " against hypotheses," ++ + " so " ++ texTN tID ++ " is done.", + s $ Done tID) + + onTableau _ _ _ = mzero + +---------------------------------------------------------------------------------------------------- + +collapseSubtableauTarget :: MoveType +collapseSubtableauTarget = tableauwise onTableau where + + onTableau :: [Statement] -> Surroundings -> Tableau -> RobotM (MoveDescription, Tableau) + onTableau _ s (Tableau tID tVs hs (Target ps)) = do + --pick a target (Target p's) which is a subtableau with no (undeleted) hypotheses + -- *and* owns no variables + (Right [Tableau tID' [] h's (Target p's)], context) <- oneOf $ eachUndeletedTargetPartWithContext ps + guard $ all deleted h's + + return (MoveDescription [] [] $ "Collapsed subtableau " ++ texTN tID' ++ " as it has no undeleted hypotheses.", + s . Tableau tID tVs hs . Target $ context p's) + + onTableau _ _ _ = mzero + +---------------------------------------------------------------------------------------------------- + + +automaticRewrite :: MoveType +automaticRewrite = movetypeFromSubmovetypes [ + automaticRewriteHypothesis, + automaticRewriteTarget + ] + +automaticRewriteHypothesis :: MoveType +automaticRewriteHypothesis = tableauwise onTableau where + + onTableau :: [Statement] -> Surroundings -> Tableau -> RobotM (MoveDescription, Tableau) + onTableau _ s tableau@(Tableau tID tVs hs t) = do + --pick a hypothesis + (Statement n f _, context) <- oneOf $ eachUndeletedHypothesisWithContext hs + + --obtain its rewrite (if one exists) + rewritten <- rewriteFormula f + expansion <- oneOf $ maybeToList rewritten + + newHypothesis <- createStatement STHypothesis expansion + return (MoveDescription [n] [] $ "Rewrite terms in hypothesis " ++ texSN n ++ ".", + s $ Tableau tID tVs (context [newHypothesis]) t) + + onTableau _ _ _ = mzero + +automaticRewriteTarget :: MoveType +automaticRewriteTarget = tableauwise onTableau where + + onTableau :: [Statement] -> Surroundings -> Tableau -> RobotM (MoveDescription, Tableau) + onTableau _ s tableau@(Tableau tID tVs hs (Target ps)) = do + --pick a target + (Left (Statement n f _), context) <- oneOf $ eachUndeletedTargetPartWithContext ps + + --obtain its rewrite (if one exists) + rewritten <- rewriteFormula f + expansion <- oneOf $ maybeToList rewritten + + newTarget <- createStatement STTarget expansion + return (MoveDescription [n] [] $ "Rewrite terms in target " ++ texSN n ++ ".", + s . Tableau tID tVs hs . Target $ context [Left newTarget]) + + onTableau _ _ _ = mzero + + +rewrite :: Term -> Variable -> Formula -> Formula +rewrite t v = mapTermInFormula onTerm where + onTerm :: Term -> Term + onTerm t' | t' == t = VariableTerm v + | otherwise = t' + + +rewriteEquality :: (Formula -> [(Variable,Term)]) -> MoveType +rewriteEquality extract = tableauwise onTableau where + + onTableau :: [Statement] -> Surroundings -> Tableau -> RobotM (MoveDescription, Tableau) + onTableau _ s tableau@(Tableau tID tVs hs (Target ps)) = do + --pick a hypothesis + (h@(Statement n f _), context) <- oneOf $ eachUndeletedHypothesisWithContext hs + + --pick v,t s.t. we can rewrite t -> v + (v,t) <- oneOf $ extract f + + guard $ v `notElem` allVariablesInTerm t + + let rewriteStatement :: StatementType -> Statement -> RobotM Statement + rewriteStatement st s@(Statement n' f' tags) = + let rewritten = rewrite t v f' in + if f' == rewritten then return s + else createStatement st rewritten + + let rewriteTableau :: Tableau -> RobotM Tableau + rewriteTableau = return . mapFormulaInTableau (rewrite t v) + + let g :: Either Statement [Tableau] -> RobotM (Either Statement [Tableau]) + g = either (liftM Left . rewriteStatement STTarget) (liftM Right . mapM rewriteTableau) + + hs' <- mapM (rewriteStatement STHypothesis) $ context [] + --remove any duplicates of old hypotheses + let oldFormulae = [f | Statement _ f _ <- hs] + hs'' = [h | h@(Statement _ f _) <- hs', h `elem` hs || f `notElem` oldFormulae] + + let rewrittenHs = hs'' \\ hs + guard . not $ null rewrittenHs + + target' <- liftM Target $ mapM g ps + + pd <- askPrintingData + return (MoveDescription [n] [since [h] $ Assertion rewrittenHs] $ + "Rewrite $" ++ tex pd t ++ "$ as $" ++ tex pd v ++ "$ throughout the tableau using hypothesis " ++ texSN n ++ ".", + s $ Tableau tID tVs hs'' target') + + onTableau _ _ _ = mzero + + +rewriteVariableTermEquality = rewriteEquality extract where + extract :: Formula -> [(Variable,Term)] + extract (AtomicFormula (Predicate "equals") [vt@(VariableTerm v), v't@(VariableTerm v')]) = [(v,v't), (v',vt)] + extract (AtomicFormula (Predicate "equals") [VariableTerm v, t]) = [(v,t)] + extract (AtomicFormula (Predicate "equals") [t, VariableTerm v]) = [(v,t)] + extract _ = [] + +rewriteVariableVariableEquality = rewriteEquality extract where + extract (AtomicFormula (Predicate "equals") [vt@(VariableTerm v), v't@(VariableTerm v')]) = [(v,v't), (v',vt)] + extract _ = [] diff --git a/src/Types.hs b/src/Types.hs new file mode 100755 index 0000000..db9acba --- /dev/null +++ b/src/Types.hs @@ -0,0 +1,356 @@ +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE NoMonomorphismRestriction #-} + +module Types where + + +import Prelude hiding (repeat, (/)) +import Control.Applicative +import Data.Functor.Identity +import Control.Monad +import Control.Monad.Writer.Lazy (Writer, tell, runWriter) +import Data.Monoid +import Data.List +import Debug.Trace + +import TexBase + +---------------------------------------------------------------------------------------------------- + +data Function = Function String deriving (Eq, Ord, Show) +data Predicate = Predicate String deriving (Eq, Ord, Show) + +type ID = Int +type HasBullet = Bool --TODO: rename to isKey/hasDagger + +data Type_ = TPoint | TSet | TFunction | TPositiveRealNumber | TSequence | TNaturalNumber | TGroup + deriving (Eq, Ord, Show) +data VariableType = VTNormal | VTDiamond | VTBullet deriving (Eq, Ord, Show) + +--TODO: Independencies should be variables, not terms. +data Dependencies = Dependencies [Term] {-dep-} [Term] {-indep-} deriving (Eq, Ord, Show) + +data Variable = Variable String ID Type_ VariableType Dependencies deriving (Eq, Ord, Show) + +data Term = VariableTerm Variable + | ApplyFn Function [Term] deriving (Eq, Ord, Show) + +data Formula = AtomicFormula Predicate [Term] + | Not Formula + | And [Formula] + | Or [Formula] + | Forall [Variable] Formula + | UniversalImplies [Variable] [Formula] Formula + | Exists [Variable] Formula deriving (Eq, Ord, Show) + + +data FormulaWithSlots = FormulaWithSlots Formula [Variable] deriving (Eq, Ord, Show) +(/) :: Formula -> [Variable] -> FormulaWithSlots +(/) = FormulaWithSlots + +infixr 4 / + +data StatementType = STHypothesis | STTarget deriving (Eq, Ord, Show) + +data StatementName = StatementName StatementType ID deriving (Eq, Ord, Show) + +data Tag = Vulnerable + | Deleted + | MovedDownFrom TableauName + | UsedForwardsWith [StatementName] + | UsedBackwardsWith [StatementName] + | CannotSubstitute [[Term]] deriving (Eq, Ord, Show) + + +data Statement = Statement StatementName Formula [Tag] deriving (Eq, Ord, Show) + +type IsUnlocked = Bool + +data TableauName = TableauName IsUnlocked ID deriving (Eq, Ord, Show) + +data Tableau = Tableau TableauName [Variable] [Statement] Target + | Done TableauName deriving (Eq, Ord, Show) + +data Target = Target [Either Statement [Tableau]] --tableaux are disjunctive + | Contradiction deriving (Eq, Ord, Show) + +data VariableChoice = VariableChoice Variable Term deriving (Eq, Ord, Show) + +data Problem = Problem String [String] String deriving (Eq, Ord, Show) + +---------------------------------------------------------------------------------------------------- +prettyID :: ID -> String +prettyID n = replicate (n-1) '\'' + +prettyVariableNameID :: String -> ID -> String +prettyVariableNameID s id = s ++ prettyID id + +class Pretty a where + pretty :: a -> String + +instance Pretty Function where + pretty (Function s) = s +instance Pretty Predicate where + pretty (Predicate s) = s + +instance Pretty Dependencies where + pretty (Dependencies [] []) = "" + pretty (Dependencies ds is) = "[" ++ intercalate "," (map pretty ds ++ (("-"++). pretty <$> is)) ++ "]" + +instance Pretty VariableType where + pretty VTNormal = "" + pretty VTDiamond = "D" + pretty VTBullet = "B" + +instance Pretty Variable where + pretty (Variable s id _ vtype d) = + prettyVariableNameID s id ++ pretty vtype ++ pretty d + + +instance Pretty Term where + pretty (ApplyFn (Function "intersect") [a,b]) = pretty a ++ " cap " ++ pretty b + + pretty (VariableTerm v) = pretty v + pretty (ApplyFn fn args) = pretty fn ++ "(" ++ intercalate "," (pretty <$> args) ++ ")" + +instance Pretty Formula where + pretty (AtomicFormula (Predicate "in") [a,b]) = pretty a ++ " in " ++ pretty b + pretty (AtomicFormula (Predicate "lessthan") [a,b]) = pretty a ++ "<" ++ pretty b + pretty (AtomicFormula (Predicate "open") [a]) = pretty a ++ " is open" + + pretty (AtomicFormula pred args) = pretty pred ++ "(" ++ intercalate "," (pretty <$> args) ++ ")" + pretty (Not f) = "¬" ++ pretty f + pretty (And fs) = intercalate " & " $ pretty <$> fs + pretty (Or fs) = intercalate " v " $ pretty <$> fs + pretty (Forall vs f) = "forall " ++ intercalate ", " (pretty <$> vs) ++ ".(" ++ pretty f ++ ")" + pretty (UniversalImplies vs fs f') = "forall " ++ intercalate ", " (pretty <$> vs) ++ + ".(" ++ pretty (And fs) ++ " => " ++ pretty f' ++ ")" + pretty (Exists vs f) = "exists " ++ intercalate ", " (pretty <$> vs) ++ ".(" ++ pretty f ++ ")" + +instance Pretty FormulaWithSlots where + pretty (FormulaWithSlots f vs) = "(" ++ pretty f ++ "/" ++ unwords (pretty <$> vs) ++ ")" + +instance Pretty StatementType where + pretty STHypothesis = "H" + pretty STTarget = "T" + +instance Pretty StatementName where + pretty (StatementName t id) = pretty t ++ show id + +instance Pretty Statement where + pretty (Statement n f _) = pretty n ++ ". " ++ pretty f + +instance Pretty Tableau where + pretty (Tableau id vs ss t) = unlines $ + [show id] ++ + (pretty <$> ss) ++ + ["--------", + pretty t] + pretty (Done _) = "Done" + +instance Pretty Target where --output goes inside an array env. + pretty (Target ps) = unlines [either pretty (unlines . map pretty) p | p <- ps] + pretty Contradiction = "Contradiction" + +---------------------------------------------------------------------------------------------------- + +allVariablesInTerm :: Term -> [Variable] +allVariablesInTerm = nub . sort . accumulateVariableInTerm return + +allVariablesInFormula :: Formula -> [Variable] +allVariablesInFormula = nub . sort . accumulateVariableInFormula return + + + +allDirectVariablesInFormula :: Formula -> [Variable] +allDirectVariablesInFormula = nub . sort . accumulateDirectVariableInFormula return +---------------------------------------------------------------------------------------------------- + +--mapXM: drills down through X to find all subXs +--mapDirectXInYM: drills down through Ys to find Xs; does not look inside Xs +--mapDirectXInYM: drills down through Ys to find Xs; does look inside Xs + + +mapVariableM :: Monad m => (Variable -> m Variable) -> Variable -> m Variable +mapVariableM fn (Variable n id t bs (Dependencies ds is)) = + fn =<< Variable n id t bs `liftM` (return Dependencies `ap` mapM (mapDirectVariableInTermM $ mapVariableM fn) ds + `ap` mapM (mapDirectVariableInTermM $ mapVariableM fn) is) + +mapDirectTermInVariableM :: Monad m => (Term -> m Term) -> Variable -> m Variable +mapDirectTermInVariableM fn (Variable n id t bs (Dependencies ds is)) = + Variable n id t bs `liftM` (return Dependencies `ap` mapM fn ds `ap` mapM fn is) + +mapTermInVariableM = mapDirectTermInVariableM . mapTermM + +mapTermM :: Monad m => (Term -> m Term) -> Term -> m Term +mapTermM f (VariableTerm (Variable n id t bs (Dependencies ds is))) = + f . VariableTerm . Variable n id t bs =<< return Dependencies `ap` mapM (mapTermM f) ds + `ap` mapM (mapTermM f) is +mapTermM f (ApplyFn fn args) = f . ApplyFn fn =<< mapM (mapTermM f) args + +mapDirectVariableInTermM :: Monad m => (Variable -> m Variable) -> Term -> m Term +mapDirectVariableInTermM f (VariableTerm v) = VariableTerm `liftM` f v +mapDirectVariableInTermM f (ApplyFn fn args) = ApplyFn fn `liftM` mapM (mapDirectVariableInTermM f) args + +mapVariableInTermM = mapDirectVariableInTermM . mapVariableM + + +mapFormulaM :: Monad m => (Formula -> m Formula) -> Formula -> m Formula +mapFormulaM fn f@(AtomicFormula _ _) = fn f +mapFormulaM fn (Not f) = fn . Not =<< mapFormulaM fn f +mapFormulaM fn (And fs) = fn . And =<< mapM (mapFormulaM fn) fs +mapFormulaM fn (Or fs) = fn . Or =<< mapM (mapFormulaM fn) fs +mapFormulaM fn (Forall vs f) = fn . Forall vs =<< mapFormulaM fn f +mapFormulaM fn (UniversalImplies vs fs f') = fn =<< UniversalImplies vs `liftM` mapM (mapFormulaM fn) fs `ap` mapFormulaM fn f' +mapFormulaM fn (Exists vs f) = fn . Exists vs =<< mapFormulaM fn f + +mapDirectVariableInFormulaM :: Monad m => (Variable -> m Variable) -> Formula -> m Formula +mapDirectVariableInFormulaM fn = mapFormulaM immediate where + immediate (AtomicFormula pred args) = AtomicFormula pred `liftM` mapM (mapDirectVariableInTermM fn) args + immediate f@(Not _) = return f + immediate f@(And _) = return f + immediate f@(Or _) = return f + immediate (Forall vs f) = Forall `liftM` mapM fn vs `ap` return f + immediate (UniversalImplies vs as c) = UniversalImplies `liftM` mapM fn vs `ap` return as `ap` return c + immediate (Exists vs f) = Exists `liftM` mapM fn vs `ap` return f + +mapVariableInFormulaM = mapDirectVariableInFormulaM . mapVariableM + +--mapDirectTermInFormulaM: drills down through formulae to find terms; does not look inside terms +mapDirectTermInFormulaM :: Monad m => (Term -> m Term) -> Formula -> m Formula +mapDirectTermInFormulaM fn = mapFormulaM onDirectSubterm where + onDirectSubterm (AtomicFormula pred args) = AtomicFormula pred `liftM` mapM fn args + onDirectSubterm f@(Not _) = return f + onDirectSubterm f@(And _) = return f + onDirectSubterm f@(Or _) = return f + onDirectSubterm (Forall vs f) = Forall `liftM` mapM (mapDirectTermInVariableM fn) vs `ap` return f + onDirectSubterm (UniversalImplies vs as c) = UniversalImplies `liftM` mapM (mapDirectTermInVariableM fn) vs `ap` return as `ap` return c + onDirectSubterm (Exists vs f) = Exists `liftM` mapM (mapDirectTermInVariableM fn) vs `ap` return f + +mapTermInFormulaM :: Monad m => (Term -> m Term) -> Formula -> m Formula --deep (affects all subterms) +mapTermInFormulaM = mapDirectTermInFormulaM . mapTermM + +mapDirectFormulaInStatementM :: Monad m => (Formula -> m Formula) -> Statement -> m Statement +mapDirectFormulaInStatementM fn (Statement n f ts) = return (Statement n) `ap` fn f `ap` return ts + + +eitherM :: Monad m => (a -> m a) -> (b -> m b) -> Either a b -> m (Either a b) +eitherM f g = either (liftM Left . f) (liftM Right . g) + +--mapTableauM : deep (affacts all subtableau of given tableau) +mapTableauM :: forall m. Monad m => (Tableau -> m Tableau) -> Tableau -> m Tableau +mapTableauM fn (Tableau id vs hs t) = fn =<< Tableau id vs hs `liftM` inTargetM t where + inTargetM :: Target -> m Target + inTargetM (Target ps) = Target `liftM` mapM g ps where + g :: Either Statement [Tableau] -> m (Either Statement [Tableau]) + g = eitherM return $ mapM (mapTableauM fn) + inTargetM Contradiction = return Contradiction +mapTableauM fn d@(Done _) = fn d + +--TODO: tidy this next function +mapDirectVariableInTableauM :: forall m. Monad m => (Variable -> m Variable) -> Tableau -> m Tableau +mapDirectVariableInTableauM fn (Tableau id vs hs t) = + return (Tableau id) `ap` mapM fn vs + `ap` mapM (mapDirectFormulaInStatementM $ mapDirectVariableInFormulaM fn) hs + `ap` inTargetM t where + inTargetM :: Target -> m Target + inTargetM (Target ps) = liftM Target (mapM g ps) where + g :: Either Statement [Tableau] -> m (Either Statement [Tableau]) + g = eitherM (mapDirectFormulaInStatementM $ mapDirectVariableInFormulaM fn) + (mapM (mapDirectVariableInTableauM fn)) + inTargetM Contradiction = return Contradiction +mapDirectVariableInTableauM _ d@(Done _) = return d + +mapVariableInTableauM = mapDirectVariableInTableauM . mapVariableM + +mapDirectTermInTableauM :: Monad m => (Term-> m Term) -> Tableau -> m Tableau --deep (affects all terms) +mapDirectTermInTableauM = mapDirectFormulaInTableauM . mapDirectTermInFormulaM + +mapTermInTableauM :: Monad m => (Term-> m Term) -> Tableau -> m Tableau --deep (affects all terms) +mapTermInTableauM = mapDirectFormulaInTableauM . mapTermInFormulaM + +--mapDirectFormulaInTableauM: drills down through tableaux and targets to find formulae; does not look inside formulae +mapDirectFormulaInTableauM :: forall m. Monad m => (Formula -> m Formula) -> Tableau -> m Tableau +mapDirectFormulaInTableauM fn (Tableau id vs hs t) = return (Tableau id vs) `ap` mapM (mapDirectFormulaInStatementM fn) hs + `ap` inTargetM t where + inTargetM :: Target -> m Target + inTargetM (Target ps) = Target `liftM` mapM g ps where + g :: Either Statement [Tableau] -> m (Either Statement [Tableau]) + g = eitherM (mapDirectFormulaInStatementM fn) + (mapM $ mapDirectFormulaInTableauM fn) + inTargetM Contradiction = return Contradiction +mapDirectFormulaInTableauM _ d@(Done _) = return d + +mapFormulaInTableauM :: Monad m => (Formula -> m Formula) -> Tableau -> m Tableau --deep (affects all subformulae) +mapFormulaInTableauM = mapDirectFormulaInTableauM . mapFormulaM + +---------------------------------------------------------------------------------------------------- + +nonmonadic :: ((a -> Identity a) -> b-> Identity b) -> (a -> a) -> b -> b +nonmonadic mm f = runIdentity . mm (return . f) + +mapVariable = nonmonadic mapVariableM +mapTerm = nonmonadic mapTermM +mapTermInVariable = nonmonadic mapTermInVariableM +mapDirectVariableInTerm = nonmonadic mapDirectVariableInTermM +mapVariableInTerm = nonmonadic mapVariableInTermM + +mapFormula = nonmonadic mapFormulaM +mapDirectVariableInFormula = nonmonadic mapDirectVariableInFormulaM +mapVariableInFormula = nonmonadic mapVariableInFormulaM +mapDirectTermInFormula = nonmonadic mapDirectTermInFormulaM +mapTermInFormula = nonmonadic mapTermInFormulaM + +mapTableau = nonmonadic mapTableauM +mapDirectVariableInTableau = nonmonadic mapDirectVariableInTableauM +mapVariableInTableau = nonmonadic mapVariableInTableauM +mapDirectTermInTableau = nonmonadic mapDirectTermInTableauM +mapTermInTableau = nonmonadic mapTermInTableauM +mapDirectFormulaInTableau = nonmonadic mapDirectFormulaInTableauM +mapFormulaInTableau = nonmonadic mapFormulaInTableauM + +---------------------------------------------------------------------------------------------------- + +accumulate :: forall w. forall a. forall b. (Monoid w) => ((a -> Writer w a) -> b-> Writer w b) -> (a -> w) -> b -> w +accumulate mm f = snd . runWriter . mm write + where write :: a -> Writer w a + write = liftM2 (>>) (tell . f) return + +accumulateVariable = accumulate mapVariableM +accumulateTerm = accumulate mapTermM +accumulateTermInVariable = accumulate mapTermInVariableM +accumulateDirectVariableInTerm = accumulate mapDirectVariableInTermM +accumulateVariableInTerm = accumulate mapVariableInTermM + +accumulateFormula = accumulate mapFormulaM +accumulateDirectVariableInFormula = accumulate mapDirectVariableInFormulaM +accumulateVariableInFormula = accumulate mapVariableInFormulaM +accumulateDirectTermInFormula = accumulate mapDirectTermInFormulaM +accumulateTermInFormula = accumulate mapTermInFormulaM + +accumulateTableau :: Monoid w => (Tableau -> w) -> Tableau -> w +accumulateTableau = accumulate mapTableauM +accumulateDirectVariableInTableau = accumulate mapDirectVariableInTableauM +accumulateVariableInTableau = accumulate mapVariableInTableauM +accumulateDirectTermInTableau = accumulate mapDirectTermInTableauM +accumulateTermInTableau = accumulate mapTermInTableauM +accumulateDirectFormulaInTableau = accumulate mapDirectFormulaInTableauM +accumulateFormulaInTableau = accumulate mapFormulaInTableauM + +---------------------------------------------------------------------------------------------------- + +isAtomic :: Formula -> Bool +isAtomic (AtomicFormula _ _) = True +isAtomic (Not _) = True +isAtomic (And fs) = True +isAtomic (Or _) = True +isAtomic (Forall _ _) = False +isAtomic (UniversalImplies _ _ _) = False +isAtomic (Exists _ _) = False + +isBulletedOrDiamonded :: Variable -> Bool +isBulletedOrDiamonded (Variable _ _ _ VTNormal _) = False +isBulletedOrDiamonded (Variable _ _ _ VTDiamond _) = True +isBulletedOrDiamonded (Variable _ _ _ VTBullet _) = True + +---------------------------------------------------------------------------------------------------- diff --git a/src/Writeup.hs b/src/Writeup.hs new file mode 100755 index 0000000..7d50308 --- /dev/null +++ b/src/Writeup.hs @@ -0,0 +1,413 @@ +{-# LANGUAGE FlexibleInstances #-} + +module Writeup + where + + +import Control.Applicative +--import Control.Arrow +----import Control.Monad.RWS hiding (msum) +--import Control.Monad.Logic hiding (msum) +--import Control.Monad.Trans.List +--import Control.Monad.Trans.State.Lazy +--import Control.Monad.Identity hiding (msum) +import Control.Monad +--import Data.Either +import Data.List +import Data.Maybe +--import Data.Map hiding (map, filter, null) +--import Data.Foldable (msum) +import Data.Char +import Data.Map (Map, (!)) +import qualified Data.Map as Map + +import Debug.Trace + +import Printing +import Types +import TexBase +import Tex + + +---------------------------------------------------------------------------------------------------- + +class Writeup a where + writeup :: PrintingData -> a -> String + +---------------------------------------------------------------------------------------------------- + +commaList :: [String] -> String +commaList [] = error "commaList called with empty list" +commaList [s] = s +commaList ss = intercalate "," ss + +andList :: [String] -> String +andList [] = "EMPTYANDLIST" -- error "andList called with empty list" +andList [s] = s +andList ss = intercalate ", " (init ss) ++ " and " ++ last ss + +orList :: [String] -> String +orList [] = error "orList called with empty list" +orList [s] = s +orList ss = intercalate ", " (init ss) ++ " or " ++ last ss + +instance Writeup Predicate where + writeup pd p = tex pd p + +instance Writeup Function where + writeup pd f = tex pd f + +writeupID :: ID -> String +writeupID n = replicate (n-1) '\'' + +instance Writeup Variable where + writeup pd (Variable s id t hasBullet d) = tex pd . Variable s id t VTNormal $ Dependencies [] [] + +writeupIntro :: PrintingData -> Variable -> String +writeupIntro pd v@(Variable _ _ TPositiveRealNumber _ _) = writeup pd v ++ " > 0" +writeupIntro pd v = writeup pd v + +writeupSequenceShort :: PrintingData -> Term -> String +writeupSequenceShort pd (VariableTerm (Variable "an" id _ _ _)) = "a_n" ++ writeupID id +writeupSequenceShort pd t = writeup pd t + +writeupSequenceElement :: Variable -> String -> String +writeupSequenceElement (Variable "an" id _ _ _) s = "a_{" ++ s ++ "}" ++ writeupID id + +instance Writeup Term where + writeup pd (ApplyFn (Function "applyfnpointwise") [f,an]) = writeup pd f ++ "(" ++ writeupSequenceShort pd an ++ ")" + writeup pd (ApplyFn (Function "kthterm") [VariableTerm an,k]) = writeupSequenceElement an (writeup pd k) + + writeup pd (VariableTerm v) = writeup pd v + writeup pd (ApplyFn fn@(Function name) args) = case Map.lookup name (termPatterns pd) of + Just p -> instantiatePattern p $ writeup pd <$> args + Nothing -> writeup pd fn ++ "(" ++ intercalate "," (writeup pd <$> args) ++ ")" + + +--TODO: generalise these to search through all conjuncts properly +-- and to handle multiple variables. +writeupST :: PrintingData -> [Variable] -> Formula -> String +writeupST pd [v] (And (AtomicFormula (Predicate "in") [VariableTerm v',t]:fs@(_:_))) + | v == v' = math (writeup pd v ++ "\\in " ++ writeup pd t) ++ " s.t. " ++ writeup pd (And fs) +writeupST pd vs f = math (commaList $ writeupIntro pd <$> vs) ++ " s.t. " ++ writeup pd f + +writeupSuchThat :: PrintingData -> [Variable] -> Formula -> String +writeupSuchThat pd [v] (And (AtomicFormula (Predicate "in") [VariableTerm v',t]:fs@(_:_))) + | v == v' = math (writeup pd v ++ "\\in " ++ writeup pd t) ++ " such that " ++ writeup pd (And fs) +writeupSuchThat pd vs f = math (commaList $ writeupIntro pd <$> vs) ++ " such that " ++ writeup pd f + + +instance Writeup Formula where + writeup pd (AtomicFormula (Predicate "tendsto") [an,b]) = math $ writeupSequenceShort pd an ++ "\\to " ++ writeup pd b + + writeup pd (AtomicFormula pred@(Predicate name) args) = case Map.lookup name (formulaPatterns pd) of + Just p -> instantiatePattern p $ writeup pd <$> args + Nothing -> math $ writeup pd pred ++ "(" ++ intercalate "," (writeup pd <$> args) ++ ")" + + writeup pd (Not f) = "it is not that case that " ++ writeup pd f + writeup pd (And fs) = andList $ writeup pd <$> fs + writeup pd (Or fs) = orList $ writeup pd <$> fs + writeup pd (Forall vs f) = math $ "\\forall " ++ commaList (writeup pd <$> vs) ++ ".(" ++ textrm (writeup pd f) ++ ")" + writeup pd (UniversalImplies _ [f@(AtomicFormula _ _)] f'@(AtomicFormula _ _)) = + writeup pd f' ++ textrm " whenever " ++ writeup pd f + writeup pd (UniversalImplies _ [f] f') = "if " ++ writeup pd f ++ ", then " ++ writeup pd f' + writeup pd (UniversalImplies vs fs f') = math $ "\\forall " ++ intercalate ", " (writeup pd <$> vs) ++ + ".(" ++ textrm (writeup pd (And fs)) ++ "\\Rightarrow " ++ textrm (writeup pd f') ++ ")" + writeup pd (Exists vs f) = "there exist " ++ writeupST pd vs f + +instance Writeup VariableChoice where + writeup pd (VariableChoice v t) = math $ writeup pd v ++ " = " ++ writeup pd t + +instance Writeup Statement where + writeup pd (Statement n f _) = writeup pd f + + +instance Writeup [Formula] where + writeup pd fs = andList $ writeup pd <$> fs + +instance Writeup [Statement] where + writeup pd ss = andList $ writeup pd <$> ss + +---------------------------------------------------------------------------------------------------- + +type Follows = Bool + +data Clause = StubClause String + | ProofDone -- we are done + | TargetReminder [Statement] -- we are trying to show X + | TargetIs [Statement] -- we would like to show X + | TargetIsIE [Statement] [Statement] -- we would like to show X, i.e. Y + | Let [LetArgs] + | Take [Variable] + | Assertion [Statement] -- X + | WeMayTake [VariableChoice] -- we may therefore take x = T + | ThereforeSettingDone [VariableChoice] -- therefore, setting x = T, we are done + | If [Statement] Statement --P and P' if Q + | Whenever [Statement] Statement --P and P' whenever Q + | Iff [Statement] [Statement] + | AssumeNow [Statement] + | ClearlyTheCaseDone -- But this is clearly the case, so we are done + + | ExistVars [Variable] Clause + | Since [Statement] Follows [Clause] + | ByDefSince [Statement] Follows [Clause] + | WeKnowThat [Clause] + | But Clause --may turn into an adverb + +data LetArgs = BeSuchThat [Variable] [Statement] -- let x and y be be s.t X + | Suspended [Variable] -- let x be a constant to be chosen later +-- | Unconstrained Variable -- let epsilon > 0 + +data Adverb = Then | So | Also | AndA | IE | Therefore | Thus deriving Eq + +data Unit = Unit (Maybe Adverb) [Clause] + +since :: [Statement] -> Clause -> Clause +since [] c = c +since ss c = Since ss False [c] + +byDefSince :: [Statement] -> Clause -> Clause +byDefSince [] c = c +byDefSince ss c = ByDefSince ss False [c] + +existVars :: [Variable] -> Clause -> Clause +existVars [] c = c +existVars vs c = ExistVars vs c + +weKnowThat :: Clause -> Clause +weKnowThat c = WeKnowThat [c] + +---------------------------------------------------------------------------------------------------- + + +isNominal :: PrintingData -> Formula -> Bool +isNominal pd (AtomicFormula (Predicate name) _) = name `Map.member` nounPatterns pd +isNominal _ _ = False + +isAdjectival :: PrintingData -> Formula -> Bool +isAdjectival pd (AtomicFormula (Predicate name) _) = name `Map.member` adjectivePatterns pd +isAdjectival _ _ = False + +writeupNoun :: PrintingData -> Formula -> String +writeupNoun pd (AtomicFormula (Predicate name) (a:as)) = + instantiatePattern (nounPatterns pd ! name) (writeup pd <$> as) + +writeupAdjective :: PrintingData -> Formula -> String +writeupAdjective pd (AtomicFormula (Predicate name) (a:as)) = + instantiatePattern (adjectivePatterns pd ! name) (writeup pd <$> as) + +---------------------------------------------------------------------------------------------------- + +addAOrAn :: String -> String +addAOrAn s@(c:_) + | c `elem` "aeiou" = "an " ++ s + | otherwise = "a " ++ s + +instance Writeup LetArgs where + writeup pd (BeSuchThat [v] ss) = + let fs = [f | Statement _ f _ <- ss] + aboutVs = [f | f@(AtomicFormula _ (VariableTerm v':_)) <- fs, v' == v] + ns = filter (isNominal pd) aboutVs + as = filter (isAdjectival pd) aboutVs + rests = fs \\ (ns ++ as) + + in "let " ++ math (writeupIntro pd v) ++ " be " ++ case (ns, as, rests) of + ((n:n's), _, _) -> + addAOrAn (concatMap ((++ " ") . writeupAdjective pd) as ++ writeupNoun pd n) ++ + (guard (not . null $ n's ++ rests) >> (" such that " ++ writeup pd (n's ++ rests))) + + _ -> "such that " ++ writeup pd fs + +-- writeup pd (BeSuchThat [v] [Statement _ (AtomicFormula (Predicate "in") [v',t]) _]) = +-- "let " ++ math (writeupIntro v) ++ " be an element of " ++ math (writeup t) + writeup pd (BeSuchThat vs ss) = "let " ++ andList (math . writeupIntro pd <$> vs) ++ + " be such that " ++ writeup pd ss + writeup pd (Suspended [v]) = "let " ++ math (writeupIntro pd v) ++ " be a constant to be chosen later" + writeup pd (Suspended vs) = "let " ++ andList (math . writeupIntro pd <$> vs) ++ " be constants to be chosen later" +-- writeup pd (Unconstrained v@(Variable _ _ TPositiveRealNumber _ _)) = "let " ++ math (writeupIntro v) +-- writeup pd (Unconstrained v@(Variable _ _ TPoint _ _)) = "let " ++ math (writeupIntro v) ++ " be a point" +-- writeup pd (Unconstrained v) = "let " ++ math (writeupIntro v) ++ " be a constant" + +writeupShow :: PrintingData -> [Statement] -> String +writeupShow pd [Statement _ (Exists vs f) _] = "find " ++ writeupST pd vs f +writeupShow pd ss = "show that " ++ writeup pd ss + +extractFormulae :: [Statement] -> Formula +extractFormulae [Statement _ f _] = f +extractFormulae ss = And [f | Statement _ f _ <- ss] + +instance Writeup Clause where + writeup pd (StubClause s) = textbf $ "[" ++ s ++ "]" + writeup pd ProofDone = "we are done" + writeup pd (TargetReminder ss) = "[we are trying to " ++ writeupShow pd ss ++ ".]" + writeup pd (TargetIs ss) = "we would like to " ++ writeupShow pd ss + writeup pd (TargetIsIE ss s's) = "we would like to show that " ++ writeup pd ss ++ ", i.e. that " ++ writeup pd s's + writeup pd (Let as) = andList $ writeup pd <$> as + writeup pd (Take [v@(Variable _ _ TPositiveRealNumber _ _)]) = "let " ++ math (writeupIntro pd v) + writeup pd (Take vs) = "take " ++ andList (math . writeupIntro pd <$> vs) + writeup pd (Assertion ss) = writeup pd ss + writeup pd (WeMayTake vcs) = "we may therefore take " ++ andList (writeup pd <$> vcs) + writeup pd (ThereforeSettingDone vcs) = "therefore, setting " ++ andList (writeup pd <$> vcs) ++ ", we are done" + writeup pd (If as c) = writeup pd c ++ " if " ++ andList (writeup pd <$> as) + writeup pd (Whenever as c) = writeup pd c ++ " whenever " ++ andList (writeup pd <$> as) + writeup pd (Iff ss s's) = writeup pd ss ++ " if and only if " ++ writeup pd s's + writeup pd (AssumeNow ss) = "assume now that " ++ writeup pd ss + writeup pd (ExistVars [v] (Assertion ss)) = + "there exists " ++ writeupSuchThat pd [v] (extractFormulae ss) + writeup pd (ExistVars [v] c) = + "there exists " ++ math (writeupIntro pd v) ++ " such that " ++ writeup pd c + writeup pd (ExistVars vs c) = + "there exist " ++ andList (math . writeupIntro pd <$> vs) ++ " such that " ++ writeup pd c + writeup pd (Since ss False cs@[Assertion [Statement _ (AtomicFormula _ _) _]]) = + "since " ++ writeup pd ss ++ ", we have that " ++ writeup pd cs + writeup pd (Since ss f cs) = "since " ++ writeup pd ss ++ ", " ++ (guard f >> "it follows that ") ++ writeup pd cs + writeup pd (ByDefSince ss False cs@[Assertion [Statement _ (AtomicFormula _ _) _]]) = + "by definition, since " ++ writeup pd ss ++ ", we have that " ++ writeup pd cs + writeup pd (ByDefSince ss f cs) = "by definition, since " ++ writeup pd ss ++ ", " ++ (guard f >> "it follows that ") ++ writeup pd cs + writeup pd (WeKnowThat cs) = "we know " ++ andList (("that " ++) . writeup pd <$> cs) + writeup pd (But c) = "but " ++ writeup pd c + writeup pd ClearlyTheCaseDone = "but this is clearly the case, so we are done" + +instance Writeup [Clause] where + writeup pd cs = andList $ writeup pd <$> cs + +instance Writeup Adverb where + writeup _ Then = "then" + writeup _ So = "so" + writeup _ Also = "also" + writeup _ AndA = "and" + writeup _ IE = "that is," + writeup _ Therefore = "therefore" + writeup _ Thus = "thus" + +instance Writeup Unit where + writeup pd (Unit (Just a) cs@(Since _ _ _:_)) + | a /= IE = writeup pd a ++ ", " ++ writeup pd cs + writeup pd (Unit (Just a) cs) = writeup pd a ++ " " ++ writeup pd cs + writeup pd (Unit Nothing cs) = writeup pd cs + +asSentence :: String -> String +asSentence (c:cs) = (toUpper c:cs) ++ (guard (length cs >= 2 && last cs /= ']') >> ".") + +---------------------------------------------------------------------------------------------------- + +--Sometimes The same statement will have different tags at different points in the proof, so +-- Also sometimes variables will have gained/lost a diamond/circle +-- So we need to compare the statement names, not the formulae + +(===) :: Statement -> Statement -> Bool +Statement n _ _ === Statement n' _ _ = n == n' + +(=:=) :: [Statement] -> [Statement] -> Bool +ss =:= s's = and $ zipWith (===) ss s's + +nameElem :: Statement -> [Statement] -> Bool +nameElem s (s':s's) + | s === s' = True + | otherwise = s `nameElem` s's +nameElem s [] = False + +nameNotElem :: Statement -> [Statement] -> Bool +nameNotElem s = not . nameElem s + +---------------------------------------------------------------------------------------------------- + +--code to fuse together clauses were possible; e.g. +-- since P, Q. since P, R. +-- is changed into +-- since P, Q and R + + +fuse :: [Clause] -> [Clause] +fuse (c:cs@(c':c's)) = case fusePair c c' of + Just f -> fuse $ f:c's + Nothing -> c:fuse cs +fuse (c:[]) = [c] +fuse [] = [] + +fusePair :: Clause -> Clause -> Maybe Clause +fusePair (Since ss False cs) (Since s's False c's) + | ss =:= s's = Just . Since ss False . fuse $ cs ++ c's +fusePair (Let as) (Let a's) = Just . Let $ as ++ a's +fusePair (WeKnowThat as) (WeKnowThat a's) = Just . WeKnowThat $ as ++ a's +fusePair t@(TargetIs ss) (TargetIs s's) + | ss == s's = Just t +fusePair t@(TargetIsIE ss s's) (TargetIs s''s) + | s's == s''s = Just t +fusePair _ _ = Nothing + +---------------------------------------------------------------------------------------------------- + +--eliminate references to facts just introduced and introduce corresponding rhetorical structure: +-- E.g. +-- P. since P and Q, R. +-- is changed into +-- P. since Q, it follows that R. + +--factsDeduced: the facts deduced in a particular step +factsDeduced :: Clause -> [Statement] +factsDeduced (StubClause s) = [] +factsDeduced ProofDone = [] +factsDeduced (TargetReminder ss) = [] +factsDeduced (TargetIs ss) = [] +factsDeduced (TargetIsIE _ _) = [] +factsDeduced (Let as) = [] +factsDeduced (Take _) = [] +factsDeduced (Assertion ss) = ss +factsDeduced (WeMayTake cs) = [] +factsDeduced (ThereforeSettingDone cs) = [] +factsDeduced (If as c) = [] +factsDeduced (Whenever as c) = [] +factsDeduced (Iff ss s's) = ss ++ s's +factsDeduced (AssumeNow ss) = ss +factsDeduced (ExistVars vs c) = [] --factsDeduced c +factsDeduced (Since ss f cs) = concatMap factsDeduced cs +factsDeduced (ByDefSince ss f cs) = concatMap factsDeduced cs +factsDeduced (WeKnowThat cs) = concatMap factsDeduced cs +factsDeduced (But c) = factsDeduced c +factsDeduced ClearlyTheCaseDone = [] + +--factsDeclared: the facts declared by 'let's, etc. in a particular step +factsDeclared :: Clause -> [Statement] +factsDeclared (Let as) = concat [ss | BeSuchThat _ ss <- as] +factsDeclared _ = [] + +isAtomicStatement :: Statement -> Bool +isAtomicStatement (Statement _ f _) = isAtomic f + +--atomicFactsPresented :: Clause -> [Statement] +--atomicFactsPresented = const [] --filter isAtomicStatement . factsDeduced + +--TODO tidy +eliminate :: [Clause] -> [Unit] +eliminate cs = zipWith4 convert factsDeducedInPrevClause factsDeclaredInPrevClause twoBack cs where + factsDeducedInPrevClause = []:(factsDeduced <$> cs) + factsDeclaredInPrevClause = []:(factsDeclared <$> cs) + twoBack = []:[]:(factsDeduced <$> cs) +-- allAtomicFactsPresented = [concatMap atomicFactsPresented prev | (c, prev) <- zip cs (inits cs)] + +--convert: factsDeducedInPrevClause -> factsDeclaredInPrevClause -> twoBack -> ThisClause -> Unit +convert :: [Statement] -> [Statement] -> [Statement] -> Clause -> Unit +convert fs ls as (Since ss _ cs) + | all (`nameElem` (fs ++ ls ++ as)) ss && any (`nameElem` (fs ++ ls)) ss = Unit (Just Then) $ cs + | any (`nameElem` fs) ss = Unit (Just Therefore) [Since (filter (`nameNotElem` (fs ++ ls ++ as)) ss) False cs] + | any (`nameElem` ls) ss = Unit (Just Then) [Since (filter (`nameNotElem` (ls ++ as)) ss) False cs] + | all (`nameElem` as) ss = Unit (Just AndA) $ cs + | any (`nameElem` as) ss = Unit (Just AndA) [Since (filter (`nameNotElem` as) ss) False cs] +convert fs ls as (ByDefSince ss _ cs) + | all (`nameElem` (ls ++ as)) ss && any (`nameElem` ls) ss = Unit (Just Then) $ cs + | all (`nameElem` (fs ++ ls ++ as)) ss && any (`nameElem` (fs ++ ls)) ss = Unit (Just IE) $ cs + | any (`nameElem` fs) ss = Unit (Just Therefore) [ByDefSince (filter (`nameNotElem` (fs ++ ls ++ as)) ss) False cs] + | any (`nameElem` ls) ss = Unit (Just Then) [ByDefSince (filter (`nameNotElem` (ls ++ as)) ss) False cs] + | all (`nameElem` as) ss = Unit (Just AndA) $ cs + | any (`nameElem` as) ss = Unit (Just AndA) [ByDefSince (filter (`nameNotElem` as) ss) False cs] +convert fs ls as c = Unit Nothing [c] + +---------------------------------------------------------------------------------------------------- + +compress :: [Unit] -> [Unit] +compress (Unit ma cs:Unit (Just AndA) c's:u's) = compress (Unit ma (cs ++ c's):u's) +compress [Unit ma cs, Unit Nothing [ProofDone]] = [Unit ma $ cs ++ [ProofDone]] +compress [Unit Nothing [TargetIs ss], Unit Nothing [ClearlyTheCaseDone]] = [Unit (Just Thus) [Assertion ss, ProofDone]] +compress (u:us)= u:compress us +compress us = us diff --git a/texput.log b/texput.log new file mode 100755 index 0000000..f50955a --- /dev/null +++ b/texput.log @@ -0,0 +1,16 @@ +This is XeTeX, Version 3.14159265-2.6-0.99992 (MiKTeX 2.9) (preloaded format=xelatex 2015.9.14) 3 FEB 2016 13:19 +entering extended mode +**\def\showsteps{1} \input{robotone.tex}^^M +^^@:0: Emergency stop +*** (cannot \read from terminal in nonstop modes) + + +Here is how much of TeX's memory you used: + 3 strings out of 428755 + 27 string characters out of 3165417 + 52045 words of memory out of 3000000 + 3436 multiletter control sequences out of 15000+200000 + 3640 words of font info for 14 fonts, out of 3000000 for 9000 + 1096 hyphenation exceptions out of 8191 + 4i,0n,3p,1b,8s stack positions out of 5000i,500n,10000p,200000b,50000s +No pages of output.