module ProverCoq: sig
.. end
val dkey : Log.category
val cluster_file : Definitions.cluster -> string
val option_file : LogicBuiltins.doption
type
coqlib = {
|
c_id : string ; |
|
c_source : string ; |
|
c_file : string ; |
|
c_path : string ; |
|
c_name : string ; |
|
c_module : string ; |
}
val name_of_path : string -> string
val find_nonwin_column : string -> int
val parse_c_option : string -> coqlib
val coqlibs : (string, coqlib) Hashtbl.t
val c_option : string -> coqlib
type
depend =
val engine : < basename : string -> string; bind : Lang.F.var -> string;
callstyle : Qed.Engine.callstyle; datatype : Lang.ADT.t -> string;
datatypename : string -> string;
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_fixpoint : prefix:string ->
Format.formatter ->
Lang.F.Fun.t ->
Lang.F.var list -> Lang.F.tau -> 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;
find : Lang.F.var -> string; funname : string -> string;
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_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_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 -> string 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 -> string 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_imply : Format.formatter -> Lang.F.term list -> Lang.F.term -> unit;
pp_int : Qed.Engine.amode -> Lang.F.Z.t Qed.Plib.printer;
pp_lambda : (string * Lang.F.tau) 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_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_tvar : int Qed.Plib.printer; pp_var : string Qed.Plib.printer;
t_atomic : Lang.F.tau -> bool; t_bool : string; t_int : string;
t_prop : string; t_real : string;
with_mode : Qed.Engine.mode -> (Qed.Engine.mode -> unit) -> unit >
class visitor : Format.formatter -> Definitions.cluster ->
object
.. end
val write_cluster : Definitions.cluster -> depend list
val need_recompile : source:string -> target:string -> bool
module CLUSTERS: Model.Index
(
sig
end
)
module Marked: Set.Make
(
sig
end
)
type
included = string * string
type
coqcc = {
|
mutable marked : Marked.t ; |
|
mutable includes : included list ; |
|
mutable sources : string list ; |
}
val add_include : coqcc -> included -> unit
val add_source : coqcc -> string -> unit
val assemble : coqcc -> Marked.elt -> unit
val assemble_cluster : coqcc -> CLUSTERS.key -> unit
val assemble_coqlib : coqcc -> coqlib -> unit
val assemble_goal : pid:WpPropId.prop_id ->
Definitions.axioms option ->
Lang.F.pred -> included list * string list * string
val coq_timeout : unit -> Wp_parameters.CoqTimeout.t
val coqidelock : Task.mutex
class runcoq : (Wp_parameters.Script.t * Wp_parameters.Script.t) list -> Wp_parameters.Script.t ->
object
.. end
val shared_demon : bool Pervasives.ref
: (Wp_parameters.Script.t, unit Task.shared) Hashtbl.t
val shared : (Wp_parameters.Script.t * Wp_parameters.Script.t) list ->
Wp_parameters.Script.t -> unit Task.shared
: (Wp_parameters.Script.t * Wp_parameters.Script.t) list ->
bool -> Wp_parameters.Script.t list -> unit Task.task
type
coq_wpo = {
|
cw_pid : WpPropId.prop_id ; |
|
cw_gid : string ; |
|
cw_goal : string ; |
|
cw_script : string ; |
|
: string list ; |
|
cw_includes : included list ; |
}
val make_script : ?admitted:bool -> coq_wpo -> string -> unit
val try_script : ?admitted:bool -> coq_wpo -> string -> bool Task.task
val try_hints : coq_wpo -> (string * string) list -> bool Task.task
val try_prove : coq_wpo -> bool Task.task
val try_coqide : coq_wpo -> bool Task.task
val prove_session : mode:VCS.mode -> coq_wpo -> VCS.result Task.task
exception Admitted_not_proved
val check_session : coq_wpo -> VCS.result Task.task
val prove_session : mode:VCS.mode -> coq_wpo -> VCS.result Task.task
val prove_prop : Wpo.t ->
mode:VCS.mode ->
axioms:Definitions.axioms option -> prop:Lang.F.pred -> VCS.result Task.task
val prove_annot : Wpo.t -> Wpo.VC_Annot.t -> mode:VCS.mode -> VCS.result Task.task
val prove_lemma : Wpo.t -> Wpo.VC_Lemma.t -> mode:VCS.mode -> VCS.result Task.task
val prove_check : Wpo.t -> Wpo.VC_Check.t -> mode:VCS.mode -> VCS.result Task.task
val prove : VCS.mode -> Wpo.t -> VCS.result Task.task