Created
April 21, 2020 16:30
-
-
Save scravy/fa263aa3a49ad25360c53860c870af1b to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE Haskell2010, LambdaCase, TupleSections #-} | |
import Data.List (nub) | |
data Symbol = M | I | U deriving (Eq, Show) | |
data Rule = Mx | III | UU | IU deriving (Eq, Show, Enum) | |
data Deduction = Axiom [Symbol] | Deduction [Symbol] Rule [Symbol] | |
instance Show Deduction where | |
show = \case | |
Deduction f r b -> map (head . show) f ++ " ~~" ++ show r ++ "~> " ++ map (head . show) b | |
Axiom xs -> "Axiom: " ++ map (head . show) xs | |
instance Eq Deduction where a == b = toList a == toList b | |
toList = \case | |
Deduction _ _ xs -> xs | |
Axiom xs -> xs | |
smap f (Deduction from rule to) = Deduction (f from) rule (f to) | |
apply word = map (uncurry (Deduction word)) $ case word of | |
M : xs -> [ (Mx,) $ M : xs ++ xs ] | |
I : I : I : xs -> [ (III,) $ U : xs ] | |
U : U : xs -> [ (UU,) $ xs ] | |
I : [] -> [ (IU,) $ I : U : [] ] | |
xs -> [] | |
applyAll = \case | |
[] -> [] | |
ss@(s : rs) -> apply ss ++ map (smap (s :)) (applyAll rs) | |
nextGen (gen, curGen, start) = (succ gen, oldGen, noDupes (start >>= (applyAll . toList))) | |
where | |
noDupes = nub . filter (not . flip elem oldGen) | |
oldGen = start ++ curGen | |
enumerateAll start = concatMap (\(a,_,c) -> map (a,) c) (iterate nextGen (0, [], [start])) | |
main = mapM_ print (enumerateAll (Axiom [M, I])) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment