Commit e8717701 authored by Andrei Paskevich's avatar Andrei Paskevich

simplify dependent transformations

parent 65f7d3c7
......@@ -138,31 +138,63 @@ module Wtds = Hashweak.Make (struct
let tag s = s.tds_tag
end)
let on_theory th fn =
let on_theory_tds th fn =
let fn = Wtds.memoize 17 fn in
fun task -> fn (find_clone task th) task
let on_meta t fn =
let on_meta_tds t fn =
let fn = Wtds.memoize 17 fn in
fun task -> fn (find_meta task t) task
let on_theory th fn =
let sml td acc = match td.td_node with
| Clone (_,sm) -> sm::acc
| _ -> assert false
in
on_theory_tds th (fun tds -> fn (Stdecl.fold sml tds.tds_set []))
let on_meta t fn =
let mal td acc = match td.td_node with
| Meta (_,ma) -> ma::acc
| _ -> assert false
in
on_meta_tds t (fun tds -> fn (Stdecl.fold mal tds.tds_set []))
let on_theories tl fn =
let rec pass acc = function
| th::tl -> on_theory th (fun st -> pass (Mid.add th.th_name st acc) tl)
| [] -> fn acc
| th::tl ->
let fn st = pass (Mid.add th.th_name st acc) tl in
on_theory_tds th fn
| [] ->
fn acc
in
pass Mid.empty tl
let on_metas tl fn =
let rec pass acc = function
| t::tl -> on_meta t (fun st -> pass (Mmeta.add t st acc) tl)
| [] -> fn acc
| t::tl ->
let fn st = pass (Mmeta.add t st acc) tl in
on_meta_tds t fn
| [] ->
fn acc
in
pass Mmeta.empty tl
let on_theories_metas thl tl fn =
on_theories thl (fun cm -> on_metas tl (fn cm))
let on_meta_excl t fn =
on_meta_tds t (fun tds -> fn (get_meta_excl t tds))
let on_tagged_ts t fn =
on_meta_tds t (fun tds -> fn (find_tagged_ts t tds Sts.empty))
let on_tagged_ls t fn =
on_meta_tds t (fun tds -> fn (find_tagged_ls t tds Sls.empty))
let on_tagged_pr t fn =
on_meta_tds t (fun tds -> fn (find_tagged_pr t tds Spr.empty))
(** register transformations *)
open Env
......
......@@ -17,6 +17,7 @@
(* *)
(**************************************************************************)
open Ty
open Term
open Decl
open Theory
......@@ -67,14 +68,20 @@ val rewrite : (term -> term) -> (fmla -> fmla) -> task -> task trans
(* dependent transformatons *)
val on_theory : theory -> (tdecl_set -> 'a trans) -> 'a trans
val on_meta : meta -> (tdecl_set -> 'a trans) -> 'a trans
val on_theories_metas : theory list -> meta list ->
(clone_map -> meta_map -> 'a trans) -> 'a trans
val on_theories : theory list -> (clone_map -> 'a trans) -> 'a trans
val on_metas : meta list -> (meta_map -> 'a trans) -> 'a trans
val on_metas : meta list -> (meta_map -> 'a trans) -> 'a trans
val on_theories_metas : theory list -> meta list ->
(clone_map -> meta_map -> 'a trans) -> 'a trans
val on_theory : theory -> (symbol_map list -> 'a trans) -> 'a trans
val on_meta : meta -> (meta_arg list list -> 'a trans) -> 'a trans
val on_meta_excl : meta -> (meta_arg list option -> 'a trans) -> 'a trans
val on_tagged_ts : meta -> (Sts.t -> 'a trans) -> 'a trans
val on_tagged_ls : meta -> (Sls.t -> 'a trans) -> 'a trans
val on_tagged_pr : meta -> (Spr.t -> 'a trans) -> 'a trans
(** {2 Registration} *)
......
......@@ -82,9 +82,8 @@ and rewriteF f = f_map rewriteT rewriteF f
let close d = [decl_map rewriteT rewriteF d]
let close_epsilon =
let td = create_null_clone highord_theory in
Trans.on_theory highord_theory (fun tds ->
if Stdecl.mem td tds.tds_set then Trans.decl close None
Trans.on_theory highord_theory (fun sml ->
if List.exists Theory.is_empty_sm sml then Trans.decl close None
else Trans.identity)
let () = Trans.register_transform "close_epsilon" close_epsilon
......
......@@ -42,9 +42,9 @@ let elim q d = match d.d_node with
ld @ id
| _ -> [d]
let eliminate_builtin = Trans.on_meta Printer.meta_syntax_logic (fun tds ->
let rem_ls = Task.find_tagged_ls Printer.meta_syntax_logic tds Sls.empty in
Trans.decl (elim rem_ls) None)
let eliminate_builtin =
Trans.on_tagged_ls Printer.meta_syntax_logic
(fun rem_ls -> Trans.decl (elim rem_ls) None)
let () = Trans.register_transform "eliminate_builtin" eliminate_builtin
......
......@@ -45,8 +45,8 @@ let poly_smt_opt = poly_opt
let poly_tptp_opt = { poly_opt with default = "explicit" }
let enco_gen opt env =
Trans.on_meta opt.meta (fun tds ->
let s = match get_meta_excl opt.meta tds with
Trans.on_meta_excl opt.meta (fun alo ->
let s = match alo with
| None -> opt.default
| Some [MAstr s] -> s
| _ -> assert false in
......@@ -61,8 +61,8 @@ let enco_poly_smt = enco_gen poly_smt_opt
let enco_poly_tptp = enco_gen poly_tptp_opt
let maybe_encoding_enumeration =
Trans.on_meta poly_smt_opt.meta (fun tds ->
let s = match get_meta_excl poly_smt_opt.meta tds with
Trans.on_meta_excl poly_smt_opt.meta (fun alo ->
let s = match alo with
| None -> poly_smt_opt.default
| Some [MAstr s] -> s
| _ -> assert false in
......
......@@ -279,8 +279,7 @@ let decl tenv d =
res
*)
let t env = Trans.on_meta meta_kept (fun tds ->
let s = Task.find_tagged_ts meta_kept tds Sts.empty in
let t env = Trans.on_tagged_ts meta_kept (fun s ->
let init_task,tenv = load_prelude s env in
Trans.tdecl (decl tenv) init_task)
......
......@@ -104,8 +104,8 @@ let mono_init =
let mono kept =
Trans.decl (d_monomorph ty_base kept (lsmap kept)) mono_init
let t = Trans.on_meta Encoding.meta_kept (fun tds ->
let kept = Libencoding.get_kept_types tds in
let t = Trans.on_tagged_ts Encoding.meta_kept (fun tss ->
let kept = Libencoding.get_kept_types tss in
Trans.compose (deco kept) (mono kept))
let () = Encoding.register_enco_poly "decorate" (const t)
......
......@@ -267,8 +267,7 @@ let decl tenv d =
res
*)
let t env = Trans.on_meta Printer.meta_syntax_logic (fun tds ->
let rem_ls = Task.find_tagged_ls Printer.meta_syntax_logic tds Sls.empty in
let t env = Trans.on_tagged_ls Printer.meta_syntax_logic (fun rem_ls ->
let init_task,tenv = load_prelude rem_ls env in
Trans.tdecl (decl tenv) init_task)
......
......@@ -81,8 +81,7 @@ let decl tenv d = match d.d_node with
let encoding_enumeration =
let projs = Hts.create 17 in
Trans.on_meta meta_enum (fun tds ->
let enum = Task.find_tagged_ts meta_enum tds Sts.empty in
Trans.on_tagged_ts meta_enum (fun enum ->
let tenv = { enum = enum ; projs = projs } in
Trans.decl (decl tenv) None)
......
......@@ -152,8 +152,8 @@ let lsmap tyb kept = Wls.memoize 63 (fun ls ->
let d_ts_base = create_ty_decl [ts_base, Tabstract]
let monomorph tyb = Trans.on_meta Encoding.meta_kept (fun tds ->
let kept = Libencoding.get_kept_types tds in
let monomorph tyb = Trans.on_tagged_ts Encoding.meta_kept (fun tss ->
let kept = Libencoding.get_kept_types tss in
let tyb = match tyb.ty_node with
| Tyapp (_,[]) when not (Sty.mem tyb kept) -> tyb
| _ -> ty_base
......@@ -161,8 +161,8 @@ let monomorph tyb = Trans.on_meta Encoding.meta_kept (fun tds ->
let decl = Libencoding.d_monomorph tyb kept (lsmap tyb kept) in
Trans.decl decl (Task.add_decl None d_ts_base))
let monomorph = Trans.on_meta Encoding.meta_base (fun tds ->
let tyb = match Task.get_meta_excl Encoding.meta_base tds with
let monomorph = Trans.on_meta_excl Encoding.meta_base (fun alo ->
let tyb = match alo with
| Some [Theory.MAts ts] when ts.ts_args = [] ->
begin match ts.ts_def with
| Some ty -> ty
......
......@@ -79,10 +79,7 @@ let keep_no_builtin rem_ls = function
let filter_trigger_builtin =
Trans.on_meta Printer.meta_syntax_logic (fun tds ->
let rem_ls =
Task.find_tagged_ls Printer.meta_syntax_logic tds Sls.empty
in
Trans.on_tagged_ls Printer.meta_syntax_logic (fun rem_ls ->
let rt,rf = make_rt_rf (keep_no_builtin rem_ls) in
Trans.rewrite rt rf None)
......
......@@ -206,8 +206,7 @@ let d_monomorph ty_base kept lsmap d =
Sls.fold add !consts dl
(* convert tysymbols tagged with meta_kept to a set of types *)
let get_kept_types tds =
let tss = Task.find_tagged_ts Encoding.meta_kept tds Sts.empty in
let get_kept_types tss =
let add ts acc =
if ts.ts_args <> [] then acc
else match ts.ts_def with
......
......@@ -49,5 +49,5 @@ val lsdecl_of_tydecl : ty_decl list -> decl list
val d_monomorph : ty -> Sty.t -> (lsymbol -> lsymbol) -> decl -> decl list
(* convert tysymbols tagged with meta_kept to a set of types *)
val get_kept_types : Task.tdecl_set -> Sty.t
val get_kept_types : Sts.t -> Sty.t
......@@ -66,11 +66,11 @@ let lift_epsilon kind = Trans.fold (lift kind) None
let meta_epsilon = Theory.register_meta_excl "lift_epsilon" [MTstring]
let lift_epsilon = Trans.on_meta meta_epsilon
(fun tset ->
let kind = match get_meta_excl meta_epsilon tset with
| Some ([MAstr "implicit"]) -> Implicit
| Some ([MAstr "implied"]) | None -> Implied
let lift_epsilon = Trans.on_meta_excl meta_epsilon
(fun alo ->
let kind = match alo with
| Some [MAstr "implicit"] -> Implicit
| Some [MAstr "implied"] | None -> Implied
| _ -> failwith "lift_epsilon accepts only 'implicit' and 'implied'"
in
lift_epsilon kind)
......
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