1.1 --- a/sml.py	Tue May 17 18:32:19 2011 +0200
     1.2 +++ b/sml.py	Tue May 17 19:11:34 2011 +0200
     1.3 @@ -30,16 +30,17 @@
     1.4      print "expanded -> and <->: \t\t", expand_imp_eq(formula)
     1.5      print "reduced ~: \t\t\t", de_morgan(expand_imp_eq(formula))
     1.6      print "reduced iterated modalities: \t", reduce_iter(de_morgan(expand_imp_eq(formula)))
     1.7 +    print "distributed modalities+: \t", reduce_iter(dist(reduce_iter(de_morgan(expand_imp_eq(formula)))))
     1.8 +
     1.9 +def values(fun, f):  
    1.10 +    return [fun(v) for v in f.values] 
    1.11  
    1.12  def expand_imp_eq(formula):  
    1.13      map = {IMP: lambda (a, b): Or([Not([a]), b]),
    1.14 -           EQ: lambda (a, b): And([Or([Not([a]), b]), Or([a, Not([b])])])}
    1.15 -    def values():       
    1.16 -        return [expand_imp_eq(v) for v in formula.values] 
    1.17 -
    1.18 +           EQ: lambda (a, b): And([Or([Not([a]), b]), Or([a, Not([b])])])}   
    1.19      if not isinstance(formula, Operator) or formula.id not in map:       
    1.20          return formula
    1.21 -    return map[formula.id](values())   
    1.22 +    return map[formula.id](values(expand_imp_eq, formula))   
    1.23  
    1.24  def de_morgan(formula):  
    1.25      negmap = {AND: lambda (a, b): Or([negate(a), negate(b)]),
    1.26 @@ -47,29 +48,37 @@
    1.27                BOX: lambda (a,): Diamond([negate(a)]),
    1.28                DIAMOND: lambda (a,): Box([negate(a)]),
    1.29                VARIABLE: lambda (a,): Not([a]),
    1.30 -              NOT: lambda (a,): a}
    1.31 -    def values():
    1.32 -        return [de_morgan(v) for v in formula.values]
    1.33 +              NOT: lambda (a,): a}    
    1.34      def negate(f):
    1.35           return negmap[f.id](f.values)
    1.36 -
    1.37      if not isinstance(formula, Operator):
    1.38          return formula  
    1.39      if formula.id == NOT:
    1.40          return negate(formula.values[0])
    1.41 -    return formula.__class__(values())
    1.42 +    return formula.__class__(values(de_morgan, formula))
    1.43  
    1.44  def reduce_iter(formula):  
    1.45      redset = set(((BOX, BOX), (DIAMOND, DIAMOND), (DIAMOND, BOX), (BOX, DIAMOND)))
    1.46 -    def values():
    1.47 -        return [reduce_iter(v) for v in formula.values]
    1.48 -
    1.49      if not isinstance(formula, Operator) or not isinstance(formula.values[0], Operator):
    1.50          return formula
    1.51      ids = (formula.id, formula.values[0].id)
    1.52      if ids in redset:
    1.53          return reduce_iter(formula.values[0])
    1.54 -    return formula.__class__(values())
    1.55 +    return formula.__class__(values(reduce_iter, formula))
    1.56 +
    1.57 +def dist(formula):    
    1.58 +    distmap = {(BOX, AND): lambda (a, b): And([Box([a]), Box([b])]),
    1.59 +               (DIAMOND, OR): lambda (a, b): Or([Diamond([a]), Diamond([b])]),
    1.60 +               (BOX, OR): lambda (a, b): (isinstance(a, Box) or isinstance(b, Box))               
    1.61 +               and Or([Box([a]), Box([b])]) or Box([Or([a, b])]),
    1.62 +               (DIAMOND, AND): lambda (a, b): (isinstance(a, Diamond) or isinstance(b, Diamond))
    1.63 +               and And([Diamond([a]), Diamond([b])]) or Diamond([And([a, b])])}   
    1.64 +    if not isinstance(formula, Operator) or not isinstance(formula.values[0], Operator):
    1.65 +        return formula
    1.66 +    ids = (formula.id, formula.values[0].id)
    1.67 +    if ids in distmap:
    1.68 +        return distmap[ids](formula.values[0].values)
    1.69 +    return formula.__class__(values(dist, formula))        
    1.70   
    1.71  NOT = "~"
    1.72  AND = "&"
    1.73 @@ -310,7 +319,7 @@
    1.74      parser.add_argument("-f", "--formula", help="your formula") 
    1.75      return parser.parse_args()
    1.76   
    1.77 -EXCUSE = """The formula was not accepted by the parser, because the parser doesn't like you or the rest of the world. It seems to have some real issues with formulae with inner nesting and generally suffers from its hasty implementation. The parser would like to thank you for your coorporation by providing the formula within the code file itself. Thank you."""
    1.78 +EXCUSE = """The formula was not accepted by me, because I don't like you and the rest of the world. I seem to have some issues with formulae with inner nesting and I generally suffer from my hasty implementation. I would like to thank you for your coorporation by providing the formula within the code file itself. Thank you. ~The Parser"""
    1.79  
    1.80  if __name__ == "__main__":
    1.81      main()