Skip to main content

Browse the archive

https://github.com/EasyCrypt/easycrypt
16 November 2022, 21:30:08 UTC
Revision 36f7f5a29ef730b23ec3b2a96e76e387e90ea0e5 authored by Alley Stoughton on 21 February 2018, 22:32:02 UTC, committed by Pierre-Yves Strub on 26 February 2018, 15:04:53 UTC 
Added clean way to clear the list of current provers.
 
The elements of prover [...] have one of the following forms, where s
is a string:

s (add s to the use-only list)
+s (add include s to the include/exclude list)
-s (add exclude s to the include/exclude list)

The include/exclude list is ordered, so that later instructions can
supersede earlier ones. The use-only list was not ordered, but now
is. The relative order of the use-only and include/exclude lists
is irrelevant, so that, e.g., prover ["Z3" +"Alt-Ergo"] and prover
[+"Alt-Ergo" "Z3"] are equivalent.

The semantics is that the use-only list is first interpreted (if it's
empty, one starts with the current provers as the base), and only then
are the instructions of the include/exclude list applied to it, in
order.

There was already the special use-only instruction "ALL". Now, there is
also the use-only instruction "CLEAR", which clears the use-only list,
but may be superseded by the use-only instructions that follow.

Examples (assuming "Z3" and "Alt-Ergo" are only known provers):
prover []. (* a no-op *)
prover [+"Z3"]  (* adds just "Z3" to whatever current provers are *)
prover [-"Z3"]  (* removes just "Z3" from whatever current provers are *)
prover ["ALL"]  (* results in "Z3", "Alt-Ergo" *)
prover ["CLEAR"]  (* results in nothing *)
prover ["CLEAR" +"Z3"]  (* results in just "Z3" *)
prover [+"Z3" "CLEAR"]  (* results in just "Z3" *)
prover ["CLEAR" "Z3"]  (* result in just "Z3" *)
prover ["Z3" "CLEAR"]  (* results in nothing *)
prover [-"Z3" "ALL"]  (* results in "Alt-Ergo" *)
prover [+"Z3" "ALL" -"Z3"]  (* results in "Alt-Ergo" *)
prover [-"Z3" "ALL" +"Z3"]  (* results in "Z3", "Alt-Ergo" *)
1 parent 5115c89
Raw File
Tip revision: 36f7f5a29ef730b23ec3b2a96e76e387e90ea0e5 authored by Alley Stoughton on 21 February 2018, 22:32:02 UTC
Added clean way to clear the list of current provers.
Tip revision: 36f7f5a
ecPrinting.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 EcIdent
open EcSymbols
open EcPath
open EcTypes
open EcFol
open EcDecl
open EcModules
open EcTheory

(* -------------------------------------------------------------------- *)
module PPEnv : sig
  type t

  val ofenv : EcEnv.env -> t
  val add_locals : ?force:bool -> t -> EcIdent.t list -> t
end

(* -------------------------------------------------------------------- *)
val string_of_hcmp : EcFol.hoarecmp -> string
(* -------------------------------------------------------------------- *)
type 'a pp = Format.formatter -> 'a -> unit

val pp_id    : 'a pp -> 'a pp
val pp_if    : bool -> 'a pp -> 'a pp -> 'a pp
val pp_maybe : bool -> ('a pp -> 'a pp) -> 'a pp -> 'a pp

val pp_enclose:
       pre:('a, 'b, 'c, 'd, 'd, 'a) format6
   -> post:('a, 'b, 'c, 'd, 'd, 'a) format6
   -> 'a pp -> 'a pp

val pp_paren : 'a pp -> 'a pp

val pp_list : ('a, 'b, 'c, 'd, 'd, 'a) format6 -> 'a pp -> 'a list pp

(* -------------------------------------------------------------------- *)
val pp_pv      : PPEnv.t -> prog_var pp
val pp_local   : ?fv:Sid.t -> PPEnv.t -> ident pp
val pp_opname  : PPEnv.t -> path pp
val pp_funname : PPEnv.t -> xpath pp
val pp_topmod  : PPEnv.t -> mpath pp
val pp_form    : PPEnv.t -> form pp
val pp_type    : PPEnv.t -> ty pp
val pp_tyname  : PPEnv.t -> path pp
val pp_axname : PPEnv.t -> path pp

val pp_mem      : PPEnv.t -> EcIdent.t pp
val pp_tyvar    : PPEnv.t -> ident pp
val pp_tyunivar : PPEnv.t -> EcUid.uid pp
val pp_path     : path pp

(* -------------------------------------------------------------------- *)
val pp_typedecl : PPEnv.t -> (path * tydecl                ) pp
val pp_opdecl   : ?long:bool -> PPEnv.t -> (path * operator) pp
val pp_added_op : PPEnv.t -> operator pp
val pp_axiom    : ?long:bool -> PPEnv.t -> (path * axiom   ) pp
val pp_theory   : PPEnv.t -> (path * (ctheory * thmode)    ) pp
val pp_modtype1 : PPEnv.t -> module_type                     pp
val pp_modtype  : PPEnv.t -> (module_type * mod_restr      ) pp
val pp_modexp   : PPEnv.t -> (mpath * module_expr          ) pp
val pp_modsig   : PPEnv.t -> (path * module_sig            ) pp

(* -------------------------------------------------------------------- *)
val pp_hoareS   : PPEnv.t -> hoareS  pp
val pp_bdhoareS : PPEnv.t -> bdHoareS pp
val pp_equivS   : PPEnv.t -> equivS  pp

val pp_stmt  : ?lineno:bool -> PPEnv.t -> stmt pp
val pp_instr : PPEnv.t -> instr pp

(* -------------------------------------------------------------------- *)
type ppgoal = (EcBaseLogic.hyps * EcFol.form) * [
  | `One of int
  | `All of (EcBaseLogic.hyps * EcFol.form) list
]

val pp_hyps : PPEnv.t -> EcEnv.LDecl.hyps pp
val pp_goal : PPEnv.t -> ppgoal pp

(* -------------------------------------------------------------------- *)
module ObjectInfo : sig
  val pr_ty  : Format.formatter -> EcEnv.env -> qsymbol -> unit
  val pr_op  : Format.formatter -> EcEnv.env -> qsymbol -> unit
  val pr_th  : Format.formatter -> EcEnv.env -> qsymbol -> unit
  val pr_ax  : Format.formatter -> EcEnv.env -> qsymbol -> unit
  val pr_mod : Format.formatter -> EcEnv.env -> qsymbol -> unit
  val pr_mty : Format.formatter -> EcEnv.env -> qsymbol -> unit
  val pr_any : Format.formatter -> EcEnv.env -> qsymbol -> unit
end
back to top