lift_epsilon.ml 3.34 KB
Newer Older
1 2 3
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
MARCHE Claude's avatar
MARCHE Claude committed
4 5 6
(*    François Bobot                                                     *)
(*    Jean-Christophe Filliâtre                                          *)
(*    Claude Marché                                                      *)
7 8 9 10 11 12 13 14 15 16 17 18 19
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

20
open Close_epsilon
21 22 23 24
open Term
open Theory
open Task

25 26 27 28
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 *)
29

30 31 32 33 34
let lift kind =
  let rec term acc t =
    match t.t_node with
    | Teps fb ->
        let fv = Svs.elements (t_freevars Svs.empty t) in
35
        let x, f = t_open_bound fb in
36 37 38 39 40 41 42
        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
        let acc = add_decl acc (Decl.create_logic_decl [xl,None]) in
        let axs =
          Decl.create_prsymbol (Ident.id_derive ("epsilon_def") x.vs_name) in
43
        let xlapp = t_app xl (List.map t_var fv) t.t_ty in
44 45 46 47 48
        let f =
          match kind with
          (* assume that lambdas always exist *)
          | Implied when not (is_lambda t) ->
              f_forall_close_merge fv
Francois Bobot's avatar
Francois Bobot committed
49
                (f_implies (f_exists_close [x] [] f)
50 51
                   (t_subst_single x xlapp f))
          | _ -> t_subst_single x xlapp f
52 53 54
        in
        let acc = add_decl acc (Decl.create_prop_decl Decl.Paxiom axs f) in
        acc, xlapp
55 56
    | _ -> TermTF.t_map_fold term form acc t
  and form acc f = TermTF.t_map_fold term form acc f in
57 58 59 60
  fun th acc ->
    let th = th.task_decl in
    match th.td_node with
    | Decl d ->
61
        let acc, d = Decl.DeclTF.decl_map_fold term form acc d in
62 63
        add_decl acc d
    | _ -> add_tdecl acc th
64

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

Francois Bobot's avatar
Francois Bobot committed
67 68
let meta_epsilon = Theory.register_meta_excl "lift_epsilon" [MTstring]

69 70 71 72 73
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
74 75 76
      | _ -> failwith "lift_epsilon accepts only 'implicit' and 'implied'"
    in
    lift_epsilon kind)
77

Francois Bobot's avatar
Francois Bobot committed
78
let () = Trans.register_transform "lift_epsilon" lift_epsilon