diff --git a/machine-integers.k b/machine-integers.k index 478db29..4d42309 100644 --- a/machine-integers.k +++ b/machine-integers.k @@ -1,7 +1,7 @@ module MACHINE-INTEGERS syntax Int ::= mult(Int, Int, Int) [function] - rule mult(I:Int, I2:Int, N:Nat) => wrap(I *Int I2, N) [function, anywhere] + rule mult(I:Int, I2:Int, N:Int) => wrap(I *Int I2, N) [function, anywhere] syntax Int ::= add(Int, Int, Int) [function] rule add(I, I2, N) => wrap(I +Int I2, N) diff --git a/python-semantics-assignment.k b/python-semantics-assignment.k index ee555a5..27b2bc9 100644 --- a/python-semantics-assignment.k +++ b/python-semantics-assignment.k @@ -7,6 +7,7 @@ module PYTHON-SEMANTICS-ASSIGNMENT | "unbindList" "(" List ")" rule (. => bind(X:Id, ref(B:ObjId))) ~> (X , Ts:Expressions => Ts) := obj(B,_) + rule (. => bind(X:Id, .Obj)) ~> (X, Ts:Expressions => Ts) := .Obj rule (. => bindList(Listify(Ts2), O, false)) ~> (tuple(Ts2:Expressions) , Ts => Ts) := O:Object rule (. => bindList(Listify(Ts2), O, false)) ~> ([ Ts2 ] , Ts => Ts) := O rule (. => ref("setattr")(O, Id2String(X), O2) ;) ~> ((O:Object . X:Id) , Ts => Ts) := O2:Object @@ -29,7 +30,7 @@ module PYTHON-SEMANTICS-ASSIGNMENT context del ((K [ HOLE ]) , _) when isKResult(K) rule (. => iterate(O, .)) ~> bindList(_, O, _) - rule (. => T, .Expressions := O) ~> list((ListItem(O) => .) _) ~> bindList((ListItem(T:Target) => .) _, _, _) when getKLabel T =/=KLabel '*_ + rule (. => T, .Expressions := O) ~> list((ListItem(O) => .) _) ~> bindList((ListItem(T:Expression) => .) _, _, _) when getKLabel T =/=KLabel '*_ rule (. => T, .Expressions := 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") diff --git a/python-semantics-attribute-ref.k b/python-semantics-attribute-ref.k index c8f75b6..8d46acf 100644 --- a/python-semantics-attribute-ref.k +++ b/python-semantics-attribute-ref.k @@ -13,21 +13,53 @@ module PYTHON-SEMANTICS-ATTRIBUTE-REF rule [attribute]: O:Object . X:Id => ref("getattr")(O, Id2String(X), .Arguments) - rule invokeBuiltin(obj("getattr",_), ListItem(O) ListItem(S:Object), .) => 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), .) => try: ref("getattr")(O, S) except ref("AttributeError") : Default else: pass - rule invokeBuiltin(obj("hasattr",_), ListItem(O) ListItem(S), .) => try: (ref("getattr")(O, S, .Arguments) ; ~> ref("True")) except ref("AttributeError") : ref("False") else: pass - - rule invokeBuiltin(obj("getattribute_object",_), ListItem(O) ListItem(O2:Object), .) => 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), .) => checkData(getmember(O, O2, false, false, false), O) -> getmember(O, O2, true, true, true) - - rule checkData(O:Object, O2:Object) => test((getmember(O, "__set__", false, false, false) -> getmember(O, "__delete__", false, false, false)) ==Obj .Obj, .Obj, descriptor(O, O2, gettype(O2), false)) - rule checkData(.Obj, _) => .Obj - - rule getmember(O:Object, O2, T:Bool, T2:Bool, true) => getmember(O, O2, T, T2, false) -> raiseInternal("AttributeError", "object has no attribute '" +String strvalue(O2) +String "'") - rule getmember(O:Object, O2, true, false, false) => descriptor(getmember(O, O2, false, false, false), O, gettype(O), false) - rule getmember(O:Object, O2, false, true, false) => basesLookup(getref(O, "__mro__"), O2) -> getmember(O, O2, false, false, false) - rule getmember(O:Object, O2, true, true, false) => descriptor(basesLookup(getref(O, "__mro__"), O2), O, gettype(O), true) -> getmember(O, O2, true, false, false) - rule getmember(O:Object, O2, false, false, false) => basesLookup(getref2(gettype(O), "__mro__"), O2) + rule invokeBuiltin("getattr", _) => try: + (try: + return getmember(String2Id("object"), "__getattribute__", true, false, true)(String2Id("name")) + except ref("AttributeError") : + (if hasmember(String2Id("object"), "__getattr__") : + return getmember(String2Id("object"), "__getattr__", true, false, true) (String2Id("name")) + else: + raise)) + except ref("AttributeError") : + (if String2Id("default") ==Obj .Obj : + raise + else: + return String2Id("default")) + + //rule invokeBuiltin(obj("hasattr",_), ListItem(O) ListItem(S), .) => try: (ref("getattr")(O, S, .Arguments) ; ~> ref("True")) except ref("AttributeError") : ref("False") else: pass + + rule invokeBuiltin("object.__getattribute__",_) => (if hasmember(String2Id("self"), String2Id("name")) : + String2Id("data"), .Expressions := getmember(String2Id("self"), String2Id("name"), false, false, true) newline + (if hasmember(String2Id("data"), "__set__") or hasmember(String2Id("data"), "__delete__") : + return descriptor(String2Id("data"), String2Id("self"), gettype(String2Id("self")), false) + else: pass) + else: pass) newline + String2Id("val"), .Expressions := mapLookup(String2Id("self"), String2Id("name")) newline + (if String2Id("val") =/=Obj .Obj : + return String2Id("val") + else: pass) newline + return getmember(String2Id("self"), String2Id("name"), true, false, true) + + + rule invokeBuiltin("type.__getattribute__",_) => (if hasmember(String2Id("self"), String2Id("name")) : + String2Id("data"), .Expressions := getmember(String2Id("self"), String2Id("name"), false, false, true) newline + (if hasmember(String2Id("data"), "__set__") or hasmember(String2Id("data"), "__delete__") : + return descriptor(String2Id("data"), String2Id("self"), gettype(String2Id("self")), false) + else: pass) + else: pass) newline + return getmember(String2Id("self"), String2Id("name"), true, true, true) + + syntax Test ::= checkMember(Expression) [strict] + rule hasmember(O:Object, O2:Object) => checkMember(getmember(O, O2, false, false, false)) -> false + rule checkMember(.Obj) => .Obj + rule checkMember(O:Object) => true + + rule getmember(O:Object, O2:Object, T:Bool, T2:Bool, true) => getmember(O, O2, T, T2, false) -> raiseInternal("AttributeError", "object has no attribute '" +String strvalue(O2) +String "'") + rule getmember(O:Object, O2:Object, true, false, false) => descriptor(getmember(O, O2, false, false, false), O, gettype(O), false) + rule getmember(O:Object, O2:Object, false, true, false) => basesLookup(getref(O, "__mro__"), O2) -> getmember(O, O2, false, false, false) + rule getmember(O:Object, O2:Object, true, true, false) => descriptor(basesLookup(getref(O, "__mro__"), O2), O, gettype(O), true) -> getmember(O, O2, true, false, false) + rule getmember(O:Object, O2:Object, false, false, false) => basesLookup(getref2(gettype(O), "__mro__"), O2) rule mapLookup(obj(B,_), O) => try: K[O] except ref("KeyError") : .Obj else: pass ... @@ -62,9 +94,9 @@ module PYTHON-SEMANTICS-ATTRIBUTE-REF //TODO: add super rule descriptor(O:Object, O2:Object, _, true) => (getmember(O, "__get__", false, false, false) ( O , ref("None") , O2, .Arguments)) -> O rule descriptor(O:Object, O2:Object, Type:Object, false) => (getmember(O, "__get__", false, false, false) ( O , O2 , Type, .Arguments )) -> O ... - ... "None" |-> None:Int ... when id(O2) =/=K None + ... "None" |-> NoneId ... when id(O2) =/=K NoneId rule descriptor(O:Object, O2:Object, Type:Object, false) => (getmember(O, "__get__", false, false, false) (O, O2, O2, .Arguments)) -> O ... - ... "None" |-> None:Int ... when id(O2) ==K None + ... "None" |-> NoneId ... when id(O2) ==K NoneId rule setmember(O:Object, Name:Object, Value:Object) => checkDataSet(getmember(O, Name, false, false, false), O, Value) -> mapInsert(O, Name, Value) -> raiseInternal("AttributeError", "object has no attribute '" +String strvalue(Name) +String "'") diff --git a/python-semantics-boolean-ops.k b/python-semantics-boolean-ops.k index 47b0f78..29314a7 100644 --- a/python-semantics-boolean-ops.k +++ b/python-semantics-boolean-ops.k @@ -14,18 +14,34 @@ module PYTHON-SEMANTICS-BOOLEAN-OPS 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("new_bool",_), ListItem(O), .) => newHelper(O, ref("bool"), .) ~> ref("False") - rule invokeBuiltin(obj("new_bool",_), ListItem(O:Object) ListItem(O2:Object), .) => newHelper(O, ref("bool"), .) ~> bool(O2) - - 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()") + rule bool(O:Object) => ref("bool")(O) + //rule invokeBuiltin(obj("new_bool",_), ListItem(O), .) => newHelper(O, ref("bool"), .) ~> ref("False") + //rule invokeBuiltin(obj("new_bool",_), ListItem(O:Object) ListItem(O2:Object), .) => newHelper(O, ref("bool"), .) ~> bool(O2) + rule invokeBuiltin("bool.__new__",_) => newHelper(String2Id("cls"), ref("bool"), .) newline + if plbool(String2Id("x") is ref("None")): + return ref("False") + else: + if hasmember(String2Id("x"), "__bool__") : + String2Id("bool"), .Expressions := getmember(String2Id("x"), "__bool__", true, false, true) (.Arguments) newline + if istype(String2Id("bool"), ref("bool")): + return String2Id("bool") + else: + raiseInternal("TypeError", "__bool__ should return bool") + else: + if hasmember(String2Id("x"), "__len__") : + return ref("len")(String2Id("x")) != 0 + else: + return ref("True") + + rule invokeBuiltin("len",_) => if hasmember(String2Id("s"), "__len__") : + String2Id("len"), .Expressions := getmember(String2Id("s"), "__len__", true, false, true) (.Arguments) newline + String2Id("len"), .Expressions := ref("index")(String2Id("len")) newline + if plbool(String2Id("len") >= 0) : + return String2Id("len") + else: + raiseInternal("ValueError", "__len__() should return >= 0") + else: + raiseInternal("TypeError", "object has no len()") syntax Test ::= plbool(Expression) [strict] rule plbool(obj(_, ... "__value__" |-> I:Int ...)) => I =/=Int 0 [function, anywhere] diff --git a/python-semantics-builtin-functions.k b/python-semantics-builtin-functions.k index 006fe23..b7b6408 100644 --- a/python-semantics-builtin-functions.k +++ b/python-semantics-builtin-functions.k @@ -3,9 +3,10 @@ require "python-semantics-common.k" module PYTHON-SEMANTICS-BUILTIN-FUNCTIONS imports PYTHON-SEMANTICS-COMMON - syntax K ::= doAll(Expression) [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("all",_) => (for String2Id("element") in String2Id("iterable") : + if String2Id("element") : + return ref("True") + else: pass) ~> + return ref("False") endmodule diff --git a/python-semantics-builtin-modules.k b/python-semantics-builtin-modules.k index d03a642..1ceb5a1 100644 --- a/python-semantics-builtin-modules.k +++ b/python-semantics-builtin-modules.k @@ -1,36 +1,42 @@ -require "python-semantics-common.k" +require "python-semantics-functions.k" module PYTHON-SEMANTICS-BUILTIN-MODULES - imports PYTHON-SEMANTICS-COMMON + imports PYTHON-SEMANTICS-FUNCTIONS syntax K ::= "builtins" | "resolve" | "modules" | "importlib" | "object" ObjId "(" String "," List "," Map "," Map ")" - | "incref" "(" List "," Int ")" - | "incref" "(" ObjId "," Int ")" + | "incref" "(" ObjId "," Set ")" | "genv" "(" String "," String ")" | "module" ObjId "(" Expression ")" [strict(2)] | "struct" ObjId "(" Expressions ")" + | invokeBuiltin(String) - syntax ObjRef ::= "def" String "(" Int "," Int "," Bool ")" + syntax ObjRef ::= "def" String "(" Bool "," Parameters")" syntax ListItem ::= "refs" "(" List ")" - rule incref(B:ObjId,N) => incref(ListItem(B),N) [macro, anywhere] rule refs(ListItem(S) L) => ListItem(ref(S)) refs(L) rule refs(.List) => .List + rule incref(B:ObjId, (SetItem(N) => .) _) ... + ... . => (B, N) ... + + syntax SetItem ::= (ObjId, Int) + + rule incref(B, .) => . + rule initialize(Program:K) => builtins ~> resolve ~> modules ~> importlib ~> executeModule(codeObject(String2Id("__main__"), .Parameters, Program, true), ref("builtins"), {.KeyData}) ... - rule (. => setref(B, "__dict__", { DeMapify(Env:Map) })) ~> resolve ... + rule (. => setref(N, "__dict__", { DeMapify(Env:Map) })) ~> resolve ... ... - B + N:Int Env ... - ... B |-> (1 => 0) ... + ... (N, 1) => . ... 1 rule (. => setref(B, "__bases__", immutable(list(L), ref("tuple")))) ~> resolve ... @@ -38,27 +44,57 @@ module PYTHON-SEMANTICS-BUILTIN-MODULES B ... "__bases__" |-> list(L:List) ... ... - ... B |-> (3 => 2) ... - 3 + ... (B, 4) => . ... + 4 rule (. => setref(B, "__mro__", immutable(getMro(ref(B), getref2(ref(B), "__bases__")), ref("tuple")))) ~> resolve ... ... B ... "__mro__" |-> _ ... ... - ... B |-> (2 => 1) - 2 + ... (B, 3) => . ... + 3 - rule ... (_ |-> 0) => . ... + rule . => setref(S, "__code__", codeObject(String2Id(S), Ps, invokeBuiltin(S), false)) ~> setref(S, "__closure__", ref("None")) ~> setattr(S, "__globals__", .Obj) ~> setref(S, "__defaults__", ref("None")) ~> setref(S, "__kwdefaults__", ref("None")) ~> makeBuiltinDefaults(S, Listify(Ps), false, ., .) ... + ... + S:String + ... "__code__" |-> Ps ... + ... + ... (S, 2) => . ... + 2 + + rule invokeBuiltin(S) => invokeBuiltin(S, M) ... + ref(N) + ... + N + ... "f_locals" |-> map(M) ... + ... + + context invokeBuiltin(_, _ (_ |-> HOLE)) + + syntax K ::= makeBuiltinDefaults(String, List, Bool, List, Map) + rule makeBuiltinDefaults(S, (ListItem(X = K:K) => .) _, false, _ (. => ListItem(K)), _) + rule makeBuiltinDefaults(S, (ListItem(X = K:K) => .) _, true, _, _ (. => Id2String(X) |-> K)) + rule makeBuiltinDefaults(S, (ListItem(X) => .) _, _, _, _) + rule makeBuiltinDefaults(S, (ListItem(* _) => ListItem(*)) _, _, _, _) + rule makeBuiltinDefaults(S, (ListItem(*) => .) _, false => true, _, _) + rule makeBuiltinDefaults(S, (ListItem(** _) => .) _, _, _, _) + rule makeBuiltinDefaults(S, ., _, Defaults, KwDefaults) => setref(S, "__defaults__", immutable(list(Defaults), ref("tuple"))) ~> setref(S, "__kwdefaults__", { DeMapify(KwDefaults) }) rule resolve => . ... - .Map + .Set rule resolve ... - M:Map - N => N -Int 1 when notBool (N in values M) + S:Set + N => N -Int 1 when notBool (N in values S) + + syntax Set ::= "values" Set [function] + rule values ((_, N:Int) S:Set) => SetItem(N) values S + rule values .Set => .Set - rule (. => incref(N, #if S2 ==String "type" #then 3 #else 0 #fi)) ~> object (S:String => N:Int)(S2:String,_,_,_) ... + syntax Set ::= "#if" Bool "#then" Set "#else" Set "#fi" [function] + + rule (. => #if S2 ==String "type" #then incref(N, SetItem(4) SetItem(3) SetItem(1)) #else . #fi) ~> object (S:String => N:Int)(S2:String,_,_,_) ... N => N +Int 1 ... . => ... @@ -101,37 +137,28 @@ module PYTHON-SEMANTICS-BUILTIN-MODULES ... . => S |-> ref(id(O)) ... ... - rule (def S:String(Min:Int, Max:Int, IsMethod:Bool) => ref(S)) ... + rule def S:String(IsMethod, Ps) => incref(S, SetItem(2)) ~> ref(S) ... (. => ... S - "__min__" |-> Min "__max__" |-> Max "__method__" |-> IsMethod "__class__" |-> #if IsMethod #then ref("builtin-method") #else ref("builtin-function") #fi + "__class__" |-> #if IsMethod #then ref("builtin-method") #else ref("builtin-function") #fi "__code__" |-> Ps .Map ...) M:Map => M[S / S] when notBool(S in keys(M)) - rule object N(_,_,_,(S |-> def S2:String(Min, Max, IsMethod) => .) _) ... - ... - N - OAttrs:Map => OAttrs[ref(S2) / S] - ... - (. => ... - S2 - "__min__" |-> Min "__max__" |-> Max "__method__" |-> IsMethod "__class__" |-> #if IsMethod #then ref("builtin-method") #else ref("builtin-function") #fi - .Map - ...) - M => M[S2 / S2] when notBool(S2 in keys(M)) - rule object N(_,_,_,(S |-> K:K => .) _) ... ... N OAttrs => OAttrs[K / S] - ... when getKLabel K =/=KLabel 'ref`(_`) andBool getKLabel K =/=KLabel 'def_`(_`,_`,_`) + ... when isObject(K) =/=K true - rule object N(_,_,_,(S |-> ref(S2) => .) _) ... + rule object N(_,_,_,(S |-> K:K => .) _) ... ... N - OAttrs => OAttrs[ref(S2) / S] - ... + OAttrs => OAttrs[ref(id(K)) / S] + ... when isObject(K) + + + context object N(_,_,_,(S |-> HOLE) _) when getKLabel HOLE ==KLabel 'def_`(_`,_`) rule object N(.,.,.,.) => . ... ... @@ -139,12 +166,6 @@ module PYTHON-SEMANTICS-BUILTIN-MODULES OAttrs ... when "__bases__" in keys(OAttrs) orBool OAttrs:Map("__class__") =/=K ref("type") - rule incref((ListItem(B) => .) _, N2:Int) ... - ... B |-> (N => N +Int N2) ... - rule incref((ListItem(B) => .) _, N2) ... - Ref:Map (. => (B |-> N2)) when notBool(B in keys(Ref)) - rule incref(.List,_) => . - rule module S(O) => ((ref(N) . String2Id("__dict__") ["__name__"]), .Expressions) := S ... N => N +Int 1 (. => ... @@ -154,12 +175,12 @@ module PYTHON-SEMANTICS-BUILTIN-MODULES ... (. => S |-> N) ... ... (. => S |-> N) ... [allocation] - rule (. => incref(N, 3)) ~> struct (S:String => N)(K) ... + rule (. => incref(N, SetItem(4) SetItem(3) SetItem(1))) ~> struct (S:String => N)(K) ... N => N +Int 1 (. => ... N "__class__" |-> ref("type") "__bases__" |-> list(ListItem(ref("tuple"))) "__order__" |-> list(.List) "__name__" |-> S "__mro__" |-> . - "__new__" |-> ref("new_structseq") + "__new__" |-> ref("structseq.__new__") ...) ... (. => S |-> N) ... [allocation] diff --git a/python-semantics-bytes.k b/python-semantics-bytes.k index b25b478..30014bd 100644 --- a/python-semantics-bytes.k +++ b/python-semantics-bytes.k @@ -5,10 +5,10 @@ module PYTHON-SEMANTICS-BYTES //TODO: memoryview - rule invokeBuiltin(obj("new_bytes",_), ListItem(Cls), .) => newHelper(Cls, ref("bytes"), .Set) ~> immutable("", Cls) - rule invokeBuiltin(obj("new_bytes",_), ListItem(Cls) ListItem(Source), .) => test(istype(Source, ref("str")), raiseInternal("TypeError", "string argument without an encoding"), test(istype(Source, ref("int")), immutable(charString(0), Cls) * Source, iterate(Source, .) ~> makebytes(.List, "", Cls))) - rule invokeBuiltin(obj("new_bytes",_), ListItem(Cls) ListItem(Source) ListItem(Encoding), .) => test(istype(Source, ref("str")), Source . String2Id("encode") (Encoding), invokeBuiltin(ref("new_bytes"), ListItem(Cls) ListItem(Source), .)) - rule invokeBuiltin(obj("new_bytes",_), ListItem(Cls) ListItem(Source) ListItem(Encoding) ListItem(Errors), .) => test(istype(Source, ref("str")), Source . String2Id("encode") (Encoding, Errors), invokeBuiltin(ref("new_bytes"), ListItem(Cls) ListItem(Source), .)) + //rule invokeBuiltin(obj("new_bytes",_), ListItem(Cls), .) => newHelper(Cls, ref("bytes"), .Set) ~> immutable("", Cls) + //rule invokeBuiltin(obj("new_bytes",_), ListItem(Cls) ListItem(Source), .) => test(istype(Source, ref("str")), raiseInternal("TypeError", "string argument without an encoding"), test(istype(Source, ref("int")), immutable(charString(0), Cls) * Source, iterate(Source, .) ~> makebytes(.List, "", Cls))) + //rule invokeBuiltin(obj("new_bytes",_), ListItem(Cls) ListItem(Source) ListItem(Encoding), .) => test(istype(Source, ref("str")), Source . String2Id("encode") (Encoding), invokeBuiltin(ref("new_bytes"), ListItem(Cls) ListItem(Source), .)) + //rule invokeBuiltin(obj("new_bytes",_), ListItem(Cls) ListItem(Source) ListItem(Encoding) ListItem(Errors), .) => test(istype(Source, ref("str")), Source . String2Id("encode") (Encoding, Errors), invokeBuiltin(ref("new_bytes"), ListItem(Cls) ListItem(Source), .)) syntax K ::= makebytes(List, String, Object) rule list((ListItem(O) => .) _) ~> makebytes(_ (. => ListItem(ref("index")(O, .Arguments))), _, _) @@ -17,16 +17,16 @@ module PYTHON-SEMANTICS-BYTES rule makebytes((ListItem(O:Object) => .) L, (S => S +String charString(intvalue(O))), _) when all(L, isKResult) rule makebytes(., S, Cls) => immutable(S, Cls) - rule invokeBuiltin(obj("add_bytes",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "bytes", "bytes", b strvalue(O) +String strvalue(O2)) - rule invokeBuiltin(obj("radd_bytes",_), ListItem(O) ListItem(O2), .) => invokeBuiltin(ref("add_bytes"), ListItem(O) ListItem(O2), .) - rule invokeBuiltin(obj("mul_bytes",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "bytes", "int", b strvalue(O) *String intvalue(O2)) - rule invokeBuiltin(obj("rmul_bytes",_), ListItem(O) ListItem(O2), .) => invokeBuiltin(ref("mul_bytes"), ListItem(O) ListItem(O2), .) + //rule invokeBuiltin(obj("add_bytes",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "bytes", "bytes", b strvalue(O) +String strvalue(O2)) + //rule invokeBuiltin(obj("radd_bytes",_), ListItem(O) ListItem(O2), .) => invokeBuiltin(ref("add_bytes"), ListItem(O) ListItem(O2), .) + //rule invokeBuiltin(obj("mul_bytes",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "bytes", "int", b strvalue(O) *String intvalue(O2)) + //rule invokeBuiltin(obj("rmul_bytes",_), ListItem(O) ListItem(O2), .) => invokeBuiltin(ref("mul_bytes"), ListItem(O) ListItem(O2), .) - rule invokeBuiltin(obj("lt_bytes",_), ListItem(O:Object) ListItem(O2:Object), .) => binaryOp(O, O2, "bytes", "bytes", bool(strvalue(O) - rule invokeBuiltin(obj("gt_bytes",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "bytes", "bytes", bool(strvalue(O) >String strvalue(O2))) ... - rule invokeBuiltin(obj("le_bytes",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "bytes", "bytes", bool(strvalue(O) <=String strvalue(O2))) ... - rule invokeBuiltin(obj("ge_bytes",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "bytes", "bytes", bool(strvalue(O) >=String strvalue(O2))) ... - rule invokeBuiltin(obj("eq_bytes",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "bytes", "bytes", bool(strvalue(O) ==String strvalue(O2))) ... - rule invokeBuiltin(obj("ne_bytes",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "bytes", "bytes", bool(strvalue(O) =/=String strvalue(O2))) ... + //rule invokeBuiltin(obj("lt_bytes",_), ListItem(O:Object) ListItem(O2:Object), .) => binaryOp(O, O2, "bytes", "bytes", bool(strvalue(O) + //rule invokeBuiltin(obj("gt_bytes",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "bytes", "bytes", bool(strvalue(O) >String strvalue(O2))) ... + //rule invokeBuiltin(obj("le_bytes",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "bytes", "bytes", bool(strvalue(O) <=String strvalue(O2))) ... + //rule invokeBuiltin(obj("ge_bytes",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "bytes", "bytes", bool(strvalue(O) >=String strvalue(O2))) ... + //rule invokeBuiltin(obj("eq_bytes",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "bytes", "bytes", bool(strvalue(O) ==String strvalue(O2))) ... + //rule invokeBuiltin(obj("ne_bytes",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "bytes", "bytes", bool(strvalue(O) =/=String strvalue(O2))) ... endmodule diff --git a/python-semantics-calls.k b/python-semantics-calls.k index 6df31e9..ff55ed2 100644 --- a/python-semantics-calls.k +++ b/python-semantics-calls.k @@ -12,13 +12,20 @@ module PYTHON-SEMANTICS-CALLS | "addDefault" "(" Expression ")" [strict] | "addKwDefaults" "(" Int "," Expression ")" [strict(2)] | "addKwDefault" "(" Expression ")" [strict] + | "invokeBuiltin" "(" Expression "," List "," Map ")" [strict(1)] + | "invokeFunction" "(" Expression "," List "," Map ")" [strict(1)] syntax Int ::= "numArgs" "(" Object ")" [function] rule numArgs(O) => getattr(O, "co_argcount") +Int getattr(O, "co_kwonlyargcount") +Int ((getattr(O, "co_flags") &Int 4) >>Int 2) +Int ((getattr(O, "co_flags") &Int 8) >>Int 3) [function, anywhere] + //can't use descriptors because method descriptors use it + rule [call]: obj(N:Int,ObjState:Bag) (Args:K) => (getmember(obj(N,ObjState), "__call__", false, false, false) (obj(N,ObjState), Args)) -> (raiseInternal("TypeError", "object is not callable")) rule obj(S:String,ObjState:Bag) (Args:K) => sortArgs(Listify(Args)) ~> processArgs(.,.,.Obj,.Obj) ~> invokeBuiltin(obj(S,ObjState), ., .) ... when isKResult(Args) - rule invokeBuiltin(obj("call_function",_), ListItem(O:Object) L:List, M:Map) => invokeFunction(O, L, M) ... - rule invokeFunction(O, L, M) => matchArgs(O, O . String2Id("__code__"), L, M, ., 0, false, false) ... + rule invokeBuiltin(O:Object, L:List, M:Map) => invokeFunction(O, L, M) ... when isBareFunction(id(O)) =/=K true + rule invokeBuiltin(obj("function.__call__",_), ListItem(O:Object) L, M) => invokeFunction(O, L, M) ... + rule invokeFunction(O, L, M) => matchArgs(O, getref(O, "__code__"), L, M, ., 0, false, false) ... + + rule isBareFunction("function.__call__") => true rule isKResult(_ = K) => true when isKResult(K) [function, anywhere] @@ -37,15 +44,35 @@ module PYTHON-SEMANTICS-CALLS rule (processArgs(L, M:Map, .Obj, .Obj) => .) ~> invokeBuiltin(_, (. => L), (. => M)) //process positional arguments - rule (. => addArg(Code . String2Id("co_varnames") [N:Int], O)) ~> matchArgs(_, Code:Object, (ListItem(O) => .) _, _, _, (N => N +Int 1), _, _) when N (. => addArg(get(L, N), O)) ~> matchArgs(_, obj(Code:ObjId,ObjState:Bag), (ListItem(O) => .) _, _, _, (N => N +Int 1), _, _) ... + ... + Code + ... "co_varnames" |-> ref(Varnames) ... + ... + ... + Varnames + ... "__value__" |-> list(L:List) ... + ... when N addArg(Code . String2Id("co_varnames") [getattr(Code, "co_argcount") +Int getattr(Code, "co_kwonlyargcount")], tuple(DeListify(L:List)))) ~> matchArgs(_, Code:Object, (L => .), _, _, N, (false => true), _) when N >=Int getattr(Code, "co_argcount") andBool (getattr(Code, "co_flags") &Int 4) =/=Int 0 - - rule (addArg(O:Object, O2:Object) => .) ~> matchArgs(_,_,_,_,_ (. => String2Id(strvalue(O)) |-> ref(id(O2))), _, _, _) - rule (addArg(O:Object, O2:Object) => .) ~> addKwArg(_,_,_) ~> matchArgs(_,_,_,_,_ (. => String2Id(strvalue(O)) |-> ref(id(O2))), _, _, _) - rule (addArg(O:Object, O2:Object) => .) ~> addDefaults(_,_) ~> addKwDefaults(_,_) ~> matchArgs(_,_,_,_,_ (. => String2Id(strvalue(O)) |-> ref(id(O2))), _, _, _) - rule (addArg(O:Object, O2:Object) => .) ~> addKwDefaults(_,_) ~> matchArgs(_,_,_,_,_ (. => String2Id(strvalue(O)) |-> ref(id(O2))), _, _, _) + rule (. => addArg(get(L, getattr(obj(Code,ObjState), "co_argcount") +Int getattr(obj(Code,ObjState), "co_kwonlyargcount")), tuple(DeListify(Args:List)))) ~> matchArgs(_, obj(Code:ObjId,ObjState:Bag), (Args => .), _, _, N, (false => true), _) ... + ... + Code + ... "co_varnames" |-> ref(Varnames) ... + ... + ... + Varnames + ... "__value__" |-> list(L:List) ... + ... when N >=Int getattr(obj(Code,ObjState), "co_argcount") andBool (getattr(obj(Code,ObjState), "co_flags") &Int 4) =/=Int 0 + + rule (addArg(O:Object, O2:Object) => .) ~> matchArgs(_,_,_,_,_ (. => strvalue(O) |-> ref(id(O2))), _, _, _) + rule (addArg(O:Object, O2:Object) => .) ~> addKwArg(_,_,_) ~> matchArgs(_,_,_,_,_ (. => strvalue(O) |-> ref(id(O2))), _, _, _) + rule (addArg(O:Object, O2:Object) => .) ~> addDefaults(_,_) ~> addKwDefaults(_,_) ~> matchArgs(_,_,_,_,_ (. => strvalue(O) |-> ref(id(O2))), _, _, _) + rule (addArg(O:Object, O2:Object) => .) ~> addKwDefaults(_,_) ~> matchArgs(_,_,_,_,_ (. => strvalue(O) |-> ref(id(O2))), _, _, _) + rule (addArg(O:Object, .Obj) => .) ~> matchArgs(_,_,_,_,_ (. => strvalue(O) |-> .Obj), _, _, _) + rule (addArg(O:Object, .Obj) => .) ~> addKwArg(_,_,_) ~> matchArgs(_,_,_,_,_ (. => strvalue(O) |-> .Obj), _, _, _) + rule (addArg(O:Object, .Obj) => .) ~> addDefaults(_,_) ~> addKwDefaults(_,_) ~> matchArgs(_,_,_,_,_ (. => strvalue(O) |-> .Obj), _, _, _) + rule (addArg(O:Object, .Obj) => .) ~> addKwDefaults(_,_) ~> matchArgs(_,_,_,_,_ (. => strvalue(O) |-> .Obj), _, _, _) // if there is no vararg, leftover positional arguments raise TypeError rule matchArgs(Function:Object, Code:Object, ListItem(_) L, _, _, N, _, _) => raiseInternal("TypeError", name(Function) + "() takes at most " +String Int2String(getattr(Code, "co_argcount")) +String " positional arguments (" +String Int2String(N +Int lengthList L +Int 1) +String " given)") when N >=Int getattr(Code, "co_argcount") andBool (getattr(Code, "co_flags") &Int 4) ==Int 0 @@ -54,24 +81,48 @@ module PYTHON-SEMANTICS-CALLS rule (. => if S in Code . String2Id("co_varnames") [0 : getattr(Code, "co_argcount") +Int getattr(Code, "co_kwonlyargcount") : ] : addArg(S, O) else: addKwArg(S, O, Code . String2Id("co_varnames") [numArgs(Code) -Int 1])) ~> matchArgs(_, Code:Object, ., (S |-> O => .) _, M, _, _, HasKwarg) when notBool(String2Id(S) in keys(M)) andBool (HasKwarg orBool getattr(Code, "co_flags") &Int 8 ==Int 0) // cannot specify a parameter both positionally and as a keyword - rule matchArgs(Function:Object, Code:Object, ., _ S |-> _, _ X |-> _, _, _, _) => raiseInternal("TypeError", name(Function) + "() got multiple values for keyword argument '" +String S +String "'") when Id2String(X) ==String S + rule matchArgs(Function:Object, Code:Object, ., _ S |-> _, _ X |-> _, _, _, _) => raiseInternal("TypeError", name(Function) + "() got multiple values for keyword argument '" +String S +String "'") when X ==String S // create dict for kwargs if present - rule (. => addArg(Code . String2Id("co_varnames") [numArgs(Code) -Int 1], {.KeyData})) ~> matchArgs(_, Code:Object, _, _, M, _, _, (false => true)) when (getattr(Code, "co_flags") &Int 8) =/=Int 0 + rule (. => addArg(get(L, numArgs(obj(Code,ObjState)) -Int 1), {.KeyData})) ~> matchArgs(_, obj(Code,ObjState:Bag), _, _, M, _, _, (false => true)) ... + ... + Code + ... "co_varnames" |-> ref(Varnames) ... + ... + ... + Varnames + ... "__value__" |-> list(L:List) ... + ... when (getattr(obj(Code,ObjState), "co_flags") &Int 8) =/=Int 0 // fill in default value for unspecified parameter - rule (. => addDefaults(0, ref("len")(Function . String2Id("__defaults__")) if Function . String2Id("__defaults__") is not ref("None") else 0) ~> addKwDefaults(0, Function . String2Id("__kwdefaults__"))) ~> matchArgs(Function:Object,Code:Object, ., ., M, _, HasVararg, HasKwarg) when lengthMap M addDefaults(0, ref("len")(getref(Function, "__defaults__")) if getref(Function, "__defaults__") is not None else 0) ~> addKwDefaults(0, getref(Function, "__kwdefaults__"))) ~> matchArgs(Function:Object,Code:Object, ., ., M, _, HasVararg, HasKwarg) when lengthMap M .) ~> addKwDefaults(_,_) ~> matchArgs(_,Code:Object, _, _, _, _, _, _) when N ==Int getattr(Code, "co_argcount") - rule (. => addDefault(Code . String2Id("co_varnames") [N:Int])) ~> addDefaults(N, O:Object) ~> addKwDefaults(_,_) ~> matchArgs(_,Code:Object, _, _, _, _, _, _) when N addDefaults(N2:Int, O2) ~> addKwDefaults(_,_) ~> matchArgs(Function:Object, Code:Object, _, _, M, N, _, _) => raiseInternal("TypeError", name(Function) + "() takes at least " +String Int2String(getattr(Code, "co_argcount") -Int intvalue(O2)) +String " arguments (" +String Int2String(N) +String " given)") when notBool(String2Id(strvalue(O)) in keys(M)) andBool N2 #if String2Id(strvalue(O)) in keys(M) #then . #else addArg(O, (Function . String2Id("__defaults__") [N -Int getattr(Code, "co_argcount") +Int intvalue(O2)])) #fi) ~> addDefaults((N => N +Int 1), O2) ~> addKwDefaults(_,_) ~> matchArgs(Function:Object, Code:Object, _, _, M, _, _, _) when N >=Int getattr(Code, "co_argcount") -Int intvalue(O2) orBool String2Id(strvalue(O)) in keys(M) + rule (. => addDefault(get(L, N))) ~> addDefaults(N, O:Object) ~> addKwDefaults(_,_) ~> matchArgs(_,obj(Code:ObjId,ObjState:Bag), _, _, _, _, _, _) ... + ... + Code + ... "co_varnames" |-> ref(Varnames) ... + ... + ... + Varnames + ... "__value__" |-> list(L) ... + ... when N addDefaults(N2:Int, O2) ~> addKwDefaults(_,_) ~> matchArgs(Function:Object, Code:Object, _, _, M, N, _, _) => raiseInternal("TypeError", name(Function) + "() takes at least " +String Int2String(getattr(Code, "co_argcount") -Int intvalue(O2)) +String " arguments (" +String Int2String(N) +String " given)") when notBool(strvalue(O) in keys(M)) andBool N2 (addDefault(O:Object) => #if strvalue(O) in keys(M) #then . #else addArg(O, get(L, N -Int getattr(Code, "co_argcount") +Int intvalue(O2))) #fi) ~> addDefaults((N => N +Int 1), O2) ~> addKwDefaults(_,_) ~> matchArgs(obj(Function:ObjId,ObjState:Bag), Code:Object, _, _, M, _, _, _) ... + ... + Function + ... "__defaults__" |-> ref(Defaults) ... + ... + ... + Defaults + ... "__value__" |-> list(L) ... + ... when N >=Int getattr(Code, "co_argcount") -Int intvalue(O2) orBool strvalue(O) in keys(M) rule (addKwDefaults(N, _) => .) ~> matchArgs(_, Code:Object, _, _, _, _, _, _) when N ==Int getattr(Code, "co_kwonlyargcount") rule (. => addKwDefault(Code . String2Id("co_varnames") [N +Int getattr(Code, "co_argcount")])) ~> addKwDefaults((N => N +Int 1), _:Object)~> matchArgs(_, Code:Object, _, _, _, _, _, _) when N #if String2Id(strvalue(O)) in keys(M) #then . #else if O in O2 : addArg(O, O2[O]) else: raiseInternal("TypeError", name(Function) + "() needs keyword-only argument " +String strvalue(O)) #fi) ~> addKwDefaults(_, O2) ~> matchArgs(Function:Object, Code:Object, _, _, M, _, _, _) + rule (addKwDefault(O:Object) => #if strvalue(O) in keys(M) #then . #else if O in O2 : addArg(O, O2[O]) else: raiseInternal("TypeError", name(Function) + "() needs keyword-only argument " +String strvalue(O)) #fi) ~> addKwDefaults(_, O2) ~> matchArgs(Function:Object, Code:Object, _, _, M, _, _, _) context addKwArg(S, _, HOLE) ~> matchArgs(_, Code:Object, _, _, _, _, _, _) when (getattr(Code, "co_flags") &Int 8) =/=Int 0 rule addKwArg(S, _, _) ~> matchArgs(Function:Object, Code:Object, _, _, _, _, _, _) => raiseInternal("TypeError", name(Function) + "() got an unexpected keyword argument '" +String S +String "'") when (getattr(Code, "co_flags") &Int 8) ==Int 0 - rule (addKwArg(S:String, O:Object, O2:Object) => (M:Map(String2Id(strvalue(O2))) [S:String], .Expressions) := O) ~> matchArgs(_, Code:Object, _, _, M, _, _, _) when (getattr(Code, "co_flags") &Int 8) =/=Int 0 + rule (addKwArg(S:String, O:Object, O2:Object) => (M:Map(strvalue(O2)) [S:String], .Expressions) := O) ~> matchArgs(_, Code:Object, _, _, M, _, _, _) when (getattr(Code, "co_flags") &Int 8) =/=Int 0 rule matchArgs(obj(B:ObjId,_),Code:Object,.,.,M,_, HasVararg, HasKwarg) => invoke(ref(B), M) ... when lengthMap M ==Int numArgs(Code) andBool (HasVararg orBool getattr(Code, "co_flags") &Int 4 ==Int 0) andBool (HasKwarg orBool getattr(Code, "co_flags") &Int 8 ==Int 0) @@ -81,11 +132,11 @@ module PYTHON-SEMANTICS-CALLS | makeCells(Expression, Expression, Expression, Int) [strict(1, 2, 3)] | makeCells(List, List, List, Expression, Int) [strict(4)] - rule invoke(obj(_:Int,... "__closure__" |-> Closure "__code__" |-> ref(Code) "__globals__" |-> Globals ...), M) ~> K:K => executeFrame(N, ref(Code), ref(Frame), makeLocals(ref(Code) . String2Id("co_freevars"), Closure), Globals, Globals ["__builtins__"], makeCells(ref(Code) . String2Id("co_freevars"), ref(Code) . String2Id("co_cellvars"), Closure, N), M) ~> return + rule invoke(obj(FuncId,... "__closure__" |-> Closure "__code__" |-> ref(Code) "__globals__" |-> Globals ...), M) ~> K:K => executeFrame(N, ref(Code), Frame, makeLocals(getref2(ref(Code), "co_freevars"), Closure), #if Globals ==K .Obj #then { .KeyData } #else Globals #fi, #if Globals ==K .Obj #then { .KeyData } #else Globals . String2Id("get") ("__builtins__", { .KeyData }) #fi, makeCells(getref2(ref(Code), "co_freevars"), getref2(ref(Code), "co_cellvars"), Closure, N), M, isInt(FuncId) =/=K true) ~> return N => N +Int 1 ... - Frame:Int => N + Frame:K => ref(N) FL => . XC (C:Bag => newFrame) @@ -100,11 +151,11 @@ module PYTHON-SEMANTICS-CALLS syntax Bag ::= "newFrame" rule newFrame => .List .List - rule makeLocals(Free:Object, O:Object) => makeLocals(listvalue(Free), listvalue(O), {.KeyData}) + rule makeLocals(Free:Object, O:Object) => if O is None : makeLocals(listvalue(Free), .List, {.KeyData}) else: makeLocals(listvalue(Free), listvalue(O), {.KeyData}) rule (. => test(getattr2(N2, "cell_contents") ==Obj .Obj, ., (((O[N:K]), .Expressions) := getref2(N2, "cell_contents")))) ~> makeLocals((ListItem(N) => .) _, (ListItem(N2) => .) _, O:Object) rule makeLocals(.List, .List, O:Object) => ref(id(O)) - rule makeCells(Free:Object, Cells:Object, O:Object, N) => makeCells(listvalue(Free), listvalue(Cells), listvalue(O), {.KeyData}, N) + rule makeCells(Free:Object, Cells:Object, O:Object, N) => if O is None : makeCells(listvalue(Free), listvalue(Cells), .List, {.KeyData}, N) else: makeCells(listvalue(Free), listvalue(Cells), listvalue(O), {.KeyData}, N) rule (. => ((O[N:K]), .Expressions) := N2) ~> makeCells((ListItem(N) => .) _, _, (ListItem(N2) => .) _, O:Object, _) rule (. => ((O[N:K]), .Expressions) := ref(N2)) ~> makeCells(_, (ListItem(N) => .) _, _, O:Object, Frame:Int) ... N2 => N2 +Int 1 diff --git a/python-semantics-classes.k b/python-semantics-classes.k index f13e2e3..e76297d 100644 --- a/python-semantics-classes.k +++ b/python-semantics-classes.k @@ -16,16 +16,16 @@ 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"), .Arguments)), N), .) ~> ((Locals["__module__"], .Expressions) := ref("globals")(.Arguments)["__name__"]) ~> (if CO . String2Id("co_consts")[0] is not ref("None") : (Locals["__doc__"], .Expressions) := CO . String2Id("co_consts")[0] else: pass) ~> restoreContext(LL, FL, Back) ~> doCall(Metaclass, ListItem(CO . String2Id("co_name")) ListItem(Bases) ListItem(Locals), 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"), .Arguments)), N), ., false) ~> ((Locals["__module__"], .Expressions) := ref("globals")(.Arguments)["__name__"]) ~> (if CO . String2Id("co_consts")[0] is not ref("None") : (Locals["__doc__"], .Expressions) := CO . String2Id("co_consts")[0] else: pass) ~> restoreContext(LL, FL, Back) ~> doCall(Metaclass, ListItem(CO . String2Id("co_name")) ListItem(Bases) ListItem(Locals), M) ... N => N +Int 1 - Back:Int + ref(Back:Int) FL => . LL => . [allocation] rule restoreContext(LL, FL, N) => . ... _ => FL _ => LL - _ => N + _ => ref(N) rule (processArgs(L:List, M:Map, .Obj, .Obj) => .) ~> invokeClass(_, _, (.Obj => immutable(list(Refify(Idify(L))), ref("tuple"))), (. => stripMetaclass(M))) @@ -39,13 +39,13 @@ module PYTHON-SEMANTICS-CLASSES rule stripMetaclass(S:String |-> K M) => S |-> K stripMetaclass(M) when S=/=String "metaclass" [function, anywhere] rule stripMetaclass(.) => . [function, anywhere] - rule invokeBuiltin(obj("prepare_type",_), _, _) => {.KeyData} + //rule invokeBuiltin(obj("prepare_type",_), _, _) => {.KeyData} - rule invokeBuiltin(obj("new_type",_), ListItem(Type:Object) ListItem(O:Object), _) => newHelper(Type, ref("type"), .Set) ~> getref(O, "__class__") + //rule invokeBuiltin(obj("new_type",_), ListItem(Type:Object) ListItem(O:Object), _) => newHelper(Type, ref("type"), .Set) ~> getref(O, "__class__") - rule invokeBuiltin(obj("new_type",_), ListItem(Type:Object) ListItem(O:Object) ListItem(O2:Object), _) => newHelper(Type, ref("type"), .Set) ~> raiseInternal("TypeError", "type() takes 1 or 3 arguments") + //rule invokeBuiltin(obj("new_type",_), ListItem(Type:Object) ListItem(O:Object) ListItem(O2:Object), _) => newHelper(Type, ref("type"), .Set) ~> raiseInternal("TypeError", "type() takes 1 or 3 arguments") - 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 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) diff --git a/python-semantics-common.k b/python-semantics-common.k index f32590f..888138e 100644 --- a/python-semantics-common.k +++ b/python-semantics-common.k @@ -7,7 +7,7 @@ module PYTHON-SEMANTICS-COMMON initialize($PGM:K) - .K + ref("None") .List ref("None") .List @@ -29,8 +29,8 @@ module PYTHON-SEMANTICS-COMMON .Map .Map .Map - .Map - 3 + .Set + 4 1 $SYSPATH:List $ENVIRON:Map @@ -53,14 +53,19 @@ module PYTHON-SEMANTICS-COMMON | "setref" "(" ObjId "," String "," Expression ")" [strict(3)] | "setenv" "(" ObjId "," Expression "," Expression ")" [strict(2, 3)] | "executeModule" "(" Expression "," Expression "," Expression ")" [strict] - | executeFrame(Int, Expression, Expression, Expression, Expression, Expression, Expression, Map) [strict(2, 3, 4, 5, 6, 7)] - | makeFrame(Int, Expression, Expression, Expression, Expression, Expression, Expression, Map) [strict(2, 3, 4, 5, 6, 7)] + | executeFrame(Int, Expression, Expression, Expression, Expression, Expression, Expression, Map, Bool) [strict(2, 3, 4, 5, 6, 7)] + | makeFrame(Int, Expression, Expression, Expression, Expression, Expression, Expression, Map, Bool) [strict(2, 3, 4, 5, 6, 7)] | setArgs(Int, Map) | getMro(Expression, Expression) [strict] | doBind(String, Expression, Expression) [strict(3)] syntax Test ::= "istype" "(" Expression "," Expression ")" [strict] | "hasbase" "(" K "," Expression ")" [strict] + | "hasmember" "(" Expression "," Expression ")" [strict(1, 2)] + + syntax Bool ::= isBareFunction(ObjId) + + syntax Int ::= hashString(String, Int, Int) [function] // TODO: figure out why the good goddamn fuck it is that if I make ref(K) of sort ObjRef then parsing dicts takes exponential time. syntax Expression ::= "ref" "(" K ")" @@ -72,8 +77,7 @@ module PYTHON-SEMANTICS-COMMON | "binaryOp" "(" Expression "," Expression "," String "," String "," K ")" [strict(1, 2)] | "unaryOp" "(" Expression "," String "," K ")" [strict(1)] | "invoke" "(" Expression "," Map ")" [strict(1)] - | "invokeBuiltin" "(" Expression "," List "," Map ")" [strict(1)] - | "invokeFunction" "(" Expression "," List "," Map ")" [strict(1)] + | invokeBuiltin(String, Map) | "doCall" "(" Expression "," List "," Map ")" | "mutable" "(" Value "," Expression ")" [strict(2)] | "mutable" "(" Map "," Expression ")" [strict(2)] @@ -202,6 +206,9 @@ module PYTHON-SEMANTICS-COMMON syntax List ::= "getl" "(" K ")" [function] rule getl(list(L)) => L [function, anywhere] + syntax Map ::= getm(K) [function] + rule getm(map(M)) => M + syntax K ::= "getattr" "(" Expression "," K ")" [function] rule getattr(obj(_, Attrs:Map ), S:String) => Attrs:Map(S) [function, anywhere] rule getattr(obj(_, Attrs:Map ), S:String[I:Int]) => get(getl(Attrs(S)), I) @@ -266,12 +273,12 @@ module PYTHON-SEMANTICS-COMMON rule hasbase(list(ListItem(N) L), Base) => or(hasbase(N, Base),hasbase(list(L), Base)) rule hasbase(list(.List), Base) => false - rule invokeBuiltin(obj("get_attr",_), ListItem(Self) ListItem(Instance) ListItem(Owner), .) => describe(Self, Instance, Owner, "get_attr") - rule invokeBuiltin(obj("set_attr",_), ListItem(Self) ListItem(Instance) ListItem(Value), .) => doCall(getref(Self, "__set__"), ListItem(Self) ListItem(Instance) ListItem(Value), .) - rule invokeBuiltin(obj("set_ref_default",_), ListItem(Self) ListItem(Instance) ListItem(Value), .) => setref(id(Instance), getattr(Self, "__get__"), Value) ~> ref("None") - rule invokeBuiltin(obj("set_attr_string",_), ListItem(Self) ListItem(Instance) ListItem(Value), .) => test(istype(Value, ref("str")), setattr(id(Instance), getattr(Self, "__get__"), getattr(Value, "__value__")), raiseInternal("TypeError", getattr(Self, "__get__") +String " must be set to a string object")) ~> ref("None") - rule doDescribe(Self, .Obj, _, "get_attr") => Self - rule doDescribe(Self, O:Object, _, "get_attr") => getattr(O, getattr(Self, "__get__")) + rule invokeBuiltin("attribute.__get__", _) => return describe(self, instance, owner, "attribute.__get__") + //rule invokeBuiltin(obj("set_attr",_), ListItem(Self) ListItem(Instance) ListItem(Value), .) => doCall(getref(Self, "__set__"), ListItem(Self) ListItem(Instance) ListItem(Value), .) + //rule invokeBuiltin(obj("set_ref_default",_), ListItem(Self) ListItem(Instance) ListItem(Value), .) => setref(id(Instance), getattr(Self, "__get__"), Value) ~> ref("None") + //rule invokeBuiltin(obj("set_attr_string",_), ListItem(Self) ListItem(Instance) ListItem(Value), .) => test(istype(Value, ref("str")), setattr(id(Instance), getattr(Self, "__get__"), getattr(Value, "__value__")), raiseInternal("TypeError", getattr(Self, "__get__") +String " must be set to a string object")) ~> ref("None") + rule doDescribe(Self, .Obj, _, "attribute.__get__") => Self + rule doDescribe(Self, O:Object, _, "attribute.__get__") => getattr(O, getattr(Self, "__get__")) rule ref(S:String) => ref(N:Int) ... ... S |-> N ... @@ -288,13 +295,13 @@ module PYTHON-SEMANTICS-COMMON N Attrs ... - +/* rule invokeBuiltin(obj(S,... "__min__" |-> N "__max__" |-> N "__method__" |-> T:Bool ...), L, .) => raiseInternal("TypeError", S +String " expected " +String Int2String(N) +String " arguments, got " +String Int2String(lengthList L -Int 1)) ... when (T andBool lengthList L -Int 1 =/=Int N) orBool ((notBool T) andBool lengthList L =/=Int N) rule invokeBuiltin(obj(S,... "__min__" |-> N "__max__" |-> I "__method__" |-> T ...), L, .) => raiseInternal("TypeError", S +String " expected at least " +String Int2String(N) +String " arguments, got " +String Int2String(lengthList L -Int 1)) ... when N =/=Int I andBool ((T andBool lengthList L -Int 1 invokeBuiltin(obj(S,... "__min__" |-> N "__max__" |-> I "__method__" |-> T ...), L, .) => raiseInternal("TypeError", S +String " expected at most " +String Int2String(I) +String " arguments, got " +String Int2String(lengthList L -Int 1)) ... when I >=Int 0 andBool N =/=Int I andBool ((T andBool lengthList L -Int 1 >Int I) orBool ((notBool T) andBool lengthList L >Int I)) - +*/ context list(.) ~> iterate(HOLE,_) rule iterate(O:Object, K) => try: (list(.) ~> iterate(ref("iter") (O, .Arguments), K)) except ref("TypeError") : test(K ==K ., raise, K) else: pass @@ -304,7 +311,6 @@ module PYTHON-SEMANTICS-COMMON rule Lbl:KLabel(Kl:KList) ~> popx => popx ~> Lbl(Kl) when isKResult(Lbl(Kl)) rule mapping(O, K) => iterate(getmember(O, "keys", true, false, false) (.Arguments) -> K, raiseInternal("TypeError", "o.keys() are not iterable")) ~> map(.) ~> mapping(O, K) ... - rule iterate(.Obj, _) ~> map(.) ~> mapping(_, _) => .Obj ... rule list((ListItem(O2:Object) => .) _) ~> (. => addPair(O2, (O [ O2 ]))) ~> map(_) ~> mapping(O,_) ... rule list(_) ~> (addPair(O:Object, O2:Object) => .) ~> map(_ (. => O |-> O2)) ... rule (list(.) => .) ~> map(_) ~> (mapping(_,_) => .) ... @@ -318,7 +324,7 @@ module PYTHON-SEMANTICS-COMMON rule raiseInternal(S, O) => raise mutable("args" |-> undefined(strvalue(O)),ref(S)) - rule executeModule(CO:Object, Builtins:Object, Dict:Object) => (Dict [ "__name__"], .Expressions := CO . String2Id("co_name")) ~> (Dict [ "__doc__" ], .Expressions := CO . String2Id("co_consts") [0]) ~> (Dict [ "__builtins__" ], .Expressions := Builtins) ~> setref(id(CO), "co_names", (getref(CO, "co_varnames") + getref(CO, "co_cellvars") + getref(CO, "co_names"))) ~> setref(id(CO), "co_varnames", tuple(.Expressions)) ~> setref(id(CO), "co_cellvars", tuple(.Expressions)) ~> ref("sys") . String2Id("modules")[CO . String2Id("co_name")], .Expressions := ref(N) ~> executeFrame(N:Int +Int 1, ref(id(CO)), ref("None"), Dict, Dict, Builtins, {.KeyData}, .) ... + rule executeModule(CO:Object, Builtins:Object, Dict:Object) => (Dict [ "__name__"], .Expressions := CO . String2Id("co_name")) ~> (Dict [ "__doc__" ], .Expressions := CO . String2Id("co_consts") [0]) ~> (Dict [ "__builtins__" ], .Expressions := Builtins) ~> setref(id(CO), "co_names", (getref(CO, "co_varnames") + getref(CO, "co_cellvars") + getref(CO, "co_names"))) ~> setref(id(CO), "co_varnames", tuple(.Expressions)) ~> setref(id(CO), "co_cellvars", tuple(.Expressions)) ~> ref("sys") . String2Id("modules")[CO . String2Id("co_name")], .Expressions := ref(N) ~> executeFrame(N:Int +Int 1, ref(id(CO)), ref("None"), Dict, Dict, Builtins, {.KeyData}, ., false) ... N => N +Int 2 (. => ... N @@ -326,16 +332,22 @@ module PYTHON-SEMANTICS-COMMON ...) [allocation] - rule makeFrame(N, CO:Object, Back:Object, Locals:Object, Globals:Object, Builtins:Object, Cells:Object, Args:Map) => setref(N, "f_code", CO) ~> setref(N, "f_back", Back) ~> setref(N, "f_locals", Locals) ~> setref(N, "f_globals", Globals) ~> test(istype(Builtins, ref("module")), setref(N, "f_builtins", Builtins . String2Id("__dict__")), setref(N, "f_builtins", Builtins)) ~> setref(N, "f_cells", Cells) ~> setArgs(N, Args) ... + rule makeFrame(N, CO:Object, Back:Object, Locals:Object, Globals:Object, Builtins:Object, Cells:Object, Args:Map, false) => setref(N, "f_code", CO) ~> setref(N, "f_back", Back) ~> setref(N, "f_locals", Locals) ~> setref(N, "f_globals", Globals) ~> test(istype(Builtins, ref("module")), setref(N, "f_builtins", Builtins . String2Id("__dict__")), setref(N, "f_builtins", Builtins)) ~> setref(N, "f_cells", Cells) ~> setArgs(N, Args) ... + (. => ... + N + "__class__" |-> ref("frame") "f_isbuiltin" |-> false + ...) [allocation] + + rule makeFrame(N, CO:Object, Back:Object, _, _, _, _, Args, true) => setref(N, "f_code", CO) ~> setref(N, "f_back", Back) ~> setattr(N, "f_locals", map(.)) ~> setArgs(N, Args) ... (. => ... N - "__class__" |-> ref("frame") + "__class__" |-> ref("frame") "f_isbuiltin" |-> true ...) [allocation] - rule [executeFrame]: executeFrame(N, CO:Object, Back:Object, Locals:Object, Globals:Object, Builtins:Object, Cells:Object, Args:Map) => makeFrame(N, CO, Back, Locals, Globals, Builtins, Cells, Args) ~> getattr(CO, "co_code") ... - _ => N + rule [executeFrame]: executeFrame(N, CO:Object, Back:Object, Locals:Object, Globals:Object, Builtins:Object, Cells:Object, Args:Map, T:Bool) => makeFrame(N, CO, Back, Locals, Globals, Builtins, Cells, Args, T:Bool) ~> getattr(CO, "co_code") ... + _ => ref(N) - rule (. => doBind(Id2String(X), ref(B), ref(N))) ~> setArgs(N, (X |-> ref(B) => .) _) + rule (. => doBind(X, O, ref(N))) ~> setArgs(N, (X |-> O => .) _) rule [dissolve-setArgs]: setArgs(_, .) => . rule describe(Self, Instance, Owner, S) => doDescribe(Self, Instance, gettype(Instance), S) ... diff --git a/python-semantics-dicts.k b/python-semantics-dicts.k index adb9f8e..b20b8e8 100644 --- a/python-semantics-dicts.k +++ b/python-semantics-dicts.k @@ -3,83 +3,94 @@ require "python-semantics-literals.k" module PYTHON-SEMANTICS-DICTS imports PYTHON-SEMANTICS-LITERALS - rule invokeBuiltin(obj("keys_dict",_), ListItem(obj(B:ObjId,_)), .) => mutable("_mapping" |-> ref(B), ref("dict_keys")) - - rule invokeBuiltin(obj("iter_dict_keys",_), ListItem(obj(_, ... "_mapping" |-> ref(B) ...)), .) => mutable("_mapping" |-> ref(B) "__revision__" |-> N:Int "__order__" |-> list(sorted(DeSetify(keys M))) "__index__" |-> 0 "__index2__" |-> 0, ref("iterator")) ... - ... - B - ... "__revision__" |-> N "__value__" |-> map(M:Map) ... - ... - - rule invokeBuiltin(obj("iter_next",_), ListItem(obj(B2,_)), .) => raiseInternal("RuntimeError", "dictionary changed size during iteration") ... - ... - B2 - ... "__revision__" |-> Rev1 "_mapping" |-> ref(B:ObjId) ... - ... - ... - B - ... "__revision__" |-> Rev2:Int ... - ... when Rev1 =/=Int Rev2 - - rule invokeBuiltin(obj("iter_next",_), ListItem(obj(B2,_)), .) => raise ref("StopIteration") ... - ... - B2 - ... "__revision__" |-> Rev "__order__" |-> list(L) "__index__" |-> (Idx) "_mapping" |-> ref(B:ObjId) ... - ... - ... - B - ... "__revision__" |-> Rev ... - ... when Idx ==Int lengthList L - - rule invokeBuiltin(obj("iter_next",_), ListItem(obj(B,_)), .) ... - ... - B - ... "__revision__" |-> Rev "__order__" |-> list(L) "__index__" |-> (Idx => Idx +Int 1) "__index2__" |-> (Idx2:Int => 0) "_mapping" |-> ref(B2:ObjId) ... - ... - ... - B2 - ... "__revision__" |-> Rev "__value__" |-> map(M) ... - ... when Idx =/=Int lengthList L andBool Idx2 ==Int lengthList getl(M:Map(get(L, Idx))) [structural] - - rule invokeBuiltin(obj("iter_next",_), ListItem(obj(B,_)), .) => key(get(getl(M:Map(get(L:List, Idx))), Idx2)) ... - ... - B - ... "__revision__" |-> Rev "__order__" |-> list(L) "__index__" |-> Idx "__index2__" |-> (Idx2:Int => Idx2 +Int 1) "_mapping" |-> ref(B2:ObjId) ... - ... - ... - B2 - ... "__revision__" |-> Rev "__value__" |-> map(M) ... - ... when Idx =/=Int lengthList L andBool Idx2 =/=Int lengthList getl(M:Map(get(L, Idx))) - - rule invokeBuiltin(obj("iter_dict",_), ListItem(O), .) => ((O . String2Id("keys")) (.Arguments) . String2Id("__iter__")) (.Arguments) - - rule invokeBuiltin(obj("len_dict",_), ListItem(O), .) => lengthMap mapvalue(O) - - rule invokeBuiltin(obj("getitem_dict",_), ListItem(obj(B,_)) ListItem(Key:Object), .) => ref("hash")(Key) ~> tableLookup(B, 0, Key) - rule (O:Object => .) ~> tableLookup(_,(_ => intvalue(O)),_) - rule (O:Object => .) ~> tableLookup(_,(_ => intvalue(O)),_) ; - - rule invokeBuiltin(obj("setitem_dict",_), ListItem(O) ListItem(Key) ListItem(Value:Object), .) => processDict(O, Key |-> Value) ; ~> ref("None") - - rule invokeBuiltin(obj("delitem_dict",_), ListItem(obj(B,_)) ListItem(Key), .) => ref("hash")(Key, .Arguments) ~> tableDelete(B, 0, Key) ~> ref("None") + //rule invokeBuiltin(obj("keys_dict",_), ListItem(obj(B:ObjId,_)), .) => mutable("_mapping" |-> ref(B), ref("dict_keys")) + + //rule invokeBuiltin(obj("iter_dict_keys",_), ListItem(obj(_, ... "_mapping" |-> ref(B) ...)), .) => mutable("_mapping" |-> ref(B) "__revision__" |-> N:Int "__order__" |-> list(sorted(DeSetify(keys M))) "__index__" |-> 0 "__index2__" |-> 0, ref("iterator")) ... + // ... + // B + // ... "__revision__" |-> N "__value__" |-> map(M:Map) ... + // ... + + //rule invokeBuiltin(obj("iter_next",_), ListItem(obj(B2,_)), .) => raiseInternal("RuntimeError", "dictionary changed size during iteration") ... + // ... + // B2 + // ... "__revision__" |-> Rev1 "_mapping" |-> ref(B:ObjId) ... + // ... + // ... + // B + // ... "__revision__" |-> Rev2:Int ... + // ... when Rev1 =/=Int Rev2 + + //rule invokeBuiltin(obj("iter_next",_), ListItem(obj(B2,_)), .) => raise ref("StopIteration") ... + // ... + // B2 + // ... "__revision__" |-> Rev "__order__" |-> list(L) "__index__" |-> (Idx) "_mapping" |-> ref(B:ObjId) ... + // ... + // ... + // B + // ... "__revision__" |-> Rev ... + // ... when Idx ==Int lengthList L + + //rule invokeBuiltin(obj("iter_next",_), ListItem(obj(B,_)), .) ... + // ... + // B + // ... "__revision__" |-> Rev "__order__" |-> list(L) "__index__" |-> (Idx => Idx +Int 1) "__index2__" |-> (Idx2:Int => 0) "_mapping" |-> ref(B2:ObjId) ... + // ... + // ... + // B2 + // ... "__revision__" |-> Rev "__value__" |-> map(M) ... + // ... when Idx =/=Int lengthList L andBool Idx2 ==Int lengthList getl(M:Map(get(L, Idx))) [structural] + + //rule invokeBuiltin(obj("iter_next",_), ListItem(obj(B,_)), .) => key(get(getl(M:Map(get(L:List, Idx))), Idx2)) ... + // ... + // B + // ... "__revision__" |-> Rev "__order__" |-> list(L) "__index__" |-> Idx "__index2__" |-> (Idx2:Int => Idx2 +Int 1) "_mapping" |-> ref(B2:ObjId) ... + // ... + // ... + // B2 + // ... "__revision__" |-> Rev "__value__" |-> map(M) ... + // ... when Idx =/=Int lengthList L andBool Idx2 =/=Int lengthList getl(M:Map(get(L, Idx))) + + //rule invokeBuiltin(obj("iter_dict",_), ListItem(O), .) => ((O . String2Id("keys")) (.Arguments) . String2Id("__iter__")) (.Arguments) + + //rule invokeBuiltin(obj("len_dict",_), ListItem(O), .) => lengthMap mapvalue(O) + + //rule invokeBuiltin(obj("getitem_dict",_), ListItem(obj(B,_)) ListItem(Key:Object), .) => ref("hash")(Key) ~> tableLookup(B, 0, Key) + rule invokeBuiltin("dict.__getitem__",_) => return tableLookup(String2Id("self"), ref("hash")(String2Id("key")), String2Id("key")) + rule invokeBuiltin("dict.__setitem__","self" |-> Self:Object "key" |-> Key:Object "value" |-> Value:Object) => processDict(Self, Key |-> Value) ; ~> return ref("None") + + //rule invokeBuiltin(obj("delitem_dict",_), ListItem(obj(B,_)) ListItem(Key), .) => ref("hash")(Key, .Arguments) ~> tableDelete(B, 0, Key) ~> ref("None") rule (O:Object => .) ~> tableDelete(_,(_ => intvalue(O)),_) syntax K ::= makeDict(Int, Expression) [strict(2)] - rule invokeBuiltin(obj("new_dict",_), ListItem(O) _, .) => newHelper(O, ref("dict"), .) ~> {.KeyData} - rule invokeBuiltin(obj("init_dict",_), ListItem(_:Object), .) => ref("None") - rule invokeBuiltin(obj("init_dict",_), ListItem(O) ListItem(O2:Object), .) => mapping(O2, .Obj) -> iterate(O2, .) ~> makeDict(0, O) - - rule (. => O[Key:K], .Expressions := Value) ~> map((Key |-> Value => .) _) ~> makeDict(_, O) - rule map(.) ~> makeDict(_, O) => ref("None") - - rule list(_) ~> (. => map(.)) ~> makeDict(_, _) ... - rule (. => iterate(O, raiseInternal("TypeError", "cannot convert dictionary update sequence element #" +String Int2String(N) +String "to a sequence"))) ~> list((ListItem(O) => .) _) ~> map(_) ~> makeDict(N, _) ... - rule (list(ListItem(O) ListItem(O2)) => .) ~> list(_) ~> map(_ (. => O |-> O2)) ~> makeDict(N => N +Int 1, _) ... - rule list(L) ~> list(_) ~> map(_) ~> makeDict(N, _) => raiseInternal("ValueError", "dictionary update sequence element #" +String Int2String(N) +String " has length " +String Int2String(lengthList L) +String "; 2 is required") ... - rule (list(.) => .) ~> map(_) ~> makeDict(_, _) ... - - rule invokeBuiltin(obj("eq_dict",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "dict", "dict", equalDict(O, O2)) + syntax #Id ::= "cls" | "__next__" | "kwargs" + rule invokeBuiltin("dict.__new__",_) => newHelper(cls, ref("dict"), .) ~> return {.KeyData} + rule invokeBuiltin("dict.__init__",_) => if String2Id("") =/=Obj .Obj : + if hasmember(String2Id(""), "keys") : + for String2Id("key") in getmember(String2Id(""), "keys", true, false, true) : + self[String2Id("key")] := String2Id("") [ String2Id("key") ] + else: + for String2Id("tuple") in String2Id("") : + (try: + String2Id("iter") := ref("iter")(String2Id("tuple")) + except ref("TypeError") : + raiseInternal("TypeError", "cannot convert dictionary update sequence element to a sequence")) newline + (try: + String2Id("key") := String2Id("iter") . __next__ (.Arguments) newline + String2Id("value") := String2Id("iter") . __next__ (.Arguments) + except ref("StopIteration") : + raiseInternal("TypeError", "dictionary update sequence element has length less than 2; 2 is required")) newline + self[String2Id("key")] := String2Id("value") newline + (try: + String2Id("iter") . __next__ (.Arguments) newline + raiseInternal("TypeError", "dictionary update sequence element has length greater than 2; 2 is required") + except ref("StopIteration") : pass) ~> + for String2Id("key") in kwargs: + self[String2Id("key")] := kwargs[String2Id("key")] ~> + return ref("None") + + //rule invokeBuiltin(obj("eq_dict",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "dict", "dict", equalDict(O, O2)) syntax ObjRef ::= equalDict(Expression, Expression) [strict] rule equalDict(O:Object, O2) => bool(lengthList DeSetify(keys(mapvalue(O))) ==Int lengthList DeSetify(keys(mapvalue(O2)))) and equalDict(mapvalue(O), O2) @@ -87,6 +98,6 @@ module PYTHON-SEMANTICS-DICTS rule equalDict(Key |-> Value M, 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) ~> tableLookup(id(Dict), 0, Key) ; ~> ref("True")) except ref("KeyError"): ref("False") else: pass endmodule diff --git a/python-semantics-dunder-builtin.k b/python-semantics-dunder-builtin.k index 2e3f0b6..cf672b9 100644 --- a/python-semantics-dunder-builtin.k +++ b/python-semantics-dunder-builtin.k @@ -13,7 +13,7 @@ module PYTHON-SEMANTICS-DUNDER-BUILTIN "args" |-> ref("args") "__cause__" |-> ref("__cause__") "__context__" |-> ref("__context__") - "__new__" |-> def "BaseException.__new__" (1, -1, false) + "__new__" |-> def "BaseException.__new__" (false, String2Id("cls"), * String2Id("args"), ** String2Id("kwargs")) "__suppress_context__" |-> ref("__suppress_context__") "__traceback__" |-> ref("__traceback__") ,.) ~> @@ -31,7 +31,7 @@ module PYTHON-SEMANTICS-DUNDER-BUILTIN object "ImportError"("type",ListItem("Exception"), "name" |-> ref("name") "path" |-> ref("path") - "__init__" |-> def "ImportError.__init__"(0, -1, true) + "__init__" |-> def "ImportError.__init__"(true, String2Id("self"), * String2Id("args")) ,.) ~> object "name"("attribute",.,.,"__get__" |-> "name") ~> object "path"("attribute",.,.,"__get__" |-> "path") ~> @@ -60,140 +60,140 @@ 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) ;) ~> + (def "all"(false, String2Id("iterable")) ;) ~> object "bool"("type",ListItem("int"), - "__new__" |-> def "new_bool" (1, 2, false) + "__new__" |-> def "bool.__new__" (false, String2Id("cls"), String2Id("x") = ref("False")) ,.) ~> object "bytes"("type",ListItem("object"), - "__add__" |-> def "add_bytes"(1, 1, true) - "__eq__" |-> def "eq_bytes"(1, 1, true) - "__ge__" |-> def "ge_bytes" (1, 1, true) - "__gt__" |-> def "gt_bytes" (1, 1, true) - "__le__" |-> def "le_bytes" (1, 1, true) - "__lt__" |-> def "lt_bytes" (1, 1, true) - "__mul__" |-> def "mul_bytes" (1, 1, true) - "__ne__" |-> def "ne_bytes" (1, 1, true) - "__new__" |-> def "new_bytes" (0, 3, true) - "__radd__" |-> def "radd_bytes"(1, 1, true) - "__rmul__" |-> def "rmul_bytes" (1, 1, true) +// "__add__" |-> def "add_bytes"(1, 1, true) +// "__eq__" |-> def "eq_bytes"(1, 1, true) +// "__ge__" |-> def "ge_bytes" (1, 1, true) +// "__gt__" |-> def "gt_bytes" (1, 1, true) +// "__le__" |-> def "le_bytes" (1, 1, true) +// "__lt__" |-> def "lt_bytes" (1, 1, true) +// "__mul__" |-> def "mul_bytes" (1, 1, true) +// "__ne__" |-> def "ne_bytes" (1, 1, true) + "__new__" |-> def "bytes.__new__" (false, String2Id("cls"), String2Id("source") = 0, String2Id("encoding") = .Obj, String2Id("errors") = .Obj) +// "__radd__" |-> def "radd_bytes"(1, 1, true) +// "__rmul__" |-> def "rmul_bytes" (1, 1, true) ,.) ~> object "classmethod"("type", ListItem("object"), - "__get__" |-> def "get_classmethod"(1, 2, true) - "__init__" |-> def "init_classmethod"(1, 1, true) - "__new__" |-> def "new_classmethod"(2, 2, false) +// "__get__" |-> def "get_classmethod"(1, 2, true) + "__init__" |-> def "classmethod.__init__"(true, String2Id("self"), String2Id("function")) + "__new__" |-> def "classmethod.__new__"(false, String2Id("cls"), String2Id("function")) ,.) ~> - (def "compile"(3, 6, false) ;) ~> + (def "compile"(false, String2Id("source"), String2Id("filename"), String2Id("mode"), String2Id("flags") = 0, String2Id("dont_inherit") = ref("False"), String2Id("optimize") = -1) ;) ~> object "complex"("type",ListItem("object"),.,.) ~> object "dict"("type",ListItem("object"), - "get" |-> def "get_dict" (1, 2, true) - "keys" |-> def "keys_dict" (0, 0, true) - "update" |-> ref("init_dict") - "__contains__" |-> def "contains_dict" (1, 1, true) - "__delitem__" |-> def "delitem_dict" (1, 1, true) - "__eq__" |-> def "eq_dict" (1, 1, true) - "__getitem__" |-> def "getitem_dict" (1, 1, true) - "__init__" |-> def "init_dict" (0, 1, true) - "__iter__" |-> def "iter_dict" (0, 0, true) - "__len__" |-> def "len_dict" (0, 0, true) - "__new__" |-> def "new_dict" (1, -1, false) - "__setitem__" |-> def "setitem_dict" (2, 2, true) +// "get" |-> def "get_dict" (1, 2, true) +// "keys" |-> def "keys_dict" (0, 0, true) + "update" |-> ref("dict.__init__") +// "__contains__" |-> def "contains_dict" (1, 1, true) +// "__delitem__" |-> def "delitem_dict" (1, 1, true) +// "__eq__" |-> def "eq_dict" (1, 1, true) + "__getitem__" |-> def "dict.__getitem__"(true, String2Id("self"), String2Id("key")) + "__init__" |-> def "dict.__init__" (true, String2Id("") = .Obj, ** String2Id("kwarg")) +// "__iter__" |-> def "iter_dict" (0, 0, true) +// "__len__" |-> def "len_dict" (0, 0, true) + "__new__" |-> def "dict.__new__" (false, String2Id("cls"), * String2Id("args"), ** String2Id("kwargs")) + "__setitem__" |-> def "dict.__setitem__"(true, String2Id("self"), String2Id("key"), String2Id("value")) ,.) ~> object "dict_keys" ("type",ListItem("object"), - "__iter__" |-> def "iter_dict_keys" (0, 0, true) - ,.) ~> +// "__iter__" |-> def "iter_dict_keys" (0, 0, true) +. ,.) ~> object "float"("type",ListItem("object"), - "__eq__" |-> def "eq_float"(1, 1, true) - "__ge__" |-> def "ge_float" (1, 1, true) - "__gt__" |-> def "gt_float" (1, 1, true) - "__le__" |-> def "le_float" (1, 1, true) - "__lt__" |-> def "lt_float" (1, 1, true) - "__ne__" |-> def "ne_float" (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) ;) ~> +// "__eq__" |-> def "eq_float"(1, 1, true) +// "__ge__" |-> def "ge_float" (1, 1, true) +// "__gt__" |-> def "gt_float" (1, 1, true) +// "__le__" |-> def "le_float" (1, 1, true) +// "__lt__" |-> def "lt_float" (1, 1, true) +// "__ne__" |-> def "ne_float" (1, 1, true) +. ,.) ~> + (def "format" (false, String2Id("value"), String2Id("format_spec") = "") ;) ~> + (def "getattr" (false, String2Id("object"), String2Id("name"), String2Id("default") = .Obj) ;) ~> + (def "globals" (false, .Parameters) ;) ~> + (def "hasattr" (false, String2Id("object"), String2Id("name")) ;) ~> + (def "hash" (false, String2Id("object")) ;) ~> + (def "id"(false, String2Id("object")) ;) ~> + (def "index" (false, String2Id("a")) ;) ~> object "int"("type",ListItem("object"), - "__abs__" |-> def "abs_int" (0, 0, true) - "__add__" |-> def "add_int" (1, 1, true) - "__and__" |-> def "and_int" (1, 1, true) - "__bool__" |-> def "bool_int" (0, 0, true) - "__ceil__" |-> def "ceil_int" (0, 0, true) +// "__abs__" |-> def "abs_int" (0, 0, true) + "__add__" |-> def "int.__add__"(true, String2Id("self"), String2Id("other")) +// "__and__" |-> def "and_int" (1, 1, true) + "__bool__" |-> def "int.__bool__"(true, String2Id("self")) +// "__ceil__" |-> def "ceil_int" (0, 0, true) //TODO: divmod, doc - "__eq__" |-> def "eq_int"(1, 1, true) + "__eq__" |-> def "int.__eq__"(true, String2Id("self"), String2Id("other")) //TODO: float - "__floor__" |-> def "floor_int" (0, 0, true) - "__floordiv__" |-> def "floordiv_int" (1, 1, true) +// "__floor__" |-> def "floor_int" (0, 0, true) +// "__floordiv__" |-> def "floordiv_int" (1, 1, true) //TODO: format - "__ge__" |-> def "ge_int" (1, 1, true) + "__ge__" |-> def "int.__ge__"(true, String2Id("self"), String2Id("other")) //TODO: getattribute, getnewargs - "__gt__" |-> def "gt_int" (1, 1, true) - "__hash__" |-> def "hash_int" (0, 0, true) - "__index__" |-> ref("int_int") - "__int__" |-> def "int_int" (0, 0, true) - "__invert__" |-> def "invert_int" (0, 0, true) - "__le__" |-> def "le_int" (1, 1, true) - "__lshift__" |-> def "lshift_int" (1, 1, true) - "__lt__" |-> def "lt_int" (1, 1, true) - "__mod__" |-> def "mod_int" (1, 1, true) - "__mul__" |-> def "mul_int" (1, 1, true) - "__ne__" |-> def "ne_int" (1, 1, true) - "__neg__" |-> def "neg_int" (0, 0, true) - "__new__" |-> def "new_int" (1, 3, false) - "__or__" |-> def "or_int" (1, 1, true) - "__pos__" |-> def "pos_int" (0, 0, true) - "__pow__" |-> def "pow_int" (1, 2, true) - "__radd__" |-> def "radd_int" (1, 1, true) - "__rand__" |-> def "rand_int" (1, 1, true) + "__gt__" |-> def "int.__gt__"(true, String2Id("self"), String2Id("other")) +// "__hash__" |-> def "hash_int" (0, 0, true) + "__index__" |-> def "int.__index__"(true, String2Id("self")) +// "__int__" |-> def "int_int" (0, 0, true) +// "__invert__" |-> def "invert_int" (0, 0, true) + "__le__" |-> def "int.__le__"(true, String2Id("self"), String2Id("other")) +// "__lshift__" |-> def "lshift_int" (1, 1, true) + "__lt__" |-> def "int.__lt__"(true, String2Id("self"), String2Id("other")) +// "__mod__" |-> def "mod_int" (1, 1, true) +// "__mul__" |-> def "mul_int" (1, 1, true) + "__ne__" |-> def "int.__ne__"(true, String2Id("self"), String2Id("other")) +// "__neg__" |-> def "neg_int" (0, 0, true) + "__new__" |-> def "int.__new__" (false, String2Id("cls"), String2Id("x") = 0, String2Id("base") = .Obj) +// "__or__" |-> def "or_int" (1, 1, true) +// "__pos__" |-> def "pos_int" (0, 0, true) +// "__pow__" |-> def "pow_int" (1, 2, true) + "__radd__" |-> def "int.__radd__"(true, String2Id("self"), String2Id("other")) +// "__rand__" |-> def "rand_int" (1, 1, true) //TODO: rdivmod, repr - "__rfloordiv__" |-> def "rfloordiv_int" (1, 1, true) - "__rlshift__" |-> def "rlshift_int" (1, 1, true) - "__rmod__" |-> def "rmod_int" (1, 1, true) - "__rmul__" |-> def "rmul_int" (1, 1, true) - "__ror__" |-> def "ror_int" (1, 1, true) +// "__rfloordiv__" |-> def "rfloordiv_int" (1, 1, true) +// "__rlshift__" |-> def "rlshift_int" (1, 1, true) +// "__rmod__" |-> def "rmod_int" (1, 1, true) +// "__rmul__" |-> def "rmul_int" (1, 1, true) +// "__ror__" |-> def "ror_int" (1, 1, true) //TODO: round - "__rpow__" |-> def "rpow_int" (1, 1, true) - "__rrshift__" |-> def "rrshift_int" (1, 1, true) - "__rshift__" |-> def "rshift_int" (1, 1, true) - "__rsub__" |-> def "rsub_int" (1, 1, true) - "__rtruediv__" |-> def "rtruediv_int" (1, 1, true) - "__rxor__" |-> def "rxor_int" (1, 1, true) +// "__rpow__" |-> def "rpow_int" (1, 1, true) +// "__rrshift__" |-> def "rrshift_int" (1, 1, true) +// "__rshift__" |-> def "rshift_int" (1, 1, true) +// "__rsub__" |-> def "rsub_int" (1, 1, true) +// "__rtruediv__" |-> def "rtruediv_int" (1, 1, true) +// "__rxor__" |-> def "rxor_int" (1, 1, true) //TODO: sizeof, str - "__sub__" |-> def "sub_int" (1, 1, true) - "__truediv__" |-> def "truediv_int" (1, 1, true) - "__trunc__" |-> def "trunc_int" (0, 0, true) - "__xor__" |-> def "xor_int" (1, 1, true) +// "__sub__" |-> def "sub_int" (1, 1, true) +// "__truediv__" |-> def "truediv_int" (1, 1, true) +// "__trunc__" |-> def "trunc_int" (0, 0, true) +// "__xor__" |-> def "xor_int" (1, 1, true) //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) ;) ~> + (def "isinstance" (false, String2Id("object"), String2Id("classinfo")) ;) ~> + (def "issubclass" (false, String2Id("class"), String2Id("classinfo")) ;) ~> + (def "iter" (false, String2Id("object"), String2Id("sentinel") = .Obj) ;) ~> object "iterator"("type",ListItem("object"), - "__iter__" |-> def "iter_iter" (0, 0, true) - "__next__" |-> def "iter_next" (0, 0, true) + "__iter__" |-> def "iterator.__iter__" (true, String2Id("self")) + "__next__" |-> def "iterator.__next__" (true, String2Id("self")) ,.) ~> - (def "len" (1, 1, false) ;) ~> + (def "len" (false, String2Id("s")) ;) ~> object "list"("type",ListItem("object"), - "append" |-> def "append_list"(1, 1, true) - "extend" |-> def "extend_list"(1, 1, true) - "__add__" |-> def "add_list" (1, 1, true) - "__eq__" |-> def "eq_list" (1, 1, true) - "__init__" |-> def "init_list" (0, 1, true) - "__iter__" |-> def "get_iter" (0, 0, true) - "__getitem__" |-> def "getitem_list" (1, 1, true) - "__len__" |-> def "len_list" (0, 0, true) - "__ne__" |-> def "ne_list" (1, 1, true) - "__new__" |-> def "new_list" (1, -1, false) - ,.) ~> - (def "locals" (0, 0, false) ;) ~> +// "append" |-> def "append_list"(1, 1, true) +// "extend" |-> def "extend_list"(1, 1, true) +// "__add__" |-> def "add_list" (1, 1, true) +// "__eq__" |-> def "eq_list" (1, 1, true) + "__init__" |-> def "list.__init__" (true, String2Id("self"), String2Id("iterable") = .Obj) +// "__iter__" |-> def "get_iter" (0, 0, true) +// "__getitem__" |-> def "getitem_list" (1, 1, true) +// "__len__" |-> def "len_list" (0, 0, true) +// "__ne__" |-> def "ne_list" (1, 1, true) + "__new__" |-> def "list.__new__" (false, String2Id("cls"), * String2Id("args"), ** String2Id("kwargs")) + ,.) ~> + (def "locals" (false, .Parameters) ;) ~> object "map"("type",ListItem("object"), - "__iter__" |-> ref("iter_iter") - "__new__" |-> def "new_map" (3, -1, false) - "__next__" |-> def "map_next" (0, 0, true) +// "__iter__" |-> ref("iter_iter") + "__new__" |-> def "map.__new__" (false, String2Id("cls"), String2Id("function"), String2Id("iterable"), * String2Id("")) +// "__next__" |-> def "map_next" (0, 0, true) ,.) ~> object "module"("type",ListItem("object"), "__dict__" |-> ref("__dict__module") @@ -201,108 +201,108 @@ module PYTHON-SEMANTICS-DUNDER-BUILTIN object "__dict__module"("attribute",.,., "__get__" |-> "__dict__") ~> object "object"("type",., "__class__" |-> ref("__class__") - "__getattribute__" |-> def "getattribute_object" (1, 1, true) - "__eq__" |-> def "eq_object" (1, 1, true) - "__format__" |-> def "format_object" (1, 1, true) - "__init__" |-> def "init_object" (0, -1, true) - "__ne__" |-> def "ne_object" (1, 1, true) - "__new__" |-> def "new_object" (1, -1, false) - "__setattr__" |-> def "setattr_object"(2, 2, true) - "__subclasshook__" |-> def "subclasshook_object"(0, -1, false) + "__getattribute__" |-> def "object.__getattribute__" (true, String2Id("self"), String2Id("name")) +// "__eq__" |-> def "eq_object" (1, 1, true) +// "__format__" |-> def "format_object" (1, 1, true) + "__init__" |-> def "object.__init__" (true, String2Id("self"), * String2Id("args"), ** String2Id("kwargs")) +// "__ne__" |-> def "ne_object" (1, 1, true) + "__new__" |-> def "object.__new__" (false, String2Id("cls"), String2Id("args"), String2Id("kwargs")) +// "__setattr__" |-> def "setattr_object"(2, 2, true) +// "__subclasshook__" |-> def "subclasshook_object"(0, -1, false) ,.) ~> object "__class__" ("attribute",.,., "__get__" |-> "__class__") ~> - (def "ord" (1, 1, false) ;) ~> + (def "ord" (false, String2Id("c")) ;) ~> object "range" ("type",ListItem("object"), - "__iter__" |-> def "iter_range" (0, 0, true) - "__new__" |-> def "new_range" (1, 4, false) +// "__iter__" |-> def "iter_range" (0, 0, true) + "__new__" |-> def "range.__new__" (false, String2Id("cls"), String2Id("1"), String2Id("2"), String2Id("step") = 1) ,.) ~> object "reversed" ("type", ListItem("object"), - "__new__" |-> def "reversed.__init__"(1, 1, true) + "__new__" |-> def "reversed.__new__"(false, String2Id("cls"), String2Id("seq")) ,.) ~> object "set" ("type", ListItem("object"), - "__contains__" |-> def "contains_set" (1, 1, true) - "__eq__" |-> def "eq_set" (1, 1, true) - "__init__" |-> def "init_set" (0, 1, true) - "__ior__" |-> def "ior_set"(1, 1, true) - "__le__" |-> def "le_set"(1, 1, true) - "__lt__" |-> def "lt_set"(1, 1, true) - "__ne__" |-> def "ne_set"(1, 1, true) - "__new__" |-> def "new_set" (1, -1, false) - ,.) ~> - (def "setattr" (3, 3, false) ;) ~> +// "__contains__" |-> def "contains_set" (1, 1, true) +// "__eq__" |-> def "eq_set" (1, 1, true) + "__init__" |-> def "set.__init__" (true, String2Id("self"), String2Id("iterable") = .Obj) +// "__ior__" |-> def "ior_set"(1, 1, true) +// "__le__" |-> def "le_set"(1, 1, true) +// "__lt__" |-> def "lt_set"(1, 1, true) +// "__ne__" |-> def "ne_set"(1, 1, true) + "__new__" |-> def "set.__new__" (false, String2Id("cls"), * String2Id("args"), ** String2Id("kwargs")) + ,.) ~> + (def "setattr" (false, String2Id("object"), String2Id("name"), String2Id("value")) ;) ~> object "slice" ("type",ListItem("object"), - "indices" |-> def "indices_slice" (1, 1, true) +// "indices" |-> def "indices_slice" (1, 1, true) "start" |-> ref("start") "stop" |-> ref("stop") "step" |-> ref("step") - "__new__" |-> def "new_slice" (1, 4, false) + "__new__" |-> def "slice.__new__" (false, String2Id("cls"), String2Id("1"), String2Id("2"), String2Id("step") = ref("None")) ,.) ~> object "start"("attribute",.,., "__get__" |-> "start") ~> object "stop"("attribute",.,., "__get__" |-> "stop") ~> object "step"("attribute",.,., "__get__" |-> "step") ~> object "staticmethod"("type", ListItem("object"), - "__get__" |-> def "get_staticmethod"(1, 2, true) - "__init__" |-> def "init_staticmethod"(1, 1, true) - "__new__" |-> def "new_staticmethod"(2, 2, false) +// "__get__" |-> def "get_staticmethod"(1, 2, true) + "__init__" |-> def "staticmethod.__init__" (true, String2Id("self"), String2Id("function")) + "__new__" |-> def "staticmethod.__new__"(false, String2Id("cls"), String2Id("function")) ,.) ~> object "str"("type",ListItem("object"), - "format" |-> def "format_str"(0, -1, true) - "join" |-> def "join_str"(1, 1, true) - "lower" |-> def "lower_str"(0, 0, true) - "partition" |-> def "partition_str"(1, 1, true) - "rpartition" |-> def "rpartition_str"(1, 1, true) - "rsplit" |-> def "rsplit_str"(0, 2, true) - "startswith" |-> def "startswith_str"(1, 3, true) - "__add__" |-> def "add_str" (1, 1, true) - "__eq__" |-> def "eq_str" (1, 1, true) - "__format__" |-> def "__format___str"(1, 1, true) - "__hash__" |-> def "hash_str" (0, 0, true) - "__len__" |-> def "len_str"(0, 0, true) - "__mod__" |-> def "mod_str"(1, 1, true) - "__ne__" |-> def "ne_str" (1, 1, true) +// "format" |-> def "format_str"(0, -1, true) +// "join" |-> def "join_str"(1, 1, true) +// "lower" |-> def "lower_str"(0, 0, true) +// "partition" |-> def "partition_str"(1, 1, true) +// "rpartition" |-> def "rpartition_str"(1, 1, true) +// "rsplit" |-> def "rsplit_str"(0, 2, true) +// "startswith" |-> def "startswith_str"(1, 3, true) +// "__add__" |-> def "add_str" (1, 1, true) +// "__eq__" |-> def "eq_str" (1, 1, true) +// "__format__" |-> def "__format___str"(1, 1, true) + "__hash__" |-> def "str.__hash__" (true, String2Id("self")) +// "__len__" |-> def "len_str"(0, 0, true) +// "__mod__" |-> def "mod_str"(1, 1, true) +// "__ne__" |-> def "ne_str" (1, 1, true) ,.) ~> object "super"("type",ListItem("object"), - "__getattribute__" |-> def "super.__getattribute__"(1, 1, true) - "__init__" |-> def "super.__init__"(0, 2, true) +// "__getattribute__" |-> def "super.__getattribute__"(1, 1, true) + "__init__" |-> def "super.__init__"(true, String2Id("self"), String2Id("type") = .Obj, String2Id("object-or-type") = ref("None")) ,.) ~> object "tuple"("type",ListItem("object"), - "__add__" |-> def "add_tuple" (1, 1, true) - "__contains__" |-> def "contains_tuple" (1, 1, true) - "__eq__" |-> def "eq_tuple" (1, 1, true) - "__getitem__" |-> def "getitem_tuple" (1, 1, true) - "__hash__" |-> def "hash_tuple" (0, 0, true) - "__iter__" |-> ref("get_iter") - "__len__" |-> def "len_tuple" (0, 0, true) - "__ne__" |-> def "ne_tuple" (1, 1, true) - "__new__" |-> def "new_tuple" (1, 2, false) + "__add__" |-> def "tuple.__add__" (true, String2Id("self"), String2Id("other")) +// "__contains__" |-> def "contains_tuple" (1, 1, true) +// "__eq__" |-> def "eq_tuple" (1, 1, true) + "__getitem__" |-> def "tuple.__getitem__"(true, String2Id("self"), String2Id("key")) +// "__hash__" |-> def "hash_tuple" (0, 0, true) + "__iter__" |-> def "tuple.__iter__" (true, String2Id("self")) + "__len__" |-> def "tuple.__len__" (true, String2Id("self")) +// "__ne__" |-> def "ne_tuple" (1, 1, true) + "__new__" |-> def "tuple.__new__" (false, String2Id("cls"), String2Id("iterable") = .Obj) ,.) ~> object "type"("type",ListItem("object"), - "mro" |-> def "mro_type"(0, 0, true) +// "mro" |-> def "mro_type"(0, 0, true) "__bases__" |-> ref("__bases__") - "__call__" |-> def "call_type" (0, -1, true) - "__getattribute__" |-> def "getattribute_type" (1, 1, true) - "__instancecheck__" |-> def "instancecheck_type" (1, 1, true) + "__call__" |-> def "type.__call__" (true, String2Id("self"), * String2Id("args"), ** String2Id("kwargs")) + "__getattribute__" |-> def "type.__getattribute__"(true, String2Id("self"), String2Id("name")) +// "__instancecheck__" |-> def "instancecheck_type" (1, 1, true) "__mro__" |-> ref("__mro__") "__name__" |-> ref("__name__type") - "__new__" |-> def "new_type"(2, 4, false) - "__prepare__" |-> def "prepare_type"(0, -1, false) - "__setattr__" |-> def "setattr_type"(2, 2, true) - "__subclasscheck__" |-> def "subclasscheck_type"(1, 1, true) + "__new__" |-> def "type.__new__"(false, String2Id("cls"), String2Id(""), String2Id("bases") = .Obj, String2Id("dict") = .Obj) +// "__prepare__" |-> def "prepare_type"(0, -1, false) +// "__setattr__" |-> def "setattr_type"(2, 2, true) +// "__subclasscheck__" |-> def "subclasscheck_type"(1, 1, true) ,.) ~> object "__name__type" ("attribute",.,., "__get__" |-> "__name__") ~> object "__bases__" ("attribute",.,., "__get__" |-> "__bases__") ~> object "__mro__" ("attribute",.,., "__get__" |-> "__mro__") ~> // module "types" object "attribute"("type",ListItem("object"), - "__get__" |-> def "get_attr" (1, 2, true) - "__set__" |-> def "set_attr" (2, 2, true) - , "__name__" |-> undefined("internal type name")) ~> + "__get__" |-> def "attribute.__get__" (true, String2Id("self"), String2Id("instance"), String2Id("owner") = ref("None")) +// "__set__" |-> def "set_attr" (2, 2, true) +. , "__name__" |-> undefined("internal type name")) ~> object "builtin-function" ("type",ListItem("object"), - "__call__" |-> def "call_builtin_function" (0, -1, true) - , "__name__" |-> undefined("internal type name")) ~> +// "__call__" |-> def "call_builtin_function" (0, -1, true) +. , "__name__" |-> undefined("internal type name")) ~> object "builtin-method" ("type",ListItem("object"), - "__get__" |-> def "get_builtin_method" (1, 2, true) - , "__name__" |-> undefined("internal type name")) ~> + "__get__" |-> def "builtin-method.__get__" (true, String2Id("self"), String2Id("instance"), String2Id("owner") = ref("None")) +. , "__name__" |-> undefined("internal type name")) ~> object "code"("type",ListItem("object"), "co_name" |-> ref("co_name") "co_argcount" |-> ref("co_argcount") @@ -335,17 +335,17 @@ module PYTHON-SEMANTICS-DUNDER-BUILTIN object "f_locals" ("attribute",.,., "__get__" |-> "f_locals") ~> object "function"("type",ListItem("object"), "__annotations__" |-> ref("__annotations__") - "__call__" |-> def "call_function" (0, -1, true) + "__call__" |-> def "function.__call__"(true, String2Id("self"), * String2Id("args"), ** String2Id("kwargs")) "__closure__" |-> ref("__closure__") "__code__" |-> ref("__code__") "__defaults__" |-> ref("__defaults__") "__dict__" |-> ref("__dict__function") "__doc__" |-> ref("__doc__") - "__get__" |-> def "get_function" (1, 2, true) +// "__get__" |-> def "get_function" (1, 2, true) "__globals__" |-> ref("__globals__") "__kwdefaults__" |-> ref("__kwdefaults__") - "__module__" |-> ref("__module__") - "__name__" |-> ref("__name__function") +// "__module__" |-> ref("__module__") +// "__name__" |-> ref("__name__function") ,.) ~> object "__annotations__" ("attribute",.,., "__get__" |-> "__annotations__") ~> object "__closure__" ("attribute",.,., "__get__" |-> "__closure__") ~> @@ -355,17 +355,17 @@ module PYTHON-SEMANTICS-DUNDER-BUILTIN object "__doc__" ("attribute",.,., "__get__" |-> "__doc__" "__set__" |-> ref("set_ref_default")) ~> object "__globals__" ("attribute",.,., "__get__" |-> "__globals__") ~> object "__kwdefaults__" ("attribute",.,., "__get__" |-> "__kwdefaults__") ~> - object "__module__" ("attribute",.,., "__get__" |-> "__module__" "__set__" |-> def "set_ref_default"(3, 3, false)) ~> - object "__name__function"("attribute",.,., "__get__" |-> "__name__" "__set__" |-> def "set_attr_string"(3, 3, false)) ~> +// object "__module__" ("attribute",.,., "__get__" |-> "__module__" "__set__" |-> def "set_ref_default"(3, 3, false)) ~> +// object "__name__function"("attribute",.,., "__get__" |-> "__name__" "__set__" |-> def "set_attr_string"(3, 3, false)) ~> object "generator"("type",ListItem("object"), - "close" |-> def "close_generator"(0, 0, true) - "send" |-> def "send_generator"(1, 1, true) - "throw" |-> def "throw_generator"(1, 3, true) - "__iter__" |-> def "iter_generator"(0, 0, true) - "__next__" |-> def "next_generator"(0, 0, true) - ,.) ~> +// "close" |-> def "close_generator"(0, 0, true) +// "send" |-> def "send_generator"(1, 1, true) +// "throw" |-> def "throw_generator"(1, 3, true) +// "__iter__" |-> def "iter_generator"(0, 0, true) +// "__next__" |-> def "next_generator"(0, 0, true) +. ,.) ~> object "method" ("type", ListItem("object"), - "__call__" |-> def "call_method" (0, -1, true) + "__call__" |-> def "method.__call__" (true, String2Id("self"), * String2Id("args"), ** String2Id("kwargs")) "__func__" |-> ref("__func__") "__self__" |-> ref("__self__") , .) ~> @@ -382,71 +382,71 @@ module PYTHON-SEMANTICS-DUNDER-BUILTIN object "cell"("type",ListItem("object"), ., .) ~> object "cell_contents" ("attribute",.,., "__get__" |-> "cell_contents") ~> - (def "new_structseq" (2, 2, false) ;) ~> + (def "structseq.__new__" (false, String2Id("cls"), String2Id("sequence"), String2Id("dict") = {.KeyData}) ;) ~> //module "sys" - (def "sys_exc_info" (0, 0, false) ;) ~> +// (def "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) ;) ~> +// (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) ;) ~> //module "_io" object "BytesIO"("type", ListItem("_BufferedIOBase"), - "__init__" |-> def "BytesIO.__init__"(0, 1, true) - "readline" |-> def "BytesIO.readline"(0, 1, true) + "__init__" |-> def "BytesIO.__init__"(true, String2Id("self"), String2Id("initial_bytes") = ref("None")) +// "readline" |-> def "BytesIO.readline"(0, 1, true) ,.) ~> object "FileIO"("type", ListItem("_RawIOBase"), - "__init__" |-> def "FileIO.__init__"(1, 4, true) - "read" |-> def "FileIO.read"(0, 1, true) - "write" |-> def "FileIO.write"(1, 1, true) - ,.) ~> + "__init__" |-> def "FileIO.__init__"(true, String2Id("self"), String2Id("name"), String2Id("mode") = "r", String2Id("closefd") = ref("True"), String2Id("opener") = ref("None")) +// "read" |-> def "FileIO.read"(0, 1, true) +// "write" |-> def "FileIO.write"(1, 1, true) +. ,.) ~> object "IncrementalNewlineDecoder"("type", ListItem("object"), - "__init__" |-> def "IncrementalNewlineDecoder.__init__"(2, 3, true) - "decode" |-> def "IncrementalNewlineDecoder.decode"(1, 2, true) - ,.) ~> + "__init__" |-> def "IncrementalNewlineDecoder.__init__"(true, String2Id("self"), String2Id("decoder"), String2Id("translate"), String2Id("errors") = "strict") +// "decode" |-> def "IncrementalNewlineDecoder.decode"(1, 2, true) +. ,.) ~> object "_IOBase"("type", ListItem("object"), - "__new__" |-> def "_IOBase.__new__"(1, -1, false) + "__new__" |-> def "_IOBase.__new__"(false, String2Id("cls"), * String2Id("args"), ** String2Id("kwargs")) ,.) ~> object "_RawIOBase"("type", ListItem("_IOBase"), - "read" |-> def "_RawIOBase.read"(0, 1, true) - ,.) ~> +// "read" |-> def "_RawIOBase.read"(0, 1, true) +. ,.) ~> object "_BufferedIOBase"("type", ListItem("_IOBase"),.,.) ~> //module "_warnings" - (def "_warnings.warn" (1, 3, false) ;) ~> +// (def "_warnings.warn" (1, 3, false) ;) ~> //module "_weakref" object "weakref"("type", ListItem("object"), - "__call__" |-> def "weakref.__call__"(0, 0, true) - "__new__" |-> def "weakref.__new__"(2, 3, false) +// "__call__" |-> def "weakref.__call__"(0, 0, true) + "__new__" |-> def "weakref.__new__"(false, String2Id("cls"), String2Id("object"), String2Id("callback") = ref("None")) ,.) ~> //module "marshal" - (def "marshal.dumps"(1, 2, false) ;) ~> - (def "marshal.loads"(1, 1, false) ;) ~> +// (def "marshal.dumps"(1, 2, false) ;) ~> +// (def "marshal.loads"(1, 1, false) ;) ~> //module "posix" - (def "getcwd"(0, 0, false) ;) ~> - (def "listdir"(0, 1, false) ;) ~> - (def "mkdir"(1, 2, false) ;) ~> - (def "open"(2, 3, false) ;) ~> - (def "replace"(2, 2, false) ;) ~> - (def "stat"(1, 1, false) ;) ~> - (def "unlink"(1, 1, false) ;) ~> +// (def "getcwd"(0, 0, false) ;) ~> +// (def "listdir"(0, 1, false) ;) ~> +// (def "mkdir"(1, 2, false) ;) ~> +// (def "open"(2, 3, false) ;) ~> +// (def "replace"(2, 2, false) ;) ~> +// (def "stat"(1, 1, false) ;) ~> +// (def "unlink"(1, 1, false) ;) ~> .K ) ... @@ -455,26 +455,26 @@ module PYTHON-SEMANTICS-DUNDER-BUILTIN // module declarations module "_imp"({ - "_fix_co_filename": ref("imp__fix_co_filename") - , "acquire_lock" : ref("imp_acquire_lock") - , "extension_suffixes" : ref("imp_extension_suffixes") - , "init_builtin" : ref("imp_init_builtin") - , "init_frozen" : ref("imp_init_frozen") - , "is_builtin" : ref("imp_is_builtin") - , "is_frozen" : ref("imp_is_frozen") - , "is_frozen_package" : ref("imp_is_frozen_package") - , "get_frozen_object" : ref("imp_get_frozen_object") - , "load_dynamic": ref("imp_load_dynamic") - , "release_lock" : ref("imp_release_lock") - }) ~> +// "_fix_co_filename": ref("imp__fix_co_filename") +// , "acquire_lock" : ref("imp_acquire_lock") +// , "extension_suffixes" : ref("imp_extension_suffixes") +// , "init_builtin" : ref("imp_init_builtin") +// , "init_frozen" : ref("imp_init_frozen") +// , "is_builtin" : ref("imp_is_builtin") +// , "is_frozen" : ref("imp_is_frozen") +// , "is_frozen_package" : ref("imp_is_frozen_package") +// , "get_frozen_object" : ref("imp_get_frozen_object") +// , "load_dynamic": ref("imp_load_dynamic") +// , "release_lock" : ref("imp_release_lock") +.KeyData }) ~> module "_io"({ "BytesIO" : ref("BytesIO") , "FileIO" : ref("FileIO") , "IncrementalNewlineDecoder" : ref("IncrementalNewlineDecoder") }) ~> module "_warnings"({ - "warn" : ref("_warnings.warn") - }) ~> +// "warn" : ref("_warnings.warn") +.KeyData }) ~> module "_weakref"({ "ref" : ref("weakref") }) ~> @@ -550,18 +550,18 @@ module PYTHON-SEMANTICS-DUNDER-BUILTIN , "type" : ref("type") }) ~> module "marshal"({ - "dumps" : ref("marshal.dumps") - , "loads" : ref("marshal.loads") - }) ~> +// "dumps" : ref("marshal.dumps") +// , "loads" : ref("marshal.loads") +.KeyData }) ~> module "posix"({ "environ" : {DeMapify(M)} - , "getcwd" : ref("getcwd") - , "listdir" : ref("listdir") - , "mkdir" : ref("mkdir") - , "open" : ref("open") - , "replace" : ref("replace") - , "stat" : ref("stat") - , "unlink" : ref("unlink") +// , "getcwd" : ref("getcwd") +// , "listdir" : ref("listdir") +// , "mkdir" : ref("mkdir") +// , "open" : ref("open") +// , "replace" : ref("replace") +// , "stat" : ref("stat") +// , "unlink" : ref("unlink") , "O_WRONLY" : Constants("posix.O_WRONLY") , "O_CREAT": Constants("posix.O_CREAT") , "O_EXCL": Constants("posix.O_EXCL") @@ -569,7 +569,7 @@ module PYTHON-SEMANTICS-DUNDER-BUILTIN module "sys"({ "builtin_module_names" : ["_imp", "_io", "_warnings", "_weakref", "builtins", "marshal", "posix", "sys", "types", .Expressions] , "dont_write_bytecode" : ref("True") - , "exc_info" : ref("sys_exc_info") +// , "exc_info" : ref("sys_exc_info") , "flags": ref("sys.flags")(tuple(#if Constants("__debug__") #then 0 #else 1 #fi, #if Constants("PYTHONVERBOSE") #then 1 #else 0 #fi, .Expressions)) , "hash_info" : ref("sys.hash_info")(tuple(Constants("sys.hash_info.width"), Constants("sys.hash_info.modulus"), Constants("sys.hash_info.inf"), Constants("sys.hash_info.nan"), Constants("sys.hash_info.imag"), .Expressions)) , "hexversion": 50528496 diff --git a/python-semantics-environment.k b/python-semantics-environment.k index 6ca7660..5429645 100644 --- a/python-semantics-environment.k +++ b/python-semantics-environment.k @@ -1,17 +1,17 @@ -require "python-semantics-common.k" +require "python-semantics-literals.k" module PYTHON-SEMANTICS-ENVIRONMENT - imports PYTHON-SEMANTICS-COMMON + imports PYTHON-SEMANTICS-LITERALS syntax ObjRef ::= "envLookup" "(" String "," Expression "," Expression ")" [strict(2, 3)] syntax K ::= "doBind2" "(" String "," Expression "," Expression "," Expression ")" [strict(3, 4)] rule unbind(X) => bind(X, ref(0)) [macro, anywhere] rule bind(X:Id, B:Expression) => doBind(Id2String(X), B, ref(N)) ... - N + ref(N) - rule X:Id => envLookup(Id2String(X),ref(N),ref(N) . String2Id("f_code")) ... - N:Int + rule X:Id => envLookup(Id2String(X),ref(N),getref2(ref(N), "f_code")) ... + ref(N:Int) rule envLookup(S:String, Frame:Object, Code:Object) => (Frame . String2Id("f_locals") [S] @@ -38,8 +38,22 @@ module PYTHON-SEMANTICS-ENVIRONMENT S in Frame . String2Id("f_builtins") else raiseInternal("NameError", "name '" +String S +String "' is not defined") + when notBool getattr(Frame, "f_isbuiltin") + + rule envLookup(S:String, Frame:Object, Code:Object) => getm(getattr(Frame, "f_locals"))(S) when getattr(Frame, "f_isbuiltin") + + rule doBind(S, B, Frame) => doBind2(S, B, Frame, Frame . String2Id("f_code")) ... when notBool getattr(Frame, "f_isbuiltin") + rule doBind(S, ref(0), obj(Frame,_)) => . ... + ... + Frame + ... "f_isbuiltin" |-> true "f_locals" |-> map(M => M[undef / S]) ... + ... + rule doBind(S, B, obj(Frame,_)) => . ... + ... + Frame + ... "f_isbuiltin" |-> true "f_locals" |-> map(M => M[B / S]) ... + ... when B =/=K ref(0) - rule doBind(S, B, Frame) => doBind2(S, B, Frame, Frame . String2Id("f_code")) rule doBind2(S:String, ref(B:ObjId), Frame:Object, Code:Object) => if S in Code . String2Id("co_varnames") or S in Code . String2Id("co_cellvars") or S in Code . String2Id("co_freevars") : @@ -62,10 +76,12 @@ module PYTHON-SEMANTICS-ENVIRONMENT (((Frame . String2Id("f_globals") [S]), .Expressions) := ref(B))) else: pass - rule [globals]: invokeBuiltin(obj("globals",_), ., .) => ref(N) . String2Id("f_globals") ... - N + syntax #Id ::= "f_globals" | "f_locals" | "f_back" + + rule invokeBuiltin("globals",_) => return Frame . f_back . f_globals ... + Frame - rule invokeBuiltin(obj("locals",_), ., .) => ref(N) . String2Id("f_locals") ... - N + rule invokeBuiltin("locals",_) => return Frame . f_back . f_locals ... + Frame endmodule diff --git a/python-semantics-exceptions.k b/python-semantics-exceptions.k index b90361c..32afdc4 100644 --- a/python-semantics-exceptions.k +++ b/python-semantics-exceptions.k @@ -3,13 +3,10 @@ require "python-semantics-common.k" module PYTHON-SEMANTICS-EXCEPTIONS imports PYTHON-SEMANTICS-COMMON - rule invokeBuiltin(obj("BaseException.__new__",_), ListItem(O) L:List, M:Map) => newHelper(O, ref("BaseException"), .) ~> setref(N, "args", immutable(list(Refify(Idify(L))), ref("tuple"))) ~> ref(N) ... - N => N +Int 1 - (. => - N - "__class__" |-> ref(id(O)) - ) [allocatoin] - - rule invokeBuiltin(obj("ImportError.__init__",_), ListItem(O) _, M:Map) => keywordHelper("ImportError", M, SetItem("name") SetItem("path")) ~> #if "name" in keys(M) #then setref(id(O), "name", M("name")) #else . #fi ~> #if "path" in keys(M) #then setref(id(O), "path", M("path")) #else . #fi ~> ref("None") + rule invokeBuiltin("BaseException.__new__","cls" |-> Cls:Object "args" |-> Args:Object "kwargs" |-> KwArgs:Object) => + newHelper(Cls, ref("BaseException"), .) ~> + return mutable("args" |-> Args, Cls) + + //rule invokeBuiltin(obj("ImportError.__init__",_), ListItem(O) _, M:Map) => keywordHelper("ImportError", M, SetItem("name") SetItem("path")) ~> #if "name" in keys(M) #then setref(id(O), "name", M("name")) #else . #fi ~> #if "path" in keys(M) #then setref(id(O), "path", M("path")) #else . #fi ~> ref("None") endmodule diff --git a/python-semantics-floats.k b/python-semantics-floats.k index e0a105a..1f72898 100644 --- a/python-semantics-floats.k +++ b/python-semantics-floats.k @@ -3,11 +3,11 @@ require "python-semantics-boolean-ops.k" module PYTHON-SEMANTICS-FLOATS imports PYTHON-SEMANTICS-BOOLEAN-OPS - rule invokeBuiltin(obj("lt_float",_), ListItem(O:Object) ListItem(O2:Object), .) => binaryOp(O, O2, "float", "float", bool(floatvalue(O) - rule invokeBuiltin(obj("gt_float",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "float", "float", bool(floatvalue(O) >Float floatvalue(O2))) ... - rule invokeBuiltin(obj("le_float",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "float", "float", bool(floatvalue(O) <=Float floatvalue(O2))) ... - rule invokeBuiltin(obj("ge_float",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "float", "float", bool(floatvalue(O) >=Float floatvalue(O2))) ... - rule invokeBuiltin(obj("eq_float",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "float", "float", bool(floatvalue(O) ==Float floatvalue(O2))) ... - rule invokeBuiltin(obj("ne_float",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "float", "float", bool(floatvalue(O) =/=Float floatvalue(O2))) ... + //rule invokeBuiltin(obj("lt_float",_), ListItem(O:Object) ListItem(O2:Object), .) => binaryOp(O, O2, "float", "float", bool(floatvalue(O) + //rule invokeBuiltin(obj("gt_float",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "float", "float", bool(floatvalue(O) >Float floatvalue(O2))) ... + //rule invokeBuiltin(obj("le_float",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "float", "float", bool(floatvalue(O) <=Float floatvalue(O2))) ... + //rule invokeBuiltin(obj("ge_float",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "float", "float", bool(floatvalue(O) >=Float floatvalue(O2))) ... + //rule invokeBuiltin(obj("eq_float",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "float", "float", bool(floatvalue(O) ==Float floatvalue(O2))) ... + //rule invokeBuiltin(obj("ne_float",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "float", "float", bool(floatvalue(O) =/=Float floatvalue(O2))) ... endmodule diff --git a/python-semantics-functions.k b/python-semantics-functions.k index f77c7b7..224c6d0 100644 --- a/python-semantics-functions.k +++ b/python-semantics-functions.k @@ -29,7 +29,7 @@ module PYTHON-SEMANTICS-FUNCTIONS setref(N, "__frame__", ref(N2)) ~> makeFunction(N, Listify(Ps), Return, false) ~> ref(N) ... N:Int => N +Int 1 - N2 + ref(N2) (. => N "__code__" |-> ref(id(O)) "__class__" |-> ref("function") @@ -87,11 +87,12 @@ module PYTHON-SEMANTICS-FUNCTIONS syntax ObjRef ::= "makeClosure" "(" Expression ")" [strict] | "cellNum" "(" Expression "," Expression "," Expression ")" [strict] - rule [dissolve-makeFunction]: makeFunction(N, ., .Obj, _) => setref(N, "__closure__", makeClosure(ref(N) . String2Id("__code__") . String2Id("co_freevars"))) - rule makeClosure(O:Object) => makeClosure(list(listvalue(O))) + rule [dissolve-makeFunction]: makeFunction(N, ., .Obj, _) => setref(N, "__closure__", makeClosure(getref2(getref2(ref(N), "__code__"), "co_freevars"))) + rule makeClosure(O:Object) => makeClosure(list(listvalue(O))) when listvalue(O) =/=List .List + rule makeClosure(O:Object) => ref("None") when listvalue(O) ==List .List rule makeClosure(list(.)) => tuple(.Expressions) rule makeClosure(list(ListItem(N) L)) => tuple((getref2(ref(Frame), "f_cells")[N]), .Expressions) + makeClosure(list(L)) ... - Frame:Int + ref(Frame:Int) syntax K ::= createFunction(Id, K, K, Expression) [strict(4)] | createLambda(K, Expression) [strict(2)] diff --git a/python-semantics-garbage-collection.k b/python-semantics-garbage-collection.k index 99ba900..71b7664 100644 --- a/python-semantics-garbage-collection.k +++ b/python-semantics-garbage-collection.k @@ -49,7 +49,7 @@ module PYTHON-SEMANTICS-GARBAGE-COLLECTION rule refcountbag( K ) => refcountk(K) - rule refcountbag( Frame ) => SetItem(Frame) + rule refcountbag( Frame ) => refcountk(Frame) rule refcountbag( finally(K, C, XL, LL, FL, K2) XL2:List ) => refcountk(K ~> K2) refcountbag(C XL XL2 LL FL ) rule refcountbag( finally(K, C, XL, LL, FL, K2) LL2:List ) => refcountk(K ~> K2) refcountbag(C XL LL LL2 FL ) diff --git a/python-semantics-generator.k b/python-semantics-generator.k index a9705c0..36640e3 100644 --- a/python-semantics-generator.k +++ b/python-semantics-generator.k @@ -3,19 +3,19 @@ require "python-semantics-calls.k" module PYTHON-SEMANTICS-GENERATOR imports PYTHON-SEMANTICS-CALLS - rule [invoke-generator-function]: invoke(obj(_:Int,... "__closure__" |-> Closure "__code__" |-> ref(Code) "__globals__" |-> Globals ...), M) ~> K:K => makeFrame(N, ref(Code), ref("None"), makeLocals(ref(Code) . String2Id("co_freevars"), Closure), Globals, Globals["__builtins__"], makeCells(ref(Code) . String2Id("co_freevars"), ref(Code) . String2Id("co_cellvars"), Closure, N), M) ~> mutable("gi_code" |-> ref(Code) "gi_frame" |-> ref(N) "gi_running" |-> ref("False") "gi_state" |-> .K, ref("generator")) ... + rule [invoke-generator-function]: invoke(obj(_:Int,... "__closure__" |-> Closure "__code__" |-> ref(Code) "__globals__" |-> Globals ...), M) ~> K:K => makeFrame(N, ref(Code), ref("None"), makeLocals(ref(Code) . String2Id("co_freevars"), Closure), Globals, Globals["__builtins__"], makeCells(ref(Code) . String2Id("co_freevars"), ref(Code) . String2Id("co_cellvars"), Closure, N), M, false) ~> mutable("gi_code" |-> ref(Code) "gi_frame" |-> ref(N) "gi_running" |-> ref("False") "gi_state" |-> .K, ref("generator")) ... N => N +Int 1 ... Code ... "co_flags" |-> Flags ... ... when Flags &Int 32 =/=Int 0 [allocation] - rule invokeBuiltin(obj("iter_generator",_), ListItem(O), .) => O - rule invokeBuiltin(obj("next_generator",_), ListItem(O), .) => runGenerator(O, ref("None")) - rule invokeBuiltin(obj("send_generator",_), ListItem(O) ListItem(O2), .) => runGenerator(O, O2) - rule invokeBuiltin(obj("throw_generator",_), ListItem(O) ListItem(Type), .) => ref("throw_generator")(O, Type, ref("None"), ref("None")) - rule invokeBuiltin(obj("throw_generator",_), ListItem(O) ListItem(Type) ListItem(Value), .) => ref("throw_generator")(O, Type, Value, ref("None")) - rule invokeBuiltin(obj("throw_generator",_), ListItem(O) ListItem(Type) ListItem(Value) ListItem(Traceback), .) => test(or(istype(Traceback, ref("NoneType")), istype(Traceback, ref("traceback"))), test(or(istype(Type, ref("BaseException")), hasbase(Type, ref("BaseException"))), test(and(istype(Type, ref("BaseException")), negate(istype(Value, ref("NoneType")))), raiseInternal("TypeError", "instance exception may not have a separate value"), createRaiseStatement(O, Type, .Obj if Value is ref("None") else Value, .Obj if Traceback is ref("None") else Traceback)), raiseInternal("TypeError", "exceptions must be classes or instances deriving from BaseException")), raiseInternal("TypeError", "throw() third argument must be a traceback object")) + //rule invokeBuiltin(obj("iter_generator",_), ListItem(O), .) => O + //rule invokeBuiltin(obj("next_generator",_), ListItem(O), .) => runGenerator(O, ref("None")) + //rule invokeBuiltin(obj("send_generator",_), ListItem(O) ListItem(O2), .) => runGenerator(O, O2) + //rule invokeBuiltin(obj("throw_generator",_), ListItem(O) ListItem(Type), .) => ref("throw_generator")(O, Type, ref("None"), ref("None")) + //rule invokeBuiltin(obj("throw_generator",_), ListItem(O) ListItem(Type) ListItem(Value), .) => ref("throw_generator")(O, Type, Value, ref("None")) + //rule invokeBuiltin(obj("throw_generator",_), ListItem(O) ListItem(Type) ListItem(Value) ListItem(Traceback), .) => test(or(istype(Traceback, ref("NoneType")), istype(Traceback, ref("traceback"))), test(or(istype(Type, ref("BaseException")), hasbase(Type, ref("BaseException"))), test(and(istype(Type, ref("BaseException")), negate(istype(Value, ref("NoneType")))), raiseInternal("TypeError", "instance exception may not have a separate value"), createRaiseStatement(O, Type, .Obj if Value is ref("None") else Value, .Obj if Traceback is ref("None") else Traceback)), raiseInternal("TypeError", "exceptions must be classes or instances deriving from BaseException")), raiseInternal("TypeError", "throw() third argument must be a traceback object")) syntax ObjRef ::= createRaiseStatement(Expression, Expression, Expression, Expression) [strict] @@ -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, .Arguments)), throwGenerator(O, Type(.Arguments) . String2Id("with_traceback")(Traceback, .Arguments))) rule createRaiseStatement(O, Type, Value:Object, Traceback:Object) => throwGenerator(O, Type(Value, .Arguments) . String2Id("with_traceback")(Traceback, .Arguments)) - rule invokeBuiltin(obj("close_generator",_), ListItem(O), .) => try: throwGenerator(O, ref("GeneratorExit")) ; except ref("GeneratorExit") : ref("None") except except ref("StopIteration") : ref("None") else: raiseInternal("RuntimeError", "generator ignored GeneratorExit") + //rule invokeBuiltin(obj("close_generator",_), ListItem(O), .) => try: throwGenerator(O, ref("GeneratorExit")) ; except ref("GeneratorExit") : ref("None") except except ref("StopIteration") : ref("None") else: raiseInternal("RuntimeError", "generator ignored GeneratorExit") syntax ObjRef ::= runGenerator(Expression, Expression) [strict] | throwGenerator(Expression, Expression) [strict] @@ -36,7 +36,7 @@ module PYTHON-SEMANTICS-GENERATOR rule [start-generator]: enterGenerator(O, Val, .K) ~> K => Val ~> getattr2(getref(O, "gi_code"), "co_code") ~> return ... - Frame => id(getattr(O, "gi_frame")) + Frame => getattr(O, "gi_frame") FL => . XC (C:Bag => newFrame) @@ -49,7 +49,7 @@ module PYTHON-SEMANTICS-GENERATOR rule [continue-generator]: enterGenerator(O, Val, (RestoredK, RestoredC, RestoredFL, RestoredXC)) ~> K => Val ~> RestoredK ~> return ... - Frame => id(getattr(O, "gi_frame")) + Frame => getattr(O, "gi_frame") FL => RestoredFL XC => RestoredXC (C:Bag => RestoredC) @@ -57,7 +57,7 @@ module PYTHON-SEMANTICS-GENERATOR . => generator(Frame, C, FL, XC, K, id(O)) ... ... - rule return O ~> _ => setattr(N, "gi_state", (#freezer (HOLE ;)(.KList), SavedC, .List, SavedXC)) ~> raise ref("StopIteration")(#if id(O) ==K None #then .Arguments #else (O, .Arguments) #fi) ~> K + rule return O ~> _ => setattr(N, "gi_state", (#freezer (HOLE ;)(.KList), SavedC, .List, SavedXC)) ~> raise ref("StopIteration")(#if id(O) ==K NoneId #then .Arguments #else (O, .Arguments) #fi) ~> K ... generator(Frame, C, FL, XC, K, N) => . ... @@ -67,7 +67,7 @@ module PYTHON-SEMANTICS-GENERATOR (SavedC => C) ... - ... "None" |-> None ... + ... "None" |-> NoneId ... rule [yield]: yield O ~> SavedK => setattr(N, "gi_state", (SavedK, SavedC, SavedFL, SavedXC)) ~> O ~> K ... diff --git a/python-semantics-import.k b/python-semantics-import.k index 3264a0d..633842b 100644 --- a/python-semantics-import.k +++ b/python-semantics-import.k @@ -21,17 +21,17 @@ module PYTHON-SEMANTICS-IMPORT rule [makeSymbol]: makeSymbol(S, O:Object) => . ... ... . => S |-> id(O) ... - rule invokeBuiltin(obj("imp_acquire_lock",_), ., .) => ref("None") - rule invokeBuiltin(obj("imp_release_lock",_), ., .) => ref("None") - rule invokeBuiltin(obj("imp_extension_suffixes",_), ., .) => [.Expressions] - rule invokeBuiltin(obj("imp_is_builtin",_), ListItem(O), .) => test(istype(O, ref("str")), bool(strvalue(O) in keys(M)), raiseInternal("TypeError", "must be str")) ... - M - rule invokeBuiltin(obj("imp_init_builtin",_), ListItem(O), .) => test(istype(O, ref("str")), test(strvalue(O) in keys(M), ref("sys") . String2Id("modules")[strvalue(O)], .Expressions := ref(M(strvalue(O))) ~> ref(M(strvalue(O))), ref("None")), raiseInternal("TypeError", "must be str")) ... - M - rule invokeBuiltin(obj("imp_is_frozen",_), ListItem(O), .) => test(istype(O, ref("str")), ref("False"), raiseInternal("TypeError", "must be str")) - rule invokeBuiltin(obj("imp_init_frozen",_), ListItem(O), .) => test(istype(O, ref("str")), ref("None"), raiseInternal("TypeError", "must be str")) - rule invokeBuiltin(obj("imp_get_frozen_object",_), ListItem(O), .) => test(istype(O, ref("str")), raiseInternal("ImportError", "no such frozen object named " +String strvalue(O)), raiseInternal("TypeError", "must be str")) - rule invokeBuiltin(obj("imp_is_frozen_package",_), ListItem(O), .) => test(istype(O, ref("str")), raiseInternal("ImportError", "no such frozen object named " +String strvalue(O)), raiseInternal("TypeError", "must be str")) + //rule invokeBuiltin(obj("imp_acquire_lock",_), ., .) => ref("None") + //rule invokeBuiltin(obj("imp_release_lock",_), ., .) => ref("None") + //rule invokeBuiltin(obj("imp_extension_suffixes",_), ., .) => [.Expressions] + //rule invokeBuiltin(obj("imp_is_builtin",_), ListItem(O), .) => test(istype(O, ref("str")), bool(strvalue(O) in keys(M)), raiseInternal("TypeError", "must be str")) ... + // M + //rule invokeBuiltin(obj("imp_init_builtin",_), ListItem(O), .) => test(istype(O, ref("str")), test(strvalue(O) in keys(M), ref("sys") . String2Id("modules")[strvalue(O)], .Expressions := ref(M(strvalue(O))) ~> ref(M(strvalue(O))), ref("None")), raiseInternal("TypeError", "must be str")) ... + // M + //rule invokeBuiltin(obj("imp_is_frozen",_), ListItem(O), .) => test(istype(O, ref("str")), ref("False"), raiseInternal("TypeError", "must be str")) + //rule invokeBuiltin(obj("imp_init_frozen",_), ListItem(O), .) => test(istype(O, ref("str")), ref("None"), raiseInternal("TypeError", "must be str")) + //rule invokeBuiltin(obj("imp_get_frozen_object",_), ListItem(O), .) => test(istype(O, ref("str")), raiseInternal("ImportError", "no such frozen object named " +String strvalue(O)), raiseInternal("TypeError", "must be str")) + //rule invokeBuiltin(obj("imp_is_frozen_package",_), ListItem(O), .) => test(istype(O, ref("str")), raiseInternal("ImportError", "no such frozen object named " +String strvalue(O)), raiseInternal("TypeError", "must be str")) // import statement diff --git a/python-semantics-integers.k b/python-semantics-integers.k index a335645..28e1a77 100644 --- a/python-semantics-integers.k +++ b/python-semantics-integers.k @@ -3,66 +3,67 @@ require "python-semantics-boolean-ops.k" module PYTHON-SEMANTICS-INTEGERS imports PYTHON-SEMANTICS-BOOLEAN-OPS - rule invokeBuiltin(obj("lt_int",_), ListItem(O:Object) ListItem(O2:Object), .) => binaryOp(O, O2, "int", "int", bool(intvalue(O) - rule invokeBuiltin(obj("gt_int",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "int", "int", bool(intvalue(O) >Int intvalue(O2))) ... - rule invokeBuiltin(obj("le_int",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "int", "int", bool(intvalue(O) <=Int intvalue(O2))) ... - rule invokeBuiltin(obj("ge_int",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "int", "int", bool(intvalue(O) >=Int intvalue(O2))) ... - rule invokeBuiltin(obj("eq_int",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "int", "int", bool(intvalue(O) ==Int intvalue(O2))) ... - rule invokeBuiltin(obj("ne_int",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "int", "int", bool(intvalue(O) =/=Int intvalue(O2))) ... + rule invokeBuiltin("int.__lt__", "self" |-> Self:Object "other" |-> Other:Object) => return binaryOp(Self, Other, "int", "int", bool(intvalue(Self) Self:Object "other" |-> Other:Object) => return binaryOp(Self, Other, "int", "int", bool(intvalue(Self) >Int intvalue(Other))) + rule invokeBuiltin("int.__le__", "self" |-> Self:Object "other" |-> Other:Object) => return binaryOp(Self, Other, "int", "int", bool(intvalue(Self) <=Int intvalue(Other))) + rule invokeBuiltin("int.__ge__", "self" |-> Self:Object "other" |-> Other:Object) => return binaryOp(Self, Other, "int", "int", bool(intvalue(Self) >=Int intvalue(Other))) + rule invokeBuiltin("int.__eq__", "self" |-> Self:Object "other" |-> Other:Object) => return binaryOp(Self, Other, "int", "int", bool(intvalue(Self) ==Int intvalue(Other))) + rule [int-ne]: invokeBuiltin("int.__ne__", "self" |-> Self:Object "other" |-> Other:Object) => return binaryOp(Self, Other, "int", "int", bool(intvalue(Self) =/=Int intvalue(Other))) - rule invokeBuiltin(obj("bool_int",_), ListItem(O), .) => bool(plbool(O)) ... + rule invokeBuiltin("int.__bool__",_) => return bool(plbool(String2Id("self"))) - rule invokeBuiltin(obj("add_int",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "int", "int", intvalue(O) +Int intvalue(O2)) ... - rule invokeBuiltin(obj("radd_int",_), ListItem(O) ListItem(O2), .) => invokeBuiltin(ref("add_int"), ListItem(O2) ListItem(O), .) ... + rule invokeBuiltin("int.__add__","self" |-> Self:Object "other" |-> Other:Object) => return binaryOp(Self, Other, "int", "int", intvalue(Self) +Int intvalue(Other)) + rule invokeBuiltin("int.__radd__","self" |-> Self:Object "other" |-> Other:Object) => return binaryOp(Self, Other, "int", "int", intvalue(Self) +Int intvalue(Other)) - rule invokeBuiltin(obj("sub_int",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "int", "int", intvalue(O) -Int intvalue(O2)) ... - rule invokeBuiltin(obj("rsub_int",_), ListItem(O) ListItem(O2), .) => invokeBuiltin(ref("sub_int"), ListItem(O2) ListItem(O), .) ... + //rule invokeBuiltin(obj("sub_int",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "int", "int", intvalue(O) -Int intvalue(O2)) ... + //rule invokeBuiltin(obj("rsub_int",_), ListItem(O) ListItem(O2), .) => invokeBuiltin(ref("sub_int"), ListItem(O2) ListItem(O), .) ... - rule invokeBuiltin(obj("mul_int",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "int", "int", intvalue(O) *Int intvalue(O2)) ... - rule invokeBuiltin(obj("rmul_int",_), ListItem(O) ListItem(O2), .) => invokeBuiltin(ref("mul_int"), ListItem(O2) ListItem(O), .) ... + //rule invokeBuiltin(obj("mul_int",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "int", "int", intvalue(O) *Int intvalue(O2)) ... + //rule invokeBuiltin(obj("rmul_int",_), ListItem(O) ListItem(O2), .) => invokeBuiltin(ref("mul_int"), ListItem(O2) ListItem(O), .) ... - rule invokeBuiltin(obj("truediv_int",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "int", "int", #if intvalue(O2) ==Int 0 #then raiseInternal("ZeroDivisionError", "division by zero") #else Int2Float(intvalue(O)) /Float Int2Float(intvalue(O2)) #fi) ... - rule invokeBuiltin(obj("rtruediv_int",_), ListItem(O) ListItem(O2), .) => invokeBuiltin(ref("truediv_int"), ListItem(O2) ListItem(O), .) ... + //rule invokeBuiltin(obj("truediv_int",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "int", "int", #if intvalue(O2) ==Int 0 #then raiseInternal("ZeroDivisionError", "division by zero") #else Int2Float(intvalue(O)) /Float Int2Float(intvalue(O2)) #fi) ... + //rule invokeBuiltin(obj("rtruediv_int",_), ListItem(O) ListItem(O2), .) => invokeBuiltin(ref("truediv_int"), ListItem(O2) ListItem(O), .) ... - rule invokeBuiltin(obj("floordiv_int",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "int", "int", #if intvalue(O2) ==Int 0 #then raiseInternal("ZeroDivisionError", "integer division by zero") #else intvalue(O) /Int intvalue(O2) #fi) ... - rule invokeBuiltin(obj("rfloordiv_int",_), ListItem(O) ListItem(O2), .) => invokeBuiltin(ref("floordiv_int"), ListItem(O2) ListItem(O), .) ... + //rule invokeBuiltin(obj("floordiv_int",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "int", "int", #if intvalue(O2) ==Int 0 #then raiseInternal("ZeroDivisionError", "integer division by zero") #else intvalue(O) /Int intvalue(O2) #fi) ... + //rule invokeBuiltin(obj("rfloordiv_int",_), ListItem(O) ListItem(O2), .) => invokeBuiltin(ref("floordiv_int"), ListItem(O2) ListItem(O), .) ... - rule invokeBuiltin(obj("mod_int",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "int", "int", #if intvalue(O2) ==Int 0 #then raiseInternal("ZeroDivisionError", "modulo by zero") #else intvalue(O) %Int intvalue(O2) #fi) ... - rule invokeBuiltin(obj("rmod_int",_), ListItem(O) ListItem(O2), .) => invokeBuiltin(ref("mod_int"), ListItem(O2) ListItem(O), .) ... + //rule invokeBuiltin(obj("mod_int",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "int", "int", #if intvalue(O2) ==Int 0 #then raiseInternal("ZeroDivisionError", "modulo by zero") #else intvalue(O) %Int intvalue(O2) #fi) ... + //rule invokeBuiltin(obj("rmod_int",_), ListItem(O) ListItem(O2), .) => invokeBuiltin(ref("mod_int"), ListItem(O2) ListItem(O), .) ... - rule invokeBuiltin(obj("pow_int",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "int", "int", #if intvalue(O2) >=Int 0 #then intvalue(O) ^Int intvalue(O2) #else #if intvalue(O) ==Int 0 #then raiseInternal("ZeroDivisionError", "0.0 cannot be raised to a negative power") #else Int2Float(1) /Float Int2Float(intvalue(O) ^Int absInt(intvalue(O2))) #fi #fi) ... - rule invokeBuiltin(obj("rpow_int",_), ListItem(O) ListItem(O2), .) => invokeBuiltin(ref("pow_int"), ListItem(O2) ListItem(O), .) ... + //rule invokeBuiltin(obj("pow_int",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "int", "int", #if intvalue(O2) >=Int 0 #then intvalue(O) ^Int intvalue(O2) #else #if intvalue(O) ==Int 0 #then raiseInternal("ZeroDivisionError", "0.0 cannot be raised to a negative power") #else Int2Float(1) /Float Int2Float(intvalue(O) ^Int absInt(intvalue(O2))) #fi #fi) ... + //rule invokeBuiltin(obj("rpow_int",_), ListItem(O) ListItem(O2), .) => invokeBuiltin(ref("pow_int"), ListItem(O2) ListItem(O), .) ... //TODO: 3-argument pow - rule invokeBuiltin(obj("lshift_int",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "int", "int", #if intvalue(O2) >=Int 0 #then intvalue(O) < - rule invokeBuiltin(obj("rlshift_int",_), ListItem(O) ListItem(O2), .) => invokeBuiltin(ref("lshift_int"), ListItem(O2) ListItem(O), .) ... + //rule invokeBuiltin(obj("lshift_int",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "int", "int", #if intvalue(O2) >=Int 0 #then intvalue(O) < + //rule invokeBuiltin(obj("rlshift_int",_), ListItem(O) ListItem(O2), .) => invokeBuiltin(ref("lshift_int"), ListItem(O2) ListItem(O), .) ... - rule invokeBuiltin(obj("rshift_int",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "int", "int", #if intvalue(O2) >=Int 0 #then intvalue(O) >>Int intvalue(O2) #else raiseInternal("ValueError", "negative shift count") #fi) ... - rule invokeBuiltin(obj("rrshift_int",_), ListItem(O) ListItem(O2), .) => invokeBuiltin(ref("rshift_int"), ListItem(O2) ListItem(O), .) ... + //rule invokeBuiltin(obj("rshift_int",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "int", "int", #if intvalue(O2) >=Int 0 #then intvalue(O) >>Int intvalue(O2) #else raiseInternal("ValueError", "negative shift count") #fi) ... + //rule invokeBuiltin(obj("rrshift_int",_), ListItem(O) ListItem(O2), .) => invokeBuiltin(ref("rshift_int"), ListItem(O2) ListItem(O), .) ... - rule invokeBuiltin(obj("and_int",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "int", "int", (intvalue(O) &Int intvalue(O2))) ... - rule invokeBuiltin(obj("rand_int",_), ListItem(O) ListItem(O2), .) => invokeBuiltin(ref("and_int"), ListItem(O2) ListItem(O), .) ... + //rule invokeBuiltin(obj("and_int",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "int", "int", (intvalue(O) &Int intvalue(O2))) ... + //rule invokeBuiltin(obj("rand_int",_), ListItem(O) ListItem(O2), .) => invokeBuiltin(ref("and_int"), ListItem(O2) ListItem(O), .) ... - rule invokeBuiltin(obj("xor_int",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "int", "int", (intvalue(O) xorInt intvalue(O2))) ... - rule invokeBuiltin(obj("rxor_int",_), ListItem(O) ListItem(O2), .) => invokeBuiltin(ref("xor_int"), ListItem(O2) ListItem(O), .) ... + //rule invokeBuiltin(obj("xor_int",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "int", "int", (intvalue(O) xorInt intvalue(O2))) ... + //rule invokeBuiltin(obj("rxor_int",_), ListItem(O) ListItem(O2), .) => invokeBuiltin(ref("xor_int"), ListItem(O2) ListItem(O), .) ... - rule invokeBuiltin(obj("or_int",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "int", "int", (intvalue(O) |Int intvalue(O2))) ... - rule invokeBuiltin(obj("ror_int",_), ListItem(O) ListItem(O2), .) => invokeBuiltin(ref("or_int"), ListItem(O2) ListItem(O), .) ... + //rule invokeBuiltin(obj("or_int",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "int", "int", (intvalue(O) |Int intvalue(O2))) ... + //rule invokeBuiltin(obj("ror_int",_), ListItem(O) ListItem(O2), .) => invokeBuiltin(ref("or_int"), ListItem(O2) ListItem(O), .) ... - rule invokeBuiltin(obj("neg_int",_), ListItem(O), .) => unaryOp(O, "int", 0 -Int intvalue(O)) ... - rule invokeBuiltin(obj("pos_int",_), ListItem(O), .) => unaryOp(O, "int", intvalue(O)) ... - rule invokeBuiltin(obj("abs_int",_), ListItem(O), .) => unaryOp(O, "int", absInt(intvalue(O))) ... - rule invokeBuiltin(obj("invert_int",_), ListItem(O), .) => unaryOp(O, "int", ~Int intvalue(O)) ... + //rule invokeBuiltin(obj("neg_int",_), ListItem(O), .) => unaryOp(O, "int", 0 -Int intvalue(O)) ... + //rule invokeBuiltin(obj("pos_int",_), ListItem(O), .) => unaryOp(O, "int", intvalue(O)) ... + //rule invokeBuiltin(obj("abs_int",_), ListItem(O), .) => unaryOp(O, "int", absInt(intvalue(O))) ... + //rule invokeBuiltin(obj("invert_int",_), ListItem(O), .) => unaryOp(O, "int", ~Int intvalue(O)) ... //TODO: string conversion - rule invokeBuiltin(obj("new_int",_), ListItem(O), .) => newHelper(O, ref("int"), SetItem("bool")) ~> immutable(0, O) - rule invokeBuiltin(obj("new_int",_), ListItem(O) ListItem(O2), .) => newHelper(O, ref("int"), SetItem("bool")) ~> immutable(intvalue(O . String2Id("__int__") (.Arguments)), O) + //rule invokeBuiltin(obj("new_int",_), ListItem(O), .) => newHelper(O, ref("int"), SetItem("bool")) ~> immutable(0, O) + //rule invokeBuiltin(obj("new_int",_), ListItem(O) ListItem(O2), .) => newHelper(O, ref("int"), SetItem("bool")) ~> immutable(intvalue(O . String2Id("__int__") (.Arguments)), O) context immutable(intvalue(HOLE), _) - rule invokeBuiltin(obj("int_int",_), ListItem(O), .) => O + //rule invokeBuiltin(obj("int_int",_), ListItem(O), .) => O + rule invokeBuiltin("int.__index__",_) => return self - rule invokeBuiltin(obj("hash_int",_), ListItem(O), .) => unaryOp(O, "int", #if intvalue(O) %Int Modulus ==Int -1 #then -2 #else intvalue(O) %Int Modulus #fi) ... - ... "sys.hash_info.modulus" |-> Modulus ... + //rule invokeBuiltin(obj("hash_int",_), ListItem(O), .) => unaryOp(O, "int", #if intvalue(O) %Int Modulus ==Int -1 #then -2 #else intvalue(O) %Int Modulus #fi) ... + // ... "sys.hash_info.modulus" |-> Modulus ... endmodule diff --git a/python-semantics-iterators.k b/python-semantics-iterators.k index be40b4e..9b18fee 100644 --- a/python-semantics-iterators.k +++ b/python-semantics-iterators.k @@ -5,32 +5,45 @@ module PYTHON-SEMANTICS-ITERATORS imports PYTHON-SEMANTICS-LITERALS imports PYTHON-SEMANTICS-TRY - rule invokeBuiltin(obj("get_iter",_), ListItem(obj(_:ObjId,... "__value__" |-> K:K ...)), .) => mutable(K, ref("iterator")) ... + rule invokeBuiltin("tuple.__iter__",_) => return valueIterator(String2Id("self")) + rule invokeBuiltin("list.__iter__",_) => return valueIterator(String2Id("self")) - rule invokeBuiltin(obj("iter_iter",_), ListItem(O:Object), .) => O ... - rule invokeBuiltin(obj("iter_next",_), ListItem(obj(B:ObjId,_)), .) => B2 ... + rule invokeBuiltin("iterator.__iter__",_) => return String2Id("self") + rule invokeBuiltin("iterator.__next__", "self" |-> obj(Self,_)) => return B ... ... - B - ... "__value__" |-> list((ListItem(B2) => .) L:List) ... + Self + ... "__value__" |-> list((ListItem(B) => .) L:List) ... ... - rule invokeBuiltin(obj("iter_next",_), ListItem(obj(B,_)), .) => raise ref("StopIteration") ... + rule invokeBuiltin("iterator.__next__", "self" |-> obj(Self,_)) => raise ref("StopIteration") ... ... - B + Self ... "__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 ... - ... - B - ... "__index__" |-> (I => I +Int 1) "__value__" |-> B2 ... - ... - - - syntax ObjRef ::= "checkIter" "(" Expression ")" [strict] - - rule invokeBuiltin(obj("iter",_), ListItem(O), .) => checkIter(getmember(O, "__iter__", true, false, false) (.Arguments) -> test(getmember(O, "__getitem__", true, false, false) =/=Obj .Obj, mutable("__index__" |-> 0 "__value__" |-> ref(id(O)), ref("iterator")), .Obj) -> (raiseInternal("TypeError", "object is not iterable"))) ... - - rule checkIter(O) => test(getmember(O, "__next__", true, false, false) ==Obj .Obj, raiseInternal("TypeError", "iter() returned non-iterator"), O) ... + //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 ... + // ... + // B + // ... "__index__" |-> (I => I +Int 1) "__value__" |-> B2 ... + // ... + + + + rule invokeBuiltin("iter",_) => (if hasmember(String2Id("object"), "__iter__") : + String2Id("object"), .Expressions := getmember(String2Id("object"), "__iter__", true, false, true) (.Arguments) + else: + if hasmember(String2Id("object"), "__getitem__") : + String2Id("object"), .Expressions := getitemIterator(String2Id("object")) + else: + raiseInternal("TypeError", "object is not iterable")) newline + if hasmember(String2Id("object"), "__next__"): + return String2Id("object") + else: + raiseInternal("TypeError", "iter() returned non-iterator") //TODO: sentinels + syntax Expression ::= getitemIterator(Expression) [strict] + rule getitemIterator(O:Object) => mutable("__index__" |-> 0 "__value__" |-> ref(id(O)), ref("iterator")) + syntax Expression ::= valueIterator(Expression) [strict] + rule valueIterator(O:Object) => mutable(getattr(O, "__value__"), ref("iterator")) + endmodule diff --git a/python-semantics-lists.k b/python-semantics-lists.k index f905af3..c92bb82 100644 --- a/python-semantics-lists.k +++ b/python-semantics-lists.k @@ -5,15 +5,15 @@ module PYTHON-SEMANTICS-LISTS syntax K ::= setValue(Object) - rule invokeBuiltin(obj("add_list",_), ListItem(O:Object) ListItem(O2:Object), .) => test(and(istype(O, ref("list")), istype(O2, ref("list"))), mutable(list(listvalue(O) listvalue(O2)),ref("list")), raiseInternal("TypeError", "can only concatenate list to list")) + //rule invokeBuiltin(obj("add_list",_), ListItem(O:Object) ListItem(O2:Object), .) => test(and(istype(O, ref("list")), istype(O2, ref("list"))), mutable(list(listvalue(O) listvalue(O2)),ref("list")), raiseInternal("TypeError", "can only concatenate list to list")) - rule invokeBuiltin(obj("getitem_list",_), ListItem(O) ListItem(O2), .) => test(istype(O2, ref("int")), test(intvalue(O2) >=Int 0 -Int lengthList listvalue(O) andBool intvalue(O2) =Int 0, get(listvalue(O), intvalue(O2)), get(listvalue(O), lengthList listvalue(O) +Int intvalue(O2))), raiseInternal("IndexError", "list index out of range")), test(istype(O2, ref("slice")), ref("list")(slice(O, O2)), raiseInternal("TypeError", "list indices must be integers or slices"))) + //rule invokeBuiltin(obj("getitem_list",_), ListItem(O) ListItem(O2), .) => test(istype(O2, ref("int")), test(intvalue(O2) >=Int 0 -Int lengthList listvalue(O) andBool intvalue(O2) =Int 0, get(listvalue(O), intvalue(O2)), get(listvalue(O), lengthList listvalue(O) +Int intvalue(O2))), raiseInternal("IndexError", "list index out of range")), test(istype(O2, ref("slice")), ref("list")(slice(O, O2)), raiseInternal("TypeError", "list indices must be integers or slices"))) - rule invokeBuiltin(obj("len_list",_), ListItem(O), .) => lengthList listvalue(O) + //rule invokeBuiltin(obj("len_list",_), ListItem(O), .) => lengthList listvalue(O) - rule invokeBuiltin(obj("new_list",_), ListItem(O) _, .) => newHelper(O, ref("list"), .) ~> mutable(list(.), O) - rule invokeBuiltin(obj("init_list",_), ListItem(_:Object), .) => ref("None") - rule invokeBuiltin(obj("init_list",_), ListItem(O) ListItem(O2), .) => iterate(O2, .) ~> setValue(O) + //rule invokeBuiltin(obj("new_list",_), ListItem(O) _, .) => newHelper(O, ref("list"), .) ~> mutable(list(.), O) + //rule invokeBuiltin(obj("init_list",_), ListItem(_:Object), .) => ref("None") + //rule invokeBuiltin(obj("init_list",_), ListItem(O) ListItem(O2), .) => iterate(O2, .) ~> setValue(O) rule list(L:List) ~> setValue(obj(B:ObjId,_)) => ref("None") ... ... @@ -21,8 +21,8 @@ module PYTHON-SEMANTICS-LISTS ... "__value__" |-> (_ => list(Refify(Idify(L)))) ... ... - rule invokeBuiltin(obj("eq_list",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "list", "list", (ref("bool") (equalList(listvalue(O), (listvalue(O2)))))) - rule invokeBuiltin(obj("ne_list",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "list", "list", not equalList(listvalue(O), listvalue(O2))) + //rule invokeBuiltin(obj("eq_list",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "list", "list", (ref("bool") (equalList(listvalue(O), (listvalue(O2)))))) + //rule invokeBuiltin(obj("ne_list",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "list", "list", not equalList(listvalue(O), listvalue(O2))) syntax ObjRef ::= "equalList" "(" List "," List ")" diff --git a/python-semantics-literals.k b/python-semantics-literals.k index 64a31bf..425c4ab 100644 --- a/python-semantics-literals.k +++ b/python-semantics-literals.k @@ -12,7 +12,7 @@ module PYTHON-SEMANTICS-LITERALS | "processSet" "(" Expression "," List ")" [strict(1)] | "processSetElement" "(" Expression "," Expression "," Expression ")" [strict] | "tableInsert" "(" ObjId "," Int "," Expression "," K ")" [strict(3)] - | "tableLookup" "(" ObjId "," Int "," Expression ")" [strict(3)] + | "tableLookup" "(" Expression "," Expression "," Expression ")" [strict(3)] | "tableDelete" "(" ObjId "," Int "," Expression ")" [strict(3)] | "bucketInsert" "(" ObjId "," Int "," Expression "," Expression "," List "," List ")" [strict(3, 4)] | "bucketLookup" "(" Expression "," List ")" [strict(1)] @@ -43,11 +43,15 @@ module PYTHON-SEMANTICS-LITERALS rule processSet(SetObj:Object, .) => ref(id(SetObj)) ... - syntax K ::= "checkHash" "(" Expression ")" [strict] - - rule invokeBuiltin(obj("hash",_), ListItem(O:Object), .) => checkHash(getmember(O, "__hash__", true, false, false) (.Arguments) -> (raiseInternal("TypeError", "unhashable type"))) ... - - rule [checkHash]: checkHash(O:Object) => test(istype(O, ref("int")), O, raiseInternal("TypeError", "__hash__ method should return an integer")) ... + syntax #Id ::= "__hash__" + rule invokeBuiltin("hash", _) => if hasmember(String2Id("object"), "__hash__") : + String2Id("object"), .Expressions := getmember(String2Id("object"), "__hash__", true, false, true) (.Arguments) newline + if istype(String2Id("object"), ref("int")) : + return String2Id("object") + else: + raiseInternal("TypeError", "__hash__ method should return an integer") + else: + raiseInternal("TypeError", "unhashable type") rule processDictElement(obj(B:ObjId,_), Key:Object, Hash:Object, Value:K) => tableInsert(B, intvalue(Hash), Key, ref(id(Key)) : ref(id(Value))) ... @@ -85,6 +89,11 @@ module PYTHON-SEMANTICS-LITERALS ... "__value__" |-> map(M => M[undef/H]) ... ... + rule tableLookup(E, H, Key) => E ~> tableLookup(HOLE, H, Key) when isObjId(E) =/=K true [heat] + rule O:Object ~> tableLookup(HOLE, H, Key) => tableLookup(id(O), H, Key) [cool] + rule tableLookup(E, H, Key) => H ~> tableLookup(E, HOLE, Key) when isInt(H) =/=K true [heat] + rule O:Object ~> tableLookup(E, HOLE, Key) => tableLookup(E, intvalue(O), Key) [cool] + rule tableLookup(B, H, Key) => bucketLookup(Key, Values) ... ... B @@ -138,10 +147,19 @@ module PYTHON-SEMANTICS-LITERALS Literals:Map (. => pair(M, B) |-> ref(N)) N => N +Int 1 when notBool(pair(M, B) in keys(Literals)) [allocation] - rule invokeBuiltin(obj("new_structseq",_), ListItem(Type) ListItem(Sequence), .) => iterate(Sequence, raiseInternal("TypeError", "constructor requires a sequence")) ~> makeStructSeq(Type) - - syntax K ::= makeStructSeq(Object) - - rule list(L) ~> makeStructSeq(Type) => test(lengthList L =/=Int lengthList getl(getattr(Type, "__order__")), raiseInternal("TypeError", getattr(Type, "__name__") +String "takes a " +String Int2String(lengthList getl(getattr(Type, "__order__"))) +String "-sequence (" +String Int2String(lengthList L) +String "-sequence given)"), mutable(list(Refify(Idify(L))), Type)) + rule invokeBuiltin("structseq.__new__","cls" |-> Cls:Object _) => + String2Id("structseq"), .Expressions := mutable(list(.), Cls) ~> + String2Id("i"), .Expressions := 0 ~> + (for String2Id("elem") in String2Id("sequence") : + addElemToStructSeq(String2Id("elem"), String2Id("structseq")) newline + String2Id("i") += 1 + else: pass) ~> + (if String2Id("i") != lengthList getl(getattr(Cls, "__order__")) : + raiseInternal("TypeError", getattr(Cls, "__name__") +String " takes a " +String Int2String(lengthList getl(getattr(Cls, "__order__"))) +String "-sequence") + else: pass) ~> + return String2Id("structseq") + + syntax K ::= addElemToStructSeq(Expression, Expression) [strict] + rule addElemToStructSeq(Elem:Object, StructSeq:Object) => setattr(id(StructSeq), "__value__", list(getl(getattr(StructSeq, "__value__")) ListItem(ref(id(Elem))))) endmodule diff --git a/python-semantics-logic.k b/python-semantics-logic.k index a72425d..0e973a3 100644 --- a/python-semantics-logic.k +++ b/python-semantics-logic.k @@ -7,11 +7,17 @@ module PYTHON-SEMANTICS-LOGIC syntax K ::= "test" "(" Test "," K "," K ")" [strict(1)] + syntax K ::= "if" Test ":" K "else" ":" K [strict(1)] + syntax Expression ::= Expression "if" Test "else" Expression [strict(2)] + syntax Test ::= "and" "(" Test "," Test ")" [strict(1)] syntax Test ::= "or" "(" Test "," Test ")" [strict(1)] syntax Test ::= "negate" "(" Test ")" [strict] syntax Test ::= Expression "==Obj" Expression [strict] syntax Test ::= Expression "=/=Obj" Expression [strict] + syntax Test ::= "not" Test [strict] + syntax Test ::= Test "or" Test [strict] + syntax Test ::= Test "and" Test [strict] rule and(false, _) => false rule and(_, false) => false @@ -20,15 +26,35 @@ module PYTHON-SEMANTICS-LOGIC rule or(_, true) => true rule or(false, K) => K rule negate(T:Bool) => notBool T + rule not T:Bool => notBool T + rule true or _ => true + rule _ or true => true + rule false or K => K + rule false and _ => false + rule _ and false => false + rule true and K => K rule O:KResult ==Obj O2:KResult => O ==K O2 rule O:KResult =/=Obj O2:KResult => O =/=K O2 rule test(true, K:K, _) => K rule test(false, _, K) => K + rule if true : K else: _ => K + rule if false : _ else: K => K + rule K if true else _ => K + rule _ if false else K => K rule (O:Object -> _) => O + rule T:Bool -> _ => T rule map(M:Map) -> _ => map(M) rule .Obj -> Chain:K => Chain rule .Obj (_) => .Obj + syntax Test ::= Expression "is" "not" "None" [strict] + syntax Test ::= Expression "is" "None" [strict] + rule O:Object is not None => not O is None + rule obj(B,_) is None => B ==K NoneId ... + ... "None" |-> NoneId ... + + syntax priorities '_|_ > '_isnotNone '_isNone + syntax priorities '_isnotNone '_isNone > 'not_ endmodule diff --git a/python-semantics-macros.k b/python-semantics-macros.k index 8cefcd8..a9aabed 100644 --- a/python-semantics-macros.k +++ b/python-semantics-macros.k @@ -30,10 +30,13 @@ module PYTHON-SEMANTICS-MACROS rule @ K:K newline K2:K => K2 newline declName(K2) , .Expressions := K(declName(K2)) [macro, anywhere] + rule try: Try ExceptClauses => try: Try ExceptClauses else: pass [macro] rule try: Try ExceptClauses else: Else finally: Finally => try: try: Try ExceptClauses else: Else finally: Finally [macro, anywhere] rule with W, W2, W3 : Body => with W, .Aliases : with W2, W3: Body [macro, anywhere] + rule for Target in Exp : Body => for Target in Exp : Body else: pass [macro] + rule [ E Comp ] => ref("list")(generator(E Comp)) [macro, anywhere] rule { E Comp } => ref("set")(generator(E Comp)) [macro, anywhere] rule { E : E2 Comp } => ref("dict")(generator(tuple(E, E2, .Expressions) Comp)) [macro, anywhere] diff --git a/python-semantics-methods.k b/python-semantics-methods.k index 3d96deb..9225628 100644 --- a/python-semantics-methods.k +++ b/python-semantics-methods.k @@ -5,32 +5,36 @@ module PYTHON-SEMANTICS-METHODS syntax ObjRef ::= "method" "(" Expression "," Expression ")" [strict] - rule invokeBuiltin(obj("get_builtin_method",_), ListItem(Self:Object) ListItem(Instance:Object) ListItem(Owner:Object), .) => describe(Self, Instance, Owner, "get_function") - rule invokeBuiltin(obj("get_function",_), ListItem(Self:Object) ListItem(Instance:Object) ListItem(Owner:Object), .) => describe(Self, Instance, Owner, "get_function") - rule doDescribe(Self, .Obj, O, "get_function") => Self - rule doDescribe(Self, O:Object, _, "get_function") => method(Self, O) + syntax #Id ::= "self" | "instance" | "owner" + rule invokeBuiltin("builtin-method.__get__",_) => return describe(self, instance, owner, "function.__get__") + //rule invokeBuiltin(obj("get_function",_), ListItem(Self:Object) ListItem(Instance:Object) ListItem(Owner:Object), .) => describe(Self, Instance, Owner, "get_function") + rule doDescribe(Self, .Obj, O, "function.__get__") => Self + rule doDescribe(Self, O:Object, _, "function.__get__") => method(Self, O) rule method(obj(FuncId,_), obj(SelfId,_)) => immutable("__func__" |-> ref(FuncId) "__self__" |-> ref(SelfId), ref("method")) - //can't use descriptors because method descriptors use it - rule [call]: obj(N:Nat,ObjState:Bag) (Args:K) => (getmember(obj(N,ObjState), "__call__", false, false, false) (obj(N,ObjState), Args)) -> (raiseInternal("TypeError", "object is not callable")) - - rule invokeBuiltin(obj("call_method",_), ListItem(obj(N, ... "__func__" |-> Func "__self__" |-> Self ...)) L:List, M:Map) => doCall(Func, ListItem(Self) L, M) + // iter() calls methods, and * x and ** x call iter(), so we can't call * x and ** x in this function. Fortunately, we know that args is a tuple and kwargs is a dict. + rule invokeBuiltin("method.__call__", "self" |-> Self:Object "args" |-> Args:Object "kwargs" |-> KwArgs:Object) => return doCall(getref(Self, "__func__"), ListItem(getref(Self, "__self__")) listvalue(Args), mapvalue(KwArgs)) rule doCall((O:Object => .), _, _) ~> (. => O (.Arguments)) rule doCall(., _ (ListItem(K:K) => .), .) ~> _:Object (Args:K => (K , Args)) rule doCall(., _, _ (S:String |-> K => .)) ~> _:Object (Args:K => (String2Id(S) = K, Args)) + rule doCall(., _, _ (ref(B) |-> K => .)) ~> _:Object (Args:K => (String2Id(S) = K, Args)) ... + ... + B + ... "__value__" |-> S:String ... + ... rule doCall(., ., .) => . - rule invokeBuiltin(obj("call_builtin_function",_), ListItem(Func) L:List, M:Map) => doCall(Func, L, M) + //rule invokeBuiltin(obj("call_builtin_function",_), ListItem(Func) L:List, M:Map) => doCall(Func, L, M) - rule invokeBuiltin(obj("new_classmethod",_), ListItem(Class) ListItem(Method), .) => newHelper(Class, ref("classmethod"), .) ~> mutable("__func__" |-> ref("None"), Class) - rule invokeBuiltin(obj("init_classmethod",_), ListItem(Self) ListItem(Method), .) => setref(id(Self), "__func__", Method) ~> ref("None") - rule invokeBuiltin(obj("get_classmethod",_), ListItem(Self) ListItem(Instance) ListItem(Owner), .) => describe(Self, Instance, Owner, "get_classmethod") + //rule invokeBuiltin(obj("new_classmethod",_), ListItem(Class) ListItem(Method), .) => newHelper(Class, ref("classmethod"), .) ~> mutable("__func__" |-> ref("None"), Class) + //rule invokeBuiltin(obj("init_classmethod",_), ListItem(Self) ListItem(Method), .) => setref(id(Self), "__func__", Method) ~> ref("None") + //rule invokeBuiltin(obj("get_classmethod",_), ListItem(Self) ListItem(Instance) ListItem(Owner), .) => describe(Self, Instance, Owner, "get_classmethod") rule doDescribe(Self, _, Owner, "get_classmethod") => method(getref(Self, "__func__"), Owner) - rule invokeBuiltin(obj("new_staticmethod",_), ListItem(Class) ListItem(Method), .) => newHelper(Class, ref("staticmethod"), .) ~> mutable("__func__" |-> ref("None"), Class) - rule invokeBuiltin(obj("init_staticmethod",_), ListItem(Self) ListItem(Method), .) => setref(id(Self), "__func__", Method) ~> ref("None") - rule invokeBuiltin(obj("get_staticmethod",_), ListItem(Self) ListItem(Instance) ListItem(Owner), .) => getref(Self, "__func__") + //rule invokeBuiltin(obj("new_staticmethod",_), ListItem(Class) ListItem(Method), .) => newHelper(Class, ref("staticmethod"), .) ~> mutable("__func__" |-> ref("None"), Class) + //rule invokeBuiltin(obj("init_staticmethod",_), ListItem(Self) ListItem(Method), .) => setref(id(Self), "__func__", Method) ~> ref("None") + //rule invokeBuiltin(obj("get_staticmethod",_), ListItem(Self) ListItem(Instance) ListItem(Owner), .) => getref(Self, "__func__") endmodule diff --git a/python-semantics-objects.k b/python-semantics-objects.k index 99a9957..40c77ce 100644 --- a/python-semantics-objects.k +++ b/python-semantics-objects.k @@ -6,24 +6,31 @@ module PYTHON-SEMANTICS-OBJECTS syntax ObjRef ::= "init" "(" Expression "," Expression "," List "," Map ")" [strict(1, 2)] | "getMros" "(" List ")" | "mroMerge" "(" KList ")" - syntax Bool ::= "notInTail" "(" ObjId "," List ")" [function] - syntax List ::= "trimHead" "(" List "," ObjId ")" [function] + syntax Bool ::= "notInTail" "(" Object "," List ")" [function] + syntax List ::= "trimHead" "(" List "," Object ")" [function] - rule invokeBuiltin(obj("call_type",_), ListItem(Type:Object) L:List, M:Map) => init(doCall(Type . String2Id("__new__"), ListItem(Type) L, M), Type, L, M) ... + syntax #Id ::= "__new__" + rule invokeBuiltin("type.__call__", "self" |-> Self:Object "args" |-> Args:Object "kwargs" |-> KwArgs:Object) => + String2Id("new"), .Expressions := doCall(Self . __new__, ListItem(Self) listvalue(Args), mapvalue(KwArgs)) ~> + (if istype(String2Id("new"), Self) : + String2Id("init"), .Expressions := doCall(getmember(String2Id("new"), "__init__", true, false, true), listvalue(Args), mapvalue(KwArgs)) newline + (if negate(plbool(String2Id("init") is ref("None"))) : + raiseInternal("TypeError", "__init__() should return None") + else: pass) + else: pass) ~> + return String2Id("new") + + //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) ... + // N:Int => N +Int 1 + // (. => + // N + // "__class__" |-> ref(id(O)) + // ) [allocation] - 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("object.__init__",_) => return ref("None") - 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) ... - N:Nat => N +Int 1 - (. => - N - "__class__" |-> ref(id(O)) - ) [allocation] - - rule [init-object]: invokeBuiltin(obj("init_object",_), _, _) => ref("None") ... - - rule invokeBuiltin(obj("eq_object",_), ListItem(O) ListItem(O2:Object), .) => test(plbool(O is O2), ref("True"), ref("NotImplemented")) ... - rule invokeBuiltin(obj("ne_object",_), ListItem(O) ListItem(O2), .) => not (O == O2) ... + //rule invokeBuiltin(obj("eq_object",_), ListItem(O) ListItem(O2:Object), .) => test(plbool(O is O2), ref("True"), ref("NotImplemented")) ... + //rule invokeBuiltin(obj("ne_object",_), ListItem(O) ListItem(O2), .) => not (O == O2) ... rule [getMro]: getMro(O:Object, Bases:Object) => mroMerge(list(ListItem(list(ListItem(O)))),,getMros(listvalue(Bases)),,list(ListItem(list(listvalue(Bases))))) context mroMerge(_,,HOLE,,_) @@ -49,18 +56,18 @@ module PYTHON-SEMANTICS-OBJECTS 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("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("setattr",_), ListItem(O) ListItem(Name:Object) ListItem(Value:Object), .) => getmember(O, "__setattr__", true, false, true) (Name, Value) - rule invokeBuiltin(obj("setattr_object",_), 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("setattr_type",_), ListItem(Type) ListItem(Name) ListItem(Value), .) => setmember(Type, Name, Value) + //rule invokeBuiltin(obj("setattr_object",_), 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("setattr_type",_), ListItem(Type) ListItem(Name) ListItem(Value), .) => setmember(Type, Name, Value) - 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("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) ListItem(Class), .) => getmember(Class, "__instancecheck__", true, false, true)(Instance, .Arguments) - rule invokeBuiltin(obj("issubclass",_), ListItem(Subclass) ListItem(Class), .) => getmember(Class, "__subclasscheck__", true, false, true)(Subclass, .Arguments) + //rule invokeBuiltin(obj("isinstance",_), ListItem(Instance) ListItem(Class), .) => getmember(Class, "__instancecheck__", true, false, true)(Instance, .Arguments) + //rule invokeBuiltin(obj("issubclass",_), ListItem(Subclass) ListItem(Class), .) => getmember(Class, "__subclasscheck__", true, false, true)(Subclass, .Arguments) endmodule diff --git a/python-semantics-ops.k b/python-semantics-ops.k index 92bb98b..34b3aa7 100644 --- a/python-semantics-ops.k +++ b/python-semantics-ops.k @@ -14,7 +14,7 @@ module PYTHON-SEMANTICS-OPS rule coerceUnary(O, X, S) => coercion(getmember(O, X, true, false, false) (.Arguments)) -> (raiseInternal("TypeError", "bad operand type for " +String S)) ... - rule coercion(obj(N:Nat,ObjState:Bag)) => test(or((N ==Int NoneId:Nat), (N ==Int NotImplementedId:Nat)), .Obj, obj(N,ObjState)) ... + rule coercion(obj(N,ObjState:Bag)) => test(or((N ==Int NoneId), (N ==Int NotImplementedId)), .Obj, obj(N,ObjState)) ... ... "None" |-> NoneId "NotImplemented" |-> NotImplementedId ... rule coercion(.Obj) => .Obj diff --git a/python-semantics-sets.k b/python-semantics-sets.k index e57c73e..7cf04b5 100644 --- a/python-semantics-sets.k +++ b/python-semantics-sets.k @@ -3,25 +3,25 @@ require "python-semantics-literals.k" module PYTHON-SEMANTICS-SETS imports PYTHON-SEMANTICS-LITERALS - rule invokeBuiltin(obj("new_set",_), ListItem(O) _, .) => newHelper(O, ref("set"), .) ~> {.Expressions} - rule invokeBuiltin(obj("init_set",_), ListItem(O), .) => ref("None") - rule invokeBuiltin(obj("init_set",_), ListItem(O) ListItem(O2), .) => iterate(O2, .) ~> makeSet(O) + //rule invokeBuiltin(obj("new_set",_), ListItem(O) _, .) => newHelper(O, ref("set"), .) ~> {.Expressions} + //rule invokeBuiltin(obj("init_set",_), ListItem(O), .) => ref("None") + //rule invokeBuiltin(obj("init_set",_), ListItem(O) ListItem(O2), .) => iterate(O2, .) ~> makeSet(O) syntax K ::= makeSet(Expression) [strict] rule (. => O |= {O2, .Expressions}) ~> list((ListItem(O2) => .) _) ~> makeSet(O) rule list(.) ~> makeSet(_) => ref("None") - rule [ior-set]: invokeBuiltin(obj("ior_set",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "set", "set", processSet(O, setvalue(O2))) +// rule [ior-set]: invokeBuiltin(obj("ior_set",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "set", "set", processSet(O, setvalue(O2))) - rule invokeBuiltin(obj("eq_set",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "set", "set", bool(lengthList setvalue(O) ==Int lengthList setvalue(O2)) and subset(setvalue(O), O2)) - rule invokeBuiltin(obj("ne_set",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "set", "set", not ref("eq_set")(O, O2, .Arguments)) - rule invokeBuiltin(obj("lt_set",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "set", "set", bool(lengthList setvalue(O) binaryOp(O, O2, "set", "set", subset(setvalue(O), O2)) + //rule invokeBuiltin(obj("eq_set",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "set", "set", bool(lengthList setvalue(O) ==Int lengthList setvalue(O2)) and subset(setvalue(O), O2)) + //rule invokeBuiltin(obj("ne_set",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "set", "set", not ref("eq_set")(O, O2, .Arguments)) + //rule invokeBuiltin(obj("lt_set",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "set", "set", bool(lengthList setvalue(O) binaryOp(O, O2, "set", "set", subset(setvalue(O), O2)) syntax ObjRef ::= subset(List, Expression) [strict(2)] rule subset(ListItem(Element) L, Set) => Element in Set and subset(L, Set) rule subset(., _) => ref("True") - rule invokeBuiltin(obj("contains_set",_), ListItem(O) ListItem(O2), .) => contains(list(setvalue(O)), O2) + //rule invokeBuiltin(obj("contains_set",_), ListItem(O) ListItem(O2), .) => contains(list(setvalue(O)), O2) endmodule diff --git a/python-semantics-slicing.k b/python-semantics-slicing.k index 0a8ee11..01ee9f5 100644 --- a/python-semantics-slicing.k +++ b/python-semantics-slicing.k @@ -21,7 +21,7 @@ module PYTHON-SEMANTICS-SLICING rule slice(O:Object, Slice:Object) => slice2(O, Slice, Slice . String2Id("indices") ( ref("len") (O))) rule slice2(O, Slice, Indices:Object) => ref("map")(O . String2Id("__getitem__"), ref("range")(* Indices), .Arguments) - rule invokeBuiltin(obj("new_map",_), ListItem(O) ListItem(O2) L:List, .) => newHelper(O, ref("map"), .) ~> iters(L) ~> list(.) ~> makeMap(O, O2, .) + //rule invokeBuiltin(obj("new_map",_), ListItem(O) ListItem(O2) L:List, .) => newHelper(O, ref("map"), .) ~> iters(L) ~> list(.) ~> makeMap(O, O2, .) rule (. => ref("iter") (O, .Arguments)) ~> iters((ListItem(O) => .) L) rule (O:Object => .) ~> iters(_) ~> list(_ (. => ListItem(O))) @@ -29,51 +29,54 @@ module PYTHON-SEMANTICS-SLICING rule (list(L) => .) ~> makeMap(_, O, (. => L)) rule makeMap(O, O2, L) => mutable("__func__" |-> ref(id(O2)) "__iters__" |-> list(Refify(Idify(L))), O) - rule invokeBuiltin(obj("map_next",_), ListItem(O), .) => getref(O, "__func__")(nexts(getl(getattr(O, "__iters__")))) + //rule invokeBuiltin(obj("map_next",_), ListItem(O), .) => getref(O, "__func__")(nexts(getl(getattr(O, "__iters__")))) rule nexts(ListItem(B) L:List) => ((B . String2Id("__next__")) (.Arguments)) , nexts(L) [function, anywhere] rule nexts(.) => .Arguments [function, anywhere] - rule invokeBuiltin(obj("new_range",_), ListItem(O) ListItem(O2), .) => newHelper(O, ref("range"), .) ~> ref("new_range") (O, 0, O2, .Arguments) + //rule invokeBuiltin(obj("new_range",_), ListItem(O) ListItem(O2), .) => newHelper(O, ref("range"), .) ~> ref("new_range") (O, 0, O2, .Arguments) - rule invokeBuiltin(obj("new_range",_), ListItem(O) ListItem(O2) ListItem(O3), .) => newHelper(O, ref("range"), .) ~> ref("new_range") (O, O2, O3, 1, .Arguments) + //rule invokeBuiltin(obj("new_range",_), ListItem(O) ListItem(O2) ListItem(O3), .) => newHelper(O, ref("range"), .) ~> ref("new_range") (O, O2, O3, 1, .Arguments) - rule [new-range]: invokeBuiltin(obj("new_range",_), ListItem(O) ListItem(O2) ListItem(O3) ListItem(O4), .) => newHelper(O, ref("range"), .) ~> range(ref("index")(O2, .Arguments), ref("index")(O3, .Arguments), ref("index")(O4, .Arguments), O) +// rule [new-range]: invokeBuiltin(obj("new_range",_), ListItem(O) ListItem(O2) ListItem(O3) ListItem(O4), .) => newHelper(O, ref("range"), .) ~> range(ref("index")(O2, .Arguments), ref("index")(O3, .Arguments), ref("index")(O4, .Arguments), O) - rule [iter-range]: invokeBuiltin(obj("iter_range",_), ListItem(O), .) => mutable("current" |-> getattr(O, "start") "stop" |-> getattr(O, "stop") "step" |-> getattr(O, "step"), ref("iterator")) +// rule [iter-range]: invokeBuiltin(obj("iter_range",_), ListItem(O), .) => mutable("current" |-> getattr(O, "start") "stop" |-> getattr(O, "stop") "step" |-> getattr(O, "step"), ref("iterator")) - rule invokeBuiltin(obj("iter_next",_), ListItem(obj(B:ObjId,_)), .) => test(test(Step Int Stop, Current - ... - B - ... "current" |-> (Current:Int => Current +Int Step) "stop" |-> Stop "step" |-> Step ... - ... + //rule invokeBuiltin(obj("iter_next",_), ListItem(obj(B:ObjId,_)), .) => test(test(Step Int Stop, Current + // ... + // B + // ... "current" |-> (Current:Int => Current +Int Step) "stop" |-> Stop "step" |-> Step ... + // ... - rule index(O:Object) => checkIndex(getmember(O, "__index__", true, false, false) (.Arguments)) - rule index(.Obj) => .Obj - rule checkIndex(O:Object) => test(istype(O, ref("int")), O, raiseInternal("TypeError", "__index__ returned non-int")) - rule checkIndex(.Obj) => .Obj - rule invokeBuiltin(obj("index",_), ListItem(O), .) => index(O) -> raiseInternal("TypeError", "object cannot be interpreted as an integer") + rule invokeBuiltin("index",_) => if hasmember(String2Id("a"), "__index__") : + String2Id("int"), .Expressions := getmember(String2Id("a"), "__index__", true, false, true) (.Arguments) newline + if istype(String2Id("int"), ref("int")) : + return String2Id("int") + else: + raiseInternal("TypeError", "__index__ returned non-int") + else: + raiseInternal("TypeError", "object cannot be interpreted as an integer") rule range(O, O2, O3, O4) => mutable("start" |-> intvalue(O) "stop" |-> intvalue(O2) "step" |-> intvalue(O3), O4) when intvalue(O3) =/=Int 0 rule range(_, _, O3, _) => raiseInternal("ValueError", "range() arg 3 must not be zero") when intvalue(O3) ==Int 0 - rule invokeBuiltin(obj("new_slice",_), ListItem(O:Object) ListItem(O2:Object), .) => newHelper(O, ref("slice"), .) ~> ref("new_slice") (O, ref("None"), O2, .Expressions) + //rule invokeBuiltin(obj("new_slice",_), ListItem(O:Object) ListItem(O2:Object), .) => newHelper(O, ref("slice"), .) ~> ref("new_slice") (O, ref("None"), O2, .Expressions) - rule invokeBuiltin(obj("new_slice",_), ListItem(O:Object) ListItem(O2:Object) ListItem(O3:Object), .) => newHelper(O, ref("slice"), .) ~> ref("new_slice") (O, O2, O3, ref("None"), .Expressions) + //rule invokeBuiltin(obj("new_slice",_), ListItem(O:Object) ListItem(O2:Object) ListItem(O3:Object), .) => newHelper(O, ref("slice"), .) ~> ref("new_slice") (O, O2, O3, ref("None"), .Expressions) - rule invokeBuiltin(obj("new_slice",_), ListItem(O) ListItem(O2) ListItem(O3) ListItem(O4:Object), .) => newHelper(O, ref("slice"), .) ~> mutable("start" |-> ref(id(O2)) "stop" |-> ref(id(O3)) "step" |-> ref(id(O4)), O) + //rule invokeBuiltin(obj("new_slice",_), ListItem(O) ListItem(O2) ListItem(O3) ListItem(O4:Object), .) => newHelper(O, ref("slice"), .) ~> mutable("start" |-> ref(id(O2)) "stop" |-> ref(id(O3)) "step" |-> ref(id(O4)), O) - rule invokeBuiltin(obj("indices_slice",_), ListItem(O) ListItem(O2), .) => indices(slicepart(getref(O, "start")), slicepart(getref(O, "stop")), slicepart(getref(O, "step")), ref("index")(O2, .Arguments)) + //rule invokeBuiltin(obj("indices_slice",_), ListItem(O) ListItem(O2), .) => indices(slicepart(getref(O, "start")), slicepart(getref(O, "stop")), slicepart(getref(O, "step")), ref("index")(O2, .Arguments)) rule slicepart(O) => test(plbool(O is ref("None")), O, index(O) -> raiseInternal("TypeError", "slice indices must be integers or None or have an __index__ method")) rule indices(StartObj:Object, StopObj:Object, StepObj:Object, LengthObj:Object) => raiseInternal("ValueError", "slice step cannot be zero") when intvalue(StepObj) ==Int 0 - rule indices(StartObj, StopObj, StepObj, LengthObj) => indices2(StartObj, StopObj, #if id(StepObj) ==K None #then 1 #else intvalue(StepObj) #fi, intvalue(LengthObj)) ... - ... "None" |-> None:Nat ... when id(StepObj) ==K None orElseBool intvalue(StepObj) =/=Int 0 + rule indices(StartObj, StopObj, StepObj, LengthObj) => indices2(StartObj, StopObj, #if id(StepObj) ==K NoneId #then 1 #else intvalue(StepObj) #fi, intvalue(LengthObj)) ... + ... "None" |-> NoneId ... when id(StepObj) ==K NoneId orElseBool intvalue(StepObj) =/=Int 0 - rule indices2(StartObj, StopObj, Step:Int, Length:Int) => indices3(#if id(StartObj) ==K None #then #if Step - ... "None" |-> None:Nat ... + rule indices2(StartObj, StopObj, Step:Int, Length:Int) => indices3(#if id(StartObj) ==K NoneId #then #if Step + ... "None" |-> NoneId ... rule indices3(Start:Int, Stop:Int, Step, Length) => indices4(#if Start . rule if O:Object : Ss:K else : Ss2:K => test(plbool(bool(O)), Ss, Ss2) - rule E:K if O else E2:K => test(plbool(bool(O)), E, E2) + rule E:K if O:Object else E2:K => test(plbool(bool(O)), E, E2) rule (. => lmark) ~> (while Condition:K : Ss else: Ss2) ~> (K:K => break) @@ -66,7 +66,7 @@ module PYTHON-SEMANTICS-STATEMENTS rule Stmt:K newline Ss => Stmt ~> Ss rule with O:Object : Ss => doWith(O . String2Id("__exit__"), O . String2Id("__enter__") (.Arguments), ., Ss) - rule with O:Object as T:Target : Ss => doWith(O . String2Id("__exit__"), O . String2Id("__enter__") (.Arguments), T, Ss) + rule with O:Object as T:Expression : Ss => doWith(O . String2Id("__exit__"), O . String2Id("__enter__") (.Arguments), T, Ss) syntax K ::= doWith(Expression, Expression, K, K) [seqstrict(1, 2)] diff --git a/python-semantics-strings.k b/python-semantics-strings.k index 54e9f4b..7ad9eb0 100644 --- a/python-semantics-strings.k +++ b/python-semantics-strings.k @@ -7,14 +7,16 @@ module PYTHON-SEMANTICS-STRINGS imports MACHINE-INTEGERS imports UNICODE - rule invokeBuiltin(obj("add_str",_), ListItem(O:Object) ListItem(O2:Object), .) => test(istype(O2, ref("str")), strvalue(O) +String strvalue(O2), raiseInternal("TypeError", ("Can't convert '" + name(gettype(O2)) + "' object to str implicitly"))) ... + //rule invokeBuiltin(obj("add_str",_), ListItem(O:Object) ListItem(O2:Object), .) => test(istype(O2, ref("str")), strvalue(O) +String strvalue(O2), raiseInternal("TypeError", ("Can't convert '" + name(gettype(O2)) + "' object to str implicitly"))) ... - rule invokeBuiltin(obj("eq_str",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "str", "str", bool(strvalue(O) ==String strvalue(O2))) ... - rule invokeBuiltin(obj("ne_str",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "str", "str", bool(strvalue(O) =/=String strvalue(O2))) ... + //rule invokeBuiltin(obj("eq_str",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "str", "str", bool(strvalue(O) ==String strvalue(O2))) ... + //rule invokeBuiltin(obj("ne_str",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "str", "str", bool(strvalue(O) =/=String strvalue(O2))) ... - rule [hash-str]: invokeBuiltin(obj("hash_str",_), ListItem(O), .) => test(lengthString(strvalue(O)) ==Int 0, 0, accumulate(strvalue(O), (asciiString(substrString(strvalue(O), 0, 1)) < + rule invokeBuiltin("str.__hash__", "self" |-> Self:Object) => return hashString(strvalue(Self), Seed, Width) ... ... "PYTHONHASHSEED" |-> Seed "sys.hash_info.width" |-> Width ... + rule hashString(S, Seed, Width) => test(lengthString(S) ==Int 0, 0, accumulate(S, (asciiString(substrString(S, 0, 1)) < accumulate((S:String => substrString(S, 1, lengthString(S) -Int 1)), (I:Int => (mult(Imag, I, Width) xorInt asciiString(substrString(S, 0, 1)))), _) ... ... "sys.hash_info.width" |-> Width "sys.hash_info.imag" |-> Imag ... when lengthString(S) =/=Int 0 - rule accumulate("", I, Len:Nat) => test((I xorInt Len xorInt hashSuffix(Seed, Width)) ==Int -1, -2, (I xorInt Len xorInt hashSuffix(Seed, Width))) ... + rule accumulate("", I, Len:Int) => test((I xorInt Len xorInt hashSuffix(Seed, Width)) ==Int -1, -2, (I xorInt Len xorInt hashSuffix(Seed, Width))) ... ... "PYTHONHASHSEED" |-> Seed "sys.hash_info.width" |-> Width ... - rule invokeBuiltin(obj("rpartition_str",_), ListItem(O) ListItem(Sep), .) => test(istype(Sep, ref("str")), #if rfindString(strvalue(O), strvalue(Sep), lengthString(strvalue(O))) ==Int -1 #then tuple("", "", strvalue(O), .Expressions) #else tuple(substrString(strvalue(O), 0, rfindString(strvalue(O), strvalue(Sep), lengthString(strvalue(O)))), strvalue(Sep), substrString(strvalue(O), rfindString(strvalue(O), strvalue(Sep), lengthString(strvalue(O))) +Int lengthString(strvalue(Sep)), lengthString(strvalue(O))), .Expressions) #fi, raiseInternal("TypeError", "Cannot convert object to str implicitly")) + //rule invokeBuiltin(obj("rpartition_str",_), ListItem(O) ListItem(Sep), .) => test(istype(Sep, ref("str")), #if rfindString(strvalue(O), strvalue(Sep), lengthString(strvalue(O))) ==Int -1 #then tuple("", "", strvalue(O), .Expressions) #else tuple(substrString(strvalue(O), 0, rfindString(strvalue(O), strvalue(Sep), lengthString(strvalue(O)))), strvalue(Sep), substrString(strvalue(O), rfindString(strvalue(O), strvalue(Sep), lengthString(strvalue(O))) +Int lengthString(strvalue(Sep)), lengthString(strvalue(O))), .Expressions) #fi, raiseInternal("TypeError", "Cannot convert object to str implicitly")) - rule invokeBuiltin(obj("ord",_), ListItem(O), .) => test(istype(O, ref("str")), test(length(strvalue(O), UTF-8) =/=Int 1, raiseInternal("TypeError", "ord() expected a character, but string of length " +String Int2String(length(strvalue(O), UTF-8)) +String " found"), codePoint(strvalue(O), UTF-8, 0)), raiseInternal("TypeError", "ord() expected string of length 1")) + //rule invokeBuiltin(obj("ord",_), ListItem(O), .) => test(istype(O, ref("str")), test(length(strvalue(O), UTF-8) =/=Int 1, raiseInternal("TypeError", "ord() expected a character, but string of length " +String Int2String(length(strvalue(O), UTF-8)) +String " found"), codePoint(strvalue(O), UTF-8, 0)), raiseInternal("TypeError", "ord() expected string of length 1")) - rule invokeBuiltin(obj("len_str",_), ListItem(O), .) => length(strvalue(O), UTF-8) + //rule invokeBuiltin(obj("len_str",_), ListItem(O), .) => length(strvalue(O), UTF-8) - rule invokeBuiltin(obj("rsplit_str",_), ListItem(O), .) => ref("rsplit_str")(O, ref("None"), -1, .Arguments) - rule invokeBuiltin(obj("rsplit_str",_), ListItem(O) ListItem(Sep), .) => ref("rsplit_str")(O, Sep, -1, .Arguments) - rule invokeBuiltin(obj("rsplit_str",_), ListItem(O) ListItem(Sep) ListItem(MaxSplit), .) => if Sep is ref("None") : rsplit(strvalue(O), ref("index")(MaxSplit, .Arguments)) else: test(istype(Sep, ref("str")), rsplit(strvalue(O), ref("index")(MaxSplit, .Arguments), strvalue(Sep)), raiseInternal("TypeError", "Cannot convert object to str implicitly")) + //rule invokeBuiltin(obj("rsplit_str",_), ListItem(O), .) => ref("rsplit_str")(O, ref("None"), -1, .Arguments) + //rule invokeBuiltin(obj("rsplit_str",_), ListItem(O) ListItem(Sep), .) => ref("rsplit_str")(O, Sep, -1, .Arguments) + //rule invokeBuiltin(obj("rsplit_str",_), ListItem(O) ListItem(Sep) ListItem(MaxSplit), .) => if Sep is ref("None") : rsplit(strvalue(O), ref("index")(MaxSplit, .Arguments)) else: test(istype(Sep, ref("str")), rsplit(strvalue(O), ref("index")(MaxSplit, .Arguments), strvalue(Sep)), raiseInternal("TypeError", "Cannot convert object to str implicitly")) syntax ObjRef ::= rsplit(Expression, Expression) [strict] | rsplit(Expression, Expression, String) [strict(1, 2)] @@ -44,7 +46,7 @@ module PYTHON-SEMANTICS-STRINGS rule rsplit(S:Object, MaxSplit:Object, Sep) => test(intvalue(MaxSplit) ==Int 0, [S], test(rfindString(strvalue(S), Sep, lengthString(strvalue(S))) ==Int -1, [strvalue(S)], rsplit(ref("rpartition_str")(strvalue(S), Sep, .Arguments)[0], intvalue(MaxSplit) -Int 1, Sep) + [ref("rpartition_str")(strvalue(S), Sep, .Arguments)[2]])) //TODO: rsplit(None, ...) - rule invokeBuiltin(obj("format_str",_), ListItem(Format) L:List, M:Map) => format(strvalue(Format), tuple(DeListify(L)), {DeMapify(M)}, .K) + //rule invokeBuiltin(obj("format_str",_), ListItem(Format) L:List, M:Map) => format(strvalue(Format), tuple(DeListify(L)), {DeMapify(M)}, .K) syntax ObjRef ::= format(String, Expression, Expression, K) [strict(2, 3)] | formatField(String, String, Object, Object, K) @@ -105,11 +107,11 @@ module PYTHON-SEMANTICS-STRINGS rule convertField(O:Object, Conversion) => raiseInternal("ValueError", "unknown conversion specifier" +String substrString(Conversion, 1, 1)) when substrString(Conversion, 0, 1) ==String "!" andBool (substrString(Conversion, 2, 1) ==String ":" orBool lengthString(Conversion) ==Int 2) rule convertField(O:Object, Conversion) => raiseInternal("ValueError", "expected ':' after format specifier") when substrString(Conversion, 0, 1) ==String "!" andBool (substrString(Conversion, 1, 1) ==String "s" orBool substrString(Conversion, 1, 1) ==String "r" orBool substrString(Conversion, 1, 1) ==String "a") andBool substrString(Conversion, 2, 1) =/=String "" andBool substrString(Conversion, 2, 1) =/=String ":" - rule invokeBuiltin(obj("format",_), ListItem(O:Object), .) => ref("format")(O, "") - rule invokeBuiltin(obj("format",_), ListItem(O:Object) ListItem(Format:Object), .) => checkFormat(getmember(O, "__format__", true, false, true)(Format)) + //rule invokeBuiltin(obj("format",_), ListItem(O:Object), .) => ref("format")(O, "") + //rule invokeBuiltin(obj("format",_), ListItem(O:Object) ListItem(Format:Object), .) => checkFormat(getmember(O, "__format__", true, false, true)(Format)) rule checkFormat(O:Object) => test(istype(O, ref("str")), O, raiseInternal("TypeError", "__format__ method did not return string")) - rule invokeBuiltin(obj("format_object",_), ListItem(O:Object) ListItem(Format:Object), .) => getmember(ref("str")(O), "__format__", true, false, true)(Format) + //rule invokeBuiltin(obj("format_object",_), ListItem(O:Object) ListItem(Format:Object), .) => getmember(ref("str")(O), "__format__", true, false, true)(Format) syntax FormatSpec ::= parseFormatSpec(String) [function] | parseFormatSpec(String, String) [function] @@ -124,7 +126,7 @@ module PYTHON-SEMANTICS-STRINGS syntax ObjRef ::= doFormatStr(String, FormatSpec) - rule invokeBuiltin(obj("__format___str",_), ListItem(O:Object) ListItem(Format:Object), .) => doFormatStr(strvalue(O), parseFormatSpec(strvalue(Format))) + //rule invokeBuiltin(obj("__format___str",_), ListItem(O:Object) ListItem(Format:Object), .) => doFormatStr(strvalue(O), parseFormatSpec(strvalue(Format))) rule parseFormatSpec(Format) => #if substrString(Format, 1, 1) =/=String "<" andBool substrString(Format, 1, 1) =/=String ">" andBool substrString(Format, 1, 1) =/=String "=" andBool substrString(Format, 1, 1) =/=String "^" #then parseFormatSpec("", Format) #else parseFormatSpec(substrString(Format, 0, 1), substrString(Format, 1, lengthString(Format))) #fi rule parseFormatSpec(Fill, Format) => #if substrString(Format, 0, 1) ==String "<" orBool substrString(Format, 0, 1) ==String ">" orBool substrString(Format, 0, 1) ==String "=" orBool substrString(Format, 0, 1) ==String "^" #then parseFormatSpec(Fill, substrString(Format, 0, 1), substrString(Format, 1, lengthString(Format))) #else parseFormatSpec(Fill, "", Format) #fi rule parseFormatSpec(Fill, Align, Format) => #if substrString(Format, 0, 1) ==String "+" orBool substrString(Format, 0, 1) ==String "-" orBool substrString(Format, 0, 1) ==String " " #then parseFormatSpec(Fill, Align, substrString(Format, 0, 1), substrString(Format, 1, lengthString(Format))) #else parseFormatSpec(Fill, Align, "", Format) #fi diff --git a/python-semantics-syntax.k b/python-semantics-syntax.k index c95facf..93aae9d 100644 --- a/python-semantics-syntax.k +++ b/python-semantics-syntax.k @@ -14,9 +14,12 @@ module PYTHON-SEMANTICS-SYNTAX syntax Expression ::= ObjRef | Null | Undefined + | ObjId syntax Null ::= ".Obj" + syntax ObjectPointer ::= Object | Null + syntax Undefined ::= "undefined" "(" String ")" rule isKResult(obj(_,_)) => true diff --git a/python-semantics-try.k b/python-semantics-try.k index a191014..0ce41fd 100644 --- a/python-semantics-try.k +++ b/python-semantics-try.k @@ -55,10 +55,10 @@ module PYTHON-SEMANTICS-TRY (_ => C:Bag) when B =/=K ref("None") - rule (. => savetb(mutable("tb_next" |-> Tb "tb_frame" |-> ref(Frame), ref("traceback")))) ~> raise ... + rule (. => savetb(mutable("tb_next" |-> Tb "tb_frame" |-> ref(Frame), ref("traceback")))) ~> raise ~> K ... ref(B) - Frame + ref(Frame) try(_, _, _:Bag, _, false) => . ... ... ... @@ -86,7 +86,7 @@ module PYTHON-SEMANTICS-TRY rule raise O:Object from O2:Object => doRaise(test(istype(O, ref("type")), O(.Arguments), O), test(istype(O2, ref("type")), O2(.Arguments), O2), false) ... rule doRaise(O, O2, T:Bool) => test(istype(O, ref("BaseException")), test(or(id(O2) ==K NoneId,istype(O2, ref("BaseException"))), (setcause(O, O2) ~> setref(id(O), "__suppress_context__", test(T, ref("False"), test(id(O2) ==K NoneId, ref("True"), ref("False")))) ~> savex(O) ~> savetb(mutable("tb_next" |-> ref("None") "tb_frame" |-> ref(Frame), ref("traceback"))) ~> raise) , raiseInternal("TypeError", "exception causes must derive from BaseException")), raiseInternal("TypeError", "exceptions must derive from BaseException")) ... - Frame + ref(Frame) ... "None" |-> NoneId ... rule savex(obj(B,_)) => . ... @@ -125,8 +125,7 @@ module PYTHON-SEMANTICS-TRY rule doExcept(Type:Object, Except, X) => test(istype(B, Type), test(Id2String(X) ==String "", except: Except, (X, .Expressions := B ~> except: (try: Except finally: unbind(X)))), .) ... B - 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") -#then ref("None") #else Ex . String2Id("__traceback__") #fi, .Expressions) ... - Ex + //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") #then ref("None") #else Ex . String2Id("__traceback__") #fi, .Expressions) ... + // Ex endmodule diff --git a/python-semantics-tuples.k b/python-semantics-tuples.k index da1ae5c..0a184ad 100644 --- a/python-semantics-tuples.k +++ b/python-semantics-tuples.k @@ -5,23 +5,40 @@ module PYTHON-SEMANTICS-TUPLES imports PYTHON-SEMANTICS-LISTS imports MACHINE-INTEGERS - rule invokeBuiltin(obj("add_tuple",_), ListItem(O:Object) ListItem(O2:Object), .) => test(and(istype(O, ref("tuple")), istype(O2, ref("tuple"))), immutable(list(listvalue(O) listvalue(O2)),ref("tuple")), raiseInternal("TypeError", "can only concatenate tuple to tuple")) - - rule invokeBuiltin(obj("contains_tuple",_), ListItem(O) ListItem(O2), .) => contains(list(listvalue(O)), O2) - - rule invokeBuiltin(obj("getitem_tuple",_), ListItem(O) ListItem(O2), .) => test(istype(O2, ref("int")), test(intvalue(O2) >=Int 0 -Int lengthList listvalue(O) andBool intvalue(O2) =Int 0, get(listvalue(O), intvalue(O2)), get(listvalue(O), lengthList listvalue(O) +Int intvalue(O2))), raiseInternal("IndexError", "tuple index out of range")), test(istype(O2, ref("slice")), ref("tuple")(slice(O, O2)), raiseInternal("TypeError", "tuple indices must be integers or slices"))) - - rule invokeBuiltin(obj("len_tuple",_), ListItem(O), .) => lengthList listvalue(O) - - rule invokeBuiltin(obj("new_tuple",_), ListItem(O), .) => newHelper(O, ref("tuple"), .) ~> immutable(list(.), O) - rule invokeBuiltin(obj("new_tuple",_), ListItem(O) ListItem(O2), .) => newHelper(O, ref("tuple"), .) ~> iterate(O2, .) ~> immutable(list(.), O) + rule invokeBuiltin("tuple.__add__","self" |-> Self:Object "other" |-> Other:Object) => + if istype(Self, ref("tuple")) and istype(Other, ref("tuple")) : + return immutable(list(listvalue(Self) listvalue(Other)), ref("tuple")) + else: + raiseInternal("TypeError", "cano only concatenate tuple to tuple") + + //rule invokeBuiltin(obj("contains_tuple",_), ListItem(O) ListItem(O2), .) => contains(list(listvalue(O)), O2) + + rule invokeBuiltin("tuple.__getitem__","self" |-> Self:Object "key" |-> Key:Object) => + if istype(Key, ref("int")) : + (if intvalue(Key) >=Int 0 -Int lengthList listvalue(Self) andBool intvalue(Key) =Int 0 : + return get(listvalue(Self), intvalue(Key)) + else: + return get(listvalue(Self), lengthList listvalue(Self) +Int intvalue(Key))) + else: + raiseInternal("IndexError", "tuple index out of range")) + else: + if istype(Key, ref("slice")) : + return ref("tuple")(slice(Self, Key)) + else: + raiseInternal("TypeError", "tuple indices must be integers or slices") + + rule invokeBuiltin("tuple.__len__", "self" |-> O:Object) => return lengthList listvalue(O) + + //rule invokeBuiltin(obj("new_tuple",_), ListItem(O), .) => newHelper(O, ref("tuple"), .) ~> immutable(list(.), O) + //rule invokeBuiltin(obj("new_tuple",_), ListItem(O) ListItem(O2), .) => newHelper(O, ref("tuple"), .) ~> iterate(O2, .) ~> immutable(list(.), O) rule (list(L:List) => .) ~> immutable(list(_ => Refify(Idify(L))), _) - rule invokeBuiltin(obj("eq_tuple",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "tuple", "tuple", (ref("bool") (equalList(listvalue(O), (listvalue(O2)))))) - rule invokeBuiltin(obj("ne_tuple",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "tuple", "tuple", not equalList(listvalue(O), listvalue(O2))) + //rule invokeBuiltin(obj("eq_tuple",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "tuple", "tuple", (ref("bool") (equalList(listvalue(O), (listvalue(O2)))))) + //rule invokeBuiltin(obj("ne_tuple",_), ListItem(O) ListItem(O2), .) => binaryOp(O, O2, "tuple", "tuple", not equalList(listvalue(O), listvalue(O2))) - rule invokeBuiltin(obj("hash_tuple",_), ListItem(O), .) => accumulateTuple(Begin, Mult, listvalue(O)) ... - ... "sys.hash_info.imag" |-> Mult "tuple.__hash__:begin" |-> Begin ... + //rule invokeBuiltin(obj("hash_tuple",_), ListItem(O), .) => accumulateTuple(Begin, Mult, listvalue(O)) ... + // ... "sys.hash_info.imag" |-> Mult "tuple.__hash__:begin" |-> Begin ... syntax ObjRef ::= accumulateTuple(Int, Int, List) diff --git a/python-syntax.k b/python-syntax.k index 1e6487a..e64fbdb 100755 --- a/python-syntax.k +++ b/python-syntax.k @@ -150,7 +150,9 @@ module PYTHON-SYNTAX imports PYTHON-TOKENS | "nonlocal" NAMES > "if" Expression ":" Statements "else" ":" Statements [strict(1)] | "while" Expression ":" Statements "else" ":" Statements + | "for" Target "in" Expression ":" Statements | "for" Target "in" Expression ":" Statements "else" ":" Statements + | "try" ":" Statements ExceptClauses | "try" ":" Statements ExceptClauses "else" ":" Statements //"finally" ":" Statements | "try" ":" Statements ExceptClauses "else" ":" Statements "finally" ":" Statements | "try" ":" Statements "finally" ":" Statements