Commit 017deebd authored by Andrei Paskevich's avatar Andrei Paskevich

keep real symbols in Clone and Meta

parent 7209c060
......@@ -86,7 +86,7 @@ module Spr = Prop.S
module Mpr = Prop.M
module Hpr = Prop.H
let pr_equal pr1 pr2 = id_equal pr1.pr_name pr2.pr_name
let pr_equal = (==)
let create_prsymbol n = { pr_name = id_register n }
......
......@@ -43,18 +43,11 @@ let iprinter,tprinter,lprinter,pprinter =
create_ident_printer bl ~sanitizer:isanitize,
create_ident_printer bl ~sanitizer:usanitize
let thash = Hid.create 63
let lhash = Hid.create 63
let phash = Hid.create 63
let forget_all () =
forget_all iprinter;
forget_all tprinter;
forget_all lprinter;
forget_all pprinter;
Hid.clear thash;
Hid.clear lhash;
Hid.clear phash
forget_all pprinter
let tv_set = ref Sid.empty
......@@ -81,20 +74,16 @@ let print_th fmt th =
fprintf fmt "%s" (id_unique iprinter ~sanitizer th.th_name)
let print_ts fmt ts =
Hid.replace thash ts.ts_name ts;
fprintf fmt "%s" (id_unique tprinter ts.ts_name)
let print_ls fmt ls =
Hid.replace lhash ls.ls_name ls;
fprintf fmt "%s" (id_unique lprinter ls.ls_name)
let print_cs fmt ls =
Hid.replace lhash ls.ls_name ls;
let sanitizer = String.capitalize in
fprintf fmt "%s" (id_unique lprinter ~sanitizer ls.ls_name)
let print_pr fmt pr =
Hid.replace phash pr.pr_name pr;
fprintf fmt "%s" (id_unique pprinter pr.pr_name)
(** Types *)
......@@ -328,41 +317,35 @@ let print_decl fmt d = match d.d_node with
| Dind il -> print_list newline print_ind_decl fmt il
| Dprop p -> print_prop_decl fmt p
let print_inst fmt (id1,id2) =
if Hid.mem thash id2 then
let n = id_unique tprinter id1 in
fprintf fmt "type %s = %a" n print_ts (Hid.find thash id2)
else if Hid.mem lhash id2 then
let n = id_unique lprinter id1 in
fprintf fmt "logic %s = %a" n print_ls (Hid.find lhash id2)
else if Hid.mem phash id2 then
let n = id_unique pprinter id1 in
fprintf fmt "prop %s = %a" n print_pr (Hid.find phash id2)
else
fprintf fmt "ident %s = %s" id1.id_string id2.id_string
let print_inst_ts fmt (ts1,ts2) =
fprintf fmt "type %a = %a" print_ts ts1 print_ts ts2
let print_inst_ls fmt (ls1,ls2) =
fprintf fmt "logic %a = %a" print_ls ls1 print_ls ls2
let print_inst_pr fmt (pr1,pr2) =
fprintf fmt "prop %a = %a" print_pr pr1 print_pr pr2
let print_meta_arg fmt = function
| MARid id ->
if Hid.mem thash id then
fprintf fmt "type %a" print_ts (Hid.find thash id)
else if Hid.mem lhash id then
fprintf fmt "logic %a" print_ls (Hid.find lhash id)
else if Hid.mem phash id then
fprintf fmt "prop %a" print_pr (Hid.find phash id)
else
fprintf fmt "ident %s" id.id_string
| MARstr s -> fprintf fmt "\"%s\"" s
| MARint i -> fprintf fmt "%d" i
| MAts ts -> fprintf fmt "type %a" print_ts ts
| MAls ls -> fprintf fmt "logic %a" print_ls ls
| MApr pr -> fprintf fmt "prop %a" print_pr pr
| MAstr s -> fprintf fmt "\"%s\"" s
| MAint i -> fprintf fmt "%d" i
let print_tdecl fmt td = match td.td_node with
| Decl d ->
print_decl fmt d
| Use th ->
fprintf fmt "@[<hov 2>(* use %a *)@]" print_th th
| Clone (th,inst) ->
let inst = Mid.fold (fun x y a -> (x,y)::a) inst [] in
fprintf fmt "@[<hov 2>(* clone %a with %a *)@]"
print_th th (print_list comma print_inst) inst
| Clone (th,tm,lm,pm) ->
let tm = Mts.fold (fun x y a -> (x,y)::a) tm [] in
let lm = Mls.fold (fun x y a -> (x,y)::a) lm [] in
let pm = Mpr.fold (fun x y a -> (x,y)::a) pm [] in
fprintf fmt "@[<hov 2>(* clone %a with %a,%a,%a *)@]"
print_th th (print_list comma print_inst_ts) tm
(print_list comma print_inst_ls) lm
(print_list comma print_inst_pr) pm
| Meta (t,al) ->
fprintf fmt "@[<hov 2>(* meta %s %a *)@]"
t (print_list space print_meta_arg) al
......
......@@ -47,7 +47,7 @@ val print_fmla : formatter -> fmla -> unit (* formula *)
val print_expr : formatter -> expr -> unit (* term or formula *)
val print_pkind : formatter -> prop_kind -> unit
val print_meta_arg : formatter -> meta_arg_real -> unit
val print_meta_arg : formatter -> meta_arg -> unit
val print_type_decl : formatter -> ty_decl -> unit
val print_logic_decl : formatter -> logic_decl -> unit
......
......@@ -113,7 +113,8 @@ let print_prelude fmt pl =
let print_th_prelude task fmt pm =
let th_used = task_fold (fun acc -> function
| { td_node = Clone (th,cl) } when Mid.is_empty cl -> th::acc
| { td_node = Clone (th,tm,lm,pm) }
when Mts.is_empty tm && Mls.is_empty lm && Mpr.is_empty pm -> th::acc
| _ -> acc) [] task
in
List.iter (fun th ->
......@@ -145,14 +146,22 @@ let remove_logic ls = create_meta meta_remove_logic [MAls ls]
let remove_prop pr = create_meta meta_remove_prop [MApr pr]
let get_remove_set task =
let add td s = match td.td_node with
| Meta (_,[MARid id]) -> Sid.add id s
let add_ts td s = match td.td_node with
| Meta (_,[MAts ts]) -> Sid.add ts.ts_name s
| _ -> assert false
in
let add_ls td s = match td.td_node with
| Meta (_,[MAls ls]) -> Sid.add ls.ls_name s
| _ -> assert false
in
let add_pr td s = match td.td_node with
| Meta (_,[MApr pr]) -> Sid.add pr.pr_name s
| _ -> assert false
in
let s = Sid.empty in
let s = Stdecl.fold add (find_meta task meta_remove_type).tds_set s in
let s = Stdecl.fold add (find_meta task meta_remove_logic).tds_set s in
let s = Stdecl.fold add (find_meta task meta_remove_prop).tds_set s in
let s = Stdecl.fold add_ts (find_meta task meta_remove_type).tds_set s in
let s = Stdecl.fold add_ls (find_meta task meta_remove_logic).tds_set s in
let s = Stdecl.fold add_pr (find_meta task meta_remove_prop).tds_set s in
s
(** {2 exceptions to use in transformations and printers} *)
......
......@@ -165,7 +165,7 @@ let add_ind_decls tk dl = List.fold_left add_decl tk (create_ind_decls dl)
let rec add_tdecl task td = match td.td_node with
| Decl d -> new_decl task d td
| Use th -> use_export task th
| Clone (th,_) -> add_clone task th td
| Clone (th,_,_,_) -> add_clone task th td
| Meta (t,_) -> add_meta task t td
and flat_tdecl task td = match td.td_node with
......@@ -215,13 +215,31 @@ let task_decls = task_fold (fun acc td ->
exception NotTaggingMeta of string
let find_tagged t tds acc =
let find_tagged_ts t tds acc =
begin match lookup_meta t with
| [MTtysymbol|MTlsymbol|MTprsymbol] -> ()
| [MTtysymbol] -> ()
| _ -> raise (NotTaggingMeta t)
end;
Stdecl.fold (fun td acc -> match td.td_node with
| Meta (s, [MARid id]) when s = t -> Sid.add id acc
| Meta (s, [MAts ts]) when s = t -> Sts.add ts acc
| _ -> assert false) tds.tds_set acc
let find_tagged_ls t tds acc =
begin match lookup_meta t with
| [MTlsymbol] -> ()
| _ -> raise (NotTaggingMeta t)
end;
Stdecl.fold (fun td acc -> match td.td_node with
| Meta (s, [MAls ls]) when s = t -> Sls.add ls acc
| _ -> assert false) tds.tds_set acc
let find_tagged_pr t tds acc =
begin match lookup_meta t with
| [MTprsymbol] -> ()
| _ -> raise (NotTaggingMeta t)
end;
Stdecl.fold (fun td acc -> match td.td_node with
| Meta (s, [MApr pr]) when s = t -> Spr.add pr acc
| _ -> assert false) tds.tds_set acc
exception NotExclusiveMeta of string
......
......@@ -99,7 +99,9 @@ val task_goal : task -> prsymbol
exception NotTaggingMeta of string
val find_tagged : string -> tdecl_set -> Sid.t -> Sid.t
val find_tagged_ts : string -> tdecl_set -> Sts.t -> Sts.t
val find_tagged_ls : string -> tdecl_set -> Sls.t -> Sls.t
val find_tagged_pr : string -> tdecl_set -> Spr.t -> Spr.t
(* special selector for exclusive metaproperties *)
......
This diff is collapsed.
......@@ -54,11 +54,6 @@ type meta_arg =
| MAstr of string
| MAint of int
type meta_arg_real =
| MARid of ident
| MARstr of string
| MARint of int
val register_meta : string -> meta_arg_type list -> string
val register_meta_exc : string -> meta_arg_type list -> string
......@@ -86,8 +81,8 @@ and tdecl = private {
and tdecl_node = private
| Decl of decl
| Use of theory
| Clone of theory * ident Mid.t
| Meta of string * meta_arg_real list
| Clone of theory * tysymbol Mts.t * lsymbol Mls.t * prsymbol Mpr.t
| Meta of string * meta_arg list
module Stdecl : Set.S with type elt = tdecl
module Mtdecl : Map.S with type key = tdecl
......
......@@ -224,9 +224,10 @@ let print_task ?(debug=false) drv fmt task =
Mid.fold (fun _ (th,s) task ->
let cs = (find_clone task th).tds_set in
Stdecl.fold (fun td task -> match td.td_node with
| Clone (_,cl) when Mid.is_empty cl ->
| Clone (_,tm,lm,pm)
when Mts.is_empty tm && Mls.is_empty lm && Mpr.is_empty pm ->
Stdecl.fold (fun td task -> add_tdecl task td) s task
| _ -> assert false (* impossible *)
| _ -> task
) cs task
) drv.drv_meta task
in
......
......@@ -53,7 +53,7 @@ let forget_var v = forget_id ident_printer v.vs_name
type info = {
info_syn : syntax_map;
info_rem : Sid.t;
info_ac : Sid.t;
info_ac : Sls.t;
}
let rec print_type info fmt ty = match ty.ty_node with
......@@ -167,7 +167,7 @@ let ac_th = ["algebra";"AC"]
let print_logic_decl info fmt (ls,ld) =
match ld with
| None ->
let sac = if Sid.mem ls.ls_name info.info_ac then "ac " else "" in
let sac = if Sls.mem ls info.info_ac then "ac " else "" in
fprintf fmt "@[<hov 2>logic %s%a : %a%s%a@]@\n"
sac print_ident ls.ls_name
(print_list comma (print_type info)) ls.ls_args
......@@ -220,7 +220,8 @@ let print_task pr thpr syn fmt task =
let info = {
info_syn = syn;
info_rem = get_remove_set task;
info_ac = Task.find_tagged meta_ac (find_meta task meta_ac) Sid.empty }
info_ac =
Task.find_tagged_ls meta_ac (find_meta task meta_ac) Sls.empty }
in
let decls = Task.task_decls task in
ignore (print_list_opt (add_flush newline2) (print_decl info) fmt decls)
......
......@@ -68,6 +68,11 @@ let print_vs fmt vs =
let forget_var vs = forget_id iprinter vs.vs_name
(* theory names always start with an upper case letter *)
let print_th fmt th =
let sanitizer = String.capitalize in
fprintf fmt "%s" (id_unique iprinter ~sanitizer th.th_name)
let print_ts fmt ts =
fprintf fmt "%s" (id_unique tprinter ts.ts_name)
......@@ -336,22 +341,34 @@ let print_decl info fmt d = match d.d_node with
let print_decls info fmt dl =
fprintf fmt "@[<hov>%a@\n@]" (print_list nothing (print_decl info)) dl
let print_inst fmt (id1,id2) =
fprintf fmt "ident %s = %s" id1.id_string id2.id_string
let print_inst_ts fmt (ts1,ts2) =
fprintf fmt "type %a = %a" print_ts ts1 print_ts ts2
let print_inst_ls fmt (ls1,ls2) =
fprintf fmt "logic %a = %a" print_ls ls1 print_ls ls2
let print_inst_pr fmt (pr1,pr2) =
fprintf fmt "prop %a = %a" print_pr pr1 print_pr pr2
let print_meta_arg fmt = function
| MARid id -> fprintf fmt "ident %s" id.id_string
| MARstr s -> fprintf fmt "\"%s\"" s
| MARint i -> fprintf fmt "%d" i
| MAts ts -> fprintf fmt "type %a" print_ts ts
| MAls ls -> fprintf fmt "logic %a" print_ls ls
| MApr pr -> fprintf fmt "prop %a" print_pr pr
| MAstr s -> fprintf fmt "\"%s\"" s
| MAint i -> fprintf fmt "%d" i
let print_tdecl info fmt td = match td.td_node with
| Decl d -> print_decl info fmt d
| Use th ->
fprintf fmt "@[<hov 2>(* use %s *)@]@\n" th.th_name.id_string
| Clone (th,inst) ->
let inst = Mid.fold (fun x y a -> (x,y)::a) inst [] in
fprintf fmt "@[<hov 2>(* clone %s with %a *)@]@\n"
th.th_name.id_string (print_list comma print_inst) inst
fprintf fmt "@[<hov 2>(* use %a *)@]@\n" print_th th
| Clone (th,tm,lm,pm) ->
let tm = Mts.fold (fun x y a -> (x,y)::a) tm [] in
let lm = Mls.fold (fun x y a -> (x,y)::a) lm [] in
let pm = Mpr.fold (fun x y a -> (x,y)::a) pm [] in
fprintf fmt "@[<hov 2>(* clone %a with %a,%a,%a *)@]"
print_th th (print_list comma print_inst_ts) tm
(print_list comma print_inst_ls) lm
(print_list comma print_inst_pr) pm
| Meta (t,al) ->
fprintf fmt "@[<hov 2>(* meta %s %a *)@]@\n"
t (print_list space print_meta_arg) al
......
......@@ -25,11 +25,11 @@ open Decl
(** Discard definitions of built-in symbols *)
let add_ld q = function
| ls, Some _ when Sid.mem ls.ls_name q -> (ls, None)
| ls, Some _ when Sls.mem ls q -> (ls, None)
| d -> d
let add_id q (ld,id) = function
| ls, _ when Sid.mem ls.ls_name q -> (ls, None)::ld, id
| ls, _ when Sls.mem ls q -> (ls, None)::ld, id
| d -> ld, d::id
let elim q d = match d.d_node with
......@@ -40,13 +40,9 @@ let elim q d = match d.d_node with
create_logic_decls (List.rev ld) @ create_ind_decls (List.rev id)
| _ -> [d]
let eliminate_builtin =
Trans.on_metas
[ Printer.meta_remove_type;
Printer.meta_remove_logic;
Printer.meta_remove_prop ]
(fun mm ->
Trans.decl (elim (Mstr.fold Task.find_tagged mm Sid.empty)) None)
let eliminate_builtin = Trans.on_meta Printer.meta_remove_logic (fun tds ->
let rem_ls = Task.find_tagged_ls Printer.meta_remove_logic tds Sls.empty in
Trans.decl (elim rem_ls) None)
let () = Trans.register_transform "eliminate_builtin" eliminate_builtin
......
......@@ -32,32 +32,11 @@ let meta_kept = register_meta "encoding_decorate : kept" [MTtysymbol]
(* From Encoding Polymorphism CADE07*)
module Prelude =
struct
(* let create_ty s = ty_app (create_tysymbol (id_fresh s) [] None) [] in
let deco = create_ty "deco" in
let undeco = create_ty "undeco" in
let ty = create_ty "ty" in
let csort = create_fsymbol (id_fresh "csort") [ty;undeco] deco in
*)
(* let spec_conv ts =
let name = ts.ts_name.id_string in
let d2ty = create_fsymbol (id_fresh ("d2"^name)) [deco] (ty_app ts []) in
let ty2u = create_fsymbol (id_fresh (name^"2u")) [(ty_app ts [])] undeco in
let axiom =
let l =
List.fold_left (fun acc ty -> Sty.add ty acc) Sty.empty l
*)
end
type lconv = {d2t : lsymbol;
t2u : lsymbol;
tty : term}
type tenv = {kept : Sid.t option;
type tenv = {kept : Sts.t option;
clone_builtin : tysymbol -> Theory.tdecl list;
specials : lconv Hty.t;
deco : ty;
......@@ -128,7 +107,7 @@ let is_kept tenv ts =
ts_equal ts ts_int || ts_equal ts ts_real (* for the constant *)
|| match tenv.kept with
| None -> true (* every_simple *)
| Some s -> Sid.mem ts.ts_name s
| Some s -> Sts.mem ts s
end
(* Translate a type to a term *)
......@@ -352,7 +331,7 @@ let decl tenv d =
*)
let t env = Trans.on_meta meta_kept (fun tds ->
let s = Task.find_tagged meta_kept tds Sid.empty in
let s = Task.find_tagged_ts meta_kept tds Sts.empty in
let init_task,tenv = load_prelude (Some s) env in
Trans.tdecl (decl tenv) init_task)
......
......@@ -34,7 +34,7 @@ let why_filename = ["transform" ; "encoding_decorate"]
let meta_kept = register_meta "encoding_decorate : kept" [MTtysymbol]
(* From Encoding Polymorphism CADE07*)
type tenv = {rem_ls : Sid.t;
type tenv = {rem_ls : Sls.t;
unsorted : ty;
sort : lsymbol;
real_to_int : lsymbol;
......@@ -221,7 +221,7 @@ Perhaps you could use eliminate_definition"
Hls.find tenv.trans_lsymbol ls1
with Not_found -> conv_ls tenv ls1 in
let acc = create_logic_decl [ls2,None] :: acc in
let acc = if Sid.mem ls1.ls_name tenv.rem_ls && is_kept ls1
let acc = if Sls.mem ls1 tenv.rem_ls && is_kept ls1
then begin
let make _ = create_vsymbol (id_fresh "x") ty_int in
let vars = List.map make ls1.ls_args in
......@@ -267,11 +267,8 @@ let decl tenv d =
res
*)
let t env = Trans.on_meta Printer.meta_remove_logic
(fun tds ->
let rem_ls =
Task.find_tagged Printer.meta_remove_logic tds Sid.empty
in
let t env = Trans.on_meta Printer.meta_remove_logic (fun tds ->
let rem_ls = Task.find_tagged_ls Printer.meta_remove_logic tds Sls.empty in
let init_task,tenv = load_prelude rem_ls env in
Trans.tdecl (decl tenv) init_task)
......
......@@ -30,7 +30,7 @@ let why_filename = Encoding_decorate.why_filename
let meta_enum = Eliminate_algebraic.meta_enum
type tenv = {kept : Sid.t;
type tenv = {kept : Sts.t;
projs : lsymbol Hts.t}
(* trans_lsymbol ne depend pour l'instant pas du but,
comme specials_type ne depend pas*)
......@@ -50,8 +50,7 @@ let add_proj tenv ts =
let find_proj tenv ty =
match ty.ty_node with
| Tyapp (tys,_) when Sid.mem tys.ts_name tenv.kept ->
Some (Hts.find tenv.projs tys)
| Tyapp (ts,_) when Sts.mem ts tenv.kept -> Some (Hts.find tenv.projs ts)
| _ -> None
......@@ -113,7 +112,7 @@ let decl (tenv:tenv) d =
let fnT = rewrite_term tenv Mvs.empty in
let fnF = rewrite_fmla tenv Mvs.empty in
match d.d_node with
| Dtype [ts,Tabstract] when Sid.mem ts.ts_name tenv.kept ->
| Dtype [ts,Tabstract] when Sts.mem ts tenv.kept ->
let ls = add_proj tenv ts in
[d;create_logic_decl [(ls,None)]]
| Dtype [_] -> [d]
......@@ -136,7 +135,7 @@ let decl tenv d =
let t env =
let init_task, projs = load_prelude env in
Trans.on_meta meta_enum (fun tds ->
let kept = Task.find_tagged meta_enum tds Sid.empty in
let kept = Task.find_tagged_ts meta_enum tds Sts.empty in
let tenv = { kept = kept; projs = projs} in
Trans.decl (decl tenv) init_task)
......
......@@ -74,14 +74,14 @@ let () = Trans.register_transform "filter_trigger" filter_trigger
let keep_no_builtin rem_ls = function
| Term _ -> true
| Fmla {f_node = Fapp (ps,_)} -> not (Ident.Sid.mem ps.ls_name rem_ls)
| Fmla {f_node = Fapp (ps,_)} -> not (Sls.mem ps rem_ls)
| _ -> false
let filter_trigger_builtin =
Trans.on_meta Printer.meta_remove_logic (fun tds ->
let rem_ls =
Task.find_tagged Printer.meta_remove_logic tds Ident.Sid.empty
Task.find_tagged_ls Printer.meta_remove_logic tds Sls.empty
in
let rt,rf = make_rt_rf (keep_no_builtin rem_ls) in
Trans.rewrite rt rf None)
......
......@@ -82,7 +82,7 @@ let string_of_expr_node node =
let b = Buffer.create 42 in
Format.bprintf b "@[%a@]" printer x;
Buffer.contents b in
let white_space = Str.regexp "[ \(\)]" in
let white_space = Str.regexp "[ ()]" in
let translate x = Str.global_replace white_space "_" x in
let repr = match node with
| Term t -> print_in_buf Pretty.print_term t
......
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