#!/usr/bin/env python2.7

"""
miu.py 0.1

Usage: miu.py [initial-words] [-g goal]

Play the MIU-game from Hofstaedter's Goedel, Escher, Bach. This is a
simple string substitution game, applying the rules below to a set of
starting words (originally "MI"), trying to derive a particular goal
(orginally, MU).

xI    -> xIU
xIIIy -> xUy
xUUy  -> xy
Mx    -> Mxx


Options:

-h Print this help.
-g Give the goal to derive

Copyright 2014 Stephan Schulz, schulz@eprover.org

This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program ; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston,
MA  02111-1307 USA 

The original copyright holder can be contacted as

Stephan Schulz
DHBW Stuttgart
Informatik
Postfach 10 05 63
D-70004 Stuttgart
Germany
schulz@eprover.org.
"""

import sys
import getopt

goal = "MU"
"""
If this word is derived, stop. Since MU is not derivable, the default
is to go on deriving words forever.
"""

words = ["MI"]
"""
Default is to play the version from the book.
"""

def rule1(word):
    if word[-1] == "I":
        return [word+"U"]
    return []

def rule2(word):
    result = []
    for i in range(len(word)-2):
        if word[i:i+3] == "III":
            new = word[:i]+"U"+word[i+3:]
            result.append(new)
    return result
    
def rule3(word):
    result = []
    for i in range(len(word)-1):
        if word[i:i+2] == "UU":
            new = word[:i]+word[i+2:]
            result.append(new)
    return result

def rule4(word):
    if word[0] == "M":
        return [word+word[1:]]
    return []

def popShortest(words):
    if words:
        result = words[0]
        minl   = len(result)
        for word in words[1:]:
            if len(word) < minl:
                result = word
                minl = len(result)
        words.remove(result)
        return result
    return None

def derivation(known, word):
    deriv = []
    while known[word]:
        word = known[word]
        deriv.append(word)
    return deriv

if __name__ == '__main__':
    opts, args = getopt.gnu_getopt(sys.argv[1:], "hg:", ["help", "goal="])

    for option, optarg in opts:
        if option == "-h" or option == "--help":
            print __doc__
            sys.exit()
        elif option == "-g" or option == "--goal":
            goal = optarg
            sys.exit()
        else:
            sys.exit("Unknown option "+ option)

    if args:
        words = args


known = {}
for word  in words:
    known[word] = False

print known

while words:
    # print words
    # given = popShortest(words)
    given = words.pop(0)
    print given
    d = derivation(known, given)
    if len(given) <= 6:
        print given, d
    
    
    if given == goal:
        print "Success"
        sys.exit()
    for rule in [rule1, rule2, rule3, rule4]:
        new = rule(given)
        for word in new:
            if not word in known:
                words.append(word)
                known[word] = given