Commit eb0d56d1 authored by Francois Bobot's avatar Francois Bobot

inlining : ajout de la transformation "inline_let"

parent 50d1b914
......@@ -15,8 +15,9 @@ fail "typing error:\\(.*\\)$" "Failure : File generation error : \\1"
(* À discuter *)
transformations
"simplify_recursive_definition"
(*"split_goal_pos_neg_goal"*) "split_goal_pos_neg_all"
"inline_let"
"inline_trivial"
(*"split_goal_pos_neg_goal"*) "split_goal_pos_neg_all"
end
......
......@@ -9,7 +9,7 @@ theory Test
goal G : (forall x:int. x=x) or
(forall x:int. x=x+1)
goal G2 : forall x:int. 0 = 1
goal G2 : forall x:int. let x = 0 + 1 in x = 1
end
theory Test_simplify_array
......
......@@ -108,7 +108,9 @@ let fold isnotinlinedt isnotinlinedf task0 (env, task) =
let t ~isnotinlinedt ~isnotinlinedf =
Register.store
(fun () -> Trans.fold_map (fold isnotinlinedt isnotinlinedf) empty_env None)
(fun () -> Trans.fold_map
(fold isnotinlinedt isnotinlinedf)
empty_env None)
let all = t ~isnotinlinedt:(fun _ -> false) ~isnotinlinedf:(fun _ -> false)
......@@ -131,3 +133,34 @@ let trivial = t
let () =
Driver.register_transform "inline_all" all;
Driver.register_transform "inline_trivial" trivial
(* Let inlining *)
let rec rewrite_t map t =
match t.t_node with
| Tlet (t1,tb) ->
let t1 = rewrite_t map t1 in
let vs,t2 = t_open_bound tb in
rewrite_t (Mvs.add vs t1 map) t2
| Tvar vs ->
begin try
Mvs.find vs map
with Not_found -> t end
| _ -> t_map (rewrite_t map) (rewrite_f map) t
and rewrite_f map f =
match f.f_node with
| Flet (t1,fb) ->
let t1 = rewrite_t map t1 in
let vs,f2 = f_open_bound fb in
rewrite_f (Mvs.add vs t1 map) f2
| _ -> f_map (rewrite_t map) (rewrite_f map) f
let remove_let_t = rewrite_t Mvs.empty
let remove_let_f = rewrite_f Mvs.empty
let inline_let =
Register.store (fun () -> Trans.rewrite remove_let_t remove_let_f None)
let () = Driver.register_transform "inline_let" inline_let
......@@ -36,6 +36,11 @@ val all : Task.task Register.trans_reg
val trivial : Task.task Register.trans_reg
(* Inline let *)
val remove_let_t : Term.term -> Term.term
val remove_let_f : Term.fmla -> Term.fmla
val inline_let : Task.task Register.trans_reg
(* Function to use in other transformations if inlining is needed *)
type env
......
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