varcontext.ml 6.23 KB
Newer Older
1 2 3 4
open Printf
exception Var_already_defined
exception Var_undefined of string

5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44
module type VARCONTEXT =
  functor (Vars : sig type var_t type array_t val cell2var : array_t -> int list -> var_t end) ->
sig
  type var_t = Vars.var_t
  type arr_t = Vars.array_t
  type t =
    {
      index2var : (int,var_t) Hashtbl.t;
      var2index : (var_t,int) Hashtbl.t;

      index2array : (int,arr_t) Hashtbl.t;
      array2index : (arr_t,int) Hashtbl.t;

      cells2vars : (int * int list, int) Hashtbl.t;

      mutable nextVarIndex : int;
      mutable nextArrayIndex : int;
    }

  val create : unit -> t

  val index_of_var : t -> var_t -> int
  val var_of_index : t -> int -> var_t
  val mem : t -> var_t -> bool

  val index_of_array : t -> arr_t -> int
  val array_of_index : t -> int -> arr_t
  val arraymem : t -> arr_t -> bool

  (* array index -> indices -> corresponding var index *)
  val index_of_cell : t -> int -> int list -> int

  val add : t -> var_t -> int
  val add_array : t -> arr_t -> unit
  val add_cell : t -> arr_t -> int list -> int

  val size : t -> int
  val iter : t -> (var_t -> int -> unit) -> unit
end

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 81 82 83 84 85
(**
 * a custom type to store array cells
 *)
module ArrayCell =
struct
  type arr = Leaf of int array | Node of arr array

  let rec make_array = function
    | [] -> failwith "an array cannot be empty"
    | [n] -> Leaf (Array.make n 0)
    | n::l -> Node (Array.init n (fun _ -> make_array l))
  
  let rec get_leaf = function
    | Leaf a -> begin function
      | [n] -> a.(n)
      | _ -> failwith "wrong array dimension"
    end
    | Node a -> begin function
      | n::l -> get_leaf a.(n) l
      | _ -> failwith "wrong array dimension"
    end

  let rec set_leaf value = function
    | Leaf a -> begin function
      | [n] -> a.(n) <- value
      | _ -> failwith "wrong array dimension"
    end
    | Node a -> begin function
      | n::l -> set_leaf value a.(n) l
      | _ -> failwith "wrong array dimension"
    end

  let rec _get_cells = function
    | Leaf a -> Array.to_list a
    | Node a -> Array.fold_left (fun acc x -> acc @ (_get_cells x)) [] a

  let get_cells x =
    List.sort Pervasives.compare (_get_cells x)

end

86
module VarContextFunctor =
87 88 89 90 91 92 93 94 95 96 97 98 99
  functor (Vars : sig type var_t type array_t val cell2var : array_t -> int list -> var_t end) ->
struct
  type var_t = Vars.var_t
  type arr_t = Vars.array_t
  
  type t =
    {
      index2var : (int,var_t) Hashtbl.t;
      var2index : (var_t,int) Hashtbl.t;

      index2array : (int,arr_t) Hashtbl.t;
      array2index : (arr_t,int) Hashtbl.t;

100
      mutable cells2vars : ArrayCell.arr array;
101 102 103 104 105 106 107 108 109 110 111 112 113

      mutable nextVarIndex : int;
      mutable nextArrayIndex : int;
    }

  let create () =
    {
      index2var = Hashtbl.create 16;
      var2index = Hashtbl.create 16;

      index2array = Hashtbl.create 16;
      array2index = Hashtbl.create 16;

114
      cells2vars = [||];
115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134

      nextVarIndex = 0;
      nextArrayIndex = 0;
    }

  let index_of_var vc var =
    Hashtbl.find vc.var2index var
  let var_of_index vc ind =
    Hashtbl.find vc.index2var ind
  let mem vc var =
    Hashtbl.mem vc.var2index var

  let index_of_array vc arr =
    Hashtbl.find vc.array2index arr
  let array_of_index vc ind =
    Hashtbl.find vc.index2array ind
  let arraymem vc arr =
    Hashtbl.mem vc.array2index arr

  let index_of_cell vc arrayId indices =
135
    ArrayCell.get_leaf vc.cells2vars.(arrayId) indices
136 137 138 139 140 141 142 143 144 145 146

  let add vc varName =
    if (Hashtbl.mem vc.var2index varName) then (
      raise Var_already_defined
    );
    let index = vc.nextVarIndex in
    vc.nextVarIndex <- vc.nextVarIndex + 1;
    Hashtbl.add vc.index2var index varName;
    Hashtbl.add vc.var2index varName index;
    index

147
  let add_array vc arrayName dims =
148 149 150 151 152 153
    if (Hashtbl.mem vc.array2index arrayName) then (
      raise Var_already_defined
    );
    let index = vc.nextArrayIndex in
    vc.nextArrayIndex <- vc.nextArrayIndex + 1;
    Hashtbl.add vc.index2array index arrayName;
154 155
    Hashtbl.add vc.array2index arrayName index;
    vc.cells2vars <- Array.append vc.cells2vars [|ArrayCell.make_array dims|]
156 157 158 159 160

  let add_cell vc arrayName indices =
    let arrayIndex = Hashtbl.find vc.array2index arrayName in
    let cellVar = Vars.cell2var arrayName indices in
    let cellIndex = add vc cellVar in
161
    ArrayCell.set_leaf cellIndex vc.cells2vars.(arrayIndex) indices;
162 163 164 165 166 167 168 169 170 171 172 173 174 175
    cellIndex

  let size vc = Hashtbl.length vc.var2index

  let iter vc f = Hashtbl.iter f vc.var2index
  
end

module StringArrayVars =
struct
  type var_t = string
  type array_t = string

  let cell2var arrayName indices =
176
    List.fold_left (fun s -> fun i -> s ^ "[" ^ (string_of_int i) ^ "]") arrayName indices
177 178 179 180 181 182 183 184 185 186
end

module VarContext = VarContextFunctor(StringArrayVars)

module ScopeStringArrayVars =
struct
  type var_t = int option * string
  type array_t = int option * string

  let cell2var (procRef,arrayName) indices =
187
    procRef, (List.fold_left (fun s -> fun i -> s ^ "[" ^ (string_of_int i) ^ "]") arrayName indices)
188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218
end

module ScopeVarContext =
struct
  include VarContextFunctor(ScopeStringArrayVars)

  (* read all elements, by prepending the process name (if any) to the
   * variable and array names
   *)
  let _prepend_procName procs s = function
    | None    -> s
    | Some i  -> procs.(i) ^ "." ^ s

  (* Convert the ScopeVarContext.t to VarContext.t, by prepending the process
   * names to variables and clocks. We just extract these elements from the
   * hash tables, along with their indices, so as to reinsert them in the
   * same order in the new VarContext. These contexts are only for pretty
   * printing and have no role in simulation.
   *)
  let to_vc : t -> string array -> VarContext.t = fun svc -> fun procs ->
    let result = VarContext.create () in
    let prep = _prepend_procName procs in
    (* Variable names *)
    let varList =
      List.sort compare
        (Hashtbl.fold (fun (p,v) index acc -> (index, prep v p)::acc) svc.var2index []) in
    List.iter (fun (_,name) -> let _ = VarContext.add result name in ()) varList;
    (* Array names *)
    let arrList =
      List.sort compare
        (Hashtbl.fold (fun (p,v) index acc -> (index, prep v p)::acc) svc.array2index []) in
219
    List.iter (fun (_,name) -> VarContext.add_array result name [0]) arrList;
220 221 222 223
    (* Do not forget the mapping from cells to vars *)
    { result with VarContext.cells2vars = svc.cells2vars }

end
224