eliminate_inductive.ml 2.33 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2019   --   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 13 14 15

open Ident
open Term
open Decl

16
let log acc (ps,_) = create_param_decl ps :: acc
17 18 19 20
let axm acc (pr,f) = create_prop_decl Paxiom pr f :: acc
let imp acc (_,al) = List.fold_left axm acc al

let exi vl (_,f) =
21
  let rec descend f = match f.t_node with
22 23 24 25 26
    | Tquant (Tforall,f) ->
        let vl,tl,f = t_open_quant f in
        t_exists_close vl tl (descend f)
    | Tbinop (Timplies,g,f) ->
        t_and g (descend f)
27
    | Tapp (_,tl) ->
28 29
        let marry acc v t = t_and_simp acc (t_equ v t) in
        List.fold_left2 marry t_true vl tl
30 31 32 33 34
    | Tlet (t, tb) ->
        let v, f = t_open_bound tb in
        t_let_close v t (descend f)
    | _ ->
        assert false (* ensured by Decl.create_ind_decl *)
35 36 37 38 39 40
  in
  descend f

let inv acc (ps,al) =
  let vl = List.map (create_vsymbol (id_fresh "z")) ps.ls_args in
  let tl = List.map t_var vl in
41
  let hd = ps_app ps tl in
42
  let dj = Lists.map_join_left (exi tl) t_or al in
43 44 45
  let hsdj =
    Simplify_formula.fmla_remove_quant ~keep_model_vars:false (t_implies hd dj)
  in
46
  let ax = t_forall_close vl [] hsdj in
47
  let nm = id_derive (ps.ls_name.id_string ^ "_inversion") ps.ls_name in
48 49 50
  create_prop_decl Paxiom (create_prsymbol nm) ax :: acc

let elim d = match d.d_node with
51
  | Dind (_, il) ->
52 53 54 55 56 57
      let dl = List.fold_left log [] il in
      let dl = List.fold_left imp dl il in
      let dl = List.fold_left inv dl il in
      List.rev dl
  | _ -> [d]

58
let eliminate_inductive = Trans.decl elim None
59

60
let () = Trans.register_transform "eliminate_inductive" eliminate_inductive
Andrei Paskevich's avatar
Andrei Paskevich committed
61 62
  ~desc:"Replace@ inductive@ predicates@ by@ (incomplete)@ axiomatic@ \
         definitions,@ i.e.@ construction@ axioms@ and@ an@ inversion@ axiom."