Commit d1ece135 authored by Andrei Paskevich's avatar Andrei Paskevich

remove 'remove_set', 'syntax_map' is enough

also, introduce in Printer the p-printing transformations
parent 975e611d
......@@ -114,7 +114,7 @@ LIBGENERATED = src/util/rc.ml src/parser/lexer.ml \
LIB_UTIL = stdlib exn_printer debug pp loc print_tree \
cmdline hashweak hashcons util sysutil rc plugin
LIB_CORE = ident ty term pattern decl theory task pretty env printer trans
LIB_CORE = ident ty term pattern decl theory task pretty env trans printer
LIB_PARSER = ptree denv typing parser lexer
......
......@@ -50,6 +50,8 @@ let lookup_printer s =
let list_printers () = Hashtbl.fold (fun k _ acc -> k::acc) printers []
let () = register_printer "(null)" (fun _ _ _ ?old _ _ -> ignore old)
(** Syntax substitutions *)
let opt_search_forward re s pos =
......@@ -99,7 +101,6 @@ let check_syntax s len =
in
iter_group regexp_arg_pos arg s
let check_syntax_typed s len ret =
let arg s =
let grp = (Str.matched_group 1 s) in
......@@ -182,50 +183,66 @@ let syntax_logic ls s =
let remove_prop pr =
create_meta meta_remove_prop [MApr pr]
let get_syntax_map, get_syntax_map_of_theory =
let add_ts m = function
| [MAts ts; MAstr s] ->
Mid.add_new ts.ts_name s (KnownTypeSyntax ts) m
| _ -> assert false
in
let add_ls m = function
| [MAls ls; MAstr s] ->
Mid.add_new ls.ls_name s (KnownLogicSyntax ls) m
| _ -> assert false
in
(fun task ->
let m = Mid.empty in
let m = Task.on_meta meta_syntax_logic add_ls m task in
let m = Task.on_meta meta_syntax_type add_ts m task in
m),
(fun theory ->
let m = Mid.empty in
let m = Theory.on_meta meta_syntax_logic add_ls m theory in
let m = Theory.on_meta meta_syntax_type add_ts m theory in
m)
let get_remove_set task =
let add_ts s = function
| [MAts ts; _] -> Sid.add ts.ts_name s
| _ -> assert false
in
let add_ls s = function
| [MAls ls; _] -> Sid.add ls.ls_name s
| _ -> assert false
in
let add_pr s = function
| [MApr pr] -> Sid.add pr.pr_name s
| _ -> assert false
in
let s = Sid.empty in
let s = Task.on_meta meta_syntax_type add_ts s task in
let s = Task.on_meta meta_syntax_logic add_ls s task in
let s = Task.on_meta meta_remove_prop add_pr s task in
s
type syntax_map = string Mid.t
let sm_add_ts sm = function
| [MAts ts; MAstr rs] -> Mid.add_new ts.ts_name rs (KnownTypeSyntax ts) sm
| _ -> assert false
let sm_add_ls sm = function
| [MAls ls; MAstr rs] -> Mid.add_new ls.ls_name rs (KnownLogicSyntax ls) sm
| _ -> assert false
let sm_add_pr sm = function
| [MApr pr] -> Mid.add pr.pr_name "" sm
| _ -> assert false
let get_syntax_map task =
let sm = Mid.empty in
let sm = Task.on_meta meta_syntax_type sm_add_ts sm task in
let sm = Task.on_meta meta_syntax_logic sm_add_ls sm task in
let sm = Task.on_meta meta_remove_prop sm_add_pr sm task in
sm
let get_syntax_map_of_theory theory =
let sm = Mid.empty in
let sm = Theory.on_meta meta_syntax_type sm_add_ts sm theory in
let sm = Theory.on_meta meta_syntax_logic sm_add_ls sm theory in
let sm = Theory.on_meta meta_remove_prop sm_add_pr sm theory in
sm
let query_syntax sm id = Mid.find_option id sm
let fold_tdecls fn acc =
Trans.on_meta meta_syntax_type (fun sts ->
Trans.on_meta meta_syntax_logic (fun sls ->
Trans.on_meta meta_remove_prop (fun spr ->
let sm = Mid.empty in
let sm = List.fold_left sm_add_ts sm sts in
let sm = List.fold_left sm_add_ls sm sls in
let sm = List.fold_left sm_add_pr sm spr in
Trans.fold (fun t -> fn sm t.task_decl) acc)))
let sprint_tdecls (fn : syntax_map -> tdecl pp) =
let buf = Buffer.create 512 in
let fmt = Format.formatter_of_buffer buf in
let print sm td acc =
Buffer.reset buf;
Format.fprintf fmt "%a@?" (fn sm) td;
Buffer.contents buf :: acc in
fold_tdecls print []
let sprint_decls (fn : syntax_map -> decl pp) =
let buf = Buffer.create 512 in
let fmt = Format.formatter_of_buffer buf in
let print sm td acc = match td.td_node with
| Decl d ->
Buffer.reset buf;
Format.fprintf fmt "%a@?" (fn sm) d;
Buffer.contents buf :: acc
| _ -> acc in
fold_tdecls print []
(** {2 exceptions to use in transformations and printers} *)
exception UnsupportedType of ty * string
......
......@@ -53,22 +53,29 @@ val syntax_type : tysymbol -> string -> tdecl
val syntax_logic : lsymbol -> string -> tdecl
val remove_prop : prsymbol -> tdecl
val get_syntax_map : task -> string Mid.t
val get_remove_set : task -> Sid.t
type syntax_map = string Mid.t
(* [syntax_map] maps the idents of removed props to "" *)
val get_syntax_map_of_theory : theory -> string Mid.t
val get_syntax_map : task -> syntax_map
val get_syntax_map_of_theory : theory -> syntax_map
val query_syntax : string Mid.t -> ident -> string option
val query_syntax : syntax_map -> ident -> string option
val syntax_arguments : string -> 'a pp -> 'a list pp
(** (syntax_arguments templ print_arg fmt l) prints in the formatter fmt
the list l using the template templ and the printer print_arg *)
val syntax_arguments_typed : string -> term pp -> ty pp ->
term option -> term list pp
val syntax_arguments_typed :
string -> term pp -> ty pp -> term option -> term list pp
(** (syntax_arguments templ print_arg fmt l) prints in the formatter fmt
the list l using the template templ and the printer print_arg *)
(** {2 pretty-printing transformations (useful for caching)} *)
val fold_tdecls : (syntax_map -> tdecl -> 'a -> 'a) -> 'a -> 'a Trans.trans
val sprint_tdecls : (syntax_map -> tdecl pp) -> string list Trans.trans
val sprint_decls : (syntax_map -> decl pp) -> string list Trans.trans
(** {2 exceptions to use in transformations and printers} *)
......
......@@ -53,8 +53,7 @@ let print_tvsymbols fmt tv =
let forget_var v = forget_id ident_printer v.vs_name
type info = {
info_syn : string Mid.t;
info_rem : Sid.t;
info_syn : syntax_map;
info_ac : Sls.t;
}
......@@ -173,7 +172,7 @@ let print_type_decl fmt ts = match ts.ts_args with
(print_list comma print_tvsymbols) tl print_ident ts.ts_name
let print_type_decl info fmt = function
| ts, Tabstract when Sid.mem ts.ts_name info.info_rem -> false
| ts, Tabstract when Mid.mem ts.ts_name info.info_syn -> false
| ts, Tabstract -> print_type_decl fmt ts; true
| _, Talgebraic _ -> unsupported
"alt-ergo : algebraic datatype are not supported"
......@@ -208,7 +207,7 @@ let print_logic_decl info fmt (ls,ld) =
List.iter forget_var vl
let print_logic_decl info fmt d =
if Sid.mem (fst d).ls_name info.info_rem then
if Mid.mem (fst d).ls_name info.info_syn then
false else (print_logic_decl info fmt d; true)
let print_decl info fmt d = match d.d_node with
......@@ -218,7 +217,7 @@ let print_decl info fmt d = match d.d_node with
print_list_opt newline (print_logic_decl info) fmt dl
| Dind _ -> unsupportedDecl d
"alt-ergo : inductive definition are not supported"
| Dprop (Paxiom, pr, _) when Sid.mem pr.pr_name info.info_rem -> false
| Dprop (Paxiom, pr, _) when Mid.mem pr.pr_name info.info_syn -> false
| Dprop (Paxiom, pr, f) ->
fprintf fmt "@[<hov 2>axiom %a :@ %a@]@\n"
print_ident pr.pr_name (print_fmla info) f; true
......@@ -235,7 +234,6 @@ let print_task pr thpr fmt task =
print_th_prelude task fmt thpr;
let info = {
info_syn = get_syntax_map task;
info_rem = get_remove_set task;
info_ac = Task.on_tagged_ls meta_ac task }
in
let decls = Task.task_decls task in
......
......@@ -100,8 +100,7 @@ let print_pr fmt pr =
(* info *)
type info = {
info_syn : string Mid.t;
info_rem : Sid.t;
info_syn : syntax_map;
realization : bool;
}
......@@ -525,7 +524,7 @@ let print_type_decl ~old info fmt (ts,def) =
fprintf fmt "@\n"
let print_type_decl ~old info fmt d =
if not (Sid.mem (fst d).ts_name info.info_rem) then
if not (Mid.mem (fst d).ts_name info.info_syn) then
(print_type_decl ~old info fmt d; forget_tvs ())
let print_ls_type ?(arrow=false) info fmt ls =
......@@ -560,7 +559,7 @@ let print_logic_decl ~old info fmt (ls,ld) =
fprintf fmt "@\n"
let print_logic_decl ~old info fmt d =
if not (Sid.mem (fst d).ls_name info.info_rem) then
if not (Mid.mem (fst d).ls_name info.info_syn) then
(print_logic_decl ~old info fmt d; forget_tvs ())
let print_recursive_decl info tm fmt (ls,ld) =
......@@ -608,7 +607,7 @@ let print_ind_decl info fmt (ps,bl) =
fprintf fmt "@\n"
let print_ind_decl info fmt d =
if not (Sid.mem (fst d).ls_name info.info_rem) then
if not (Mid.mem (fst d).ls_name info.info_syn) then
(print_ind_decl info fmt d; forget_tvs ())
let print_pkind info fmt = function
......@@ -644,7 +643,7 @@ let print_decl ~old info fmt d = match d.d_node with
print_recursive_decl info fmt ll
| Dind il ->
print_list nothing (print_ind_decl info) fmt il
| Dprop (_,pr,_) when Sid.mem pr.pr_name info.info_rem ->
| Dprop (_,pr,_) when Mid.mem pr.pr_name info.info_syn ->
()
| Dprop (k,pr,f) ->
print_proof_context ~old info fmt k;
......@@ -665,7 +664,6 @@ let print_task _env pr thpr ?old fmt task =
print_th_prelude task fmt thpr;
let info = {
info_syn = get_syntax_map task;
info_rem = get_remove_set task;
realization = false;
} in
let old = match old with
......@@ -702,11 +700,10 @@ let print_theory _env pr thpr ?old fmt th =
(* TODO
let info = {
info_syn = get_syntax_map th;
info_rem = get_remove_set th} in
info_syn = get_remove_set th} in
*)
let info = {
info_syn = Mid.empty (* get_syntax_map_of_theory th *);
info_rem = Mid.empty;
realization = true;
}
in
......
......@@ -63,8 +63,7 @@ let print_ident fmt id =
(** type *)
type info = {
info_syn : string Mid.t;
info_rem : Sid.t;
info_syn : syntax_map;
complex_type : ty Hty.t;
}
......@@ -240,7 +239,7 @@ let print_logic_binder info fmt v =
(print_type info) v.vs_ty
let print_type_decl info fmt = function
| ts, Tabstract when Sid.mem ts.ts_name info.info_rem -> false
| ts, Tabstract when Mid.mem ts.ts_name info.info_syn -> false
| ts, Tabstract when ts.ts_args = [] ->
fprintf fmt "%a : TYPE;" print_ident ts.ts_name; true
| _, Tabstract -> false
......@@ -273,7 +272,7 @@ let print_logic_decl info fmt (ls,ld) =
List.iter forget_var vsl
let print_logic_decl info fmt d =
if Sid.mem (fst d).ls_name info.info_rem then
if Mid.mem (fst d).ls_name info.info_syn then
false else (print_logic_decl info fmt d; true)
let print_decl info fmt d = match d.d_node with
......@@ -283,7 +282,7 @@ let print_decl info fmt d = match d.d_node with
print_list_opt newline (print_logic_decl info) fmt dl
| Dind _ -> unsupportedDecl d
"cvc3 : inductive definition are not supported"
| Dprop (Paxiom, pr, _) when Sid.mem pr.pr_name info.info_rem -> false
| Dprop (Paxiom, pr, _) when Mid.mem pr.pr_name info.info_syn -> false
| Dprop (Paxiom, pr, f) ->
find_complex_type info fmt f;
fprintf fmt "@[<hov 2>%% %s@\nASSERT@ %a;@]@\n"
......@@ -325,7 +324,6 @@ let print_task pr thpr fmt task =
let info = {
info_syn = Mid.union (fun _ _ s -> Some s)
(get_syntax_map task) (Trans.apply distingued task);
info_rem = get_remove_set task;
complex_type = Hty.create 5;
}
in
......
......@@ -84,8 +84,7 @@ type info = {
info_env : Env.env;
info_symbols : Sid.t;
info_ops_of_rel : (string * string * string) Mls.t;
info_syn : string Mid.t;
info_rem : Sid.t;
info_syn : syntax_map;
}
let int_minus = ref ps_equ
......@@ -120,7 +119,6 @@ let get_info env task =
info_symbols = symb;
info_ops_of_rel = ops;
info_syn = syn;
info_rem = get_remove_set task;
}
(* Gappa printing *)
......
......@@ -41,8 +41,7 @@ let forget_var v = forget_id ident_printer v.vs_name
let print_var fmt {vs_name = id} = print_ident fmt id
type info = {
info_syn : string Mid.t;
info_rem : Sid.t;
info_syn : syntax_map;
}
let rec print_term info fmt t = match t.t_node with
......@@ -140,7 +139,7 @@ let print_logic_decl _drv _fmt (_ls,ld) = match ld with
unsupported "Predicate and function definition aren't supported"
let print_logic_decl info fmt d =
if Sid.mem (fst d).ls_name info.info_rem then false
if Mid.mem (fst d).ls_name info.info_syn then false
else begin print_logic_decl info fmt d; true end
let print_decl info fmt d = match d.d_node with
......@@ -150,7 +149,7 @@ let print_decl info fmt d = match d.d_node with
print_list_opt newline (print_logic_decl info) fmt dl
| Dind _ ->
unsupportedDecl d "simplify : inductive definition are not supported"
| Dprop (Paxiom, pr, _) when Sid.mem pr.pr_name info.info_rem ->
| Dprop (Paxiom, pr, _) when Mid.mem pr.pr_name info.info_syn ->
false
| Dprop (Paxiom, pr, f) ->
fprintf fmt "@[(BG_PUSH@\n ;; axiom %s@\n @[<hov 2>%a@])@]@\n"
......@@ -174,8 +173,7 @@ let print_task pr thpr fmt task =
print_prelude fmt pr;
print_th_prelude task fmt thpr;
let info = {
info_syn = get_syntax_map task;
info_rem = get_remove_set task }
info_syn = get_syntax_map task }
in
let decls = Task.task_decls task in
ignore (print_list_opt (add_flush newline2) (print_decl info) fmt decls)
......
......@@ -57,8 +57,7 @@ let print_var fmt {vs_name = id} =
fprintf fmt "%s" n
type info = {
info_syn : string Mid.t;
info_rem : Sid.t;
info_syn : syntax_map;
use_trigger : bool;
}
......@@ -175,7 +174,7 @@ let print_logic_binder info fmt v =
fprintf fmt "%a: %a" print_ident v.vs_name (print_type info) v.vs_ty
let print_type_decl info fmt = function
| ts, Tabstract when Sid.mem ts.ts_name info.info_rem -> false
| ts, Tabstract when Mid.mem ts.ts_name info.info_syn -> false
| ts, Tabstract when ts.ts_args = [] ->
fprintf fmt ":extrasorts (%a)" print_ident ts.ts_name; true
| _, Tabstract -> unsupported
......@@ -200,7 +199,7 @@ let print_logic_decl info fmt (ls,ld) = match ld with
"Predicate and function definition aren't supported"
let print_logic_decl info fmt d =
if Sid.mem (fst d).ls_name info.info_rem then
if Mid.mem (fst d).ls_name info.info_syn then
false else (print_logic_decl info fmt d; true)
let print_decl info fmt d = match d.d_node with
......@@ -210,7 +209,7 @@ let print_decl info fmt d = match d.d_node with
print_list_opt newline (print_logic_decl info) fmt dl
| Dind _ -> unsupportedDecl d
"smt : inductive definition are not supported"
| Dprop (Paxiom, pr, _) when Sid.mem pr.pr_name info.info_rem -> false
| Dprop (Paxiom, pr, _) when Mid.mem pr.pr_name info.info_syn -> false
| Dprop (Paxiom, pr, f) ->
fprintf fmt "@[<hov 2>;; %s@\n:assumption@ %a@]@\n"
pr.pr_name.id_string
......@@ -235,7 +234,6 @@ let print_task pr thpr fmt task =
print_th_prelude task fmt thpr;
let info = {
info_syn = get_syntax_map task;
info_rem = get_remove_set task;
use_trigger = false;
}
in
......
......@@ -63,8 +63,7 @@ let print_ident fmt id =
(** type *)
type info = {
info_syn : string Mid.t;
info_rem : Sid.t;
info_syn : syntax_map;
use_trigger : bool;
complex_type : ty Hty.t;
}
......@@ -247,7 +246,7 @@ let print_logic_binder info fmt v =
(print_type info) v.vs_ty
let print_type_decl info fmt = function
| ts, Tabstract when Sid.mem ts.ts_name info.info_rem -> false
| ts, Tabstract when Mid.mem ts.ts_name info.info_syn -> false
| ts, Tabstract when ts.ts_args = [] ->
fprintf fmt "(declare-sort %a 0)" print_ident ts.ts_name; true
| ts, Tabstract when ts.ts_def = None ->
......@@ -276,7 +275,7 @@ let print_logic_decl info fmt (ls,ld) =
List.iter forget_var vsl
let print_logic_decl info fmt d =
if Sid.mem (fst d).ls_name info.info_rem then
if Mid.mem (fst d).ls_name info.info_syn then
false else (print_logic_decl info fmt d; true)
let print_decl info fmt d = match d.d_node with
......@@ -286,7 +285,7 @@ let print_decl info fmt d = match d.d_node with
print_list_opt newline (print_logic_decl info) fmt dl
| Dind _ -> unsupportedDecl d
"smt : inductive definition are not supported"
| Dprop (Paxiom, pr, _) when Sid.mem pr.pr_name info.info_rem -> false
| Dprop (Paxiom, pr, _) when Mid.mem pr.pr_name info.info_syn -> false
| Dprop (Paxiom, pr, f) ->
find_complex_type info fmt f;
fprintf fmt "@[<hov 2>;; %s@\n(assert@ %a)@]@\n"
......@@ -329,7 +328,6 @@ let print_task pr thpr fmt task =
let info = {
info_syn = Mid.union (fun _ _ s -> Some s)
(get_syntax_map task) (Trans.apply distingued task);
info_rem = get_remove_set task;
use_trigger = false;
complex_type = Hty.create 5;
}
......
......@@ -42,8 +42,7 @@ let print_var fmt {vs_name = id} =
let forget_var v = forget_id ident_printer v.vs_name
type info = {
info_syn : string Mid.t;
info_rem : Sid.t;
info_syn : syntax_map;
}
let rec print_term info fmt t = match t.t_node with
......@@ -114,7 +113,7 @@ let print_logic_decl _ _ (_,ld) = match ld with
| Some _ -> unsupported "Predicate and function definition aren't supported"
let print_logic_decl info fmt d =
if Sid.mem (fst d).ls_name info.info_rem then
if Mid.mem (fst d).ls_name info.info_syn then
false else (print_logic_decl info fmt d; true)
let print_decl info fmt d = match d.d_node with
......@@ -124,7 +123,7 @@ let print_decl info fmt d = match d.d_node with
print_list_opt newline (print_logic_decl info) fmt dl
| Dind _ -> unsupportedDecl d
"tptp : inductive definition are not supported"
| Dprop (Paxiom, pr, _) when Sid.mem pr.pr_name info.info_rem -> false
| Dprop (Paxiom, pr, _) when Mid.mem pr.pr_name info.info_syn -> false
| Dprop (Paxiom, pr, f) ->
fprintf fmt "@[<hov 2>fof(%s, axiom,@ %a).@]@\n"
(id_unique ~sanitizer:String.uncapitalize ident_printer pr.pr_name)
......@@ -142,8 +141,7 @@ let print_task pr thpr fmt task =
print_prelude fmt pr;
print_th_prelude task fmt thpr;
let info = {
info_syn = get_syntax_map task;
info_rem = get_remove_set task }
info_syn = get_syntax_map task }
in
ignore (print_list_opt (add_flush newline2)
(print_decl info) fmt (Task.task_decls task))
......
......@@ -85,18 +85,12 @@ let print_pr fmt pr =
(* info *)
type info = {
info_syn : string Mid.t;
info_rem : Sid.t;
}
type info = { info_syn : syntax_map }
let info = ref {
info_syn = Mid.empty;
info_rem = Sid.empty
}
let info = ref { info_syn = Mid.empty }
let query_syntax id = query_syntax !info.info_syn id
let query_remove id = Sid.mem id !info.info_rem
let query_remove id = Mid.mem id !info.info_syn
(** Types *)
......@@ -371,9 +365,7 @@ let print_task _env pr thpr ?old:_ fmt task =
forget_all ();
print_prelude fmt pr;
print_th_prelude task fmt thpr;
info := {
info_syn = get_syntax_map task;
info_rem = get_remove_set task };
info := { info_syn = get_syntax_map task };
fprintf fmt "@[<hov 2>theory Task@\n%a@]@\nend@."
(print_list nothing print_tdecl) (Task.task_tdecls task)
......
......@@ -67,8 +67,7 @@ let print_ident fmt id =
(** type *)
type info = {
info_syn : string Mid.t;
info_rem : Sid.t;
info_syn : syntax_map;
complex_type : ty Hty.t;
}
......@@ -247,7 +246,7 @@ let print_logic_binder info fmt v =
(print_type info) v.vs_ty
let print_type_decl info fmt = function
| ts, Tabstract when Sid.mem ts.ts_name info.info_rem -> false
| ts, Tabstract when Mid.mem ts.ts_name info.info_syn -> false
| ts, Tabstract when ts.ts_args = [] ->
fprintf fmt "(define-type %a)" print_ident ts.ts_name; true
| _, Tabstract -> false
......@@ -273,7 +272,7 @@ let print_logic_decl info fmt (ls,ld) =
end
let print_logic_decl info fmt d =
if Sid.mem (fst d).ls_name info.info_rem then
if Mid.mem (fst d).ls_name info.info_syn then
false else (print_logic_decl info fmt d; true)
let print_decl info fmt d = match d.d_node with
......@@ -283,7 +282,7 @@ let print_decl info fmt d = match d.d_node with
print_list_opt newline (print_logic_decl info) fmt dl
| Dind _ -> unsupportedDecl d
"yices : inductive definition are not supported"
| Dprop (Paxiom, pr, _) when Sid.mem pr.pr_name info.info_rem -> false
| Dprop (Paxiom, pr, _) when Mid.mem pr.pr_name info.info_syn -> false
| Dprop (Paxiom, pr, f) ->
find_complex_type info fmt f;
fprintf fmt "@[<hov 2>;; %s@\n(assert@ %a);@]@\n"
......@@ -325,7 +324,6 @@ let print_task pr thpr fmt task =
let info = {
info_syn = Mid.union (fun _ _ s -> Some s)
(get_syntax_map task) (Trans.apply distingued task);
info_rem = get_remove_set task;
complex_type = Hty.create 5;
}
in
......
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