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
bfs :: Eq a => a -> a -> (a -> [(edge, a)]) -> Maybe [edge]
bfs goal start getEdges = reverse <$> aux [([], start)] []
import Data.Set (Set, insert)
bfs :: (Eq a, Ord a) => a -> a -> (a -> [(edge, a)]) -> Maybe [edge]
bfs goal start getEdges = reverse <$> aux [([], start)] mempty
where
aux [] _ = Nothing
aux ((path, vertex):queue) visited
@ -12,7 +14,7 @@ bfs goal start getEdges = reverse <$> aux [([], start)] []
case filter (\(_, v) -> v == goal) new of
[] ->
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)
getUnvisitedAdjacent vertex visited =

View file

@ -7,7 +7,7 @@ instance Show a => Show (ConcatShowList a) where
-- Formal language (/grammar/production system/whatever)
-- 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
-- If Haskell had dependent types these could be generalized.

View file

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

View file

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

View file

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

View file

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

View file

@ -3,6 +3,7 @@ module Logic.Statement.Laws where
import Logic.Parse (eof, mkInput)
import Logic.Statement (Statement(..))
import Logic.Statement.Parse (stmt)
import Logic.Statement.Serialize (serialize, SerializeFormat(Plain))
import Logic.Graph (bfs)
import Data.Either (fromRight, rights)
@ -12,7 +13,17 @@ data Law = Law
{ lawName :: String
, lawLhs :: 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 name lhs rhs = Law name (fromString lhs) (fromString rhs)
@ -208,7 +219,16 @@ data LawsGraphEdge = LawsGraphEdge
{ lgeLaw :: Law
, lgeReverse :: Bool
, 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 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")
Just ["> dbl_neg 0","> dbl_neg 0","> dbl_neg 0","> dbl_neg 0","> dbl_neg 0"]
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"]
3066.211460539s
-}

View file

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