#!/usr/bin/env nix-script
#!>haskell
#! haskell | regex-compat random

{- GEB exercise -}

import Text.Regex
import Text.Printf
import System.Random

type Theorem = String
type Rule    = String

choice :: [a] -> IO a
choice xs = (xs !!) <$> randomRIO (0, length xs - 1) 

step :: (Rule, Theorem) -> String
step = uncurry $ printf " -%s-> %s"

derive :: Theorem -> IO [(Rule, Theorem)]
derive "M"  = return []
derive "MU" = return []
derive t = do
  (rule, name) <- choice rules
  let next = rule t
  if rule t /= t
    then ((name, next) :) <$> derive next
    else derive t

axiom = "MI"

transforms =
  [ ("I$",    "IU")
  , ("M(.?)", "M\\1\\1")
  , ("III",   "U")
  , ("UU",    "") ]

rules = zip (map make transforms) ["I", "II", "III", "IV"] where
  make (a, b) = flip (subRegex $ mkRegex a) b

main = do
  proof <- concatMap step <$> derive axiom
  putStrLn $ axiom ++ proof