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
87 lines (75 loc) · 4.6 KB
/
Copy pathpython-semantics-environment.k
File metadata and controls
87 lines (75 loc) · 4.6 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
require "python-semantics-literals.k"
module PYTHON-SEMANTICS-ENVIRONMENT
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 <k> bind(X:Id, B:Expression) => doBind(Id2String(X), B, ref(N)) ...</k>
<frameObject> ref(N) </frameObject>
rule <k> X:Id => envLookup(Id2String(X),ref(N),getref2(ref(N), "f_code")) ...</k>
<frameObject> ref(N:Int) </frameObject>
rule envLookup(S:String, Frame:Object, Code:Object) =>
(Frame . String2Id("f_locals") [S]
if
S in Frame . String2Id("f_locals")
else
raiseInternal("UnboundLocalError", "local variable '" +String S +String "' referenced before assignment"))
if
S in Code . String2Id("co_varnames") or
S in Code . String2Id("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 Code . String2Id("co_freevars")
else
Frame . String2Id("f_globals") [S]
if
S in Frame . String2Id("f_globals")
else
Frame . String2Id("f_builtins") [S]
if
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 <k> doBind(S, B, Frame) => doBind2(S, B, Frame, Frame . String2Id("f_code")) ...</k> when notBool getattr(Frame, "f_isbuiltin")
rule <k> doBind(S, ref(0), obj(Frame,_)) => . ...</k>
<object>...
<id>Frame</id>
<oattrs>... "f_isbuiltin" |-> true "f_locals" |-> map(M => M[undef / S]) ...</oattrs>
...</object>
rule <k> doBind(S, B, obj(Frame,_)) => . ...</k>
<object>...
<id>Frame</id>
<oattrs>... "f_isbuiltin" |-> true "f_locals" |-> map(M => M[B / S]) ...</oattrs>
...</object> when B =/=K ref(0)
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") :
test(B ==K 0,
(del Frame . String2Id("f_locals") [S], .Expressions),
Frame . String2Id("f_locals") [S], .Expressions := ref(B))
else: pass ~>
if S in Code . String2Id("co_cellvars") or
S in Code . String2Id("co_freevars") :
test(B ==K 0,
setattr(id(getref(Frame, "f_cells")[S]), "cell_contents", .Obj),
setref(id(getref(Frame, "f_cells")[S]), "cell_contents", ref(B)))
else: pass ~>
if S in Code . String2Id("co_freevars") :
doBind(S, ref(B), getref2(getref(Frame, "f_cells")[S], "cell_frame"))
else: pass ~>
if S in Code . String2Id("co_names") :
test(B ==K 0,
(del ((Frame . String2Id("f_globals") [S]), .Expressions)),
(((Frame . String2Id("f_globals") [S]), .Expressions) := ref(B)))
else: pass
syntax #Id ::= "f_globals" | "f_locals" | "f_back"
rule <k> invokeBuiltin("globals",_) => return Frame . f_back . f_globals ...</k>
<frameObject> Frame </frameObject>
rule <k> invokeBuiltin("locals",_) => return Frame . f_back . f_locals ...</k>
<frameObject> Frame </frameObject>
endmodule