transform.ml 5.99 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24
(**************************************************************************)
(*                                                                        *)
(*  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.                  *)
(*                                                                        *)
(**************************************************************************)

(* This module has the invariant that each type has only one tag function *)

type 'a hashconsedlist = (int * 'a) list


25 26 27 28 29 30
module type Sig =
sig
  type t
  val tag : t -> int
end

31 32
(* The datastructure for hashconsed list *)
module LH (X:Sig) = 
33
struct
34
  module L =
35
  struct
36
    type t = X.t hashconsedlist
37 38 39 40 41 42 43 44 45 46 47 48
    let equal a b = 
      match a,b with
        | [], [] -> true
        | [], _ | _, [] -> false
            (* work evenif al and bl are nil *)
        | (_,ae)::al,(_,be)::bl -> X.tag ae = X.tag be && al == bl
    let hash a = 
      match a with
        | [] -> 0
        | (_,ae)::[] -> X.tag ae
        | (_,ae)::(at,_)::_ -> Hashcons.combine (X.tag ae) at
    let tag t = function
49 50
      | [] -> []
      | (_,ae)::al -> (t,ae)::al
51 52
  end
  module LH = Hashcons.Make(L)
53 54 55 56 57
    
  type t = L.t

  let empty : t = []
  let cons e l : t = LH.hashcons ((0,e)::l)
58

59 60 61 62 63 64 65 66 67 68 69
  let to_list : t -> X.t list =
    let rec aux acc t =
      match t with
        | [] -> acc
        | (_,e)::t -> aux (e::acc) t
    in
    aux []
      
  let from_list = List.fold_left (fun t e -> cons e t) empty        

  let tag = function
70 71
    | [] -> -1
    | (t,_)::_ -> t
72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92
    
end


(* the memoisation is inside the function *)
type ('a,'b) t = { all : 'a hashconsedlist -> 'b hashconsedlist;
                   clear : unit -> unit;
                   from_list : 'a list -> 'a hashconsedlist;
                   to_list : 'b hashconsedlist -> 'b list;
                   clear_to_list : unit -> unit}


let compose f g = {all = (fun x -> g.all (f.all x));
                   clear = (fun () -> f.clear (); g.clear ());
                   from_list = f.from_list;
                   to_list = g.to_list;
                   clear_to_list = g.clear_to_list}

let apply f x = f.to_list (f.all (f.from_list x))
    
let clear f = f.clear ();f.clear_to_list ()
93

94 95 96 97 98 99
let memo f tag h x =
  try Hashtbl.find h (tag x:int)
  with Not_found -> 
    let r = f x in
    Hashtbl.add h (tag x) r;
    r
100 101


102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131
module type S =
sig
  type elt1
  type elt2

  val all : (elt1 list -> elt2 list) -> (elt1,elt2) t
  val fold_map_right : ('a -> elt1 -> ('a * elt2 list)) -> 'a -> (elt1,elt2) t
  val fold_map_left : ('a -> elt1 -> ('a * elt2 list)) -> 'a -> (elt1,elt2) t
  val elt : (elt1 -> elt2 list) -> (elt1,elt2) t
end

module Make (X1 : Sig) (X2 : Sig) =
struct
  type elt1 = X1.t
  type elt2 = X2.t

  module LH1 = LH(X1)
  module LH2 = LH(X2)

  let memo_to_list2 h : X2.t hashconsedlist -> X2.t list = 
    memo LH2.to_list LH2.tag h

  let t all clear = 
    let h_to_list = Hashtbl.create 16 in
    {all = all;
     clear = clear;
     from_list = LH1.from_list;
     to_list = memo_to_list2 h_to_list;
     clear_to_list = (fun () -> Hashtbl.clear h_to_list)
    } 
132 133 134 135 136 137 138

  let fold_map_left f_fold v_empty =
    let memo_t = Hashtbl.create 64 in
    let rewind edonev eltss = 
      let edone,_ = List.fold_left 
        (fun (edone,v) (tag,elts) -> 
           let v,l = f_fold v elts in
139
           let edone = List.fold_left (fun e t -> LH2.cons t e) edone l in
140 141 142 143 144
           Hashtbl.add memo_t tag (edone,v);
           (edone,v)) edonev eltss in
      edone in
    let rec f acc t1 = 
      match t1 with
145
        | [] -> rewind (LH2.empty,v_empty) acc
146 147 148 149 150 151
        | (tag,e)::t2 -> 
            try 
              let edonev = Hashtbl.find memo_t tag in
              rewind edonev acc
            with Not_found -> f ((tag,e)::acc) t2 
    in
152
    t (f []) (fun () -> Hashtbl.clear memo_t)
153 154 155

  let elt f_elt = 
    let memo_elt = Hashtbl.create 64 in
156
    let f_elt () x = (),memo f_elt X1.tag memo_elt x in
157 158 159 160 161 162
    let f = fold_map_left f_elt () in
    {f with clear = fun () -> Hashtbl.clear memo_elt; f.clear ()}

  let fold_map_right f_fold v_empty =
    let rec f (acc,v) t = 
      match t with
163
        | [] -> List.fold_left (List.fold_left (fun t e -> LH2.cons e t)) LH2.empty acc
164 165 166 167
        | (_,e)::t -> 
            let v,res = f_fold v e in
            f (res::acc,v) t in
    let memo_t = Hashtbl.create 16 in
168
    t (memo (f ([],v_empty)) LH1.tag memo_t) (fun () -> Hashtbl.clear memo_t)
169 170

  let all f =
171
    let f x = LH2.from_list (f (LH1.to_list x)) in
172
    let memo_t = Hashtbl.create 16 in
173
    t (memo f LH1.tag memo_t) (fun () -> Hashtbl.clear memo_t)
174 175 176 177 178 179 180 181 182 183 184 185
end

open Term
open Ty
open Theory

module SDecl =
  struct
    type t = decl
    let tag x = x.d_tag
  end

186
module TDecl = Make(SDecl)(SDecl)
187 188 189 190 191 192 193 194 195

module SDecl_or_Use =
  struct
    type t = decl_or_use
    let tag = function
      | Decl d -> -d.d_tag
      | Use t -> 1+t.th_name.Ident.id_tag 
  end

196 197 198 199 200 201 202 203 204 205 206
module TDecl_or_Use = Make(SDecl_or_Use)(SDecl_or_Use)

module STheory =
  struct
    type t = theory
    let tag t = t.th_name.Ident.id_tag 
  end

module TTheory = Make(STheory)(STheory)

module TTheory_Decl = Make(STheory)(SDecl)