From 57373f31c82f6b308755ac96e51e2f12242324c5 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 19 Sep 2023 10:54:45 +0200
Subject: [PATCH] [wp] Merge VC_Annot and VC_Lemma
---
src/plugins/wp/ProofEngine.ml | 14 +-
src/plugins/wp/ProverWhy3.ml | 18 +-
src/plugins/wp/VC.ml | 9 +-
src/plugins/wp/VC.mli | 5 -
src/plugins/wp/cfgWP.ml | 15 +-
src/plugins/wp/gui/GuiSource.ml | 13 +-
src/plugins/wp/ptip.ml | 13 +-
src/plugins/wp/tests/wp/stmtcompiler_test.ml | 6 +-
.../wp/tests/wp/stmtcompiler_test_rela.ml | 4 +-
src/plugins/wp/wpo.ml | 203 +++---------------
src/plugins/wp/wpo.mli | 35 +--
11 files changed, 65 insertions(+), 270 deletions(-)
diff --git a/src/plugins/wp/ProofEngine.ml b/src/plugins/wp/ProofEngine.ml
index 627bad9ac3c..a131316102e 100644
--- a/src/plugins/wp/ProofEngine.ml
+++ b/src/plugins/wp/ProofEngine.ml
@@ -313,20 +313,8 @@ let cancel t =
(* --- Sub-Goal --- *)
(* -------------------------------------------------------------------------- *)
-let mk_annot axioms goal vc =
- let open Wpo.VC_Annot in
- match vc with
- | Wpo.GoalAnnot annot -> { annot with goal ; axioms }
- | _ -> {
- axioms ; goal ;
- tags = [] ; warn = [] ;
- deps = Property.Set.empty ;
- path = Cil_datatype.Stmt.Set.empty ;
- source = None ;
- }
-
let mk_formula ~main axioms sequent =
- Wpo.(GoalAnnot (mk_annot axioms (GOAL.make sequent) main))
+ Wpo.VC_Annot.{ main with goal = Wpo.GOAL.make sequent ; axioms }
let mk_goal t ~title ~part ~axioms sequent =
let id = t.gid in t.gid <- succ id ;
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index a0abe91f0fe..d0bf28e123f 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -1100,20 +1100,12 @@ let prove_prop ?axioms ~pid prop =
Why3.Task.add_decl t decl
let task_of_wpo wpo =
+ let v = wpo.Wpo.po_formula in
let pid = wpo.Wpo.po_pid in
- match wpo.Wpo.po_formula with
- | Wpo.GoalAnnot v ->
- let pid = wpo.Wpo.po_pid in
- let axioms = v.Wpo.VC_Annot.axioms in
- let prop = Wpo.GOAL.compute_proof ~pid v.Wpo.VC_Annot.goal in
- (* Format.printf "Goal: %a@." Lang.F.pp_pred prop; *)
- prove_prop ~pid prop ?axioms
- | Wpo.GoalLemma v ->
- let lemma = v.Wpo.VC_Lemma.lemma in
- let depends = v.Wpo.VC_Lemma.depends in
- let prop = Lang.F.p_forall lemma.l_forall lemma.l_lemma in
- let axioms = Some(lemma.l_cluster,depends) in
- prove_prop ~pid prop ?axioms
+ let axioms = v.Wpo.VC_Annot.axioms in
+ let prop = Wpo.GOAL.compute_proof ~pid v.Wpo.VC_Annot.goal in
+ (* Format.printf "Goal: %a@." Lang.F.pp_pred prop; *)
+ prove_prop ~pid prop ?axioms
(* -------------------------------------------------------------------------- *)
(* --- Prover Task --- *)
diff --git a/src/plugins/wp/VC.ml b/src/plugins/wp/VC.ml
index a91f103651c..59be9f01aad 100644
--- a/src/plugins/wp/VC.ml
+++ b/src/plugins/wp/VC.ml
@@ -37,19 +37,14 @@ let get_property = Wpo.get_property
let get_sequent w = snd (Wpo.compute w)
let get_result = Wpo.get_result
let get_results = Wpo.get_results
-let get_logout = Wpo.get_file_logout
-let get_logerr = Wpo.get_file_logerr
let is_trivial = Wpo.is_trivial
let is_valid = Wpo.is_valid
let is_passed = Wpo.is_passed
let has_unknown = Wpo.has_unknown
let get_formula po =
- match po.po_formula with
- | GoalLemma l -> l.VC_Lemma.lemma.Definitions.l_lemma
- | GoalAnnot { VC_Annot.goal = g } ->
- WpContext.on_context
- (get_context po) (Wpo.GOAL.compute_proof ~pid:po.po_pid) g
+ 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
diff --git a/src/plugins/wp/VC.mli b/src/plugins/wp/VC.mli
index d585e618563..af2675f9f24 100644
--- a/src/plugins/wp/VC.mli
+++ b/src/plugins/wp/VC.mli
@@ -38,11 +38,6 @@ val get_description : t -> string
val get_property : t -> Property.t
val get_result : t -> prover -> result
val get_results : t -> (prover * result) list
-val get_logout : t -> prover -> string
-(** only file name, might not exists *)
-
-val get_logerr : t -> prover -> string
-(** only file name, might not exists *)
val get_sequent : t -> Conditions.sequent
val get_formula: t -> Lang.F.pred
diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index e1a4d022b51..c43def5003d 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -1555,7 +1555,7 @@ struct
po_gid = "" ;
po_name = "" ;
po_idx = index ;
- po_formula = GoalAnnot vcq ;
+ po_formula = vcq ;
}
(* -------------------------------------------------------------------------- *)
@@ -1631,10 +1631,15 @@ struct
let id = WpPropId.mk_lemma_id l in
let def = L.lemma l in
let model = WpContext.get_model () in
+ let sequent = Conditions.lemma def.l_lemma in
let vca = {
- Wpo.VC_Lemma.depends = l.lem_depends ;
- Wpo.VC_Lemma.lemma = def ;
- Wpo.VC_Lemma.sequent = None ;
+ Wpo.VC_Annot.axioms = Some (def.l_cluster, l.lem_depends) ;
+ goal = GOAL.make sequent ;
+ tags = [] ;
+ warn = [] ; (* TODO: complete *)
+ deps = Property.Set.empty ;
+ path = Stmt.Set.empty ;
+ source = None ;
} in
let index = match LogicUsage.section_of_lemma l.lem_name with
| LogicUsage.Toplevel _ -> Wpo.Axiomatic None
@@ -1648,7 +1653,7 @@ struct
Wpo.po_name = Printf.sprintf "Lemma '%s'" l.lem_name ;
Wpo.po_idx = index ;
Wpo.po_pid = id ;
- Wpo.po_formula = Wpo.GoalLemma vca ;
+ Wpo.po_formula = vca ;
} in
Wpo.add wpo ; wpo
end
diff --git a/src/plugins/wp/gui/GuiSource.ml b/src/plugins/wp/gui/GuiSource.ml
index f076087e08d..b2fff1a7327 100644
--- a/src/plugins/wp/gui/GuiSource.ml
+++ b/src/plugins/wp/gui/GuiSource.ml
@@ -169,9 +169,6 @@ let instructions path =
| _ -> false)
path
-let lemmas ls =
- List.fold_left (fun s l -> DEPS.add (LogicUsage.ip_lemma l) s) DEPS.empty ls
-
class highlighter (main:Design.main_window_extension_points) =
object(self)
@@ -208,13 +205,9 @@ class highlighter (main:Design.main_window_extension_points) =
| None -> Wutil.later main#rehighlight ;
| Some { Wpo.po_pid = pid ; Wpo.po_formula = f } ->
begin
- match f with
- | GoalLemma l ->
- deps <- lemmas l.VC_Lemma.depends
- | GoalAnnot a ->
- source <- a.VC_Annot.source ;
- path <- instructions a.VC_Annot.path ;
- deps <- a.VC_Annot.deps ;
+ source <- f.VC_Annot.source ;
+ path <- instructions f.VC_Annot.path ;
+ deps <- f.VC_Annot.deps ;
end ;
if not (WpPropId.is_check pid || WpPropId.is_tactic pid)
then
diff --git a/src/plugins/wp/ptip.ml b/src/plugins/wp/ptip.ml
index d95e4252fb8..8254af45dec 100644
--- a/src/plugins/wp/ptip.ml
+++ b/src/plugins/wp/ptip.ml
@@ -579,16 +579,9 @@ class pseq
pcond#pp_esequent env fmt s
method pp_goal fmt w =
- let open Wpo in
- match w.po_formula with
- | GoalLemma _ ->
- Format.fprintf fmt "@\n@{<wp:clause>Lemma@} %a:@\n" Wpo.pp_title w ;
- let _,sequent = Wpo.compute w in
- self#pp_sequent fmt sequent
- | GoalAnnot _ ->
- Format.fprintf fmt "@\n@{<wp:clause>Goal@} %a:@\n" Wpo.pp_title w ;
- let _,sequent = Wpo.compute w in
- self#pp_sequent fmt sequent
+ Format.fprintf fmt "@\n@{<wp:clause>Goal@} %a:@\n" Wpo.pp_title w ;
+ let _,sequent = Wpo.compute w in
+ self#pp_sequent fmt sequent
end
diff --git a/src/plugins/wp/tests/wp/stmtcompiler_test.ml b/src/plugins/wp/tests/wp/stmtcompiler_test.ml
index 983e9e738aa..ead9ff488bb 100644
--- a/src/plugins/wp/tests/wp/stmtcompiler_test.ml
+++ b/src/plugins/wp/tests/wp/stmtcompiler_test.ml
@@ -6,6 +6,8 @@ open Sigs
let mode = `Tree
+let bar = String.make 60 '-'
+
let run () =
let setup : Factory.setup = { mheap = Typed MemTyped.NoCast;
mvar = Var;
@@ -53,11 +55,11 @@ let run () =
po_gid = ""; po_sid = ""; po_name = "";
po_idx = Function(kf, None); po_model = model;
po_pid = prop_id;
- po_formula = Wpo.GoalAnnot vc_annot;
+ po_formula = vc_annot;
} in
Format.printf "@[%a@]" Wpo.pp_goal po;
spawn po;
- Format.printf "%s@." Wpo.bar ;
+ Format.printf "%s@." bar ;
in
let goal_read acc g =
diff --git a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
index 160ecd34770..3e167f78bf9 100644
--- a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
+++ b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
@@ -63,7 +63,7 @@ let run () =
po_idx = Function(kf, None);
po_model = model;
po_pid = WpPropId.mk_assert_id kf stmt annot;
- po_formula = Wpo.GoalAnnot vc_annot;
+ po_formula = vc_annot;
}
in
let inter_po = ref po in
@@ -77,7 +77,7 @@ let run () =
po_idx = Function(kf, None);
po_model = model;
po_pid = h.po_pid;
- po_formula = Wpo.GoalAnnot vc_annot;
+ po_formula = vc_annot;
}
| _ -> ()
);
diff --git a/src/plugins/wp/wpo.ml b/src/plugins/wp/wpo.ml
index 05f5828606b..574597b0795 100644
--- a/src/plugins/wp/wpo.ml
+++ b/src/plugins/wp/wpo.ml
@@ -113,44 +113,6 @@ struct
in
let id = WpPropId.get_propid pid in
file ~id ~model ~prover ~ext ()
-
- let file_kf ~kf ~model ~prover =
- let ext = match prover with
- | Qed -> "qed"
- | Why3 _ -> "why"
- | Tactical -> "tac"
- in
- let id = (Kf.vi kf).vname in
- file ~id ~model ~prover ~ext ()
-
- let dump_file fmt title file =
- if Sys.file_exists file then
- begin
- Format.fprintf fmt "--- %s ---------------------------------@\n" title ;
- Command.pp_from_file fmt file
- end
-
- let pretty ~pid ~model ~prover ~result fmt =
- begin
- Format.fprintf fmt "[%a] Goal %a : %a@\n"
- pp_prover prover WpPropId.pp_propid pid pp_result result ;
- dump_file fmt "StdOut" (file_logout ~pid ~model ~prover) ;
- dump_file fmt "StdErr" (file_logerr ~pid ~model ~prover) ;
- end
-
- let cache_log ~pid ~model ~prover ~result =
- (*TODO: put a cache here *)
- let dir = Wp_parameters.get_output () in
- let file = Printf.sprintf "%s/log.txt" (dir :> string) in
- Command.print_file file (pretty ~pid ~model ~prover ~result) ;
- file
-
- let cache_descr pretty =
- (*TODO: put a cache here *)
- let dir = Wp_parameters.get_output () in
- let file = Printf.sprintf "%s/goal.txt" (dir :> string) in
- Command.print_file file (fun fmt -> pretty fmt) ; file
-
end
module GOAL =
@@ -194,7 +156,7 @@ struct
let apply option phi g =
try
Db.yield () ;
- Wp_parameters.debug ~dkey "Appy %s" option ;
+ Wp_parameters.debug ~dkey "Apply %s" option ;
g.sequent <- phi g.sequent ;
with exn when Wp_parameters.protect exn ->
Wp_parameters.warning ~current:false ~once:true
@@ -256,57 +218,11 @@ struct
end
-module VC_Lemma =
-struct
-
- open Definitions
-
- type t = {
- lemma : Definitions.dlemma ;
- depends : logic_lemma list ;
- mutable sequent : Conditions.sequent option ;
- }
-
- let is_trivial vc = vc.lemma.l_lemma == F.p_true
-
- let sequent vc =
- match vc.sequent with
- | Some s -> s
- | None ->
- let s = Conditions.lemma vc.lemma.l_lemma in
- vc.sequent <- Some s ; s
-
- let pretty fmt vc results =
- begin
- Format.fprintf fmt "Lemma %s:@\n" vc.lemma.l_name ;
- if vc.depends <> [] then
- begin
- Format.fprintf fmt "@[<hov 2>@{<bf>Assume@}:" ;
- List.iter
- (fun a -> Format.fprintf fmt "@ '%s'" a.lem_name)
- vc.depends ;
- Format.fprintf fmt "@]@." ;
- end ;
- let env = F.env (List.fold_right F.Vars.add vc.lemma.l_forall F.Vars.empty) in
- Format.fprintf fmt "@{<bf>Prove@}: @[<hov 2>%a@]@." (F.pp_epred env) vc.lemma.l_lemma ;
- List.iter
- (fun (prover,result) ->
- if result.verdict <> NoResult then
- Format.fprintf fmt "Prover %a returns %t@\n"
- pp_prover prover (pp_result_qualif prover result)
- ) results ;
- end
-
- let cache_descr vc results =
- DISK.cache_descr (fun fmt -> pretty fmt vc results)
-
-end
-
module VC_Annot =
struct
type t = {
- (* Generally empty, but for Lemma sub-goals *)
+ (* Generally empty, but for Lemmas *)
axioms : Definitions.axioms option ;
goal : GOAL.t ;
tags : Splitter.tag list ;
@@ -367,6 +283,15 @@ struct
List.iter (fun tg -> Format.fprintf fmt "@ %a" Splitter.pretty tg) vc.tags ;
Format.fprintf fmt "@].@\n" ;
end ;
+ begin match vc.axioms with
+ | Some (_, depends) when depends <> [] ->
+ Format.fprintf fmt "@[<hov 2>@{<bf>Assume Lemmas@}:" ;
+ List.iter
+ (fun a -> Format.fprintf fmt "@ '%s'" a.lem_name)
+ depends ;
+ Format.fprintf fmt "@]@." ;
+ | _ -> ()
+ end ;
pp_warnings fmt vc.warn ;
Pcond.pretty fmt (GOAL.compute_descr ~pid vc.goal) ;
List.iter
@@ -378,19 +303,12 @@ struct
) results ;
end
- let cache_descr ~pid vc results =
- DISK.cache_descr (fun fmt -> pretty fmt pid vc results)
-
end
(* ------------------------------------------------------------------------ *)
(* --- Proof Obligations Database --- *)
(* ------------------------------------------------------------------------ *)
-type formula =
- | GoalLemma of VC_Lemma.t
- | GoalAnnot of VC_Annot.t
-
type po = t and t = {
po_gid : string ; (* goal identifier *)
po_sid : string ; (* goal short identifier (without model) *)
@@ -398,7 +316,7 @@ type po = t and t = {
po_idx : index ; (* goal index *)
po_model : WpContext.model ;
po_pid : WpPropId.prop_id ; (* goal target property *)
- po_formula : formula ; (* proof obligation *)
+ po_formula : VC_Annot.t ; (* proof obligation *)
}
let get_index w = w.po_idx
@@ -409,11 +327,13 @@ let get_scope w = match w.po_idx with
| Function(kf,_) -> WpContext.Kf kf
let get_context w = w.po_model , get_scope w
-let get_depend = function
- | { po_formula = GoalAnnot { VC_Annot.deps = ips } } ->
- Property.Set.elements ips
- | { po_formula = GoalLemma { VC_Lemma.depends = ips } } ->
- List.map LogicUsage.ip_lemma ips
+let get_depend wpo =
+ let open LogicUsage in
+ let deps = wpo.po_formula.deps in
+ let axioms = wpo.po_formula.axioms in
+ List.rev_append
+ (Option.fold ~none:[] ~some:(fun (_, l) -> List.map ip_lemma l) axioms)
+ (Property.Set.elements deps)
let get_file_logout w prover =
DISK.file_logout ~pid:w.po_pid ~model:(get_model w) ~prover
@@ -472,7 +392,7 @@ module S =
po_gid = "";
po_model = WpContext.MODEL.repr ;
po_name = "dummy";
- po_formula = GoalAnnot VC_Annot.repr ;
+ po_formula = VC_Annot.repr ;
}]
end)
(* to get a "reasonable" API doc: *)
@@ -511,9 +431,7 @@ let get_gid g = g.po_gid
let get_property g = WpPropId.property_of_id g.po_pid
let qed_time wpo =
- match wpo.po_formula with
- | GoalLemma _ -> 0.0
- | GoalAnnot { VC_Annot.goal = g } -> GOAL.qed_time g
+ GOAL.qed_time wpo.po_formula.goal
(* -------------------------------------------------------------------------- *)
(* --- Proof Collector --- *)
@@ -716,9 +634,7 @@ let remove g =
removed g ;
end
-let warnings = function
- | { po_formula = GoalAnnot vcq } -> vcq.VC_Annot.warn
- | { po_formula = GoalLemma _ } -> []
+let warnings wpo = wpo.po_formula.VC_Annot.warn
let get_target g = WpPropId.property_of_id g.po_pid
@@ -813,17 +729,11 @@ let get_results g =
with Not_found -> []
let is_trivial g =
- match g.po_formula with
- | GoalLemma vc -> VC_Lemma.is_trivial vc
- | GoalAnnot vc -> VC_Annot.is_trivial vc
+ VC_Annot.is_trivial g.po_formula
let reduce g =
- match g.po_formula with
- | GoalLemma vc ->
- WpContext.on_context (get_context g) VC_Lemma.is_trivial vc
- | GoalAnnot vc ->
- let pid = g.po_pid in
- WpContext.on_context (get_context g) (VC_Annot.resolve ~pid) vc
+ let pid = g.po_pid in
+ WpContext.on_context (get_context g) (VC_Annot.resolve ~pid) g.po_formula
let resolve g =
let valid = reduce g in
@@ -833,24 +743,16 @@ let resolve g =
else false
let computed g =
- match g.po_formula with
- | GoalAnnot { VC_Annot.goal = goal } ->
- GOAL.is_computed goal
- | GoalLemma _ -> false
+ GOAL.is_computed g.po_formula.goal
let compute g =
let ctxt = get_context g in
- match g.po_formula with
- | GoalAnnot { VC_Annot.axioms ; VC_Annot.goal = goal } ->
- let pid = g.po_pid in
- axioms ,
- let qed = GOAL.is_computed goal in
- let seq = WpContext.on_context ctxt (GOAL.compute_descr ~pid) goal in
- if not qed then modified g ; seq
- | GoalLemma ({ VC_Lemma.depends = depends ; VC_Lemma.lemma = lemma } as w) ->
- let open Definitions in
- Some( lemma.l_cluster , depends ) ,
- WpContext.on_context ctxt VC_Lemma.sequent w
+ let pid = g.po_pid in
+ g.po_formula.axioms ,
+ let goal = g.po_formula.goal in
+ let qed = GOAL.is_computed goal in
+ let seq = WpContext.on_context ctxt (GOAL.compute_descr ~pid) goal in
+ if not qed then modified g ; seq
let is_valid g =
is_trivial g || List.exists (fun (_,r) -> VCS.is_valid r) (get_results g)
@@ -878,13 +780,7 @@ let has_unknown g =
let pp_title fmt w = Format.pp_print_string fmt w.po_name
let pp_goal_model fmt w =
- begin
- match w.po_formula with
- | GoalAnnot vcq ->
- VC_Annot.pretty fmt w.po_pid vcq (get_results w)
- | GoalLemma vca ->
- VC_Lemma.pretty fmt vca (get_results w)
- end
+ VC_Annot.pretty fmt w.po_pid w.po_formula (get_results w)
let pp_goal fmt w = WpContext.on_context (get_context w) (pp_goal_model fmt) w
@@ -973,39 +869,6 @@ let goals_of_property prop =
let get_model w = w.po_model
-let get_logfile w prover result =
- let model = get_model w in
- DISK.cache_log ~pid:w.po_pid ~model ~prover ~result
-
-let pp_logfile fmt w prover =
- let model = get_model w in
- let result = get_result w prover in
- DISK.pretty ~pid:w.po_pid ~model ~prover ~result fmt
-
-let is_computing = function VCS.Computing _ -> true | _ -> false
-
-let get_files w =
- let results = get_results w in
- let descr_files = match w.po_formula with
- | GoalAnnot vcq ->
- [ "Goal" , VC_Annot.cache_descr ~pid:w.po_pid vcq results ]
- | GoalLemma vca ->
- [ "Lemma" , VC_Lemma.cache_descr vca results ]
- in
- let result_files =
- List.fold_right
- (fun (prover,result) files ->
- if prover <> VCS.Qed && not (is_computing result.verdict) then
- let filename = get_logfile w prover result in
- if filename <> "" && Sys.file_exists filename then
- let title = title_of_prover prover in
- (title,filename) :: files
- else files
- else files
- ) results []
- in
- descr_files @ result_files
-
(* -------------------------------------------------------------------------- *)
(* --- Generators --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/wpo.mli b/src/plugins/wp/wpo.mli
index ee373c54bc5..62cb7a1f1fe 100644
--- a/src/plugins/wp/wpo.mli
+++ b/src/plugins/wp/wpo.mli
@@ -20,7 +20,6 @@
(* *)
(**************************************************************************)
-open LogicUsage
open VCS
open Cil_types
open Cil_datatype
@@ -36,14 +35,7 @@ type index =
module DISK :
sig
- val cache_log : pid:prop_id -> model:WpContext.model ->
- prover:prover -> result:result -> string
- val pretty : pid:prop_id -> model:WpContext.model ->
- prover:prover -> result:result -> Format.formatter -> unit
- val file_kf : kf:kernel_function -> model:WpContext.model -> prover:prover -> string
val file_goal : pid:prop_id -> model:WpContext.model -> prover:prover -> string
- val file_logout : pid:prop_id -> model:WpContext.model -> prover:prover -> string
- val file_logerr : pid:prop_id -> model:WpContext.model -> prover:prover -> string
end
module GOAL :
@@ -62,24 +54,10 @@ sig
val qed_time : t -> float
end
-module VC_Lemma :
-sig
-
- type t = {
- lemma : Definitions.dlemma ;
- depends : logic_lemma list ;
- mutable sequent : Conditions.sequent option ;
- }
-
- val is_trivial : t -> bool
- val cache_descr : t -> (prover * result) list -> string
-
-end
-
module VC_Annot :
sig
-
type t = {
+ (* Generally empty, but for Lemmas *)
axioms : Definitions.axioms option ;
goal : GOAL.t ;
tags : Splitter.tag list ;
@@ -91,7 +69,6 @@ sig
val is_trivial : t -> bool
val resolve : pid:prop_id -> t -> bool
- val cache_descr : pid:prop_id -> t -> (prover * result) list -> string
end
@@ -99,10 +76,6 @@ end
(**{1 Proof Obligations} *)
(* ------------------------------------------------------------------------ *)
-type formula =
- | GoalLemma of VC_Lemma.t
- | GoalAnnot of VC_Annot.t
-
type po = t and t = {
po_gid : string ; (** goal identifier *)
po_sid : string ; (** goal short identifier (without model) *)
@@ -110,7 +83,7 @@ type po = t and t = {
po_idx : index ; (** goal index *)
po_model : WpContext.model ;
po_pid : WpPropId.prop_id ; (* goal target property *)
- po_formula : formula ; (* proof obligation *)
+ po_formula : VC_Annot.t ; (* proof obligation *)
}
module S : Datatype.S_with_collections with type t = po
@@ -130,8 +103,6 @@ val get_file_logout : t -> prover -> string
val get_file_logerr : t -> prover -> string
(** only filename, might not exists *)
-val get_files : t -> (string * string) list
-
val qed_time : t -> float
val clear : unit -> unit
@@ -220,7 +191,6 @@ val iter :
val iter_on_goals: (t -> unit) -> unit
val goals_of_property: Property.t -> t list
-val bar : string
val kf_context : index -> Description.kf
val pp_index : Format.formatter -> index -> unit
val pp_warnings : Format.formatter -> Warning.t list -> unit
@@ -229,7 +199,6 @@ val pp_dependency : Description.kf -> Format.formatter -> Property.t -> unit
val pp_dependencies : Description.kf -> Format.formatter -> Property.t list -> unit
val pp_goal : Format.formatter -> t -> unit
val pp_title : Format.formatter -> t -> unit
-val pp_logfile : Format.formatter -> t -> prover -> unit
val pp_axiomatics : Format.formatter -> string option -> unit
val pp_function : Format.formatter -> Kernel_function.t -> string option -> unit
--
GitLab