module Logic.Language.Impl.MIU where

import Logic.Language (Language(..))
import Logic.Language.Derivation (Derivation(..))

-- The MIU system
-- (from "Gödel, Escher, Bach: An Eternal Golden Braid" by Douglas Hofstadter)
data AlphaMIU
  = M
  | I
  | U
  deriving Show

type StringMIU = [AlphaMIU]

instance Language AlphaMIU where
  isWellFormed (M:_) = True
  isWellFormed _ = False

  axiom0 = [[M, I]]
  infer1 =
    [ miuRule1
    , miuRule2
    , miuRule3
    , miuRule4
    ]

-- RULE I: If you possess a string whose last letter is I, you can add on a U at the end.
miuRule1 :: StringMIU -> [StringMIU]
miuRule1 [I] = [[I, U]]
miuRule1 (x:xs) = (x:) <$> miuRule1 xs
miuRule1 _ = []

-- RULE II: Suppose you have Mx. Then you may add Mxx to your collection.
miuRule2 :: StringMIU -> [StringMIU]
miuRule2 string@(M:xs) = [string ++ xs]
miuRule2 _ = []

-- RULE III: If III occurs in one of the strings in your collection, you may
-- make a new string with U in place of III.
miuRule3 :: StringMIU -> [StringMIU]
miuRule3 string@(M:xs) = (M:) <$> aux xs
  where
    aux (x@I:xs@(I:I:xs')) = (U:xs'):((x:) <$> aux xs)
    aux (x:xs) = (x:) <$> aux xs
    aux _  = []
miuRule3 _ = []

-- RULE IV: If UU occurs inside one of your strings, you can drop it.
miuRule4 :: StringMIU -> [StringMIU]
miuRule4 string@(M:xs) = (M:) <$> aux xs
  where
    aux (x@U:xs@(U:xs')) = xs':((x:) <$> aux xs)
    aux (x:xs) = (x:) <$> aux xs
    aux _ = []
miuRule4 _ = []

{-
ghci> import Logic.Language (ConcatShowList(..))
ghci> map ConcatShowList infer0 :: [ConcatShowList AlphaMIU]
[MI]
ghci> map ConcatShowList $ concat $ map ($ [M, I, I, I, I, U, U, I]) infer1
[MIIIIUUIU,MIIIIUUIIIIIUUI,MUIUUI,MIUUUI,MIIIII]
-}

deriveMIIUII :: Derivation AlphaMIU
deriveMIIUII =
  Infer1 3 0 $
  Infer1 2 2 $
  Infer1 0 0 $
  Infer1 3 0 $
  Infer1 3 0 $
  Infer1 2 2 $
  Infer1 1 0 $
  Infer1 2 5 $
  Infer1 0 0 $
  Infer1 1 0 $
  Infer1 1 0 $
  Infer1 1 0 $
  Axiom0 0

{-
ghci> import Logic.Language.Derivation (resolveDerivation)
ghci> ConcatShowList <$> resolveDerivation deriveMIIUII
Right MIIUII
-}