Commit b29d4d0d authored by Francois Bobot's avatar Francois Bobot

signature et implementation des transformations mise a jour

parent 9ca46334
......@@ -8,7 +8,7 @@ theory AC
axiom Assoc : forall x,y,z:t. op(op(x,y),z)=op(x,op(y,z))
end
theory Group
theory GroupStructure
type t
logic neutral : t
......@@ -22,4 +22,23 @@ theory Group
logic op = op
axiom Inv_def : forall x:t. op(x,inv(x)) = neutral
end
\ No newline at end of file
end
theory RingStructure
type t
logic zero : t
logic (_+_)(t, t) : t
logic (-_)(t) : t
logic (_*_)(t, t) : t
clone GroupStructure with type t = t,
logic neutral = zero,
logic op = (_+_),
logic inv = (-_)
clone AC with type t = t,
logic op = (_*_)
axiom Mul_distr: forall x,y,z:t. x * (y + z) = x * y + x * z
end
......@@ -22,130 +22,87 @@ open Theory
open Context
(* the memoisation is inside the function *)
type ('a,'b) t = { all : 'a -> 'b;
clear : unit -> unit;
type 'a t = { all : context -> 'a;
clear : unit -> unit;
}
type ctxt_t = context t
let compose f g = {all = (fun x -> g.all (f.all x));
clear = (fun () -> f.clear (); g.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 compose f g = {all = (fun x -> g.all (f.all x));
clear = (fun () -> f.clear (); g.clear ());
}
let apply f x = f.all x
let clear f = f.clear ()
let memo f tag h x =
try Hashtbl.find h (tag x)
with Not_found ->
let r = f x in
Hashtbl.add h (tag x) r;
r
let ymemo f tag h =
let rec aux x =
let t = tag x in
try
Hashtbl.find h t
with Not_found ->
let r = f aux x in
Hashtbl.add h t r;
r in
aux
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 memo f tag h = ymemo (fun _ -> f) tag h
let d_tag d = d.d_tag
let ctxt_tag c = c.ctxt_tag
let t all clear clearf =
let t ?(clear=(fun () -> ())) all clear_all =
{all = all;
clear = match clear with
| None -> clearf
| Some clear -> (fun () -> clear ();clear ())
clear = (fun () -> clear ();clear_all ())
}
let fold_up ?clear f_fold v_empty =
let fold ?clear f_fold v_empty =
let memo_t = Hashtbl.create 64 in
let rewind env todo =
List.fold_left
(fun env (desc,ctxt) ->
let env = f_fold ctxt env desc in
(fun env ctxt ->
let env = f_fold ctxt env in
Hashtbl.add memo_t ctxt.ctxt_tag env;
env) env todo in
let rec f todo ctxt = assert false
(*
match ctxt.ctxt_decls with
let rec f todo ctxt =
match ctxt.ctxt_prev with
| None -> rewind v_empty todo
| Some (decls,ctxt2) ->
| Some (ctxt2) ->
try
let env = Hashtbl.find memo_t ctxt2.ctxt_tag in
rewind env ((decls,ctxt)::todo)
with Not_found -> f ((decls,ctxt)::todo) ctxt2
*)
rewind env (ctxt::todo)
with Not_found -> f (ctxt::todo) ctxt2
in
t (f []) clear (fun () -> Hashtbl.clear memo_t)
let fold_bottom_up ?tag ?clear ~top ~down f_fold v_empty =
let rewind ldone env_down =
List.fold_left down env_down ldone in
let tag_clear,tag_memo = match tag with
| None -> (fun () -> ()), (fun f ldone v ctxt -> f ldone v ctxt)
| Some tag_env ->
let memo_t = Hashtbl.create 64 in
(fun () -> Hashtbl.clear memo_t),(fun f ldone v ctxt ->
try
let env_down = Hashtbl.find memo_t (ctxt.ctxt_tag,tag_env v) in
rewind ldone env_down
with Not_found ->
let env_down = f ldone v ctxt in
Hashtbl.add memo_t (ctxt.ctxt_tag,tag_env v) env_down;
env_down
) in
let rec f ldone v ctxt = assert false
(*
match ctxt.ctxt_decls with
| None -> rewind ldone (top v)
| Some(d,ctxt2) ->
let v,res = f_fold ctxt v d in
tag_memo f (res::ldone) 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)
t ?clear (f []) (fun () -> Hashtbl.clear memo_t)
let fold_bottom ?tag ?clear f_fold v_empty =
let top x = x in
let down x () = x in
let f_fold ctxt env d = f_fold ctxt env d, () in
fold_bottom_up ?tag ?clear ~top ~down f_fold v_empty
let fold_map_up ?clear f_fold v_empty =
let fold_map ?clear f_fold v_empty =
let v_empty = v_empty,create_context in
let f_fold ctxt (env,ctxt2) decl = f_fold ctxt env ctxt2 decl in
conv_res (fold_up ?clear f_fold v_empty) snd
let f_fold ctxt (env,ctxt2) = f_fold ctxt ctxt2 env in
conv_res (fold ?clear f_fold v_empty) snd
let map ?clear f_map =
fold_map ?clear (fun ctxt1 ctxt2 () -> (),f_map ctxt1 ctxt2) ()
let map_concat ?clear f_elt =
let f_elt ctxt0 ctxt =
List.fold_left add_decl ctxt (f_elt ctxt0) in
map ?clear f_elt
let elt ?clear f_elt =
let memo_elt = Hashtbl.create 64 in
let f_elt _ () ctx x = (),
List.fold_left add_decl ctx (memo f_elt d_tag memo_elt x) in
let f = fold_map_up ?clear f_elt () in
let f_elt ctxt0 = memo f_elt d_tag memo_elt ctxt0.ctxt_decl in
let f = map_concat ?clear f_elt in
{f with clear = fun () -> Hashtbl.clear memo_elt; f.clear ()}
let fold_map_bottom ?tag ?clear f_fold v_empty =
let top _ = create_context in
let down = (List.fold_left add_decl) in
fold_bottom_up ?tag ?clear ~top ~down f_fold v_empty
let all ?clear f =
let register ?clear f =
let memo_t = Hashtbl.create 16 in
t (memo f ctxt_tag memo_t) clear (fun () -> Hashtbl.clear memo_t)
t ?clear (memo f ctxt_tag memo_t) (fun () -> Hashtbl.clear memo_t)
(* Utils *)
......@@ -170,7 +127,8 @@ let fold_context_of_decl f ctxt env ctxt_done d =
env,List.fold_left add_decl ctxt_done decls
let split_goals =
let f _ (ctxt,l) decl =
let f ctxt0 (ctxt,l) =
let decl = ctxt0.ctxt_decl in
match decl.d_node with
| Dprop (Pgoal,_) -> (ctxt,(add_decl ctxt decl)::l)
| Dprop (Plemma,f) ->
......@@ -179,11 +137,12 @@ let split_goals =
(add_decl ctxt d1,
(add_decl ctxt d2)::l)
| _ -> (add_decl ctxt decl,l) in
let g = fold_up f (create_context,[]) in
let g = fold f (create_context,[]) in
conv_res g snd
let extract_goals =
let f _ (ctxt,l) decl =
let f ctxt0 (ctxt,l) =
let decl = ctxt0.ctxt_decl in
match decl.d_node with
| Dprop (Pgoal,f) -> (ctxt,(f.pr_name,f.pr_fmla,ctxt)::l)
| Dprop (Plemma,f) ->
......@@ -191,7 +150,7 @@ let extract_goals =
(add_decl ctxt d,
(f.pr_name,f.pr_fmla,ctxt)::l)
| _ -> (add_decl ctxt decl,l) in
let g = fold_up f (create_context,[]) in
let g = fold f (create_context,[]) in
conv_res g snd
......
......@@ -25,81 +25,54 @@ open Theory
(** General functions *)
(* The type of transformation from list of 'a to list of 'b *)
type ('a,'b) t
type 'a t
type ctxt_t = context t
(* compose two transformations, the underlying datastructures for
the memoisation are shared *)
val compose : ('a,'b) t -> ('b,'c) t -> ('a,'c) t
val compose : context t -> 'a t -> 'a t
(* apply a transformation and memoise *)
val apply : ('a,'b) t -> 'a -> 'b
(* 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
val apply : 'a t -> context -> 'a
(* clear the datastructures used to store the memoisation *)
val clear : ('a,'b) t -> unit
val clear : 'a t -> unit
(** General constructors *)
val fold_up :
(* create a transformation with only one memoisation *)
val register :
?clear:(unit -> unit) ->
(context -> 'a -> decl -> 'a) -> 'a -> (context,'a) t
(context -> 'a) -> 'a t
val fold_bottom :
?tag:('a -> int) ->
(* Fold from the first declaration to the last with a memoisation at
each step *)
val fold :
?clear:(unit -> unit) ->
(context -> 'a -> decl -> 'a) -> 'a -> (context,'a) t
(context -> 'a -> 'a) -> 'a -> 'a t
val fold_bottom_up :
?tag:('a -> int) ->
val fold_map :
?clear:(unit -> unit) ->
top:('a -> 'c) ->
down:('c -> 'b -> 'c) ->
(context -> 'a -> decl -> 'a * 'b) -> 'a -> (context,'c) t
(context -> context -> 'a -> ('a * context)) -> 'a ->
context t
(* the general tranformation only one memoisation is performed at the
beginning *)
val all :
val map :
?clear:(unit -> unit) ->
(context -> 'a) -> (context,'a) t
(context -> context -> context) -> context 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) ->
?clear:(unit -> unit) ->
(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 :
val map_concat :
?clear:(unit -> unit) ->
(context -> 'a -> context -> decl -> ('a * context)) -> 'a ->
(context,context) t
(context -> decl list) -> 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,context) t
(decl -> decl list) -> context t
(** Utils *)
(*type odecl =
| Otype of ty_decl
| Ologic of logic_decl
......@@ -124,8 +97,8 @@ val fold_context_of_decl:
(* Utils *)
val unit_tag : unit -> int
val split_goals : (context,context list) t
val split_goals : 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
val identity : context t
......@@ -47,15 +47,14 @@ let () =
let in_emacs = Sys.getenv "TERM" = "dumb"
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 transformation l =
List.map (fun (t,c) ->
let c = if !simplify_recursive
then Transform.apply Simplify_recursive_definition.t c
else c in
let c = if !inlining then Transform.apply Inlining.all c
else c in
(t,c)) l
let rec report fmt = function
| Lexer.Error e ->
......@@ -91,7 +90,7 @@ let transform env l =
let l = List.map
(fun t -> t, Context.use_export Context.create_context t)
(Typing.list_theory l) in
let l = Transform.apply transformation l in
let l = transformation l in
if !print_stdout then
List.iter
(fun (t,ctxt) -> Why3.print_context_th std_formatter t.th_name ctxt) l
......
......@@ -19,4 +19,4 @@
(* a list of decl_or_use to a list of decl *)
val t : (Theory.context,Theory.context) Transform.t
val t : Transform.ctxt_t
......@@ -66,8 +66,9 @@ and replacep env f =
and substt env d = t_map (replacet env) (replacep env) d
and substp env d = f_map (replacet env) (replacep env) d
let fold isnotinlinedt isnotinlinedf _ env ctxt d =
let fold isnotinlinedt isnotinlinedf ctxt0 ctxt env =
(* Format.printf "I see : %a@\n%a@\n" Pretty.print_decl d print_env env;*)
let d = ctxt0.ctxt_decl in
match d.d_node with
| Dlogic [l] -> begin
match l with
......@@ -117,7 +118,7 @@ let fold isnotinlinedt isnotinlinedf _ env ctxt d =
| Duse _ | Dclone _ -> env,add_decl ctxt d
let t ~isnotinlinedt ~isnotinlinedf =
Transform.fold_map_up (fold isnotinlinedt isnotinlinedf) empty_env
Transform.fold_map (fold isnotinlinedt isnotinlinedf) empty_env
let all = t ~isnotinlinedt:(fun _ -> false) ~isnotinlinedf:(fun _ -> false)
......
......@@ -23,17 +23,17 @@
val t :
isnotinlinedt:(Term.term -> bool) ->
isnotinlinedf:(Term.fmla -> bool) ->
(Theory.context,Theory.context) Transform.t
Transform.ctxt_t
(* Inline them all *)
val all : (Theory.context,Theory.context) Transform.t
val all : Transform.ctxt_t
(* Inline only the trivial definition :
logic c : t = a
logic f(x : t,...., ) : t = g(y : t2,...) *)
val trivial : (Theory.context,Theory.context) Transform.t
val trivial : Transform.ctxt_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,Theory.context) Transform.t
val t : Transform.ctxt_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