minor: substatements function, comments

This commit is contained in:
hi 2025-08-12 03:57:13 +00:00
parent 0d13b807f0
commit d0ba6ce9d4
2 changed files with 20 additions and 5 deletions

View file

@ -41,6 +41,12 @@ laws =
, mkLaw "iff_or" "(A<->B)" "((A&B)|(!A&!B))"
]
{-
ghci> import Logic.Statement.Eval (bucket, Bucket(Tautology))
ghci> all (== Tautology) $ map (\law -> bucket $ Iff (lawLhs law) (lawRhs law)) laws
True
-}
lookupLaw :: String -> Maybe Law
lookupLaw name = listToMaybe $ filter (\law -> lawName law == name) laws
@ -48,7 +54,7 @@ match
:: Statement
-- ^ pattern
-> Statement
-- ^ statement to search
-- ^ statement to search within
-> Maybe [(String, Statement)]
-- ^ mapping from pattern-statement atoms to search-statement parts
match = aux []
@ -104,19 +110,20 @@ Just [("C",Atom "r"),("B",Atom "q"),("A",Atom "p")]
-}
data SwapError
= Indeterminate
= IndeterminateSwap
-- ^ An atom in p2 doesn't exist in p1.
-- Strictly: an atom in p2 doesn't exist in the result from `match`
-- (matters only if `match` is implemented incorrectly).
-- If for atoms we used terms of a type instead of strings,
-- we could avoid needing this error.
-- Theoretically if for atoms we used terms of a type instead of strings, we
-- could avoid needing this error, but I think we still wouldn't be able
-- to return a mapping from atom-type-1 to atom-type-2 in a type safe way.
| NonMatchingPattern
deriving Show
swap :: Statement -> Statement -> Statement -> Either SwapError Statement
swap p1 p2 s = do
mapping <- maybe (Left NonMatchingPattern) Right $ match p1 s
maybe (Left Indeterminate) Right $ aux mapping p2
maybe (Left IndeterminateSwap) Right $ aux mapping p2
where
aux :: [(String, Statement)] -> Statement -> Maybe Statement
aux mapping (Atom key) = lookup key mapping