prototype of a transformation from polymorphic logic to (almost) untyped logic.

It does nothing, but should not disturb the compilation/use of the rest of the system.

Makefile.in

@@ -104,7 +104,8 @@ LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \
 LIB_TRANSFORM = simplify_recursive_definition simplify_formula inlining \
 		split_conjunction encoding_decorate \
 		eliminate_definition eliminate_algebraic \
-		eliminate_inductive eliminate_let eliminate_if
+		eliminate_inductive eliminate_let eliminate_if \
+		polymorphic_to_untyped
 
 LIB_PRINTER = print_real alt_ergo why3 smt coq tptp
 

src/transform/polymorphic_to_untyped.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  Copyright (C) 2010-                                                   *)
+(*    Francois Bobot                                                      *)
+(*    Jean-Christophe Filliatre                                           *)
+(*    Johannes Kanig                                                      *)
+(*    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.                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Util
+open Ident
+open Ty
+open Term
+open Decl
+open Task
+
+
+let eliminate_polymorphism = Register.store (fun () -> Trans.identity)
+
+let polymorphic_to_untyped = Register.store (fun () -> Trans.identity)
+
+let () = Register.register_transform "polymorphic_to_untyped" polymorphic_to_untyped

src/transform/polymorphic_to_untyped.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  Copyright (C) 2010-                                                   *)
+(*    Francois Bobot                                                      *)
+(*    Jean-Christophe Filliatre                                           *)
+(*    Johannes Kanig                                                      *)
+(*    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 eliminate_polymorphism : Task.task Register.trans_reg