44 lines
881 B
Haskell
44 lines
881 B
Haskell
|
#!/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
|