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

11
open Close_epsilon
12 13 14 15
open Term
open Theory
open Task

16 17 18 19
type lift_kind =
(*   | Goal (* prove the existence of a witness *) *)
  | Implied (* require the existence of a witness in an axiom *)
  | Implicit (* do not require a witness *)
20

21 22 23 24
let lift kind =
  let rec term acc t =
    match t.t_node with
    | Teps fb ->
25
        let fv = Mvs.keys (t_vars t) in
26
        let x, f = t_open_bound fb in
27 28 29 30
        let acc, f = form acc f in
        let tys = List.map (fun x -> x.vs_ty) fv in
        let xs = Ident.id_derive "epsilon" x.vs_name in
        let xl = create_fsymbol xs tys x.vs_ty in
31
        let acc = add_decl acc (Decl.create_param_decl xl) in
32 33
        let axs =
          Decl.create_prsymbol (Ident.id_derive ("epsilon_def") x.vs_name) in
34
        let xlapp = t_app xl (List.map t_var fv) t.t_ty in
35 36 37 38
        let f =
          match kind with
          (* assume that lambdas always exist *)
          | Implied when not (is_lambda t) ->
39 40
              t_forall_close_merge fv
                (t_implies (t_exists_close [x] [] f)
41 42
                   (t_subst_single x xlapp f))
          | _ -> t_subst_single x xlapp f
43 44 45
        in
        let acc = add_decl acc (Decl.create_prop_decl Decl.Paxiom axs f) in
        acc, xlapp
46 47
    | _ -> TermTF.t_map_fold term form acc t
  and form acc f = TermTF.t_map_fold term form acc f in
48 49 50 51
  fun th acc ->
    let th = th.task_decl in
    match th.td_node with
    | Decl d ->
52
        let acc, d = Decl.DeclTF.decl_map_fold term form acc d in
53 54
        add_decl acc d
    | _ -> add_tdecl acc th
55

Francois Bobot's avatar
Francois Bobot committed
56
let lift_epsilon kind = Trans.fold (lift kind) None
57

Francois Bobot's avatar
Francois Bobot committed
58
let meta_epsilon = Theory.register_meta_excl "lift_epsilon" [MTstring]
Andrei Paskevich's avatar
Andrei Paskevich committed
59 60 61 62 63 64 65
  ~desc:"Specify@ whether@ the@ existence@ of@ a@ witness@ for@ the@ \
    formula@ under@ epsilon@ is@ assumed:@;  \
    @[\
      - @[<hov 2>implicit:@ implicitly@ assume@ existence@]@\n\
      - @[<hov 2>implied:@ @ do@ not@ assume@ the@ existence@ \
          of@ a@ witness.@]\
    @]"
Francois Bobot's avatar
Francois Bobot committed
66

67 68 69 70 71
let lift_epsilon = Trans.on_meta_excl meta_epsilon
  (fun alo ->
    let kind = match alo with
      | Some [MAstr "implicit"] -> Implicit
      | Some [MAstr "implied"] | None -> Implied
Francois Bobot's avatar
Francois Bobot committed
72 73 74
      | _ -> failwith "lift_epsilon accepts only 'implicit' and 'implied'"
    in
    lift_epsilon kind)
75

Francois Bobot's avatar
Francois Bobot committed
76
let () = Trans.register_transform "lift_epsilon" lift_epsilon
Andrei Paskevich's avatar
Andrei Paskevich committed
77
  ~desc:"Move@ epsilon-terms@ into@ separate@ function@ definitions."