simplify_array.ml 1.66 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University  *)
5 6 7 8 9 10
(*                                                                  *)
(*  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.                           *)
(*                                                                  *)
(********************************************************************)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
11

12 13
open Term
open Theory
Francois Bobot's avatar
Francois Bobot committed
14
open Env
15

16 17 18 19
let prelude = ["map"]
let array = "Map"
let store = ["set"]
let select = ["get"]
20

Francois Bobot's avatar
Francois Bobot committed
21
let make_rt_rf env =
Andrei Paskevich's avatar
Andrei Paskevich committed
22
  let array  =
23
    try
24
      read_theory ~format:"why" env prelude array
Andrei Paskevich's avatar
Andrei Paskevich committed
25 26 27
    with TheoryNotFound (_,s) ->
      Format.eprintf "The theory %s is unknown" s;
      exit 1 in
Francois Bobot's avatar
Francois Bobot committed
28 29 30
  let store  = (ns_find_ls array.th_export store).ls_name in
  let select = (ns_find_ls array.th_export select).ls_name in
  let rec rt t =
31
    let t = TermTF.t_map rt rf t in
32 33
    match t.t_node with
      | Tapp (lselect,[{t_node=Tapp(lstore,[_;a1;b])};a2])
34 35
          when lselect.ls_name == select &&
            lstore.ls_name == store &&
36 37
            t_equal_alpha a1 a2 -> b
      | _ -> t
38
  and rf f = TermTF.t_map rt rf f  in
39
  rt,rf
Andrei Paskevich's avatar
Andrei Paskevich committed
40

41
let t env = let rt,rf = make_rt_rf env in Trans.rewriteTF rt rf None
42

43
let () = Trans.register_env_transform "simplify_array" t
Andrei Paskevich's avatar
Andrei Paskevich committed
44 45
  ~desc:"Apply,@ wherever@ possible,@ the@ axiom@ 'Select_eq'@ of@ \
         the@ library@ theory@ map.Map."