Commit 2962213b authored by MARCHE Claude's avatar MARCHE Claude
Browse files

why3 printer: forget names of bound variables

It remains to remove all occurences of Trans.
parent 6164fd5f
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 ()
......@@ -50,9 +50,7 @@ let print_tv tables fmt tv =
let print_vs tables fmt vs =
fprintf fmt "%s" (id_unique tables vs.vs_name)
(*
let forget_var vs = forget_id iprinter vs.vs_name
*)
let forget_var tables vs = forget_id tables.printer vs.vs_name
(* theory names always start with an upper case letter *)
let print_th tables fmt th =
......@@ -192,7 +190,8 @@ and print_tnode pri tables fmt t = match t.t_node with
| Tlet (t1,tb) ->
let v,t2 = t_open_bound tb in
fprintf fmt (protect_on (pri > 0) "let %a = @[%a@] in@ %a")
(print_vs tables) v (print_lterm 4 tables) t1 (print_term tables) t2
(print_vs tables) v (print_lterm 4 tables) t1 (print_term tables) t2;
forget_var tables v
| Tcase (t1,bl) ->
fprintf fmt "match @[%a@] with@\n@[<hov>%a@]@\nend"
(print_term tables) t1 (print_list newline (print_tbranch tables)) bl
......@@ -205,11 +204,13 @@ and print_tnode pri tables fmt t = match t.t_node with
end else begin
fprintf fmt (protect_on (pri > 0) "\\ %a%a.@ %a")
(print_list comma (print_vsty tables)) vl (print_tl tables) tl (print_term tables) e
end
end;
List.iter (forget_var tables) vl
| Tquant (q,fq) ->
let vl,tl,f = t_open_quant fq in
fprintf fmt (protect_on (pri > 0) "%a %a%a.@ %a") print_quant q
(print_list comma (print_vsty tables)) vl (print_tl tables) tl (print_term tables) f
(print_list comma (print_vsty tables)) vl (print_tl tables) tl (print_term tables) f;
List.iter (forget_var tables) vl
| Ttrue ->
fprintf fmt "true"
| Tfalse ->
......@@ -224,7 +225,8 @@ and print_tnode pri tables fmt t = match t.t_node with
and print_tbranch tables fmt br =
let p,t = t_open_branch br in
fprintf fmt "@[<hov 4>| %a ->@ %a@]" (print_pat tables) p (print_term tables) t
fprintf fmt "@[<hov 4>| %a ->@ %a@]" (print_pat tables) p (print_term tables) t;
Svs.iter (forget_var tables) p.pat_vars
and print_tl tables fmt tl =
if tl = [] then () else fprintf fmt "@ [%a]"
......@@ -298,7 +300,8 @@ let print_logic_decl fst tables fmt (ls,ld) =
(print_ls_kind ~fst) ls (print_ls tables) ls
print_ident_labels ls.ls_name
(print_list nothing (print_vs_arg tables)) vl
(print_option (print_ls_type tables)) ls.ls_value (print_term tables) e
(print_option (print_ls_type tables)) ls.ls_value (print_term tables) e;
List.iter (forget_var tables) vl
let print_logic_decl first tables fmt d =
if not (query_remove (fst d).ls_name) then
......@@ -423,9 +426,6 @@ let print_sequent _args ?old:_ fmt =
info := {info_syn = sm; itp = true};
Trans.store
(fun task ->
(*
let task = Trans.apply (Trans.goal Introduction.intros) task in
*)
(* print_th_prelude task fmt args.th_prelude; *)
let tables = build_name_tables task in
let ut = Task.used_symbols (Task.used_theories task) in
......
module Power
use import int.Int
function power int int : int
axiom power_0 : forall x:int. power x 0 = 1
axiom power_s : forall x n:int. n >= 0 ->
power x (n+1) = x * power x n
(* turn the following lemma into a lemma function : *)
lemma power_1 : forall x:int. power x 1 = x
(* idem *)
lemma sqrt4_256 : exists x:int. power x 4 = 256
(* idem *)
lemma power_sum : forall x n m: int.
0 <= n /\ 0 <= m ->
power x (n+m) = power x n * power x m
(* Fermat's little theorem for n = 3 *)
lemma power_0_left : forall n. n >= 1 -> power 0 n = 0
lemma power_3 : forall x. x >= 1 ->
power (x-1) 3 = power x 3 - 3 * x * x + 3 * x - 1
let rec ghost little_fermat_3 (x : int) : int
requires { x >= 0 }
variant { x }
ensures { power x 3 - x = 3 * result }
= if x = 0 then 0
else let r = little_fermat_3 (x-1) in
r + x * x - x
end
(*
Local Variables:
compile-command: "why3 ide lemma_functions.mlw"
End:
*)
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