Set For Loop Iterable Property

After the "for" statement iterable has finished evaluating, we save the result to the "control" map.

More formally,

if the following are true:

  • the line at time t = i
  • the tab at time t = j
  • statement at line i, tab j = for target in iterable_ex:
  • Expression Stack at time t = [ [ ], [ ] ]
  • Value Stack at time t = [ [ Python reference index, [ ] ], v_stack ]
  • the element at index index of stack (Python Object Store at time t) = Python list elements

then Control Map at time (t + 1) = result of storing (trio ("for", i, elements)) at key: j in map: (Control Map at time t)

LW Python saves the iterable in the "control" map so that it can go through each element in the "for" loop body. For example,

  • the line at time 9 = 2
  • the tab at time 9 = 0
  • statement at line 2, tab 0 = for value in numbers:
  • Expression Stack at time 9 = [ [ ], [ ] ]
  • Value Stack at time 9 = [ [ Python reference 0, [ ] ], [ ] ]
  • Control Map at time 9 = [ ]
  • Python Object Store at time 9 = [ [1, 2, 3], [ ] ]

We claim that:

the element at index 0 of stack (Python Object Store at time 9) = [1, 2, 3]

Then we can conclude that:

Control Map at time (9 + 1) = result of storing (trio ("for", 2, [ 1, [ 2, [ 3, [ ] ] ] ])) at key: 0 in map: (Control Map at time 9)

We claim that:

result of storing (trio ("for", 2, [ 1, [ 2, [ 3, [ ] ] ] ])) at key: 0 in map: (Control Map at time 9) = [ entry 0: (trio ("for", 2, [ 1, [ 2, [ 3, [ ] ] ] ])), [ ] ]

Then we conclude that:

Control Map at time (9 + 1) = [ entry 0: (trio ("for", 2, [ 1, [ 2, [ 3, [ ] ] ] ])), [ ] ]

Which simplifies to:

Control Map at time 10 = [ entry 0: (trio ("for", 2, [ 1, [ 2, [ 3, [ ] ] ] ])), [ ] ]

See the full proof here.

Try stepping through the simulator to see LW Python update the "Control" map.

Code Editor
numbers = [1, 2, 3]
for value in numbers:
x = value * 4


LW Python State
Current Line1Current Tab0Time0
LW Python Simulator

Comments

Please log in to add comments