parsing for mem_restr

EasyCrypt · Apr 22, 2024 · cfc42a6 · cfc42a6
1 parent 919650b
commit cfc42a6
Show file tree

Hide file tree

Showing 4 changed files with 26 additions and 28 deletions.
diff --git a/src/ecLexer.mll b/src/ecLexer.mll
@@ -200,6 +200,7 @@
     "section"     , SECTION    ;        (* KW: global *)
     "type"        , TYPE       ;        (* KW: global *)
     "class"       , CLASS      ;        (* KW: global *)
+    "classical"   , CLASSICAL  ;        (* KW: global *)
     "instance"    , INSTANCE   ;        (* KW: global *)
     "print"       , PRINT      ;        (* KW: global *)
     "search"      , SEARCH     ;        (* KW: global *)

diff --git a/src/ecMemRestr.ml b/src/ecMemRestr.ml
@@ -476,16 +476,3 @@ let is_mem env sign x s =
 
 let has_quantum env s =
   not (disjoint env s Quantum)
-
-
-
-
-glob M
-
-
-glob (mp, MT)
-
-
-globfun(ff)
-
-glo
diff --git a/src/ecParser.mly b/src/ecParser.mly
@@ -408,6 +408,7 @@
 %token CFOLD
 %token CHANGE
 %token CLASS
+%token CLASSICAL
 %token CLEAR
 %token CLONE
 %token COLON
@@ -1710,13 +1711,23 @@ mod_params:
 (* -------------------------------------------------------------------- *)
 (* Memory restrictions *)
 
-mem_restr_el:
-  | PLUS  el=f_or_mod_ident { PMPlus el }
-  | MINUS el=f_or_mod_ident { PMMinus el }
-  |       el=f_or_mod_ident { PMDefault el }
-
 mem_restr:
-  | ol=rlist0(mem_restr_el,COMMA) { ol }
+| i=loc(UINT) {
+   if BI.equal (unloc i) BI.zero then PMempty
+   else parse_error (loc i) (Some "Only 0 is accepted")
+  }
+
+| QUANTUM                         { PMquantum      }
+| CLASSICAL                       { PMclassical    }
+| el=f_or_mod_ident               { PMvar el       }
+| s1=mem_restr PLUS  s2=mem_restr { PMunion(s1,s2) }
+| s1=mem_restr MINUS s2=mem_restr { PMdiff (s1,s2) }
+| s1=mem_restr HAT   s2=mem_restr { PMinter(s1,s2) }
+| LPAREN s=mem_restr RPAREN       { s              }
+
+| PLUS  el=mem_restr          { PMunion(PMclassical, el) }
+| MINUS el=mem_restr          { PMdiff (PMclassical, el) }
+
 
 (* -------------------------------------------------------------------- *)
 (* qident optionally taken in a (implicit) module parameters. *)
@@ -1741,8 +1752,6 @@ mod_restr_el:
 mod_restr:
   | LBRACE mr=mem_restr RBRACE
     { { pmr_mem = mr; pmr_procs = [] } }
-  | LBRACKET l=rlist1(mod_restr_el,COMMA) RBRACKET
-    { { pmr_mem = []; pmr_procs = l } }
   | LBRACE mr=mem_restr RBRACE LBRACKET l=rlist1(mod_restr_el,COMMA) RBRACKET
     { { pmr_mem = mr;	pmr_procs = l } }
   | LBRACKET l=rlist1(mod_restr_el,COMMA) RBRACKET LBRACE mr=mem_restr RBRACE

diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml
@@ -166,14 +166,15 @@ type f_or_mod_ident =
   | FM_FunOrVar of pgamepath
   | FM_Mod of pmsymbol located
 
-
-type pmod_restr_mem_el =
-  | PMPlus    of f_or_mod_ident
-  | PMMinus   of f_or_mod_ident
-  | PMDefault of f_or_mod_ident
-
 (* A memory restricition. *)
-type pmod_restr_mem = pmod_restr_mem_el list
+type pmod_restr_mem =
+  | PMempty
+  | PMquantum
+  | PMclassical
+  | PMvar     of f_or_mod_ident
+  | PMunion   of pmod_restr_mem * pmod_restr_mem
+  | PMinter   of pmod_restr_mem * pmod_restr_mem
+  | PMdiff    of pmod_restr_mem * pmod_restr_mem
 
 (* -------------------------------------------------------------------- *)
 type pmemory   = psymbol