Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

Commit 349a0eb4 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

add inline_goal to transform/inlining

+ change inline_trivial: now we only inline right-linear
definitions where no variable occurs deeper than level 1.

Attention: this inlines definitions with arbitrarily complex
ground terms on the right-hand side - which might be a BAD IDEA,
but I still want to give it a try.

+ add find_logic_definition to Decl
parent e9bd8564
......@@ -592,6 +592,14 @@ let find_inductive_cases kn ps =
match (Mid.find ps.ls_name kn).d_node with
| Dind dl -> List.assq ps dl
| Dlogic _ -> []
| Dtype _ -> []
| _ -> assert false
let find_logic_definition kn ls =
match (Mid.find ls.ls_name kn).d_node with
| Dlogic dl -> List.assq ls dl
| Dind _ -> None
| Dtype _ -> None
| _ -> assert false
let find_prop kn pr =
......
......@@ -155,6 +155,7 @@ exception NonExhaustiveExpr of (pattern list * expr)
val find_constructors : known_map -> tysymbol -> lsymbol list
val find_inductive_cases : known_map -> lsymbol -> (prsymbol * fmla) list
val find_logic_definition : known_map -> lsymbol -> ls_defn option
val find_prop : known_map -> prsymbol -> fmla
val find_prop_decl : known_map -> prsymbol -> prop_kind * fmla
......@@ -19,188 +19,142 @@
open Util
open Ident
open Ty
open Term
open Decl
open Theory
open Task
type env = { fs : (vsymbol list * term) Mls.t;
ps : (vsymbol list * fmla) Mls.t}
let empty_env = { fs = Mls.empty;
ps = Mls.empty}
open Format
(*
let print_env fmt env =
let print_map iter pterm pfs = Pp.print_iter2 iter Pp.newline Pp.comma pfs
(Pp.print_pair (Pp.print_list Pp.comma Pretty.print_vsymbol) pterm) in
fprintf fmt "fs:@[<hov>%a@]@\nps:@[<hov>%a@]@\n"
(print_map Mls.iter Pretty.print_term Pretty.print_lsymbol) env.fs
(print_map Mls.iter Pretty.print_fmla Pretty.print_lsymbol) env.ps
*)
let rec replacet env t =
let t = substt env t in
let t_unfold env fs tl ty =
match Mls.find_option fs env with
| None ->
t_app fs tl ty
| Some (vl, Term e) ->
let add (mt,mv) x y = ty_match mt x.vs_ty y.t_ty, Mvs.add x y mv in
let (mt,mv) = List.fold_left2 add (Ty.Mtv.empty, Mvs.empty) vl tl in
let mt = ty_match mt e.t_ty ty in
t_ty_subst mt mv e
| _ ->
assert false
let f_unfold env ps tl =
match Mls.find_option ps env with
| None ->
f_app ps tl
| Some (vs, Fmla e) ->
let add (mt,mv) x y = ty_match mt x.vs_ty y.t_ty, Mvs.add x y mv in
let (mt,mv) = List.fold_left2 add (Ty.Mtv.empty, Mvs.empty) vs tl in
f_ty_subst mt mv e
| _ ->
assert false
(* inline every symbol *)
let rec t_replace_all env t =
let t = t_map (t_replace_all env) (f_replace_all env) t in
match t.t_node with
| Tapp (fs,tl) ->
begin try
let (vs,t) = Mls.find fs env.fs in
let add (mt,mv) x y =
(Ty.ty_match mt x.vs_ty y.t_ty, Mvs.add x y mv)
in
let (mt,mv) = List.fold_left2 add (Ty.Mtv.empty, Mvs.empty) vs tl in
let mt = Ty.ty_match mt (of_option fs.ls_value) t.t_ty in
t_ty_subst mt mv t
with Not_found -> t end
| _ -> t
and replacep env f =
let f = substp env f in
| Tapp (fs,tl) -> t_label_copy t (t_unfold env fs tl t.t_ty)
| _ -> t
and f_replace_all env f =
let f = f_map (t_replace_all env) (f_replace_all env) f in
match f.f_node with
| Fapp (ps,tl) ->
begin try
let (vs,f) = Mls.find ps env.ps in
let add (mt,mv) x y =
(Ty.ty_match mt x.vs_ty y.t_ty, Mvs.add x y mv)
in
let (mt,mv) = List.fold_left2 add (Ty.Mtv.empty, Mvs.empty) vs tl in
f_ty_subst mt mv f
with Not_found -> f end
| _ -> f
and substt env d = t_map (replacet env) (replacep env) d
and substp env d = f_map (replacet env) (replacep env) d
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;*)
| Fapp (ps,tl) -> f_label_copy f (f_unfold env ps tl)
| _ -> f
(* inline the top-most symbol *)
let t_replace_top env t = match t.t_node with
| Tapp (fs,tl) -> t_label_copy t (t_unfold env fs tl t.t_ty)
| _ -> t
let rec f_replace_top env f = match f.f_node with
| Fapp (ps,[l;r]) when ls_equal ps ps_equ ->
f_label_copy f (f_equ (t_replace_top env l) (t_replace_top env r))
| Fapp (ps,tl) ->
f_label_copy f (f_unfold env ps tl)
| _ ->
f_map (fun t -> t) (f_replace_top env) f
(* treat a declaration *)
let fold in_goal notdeft notdeff notls d (env, task) =
let d = match d.d_node with
| Dprop (Pgoal,_,_) when in_goal ->
decl_map (fun t -> t) (f_replace_top env) d
| _ when in_goal ->
d
| _ ->
decl_map (t_replace_all env) (f_replace_all env) d
in
match d.d_node with
| Dlogic [ls,ld] when not (notls ls) -> begin
match ld with
| None -> env,add_decl task d
| Some ld ->
let vs,e = open_ls_defn ld in
match e with
| Term t ->
let t = replacet env t in
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 (addfs env ls vs t),task
| Fmla f ->
let f = replacep env f in
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 (addps env ls vs f),task
end
| Dind dl ->
env, add_decl task (create_ind_decl
(List.map (fun (ps,fmlal) -> ps, List.map
(fun (pr,f) -> pr, replacep env f) fmlal) dl))
| Dlogic dl ->
env,
add_decl task (create_logic_decl
(List.map (fun (ls,ld) -> match ld with
| None -> ls, None
| Some ld ->
let vs,e = open_ls_defn ld in
let e = e_map (replacet env) (replacep env) e in
make_ls_defn ls vs e) dl))
| Dtype _ -> env,add_decl task d
| Dprop (k,pr,f) ->
env,add_decl task (create_prop_decl k pr (replacep env f))
let fold notdeft notdeff notls task0 (env, task) =
match task0.task_decl with
| { Theory.td_node = Theory.Decl d } ->
fold notdeft notdeff notls d (env, task)
| td -> env, add_tdecl task td
| Dlogic [ls,Some ld] when notls ls ->
let vl,e = open_ls_defn ld in
let inline = match e with
| Term t when notdeft t || t_s_any ffalse (ls_equal ls) t -> false
| Fmla f when notdeff f || f_s_any ffalse (ls_equal ls) f -> false
| _ -> true
in
let env = if inline then Mls.add ls (vl,e) env else env in
let task = if inline && not in_goal then task else add_decl task d in
env, task
| _ ->
env, add_decl task d
let fold in_goal notdeft notdeff notls task_hd (env, task) =
match task_hd.task_decl.td_node with
| Decl d ->
fold in_goal notdeft notdeff notls d (env, task)
| _ ->
env, add_tdecl task task_hd.task_decl
(* transformations *)
let meta = Theory.register_meta "inline : no" [Theory.MTlsymbol]
let t ?(use_meta=true) ~notdeft ~notdeff ~notls =
let t ?(use_meta=true) ?(in_goal=false) ~notdeft ~notdeff ~notls =
let trans notls =
Trans.fold_map (fold notdeft notdeff notls) empty_env None in
Trans.fold_map (fold in_goal notdeft notdeff notls) Mls.empty 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
Trans.on_tagged_ls meta (fun sls ->
let notls ls = Sls.mem ls sls || notls ls in
trans notls)
else trans notls
(*
let fold_on_logic f task env =
match task.Task.task_decl with
| { Theory.td_node = Theory.Decl d } ->
begin
match d.d_node with
| Dlogic dl ->
List.fold_left
(fun acc (ls,ld) -> f ls ld acc)
env dl
| _ -> env
end
| _ -> env
*)
let get_goal task =
match task.Task.task_decl with
| { Theory.td_node = Theory.Decl d } ->
begin
match d.d_node with
| Dprop(Pgoal,_pr,f) ->
begin
match f.f_node with
| Fapp(ps,_tl) ->
try
match
(Mid.find ps.ls_name task.Task.task_known).d_node
with
| Dlogic dl ->
let def = List.assoc ps dl in
begin
match def with
| Some _def -> assert false (* TODO *)
| None ->
Printer.unsupportedFmla f "has no definition"
end
| Dind _ ->
Printer.unsupportedFmla f
"inductive def cannot be inlined"
| Dprop _ | Dtype _ -> assert false
with Not_found -> assert false
end
| _ -> assert false
end
| _ -> assert 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
~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 )
~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
else
trans notls
let all = t ~use_meta:true ~in_goal:false
~notdeft:ffalse ~notdeff:ffalse ~notls:ffalse
let goal = t ~use_meta:true ~in_goal:true
~notdeft:ffalse ~notdeff:ffalse ~notls:ffalse
(* inline_trivial *)
let trivial tl =
let add vs t = match t.t_node with
| Tvar v when Mvs.mem v vs -> raise Util.FoldSkip
| Tvar v -> Svs.add v vs
| _ when Svs.is_empty (t_freevars Svs.empty t) -> vs
| _ -> raise Util.FoldSkip
in
try ignore (List.fold_left add Svs.empty tl); true
with Util.FoldSkip -> false
let notdeft t = match t.t_node with
| Tvar _ | Tconst _ -> false
| Tapp (_,tl) -> not (trivial tl)
| _ -> true
let notdeff f = match f.f_node with
| Ftrue | Ffalse -> false
| Fapp (_,tl) -> not (trivial tl)
| _ -> true
let trivial = t ~use_meta:true ~in_goal:false
~notdeft:notdeft ~notdeff:notdeff ~notls:ffalse
let () =
Trans.register_transform "inline_all" all;
Trans.register_transform "inline_goal" goal;
Trans.register_transform "inline_trivial" trivial
......@@ -17,8 +17,7 @@
(* *)
(**************************************************************************)
(** Inline the definitions not recursive *)
(** Inline non-recursive definitions *)
val meta : Theory.meta
......@@ -26,20 +25,26 @@ val meta : Theory.meta
val t :
?use_meta:bool ->
?in_goal: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 all of these conditions :
- 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 : no"
(** [t ~use_meta ~in_goal ~notdeft ~notdeff ~notls] returns a transformation
that expands a symbol [ls] in the subsequent declarations unless [ls]
satisfies one of the following conditions:
- [ls] is defined via a (mutually) recursive definition;
- [ls] is an inductive predicate or an algebraic type constructor;
- [ls] is a function symbol and [notdeft] returns true on its definition;
- [ls] is a predicate symbol and [notdeff] returns true on its definition;
- [notls ls] returns [true];
- [use_meta] is set and [ls] is tagged by "inline : no"
Notice that [use_meta], [notdeft], [notdeff], [notls] restrict only which
symbols are inlined not when.
If [in_goal] is set, only the top-most symbols in the goal are expanded.
*)
(** {2 Registered Transformation} *)
......@@ -47,7 +52,8 @@ val t :
val all : Task.task Trans.trans
(** [all] corresponds to the transformation "inline_all" *)
val goal : Task.task Trans.trans
(** [goal] corresponds to the transformation "inline_goal" *)
val trivial : Task.task Trans.trans
(** [trivial] corresponds to the transformation "inline_trivial"
......@@ -55,6 +61,7 @@ val trivial : Task.task Trans.trans
logic c : t = a
logic f(x : t,...., ) : t = g(y : t2,...) *)
(*
(** Functions to use in other transformations if inlining is needed *)
type env
......@@ -69,3 +76,4 @@ val addps : env -> Term.lsymbol -> Term.vsymbol list -> Term.fmla -> env
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