detect_polymorphism.ml 4.26 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
5 6 7 8 9 10 11 12 13
(*                                                                  *)
(*  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
14 15 16

let debug = Debug.register_info_flag "detect_poly"
  ~desc:"Print@ debugging@ messages@ of@ the@ 'detect_polymorphism'@ transformation."
17 18

let meta_monomorphic_types_only =
MARCHE Claude's avatar
MARCHE Claude committed
19
  register_meta_excl "encoding:monomorphic_only" []
20 21 22 23 24 25 26
  ~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."
*)
27

MARCHE Claude's avatar
MARCHE Claude committed
28 29
exception Found

30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51
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

52 53
let find_in_decl d =
  match d.d_node with
MARCHE Claude's avatar
MARCHE Claude committed
54
  | Dtype ts ->
55 56 57 58 59
    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;
60
    List.iter (fun (ts,_) -> check_ts ts) dl
61 62 63 64 65 66 67
  | 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
68
    (* TODO: check also that definition bodies are monomorphic ? *)
69 70 71 72
  | 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
73
    (* TODO: check also that clauses are monomorphic ? *)
74 75 76 77 78 79 80 81 82
  | 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


(**)
83

84 85
let (*
rec find_in_theory th = List.iter find_in_tdecl th.th_decls
86

87 88 89
and
    *)
find_in_tdecl td =
90 91
  match td.td_node with
  | Decl d -> find_in_decl d
92 93 94 95 96 97 98 99
  | 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 *)
MARCHE Claude's avatar
MARCHE Claude committed
100
  | Meta  _ -> ()
101 102 103

let rec find_in_task task =
  match task with
MARCHE Claude's avatar
MARCHE Claude committed
104
  | None -> ()
105
  | Some t -> find_in_task t.Task.task_prev ; find_in_tdecl t.Task.task_decl
106 107

let detect_polymorphism task =
MARCHE Claude's avatar
MARCHE Claude committed
108 109 110
  try
    find_in_task task;
    try
111 112
      let g,t = Task.task_separate_goal task in
      let ta = Task.add_meta t meta_monomorphic_types_only [] in
MARCHE Claude's avatar
MARCHE Claude committed
113
      Task.add_tdecl ta g
114 115
    with Task.GoalNotFound ->
      Task.add_meta task meta_monomorphic_types_only []
MARCHE Claude's avatar
MARCHE Claude committed
116 117 118 119 120
  with Found -> task

let () = Trans.register_transform "detect_polymorphism"
  (Trans.store detect_polymorphism)
  ~desc:"Detect if task has polymorphic types somewhere."
121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139


(* 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."

*)