Changeset 1297


Ignore:
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:
3 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightLabelling.ml

    r1291 r1297  
    162162  let cost_prefix = CostLabel.Atom.Gen.fresh_prefix labs "_cost" in
    163163  let cost_universe = CostLabel.Atom.Gen.new_universe cost_prefix in
    164         let ind = CostLabel.Indexing.empty in
     164        let ind = CostLabel.id_indexing 0 in
    165165  {
    166166    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

    r1291 r1297  
    1717let sexpr_id = Sexpr(1, 0)
    1818
    19 let sexpr_of i l = snd (List.find (function (j, _) -> j = i) l)
     19type index = int
    2020
    21 (** not using Map as insertion order matters *)
    22 module Indexing =
    23         struct
    24                 type t = (Index.t * sexpr) list
    25                 let compare = compare (* built-in lexicographic order *)
    26                 let empty = []
    27         end
     21type indexing = sexpr array
     22
     23let sexpr_of i l =
     24    try
     25        l.(i)
     26    with
     27        | Invalid_argument _ -> invalid_arg("costLabel.sexpr_of")
     28
     29let id_indexing n = Array.make n sexpr_id
    2830
    2931(* a*_+b is composed with c*_+d by substitution: *)
     
    3234    Sexpr (a * c, b * c + d)
    3335
    34 (* i|-->e ° j|-->f = j|-->e°f   if i=j,  j|-->f otherwise *)
    35 (* NB: if simple expressions are changed to more complex ones,*)
    36 (* this must change *)
    37 let compose_index_singl i1 s1 (i2,s2) =
    38     (i2, if i1 = i2 then compose_sexpr s1 s2 else s2)
     36(* i|-->e ° I *)
     37let compose_index i s l =
     38  try
     39                l.(i) <- compose_sexpr s l.(i)
     40        with
     41                | Not_found -> ()
    3942
    40 (* i|-->e ° I *)
    41 let compose_index i s = List.map (compose_index_singl i s)
    4243
    4344(* I°J applies every mapping in I to every mapping in J *)
    44 (* TODO: can we use the shape indexings have in actual usage? *)
    45 let compose_indexing = List.fold_right (function (i,s) -> compose_index i s)
     45let compose_indexing m n =
     46        let f i a = compose_index i a n in
     47        Array.iteri f m
    4648
    4749
    48 module IndexingSet = Set.Make(Indexing)
     50module IndexingSet = Set.Make(struct
     51    type t = indexing
     52                let compare = compare
     53        end)
    4954
    5055
    5156type t = {
    5257    name : Atom.t;
    53     i : Indexing.t
     58    i : indexing
    5459}
     60
    5561
    5662(* if [pretty] is false then a name suitable for labels is given*)
     
    5864let string_of_sexpr pretty id (Sexpr(a, b)) =
    5965        let plus = if pretty then "+" else "P" in
    60   let a_id_s = if a = 1 then id else string_of_int a^id in
     66  let a_id_s = if a = 1 then id else string_of_int a ^ id in
    6167        let b_s = string_of_int b in
    6268        if a = 0 then b_s else
    63         if b = 0 then a_id_s else a_id_s^plus^b_s
     69        if b = 0 then a_id_s else a_id_s ^ plus ^ b_s
    6470       
    6571(* examples:*)
    66 (* [pretty] true:  (0,i+1,2j+2)*)
    67 (* [pretty] false: _0_iP1_2jP2 *)
    68 let string_of_indexing pretty = function
    69         | [] -> ""
    70         | (i, s) :: l ->
    71                 (* !!! assuming i starts with '_' which can be omitted !!! *)
    72                 let i = String.sub i 1 (String.length i) in
    73                 let left = if pretty then "(" else "_" in
    74                 let right = if pretty then ")" else "" in
    75                 let sep = if pretty then "," else "_" in
    76                 let first = string_of_sexpr pretty i s in
    77                 let f accu (j, t) = accu ^ sep ^ (string_of_sexpr pretty j t) in
    78                 left ^ List.fold_left f first l ^ right
     72(* [pretty] true:  (0,i1+1,2i2+2)*)
     73(* [pretty] false: _0_i1P1_2i2P2 *)
     74let string_of_indexing pretty prefix m =
     75        if Array.length m = 0 then "" else
     76        let buff = Buffer.create 16 in
     77  Buffer.add_char buff (if pretty then '(' else '_');
     78        let sep = if pretty then ',' else '_' in
     79        let f i a =
     80                if i > 0 then Buffer.add_char buff sep;
     81                let str = string_of_sexpr pretty (prefix ^ string_of_int i) a in
     82                Buffer.add_string buff str in
     83        Array.iteri f m;
     84        Buffer.contents buff
    7985               
    8086let string_of_cost_label ?(pretty = false) lab =
    81         lab.name ^ string_of_indexing pretty lab.i
     87        lab.name ^ string_of_indexing pretty "i" lab.i
    8288
    8389let fresh l universe =
  • Deliverables/D2.2/8051-indexed-labels-branch/src/common/costLabel.mli

    r1291 r1297  
    88end
    99
    10 (** Loop indices, to be identified with Clight identifiers *)
    11 module Index : sig
    12         include StringSig.S
    13 end
    14 
    15 (** Simple expressions corresponding to loop tranformations. *)
     10(** Simple expressions corresponding to loop tranformations.
     11    TODO: leave it abstract or not? *)
    1612type sexpr
    1713
    1814val sexpr_id : sexpr
    1915
    20 module Indexing : sig
    21         include Set.OrderedType
    22         val empty : t
    23 end
     16(* trying a nameless approach *)
     17type index = int
    2418
    25 (** [sexpr_of i l] extracts the simple expression relative to [i] in [l].
    26     It raises an [Invalid_argument] exception if [i] is not handled by [l] *)
    27 val sexpr_of : Index.t -> Indexing.t -> sexpr
     19type indexing = sexpr array
     20
     21(** [id_indexing n] generates an identity indexing nested in [n] loops *)
     22val id_indexing : int -> indexing
    2823
    2924(** [compose_index i s l] applies the transformation [i] |--> [s] to [l] *)
    30 val compose_index : Index.t -> sexpr -> Indexing.t -> Indexing.t
     25val compose_index : index -> sexpr -> indexing -> unit
    3126
    3227(** [compose_index l m] applies all the transformations in  [l] to [m] *)
    33 val compose_indexing : Indexing.t -> Indexing.t -> Indexing.t
     28val compose_indexing : indexing -> indexing -> unit
    3429
    35 module IndexingSet : Set.S with type elt = Indexing.t
     30module IndexingSet : Set.S with type elt = indexing
    3631
    3732type t = {
    3833        name : Atom.t;
    39         i : Indexing.t
     34        i : indexing
    4035}
    4136
    42 (** [string_of_cost_label t] converts an indexed label to a
    43     string suitable for a label name in source.
     37(** [string_of_cost_label pref t] converts an indexed label to a
     38    string suitable for a label name in source
    4439                [string_of_cost_label ~pretty:true t] prints a more readable form *)
    4540val string_of_cost_label : ?pretty : bool -> t -> string
     
    4742(** [fresh i u] creates a fresh label using [u] as name universe, inside
    4843    the indexing [i] (which represents the nested loops containing the label) *)
    49 val fresh : Indexing.t -> Atom.Gen.universe -> t
     44val fresh : indexing -> Atom.Gen.universe -> t
    5045
    5146module Set : Set.S with type elt = t
Note: See TracChangeset for help on using the changeset viewer.