require "python-semantics-common.k"

module PYTHON-SEMANTICS-ASSIGNMENT
  imports PYTHON-SEMANTICS-COMMON

  syntax K ::= "bindList" "(" List "," Object "," Bool ")"
             | "unbindList" "(" List ")"

  rule (. => bind(X:Id, ref(B:ObjId))) ~> ((X)::Target = Ts:AssignTargets => Ts) = obj(B,_)
  rule (. => bindList(Listify(Ts2), O, false)) ~> (tuple(Ts2:Targets) = Ts:AssignTargets => Ts) = O:Object
  rule (. => bindList(Listify(Ts2), O, false)) ~> ([ Ts2 ] = Ts:AssignTargets => Ts) = O
  rule (. => ref("setattr")(O, Id2String(X), O2) ;) ~> (O:Object . X:Id = Ts:AssignTargets => Ts) = O2:Object
  rule (. => (getmember(O, "__setitem__", true, false, false) -> raiseInternal("TypeError", "object does not support item assignment")) (Key:Object, Value:Object) ;) ~> (O:Object [ Key:Object ] = Ts:AssignTargets => Ts) = Value
  rule .AssignTargets = _ => .

  context HOLE . _:Id = _ = K:Exp when isKResult(K)
  context HOLE [ _ ] = _ = K:Exp when isKResult(K)
  context K [ HOLE ] = _ = K2:Exp when isKResult(K) andBool isKResult(K2)

  rule (. => unbind(X:Id)) ~> del (X , Ts:NeTargets => Ts)
  rule (. => unbindList(Listify(Ts2))) ~> del (tuple(Ts2) , Ts => Ts)
  rule (. => unbindList(Listify(Ts2))) ~> del ([ Ts2 ] , Ts => Ts)
  rule (. => (getmember(O, "__delattr__", true, false, true) (Id2String(X)) ;)) ~> del (O:Object . X:Id , Ts => Ts)
  rule (. => (getmember(O, "__delitem__", true, false, false) -> raiseInternal("TypeError", "object does not support item deletion")) (Key) ;)  ~> del (O:Object [ Key:Object ] , Ts => Ts)
  rule del .NeTargets => .

  context del HOLE . _:Id , _
  context del HOLE [ _ ] , _
  context del K [ HOLE ] , _ when isKResult(K)

  rule (. => iterate(O, .)) ~> bindList(_, O, _)
  rule (. => T = O:Object) ~> list((ListItem(O) => .) _) ~> bindList((ListItem(T:Target) => .) _, _, _) when getKLabel T =/=KLabel 'Starred
  rule (. => T:Target = mutable(list(Refify(Idify(L))), ref("list"))) ~> list((L:List => .) L2:List) ~> bindList((ListItem(* T) => .) L3:List, _, (false => true)) when lengthList L2 ==Int lengthList L3
  rule list(.) ~> bindList(., _, _) => .
  rule list(ListItem(_) _) ~> bindList(., _, _) => raiseInternal("ValueError", "too many values to unpack")
  rule list(.) ~> bindList(ListItem(T) _, _, _) => raiseInternal("ValueError", "need more values to unpack") when getKLabel T =/=KLabel 'Starred

  rule (. => del (T ::Target)) ~> unbindList((ListItem(T) => .) _)
  rule unbindList(.) => .

endmodule