simplify_recursive_definition.ml 3.89 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
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 13 14

open Ident
open Ty
open Term
Andrei Paskevich's avatar
Andrei Paskevich committed
15
open Decl
16 17 18 19 20 21

type seen =
  | SNot
  | SOnce
  | SBack

Andrei Paskevich's avatar
Andrei Paskevich committed
22
let rec find h e =
23 24
  try
    let r = Hid.find h e in
Andrei Paskevich's avatar
Andrei Paskevich committed
25 26
    if r == e then e
    else
27 28 29 30 31 32 33
      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
34
let connexe (m:Sid.t Mid.t)  =
35 36 37
  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
38
  let rec visit i last =
39
    match Hid.find visited i with
Andrei Paskevich's avatar
Andrei Paskevich committed
40
      | SNot ->
41 42 43 44 45
          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
46 47
      | SOnce ->
          (try
48 49 50 51 52 53
             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
54
  Mid.iter (fun e es ->
55 56 57 58 59 60 61 62 63 64
              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
65 66
        let acc = Sid.fold (fun e acc ->
                              try
67 68 69 70 71
                                visit (Hid.find ce e) acc
                              with Not_found -> acc) s acc in
        l::acc
      end
  in
Francois Bobot's avatar
Francois Bobot committed
72
  List.rev (Hid.fold (fun _ -> visit) ce [])
73 74 75



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

115
let t = Trans.decl elt None
116

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