import pyparsing as pyp
import json
from xml.dom import minidom
from copy import deepcopy

from dds.expr import Expr, Num, Var, Charstr, Cmp, BinOp, UnCon, BinCon, \
  PropVar, Visitor
from dds.read import parse_prop_atom
from dds.util import VarType

pyp.ParserElement.enablePackrat()

def mk_bin(ts):
  items = ts[0][1:]
  expr = ts[0][0]
  while len(items) > 0:
    expr = BinCon(expr, items[0], items[1])
    items = items[2:]
  return expr

def mkPropVar(name, vars, state_names):
  if (name in vars and vars[name] == VarType.bool) or name in state_names:
    return PropVar(name)
  else:
    raise NameError(name + " is neither propositional variable nor state name")

class Property:
 
  def __str__(self):
    return str(self._property)

  def get_constraints(self):
    def constraints_in_formula(f):
      if isinstance(f, Cmp):
        return [f]
      elif isinstance(f, UnCon):
        return constraints_in_formula(f.arg)
      elif isinstance(f, BinCon):
        return constraints_in_formula(f.left) + constraints_in_formula(f.right)
      else:
        return []
    return constraints_in_formula(self._property)

class LTLProperty(Property):
  def __init__(self, prop, var_names = None, state_names = None):
    self._var_names = var_names
    self._state_names = state_names
    if isinstance(prop, Expr):
      self._property = prop
    else:
      try:
        self._property = self.parse(prop)
      except pyp.ParseException as err:
        print("parse error")
        self._property = None
  
  def vars(self):
    return self._property.vars()

  def parse(self, prop_str):
    pvnames = [ v for v in self._var_names if self._var_names[v] == VarType.bool ]
    patom = parse_prop_atom(self._var_names)

    LBRA = pyp.Literal('<').suppress()
    RBRA = pyp.Literal('>').suppress()
    propvar = pyp.oneOf(self._state_names + pvnames).\
      setParseAction(lambda toks: PropVar(toks[0]))
    actionvar = (pyp.Word(pyp.srange("[a-zA-Z0-9]"))).\
      setParseAction(lambda toks: PropVar(toks[0]))
    action = LBRA + actionvar + RBRA
    # next with action a is replaced using PropVar a below

    formula = pyp.Forward()
    formula << pyp.infixNotation(propvar | patom, [
          (pyp.oneOf("F G X"), 1, pyp.opAssoc.RIGHT, lambda ts: UnCon(ts[0][0], ts[0][1])),
          (action, 1, pyp.opAssoc.RIGHT, lambda ts: UnCon("X", BinCon(ts[0][0], "&&", ts[0][1]))),
          (pyp.oneOf("U"), 2, pyp.opAssoc.LEFT, lambda ts: BinCon(ts[0][0], ts[0][1], ts[0][2])),
          (pyp.oneOf("&& ||"), 2, pyp.opAssoc.LEFT, mk_bin),
      ])

    res = formula.parseString(prop_str)
    r = res[0] if len(res) > 0 else None
    return r

  def shift_to_lookback(self):
    # is destructive, modifies current object
    class BackShifter(Visitor):
      def __init__(self):
        pass
 
      def add_next(self, e):
        return UnCon("Xw", e)

      def visit_cmp(self, cmp):
        if all(not v.is_prime for v in cmp.vars()):
          return self.STOP_RECURSION
        else:
          return not self.STOP_RECURSION

      def visit_var(self, var):
        if var.is_prime:
          var.is_prime = False
        else:
          var.is_back = True
      
      def visit_bincon(self, e):
        left = deepcopy(e.left)
        right = deepcopy(e.right)
        # visit arguments explicitly and stop recursion below ...
        e.left.accept(self)
        e.right.accept(self)
        # ... in order to save results here:
        if isinstance(left, Cmp) and left != e.left: # was modified
          e.left = self.add_next(e.left)
        if isinstance(right, Cmp) and right != e.right:
          e.right = self.add_next(e.right)
        return self.STOP_RECURSION
      
      def visit_uncon(self, e):
        arg = deepcopy(e.arg)
        e.arg.accept(self)
        if isinstance(arg, Cmp) and arg != e.arg:
          e.arg = self.add_next(e.arg)
        return self.STOP_RECURSION
    
    varshifter = BackShifter()
    self._property.accept(varshifter)


class CTLStarProperty(Property):
  def __init__(self, prop_str, vars, state_names):
    self._vars = vars
    self._state_names = state_names
    try:
      self._property = self.parse(prop_str)
    except pyp.ParseException as err:
      self._property = None

  def parse(self, prop_str):
    pvnames = [ v for v in self._vars if self._vars[v] == VarType.bool ]
    patom = parse_prop_atom(self._vars)

    LBRA = pyp.Literal('<').suppress()
    RBRA = pyp.Literal('>').suppress()
    propvar = pyp.oneOf(self._state_names + pvnames).\
      setParseAction(lambda toks: PropVar(toks[0]))
    actionvar = (pyp.Word(pyp.srange("[a-zA-Z0-9]"))).\
      setParseAction(lambda toks: PropVar(toks[0]))
    action = LBRA + actionvar + RBRA
    # next with action a is replaced using PropVar a below

    pathformula = pyp.Forward()
    stateformula = pyp.Forward()
    pathformula << pyp.infixNotation(stateformula, [
          (pyp.oneOf("F G X"), 1, pyp.opAssoc.RIGHT, lambda ts: UnCon(ts[0][0], ts[0][1])),
          (action, 1, pyp.opAssoc.RIGHT, lambda ts: UnCon("X", BinCon(ts[0][0], "&&", ts[0][1]))),
          (pyp.oneOf("U"), 2, pyp.opAssoc.LEFT, lambda ts: BinCon(ts[0][0], ts[0][1], ts[0][2])),
          (pyp.oneOf("&& ||"), 2, pyp.opAssoc.LEFT, mk_bin),
      ])
    stateformula << pyp.infixNotation(propvar | patom |
          (pyp.oneOf("A E !") + pathformula).setParseAction(lambda toks: UnCon(toks[0], toks[1])), [
          (pyp.oneOf("&& ||"), 2, pyp.opAssoc.LEFT, mk_bin),
      ])
    res = stateformula.parseString(prop_str)
    r = res[0] if len(res) > 0 else None
    return r
