simplify_recursive_definition.ml 4.64 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
MARCHE Claude's avatar
MARCHE Claude committed
3
(*  Copyright (C) 2010-2012                                               *)
4 5 6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
MARCHE Claude's avatar
MARCHE Claude committed
7
(*    Guillaume Melquiond                                                 *)
8 9 10 11 12 13 14 15 16 17 18 19 20
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

21
open Util
22 23 24
open Ident
open Ty
open Term
Andrei Paskevich's avatar
Andrei Paskevich committed
25
open Decl
26 27 28 29 30 31

type seen =
  | SNot
  | SOnce
  | SBack

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



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

125
let t = Trans.decl elt None
126

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