require "python-semantics-boolean-ops.k"

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

  syntax ObjRef ::= "init" "(" Exp "," Exp "," List "," Map ")" [strict(1, 2)] 
                  | "mroMerge" "(" KList ")"
  syntax KList ::= "getMros" "(" List ")" [function]
  syntax Bool ::= "notInTail" "(" Object "," List ")" [function]
  syntax List ::= "trimHead" "(" List "," Object ")" [function] 

  rule <k> invokeBuiltin(obj("call_type",_), ListItem(Type:Object) L:List, M:Map) => init(doCall(Type . String2Id("__new__"), ListItem(Type) L, M), Type, L, M) ...</k>

  rule <k> init(O:Object, Type, L, M) => test(istype(O, Type), test(plbool(doCall(getmember(O, "__init__", true, false, false), L, M) is ref("None")), ref(id(O)), raiseInternal("TypeError", "__init__() should return None")), O) ...</k>
 
  // since object is the base class of absolutely everything, we need object.__new__ to fail if we
  // call it with any other builtin type.
  rule <k> invokeBuiltin(obj("new_object",_), ListItem(O:Object) _, _) => newHelper(O, ref("object"), Objects -Set SetItem("object")) ~> mutable(., O) ...</k>
       <builtinObjectsWithNewMethod> Objects:Set </builtinObjectsWithNewMethod>

  rule [init-object]: <k> invokeBuiltin(obj("init_object",_), _, _) => ref("None") ...</k>

  rule <k> invokeBuiltin(obj("eq_object",_), ListItem(O) ListItem(O2:Object), .) => test(plbool(O is O2), ref("True"), ref("NotImplemented")) ...</k>
  rule <k> invokeBuiltin(obj("ne_object",_), ListItem(O) ListItem(O2), .) => not (O == O2) ...</k>
 
  syntax Test ::= hasDuplicates(List) [function]
  rule hasDuplicates(ListItem(B) L:List) => true when B in Setify(L)
  rule hasDuplicates((ListItem(B) => .) L:List) when notBool B in Setify(L)
  rule hasDuplicates(.) => false

  rule [getMro]: getMro(O:Object, Bases:Object) => test(hasDuplicates(Idify(listvalue(Bases))), raiseInternal("TypeError", "duplicate base class object"), mroMerge(list(ListItem(list(ListItem(O)))),,getMros(listvalue(Bases)),,list(ListItem(list(listvalue(Bases))))))
  context mroMerge(_,,HOLE,,_)
  context mroMerge(_,,list(_ ListItem(HOLE) _),,_)
  context mroMerge(_,,list(_ ListItem(list(_ ListItem(HOLE) _)) _),,_)
  rule getMros(ListItem(B) L:List) => list(ListItem(getMro(B, getref2(B, "__bases__")))) ,, getMros(L)
  rule getMros(.List) => .KList
  rule mroMerge(((list(L:List),,list(L2:List)) => list(L L2)),,_) when all(L L2, isMroReady)
  rule (. => list(.) ~> 0) ~> mroMerge(list(L))
  rule list(_ (. => ListItem(B))) ~> (N:Int => 0) ~> mroMerge(list((L:List => trimHead(L, B)) ListItem(list((ListItem(B:Object) => .) _)) (L2:List => trimHead(L2, B)))) when lengthList L ==Int N andBool notInTail(B, L L2)
  rule notInTail(B, ListItem(list(ListItem(_) L)) L2) => notBool(B in Setify(L)) andBool notInTail(B, L2) 
  rule notInTail(B, .) => true 
  rule trimHead(ListItem(list(ListItem(B) L:List)) L2:List, B2) => ListItem(#if B ==K B2 #then list(L) #else list(ListItem(B) L) #fi) trimHead(L2, B2) 
  rule trimHead(., _) => . 
  rule list(_) ~> _ ~> mroMerge(list(_ (ListItem(list(.)) => .) _))
  rule list(_) ~> (N:Int => N +Int 1) ~> mroMerge(list(L:List ListItem(list(ListItem(B:Object) _)) L2:List)) when lengthList L ==Int N andBool notBool notInTail(B, L L2)
  rule list(_) ~> N:Int ~> mroMerge(list(L)) => raiseInternal("TypeError", "Cannot create a consistent method resolution order (MRO)") when N ==Int lengthList(L) andBool L =/=List .
  rule [getMro-finish]: list(L => Refify(Idify(L))) ~> (_:Int ~> mroMerge(list(.)) => .)
  context mutable(HOLE,_) when getKLabel HOLE ==KLabel 'getMro
  context immutable(HOLE,_) when getKLabel HOLE ==KLabel 'getMro

  syntax KLabel ::= "isMroReady"

  rule isMroReady(list(L:List)) => all(L, isObject)

  rule invokeBuiltin(obj("mro_type",_), ListItem(Type), .) => mutable(getMro(Type, getref(Type, "__bases__")), ref("list"))

  rule invokeBuiltin(obj("setattr",_), ListItem(O) ListItem(Name:Object) ListItem(Value:Object), .) => getmember(O, "__setattr__", true, false, true) (Name, Value)

  rule invokeBuiltin(obj("object.__setattr__",_), ListItem(O) ListItem(Name) ListItem(Value), .) => test(istype(O, ref("type")), raiseInternal("TypeError", "can't apply this __setattr__ to type object"), setmember(O, Name, Value))
  rule invokeBuiltin(obj("module.__setattr__",_), ListItem(O) ListItem(Name) ListItem(Value), .) => setmember(O, Name, Value)
  rule invokeBuiltin(obj("type.__setattr__",_), ListItem(Type) ListItem(Name) ListItem(Value), .) => setmember(Type, Name, Value)

  rule invokeBuiltin(obj("set_ref_dict",_), ListItem(Self) ListItem(Instance) ListItem(Value), .) => test(istype(Value, ref("dict")), setref(id(Instance), getattr(Self, "__get__"), Value), raiseInternal("TypeError", getattr(Self, "__get__") +String " must be set to a dictionary"))

  rule invokeBuiltin(obj("subclasshook_object",_), L:List, .) => ref("NotImplemented")
  rule invokeBuiltin(obj("instancecheck_type",_), ListItem(Self) ListItem(Instance), .) => bool(istype(Instance, Self))
  rule invokeBuiltin(obj("subclasscheck_type",_), ListItem(Self) ListItem(Subclass), .) => bool(hasbase(Subclass, Self))

  rule invokeBuiltin(obj("isinstance",_), ListItem(Instance:Object) ListItem(Class:Object), .) => test(istype(Class, ref("tuple")), AnyIsInstance(Instance, listvalue(Class)), test(istype(Class, ref("type")), getmember(Class, "__instancecheck__", true, false, true)(Instance), raiseInternal("TypeError", "isinstance() arg 2 must be a type or tuple of types")))
  rule invokeBuiltin(obj("issubclass",_), ListItem(Subclass:Object) ListItem(Class:Object), .) => test(istype(Class, ref("tuple")), AnyIsSubclass(Subclass, listvalue(Class)), test(istype(Class, ref("type")), getmember(Class, "__subclasscheck__", true, false, true)(Subclass), raiseInternal("TypeError", "issubclass() arg 2 must be a class or tuple of classes")))
  syntax Exp ::= AnyIsInstance(Object, List)
               | AnyIsSubclass(Object, List)
  context AnyIsInstance(_, ListItem(HOLE) _)
  context AnyIsSubclass(_, ListItem(HOLE) _)
  rule AnyIsInstance(Instance, ListItem(O:Object) L) => ref("isinstance")(Instance, O) or AnyIsInstance(Instance, L)
  rule AnyIsSubclass(Subclass, ListItem(O:Object) L) => ref("issubclass")(Subclass, O) or AnyIsSubclass(Subclass, L)
  rule AnyIsInstance(_, .List) => ref("False")
  rule AnyIsSubclass(_, .List) => ref("False")

  rule invokeBuiltin(obj("NoneType.__new__",_), ListItem(Cls), .) => newHelper(Cls, ref("NoneType"), .) ~> ref("None")

endmodule