Commit 54887600 authored by MARCHE Claude's avatar MARCHE Claude Committed by Clément Fumex

ITP: attempt to generate a 'sequent' data structure instead of printing

parent 6181688e
......@@ -1566,6 +1566,10 @@ bench:: bin/why3.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ plugins $(TOOLS) \
# test targets
###############
test-itp.opt: src/printer/itp.ml lib/why3/why3.cmxa
$(if $(QUIET),@echo 'Ocamlopt $<' &&) \
$(OCAMLOPT) -o $@ -I lib/why3 $(INCLUDES) $(EXTCMXA) lib/why3/why3.cmxa $<
test-api-logic.byte: examples/use_api/logic.ml lib/why3/why3.cma
$(if $(QUIET),@echo 'Ocaml $<' &&) \
ocaml -I lib/why3 $(INCLUDES) $(EXTCMA) lib/why3/why3.cma $< > /dev/null \
......
open Why3
(* reads the config file *)
let config : Whyconf.config = Whyconf.read_config None
(* the [main] section of the config file *)
let main : Whyconf.main = Whyconf.get_main config
(* builds the environment from the [loadpath] *)
let env : Env.env = Env.create_env (Whyconf.loadpath main)
open Ident
open Term
open Decl
type element = Formula of string * term | Symbol of lsymbol
type sequent = (Loc.position option * element) list
type itp_state = sequent list
(* or a tree ? *)
(*
a "tactic" should be any function of type sequent -> sequent list
applying a tactic :
apply state tactic =
let s = pop first sequnt from state
not right if the state is a tree
*)
let extract_decl acc d =
match d.d_node with
| Dtype _ -> acc
| Ddata _ -> acc
| Dparam ls -> (ls.ls_name.id_loc,Symbol ls) :: acc
| Dlogic ld ->
List.fold_left (fun acc (ls,_) -> (ls.ls_name.id_loc,Symbol ls) :: acc) acc ld
| Dind (_,ld) ->
List.fold_left (fun acc (ls,_) -> (ls.ls_name.id_loc,Symbol ls) :: acc) acc ld
| Dprop (k,pr,t) ->
let name = match k with
| Plemma | Paxiom -> pr.pr_name.id_string
| Pgoal -> ""
| Pskip -> assert false
in
(t.t_loc,Formula (name,t)) :: acc
let build_sequent task =
let task = Trans.apply (Trans.goal Introduction.intros) task in
let ut = Task.used_symbols (Task.used_theories task) in
let ld = Task.local_decls task ut in
List.rev (List.fold_left extract_decl [] ld)
open Format
let print_elem fmt (loc,e) =
Opt.iter (fprintf fmt "[%a]" Pretty.print_loc) loc;
match e with
| Symbol ls -> fprintf fmt "%a@\n" Pretty.print_param_decl ls
| Formula (n,t) -> fprintf fmt "%s : %a@\n" n Pretty.print_term t
let print_sequent fmt s =
fprintf fmt "========================@\n";
List.iter (print_elem fmt) s;
fprintf fmt "========================@."
let test () =
let file = Sys.argv.(1) in
printf "Reading file %s@." file;
let theories = Env.read_file Env.base_language env file in
let tasks =
Stdlib.Mstr.fold
(fun _k th acc ->
let tasks = Task.split_theory th None None in
let tasks =
List.fold_left
(fun acc task ->
let tasks = Trans.apply Split_goal.split_goal_wp task in
List.fold_left
(fun acc task ->
let task = Trans.apply (Trans.goal Introduction.intros) task in
task :: acc)
acc (List.rev tasks))
acc tasks
in
tasks) theories []
in
let sequents = List.map build_sequent tasks in
List.iter (print_sequent Format.std_formatter) sequents
let () = Printexc.catch test ()
......@@ -9,17 +9,17 @@ module BinaryMultiplication
let binary_mult (a b: int)
requires { b >= 0 }
ensures { result = a * b }
ensures { result = a - b }
= let x = ref a in
let y = ref b in
let z = ref 0 in
while !y <> 0 do
invariant { 0 <= !y }
invariant { !z + !x * !y = a * b }
invariant { !z + !x - !y = a - b }
variant { !y }
if odd !y then z := !z + !x;
x := 2 * !x;
y := !y / 2
if !y <> 1 then z := !z + !x;
x := 2 - !x;
y := !y - 2
done;
!z
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="1" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<file name="../test_itp.mlw" expanded="true">
<theory name="BinaryMultiplication" sum="18d9b523d8c709e361c954d7b3ddb1ef" expanded="true">
<goal name="l" expanded="true">
</goal>
<goal name="WP_parameter binary_mult" expl="VC for binary_mult" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter binary_mult.1" expl="1. loop invariant init" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter binary_mult.2" expl="2. loop invariant init">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter binary_mult.3" expl="3. check division by zero">
<proof prover="0"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter binary_mult.4" expl="4. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter binary_mult.5" expl="5. loop invariant preservation" expanded="true">
<proof prover="0"><result status="highfailure" time="0.02"/></proof>
<proof prover="1"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="WP_parameter binary_mult.6" expl="6. loop variant decrease">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter binary_mult.7" expl="7. check division by zero">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter binary_mult.8" expl="8. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter binary_mult.9" expl="9. loop invariant preservation">
<proof prover="0"><result status="timeout" time="5.02"/></proof>
</goal>
<goal name="WP_parameter binary_mult.10" expl="10. loop variant decrease">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter binary_mult.11" expl="11. postcondition">
<proof prover="0"><result status="valid" time="0.00"/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
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