diff --git a/Makefile.in b/Makefile.in index be94723feff09d28d5cf611042d34c1a8be53e99..d51476d8304d382dca4534692ee40e3980c3d494 100644 --- a/Makefile.in +++ b/Makefile.in @@ -133,7 +133,8 @@ LIB_TRANSFORM = simplify_recursive_definition simplify_formula \ introduction abstraction close_epsilon lift_epsilon \ eval_match -LIB_PRINTER = print_real alt_ergo why3 smt smt2 coq tptp simplify gappa cvc3 +LIB_PRINTER = print_real alt_ergo why3printer smtv1 smtv2 \ + coq tptp simplify gappa cvc3 LIBMODULES = src/config \ $(addprefix src/util/, $(LIB_UTIL)) \ diff --git a/src/main.ml b/src/main.ml index 27bf96914f3b23d8720fe9de75966521b52f789a..ee6d71db3d4b80d6c4c8fb2e184cb22b4eabb373 100644 --- a/src/main.ml +++ b/src/main.ml @@ -498,7 +498,7 @@ let do_coq_realize_theory env _drv oldf fname m (tname,_,t,_glist) = in let ch = open_out oldf in let fmt = formatter_of_out_channel ch in - Coq.print_theory ~old env [] Ident.Mid.empty fmt th + Coq.print_theory ?old env [] Ident.Mid.empty fmt th let do_input env drv = function | None, _ when !opt_parse_only || !opt_type_only -> diff --git a/src/printer/coq.ml b/src/printer/coq.ml index 70bf85e512408c8c28555ae04b0b7faba2593d7a..dc0b416e2ca125d2369b3ee0b75c9ca8d50008af 100644 --- a/src/printer/coq.ml +++ b/src/printer/coq.ml @@ -547,7 +547,7 @@ let print_tdecl ~old info fmt d = match d.td_node with let print_tdecls ~old info fmt dl = fprintf fmt "@[%a@\n@]" (print_list nothing (print_tdecl ~old info)) dl -let print_theory _env pr thpr ~old fmt th = +let print_theory _env pr thpr ?old fmt th = forget_all (); print_prelude fmt pr; print_prelude_for_theory th fmt thpr; diff --git a/src/printer/coq.mli b/src/printer/coq.mli new file mode 100644 index 0000000000000000000000000000000000000000..886bdd3e1903e4f40162a51bdf99174545deee5d --- /dev/null +++ b/src/printer/coq.mli @@ -0,0 +1,21 @@ +(**************************************************************************) +(* *) +(* Copyright (C) 2010-2011 *) +(* François Bobot *) +(* Jean-Christophe Filliâtre *) +(* Claude Marché *) +(* Andrei Paskevich *) +(* *) +(* This software is free software; you can redistribute it and/or *) +(* modify it under the terms of the GNU Library General Public *) +(* License version 2.1, with the special exception on linking *) +(* described in file LICENSE. *) +(* *) +(* This software is distributed in the hope that it will be useful, *) +(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) +(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *) +(* *) +(**************************************************************************) + +val print_theory : Env.env -> Printer.prelude -> Printer.prelude_map -> + ?old:Pervasives.in_channel -> Format.formatter -> Theory.theory -> unit diff --git a/src/printer/smt.mli b/src/printer/cvc3.mli similarity index 100% rename from src/printer/smt.mli rename to src/printer/cvc3.mli diff --git a/src/printer/gappa.mli b/src/printer/gappa.mli new file mode 100644 index 0000000000000000000000000000000000000000..e866134fc6daaecb43a262b5fae68628a1b192c8 --- /dev/null +++ b/src/printer/gappa.mli @@ -0,0 +1,20 @@ +(**************************************************************************) +(* *) +(* Copyright (C) 2010-2011 *) +(* François Bobot *) +(* Jean-Christophe Filliâtre *) +(* Claude Marché *) +(* Guillaume Melquiond *) +(* Andrei Paskevich *) +(* *) +(* This software is free software; you can redistribute it and/or *) +(* modify it under the terms of the GNU Library General Public *) +(* License version 2.1, with the special exception on linking *) +(* described in file LICENSE. *) +(* *) +(* This software is distributed in the hope that it will be useful, *) +(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) +(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *) +(* *) +(**************************************************************************) + diff --git a/src/printer/why3.mli b/src/printer/simplify.mli similarity index 100% rename from src/printer/why3.mli rename to src/printer/simplify.mli diff --git a/src/printer/smt.ml b/src/printer/smtv1.ml similarity index 100% rename from src/printer/smt.ml rename to src/printer/smtv1.ml diff --git a/src/printer/smtv1.mli b/src/printer/smtv1.mli new file mode 100644 index 0000000000000000000000000000000000000000..41b75d87e67000c65ac71c9c05c5f44d3188db44 --- /dev/null +++ b/src/printer/smtv1.mli @@ -0,0 +1,19 @@ +(**************************************************************************) +(* *) +(* Copyright (C) 2010-2011 *) +(* François Bobot *) +(* Jean-Christophe Filliâtre *) +(* Claude Marché *) +(* Andrei Paskevich *) +(* *) +(* This software is free software; you can redistribute it and/or *) +(* modify it under the terms of the GNU Library General Public *) +(* License version 2.1, with the special exception on linking *) +(* described in file LICENSE. *) +(* *) +(* This software is distributed in the hope that it will be useful, *) +(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) +(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *) +(* *) +(**************************************************************************) + diff --git a/src/printer/smt2.ml b/src/printer/smtv2.ml similarity index 100% rename from src/printer/smt2.ml rename to src/printer/smtv2.ml diff --git a/src/printer/smtv2.mli b/src/printer/smtv2.mli new file mode 100644 index 0000000000000000000000000000000000000000..41b75d87e67000c65ac71c9c05c5f44d3188db44 --- /dev/null +++ b/src/printer/smtv2.mli @@ -0,0 +1,19 @@ +(**************************************************************************) +(* *) +(* Copyright (C) 2010-2011 *) +(* François Bobot *) +(* Jean-Christophe Filliâtre *) +(* Claude Marché *) +(* Andrei Paskevich *) +(* *) +(* This software is free software; you can redistribute it and/or *) +(* modify it under the terms of the GNU Library General Public *) +(* License version 2.1, with the special exception on linking *) +(* described in file LICENSE. *) +(* *) +(* This software is distributed in the hope that it will be useful, *) +(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) +(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *) +(* *) +(**************************************************************************) + diff --git a/src/printer/why3.ml b/src/printer/why3printer.ml similarity index 100% rename from src/printer/why3.ml rename to src/printer/why3printer.ml diff --git a/src/printer/why3printer.mli b/src/printer/why3printer.mli new file mode 100644 index 0000000000000000000000000000000000000000..41b75d87e67000c65ac71c9c05c5f44d3188db44 --- /dev/null +++ b/src/printer/why3printer.mli @@ -0,0 +1,19 @@ +(**************************************************************************) +(* *) +(* Copyright (C) 2010-2011 *) +(* François Bobot *) +(* Jean-Christophe Filliâtre *) +(* Claude Marché *) +(* Andrei Paskevich *) +(* *) +(* This software is free software; you can redistribute it and/or *) +(* modify it under the terms of the GNU Library General Public *) +(* License version 2.1, with the special exception on linking *) +(* described in file LICENSE. *) +(* *) +(* This software is distributed in the hope that it will be useful, *) +(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) +(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *) +(* *) +(**************************************************************************) +