Commit d4484d2e authored by MARCHE Claude's avatar MARCHE Claude

Completed support for counter-examples provided by Alt-Ergo 0.95

parent 762a4dfb
import "alt_ergo_bare.drv"
theory BuiltIn
meta "eliminate_algebraic" "keep_enums"
meta "eliminate_algebraic" "keep_recs"
meta "printer_option" "show_labels"
end
theory map.Map
syntax type map "(%1,%2) farray"
syntax function get "(%1[%2])"
syntax function set "(%1[%2 <- %3])"
remove prop Select_eq
remove prop Select_neq
end
(*
Local Variables:
mode: why
compile-command: "make -C .. bench"
End:
*)
module M1
use import int.Int
let f (x:int) : int =
{ }
if x >= 42 then x + 3 else 0
{ result <= 50 }
end
......@@ -6,14 +6,71 @@
id="0"
name="Alt-Ergo"
version="0.95-dev"/>
<file
name="../alt-ergo-models.mlw"
verified="false"
expanded="true">
<theory
name="WP M1"
locfile="alt-ergo-models/../alt-ergo-models.mlw"
loclnum="2" loccnumb="7" loccnume="9"
verified="false"
expanded="true">
<goal
name="WP_parameter f"
locfile="alt-ergo-models/../alt-ergo-models.mlw"
loclnum="6" loccnumb="6" loccnume="7"
expl="normal postcondition"
sum="a0d81048eafffca9c2034507529acd5c"
proved="false"
expanded="true"
shape="ainfix &lt;=iainfix &gt;=V0c42ainfix +V0c3c0c50F">
<label
name="expl:parameter f"/>
<proof
prover="0"
timelimit="5"
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
</proof>
<transf
name="split_goal"
proved="false"
expanded="true">
<goal
name="WP_parameter f.0"
locfile="alt-ergo-models/../alt-ergo-models.mlw"
loclnum="6" loccnumb="6" loccnume="7"
expl="normal postcondition"
sum="a0d81048eafffca9c2034507529acd5c"
proved="false"
expanded="true"
shape="ainfix &lt;=iainfix &gt;=V0c42ainfix +V0c3c0c50F">
<label
name="expl:parameter f"/>
<proof
prover="0"
timelimit="5"
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
</proof>
</goal>
</transf>
</goal>
</theory>
</file>
<file
name="../alt-ergo-models.why"
verified="false"
expanded="true">
<theory
name="T"
name="T1"
locfile="alt-ergo-models/../alt-ergo-models.why"
loclnum="2" loccnumb="7" loccnume="8"
loclnum="2" loccnumb="7" loccnume="9"
verified="false"
expanded="true">
<goal
......@@ -28,7 +85,30 @@
prover="0"
timelimit="5"
memlimit="0"
edited="altmnergomnmodels-T-G_4.why"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
</proof>
</goal>
</theory>
<theory
name="T2"
locfile="alt-ergo-models/../alt-ergo-models.why"
loclnum="10" loccnumb="7" loccnume="9"
verified="false"
expanded="true">
<goal
name="g"
locfile="alt-ergo-models/../alt-ergo-models.why"
loclnum="16" loccnumb="7" loccnume="8"
sum="48acce19ca5523eaf2c70c5691e994a9"
proved="false"
expanded="true"
shape="ainfix &gt;=axV0F">
<proof
prover="0"
timelimit="5"
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
......
......@@ -16,7 +16,7 @@ version_bad = "0.91"
version_bad = "0.9"
version_bad = "0.8"
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -model %f"
driver = "drivers/alt_ergo.drv"
driver = "drivers/alt_ergo_0.95.drv"
editor = "altgr-ergo"
[ATP alt-ergo]
......
......@@ -30,6 +30,16 @@ open Task
open Printer
let meta_ac = Theory.register_meta "AC" [Theory.MTlsymbol]
let meta_printer_option = Theory.register_meta "printer_option" [Theory.MTstring]
type info = {
info_syn : syntax_map;
info_ac : Sls.t;
info_show_labels : bool;
info_csm : lsymbol list Mls.t;
info_pjs : Sls.t;
info_axs : Spr.t;
}
let ident_printer =
let bls = [
......@@ -49,10 +59,8 @@ let print_ident fmt id =
let print_label fmt l =
fprintf fmt "\"%s\"" l.lab_string
let version_0_95 = false (* TODO *)
let print_ident_label fmt id =
if version_0_95 then
let print_ident_label info fmt id =
if info.info_show_labels then
fprintf fmt "%s %a"
(id_unique ident_printer id)
(print_list space print_label) (Slab.elements id.id_label)
......@@ -70,14 +78,6 @@ let print_tvsymbol fmt tv =
let forget_tvs () = forget_all tv_printer
type info = {
info_syn : syntax_map;
info_ac : Sls.t;
info_csm : lsymbol list Mls.t;
info_pjs : Sls.t;
info_axs : Spr.t;
}
let rec print_type info fmt ty = match ty.ty_node with
| Tyvar id ->
print_tvsymbol fmt id
......@@ -135,7 +135,7 @@ and print_tapp info fmt = function
| tl -> fprintf fmt "(%a)" (print_list comma (print_term info)) tl
let rec print_fmla info fmt f =
if version_0_95 then
if info.info_show_labels then
match Slab.elements f.t_label with
| [] -> print_fmla_node info fmt f
| l ->
......@@ -160,7 +160,8 @@ and print_fmla_node info fmt f = match f.t_node with
| Texists -> "exists", [] (* Alt-ergo has no triggers for exists *)
in
let forall fmt v =
fprintf fmt "%s %a:%a" q print_ident_label v.vs_name (print_type info) v.vs_ty
fprintf fmt "%s %a:%a" q (print_ident_label info) v.vs_name
(print_type info) v.vs_ty
in
fprintf fmt "@[(%a%a.@ %a)@]" (print_list dot forall) vl
(print_triggers info) tl (print_fmla info) f;
......@@ -307,6 +308,20 @@ let add_projection (csm,pjs,axs) = function
csm, Sls.add ls pjs, Spr.add pr axs
| _ -> assert false
let check_showlabels acc l =
match l with
| [Theory.MAstr s] ->
begin match s with
| "show_labels" ->
eprintf "printer_option show_labels set@.";
true
| _ ->
eprintf "printer_option %s ignored@." s;
acc
end
| _ -> assert false
(*
let print_task_old pr thpr fmt task =
print_prelude fmt pr;
print_th_prelude task fmt thpr;
......@@ -315,6 +330,8 @@ let print_task_old pr thpr fmt task =
let info = {
info_syn = get_syntax_map task;
info_ac = Task.on_tagged_ls meta_ac task;
info_show_labels =
Task.on_meta meta_printer_option check_showlabels false task;
info_csm = Mls.map Array.to_list csm;
info_pjs = pjs;
info_axs = axs;
......@@ -326,22 +343,26 @@ let () = register_printer "alt-ergo-old"
(fun _env pr thpr ?old:_ fmt task ->
forget_all ident_printer;
print_task_old pr thpr fmt task)
*)
let print_decls =
let print ac csm pjs axs sm fmt d =
let print ac sl csm pjs axs sm fmt d =
let info = {
info_syn = sm;
info_ac = ac;
info_show_labels = sl;
info_csm = Mls.map Array.to_list csm;
info_pjs = pjs;
info_axs = axs;
} in
print_decl info fmt d in
Trans.on_tagged_ls meta_ac (fun ac ->
Trans.on_meta meta_printer_option (fun args ->
let sl = List.fold_left check_showlabels false args in
Trans.on_meta Eliminate_algebraic.meta_proj (fun mal ->
let csm,pjs,axs = List.fold_left
add_projection (Mls.empty,Sls.empty,Spr.empty) mal in
Printer.sprint_decls (print ac csm pjs axs)))
Printer.sprint_decls (print ac sl csm pjs axs))))
let print_task _env pr thpr ?old:_ fmt task =
(* In trans-based p-printing [forget_all] is a no-no *)
......
Markdown is supported
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