Transformation detect_polymorphism seems to work, although

probably not efficient because not memoized (Claude needs help for that)

src/core/ty.mli

@@ -112,6 +112,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
 
@@ -151,4 +152,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/transform/detect_polymorphism.ml

@@ -11,57 +11,124 @@
 
 open Decl
 open Theory
-open Task
+
+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@ occurence@ of@ type@ variables@ occur."
+  ~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 ->
-    Format.eprintf "======@\nFound type %a@\n" Pretty.print_ts ts;
-    if ts.Ty.ts_args <> [] then
-      (Format.eprintf "Type is polymorphic!@\n=======@.";
-       raise Found);
-    Format.eprintf "=======@."
-  | Ddata _dl -> () (* TODO *)
-  | Dparam _ls -> () (* TODO *)
-  | Dlogic _dl -> () (* TODO *)
-  | Dind _ind -> () (* TODO *)
-  | Dprop _p ->  () (* TODO *)
+    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
+  | 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
+  | 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 ->
-    Format.eprintf "======@\nLook up in used theory %a@." Pretty.print_th th;
-    find_in_theory th
-  | Clone (th,_) ->
-    Format.eprintf "======@\nLook up in cloned theory %a@." Pretty.print_th th;
-    find_in_theory th
+  | 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  _ -> ()
 
 let rec find_in_task task =
   match task with
   | None -> ()
-  | Some t -> find_in_task t.task_prev ; find_in_tdecl t.task_decl
+  | Some t -> find_in_task t.Task.task_prev ; find_in_tdecl t.Task.task_decl
 
 let detect_polymorphism task =
   try
     find_in_task task;
     try
-      let g,t = task_separate_goal task in
-      let ta = add_meta t meta_monomorphic_types_only [] in
+      let g,t = Task.task_separate_goal task in
+      let ta = Task.add_meta t meta_monomorphic_types_only [] in
       Task.add_tdecl ta g
-    with GoalNotFound ->
-      add_meta task meta_monomorphic_types_only []
+    with Task.GoalNotFound ->
+      Task.add_meta task meta_monomorphic_types_only []
   with Found -> task
 
 let () = Trans.register_transform "detect_polymorphism"
   (Trans.store detect_polymorphism)
   ~desc:"Detect if task has polymorphic types somewhere."
+
+
+(* A variant, not satisfactory
+let check_decl d =
+  try
+    find_in_decl d;
+    [Theory.create_decl d]
+  with Found ->
+    [Theory.create_meta meta_has_polymorphic_types [];
+     Theory.create_decl d]
+
+
+let detect_polymorphism = Trans.tdecl check_decl None
+
+let () = Trans.register_transform "detect_polymorphism"
+  detect_polymorphism
+  ~desc:"Detect if task has polymorphic types somewhere."
+
+*)

src/transform/discriminate.ml

@@ -24,7 +24,7 @@ let meta_inst = register_meta "encoding : inst" [MTty]
 let meta_lskept = register_meta "encoding : lskept" [MTlsymbol]
   ~desc:"Specify@ which@ function/predicate@ symbols@ should@ be@ kept.@ \
          When@ the@ symbol@ is@ polymorphic,@ generate@ every@ possible@ \
-         type@ insntance@ with@ types@ marked@ by@ 'encoding : inst'."
+         type@ instances@ with@ types@ marked@ by@ 'encoding : inst'."
 
 let meta_lsinst = register_meta "encoding : lsinst" [MTlsymbol;MTlsymbol]
   ~desc:"Specify@ which@ type@ instances@ of@ symbols@ should@ be@ kept.@ \

tests/test-poly.why

@@ -2,6 +2,8 @@
 
 theory Mono
 
+goal g0 : 2 = 3
+
 use import int.Int
 
 goal g : 2+2 = 5
@@ -15,6 +17,8 @@ type t 'a = A 'a
 
 goal g: forall x y:'a. A x = A y
 
+(* bin/why3prove.byte tests/test-poly.why --debug detect_poly -a detect_polymorphism -D why3 -T PolyType -G g *)
+
 end
 
 
@@ -25,3 +29,22 @@ use import list.List
 goal g : match Cons 42 Nil with Nil -> false | Cons x _ -> x=42 end
 
 end
+
+
+theory PolySymb
+
+function id (x:'a) : 'a = 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 PolyProp
+
+goal g: forall x:'a. x = x
+
+(* bin/why3prove.byte tests/test-poly.why --debug detect_poly -a detect_polymorphism -D why3 -T PolyProp -G g *)
+
+end