pancake: scope checker, updates for shared memory

CakeML · Mar 20, 2024 · 7db505e · 7db505e
1 parent 3e8daf1
commit 7db505e
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/pancake/panScopeScript.sml b/pancake/panScopeScript.sml
@@ -86,6 +86,10 @@ Definition scope_check_prog_def:
     scope_check_exps ctxt [ptr1;len1;ptr2;len2] ∧
   scope_check_prog ctxt (Raise eid excp) = scope_check_exp ctxt excp ∧
   scope_check_prog ctxt (Return rt) = scope_check_exp ctxt rt ∧
+  scope_check_prog ctxt (ShMem mop v e) =
+    (if ¬MEM v ctxt.vars
+        then SOME (v, ctxt.fname)
+     else scope_check_exp ctxt e) ∧
   scope_check_prog ctxt Tick = NONE
 End