https://github.com/EasyCrypt/easycrypt
Tip revision: e56737bc84078420ab06efc7bb357fa1524cde46 authored by Pierre-Yves Strub on 08 April 2020, 13:58:49 UTC
matching for Pr
matching for Pr
Tip revision: e56737b
ecCoreGoal.mli
(* --------------------------------------------------------------------
* 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 EcUtils
open EcIdent
open EcSymbols
open EcTypes
open EcFol
open EcEnv
(* -------------------------------------------------------------------- *)
exception InvalidGoalShape
(* -------------------------------------------------------------------- *)
type clearerror = [
| `ClearInGoal of EcIdent.t list
| `ClearDep of EcIdent.t pair
]
exception ClearError of clearerror Lazy.t
(* -------------------------------------------------------------------- *)
(* Proof-node ID *)
(* -------------------------------------------------------------------- *)
type handle
val eq_handle : handle -> handle -> bool
(* -------------------------------------------------------------------- *)
(* EasyCrypt proof-term: *)
(* *)
(* pt ::= pt-head pt-arg* *)
(* *)
(* pt-head ::= *)
(* | form<ft> (cut <ft> - generate subgoal) *)
(* | handle (formula associated to <handle>) *)
(* | local<id> (local hypothesis <id>) *)
(* | global<p,tyargs> (global lemma <p<:tyargs>>) *)
(* *)
(* pt-arg ::= *)
(* | formula (∀-elimination) *)
(* | memory (∀[mem]-elimination) *)
(* | module-path (∀[mod]-elimination) *)
(* | pt (⇒-elimination) *)
(* -------------------------------------------------------------------- *)
type proofterm = { pt_head : pt_head; pt_args : pt_arg list; }
and pt_head =
| PTCut of EcFol.form
| PTHandle of handle
| PTLocal of EcIdent.t
| PTGlobal of EcPath.path * (ty list)
and pt_arg =
| PAFormula of EcFol.form
| PAMemory of EcMemory.memory
| PAModule of (EcPath.mpath * EcModules.module_sig)
| PASub of proofterm option
(* -------------------------------------------------------------------- *)
val is_ptcut : pt_head -> bool
val is_pthandle : pt_head -> bool
val is_ptlocal : pt_head -> bool
val is_ptglobal : pt_head -> bool
(* -------------------------------------------------------------------- *)
val is_paformula : pt_arg -> bool
val is_pamemory : pt_arg -> bool
val is_pamodule : pt_arg -> bool
val is_pasub : pt_arg -> bool
val paformula : EcFol.form -> pt_arg
val pamemory : EcMemory.memory -> pt_arg
val pamodule : EcPath.mpath * EcModules.module_sig -> pt_arg
val paglobal : EcPath.path -> ty list -> pt_arg
val palocal : EcIdent.t -> pt_arg
val pahandle : handle -> pt_arg
(* -------------------------------------------------------------------- *)
(* EasyCrypt rewrite proof-term: *)
(* rwpt := pt * position list * local hyp *)
(* <pt>: equality-proof term *)
(* *)
(* position := EcMatching.ptnpos - pattern position *)
(* -------------------------------------------------------------------- *)
type rwproofterm = {
rpt_proof : proofterm;
rpt_occrs : EcMatching.ptnpos option;
rpt_lc : ident option;
}
(* -------------------------------------------------------------------- *)
(* The type [proof] represents the state an interactive proof at top
* level, i.e. the set of goals (opened or closed) + the list of
* opened, top-level goals. It cannot be use for proof-progress. Instead,
* a [proofenv] or [tcenv] must be created (resp. for forward / backward
* reasoning) first.
*
* A [proofenv] represents the set of goals (opened or closed) of a given
* [proof]. An API is provided that allows the creation of new *closed*
* goals, i.e. for doing forward reasoning from existing (proven or not)
* facts.
*
* A [tcenv] represents the set of opened goals of a given [proof]. These
* goals are organized as a tree + a focus (i.e. a pointed leaf of the
* tree). An API is provided allowing reasoning in a mix of backward /
* forward reasoning, creating open of closed goals or solving the
* current focus. The [tcenv] handle the focus automatically when goals
* are created, closed or when composing tactics; but can also be
* manipulated explicitely via tacticals.
*
* A [tcenv1] is a [tcenv] where it is statically known that the focused
* goal has sibling goals. A coercion is given from [tcenv1] to [tcenv].
*)
type proof
type proofenv
type tcenv1
type tcenv
type pregoal = {
g_uid : handle;
g_hyps : LDecl.hyps;
g_concl : form;
}
type validation =
| VSmt (* SMT call *)
| VAdmit (* admit *)
| VIntros of (handle * ident option list) (* intros *)
| VConv of (handle * Sid.t) (* weakening + conversion *)
| VLConv of (handle * ident) (* hypothesis conversion *)
| VRewrite of (handle * rwproofterm) (* rewrite *)
| VApply of proofterm (* modus ponens *)
| VShuffle of ident list (* goal shuffling *)
(* external (hl/phl/prhl/...) proof-node *)
| VExtern : 'a * handle list -> validation
(* -------------------------------------------------------------------- *)
type location = {
plc_parent : location option;
plc_name : string option;
plc_loc : EcLocation.t;
}
type tcemsg =
| TCEUser : 'a * ('a -> string) -> tcemsg
| TCEExn : exn -> tcemsg
type tcerror = {
tc_catchable : bool;
tc_proofenv : proofenv option;
tc_location : location option;
tc_message : tcemsg;
tc_reloced : (symbol * bool) option;
}
exception TcError of tcerror
(* -------------------------------------------------------------------- *)
val tcenv1_of_proof : proof -> tcenv1
val tcenv_of_proof : proof -> tcenv
val proof_of_tcenv : tcenv -> proof
val proofenv_of_proof : proof -> proofenv
(* Start a new interactive proof in a given local context
* [LDecl.hyps] for given [form]. Mainly, a [proof] records the set
* of all goals (closed or not - i.e. a proof-environment) + the list
* of opened, top-level goals. *)
val start : LDecl.hyps -> form -> proof
(* Return the first opened goal of this interactive proof and the
* number of open goals. *)
val opened : proof -> (int * pregoal) option
(* Return the list of opened goals - by handle *)
val all_hd_opened : proof -> handle list
(* Return the list of opened goals - by pregoal *)
val all_opened : proof -> pregoal list
(* Check if a proof is done *)
val closed : proof -> bool
(* -------------------------------------------------------------------- *)
val tc_error :
proofenv -> ?catchable:bool -> ?loc:EcLocation.t -> ?who:string
-> ('a, Format.formatter, unit, 'b) format4 -> 'a
val tc_error_exn :
proofenv -> ?catchable:bool -> ?loc:EcLocation.t -> ?who:string
-> exn -> 'a
val tc_error_lazy :
proofenv -> ?catchable:bool -> ?loc:EcLocation.t -> ?who:string
-> (Format.formatter -> unit) -> 'a
(* -------------------------------------------------------------------- *)
val tacuerror :
?catchable:bool -> ('a, Format.formatter, unit, 'b) format4 -> 'a
val tacuerror_exn :
?catchable:bool -> exn -> 'a
(* -------------------------------------------------------------------- *)
type symkind = [`Lemma | `Operator | `Local]
val tc_lookup_error :
proofenv -> ?loc:EcLocation.t -> ?who:string -> symkind -> qsymbol -> 'a
(* -------------------------------------------------------------------- *)
val reloc : EcLocation.t -> ('a -> 'b) -> 'a -> 'b
(* -------------------------------------------------------------------- *)
(* Functional API *)
(* -------------------------------------------------------------------- *)
module FApi : sig
(* - [forward tactic]: take a proofenv, i.e. a set of goals (proven or
* not) and generate a new (1-level proven) goal [handle]. Examples
* of such tactics are forward congruence or closed rewriting.
*
* - [backward tactic]: take a tcenv, i.e. an opened goal, and make
* progress over it, potentially creating new subgoals. Examples of
* such tactics are backward apply, rewriting, backward congruence.
*)
exception InvalidStateException of string
type forward = proofenv -> proofenv * handle
type backward = tcenv1 -> tcenv
type ibackward = int -> backward
type tactical = tcenv -> tcenv
val tcenv_of_tcenv1 : tcenv1 -> tcenv
val as_tcenv1 : tcenv -> tcenv1
val get_pregoal_by_id : handle -> proofenv -> pregoal
val get_main_pregoal : proofenv -> pregoal
(* Create a new opened goal for the given [form] in the backward
* environment [tcenv]. If no local context [LDecl.hyps] is given,
* use the one of the focused goal in [tcenv] -- it is then an
* internal error is no goal is focused. By default, the goal is
* created as the last sibling of the current focus. Return the
* mutated [tcenv] along with the handle of the new goal. *)
val newgoal : tcenv -> ?hyps:LDecl.hyps -> form -> tcenv * handle
(* Mark the focused goal in [tcenv] as solved using the given
* [validation]. It is an internal error if no goal is focused. The
* focus is then changed to the next opened sibling. *)
val close : tcenv -> validation -> tcenv
(* Mutate current goal in [tcenv]. Focused goal will be marked as
* resolved using the given [validation] producer. This producer is
* applied to the goal freshly created, using given formulas and
* focused goal local context. *)
val mutate : tcenv -> (handle -> validation) -> ?hyps:LDecl.hyps -> form -> tcenv
val mutate1 : tcenv1 -> (handle -> validation) -> ?hyps:LDecl.hyps -> form -> tcenv1
(* Same as xmutate, but for an external node resolution depending on
* a unbounded numbers of premises. The ['a] argument is the external
* validation node. *)
val xmutate : tcenv -> 'a -> form list -> tcenv
val xmutate1 : tcenv1 -> 'a -> form list -> tcenv
val xmutate_hyps : tcenv -> 'a -> (LDecl.hyps * form) list -> tcenv
val xmutate1_hyps : tcenv1 -> 'a -> (LDecl.hyps * form) list -> tcenv
(* Apply a forward tactic to a backward environment, using the
* proof-environment of the latter *)
val bwd1_of_fwd : forward -> tcenv1 -> tcenv1 * handle
val bwd_of_fwd : forward -> tcenv -> tcenv * handle
(* Insert a new fact in a proof-environment *)
val newfact :
proofenv -> validation -> LDecl.hyps -> form
-> proofenv * handle
(* Check if a tcenv is closed (no focused goal *)
val tc_done : tcenv -> bool
val tc_count : tcenv -> int
val tc_opened : tcenv -> handle list
(* Accessors for focused goal parts (tcenv) *)
val tc_handle : tcenv -> handle
val tc_penv : tcenv -> proofenv
val tc_goal : tcenv -> form
val tc_env : tcenv -> EcEnv.env
val tc_flat : ?target:ident -> tcenv -> LDecl.hyps * form
val tc_eflat : ?target:ident -> tcenv -> env * LDecl.hyps * form
val tc_hyps : ?target:ident -> tcenv -> LDecl.hyps
(* Accessors for focused goal parts (tcenv1) *)
val tc1_handle : tcenv1 -> handle
val tc1_penv : tcenv1 -> proofenv
val tc1_flat : ?target:ident -> tcenv1 -> LDecl.hyps * form
val tc1_eflat : ?target:ident -> tcenv1 -> env * LDecl.hyps * form
val tc1_hyps : ?target:ident -> tcenv1 -> LDecl.hyps
val tc1_goal : tcenv1 -> form
val tc1_env : tcenv1 -> EcEnv.env
(* Low-level tactic markers *)
val t_low0 : string -> backward -> backward
val t_low1 : string -> ('a -> backward) -> 'a -> backward
val t_low2 : string -> ('a -> 'b -> backward) -> ('a -> 'b -> backward)
val t_low3 : string -> ('a -> 'b -> 'c -> backward) -> ('a -> 'b -> 'c -> backward)
val t_low4 : string -> ('a -> 'b -> 'c -> 'd -> backward) -> ('a -> 'b -> 'c -> 'd -> backward)
(* Tacticals *)
type direction = [ `Left | `Right ]
type tfocus = (int -> bool)
val t_focus : backward -> tactical
val t_map : (tcenv1 -> 'a * tcenv) -> tcenv -> 'a list * tcenv
val t_onalli : (int -> backward) -> tactical
val t_onall : backward -> tactical
val t_onfsub : (int -> backward option) -> tactical
val t_onselecti : tfocus -> ?ttout:ibackward -> ibackward -> tactical
val t_onselect : tfocus -> ?ttout:backward -> backward -> tactical
val t_on1 : int -> ?ttout:backward -> backward -> tactical
val t_firsts : backward -> int -> tactical
val t_lasts : backward -> int -> tactical
val t_subfirsts : backward list -> tactical
val t_sublasts : backward list -> tactical
val t_first : backward -> tactical
val t_last : backward -> tactical
val t_rotate : direction -> int -> tactical
val t_swap_goals : int -> int -> tactical
val t_sub : backward list -> tactical
val t_submap : (tcenv1 -> 'a * tcenv) list -> tcenv -> 'a list * tcenv
val t_seq : backward -> backward -> backward
val t_seqs : backward list -> backward
val t_seqsub : backward -> backward list -> backward
val t_on1seq : int -> backward -> ?ttout:backward -> backward -> backward
val t_try_base : backward -> tcenv1 -> [`Failure of exn | `Success of tcenv]
val t_try : backward -> backward
val t_xswitch: ?on:[`All|`Focus] -> (tcenv1 -> tcenv * backward) -> iffail:backward -> backward
val t_switch : ?on:[`All|`Focus] -> backward -> ifok:backward -> iffail:backward -> backward
val t_do_r : ?focus:int -> [`All | `Maybe] -> int option -> backward -> tcenv -> tcenv
val t_do : [`All | `Maybe] -> int option -> backward -> backward
val t_repeat : backward -> backward
val t_or : backward -> backward -> backward
val t_or_map : (tcenv1 -> 'a * tcenv) list -> tcenv1 -> 'a * tcenv
val t_ors_pmap : ('a -> backward option) -> 'a list -> backward
val t_ors_map : ('a -> backward) -> 'a list -> backward
val t_ors : backward list -> backward
val t_internal : ?info:string -> backward -> backward
end
val (!!) : tcenv1 -> proofenv
val (!$) : tcenv -> proofenv
val (!@) : tcenv1 -> tcenv
(* -------------------------------------------------------------------- *)
(* Imperative API *)
(* -------------------------------------------------------------------- *)
module RApi : sig
type rproofenv
type rtcenv
val rtcenv_of_tcenv : tcenv -> rtcenv
val tcenv_of_rtcenv : rtcenv -> tcenv
val rtcenv_of_tcenv1 : tcenv1 -> rtcenv
(* For the following functions, see the [FApi] module *)
val pf_get_pregoal_by_id : handle -> rproofenv -> pregoal
val tc_get_pregoal_by_id : handle -> rtcenv -> pregoal
val newgoal : rtcenv -> ?hyps:LDecl.hyps -> form -> handle
val close : rtcenv -> validation -> unit
val bwd_of_fwd : FApi.forward -> rtcenv -> handle
(* Accessors for focused goal parts (rtcenv) *)
val tc_penv : rtcenv -> proofenv
val tc_flat : ?target:ident -> rtcenv -> LDecl.hyps * form
val tc_eflat : ?target:ident -> rtcenv -> env * LDecl.hyps * form
val tc_hyps : ?target:ident -> rtcenv -> LDecl.hyps
val tc_goal : rtcenv -> form
val tc_env : rtcenv -> env
(* Recast a rtcenv-imperative function as a tcenv-pure function. *)
val of_pure_u : ( tcenv -> tcenv) -> rtcenv -> unit
val to_pure_u : (rtcenv -> unit ) -> tcenv -> tcenv
val of_pure : (tcenv -> 'a * tcenv) -> rtcenv -> 'a
val to_pure : (rtcenv -> 'a) -> tcenv -> tcenv * 'a
(* [freeze] returns a copy of the input [rtcenv], whereas [restore]
* copies the contents of [src:rtcenv] to [dst:rtcenv]. These
* operations are done in constant time. *)
val freeze : rtcenv -> rtcenv
val restore : dst:rtcenv -> src:rtcenv -> unit
end
type rproofenv = RApi.rproofenv
type rtcenv = RApi.rtcenv
(* -------------------------------------------------------------------- *)
module Exn : sig
(* Apply the given function in the context of a proof-environment,
* adding some more location informations when a typing error is
* raised *)
val recast_pe : proofenv -> LDecl.hyps -> (unit -> 'a) -> 'a
val recast_tc : tcenv -> (LDecl.hyps -> 'a) -> 'a
val recast_tc1 : tcenv1 -> (LDecl.hyps -> 'a) -> 'a
end