Set For Loop Iterable Property

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

More formally,

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.

Comments

Please log in to add comments