Commit cb8077a1 authored by Francois Bobot's avatar Francois Bobot

Experimentation sur l'interface de transform.ml. Par contre quand est ce que...

Experimentation sur l'interface de transform.ml. Par contre quand est ce que le contexte est applati dans theory.ml?
parent d2680d5c
......@@ -22,8 +22,8 @@ open Theory
open Context
(* the memoisation is inside the function *)
type 'a t = { all : context -> 'a;
clear : unit -> unit;
type ('a,'b) t = { all : 'a -> 'b;
clear : unit -> unit;
}
......@@ -31,8 +31,19 @@ let compose f g = {all = (fun x -> g.all (f.all x));
clear = (fun () -> f.clear (); g.clear ());
}
let conv f c = {all = (fun x -> c (f.all x));
clear = f.clear}
let conv_arg f c = {all = (fun x -> f.all (c x));
clear = f.clear}
let conv_res f c = {all = (fun x -> c (f.all x));
clear = f.clear}
let conv f c1 c2 = {all = (fun x -> let arg,env = c1 x in
c2 ((f.all arg),env));
clear = f.clear}
let conv_map f m = {all = (fun x -> m f.all x);
clear = f.clear}
let apply f x = f.all x
......@@ -45,6 +56,11 @@ let memo f tag h x =
Hashtbl.add h (tag x) r;
r
let conv_memo f tag =
let h = Hashtbl.create 16 in
{all = memo f.all tag h;
clear = (fun () -> Hashtbl.clear h; f.clear ())}
let d_tag d = d.d_tag
let ctxt_tag c = c.ctxt_tag
......@@ -109,7 +125,7 @@ let fold_bottom ?tag ?clear f_fold v_empty =
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
conv (fold_up ?clear f_fold v_empty) snd
conv_res (fold_up ?clear f_fold v_empty) snd
let elt ?clear f_elt =
let memo_elt = Hashtbl.create 64 in
......@@ -156,7 +172,7 @@ let split_goals =
| Dprop (Pgoal,_) -> (ctxt,(add_decl ctxt decl)::l)
| _ -> (add_decl ctxt decl,l) in
let g = fold_up f (empty_context,[]) in
conv g snd
conv_res g snd
let extract_goals =
let f _ (ctxt,l) decl =
......@@ -164,7 +180,10 @@ let extract_goals =
| Dprop (Pgoal,f) -> (ctxt,(f.pr_name,f.pr_fmla,ctxt)::l)
| _ -> (add_decl ctxt decl,l) in
let g = fold_up f (empty_context,[]) in
conv g snd
conv_res g snd
let unit_tag () = 0
let identity = {all = (fun x -> x);
clear = (fun () -> ())}
......@@ -25,31 +25,40 @@ open Theory
(** General functions *)
(* The type of transformation from list of 'a to list of 'b *)
type 'a t
type ('a,'b) t
(* compose two transformations, the underlying datastructures for
the memoisation are shared *)
val compose : context t -> 'a t -> 'a t
val compose : ('a,'b) t -> ('b,'c) t -> ('a,'c) t
(* apply a transformation and memoise *)
val apply : 'a t -> context -> 'a
val apply : ('a,'b) t -> 'a -> 'b
(* convert the result of a transformation witout memoisation *)
val conv : 'a t -> ('a -> 'b) -> 'b t
(* convert the argument of a transformation without memoisation *)
val conv_arg : ('a,'b) t -> ('c -> 'a) -> ('c,'b) t
(* convert the result of a transformation without memoisation *)
val conv_res : ('a,'b) t -> ('b -> 'c) -> ('a,'c) t
val conv : ('a,'b) t -> ('c -> 'a * 'e) -> ('b * 'e -> 'd) -> ('c,'d) t
val conv_map : ('a,'b) t -> (('a -> 'b) -> 'c -> 'd) -> ('c,'d) t
val conv_memo : ('a,'b) t -> ('a -> int) -> ('a,'b) t
(* clear the datastructures used to store the memoisation *)
val clear : 'a t -> unit
val clear : ('a,'b) t -> unit
(** General constructors *)
val fold_up :
?clear:(unit -> unit) ->
(context -> 'a -> decl -> 'a) -> 'a -> 'a t
(context -> 'a -> decl -> 'a) -> 'a -> (context,'a) t
val fold_bottom :
?tag:('a -> int) ->
?clear:(unit -> unit) ->
(context -> 'a -> decl -> 'a) -> 'a -> 'a t
(context -> 'a -> decl -> 'a) -> 'a -> (context,'a) t
val fold_bottom_up :
......@@ -57,7 +66,7 @@ val fold_bottom_up :
?clear:(unit -> unit) ->
top:('a -> 'c) ->
down:('c -> 'b -> 'c) ->
(context -> 'a -> decl -> 'a * 'b) -> 'a -> 'c t
(context -> 'a -> decl -> 'a * 'b) -> 'a -> (context,'c) t
......@@ -66,7 +75,7 @@ val fold_bottom_up :
beginning *)
val all :
?clear:(unit -> unit) ->
(context -> 'a) -> 'a t
(context -> 'a) -> (context,'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
......@@ -74,19 +83,20 @@ val all :
val fold_map_bottom :
?tag:('a -> int) ->
?clear:(unit -> unit) ->
(context -> 'a -> decl -> 'a * decl list) -> 'a -> context t
(context -> 'a -> decl -> 'a * decl list) -> 'a -> (context,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 -> context t
(context -> 'a -> context -> decl -> ('a * context)) -> 'a ->
(context,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) -> context t
(decl -> decl list) -> (context,context) t
......@@ -114,6 +124,8 @@ val fold_context_of_decl:
(* Utils *)
val unit_tag : unit -> int
val split_goals : context list t
val split_goals : (context,context list) t
val extract_goals : (context,(Ident.ident * Term.fmla * context) list) t
val extract_goals : (Ident.ident * Term.fmla * context) list t
val identity : ('a,'a) t
......@@ -46,7 +46,15 @@ let () =
"usage: why [options] files..."
let in_emacs = Sys.getenv "TERM" = "dumb"
let transform = !simplify_recursive || !inlining
let transformation =
Transform.conv_map
(Transform.compose
(if !simplify_recursive then Simplify_recursive_definition.t
else Transform.identity)
(if !inlining then Inlining.all
else Transform.identity)
)
(fun f l -> List.map (fun (t,c) -> t,f c) l)
let rec report fmt = function
| Lexer.Error e ->
......@@ -79,13 +87,7 @@ let extract_goals ctxt =
let transform l =
let l = List.map (fun t -> t,t.th_ctxt) (Typing.list_theory l) in
let l = if !simplify_recursive
then List.map (fun (t,dl) -> t,Transform.apply
Simplify_recursive_definition.t dl) l
else l in
let l = if !inlining
then List.map (fun (t,dl) -> t,Transform.apply Inlining.all dl) l
else l in
let l = Transform.apply transformation l in
if !print_stdout then
List.iter (fun (t,ctxt) -> Why3.print_context_th std_formatter t.th_name ctxt) l
else if !alt_ergo then match l with
......
......@@ -146,4 +146,4 @@ let print_context fmt ctxt =
let print_goal fmt (id, f, ctxt) =
print_context fmt ctxt;
fprintf fmt "@[<hov 2>goal %a : %a@]" print_ident id print_fmla f
fprintf fmt "@\n@[<hov 2>goal %a : %a@]" print_ident id print_fmla f
(* a list of decl_or_use to a list of decl *)
val t : Theory.context Transform.t
val t : (Theory.context,Theory.context) Transform.t
......@@ -4,17 +4,18 @@
val t :
isnotinlinedt:(Term.term -> bool) ->
isnotinlinedf:(Term.fmla -> bool) -> Theory.context Transform.t
isnotinlinedf:(Term.fmla -> bool) ->
(Theory.context,Theory.context) Transform.t
(* Inline them all *)
val all : Theory.context Transform.t
val all : (Theory.context,Theory.context) Transform.t
(* Inline only the trivial definition :
logic c : t = a
logic f(x : t,...., ) : t = g(y : t2,...) *)
val trivial : Theory.context Transform.t
val trivial : (Theory.context,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 : Theory.context Transform.t
val t : (Theory.context,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