require "python-semantics-ops.k"

module PYTHON-SEMANTICS-BOOLEAN-OPS
  imports PYTHON-SEMANTICS-OPS

  syntax ObjRef ::= bool(K) [strict]
                  | coerceBoolean(Exp, Exp, Exp, Exp, String) [strict(1, 2)]
                  | len(Exp) [strict]
                  | checkBool(Exp) [strict]
                  | checkInt(Exp) [strict]
                  | checkLen(Exp) [strict]
                  | contains(K, Exp) [strict]
                  | index(Exp) [strict]

  rule bool(true) => ref("True")
  rule bool(false) => ref("False")
  rule bool(O:Object) => test(plbool(O is ref("None")), ref("False"), checkBool(getmember(O, "__bool__", true, false, false) (.Arguments)) -> checkInt(len(O)) -> ref("True")) 
  rule checkBool(O:Object) => test(istype(O, ref("bool")), O, raiseInternal("TypeError", "__bool__ should return bool"))
  rule checkBool(.Obj) => .Obj
  rule checkInt(O:Object) => test(intvalue(O) ==Int 0, ref("False"), ref("True"))
  rule checkInt(.Obj) => .Obj
  rule invokeBuiltin(obj("bool.__new__",_), ListItem(O), .) => newHelper(O, ref("bool"), .) ~> ref("False")
  rule invokeBuiltin(obj("bool.__new__",_), ListItem(O:Object) ListItem(O2:Object), .) => newHelper(O, ref("bool"), .) ~> bool(O2)
  rule invokeBuiltin(obj("bool.__str__",_), ListItem(O:Object), .) => if O: "True" else: "False"

  rule len(O) => checkLen(index(getmember(O, "__len__", true, false, false) (.Arguments)))
  rule checkLen(O:Object) => test(intvalue(O) >=Int 0, O, raiseInternal("ValueError", "__len__() should return >= 0"))
  rule checkLen(.Obj) => .Obj
  rule invokeBuiltin(obj("len",_), ListItem(O), .) => len(O) -> raiseInternal("TypeError", "object has no len()")

  syntax Test ::= plbool(Exp) [strict]
  rule plbool(obj(_, <oattrs>... "__value__" |-> I:Int ...</oattrs>)) => I =/=Int 0 

  rule not O:Object => bool(negate(plbool(bool(O))))
  rule O:Object and K:K => test(plbool(bool(O)), K, O)
  rule O:Object or K => test(plbool(bool(O)), O, K)

  syntax Exp ::= comparison(Exp, Exp, KLabel) [strict(1)]

  rule A ::Exp is B ::Exp => comparison(A, B, '_is_) [macro]
  rule A ::Exp is not B ::Exp => comparison(A, B, '_isnot_) [macro]
  rule A ::Exp < B ::Exp => comparison(A, B, '_<_) [macro]
  rule A ::Exp > B ::Exp => comparison(A, B, '_>_) [macro]
  rule A ::Exp <= B ::Exp => comparison(A, B, '_<=_) [macro]
  rule A ::Exp >= B ::Exp => comparison(A, B, '_>=_) [macro]
  rule A ::Exp != B ::Exp => comparison(A, B, '_!=_) [macro]
  rule A ::Exp == B ::Exp => comparison(A, B, '_==_) [macro]
  rule A ::Exp in B ::Exp => comparison(A, B, '_in_) [macro]
  rule A ::Exp not in B ::Exp => comparison(A, B, '_notin_) [macro]

  rule 'Compare(O:Object) => O

  context comparison(O:Object, HOLE, _) when getKLabel HOLE =/=KLabel 'comparison
  context comparison(O:Object, comparison(HOLE, _, _), _)
  rule comparison(O:Object, comparison(O2:Object, Rest, Lbl2), Lbl) => comparison(O, O2, Lbl) and comparison(O2, Rest, Lbl2)

  rule comparison(obj(B:ObjId,_), obj(B2:ObjId,_), '_is_) => bool(B ==K B2)
  rule comparison(O:Object, O2:Object, '_isnot_) => not (O is O2)
  rule comparison(O:Object, O2:Object, '_<_) => coerceBoolean(O, O2, "__lt__", "__gt__", "<")
  rule comparison(O:Object, O2:Object, '_>_) => coerceBoolean(O, O2, "__gt__", "__lt__", ">")
  rule comparison(O:Object, O2:Object, '_<=_) => coerceBoolean(O, O2, "__le__", "__ge__", "<=")
  rule comparison(O:Object, O2:Object, '_>=_) => coerceBoolean(O, O2, "__ge__", "__le__", ">=")
  rule comparison(O:Object, O2:Object, '_!=_) => coerceBinaryBase(O, O2, "__ne__", "__ne__") -> (not (O == O2))
  rule comparison(O:Object, O2:Object, '_==_) => coerceBinaryBase(O, O2, "__eq__", "__eq__") -> (O is O2)
  rule comparison(O:Object, O2:Object, '_in_) => bool((getmember(O2, "__contains__", true, false, false) (O)) -> contains(iterate(O2, .), O))
  rule comparison(O:Object, O2:Object, '_notin_) => not O in O2

  rule contains(list(ListItem(O:Object) L:List), O2) => ref("True") if O == O2 else contains(list(L), O2)
  context contains(list(ListItem(HOLE) _), _)
  rule contains(list(.), O2) => ref("False")

  rule <k> coerceBoolean(O, O2, X, RX, S:String) => coerceBinaryBase(O, O2, X, RX) -> (raiseInternal("TypeError", "unorderable types: " +String S)) ...</k>

endmodule