Changeset 1297 for Deliverables/D2.2

Timestamp:

Oct 5, 2011, 6:04:47 PM (8 years ago)

Author:

tranquil

Message:

changed representation of indexings to a nameless one implemented with arrays

Location:

Deliverables/D2.2/8051-indexed-labels-branch/src

Files:

• clight/clightLabelling.ml (modified) (1 diff)
• common/costLabel.ml (modified) (3 diffs)
• common/costLabel.mli (modified) (2 diffs)

Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightLabelling.ml

@@ -162 +162 @@
   let cost_prefix = CostLabel.Atom.Gen.fresh_prefix labs "_cost" in
   let cost_universe = CostLabel.Atom.Gen.new_universe cost_prefix in
-        let ind = CostLabel.Indexing.empty in
+        let ind = CostLabel.id_indexing 0 in
   {
     prog_funct = List.map (add_cost_labels_f ind cost_universe) p.prog_funct;

Deliverables/D2.2/8051-indexed-labels-branch/src/common/costLabel.ml

@@ -17 +17 @@
 let sexpr_id = Sexpr(1, 0)
 
-let sexpr_of i l = snd (List.find (function (j, _) -> j = i) l)
+type index = int
 
-(** not using Map as insertion order matters *)
-module Indexing =
-        struct
-                type t = (Index.t * sexpr) list
-                let compare = compare (* built-in lexicographic order *)
-                let empty = []
-        end
+type indexing = sexpr array
+
+let sexpr_of i l = 
+    try
+        l.(i)
+    with
+        | Invalid_argument _ -> invalid_arg("costLabel.sexpr_of")
+
+let id_indexing n = Array.make n sexpr_id
 
 (* a*_+b is composed with c*_+d by substitution: *)
@@ -32 +34 @@
     Sexpr (a * c, b * c + d)
 
-(* i|-->e ° j|-->f = j|-->e°f   if i=j,  j|-->f otherwise *)
-(* NB: if simple expressions are changed to more complex ones,*)
-(* this must change *)
-let compose_index_singl i1 s1 (i2,s2) =
-    (i2, if i1 = i2 then compose_sexpr s1 s2 else s2)
+(* i|-->e ° I *)
+let compose_index i s l = 
+  try
+                l.(i) <- compose_sexpr s l.(i)
+        with
+                | Not_found -> ()
 
-(* i|-->e ° I *)
-let compose_index i s = List.map (compose_index_singl i s)
 
 (* I°J applies every mapping in I to every mapping in J *)
-(* TODO: can we use the shape indexings have in actual usage? *)
-let compose_indexing = List.fold_right (function (i,s) -> compose_index i s)
+let compose_indexing m n =
+        let f i a = compose_index i a n in
+        Array.iteri f m
 
 
-module IndexingSet = Set.Make(Indexing)
+module IndexingSet = Set.Make(struct
+    type t = indexing
+                let compare = compare
+        end)
 
 
 type t = {
     name : Atom.t;
-    i : Indexing.t
+    i : indexing
 }
+
 
 (* if [pretty] is false then a name suitable for labels is given*)
@@ -58 +64 @@
 let string_of_sexpr pretty id (Sexpr(a, b)) =
         let plus = if pretty then "+" else "P" in
-  let a_id_s = if a = 1 then id else string_of_int a^id in
+  let a_id_s = if a = 1 then id else string_of_int a ^ id in
         let b_s = string_of_int b in
         if a = 0 then b_s else
-        if b = 0 then a_id_s else a_id_s^plus^b_s
+        if b = 0 then a_id_s else a_id_s ^ plus ^ b_s
         
 (* examples:*)
-(* [pretty] true:  (0,i+1,2j+2)*)
-(* [pretty] false: _0_iP1_2jP2 *)
-let string_of_indexing pretty = function
-        | [] -> ""
-        | (i, s) :: l ->
-                (* !!! assuming i starts with '_' which can be omitted !!! *) 
-                let i = String.sub i 1 (String.length i) in
-                let left = if pretty then "(" else "_" in
-                let right = if pretty then ")" else "" in
-                let sep = if pretty then "," else "_" in
-                let first = string_of_sexpr pretty i s in
-                let f accu (j, t) = accu ^ sep ^ (string_of_sexpr pretty j t) in
-                left ^ List.fold_left f first l ^ right
+(* [pretty] true:  (0,i1+1,2i2+2)*)
+(* [pretty] false: _0_i1P1_2i2P2 *)
+let string_of_indexing pretty prefix m = 
+        if Array.length m = 0 then "" else
+        let buff = Buffer.create 16 in
+  Buffer.add_char buff (if pretty then '(' else '_');
+        let sep = if pretty then ',' else '_' in
+        let f i a =
+                if i > 0 then Buffer.add_char buff sep;
+                let str = string_of_sexpr pretty (prefix ^ string_of_int i) a in
+                Buffer.add_string buff str in
+        Array.iteri f m;
+        Buffer.contents buff
                 
 let string_of_cost_label ?(pretty = false) lab =
-        lab.name ^ string_of_indexing pretty lab.i
+        lab.name ^ string_of_indexing pretty "i" lab.i
 
 let fresh l universe =

Deliverables/D2.2/8051-indexed-labels-branch/src/common/costLabel.mli

@@ -8 +8 @@
 end
 
-(** Loop indices, to be identified with Clight identifiers *)
-module Index : sig
-        include StringSig.S
-end
-
-(** Simple expressions corresponding to loop tranformations. *)
+(** Simple expressions corresponding to loop tranformations. 
+    TODO: leave it abstract or not? *)
 type sexpr
 
 val sexpr_id : sexpr
 
-module Indexing : sig
-        include Set.OrderedType
-        val empty : t
-end
+(* trying a nameless approach *)
+type index = int
 
-(** [sexpr_of i l] extracts the simple expression relative to [i] in [l].
-    It raises an [Invalid_argument] exception if [i] is not handled by [l] *)
-val sexpr_of : Index.t -> Indexing.t -> sexpr
+type indexing = sexpr array
+
+(** [id_indexing n] generates an identity indexing nested in [n] loops *) 
+val id_indexing : int -> indexing
 
 (** [compose_index i s l] applies the transformation [i] |--> [s] to [l] *) 
-val compose_index : Index.t -> sexpr -> Indexing.t -> Indexing.t
+val compose_index : index -> sexpr -> indexing -> unit
 
 (** [compose_index l m] applies all the transformations in  [l] to [m] *)
-val compose_indexing : Indexing.t -> Indexing.t -> Indexing.t
+val compose_indexing : indexing -> indexing -> unit
 
-module IndexingSet : Set.S with type elt = Indexing.t
+module IndexingSet : Set.S with type elt = indexing
 
 type t = {
         name : Atom.t;
-        i : Indexing.t
+        i : indexing
 }
 
-(** [string_of_cost_label t] converts an indexed label to a
-    string suitable for a label name in source. 
+(** [string_of_cost_label pref t] converts an indexed label to a
+    string suitable for a label name in source 
                 [string_of_cost_label ~pretty:true t] prints a more readable form *)
 val string_of_cost_label : ?pretty : bool -> t -> string
@@ -47 +42 @@
 (** [fresh i u] creates a fresh label using [u] as name universe, inside
     the indexing [i] (which represents the nested loops containing the label) *)
-val fresh : Indexing.t -> Atom.Gen.universe -> t
+val fresh : indexing -> Atom.Gen.universe -> t
 
 module Set : Set.S with type elt = t