miu-trace.hs

{-# 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]))