Allow pure constraints in preconditions

hipsleek · May 18, 2023 · a4a0cf7 · a4a0cf7
1 parent 23f5f21
commit a4a0cf7
Showing 1 changed file with 6 additions and 3 deletions.
diff --git a/parsing/parser.mly b/parsing/parser.mly
@@ -2616,12 +2616,11 @@ heapES:
 
 
 stagedSpecArgs :
-  | h=heapkappa COMMA rest=separated_nonempty_list(COMMA, effect_trace_value) { (True, h, rest) }
-  | p=pure_formula CONJUNCTION h=heapkappa COMMA rest=separated_nonempty_list(COMMA, effect_trace_value) { (p, h, rest) }
+  | s=statefml COMMA rest=separated_nonempty_list(COMMA, effect_trace_value) { (fst s, snd s, rest) }
 
 stagedSpec1 : 
   | EXISTS vs=nonempty_list(LIDENT) { Exists vs }
-  | REQUIRES heap=heapkappa { Require (True, heap) }
+  | REQUIRES f=statefml { Require (fst f, snd f) }
   | constr=UIDENT args=delimited(LPAREN, stagedSpecArgs, RPAREN)
   {
     match constr, args with
@@ -2641,6 +2640,10 @@ stagedSpec1 :
     HigherOrder (True, EmptyHeap, (constr, init), last)
   }
 
+statefml:
+  | h=heapkappa { (True, h) }
+  | p=pure_formula CONJUNCTION h=heapkappa { (p, h) }
+
 heapkappa:
 | EMP { EmptyHeap }
 | str=LIDENT MINUSGREATER args = pure_formula_term