Commit 9971a6b6 authored by Andrei Paskevich's avatar Andrei Paskevich

remove duplicate code in Inlining

parent 77b4dbe4
......@@ -35,62 +35,43 @@ let t_unfold env fs tl ty =
let mt = oty_match mt e.t_ty ty in
t_ty_subst mt mv e
let f_unfold env ps tl =
match Mls.find_option ps env with
| None ->
ps_app ps tl
| Some (vs,e) ->
let add (mt,mv) x y = ty_match mt x.vs_ty (t_type y), Mvs.add x y mv in
let (mt,mv) = List.fold_left2 add (Ty.Mtv.empty, Mvs.empty) vs tl in
t_ty_subst mt mv e
(* inline every symbol *)
let rec t_replace_all env t =
let t = TermTF.t_map (t_replace_all env) (f_replace_all env) t in
let t = t_map (t_replace_all env) t in
match t.t_node with
| Tapp (fs,tl) -> t_label_copy t (t_unfold env fs tl t.t_ty)
| _ -> t
and f_replace_all env f =
let f = TermTF.t_map (t_replace_all env) (f_replace_all env) f in
match f.t_node with
| Tapp (ps,tl) -> t_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.t_node with
| Tapp (ps,[l;r]) when ls_equal ps ps_equ ->
t_label_copy f (t_equ (t_replace_top env l) (t_replace_top env r))
| Tapp (ps,tl) ->
t_label_copy f (f_unfold env ps tl)
| _ ->
| Tapp (ps,_) when ls_equal ps ps_equ ->
t_map (f_replace_top env) f
| Tapp (ls,tl) ->
t_label_copy f (t_unfold env ls tl f.t_ty)
| _ when f.t_ty = None ->
TermTF.t_map (fun t -> t) (f_replace_top env) f
| _ ->
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 ->
DeclTF.decl_map (fun t -> t) (f_replace_top env) d
decl_map (f_replace_top env) d
| _ when in_goal ->
d
| _ ->
DeclTF.decl_map (t_replace_all env) (f_replace_all env) d
decl_map (t_replace_all env) d
in
match d.d_node with
| Dlogic [ls,Some ld] when not (notls ls) ->
let vl,e = open_ls_defn ld in
let inline = match e.t_ty with
| Some _ when notdeft e || t_s_any ffalse (ls_equal ls) e -> false
| None when notdeff e || t_s_any ffalse (ls_equal ls) e -> false
| _ -> true
in
let inline =
not (TermTF.t_select notdeft notdeff e
|| t_s_any ffalse (ls_equal ls) e) 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
......@@ -138,16 +119,12 @@ let trivial tl =
let notdeft t = match t.t_node with
| Tvar _ | Tconst _ -> false
| Tapp (_,tl) -> not (trivial tl)
| _ -> true
let notdeff f = match f.t_node with
| Ttrue | Tfalse -> false
| Ttrue | Tfalse -> false
| Tapp (_,tl) -> not (trivial tl)
| _ -> true
let trivial = t ~use_meta:true ~in_goal:false
~notdeft:notdeft ~notdeff:notdeff ~notls:ffalse
~notdeft:notdeft ~notdeff:notdeft ~notls:ffalse
let () =
Trans.register_transform "inline_all" all;
......
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