detect_polymorphism.ml 4.15 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 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39
(* metas to attach to symbols or propositions to tell their polymorphic
nature can be ignored because it will be treated specifically by
drivers *)

let meta_ignore_polymorphism_ts =
  register_meta
    "encoding:ignore_polymorphism_ts" [MTtysymbol]
    ~desc:"Ignore@ polymorphism@ of@ given@ type@ symbol."

let meta_ignore_polymorphism_ls =
  register_meta
    "encoding:ignore_polymorphism_ls" [MTlsymbol]
    ~desc:"Ignore@ polymorphism@ of@ given@ logic@ symbol."

let meta_ignore_polymorphism_pr =
  register_meta
    "encoding:ignore_polymorphism_pr" [MTprsymbol]
    ~desc:"Ignore@ polymorphism@ of@ given@ proposition."

(* exclusive meta that is set by the transformation when no
   polymorphic definition is found *)

40
let meta_monomorphic_types_only =
MARCHE Claude's avatar
MARCHE Claude committed
41
  register_meta_excl "encoding:monomorphic_only" []
42 43
  ~desc:"Set@ when@ no@ occurrences@ of@ type@ variables@ occur."

MARCHE Claude's avatar
MARCHE Claude committed
44

45 46
let check_ts ign_ts ts =
  ts.Ty.ts_args <> [] && not (Ty.Sts.mem ts ign_ts)
47

48 49 50 51 52 53
let check_ls ign_ls ls =
  not (Term.Sls.mem ls ign_ls) &&
  List.fold_left
    (fun acc ty -> acc || not (Ty.ty_closed ty))
    false
    ls.Term.ls_args
54

55 56 57 58 59 60 61
let detect_polymorphism_in_decl ign_ts ign_ls ign_pr d =
  Debug.dprintf debug "[detect_polymorphism] |sts|=%d |sls|=%d |spr|=%d@."
                (Ty.Sts.cardinal ign_ts)
                (Term.Sls.cardinal ign_ls)
                (Spr.cardinal ign_pr);
  Debug.dprintf debug "[detect_polymorphism] decl %a@."
                Pretty.print_decl d;
62
  match d.d_node with
63
  | Dtype ts -> check_ts ign_ts ts
64
  | Ddata dl ->
65
     List.fold_left (fun acc (ts,_) -> acc || check_ts ign_ts ts) false dl
66
  | Dparam ls ->
67 68 69
     Debug.dprintf debug "[detect_polymorphism] param %a@."
                Pretty.print_ls ls;
     check_ls ign_ls ls
70
  | Dlogic dl ->
71 72 73
     (* note: we don't need to check also that definition bodies are
        monomorphic, since it is checked by typing *)
     List.fold_left (fun acc (ls,_) -> acc || check_ls ign_ls ls) false dl
74
  | Dind (_,indl) ->
75 76 77
     (* note: we don't need to check also that clauses are
        monomorphic, since it is checked by typing *)
     List.fold_left (fun acc (ls,_) -> acc || check_ls ign_ls ls) false indl
78
  | Dprop (_,pr,t) ->
79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102
     not (Spr.mem pr ign_pr) &&
       let s = Term.t_ty_freevars Ty.Stv.empty t in
       not (Ty.Stv.is_empty s)


let detect_polymorphism_in_task_hd ign_ts ign_l ign_pr t acc =
  match t.Task.task_decl.td_node with
  | Decl d -> acc || detect_polymorphism_in_decl ign_ts ign_l ign_pr d
  | Use _ | Clone _ | Meta _ -> acc


let detect_polymorphism_in_task =
  Trans.on_tagged_ts
    meta_ignore_polymorphism_ts
    (fun sts ->
     Trans.on_tagged_ls
       meta_ignore_polymorphism_ls
       (fun sls ->
        Trans.on_tagged_pr
          meta_ignore_polymorphism_pr
          (fun spr ->
           Trans.fold
             (detect_polymorphism_in_task_hd sts sls spr)
             false)))
103 104

let detect_polymorphism task =
105
  if Trans.apply detect_polymorphism_in_task task then task else
MARCHE Claude's avatar
MARCHE Claude committed
106
    try
107 108
      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
109
      Task.add_tdecl ta g
110 111
    with Task.GoalNotFound ->
      Task.add_meta task meta_monomorphic_types_only []
MARCHE Claude's avatar
MARCHE Claude committed
112 113 114 115

let () = Trans.register_transform "detect_polymorphism"
  (Trans.store detect_polymorphism)
  ~desc:"Detect if task has polymorphic types somewhere."