module ProverErgo: sig
.. end
val dkey : Log.category
val option_file : LogicBuiltins.doption
val altergo_gui : bool lazy_t
val append_file : Pervasives.out_channel -> string -> int
val locate_error : (string * int) list -> string -> int -> Lexing.position
val cluster_file : Definitions.cluster -> string
type
depend =
val pp_depend : Format.formatter -> depend -> unit
module TYPES: Model.Index
(
sig
end
)
val engine : < basename : string -> string; bind : Lang.F.var -> unit;
callstyle : Qed.Engine.callstyle; datatype : Lang.ADT.t -> string;
datatypename : string -> string; declare : string -> unit;
declare_all : string list -> unit;
declare_axiom : Format.formatter ->
string ->
Lang.F.var list ->
Definitions.trigger list list -> Lang.F.term -> unit;
declare_definition : Format.formatter ->
Lang.F.Fun.t ->
Lang.F.var list -> Lang.F.tau -> Lang.F.term -> unit;
declare_prop : kind:string ->
Format.formatter ->
string ->
Lang.F.var list ->
(Lang.F.var, Lang.F.Fun.t) Qed.Engine.ftrigger list list ->
Lang.F.term -> unit;
declare_signature : Format.formatter ->
Lang.F.Fun.t -> Lang.F.tau list -> Lang.F.tau -> unit;
declare_type : Format.formatter ->
Lang.F.ADT.t -> int -> Definitions.typedef -> unit;
e_false : Qed.Engine.cmode -> string; e_true : Qed.Engine.cmode -> string;
field : Lang.Field.t -> string; fieldname : string -> string;
funname : string -> string;
get_typedef : Lang.F.ADT.t -> Lang.F.tau option;
global : (unit -> unit) -> unit; infoprover : 'a. 'a Lang.infoprover -> 'a;
is_atomic : Lang.F.term -> bool; is_shareable : Lang.F.term -> bool;
link : Lang.Fun.t -> Qed.Engine.link; local : (unit -> unit) -> unit;
mode : Qed.Engine.mode; op_add : Qed.Engine.amode -> Qed.Engine.op;
op_and : Qed.Engine.cmode -> Qed.Engine.op;
op_div : Qed.Engine.amode -> Qed.Engine.op;
op_eq : Qed.Engine.cmode -> Qed.Engine.amode -> Qed.Engine.op;
op_equal : Qed.Engine.cmode -> Qed.Engine.op;
op_equiv : Qed.Engine.cmode -> Qed.Engine.op;
op_imply : Qed.Engine.cmode -> Qed.Engine.op;
op_leq : Qed.Engine.cmode -> Qed.Engine.amode -> Qed.Engine.op;
op_lt : Qed.Engine.cmode -> Qed.Engine.amode -> Qed.Engine.op;
op_minus : Qed.Engine.amode -> Qed.Engine.op;
op_mod : Qed.Engine.amode -> Qed.Engine.op;
op_mul : Qed.Engine.amode -> Qed.Engine.op;
op_neq : Qed.Engine.cmode -> Qed.Engine.amode -> Qed.Engine.op;
op_not : Qed.Engine.cmode -> Qed.Engine.op;
op_noteq : Qed.Engine.cmode -> Qed.Engine.op;
op_or : Qed.Engine.cmode -> Qed.Engine.op; op_real_of_int : Qed.Engine.op;
op_record : string * string; op_scope : Qed.Engine.amode -> string option;
op_spaced : string -> bool; op_sub : Qed.Engine.amode -> Qed.Engine.op;
pp_apply : Qed.Engine.cmode ->
Lang.F.term -> Lang.F.term list Qed.Plib.printer;
pp_array : Lang.F.tau Qed.Plib.printer;
pp_array_get : Format.formatter -> Lang.F.term -> Lang.F.term -> unit;
pp_array_set : Format.formatter ->
Lang.F.term -> Lang.F.term -> Lang.F.term -> unit;
pp_atom : Lang.F.term Qed.Plib.printer;
pp_conditional : Format.formatter ->
Lang.F.term -> Lang.F.term -> Lang.F.term -> unit;
pp_cst : Qed.Numbers.cst Qed.Plib.printer;
pp_datatype : Lang.F.ADT.t -> Lang.F.tau list Qed.Plib.printer;
pp_declare_adt : Format.formatter -> Lang.F.ADT.t -> int -> unit;
pp_declare_def : Format.formatter ->
Lang.F.ADT.t -> int -> Lang.F.tau -> unit;
pp_declare_sum : Format.formatter ->
Lang.F.ADT.t ->
int -> (Lang.F.Fun.t * Lang.F.tau list) list -> unit;
pp_declare_symbol : Qed.Engine.cmode -> Lang.F.Fun.t Qed.Plib.printer;
pp_def_fields : (Lang.F.Field.t * Lang.F.term) list Qed.Plib.printer;
pp_equal : Lang.F.term Qed.Plib.printer2;
pp_exists : Lang.F.tau -> Lang.F.var list Qed.Plib.printer;
pp_expr : Lang.F.tau -> Lang.F.term Qed.Plib.printer;
pp_farray : Lang.F.tau Qed.Plib.printer2;
pp_flow : Lang.F.term Qed.Plib.printer;
pp_forall : Lang.F.tau -> Lang.F.var list Qed.Plib.printer;
pp_fun : Qed.Engine.cmode ->
Lang.F.Fun.t -> Lang.F.term list Qed.Plib.printer;
pp_get_field : Format.formatter -> Lang.F.term -> Lang.F.Field.t -> unit;
pp_goal : model:int -> Format.formatter -> Lang.F.term -> unit;
pp_imply : Format.formatter -> Lang.F.term list -> Lang.F.term -> unit;
pp_int : Qed.Engine.amode -> Lang.F.Z.t Qed.Plib.printer;
pp_intros : Lang.F.tau -> Lang.F.var list Qed.Plib.printer;
pp_lambda : Lang.F.var list Qed.Plib.printer;
pp_let : Format.formatter ->
Qed.Engine.pmode -> string -> Lang.F.term -> unit;
pp_not : Lang.F.term Qed.Plib.printer;
pp_noteq : Lang.F.term Qed.Plib.printer2;
pp_param : Lang.F.var Qed.Plib.printer;
pp_prop : Lang.F.term Qed.Plib.printer; pp_real : Qed.R.t Qed.Plib.printer;
pp_subtau : Lang.F.tau Qed.Plib.printer;
pp_tau : Lang.F.tau Qed.Plib.printer;
pp_term : Lang.F.term Qed.Plib.printer;
pp_times : Format.formatter -> Lang.F.Z.t -> Lang.F.term -> unit;
pp_trigger : (Lang.F.var, Lang.F.Fun.t) Qed.Engine.ftrigger
Qed.Plib.printer;
pp_tvar : int Qed.Plib.printer; pp_var : Lang.F.var Qed.Plib.printer;
set_quantify_let : bool -> unit;
set_typedef : Lang.F.ADT.t -> Lang.F.tau -> unit;
t_atomic : Lang.F.tau -> bool; t_bool : string; t_int : string;
t_prop : string; t_real : string; typecheck : Lang.F.term -> Lang.F.tau;
typeof_call : Lang.F.Fun.t -> Lang.F.tau;
typeof_getfield : Lang.F.Field.t -> Lang.F.tau;
typeof_setfield : Lang.F.Field.t -> Lang.F.tau;
with_mode : Qed.Engine.mode -> (Qed.Engine.mode -> unit) -> unit >
class visitor : Format.formatter -> Definitions.cluster ->
object
.. end
val write_cluster : Definitions.cluster -> (visitor -> 'a) -> depend list
module CLUSTERS: Model.Index
(
sig
end
)
type
export = {
}
val assemble : export -> depend -> unit
val assemble_file : export -> string -> unit
val assemble_cluster : export -> CLUSTERS.key -> unit
val assemble_lib : export -> string -> unit
val assemble_goal : file:string ->
id:string ->
title:string ->
axioms:Definitions.axioms option -> Lang.F.pred -> (string * int) list
val p_loc : string
val p_valid : string
val p_unsat : string
val p_limit : string
val re_error : Str.regexp
val re_valid : Str.regexp
val re_limit : Str.regexp
val re_unsat : Str.regexp
class altergo : pid:'a -> gui:bool -> file:string -> lines:(string * int) list -> logout:string -> logerr:string ->
object
.. end
val try_prove : pid:'a ->
gui:bool ->
file:string ->
lines:(string * int) list ->
logout:string -> logerr:string -> VCS.result Task.task
val prove_file : pid:'a ->
mode:VCS.mode ->
file:string ->
lines:(string * int) list ->
logout:string -> logerr:string -> VCS.result Task.task
val prove_prop : pid:WpPropId.prop_id ->
mode:VCS.mode ->
model:Model.t ->
axioms:Definitions.axioms option -> prop:Lang.F.pred -> VCS.result Task.task
val prove_annot : Model.t ->
WpPropId.prop_id -> Wpo.VC_Annot.t -> mode:VCS.mode -> VCS.result Task.task
val prove_lemma : Model.t ->
WpPropId.prop_id -> Wpo.VC_Lemma.t -> mode:VCS.mode -> VCS.result Task.task
val prove_check : Model.t ->
WpPropId.prop_id -> Wpo.VC_Check.t -> mode:VCS.mode -> VCS.result Task.task
val prove : VCS.mode -> Wpo.t -> VCS.result Task.task