forked from runtimeverification/python-semantics
-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathpython-semantics-environment.k
More file actions
98 lines (85 loc) · 5.28 KB
/
Copy pathpython-semantics-environment.k
File metadata and controls
98 lines (85 loc) · 5.28 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
require "python-semantics-common.k"
module PYTHON-SEMANTICS-ENVIRONMENT
imports PYTHON-SEMANTICS-COMMON
syntax ObjRef ::= "envLookup" "(" String "," Exp "," Exp ")" [strict(2, 3)]
syntax K ::= doBind2(String, Exp, Exp, Exp) [strict(3, 4)]
rule unbind(X) => bind(X, ref(0)) [macro]
rule <k> bind(X:Id, B:Exp) => doBind(Id2String(X), B, ref(N)) ...</k>
<frameObject> N </frameObject>
rule <k> X:Id => envLookup(Id2String(X),ref(N),ref(N) . String2Id("f_code")) ...</k>
<frameObject> N:Int </frameObject>
syntax #Id ::= "f_locals" | "f_globals"
rule envLookup(S:String, Frame:Object, Code:Object) =>
(getref(Frame, "f_locals") [S]
if
S in getref(Frame, "f_locals")
else
raiseInternal("UnboundLocalError", "local variable '" +String S +String "' referenced before assignment"))
if
S in getref(Code, "co_varnames") or
S in getref(Code, "co_cellvars")
else
test(getattr2(getref(Frame, "f_cells")[S], "cell_contents") ==Obj .Obj,
raiseInternal("NameError", "free variable '" +String S +String "' referenced before assignment in enclosing scope"),
getref2(getref(Frame, "f_cells")[S], "cell_contents"))
if
S in getref(Code, "co_freevars")
else
(try:
getref(Frame, "f_locals") [S]
except ref("KeyError"):
(try:
getref(Frame, "f_globals") [S]
except ref("KeyError"):
(try:
getref(Frame, "f_builtins") [S]
except ref("KeyError"):
raiseInternal("NameError", "name '" +String S +String "' is not defined"))))::K
rule doBind(S, B, Frame) => doBind2(S, B, Frame, getref2(Frame, "f_code"))
rule doBind2(S, B, Frame, Code:Object) =>
test(getattr(Code, "co_type"),
(if S in getref(Code, "co_nonlocals") :
STOREDEREF(S, B, Frame, Code)
else:
if S in getref(Code, "co_globals") :
STOREGLOBAL(S, B, Frame, Code)
else:
STORENAME(S, B, Frame, Code)),
if S in getref(Code, "co_names") :
STOREGLOBAL(S, B, Frame, Code)
else:
STOREDEREF(S, B, Frame, Code))
syntax K ::= STOREDEREF(String, K, Exp) [strict(3)]
rule STOREDEREF(S, ref(B), Frame:Object) => STOREDEREF(S, ref(B), Frame, getref2(Frame, "f_code"))
rule STOREDEREF(S:String, ref(B:ObjId), Frame:Object, Code:Object) =>
if S in getref(Code, "co_varnames") or
S in getref(Code, "co_cellvars") or
S in getref(Code, "co_freevars") :
test(getattr(Code, "co_type"),
.K,
test(B ==K 0,
(if S in getref(Frame, "f_locals") : del getref(Frame, "f_locals") [S] else: raiseInternal("UnboundLocalError", "local variable '" +String S +String "' referenced before assignment")),
getref(Frame, "f_locals") [S] = ref(B)))
else: pass ~>
if S in getref(Code, "co_cellvars") or
S in getref(Code, "co_freevars") :
test(B ==K 0,
setattr(id(getref(Frame, "f_cells")[S]), "cell_contents", .Obj),
setref(id(getref(Frame, "f_cells")[S]), "cell_contents", ref(B)))
else: pass ~>
if S in getref(Code, "co_freevars") :
STOREDEREF(S, ref(B), getref2(getref(Frame, "f_cells")[S], "cell_frame"))
else: pass
rule STOREGLOBAL(S:String, ref(B:ObjId), Frame:Object, Code:Object) =>
test(B ==K 0,
(if S in getref(Frame, "f_globals") : del ((getref(Frame, "f_globals") [S])) else: raiseInternal("NameError", "name '" +String S +String "' is not defined")),
(getref(Frame, "f_globals") [S] = ref(B)))
rule STORENAME(S:String, ref(B:ObjId), Frame:Object, Code:Object) =>
test(B ==K 0,
(if S in getref(Frame, "f_locals") : del getref(Frame, "f_locals") [S] else: raiseInternal("NameError", "name '" +String S +String "' is not defined")),
getref(Frame, "f_locals") [S] = ref(B))
rule [globals]: <k> invokeBuiltin(obj("globals",_), ., .) => ref(N) . f_globals ...</k>
<frameObject> N </frameObject>
rule <k> invokeBuiltin(obj("locals",_), ., .) => ref(N) . f_locals ...</k>
<frameObject> N </frameObject>
endmodule