Commit 96c294fe authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

Alt-ergo: switch to direct printing with a fresh ident_printer per task

parent a8911534
...@@ -39,9 +39,10 @@ type info = { ...@@ -39,9 +39,10 @@ type info = {
info_pjs : Sls.t; info_pjs : Sls.t;
info_axs : Spr.t; info_axs : Spr.t;
info_inv_trig : Sls.t; info_inv_trig : Sls.t;
info_printer : ident_printer;
} }
let ident_printer = let ident_printer () =
let bls = [ let bls = [
"ac"; "and"; "array"; "as"; "axiom"; "bitv"; "bool"; "ac"; "and"; "array"; "as"; "axiom"; "bitv"; "bool";
"check"; "cut"; "distinct"; "else"; "exists"; "check"; "cut"; "distinct"; "else"; "exists";
...@@ -55,8 +56,8 @@ let ident_printer = ...@@ -55,8 +56,8 @@ let ident_printer =
let san = sanitizer char_to_alpha char_to_alnumus in let san = sanitizer char_to_alpha char_to_alnumus in
create_ident_printer bls ~sanitizer:san create_ident_printer bls ~sanitizer:san
let print_ident fmt id = let print_ident info fmt id =
fprintf fmt "%s" (id_unique ident_printer id) fprintf fmt "%s" (id_unique info.info_printer id)
let print_label fmt l = let print_label fmt l =
fprintf fmt "\"%s\"" l.lab_string fprintf fmt "\"%s\"" l.lab_string
...@@ -64,12 +65,12 @@ let print_label fmt l = ...@@ -64,12 +65,12 @@ let print_label fmt l =
let print_ident_label info fmt id = let print_ident_label info fmt id =
if info.info_show_labels then if info.info_show_labels then
fprintf fmt "%s %a" fprintf fmt "%s %a"
(id_unique ident_printer id) (id_unique info.info_printer id)
(print_list space print_label) (Slab.elements id.id_label) (print_list space print_label) (Slab.elements id.id_label)
else else
print_ident fmt id print_ident info fmt id
let forget_var v = forget_id ident_printer v.vs_name let forget_var info v = forget_id info.info_printer v.vs_name
(* (*
let tv_printer = let tv_printer =
...@@ -85,19 +86,20 @@ let forget_tvs () = forget_all tv_printer ...@@ -85,19 +86,20 @@ let forget_tvs () = forget_all tv_printer
(* work around a "duplicate type variable" bug of Alt-Ergo 0.94 *) (* work around a "duplicate type variable" bug of Alt-Ergo 0.94 *)
let print_tvsymbol, forget_tvs = let print_tvsymbol, forget_tvs =
let htv = Hid.create 5 in let htv = Hid.create 5 in
(fun fmt tv -> (fun info fmt tv ->
Hid.replace htv tv.tv_name (); Hid.replace htv tv.tv_name ();
fprintf fmt "'%s" (id_unique ident_printer tv.tv_name)), fprintf fmt "'%s" (id_unique info.info_printer tv.tv_name)),
(fun () -> (fun info ->
Hid.iter (fun id _ -> forget_id ident_printer id) htv; Hid.iter (fun id _ -> forget_id info.info_printer id) htv;
Hid.clear htv) Hid.clear htv)
let rec print_type info fmt ty = match ty.ty_node with let rec print_type info fmt ty = match ty.ty_node with
| Tyvar id -> | Tyvar id ->
print_tvsymbol fmt id print_tvsymbol info fmt id
| Tyapp (ts, tl) -> begin match query_syntax info.info_syn ts.ts_name with | Tyapp (ts, tl) -> begin match query_syntax info.info_syn ts.ts_name with
| Some s -> syntax_arguments s (print_type info) fmt tl | Some s -> syntax_arguments s (print_type info) fmt tl
| None -> fprintf fmt "%a%a" (print_tyapp info) tl print_ident ts.ts_name | None -> fprintf fmt "%a%a" (print_tyapp info) tl
(print_ident info) ts.ts_name
end end
and print_tyapp info fmt = function and print_tyapp info fmt = function
...@@ -135,21 +137,21 @@ let rec print_term info fmt t = match t.t_node with ...@@ -135,21 +137,21 @@ let rec print_term info fmt t = match t.t_node with
} in } in
Number.print number_format fmt c Number.print number_format fmt c
| Tvar { vs_name = id } -> | Tvar { vs_name = id } ->
print_ident fmt id print_ident info fmt id
| Tapp (ls, tl) -> begin match query_syntax info.info_syn ls.ls_name with | Tapp (ls, tl) -> begin match query_syntax info.info_syn ls.ls_name with
| Some s -> syntax_arguments s (print_term info) fmt tl | Some s -> syntax_arguments s (print_term info) fmt tl
| None when Mls.mem ls info.info_csm -> | None when Mls.mem ls info.info_csm ->
let print_field fmt ({ls_name = id},t) = let print_field fmt ({ls_name = id},t) =
fprintf fmt "%a =@ %a" print_ident id (print_term info) t in fprintf fmt "%a =@ %a" (print_ident info) id (print_term info) t in
fprintf fmt "{@ %a@ }" (print_list semi print_field) fprintf fmt "{@ %a@ }" (print_list semi print_field)
(List.combine (Mls.find ls info.info_csm) tl) (List.combine (Mls.find ls info.info_csm) tl)
| None when Sls.mem ls info.info_pjs -> | None when Sls.mem ls info.info_pjs ->
fprintf fmt "%a.%a" (print_tapp info) tl print_ident ls.ls_name fprintf fmt "%a.%a" (print_tapp info) tl (print_ident info) ls.ls_name
| None when unambig_fs ls || not info.info_type_casts -> | None when unambig_fs ls || not info.info_type_casts ->
fprintf fmt "%a%a" print_ident ls.ls_name (print_tapp info) tl fprintf fmt "%a%a" (print_ident info) ls.ls_name (print_tapp info) tl
| None -> | None ->
fprintf fmt "(%a%a : %a)" print_ident ls.ls_name (print_tapp info) tl fprintf fmt "(%a%a : %a)" (print_ident info) ls.ls_name
(print_type info) (t_type t) (print_tapp info) tl (print_type info) (t_type t)
end end
| Tlet _ -> unsupportedTerm t | Tlet _ -> unsupportedTerm t
"alt-ergo : you must eliminate let in term" "alt-ergo : you must eliminate let in term"
...@@ -178,10 +180,10 @@ let rec print_fmla info fmt f = ...@@ -178,10 +180,10 @@ let rec print_fmla info fmt f =
and print_fmla_node info fmt f = match f.t_node with and print_fmla_node info fmt f = match f.t_node with
| Tapp ({ ls_name = id }, []) -> | Tapp ({ ls_name = id }, []) ->
print_ident fmt id print_ident info fmt id
| Tapp (ls, tl) -> begin match query_syntax info.info_syn ls.ls_name with | Tapp (ls, tl) -> begin match query_syntax info.info_syn ls.ls_name with
| Some s -> syntax_arguments s (print_term info) fmt tl | Some s -> syntax_arguments s (print_term info) fmt tl
| None -> fprintf fmt "%a(%a)" print_ident ls.ls_name | None -> fprintf fmt "%a(%a)" (print_ident info) ls.ls_name
(print_list comma (print_term info)) tl (print_list comma (print_term info)) tl
end end
| Tquant (q, fq) -> | Tquant (q, fq) ->
...@@ -196,7 +198,7 @@ and print_fmla_node info fmt f = match f.t_node with ...@@ -196,7 +198,7 @@ and print_fmla_node info fmt f = match f.t_node with
in in
fprintf fmt "@[(%a%a.@ %a)@]" (print_list dot forall) vl fprintf fmt "@[(%a%a.@ %a)@]" (print_list dot forall) vl
(print_triggers info) tl (print_fmla info) f; (print_triggers info) tl (print_fmla info) f;
List.iter forget_var vl List.iter (forget_var info) vl
| Tbinop (Tand, f1, f2) -> | Tbinop (Tand, f1, f2) ->
fprintf fmt "(%a and@ %a)" (print_fmla info) f1 (print_fmla info) f2 fprintf fmt "(%a and@ %a)" (print_fmla info) f1 (print_fmla info) f2
| Tbinop (Tor, f1, f2) -> | Tbinop (Tor, f1, f2) ->
...@@ -235,37 +237,37 @@ and print_triggers info fmt tl = ...@@ -235,37 +237,37 @@ and print_triggers info fmt tl =
(print_list alt (print_list comma (print_expr info))) tl (print_list alt (print_list comma (print_expr info))) tl
let print_logic_binder info fmt v = let print_logic_binder info fmt v =
fprintf fmt "%a: %a" print_ident v.vs_name (print_type info) v.vs_ty fprintf fmt "%a: %a" (print_ident info) v.vs_name (print_type info) v.vs_ty
let print_type_decl fmt ts = match ts.ts_args with let print_type_decl info fmt ts = match ts.ts_args with
| [] -> fprintf fmt "type %a" | [] -> fprintf fmt "type %a"
print_ident ts.ts_name (print_ident info) ts.ts_name
| [tv] -> fprintf fmt "type %a %a" | [tv] -> fprintf fmt "type %a %a"
print_tvsymbol tv print_ident ts.ts_name (print_tvsymbol info) tv (print_ident info) ts.ts_name
| tl -> fprintf fmt "type (%a) %a" | tl -> fprintf fmt "type (%a) %a"
(print_list comma print_tvsymbol) tl print_ident ts.ts_name (print_list comma (print_tvsymbol info)) tl (print_ident info) ts.ts_name
let print_enum_decl fmt ts csl = let print_enum_decl info fmt ts csl =
let print_cs fmt (ls,_) = print_ident fmt ls.ls_name in let print_cs fmt (ls,_) = print_ident info fmt ls.ls_name in
fprintf fmt "@[<hov 2>type %a =@ %a@]@\n@\n" print_ident ts.ts_name fprintf fmt "@[<hov 2>type %a =@ %a@]@\n@\n" (print_ident info) ts.ts_name
(print_list alt2 print_cs) csl (print_list alt2 print_cs) csl
let print_ty_decl info fmt ts = let print_ty_decl info fmt ts =
if ts.ts_def <> None then () else if ts.ts_def <> None then () else
if Mid.mem ts.ts_name info.info_syn then () else if Mid.mem ts.ts_name info.info_syn then () else
(fprintf fmt "%a@\n@\n" print_type_decl ts; forget_tvs ()) (fprintf fmt "%a@\n@\n" (print_type_decl info) ts; forget_tvs info)
let print_data_decl info fmt = function let print_data_decl info fmt = function
| ts, csl (* monomorphic enumeration *) | ts, csl (* monomorphic enumeration *)
when ts.ts_args = [] && List.for_all (fun (_,l) -> l = []) csl -> when ts.ts_args = [] && List.for_all (fun (_,l) -> l = []) csl ->
print_enum_decl fmt ts csl print_enum_decl info fmt ts csl
| ts, [cs,_] (* non-recursive records *) | ts, [cs,_] (* non-recursive records *)
when Mls.mem cs info.info_csm -> when Mls.mem cs info.info_csm ->
let pjl = Mls.find cs info.info_csm in let pjl = Mls.find cs info.info_csm in
let print_field fmt ls = let print_field fmt ls =
fprintf fmt "%a@ :@ %a" print_ident ls.ls_name fprintf fmt "%a@ :@ %a" (print_ident info) ls.ls_name
(print_type info) (Opt.get ls.ls_value) in (print_type info) (Opt.get ls.ls_value) in
fprintf fmt "%a@ =@ {@ %a@ }@\n@\n" print_type_decl ts fprintf fmt "%a@ =@ {@ %a@ }@\n@\n" (print_type_decl info) ts
(print_list semi print_field) pjl (print_list semi print_field) pjl
| _, _ -> unsupported | _, _ -> unsupported
"alt-ergo : algebraic datatype are not supported" "alt-ergo : algebraic datatype are not supported"
...@@ -277,14 +279,14 @@ let print_data_decl info fmt ((ts, _csl) as p) = ...@@ -277,14 +279,14 @@ let print_data_decl info fmt ((ts, _csl) as p) =
let print_param_decl info fmt ls = let print_param_decl info fmt ls =
let sac = if Sls.mem ls 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@\n" fprintf fmt "@[<hov 2>logic %s%a : %a%s%a@]@\n@\n"
sac print_ident ls.ls_name sac (print_ident info) ls.ls_name
(print_list comma (print_type info)) ls.ls_args (print_list comma (print_type info)) ls.ls_args
(if ls.ls_args = [] then "" else " -> ") (if ls.ls_args = [] then "" else " -> ")
(print_option_or_default "prop" (print_type info)) ls.ls_value (print_option_or_default "prop" (print_type info)) ls.ls_value
let print_param_decl info fmt ls = let print_param_decl info fmt ls =
if Mid.mem ls.ls_name info.info_syn || Sls.mem ls info.info_pjs if Mid.mem ls.ls_name info.info_syn || Sls.mem ls info.info_pjs
then () else (print_param_decl info fmt ls; forget_tvs ()) then () else (print_param_decl info fmt ls; forget_tvs info)
let print_logic_decl info fmt ls ld = let print_logic_decl info fmt ls ld =
let vl,e = open_ls_defn ld in let vl,e = open_ls_defn ld in
...@@ -292,34 +294,34 @@ let print_logic_decl info fmt ls ld = ...@@ -292,34 +294,34 @@ let print_logic_decl info fmt ls ld =
| Some _ -> | Some _ ->
(* TODO AC? *) (* TODO AC? *)
fprintf fmt "@[<hov 2>function %a(%a) : %a =@ %a@]@\n@\n" fprintf fmt "@[<hov 2>function %a(%a) : %a =@ %a@]@\n@\n"
print_ident ls.ls_name (print_ident info) ls.ls_name
(print_list comma (print_logic_binder info)) vl (print_list comma (print_logic_binder info)) vl
(print_type info) (Opt.get ls.ls_value) (print_type info) (Opt.get ls.ls_value)
(print_term info) e (print_term info) e
| None -> | None ->
fprintf fmt "@[<hov 2>predicate %a(%a) =@ %a@]@\n@\n" fprintf fmt "@[<hov 2>predicate %a(%a) =@ %a@]@\n@\n"
print_ident ls.ls_name (print_ident info) ls.ls_name
(print_list comma (print_logic_binder info)) vl (print_list comma (print_logic_binder info)) vl
(print_fmla info) e (print_fmla info) e
end; end;
List.iter forget_var vl List.iter (forget_var info) vl
let print_logic_decl info fmt (ls,ld) = let print_logic_decl info fmt (ls,ld) =
if Mid.mem ls.ls_name info.info_syn || Sls.mem ls info.info_pjs if Mid.mem ls.ls_name info.info_syn || Sls.mem ls info.info_pjs
then () else (print_logic_decl info fmt ls ld; forget_tvs ()) then () else (print_logic_decl info fmt ls ld; forget_tvs info)
let print_prop_decl info fmt k pr f = match k with let print_prop_decl info fmt k pr f = match k with
| Paxiom -> | Paxiom ->
fprintf fmt "@[<hov 2>axiom %a :@ %a@]@\n@\n" fprintf fmt "@[<hov 2>axiom %a :@ %a@]@\n@\n"
print_ident pr.pr_name (print_fmla info) f (print_ident info) pr.pr_name (print_fmla info) f
| Pgoal -> | Pgoal ->
fprintf fmt "@[<hov 2>goal %a :@ %a@]@\n" fprintf fmt "@[<hov 2>goal %a :@ %a@]@\n"
print_ident pr.pr_name (print_fmla info) f (print_ident info) pr.pr_name (print_fmla info) f
| Plemma| Pskip -> assert false | Plemma| Pskip -> assert false
let print_prop_decl info fmt k pr f = let print_prop_decl info fmt k pr f =
if Mid.mem pr.pr_name info.info_syn || Spr.mem pr info.info_axs if Mid.mem pr.pr_name info.info_syn || Spr.mem pr info.info_axs
then () else (print_prop_decl info fmt k pr f; forget_tvs ()) then () else (print_prop_decl info fmt k pr f; forget_tvs info)
let print_decl info fmt d = match d.d_node with let print_decl info fmt d = match d.d_node with
| Dtype ts -> | Dtype ts ->
...@@ -342,50 +344,40 @@ let add_projection (csm,pjs,axs) = function ...@@ -342,50 +344,40 @@ let add_projection (csm,pjs,axs) = function
csm, Sls.add ls pjs, Spr.add pr axs csm, Sls.add ls pjs, Spr.add pr axs
| _ -> assert false | _ -> assert false
let check_showlabels acc = function let check_options ((show,cast) as acc) = function
| [Theory.MAstr "show_labels"] -> true | [Theory.MAstr "show_labels"] -> true, cast
| [Theory.MAstr "no_type_cast"] -> show, false
| [Theory.MAstr _] -> acc | [Theory.MAstr _] -> acc
| _ -> assert false | _ -> assert false
let check_typecasts acc = function let print_task args ?old:_ fmt task =
| [Theory.MAstr "no_type_cast"] -> false print_prelude fmt args.prelude;
| [Theory.MAstr _] -> acc print_th_prelude task fmt args.th_prelude;
| _ -> assert false let csm,pjs,axs = Task.on_meta Eliminate_algebraic.meta_proj
add_projection (Mls.empty,Sls.empty,Spr.empty) task in
let print_decls = let inv_trig = Task.on_tagged_ls meta_invalid_trigger task in
let print_decl info fmt d = let show,cast = Task.on_meta meta_printer_option
try print_decl info fmt d; info, [] check_options (false,true) task in
with Unsupported s -> raise (UnsupportedDecl (d,s)) in
let print_decl = Printer.sprint_decl print_decl in
let print_decl task acc = print_decl task.Task.task_decl acc in
Discriminate.on_syntax_map (fun sm ->
Trans.on_tagged_ls meta_ac (fun ac ->
Trans.on_meta meta_printer_option (fun args ->
Trans.on_meta Eliminate_algebraic.meta_proj (fun mal ->
Trans.on_tagged_ls meta_invalid_trigger (fun inv_trig ->
let csm,pjs,axs =
List.fold_left add_projection (Mls.empty,Sls.empty,Spr.empty) mal in
let info = { let info = {
info_syn = sm; info_syn = Discriminate.get_syntax_map task;
info_ac = ac; info_ac = Task.on_tagged_ls meta_ac task;
info_show_labels = List.fold_left check_showlabels false args; info_show_labels = show;
info_type_casts = List.fold_left check_typecasts true args; info_type_casts = cast;
info_csm = Mls.map Array.to_list csm; info_csm = Mls.map Array.to_list csm;
info_pjs = pjs; info_pjs = pjs;
info_axs = axs; info_axs = axs;
info_inv_trig = Sls.add ps_equ inv_trig; info_inv_trig = Sls.add ps_equ inv_trig;
} in info_printer = ident_printer () } in
Trans.fold print_decl (info,[])))))) let rec print_decls = function
| Some t ->
let print_task args ?old:_ fmt task = print_decls t.Task.task_prev;
(* In trans-based p-printing [forget_all] is a no-no *) begin match t.Task.task_decl.Theory.td_node with
(* forget_all ident_printer; *) | Theory.Decl d ->
print_prelude fmt args.prelude; begin try print_decl info fmt d
print_th_prelude task fmt args.th_prelude; with Unsupported s -> raise (UnsupportedDecl (d,s)) end
let rec print = function | _ -> () end
| x :: r -> print r; Pp.string fmt x | None -> () in
| [] -> () in print_decls task;
print (snd (Trans.apply print_decls task));
pp_print_flush fmt () pp_print_flush fmt ()
let () = register_printer "alt-ergo" print_task let () = register_printer "alt-ergo" print_task
......
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