Commit 8f9e020e authored by Loïc Correnson's avatar Loïc Correnson Committed by Allan Blanchard
Browse files

[wp] clarify results meaning wrt smoke tests

parent 04b9a4a7
......@@ -122,13 +122,13 @@ let set_saved t s = t.saved <- s
(* -------------------------------------------------------------------------- *)
let rec walk f node =
if not (Wpo.is_proved node.goal) then
if not (Wpo.is_valid node.goal) then
match node.script with
| Tactic (_,children) -> iter_all (walk f) children
| Opened | Script _ -> f node
let rec witer f node =
let proved = Wpo.is_proved node.goal in
let proved = Wpo.is_valid node.goal in
if proved then f ~proved node else
match node.script with
| Tactic (_,children) -> iter_all (witer f) children
......@@ -145,7 +145,7 @@ let iteri f tree =
(* --- Consolidating --- *)
(* -------------------------------------------------------------------------- *)
let proved n = Wpo.is_proved n.goal
let proved n = Wpo.is_valid n.goal
let pending n =
let k = ref 0 in
......@@ -168,7 +168,7 @@ let validate ?(incomplete=false) tree =
match tree.root with
| None -> ()
| Some root ->
if not (Wpo.is_proved tree.main) then
if not (Wpo.is_valid tree.main) then
if incomplete then
let result = consolidate root in
Wpo.set_result tree.main VCS.Tactical result
......@@ -217,7 +217,7 @@ type status = [
let status t : status =
match t.root with
| None ->
if Wpo.is_proved t.main
if Wpo.is_valid t.main
then if Wpo.is_smoke_test t.main then `Invalid else `Proved
else if Wpo.is_smoke_test t.main then `Passed else `Unproved
| Some root ->
......
......@@ -150,7 +150,7 @@ struct
ProofEngine.validate ~incomplete:true env.tree ;
if not env.signaled then
let wpo = ProofEngine.main env.tree in
let proved = Wpo.is_proved wpo in
let proved = Wpo.is_valid wpo in
if proved || finalize then
begin
env.signaled <- true ;
......
......@@ -40,7 +40,9 @@ 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_proved = Wpo.is_proved
let is_valid = Wpo.is_valid
let is_unknown = Wpo.is_unknown
let is_passed = Wpo.is_passed
let get_formula po =
match po.po_formula with
......
......@@ -47,7 +47,16 @@ val get_logerr : t -> prover -> string
val get_sequent : t -> Conditions.sequent
val get_formula: t -> Lang.F.pred
val is_trivial : t -> bool
val is_proved : t -> bool
(** One prover at least returns Valid verdict. *)
val is_valid : t -> bool
(** No prover with Valid verdict, and at least one non-Valid verdict. *)
val is_unknown : t -> bool
(** Same as [is_valid] for non-smoke tests. For smoke-tests,
same as [is_unknown]. *)
val is_passed : t -> bool
(** {2 Database}
Notice that a property or a function have no proof obligation until you
......
......@@ -128,7 +128,7 @@ class behavior
list#reload ;
let to_prove g =
not (Wpo.is_smoke_test g) &&
not (Wpo.is_proved g || Wpo.reduce g) in
not (Wpo.is_valid g || Wpo.reduce g) in
let has_proof g =
match ProofEngine.get g with
| `None -> false
......
......@@ -193,7 +193,7 @@ class printer (text : Wtext.text) =
| `Internal here | `Leaf(_,here) ->
begin
let root,path = rootchain here [here] in
let qed = if Wpo.is_proved (ProofEngine.main tree) then "Qed" else "End"
let qed = if Wpo.is_valid (ProofEngine.main tree) then "Qed" else "End"
in text#printf "@[<hv 0>@{<bf>Proof@}:%a@\n@{<bf>%s@}.@]@."
(self#proofstep ~prefix:" " ~direct:" " ~path ~here) root qed ;
end
......
......@@ -215,8 +215,8 @@ let add_results ~status (plist:pstats list) (wpo:Wpo.t) =
List.iter
(fun (p,r) ->
let re = result ~status ~smoke r in
let st = Wpo.get_steps r in
let tc = Wpo.get_time r in
let st = r.VCS.prover_steps in
let tc = r.VCS.prover_time in
let ts = r.VCS.solver_time in
if re <> NORESULT then
begin
......
......@@ -693,8 +693,6 @@ let warnings = function
| { po_formula = GoalAnnot vcq } -> vcq.VC_Annot.warn
| { po_formula = GoalLemma _ } -> []
let get_time = function { prover_time=t } -> t
let get_steps= function { prover_steps=n } -> n
let get_target g = WpPropId.property_of_id g.po_pid
let get_proof g =
......@@ -813,27 +811,20 @@ let compute g =
Some( lemma.l_cluster , depends ) ,
WpContext.on_context ctxt VC_Lemma.sequent w
let is_proved g =
let is_valid g =
is_trivial g || List.exists (fun (_,r) -> VCS.is_valid r) (get_results g)
let is_unknown g = List.exists
let is_unknown g =
not (is_valid g) &&
List.exists
(fun (_,r) -> VCS.is_verdict r && not (VCS.is_valid r))
( get_results g )
(get_results g)
let is_passed g =
if is_smoke_test g then
not (is_proved g)
is_unknown g
else
is_proved g
let get_result =
Dynamic.register ~plugin:"Wp" "Wpo.get_result"
(Datatype.func2 WpoType.ty ProverType.ty ResultType.ty)
get_result
let is_valid =
Dynamic.register ~plugin:"Wp" "Wpo.is_valid"
(Datatype.func ResultType.ty Datatype.bool) VCS.is_valid
is_valid g
(* -------------------------------------------------------------------------- *)
(* --- Proof Obligations : Pretty-printing --- *)
......
......@@ -158,33 +158,43 @@ val clear_results : t -> unit
val compute : t -> Definitions.axioms option * Conditions.sequent
(** Warning: Prover results are stored as they are from prover output,
without taking into consideration that validity is inverted
for smoke tests.
On the contrary, proof validity is computed with respect to
smoke test/non-smoke test.
*)
(** Definite result for this prover (not computing) *)
val has_verdict : t -> prover -> bool
(** Raw prover result (without any respect to smoke tests) *)
val get_result : t -> prover -> result
(** All raw prover results (without any respect to smoke tests) *)
val get_results : t -> (prover * result) list
(** Consolidated wrt to associated property and smoke test. *)
val get_proof : t -> [`Passed|`Failed|`Unknown] * Property.t
(** Associated property. *)
val get_target : t -> Property.t
val is_trivial : t -> bool
(** do not tries simplification, do not check prover results *)
(** Currently trivial sequent (no forced simplification) *)
val is_proved : t -> bool
(** do not tries simplification, check prover results *)
val is_valid : t -> bool
(** Checks for some prover with valid verdict (no forced simplification) *)
val is_unknown : t -> bool
(** at least one prover returns « Unknown » *)
(** Checks that all provers has a non-valid verdict *)
val is_passed : t -> bool
(** proved, or unknown for smoke tests *)
(** valid, or unknown for smoke tests *)
val warnings : t -> Warning.t list
(** [true] if the result is valid. Dynamically exported.
@since Nitrogen-20111001
*)
val is_valid: result -> bool
val get_time: result -> float
val get_steps: result -> int
val is_tactic : t -> bool
val is_smoke_test : t -> bool
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment