1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
open Wpo
type t = Wpo.t
let get_id = Wpo.get_gid
let get_model = Wpo.get_model
let get_scope = Wpo.get_scope
let get_context = Wpo.get_context
let get_description = Wpo.get_label
let get_property = Wpo.get_property
let get_sequent w = snd (Wpo.compute w)
let get_result = Wpo.get_result
let get_results = ProofEngine.results
let is_trivial = Wpo.is_trivial
let is_valid = Wpo.is_fully_valid
let is_passed = Wpo.is_passed
let has_unknown = Wpo.has_unknown
let get_formula po =
WpContext.on_context
(get_context po) (Wpo.GOAL.compute_proof ~pid:po.po_pid) po.po_formula.goal
let clear = Wpo.clear
let proof = Wpo.goals_of_property
let iter_ip on_goal ip = Wpo.iter ~ip ~on_goal ()
let iter_kf on_goal ?bhv kf =
match bhv with
| None ->
Wpo.iter ~index:(Wpo.Function(kf,None)) ~on_goal ()
| Some bs ->
List.iter
(fun b ->
Wpo.iter ~index:(Wpo.Function(kf,Some b)) ~on_goal ()
) bs
let remove = iter_ip Wpo.remove
let () = Property_status.register_property_remove_hook remove
let generator model =
let setup = match model with
| None -> None
| Some s -> Some (Factory.parse [s]) in
Generator.create ~dump:false ?setup ()
let generate_ip ?model ip =
(generator model)#compute_ip ip
let generate_kf ?model ?bhv ?prop kf =
let kfs = Kernel_function.Set.singleton kf in
(generator model)#compute_main ~fct:(Fct_list kfs) ?bhv ?prop ()
let generate_call ?model stmt =
(generator model)#compute_call stmt
let prove = Prover.prove
let spawn = Prover.spawn ~delayed:true
let server = ProverTask.server
let command ?provers ?tip vcs =
Register.do_wp_proofs ?provers ?tip vcs