Merge branch 'claude'

Conflicts:
	drivers/smt-libv2.drv

Makefile.in

@@ -152,6 +152,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 \

drivers/cvc4.drv

-import "cvc4_bare.drv"
+(** Why3 driver for CVC4 <= 1.3 *)
+
+prelude "(set-logic AUFNIRA)"
+(*
+    A  : Array
+    UF : Uninterpreted Function
+    NIRA : NonLinear Integer Reals Arithmetic
+*)
+
+import "smt-libv2.drv"
 import "discrimination.gen"
+
+transformation "inline_trivial"
+transformation "eliminate_builtin"
+transformation "eliminate_definition"
+transformation "eliminate_inductive"
+transformation "eliminate_algebraic"
+transformation "eliminate_epsilon"
+
+transformation "simplify_formula"
+(*transformation "simplify_trivial_quantification"*)
+
+transformation "discriminate"
+transformation "encoding_smt"
+
+(** Error messages specific to CVC4 *)
+
+outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
+timeout "interrupted by timeout"
+steps "smt::SmtEngine::resourceUnitsUsed, \\([0-9]+.?[0-9]*\\)" 1
+
+
+(** Extra theories supported by CVC4 *)
+
+(* Disabled:
+   CVC4 division seems to be neither the Euclidean one, nor the Computer one
+
+theory int.EuclideanDivision
+   syntax function div "(div %1 %2)"
+   syntax function mod "(mod %1 %2)"
+   remove prop Mod_bound
+   remove prop Div_mod
+   remove prop Mod_1
+   remove prop Div_1
+end
+
+theory int.ComputerDivision
+   syntax function div "(div %1 %2)"
+   syntax function mod "(mod %1 %2)"
+   remove prop Mod_bound
+   remove prop Div_mod
+   remove prop Mod_1
+   remove prop Div_1
+end
+*)

drivers/cvc4_bare.drv → drivers/cvc4_14.drv

-prelude "(set-logic AUFBVNIRA)"
-(** A  : Array
+(** Why3 driver for CVC4 >= 1.4 *)
+
+prelude "(set-logic AUFBVDTNIRA)"
+(*
+    A  : Array
     UF : Uninterpreted Function
-    DT : Datatypes (not needed at the end ...)
+    BV : BitVectors
+    DT : Datatypes
     NIRA : NonLinear Integer Reals Arithmetic
 *)
-(* prelude "(set-logic ALL_SUPPORTED)" *)
+(* prelude "(set-logic ALL_SUPPORTED)"
+   does not seem to include DT
+*)
 
 import "smt-libv2.drv"
+import "discrimination.gen"
+
+transformation "inline_trivial"
+transformation "eliminate_builtin"
+(* temporarily disabled: too much experimental
+transformation "detect_polymorphism"
+*)
+transformation "eliminate_definition_if_poly"
+transformation "eliminate_inductive"
+transformation "eliminate_algebraic_if_poly"
+transformation "eliminate_epsilon"
 
-(* regexp for steps *)
-steps "smt::SmtEngine::resourceUnitsUsed, \\([0-9]+.?[0-9]*\\)" 1
+transformation "simplify_formula"
+(*transformation "simplify_trivial_quantification"*)
 
+transformation "discriminate_if_poly"
+transformation "encoding_smt_if_poly"
+
+(** Error messages specific to CVC4 *)
+
+outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
+timeout "interrupted by timeout"
+
+(* regexp for steps should match things like
+
+smt::SmtEngine::resourceUnitsUsed, 1041
+
+but not in the same line as the "valid" answer
+
+*)
+
+(** Extra theories supported by CVC4 *)
+
+(* Disabled:
+   CVC4 division seems to be neither the Euclidean one, nor the Computer one
 
-(* CVC4 division seems to be neither the Euclidean one, nor the Computer one *)
-(*
 theory int.EuclideanDivision
    syntax function div "(div %1 %2)"
    syntax function mod "(mod %1 %2)"

drivers/smt-libv2.drv

-(* Why driver for SMTLIB2 syntax *)
+(* Why3 driver for SMT-LIB2 syntax, excluding bit-vectors *)
 
-prelude ";;; this is a prelude for smt-lib v2"
+prelude ";;; generated by SMT-LIB2 driver"
+
+(*
+
+Note: we do not insert any command "set-logic" because its
+interpretation is specific to provers
+
+prelude "(set-logic AUFNIRA)"
+
+    A  : Array
+    UF : Uninterpreted Function
+    DT : Datatypes (not needed at the end ...)
+    NIRA : NonLinear Integer Reals Arithmetic
+
+*)
 
 printer "smtv2"
 filename "%f-%t-%g.smt2"
 unknown "^\\(unknown\\|sat\\|Fail\\)" ""
-outofmemory "^(error \".*out of memory\")\\|Cannot allocate memory"
-fail "^(error \"\\(W\\(A\\(R\\(N\\(I\\(N[^G]\\|[^N]\\)\\|[^I]\\)\\|[^N]\\)\\|[^R]\\)\\|[^A]\\)\\|[^W]\\)\\(.*\\)\")" "Error: \\1"
-timeout "interrupted by timeout"
 time "why3cpulimit time : %s s"
 valid "^unsat"
 
-(* À discuter *)
-transformation "inline_trivial"
-
-transformation "eliminate_builtin"
-transformation "eliminate_definition"
-transformation "eliminate_inductive"
-transformation "eliminate_algebraic"
-transformation "eliminate_epsilon"
-
-transformation "simplify_formula"
-(*transformation "simplify_trivial_quantification"*)
-
-transformation "discriminate"
-transformation "encoding_smt"
 
 theory BuiltIn
   syntax type int   "Int"
@@ -36,7 +33,7 @@ end
 
 theory int.Int
 
-  prelude ";;; this is a prelude for smt-lib v2 integer arithmetic"
+  prelude ";;; SMT-LIB2: integer arithmetic"
 
   syntax function zero "0"
   syntax function one  "1"
@@ -74,7 +71,7 @@ end
 
 theory real.Real
 
-  prelude ";;; this is a prelude for smt-lib v2 real arithmetic"
+  prelude ";;; SMT-LIB2: real arithmetic"
 
   syntax function zero "0.0"
   syntax function one  "1.0"
@@ -135,7 +132,7 @@ theory bool.Ite
   meta "encoding : lskept" function ite
 end
 
-(*
+(* not uniformly interpreted by provers
 theory real.Truncate
   syntax function floor "(to_int %1)"
   remove prop Floor_down

drivers/z3.drv

+(** Why3 driver for Z3 <= 4.3.1 *)
+
 prelude "(set-logic AUFNIRA)"
-(** A  : Array
-    UF : Uninterpreted Function
-    DT : Datatypes (not needed at the end ...)
-    NIRA : NonLinear Integer Reals Arithmetic
+(* A  : Array
+   UF : Uninterpreted Function
+   NIRA : NonLinear Integer Reals Arithmetic
 *)
 
-import "z3_bare.drv"
+import "smt-libv2.drv"
+import "discrimination.gen"
+
+transformation "inline_trivial"
+transformation "eliminate_builtin"
+transformation "eliminate_definition"
+transformation "eliminate_inductive"
+transformation "eliminate_algebraic"
+transformation "eliminate_epsilon"
+
+transformation "simplify_formula"
+(* transformation "simplify_trivial_quantification" *)
+
+transformation "discriminate"
+transformation "encoding_smt"
+
+(** Error messages specific to Z3 *)
+
+outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
+timeout "interrupted by timeout"
+(* stop reporting Z3 2.19 warnings as errors *)
+fail "^(error \"\\(W\\(A\\(R\\(N\\(I\\(N[^G]\\|[^N]\\)\\|[^I]\\)\\|[^N]\\)\\|[^R]\\)\\|[^A]\\)\\|[^W]\\)\\(.*\\)\")" "Error: \1"
+
 
+(** Extra theories supported by Z3 *)
+
+(* div/mod of Z3 seems to be Euclidean Division *)
+theory int.EuclideanDivision
+   syntax function div "(div %1 %2)"
+   syntax function mod "(mod %1 %2)"
+   remove prop Mod_bound
+   remove prop Div_mod
+   remove prop Mod_1
+   remove prop Div_1
+end
+
+theory real.FromInt
+  syntax function from_int "(to_real %1)"
+  remove prop Zero
+  remove prop One
+  remove prop Add
+  remove prop Sub
+  remove prop Mul
+  remove prop Neg
+end
+
+(* does not work: Z3 segfaults
+theory real.Trigonometry
+
+  syntax function cos "(cos %1)"
+  syntax function sin "(sin %1)"
+  syntax function pi "pi"
+  syntax function tan "(tan %1)"
+  syntax function atan "(atan %1)"
+
+end
+*)

drivers/z3_bare.drv → drivers/z3_432.drv

+(** Why3 driver for Z3 >= 4.3.2 *)
+
+(* Do not set any logic, let z3 choose by itself
+   prelude "(set-logic AUFNIRA)"
+*)
+
 import "smt-libv2.drv"
+import "discrimination.gen"
+
+transformation "inline_trivial"
+transformation "eliminate_builtin"
+(* temporarily disabled: too much experimental
+transformation "detect_polymorphism"
+*)
+transformation "eliminate_definition_if_poly"
+transformation "eliminate_inductive"
+transformation "eliminate_algebraic_if_poly"
+transformation "eliminate_epsilon"
+
+transformation "simplify_formula"
+(*transformation "simplify_trivial_quantification"*)
+
+transformation "discriminate_if_poly"
+transformation "encoding_smt_if_poly"
+
+
+(** Error messages specific to Z3 *)
+
+outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
+timeout "interrupted by timeout"
+
+(** Extra theories supported by Z3 *)
 
 (* div/mod of Z3 seems to be Euclidean Division *)
 theory int.EuclideanDivision
@@ -32,7 +63,6 @@ theory real.Trigonometry
 end
 *)
 
-import "discrimination.gen"
 
 (* bitvector modules, is not in smt-libv2.drv since cvc4 and z3 don't
    have the same name for the function to_int *)

examples/bts/12475/why3session.xml

@@ -2,17 +2,19 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
-<prover id="0" name="CVC3" version="2.4.1" timelimit="2" memlimit="0"/>
+<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
 <prover id="1" name="Alt-Ergo" version="0.95.1" timelimit="2" memlimit="0"/>
-<prover id="2" name="Z3" version="2.19" timelimit="2" memlimit="0"/>
-<prover id="3" name="Gappa" version="1.1.1" timelimit="5" memlimit="0"/>
-<file name="../12475.why">
+<prover id="2" name="CVC3" version="2.4.1" timelimit="2" memlimit="0"/>
+<prover id="3" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
+<prover id="4" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
+<file name="../12475.why" expanded="true">
 <theory name="Stmt" sum="468c7dbd45c8c0959e1b169a3ca1bbe3" expanded="true">
  <goal name="toto" expanded="true">
- <proof prover="0"><result status="valid" time="0.00"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="3"/></proof>
  <proof prover="1"><result status="valid" time="0.01"/></proof>
- <proof prover="2"><result status="valid" time="0.02"/></proof>
- <proof prover="3"><result status="unknown" time="0.00"/></proof>
+ <proof prover="2"><result status="valid" time="0.00"/></proof>
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <proof prover="4"><result status="valid" time="0.00"/></proof>
  </goal>
 </theory>
 </file>

examples/logic/lagrange_inequality/lagrange_inequality_CauchySchwarzInequality_CauchySchwarz_1.v

-(* This file is generated by Why3's Coq 8.4 driver *)
+(* This file is generated by Why3's Coq driver *)
 (* Beware! Only edit allowed sections below    *)
 Require Import BuiltIn.
 Require Reals.R_sqrt.
@@ -33,7 +33,7 @@ Axiom sqr_le_sqrt : forall (x:R) (y:R), ((Reals.RIneq.Rsqr x) <= y)%R ->
   (x <= (Reals.R_sqrt.sqrt y))%R.
 
 Require Import Why3.
-Ltac ae := why3 "Alt-Ergo,0.95.1," timelimit 3.
+Ltac ae := why3 "Alt-Ergo,0.99.1," timelimit 3.
 
 (* Why3 goal *)
 Theorem CauchySchwarz : forall (x1:R) (x2:R) (y1:R) (y2:R), ((dot x1 x2 y1

examples/logic/lagrange_inequality/lagrange_inequality_CauchySchwarzInequality_sqr_le_sqrt_1.v

-(* This file is generated by Why3's Coq 8.4 driver *)
+(* This file is generated by Why3's Coq driver *)
 (* Beware! Only edit allowed sections below    *)
 Require Import BuiltIn.
 Require Reals.R_sqrt.
@@ -30,7 +30,7 @@ Definition norm (x1:R) (x2:R): R := (Reals.R_sqrt.sqrt (norm2 x1 x2)).
 Axiom norm_pos : forall (x1:R) (x2:R), (0%R <= (norm x1 x2))%R.
 
 Require Import Why3.
-Ltac ae := why3 "Alt-Ergo,0.95.1," timelimit 3.
+Ltac ae := why3 "Alt-Ergo,0.99.1," timelimit 3.
 Import R_sqrt.
 
 Open Scope R_scope.

share/provers-detection-data.conf

@@ -107,7 +107,7 @@ exec = "cvc4-1.4"
 version_switch = "--version"
 version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
 version_ok  = "1.4"
-driver = "drivers/cvc4.drv"
+driver = "drivers/cvc4_14.drv"
 # --random-seed=42 is not needed as soon as --random-freq=0.0 by default
 # to try: --inst-when=full-last-call
 # --rlimit=%S : cvc4 1.4 DOES NOT accept -1 as argument
@@ -338,6 +338,7 @@ version_ok = "201310"
 
 # Z3 4.3.2 does not support option global option -rs anymore.
 # use settings given by "z3 -p" instead
+# Z3 4.3.2 supports Datatypes
 [ATP z3]
 name = "Z3"
 exec = "z3"
@@ -347,7 +348,7 @@ version_switch = "-version"
 version_regexp = "Z3 version \\([^ \n\r]+\\)"
 version_ok  = "4.3.3"
 version_ok = "4.3.2"
-driver = "drivers/z3_bare.drv"  # Do not set any logic, let z3 choose by itself
+driver = "drivers/z3_432.drv"
 command = "%l/why3-cpulimit %t %m -s %e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f"
 
 [ATP z3]

src/core/decl.ml

@@ -803,4 +803,3 @@ let make_record_pattern kn fll ty =
     | None -> pat_wild (ty_inst s (Opt.get pj.ls_value))
   in
   pat_app cs (List.map get_arg pjl) ty
-

src/core/printer.ml

@@ -336,6 +336,7 @@ let sprint_decl (fn : 'a -> Format.formatter -> decl -> 'a * string list) =
 
 exception UnsupportedType of ty   * string
 exception UnsupportedTerm of term * string
+exception UnsupportedPattern of pattern * string
 exception UnsupportedDecl of decl * string
 exception NotImplemented  of        string
 exception Unsupported     of        string
@@ -344,6 +345,7 @@ exception Unsupported     of        string
 
 let unsupportedType e s = raise (UnsupportedType (e,s))
 let unsupportedTerm e s = raise (UnsupportedTerm (e,s))
+let unsupportedPattern p s = raise (UnsupportedPattern (p,s))
 let unsupportedDecl e s = raise (UnsupportedDecl (e,s))
 let notImplemented    s = raise (NotImplemented s)
 let unsupported       s = raise (Unsupported s)
@@ -383,6 +385,9 @@ let () = Exn_printer.register (fun fmt exn -> match exn with
   | UnsupportedTerm (e,s) ->
       fprintf fmt "@[@[<hov 3> This expression isn't supported:@\n%a@]@\n %s@]"
         Pretty.print_term e s
+  | UnsupportedPattern (p,s) ->
+      fprintf fmt "@[@[<hov 3> This pattern isn't supported:@\n%a@]@\n %s@]"
+        Pretty.print_pat p s
   | UnsupportedDecl (d,s) ->
       fprintf fmt "@[@[<hov 3> This declaration isn't supported:@\n%a@]@\n %s@]"
         Pretty.print_decl d s

src/core/printer.mli

@@ -108,6 +108,7 @@ exception NotImplemented  of        string
 
 val unsupportedType : ty   -> string -> 'a
 val unsupportedTerm : term -> string -> 'a
+val unsupportedPattern : pattern -> string -> 'a
 val unsupportedDecl : decl -> string -> 'a
 val notImplemented  :         string -> 'a
 

src/core/task.mli

@@ -106,7 +106,11 @@ val task_decls  : task -> decl list
 
 val task_goal  : task -> prsymbol
 val task_goal_fmla  : task -> term
+
 val task_separate_goal : task -> tdecl * task
+(** [task_separate_goal t] returns a pair [(g,t')] where [g] is the
+    goal of the task [t] and [t'] is the rest.  raises [GoalNotFound]
+    if task [t] has no goal *)
 
 (** {2 selectors} *)
 
@@ -130,4 +134,3 @@ exception GoalNotFound
 exception GoalFound
 exception SkipFound
 exception LemmaFound
-

src/core/ty.mli

@@ -111,6 +111,7 @@ val ty_match : ty Mtv.t -> ty -> ty -> ty Mtv.t
 val ty_inst  : ty Mtv.t -> ty -> ty
 val ty_freevars : Stv.t -> ty -> Stv.t
 val ty_closed : ty -> bool
+(** [ty_closed ty] returns true when [ty] is not polymorphic *)
 
 val ty_equal_check : ty -> ty -> unit
 
@@ -150,4 +151,3 @@ val oty_cons : ty list -> ty option -> ty list
 val oty_match : ty Mtv.t -> ty option -> ty option -> ty Mtv.t
 val oty_inst  : ty Mtv.t -> ty option -> ty option
 val oty_freevars : Stv.t -> ty option -> Stv.t
-

src/printer/smtv2.ml

@@ -158,12 +158,59 @@ let rec print_term info fmt t = match t.t_node with
   | Tif (f1,t1,t2) ->
       fprintf fmt "@[(ite %a@ %a@ %a)@]"
         (print_fmla info) f1 (print_term info) t1 (print_term info) t2
+(*
   | Tcase _ -> unsupportedTerm t
-      "smtv2 : you must eliminate match"
+      "smtv2: you must eliminate match"
+*)
+  | Tcase(t,bl) ->
+     let subject = create_vsymbol (id_fresh "subject") (t_type t) in
+     fprintf fmt "@[(let ((%a @[%a@]))@ %a)@]"
+             print_var subject (print_term info) t
+             (print_branches info subject print_term) bl;
+     forget_var subject
   | Teps _ -> unsupportedTerm t
-      "smtv2 : you must eliminate epsilon"
+      "smtv2: you must eliminate epsilon"
   | Tquant _ | Tbinop _ | Tnot _ | Ttrue | Tfalse -> raise (TermExpected t)
 
+and print_branches info subject pr fmt bl =
+  match bl with
+  | [] -> assert false
+  | br::bl ->
+     let (p,t) = t_open_branch br in
+     let constr,args =
+       try
+         match p.pat_node with
+         | Papp(cs,args) ->
+            let vars = List.map
+                         (function { pat_node = Pvar v} -> v
+                                 | _ -> raise Exit) args
+            in cs,vars
+         | _ -> raise Exit
+       with Exit ->
+         unsupportedPattern p
+           "smtv2: you must compile nested pattern-matching"
+     in
+     match bl with
+     | [] -> print_branch info subject pr fmt (constr,args,t)
+     | _ ->
+        fprintf fmt "@[(ite (is-%a %a) %a %a)@]"
+                print_ident constr.ls_name print_var subject
+                (print_branch info subject pr) (constr,args,t)
+                (print_branches info subject pr) bl
+
+and print_branch info subject pr fmt (cs,vars,t) =
+  let i = ref 0 in
+  let print_proj fmt v =
+    incr i;
+    fprintf fmt "(%a (%a_proj_%d %a))" print_var v print_ident cs.ls_name
+            !i print_var subject
+  in
+  match vars with
+  | [] -> pr info fmt t
+  | _ -> fprintf fmt "@[(let (%a) %a)@]"
+                 (print_list space print_proj) vars
+                 (pr info) t
+
 and print_fmla info fmt f = match f.t_node with
   | Tapp ({ ls_name = id }, []) ->
       print_ident fmt id
@@ -215,8 +262,16 @@ and print_fmla info fmt f = match f.t_node with
       fprintf fmt "@[(let ((%a %a))@ %a)@]" print_var v
         (print_term info) t1 (print_fmla info) f2;
       forget_var v
+(*
   | Tcase _ -> unsupportedTerm f
       "smtv2 : you must eliminate match"
+ *)
+  | Tcase(t,bl) ->
+     let subject = create_vsymbol (id_fresh "subject") (t_type t) in
+     fprintf fmt "@[(let ((%a @[%a@]))@ %a)@]"
+             print_var subject (print_term info) t
+             (print_branches info subject print_fmla) bl;
+     forget_var subject
   | Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
 
 and print_expr info fmt =
@@ -269,11 +324,36 @@ let print_prop_decl info fmt k pr f = match k with
       fprintf fmt "@[(check-sat)@]@\n"
   | Plemma| Pskip -> assert false
 
+let print_constructor_decl info fmt (ls,args) =
+  match args with
+  | [] -> fprintf fmt "(%a)" print_ident ls.ls_name
+  | _ ->
+     fprintf fmt "@[(%a@ " print_ident ls.ls_name;
+     let _ = 
+       List.fold_left2
+         (fun i ty pr ->
+          begin match pr with
+                | Some pr -> fprintf fmt "(%a" print_ident pr.ls_name
+                | None -> fprintf fmt "(%a_proj_%d" print_ident ls.ls_name i
+          end;
+          fprintf fmt " %a)" (print_type info) ty;
+          succ i) 1 ls.ls_args args
+     in
+     fprintf fmt ")@]"
+
+let print_data_decl info fmt (ts,cl) =
+  fprintf fmt "@[(%a@ %a)@]"
+    print_ident ts.ts_name
+    (print_list space (print_constructor_decl info)) cl
+
 let print_decl info fmt d = match d.d_node with
   | Dtype ts ->
       print_type_decl info fmt ts
-  | Ddata _ -> unsupportedDecl d
-      "smtv2 : algebraic type are not supported"
+  | Ddata dl ->
+    (*unsupportedDecl d
+      "smtv2 : algebraic type are not supported" *)
+    fprintf fmt "@[(declare-datatypes ()@ (%a))@]@\n"
+      (print_list space (print_data_decl info)) dl
   | Dparam ls ->
       print_param_decl info fmt ls
   | Dlogic dl ->

src/transform/detect_polymorphism.ml

+(********************************************************************)
+(*                                                                  *)
+(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
+(*  Copyright 2010-2014   --   INRIA - CNRS - Paris-Sud University  *)
+(*                                                                  *)
+(*  This software is distributed under the terms of the GNU Lesser  *)
+(*  General Public License version 2.1, with the special exception  *)
+(*  on linking described in file LICENSE.                           *)
+(*                                                                  *)
+(********************************************************************)
+
+open Decl
+open Theory
+
+let debug = Debug.register_info_flag "detect_poly"
+  ~desc:"Print@ debugging@ messages@ of@ the@ 'detect_polymorphism'@ transformation."
+
+let meta_monomorphic_types_only =
+  register_meta_excl "encoding:monomorphic_only" []
+  ~desc:"Set@ when@ no@ occurrences@ of@ type@ variables@ occur."
+
+(*
+let meta_has_polymorphic_types =
+  register_meta_excl "encoding:polymorphic_types" []
+  ~desc:"Set@ when@ occurrences@ of@ type@ variables@ occur."
+*)
+
+exception Found
+
+open Term
+
+let check_ts ts =
+  if ts.Ty.ts_args <> [] then
+    (Debug.dprintf debug "====== Type %a is polymorphic =======@."
+       Pretty.print_ts ts;
+     raise Found)
+
+let check_ls ls =
+  if not (ls_equal ls ps_equ) then
+    try
+      List.iter (fun ty -> if not (Ty.ty_closed ty) then raise Found)
+        ls.ls_args
+    with Found ->
+      Debug.dprintf debug "====== Symbol %a is polymorphic =======@."
+        Pretty.print_ls ls;
+      raise Found
+
+let check_term t =
+  let s = Term.t_ty_freevars Ty.Stv.empty t in
+  if not (Ty.Stv.is_empty s) then raise Found
+
+let find_in_decl d =
+  match d.d_node with
+  | Dtype ts ->
+    Debug.dprintf debug "@[Dtype %a@]@." Pretty.print_ts ts;
+    check_ts ts
+  | Ddata dl ->
+    Debug.dprintf debug "@[Ddata %a@]@."
+      (Pp.print_list Pp.space Pretty.print_data_decl) dl;
+    List.iter (fun (ts,_) -> check_ts ts) dl
+  | Dparam ls ->
+    Debug.dprintf debug "@[Dparam %a@]@." Pretty.print_ls ls;
+    check_ls ls
+  | Dlogic dl ->
+    Debug.dprintf debug "@[Dlogic %a@]@."
+      (Pp.print_list Pp.space Pretty.print_ls) (List.map fst dl);
+    List.iter (fun (ls,_) -> check_ls ls) dl
+    (* TODO: check also that definition bodies are monomorphic ? *)
+  | Dind (_,indl) ->
+    Debug.dprintf debug "@[Dind %a@]@."
+      (Pp.print_list Pp.space Pretty.print_ls) (List.map fst indl);
+    List.iter (fun (ls,_) -> check_ls ls) indl
+    (* TODO: check also that clauses are monomorphic ? *)
+  | Dprop (_,pr,t) ->
+    Debug.dprintf debug "@[Dprop %a@]@." Pretty.print_pr pr;
+    try check_term t
+    with Found ->
+      Debug.dprintf debug "====== prop is polymorphic =======@.";
+      raise Found
+
+
+(**)
+
+let (*
+rec find_in_theory th = List.iter find_in_tdecl th.th_decls
+
+and
+    *)
+find_in_tdecl td =
+  match td.td_node with
+  | Decl d -> find_in_decl d
+  | Use _th ->
+    (* Debug.dprintf debug "Look up in used theory %a@." Pretty.print_th th; *)
+    (* find_in_theory th *)
+    () (* no need to traverse used theories *)
+  | Clone (_th,_) ->
+    (* Debug.dprintf debug "Look up in cloned theory %a@." Pretty.print_th th; *)
+    (* find_in_theory th *)
+    () (* no need to traverse used theories *)
+  | Meta  _ -> ()
+