ecParsetree.ml

(* -------------------------------------------------------------------- *)
open EcBigInt
open EcMaps
open EcSymbols
open EcLocation
open EcUtils
open EcTypes

(* -------------------------------------------------------------------- *)
exception ParseError of EcLocation.t * string option

(* -------------------------------------------------------------------- *)
type side  = [`Left | `Right]
type oside = side option

let side2str (side : side) =
  match side with
  | `Left  -> "left"
  | `Right -> "right"

let negside (side : side) : side =
  match side with `Left -> `Right | `Right -> `Left

let sideif (side : side) xt xf =
  match side with `Left -> xt | `Right -> xf

(* -------------------------------------------------------------------- *)
let qsymb_of_symb (x : symbol) : qsymbol = ([], x)

(* -------------------------------------------------------------------- *)
type psymbol   = symbol  located
type pqsymbol  = qsymbol located
type pmsymbol  = (psymbol * ((pmsymbol located) list) option) list
type pgamepath = (pmsymbol * psymbol) located

type osymbol_r   = psymbol option
type osymbol     = osymbol_r located

(* -------------------------------------------------------------------- *)
(* A bullet at the start of a `.`-terminated tactic phrase. The kind
   identifies the bullet character (`-`, `+`, `*`); the count is the
   number of repetitions (`>= 1`). *)
type bullet_kind = [ `Minus | `Plus | `Star ]
type bullet = { b_kind : bullet_kind; b_count : int; }

(* -------------------------------------------------------------------- *)
type pcp_match = [
  | `If
  | `While
  | `Match
  | `Assign of plvmatch
  | `AssignTuple of plvmatch
  | `Sample of plvmatch
  | `Call of plvmatch
]

and plvmatch = [ `LvmNone | `LvmVar of pqsymbol ]

(* `Index1: 1-indexed position (standard user syntax)
   `Index0: 0-indexed position (used by seq, rndsem, etc.) *)
type pcp_base  = [
  | `ByPos of int * [`Index0 | `Index1]
  |`ByMatch of int option * pcp_match
]

(* Code positions *)
type pbranch_select = [`Cond of bool | `Match of psymbol]
type pcodepos1 = int * pcp_base
type pcodepos_step = (pcodepos1 * pbranch_select)
type pcodepos_path = pcodepos_step list 
type pcodepos  = pcodepos_path * pcodepos1
type pdocodepos1 = pcodepos1 doption option

(* Code position offsets *)
type pcodeoffset1 = [
  | `Relative of int
  | `Absolute of pcodepos1
]

(* Code gap types *)
type pcodegap1 =
  | GapBefore of pcodepos1
  | GapAfter  of pcodepos1

(* Boundary gap constructors *)
type pcodegap        = pcodepos_path * pcodegap1
type pcodegap1_range = pcodegap1 * pcodegap1
type pcodegap_range  = pcodepos_path * pcodegap1_range

(* Code position ranges *)
type pcodepos_or_range =
  | Pos   of pcodepos
  | Range of pcodegap_range

type prange1_or_insert =
  | PosOrRange of pcodepos_or_range
  | Gap        of pcodegap

(* Gap-based offset for swap *)
type pcodegap_offset1 =
  | PGapAbsolute of pcodegap1
  | PGapRelative of int

type pdocodegap1 = pcodegap1 doption option

(* -------------------------------------------------------------------- *)
type pty_r =
  | PTunivar
  | PTtuple  of pty list
  | PTnamed  of pqsymbol
  | PTvar    of psymbol
  | PTapp    of pqsymbol * pty list
  | PTfun    of pty * pty
  | PTglob   of pmsymbol located
and pty = pty_r located

type ptyannot_r =
  | TVIunamed of pty list
  | TVInamed  of (psymbol * pty) list

and ptyannot  = ptyannot_r  located

type plpattern_r =
  | LPSymbol of psymbol
  | LPTuple  of osymbol list
  | LPRecord of (pqsymbol * psymbol) list

and plpattern = plpattern_r located

type ppattern =
| PPApp of (pqsymbol * ptyannot option) * osymbol list
| PPAny

type ptybinding  = osymbol list * pty
and  ptybindings = ptybinding list

and 'a rfield = {
  rf_name  : pqsymbol;
  rf_tvi   : ptyannot option;
  rf_value : 'a;
}

(* -------------------------------------------------------------------- *)
type pmodule_type = pqsymbol

type ptyparam  = psymbol
type ptyparams = ptyparam list
type ptydname  = (ptyparams * psymbol) located

type ptydecl = {
  pty_name   : psymbol;
  pty_tyvars : ptyparams;
  pty_body   : ptydbody;
  pty_locality : locality;
}

and ptydbody =
  | PTYD_Abstract
  | PTYD_Alias    of pty
  | PTYD_Record   of precord
  | PTYD_Datatype of pdatatype

and pdatatype = (psymbol * pty list) list

and precord = (psymbol * pty) list

(* -------------------------------------------------------------------- *)
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 pmemory   = psymbol

type phoarecmp = EcFol.hoarecmp

type glob_or_var =
  | GVglob of pmsymbol located * pqsymbol list
  | GVvar  of pqsymbol

(* -------------------------------------------------------------------- *)
type plvalue_r =
  | PLvSymbol of pqsymbol
  | PLvTuple  of pqsymbol list
  | PLvMap    of pqsymbol * ptyannot option * pty option * pexpr list

and plvalue = plvalue_r located

and pinstr_r =
  | PSident  of psymbol
  | PSasgn   of plvalue * pexpr
  | PSrnd    of plvalue * pexpr
  | PScall   of plvalue option * pgamepath * (pexpr list) located
  | PSif     of pscond * pscond list * pstmt
  | PSwhile  of pscond
  | PSmatch  of pexpr * psmatch
  | PSraise  of pexpr

and psmatch = [
  | `Full of (ppattern * pstmt) list
  | `If   of (ppattern * pstmt) * pstmt option
]

and pscond = pexpr * pstmt
and pinstr = pinstr_r located
and pstmt  = pinstr list

and pexpr   = pexpr_r located
and pexpr_r = Expr of pformula

and pformula  = pformula_r located

and phoare_exception =
  (ppattern * pformula) list located

and phoare_post = {
  pnormal : pformula;
  pexcept : phoare_exception;
}

and pformula_r =
  | PFhole
  | PFcast    of pformula * pty
  | PFint     of zint
  | PFdecimal of (zint * (int * zint))
  | PFtuple   of pformula list
  | PFident   of pqsymbol * ptyannot option
  | PFref     of psymbol * pffilter list
  | PFmem     of psymbol
  | PFside    of pformula * (bool * symbol located)
  | PFapp     of pformula * pformula list
  | PFif      of pformula * pformula * pformula
  | PFmatch   of pformula * (ppattern * pformula) list
  | PFlet     of plpattern * (pformula * pty option) * pformula
  | PFforall  of pgtybindings * pformula
  | PFexists  of pgtybindings * pformula
  | PFlambda  of ptybindings * pformula
  | PFrecord  of pformula option * pformula rfield list
  | PFproj    of pformula * pqsymbol
  | PFproji   of pformula * int
  | PFglob    of pmsymbol located
  | PFeqveq   of glob_or_var list * (pmsymbol pair) option
  | PFeqf     of pformula list
  | PFlsless  of pgamepath
  | PFscope   of pqsymbol * pformula
  | PFhoareF   of psymbol option * pformula * pgamepath * phoare_post
  | PFehoareF  of psymbol option * pformula * pgamepath * pformula
  | PFequivF   of psymbol option * psymbol option * pformula * (pgamepath * pgamepath) * pformula
  | PFeagerF   of psymbol option * psymbol option * pformula * (pstmt * pgamepath * pgamepath * pstmt) * pformula
  | PFprob     of psymbol option * pgamepath * (pformula list) * pmemory * pformula
  | PFBDhoareF of psymbol option * pformula * pgamepath * pformula * phoarecmp * pformula

and pmemtype_el = ([`Single|`Tuple] * (psymbol list)) located * pty
and pmemtype    = pmemtype_el list

and pgtybinding  = osymbol list * pgty
and pgtybindings = pgtybinding list

and pgscbinding  = psymbol list * pty
and pgscbindings = pgscbinding list

and pgty =
| PGTY_Type  of pty
| PGTY_ModTy of pmodule_type_restr
| PGTY_Mem   of pmemtype option

and pffilter =
| PFRange      of bool * pfrange list
| PFMatch      of bool * psymbol * pformula
| PFMatchBuild of bool * psymbol list * pformula * pformula
| PFKeep       of bool * bool * bool * pffilter_pattern

and pffilter_pattern = [
  | `Pattern of pformula
  | `VarSet  of (pqsymbol * psymbol option) list
]

and pfrange = [
  | `Single of pfindex
  | `Range  of pfindex option pair
]

and pfindex = [ `Index of int | `Match of pformula * int option]

(* if [pmty_mem] is [None], there are no user-supplied restriction, which is
   different from the user supplying an empty restriction.
   In the former case, we keep the restriction we obtain by type-checking,
   while in the latter case, we replace the type-checking restriction by an
   empty restriction.  *)
and pmodule_type_restr =
  { pmty_pq  : pqsymbol;
    pmty_mem : pmod_restr option; }

(* -------------------------------------------------------------------- *)
(* qident optionally taken in a (implicit) module parameters. *)
and qident_inparam = { inp_in_params : bool;
	                     inp_qident    : pqsymbol; }

and poracles = qident_inparam list

and pmod_restr_el = {
	pmre_name  : psymbol;
  pmre_orcls : poracles option;  (* None means no restriction *)
}

and pmod_restr = {
  pmr_mem   : pmod_restr_mem;
 }

(* -------------------------------------------------------------------- *)
and pmodule_sig =
  | Pmty_struct of pmodule_sig_struct

and pmodule_sig_struct = {
  pmsig_params : (psymbol * pmodule_type) list;
  pmsig_body   : pmodule_sig_struct_body;
}

and pmodule_sig_struct_body = pmodule_sig_item list

and minclude_proc = [
  | `MInclude of psymbol list
  | `MExclude of psymbol list
]

and pmodule_sig_item = [
  | `Include      of pmodule_type * minclude_proc option * qident_inparam list option
  | `FunctionDecl of pfunction_decl
]

and pvariable_decl = {
  pvd_name : psymbol;
  pvd_type : pty;
}

and fun_params = (osymbol * pty) list

and pfunction_decl = {
  pfd_name     : psymbol;
  pfd_tyargs   : fun_params;
  pfd_tyresult : pty;
  pfd_uses     : pmod_restr_el;
}

(* -------------------------------------------------------------------- *)
and pmodule_def_or_decl = {
  ptm_locality : locality;
  ptm_def      : [`Concrete of pmodule_def | `Abstract of pmodule_decl];
}

and pmodule_decl = {
  ptm_name  : psymbol;
  ptm_modty : pmodule_type_restr;
}

and pmodule_def = {
  ptm_header : pmodule_header;
  ptm_body   : pmodule_expr;
}

and pmodule_header =
  | Pmh_ident  of psymbol
  | Pmh_params of (pmodule_header * pmodule_params) located
  | Pmh_cast   of pmodule_header * pqsymbol list

and pmodule_params = (psymbol * pmodule_type) list

and pmodule_expr_r =
  | Pm_ident  of pmsymbol
  | Pm_struct of pstructure
  | Pm_update of pmsymbol * psymbol list * pupdate_var list * pupdate_fun list

and pmodule_expr = pmodule_expr_r located

and pstructure = pstructure_item located list

and pstructure_item =
  | Pst_mod      of (psymbol * pqsymbol list * pmodule_expr)
  | Pst_var      of (psymbol list * pty)
  | Pst_fun      of (pfunction_decl * pfunction_body)
  | Pst_alias    of (psymbol * pgamepath)
  | Pst_include  of (pmsymbol located * bool * minclude_proc option)
  | Pst_import   of (pmsymbol located) list

and pupdate_var = psymbol list * pty
and pupdate_fun = psymbol * (psymbol list * pty) list * ((pcodepos_or_range located * pupdate_item) list * pexpr option)

and pupdate_item =
  | Pup_stmt of pupdate_stmt
  | Pup_cond of pupdate_cond

and pupdate_stmt =
  | Pups_add of (pstmt * bool)
  | Pups_del

and pupdate_cond =
  | Pupc_add of (pexpr * bool)
  | Pupc_mod of pexpr
  | Pupc_del of pbranch_select

and pfunction_body = {
  pfb_locals : pfunction_local list;
  pfb_body   : pstmt;
  pfb_return : pexpr option;
}

and pfunction_local = {
  pfl_names : ([`Single|`Tuple] * (psymbol list)) located;
  pfl_type  : pty   option;
  pfl_init  : pexpr option;
}

type pinterface = {
  pi_name : psymbol;
  pi_sig : pmodule_sig;
  pi_locality : is_local;
}

(* -------------------------------------------------------------------- *)
let rec pf_ident ?(raw = false) f =
  match unloc f with
  | PFident ({ pl_desc = ([], x) }, _) -> Some x
  | PFtuple [f] when not raw -> pf_ident ~raw f
  | _ -> None

  let rec pcmhd_ident (pcmhd : pmodule_header) : psymbol =
    match pcmhd with
    | Pmh_ident nm -> nm
    | Pmh_params x -> pcmhd_ident (fst (unloc x))
    | Pmh_cast (pmh, _) -> pcmhd_ident pmh

(* -------------------------------------------------------------------- *)
type psubtype = {
  pst_name    : psymbol;
  pst_cname   : psymbol option;
  pst_carrier : pty;
  pst_pred    : (psymbol * pformula);
  pst_rename  : (string * string) option;
}

(* -------------------------------------------------------------------- *)
type ptyvardecls =
  psymbol list

type pop_def =
  | PO_abstr of pty
  | PO_concr of pty * pformula
  | PO_case  of pty * pop_branch list
  | PO_reft  of pty * (psymbol * pformula)

and pop_branch = {
  pop_patterns : pop_pattern list;
  pop_body     : pexpr;
}

and pop_pattern = {
  pop_name    : psymbol;
  pop_pattern : ppattern;
}

type poperator = {
  po_kind   : [`Op | `Const];
  po_name   : psymbol;
  po_aliases: psymbol list;
  po_tags   : psymbol list;
  po_tyvars : ptyvardecls option;
  po_args   : ptybindings * ptybindings option;
  po_def    : pop_def;
  po_ax     : osymbol_r;
  po_locality : locality;
}

and pprocop = {
  ppo_name     : psymbol;
  ppo_target   : pgamepath;
  ppo_locality : locality;
}

type pexception_decl = {
  pe_name     : psymbol;
  pe_dom      : pty list;
  pe_locality : locality;
}

type ppred_def =
  | PPabstr of pty list
  | PPconcr of ptybindings * pformula
  | PPind   of ppind

and ppind_ctor = {
  pic_name : psymbol;
  pic_bds  : pgtybindings;
  pic_spec : pformula list;
}

and ppind = ptybindings * (ppind_ctor list)

type ppredicate = {
  pp_name   : psymbol;
  pp_tyvars : psymbol list option;
  pp_def    : ppred_def;
  pp_tags   : psymbol list;
  pp_locality  : locality;
}

(* -------------------------------------------------------------------- *)
type pnotation = {
  nt_name  : psymbol;
  nt_tv    : ptyvardecls option;
  nt_bd    : (psymbol * pty) list;
  nt_args  : (psymbol * (psymbol list * pty option)) list;
  nt_codom : pty;
  nt_body  : pexpr;
  nt_local : is_local;
}

(* -------------------------------------------------------------------- *)
type abrvopt  = [`Printing]
type abrvopts = (bool * abrvopt) list

type pabbrev = {
  ab_name  : psymbol;
  ab_tv    : ptyvardecls option;
  ab_args  : ptybindings;
  ab_def   : pty * pexpr;
  ab_opts  : abrvopts;
  ab_local : is_local;
}

(* -------------------------------------------------------------------- *)
type 'a ppt_head =
  | FPNamed of pqsymbol * ptyannot option
  | FPCut   of 'a

type ppt_arg =
  | EA_none
  | EA_form   of pformula
  | EA_mem    of pmemory
  | EA_mod    of pmsymbol located
  | EA_proof  of (pformula option) gppterm
  | EA_tactic of [`Done | `Smt | `DoneSmt]

and 'a gppterm = {
  fp_mode : [`Implicit | `Explicit];
  fp_head : 'a ppt_head;
  fp_args : ppt_arg located list
}

type ppterm  = (pformula option) gppterm

type pcutdef = {
  ptcd_name : pqsymbol;
  ptcd_tys  : ptyannot option;
  ptcd_args : ppt_arg located list;
}

(* λ mem → formula *)
type pmpred_args = (osymbol * pformula) list

(* -------------------------------------------------------------------- *)
(* The [hint …] clause of a [simplify]/[cbv] call. [ph_select] is the
   unsigned base database selection (empty = use the proof-local default
   / active set); [ph_dbs] are signed activate ([true]) / deactivate
   ([false]) deltas on the current set; [ph_select] and [ph_dbs] are
   mutually exclusive. [ph_hd] is the optional single-mode head filter;
   [ph_lemmas] are lemmas added to the default DB for this call (lemma
   sets are add-only -- the head filter restricts which rules apply). *)
type psimplify_hint = {
  ph_select : symbol list;
  ph_dbs    : (bool * symbol) list;
  ph_hd     : ([`Include | `Exclude] * pqsymbol list) option;
  ph_lemmas : pqsymbol list;
}

let empty_simplify_hint = {
  ph_select = []; ph_dbs = []; ph_hd = None; ph_lemmas = [];
}

(* -------------------------------------------------------------------- *)
type preduction = {
  pbeta    : bool;                      (* β-reduction *)
  pdelta   : pqsymbol list option;      (* definition unfolding *)
  pzeta    : bool;                      (* let-reduction *)
  piota    : bool;                      (* case/if-reduction *)
  peta     : bool;                      (* η-reduction *)
  plogic   : bool;                      (* logical simplification *)
  pmodpath : bool;                      (* modpath normalization *)
  puser    : bool;                      (* user reduction *)
  phint    : psimplify_hint;            (* use-site [hint …] clause *)
}

(* -------------------------------------------------------------------- *)
type pswap_kind = {
  interval : pcodepos_or_range option;
  offset   : pcodegap_offset1;
}

type interleave_info = oside * (int * int) * ((int * int) list) * int

type pspattern = unit

type pipattern =
  | PtAny
  | PtAsgn  of psymbol list
  | PtIf    of pspattern * [`NoElse | `MaybeElse | `Else of pspattern]
  | PtWhile of pspattern

type fun_upto_info = {
  fui_is_ll_variant : bool option;
  fui_bad : pformula;
  fui_pre : pformula;
  fui_pos : pformula option;
}

type call_info =
  | CI_spec of (pformula * phoare_post)
  | CI_inv of pformula
  | CI_upto of fun_upto_info

type p_seq_xt_info =
  | PSeqNone
  | PSeqSingle of pformula
  | PSeqMult   of (pformula option) tuple5

type ('a, 'b, 'c) rnd_tac_info =
  | PNoRndParams
  | PSingleRndParam of 'c
  | PTwoRndParams   of 'a * 'a
  | PMultRndParams  of ('a tuple5) * 'b

type rnd_tac_info_f =
  (pformula, pformula option, pformula) rnd_tac_info

type psemrndpos = (bool * pcodegap1) doption

type pfel_spec_preds = (pgamepath * pformula) list

(* -------------------------------------------------------------------- *)
type pim_repeat_kind =
  | IM_R_Repeat of int option pair
  | IM_R_May    of int option

type pim_repeat =
  bool * pim_repeat_kind

type anchor =
  | Without_anchor
  | With_anchor

type pim_regexp =
  | IM_Any
  | IM_Parens of pim_regexp
  | IM_Assign
  | IM_Sample
  | IM_Call
  | IM_If     of pim_block option * pim_block option
  | IM_While  of pim_block option
  | IM_Named  of psymbol * pim_regexp option
  | IM_Repeat of pim_repeat * pim_regexp
  | IM_Seq    of pim_regexp list
  | IM_Choice of pim_regexp list

and pim_block = anchor pair * pim_regexp

(* -------------------------------------------------------------------- *)
type trans_kind =
  | TKfun        of pgamepath
  | TKstmt       of side * pstmt
  | TKparsedStmt of side * pim_block * pstmt

type trans_formula =
  | TFform of pformula * pformula * pformula * pformula
  | TFeq

type trans_info =
  trans_kind * trans_formula

(* -------------------------------------------------------------------- *)
type bdh_split =
  | BDH_split_bop     of pformula * pformula * pformula option
  | BDH_split_or_case of pformula * pformula * pformula
  | BDH_split_not     of pformula option * pformula

(* -------------------------------------------------------------------- *)
type fun_info = [
  | `Def
  | `Code
  | `Abs  of pformula
  | `Upto of fun_upto_info
]

(* -------------------------------------------------------------------- *)
type seq_info =
  oside * pcodegap1 doption * pformula doption * p_seq_xt_info

(* -------------------------------------------------------------------- *)
type pcond_info = [
  | `Head   of oside
  | `Seq    of oside * pcodegap1 option pair * pformula
  | `SeqOne of  side * pcodegap1 option * pformula * pformula
]

(* -------------------------------------------------------------------- *)
type while_info = {
  wh_inv  : pformula;
  wh_vrnt : pformula option;
  wh_bds  : [`Bd of pformula pair] option;
}

(* -------------------------------------------------------------------- *)
type async_while_info = {
  asw_test : (pexpr * pformula) pair;
  asw_pred : pformula * pformula;
  asw_inv  : pformula;
}

(* -------------------------------------------------------------------- *)
type inlineopt = [`UseTuple of bool] option

type inline_pat1 = [
  | `InlineXpath of pgamepath
  | `InlinePat of pmsymbol located * (psymbol list * psymbol option)
  | `InlineAll
]


type inline_pat = ([ `DIFF | `UNION] * inline_pat1) list

type inline_info = [
  | `ByName    of oside * inlineopt * (inline_pat * int list option)
  | `CodePos   of (oside * inlineopt * pcodepos)
 (* | `All       of oside * inlineopt *)
]

(* -------------------------------------------------------------------- *)
type outline_kind =
  | OKstmt of pstmt
  | OKproc of pgamepath * bool

type outline_info = {
    outline_side: side;
    outline_range: pcodepos_or_range;
    outline_kind: outline_kind;
}

(* -------------------------------------------------------------------- *)
type fel_info = {
  pfel_cntr  : pformula;
  pfel_asg   : pformula;
  pfel_q     : pformula;
  pfel_event : pformula;
  pfel_specs : pfel_spec_preds;
  pfel_inv   : pformula option;
}

(* -------------------------------------------------------------------- *)
type deno_ppterm = (pformula option pair) gppterm

type conseq_info =
  | CQI_bd of phoarecmp option * pformula

type conseq_contra =
  pformula option * pformula option * phoare_exception option

type conseq_ppterm = (conseq_contra * (conseq_info) option) gppterm

(* -------------------------------------------------------------------- *)
type psim_info = {
  psim_pos  : pcodegap1 pair option;
  psim_hint : (pgamepath option pair * pformula) list * pformula option;
  psim_eqs  : pformula option
}

(* -------------------------------------------------------------------- *)
type rw_eqv_info = {
  rw_eqv_side  : side;
  rw_eqv_dir   : [`LtoR | `RtoL];
  rw_eqv_pos   : pcodepos1;
  rw_eqv_lemma : ppterm;
  rw_eqv_proc  : (pexpr list located * pexpr option) option;
}

(* -------------------------------------------------------------------- *)
type pcqoption  = [ `Frame ]
type pcqoptions = (bool * pcqoption) list

(* -------------------------------------------------------------------- *)
type crushmode = { cm_simplify : bool; cm_solve : bool; }

(* -------------------------------------------------------------------- *)
type matchmode = [
  | `DSided of [ `Eq | `ConstrSynced ]
  | `SSided of side
]

(* -------------------------------------------------------------------- *)
type bdepvar = [`Var of psymbol | `VarRange of psymbol * int | `Slice of psymbol * (pqsymbol * zint)]

type bdep_info =
  { n     : int
  ; m     : int
  ; invs  : bdepvar list
  ; inpvs : bdepvar list
  ; outvs : bdepvar list
  ; pcond : psymbol
  ; lane  : psymbol
  ; perm  : psymbol option 
  ; debug : bool }

type bdep_eval_info =
  { in_ty     : pty
  ; out_ty    : pty
  ; invs  : bdepvar list
  ; inpvs : bdepvar list
  ; outvs : bdepvar list
  ; lane  : psymbol 
  ; range : pformula 
  ; sign  : bool }

type bdepeq_info =
  { n          : int
  ; inpvs_l    : bdepvar list
  ; inpvs_r    : bdepvar list
  ; out_blocks : (int * bdepvar list * bdepvar list) list
  ; pcond      : psymbol option 
  ; preprocess : bool }

(* -------------------------------------------------------------------- *)
type prrewrite = [`Rw of ppterm | `Simpl]

(* -------------------------------------------------------------------- *)
type pecall = pqsymbol * ptyannot option * ppt_arg located list

(* -------------------------------------------------------------------- *)
type pdirection = [`Forward | `Backward]

(* -------------------------------------------------------------------- *)
type phltactic =
  | Pskip
  | Prepl_stmt     of trans_info
  | Pfun           of fun_info
  | Pseq           of seq_info
  | Pwp            of pdocodegap1
  | Psp            of pdocodegap1
  | Pwhile         of (oside * while_info)
  | Pasyncwhile    of async_while_info
  | Pfission       of (oside * pcodepos * (int * (int * int)))
  | Pfusion        of (oside * pcodepos * (int * (int * int)))
  | Punroll        of (oside * pcodepos * [`While | `For of bool])
  | Psplitwhile    of (pexpr * oside * pcodepos)
  | Pcall          of (oside * call_info gppterm)
  | Pcallconcave   of (pformula * call_info gppterm)
  | Prcond         of (oside * bool * pcodepos1)
  | Prmatch        of (oside * symbol * pcodepos1)
  | Pcond          of pcond_info
  | Pmatch         of matchmode
  | Pswap          of ((oside * pswap_kind) located list)
  | Pcfold         of pcfold
  | Pinline        of inline_info
  | Poutline       of outline_info
  | Pinterleave    of interleave_info located
  | Pkill          of (oside * pcodepos * int option)
  | PsimplifyIf    of (oside * pcodepos option)
  | Pasgncase      of (oside * pcodepos)
  | Prnd           of oside * psemrndpos option * rnd_tac_info_f
  | Prndsem        of bool * oside * pcodegap1
  | Palias         of (oside * pcodepos * osymbol_r)
  | Pweakmem       of (oside * psymbol * fun_params)
  | Pset           of (oside * pcodepos * bool * psymbol * pexpr)
  | Psetmatch      of (oside * pcodepos * psymbol * pformula)
  | Pconseq        of (pcqoptions * (conseq_ppterm option tuple3))
  | Pconseqauto    of crushmode
  | Pconcave       of (pformula option tuple2 gppterm * pformula)
  | Phrex_elim
  | Phrex_intro    of (pformula list * bool)
  | Phecall        of (pdirection * oside * pecall)
  | Pexfalso
  | Pbydeno        of ([`PHoare | `Equiv | `EHoare ] * (deno_ppterm * bool * pformula option))
  | PPr            of (pformula * pformula) option
  | Pbyupto
  | Pfel           of (pcodegap1 * fel_info)
  | Phoare
  | Pprbounded
  | Psim           of crushmode option* psim_info
  | Ptrans_stmt    of trans_info
  | Prw_equiv      of rw_eqv_info
  | Psymmetry
  | Pbdhoare_split of bdh_split
  | Pprocrewrite   of side option * pcodepos * prrewrite
  | Pprocrewriteat of psymbol * ppterm
  | Pchangestmt    of side option * ptybindings option * prange1_or_insert * pstmt
  | Phoaresplit

    (* Eager *)
  | Peager_seq       of (pcodegap1 pair * pstmt * pformula doption)
  | Peager_if
  | Peager_while     of pformula
  | Peager_fun_def
  | Peager_fun_abs   of pformula
  | Peager_call      of call_info gppterm

    (* Relation between logic *)
  | Pbd_equiv of (side * pformula * pformula)

    (* Automation *)
  | Pauto
  | Plossless

    (* Map-reduce *)
  | Pcircuit of circuit_mode

    (* Program rewriting *)
  | Prwprgm of rwprgm

and rwprgm = [
  | `IdAssign of pcodepos * pqsymbol
  | `Change   of pcodepos * ptybindings option * int * pstmt
]

and circuit_mode = [
  | `Simplify
  | `Solve
]

and pcfold =
  { side   : oside
  ; start  : pcodepos
  ; length : int option
  ; eager : bool }

(* -------------------------------------------------------------------- *)
type include_exclude = [ `Include | `Exclude ]
type pdbmap1 = {
  pht_flag : include_exclude;
  pht_kind : [ `Theory  | `Lemma   ];
  pht_name : pqsymbol;
}

and pdbhint = pdbmap1 list

(* -------------------------------------------------------------------- *)
type pprover_list = {
  pp_use_only : string located list;
  pp_add_rm   : (include_exclude * string located) list;
}

let empty_pprover_list = {
  pp_use_only = [];
  pp_add_rm   = [];
}

type pprover_infos = {
  pprov_max       : int option;
  pprov_timeout   : int option;
  pprov_cpufactor : int option;
  pprov_names     : pprover_list option;
  pprov_quorum    : int option;
  pprov_verbose   : int option option;
  pprov_version   : [`Lazy | `Full] option;
  plem_all        : bool option;
  plem_max        : int option option;
  plem_wanted     : pdbhint option;
  plem_unwanted   : pdbhint option;
  plem_dumpin     : string located option;
  plem_selected   : bool option;
  psmt_debug      : bool option;
}

let empty_pprover = {
  pprov_max       = None;
  pprov_timeout   = None;
  pprov_cpufactor = None;
  pprov_names     = None;
  pprov_quorum    = None;
  pprov_verbose   = None;
  pprov_version   = None;
  plem_all        = None;
  plem_max        = None;
  plem_wanted     = None;
  plem_unwanted   = None;
  plem_dumpin     = None;
  plem_selected   = None;
  psmt_debug      = None;
}

(* -------------------------------------------------------------------- *)
type trepeat = [`All | `Maybe] * int option
type tfocus1 = (int option) pair
type tfocus  = (tfocus1 list option) pair

type rwarg = (tfocus located) option * rwarg1 located

and rwarg1 =
  | RWSimpl  of [`Default | `Variant]
  | RWDelta  of (bool * rwoptions * pformula)
  | RWRw     of (rwoptions * (rwside * ppterm) list)
  | RWPr     of (psymbol * pformula option)
  | RWDone   of [`Default | `Variant] option
  | RWSmt    of (bool * pprover_infos)
  | RWApp    of ppterm
  | RWTactic of rwtactic

and rwmatch =
  | RWM_Plain   of pformula
  | RWM_Context of psymbol * pformula

and rwside    = [`LtoR | `RtoL]
and rwocc     = rwocci option
and rwocci    = [`Inclusive of Sint.t | `Exclusive of Sint.t | `All]
and rwtactic  = [`Ring | `Field]

and rwoptions =
  { side       : rwside
  ; repeat     : trepeat option
  ; occurrence : rwocc
  ; match_     : rwmatch option }

(* -------------------------------------------------------------------- *)
let norm_rwocci (x : rwocci) =
  match x with
  | `Inclusive x -> Some (`Inclusive, x)
  | `Exclusive x -> Some (`Exclusive, x)
  | `All         -> None

let norm_rwocc (x : rwocc) =
  obind norm_rwocci x

(* -------------------------------------------------------------------- *)
type intropattern1 =
  | IPCore   of ipcore
  | IPDup
  | IPCase     of (icasemode * intropattern list)
  | IPView     of ppterm
  | IPRw       of (rwocc * rwside * (int option) option)
  | IPDelta    of ((rwside * rwocc) * pformula)
  | IPSubst    of (rwside * (int option) option)
  | IPClear    of psymbol list
  | IPDone     of [`Default | `Variant] option
  | IPSmt      of (bool * pprover_infos)
  | IPSubstTop of (int option * [`LtoR | `RtoL] option)
  | IPSimplify of [`Default | `Variant]
  | IPCrush    of crushmode
  | IPBreak

and intropattern = (intropattern1 located) list

and ipcore = [
  | `Revert
  | `Clear
  | `Named     of string
  | `Anonymous of (int option) option
]

and icasemode =
  [`One | `Full of (bool * bool) * bool * icasemode_full option]

and icasemode_full =
  [`AtMost of int | `AsMuch]

type genpattern =
  [ `ProofTerm of ppterm
  | `Form of (rwocc * pformula)
  | `LetIn of psymbol ]

type prevert = {
  pr_clear : psymbol list;
  pr_genp  : genpattern list;
}

type prevertv = {
  pr_rev  : prevert;
  pr_view : ppterm list;
}

let prevert0  = { pr_clear = []; pr_genp = []; }
let prevertv0 = { pr_rev = prevert0; pr_view = []; }

(* -------------------------------------------------------------------- *)
type ppgoption = [
  | `Delta of [`Case | `Split] option
  | `Split
  | `Solve
  | `Subst
  | `Disjunctive
]

type ppgoptions = (bool * ppgoption) list

(* -------------------------------------------------------------------- *)
type pcaseoption  = [ `Ambient ]
type pcaseoptions = (bool * pcaseoption) list

(* -------------------------------------------------------------------- *)
type apply_info = [
  | `ApplyIn of ppterm * psymbol
  | `Apply   of ppterm list * [`Apply|`Exact|`Alpha]
  | `Top     of [`Apply|`Exact|`Alpha]
  | `Alpha   of ppterm
]

(* -------------------------------------------------------------------- *)
type clear_info = [
  | `Exclude of psymbol list
  | `Include of psymbol list
]

(* -------------------------------------------------------------------- *)
type pgenhave = psymbol * intropattern option * psymbol list * pformula

(* -------------------------------------------------------------------- *)
type pcongr_mode =
  | PCongrDefault
  | PCongrStar
  | PCongrPattern of pformula

(* -------------------------------------------------------------------- *)
type phintdbmode = [ `Add | `Remove ]

(* A proof-local simplify-hint command. [PLHClause] applies a unified
   [hint] clause: signed [+d]/[-d] activate/deactivate databases, signed
   lemma sets [+{L}]/[-{L}] add/remove local lemmas (default DB), an
   unsigned database list sets the proof-local default databases, and a
   [+[ops]]/[-[ops]] filter sets the proof-local default head filter.
   [PLHClear] / [PLHClearDefault] reset the local lemmas / the defaults. *)
type plocalhint =
  | PLHClause of psimplify_hint
  | PLHClear of symbol option
  | PLHClearDefault

(* -------------------------------------------------------------------- *)
type logtactic =
  | Preflexivity
  | Passumption
  | Psmt        of pprover_infos
  | Psplit      of [ `Default of int option | `All of [ `Maybe | `One ] ]
  | Pfield      of psymbol option * psymbol list
  | Pring       of psymbol option * psymbol list
  | Palg_norm
  | Pexists     of ppt_arg located list
  | Pleft
  | Pright
  | Ptrivial
  | Pcongr      of pcongr_mode
  | Pelim       of (prevert * pqsymbol option)
  | Papply      of (apply_info * prevert option)
  | Pcut        of pcut
  | Pcutdef     of (intropattern * pcutdef)
  | Pmove       of prevertv
  | Pclear      of clear_info
  | Prewrite    of (rwarg list * osymbol_r)
  | Prwnormal   of pformula * pqsymbol list
  | Psubst      of pformula list
  | Psimplify   of preduction
  | Pcbv        of preduction
  | Pchange     of pformula
  | Ppose       of (psymbol * ptybinding list * rwocc * pformula)
  | Pmemory     of psymbol
  | Pgenhave    of pgenhave
  | Pwlog       of (psymbol list * bool * pformula)
  | Pcoq        of (EcProvers.coq_mode option * psymbol * pprover_infos)
  | PlocalHint  of plocalhint

(* -------------------------------------------------------------------- *)
and ptactic_core_r =
  | Pidtac      of string option
  | Pdo         of trepeat * ptactic_core
  | Ptry        of ptactic_core
  | Pby         of (ptactics) option
  | Psolve      of (int option * psymbol list option)
  | Por         of ptactic * ptactic
  | Pseq        of ptactics
  | Pcase       of (bool * pcaseoptions * prevertv)
  | Pextens     of (ptactic_core * psymbol option)
  | Plogic      of logtactic
  | PPhl        of phltactic
  | Pprogress   of ppgoptions * ptactic_core option
  | Psubgoal    of ptactic_chain
  | Pnstrict    of ptactic_core
  | Pwith       of plocalhint * ptactics
  | Padmit

(* -------------------------------------------------------------------- *)
and ptactic_core = ptactic_core_r located
and ptactics     = ptactic list

(* -------------------------------------------------------------------- *)
and ptactic = {
  pt_core   : ptactic_core;
  pt_intros : introgenpattern list;
}

(* ---------------------`----------------------------------------------- *)
and introgenpattern = [`Ip of intropattern | `Gen of prevert]

(* -------------------------------------------------------------------- *)
and pexpect  = [
  | `None
  | `Tactic of ptactic
  | `Chain  of ptactic_chain list located
]

(* -------------------------------------------------------------------- *)
and ptactic_chain =
  | Psubtacs  of ptactics
  | Pfsubtacs of (tfocus * ptactic) list * ptactic option
  | Pfirst    of ptactic * int
  | Plast     of ptactic * int
  | Pexpect   of pexpect * int
  | Pfocus    of ptactic * tfocus
  | Protate   of [`Left | `Right] * int

(* -------------------------------------------------------------------- *)
and pcut =
  [`Have | `Suff] * intropattern * pformula * ptactics located option

(* -------------------------------------------------------------------- *)
type paxiom_kind =
| PAxiom of psymbol list
| PLemma of ptactics option option

type mempred_binding = PT_MemPred of psymbol list

type paxiom = {
  pa_name     : psymbol;
  pa_pvars    : mempred_binding option;
  pa_tyvars   : ptyparams option;
  pa_vars     : pgtybindings option;
  pa_formula  : pformula;
  pa_kind     : paxiom_kind;
  pa_locality : locality;
}

(* -------------------------------------------------------------------- *)
type prealize = {
  pr_name  : pqsymbol;
  pr_proof : (ptactics option) option;
}

(* -------------------------------------------------------------------- *)
type ptycinstance = {
  pti_name : pqsymbol;
  pti_as   : psymbol option;
  pti_type : ptyparams * pty;
  pti_ops  : (psymbol * (pty list * pqsymbol)) list;
  pti_axs  : (psymbol * ptactic_core) list;
  pti_args : [`Ring of (zint option * zint option)] option;
  pti_loca : is_local;
}

(* -------------------------------------------------------------------- *)
type ident_spec = psymbol list

(* -------------------------------------------------------------------- *)
type ('inv, 's) gphelper =
  | Helper_inv   of 'inv
  | Helper_eager of 's

type ('p, 'bad) gpinv =
  | Inv_global of 'p
  | Inv_upto   of 'bad

type pinv = (pformula, (pformula * pformula) * pformula option) gpinv

type equiv_concl =
  | Aequiv_spec of (pformula * pformula) * (pexpr * pexpr) option
  | Aequiv_inv  of pinv

type auto_info = pinv option * ident_spec

type auto_eager = (auto_info, pstmt) gphelper

type equiv = {
  eq_name  : psymbol          ;
  eq_left  : pqsymbol         ;
  eq_right : pqsymbol         ;
  eq_concl : equiv_concl      ;
  eq_auto  : auto_eager option;
}

(* -------------------------------------------------------------------- *)
type cnst_decl = (psymbol list * pty) * pexpr option

(* -------------------------------------------------------------------- *)
type pprint =
  | Pr_any  of pqsymbol
  | Pr_ty   of pqsymbol
  | Pr_op   of pqsymbol
  | Pr_th   of pqsymbol
  | Pr_pr   of pqsymbol
  | Pr_ax   of pqsymbol
  | Pr_mod  of pqsymbol
  | Pr_proc of pqsymbol
  | Pr_mty  of pqsymbol
  | Pr_glob of pmsymbol located
  | Pr_goal of int
  | Pr_db   of [`Rewrite of pqsymbol | `Solve of psymbol]
  | Pr_axioms
  | Pr_hint of [`Simplify | `Rewrite | `Solve] option

(* -------------------------------------------------------------------- *)
type renaming_kind =
  | RNty
  | RNop
  | RNpr

type w3_renaming =
    string list * renaming_kind * string

(* -------------------------------------------------------------------- *)
type theory_cloning = {
  pthc_base   : pqsymbol;
  pthc_name   : osymbol_r;
  pthc_ext    : (pqsymbol * theory_override) list;
  pthc_prf    : theory_cloning_proof list;
  pthc_rnm    : theory_renaming list;
  pthc_opts   : theory_cloning_options;
  pthc_clears : theory_cloning_clear list;
  pthc_local  : is_local option;
  pthc_import : [`Export | `Import | `Include] option;
}

and theory_renaming_kind =
  [ `Lemma | `Op | `Pred | `Exn | `Type | `Module | `ModType | `Theory ]

and theory_renaming =
  (theory_renaming_kind list * string located pair)

and theory_cloning_clear =
  ([`Abbrev] * pqsymbol)

and theory_cloning_option =
  [ `Abstract ]

and theory_cloning_options =
  (bool * theory_cloning_option) list

and theory_cloning_proof = {
  pthp_mode   : [
    | `All   of (pqsymbol option * theory_cloning_proof_tag list)
    | `Named of pqsymbol * clmode
  ];
  pthp_tactic : ptactic_core option;
}

and theory_cloning_proof_tag =
  [`Include | `Exclude] * psymbol

and theory_override =
| PTHO_Type   of ty_override
| PTHO_Op     of op_override
| PTHO_Pred   of pr_override
| PTHO_Axiom  of ax_override
| PTHO_ModTyp of mt_override
| PTHO_Theory of th_override

and ty_override = ty_override_def genoverride * clmode
and op_override = op_override_def genoverride * clmode
and pr_override = pr_override_def genoverride * clmode
and me_override = pqsymbol * clmode
and mt_override = pqsymbol * clmode
and th_override = pqsymbol * clmode * theory_renaming list
and ax_override = pqsymbol * clmode
and nt_override = EcPath.path * clmode

and clmode = [`Alias | `Inline of [`Keep | `Clear]]

and 'a genoverride = [
| `ByPath   of EcPath.path
| `BySyntax of 'a
]

and ty_override_def = psymbol list * pty

and op_override_def = {
  opov_tyvars : psymbol list option;
  opov_args   : ptybinding list;
  opov_retty  : pty;
  opov_body   : pformula;
}

and pr_override_def = {
  prov_tyvars : psymbol list option;
  prov_args   : ptybinding list;
  prov_body   : pformula;
}

(* -------------------------------------------------------------------- *)
type proofmode = {
  pm_strict : bool;
}

(* -------------------------------------------------------------------- *)
type tcdump = {
  tcd_source : string * (int * int);
  tcd_width  : int option;
  tcd_output : string;
}

(* -------------------------------------------------------------------- *)
type save = [ `Qed | `Admit | `Abort ]

(* -------------------------------------------------------------------- *)
type theory_clear = (pqsymbol option) list

(* -------------------------------------------------------------------- *)
type phintoption = [ `Rigid ]

(* -------------------------------------------------------------------- *)
type phint = {
  ht_local   : is_local;
  ht_prio    : int;
  ht_base    : psymbol option;
  ht_names   : pqsymbol list;
  ht_options : phintoption list;
}

(* -------------------------------------------------------------------- *)
type puseroption =
  [`Delta | `EqTrue]

type puserred =
  symbol option * puseroption list * (pqsymbol list * int option) list

type threquire =
  psymbol option * (psymbol * psymbol option) list * [`Import|`Export] option

(* -------------------------------------------------------------------- *)
type pbind_bitstring =
  { from_  : pqsymbol
  ; to_    : pqsymbol
  ; touint : pqsymbol
  ; tosint : pqsymbol
  ; ofint  : pqsymbol
  ; type_  : pqsymbol
  ; size   : pformula }
  
(* -------------------------------------------------------------------- *)
type pbind_array =
  { get    : pqsymbol
  ; set    : pqsymbol
  ; tolist : pqsymbol
  ; oflist : pqsymbol
  ; type_  : pqsymbol
  ; size   : pformula }

(* -------------------------------------------------------------------- *)
type pbind_bvoperator =
  { name     : string located
  ; types    : pqsymbol list
  ; operator : pqsymbol }

(* -------------------------------------------------------------------- *)
type pbind_circuit =
  { bindings : (pqsymbol * string located) list 
  ; file     : string located }

(* -------------------------------------------------------------------- *)
type pcrbinding_r =
  | CRB_Bitstring  of pbind_bitstring
  | CRB_Array      of pbind_array
  | CRB_BvOperator of pbind_bvoperator
  | CRB_Circuit    of pbind_circuit

(* -------------------------------------------------------------------- *)
type pcrbinding = { locality : is_local; binding : pcrbinding_r }

(* -------------------------------------------------------------------- *)
type global_action =
  | Gmodule      of pmodule_def_or_decl
  | Ginterface   of pinterface
  | Goperator    of poperator
  | Gexception   of pexception_decl
  | Gprocop      of pprocop
  | Gpredicate   of ppredicate
  | Gnotation    of pnotation
  | Gabbrev      of pabbrev
  | Gaxiom       of paxiom
  | Gtype        of ptydecl list
  | Gsubtype     of psubtype
  | Gtycinstance of ptycinstance
  | Gaddrw       of (is_local * pqsymbol * pqsymbol list)
  | Greduction   of puserred
  | Ghint        of phint
  | Gprint       of pprint
  | Gexpect      of (string located * pprint)
  | Gsearch      of pformula list
  | Glocate      of pqsymbol
  | GthOpen      of (is_local * bool * psymbol)
  | GthClose     of (theory_clear * psymbol)
  | GthClear     of theory_clear
  | GthRequire   of threquire
  | GthImport    of pqsymbol list
  | GthExport    of pqsymbol list
  | GthClone     of theory_cloning
  | GthAlias     of (psymbol * pqsymbol list)
  | GModImport   of pmsymbol located list
  | GsctOpen     of osymbol_r
  | GsctClose    of osymbol_r
  | Grealize     of prealize located
  | Gtactics     of [`Proof | `Actual of bullet located option * ptactic list]
  | Gtcdump      of (tcdump * (bullet located option * ptactic list))
  | Gprover_info of pprover_infos
  | Gsave        of save located
  | Gpragma      of psymbol
  | Goption      of (psymbol * [`Bool of bool | `Int of int])
  | GdumpWhy3    of string
  | Gcrbinding   of pcrbinding

type global = {
  gl_action : global_action located;
  gl_fail   : bool;
  gl_expect : string located option;   (* [expect fail "…"]: expected error *)
  gl_debug  : [`Timed | `Break] option;
}

type prog_r =
  | P_Prog of global list * bool
  | P_Exit
  | P_Undo of int
  | P_DocComment of (dockind * string)

and dockind = [`Global | `Item]

type prog = prog_r located