Skip to content

Commit

Permalink
pancake: update loopLang for shared memory
Browse files Browse the repository at this point in the history
  • Loading branch information
mktnk3 committed Nov 27, 2023
1 parent e771ff7 commit 4a2444c
Showing 1 changed file with 3 additions and 0 deletions.
3 changes: 3 additions & 0 deletions pancake/loopLangScript.sml
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,7 @@ Datatype:
| Continue
| Raise num
| Return num
| ShMem memop num ('a exp)
| Tick
| Mark prog
| Fail
Expand Down Expand Up @@ -94,6 +95,7 @@ Definition assigned_vars_def:
(assigned_vars (Seq p q) = assigned_vars p ++ assigned_vars q) ∧
(assigned_vars (If cmp n r p q ns) = assigned_vars p ++ assigned_vars q) ∧
(assigned_vars (LocValue n m) = [n]) ∧
(assigned_vars (ShMem op n e) = [n]) ∧
(assigned_vars (Mark p) = assigned_vars p) ∧
(assigned_vars (Loop _ p _) = assigned_vars p) ∧
(assigned_vars (Call NONE _ _ _) = []) ∧
Expand Down Expand Up @@ -131,6 +133,7 @@ Definition acc_vars_def:
acc_vars p1 (acc_vars p2 (insert n () l))) /\
(acc_vars (LocValue n m) l = insert n () l) /\
(acc_vars (Assign n exp) l = insert n () l) /\
(acc_vars (ShMem op n exp) l = insert n () l) /\
(acc_vars (Store exp n) l = l) /\
(acc_vars (SetGlobal w exp) l = l) /\
(acc_vars (LoadByte n m) l = insert m () l) /\
Expand Down

0 comments on commit 4a2444c

Please sign in to comment.