Skip to main content

Browse the archive

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
ecTheoryReplay.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 EcSymbols
open EcPath
open EcParsetree
open EcTypes
open EcDecl
open EcModules
open EcTheory
open EcThCloning

(* ------------------------------------------------------------------ *)
type ovoptions = {
  clo_abstract : bool;
}

type 'a ovrenv = {
  ovre_ovrd     : EcThCloning.evclone;
  ovre_rnms     : EcThCloning.renaming list;
  ovre_ntclr    : EcPath.Sp.t;
  ovre_opath    : EcPath.path;
  ovre_npath    : EcPath.path;
  ovre_prefix   : (symbol list) EcUtils.pair;
  ovre_glproof  : (ptactic_core option * evtags option) list;
  ovre_abstract : bool;
  ovre_local    : bool;
  ovre_hooks    : 'a ovrhooks;
}

and 'a ovrhooks = {
  henv     : 'a -> EcEnv.env;
  hty      : 'a -> (symbol * tydecl) -> 'a;
  hop      : 'a -> (symbol * operator) -> 'a;
  hmodty   : 'a -> (symbol * module_sig) -> 'a;
  hmod     : 'a -> bool -> module_expr -> 'a;
  hax      : 'a -> bool -> (symbol * axiom) -> 'a;
  hexport  : 'a -> EcPath.path -> 'a;
  hbaserw  : 'a -> symbol -> 'a;
  haddrw   : 'a -> EcPath.path * EcPath.path list -> 'a;
  hauto    : 'a -> bool * int * string option * EcPath.path list -> 'a;
  htycl    : 'a -> symbol * typeclass -> 'a;
  hinst    : 'a -> (ty_params * ty) * tcinstance -> 'a;
  hthenter : 'a -> thmode -> symbol -> 'a;
  hthexit  : 'a -> [`Full | `ClearOnly | `No] -> 'a;
  herr     : 'b . ?loc:EcLocation.t -> string -> 'b;
}

(* -------------------------------------------------------------------- *)
val replay : 'a ovrhooks
  -> abstract:bool -> local:bool -> incl:bool
  -> clears:Sp.t -> renames:(renaming list)
  -> opath:path -> npath:path -> evclone
  -> 'a -> symbol * ctheory_item list
  ->  axclone list * 'a
back to top