Wp.ProofScript
class console : pool:Lang.F.pool -> title:string -> Wp__Tactical.feedback
type jscript = alternative list
and alternative = private
| Prover of VCS.prover * VCS.result | |
| Tactic of int * jtactic * (string * jscript) list | (* With number of pending goals *) |
| Error of string * Frama_c_kernel.Json.t |
and jtactic = {
header : string; |
tactic : string; |
params : Frama_c_kernel.Json.t; |
select : Frama_c_kernel.Json.t; |
}
val is_prover : alternative -> bool
val is_tactic : alternative -> bool
val a_prover : VCS.prover -> VCS.result -> alternative
val a_tactic : jtactic -> (string * jscript) list -> alternative
val pending : alternative -> int
pending goals
val pending_any : jscript -> int
minimum of pending goals
val has_proof : jscript -> bool
Has a tactical alternative
val decode : Frama_c_kernel.Json.t -> jscript
val encode : jscript -> Frama_c_kernel.Json.t
val jtactic :
title:string ->
Tactical.tactical ->
Tactical.selection ->
jtactic
val configure :
jtactic ->
Conditions.sequent ->
(Tactical.tactical * Tactical.selection) option
Json Codecs
val json_of_selection : Tactical.selection -> Frama_c_kernel.Json.t
val selection_of_json :
Conditions.sequent ->
Frama_c_kernel.Json.t ->
Tactical.selection
val selection_target : Frama_c_kernel.Json.t -> string
val json_of_param :
Tactical.tactical ->
Tactical.parameter ->
string * Frama_c_kernel.Json.t
val param_of_json :
Tactical.tactical ->
Conditions.sequent ->
Frama_c_kernel.Json.t ->
Tactical.parameter ->
unit
val json_of_parameters : Tactical.tactical -> Frama_c_kernel.Json.t
val parameters_of_json :
Tactical.tactical ->
Conditions.sequent ->
Frama_c_kernel.Json.t ->
unit
val json_of_tactic :
jtactic ->
(string * Frama_c_kernel.Json.t) list ->
Frama_c_kernel.Json.t
val json_of_result : VCS.prover -> VCS.result -> Frama_c_kernel.Json.t
val prover_of_json : Frama_c_kernel.Json.t -> VCS.prover option
val result_of_json : Frama_c_kernel.Json.t -> VCS.result