root/logic
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

big tidy

Browse source
This commit is contained in:
hi 2025-08-15 10:06:31 +00:00
parent bd9b58c405
commit 687b5f1040
6 changed files with 54 additions and 39 deletions
Download patch file Download diff file Expand all files Collapse all files

56
Logic/Statement/Laws.hs
View file

@ -15,6 +15,11 @@ data Law = Law
, lawRhs :: Statement
}
instance Eq Law where
law1 == law2 =
lawLhs law1 == lawLhs law2
&& lawRhs law1 == lawRhs law2
instance Show Law where
show law =
"Law{"
@ -29,28 +34,28 @@ mkLaw :: String -> String -> String -> Law
mkLaw name lhs rhs = Law name (fromString lhs) (fromString rhs)
where
fromString :: String -> Statement
fromString string = fromRight undefined (eof stmt $ mkInput string)
fromString string = fromRight undefined $ eof stmt $ mkInput string
laws :: [Law]
laws =
[ mkLaw "dbl_neg" "A" "!!A"
, mkLaw "and_comm" "(A&B)" "(B&A)"
, mkLaw "or_comm" "(A|B)" "(B|A)"
, mkLaw "and_assoc" "(A&(B&C))" "((A&B)&C)"
, mkLaw "or_assoc" "(A|(B|C))" "((A|B)|C)"
, mkLaw "and_or_distrib" "(A&(B|C))" "((A&B)|(A&C))"
, mkLaw "or_and_distrib" "(A|(B&C))" "((A|B)&(A|C))"
, mkLaw "and_symm_eq" "A" "(A&A)"
, mkLaw "or_symm_eq" "A" "(A|A)"
, mkLaw "not_and_distrib" "!(A&B)" "(!A|!B)"
, mkLaw "not_or_distrib" "!(A|B)" "(!A&!B)"
, mkLaw "implies_or" "(A->B)" "(!A|B)"
, mkLaw "implies_and" "(A->B)" "!(A&!B)"
, mkLaw "or_contr_eq" "A" "(A|(B&!B))"
, mkLaw "and_or_cancel" "A" "(A&(A|B))"
, mkLaw "or_and_cancel" "A" "(A|(A&B))"
, mkLaw "iff_and" "(A<->B)" "((A->B)&(B->A))"
, mkLaw "iff_or" "(A<->B)" "((A&B)|(!A&!B))"
[ mkLaw "dbl_neg" "A" "!!A"
, mkLaw "and_comm" "(A&B)" "(B&A)"
, mkLaw "or_comm" "(A|B)" "(B|A)"
, mkLaw "and_assoc" "(A&(B&C))" "((A&B)&C)"
, mkLaw "or_assoc" "(A|(B|C))" "((A|B)|C)"
, mkLaw "and_or_distrib" "(A&(B|C))" "((A&B)|(A&C))"
, mkLaw "or_and_distrib" "(A|(B&C))" "((A|B)&(A|C))"
, mkLaw "and_symm_eq" "A" "(A&A)"
, mkLaw "or_symm_eq" "A" "(A|A)"
, mkLaw "not_and_distrib" "!(A&B)" "(!A|!B)"
, mkLaw "not_or_distrib" "!(A|B)" "(!A&!B)"
, mkLaw "implies_or" "(A->B)" "(!A|B)"
, mkLaw "implies_and" "(A->B)" "!(A&!B)"
, mkLaw "or_contr_eq" "A" "(A|(B&!B))"
, mkLaw "and_or_cancel" "A" "(A&(A|B))"
, mkLaw "or_and_cancel" "A" "(A|(A&B))"
, mkLaw "iff_and" "(A<->B)" "((A->B)&(B->A))"
, mkLaw "iff_or" "(A<->B)" "((A&B)|(!A&!B))"
]
{-
@ -219,7 +224,7 @@ data LawsGraphEdge = LawsGraphEdge
{ lgeLaw :: Law
, lgeReverse :: Bool
, lgeIndex :: Integer
}
} deriving Eq
instance Show LawsGraphEdge where
show edge =
@ -231,14 +236,15 @@ instance Show LawsGraphEdge where
<> "}"
bfsLaws :: Statement -> Statement -> Maybe [LawsGraphEdge]
bfsLaws goal start = bfs goal start getLawsGraphEdges
bfsLaws = bfs getLawsGraphEdges
getLawsGraphEdges :: Statement -> [(LawsGraphEdge, Statement)]
getLawsGraphEdges :: Statement -> [(Statement, LawsGraphEdge)]
getLawsGraphEdges s = concat $ rights $ map aux laws
-- ^ `rights` here because we can't apply
-- e.g. or_contr_eq forwards without inventing B
-- and the `Left` case is `Left IndeterminateReplace`
where
aux :: Law -> Either ReplaceError [(LawsGraphEdge, Statement)]
aux :: Law -> Either ReplaceError [(Statement, LawsGraphEdge)]
aux law = do
forward <- direction law lawLhs lawRhs False
reverse <- direction law lawRhs lawLhs True
@ -249,7 +255,7 @@ getLawsGraphEdges s = concat $ rights $ map aux laws
-> (Law -> Statement)
-> (Law -> Statement)
-> Bool
-> Either ReplaceError [(LawsGraphEdge, Statement)]
-> Either ReplaceError [(Statement, LawsGraphEdge)]
direction law mkPattern1 mkPattern2 isReverse = do
replaceds <- replace (mkPattern1 law) (mkPattern2 law) s
return $
@ -260,7 +266,7 @@ getLawsGraphEdges s = concat $ rights $ map aux laws
, lgeReverse = isReverse
, lgeIndex = index
}
in (edge, s')
in (s', edge)
{-
ghci> fromString x = fromRight undefined $ eof stmt $ mkInput x