encoding_select.ml 3.74 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
4
(*  Copyright 2010-2016   --   INRIA - CNRS - Paris-Sud University  *)
5 6 7 8
(*                                                                  *)
(*  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.                           *)
9
(*                                                                  *)
10
(********************************************************************)
11

12
open Stdlib
13 14
open Ty
open Term
15
open Decl
16 17 18
open Theory
open Task
open Encoding
19
open Discriminate
20

21
let register pr l = List.iter (fun (n,f) -> Hstr.replace pr n (Util.const f)) l
22

23 24
let register pr none goal all =
  register pr ["none",none; "goal",goal; "all",all]
25

26
(** {2 select Kept} *)
27

28 29 30
let trans_on_goal fn = Trans.store (function
  | Some { task_decl = { td_node = Decl { d_node = Dprop (_,_,f) }}} -> fn f
  | _ -> assert false)
31 32

module Kept = struct
33 34 35 36 37
  (* we ignore the type of the result as we are
     only interested in application arguments *)
  let add_kept sty _ls tyl _tyv =
    let add sty ty = if ty_closed ty then Sty.add ty sty else sty in
    List.fold_left add sty tyl
38

39
  let add_kept = t_app_fold add_kept
40

41 42 43
  let all_kept task sty = match task.task_decl.td_node with
    | Decl d -> decl_fold add_kept sty d
    | _ -> sty
44

45 46 47
  let kept_none = Trans.return Sty.empty
  let kept_goal = trans_on_goal (add_kept Sty.empty)
  let kept_all  = Trans.fold all_kept Sty.empty
48

49 50
  let () = register ft_select_kept kept_none kept_goal kept_all
  let () = register ft_select_inst kept_none kept_goal kept_all
51 52
end

53
(** {2 select Lskept} *)
54

55
module Lskept = struct
56

57 58 59 60 61 62 63 64 65 66 67 68 69
  let add_lskept sls ls =
    (* We require that every freely standing type variable occurs
       under a type constructor elsewhere in the lsymbol's signature.
       Thus we bound the (lskept * inst) product and avoid explosion. *)
    let ls_sig = oty_cons ls.ls_args ls.ls_value in
    let add_ty_t s ty = match ty.ty_node with
      | Tyapp _ -> ty_freevars s ty | _ -> s in
    let ls_tvs_t = List.fold_left add_ty_t Stv.empty ls_sig in
    if Stv.is_empty ls_tvs_t then sls else
    let add_ty_v s ty = match ty.ty_node with
      | Tyvar v -> Stv.add v s | _ -> s in
    let ls_tvs_v = List.fold_left add_ty_v Stv.empty ls_sig in
    if Stv.subset ls_tvs_v ls_tvs_t then Sls.add ls sls else sls
70

71
  let all_lskept task sls = match task.task_decl.td_node with
72 73
    | Decl { d_node = Dparam ls } ->
        add_lskept sls ls
74 75 76
    | Decl { d_node = Dlogic l } ->
        List.fold_left (fun sls (ls,_) -> add_lskept sls ls) sls l
    | _ -> sls
77

78
  let add_lskept = t_app_fold (fun sls ls _ _ -> add_lskept sls ls)
79

80 81 82
  let lskept_none = Trans.return Sls.empty
  let lskept_goal = trans_on_goal (add_lskept Sls.empty)
  let lskept_all  = Trans.fold all_lskept Sls.empty
83

84 85
  let () = register ft_select_lskept lskept_none lskept_goal lskept_all
end
86

87
(** {2 select Lsinst} *)
88

89
module Lsinst = struct
90

91
  let add_lsinst mls ls tyl tyv =
92
    if ls_equal ls ps_equ ||
93
      List.for_all ty_closed (oty_cons ls.ls_args ls.ls_value) ||
94 95
      List.exists (fun ty -> not (ty_closed ty)) (oty_cons tyl tyv)
    then mls else Lsmap.add ls tyl tyv mls
96

97
  let add_lsinst mls t = t_app_fold add_lsinst mls t
98

99 100 101
  let all_lsinst task mls = match task.task_decl.td_node with
    | Decl d -> decl_fold add_lsinst mls d
    | _ -> mls
102

103 104 105
  let lsinst_none = Trans.return Lsmap.empty
  let lsinst_goal = trans_on_goal (add_lsinst Lsmap.empty)
  let lsinst_all  = Trans.fold all_lsinst Lsmap.empty
106

107 108
  let () = register ft_select_lsinst lsinst_none lsinst_goal lsinst_all
end