1.1 --- a/sml.py	Tue May 17 18:05:04 2011 +0200
     1.2 +++ b/sml.py	Tue May 17 18:32:19 2011 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4      formula1 = Imp([Eq([p, q]), r])
     1.5      formula2 = Not([Or([p, q])])
     1.6      formula3 = Not([Not([p])])
     1.7 -    formula =  formula1 # choose your formula here
     1.8 +    formula = formula1 # choose your formula here
     1.9  
    1.10      args = parse_arguments()
    1.11      if (args.formula):
    1.12 @@ -26,9 +26,10 @@
    1.13          tree = SyntaxTree(out, tree_nodes) 
    1.14          formula = tree.root
    1.15     
    1.16 -    print "formula: \t\t", formula
    1.17 -    print "expanded -> and <->: \t", expand_imp_eq(formula)
    1.18 -    print "reduced ~: \t\t", reduce_not(expand_imp_eq(formula))
    1.19 +    print "formula: \t\t\t", formula
    1.20 +    print "expanded -> and <->: \t\t", expand_imp_eq(formula)
    1.21 +    print "reduced ~: \t\t\t", de_morgan(expand_imp_eq(formula))
    1.22 +    print "reduced iterated modalities: \t", reduce_iter(de_morgan(expand_imp_eq(formula)))
    1.23  
    1.24  def expand_imp_eq(formula):  
    1.25      map = {IMP: lambda (a, b): Or([Not([a]), b]),
    1.26 @@ -40,21 +41,35 @@
    1.27          return formula
    1.28      return map[formula.id](values())   
    1.29  
    1.30 -def reduce_not(formula):  
    1.31 +def de_morgan(formula):  
    1.32      negmap = {AND: lambda (a, b): Or([negate(a), negate(b)]),
    1.33                OR: lambda (a, b): And([negate(a), negate(b)]),
    1.34 +              BOX: lambda (a,): Diamond([negate(a)]),
    1.35 +              DIAMOND: lambda (a,): Box([negate(a)]),
    1.36                VARIABLE: lambda (a,): Not([a]),
    1.37                NOT: lambda (a,): a}
    1.38      def values():
    1.39 -        return [reduce_not(v) for v in formula.values]
    1.40 +        return [de_morgan(v) for v in formula.values]
    1.41      def negate(f):
    1.42           return negmap[f.id](f.values)
    1.43  
    1.44      if not isinstance(formula, Operator):
    1.45 -        return formula   
    1.46 +        return formula  
    1.47      if formula.id == NOT:
    1.48          return negate(formula.values[0])
    1.49      return formula.__class__(values())
    1.50 +
    1.51 +def reduce_iter(formula):  
    1.52 +    redset = set(((BOX, BOX), (DIAMOND, DIAMOND), (DIAMOND, BOX), (BOX, DIAMOND)))
    1.53 +    def values():
    1.54 +        return [reduce_iter(v) for v in formula.values]
    1.55 +
    1.56 +    if not isinstance(formula, Operator) or not isinstance(formula.values[0], Operator):
    1.57 +        return formula
    1.58 +    ids = (formula.id, formula.values[0].id)
    1.59 +    if ids in redset:
    1.60 +        return reduce_iter(formula.values[0])
    1.61 +    return formula.__class__(values())
    1.62   
    1.63  NOT = "~"
    1.64  AND = "&"