Commit 3a2b06b6 authored by Francois Bobot's avatar Francois Bobot

driver utilise register

parent f603a202
......@@ -231,6 +231,8 @@ bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS) $(BINARY) byte
--output-dir - --goal Test.G src/test.why
bin/why.$(OCAMLBEST) --driver bench/plugins/helloworld.drv -I lib/prelude/ \
--output-dir - --goal Test.G src/test.why
bin/why.$(OCAMLBEST) --driver bench/plugins/simplify_array.drv -I lib/prelude/ \
--output-file - --goal Test_simplify_array.G src/test.why
# installation
##############
......
let print_context _ fmt _ = Format.fprintf fmt "helloworld@\n"
let transform_context () = Transform.identity
let transform_context = Register.identity_trans
let () =
Driver.register_printer "helloworld" print_context;
......
......@@ -4,6 +4,13 @@ printer "why3"
filename "%f-%t-%s.why"
apply_after_split_goals
transformations
"simplify_array"
end
\ No newline at end of file
end
theory BuiltIn
syntax type int "int"
syntax type real "real"
syntax logic (_=_) "(%1 = %2)"
syntax logic (_<>_) "(%1 <> %2)"
end
open Term
open Termlib
open Theory
open Env
let prelude = ["prelude"]
let array = "Array"
let store = ["store"]
let select = ["select"]
let make_rt_rf h =
let rec rt env t =
let t = t_map (rt env) (rf env) t in
let array = find_theory env prelude array in
let store = (ns_find_ls array.th_export store).ls_name in
let select = (ns_find_ls array.th_export select).ls_name in
let make_rt_rf env =
let array = find_theory env prelude array in
let store = (ns_find_ls array.th_export store).ls_name in
let select = (ns_find_ls array.th_export select).ls_name in
let rec rt t =
let t = t_map rt rf t in
match t.t_node with
| Tapp (lselect,[{t_node=Tapp(lstore,[_;a1;b])};a2])
when lselect.ls_name == select &&
lstore.ls_name == store &&
t_equal_alpha a1 a2 -> b
| _ -> t
and rf ctxt f = f_map (rt ctxt) (rf ctxt) f in
and rf f = f_map rt rf f in
rt,rf
let t () =
let h = Hashtbl.create 5 in
let rt,rf = make_rt_rf h in
Transform.rewrite_env rt rf
let t =
Register.store_env
(fun () env ->
let rt,rf = make_rt_rf env in
Trans.rewrite rt rf None)
let () = Driver.register_transform "simplify_array" t
......@@ -107,3 +107,12 @@ let compose_trans reg1 reg2 = compose0 (fun f g -> Trans.compose f g) reg1 reg2
let compose_trans_l reg1 reg2 = compose0 (fun f g -> Trans.compose_l f g)
reg1 reg2
let conv_res conv reg1 =
let gen () =
let reg1 = reg1.generate () in
fun env cl -> conv (reg1 env cl) in
create gen
let identity_trans = store (fun () -> identity)
let identity_trans_l = store (fun () -> identity_l)
......@@ -50,5 +50,11 @@ val compose_trans :
val compose_trans_l :
task tlist registered -> 'a tlist registered -> 'a tlist registered
val conv_res : ('a -> 'b) -> 'a registered -> 'b registered
(* Sould be used only with function working in constant time*)
val clear_all : unit -> unit
val clear : 'a registered -> unit
val identity_trans : task trans registered
val identity_trans_l : task tlist registered
......@@ -132,5 +132,5 @@ let rewrite fnT fnF d = match d.d_node with
| Dprop (k,pr,f) ->
create_prop_decl k pr (fnF f)
let expr fnT fnF = decl (fun d -> [rewrite fnT fnF d])
let rewrite fnT fnF = decl (fun d -> [rewrite fnT fnF d])
......@@ -54,5 +54,5 @@ val map_l : (task_hd -> task -> task list) -> task -> task tlist
val decl : (decl -> decl list ) -> task -> task trans
val decl_l : (decl -> decl list list) -> task -> task tlist
val expr : (term -> term) -> (fmla -> fmla) -> task -> task trans
val rewrite : (term -> term) -> (fmla -> fmla) -> task -> task trans
......@@ -25,7 +25,7 @@ open Term
open Decl
open Theory
open Task
open Trans
open Register
open Env
open Driver_ast
......@@ -132,7 +132,7 @@ and driver = {
drv_prover : Call_provers.prover;
drv_prelude : string option;
drv_filename : string option;
drv_transforms : task tlist;
drv_transforms : task Trans.tlist registered;
drv_rules : theory_rules list;
drv_thprelude : string Hid.t;
(* the first is the translation only for this ident, the second is also for representant *)
......@@ -150,12 +150,11 @@ let print_driver fmt driver =
(** registering transformation *)
let (transforms : (string, unit -> task tlist) Hashtbl.t)
let (transforms : (string, task Trans.tlist registered) Hashtbl.t)
= Hashtbl.create 17
let register_transform_l name transform = Hashtbl.replace transforms name transform
let register_transform name t = register_transform_l name
(fun () -> Trans.singleton (t ()))
let register_transform name t = register_transform_l name (conv_res Trans.singleton t)
let list_transforms () = Hashtbl.fold (fun k _ acc -> k::acc) transforms []
(** registering printers *)
......@@ -321,11 +320,11 @@ let load_driver file env =
List.fold_left
(fun acc (loc,s) ->
let t =
try (Hashtbl.find transforms s) ()
try Hashtbl.find transforms s
with Not_found -> errorm ~loc "unknown transformation %s" s in
Trans.compose_l acc t
compose_trans_l acc t
)
Trans.identity_l transformations in
identity_trans_l transformations in
let transforms = trans ltransforms in
{ drv_printer = !printer;
drv_task = None;
......@@ -369,7 +368,7 @@ let syntax_arguments s print fmt l =
(** using drivers *)
let apply_transforms drv = Trans.apply drv.drv_transforms
let apply_transforms env clone drv = apply_trans_clone drv.drv_transforms env clone
let print_task env clone drv fmt task = match drv.drv_printer with
| None -> errorm "no printer"
......
......@@ -46,8 +46,8 @@ type printer = driver -> formatter -> task -> unit
val register_printer : string -> printer -> unit
val register_transform : string -> (unit -> task trans) -> unit
val register_transform_l : string -> (unit -> task tlist) -> unit
val register_transform : string -> task trans Register.registered -> unit
val register_transform_l : string -> task tlist Register.registered -> unit
val list_printers : unit -> string list
val list_transforms : unit -> string list
......@@ -55,7 +55,7 @@ val list_transforms : unit -> string list
(** using drivers *)
(** transform task *)
val apply_transforms : driver -> task -> task list
val apply_transforms : env -> clone -> driver -> task -> task list
(** print_task *)
val print_task : env -> clone -> printer
......
......@@ -211,7 +211,7 @@ let do_file env drv filename_printer file =
let goals = List.fold_left
(fun acc (th,(task,cl)) ->
List.rev_append
(List.map (fun e -> (th,e,cl)) (Driver.apply_transforms drv task)
(List.map (fun e -> (th,e,cl)) (Driver.apply_transforms env cl drv task)
) acc) [] goals in
(* Pretty-print the goals or call the prover *)
begin
......
......@@ -107,11 +107,11 @@ let fold isnotinlinedt isnotinlinedf task0 (env, task) =
env,add_decl task (create_prop_decl k pr (replacep env f))
let t ~isnotinlinedt ~isnotinlinedf =
Trans.fold_map (fold isnotinlinedt isnotinlinedf) empty_env None
Register.store (fun () -> Trans.fold_map (fold isnotinlinedt isnotinlinedf) empty_env None)
let all () = t ~isnotinlinedt:(fun _ -> false) ~isnotinlinedf:(fun _ -> false)
let all = t ~isnotinlinedt:(fun _ -> false) ~isnotinlinedf:(fun _ -> false)
let trivial () = t
let trivial = t
~isnotinlinedt:(fun m -> match m.t_node with
| Tconst _ | Tvar _ -> false
| Tapp (ls,tl) when List.for_all
......
......@@ -23,17 +23,17 @@
val t :
isnotinlinedt:(Term.term -> bool) ->
isnotinlinedf:(Term.fmla -> bool) ->
Task.task Trans.trans
Task.task Trans.trans Register.registered
(* Inline them all *)
val all : unit -> Task.task Trans.trans
val all : Task.task Trans.trans Register.registered
(* Inline only the trivial definition :
logic c : t = a
logic f(x : t,...., ) : t = g(y : t2,...) *)
val trivial : unit -> Task.task Trans.trans
val trivial : Task.task Trans.trans Register.registered
(* Function to use in other transformations if inlining is needed *)
......
......@@ -128,6 +128,6 @@ let elt d =
| Dind _ -> [d] (* TODO *)
| Dprop _ -> [d]
let t () = Trans.decl elt None
let t = Register.store (fun () -> Trans.decl elt None)
let () = Driver.register_transform "simplify_recursive_definition" t
......@@ -20,7 +20,7 @@
(* Simplify the recursive type and logic definition *)
val t : unit -> Task.task Trans.trans
val t : Task.task Trans.trans Register.registered
(* ungroup recursive definition *)
......
......@@ -88,14 +88,15 @@ let elt split_pos d =
(create_prop (id_clone (pr_name pr))) p]) l
| _ -> [[d]]
let t fsp = Register.store (fun () -> Trans.decl_l (elt fsp) None)
let split_pos1 = split_pos (fun acc x -> x::acc)
let rec split_pos2 acc d = split_pos split_neg2 acc d
and split_neg2 acc d = split_neg split_pos2 acc d
let split_pos () = Trans.decl_l (elt split_pos1) None
let split_pos_neg () = Trans.decl_l (elt split_pos2) None
let split_pos = t split_pos1
let split_pos_neg = t split_pos2
let () = Driver.register_transform_l "split_goal_pos" split_pos
let () = Driver.register_transform_l "split_goal_pos_neg" split_pos_neg
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