swh:1:snp:0e3a7a90b5b85feca1ee6285ebc0301d2b85deae
Tip revision: 0dd57f714852f6f779d230c5bbf3e98e4594f41f authored by François Dupressoir on 06 December 2019, 09:55:55 UTC
OneMap-PRP: a PRP with a single map and lemmas to switch
OneMap-PRP: a PRP with a single map and lemmas to switch
Tip revision: 0dd57f7
ecCommands.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 EcLocation
(* -------------------------------------------------------------------- *)
exception Restart
(* -------------------------------------------------------------------- *)
val addidir : ?namespace:EcLoader.namespace -> ?recursive:bool -> string -> unit
val loadpath : unit -> (EcLoader.namespace option * string) list
(* -------------------------------------------------------------------- *)
type notifier = EcGState.loglevel -> string Lazy.t -> unit
type checkmode = {
cm_checkall : bool;
cm_timeout : int;
cm_cpufactor: int;
cm_nprovers : int;
cm_provers : string list option;
cm_profile : bool;
cm_iterate : bool;
}
val initialize :
restart:bool
-> undo:bool
-> boot:bool
-> checkmode:checkmode
-> unit
val current : unit -> EcScope.scope
val addnotifier : notifier -> unit
(* -------------------------------------------------------------------- *)
val process : ?timed:bool -> EcParsetree.global_action located -> float option
val undo : int -> unit
val reset : unit -> unit
val uuid : unit -> int
val mode : unit -> string
val check_eco : string -> bool
(* -------------------------------------------------------------------- *)
val pp_current_goal : ?all:bool -> Format.formatter -> unit
val pp_maybe_current_goal : Format.formatter -> unit
(* -------------------------------------------------------------------- *)
val pragma_verbose : bool -> unit
val pragma_g_prall : bool -> unit
val pragma_check : EcScope.Ax.mode -> unit
exception InvalidPragma of string
val apply_pragma : string -> unit