Compare commits

...

2 commits

Author SHA1 Message Date
hi
88c140fed5 tidy: del unused Eq, add custom Show 2025-08-12 13:29:08 +00:00
hi
56a8dd2b30 bfs: use a Set for visited nodes 2025-08-12 13:28:23 +00:00
8 changed files with 38 additions and 15 deletions

View file

@ -1,7 +1,9 @@
module Logic.Graph where module Logic.Graph where
bfs :: Eq a => a -> a -> (a -> [(edge, a)]) -> Maybe [edge] import Data.Set (Set, insert)
bfs goal start getEdges = reverse <$> aux [([], start)] []
bfs :: (Eq a, Ord a) => a -> a -> (a -> [(edge, a)]) -> Maybe [edge]
bfs goal start getEdges = reverse <$> aux [([], start)] mempty
where where
aux [] _ = Nothing aux [] _ = Nothing
aux ((path, vertex):queue) visited aux ((path, vertex):queue) visited
@ -12,7 +14,7 @@ bfs goal start getEdges = reverse <$> aux [([], start)] []
case filter (\(_, v) -> v == goal) new of case filter (\(_, v) -> v == goal) new of
[] -> [] ->
let queue' = queue ++ map (\(edge, next) -> (edge:path, next)) new let queue' = queue ++ map (\(edge, next) -> (edge:path, next)) new
in aux queue' (vertex:visited) in aux queue' $ insert vertex visited
((edge, _):_) -> Just (edge:path) ((edge, _):_) -> Just (edge:path)
getUnvisitedAdjacent vertex visited = getUnvisitedAdjacent vertex visited =

View file

@ -7,7 +7,7 @@ instance Show a => Show (ConcatShowList a) where
-- Formal language (/grammar/production system/whatever) -- Formal language (/grammar/production system/whatever)
-- https://en.wikipedia.org/wiki/Post_canonical_system -- https://en.wikipedia.org/wiki/Post_canonical_system
class (Eq symbol, Show symbol) => Language symbol where class Show symbol => Language symbol where
isWellFormed :: [symbol] -> Bool isWellFormed :: [symbol] -> Bool
-- If Haskell had dependent types these could be generalized. -- If Haskell had dependent types these could be generalized.

View file

@ -10,7 +10,7 @@ data Derivation symbol
| Axiom3 Integer [symbol] [symbol] [symbol] | Axiom3 Integer [symbol] [symbol] [symbol]
| Infer1 Integer Integer (Derivation symbol) | Infer1 Integer Integer (Derivation symbol)
| Infer2 Integer Integer (Derivation symbol) (Derivation symbol) | Infer2 Integer Integer (Derivation symbol) (Derivation symbol)
deriving (Eq, Show) deriving Show
data DerivationError s data DerivationError s
= SelectIndexError (DerivationSelectIndexError s) = SelectIndexError (DerivationSelectIndexError s)

View file

@ -9,7 +9,7 @@ data AlphaMIU
= M = M
| I | I
| U | U
deriving (Eq, Show) deriving Show
type StringMIU = [AlphaMIU] type StringMIU = [AlphaMIU]

View file

@ -10,7 +10,7 @@ newtype Parser symbol output = Parser
data Input symbol = Input data Input symbol = Input
{ inputPos :: Int { inputPos :: Int
, inputSeq :: [symbol] , inputSeq :: [symbol]
} deriving (Eq, Show) } deriving Show
mkInput :: [symbol] -> Input symbol mkInput :: [symbol] -> Input symbol
mkInput = Input 0 mkInput = Input 0

View file

@ -9,7 +9,7 @@ data Statement
| Or Statement Statement | Or Statement Statement
| Implies Statement Statement | Implies Statement Statement
| Iff Statement Statement | Iff Statement Statement
deriving (Show, Eq) deriving (Eq, Ord, Show)
atoms :: Statement -> [String] atoms :: Statement -> [String]
atoms = toAscList . mkSet atoms = toAscList . mkSet

View file

@ -3,6 +3,7 @@ module Logic.Statement.Laws where
import Logic.Parse (eof, mkInput) import Logic.Parse (eof, mkInput)
import Logic.Statement (Statement(..)) import Logic.Statement (Statement(..))
import Logic.Statement.Parse (stmt) import Logic.Statement.Parse (stmt)
import Logic.Statement.Serialize (serialize, SerializeFormat(Plain))
import Logic.Graph (bfs) import Logic.Graph (bfs)
import Data.Either (fromRight, rights) import Data.Either (fromRight, rights)
@ -12,7 +13,17 @@ data Law = Law
{ lawName :: String { lawName :: String
, lawLhs :: Statement , lawLhs :: Statement
, lawRhs :: Statement , lawRhs :: Statement
} deriving (Eq, Show) }
instance Show Law where
show law =
"Law{"
<> lawName law
<> ": "
<> serialize Plain (lawLhs law)
<> " <=> "
<> serialize Plain (lawRhs law)
<> "}"
mkLaw :: String -> String -> String -> Law mkLaw :: String -> String -> String -> Law
mkLaw name lhs rhs = Law name (fromString lhs) (fromString rhs) mkLaw name lhs rhs = Law name (fromString lhs) (fromString rhs)
@ -208,7 +219,16 @@ data LawsGraphEdge = LawsGraphEdge
{ lgeLaw :: Law { lgeLaw :: Law
, lgeReverse :: Bool , lgeReverse :: Bool
, lgeIndex :: Integer , lgeIndex :: Integer
} deriving (Eq, Show) }
instance Show LawsGraphEdge where
show edge =
"LawsGraphEdge{"
<> (if lgeReverse edge then "< " else "> ")
<> lawName (lgeLaw edge)
<> " "
<> show (lgeIndex edge)
<> "}"
bfsLaws :: Statement -> Statement -> Maybe [LawsGraphEdge] bfsLaws :: Statement -> Statement -> Maybe [LawsGraphEdge]
bfsLaws goal start = bfs goal start getLawsGraphEdges bfsLaws goal start = bfs goal start getLawsGraphEdges
@ -284,6 +304,7 @@ Just ["> dbl_neg 0","> dbl_neg 0","> dbl_neg 0","> dbl_neg 0"]
ghci> time $ putStrLn $ show $ niceEdges <$> bfsLaws (fromString "!!!!!!!!!!p") (fromString "p") ghci> time $ putStrLn $ show $ niceEdges <$> bfsLaws (fromString "!!!!!!!!!!p") (fromString "p")
Just ["> dbl_neg 0","> dbl_neg 0","> dbl_neg 0","> dbl_neg 0","> dbl_neg 0"] Just ["> dbl_neg 0","> dbl_neg 0","> dbl_neg 0","> dbl_neg 0","> dbl_neg 0"]
3.244101767s 3.244101767s
ghci> time $ putStrLn $ show $ niceEdges <$> bfsLaws (fromString "!!!!!!!!!!!!p") (fromString "p")
Just ["> dbl_neg 0","> dbl_neg 0","> dbl_neg 0","> dbl_neg 0","> dbl_neg 0","> dbl_neg 0"] Just ["> dbl_neg 0","> dbl_neg 0","> dbl_neg 0","> dbl_neg 0","> dbl_neg 0","> dbl_neg 0"]
3066.211460539s 3066.211460539s
-} -}

View file

@ -10,28 +10,28 @@ data TokenString = TokenString
{ tsCanEval :: CanEval { tsCanEval :: CanEval
, tsLevel :: Int , tsLevel :: Int
, tsString :: String , tsString :: String
} deriving (Show, Eq) } deriving Show
data CanEval data CanEval
= Filler = Filler
| CanEval | CanEval
deriving (Show, Eq) deriving Show
data TokenValue = TokenValue data TokenValue = TokenValue
{ tvLevel :: Int { tvLevel :: Int
, tvValue :: Value , tvValue :: Value
} deriving (Show, Eq) } deriving Show
data Value data Value
= NoValue = NoValue
| Value Bool | Value Bool
deriving (Show, Eq) deriving Show
data SerializeFormat data SerializeFormat
= Plain = Plain
| Latex | Latex
-- | PrefixPlain -- | PrefixPlain
deriving (Show, Eq) deriving Show
serialize :: SerializeFormat -> Statement -> String serialize :: SerializeFormat -> Statement -> String
serialize fmt s = concat $ map tsString $ serializeStrings fmt s serialize fmt s = concat $ map tsString $ serializeStrings fmt s