Compare commits

..

No commits in common. "88c140fed5a113489eaa680309bbf36850131549" and "7f0afa76a6b04886b2abca9a42484d07f603ff72" have entirely different histories.

8 changed files with 15 additions and 38 deletions

View file

@ -1,9 +1,7 @@
module Logic.Graph where module Logic.Graph where
import Data.Set (Set, insert) bfs :: Eq a => a -> a -> (a -> [(edge, a)]) -> Maybe [edge]
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
@ -14,7 +12,7 @@ bfs goal start getEdges = reverse <$> aux [([], start)] mempty
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' $ insert vertex visited in aux queue' (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 Show symbol => Language symbol where class (Eq symbol, 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 Show deriving (Eq, 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 Show deriving (Eq, 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 Show } deriving (Eq, 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 (Eq, Ord, Show) deriving (Show, Eq)
atoms :: Statement -> [String] atoms :: Statement -> [String]
atoms = toAscList . mkSet atoms = toAscList . mkSet

View file

@ -3,7 +3,6 @@ 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)
@ -13,17 +12,7 @@ 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)
@ -219,16 +208,7 @@ 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
@ -304,7 +284,6 @@ 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 } deriving (Show, Eq)
data CanEval data CanEval
= Filler = Filler
| CanEval | CanEval
deriving Show deriving (Show, Eq)
data TokenValue = TokenValue data TokenValue = TokenValue
{ tvLevel :: Int { tvLevel :: Int
, tvValue :: Value , tvValue :: Value
} deriving Show } deriving (Show, Eq)
data Value data Value
= NoValue = NoValue
| Value Bool | Value Bool
deriving Show deriving (Show, Eq)
data SerializeFormat data SerializeFormat
= Plain = Plain
| Latex | Latex
-- | PrefixPlain -- | PrefixPlain
deriving Show deriving (Show, Eq)
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