simplify_recursive_definition.ml 3.9 KB
Newer Older
1 2 3 4 5 6 7 8 9 10
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2012   --   INRIA - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  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.                           *)
(*                                                                  *)
(********************************************************************)
11

12
open Util
13 14 15
open Ident
open Ty
open Term
Andrei Paskevich's avatar
Andrei Paskevich committed
16
open Decl
17 18 19 20 21 22

type seen =
  | SNot
  | SOnce
  | SBack

Andrei Paskevich's avatar
Andrei Paskevich committed
23
let rec find h e =
24 25
  try
    let r = Hid.find h e in
Andrei Paskevich's avatar
Andrei Paskevich committed
26 27
    if r == e then e
    else
28 29 30 31 32 33 34
      let r = find h r in
      Hid.replace h e r;
      r
  with Not_found -> e

let union h e1 e2 = Hid.replace h (find h e1) (find h e2)

Andrei Paskevich's avatar
Andrei Paskevich committed
35
let connexe (m:Sid.t Mid.t)  =
36 37 38
  let uf = Hid.create 32 in
  let visited = Hid.create 32 in
  Mid.iter (fun e _ -> Hid.replace visited e SNot) m;
Andrei Paskevich's avatar
Andrei Paskevich committed
39
  let rec visit i last =
40
    match Hid.find visited i with
Andrei Paskevich's avatar
Andrei Paskevich committed
41
      | SNot ->
42 43 44 45 46
          Hid.replace visited i SOnce;
          let s = Mid.find i m in
          let last = i::last in
          Sid.iter (fun x -> visit x last) s;
          Hid.replace visited i SBack
Andrei Paskevich's avatar
Andrei Paskevich committed
47 48
      | SOnce ->
          (try
49 50 51 52 53 54
             List.iter (fun e -> if e==i then raise Exit else union uf i e) last
           with Exit -> ())
      | SBack -> ()
  in
  Mid.iter (fun e _ -> visit e []) m;
  let ce = Hid.create 32 in
Andrei Paskevich's avatar
Andrei Paskevich committed
55
  Mid.iter (fun e es ->
56 57 58 59 60 61 62 63 64 65
              let r = find uf e in
              let rl,rs,rb = try
                Hid.find ce r
              with Not_found -> [],Sid.empty, ref false in
              Hid.replace ce r (e::rl,Sid.union rs es,rb)) m;
  let rec visit (l,s,b) acc =
    if !b then acc
    else
      begin
        b := true;
Andrei Paskevich's avatar
Andrei Paskevich committed
66 67
        let acc = Sid.fold (fun e acc ->
                              try
68 69 70 71 72
                                visit (Hid.find ce e) acc
                              with Not_found -> acc) s acc in
        l::acc
      end
  in
Francois Bobot's avatar
Francois Bobot committed
73
  List.rev (Hid.fold (fun _ -> visit) ce [])
74 75 76



Andrei Paskevich's avatar
Andrei Paskevich committed
77
let elt d =
78
  match d.d_node with
Andrei Paskevich's avatar
Andrei Paskevich committed
79
    | Dlogic l ->
80
        let mem = Hid.create 16 in
81
        List.iter (fun a -> Hid.add mem (fst a).ls_name a) l;
Francois Bobot's avatar
Francois Bobot committed
82
        let tyoccurences acc _ = acc in
Andrei Paskevich's avatar
Andrei Paskevich committed
83
        let loccurences acc ls =
84
          if Hid.mem mem ls.ls_name then Sid.add ls.ls_name acc else acc in
Andrei Paskevich's avatar
Andrei Paskevich committed
85
        let m = List.fold_left
86
          (fun acc (ls,ld) ->
87
                 let fd = ls_defn_axiom ld in
88
                 let s = t_s_fold tyoccurences loccurences Sid.empty fd in
89
                 Mid.add ls.ls_name s acc) Mid.empty l in
90 91 92
        let l = connexe m in
        List.map (fun e -> create_logic_decl (List.map (Hid.find mem) e)) l
    | Ddata l ->
93 94
        let mem = Hid.create 16 in
        List.iter (fun ((ts,_) as a) -> Hid.add mem ts.ts_name a) l;
Andrei Paskevich's avatar
Andrei Paskevich committed
95
        let tyoccurences acc ts =
96 97
          if Hid.mem mem ts.ts_name then Sid.add ts.ts_name acc else acc
        in
Andrei Paskevich's avatar
Andrei Paskevich committed
98
        let m = List.fold_left
99 100
          (fun m (ts,l) ->
             let s =
Andrei Paskevich's avatar
Andrei Paskevich committed
101
                   List.fold_left
102
                     (fun acc ({ls_args = tyl; ls_value = ty},_) ->
103
                        let ty = of_option ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
104 105
                        List.fold_left
                          (fun acc ty -> ty_s_fold tyoccurences acc ty)
106
                          acc (ty::tyl)
Andrei Paskevich's avatar
Andrei Paskevich committed
107
                     ) Sid.empty l
108
             in
Andrei Paskevich's avatar
Andrei Paskevich committed
109
             Mid.add ts.ts_name s m) Mid.empty l
110
        in
111
        let l = connexe m in
112
        List.map (fun e -> create_data_decl (List.map (Hid.find mem) e)) l
113
    | Dind _ -> [d] (* TODO *)
114
    | Dtype _ | Dparam _ | Dprop _ -> [d]
115

116
let t = Trans.decl elt None
117

118
let () = Trans.register_transform "simplify_recursive_definition" t
119
  ~desc:"Separate@ the@ definitions@ that@ are@ not@ really@ recursive."