Compare commits
No commits in common. "88c140fed5a113489eaa680309bbf36850131549" and "7f0afa76a6b04886b2abca9a42484d07f603ff72" have entirely different histories.
88c140fed5
...
7f0afa76a6
8 changed files with 15 additions and 38 deletions
|
@ -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 =
|
||||||
|
|
|
@ -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.
|
||||||
|
|
|
@ -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)
|
||||||
|
|
|
@ -9,7 +9,7 @@ data AlphaMIU
|
||||||
= M
|
= M
|
||||||
| I
|
| I
|
||||||
| U
|
| U
|
||||||
deriving Show
|
deriving (Eq, Show)
|
||||||
|
|
||||||
type StringMIU = [AlphaMIU]
|
type StringMIU = [AlphaMIU]
|
||||||
|
|
||||||
|
|
|
@ -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
|
||||||
|
|
|
@ -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
|
||||||
|
|
|
@ -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
|
||||||
-}
|
-}
|
||||||
|
|
|
@ -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
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue