diff --git a/python-semantics-assignment.k b/python-semantics-assignment.k index a67a24b..865b0db 100644 --- a/python-semantics-assignment.k +++ b/python-semantics-assignment.k @@ -9,8 +9,8 @@ module PYTHON-SEMANTICS-ASSIGNMENT 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 (. => 'Expr(ref("setattr")(O, Id2String(X), O2))) ~> (O:Object . X:Id = Ts:AssignTargets => Ts) = O2:Object + rule (. => 'Expr((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) @@ -20,8 +20,8 @@ module PYTHON-SEMANTICS-ASSIGNMENT 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 (. => 'Expr(getmember(O, "__delattr__", true, false, true) (Id2String(X)))) ~> del (O:Object . X:Id , Ts => Ts) + rule (. => 'Expr((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 , _ diff --git a/python-semantics-attribute-ref.k b/python-semantics-attribute-ref.k index 058fda2..bedc712 100644 --- a/python-semantics-attribute-ref.k +++ b/python-semantics-attribute-ref.k @@ -16,9 +16,9 @@ module PYTHON-SEMANTICS-ATTRIBUTE-REF rule [attribute]: O:Object . X:Id => ref("getattr")(O, Id2String(X)) - rule invokeBuiltin(obj("getattr",_), ListItem(O) ListItem(S:Object), .) => checkAttribute(S) ~> try: (getmember(O, "__getattribute__", true, false, true) (S)) except ref("AttributeError") : (getmember(O, "__getattr__", true, false, false) (S) -> raise) else: pass - rule invokeBuiltin(obj("getattr",_), ListItem(O:Object) ListItem(S:Object) ListItem(Default), .) => checkAttribute(S) ~> try: ref("getattr")(O, S) except ref("AttributeError") : Default else: pass - rule invokeBuiltin(obj("hasattr",_), ListItem(O:Object) ListItem(S:Object), .) => checkAttribute(S) ~> try: (ref("getattr")(O, S) ; ~> ref("True")) except ref("AttributeError") : ref("False") else: pass + rule invokeBuiltin(obj("getattr",_), ListItem(O) ListItem(S:Object), .) => checkAttribute(S) ~> try: returnInternal(getmember(O, "__getattribute__", true, false, true) (S)) except ref("AttributeError") : returnInternal(getmember(O, "__getattr__", true, false, false) (S) -> raise) else: .K + rule invokeBuiltin(obj("getattr",_), ListItem(O:Object) ListItem(S:Object) ListItem(Default), .) => checkAttribute(S) ~> try: returnInternal(ref("getattr")(O, S)) except ref("AttributeError") : returnInternal(Default) else: .K + rule invokeBuiltin(obj("hasattr",_), ListItem(O:Object) ListItem(S:Object), .) => checkAttribute(S) ~> try: returnInternal('Expr((ref("getattr")(O, S)) ~> ref("True"))) except ref("AttributeError") : returnInternal(ref("False")) else: .K rule invokeBuiltin(obj("getattribute_object",_), ListItem(O) ListItem(O2:Object), .) => checkAttribute(O2) ~> checkData(getmember(O, O2, false, false, false), O) -> mapLookup(O, O2) -> getmember(O, O2, true, false, true) rule invokeBuiltin(obj("getattribute_type",_), ListItem(O) ListItem(O2), .) => checkAttribute(O2) ~> checkData(getmember(O, O2, false, false, false), O) -> getmember(O, O2, true, true, true) @@ -44,7 +44,7 @@ module PYTHON-SEMANTICS-ATTRIBUTE-REF rule hasmember(O:Object, O2:Object) => getmember(O, O2, false, false, false) =/=Obj .Obj - rule mapLookup(obj(B,_), O) => try: K[O] except ref("KeyError") : .Obj else: pass ... + rule mapLookup(obj(B,_), O) => try: returnInternal(K[O]) except ref("KeyError") : returnInternal(.Obj) else: .K ... B ... "__dict__" |-> K ... diff --git a/python-semantics-augmented-assignment.k b/python-semantics-augmented-assignment.k index efdee61..93af382 100644 --- a/python-semantics-augmented-assignment.k +++ b/python-semantics-augmented-assignment.k @@ -26,7 +26,7 @@ module PYTHON-SEMANTICS-AUGMENTED-ASSIGNMENT rule augAssign(T, O, Lbl:KLabel, IX) => augAssign2(T, T, O, Lbl, IX) rule augAssign2(T, O, O2:Object, Lbl, IX) => augAssign3(T, O, O2, Lbl, getmember(O, IX, true, false, false)) - rule augAssign3(T, O, O2:Object, Lbl, IO:Object) => IO(O2) ; + rule augAssign3(T, O, O2:Object, Lbl, IO:Object) => 'Expr(IO(O2)) rule augAssign3(T:Target, O, O2, Lbl, .Obj) => T = (Lbl(O,,O2))::Exp endmodule diff --git a/python-semantics-builtin-functions.k b/python-semantics-builtin-functions.k index 3668b91..4ba0887 100644 --- a/python-semantics-builtin-functions.k +++ b/python-semantics-builtin-functions.k @@ -5,8 +5,8 @@ module PYTHON-SEMANTICS-BUILTIN-FUNCTIONS syntax K ::= doAll(Exp) [strict] - rule invokeBuiltin(obj("all",_), ListItem(O:Object), .) => try: doAll(ref("iter")(O)) except ref("StopIteration"): ref("True") else: pass - rule doAll(Iter:Object) => if not getmember(Iter, "__next__", true, false, true)(.Arguments) : ref("False") else: doAll(Iter) + rule invokeBuiltin(obj("all",_), ListItem(O:Object), .) => try: doAll(ref("iter")(O)) except ref("StopIteration"): returnInternal(ref("True")) else: .K + rule doAll(Iter:Object) => if not getmember(Iter, "__next__", true, false, true)(.Arguments) : returnInternal(ref("False")) else: doAll(Iter) rule invokeBuiltin(obj("super.__new__",_), ListItem(Cls) L:List, .) => newHelper(Cls, ref("super"), .) ~> mutable("__self__" |-> ref("None") "__self_class__" |-> ref("None") "__thisclass__" |-> ref("None"), Cls) rule invokeBuiltin(obj("super.__init__",_), ListItem(O), .) => #if ArgCount >Int 0 #then if VarNames[0] in Locals: if "__class__" in Cells: test(getattr2(Cells["__class__"], "cell_contents") =/=Obj .Obj, test(istype(getref2(Cells["__class__"], "cell_contents"), ref("type")), ref("super.__init__")(O, getref2(Cells["__class__"], "cell_contents"), Locals[VarNames[0]]), raiseInternal("SystemError", "super(): __class__ is not a type")), raiseInternal("SystemError", "super(): empty __class__ cell")) else: raiseInternal("SystemError", "super(): __class__ cell not found") else: raiseInternal("SystemError", "super(): arg[0] deleted") #else raiseInternal("SystemError", "super(): no arguments") #fi ... diff --git a/python-semantics-classes.k b/python-semantics-classes.k index 164a919..7beff54 100644 --- a/python-semantics-classes.k +++ b/python-semantics-classes.k @@ -17,7 +17,7 @@ module PYTHON-SEMANTICS-CLASSES rule invokeClass(Metaclass:Object, CO:Object, Bases:Object, M:Map) => executeClass(Metaclass, CO, Bases, ref("builtins"), ref("globals")(.Arguments), doCall(Metaclass . String2Id("__prepare__"), ListItem(CO . String2Id("co_name")) ListItem(Bases), M), M) - rule executeClass(Metaclass:Object, CO:Object, Bases:Object, Builtins:Object, Globals:Object, Locals:Object, M:Map) => executeFrame(N, CO, ref(Back), Locals, Globals, Builtins, makeCells(CO . String2Id("co_freevars"), CO . String2Id("co_cellvars"), ref("tuple")(ref("map")(getref2(ref(Back), "f_cells") . String2Id("__getitem__"), CO . String2Id("co_freevars"))), N), .) ~> ((Locals["__module__"]) = ref("globals")(.Arguments)["__name__"]::Exp) ~> (if CO . String2Id("co_consts")[0] is not ref("None") : (Locals["__doc__"]) = CO . String2Id("co_consts")[0] else: pass) ~> restoreContext(LL, FL, Back) ~> setClass(doCall(Metaclass, ListItem(CO . String2Id("co_name")) ListItem(Bases) ListItem(Locals), M), CO, ref(N)) ... + rule executeClass(Metaclass:Object, CO:Object, Bases:Object, Builtins:Object, Globals:Object, Locals:Object, M:Map) => executeFrame(N, CO, ref(Back), Locals, Globals, Builtins, makeCells(CO . String2Id("co_freevars"), CO . String2Id("co_cellvars"), ref("tuple")(ref("map")(getref2(ref(Back), "f_cells") . String2Id("__getitem__"), CO . String2Id("co_freevars"))), N), .) ~> ((Locals["__module__"]) = ref("globals")(.Arguments)["__name__"]::Exp) ~> (if CO . String2Id("co_consts")[0] is not ref("None") : (Locals["__doc__"]) = CO . String2Id("co_consts")[0] else: .K) ~> restoreContext(LL, FL, Back) ~> setClass(doCall(Metaclass, ListItem(CO . String2Id("co_name")) ListItem(Bases) ListItem(Locals), M), CO, ref(N)) ... N => N +Int 1 Back:Int FL => . @@ -51,11 +51,11 @@ module PYTHON-SEMANTICS-CLASSES rule invokeBuiltin(obj("new_type",_), ListItem(Type:Object) ListItem(Name:Object) ListItem(Bases:Object) ListItem(Dict:Object), _) => newHelper(Type, ref("type"), .Set) ~> test(istype(Name, ref("str")), test(istype(Bases, ref("tuple")), test(istype(Dict, ref("dict")), calculateMetaclass(Name, Bases, Type, Dict, Type), raiseInternal("TypeError", "type() argument 3 must be dict")), raiseInternal("TypeError", "type() argument 2 must be tuple")), raiseInternal("TypeError", "type() argument 1 must be str")) rule (. => iterate(Bases, .)) ~> calculateMetaclass(_, Bases, _, _, _) - rule (. => if gettype(O) is ref("type") or bool(hasbase(Winner, gettype(O))) : pass else: test(hasbase(gettype(O), Winner), setWinner(gettype(O)), raiseInternal("TypeError", "metaclass conflict: the metaclass of a derived class must be a (non-strict) subclass of the metaclasses of all its bases"))) ~> list((ListItem(O) => .) _) ~> calculateMetaclass(_, _, _, _, Winner) + rule (. => if gettype(O) is ref("type") or bool(hasbase(Winner, gettype(O))) : .K else: test(hasbase(gettype(O), Winner), setWinner(gettype(O)), raiseInternal("TypeError", "metaclass conflict: the metaclass of a derived class must be a (non-strict) subclass of the metaclasses of all its bases"))) ~> list((ListItem(O) => .) _) ~> calculateMetaclass(_, _, _, _, Winner) rule (setWinner(O:Object) => .) ~> list(_) ~> calculateMetaclass(_, _, _, _, (_ => O)) rule list(.) ~> calculateMetaclass(Name, Bases, Type, Dict:Object, Type) => makeType(mutable("__name__" |-> strvalue(Name) "__bases__" |-> ref(id(Bases)), Type), ref("dict")(Dict)) rule list(.) ~> calculateMetaclass(Name:Object, Bases:Object, Type, Dict:Object, Winner:Object) => Winner . String2Id("__new__") (Winner, Name, Bases, Dict) when Winner =/=K Type - rule makeType(O:Object, Dict:Object) => (if "__doc__" not in Dict : Dict["__doc__"] = ref("None") else: pass) ~> (if "__module__" not in Dict : Dict["__module__"] = ref("globals")(.Arguments)["__name__"] else: pass) ~> (if getref(O, "__bases__") == tuple(.Exps) : setref(id(O), "__bases__", tuple(ref("object"))) else: pass) ~> (if "__hash__" not in Dict and "__eq__" in Dict : Dict["__hash__"] = ref("None") else: pass) ~> (if "__new__" in Dict and bool(istype(Dict["__new__"], ref("function"))) : Dict["__new__"] = ref("staticmethod")(Dict["__new__"]) else: pass) ~> setref(id(O), "__dict__", Dict) ~> setref(id(O), "__mro__", ref("tuple")(getmember(O, "mro", true, false, true) (.Arguments))) ~> ref(id(O)) + rule makeType(O:Object, Dict:Object) => (if "__doc__" not in Dict : Dict["__doc__"] = ref("None") else: .K) ~> (if "__module__" not in Dict : Dict["__module__"] = ref("globals")(.Arguments)["__name__"] else: .K) ~> (if getref(O, "__bases__") == tuple(.Exps) : setref(id(O), "__bases__", tuple(ref("object"))) else: .K) ~> (if "__hash__" not in Dict and "__eq__" in Dict : Dict["__hash__"] = ref("None") else: .K) ~> (if "__new__" in Dict and bool(istype(Dict["__new__"], ref("function"))) : Dict["__new__"] = ref("staticmethod")(Dict["__new__"]) else: .K) ~> setref(id(O), "__dict__", Dict) ~> setref(id(O), "__mro__", ref("tuple")(getmember(O, "mro", true, false, true) (.Arguments))) ~> ref(id(O)) endmodule diff --git a/python-semantics-common.k b/python-semantics-common.k index 3ee1058..33d5cfe 100644 --- a/python-semantics-common.k +++ b/python-semantics-common.k @@ -58,6 +58,9 @@ module PYTHON-SEMANTICS-COMMON | getMro(Exp, Exp) [strict] | doBind(String, Exp, Exp) [strict(3)] + syntax Suite ::= returnInternal(Exp) + rule returnInternal(E) => E [macro] + syntax #Id ::= "__class__" | "__dict__" | "__next__" syntax Test ::= "istype" "(" Exp "," Exp ")" [strict] @@ -103,11 +106,11 @@ module PYTHON-SEMANTICS-COMMON rule reduce(ListItem(I) L:List, K, Lbl) => Lbl(I,,reduce(L, K, Lbl)) syntax String ::= "docString" "(" K ")" [function] - rule docString(S:String ;) => S - rule docString(S:String ; newline _) => S - rule docString(Lbl:KLabel(_)) => ref("None") when Lbl =/=KLabel '_newline_ andBool Lbl =/=KLabel 'Expr - rule docString(Lbl:KLabel(Lbl2:KLabel(_),,_)) => ref("None") when Lbl ==KLabel '_newline_ andBool Lbl2 =/=KLabel 'Expr - rule docString(Lbl:KLabel(Lbl2:KLabel(K),,_)) => ref("None") when Lbl ==KLabel '_newline_ andBool Lbl2 ==KLabel 'Expr andBool isString(K) =/=K true + rule docString('Expr(S:String)) => S + rule docString('Expr(S:String) ; _) => S + rule docString(Lbl:KLabel(_)) => ref("None") when Lbl =/=KLabel '_;_ andBool Lbl =/=KLabel 'Expr + rule docString(Lbl:KLabel(Lbl2:KLabel(_),,_)) => ref("None") when Lbl ==KLabel '_;_ andBool Lbl2 =/=KLabel 'Expr + rule docString(Lbl:KLabel(Lbl2:KLabel(K),,_)) => ref("None") when Lbl ==KLabel '_;_ andBool Lbl2 ==KLabel 'Expr andBool isString(K) =/=K true rule docString(Lbl:KLabel(K,,_)) => ref("None") when Lbl ==KLabel 'Expr andBool isString(K) =/=K true rule docString(.) => ref("None") @@ -317,7 +320,7 @@ module PYTHON-SEMANTICS-COMMON context list(.) ~> iterate(HOLE,_) - rule iterate(O:Object, K) => try: (list(.) ~> iterate(ref("iter") (O), K)) except ref("TypeError") : test(K ==K ., raise, K) else: pass + rule iterate(O:Object, K) => try: (list(.) ~> iterate(ref("iter") (O), K)) except ref("TypeError") : test(K ==K ., raise, K) else: .K rule list(L:List) ~> iterate(O:Object, K) => try: addItem(getmember(O, "__next__", true, false, false) (.Arguments)) except ref("StopIteration") : list(L) else: (list(L) ~> iterate(O, K)) rule (addItem(O:Object) => .) ~> popx ~> list(_ (. => ListItem(O))) rule Lbl:KLabel(Kl:KList) ~> setx(K2) => setx(K2) ~> Lbl(Kl) when isKResult(Lbl(Kl)) diff --git a/python-semantics-dicts.k b/python-semantics-dicts.k index 9584cb9..79c081a 100644 --- a/python-semantics-dicts.k +++ b/python-semantics-dicts.k @@ -59,9 +59,9 @@ module PYTHON-SEMANTICS-DICTS rule invokeBuiltin(obj("get_dict",_), ListItem(O:Object) ListItem(Key:Object), .) => ref("get_dict")(O, Key, ref("None")) rule invokeBuiltin(obj("get_dict",_), ListItem(obj(B,_)) ListItem(Key:Object) ListItem(Default:Object), .) => try: (ref("hash")(Key) ~> tableLookup(B, 0, Key)) except ref("KeyError"): Default rule (O:Object => .) ~> tableLookup(_,(_ => intvalue(O)),_) - rule (O:Object => .) ~> tableLookup(_,(_ => intvalue(O)),_) ; + rule (O:Object => .) ~> 'Expr(tableLookup(_,(_ => intvalue(O)),_)) - rule invokeBuiltin(obj("setitem_dict",_), ListItem(O) ListItem(Key) ListItem(Value:Object), .) => processDict(O, Key |-> Value) ; ~> ref("None") + rule invokeBuiltin(obj("setitem_dict",_), ListItem(O) ListItem(Key) ListItem(Value:Object), .) => 'Expr(processDict(O, Key |-> Value)) ~> ref("None") rule invokeBuiltin(obj("delitem_dict",_), ListItem(obj(B,_)) ListItem(Key:Object), .) => ref("hash")(Key) ~> tableDelete(B, 0, Key) ~> ref("None") rule (O:Object => .) ~> tableDelete(_,(_ => intvalue(O)),_) @@ -89,6 +89,6 @@ module PYTHON-SEMANTICS-DICTS rule equalDict(Key |-> Value M:Map, Dict) => Key in Dict and Dict[Key] == Value and equalDict(M, Dict) rule equalDict(.Map, _) => ref("True") - rule invokeBuiltin(obj("contains_dict",_), ListItem(Dict) ListItem(Key:Object), .) => try: (ref("hash")(Key) ~> tableLookup(id(Dict), 0, Key) ; ~> ref("True")) except ref("KeyError"): ref("False") else: pass + rule invokeBuiltin(obj("contains_dict",_), ListItem(Dict) ListItem(Key:Object), .) => try: (ref("hash")(Key) ~> 'Expr(tableLookup(id(Dict), 0, Key)) ~> ref("True")) except ref("KeyError"): ref("False") else: .K endmodule diff --git a/python-semantics-dunder-builtin.k b/python-semantics-dunder-builtin.k index 8f91000..d2e7e61 100644 --- a/python-semantics-dunder-builtin.k +++ b/python-semantics-dunder-builtin.k @@ -65,7 +65,7 @@ module PYTHON-SEMANTICS-DUNDER-BUILTIN object "ValueError"("type",ListItem("Exception"),.,.) ~> object "Warning"("type",ListItem("Exception"),.,.) ~> object "ZeroDivisionError"("type", ListItem("ArithmeticError"),.,.) ~> - (def "all"(1, 1, false) ;) ~> + ('Expr( "all"(1, 1, false) )) ~> object "bool"("type",ListItem("int"), "__new__" |-> def "new_bool" (1, 2, false) ,.) ~> @@ -91,7 +91,7 @@ module PYTHON-SEMANTICS-DUNDER-BUILTIN "__init__" |-> def "init_classmethod"(1, 1, true) "__new__" |-> def "new_classmethod"(2, 2, false) ,.) ~> - (def "compile"(3, 6, false) ;) ~> + ('Expr( "compile"(3, 6, false) )) ~> object "complex"("type",ListItem("object"),.,.) ~> object "dict"("type",ListItem("object"), "get" |-> def "get_dict" (1, 2, true) @@ -110,8 +110,8 @@ module PYTHON-SEMANTICS-DUNDER-BUILTIN object "dict_keys" ("type",ListItem("object"), "__iter__" |-> def "iter_dict_keys" (0, 0, true) ,.) ~> - (def "eval" (1, 3, false) ;) ~> - (def "exec" (1, 3, false) ;) ~> + ('Expr( "eval" (1, 3, false) )) ~> + ('Expr( "exec" (1, 3, false) )) ~> object "float"("type",ListItem("object"), "__eq__" |-> def "float.__eq__"(1, 1, true) "__ge__" |-> def "float.__ge__" (1, 1, true) @@ -121,13 +121,13 @@ module PYTHON-SEMANTICS-DUNDER-BUILTIN "__lt__" |-> def "float.__lt__" (1, 1, true) "__ne__" |-> def "float.__ne__" (1, 1, true) ,.) ~> - (def "format" (1, 2, false) ;) ~> - (def "getattr" (2, 3, false) ;) ~> - (def "globals" (0, 0, false) ;) ~> - (def "hasattr" (2, 2, false) ;) ~> - (def "hash" (1, 1, false) ;) ~> - (def "id"(1, 1, false) ;) ~> - (def "index" (1, 1, false) ;) ~> + ('Expr( "format" (1, 2, false) )) ~> + ('Expr( "getattr" (2, 3, false) )) ~> + ('Expr( "globals" (0, 0, false) )) ~> + ('Expr( "hasattr" (2, 2, false) )) ~> + ('Expr( "hash" (1, 1, false) )) ~> + ('Expr( "id"(1, 1, false) )) ~> + ('Expr( "index" (1, 1, false) )) ~> object "int"("type",ListItem("object"), "__abs__" |-> def "abs_int" (0, 0, true) "__add__" |-> def "add_int" (1, 1, true) @@ -181,14 +181,14 @@ module PYTHON-SEMANTICS-DUNDER-BUILTIN //TODO: bit_length, conjugate, denominator, from_bytes, imag, // numerator, real, to_bytes ,.) ~> - (def "isinstance" (2, 2, false) ;) ~> - (def "issubclass" (2, 2, false) ;) ~> - (def "iter" (1, 2, false) ;) ~> + ('Expr( "isinstance" (2, 2, false) )) ~> + ('Expr( "issubclass" (2, 2, false) )) ~> + ('Expr( "iter" (1, 2, false) )) ~> object "iterator"("type",ListItem("object"), "__iter__" |-> def "iter_iter" (0, 0, true) "__next__" |-> def "iter_next" (0, 0, true) ,.) ~> - (def "len" (1, 1, false) ;) ~> + ('Expr( "len" (1, 1, false) )) ~> object "list"("type",ListItem("object"), "append" |-> def "append_list"(1, 1, true) "extend" |-> def "extend_list"(1, 1, true) @@ -202,7 +202,7 @@ module PYTHON-SEMANTICS-DUNDER-BUILTIN "__new__" |-> def "new_list" (1, -1, false) "__setitem__" |-> def "setitem_list" (2, 2, true) ,.) ~> - (def "locals" (0, 0, false) ;) ~> + ('Expr( "locals" (0, 0, false) )) ~> object "map"("type",ListItem("object"), "__iter__" |-> ref("iter_iter") "__new__" |-> def "new_map" (3, -1, false) @@ -229,12 +229,12 @@ module PYTHON-SEMANTICS-DUNDER-BUILTIN "__subclasshook__" |-> def "subclasshook_object"(0, -1, false) ,.) ~> object "__class__" ("attribute",.,., "__get__" |-> "__class__") ~> - (def "ord" (1, 1, false) ;) ~> + ('Expr( "ord" (1, 1, false) )) ~> object "range" ("type",ListItem("object"), "__iter__" |-> def "iter_range" (0, 0, true) "__new__" |-> def "new_range" (1, 4, false) ,.) ~> - (def "repr" (1, 1, false) ;) ~> + ('Expr( "repr" (1, 1, false) )) ~> object "reversed" ("type", ListItem("object"), "__new__" |-> def "reversed.__new__"(2, 2, false) "__next__" |-> def "reversed.__next__"(0, 0, true) @@ -250,7 +250,7 @@ module PYTHON-SEMANTICS-DUNDER-BUILTIN "__ne__" |-> def "ne_set"(1, 1, true) "__new__" |-> def "new_set" (1, -1, false) ,.) ~> - (def "setattr" (3, 3, false) ;) ~> + ('Expr( "setattr" (3, 3, false) )) ~> object "slice" ("type",ListItem("object"), "indices" |-> def "indices_slice" (1, 1, true) "start" |-> ref("start") @@ -412,27 +412,27 @@ module PYTHON-SEMANTICS-DUNDER-BUILTIN object "cell"("type",ListItem("object"), ., .) ~> object "cell_contents" ("attribute",.,., "__get__" |-> "cell_contents") ~> - (def "new_structseq" (2, 2, false) ;) ~> + ('Expr( "new_structseq" (2, 2, false) )) ~> //module "sys" - (def "sys_exc_info" (0, 0, false) ;) ~> + ('Expr( "sys_exc_info" (0, 0, false) )) ~> struct "sys.flags"("optimize","verbose") ~> struct "sys.hash_info"("width", "modulus", "inf", "nan", "imag") ~> struct "sys.version_info"("major", "minor", "micro", "releaselevel", "serial") ~> struct "sys.implementation"("name", "version", "hexversion", "cache_tag") ~> //module "_imp" - (def "imp__fix_co_filename"(2, 2, false) ;) ~> - (def "imp_acquire_lock" (0, 0, false) ;) ~> - (def "imp_extension_suffixes" (0, 0, false) ;) ~> - (def "imp_init_builtin" (1, 1, false) ;) ~> - (def "imp_init_frozen" (1, 1, false) ;) ~> - (def "imp_is_builtin" (1, 1, false) ;) ~> - (def "imp_is_frozen" (1, 1, false) ;) ~> - (def "imp_is_frozen_package" (1, 1, false) ;) ~> - (def "imp_get_frozen_object" (1, 1, false) ;) ~> - (def "imp_load_dynamic" (2, 3, false) ;) ~> - (def "imp_release_lock" (0, 0, false) ;) ~> + ('Expr( "imp__fix_co_filename"(2, 2, false) )) ~> + ('Expr( "imp_acquire_lock" (0, 0, false) )) ~> + ('Expr( "imp_extension_suffixes" (0, 0, false) )) ~> + ('Expr( "imp_init_builtin" (1, 1, false) )) ~> + ('Expr( "imp_init_frozen" (1, 1, false) )) ~> + ('Expr( "imp_is_builtin" (1, 1, false) )) ~> + ('Expr( "imp_is_frozen" (1, 1, false) )) ~> + ('Expr( "imp_is_frozen_package" (1, 1, false) )) ~> + ('Expr( "imp_get_frozen_object" (1, 1, false) )) ~> + ('Expr( "imp_load_dynamic" (2, 3, false) )) ~> + ('Expr( "imp_release_lock" (0, 0, false) )) ~> //module "_io" object "BytesIO"("type", ListItem("_BufferedIOBase"), @@ -496,7 +496,7 @@ module PYTHON-SEMANTICS-DUNDER-BUILTIN object "_BufferedIOBase"("type", ListItem("_IOBase"),.,.) ~> //module "_warnings" - (def "_warnings.warn" (1, 3, false) ;) ~> + ('Expr( "_warnings.warn" (1, 3, false) )) ~> //module "_weakref" object "weakref"("type", ListItem("object"), @@ -505,20 +505,20 @@ module PYTHON-SEMANTICS-DUNDER-BUILTIN ,.) ~> //module "gc" - (def "gc.collect"(0, 0, false) ;) ~> + ('Expr( "gc.collect"(0, 0, false) )) ~> //module "marshal" - (def "marshal.dumps"(1, 2, false) ;) ~> - (def "marshal.loads"(1, 1, false) ;) ~> + ('Expr( "marshal.dumps"(1, 2, false) )) ~> + ('Expr( "marshal.loads"(1, 1, false) )) ~> //module "posix" - (def "posix.getcwd"(0, 0, false) ;) ~> - (def "posix.listdir"(0, 1, false) ;) ~> - (def "posix.mkdir"(1, 2, false) ;) ~> - (def "posix.open"(2, 3, false) ;) ~> - (def "posix.replace"(2, 2, false) ;) ~> - (def "posix.stat"(1, 1, false) ;) ~> - (def "posix.unlink"(1, 1, false) ;) ~> + ('Expr( "posix.getcwd"(0, 0, false) )) ~> + ('Expr( "posix.listdir"(0, 1, false) )) ~> + ('Expr( "posix.mkdir"(1, 2, false) )) ~> + ('Expr( "posix.open"(2, 3, false) )) ~> + ('Expr( "posix.replace"(2, 2, false) )) ~> + ('Expr( "posix.stat"(1, 1, false) )) ~> + ('Expr( "posix.unlink"(1, 1, false) )) ~> struct "posix.stat_result" ("st_mode", "st_ino", "st_dev", "st_nlink", "st_uid", "st_gid", "st_size", "st_atime", "st_mtime", "st_ctime") ~> .K ) diff --git a/python-semantics-environment.k b/python-semantics-environment.k index 3011c87..ee230c6 100644 --- a/python-semantics-environment.k +++ b/python-semantics-environment.k @@ -48,18 +48,18 @@ module PYTHON-SEMANTICS-ENVIRONMENT test(B ==K 0, (if S in Frame . f_locals : del Frame . f_locals [S] else: raiseInternal("UnboundLocalError", "local variable '" +String S +String "' referenced before assignment")), Frame . f_locals [S] = ref(B)) - else: pass ~> + else: .K ~> if S in Code . String2Id("co_cellvars") or S in Code . String2Id("co_freevars") : test(B ==K 0, setattr(id(getref(Frame, "f_cells")[S]), "cell_contents", .Obj), setref(id(getref(Frame, "f_cells")[S]), "cell_contents", ref(B))) - else: pass ~> + else: .K ~> if S in Code . String2Id("co_names") : test(B ==K 0, (if S in Frame . f_globals : del ((Frame . f_globals [S])) else: raiseInternal("NameError", "name '" +String S +String "' is not defined")), (Frame . f_globals [S] = ref(B))) - else: pass + else: .K rule [globals]: invokeBuiltin(obj("globals",_), ., .) => ref(N) . f_globals ... N diff --git a/python-semantics-functions.k b/python-semantics-functions.k index e716523..6519aa6 100644 --- a/python-semantics-functions.k +++ b/python-semantics-functions.k @@ -164,9 +164,9 @@ module PYTHON-SEMANTICS-FUNCTIONS rule createClass(X:Id, As, O:Object) => visited((X)::Target = class(As, O)) rule createGenerator(O:Object) => visited(function(.Parameters, O, .Obj)(.Arguments)) - rule comprehension(E, for T in E2 Comps ::Comps) => for T in E2 : comprehension(E, Comps) else: pass - rule comprehension(E, if E2 Comps ::Comps) => if E2 : comprehension(E, Comps) else: pass - rule comprehension(E, .Comps) => yield E ; + rule comprehension(E, for T in E2 Comps ::Comps) => for T in E2 : comprehension(E, Comps) else: .K + rule comprehension(E, if E2 Comps ::Comps) => if E2 : comprehension(E, Comps) else: .K + rule comprehension(E, .Comps) => 'Expr(yield E) rule makeCodeObject(N, ., Ss, _) => visit(Ss, 'compileVisitor) ~> visit(Ss, 'childScopeVisitor) ~> storescope ~> propscope ~> delscope rule (visited(_) => .) ~> visit(_, 'childScopeVisitor) diff --git a/python-semantics-garbage-collection.k b/python-semantics-garbage-collection.k index 9e5cb64..c99c125 100644 --- a/python-semantics-garbage-collection.k +++ b/python-semantics-garbage-collection.k @@ -127,7 +127,7 @@ module PYTHON-SEMANTICS-GARBAGE-COLLECTION C:Bag syntax K ::= clearWeakrefs(K) - rule clearWeakrefs(list(ListItem(ref(N)) L:List)) => setattr(N, "referent", .Obj) ~> try: test(getref2(ref(N), "callback") ==Obj .Obj, pass, getref2(ref(N), "callback") (ref(N)) ;) except ref("BaseException") : ref("print")("Exception " + ref("sys_exc_info")(.Arguments)[1] + " ignored") ; else: pass ~> clearWeakrefs(list(L)) + rule clearWeakrefs(list(ListItem(ref(N)) L:List)) => setattr(N, "referent", .Obj) ~> try: test(getref2(ref(N), "callback") ==Obj .Obj, .K, 'Expr(getref2(ref(N), "callback") (ref(N)))) except ref("BaseException") : 'Expr(ref("print")("Exception " + ref("sys_exc_info")(.Arguments)[1] + " ignored")) else: .K ~> clearWeakrefs(list(L)) rule clearWeakrefs(list(.)) => . // since garbage collection is implementation specific, we treat the number of objects collected by any given call to the garbage collector as a symbolic int diff --git a/python-semantics-generator.k b/python-semantics-generator.k index cc6fc5a..31dc473 100644 --- a/python-semantics-generator.k +++ b/python-semantics-generator.k @@ -24,7 +24,7 @@ module PYTHON-SEMANTICS-GENERATOR rule createRaiseStatement(O, Type, .Obj, Traceback:Object) => test(istype(Type, ref("BaseException")), throwGenerator(O, Type . String2Id("with_traceback")(Traceback)), throwGenerator(O, Type(.Arguments) . String2Id("with_traceback")(Traceback))) rule createRaiseStatement(O, Type, Value:Object, Traceback:Object) => throwGenerator(O, Type(Value) . String2Id("with_traceback")(Traceback)) - rule invokeBuiltin(obj("close_generator",_), ListItem(O), .) => try: throwGenerator(O, ref("GeneratorExit")) ; except ref("GeneratorExit") : ref("None") except ref("StopIteration") : ref("None") else: raiseInternal("RuntimeError", "generator ignored GeneratorExit") + rule invokeBuiltin(obj("close_generator",_), ListItem(O), .) => try: 'Expr(throwGenerator(O, ref("GeneratorExit"))) except ref("GeneratorExit") : ref("None") except ref("StopIteration") : ref("None") else: raiseInternal("RuntimeError", "generator ignored GeneratorExit") syntax ObjRef ::= runGenerator(Exp, Exp) [strict] | throwGenerator(Exp, Exp) [strict] @@ -58,7 +58,7 @@ module PYTHON-SEMANTICS-GENERATOR ... syntax Arguments ::= "#if" Bool "#then" Arguments "#else" Arguments "#fi" [function] - rule return O:Object ~> _ => setattr(N, "gi_state", (#freezer (HOLE ;)(.KList), SavedC, .List, SavedXC)) ~> raise ref("StopIteration")(#if id(O) ==K NoneId #then .Arguments #else O #fi) ~> K + rule return O:Object ~> _ => setattr(N, "gi_state", (#freezer ('Expr(HOLE))(.KList), SavedC, .List, SavedXC)) ~> raise ref("StopIteration")(#if id(O) ==K NoneId #then .Arguments #else O #fi) ~> K ... ListItem(generator(Frame, C, FL, XC, K, ref(N))) => . ... @@ -81,7 +81,7 @@ module PYTHON-SEMANTICS-GENERATOR - rule [raise-out-of-generator]: (. => setattr(N, "gi_state", (#freezer (HOLE ;)(.KList), . SavedC, .List, ref("None")))) ~> raise ... + rule [raise-out-of-generator]: (. => setattr(N, "gi_state", (#freezer 'Expr((HOLE))(.KList), . SavedC, .List, ref("None")))) ~> raise ... ... ListItem(generator(Frame, C, FL, _, _, ref(N))) => . ... diff --git a/python-semantics-import.k b/python-semantics-import.k index 0b17869..6214910 100644 --- a/python-semantics-import.k +++ b/python-semantics-import.k @@ -12,7 +12,7 @@ module PYTHON-SEMANTICS-IMPORT // importlib rule importlib => doImportlib({.KeyData}) - rule doImportlib(Dict:Object) => executeModule(codeObject(String2Id("importlib._bootstrap"), .Parameters, Importlib, moduleobject), ref("builtins"), Dict) ~> Dict["_install"](ref("sys"), ref("_imp")) ; ~> ref("builtins") . String2Id("__import__") = Dict["__import__"]::Exp ... + rule doImportlib(Dict:Object) => executeModule(codeObject(String2Id("importlib._bootstrap"), .Parameters, Importlib, moduleobject), ref("builtins"), Dict) ~> 'Expr(Dict["_install"](ref("sys"), ref("_imp"))) ~> ref("builtins") . String2Id("__import__") = Dict["__import__"]::Exp ... Importlib rule (. => Dict[S] = ref(S)) ~> bootstrap(Dict, (SetItem(S) => .) _) diff --git a/python-semantics-io.k b/python-semantics-io.k index d98baad..84665c8 100644 --- a/python-semantics-io.k +++ b/python-semantics-io.k @@ -54,7 +54,7 @@ module PYTHON-SEMANTICS-IO syntax #Id ::= "DEFAULT_BUFFER_SIZE" rule invokeBuiltin(obj("_IOBase.__new__",_), ListItem(Cls) L:List, M:Map) => newHelper(Cls, ref("_IOBase"), SetItem("FileIO") SetItem("BytesIO") SetItem("BufferedReader") SetItem("BufferedWriter") SetItem("BufferedRandom") SetItem("BufferedRWPair") SetItem("TextIOWrapper") SetItem("StringIO") SetItem("IncrementalNewlineDecoder")) ~> mutable("closed" |-> ref("False"), Cls) rule invokeBuiltin(obj("_IOBase.__iter__",_), ListItem(Self), .) => Self - rule invokeBuiltin(obj("_IOBase.close",_), ListItem(Self), .) => if getref(Self, "closed"): pass else: (Self . String2Id("flush")(.Arguments) ; ~> setref(id(Self), "closed", ref("True"))) ~> ref("None") + rule invokeBuiltin(obj("_IOBase.close",_), ListItem(Self), .) => if getref(Self, "closed"): .K else: 'Expr((Self . String2Id("flush")(.Arguments)) ~> setref(id(Self), "closed", ref("True"))) ~> ref("None") rule invokeBuiltin(obj("_IOBase.__enter__",_), ListItem(Self), .) => if getref(Self, "closed") : raiseInternal("ValueError", "I/O operation on closed file") else: Self rule invokeBuiltin(obj("_IOBase.__exit__",_), ListItem(Self:Object) L:List, M:Map) => ref("_IOBase.close")(Self) rule invokeBuiltin(obj("_IOBase.flush",_), ListItem(Self), .) => if getref(Self, "closed"): raiseInternal("ValueError", "I/O operation on closed file") else: ref("None") @@ -69,7 +69,7 @@ module PYTHON-SEMANTICS-IO //StopIteration rule writelines(O:Object, Self) => doWrite(O.__next__(.Arguments), Self) ~> writelines(O, Self) syntax K ::= doWrite(Exp, Exp) [strict] - rule doWrite(O:Object, Self) => Self . write(O) ; + rule doWrite(O:Object, Self) => 'Expr(Self . write(O)) rule invokeBuiltin(obj("_IOBase.fileno",_), ListItem(Self), .) => raise ref("UnsupportedOperation")("fileno") rule invokeBuiltin(obj("_IOBase.readline",_), ListItem(Self), .) => ref("_IOBase.readline")(Self, ref("None")) rule invokeBuiltin(obj("_IOBase.readline",_), ListItem(Self) ListItem(Limit), .) => test(Limit is None, readLine(Self, -1), readLine(Self, ref(id(Limit)))) @@ -84,7 +84,7 @@ module PYTHON-SEMANTICS-IO syntax K ::= readLines(Exp, Exp, Exp) [strict(1, 3)] rule readLines(S, L, R) => ref("index")(L ::Exp) ~> readLines(S, HOLE, R) when isInt(L) =/=K true [heat] rule O ~> readLines(S, HOLE, R) => readLines(S, intvalue(O), R) [cool] - rule readLines(Self, Hint:Int, List:Object) => try: List . extend(Self . __next__(.Arguments)) ; except ref("StopIteration"): ref(id(List)) else: if Hint - ref("len")(List[-1]) < 0 and bool(Hint >=Int 0) : ref(id(List)) else: readLines(Self, Hint - ref("len")(List[-1]), List) + rule readLines(Self, Hint:Int, List:Object) => try: 'Expr(List . extend(Self . __next__(.Arguments))) except ref("StopIteration"): ref(id(List)) else: if Hint - ref("len")(List[-1]) < 0 and bool(Hint >=Int 0) : ref(id(List)) else: readLines(Self, Hint - ref("len")(List[-1]), List) rule invokeBuiltin(obj("_IOBase.seek",_), ListItem(Self) L:List, M:Map) => raise ref("UnsupportedOperation")("seek") rule invokeBuiltin(obj("_IOBase.tell",_), ListItem(Self), .) => Self . seek(0, 1) @@ -100,7 +100,7 @@ module PYTHON-SEMANTICS-IO rule O ~> doRead(S, HOLE) => doRead(S, intvalue(O)) [cool] rule doRead(Self, N:Int) => test(N Self . readinto(ByteArray) ; ~> ref("bytes")(ref(id(ByteArray))) + rule doRead(Self, _, ByteArray:Object) => 'Expr(Self . readinto(ByteArray)) ~> ref("bytes")(ref(id(ByteArray))) rule invokeBuiltin(obj("_RawIOBase.readall",_), ListItem(Self), .) => readAll(Self . read(ref("_io") . DEFAULT_BUFFER_SIZE), b "", Self) syntax Exp ::= readAll(Exp, Exp, Exp) [strict] rule readAll(O:Object, Bytes, Self) => test(O is None, test(strvalue(Bytes) ==String "", ref("None"), Bytes), test(istype(O, ref("bytes")), test(strvalue(O) ==String "", Bytes, readAll(Self . read(ref("_io") . DEFAULT_BUFFER_SIZE), Bytes + O, Self)), raiseInternal("TypeError", "read() should return bytes"))) diff --git a/python-semantics-iterators.k b/python-semantics-iterators.k index 128123a..d6d8150 100644 --- a/python-semantics-iterators.k +++ b/python-semantics-iterators.k @@ -19,7 +19,7 @@ module PYTHON-SEMANTICS-ITERATORS ... "__value__" |-> list(.) ... ... - rule invokeBuiltin(obj("iter_next",_), ListItem(obj(B,_)), .) => try: (getmember(B2, "__getitem__", true, false, true) (I:Int)) except ref("IndexError"): (setx(.Obj) ~> raise ref("StopIteration")) else: pass ... + rule invokeBuiltin(obj("iter_next",_), ListItem(obj(B,_)), .) => try: (getmember(B2, "__getitem__", true, false, true) (I:Int)) except ref("IndexError"): (setx(.Obj) ~> raise ref("StopIteration")) else: .K ... ... B ... "__index__" |-> (I => I +Int 1) "__value__" |-> B2 ... diff --git a/python-semantics-logic.k b/python-semantics-logic.k index 1078cf6..763adbd 100644 --- a/python-semantics-logic.k +++ b/python-semantics-logic.k @@ -14,6 +14,7 @@ module PYTHON-SEMANTICS-LOGIC syntax Test ::= Exp "=/=Obj" Exp [strict] syntax Test ::= Test "or" Test [strict(1), left] + syntax K ::= "if" Test ":" K "else" ":" K [strict(1)] syntax Test ::= Exp "is" "None" [strict] //TODO: is None / is not None @@ -33,6 +34,8 @@ module PYTHON-SEMANTICS-LOGIC rule test(true, K:K, _) => K rule test(false, _, K) => K + rule if true: K else: _ => K + rule if false: _ else: K => K rule (O:Object -> _) => O rule map(M:Map) -> _ => map(M) diff --git a/python-semantics-macros.k b/python-semantics-macros.k index a0db7cc..050aff1 100644 --- a/python-semantics-macros.k +++ b/python-semantics-macros.k @@ -11,7 +11,7 @@ module PYTHON-SEMANTICS-MACROS rule assert E => if __debug__ : if not E : raise AssertionError [macro] rule assert E , E2 => if __debug__ : if not E : raise AssertionError(E2 ::Exp) [macro] - rule if E ::Exp : S => if E : S else : pass [macro] + rule if E ::Exp : S => if E : S else : .K [macro] rule return => return ref("None") [macro] rule yield => yield ref("None") [macro] @@ -29,12 +29,12 @@ module PYTHON-SEMANTICS-MACROS rule declName(def X:Id ( _ ) -> _ : _) => X rule declName(def X ( _ ) : _) => X rule declName(class X ( _ ) : _) => X - rule declName(K newline _) => declName(K) + rule declName(K ; _) => declName(K) - rule @ K ::Exp K2:K => K2 newline declName(K2) = K(declName(K2)) [macro] + rule @ K ::Exp _:NEWLINE K2:K => K2 ?Newline:NEWLINE declName(K2) = K(declName(K2)) [macro] rule try: Try ExceptClauses else: Else finally: Finally => try: try: Try ExceptClauses else: Else finally: Finally [macro] - rule try: Try ExceptClauses => try: Try ExceptClauses else: pass [macro] + rule try: Try ExceptClauses => try: Try ExceptClauses else: .K [macro] rule with W, W2, W3 : Body => with W ::Alias : with W2, W3 : Body [macro] diff --git a/python-semantics-objects.k b/python-semantics-objects.k index 1e43fca..aeff24e 100644 --- a/python-semantics-objects.k +++ b/python-semantics-objects.k @@ -13,7 +13,7 @@ module PYTHON-SEMANTICS-OBJECTS rule 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) ... - rule invokeBuiltin(obj("new_object",_), ListItem(O:Object) _, _) => newHelper(O, ref("object"), SetItem("iterator") SetItem("attribute") SetItem("builtin-function") SetItem("builtin-method") SetItem("frame") SetItem("reference")) ~> (if O is not ref("object") : setref(N, "__dict__", {.KeyData}) else: pass) ~> ref(N) ... + rule invokeBuiltin(obj("new_object",_), ListItem(O:Object) _, _) => newHelper(O, ref("object"), SetItem("iterator") SetItem("attribute") SetItem("builtin-function") SetItem("builtin-method") SetItem("frame") SetItem("reference")) ~> (if O is not ref("object") : setref(N, "__dict__", {.KeyData}) else: .K) ~> ref(N) ... N => N +Int 1 (. => N diff --git a/python-semantics-statements.k b/python-semantics-statements.k index 12cd478..a0c5318 100644 --- a/python-semantics-statements.k +++ b/python-semantics-statements.k @@ -61,10 +61,10 @@ module PYTHON-SEMANTICS-STATEMENTS rule [unroll-for]: lmark ~> for Target:Target in O : Ss else: Ss2 => try: (((Target) = getmember(O, "__next__", true, false, true) (.Arguments)) ~> Ss ~> lmark ~> for Target in O : Ss else: Ss2) except ref("StopIteration"): Ss2 else: . - rule O:Object ; => . + rule 'Expr(O:Object) => . - rule Stmt:K newline Ss => Stmt ~> Ss when Ss =/=K .Stmts - rule Stmt:K newline .Stmts => Stmt [macro] + rule Stmt:K ; Ss => Stmt ~> Ss when Ss =/=K .StmtList + rule Stmt:K ; .StmtList => Stmt [macro] rule with O:Object : Ss => doWith(O . String2Id("__exit__"), O . String2Id("__enter__") (.Arguments), ., Ss) rule with O:Object as T:Exp : Ss => doWith(O . String2Id("__exit__"), O . String2Id("__enter__") (.Arguments), T, Ss) @@ -74,11 +74,11 @@ module PYTHON-SEMANTICS-STATEMENTS rule isKResult(O:KResult as _) => true // we copy from python-semantics-try.k so we can reuse finally functionality and still choose whether we suppress a raised exception - rule (doWith(Exit:Object, Enter:Object, T, Ss) => #if T ==K . #then . #else T ::Target = Enter #fi ~> Ss ~> popfinally ~> Exit(* ref("sys_exc_info")(.Arguments)) ;) ~> K + rule (doWith(Exit:Object, Enter:Object, T, Ss) => #if T ==K . #then . #else T ::Target = Enter #fi ~> Ss ~> popfinally ~> Expr(Exit(* ref("sys_exc_info")(.Arguments)))) ~> K (. => ListItem(finally(if not Exit(* ref("sys_exc_info")(.Arguments)): raise else: (setx(Ex) ~> K), C, XL, LL, FL, Ex))) XL:List - (. => ListItem(finally(Exit(* ref("sys_exc_info")(.Arguments)) ;, C, XL, LL, FL, Ex))) LL:List - (. => ListItem(finally(Exit(* ref("sys_exc_info")(.Arguments)) ;, C, XL, LL, FL, Ex))) FL:List + (. => ListItem(finally('Expr(Exit(* ref("sys_exc_info")(.Arguments))), C, XL, LL, FL, Ex))) LL:List + (. => ListItem(finally('Expr(Exit(* ref("sys_exc_info")(.Arguments))), C, XL, LL, FL, Ex))) FL:List Ex C:Bag diff --git a/python-semantics-syntax.k b/python-semantics-syntax.k index 8964775..ddb0fae 100644 --- a/python-semantics-syntax.k +++ b/python-semantics-syntax.k @@ -23,8 +23,6 @@ module PYTHON-SEMANTICS-SYNTAX rule isKResult(list(_)) => true rule isKResult(map(_)) => true - syntax Stmt ::= Exp - syntax Test ::= Bool syntax ObjRef ::= Object syntax K ::= "list" "(" List ")" @@ -35,4 +33,8 @@ module PYTHON-SEMANTICS-SYNTAX rule isValue(map(_)) => true rule isExp(map(_)) => true + syntax NEWLINE ::= "newline" + syntax INDENT ::= "indent" + syntax DEDENT ::= "dedent" + endmodule diff --git a/python-semantics-try.k b/python-semantics-try.k index f1ee655..b3374d3 100644 --- a/python-semantics-try.k +++ b/python-semantics-try.k @@ -122,7 +122,7 @@ module PYTHON-SEMANTICS-TRY rule doExcepts(., Except, X) => . ... rule doExcepts(ListItem(B) L:List, Except, X) => doExcept(B, Except, X) ~> doExcepts(L, Except, X) ... - rule doExcept(Type:Object, Except, X) => test(istype(B, Type), test(Id2String(X) ==String "", except: Except, ((X:Id)::Target = B ~> except: (try: Except finally: try: unbind(X) except ref("NameError"): pass))), .) ... + rule doExcept(Type:Object, Except, X) => test(istype(B, Type), test(Id2String(X) ==String "", except: Except, ((X:Id)::Target = B ~> except: (try: Except finally: try: unbind(X) except ref("NameError"): .K))), .) ... B:Exp rule invokeBuiltin(obj("sys_exc_info",_), ., .) => tuple(#if Ex ==K ref("None") #then ref("None") #else Ex . String2Id("__class__") #fi, Ex, #if Ex ==K ref("None") diff --git a/python-syntax.k b/python-syntax.k index 16474d9..b56656a 100644 --- a/python-syntax.k +++ b/python-syntax.k @@ -140,7 +140,16 @@ module PYTHON-SYNTAX imports PYTHON-TOKENS syntax ExceptClauses ::= NeList{ExceptClause,""} - syntax Stmt ::= Exp ";" [strict, klabel('Expr)] //TODO: subsort + syntax Suite ::= StmtList NEWLINE | NEWLINE INDENT Stmts DEDENT + syntax Stmt ::= StmtList NEWLINE | CompoundStmt + syntax Stmts ::= NeList{Stmt,""} + + //TODO: add lexer rules + syntax NEWLINE + syntax INDENT + syntax DEDENT + + syntax SimpleStmt ::= Exp [strict, klabel('Expr), onlyLabel] //TODO: remove onlyLabel | AssignTargets "=" Exp [strict(2)] | Target "+=" Exp [strict(2)] | Target "-=" Exp [strict(2)] @@ -171,39 +180,38 @@ module PYTHON-SYNTAX imports PYTHON-TOKENS | "global" NAMES | "nonlocal" NAMES //TODO: elif - > "if" Exp ":" Stmts - | "if" Exp ":" Stmts "else" ":" Stmts [strict(1)] - | "while" Exp ":" Stmts - | "while" Exp ":" Stmts "else" ":" Stmts - | "for" Target "in" Exp ":" Stmts - | "for" Target "in" Exp ":" Stmts "else" ":" Stmts - | "try" ":" Stmts ExceptClauses - | "try" ":" Stmts ExceptClauses "else" ":" Stmts //"finally" ":" Stmts - | "try" ":" Stmts ExceptClauses "else" ":" Stmts "finally" ":" Stmts - | "try" ":" Stmts "finally" ":" Stmts - | "with" Aliases ":" Stmts [strict(1)] - | Decorated - - syntax Stmts ::= Stmt - > List{Stmt,"newline"} - - syntax ExceptClause ::= "except" ":" Stmts - | "except" Exp ":" Stmts [strict(1)] - | "except" Exp "as" NAME ":" Stmts [strict(1)] + syntax CompoundStmt ::= "if" Exp ":" Suite + | "if" Exp ":" Suite "else" ":" Suite [strict(1)] + | "while" Exp ":" Suite + | "while" Exp ":" Suite "else" ":" Suite + | "for" Target "in" Exp ":" Suite + | "for" Target "in" Exp ":" Suite "else" ":" Suite + | "try" ":" Suite ExceptClauses + | "try" ":" Suite ExceptClauses "else" ":" Suite + | "try" ":" Suite ExceptClauses "else" ":" Suite "finally" ":" Suite + | "try" ":" Suite "finally" ":" Suite + | "with" Aliases ":" Suite [strict(1)] + | Decorated + + syntax StmtList ::= List{SimpleStmt,";"} + + syntax ExceptClause ::= "except" ":" Suite + | "except" Exp ":" Suite [strict(1)] + | "except" Exp "as" NAME ":" Suite [strict(1)] syntax Decorated ::= ClassDef | FuncDef - | "@" Exp Decorated [strict(1)] + | "@" Exp NEWLINE Decorated [strict(1)] syntax Parameters ::= List{Parameter,","} [seqstrict] syntax Parameter ::= Argument | Argument ":" Exp [klabel('annotation)] | "*" - syntax FuncDef ::= "def" NAME "(" Parameters ")" "->" Exp ":" Stmts - | "def" NAME "(" Parameters ")" ":" Stmts + syntax FuncDef ::= "def" NAME "(" Parameters ")" "->" Exp ":" Suite + | "def" NAME "(" Parameters ")" ":" Suite - syntax ClassDef ::= "class" NAME "(" Arguments ")" ":" Stmts [strict(2)] + syntax ClassDef ::= "class" NAME "(" Arguments ")" ":" Suite [strict(2)] endmodule