[refactoring]: split parser into multiple components

src/dune

@@ -24,7 +24,3 @@
  (libraries batteries camlp-streams dune-build-info dune-site inifiles why3 yojson zarith ecLib))
 
 (ocamllex ecLexer)
-
-(menhir
- (modules ecParser)
- (flags --table --explain))

src/parser/dune

@@ -0,0 +1,12 @@
+(menhir
+ (modules
+    ecParserPrelude
+    ecParserTokens
+    ecParserIdents
+    ecParserExpressions
+    ecParserFormulas
+    ecParserTactics
+    ecParserCloning
+    ecParser)
+ (merge_into ecParser)
+ (flags --table --explain))

src/parser/ecParserCloning.mly

@@ -0,0 +1,164 @@
+%%
+(* -------------------------------------------------------------------- *)
+(* Theory cloning                                                       *)
+
+clone_import:
+| EXPORT  { `Export  }
+| IMPORT  { `Import  }
+| INCLUDE { `Include }
+
+clone_opt:
+| b=boption(MINUS) ABSTRACT { (not b, `Abstract) }
+
+clone_opts:
+| xs=bracket(clone_opt+) { xs }
+
+clone_with:
+| WITH x=plist1(clone_override, COMMA) { x }
+
+clone_lemma_tag:
+|       x=ident { (`Include, x) }
+| MINUS x=ident { (`Exclude, x) }
+
+clone_lemma_base:
+| STAR x=bracket(clone_lemma_tag+)?
+    { `All (odfl [] x) }
+
+| x=_ident
+    { `Named x }
+
+clone_lemma_1_core:
+| l=genqident(clone_lemma_base) {
+    match unloc l with
+    | (xs, `Named x ) -> `Named (mk_loc l.pl_loc (xs, x), `Alias)
+    | (xs, `All tags) -> begin
+      match List.rev xs with
+      | []      -> `All (None, tags)
+      | x :: xs -> `All (Some (mk_loc l.pl_loc (List.rev xs, x)), tags)
+    end
+  }
+
+clone_lemma_1:
+| cl=clone_lemma_1_core
+    { { pthp_mode = cl; pthp_tactic = None; } }
+
+| cl=clone_lemma_1_core BY t=tactic_core
+    { { pthp_mode = cl; pthp_tactic = Some t; } }
+
+clone_lemma:
+| x=plist1(clone_lemma_1, COMMA) { x }
+
+clone_proof:
+| PROOF x=clone_lemma { x }
+
+clone_rename_kind:
+| TYPE        { `Type    }
+| OP          { `Op      }
+| PRED        { `Pred    }
+| LEMMA       { `Lemma   }
+| MODULE      { `Module  }
+| MODULE TYPE { `ModType }
+| THEORY      { `Theory  }
+
+clone_rename_1:
+| k=bracket(plist1(clone_rename_kind, COMMA))? r1=loc(STRING) AS r2=loc(STRING)
+    { (odfl [] k, (r1, r2)) }
+
+clone_rename:
+| RENAME rnm=clone_rename_1+ { rnm }
+
+clone_clear_1:
+| ABBREV qs=qoident+
+  { List.map (fun x -> (`Abbrev, x)) qs }
+
+clone_clear:
+| REMOVE cl=clone_clear_1+ { List.flatten cl }
+
+opclmode:
+| EQ       { `Alias         }
+| LARROW   { `Inline `Clear }
+| LE       { `Inline `Keep  }
+
+cltyparams:
+| empty { [] }
+| x=tident { [x] }
+| xs=paren(plist1(tident, COMMA)) { xs }
+
+clone_override:
+| TYPE ps=cltyparams x=qident mode=opclmode t=loc(type_exp)
+   { (x, PTHO_Type (`BySyntax (ps, t), mode)) }
+
+| OP st=nosmt x=qoident tyvars=bracket(tident*)?
+    p=ptybinding1* sty=ioption(prefix(COLON, loc(type_exp)))
+    mode=loc(opclmode) f=form
+
+   { let ov = {
+       opov_nosmt  = st;
+       opov_tyvars = tyvars;
+       opov_args   = List.flatten p;
+       opov_retty  = odfl (mk_loc mode.pl_loc PTunivar) sty;
+       opov_body   = f;
+     } in
+
+     (x, PTHO_Op (`BySyntax ov, unloc mode)) }
+
+| PRED x=qoident tyvars=bracket(tident*)? p=ptybinding1* mode=loc(opclmode) f=form
+   { let ov = {
+       prov_tyvars = tyvars;
+       prov_args   = List.flatten p;
+       prov_body   = f;
+     } in
+
+      (x, PTHO_Pred (`BySyntax ov, unloc mode)) }
+
+| AXIOM x=qoident mode=loc(opclmode) y=qoident
+  { x, PTHO_Axiom (y, unloc mode) }
+
+| LEMMA x=qoident mode=loc(opclmode) y=qoident
+  { x, PTHO_Axiom (y, unloc mode) }
+
+| MODULE uqident loc(opclmode) uqident
+   { parse_error
+       (EcLocation.make $startpos $endpos)
+       (Some "Module overriding is no longer supported.")
+   }
+
+| MODULE TYPE x=uqident mode=loc(opclmode) y=uqident
+   { (x, PTHO_ModTyp (y, unloc mode)) }
+
+| THEORY x=uqident mode=loc(opclmode) y=uqident
+   { (x, PTHO_Theory (y, unloc mode)) }
+
+(* -------------------------------------------------------------------- *)
+%public realize:
+| REALIZE x=qident
+    {  { pr_name = x; pr_proof = None; } }
+
+| REALIZE x=qident BY t=tactics
+    {  { pr_name = x; pr_proof = Some (Some t); } }
+
+| REALIZE x=qident BY bracket(empty)
+    {  { pr_name = x; pr_proof = Some None; } }
+
+(* -------------------------------------------------------------------- *)
+%public theory_clone:
+| local=is_local CLONE options=clone_opts?
+    ip=clone_import? x=uqident y=prefix(AS, uident)? cw=clone_with?
+    c=or3(clone_proof, clone_rename, clone_clear)*
+
+   { let (cp, cr, cl) =
+       List.fold_left (fun (cp, cr, cl) -> function
+        | `Or13 x -> (cp@x, cr, cl)
+        | `Or23 y -> (cp, cr@y, cl)
+        | `Or33 z -> (cp, cr, cl@z))
+       ([], [], []) c in
+
+     { pthc_base   = x;
+       pthc_name   = y;
+       pthc_ext    = EcUtils.odfl [] cw;
+       pthc_prf    = cp;
+       pthc_rnm    = cr;
+       pthc_clears = cl;
+       pthc_opts   = odfl [] options;
+       pthc_local  = local;
+       pthc_import = ip; } }

src/parser/ecParserExpressions.mly

@@ -0,0 +1,136 @@
+%%
+
+(* -------------------------------------------------------------------- *)
+%public %inline sexpr: x=loc(sexpr_u) { x }
+%public %inline  expr: x=loc( expr_u) { x }
+
+sexpr_u:
+| e=sexpr PCENT p=uqident
+   { PEscope (p, e) }
+
+| e=sexpr p=loc(prefix(PCENT, _lident))
+   { if unloc p = "top" then
+       PEscope (pqsymb_of_symb p.pl_loc "<top>", e)
+     else
+       let p = lmap (fun x -> "%" ^ x) p in
+       PEapp (mk_loc (loc p) (PEident (pqsymb_of_psymb p, None)), [e]) }
+
+| LPAREN e=expr COLONTILD ty=loc(type_exp) RPAREN
+   { PEcast (e, ty) }
+
+| n=uint
+   { PEint n }
+
+| d=DECIMAL
+   { PEdecimal d }
+
+| x=qoident ti=tvars_app?
+   { PEident (x, ti) }
+
+| op=loc(numop) ti=tvars_app?
+    { peapp_symb op.pl_loc op.pl_desc ti [] }
+
+| se=sexpr DLBRACKET ti=tvars_app? e=loc(plist1(expr, COMMA)) RBRACKET
+   { let e = List.reduce1 (fun _ -> lmap (fun x -> PEtuple x) e) (unloc e) in
+     peget (EcLocation.make $startpos $endpos) ti se e }
+
+| se=sexpr DLBRACKET ti=tvars_app? e1=loc(plist1(expr, COMMA)) LARROW e2=expr RBRACKET
+   { let e1 = List.reduce1 (fun _ -> lmap (fun x -> PEtuple x) e1) (unloc e1) in
+     peset (EcLocation.make $startpos $endpos) ti se e1 e2 }
+
+| TICKPIPE ti=tvars_app? e=expr PIPE
+   { peapp_symb e.pl_loc EcCoreLib.s_abs ti [e] }
+
+| LBRACKET ti=tvars_app? es=loc(plist0(expr, SEMICOLON)) RBRACKET
+   { unloc (pelist es.pl_loc ti es.pl_desc) }
+
+| LBRACKET ti=tvars_app? e1=expr op=loc(DOTDOT) e2=expr RBRACKET
+   { let id =
+       PEident (mk_loc op.pl_loc EcCoreLib.s_dinter, ti)
+     in
+       PEapp(mk_loc op.pl_loc id, [e1; e2]) }
+
+| LPAREN es=plist0(expr, COMMA) RPAREN
+   { PEtuple es }
+
+| r=loc(RBOOL)
+   { PEident (mk_loc r.pl_loc EcCoreLib.s_dbool, None) }
+
+| LPBRACE fields=rlist1(expr_field, SEMICOLON) SEMICOLON? RPBRACE
+   { PErecord (None, fields) }
+
+| LPBRACE b=sexpr WITH fields=rlist1(expr_field, SEMICOLON) SEMICOLON? RPBRACE
+   { PErecord (Some b, fields) }
+
+| e=sexpr DOTTICK x=qident
+   { PEproj (e, x) }
+
+| e=sexpr DOTTICK n=loc(word)
+   { if n.pl_desc = 0 then
+       parse_error n.pl_loc (Some "tuple projection start at 1");
+     PEproji(e,n.pl_desc - 1) }
+
+expr_u:
+| e=sexpr_u { e }
+
+| e=sexpr args=sexpr+
+    { PEapp (e, args) }
+
+| op=loc(uniop) ti=tvars_app? e=expr
+    { peapp_symb op.pl_loc op.pl_desc ti [e] }
+
+| e=expr_chained_orderings %prec prec_below_order
+    { fst e }
+
+| e1=expr op=loc(binop) ti=tvars_app? e2=expr
+    { peapp_symb op.pl_loc op.pl_desc ti [e1; e2] }
+
+| c=expr QUESTION e1=expr COLON e2=expr %prec LOP2
+   { PEif (c, e1, e2) }
+
+| IF c=expr THEN e1=expr ELSE e2=expr
+   { PEif (c, e1, e2) }
+
+| MATCH e=expr WITH
+    PIPE? bs=plist0(p=mcptn(sbinop) IMPL be=expr { (p, be) }, PIPE)
+  END
+    { PEmatch (e, bs) }
+
+| LET p=lpattern EQ e1=expr IN e2=expr
+   { PElet (p, (e1, None), e2) }
+
+| LET p=lpattern COLON ty=loc(type_exp) EQ e1=expr IN e2=expr
+   { PElet (p, (e1, Some ty), e2) }
+
+| r=loc(RBOOL) TILD e=sexpr
+    { let id  = PEident(mk_loc r.pl_loc EcCoreLib.s_dbitstring, None) in
+      let loc = EcLocation.make $startpos $endpos in
+        PEapp (mk_loc loc id, [e]) }
+
+| FUN pd=ptybindings IMPL  e=expr
+| FUN pd=ptybindings COMMA e=expr { PElambda (pd, e) }
+
+| FORALL pd=ptybindings COMMA e=expr { PEforall (pd, e) }
+| EXIST  pd=ptybindings COMMA e=expr { PEexists (pd, e) }
+
+expr_field:
+| x=qident EQ e=expr
+    { { rf_name = x ; rf_tvi = None; rf_value = e; } }
+
+expr_ordering:
+| e1=expr op=loc(ordering_op) ti=tvars_app? e2=expr
+    { (op, ti, e1, e2) }
+
+expr_chained_orderings:
+| e=expr_ordering
+    { let (op, ti, e1, e2) = e in
+        (peapp_symb op.pl_loc (unloc op) ti [e1; e2], e2) }
+
+| e1=loc(expr_chained_orderings) op=loc(ordering_op) ti=tvars_app? e2=expr
+    { let (lce1, (e1, le)) = (e1.pl_loc, unloc e1) in
+      let loc = EcLocation.make $startpos $endpos in
+        (peapp_symb loc "&&" None
+           [EcLocation.mk_loc lce1 e1;
+            EcLocation.mk_loc loc
+              (peapp_symb op.pl_loc (unloc op) ti [le; e2])],
+         e2) }

src/parser/ecParserFormulas.mly

@@ -0,0 +1,220 @@
+%%
+
+%public %inline sform_r(P): x=loc(sform_u(P)) { x }
+%public %inline  form_r(P): x=loc( form_u(P)) { x }
+
+%public %inline sform: x=sform_r(none) { x }
+%public %inline  form: x=form_r (none) { x }
+
+%public %inline sform_h: x=loc(sform_u(hole)) { x }
+%public %inline  form_h: x=loc( form_u(hole)) { x }
+
+%public %inline none: IMPOSSIBLE { assert false }
+%public %inline hole: UNDERSCORE { PFhole }
+
+sform_u(P):
+| x=P
+   { x }
+
+| f=sform_r(P) PCENT p=uqident
+   { PFscope (p, f) }
+
+| f=sform_r(P) p=loc(prefix(PCENT, _lident))
+
+   { if unloc p = "top" then
+       PFscope (pqsymb_of_symb p.pl_loc "<top>", f)
+     else
+       let p = lmap (fun x -> "%" ^ x) p in
+       PFapp (mk_loc (loc p) (PFident (pqsymb_of_psymb p, None)), [f]) }
+
+| SHARP pf=pffilter* x=ident
+   { PFref (x, pf) }
+
+| LPAREN f=form_r(P) COLONTILD ty=loc(type_exp) RPAREN
+   { PFcast (f, ty) }
+
+| n=uint
+   { PFint n }
+
+| d=DECIMAL
+   { PFdecimal d }
+
+| x=loc(RES)
+   { PFident (mk_loc x.pl_loc ([], "res"), None) }
+
+| x=qoident ti=tvars_app?
+   { PFident (x, ti) }
+
+| x=mident
+   { PFmem x }
+
+| se=sform_r(P) DLBRACKET ti=tvars_app? e=loc(plist1(form_r(P), COMMA)) RBRACKET
+   { let e = List.reduce1 (fun _ -> lmap (fun x -> PFtuple x) e) (unloc e) in
+     pfget (EcLocation.make $startpos $endpos) ti se e }
+
+| se=sform_r(P) DLBRACKET
+    ti=tvars_app? e1=loc(plist1(form_r(P), COMMA))LARROW e2=form_r(P)
+  RBRACKET
+   { let e1 = List.reduce1 (fun _ -> lmap (fun x -> PFtuple x) e1) (unloc e1) in
+     pfset (EcLocation.make $startpos $endpos) ti se e1 e2 }
+
+| x=sform_r(P) s=loc(pside)
+   { PFside (x, s) }
+
+| op=loc(numop) ti=tvars_app?
+    { pfapp_symb op.pl_loc op.pl_desc ti [] }
+
+| TICKPIPE ti=tvars_app? e =form_r(P) PIPE
+   { pfapp_symb e.pl_loc EcCoreLib.s_abs ti [e] }
+
+| LPAREN fs=plist0(form_r(P), COMMA) RPAREN
+   { PFtuple fs }
+
+| LPBRACE fields=rlist1(form_field, SEMICOLON) SEMICOLON? RPBRACE
+   { PFrecord (None, fields) }
+
+| LPBRACE b=sform WITH fields=rlist1(form_field, SEMICOLON) SEMICOLON? RPBRACE
+   { PFrecord (Some b, fields) }
+
+| LBRACKET ti=tvars_app? es=loc(plist0(form_r(P), SEMICOLON)) RBRACKET
+   { (pflist es.pl_loc ti es.pl_desc).pl_desc }
+
+| f=sform_r(P) DOTTICK x=qident
+    { PFproj (f, x) }
+
+| f=sform_r(P) DOTTICK n=loc(word)
+   { if n.pl_desc = 0 then
+       parse_error n.pl_loc (Some "tuple projection start at 1");
+     PFproji(f,n.pl_desc - 1) }
+
+| HOARE LBRACKET hb=hoare_body(P) RBRACKET { hb }
+
+| EHOARE LBRACKET hb=ehoare_body(P) RBRACKET { hb }
+
+| EQUIV LBRACKET eb=equiv_body(P) RBRACKET { eb }
+
+| EAGER LBRACKET eb=eager_body(P) RBRACKET { eb }
+
+| PR LBRACKET
+    mp=loc(fident) args=paren(plist0(form_r(P), COMMA)) AT pn=mident
+    COLON event=form_r(P)
+  RBRACKET
+    { PFprob (mp, args, pn, event) }
+
+| r=loc(RBOOL)
+    { PFident (mk_loc r.pl_loc EcCoreLib.s_dbool, None) }
+
+| LBRACKET ti=tvars_app? e1=form_r(P) op=loc(DOTDOT) e2=form_r(P) RBRACKET
+    { let id = PFident(mk_loc op.pl_loc EcCoreLib.s_dinter, ti) in
+      PFapp(mk_loc op.pl_loc id, [e1; e2]) }
+
+form_u(P):
+| GLOB mp=loc(mod_qident) { PFglob mp }
+
+| e=sform_u(P) { e }
+
+| e=sform_r(P) args=sform_r(P)+ { PFapp (e, args) }
+
+| op=loc(uniop) ti=tvars_app? e=form_r(P)
+   { pfapp_symb op.pl_loc op.pl_desc ti [e] }
+
+| f=form_chained_orderings(P) %prec prec_below_order
+    { fst f }
+
+| e1=form_r(P) op=loc(binop) ti=tvars_app? e2=form_r(P)
+    { pfapp_symb op.pl_loc op.pl_desc ti [e1; e2] }
+
+| c=form_r(P) QUESTION e1=form_r(P) COLON e2=form_r(P) %prec LOP2
+    { PFif (c, e1, e2) }
+
+| MATCH f=form_r(P) WITH
+    PIPE? bs=plist0(p=mcptn(sbinop) IMPL bf=form_r(P) { (p, bf) }, PIPE)
+  END
+    { PFmatch (f, bs) }
+
+| EQ LBRACE xs=plist1(qident_or_res_or_glob, COMMA) RBRACE
+    { PFeqveq (xs, None) }
+
+| EQ LBRACE xs=plist1(qident_or_res_or_glob, COMMA) RBRACE
+    LPAREN  m1=mod_qident COMMA m2=mod_qident RPAREN
+    { PFeqveq (xs, Some (m1, m2)) }
+
+| EQ LPBRACE xs=plist1(form_r(P), COMMA) RPBRACE
+    { PFeqf xs }
+
+| IF c=form_r(P) THEN e1=form_r(P) ELSE e2=form_r(P)
+    { PFif (c, e1, e2) }
+
+| LET p=lpattern EQ e1=form_r(P) IN e2=form_r(P)
+    { PFlet (p, (e1, None), e2) }
+
+| LET p=lpattern COLON ty=loc(type_exp) EQ e1=form_r(P) IN e2=form_r(P)
+    { PFlet (p, (e1, Some ty), e2) }
+
+| FORALL pd=pgtybindings COMMA e=form_r(P) { PFforall (pd, e) }
+| EXIST  pd=pgtybindings COMMA e=form_r(P) { PFexists (pd, e) }
+| FUN    pd=ptybindings  COMMA e=form_r(P) { PFlambda (pd, e) }
+| FUN    pd=ptybindings  IMPL  e=form_r(P) { PFlambda (pd, e) }
+
+| r=loc(RBOOL) TILD e=sform_r(P)
+    { let id  = PFident (mk_loc r.pl_loc EcCoreLib.s_dbitstring, None) in
+      let loc = EcLocation.make $startpos $endpos in
+        PFapp (mk_loc loc id, [e]) }
+
+| PHOARE pb=phoare_body(P) { pb }
+
+| LOSSLESS mp=loc(fident)
+    { PFlsless mp }
+
+form_field:
+| x=qident EQ f=form
+    { { rf_name = x; rf_tvi = None; rf_value = f; } }
+
+form_ordering(P):
+| f1=form_r(P) op=loc(ordering_op) ti=tvars_app? f2=form_r(P)
+    { (op, ti, f1, f2) }
+
+form_chained_orderings(P):
+| f=form_ordering(P)
+    { let (op, ti, f1, f2) = f in
+        (pfapp_symb op.pl_loc (unloc op) ti [f1; f2], f2) }
+
+| f1=loc(form_chained_orderings(P)) op=loc(ordering_op) ti=tvars_app? f2=form_r(P)
+    { let (lcf1, (f1, le)) = (f1.pl_loc, unloc f1) in
+      let loc = EcLocation.make $startpos $endpos in
+        (pfapp_symb loc "&&" None
+           [EcLocation.mk_loc lcf1 f1;
+            EcLocation.mk_loc loc
+              (pfapp_symb op.pl_loc (unloc op) ti [le; f2])],
+         f2) }
+
+%public hoare_bd_cmp :
+| LE { EcAst.FHle }
+| EQ { EcAst.FHeq }
+| GE { EcAst.FHge }
+
+%public hoare_body(P):
+  mp=loc(fident) COLON pre=form_r(P) LONGARROW post=form_r(P)
+    { PFhoareF (pre, mp, post) }
+
+%public ehoare_body(P):
+  mp=loc(fident) COLON pre=form_r(P) LONGARROW
+                       post=form_r(P)
+    { PFehoareF (pre, mp, post) }
+
+%public phoare_body(P):
+  LBRACKET mp=loc(fident) COLON
+    pre=form_r(P) LONGARROW post=form_r(P)
+  RBRACKET
+    cmp=hoare_bd_cmp bd=sform_r(P)
+  { PFBDhoareF (pre, mp, post, cmp, bd) }
+
+%public equiv_body(P):
+  mp1=loc(fident) TILD mp2=loc(fident)
+  COLON pre=form_r(P) LONGARROW post=form_r(P)
+    { PFequivF (pre, (mp1, mp2), post) }
+
+%public eager_body(P):
+| s1=stmt COMMA  mp1=loc(fident) TILD mp2=loc(fident) COMMA s2=stmt
+    COLON pre=form_r(P) LONGARROW post=form_r(P)
+    { PFeagerF (pre, (s1, mp1, mp2,s2), post) }

src/parser/ecParserIdents.mly

@@ -0,0 +1,152 @@
+%%
+
+(* -------------------------------------------------------------------- *)
+%public _lident:
+| x=LIDENT   { x }
+| ABORT      { "abort"      }
+| ADMITTED   { "admitted"   }
+| ASYNC      { "async"      }
+| DEBUG      { "debug"      }
+| DUMP       { "dump"       }
+| EXPECT     { "expect"     }
+| FIRST      { "first"      }
+| GEN        { "gen"        }
+| INTERLEAVE { "interleave" }
+| LAST       { "last"       }
+| LEFT       { "left"       }
+| RIGHT      { "right"      }
+| SOLVE      { "solve"      }
+| WLOG       { "wlog"       }
+| EXLIM      { "exlim"      }
+| ECALL      { "ecall"      }
+| FROM       { "from"       }
+| EXIT       { "exit"       }
+
+| x=RING  { match x with `Eq -> "ringeq"  | `Raw -> "ring"  }
+| x=FIELD { match x with `Eq -> "fieldeq" | `Raw -> "field" }
+
+%public %inline _uident:
+| x=UIDENT { x }
+
+%public %inline _tident:
+| x=TIDENT { x }
+
+%public %inline _mident:
+| x=MIDENT { x }
+
+%public %inline lident: x=loc(_lident) { x }
+%public %inline uident: x=loc(_uident) { x }
+%public %inline tident: x=loc(_tident) { x }
+%public %inline mident: x=loc(_mident) { x }
+
+%public %inline _ident:
+| x=_lident { x }
+| x=_uident { x }
+
+%public %inline ident:
+| x=loc(_ident) { x }
+
+%public %inline uint: n=UINT { n }
+
+%public %inline word:
+| n=loc(UINT) {
+    try  BI.to_int (unloc n)
+    with BI.Overflow ->
+      parse_error (loc n) (Some "literal is too large")
+  }
+
+%public %inline sword:
+|       n=word {  n }
+| MINUS n=word { -n }
+
+(* -------------------------------------------------------------------- *)
+%inline namespace:
+| nm=rlist1(UIDENT, DOT)
+    { nm }
+
+| TOP nm=rlist0(prefix(DOT, UIDENT), empty)
+    { EcCoreLib.i_top :: nm }
+
+| SELF nm=rlist0(prefix(DOT, UIDENT), empty)
+    { EcCoreLib.i_self :: nm }
+
+_genqident(X):
+| x=X { ([], x) }
+| xs=namespace DOT x=X { (xs, x) }
+
+%public genqident(X):
+| x=loc(_genqident(X)) { x }
+
+
+(* -------------------------------------------------------------------- *)
+%public %inline  qident: x=genqident(_ident ) { x }
+%public %inline uqident: x=genqident(_uident) { x }
+%public %inline lqident: x=genqident(_lident) { x }
+
+(* -------------------------------------------------------------------- *)
+%inline _boident:
+| x=_lident { x }
+| x=_uident { x }
+| x=PUNIOP  { x }
+| x=PBINOP  { x }
+| x=PNUMOP  { x }
+| x=PPSTOP  { x }
+
+| x=loc(STRING)   {
+    if not (EcCoreLib.is_mixfix_op (unloc x)) then
+      parse_error x.pl_loc (Some "invalid mixfix operator");
+    unloc x
+  }
+
+%inline _oident:
+| x=_boident      { x }
+| x=paren(PUNIOP) { x }
+
+%public %inline boident: x=loc(_boident) { x }
+%public %inline  oident: x=loc( _oident) { x }
+
+%public qoident:
+| x=boident
+    { pqsymb_of_psymb x }
+
+| xs=namespace DOT x=oident
+| xs=namespace DOT x=loc(NOP) {
+    { pl_desc = (xs, unloc x);
+      pl_loc  = EcLocation.make $startpos $endpos;
+    }
+  }
+
+(* -------------------------------------------------------------------- *)
+mod_ident1:
+| x=uident
+    { (x, None) }
+
+| x=uident LPAREN args=plist1(loc(mod_qident), COMMA) RPAREN
+    { (x, Some args) }
+
+
+%public %inline mod_qident:
+| x=rlist1(mod_ident1, DOT)
+    { x }
+
+| _l=TOP DOT x=rlist1(mod_ident1, DOT)
+    { (mk_loc (EcLocation.make $startpos(_l) $endpos(_l))
+         EcCoreLib.i_top, None) :: x }
+
+| _l=SELF DOT x=rlist1(mod_ident1, DOT)
+    { (mk_loc (EcLocation.make $startpos(_l) $endpos(_l))
+         EcCoreLib.i_self, None) :: x }
+
+%public %inline fident:
+| nm=mod_qident DOT x=lident { (nm, x) }
+| x=lident { ([], x) }
+
+%public f_or_mod_ident:
+| nm=mod_qident DOT x=lident
+    { let fv = mk_loc (EcLocation.make $startpos(nm) $endpos(x)) (nm, x) in
+      FM_FunOrVar fv }
+| x=lident
+    { let fv = mk_loc (EcLocation.make $startpos(x) $endpos(x)) ([], x) in
+      FM_FunOrVar fv}
+| m=loc(mod_qident) { FM_Mod m }
+

src/parser/ecParserTokens.mly

@@ -0,0 +1,290 @@
+%token <EcSymbols.symbol> LIDENT
+%token <EcSymbols.symbol> UIDENT
+%token <EcSymbols.symbol> TIDENT
+%token <EcSymbols.symbol> MIDENT
+%token <EcSymbols.symbol> PUNIOP
+%token <EcSymbols.symbol> PBINOP
+%token <EcSymbols.symbol> PNUMOP
+%token <EcSymbols.symbol> PPSTOP
+
+%token <EcBigInt.zint> UINT
+%token <EcBigInt.zint * (int * EcBigInt.zint)> DECIMAL
+%token <string> STRING
+
+(* Tokens *)
+%token ANDA AND (* asym : &&, sym : /\ *)
+%token ORA  OR  (* asym : ||, sym : \/ *)
+
+%token<[`Raw|`Eq]> RING
+%token<[`Raw|`Eq]> FIELD
+
+%token ABORT
+%token ABBREV
+%token ABSTRACT
+%token ADMIT
+%token ADMITTED
+%token ALGNORM
+%token ALIAS
+%token AMP
+%token APPLY
+%token AS
+%token ASSERT
+%token ASSUMPTION
+%token ASYNC
+%token AT
+%token AUTO
+%token AXIOM
+%token AXIOMATIZED
+%token BACKS
+%token BACKSLASH
+%token BETA
+%token BY
+%token BYEQUIV
+%token BYPHOARE
+%token BYEHOARE
+%token BYPR
+%token BYUPTO
+%token CALL
+%token CASE
+%token CBV
+%token CEQ
+%token CFOLD
+%token CHANGE
+%token CLASS
+%token CLEAR
+%token CLONE
+%token COLON
+%token COLONTILD
+%token COMMA
+%token CONGR
+%token CONSEQ
+%token CONST
+%token DEBUG
+%token DECLARE
+%token DELTA
+%token DLBRACKET
+%token DO
+%token DONE
+%token DOT
+%token DOTDOT
+%token DOTTICK
+%token DROP
+%token DUMP
+%token EAGER
+%token ECALL
+%token EHOARE
+%token ELIF
+%token ELIM
+%token ELSE
+%token END
+%token EOF
+%token EQ
+%token EQUIV
+%token ETA
+%token EXACT
+%token EXFALSO
+%token EXIST
+%token EXIT
+%token EXLIM
+%token EXPECT
+%token EXPORT
+%token FAIL
+%token FEL
+%token FIRST
+%token FISSION
+%token FOR
+%token FORALL
+%token FROM
+%token FUN
+%token FUSION
+%token FWDS
+%token GEN
+%token GLOB
+%token GOAL
+%token HAT
+%token HAVE
+%token HINT
+%token HOARE
+%token IDTAC
+%token IF
+%token IFF
+%token IMPL
+%token IMPORT
+%token IMPOSSIBLE
+%token IN
+%token INCLUDE
+%token INDUCTIVE
+%token INLINE
+%token INTERLEAVE
+%token INSTANCE
+%token IOTA
+%token IS
+%token KILL
+%token LARROW
+%token LAST
+%token LBRACE
+%token LBRACKET
+%token LEAT
+%token LEFT
+%token LEMMA
+%token LESAMPLE
+%token LET
+%token LLARROW
+%token LOCAL
+%token LOCATE
+%token LOGIC
+%token LONGARROW
+%token LOSSLESS
+%token LPAREN
+%token LPBRACE
+%token MATCH
+%token MINUS
+%token MODPATH
+%token MODULE
+%token MOVE
+%token NE
+%token NOSMT
+%token NOT
+%token NOTATION
+%token OF
+%token OP
+%token OUTLINE
+%token PCENT
+%token PHOARE
+%token PIPE
+%token PIPEGT
+%token PIPEPIPEGT
+%token PLUS
+%token POSE
+%token PR
+%token PRAGMA
+%token PRBOUNDED
+%token PRED
+%token PRINT
+%token PROC
+%token PROGRESS
+%token PROOF
+%token PROVER
+%token QED
+%token QUESTION
+%token RARROW
+%token RBOOL
+%token RBRACE
+%token RBRACKET
+%token RCONDF
+%token RCONDT
+%token REALIZE
+%token REFLEX
+%token REMOVE
+%token RENAME
+%token REPLACE
+%token REQUIRE
+%token RES
+%token RETURN
+%token REWRITE
+%token RIGHT
+%token RND
+%token RNDSEM
+%token RPAREN
+%token RPBRACE
+%token RRARROW
+%token RWNORMAL
+%token SEARCH
+%token SECTION
+%token SELF
+%token SEMICOLON
+%token SEQ
+%token SHARP
+%token SHARPPIPE
+%token SIM
+%token SIMPLIFY
+%token SKIP
+%token SLASH
+%token SLASHEQ
+%token SLASHGT
+%token SLASHSHARP
+%token SLASHSLASHGT
+%token SLASHTILDEQ
+%token SLASHSLASH
+%token SLASHSLASHEQ
+%token SLASHSLASHTILDEQ
+%token SLASHSLASHSHARP
+%token SMT
+%token SOLVE
+%token SP
+%token SPLIT
+%token SPLITWHILE
+%token STAR
+%token SUBST
+%token SUFF
+%token SWAP
+%token SYMMETRY
+%token THEN
+%token THEORY
+%token TICKBRACE
+%token TICKPIPE
+%token TILD
+%token TIME
+%token TIMEOUT
+%token TOP
+%token TRANSITIVITY
+%token TRIVIAL
+%token TRY
+%token TYPE
+%token UNDERSCORE
+%token UNDO
+%token UNROLL
+%token VAR
+%token WEAKMEM
+%token WHILE
+%token WHY3
+%token WITH
+%token WLOG
+%token WP
+%token ZETA
+%token <string> NOP LOP1 ROP1 LOP2 ROP2 LOP3 ROP3 LOP4 ROP4 NUMOP
+%token LTCOLON DASHLT GT LT GE LE LTSTARGT LTLTSTARGT LTSTARGTGT
+%token < Lexing.position> FINAL
+
+%nonassoc prec_below_comma
+%nonassoc COMMA ELSE
+
+%nonassoc IN
+%nonassoc prec_below_IMPL
+%right    IMPL LEAT
+%nonassoc IFF
+%right    ORA  OR
+%right    ANDA AND
+%nonassoc NOT
+
+%nonassoc EQ NE
+
+%nonassoc prec_below_order
+
+%left  NOP
+%left  GT LT GE LE
+%left  LOP1
+%right ROP1
+%right QUESTION
+%left  LOP2 MINUS PLUS
+%right ROP2
+%right RARROW
+%left  LOP3 STAR SLASH
+%right ROP3
+%left  LOP4 AT AMP HAT BACKSLASH
+%right ROP4
+
+%nonassoc LBRACE
+
+%right SEMICOLON
+
+%nonassoc prec_tactic
+
+%type <EcParsetree.global> global
+%type <EcParsetree.prog  > prog
+
+%type <unit> is_uniop
+%type <unit> is_binop
+%type <unit> is_numop
+
+%%