Changeset 1297 for Deliverables/D2.2
- Timestamp:
- Oct 5, 2011, 6:04:47 PM (9 years ago)
- 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 162 162 let cost_prefix = CostLabel.Atom.Gen.fresh_prefix labs "_cost" in 163 163 let cost_universe = CostLabel.Atom.Gen.new_universe cost_prefix in 164 let ind = CostLabel. Indexing.emptyin164 let ind = CostLabel.id_indexing 0 in 165 165 { 166 166 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 17 17 let sexpr_id = Sexpr(1, 0) 18 18 19 let sexpr_of i l = snd (List.find (function (j, _) -> j = i) l) 19 type index = int 20 20 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 21 type indexing = sexpr array 22 23 let sexpr_of i l = 24 try 25 l.(i) 26 with 27 | Invalid_argument _ -> invalid_arg("costLabel.sexpr_of") 28 29 let id_indexing n = Array.make n sexpr_id 28 30 29 31 (* a*_+b is composed with c*_+d by substitution: *) … … 32 34 Sexpr (a * c, b * c + d) 33 35 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 *) 37 let compose_index i s l = 38 try 39 l.(i) <- compose_sexpr s l.(i) 40 with 41 | Not_found -> () 39 42 40 (* i|-->e ° I *)41 let compose_index i s = List.map (compose_index_singl i s)42 43 43 44 (* 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) 45 let compose_indexing m n = 46 let f i a = compose_index i a n in 47 Array.iteri f m 46 48 47 49 48 module IndexingSet = Set.Make(Indexing) 50 module IndexingSet = Set.Make(struct 51 type t = indexing 52 let compare = compare 53 end) 49 54 50 55 51 56 type t = { 52 57 name : Atom.t; 53 i : Indexing.t58 i : indexing 54 59 } 60 55 61 56 62 (* if [pretty] is false then a name suitable for labels is given*) … … 58 64 let string_of_sexpr pretty id (Sexpr(a, b)) = 59 65 let plus = if pretty then "+" else "P" in 60 let a_id_s = if a = 1 then id else string_of_int a ^id in66 let a_id_s = if a = 1 then id else string_of_int a ^ id in 61 67 let b_s = string_of_int b in 62 68 if a = 0 then b_s else 63 if b = 0 then a_id_s else a_id_s ^plus^b_s69 if b = 0 then a_id_s else a_id_s ^ plus ^ b_s 64 70 65 71 (* examples:*) 66 (* [pretty] true: (0,i +1,2j+2)*)67 (* [pretty] false: _0_i P1_2jP2 *)68 let string_of_indexing pretty = function69 | [] -> ""70 | (i, s) :: l ->71 (* !!! assuming i starts with '_' which can be omitted !!! *) 72 let i = String.sub i 1 (String.length i)in73 let left = if pretty then "(" else "_" in74 let right = if pretty then ")" else "" in75 let s ep = if pretty then "," else "_"in76 let first = string_of_sexpr pretty i sin77 let f accu (j, t) = accu ^ sep ^ (string_of_sexpr pretty j t) in78 left ^ List.fold_left f first l ^ right72 (* [pretty] true: (0,i1+1,2i2+2)*) 73 (* [pretty] false: _0_i1P1_2i2P2 *) 74 let 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 79 85 80 86 let string_of_cost_label ?(pretty = false) lab = 81 lab.name ^ string_of_indexing pretty lab.i87 lab.name ^ string_of_indexing pretty "i" lab.i 82 88 83 89 let fresh l universe = -
Deliverables/D2.2/8051-indexed-labels-branch/src/common/costLabel.mli
r1291 r1297 8 8 end 9 9 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? *) 16 12 type sexpr 17 13 18 14 val sexpr_id : sexpr 19 15 20 module Indexing : sig 21 include Set.OrderedType 22 val empty : t 23 end 16 (* trying a nameless approach *) 17 type index = int 24 18 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 19 type indexing = sexpr array 20 21 (** [id_indexing n] generates an identity indexing nested in [n] loops *) 22 val id_indexing : int -> indexing 28 23 29 24 (** [compose_index i s l] applies the transformation [i] |--> [s] to [l] *) 30 val compose_index : Index.t -> sexpr -> Indexing.t -> Indexing.t25 val compose_index : index -> sexpr -> indexing -> unit 31 26 32 27 (** [compose_index l m] applies all the transformations in [l] to [m] *) 33 val compose_indexing : Indexing.t -> Indexing.t -> Indexing.t28 val compose_indexing : indexing -> indexing -> unit 34 29 35 module IndexingSet : Set.S with type elt = Indexing.t30 module IndexingSet : Set.S with type elt = indexing 36 31 37 32 type t = { 38 33 name : Atom.t; 39 i : Indexing.t34 i : indexing 40 35 } 41 36 42 (** [string_of_cost_label t] converts an indexed label to a43 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 44 39 [string_of_cost_label ~pretty:true t] prints a more readable form *) 45 40 val string_of_cost_label : ?pretty : bool -> t -> string … … 47 42 (** [fresh i u] creates a fresh label using [u] as name universe, inside 48 43 the indexing [i] (which represents the nested loops containing the label) *) 49 val fresh : Indexing.t-> Atom.Gen.universe -> t44 val fresh : indexing -> Atom.Gen.universe -> t 50 45 51 46 module Set : Set.S with type elt = t
Note: See TracChangeset
for help on using the changeset viewer.