Commit 01600fe0 authored by Francois Bobot's avatar Francois Bobot

generalisation des transformations

parent e4e9ae99
......@@ -22,7 +22,7 @@ open Theory
open Context
(* the memoisation is inside the function *)
type t = { all : context -> context;
type 'a t = { all : context -> 'a;
clear : unit -> unit;
}
......@@ -31,6 +31,9 @@ let compose f g = {all = (fun x -> g.all (f.all x));
clear = (fun () -> f.clear (); g.clear ());
}
let translation f c = {all = (fun x -> c (f.all x));
clear = f.clear}
let apply f x = f.all x
let clear f = f.clear ()
......@@ -52,26 +55,31 @@ let t all clear clearf =
| Some clear -> (fun () -> clear ();clear ())
}
let fold_map_up ?clear f_fold v_empty =
let fold_up ?clear f_fold v_empty =
let memo_t = Hashtbl.create 64 in
let rewind ecdone todo =
let _,ctxt_done = List.fold_left
(fun (env_done,ctxt_done) (desc,ctxt) ->
let ecdone = f_fold ctxt env_done ctxt_done desc in
Hashtbl.add memo_t ctxt.ctxt_tag ecdone;
ecdone) ecdone todo in
ctxt_done in
let rewind env todo =
List.fold_left
(fun env (desc,ctxt) ->
let env = f_fold ctxt env desc in
Hashtbl.add memo_t ctxt.ctxt_tag env;
env) env todo in
let rec f todo ctxt =
match ctxt.ctxt_decls with
| None -> rewind (v_empty,empty_context) todo
| None -> rewind v_empty todo
| Some (decls,ctxt2) ->
try
let ecdone = Hashtbl.find memo_t ctxt2.ctxt_tag in
rewind ecdone ((decls,ctxt)::todo)
let env = Hashtbl.find memo_t ctxt2.ctxt_tag in
rewind env ((decls,ctxt)::todo)
with Not_found -> f ((decls,ctxt)::todo) ctxt2
in
t (f []) clear (fun () -> Hashtbl.clear memo_t)
let fold_map_up ?clear f_fold v_empty =
let v_empty = v_empty,empty_context in
let f_fold ctxt (env,ctxt2) decl = f_fold ctxt env ctxt2 decl in
translation (fold_up ?clear f_fold v_empty) snd
let elt ?clear f_elt =
let memo_elt = Hashtbl.create 64 in
let f_elt _ () ctx x = (),
......@@ -79,6 +87,29 @@ let elt ?clear f_elt =
let f = fold_map_up ?clear f_elt () in
{f with clear = fun () -> Hashtbl.clear memo_elt; f.clear ()}
let fold_bottom ?tag ?clear f_fold v_empty =
let tag_clear,tag_memo = match tag with
| None -> (fun () -> ()), (fun f v ctxt -> f v ctxt)
| Some tag_env ->
let memo_t = Hashtbl.create 64 in
(fun () -> Hashtbl.clear memo_t),(fun f v ctxt ->
try
Hashtbl.find memo_t (ctxt.ctxt_tag,(tag_env v : int))
with Not_found ->
let r = f v ctxt in
Hashtbl.add memo_t (ctxt.ctxt_tag,tag_env v) r;
r
) in
let rec f v ctxt =
match ctxt.ctxt_decls with
| None -> v
| Some(d,ctxt2) ->
let v = f_fold ctxt v d in
tag_memo f v ctxt2 in
let memo_t = Hashtbl.create 16 in
t (memo (f v_empty) ctxt_tag memo_t) clear (fun () -> tag_clear ();Hashtbl.clear memo_t)
let fold_map_bottom ?tag ?clear f_fold v_empty =
let rewind ldone ctxt =
List.fold_left (List.fold_left add_decl) ctxt ldone in
......
......@@ -23,43 +23,55 @@ open Theory
(* Tranformation on context with some memoisations *)
(* The type of transformation from list of 'a to list of 'b *)
type t
type 'a t
(* compose two transformations, the underlying datastructures for
the memoisation are shared *)
val compose : t -> t -> t
val compose : context t -> 'a t -> 'a t
(* apply a transformation and memoise *)
val apply : t -> context -> context
val apply : 'a t -> context -> 'a
(* clear the datastructures used to store the memoisation *)
val clear : t -> unit
val clear : 'a t -> unit
(* the general tranformation only one memoisation is performed at the
beginning *)
val all :
?clear:(unit -> unit) ->
(context -> context) -> t
(context -> 'a) -> 'a t
(* map the element of the list from the first to the last. only one
memoisation is performed at the beginning. But if a tag function is
given a memoisation is performed at each step *)
val fold_map_bottom :
?tag:('a -> int) ->
?tag:('a -> int) ->
?clear:(unit -> unit) ->
(context -> 'a -> decl -> 'a * decl list) -> 'a -> t
(context -> 'a -> decl -> 'a * decl list) -> 'a -> context t
(* map the element of the list from the last to the first.
A memoisation is performed at each step *)
val fold_map_up :
?clear:(unit -> unit) ->
(context -> 'a -> context -> decl -> ('a * context)) -> 'a -> t
(context -> 'a -> context -> decl -> ('a * context)) -> 'a -> context t
(* map the element of the list without an environnment.
A memoisation is performed at each step, and for each elements *)
val elt :
?clear:(unit -> unit) ->
(decl -> decl list) -> t
(decl -> decl list) -> context t
val fold_bottom :
?tag:('a -> int) ->
?clear:(unit -> unit) ->
(context -> 'a -> decl -> 'a) -> 'a -> 'a t
val fold_up :
?clear:(unit -> unit) ->
(context -> 'a -> decl -> 'a) -> 'a -> 'a t
(*type odecl =
......
(* a list of decl_or_use to a list of decl *)
val t : Transform.t
val t : Theory.context Transform.t
(* Inline the definition not recursive *)
val t : Transform.t
val t : Theory.context Transform.t
(* Function to use in other transformations if inlining is needed *)
......
......@@ -20,7 +20,7 @@
(* Simplify the recursive type and logic definition *)
val t : Transform.t
val t : Theory.context Transform.t
(* ungroup recursive definition *)
......
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