trans-based printing in Alt_ergo

src/core/pretty.ml

@@ -30,7 +30,7 @@ open Task
 let debug_print_labels = Debug.register_flag "print_labels"
 let debug_print_locs = Debug.register_flag "print_locs"
 
-let iprinter,tprinter,pprinter =
+let iprinter,aprinter,tprinter,pprinter =
   let bl = ["theory"; "type"; "function"; "predicate"; "inductive";
             "axiom"; "lemma"; "goal"; "use"; "clone"; "prop"; "meta";
             "namespace"; "import"; "export"; "end";
@@ -40,24 +40,21 @@ let iprinter,tprinter,pprinter =
   let lsanitize = sanitizer char_to_lalpha char_to_alnumus in
   create_ident_printer bl ~sanitizer:isanitize,
   create_ident_printer bl ~sanitizer:lsanitize,
+  create_ident_printer bl ~sanitizer:lsanitize,
   create_ident_printer bl ~sanitizer:isanitize
 
+let forget_tvs () =
+  forget_all aprinter
+
 let forget_all () =
   forget_all iprinter;
+  forget_all aprinter;
   forget_all tprinter;
   forget_all pprinter
 
-let tv_set = ref Sid.empty
-
 (* type variables always start with a quote *)
 let print_tv fmt tv =
-  tv_set := Sid.add tv.tv_name !tv_set;
-  let sanitizer n = "'" ^ n in
-  fprintf fmt "%s" (id_unique iprinter ~sanitizer tv.tv_name)
-
-let forget_tvs () =
-  Sid.iter (forget_id iprinter) !tv_set;
-  tv_set := Sid.empty
+  fprintf fmt "'%s" (id_unique aprinter tv.tv_name)
 
 (* logic variables always start with a lower case letter *)
 let print_vs fmt vs =
@@ -417,7 +414,7 @@ let print_meta_arg_type fmt = function
   | MTint      -> fprintf fmt "[integer]"
 
 let print_meta_arg fmt = function
-  | MAty ty -> fprintf fmt "type %a" print_ty ty
+  | MAty ty -> fprintf fmt "type %a" print_ty ty; forget_tvs ()
   | MAts ts -> fprintf fmt "type %a" print_ts ts
   | MAls ls -> fprintf fmt "%s %a" (ls_kind ls) print_ls ls
   | MApr pr -> fprintf fmt "prop %a" print_pr pr

src/printer/alt_ergo.ml

@@ -45,13 +45,17 @@ let ident_printer =
 let print_ident fmt id =
   fprintf fmt "%s" (id_unique ident_printer id)
 
-let print_tvsymbols fmt tv =
-  let sanitize n = "'" ^ n in
-  let n = id_unique ident_printer ~sanitizer:sanitize tv.tv_name in
-  fprintf fmt "%s" n
-
 let forget_var v = forget_id ident_printer v.vs_name
 
+let tv_printer =
+  let san = sanitizer char_to_lalpha char_to_alnumus in
+  create_ident_printer [] ~sanitizer:san
+
+let print_tvsymbol fmt tv =
+  fprintf fmt "'%s" (id_unique tv_printer tv.tv_name)
+
+let forget_tvs () = forget_all tv_printer
+
 type info = {
   info_syn : syntax_map;
   info_ac  : Sls.t;
@@ -59,7 +63,7 @@ type info = {
 
 let rec print_type info fmt ty = match ty.ty_node with
   | Tyvar id ->
-      print_tvsymbols fmt id
+      print_tvsymbol fmt id
   | Tyapp (ts, tl) -> begin match query_syntax info.info_syn ts.ts_name with
       | Some s -> syntax_arguments s (print_type info) fmt tl
       | None -> fprintf fmt "%a%a" (print_tyapp info) tl print_ident ts.ts_name
@@ -166,24 +170,23 @@ 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 fmt ts = match ts.ts_args with
-  | [] -> fprintf fmt "type %a" print_ident ts.ts_name
-  | [tv] -> fprintf fmt "type %a %a" print_tvsymbols tv print_ident ts.ts_name
-  | tl -> fprintf fmt "type (%a) %a"
-      (print_list comma print_tvsymbols) tl print_ident ts.ts_name
+  | [] -> fprintf fmt "type %a@\n@\n"
+      print_ident ts.ts_name
+  | [tv] -> fprintf fmt "type %a %a@\n@\n"
+      print_tvsymbol tv print_ident ts.ts_name
+  | tl -> fprintf fmt "type (%a) %a@\n@\n"
+      (print_list comma print_tvsymbol) tl print_ident ts.ts_name
 
 let print_type_decl info fmt = function
-  | ts, Tabstract when Mid.mem ts.ts_name info.info_syn -> false
-  | ts, Tabstract -> print_type_decl fmt ts; true
+  | ts, Tabstract when Mid.mem ts.ts_name info.info_syn -> ()
+  | ts, Tabstract -> print_type_decl fmt ts; forget_tvs ()
   | _, Talgebraic _ -> unsupported
       "alt-ergo : algebraic datatype are not supported"
 
-let ac_th = ["algebra";"AC"]
-
-let print_logic_decl info fmt (ls,ld) =
-  match ld with
+let print_logic_decl info fmt ls = function
     | None ->
         let sac = if Sls.mem ls info.info_ac then "ac " else "" in
-        fprintf fmt "@[<hov 2>logic %s%a : %a%s%a@]@\n"
+        fprintf fmt "@[<hov 2>logic %s%a : %a%s%a@]@\n@\n"
           sac print_ident ls.ls_name
           (print_list comma (print_type info)) ls.ls_args
           (if ls.ls_args = [] then "" else " -> ")
@@ -193,43 +196,48 @@ let print_logic_decl info fmt (ls,ld) =
         begin match e.t_ty with
           | Some _ ->
               (* TODO AC? *)
-              fprintf fmt "@[<hov 2>function %a(%a) : %a =@ %a@]@\n"
+              fprintf fmt "@[<hov 2>function %a(%a) : %a =@ %a@]@\n@\n"
                 print_ident ls.ls_name
                 (print_list comma (print_logic_binder info)) vl
                 (print_type info) (Util.of_option ls.ls_value)
                 (print_term info) e
           | None ->
-              fprintf fmt "@[<hov 2>predicate %a(%a) =@ %a@]"
+              fprintf fmt "@[<hov 2>predicate %a(%a) =@ %a@]@\n@\n"
                 print_ident ls.ls_name
                 (print_list comma (print_logic_binder info)) vl
                 (print_fmla info) e
         end;
         List.iter forget_var vl
 
-let print_logic_decl info fmt d =
-  if Mid.mem (fst d).ls_name info.info_syn then
-    false else (print_logic_decl info fmt d; true)
+let print_logic_decl info fmt (ls,ld) =
+  if Mid.mem ls.ls_name info.info_syn then () else
+  print_logic_decl info fmt ls ld; forget_tvs ()
+
+let print_prop_decl info fmt k pr f = match k with
+  | Paxiom ->
+      fprintf fmt "@[<hov 2>axiom %a :@ %a@]@\n@\n"
+        print_ident pr.pr_name (print_fmla info) f
+  | Pgoal ->
+      fprintf fmt "@[<hov 2>goal %a :@ %a@]@\n"
+        print_ident pr.pr_name (print_fmla info) f
+  | Plemma| Pskip -> assert false
+
+let print_prop_decl info fmt k pr f =
+  if Mid.mem pr.pr_name info.info_syn then () else
+  print_prop_decl info fmt k pr f; forget_tvs ()
 
 let print_decl info fmt d = match d.d_node with
   | Dtype dl ->
-      print_list_opt newline (print_type_decl info) fmt dl
+      print_list nothing (print_type_decl info) fmt dl
   | Dlogic dl ->
-      print_list_opt newline (print_logic_decl info) fmt dl
+      print_list nothing (print_logic_decl info) fmt dl
   | Dind _ -> unsupportedDecl d
       "alt-ergo : inductive definition are not supported"
-  | 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
-  | Dprop (Pgoal, pr, f) ->
-      fprintf fmt "@[<hov 2>goal %a :@ %a@]@\n"
-        print_ident pr.pr_name (print_fmla info) f; true
-  | Dprop ((Plemma|Pskip), _, _) ->
-      assert false
+  | Dprop (k,pr,f) -> print_prop_decl info fmt k pr f
 
 let print_decl info fmt = catch_unsupportedDecl (print_decl info fmt)
 
-let print_task pr thpr fmt task =
+let print_task_old pr thpr fmt task =
   print_prelude fmt pr;
   print_th_prelude task fmt thpr;
   let info = {
@@ -237,12 +245,31 @@ let print_task pr thpr fmt task =
     info_ac  = Task.on_tagged_ls meta_ac task }
   in
   let decls = Task.task_decls task in
-  ignore (print_list_opt (add_flush newline2) (print_decl info) fmt decls)
+  fprintf fmt "%a@." (print_list nothing (print_decl info)) decls
 
-let () = register_printer "alt-ergo"
+let () = register_printer "alt-ergo-old"
   (fun _env pr thpr ?old:_ fmt task ->
      forget_all ident_printer;
-     print_task pr thpr fmt task)
+     print_task_old pr thpr fmt task)
+
+let print_decls =
+  let print ac sm fmt d =
+    let info = {
+      info_syn = sm;
+      info_ac  = ac } in
+    print_decl info fmt d in
+  Trans.on_tagged_ls meta_ac (fun ac ->
+    Printer.sprint_decls (print ac))
+
+let print_task _env pr thpr ?old:_ fmt task =
+  (* In trans-based p-printing [forget_all] is a no-no *)
+  (* forget_all ident_printer; *)
+  print_prelude fmt pr;
+  print_th_prelude task fmt thpr;
+  fprintf fmt "%a@." (print_list nothing string)
+    (List.rev (Trans.apply print_decls task))
+
+let () = register_printer "alt-ergo" print_task
 
 (*
 let print_goal info fmt (id, f, task) =

src/printer/why3printer.ml

@@ -29,7 +29,7 @@ open Decl
 open Printer
 open Theory
 
-let iprinter,tprinter,pprinter =
+let iprinter,aprinter,tprinter,pprinter =
   let bl = ["theory"; "type"; "function"; "predicate"; "inductive";
             "axiom"; "lemma"; "goal"; "use"; "clone"; "prop"; "meta";
             "namespace"; "import"; "export"; "end";
@@ -39,24 +39,21 @@ let iprinter,tprinter,pprinter =
   let lsanitize = sanitizer char_to_lalpha char_to_alnumus in
   create_ident_printer bl ~sanitizer:isanitize,
   create_ident_printer bl ~sanitizer:lsanitize,
+  create_ident_printer bl ~sanitizer:lsanitize,
   create_ident_printer bl ~sanitizer:isanitize
 
+let forget_tvs () =
+  forget_all aprinter
+
 let forget_all () =
   forget_all iprinter;
+  forget_all aprinter;
   forget_all tprinter;
   forget_all pprinter
 
-let tv_set = ref Sid.empty
-
 (* type variables always start with a quote *)
 let print_tv fmt tv =
-  tv_set := Sid.add tv.tv_name !tv_set;
-  let sanitizer n = "'" ^ n in
-  fprintf fmt "%s" (id_unique iprinter ~sanitizer tv.tv_name)
-
-let forget_tvs () =
-  Sid.iter (forget_id iprinter) !tv_set;
-  tv_set := Sid.empty
+  fprintf fmt "'%s" (id_unique aprinter tv.tv_name)
 
 (* logic variables always start with a lower case letter *)
 let print_vs fmt vs =
@@ -343,7 +340,7 @@ let print_inst_pr fmt (pr1,pr2) =
   fprintf fmt "prop %a = %a" print_pr pr1 print_pr pr2
 
 let print_meta_arg fmt = function
-  | MAty ty -> fprintf fmt "type %a" print_ty ty
+  | MAty ty -> fprintf fmt "type %a" print_ty ty; forget_tvs ()
   | MAts ts -> fprintf fmt "type %a" print_ts ts
   | MAls ls -> fprintf fmt "%s %a" (ls_kind ls) print_ls ls
   | MApr pr -> fprintf fmt "prop %a" print_pr pr