swh:1:snp:9f9174fb54ac68d4510837c2f930cf0558bce5b6
Tip revision: 82cc4d7ad1ca93dc93773f50b053591da4d479b1 authored by Pierre-Yves Strub on 09 June 2020, 19:55:20 UTC
binomial law + basic lemmas (full / support)
binomial law + basic lemmas (full / support)
Tip revision: 82cc4d7
ecParsetree.ml
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2016 - IMDEA Software Institute
* Copyright (c) - 2012--2018 - Inria
* Copyright (c) - 2012--2018 - Ecole Polytechnique
*
* Distributed under the terms of the CeCILL-C-V1 license
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
open EcBigInt
open EcMaps
open EcSymbols
open EcLocation
open EcUtils
(* -------------------------------------------------------------------- *)
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
(* -------------------------------------------------------------------- *)
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 ptybinding = osymbol list * pty
and ptybindings = ptybinding list
and pexpr_r =
| PEcast of pexpr * pty (* type cast *)
| PEint of zint (* int. literal *)
| PEdecimal of (zint * (int * zint)) (* dec. literal *)
| PEident of pqsymbol * ptyannot option (* symbol *)
| PEapp of pexpr * pexpr list (* op. application *)
| PElet of plpattern * pexpr_wty * pexpr (* let binding *)
| PEtuple of pexpr list (* tuple constructor *)
| PEif of pexpr * pexpr * pexpr (* _ ? _ : _ *)
| PEforall of ptybindings * pexpr (* forall quant. *)
| PEexists of ptybindings * pexpr (* exists quant. *)
| PElambda of ptybindings * pexpr (* lambda abstraction *)
| PErecord of pexpr option * pexpr rfield list (* record *)
| PEproj of pexpr * pqsymbol (* projection *)
| PEproji of pexpr * int (* tuple projection *)
| PEscope of pqsymbol * pexpr (* scope selection *)
and pexpr = pexpr_r located
and pexpr_wty = pexpr * pty option
and 'a rfield = {
rf_name : pqsymbol;
rf_tvi : ptyannot option;
rf_value : 'a;
}
(* -------------------------------------------------------------------- *)
type plvalue_r =
| PLvSymbol of pqsymbol
| PLvTuple of pqsymbol list
| PLvMap of pqsymbol * ptyannot option * pexpr
and plvalue = plvalue_r located
type 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
| PSassert of pexpr
and pscond = pexpr * pstmt
and pinstr = pinstr_r located
and pstmt = pinstr list
(* -------------------------------------------------------------------- *)
type pmodule_type = pqsymbol
type pmodule_type_restr = pqsymbol * pmsymbol located list
type 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 include_proc = [
| `Include_proc of psymbol list
| `Exclude_proc of psymbol list
]
and pmodule_sig_item = [
| `Include of pmodule_type * include_proc option * pqsymbol list option
| `FunctionDecl of pfunction_decl
]
and pvariable_decl = {
pvd_name : psymbol;
pvd_type : pty;
}
and fun_params =
| Fparams_exp of (psymbol * pty) list
| Fparams_imp of pty
and pfunction_decl = {
pfd_name : psymbol;
pfd_tyargs : fun_params;
pfd_tyresult : pty;
pfd_uses : bool * pqsymbol list option;
}
(* -------------------------------------------------------------------- *)
and pmodule_def = {
ptm_header : pmodule_header;
ptm_body : pmodule_expr;
ptm_local : bool;
}
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
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_maliases of (pmsymbol located * include_proc option)
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 pmodule_decl = {
ptmd_name : psymbol;
ptmd_modty : pmodule_type_restr;
}
(* -------------------------------------------------------------------- *)
type ptyparams = (psymbol * pqsymbol list) list
type ptydname = (ptyparams * psymbol) located
type ptydecl = {
pty_name : psymbol;
pty_tyvars : ptyparams;
pty_body : ptydbody;
}
and ptydbody =
| PTYD_Abstract of pqsymbol list
| PTYD_Alias of pty
| PTYD_Record of precord
| PTYD_Datatype of pdatatype
and pdatatype = (psymbol * pty list) list
and precord = (psymbol * pty) list
(* -------------------------------------------------------------------- *)
type pmemory = psymbol
type phoarecmp = EcFol.hoarecmp
type glob_or_var =
| GVglob of pmsymbol located
| GVvar of pqsymbol
type pformula = pformula_r located
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 * symbol located
| PFapp of pformula * pformula list
| PFif of pformula * pformula * pformula
| 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 pformula * pgamepath * pformula
| PFequivF of pformula * (pgamepath * pgamepath) * pformula
| PFeagerF of pformula * (pstmt * pgamepath * pgamepath * pstmt) * pformula
| PFprob of pgamepath * (pformula list) * pmemory * pformula
| PFBDhoareF of pformula * pgamepath * pformula * phoarecmp * pformula
and pgtybinding = osymbol list * pgty
and pgtybindings = pgtybinding list
and pgty =
| PGTY_Type of pty
| PGTY_ModTy of pmodule_type_restr
| PGTY_Mem
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]
(* -------------------------------------------------------------------- *)
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
(* -------------------------------------------------------------------- *)
type ppattern =
| PPApp of (pqsymbol * ptyannot option) * osymbol list
type ptyvardecls =
(psymbol * pqsymbol list) list
type pop_def =
| PO_abstr of pty
| PO_concr of pty * pexpr
| 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;
po_def : pop_def;
po_ax : osymbol_r;
po_nosmt : bool;
}
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 * pqsymbol list) list option;
pp_def : ppred_def;
}
(* -------------------------------------------------------------------- *)
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;
}
(* -------------------------------------------------------------------- *)
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;
}
(* -------------------------------------------------------------------- *)
type pdeclare =
| PDCL_Module of pmodule_decl
(* -------------------------------------------------------------------- *)
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
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;
}
(* -------------------------------------------------------------------- *)
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 *)
}
(* -------------------------------------------------------------------- *)
type cp_match = [ `If | `While | `Assign | `Sample | `Call ]
type cp_base = [ `ByPos of int | `ByMatch of int option * cp_match ]
type codepos1 = int * cp_base
type codepos = (codepos1 * int) list * codepos1
(* -------------------------------------------------------------------- *)
type 'a doption =
| Single of 'a
| Double of ('a * 'a)
type swap_kind =
| SKbase of int * int * int
| SKmove of int
| SKmovei of int * int
| SKmoveinter of int * int * int
type interleave_info = oside * (int * int) * ((int * int) list) * int
type pipattern =
| PtAny
| PtAsgn of psymbol list
| PtIf of pspattern * [`NoElse | `MaybeElse | `Else of pspattern]
| PtWhile of pspattern
and pspattern = unit
type call_info =
| CI_spec of (pformula * pformula)
| CI_inv of pformula
| CI_upto of (pformula * pformula * pformula option)
type p_app_bd_info =
| PAppNone
| PAppSingle of pformula
| PAppMult 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 tac_dir = Backs | Fwds
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 eager_info =
| LE_done of psymbol
| LE_todo of psymbol * pstmt * pstmt * pformula * pformula
(* -------------------------------------------------------------------- *)
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 pformula * pformula * pformula option
]
(* -------------------------------------------------------------------- *)
type app_info =
oside * tac_dir * codepos1 doption * pformula doption * p_app_bd_info
(* -------------------------------------------------------------------- *)
type pcond_info = [
| `Head of oside
| `Seq of oside * codepos1 option pair * pformula
| `SeqOne of side * codepos1 option * pformula * pformula
]
(* -------------------------------------------------------------------- *)
type while_info = {
wh_inv : pformula;
wh_vrnt : pformula option;
wh_bds : 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_info = [
| `ByName of oside * inlineopt * (pgamepath list * int list option)
| `CodePos of (oside * inlineopt * codepos)
| `All of oside * inlineopt
]
(* -------------------------------------------------------------------- *)
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_ppterm = ((pformula option pair) * (phoarecmp option * pformula) option) gppterm
(* -------------------------------------------------------------------- *)
type sim_info = {
sim_pos : codepos1 pair option;
sim_hint : (pgamepath option pair * pformula) list * pformula option;
sim_eqs : pformula option
}
(* -------------------------------------------------------------------- *)
type pcqoption = [ `Frame ]
type pcqoptions = (bool * pcqoption) list
(* -------------------------------------------------------------------- *)
type crushmode = { cm_simplify : bool; cm_solve : bool; }
(* -------------------------------------------------------------------- *)
type phltactic =
| Pskip
| Prepl_stmt of trans_info
| Pfun of fun_info
| Papp of app_info
| Pwp of codepos1 doption option
| Psp of codepos1 doption option
| Pwhile of (oside * while_info)
| Pasyncwhile of async_while_info
| Pfission of (oside * codepos * (int * (int * int)))
| Pfusion of (oside * codepos * (int * (int * int)))
| Punroll of (oside * codepos * bool)
| Psplitwhile of (pexpr * oside * codepos)
| Pcall of oside * call_info gppterm
| Prcond of (oside * bool * codepos1)
| Pcond of pcond_info
| Pswap of ((oside * swap_kind) located list)
| Pcfold of (oside * codepos * int option)
| Pinline of inline_info
| Pinterleave of interleave_info located
| Pkill of (oside * codepos * int option)
| Prnd of oside * (pformula, pformula option, pformula) rnd_tac_info
| Palias of (oside * codepos * osymbol_r)
| Pset of (oside * codepos * bool * psymbol * pexpr)
| Pconseq of (pcqoptions * (conseq_ppterm option tuple3))
| Pconseqauto of crushmode
| Phrex_elim
| Phrex_intro of (pformula list * bool)
| Phecall of (oside * (pqsymbol * ptyannot option * pformula list))
| Pexfalso
| Pbydeno of ([`PHoare | `Equiv ] * (deno_ppterm * bool * pformula option))
| PPr of (pformula * pformula) option
| Pfel of (codepos1 * fel_info)
| Phoare
| Pprbounded
| Psim of crushmode option* sim_info
| Ptrans_stmt of trans_info
| Psymmetry
| Pbdhoare_split of bdh_split
(* Eager *)
| Peager_seq of (eager_info * codepos1 pair * pformula)
| Peager_if
| Peager_while of (eager_info)
| Peager_fun_def
| Peager_fun_abs of (eager_info * pformula)
| Peager_call of (call_info gppterm)
| Peager of (eager_info * pformula)
(* Relation between logic *)
| Pbd_equiv of (side * pformula * pformula)
(* Automation *)
| Pauto
| Plossless
(* -------------------------------------------------------------------- *)
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_iterate : bool option;
plem_wanted : pdbhint option;
plem_unwanted : pdbhint option;
plem_selected : 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_iterate = None;
plem_wanted = None;
plem_unwanted = None;
plem_selected = 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 (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 rwoptions = rwside * trepeat option * rwocc
and rwside = [`LtoR | `RtoL]
and rwocc = rwocci option
and rwocci = [`Inclusive of Sint.t | `Exclusive of Sint.t | `All]
and rwtactic = [`Ring | `Field]
(* -------------------------------------------------------------------- *)
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]
| `Top of [`Apply|`Exact]
]
(* -------------------------------------------------------------------- *)
type logtactic =
| Preflexivity
| Passumption
| Psmt of pprover_infos
| Psplit
| Pfield of psymbol list
| Pring of psymbol list
| Palg_norm
| Pexists of ppt_arg located list
| Pleft
| Pright
| Ptrivial
| Pcongr
| Pelim of (prevert * pqsymbol option)
| Papply of (apply_info * prevert option)
| Pcut of pcut
| Pcutdef of (intropattern * pcutdef)
| Pmove of prevertv
| Pclear of psymbol list
| 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)
| Pwlog of (psymbol list * pformula)
(* -------------------------------------------------------------------- *)
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)
| Plogic of logtactic
| PPhl of phltactic
| Pprogress of ppgoptions * ptactic_core option
| Psubgoal of ptactic_chain
| Pnstrict of ptactic_core
| Padmit
| Pdebug
(* -------------------------------------------------------------------- *)
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
| PILemma
type paxiom = {
pa_name : psymbol;
pa_tyvars : (psymbol * pqsymbol list) list option;
pa_vars : pgtybindings option;
pa_formula : pformula;
pa_kind : paxiom_kind;
pa_nosmt : bool;
pa_local : bool;
}
(* -------------------------------------------------------------------- *)
type prealize = {
pr_name : pqsymbol;
pr_proof : (ptactics option) option;
}
(* -------------------------------------------------------------------- *)
type ptypeclass = {
ptc_name : psymbol;
ptc_inth : pqsymbol option;
ptc_ops : (psymbol * pty) list;
ptc_axs : (psymbol * pformula) list;
}
type ptycinstance = {
pti_name : pqsymbol;
pti_type : (psymbol * pqsymbol list) list * pty;
pti_ops : (psymbol * (pty list * pqsymbol)) list;
pti_axs : (psymbol * ptactic_core) list;
pti_args : [`Ring of (zint option * zint option)] option;
}
(* -------------------------------------------------------------------- *)
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_mty of pqsymbol
| Pr_glob of pmsymbol located
| Pr_goal of int
| Pr_db of [`Rewrite of pqsymbol | `Solve of psymbol]
(* -------------------------------------------------------------------- *)
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 : bool;
pthc_import : [`Export | `Import | `Include] option;
}
and theory_renaming_kind =
[ `Lemma | `Op | `Pred | `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
];
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_Theory of th_override
and ty_override = psymbol list * pty * [`Alias | `Inline]
and op_override = op_override_def * [`Alias | `Inline]
and pr_override = pr_override_def * [`Alias | `Inline]
and th_override = pqsymbol
and op_override_def = {
opov_nosmt : bool;
opov_tyvars : psymbol list option;
opov_args : ptybinding list;
opov_retty : pty;
opov_body : pexpr;
}
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 phint = {
ht_local : bool;
ht_prio : int;
ht_base : psymbol option;
ht_names : pqsymbol list;
}
(* -------------------------------------------------------------------- *)
type puseroption =
[`Delta | `EqTrue]
type puserred =
puseroption list * (pqsymbol list * int option) list
type threquire =
psymbol option * (psymbol * psymbol option) list * [`Import|`Export] option
(* -------------------------------------------------------------------- *)
type global_action =
| Gdeclare of pdeclare
| Gmodule of pmodule_def
| Ginterface of (psymbol * pmodule_sig)
| Goperator of poperator
| Gpredicate of ppredicate
| Gnotation of pnotation
| Gabbrev of pabbrev
| Gaxiom of paxiom
| Gtype of ptydecl list
| Gtypeclass of ptypeclass
| Gtycinstance of ptycinstance
| Gaddrw of (bool * pqsymbol * pqsymbol list)
| Greduction of puserred
| Ghint of phint
| Gprint of pprint
| Gsearch of pformula list
| GthOpen of (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
| GsctOpen of osymbol_r
| GsctClose of osymbol_r
| Grealize of prealize located
| Gtactics of [`Proof of proofmode | `Actual of ptactic list]
| Gtcdump of (tcdump * 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
type global = {
gl_action : global_action located;
gl_timed : bool;
}
type prog_r =
| P_Prog of global list * bool
| P_Undo of int
type prog = prog_r located