diff --git a/src/ecLexer.mll b/src/ecLexer.mll index 582f16dc1..b33c5fae8 100644 --- 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 index bc429ad56..8aaf733aa 100644 --- 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 index faebf69ad..1e58ca8ba 100644 --- 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 index 687e5a854..5f0abbd43 100644 --- 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