Commit 4eb59010 authored by MARCHE Claude's avatar MARCHE Claude

test using API directly

parent a45530b0
......@@ -554,7 +554,7 @@ install::
.PHONY: bench test
bench:: bin/why.@OCAMLBEST@ bin/whyml.@OCAMLBEST@ $(TOOLS) $(DRIVERS)
bench:: bin/why.@OCAMLBEST@ bin/whyml.@OCAMLBEST@ $(TOOLS) $(DRIVERS) test-api
sh bench/bench \
"bin/why.@OCAMLBEST@" \
"bin/whyml.@OCAMLBEST@"
......@@ -602,6 +602,10 @@ testl: bin/whyml.byte
testl-type: bin/whyml.byte
ocamlrun -bt bin/whyml.byte --type-only tests/test-pgm-jcf.mlw
test-api: src/why.cma
ocaml unix.cma str.cma nums.cma dynlink.cma ocamlgraph/graph.cma \
src/why.cma -I src examples/use_api.ml
## install: install-binary install-lib install-man
##
......
......@@ -137,7 +137,7 @@ echo "ocaml version is $OCAMLVERSION"
case "$OCAMLVERSION" in
0.*|1.*|2.*|3.0*)
AC_MSG_ERROR(You need Objective Caml 3.10 or later);;
AC_MSG_ERROR(You need Objective Caml 3.10 or higher);;
3.10*)
enable_plugins=no;;
esac
......
(*
*)
open Why
open Format
(***************
This file builds some goals using the API and calls
the alt-ergo prover to check them
******************)
(* First, we need to access the Why configuration *)
let config = Whyconf.read_config None
let main = Whyconf.get_main config
let env = Env.create_env (Lexer.retrieve main.Whyconf.loadpath)
let provers = Whyconf.get_provers config
let alt_ergo =
try
Util.Mstr.find "alt-ergo" provers
with Not_found ->
eprintf "Prover alt-ergo not installed or not configured@.";
failwith "Cannot continue without alt-ergo installed"
let alt_ergo_driver = Driver.load_driver env alt_ergo.Whyconf.driver
(*
a ground propositional goal: True or False
*)
let fmla_true = Term.f_true
let fmla_false = Term.f_false
let fmla1 = Term.f_or fmla_true fmla_false
let () = printf "@[formula 1 created:@ %a@]@." Pretty.print_fmla fmla1
let task1 = None
let goal_id1 = Decl.create_prsymbol (Ident.id_fresh "goal1")
let task1 = Task.add_prop_decl task1 Decl.Pgoal goal_id1 fmla1
let () = printf "@[task 1 created:@\n%a@]@." Pretty.print_task task1
let result1 =
Driver.prove_task ~command:alt_ergo.Whyconf.command
alt_ergo_driver task1 ()
let () = printf "@[On task 1, alt-ergo answers %a@."
Call_provers.print_prover_result result1
(*
a propositional goal: A and B implies B
*)
let prop_var_A = Term.create_psymbol (Ident.id_fresh "A") []
let prop_var_B = Term.create_psymbol (Ident.id_fresh "B") []
let fmla_A = Term.f_app prop_var_A []
let fmla_B = Term.f_app prop_var_B []
let fmla2 = Term.f_implies (Term.f_and fmla_A fmla_B) fmla_B
let () = printf "@[formula 2 created:@ %a@]@." Pretty.print_fmla fmla2
let task2 = None
let task2 = Task.add_logic_decl task2 [prop_var_A, None]
let task2 = Task.add_logic_decl task2 [prop_var_B, None]
let goal_id2 = Decl.create_prsymbol (Ident.id_fresh "goal2")
let task2 = Task.add_prop_decl task2 Decl.Pgoal goal_id2 fmla2
let () = printf "@[task 2 created:@\n%a@]@." Pretty.print_task task2
let result2 =
Driver.prove_task ~command:alt_ergo.Whyconf.command
alt_ergo_driver task2 ()
let () = printf "@[On task 2, alt-ergo answers %a@."
Call_provers.print_prover_result result2
(*
An arithmetic goal: 2+2 = 4
*)
let two = Term.t_const (Term.ConstInt "2")
let four = Term.t_const (Term.ConstInt "4")
let int_theory = Env.find_theory env ["int"] "Int"
let plus_symbol = Theory.ns_find_ls int_theory.Theory.th_export ["infix +"]
let two_plus_two = Term.t_app plus_symbol [two;two] Ty.ty_int
let fmla3 = Term.f_equ two_plus_two four
let task3 = None
let task3 = Task.use_export task3 int_theory
let goal_id3 = Decl.create_prsymbol (Ident.id_fresh "goal3")
let task3 = Task.add_prop_decl task3 Decl.Pgoal goal_id3 fmla3
let () = printf "@[task 3 created:@\n%a@]@." Pretty.print_task task3
let result3 =
Driver.prove_task ~command:alt_ergo.Whyconf.command
alt_ergo_driver task3 ()
let () = printf "@[On task 3, alt-ergo answers %a@."
Call_provers.print_prover_result result3
(* build a theory with all these goals *)
......@@ -19,6 +19,12 @@
open Util
(** Labels *)
type label = string * Loc.position option
let label ?loc s = (s,loc)
(** Identifiers *)
type ident = {
......
......@@ -17,7 +17,13 @@
(* *)
(**************************************************************************)
(** Identifiers *)
(** {2 Labels} *)
type label = string * Loc.position option
val label : ?loc:Loc.position -> string -> label
(** {2 Identifiers} *)
type ident = private {
id_string : string; (* non-unique name *)
......
......@@ -252,12 +252,6 @@ let rec pat_gen_fold fnT fnV fnL acc pat =
| Por (p, q) -> fn (fn acc p) q
| Pas (p, v) -> fn (fnV acc v) p
(** Labels *)
type label = string * Loc.position option
let label ?loc s = (s,loc)
(** Terms and formulas *)
type quant =
......
......@@ -103,12 +103,6 @@ val pat_fold : ('a -> pattern -> 'a) -> 'a -> pattern -> 'a
val pat_all : (pattern -> bool) -> pattern -> bool
val pat_any : (pattern -> bool) -> pattern -> bool
(** {2 Labels} *)
type label = string * Loc.position option
val label : ?loc:Loc.position -> string -> label
(** {2 Terms and formulas} *)
type quant =
......
......@@ -47,7 +47,7 @@ let default_ide =
ide_tree_width = 512;
ide_task_height = 384;
ide_verbose = 0;
ide_default_editor = ""; (*TODO : editor? *)
ide_default_editor = "";
}
let load_ide section =
......@@ -89,19 +89,19 @@ let load_config config =
| Some s -> load_ide s in
let provers = get_provers config in
let env = Env.create_env (Lexer.retrieve main.loadpath) in
{ window_height = ide.ide_window_height;
window_width = ide.ide_window_width;
tree_width = ide.ide_tree_width;
task_height = ide.ide_task_height;
time_limit = main.Whyconf.timelimit;
mem_limit = main.Whyconf.memlimit;
verbose = ide.ide_verbose;
max_running_processes = main.Whyconf.running_provers_max;
provers = Mstr.fold (get_prover_data env) provers [];
default_editor = ide.ide_default_editor;
config = config;
env = env
}
{ window_height = ide.ide_window_height;
window_width = ide.ide_window_width;
tree_width = ide.ide_tree_width;
task_height = ide.ide_task_height;
time_limit = main.Whyconf.timelimit;
mem_limit = main.Whyconf.memlimit;
verbose = ide.ide_verbose;
max_running_processes = main.Whyconf.running_provers_max;
provers = Mstr.fold (get_prover_data env) provers [];
default_editor = ide.ide_default_editor;
config = config;
env = env
}
let read_config () =
let config = Whyconf.read_config None in
......
......@@ -60,7 +60,7 @@ and dterm_node =
| Tif of dfmla * dterm * dterm
| Tlet of dterm * ident * dterm
| Tmatch of dterm * (dpattern * dterm) list
| Tnamed of label * dterm
| Tnamed of Ident.label * dterm
| Teps of ident * dty * dfmla
and dfmla =
......@@ -73,7 +73,7 @@ and dfmla =
| Fif of dfmla * dfmla * dfmla
| Flet of dterm * ident * dfmla
| Fmatch of dterm * (dpattern * dfmla) list
| Fnamed of label * dfmla
| Fnamed of Ident.label * dfmla
| Fvar of fmla
and dtrigger =
......
......@@ -405,12 +405,12 @@ lexpr:
| lexpr OR lexpr
{ infix_pp $1 PPor $3 }
| lexpr ASYM_OR lexpr
{ let label = Term.label "asym_split" in
{ let label = Ident.label "asym_split" in
mk_pp (PPnamed (label, infix_pp $1 PPor $3)) }
| lexpr AND lexpr
{ infix_pp $1 PPand $3 }
| lexpr ASYM_AND lexpr
{ let label = Term.label "asym_split" in
{ let label = Ident.label "asym_split" in
mk_pp (PPnamed (label, infix_pp $1 PPand $3)) }
| NOT lexpr
{ prefix_pp PPnot $2 }
......@@ -444,7 +444,7 @@ lexpr:
| EXISTS list1_param_var_sep_comma triggers DOT lexpr
{ mk_pp (PPquant (PPexists, $2, $3, $5)) }
| STRING lexpr %prec prec_named
{ mk_pp (PPnamed (Term.label ~loc:(loc ()) $1, $2)) }
{ mk_pp (PPnamed (Ident.label ~loc:(loc ()) $1, $2)) }
| LET pattern EQUAL lexpr IN lexpr
{ match $2.pat_desc with
| PPpvar id -> mk_pp (PPlet (id, $4, $6))
......
......@@ -25,7 +25,7 @@ type loc = Loc.position
type real_constant = Term.real_constant
type constant = Term.constant
type label = Term.label
type label = Ident.label
type pp_quant =
| PPforall | PPexists
......
......@@ -391,6 +391,7 @@ let proof_end = "(* DO NOT EDIT BELOW *)"
let print_empty_proof fmt =
fprintf fmt "%s@\n" proof_begin;
fprintf fmt "intuition.@\n";
fprintf fmt "@\n";
fprintf fmt "Qed.@\n";
fprintf fmt "%s@\n" proof_end
......
......@@ -35,7 +35,7 @@ let split_case spl c acc tl bl =
in
apply_append (f_case tl) acc bll
let asym_split = Term.label "asym_split"
let asym_split = Ident.label "asym_split"
let to_split f = List.exists (fun (l,_) -> l = "asym_split") f.f_label
......
......@@ -17,7 +17,7 @@
(* *)
(**************************************************************************)
val asym_split : Term.label
val asym_split : Ident.label
val split_pos : Term.fmla list -> Term.fmla -> Term.fmla list
val split_neg : Term.fmla list -> Term.fmla -> Term.fmla list
......
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