simplify_recursive_definition.ml 4.83 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    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.                  *)
(*                                                                        *)
(**************************************************************************)

20
open Util
21 22 23
open Ident
open Ty
open Term
Andrei Paskevich's avatar
Andrei Paskevich committed
24
open Decl
25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80

type seen =
  | SNot
  | SOnce
  | SBack

let rec find h e = 
  try
    let r = Hid.find h e in
    if r == e then e 
    else 
      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)

let connexe (m:Sid.t Mid.t)  = 
  let uf = Hid.create 32 in
  let visited = Hid.create 32 in
  Mid.iter (fun e _ -> Hid.replace visited e SNot) m;
  let rec visit i last = 
    match Hid.find visited i with
      | SNot -> 
          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
      | SOnce ->  
          (try 
             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
  Mid.iter (fun e es -> 
              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;
        let acc = Sid.fold (fun e acc -> 
                              try 
                                visit (Hid.find ce e) acc
                              with Not_found -> acc) s acc in
        l::acc
      end
  in
Francois Bobot's avatar
Francois Bobot committed
81
  List.rev (Hid.fold (fun _ -> visit) ce [])
82 83 84 85 86 87 88



let elt d = 
  match d.d_node with
    | Dlogic l -> 
        let mem = Hid.create 16 in
89
        List.iter (fun a -> Hid.add mem (fst a).ls_name a) l;
Francois Bobot's avatar
Francois Bobot committed
90
        let tyoccurences acc _ = acc in
91 92
        let loccurences acc ls = 
          if Hid.mem mem ls.ls_name then Sid.add ls.ls_name acc else acc in
93
        let m = List.fold_left 
94 95 96 97 98 99
          (fun acc (ls,ld) -> match ld with 
             | None -> Mid.add ls.ls_name Sid.empty acc
             | Some ld -> 
                 let fd = ls_defn_axiom ld in
                 let s = f_s_fold tyoccurences loccurences Sid.empty fd in
                 Mid.add ls.ls_name s acc) Mid.empty l in
100
          let l = connexe m in
101
          List.map (fun e -> create_logic_decl (List.map (Hid.find mem) e)) l
102
    | Dtype l ->
103 104
        let mem = Hid.create 16 in
        List.iter (fun ((ts,_) as a) -> Hid.add mem ts.ts_name a) l;
105 106 107
        let tyoccurences acc ts = 
	  if Hid.mem mem ts.ts_name then Sid.add ts.ts_name acc else acc
	in
108
        let m = List.fold_left 
109
          (fun m (ts,def) -> 
110 111 112 113
             let s = match def with
               | Tabstract -> 
                   begin match ts.ts_def with
                     | None -> Sid.empty
114
                     | Some ty -> ty_s_fold tyoccurences Sid.empty ty
115 116 117
                   end
               | Talgebraic l -> 
                   List.fold_left 
118 119
                     (fun acc {ls_args = tyl; ls_value = ty} ->
                        let ty = of_option ty in
120
                        List.fold_left 
121 122 123 124 125 126
                          (fun acc ty -> ty_s_fold tyoccurences acc ty) 
			  acc (ty::tyl)
                     ) Sid.empty l 
	     in
             Mid.add ts.ts_name s m) Mid.empty l 
	in
127
        let l = connexe m in
128 129
        List.map (fun e -> create_ty_decl (List.map (Hid.find mem) e)) l
    | Dind _ -> [d] (* TODO *)
Andrei Paskevich's avatar
Andrei Paskevich committed
130
    | Dprop _ -> [d]
131

Francois Bobot's avatar
Francois Bobot committed
132
let t = Register.store (fun () -> Trans.decl elt None)
133

134
let () = Register.register_transform "simplify_recursive_definition" t