detect_polymorphism.ml 4.23 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

let debug = Debug.register_info_flag "detect_poly"
Andrei Paskevich's avatar
Andrei Paskevich committed
16 17
  ~desc:"Print@ debugging@ messages@ of@ the@ \
    'detect_polymorphism'@ transformation."
18

19
(* metas to attach to symbols or propositions to tell their polymorphic
Andrei Paskevich's avatar
Andrei Paskevich committed
20 21
   nature can be ignored because it will be treated specifically by
   drivers *)
22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40

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 *)

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

MARCHE Claude's avatar
MARCHE Claude committed
45

46 47
let check_ts ign_ts ts =
  ts.Ty.ts_args <> [] && not (Ty.Sts.mem ts ign_ts)
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
Andrei Paskevich's avatar
Andrei Paskevich committed
54
    (Ty.oty_cons ls.Term.ls_args ls.Term.ls_value)
55

56 57 58 59 60 61 62
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;
63
  match d.d_node with
64
  | Dtype ts -> check_ts ign_ts ts
65
  | Ddata dl ->
66
     List.fold_left (fun acc (ts,_) -> acc || check_ts ign_ts ts) false dl
67
  | Dparam ls ->
68 69 70
     Debug.dprintf debug "[detect_polymorphism] param %a@."
                Pretty.print_ls ls;
     check_ls ign_ls ls
71
  | Dlogic dl ->
72 73 74
     (* 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
75
  | Dind (_,indl) ->
76 77 78
     (* 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
79
  | Dprop (_,pr,t) ->
80
     (* todo: NE PAS TESTER le goal *)
81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104
     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)))
105 106

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

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