simplify_array.ml 838 Bytes
Newer Older
Francois Bobot's avatar
   
Francois Bobot committed
1
2
3
4
5
6
7
8
9
10
11
open Term
open Termlib
open Theory

open Transform

let prelude = ["prelude"]
let array = "Array"
let store = ["store"]
let select = ["select"]

12
13
14
15
let make_rt_rf h =
  let rec rt env t =
    let t = t_map (rt env) (rf env) t in
    let array  = find_theory env prelude array in
16
17
    let store  = (ns_find_ls array.th_export store).ls_name in
    let select = (ns_find_ls array.th_export select).ls_name in
Francois Bobot's avatar
   
Francois Bobot committed
18
19
    match t.t_node with
      | Tapp (lselect,[{t_node=Tapp(lstore,[_;a1;b])};a2])
20
21
          when lselect.ls_name == select &&
            lstore.ls_name == store &&
Francois Bobot's avatar
   
Francois Bobot committed
22
23
24
25
26
27
            t_equal_alpha a1 a2 -> b
      | _ -> t
  and rf ctxt f = f_map (rt ctxt) (rf ctxt) f  in
  rt,rf
  
let t () =
28
29
30
  let h = Hashtbl.create 5 in
  let rt,rf = make_rt_rf h in
  Transform.rewrite_env rt rf
Francois Bobot's avatar
   
Francois Bobot committed
31
32

let () = Driver.register_transform "simplify_array" t