swh:1:snp:04e159a4411e97cbe416dcf21d082639f654120b
Tip revision: a79f9aeb6de046ca12210d26317fab59c175d0dd authored by Pierre-Yves Strub on 08 July 2014, 09:43:21 UTC
Fix bug w.r.t. _tools presence detection.
Fix bug w.r.t. _tools presence detection.
Tip revision: a79f9ae
ecParser.mly
(* Copyright (c) - 2012-2014 - IMDEA Software Institute and INRIA
* Distributed under the terms of the CeCILL-B license *)
%{
open EcUtils
open EcLocation
open EcParsetree
let parse_error loc msg = raise (ParseError (loc, msg))
let pqsymb_of_psymb (x : psymbol) : pqsymbol =
mk_loc x.pl_loc ([], x.pl_desc)
let pqsymb_of_symb loc x : pqsymbol =
mk_loc loc ([], x)
let mk_mod ?(modtypes = []) params body = Pm_struct {
ps_params = params;
ps_signature = modtypes;
ps_body = body;
}
let mk_tydecl (tyvars, name) body = {
pty_name = name;
pty_tyvars = tyvars;
pty_body = body;
}
let opdef_of_opbody ty b =
match b with
| None -> PO_abstr ty
| Some (args, `Expr e ) -> PO_concr (args, ty, e)
| Some (args, `Case bs) -> PO_case (args, ty, bs)
let lqident_of_fident (nm, name) =
let module E = struct exception Invalid end in
let nm =
let for1 (x, args) =
if args <> None then raise E.Invalid else unloc x
in
List.map for1 nm
in
try Some (nm, unloc name) with E.Invalid -> None
let mk_peid_symb loc s ti =
mk_loc loc (PEident (pqsymb_of_symb loc s, ti))
let mk_pfid_symb loc s ti =
mk_loc loc (PFident (pqsymb_of_symb loc s, ti))
let peapp_symb loc s ti es =
PEapp (mk_peid_symb loc s ti, es)
let peget loc ti e1 e2 =
peapp_symb loc EcCoreLib.s_get ti [e1;e2]
let peset loc ti e1 e2 e3 =
peapp_symb loc EcCoreLib.s_set ti [e1;e2;e3]
let pfapp_symb loc s ti es =
PFapp(mk_pfid_symb loc s ti, es)
let pfget loc ti e1 e2 =
pfapp_symb loc EcCoreLib.s_get ti [e1;e2]
let pfset loc ti e1 e2 e3 =
pfapp_symb loc EcCoreLib.s_set ti [e1;e2;e3]
let pe_nil loc ti =
mk_peid_symb loc EcCoreLib.s_nil ti
let pe_cons loc ti e1 e2 =
mk_loc loc (peapp_symb loc EcCoreLib.s_cons ti [e1; e2])
let pelist loc ti (es : pexpr list) : pexpr =
List.fold_right (fun e1 e2 -> pe_cons loc ti e1 e2) es (pe_nil loc ti)
let pf_nil loc ti =
mk_pfid_symb loc EcCoreLib.s_nil ti
let pf_cons loc ti e1 e2 =
mk_loc loc (pfapp_symb loc EcCoreLib.s_cons ti [e1; e2])
let pflist loc ti (es : pformula list) : pformula =
List.fold_right (fun e1 e2 -> pf_cons loc ti e1 e2) es (pf_nil loc ti)
let mk_axiom ?(local = false) ?(nosmt = false) (x, ty, vd, f) k =
{ pa_name = x;
pa_tyvars = ty;
pa_vars = vd;
pa_formula = f;
pa_kind = k;
pa_nosmt = nosmt;
pa_local = local; }
let str_and b = if b then "&&" else "/\\"
let str_or b = if b then "||" else "\\/"
let mk_simplify l =
if l = [] then
{ pbeta = true; pzeta = true;
piota = true; plogic = true;
pdelta = None; pmodpath = true }
else
let doarg acc = function
| `Delta l ->
if l = [] || acc.pdelta = None
then { acc with pdelta = None }
else { acc with pdelta = Some (oget acc.pdelta @ l) }
| `Zeta -> { acc with pzeta = true }
| `Iota -> { acc with piota = true }
| `Beta -> { acc with pbeta = true }
| `Logic -> { acc with plogic = true }
| `ModPath -> { acc with pmodpath = true}
in
List.fold_left doarg
{ pbeta = false; pzeta = false;
piota = false; plogic = false;
pdelta = Some []; pmodpath = false } l
let simplify_red = [`Zeta; `Iota; `Beta; `Logic; `ModPath]
let mk_fpattern kind args =
{ fp_kind = kind;
fp_args = args; }
let mk_core_tactic t = { pt_core = t; pt_intros = []; }
let mk_topmod ~local (name, body) =
{ ptm_name = name ;
ptm_body = body ;
ptm_local = local; }
%}
%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 <int> UINT
%token <string> STRING
(* Tokens *)
%token ANDA AND (* asym : &&, sym : /\ *)
%token ORA OR (* asym : ||, sym : \/ *)
%token <EcParsetree.codepos> CPOS
%token ADD
%token ADMIT
%token ALGNORM
%token ALIAS
%token APPLY
%token AS
%token ASSERT
%token ASSUMPTION
%token AT
%token AUTO
%token AXIOM
%token AXIOMATIZED
%token BACKS
%token BETA
%token BY
%token BYEQUIV
%token BYPHOARE
%token BYPR
%token CALL
%token CASE
%token CEQ
%token CFOLD
%token CHANGE
%token CLASS
%token CLEAR
%token CLONE
%token COLON
%token COMMA
%token CONGR
%token CONSEQ
%token CONST
%token CUT
%token DCOLON
%token DEBUG
%token DECLARE
%token DELTA
%token DLBRACKET
%token DO
%token DONE
%token DOT
%token DOTDOT
%token DOTTICK
%token DROP
%token EAGER
%token ELIM
%token ELSE
%token END
%token EOF
%token EQ
%token EQUIV
%token EXACT
%token EXFALSO
%token EXIST
%token EXPECT
%token EXPORT
%token EXTRACTION
%token FEL
%token FIELD
%token FINAL
%token FIRST
%token FISSION
%token FORALL
%token FROM_INT
%token FUN
%token FUSION
%token FWDS
%token GENERALIZE
%token GLOB
%token HINT
%token HOARE
%token HYPOTHESIS
%token IDTAC
%token IF
%token IFF
%token IMPL
%token IMPORT
%token IMPOSSIBLE
%token IN
%token INLINE
%token INSTANCE
%token INTROS
%token IOTA
%token KILL
%token LARROW
%token LAST
%token LBRACE
%token LBRACKET
%token LEFT
%token LEMMA
%token LET
%token LLARROW
%token LOCAL
%token LOGIC
%token LONGARROW
%token LOSSLESS
%token LPAREN
%token LPBRACE
%token MINUS
%token MODPATH
%token MODULE
%token MOVE
%token NE
%token NOLOCALS
%token NOSMT
%token NOT
%token OF
%token OP
%token PCENT
%token PHOARE
%token PIPE
%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 REQUIRE
%token RES
%token RETURN
%token REWRITE
%token RIGHT
%token RING
%token RND
%token RPAREN
%token RPBRACE
%token RRARROW
%token RWNORMAL
%token SAMPLE
%token SECTION
%token SEMICOLON
%token SEQ
%token SIM
%token SIMPLIFY
%token SKIP
%token SLASH
%token SLASHEQ
%token SLASHSLASH
%token SLASHSLASHEQ
%token SMT
%token SP
%token SPLIT
%token SPLITWHILE
%token STAR
%token STRICT
%token SUBST
%token SWAP
%token SYMMETRY
%token THEN
%token THEORY
%token TICKPIPE
%token TILD
%token TIMEOUT
%token TOP
%token TRANSITIVITY
%token TRIVIAL
%token TRY
%token TYPE
%token UNDERSCORE
%token UNDO
%token UNROLL
%token VAR
%token WHILE
%token WHY3
%token WITH
%token WP
%token ZETA
%token <string> OP1 OP2 OP3 OP4
%token LTCOLON GT LT GE LE
%nonassoc prec_below_comma
%nonassoc COMMA ELSE
%nonassoc IN
%nonassoc prec_below_IMPL
%right IMPL
%nonassoc IFF
%right ORA OR
%right ANDA AND
%nonassoc NOT
%nonassoc EQ NE
%nonassoc prec_below_order
%left GT LT GE LE
%left OP1
%right QUESTION
%left OP2 MINUS ADD
%right RARROW
%left OP3 STAR SLASH
%left OP4 AT
%right DCOLON
%nonassoc LBRACE
%right SEMICOLON
%nonassoc prec_tactic
%type <EcParsetree.global EcLocation.located> global
%type <EcParsetree.prog EcLocation.located> prog
%start prog global
%%
(* -------------------------------------------------------------------- *)
%inline lident: x=loc(LIDENT) { x };
%inline uident: x=loc(UIDENT) { x };
%inline tident: x=loc(TIDENT) { x };
%inline mident: x=loc(MIDENT) { x };
%inline _ident:
| x=LIDENT { x }
| x=UIDENT { x }
;
%inline ident:
| x=loc(_ident) { x }
;
%inline uint: n=UINT { n };
(* -------------------------------------------------------------------- *)
%inline namespace:
| nm=rlist1(UIDENT, DOT)
{ nm }
| TOP
{ [EcCoreLib.id_top] }
| TOP DOT nm=rlist1(UIDENT, DOT)
{ EcCoreLib.id_top :: nm }
;
_genqident(X):
| x=X { ([], x) }
| xs=namespace DOT x=X { (xs, x) }
;
genqident(X):
| x=loc(_genqident(X)) { x }
;
(* -------------------------------------------------------------------- *)
%inline qident: x=genqident(_ident) { x };
%inline uqident: x=genqident(UIDENT) { x };
%inline lqident: x=genqident(LIDENT) { x };
(* -------------------------------------------------------------------- *)
%inline _oident:
| x=LIDENT { x }
| x=UIDENT { x }
| x=PUNIOP { x }
| x=paren(PUNIOP) { x }
| x=PBINOP { x }
| paren(DCOLON) { EcCoreLib.s_cons }
| 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=loc(_oident) { x }
;
qoident:
| x=oident
{ pqsymb_of_psymb x }
| xs=namespace DOT x=oident {
{ 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) }
;
%inline mod_qident:
| x=rlist1(mod_ident1, DOT) { x }
;
fident:
| nm=mod_qident DOT x=lident { (nm, x) }
| x=lident { ([], x) }
;
(* -------------------------------------------------------------------- *)
%inline ordering_op:
| GT { ">" }
| LT { "<" }
| GE { ">=" }
| LE { "<=" }
;
%inline uniop:
| x=OP1 { Printf.sprintf "[%s]" x }
| ADD { "[+]" }
| MINUS { "[-]" }
(* -------------------------------------------------------------------- *)
%inline or_:
| ORA { true }
| OR { false }
%inline and_:
| ANDA { true }
| AND { false }
(* -------------------------------------------------------------------- *)
pside_:
| x=LIDENT { (0, Printf.sprintf "&%s" x) }
| x=UINT { (0, Printf.sprintf "&%d" x) }
| ADD x=pside_ { (1 + fst x, snd x) }
;
pside:
| x=brace(pside_) { x }
;
(* -------------------------------------------------------------------- *)
(* Patterns *)
lpattern_u:
| x=ident
{ LPSymbol x }
| LPAREN p=plist2(ident, COMMA) RPAREN
{ LPTuple p }
| LPBRACE fs=rlist1(lp_field, SEMICOLON) SEMICOLON? RPBRACE
{ LPRecord fs }
;
lp_field:
| f=qident EQ x=ident { (f, x) }
;
%inline lpattern:
| x=loc(lpattern_u) { x }
;
(* -------------------------------------------------------------------- *)
(* Expressions: program expression, real expression *)
tyvar_byname1:
| x=tident EQ ty=loc(type_exp) { (x, ty) }
;
tyvar_annot:
| lt = plist1(loc(type_exp), COMMA) { TVIunamed lt }
| lt = plist1(tyvar_byname1, COMMA) { TVInamed lt }
;
%inline tvars_app:
| LTCOLON k=loc(tyvar_annot) GT { k }
;
(* -------------------------------------------------------------------- *)
%inline sexpr: x=loc(sexpr_u) { x };
%inline expr: x=loc( expr_u) { x };
sexpr_u:
| e=sexpr PCENT p=uqident
{ PEscope (p, e) }
| e=sexpr PCENT p=lident
{ if unloc p <> "top" then
parse_error p.pl_loc (Some "invalid scope name");
PEscope (pqsymb_of_symb p.pl_loc "<top>", e) }
| n=uint
{ PEint n }
| x=qoident ti=tvars_app?
{ PEident (x, ti) }
| se=sexpr op=loc(FROM_INT)
{ let id =
PEident (mk_loc op.pl_loc EcCoreLib.s_real_of_int, None)
in
PEapp (mk_loc op.pl_loc id, [se]) }
| se=sexpr DLBRACKET ti=tvars_app? e=expr RBRACKET
{ peget (EcLocation.make $startpos $endpos) ti se e }
| se=sexpr DLBRACKET ti=tvars_app? e1=expr LARROW e2=expr RBRACKET
{ 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 fields }
| e=sexpr DOTTICK x=qident
{ PEproj (e, x) }
| e=sexpr DOTTICK n=loc(uint)
{ 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(NOT) ti=tvars_app? e=expr
{ peapp_symb op.pl_loc "[!]" ti [e] }
| 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(OP1) ti=tvars_app? e2=expr
{ peapp_symb op.pl_loc op.pl_desc ti [e1; e2] }
| e1=expr op=loc(EQ) ti=tvars_app? e2=expr
{ peapp_symb op.pl_loc "=" ti [e1; e2] }
| e1=expr op=loc(NE) ti=tvars_app? e2=expr
{ peapp_symb op.pl_loc "[!]" None
[ mk_loc op.pl_loc (peapp_symb op.pl_loc "=" ti [e1; e2])] }
| e1=expr op=loc(ADD) ti=tvars_app? e2=expr
{ peapp_symb op.pl_loc "+" ti [e1; e2] }
| e1=expr op=loc(MINUS) ti=tvars_app? e2=expr
{ peapp_symb op.pl_loc "-" ti [e1; e2] }
| e1=expr op=loc(OP2) ti=tvars_app? e2=expr
{ peapp_symb op.pl_loc op.pl_desc ti [e1; e2] }
| e1=expr op=loc(OP3) ti=tvars_app? e2=expr
{ peapp_symb op.pl_loc op.pl_desc ti [e1; e2] }
| e1=expr op=loc(OP4) ti=tvars_app? e2=expr
{ peapp_symb op.pl_loc op.pl_desc ti [e1; e2] }
| e1=expr op=loc(DCOLON) ti=tvars_app? e2=expr
{ peapp_symb op.pl_loc EcCoreLib.s_cons ti [e1; e2] }
| e1=expr op=loc(IMPL) ti=tvars_app? e2=expr
{ peapp_symb op.pl_loc "=>" ti [e1; e2] }
| e1=expr op=loc(IFF) ti=tvars_app? e2=expr
{ peapp_symb op.pl_loc "<=>" ti [e1; e2] }
| e1=expr op=loc(or_) ti=tvars_app? e2=expr
{ peapp_symb op.pl_loc (str_or op.pl_desc) ti [e1; e2] }
| e1=expr op=loc(and_) ti=tvars_app? e2=expr
{ peapp_symb op.pl_loc (str_and op.pl_desc) ti [e1; e2] }
| e1=expr op=loc(STAR) ti=tvars_app? e2=expr
{ peapp_symb op.pl_loc "*" ti [e1; e2] }
| e1=expr op=loc(SLASH) ti=tvars_app? e2=expr
{ peapp_symb op.pl_loc "/" ti [e1; e2] }
| e1=expr op=loc(AT) ti=tvars_app? e2=expr
{ peapp_symb op.pl_loc "@" ti [e1; e2] }
| c=expr QUESTION e1=expr COLON e2=expr %prec OP2
{ PEif (c, e1, e2) }
| IF c=expr THEN e1=expr ELSE e2=expr
{ PEif (c, e1, e2) }
| 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 COMMA e=expr { PElambda (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 (str_and true) None
[EcLocation.mk_loc lce1 e1;
EcLocation.mk_loc loc
(peapp_symb op.pl_loc (unloc op) ti [le; e2])],
e2) }
;
%inline pty_varty:
| x=ident+
{ let loc = EcLocation.make $startpos $endpos in
(x, mk_loc loc PTunivar) }
| x=ident+ COLON ty=loc(type_exp)
{ (x, ty) }
;
ptybinding1:
| LPAREN bds=plist1(pty_varty, COMMA) RPAREN { bds }
| x=ident { [[x], mk_loc x.pl_loc PTunivar] }
;
ptybindings:
| x=ptybinding1+ { List.flatten x }
;
(* -------------------------------------------------------------------- *)
(* Formulas *)
%inline sform_r(P): x=loc(sform_u(P)) { x }
%inline form_r(P): x=loc( form_u(P)) { x }
%inline sform: x=sform_r(none) { x }
%inline form: x=form_r (none) { x }
%inline sform_h: x=loc(sform_u(hole)) { x }
%inline form_h: x=loc( form_u(hole)) { x }
%inline hole: UNDERSCORE { PFhole; }
%inline none: IMPOSSIBLE { assert false; }
qident_or_res_or_glob:
| x=qident { GVvar x }
| x=loc(RES) { GVvar (mk_loc x.pl_loc ([], "res")) }
| GLOB mp=loc(mod_qident) { GVglob mp }
sform_u(P):
| x=P
{ x }
| f=sform_r(P) PCENT p=qident
{ PFscope (p, f) }
| n=uint
{ PFint n }
| x=loc(RES)
{ PFident (mk_loc x.pl_loc ([], "res"), None) }
| x=qoident ti=tvars_app?
{ PFident (x, ti) }
| se=sform_r(P) op=loc(FROM_INT)
{ let id = PFident(mk_loc op.pl_loc EcCoreLib.s_real_of_int, None) in
PFapp (mk_loc op.pl_loc id, [se]) }
| se=sform_r(P) DLBRACKET ti=tvars_app? e=form_r(P) RBRACKET
{ pfget (EcLocation.make $startpos $endpos) ti se e }
| se=sform_r(P) DLBRACKET ti=tvars_app? e1=form_r(P) LARROW e2=form_r(P) RBRACKET
{ pfset (EcLocation.make $startpos $endpos) ti se e1 e2 }
| x=sform_r(P) s=loc(pside)
{ PFside (x, s) }
| 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 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(uint)
{ 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 }
| 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(NOT) ti=tvars_app? e=form_r(P)
{ pfapp_symb op.pl_loc "[!]" ti [e] }
| op=loc(uniop) ti=tvars_app? e=form_r(P)
{ pfapp_symb op.pl_loc op.pl_desc ti [e] }
| e1=form_r(P) op=loc(OP1) ti=tvars_app? e2=form_r(P)
{ pfapp_symb op.pl_loc op.pl_desc ti [e1; e2] }
| f=form_chained_orderings(P) %prec prec_below_order
{ fst f }
| e1=form_r(P) op=loc(EQ) ti=tvars_app? e2=form_r(P)
{ pfapp_symb op.pl_loc "=" ti [e1; e2] }
| e1=form_r(P) op=loc(NE) ti=tvars_app? e2=form_r(P)
{ pfapp_symb op.pl_loc "[!]" None
[ mk_loc op.pl_loc (pfapp_symb op.pl_loc "=" ti [e1; e2])] }
| e1=form_r(P) op=loc(MINUS) ti=tvars_app? e2=form_r(P)
{ pfapp_symb op.pl_loc "-" ti [e1; e2] }
| e1=form_r(P) op=loc(ADD) ti=tvars_app? e2=form_r(P)
{ pfapp_symb op.pl_loc "+" ti [e1; e2] }
| e1=form_r(P) op=loc(OP2) ti=tvars_app? e2=form_r(P)
{ pfapp_symb op.pl_loc op.pl_desc ti [e1; e2] }
| e1=form_r(P) op=loc(OP3) ti=tvars_app? e2=form_r(P)
{ pfapp_symb op.pl_loc op.pl_desc ti [e1; e2] }
| e1=form_r(P) op=loc(OP4) ti=tvars_app? e2=form_r(P)
{ pfapp_symb op.pl_loc op.pl_desc ti [e1; e2] }
| e1=form_r(P) op=loc(DCOLON) ti=tvars_app? e2=form_r(P)
{ pfapp_symb op.pl_loc EcCoreLib.s_cons ti [e1; e2] }
| e1=form_r(P) op=loc(IMPL) ti=tvars_app? e2=form_r(P)
{ pfapp_symb op.pl_loc "=>" ti [e1; e2] }
| e1=form_r(P) op=loc(IFF) ti=tvars_app? e2=form_r(P)
{ pfapp_symb op.pl_loc "<=>" ti [e1; e2] }
| e1=form_r(P) op=loc(or_) ti=tvars_app? e2=form_r(P)
{ pfapp_symb op.pl_loc (str_or op.pl_desc) ti [e1; e2] }
| e1=form_r(P) op=loc(and_) ti=tvars_app? e2=form_r(P)
{ pfapp_symb op.pl_loc (str_and op.pl_desc) ti [e1; e2] }
| e1=form_r(P) op=loc(STAR) ti=tvars_app? e2=form_r(P)
{ pfapp_symb op.pl_loc "*" ti [e1; e2] }
| e1=form_r(P) op=loc(SLASH) ti=tvars_app? e2=form_r(P)
{ pfapp_symb op.pl_loc "/" ti [e1; e2] }
| e1=form_r(P) op=loc(AT) ti=tvars_app? e2=form_r(P)
{ pfapp_symb op.pl_loc "@" ti [e1; e2] }
| c=form_r(P) QUESTION e1=form_r(P) COLON e2=form_r(P) %prec OP2
{ PFif (c, e1, e2) }
| EQ LBRACE xs=plist1(qident_or_res_or_glob, COMMA) RBRACE
{ PFeqveq 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) }
| 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 (str_and true) None
[EcLocation.mk_loc lcf1 f1;
EcLocation.mk_loc loc
(pfapp_symb op.pl_loc (unloc op) ti [le; f2])],
f2) }
;
hoare_bd_cmp :
| LE { EcFol.FHle }
| EQ { EcFol.FHeq }
| GE { EcFol.FHge }
hoare_body(P):
mp=loc(fident) COLON pre=form_r(P) LONGARROW post=form_r(P)
{ PFhoareF (pre, mp, post) }
;
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) }
;
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) }
;
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) }
;
pgtybinding1:
| x=ptybinding1 { List.map (fun (xs,ty) -> xs, PGTY_Type ty) x }
| LPAREN x=uident LTCOLON mi=mod_type_restr RPAREN
{ [[x], PGTY_ModTy mi] }
| pn=mident
{ [[pn], PGTY_Mem] }
;
pgtybindings:
| x=pgtybinding1+ { List.flatten x }
;
(* -------------------------------------------------------------------- *)
(* Type expressions *)
simpl_type_exp:
| UNDERSCORE { PTunivar }
| x=qident { PTnamed x }
| x=tident { PTvar x }
| tya=type_args x=qident { PTapp (x, tya) }
| GLOB m=loc(mod_qident) { PTglob m }
| LPAREN ty=type_exp RPAREN { ty }
;
type_args:
| ty=loc(simpl_type_exp) { [ty] }
| LPAREN tys=plist2(loc(type_exp), COMMA) RPAREN { tys }
;
type_exp:
| ty=simpl_type_exp { ty }
| ty=plist2(loc(simpl_type_exp), STAR) { PTtuple ty }
| ty1=loc(type_exp) RARROW ty2=loc(type_exp) { PTfun(ty1,ty2) }
;
(* -------------------------------------------------------------------- *)
(* Parameter declarations *)
typed_vars:
| xs=ident+ COLON ty=loc(type_exp)
{ List.map (fun v -> (v, ty)) xs }
| xs=ident+
{ List.map (fun v -> (v, mk_loc v.pl_loc PTunivar)) xs }
;
param_decl:
| LPAREN aout=plist0(typed_vars, COMMA) RPAREN
{ Fparams_exp (List.flatten aout )}
| LPAREN UNDERSCORE COLON ty=loc(type_exp) RPAREN
{ Fparams_imp ty }
;
(* -------------------------------------------------------------------- *)
(* Statements *)
lvalue_u:
| x=loc(fident)
{ match lqident_of_fident x.pl_desc with
| None -> parse_error x.pl_loc None
| Some v -> PLvSymbol (mk_loc x.pl_loc v) }
| LPAREN p=plist2(qident, COMMA) RPAREN
{ PLvTuple p }
| x=loc(fident) DLBRACKET ti=tvars_app? e=expr RBRACKET
{ match lqident_of_fident x.pl_desc with
| None -> parse_error x.pl_loc None
| Some v -> PLvMap (mk_loc x.pl_loc v, ti, e) }
;
%inline lvalue:
| x=loc(lvalue_u) { x }
;
base_instr:
| x=lvalue EQ SAMPLE e=expr
{ PSrnd (x, e) }
| x=lvalue EQ e=expr
{ PSasgn (x, e) }
| x=lvalue LARROW f=loc(fident) LPAREN es=loc(plist0(expr, COMMA)) RPAREN
{ PScall (Some x, f, es) }
| f=loc(fident) LPAREN es=loc(plist0(expr, COMMA)) RPAREN
{ PScall (None, f, es) }
| ASSERT LPAREN c=expr RPAREN
{ PSassert c }
;
instr:
| bi=base_instr SEMICOLON
{ bi }
| IF LPAREN c=expr RPAREN b1=block ELSE b2=block
{ PSif (c, b1, b2) }
| IF LPAREN c=expr RPAREN b=block
{ PSif (c, b , []) }
| WHILE LPAREN c=expr RPAREN b=block
{ PSwhile (c, b) }
;
block:
| i=loc(base_instr) SEMICOLON
{ [i] }
| stmt=brace(stmt)
{ stmt }
;
stmt: aout=loc(instr)* { aout }
(* -------------------------------------------------------------------- *)
(* Module definition *)
var_decl:
| VAR xs=plist1(lident, COMMA) COLON ty=loc(type_exp)
{ (xs, ty) }
;
loc_decl_names:
| x=plist1(lident, COMMA) { (`Single, x) }
| LPAREN x=plist2(lident, COMMA) RPAREN { (`Tuple, x) }
;
loc_decl_r:
| VAR x=loc(loc_decl_names)
{ { pfl_names = x; pfl_type = None; pfl_init = None; } }
| VAR x=loc(loc_decl_names) COLON ty=loc(type_exp)
{ { pfl_names = x; pfl_type = Some ty; pfl_init = None; } }
| VAR x=loc(loc_decl_names) COLON ty=loc(type_exp) EQ e=expr
{ { pfl_names = x; pfl_type = Some ty; pfl_init = Some e; } }
| VAR x=loc(loc_decl_names) EQ e=expr
{ { pfl_names = x; pfl_type = None; pfl_init = Some e; } }
;
loc_decl:
| x=loc_decl_r SEMICOLON { x }
;
ret_stmt:
| RETURN e=expr SEMICOLON
{ Some e }
| empty
{ None }
;
fun_def_body:
| LBRACE decl=loc_decl* s=stmt rs=ret_stmt RBRACE
{ { pfb_locals = decl;
pfb_body = s ;
pfb_return = rs ; }
}
;
fun_decl:
| x=lident pd=param_decl COLON ty=loc(type_exp)
{ { pfd_name = x ;
pfd_tyargs = pd ;
pfd_tyresult = ty ;
pfd_uses = (true, None); }
}
;
mod_item:
| v=var_decl
{ Pst_var v }
| m=mod_def
{ let (x, m) = m in Pst_mod (x, m) }
| PROC decl=loc(fun_decl) EQ body=fun_def_body {
let { pl_loc = loc; pl_desc = decl; } = decl in
match decl.pfd_tyargs with
| Fparams_imp _ ->
let msg = "implicite declaration of parameters not allowed" in
parse_error loc (Some msg)
| _ -> Pst_fun (decl, body)
}
| PROC x=lident EQ f=loc(fident)
{ Pst_alias (x, f) }
;
(* -------------------------------------------------------------------- *)
(* Modules *)
mod_body:
| m=mod_qident
{ `Alias m }
| LBRACE stt=loc(mod_item)* RBRACE
{ `Struct stt }
;
mod_def:
| MODULE x=uident p=mod_params? t=mod_aty? EQ body=loc(mod_body)
{ let p = EcUtils.odfl [] p in
match body.pl_desc with
| `Alias m ->
if t <> None then
parse_error (EcLocation.make $startpos $endpos)
(Some "cannot bind module type to module alias");
(x, mk_loc body.pl_loc (Pm_ident(p, m)))
| `Struct st ->
(x, mk_loc body.pl_loc (mk_mod ?modtypes:t p st)) }
;
top_mod_def:
| LOCAL x=mod_def { mk_topmod ~local:true x }
| /*-*/ x=mod_def { mk_topmod ~local:false x }
;
top_mod_decl:
| DECLARE MODULE x=uident COLON t=mod_type_restr
{ { ptmd_name = x; ptmd_modty = t; } }
;
mod_params:
| LPAREN a=plist1(sig_param, COMMA) RPAREN { a }
;
mod_aty:
| COLON t=plist1(loc(mod_aty1), COMMA) { t }
;
mod_aty1:
| x=qident { (x, []) }
| x=qident xs=paren(ident+) { (x, xs) }
;
(* -------------------------------------------------------------------- *)
(* Modules interfaces *)
%inline mod_type:
| x = qident { x }
;
%inline mod_type_restr:
| x = qident
{ (x, []) }
| x = qident LBRACE restr=plist1(loc(mod_qident), COMMA) RBRACE
{ (x, restr) }
;
sig_def:
| MODULE TYPE x=uident args=sig_params? EQ i=sig_body
{
let args = EcUtils.odfl [] args in
(x, Pmty_struct { pmsig_params = args;
pmsig_body = i; })
}
;
sig_body:
| body=sig_struct_body { body }
;
sig_struct_body:
| LBRACE ty=signature_item* RBRACE
{ ty }
;
sig_params:
| LPAREN params=plist1(sig_param, COMMA) RPAREN
{ params }
;
sig_param:
| x=uident COLON i=mod_type { (x, i) }
;
signature_item:
| PROC i=boption(STAR) x=lident pd=param_decl COLON ty=loc(type_exp) qs=brace(qident*)?
{ `FunctionDecl
{ pfd_name = x;
pfd_tyargs = pd;
pfd_tyresult = ty;
pfd_uses = (not i, qs); } }
;
(* -------------------------------------------------------------------- *)
(* EcTypes declarations / definitions *)
typaram:
| x=tident { (x, []) }
| x=tident LTCOLON tc=plist1(lqident, tcand) { (x, tc) }
;
typarams:
| empty { [] }
| x=tident { [(x, [])] }
| xs=paren(plist1(typaram, COMMA)) { xs }
;
%inline tyd_name:
| tya=typarams x=ident { (tya, x) }
;
tcand:
| x=loc(OP4) { if unloc x <> "&" then parse_error x.pl_loc None }
;
dt_ctor_def:
| x=oident { (x, []) }
| x=oident OF ty=plist1(loc(simpl_type_exp), tcand) { (x, ty) }
;
%inline datatype_def:
| LBRACKET PIPE? ctors=plist1(dt_ctor_def, PIPE) RBRACKET { ctors }
;
rec_field_def:
| x=ident COLON ty=loc(type_exp) { (x, ty); }
;
%inline record_def:
| LBRACE fields=rlist1(rec_field_def, SEMICOLON) SEMICOLON? RBRACE
{ fields }
;
typedecl:
| TYPE td=rlist1(tyd_name, COMMA)
{ List.map (mk_tydecl^~ (PTYD_Abstract [])) td }
| TYPE td=tyd_name LTCOLON tcs=rlist1(qident, COMMA)
{ [mk_tydecl td (PTYD_Abstract tcs)] }
| TYPE td=tyd_name EQ te=loc(type_exp)
{ [mk_tydecl td (PTYD_Alias te)] }
| TYPE td=tyd_name EQ te=record_def
{ [mk_tydecl td (PTYD_Record te)] }
| TYPE td=tyd_name EQ te=datatype_def
{ [mk_tydecl td (PTYD_Datatype te)] }
;
(* -------------------------------------------------------------------- *)
(* Type classes *)
typeclass:
| TYPE CLASS x=lident inth=tc_inth? EQ LBRACE body=tc_body RBRACE {
{ ptc_name = x;
ptc_inth = inth;
ptc_ops = fst body;
ptc_axs = snd body; }
}
;
tc_inth:
| LTCOLON x=lqident { x }
;
tc_body:
| ops=tc_op* axs=tc_ax* { (ops, axs) }
;
tc_op:
| OP x=oident COLON ty=loc(type_exp) { (x, ty) }
;
tc_ax:
| AXIOM x=ident COLON ax=form { (x, ax) }
;
(* -------------------------------------------------------------------- *)
(* Type classes (instances) *)
tycinstance:
| INSTANCE x=qident WITH typ=tyvars_decl? ty=loc(type_exp) ops=tyci_op* axs=tyci_ax* {
{ pti_name = x;
pti_type = (odfl [] typ, ty);
pti_ops = ops;
pti_axs = axs; }
}
;
tyci_op:
| OP x=oident EQ tg=qoident
{ (x, ([], tg)) }
| OP x=oident EQ tg=qoident LTCOLON tvi=plist0(loc(type_exp), COMMA) GT
{ (x, (tvi, tg)) }
;
tyci_ax:
| PROOF x=ident BY tg=tactic_core { (x, tg) }
;
(* -------------------------------------------------------------------- *)
(* Operator definitions *)
op_tydom:
| LPAREN RPAREN
{ [ ] }
| ty=loc(simpl_type_exp)
{ [ty] }
| tys=paren(plist2(loc(type_exp), COMMA))
{ tys }
;
tyvars_decl:
| LBRACKET tyvars=rlist0(typaram, COMMA) RBRACKET { tyvars }
| LBRACKET tyvars=rlist2(tident , empty) RBRACKET { List.map (fun x -> (x, [])) tyvars }
;
%inline op_or_const:
| OP x=nosmt { (`Op , x) }
| CONST x=nosmt { (`Const, x) }
;
operator:
| k=op_or_const x=oident tyvars=tyvars_decl? COLON sty=loc(type_exp) {
{ po_kind = fst k;
po_name = x;
po_tyvars = tyvars;
po_def = opdef_of_opbody sty None;
po_ax = None;
po_nosmt = snd k; }
}
| k=op_or_const x=oident tyvars=tyvars_decl? COLON sty=loc(type_exp) EQ b=opbody opax=opax? {
{ po_kind = fst k;
po_name = x;
po_tyvars = tyvars;
po_def = opdef_of_opbody sty (Some ([], b));
po_ax = opax;
po_nosmt = snd k; }
}
| k=op_or_const x=oident tyvars=tyvars_decl? eq=loc(EQ) b=opbody opax=opax? {
{ po_kind = fst k;
po_name = x;
po_tyvars = tyvars;
po_def = opdef_of_opbody (mk_loc eq.pl_loc PTunivar) (Some ([], b));
po_ax = opax;
po_nosmt = snd k; }
}
| k=op_or_const x=oident tyvars=tyvars_decl? p=ptybindings eq=loc(EQ) b=opbody opax=opax? {
{ po_kind = fst k;
po_name = x;
po_tyvars = tyvars;
po_def = opdef_of_opbody (mk_loc eq.pl_loc PTunivar) (Some (p, b));
po_ax = opax;
po_nosmt = snd k; }
}
| k=op_or_const x=oident tyvars=tyvars_decl? p=ptybindings COLON codom=loc(type_exp) EQ b=opbody opax=opax? {
{ po_kind = fst k;
po_name = x;
po_tyvars = tyvars;
po_def = opdef_of_opbody codom (Some (p, b));
po_ax = opax;
po_nosmt = snd k; }
}
;
opbody:
| e=expr { `Expr e }
| bs=opcase+ { `Case bs }
;
opax:
| AXIOMATIZED BY x=ident { x }
;
opcase:
| WITH ptn=plist1(opptn, COMMA) IMPL e=expr
{ { pop_patterns = ptn; pop_body = e; } }
;
opptn:
| x=ident EQ c=qoident tvi=tvars_app? ps=ident*
{ { pop_name = x; pop_tvi = tvi; pop_pattern = (c, ps); } }
;
predicate:
| PRED x = oident
{ { pp_name = x;
pp_tyvars = None;
pp_def = PPabstr []; } }
| PRED x = oident tyvars=tyvars_decl? COLON sty = op_tydom
{ { pp_name = x;
pp_tyvars = tyvars;
pp_def = PPabstr sty; } }
| PRED x = oident tyvars=tyvars_decl? p=ptybindings EQ f=form
{ { pp_name = x;
pp_tyvars = tyvars;
pp_def = PPconcr(p,f); } }
;
(* -------------------------------------------------------------------- *)
top_decl:
| x=top_mod_decl { PDCL_Module x }
;
(* -------------------------------------------------------------------- *)
(* Global entries *)
lemma_decl :
| x=ident tyvars=tyvars_decl? pd=pgtybindings? COLON f=form { x,tyvars,pd,f }
;
nosmt:
| NOSMT { true }
| empty { false }
;
%inline local:
| LOCAL { true }
| empty { false }
;
axiom_tc:
| /* empty */ { PILemma }
| BY bracket(empty) { PLemma None }
| BY t=tactic { PLemma (Some t) }
;
axiom:
| l=local AXIOM o=nosmt d=lemma_decl
{ mk_axiom ~local:l ~nosmt:o d (PAxiom `Axiom) }
| l=local HYPOTHESIS o=nosmt d=lemma_decl
{ mk_axiom ~local:l ~nosmt:o d (PAxiom `Hypothesis) }
| l=local LEMMA o=nosmt d=lemma_decl ao=axiom_tc
{ mk_axiom ~local:l ~nosmt:o d ao }
| l=local EQUIV x=ident pd=pgtybindings? COLON p=loc( equiv_body(none)) ao=axiom_tc
| l=local HOARE x=ident pd=pgtybindings? COLON p=loc( hoare_body(none)) ao=axiom_tc
| l=local PHOARE x=ident pd=pgtybindings? COLON p=loc(phoare_body(none)) ao=axiom_tc
{ mk_axiom ~local:l (x, None, pd, p) ao }
;
(* -------------------------------------------------------------------- *)
(* Theory interactive manipulation *)
theory_open : THEORY x=uident { x }
theory_close : END x=uident { x }
section_open : SECTION x=option(uident) { x }
section_close : END SECTION x=option(uident) { x }
import_flag:
| IMPORT { `Import }
| EXPORT { `Export }
;
theory_require :
| REQUIRE ip=import_flag? x=uident { (x, ip) }
;
theory_import: IMPORT x=uqident { x }
theory_export: EXPORT x=uqident { x }
theory_w3:
| IMPORT WHY3 path=string_list r=plist0(renaming,SEMICOLON)
{
let l = List.rev path in
let th = List.hd l in
let path = List.rev (List.tl l) in
path,th,r }
;
renaming:
| TYPE l=string_list AS s=STRING { l, RNty, s }
| OP l=string_list AS s=STRING { l, RNop, s }
| AXIOM l=string_list AS s=STRING { l, RNpr, s }
;
%inline string_list: l=plist1(STRING,empty) { l };
(* -------------------------------------------------------------------- *)
(* pattern selection (tactics) *)
idpattern:
| x=ident { [x] }
| LBRACKET xs=ident+ RBRACKET { xs }
;
ipattern:
| UNDERSCORE
{ PtAny }
| UNDERSCORE CEQ f=idpattern LPAREN UNDERSCORE RPAREN
{ PtAsgn f }
| IF UNDERSCORE LBRACE p=spattern RBRACE
{ PtIf (p, `NoElse) }
| IF UNDERSCORE LBRACE p=spattern RBRACE UNDERSCORE
{ PtIf (p, `MaybeElse) }
| IF UNDERSCORE LBRACE p1=spattern RBRACE ELSE LBRACE p2=spattern RBRACE
{ PtIf (p1, `Else p2) }
| WHILE UNDERSCORE LBRACE p=spattern RBRACE
{ PtWhile p }
;
spattern:
| UNDERSCORE { () }
;
tselect:
| p=ipattern { p }
;
(* -------------------------------------------------------------------- *)
(* tactic *)
intro_pattern_1_name:
| s=LIDENT { s }
| s=UIDENT { s }
| s=MIDENT { s }
;
intro_pattern_1:
| UNDERSCORE
{ `NoName }
| QUESTION
{ `FindName }
| s=intro_pattern_1_name
{`NoRename s}
| s=intro_pattern_1_name NOT
{`WithRename s}
;
intro_pattern:
| x=loc(intro_pattern_1)
{ IPCore x }
| LBRACKET RBRACKET
{ IPCase [] }
| LBRACKET ip=intro_pattern+ RBRACKET
{ IPCase [ip] }
| LBRACKET ip=plist2(intro_pattern*, PIPE) RBRACKET
{ IPCase ip }
| o=rwocc? RARROW
{ IPRw (o |> omap (snd_map EcMaps.Sint.of_list), `LtoR) }
| o=rwocc? LARROW
{ IPRw (o |> omap (snd_map EcMaps.Sint.of_list), `RtoL) }
| RRARROW
{ IPSubst `LtoR }
| LLARROW
{ IPSubst `RtoL }
| LBRACE xs=ident+ RBRACE
{ IPClear xs }
| SLASHSLASH
{ IPDone false }
| SLASHSLASHEQ
{ IPDone true }
| SLASHEQ
{ IPSimplify }
| SLASH f=fpattern(form)
{ IPView f }
;
fpattern_head(F):
| p=qident tvi=tvars_app?
{ FPNamed (p, tvi) }
| LPAREN UNDERSCORE COLON f=F RPAREN
{ FPCut f }
;
fpattern_arg:
| UNDERSCORE
{ EA_none }
| LPAREN LTCOLON m=loc(mod_qident) RPAREN
{ EA_mod m }
| f=sform
{ EA_form f }
| s=mident
{ EA_mem s }
;
fpattern(F):
| hd=fpattern_head(F)
{ mk_fpattern hd [] }
| LPAREN hd=fpattern_head(F) args=loc(fpattern_arg)* RPAREN
{ mk_fpattern hd args }
;
pterm:
| p=qident tvi=tvars_app? args=loc(fpattern_arg)*
{ { pt_name = p; pt_tys = tvi; pt_args = args; } }
;
%inline rwside:
| MINUS { `RtoL }
| empty { `LtoR }
;
%inline rwrgint:
| i=loc(int) {
if i.pl_desc = 0 then
parse_error i.pl_loc (Some "focus-index cannot be 0");
i.pl_desc
}
;
%inline rwrg:
| i=rwrgint { ((Some i, Some i), `Include) }
| TILD i=rwrgint { ((Some i, Some i), `Exclude) }
| rg=rgrw_cp { (rg, `Include) }
| TILD rg=paren(rgrw_cp) { (rg, `Exclude) }
;
%inline rgrw_cp:
| i1=rwrgint DOTDOT i2=rwrgint { (Some i1, Some i2) }
| i1=rwrgint DOTDOT { (Some i1, None ) }
| DOTDOT i2=rwrgint { (None , Some i2) }
;
rwrepeat:
| NOT { (`All , None ) }
| QUESTION { (`Maybe, None ) }
| n=uint NOT { (`All , Some n) }
| n=uint QUESTION { (`Maybe, Some n) }
;
rwocc:
| LBRACE x=uint+ RBRACE { (`Inclusive, x) }
| LBRACE MINUS x=uint+ RBRACE { (`Exclusive, x) }
;
rwarg1:
| SLASHSLASH
{ RWDone false }
| SLASHSLASHEQ
{ RWDone true }
| SLASHEQ
{ RWSimpl }
| s=rwside r=rwrepeat? o=rwocc? fp=rwfpatterns(form)
{ RWRw (s, r, o |> omap (snd_map EcMaps.Sint.of_list), fp) }
| s=rwside r=rwrepeat? o=rwocc? SLASH x=sform_h %prec prec_tactic
{ RWDelta (s, r, o |> omap (snd_map EcMaps.Sint.of_list), x); }
| PR s=bracket(ident)
{ RWPr s }
| SMT
{ RWSmt }
;
rwfpatterns(F):
| f=fpattern(F)
{ [(`LtoR, f)] }
| LPAREN fs=rlist2(rwfpattern(F), COMMA) RPAREN
{ fs }
;
rwfpattern(F):
| s=rwside f=fpattern(F)
{ (s, f) }
;
rwarg:
| r=rwarg1 { (None, r) }
| rg=loc(rwrg) COLON r=rwarg1 { (Some rg, r) }
;
genpattern:
| l=sform_h %prec prec_tactic
{ `Form (None, l) }
| o=rwocc l=sform_h %prec prec_tactic
{ `Form (Some (snd_map EcMaps.Sint.of_list o), l) }
| LPAREN UNDERSCORE COLON f=form RPAREN
{ `FPattern (mk_fpattern (FPCut f) []) }
| LPAREN LPAREN UNDERSCORE COLON f=form RPAREN args=loc(fpattern_arg)* RPAREN
{ `FPattern (mk_fpattern (FPCut f) args) }
;
simplify_arg:
| DELTA l=qoident* { `Delta l }
| ZETA { `Zeta }
| IOTA { `Iota }
| BETA { `Beta }
| LOGIC { `Logic }
| MODPATH { `ModPath }
;
simplify:
| l=simplify_arg+ { l }
| SIMPLIFY { simplify_red }
| SIMPLIFY l=qoident+ { `Delta l :: simplify_red }
| SIMPLIFY DELTA { `Delta [] :: simplify_red }
;
conseq:
| empty { None, None }
| f1=form { Some f1, None }
| f1=form LONGARROW { Some f1, None }
| f1=form LONGARROW UNDERSCORE { Some f1, None }
| LONGARROW f2=form { None, Some f2 }
| UNDERSCORE LONGARROW f2=form { None, Some f2 }
| f1=form LONGARROW f2=form { Some f1, Some f2 }
;
conseq_bd:
| c=conseq { c, None }
| c=conseq COLON cmp=hoare_bd_cmp? bd=sform { c, Some (cmp, bd) }
| UNDERSCORE COLON cmp=hoare_bd_cmp? bd=sform { (None, None), Some(cmp, bd) }
call_info:
| f1=form LONGARROW f2=form { CI_spec (f1, f2) }
| f=form { CI_inv f }
| bad=form COMMA p=form { CI_upto (bad,p,None) }
| bad=form COMMA p=form COMMA q=form { CI_upto (bad,p,Some q) }
tac_dir:
| BACKS { Backs }
| FWDS { Fwds }
| empty { Backs }
;
codepos:
| i=uint { (i, None) }
| c=CPOS { c }
;
code_position:
| n=uint { Single n }
| n1=uint n2=uint { Double (n1, n2) }
;
while_tac_info :
| inv=sform
{ (inv, None, None) }
| inv=sform vrnt=sform
{ (inv, Some vrnt, None) }
| inv=sform vrnt=sform k=sform eps=sform
{ (inv, Some vrnt, Some (k,eps)) }
;
rnd_info:
| empty
{ PNoRndParams }
| f=sform
{ PSingleRndParam f }
| f=sform g=sform
{ PTwoRndParams (f, g) }
| phi=sform d1=sform d2=sform d3=sform d4=sform p=sform?
{ PMultRndParams ((phi, d1, d2, d3, d4), p) }
;
swap_info:
| s=side? p=swap_pos { s,p }
;
swap_pos:
| i1=uint i2=uint i3=uint
{ SKbase (i1, i2, i3) }
| p=int
{ SKmove p }
| i1=uint p=int
{ SKmovei (i1, p) }
| LBRACKET i1=uint DOTDOT i2=uint RBRACKET p=int
{ SKmoveinter (i1, i2, p) }
;
int:
| n=uint { n }
| loc(MINUS) n=uint { -n }
;
side:
| LBRACE n=uint RBRACE {
match n with
| 1 -> true
| 2 -> false
| _ -> parse_error
(EcLocation.make $startpos $endpos)
(Some "variable side must be 1 or 2")
}
;
occurences:
| p=paren(uint+) {
if List.mem 0 p then
parse_error
(EcLocation.make $startpos $endpos)
(Some "`0' is not a valid occurence");
p
}
;
dbmap1:
| f=dbmap_flag? x=dbmap_target {
{ pht_flag = odfl `Include f;
pht_kind = (fst x);
pht_name = (snd x); }
}
;
dbmap_flag:
| ADD { `Include }
| MINUS { `Exclude }
;
dbmap_target:
| AT x=uqident { (`Theory, x) }
| x=qident { (`Lemma, x) }
;
dbhint:
| nl=boption(NOLOCALS) m=dbmap1* {
{ pht_nolocals = nl; pht_map = m; }
}
;
%inline prod_form:
| f1=sform f2=sform { Some f1, Some f2 }
| UNDERSCORE f2=sform { None , Some f2 }
| f1=sform UNDERSCORE { Some f1, None }
;
app_bd_info:
| empty { PAppNone }
| f=sform { PAppSingle f }
| f=prod_form g=prod_form s=sform?
{ PAppMult (s,fst f,snd f,fst g, snd g) }
;
logtactic:
| REFLEX
{ Preflexivity }
| ASSUMPTION
{ Passumption }
| GENERALIZE l=genpattern+
{ Pgeneralize l }
| MOVE
{ Pgeneralize [] }
| MOVE COLON gp=genpattern+
{ Pgeneralize gp }
| CLEAR l=ident+
{ Pclear l }
| CONGR
{ Pcongr }
| TRIVIAL
{ Ptrivial }
| SMT db=dbhint pi=prover_info
{ Psmt (Some db, pi) }
| INTROS a=intro_pattern*
{ Pintro a }
| SPLIT
{ Psplit }
| FIELD eqs=ident*
{ Pfield eqs }
| RING eqs=ident*
{ Pring eqs }
| ALGNORM
{ Palg_norm }
| EXIST a=iplist1(loc(fpattern_arg), COMMA) %prec prec_below_comma
{ Pexists a }
| LEFT
{ Pleft }
| RIGHT
{ Pright }
| ELIM e=genpattern*
{ Pelim (e, None) }
| ELIM SLASH p=qident e=genpattern*
{ Pelim (e, Some p) }
| APPLY e=fpattern(form)
{ Papply (e, `Apply None) }
| APPLY e=fpattern(form) IN x=ident
{ Papply (e, `Apply (Some x)) }
| EXACT e=fpattern(form)
{ Papply (e, `Exact) }
| l=simplify
{ Psimplify (mk_simplify l) }
| CHANGE f=sform
{ Pchange f }
| REWRITE a=rwarg+
{ Prewrite a }
| RWNORMAL f=sform WITH ps=qident+
{ Prwnormal (f, ps) }
| SUBST l=sform*
{ Psubst l }
| CUT ip=intro_pattern* COLON p=form %prec prec_below_IMPL
{ Pcut (ip, p, None) }
| CUT ip=intro_pattern* COLON p=form BY t=tactic_core
{ Pcut (ip, p, Some t) }
| CUT ip=intro_pattern* CEQ fp=pterm
{ Pcutdef (ip, fp) }
| POSE o=rwocc? x=ident CEQ p=form_h %prec prec_below_IMPL
{ Ppose (x, o |> omap (snd_map EcMaps.Sint.of_list), p) }
;
eager_info:
| h=ident
{ LE_done h }
| LPAREN h=ident COLON s1=stmt TILD s2=stmt COLON pr=form LONGARROW po=form RPAREN
{ LE_todo (h, s1, s2, pr, po) }
;
eager_tac:
| SEQ n1=uint n2=uint i=eager_info COLON p=sform
{ Peager_seq (i,(n1,n2),p) }
| IF
{ Peager_if }
| WHILE i=eager_info
{ Peager_while i }
| PROC
{ Peager_fun_def }
| PROC i=eager_info f=sform
{ Peager_fun_abs (i, f) }
| CALL info=fpattern(call_info)
{ Peager_call info }
| info=eager_info COLON p=sform
{ Peager (info, p) }
;
phltactic:
| PROC
{ Pfun `Def }
| PROC f=sform
{ Pfun (`Abs f) }
| PROC bad=sform p=sform q=sform?
{ Pfun (`Upto (bad, p, q)) }
| PROC STAR
{ Pfun `Code }
| SEQ d=tac_dir pos=code_position COLON p=sform f=app_bd_info
{ Papp (d, pos, p, f) }
| WP n=code_position?
{ Pwp n }
| SP n=code_position?
{ Psp n }
| SKIP
{ Pskip }
| WHILE s=side? info=while_tac_info
{ Pwhile (s, info) }
| CALL s=side? info=fpattern(call_info)
{ Pcall (s, info) }
| RCONDT s=side? i=uint
{ Prcond (s, true, i) }
| RCONDF s=side? i=uint
{ Prcond (s, false, i) }
| IF s=side?
{ Pcond s }
| SWAP info=iplist1(loc(swap_info), COMMA) %prec prec_below_comma
{ Pswap info }
| CFOLD s=side? c=codepos NOT n=uint
{ Pcfold (s, c, Some n) }
| CFOLD s=side? c=codepos
{ Pcfold (s, c, None) }
| RND s=side? info=rnd_info
{ Prnd (s, info) }
| INLINE s=side? o=occurences? f=plist1(loc(fident), empty)
{ Pinline (`ByName (s, (f, o))) }
| INLINE s=side? STAR
{ Pinline (`All s) }
| KILL s=side? o=codepos
{ Pkill (s, o, Some 1) }
| KILL s=side? o=codepos NOT n=uint
{ Pkill (s, o, Some n) }
| KILL s=side? o=codepos NOT STAR
{ Pkill (s, o, None) }
| p=tselect INLINE
{ Pinline (`ByPattern p) }
| ALIAS s=side? o=codepos
{ Palias (s, o, None) }
| ALIAS s=side? o=codepos WITH x=lident
{ Palias (s, o, Some x) }
| ALIAS s=side? o=codepos x=lident EQ e=expr
{ Pset (s, o, false, x,e) }
| FISSION s=side? o=codepos AT d1=uint COMMA d2=uint
{ Pfission (s, o, (1, (d1, d2))) }
| FISSION s=side? o=codepos NOT i=uint AT d1=uint COMMA d2=uint
{ Pfission (s, o, (i, (d1, d2))) }
| FUSION s=side? o=codepos AT d1=uint COMMA d2=uint
{ Pfusion (s, o, (1, (d1, d2))) }
| FUSION s=side? o=codepos NOT i=uint AT d1=uint COMMA d2=uint
{ Pfusion (s, o, (i, (d1, d2))) }
| UNROLL s=side? o=codepos
{ Punroll (s, o) }
| SPLITWHILE c=expr COLON s=side? o=codepos
{ Psplitwhile (c, s, o) }
| BYPHOARE info=fpattern(conseq)
{ Pbydeno (`PHoare, info) }
| BYEQUIV info=fpattern(conseq)
{ Pbydeno (`Equiv, info) }
| CONSEQ nm=STAR?
{ Pconseq(nm<>None, (None,None,None)) }
| CONSEQ nm=STAR? info1=fpattern(conseq_bd)
{ Pconseq (nm<>None, (Some info1,None,None)) }
| CONSEQ nm=STAR? info1=fpattern(conseq_bd) info2=fpattern(conseq_bd) UNDERSCORE?
{ Pconseq(nm<>None, (Some info1,Some info2, None)) }
| CONSEQ nm=STAR? info1=fpattern(conseq_bd) UNDERSCORE info3=fpattern(conseq_bd)
{ Pconseq(nm<>None, (Some info1,None,Some info3)) }
| CONSEQ nm=STAR?
info1=fpattern(conseq_bd)
info2=fpattern(conseq_bd)
info3=fpattern(conseq_bd)
{ Pconseq (nm<>None, (Some info1,Some info2,Some info3)) }
| CONSEQ nm=STAR? UNDERSCORE info2=fpattern(conseq_bd) UNDERSCORE?
{ Pconseq(nm<>None, (None,Some info2, None)) }
| CONSEQ nm=STAR? UNDERSCORE UNDERSCORE info3=fpattern(conseq_bd)
{ Pconseq(nm<>None, (None,None,Some info3)) }
| ELIM STAR
{ Phr_exists_elim }
| EXIST STAR l=iplist1(sform, COMMA) %prec prec_below_comma
{ Phr_exists_intro l }
| EXFALSO
{ Pexfalso }
| BYPR
{ PPr None }
| BYPR f1=sform f2=sform
{ PPr (Some (f1, f2)) }
| FEL at_pos=uint cntr=sform delta=sform q=sform f_event=sform some_p=fel_pred_specs inv=sform?
{ Pfel (at_pos,(cntr,delta,q,f_event,some_p,inv)) }
| SIM info=eqobs_in
{ Psim info }
| TRANSITIVITY tk=trans_kind h1=trans_hyp h2=trans_hyp
{ Ptrans_stmt (tk, fst h1, snd h1, fst h2, snd h2) }
| SYMMETRY
{ Psymmetry }
| EAGER t=eager_tac
{ t }
| HOARE
{ Phoare }
| PRBOUNDED
{ Pprbounded }
| PHOARE SPLIT i=bdhoare_split
{ Pbdhoare_split i }
| PHOARE EQUIV s=side pr=sform po=sform
{ Pbd_equiv(s, pr, po) }
| AUTO { Pauto }
;
bdhoare_split:
| b1=sform b2=sform b3=sform?
{ BDH_split_bop (b1,b2,b3) }
| b1=sform b2=sform COLON f=sform
{ BDH_split_or_case (b1,b2,f) }
| NOT b1=sform b2=sform
{ BDH_split_not (Some b1,b2) }
;
trans_kind:
| s=side c=brace(stmt) { TKstmt(Some s, c) }
| f=loc(fident) { TKfun (f) }
;
trans_hyp:
| LPAREN p=form LONGARROW q=form RPAREN { (p,q) }
;
fel_pred_spec:
| f=loc(fident) COLON p=sform
{ (f, p) }
fel_pred_specs:
| LBRACKET assoc_ps = plist0(fel_pred_spec, SEMICOLON) RBRACKET
{assoc_ps}
eqobs_in:
| empty { (None , None , None) }
| COLON f3=sform { (None , None , Some f3) }
| f1=sform COLON f3=sform? { (Some f1, None , f3) }
| f1=sform f2=sform COLON f3=sform? { (Some f1, Some f2, f3) }
;
pgoptionkw:
| x=loc(SPLIT) { mk_loc x.pl_loc "split" }
| x=loc(SUBST) { mk_loc x.pl_loc "subst" }
| x=lident { x }
;
pgoption:
| b=boption(MINUS) DELTA
{ (not b, `Delta None) }
| b=boption(MINUS) DELTA COLON SPLIT
{ (not b, `Delta (Some `Split)) }
| b=boption(MINUS) DELTA COLON CASE
{ (not b, `Delta (Some `Case)) }
| b=boption(MINUS) x=pgoptionkw {
match unloc x with
| "split" -> (not b, `Split)
| "solve" -> (not b, `Solve)
| "subst" -> (not b, `Subst)
| _ ->
parse_error x.pl_loc
(Some ("invalid option: " ^ (unloc x)))
}
;
pgoptions:
| xs=bracket(pgoption+) { xs }
;
tactic_core_r:
| IDTAC
{ Pidtac None }
| IDTAC s=STRING
{ Pidtac (Some s) }
| TRY t=tactic_core
{ Ptry t }
| BY t=tactics
{ Pby (Some t) }
| BY bracket(empty) | DONE
{ Pby None }
| DO t=tactic_core
{ Pdo ((`All, None), t) }
| DO n=uint? NOT t=tactic_core
{ Pdo ((`All, n), t) }
| DO n=uint? QUESTION t=tactic_core
{ Pdo ((`Maybe, n), t) }
| LPAREN s=tactics RPAREN
{ Pseq s }
| ADMIT
{ Padmit }
| CASE gp=genpattern*
{ Pcase gp }
| PROGRESS opts=pgoptions? t=tactic_core? {
Pprogress (odfl [] opts, t)
}
| x=logtactic
{ Plogic x }
| x=phltactic
{ PPhl x }
(* DEBUG *)
| DEBUG
{ Pdebug }
;
%inline tactic_core:
| x=loc(tactic_core_r) { x }
;
tactic_ip:
| t=tactic_core %prec prec_below_IMPL
{ mk_core_tactic t }
| t=tactic_core IMPL ip=intro_pattern+
{ { pt_core = t; pt_intros = ip; } }
;
tactic:
| t=tactic_ip %prec prec_below_IMPL
{ t }
| t1=tactic_ip ORA t2=tactic_ip
{ let loc = EcLocation.make $startpos $endpos in
mk_core_tactic (mk_loc loc (Por (t1, t2))) }
;
tactic_chain:
| LBRACKET ts=plist1(loc(tactics0), PIPE) RBRACKET
{ Psubtacs (List.map mk_core_tactic ts) }
| FIRST t=loc(tactics) { Pfirst (mk_core_tactic (mk_loc t.pl_loc (Pseq (unloc t))), 1) }
| LAST t=loc(tactics) { Plast (mk_core_tactic (mk_loc t.pl_loc (Pseq (unloc t))), 1) }
| FIRST n=uint t=loc(tactics) { Pfirst (mk_core_tactic (mk_loc t.pl_loc (Pseq (unloc t))), n) }
| LAST n=uint t=loc(tactics) { Plast (mk_core_tactic (mk_loc t.pl_loc (Pseq (unloc t))), n) }
| FIRST LAST { Protate (`Left , 1) }
| LAST FIRST { Protate (`Right, 1) }
| FIRST n=uint LAST { Protate (`Left , n) }
| LAST n=uint FIRST { Protate (`Right, n) }
| EXPECT n=uint t=loc(tactics) { Pexpect (mk_core_tactic (mk_loc t.pl_loc (Pseq (unloc t))), n) }
;
subtactic:
| t=loc(tactic_chain)
{ mk_core_tactic (mk_loc t.pl_loc (Psubgoal (unloc t))) }
| t=tactic
{ t }
;
subtactics:
| t=subtactic { [t] }
| ts=subtactics SEMICOLON t=subtactic { t :: ts }
;
tactics:
| t=tactic %prec SEMICOLON { [t] }
| t=tactic SEMICOLON ts=subtactics { t :: (List.rev ts) }
;
tactics0:
| ts=tactics { Pseq ts }
| x=loc(empty) { Pseq [mk_core_tactic (mk_loc x.pl_loc (Pidtac None))] }
tactics_or_prf:
| t=tactics { `Actual t }
| p=proof { `Proof p }
;
proof:
| PROOF modes=proofmode1* {
let seen = Hashtbl.create 0 in
List.fold_left
(fun pmodes (mode, flag) ->
if Hashtbl.mem seen mode then
parse_error mode.pl_loc (Some "duplicated flag");
Hashtbl.add seen mode ();
match unloc mode with
| `Strict -> { pmodes with pm_strict = flag; })
{ pm_strict = true; } modes
}
;
proofmode1:
| b=boption(MINUS) pm=loc(proofmodename) { (pm, not b) }
;
proofmodename:
| STRICT { `Strict }
;
(* -------------------------------------------------------------------- *)
(* Theory cloning *)
theory_clone:
| CLONE ip=import_flag? x=uqident cw=clone_with? cp=clone_proof?
{ let oth =
{ pthc_base = x;
pthc_name = None;
pthc_ext = EcUtils.odfl [] cw;
pthc_prf = EcUtils.odfl [] cp; }
in
(oth, ip) }
| CLONE ip=import_flag? x=uqident AS y=uident cw=clone_with? cp=clone_proof?
{ let oth =
{ pthc_base = x;
pthc_name = Some y;
pthc_ext = EcUtils.odfl [] cw;
pthc_prf = EcUtils.odfl [] cp; }
in
(oth, ip) }
;
clone_with:
| WITH x=plist1(clone_override, COMMA) { x }
;
clone_lemma_base:
| STAR { `All }
| 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))
| (xs, `All ) -> begin
match List.rev xs with
| [] -> `All None
| x :: xs -> `All (Some (mk_loc l.pl_loc (List.rev xs, x)))
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=clone_lemma_1
{ [x] }
| xs=clone_lemma COMMA x=clone_lemma_1
{ x :: xs }
;
clone_proof:
| PROOF x=clone_lemma { List.rev x }
;
opclmode:
| EQ { `Alias }
| LARROW { `Inline }
;
cltyparams:
| empty { [] }
| x=tident { [x] }
| xs=paren(plist1(tident, COMMA)) { xs }
;
clone_override:
| TYPE ps=cltyparams x=qident EQ t=loc(type_exp)
{ (x, PTHO_Type (ps, t, `Alias)) }
| TYPE ps=cltyparams x=qident LARROW t=loc(type_exp)
{ (x, PTHO_Type (ps, t, `Inline)) }
| OP x=qoident tyvars=bracket(tident*)? COLON sty=loc(type_exp) mode=opclmode e=expr
{ let ov = {
opov_tyvars = tyvars;
opov_args = [];
opov_retty = sty;
opov_body = e;
} in
(x, PTHO_Op (ov, mode)) }
| OP x=qoident tyvars=bracket(tident*)? mode=loc(opclmode) e=expr
{ let ov = {
opov_tyvars = tyvars;
opov_args = [];
opov_retty = mk_loc mode.pl_loc PTunivar;
opov_body = e;
} in
(x, PTHO_Op (ov, unloc mode)) }
| OP x=qoident tyvars=bracket(tident*)? p=ptybindings mode=loc(opclmode) e=expr
{ let ov = {
opov_tyvars = tyvars;
opov_args = p;
opov_retty = mk_loc mode.pl_loc PTunivar;
opov_body = e;
} in
(x, PTHO_Op (ov, unloc mode)) }
| PRED x=qoident tyvars=bracket(tident*)? p=ptybindings EQ f=form
{ let ov = {
prov_tyvars = tyvars;
prov_args = p;
prov_body = f;
} in
(x, PTHO_Pred ov) }
| PRED x=qoident tyvars=bracket(tident*)? EQ f=form
{ let ov = {
prov_tyvars = tyvars;
prov_args = [];
prov_body = f;
} in
(x, PTHO_Pred ov) }
| THEORY x=uqident EQ y=uqident
{ (x, PTHO_Theory y) }
;
realize:
| REALIZE x=qident { x }
;
(* -------------------------------------------------------------------- *)
(* Printing *)
print:
| TYPE qs=qident { Pr_ty qs }
| GLOB qs=loc(mod_qident) { Pr_glob qs }
| OP qs=qoident { Pr_op qs }
| THEORY qs=qident { Pr_th qs }
| PRED qs=qoident { Pr_pr qs }
| AXIOM qs=qident { Pr_ax qs }
| MODULE qs=qident { Pr_mod qs }
| MODULE TYPE qs=qident { Pr_mty qs }
;
prover_iconfig:
| /* empty */ { (None , None ) }
| i=uint { (Some i , None ) }
| i1=uint i2=uint { (Some i1, Some i2) }
;
prover_info:
| ic=prover_iconfig pl=plist1(loc(STRING), empty)?
{ let (m, t) = ic in
{ pprov_max = m;
pprov_time = t;
pprov_names = pl; } }
;
gprover_info:
| PROVER x=prover_info
{ x }
| TIMEOUT t=uint
{ { pprov_max = None; pprov_time = Some t; pprov_names = None } }
;
addrw:
| HINT REWRITE p=lqident COLON l=lqident* {p,l}
;
(* -------------------------------------------------------------------- *)
(* Global entries *)
global_:
| theory_open { GthOpen $1 }
| theory_close { GthClose $1 }
| theory_require { GthRequire $1 }
| theory_import { GthImport $1 }
| theory_export { GthExport $1 }
| theory_clone { GthClone $1 }
| theory_w3 { GthW3 $1 }
| section_open { GsctOpen $1 }
| section_close { GsctClose $1 }
| top_decl { Gdeclare $1 }
| top_mod_def { Gmodule $1 }
| sig_def { Ginterface $1 }
| typedecl { Gtype $1 }
| typeclass { Gtypeclass $1 }
| tycinstance { Gtycinstance $1 }
| operator { Goperator $1 }
| predicate { Gpredicate $1 }
| axiom { Gaxiom $1 }
| tactics_or_prf { Gtactics $1 }
| realize { Grealize $1 }
| gprover_info { Gprover_info $1 }
| x=loc(QED) { Gsave x.pl_loc }
| PRINT p=print { Gprint p }
| PRAGMA x=lident { Gpragma x }
| EXTRACTION i=extract_info { Gextract i }
| addrw { Gaddrw $1 }
;
extract_info:
| s=STRING? qs=plist1(toextract,COMMA) w=withextract { (s,qs,w) }
;
toextract:
| OP q=qoident {ExOp q}
| TYPE q=qoident {ExTy q}
| THEORY q=qoident {ExTh q}
;
withextract:
| empty { [] }
| WITH w=plist1(withextract1,COMMA) { w }
;
withextract1:
| p=toextract EQ s=STRING { p,s }
;
stop:
| EOF { }
| DROP DOT { }
;
global:
| g=loc(global_) FINAL { g }
;
prog_r:
| g=global { P_Prog ([g], false) }
| stop { P_Prog ([ ], true ) }
| UNDO d=uint FINAL
{ P_Undo d }
| error
{ parse_error (EcLocation.make $startpos $endpos) None }
;
prog:
| x=loc(prog_r) { x }
;
(* -------------------------------------------------------------------- *)
%inline plist0(X, S):
| aout=separated_list(S, X) { aout }
;
iplist1_r(X, S):
| x=X { [x] }
| xs=iplist1_r(X, S) S x=X { x :: xs }
;
%inline iplist1(X, S):
| xs=iplist1_r(X, S) { List.rev xs }
;
%inline plist1(X, S):
| aout=separated_nonempty_list(S, X) { aout }
;
%inline plist2(X, S):
| x=X S xs=plist1(X, S) { x :: xs }
;
%inline list2(X):
| x=X xs=X+ { x :: xs }
;
%inline empty:
| /**/ { () }
;
(* -------------------------------------------------------------------- *)
__rlist1(X, S): (* left-recursive *)
| x=X { [x] }
| xs=__rlist1(X, S) S x=X { x :: xs }
;
%inline rlist0(X, S):
| /* empty */ { [] }
| xs=rlist1(X, S) { xs }
;
%inline rlist1(X, S):
| xs=__rlist1(X, S) { List.rev xs }
;
%inline rlist2(X, S):
| xs=__rlist1(X, S) S x=X { List.rev (x :: xs) }
;
(* -------------------------------------------------------------------- *)
%inline paren(X):
| LPAREN x=X RPAREN { x }
;
%inline brace(X):
| LBRACE x=X RBRACE { x }
;
%inline bracket(X):
| LBRACKET x=X RBRACKET { x }
;
(* -------------------------------------------------------------------- *)
%inline loc(X):
| x=X {
{ pl_desc = x;
pl_loc = EcLocation.make $startpos $endpos;
}
}
;