New transformation eliminate_definition_if_poly, seems to work so far

Makefile.in

@@ -147,6 +147,7 @@ LIB_MLW = ity expr dexpr
 LIB_PARSER = ptree glob parser typing lexer
 
 LIB_TRANSFORM = simplify_formula inlining split_goal induction \
+		detect_polymorphism \
 		eliminate_definition eliminate_algebraic \
 		eliminate_inductive eliminate_let eliminate_if \
 		libencoding discriminate encoding encoding_select \
@@ -156,8 +157,7 @@ LIB_TRANSFORM = simplify_formula inlining split_goal induction \
 		introduction abstraction close_epsilon lift_epsilon \
 		eliminate_epsilon \
 		eval_match instantiate_predicate smoke_detector \
-		reduction_engine compute induction_pr prop_curry \
-		detect_polymorphism
+		reduction_engine compute induction_pr prop_curry
 
 LIB_PRINTER = alt_ergo why3printer smtv1 smtv2 coq pvs isabelle \
 	      simplify gappa cvc3 yices mathematica

src/transform/detect_polymorphism.ml

@@ -79,9 +79,12 @@ let find_in_decl d =
 
 (**)
 
-let rec find_in_theory th = List.iter find_in_tdecl th.th_decls
+let (*
+rec find_in_theory th = List.iter find_in_tdecl th.th_decls
 
-and find_in_tdecl td =
+and
+    *)
+find_in_tdecl td =
   match td.td_node with
   | Decl d -> find_in_decl d
   | Use _th ->

src/transform/detect_polymorphism.mli

+
+val meta_monomorphic_types_only : Theory.meta

src/transform/eliminate_algebraic.ml

@@ -431,7 +431,7 @@ let meta_elim = register_meta "eliminate_algebraic" [MTstring]
     \"keep_types\" : @[keep algebraic type definitions@]@\n\
     \"keep_enums\" : @[keep monomorphic enumeration types@]@\n\
     \"keep_recs\"  : @[keep non-recursive records@]@\n\
-    \"no_index\"   : @[do not generate indexing funcitons@]@]"
+    \"no_index\"   : @[do not generate indexing functions@]@]"
 
 let eliminate_algebraic = Trans.compose compile_match
   (Trans.on_meta meta_elim (fun ml ->

src/transform/eliminate_definition.ml

@@ -173,6 +173,19 @@ let () =
     ~desc:"Same@ as@ eliminate_recursion,@ but@ only@ for@ mutually@ \
            recursive@ definitions."
 
+(** conditional transformations, only applied when polymorphic types occur *)
+
+let eliminate_definition_if_poly =
+  Trans.on_meta Detect_polymorphism.meta_monomorphic_types_only
+    (function
+    | [] -> eliminate_definition
+    | _ -> Trans.identity)
+
+let () =
+  Trans.register_transform "eliminate_definition_if_poly"
+    eliminate_definition_if_poly
+    ~desc:"Same@ as@ eliminate_definition@ but@ only@ if@ polymorphism@ appear.";
+
 (** Bisect *)
 open Task
 open Theory

tests/test-poly.why

@@ -31,6 +31,16 @@ goal g : match Cons 42 Nil with Nil -> false | Cons x _ -> x=42 end
 end
 
 
+theory MonoSymb
+
+function id (x:int) : int = x
+
+goal g: forall x:int. id x = x
+
+(* bin/why3prove.byte tests/test-poly.why --debug detect_poly -a detect_polymorphism -D why3 -T PolySymb -G g *)
+
+end
+
 theory PolySymb
 
 function id (x:'a) : 'a = x