Commit 97d7abb7 authored by François Bobot's avatar François Bobot

Inlining : ajout d'un meta + documentation;

gappa use this meta for comparison (<= mostly)
parent 9b901734
......@@ -39,6 +39,10 @@ theory int.Int
syntax logic (*) "(%1 * %2)"
syntax logic (-_) "(-%1)"
meta "inline : no" logic (<=)
meta "inline : no" logic (>=)
meta "inline : no" logic (>)
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc.Assoc
remove prop CommutativeGroup.Unit_def
......@@ -86,6 +90,10 @@ theory real.Real
syntax logic (-_) "(-%1)"
syntax logic inv "(1.0 / %1)"
meta "inline : no" logic (<=)
meta "inline : no" logic (>=)
meta "inline : no" logic (>)
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc.Assoc
remove prop CommutativeGroup.Unit_def
......
......@@ -385,17 +385,17 @@ let print_goal info fmt g =
let print_task env pr thpr ?old:_ fmt task =
forget_all ident_printer;
let info = get_info env task in
let isnotinlinedt _t = true in
let isnotinlinedf f = match f.f_node with
| Fapp (ps,_) when Sls.mem ps info.info_inline ->
eprintf "inlining no_overflow_single!!@.";
false
| Fapp (ps,_) ->
eprintf "NOT inlining symbol %a@." print_ident ps.ls_name;
false
| _ -> true
in
let task = Trans.apply (Inlining.t ~isnotinlinedt ~isnotinlinedf) task in
(* let isnotinlinedt _t = true in *)
(* let isnotinlinedf f = match f.f_node with *)
(* | Fapp (ps,_) when Sls.mem ps info.info_inline -> *)
(* eprintf "inlining no_overflow_single!!@."; *)
(* false *)
(* | Fapp (ps,_) -> *)
(* eprintf "NOT inlining symbol %a@." print_ident ps.ls_name; *)
(* false *)
(* | _ -> true *)
(* in *)
(* let task = Trans.apply (Inlining.t ~isnotinlinedt ~isnotinlinedf) task in *)
let task =
Abstraction.abstraction
(fun f -> Sls.mem f info.info_symbols)
......
......@@ -69,10 +69,13 @@ 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 d (env, task) =
let addfs env ls vs t = {env with fs = Mls.add ls (vs,t) env.fs}
let addps env ls vs f = {env with ps = Mls.add ls (vs,f) env.ps}
let fold notdeft notdeff notls d (env, task) =
(* Format.printf "I see : %a@\n%a@\n" Pretty.print_decl d print_env env;*)
match d.d_node with
| Dlogic [ls,ld] -> begin
| Dlogic [ls,ld] when not (notls ls) -> begin
match ld with
| None -> env,add_decl task d
| Some ld ->
......@@ -80,16 +83,16 @@ let fold isnotinlinedt isnotinlinedf d (env, task) =
match e with
| Term t ->
let t = replacet env t in
if isnotinlinedt t || t_s_any ffalse (ls_equal ls) t
if notdeft t || t_s_any ffalse (ls_equal ls) t
then env, add_decl task
(create_logic_decl [make_fs_defn ls vs t])
else {env with fs = Mls.add ls (vs,t) env.fs},task
else (addfs env ls vs t),task
| Fmla f ->
let f = replacep env f in
if isnotinlinedf f || f_s_any ffalse (ls_equal ls) f
if notdeff f || f_s_any ffalse (ls_equal ls) f
then env, add_decl task
(create_logic_decl [make_ps_defn ls vs f])
else {env with ps = Mls.add ls (vs,f) env.ps},task
else (addps env ls vs f),task
end
| Dind dl ->
env, add_decl task (create_ind_decl
......@@ -108,32 +111,48 @@ let fold isnotinlinedt isnotinlinedf d (env, task) =
| Dprop (k,pr,f) ->
env,add_decl task (create_prop_decl k pr (replacep env f))
let fold isnotinlinedt isnotinlinedf task0 (env, task) =
let fold notdeft notdeff notls task0 (env, task) =
match task0.task_decl with
| { Theory.td_node = Theory.Decl d } ->
fold isnotinlinedt isnotinlinedf d (env, task)
fold notdeft notdeff notls d (env, task)
| td -> env, add_tdecl task td
let t ~isnotinlinedt ~isnotinlinedf =
Trans.fold_map (fold isnotinlinedt isnotinlinedf) empty_env None
let meta = Theory.register_meta "inline : no" [Theory.MTlsymbol]
let t ?(use_meta=true) ~notdeft ~notdeff ~notls =
let trans notls =
Trans.fold_map (fold notdeft notdeff notls) empty_env None in
if use_meta then
Trans.on_meta meta (fun ml ->
let sls = List.fold_left (fun acc e ->
match e with
| [Theory.MAls ls] -> Sls.add ls acc
|_ -> assert false) Sls.empty ml in
let notls ls = Sls.mem ls sls || notls ls in
trans notls)
else trans notls
let all = t ~isnotinlinedt:(fun _ -> false) ~isnotinlinedf:(fun _ -> false)
let all = t ~use_meta:true ~notdeft:ffalse ~notdeff:ffalse ~notls:ffalse
(** TODO : restrict to linear substitution,
ie each variable appear exactly once *)
let trivial = t
~isnotinlinedt:(fun m -> match m.t_node with
~use_meta:true
~notdeft:(fun m -> match m.t_node with
| Tconst _ | Tvar _ -> false
| Tapp (_,tl) when List.for_all
(fun m -> match m.t_node with
| Tvar _ -> true
| _ -> false) tl -> false
| _ -> true )
~isnotinlinedf:(fun m -> match m.f_node with
~notdeff:(fun m -> match m.f_node with
| Ftrue | Ffalse -> false
| Fapp (_,tl) when List.for_all
(fun m -> match m.t_node with
| Tvar _ -> true
| _ -> false) tl -> false
| _ -> true)
~notls:ffalse
let () =
Trans.register_transform "inline_all" all;
......
......@@ -18,31 +18,54 @@
(**************************************************************************)
(* Inline the definition not recursive *)
(** Inline the definitions not recursive *)
val meta : Theory.meta
(** {2 Generic inlining} *)
val t :
isnotinlinedt:(Term.term -> bool) ->
isnotinlinedf:(Term.fmla -> bool) ->
?use_meta:bool ->
notdeft:(Term.term -> bool) ->
notdeff:(Term.fmla -> bool) ->
notls :(Term.lsymbol -> bool) ->
Task.task Trans.trans
(** [t ~use_meta ~notdeft ~notdeff ~notls] returns a transformation which
inlines a symbol definition in the other definitions and propositions when
it verifies this condition :
- Its definitions doesn't verify [notdeft] in case of a logic function or
[notdeff] in case of a predicate
- Its logic symbol doesn't verify [notls]
- use_meta is not set or its logic symbol is not tagged by "inline : not"
Notice that [use_meta], [notdeft], [notdeff], [notls] restrict only which
symbols are inlined not when.
*)
(* Inline them all *)
(** {2 Registered Transformation} *)
val all : Task.task Trans.trans
(** [all] corresponds to the transformation "inline_all" *)
(* Inline only the trivial definition :
logic c : t = a
logic f(x : t,...., ) : t = g(y : t2,...) *)
val trivial : Task.task Trans.trans
(* Function to use in other transformations if inlining is needed *)
val trivial : Task.task Trans.trans
(** [trivial] corresponds to the transformation "inline_trivial"
Inline only the trivial definition :
logic c : t = a
logic f(x : t,...., ) : t = g(y : t2,...) *)
(** Functions to use in other transformations if inlining is needed *)
type env
val empty_env : env
(*val add_decl : env -> Theory.decl -> env *)
val addfs : env -> Term.lsymbol -> Term.vsymbol list -> Term.term -> env
val addps : env -> Term.lsymbol -> Term.vsymbol list -> Term.fmla -> env
(** [addls env ls vs t] trigger the inlining of [ls] by the definition
[t] with the free variables [vs]. The variables of [vs] must have
the type of the arguments of [ls] *)
val replacet : env -> Term.term -> Term.term
val replacep : env -> Term.fmla -> Term.fmla
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