Commit 8b2890b7 authored by Simon Cruanes's avatar Simon Cruanes

prototype for explicit_polymorphism transformation

parent e601a71d
......@@ -105,7 +105,7 @@ LIB_TRANSFORM = simplify_recursive_definition simplify_formula inlining \
split_conjunction encoding_decorate \
eliminate_definition eliminate_algebraic \
eliminate_inductive eliminate_let eliminate_if \
polymorphic_to_untyped
explicit_polymorphism
LIB_PRINTER = print_real alt_ergo why3 smt coq tptp
......
......@@ -25,7 +25,7 @@ transformation "eliminate_algebraic"
transformation "eliminate_if"
transformation "eliminate_let"
transformation "polymorphic_to_untyped"
transformation "explicit_polymorphism"
(* TODO : transformation to eliminate types *)
......
......@@ -24,7 +24,19 @@ open Term
open Decl
open Task
(* TODO : preserve some types (builtin types) ? *)
let polymorphic_to_untyped = Register.store (fun () -> Trans.identity)
let () = Register.register_transform "polymorphic_to_untyped" polymorphic_to_untyped
let decl_transform tbl d = match d.d_node with
| Dtype tys -> failwith "Dtype : not implemented"
| Dind inds -> failwith "Dind : should not be here !"
| Dlogic decls -> failwith "not implemented"
| Dprop prop -> failwith "not implemented"
(** the transformation to be registered. *)
let explicit_polymorphism = Register.store
(fun () -> Trans.decl (decl_transform (Hashtbl.create 42)) None)
let () = Register.register_transform "explicit_polymorphism" explicit_polymorphism
......@@ -17,4 +17,7 @@
(* *)
(**************************************************************************)
val polymorphic_to_untyped : Task.task Register.trans_reg
(** transformation from polymorphic logic to untyped logic. The polymorphic
logic must not have finite support types. *)
val explicit_polymorphism : Task.task Register.trans_reg
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