source: Deliverables/D2.2/8051/src/common/costLabel.ml @ 1585

Last change on this file since 1585 was 1585, checked in by tranquil, 8 years ago

fighting with a bug of the translation from RTL to ERTL

File size: 4.6 KB
Line 
1module Atom =
2  struct
3    include StringTools
4  end
5
6module StringMap = Map.Make(String)
7
8(** Simple expressions are for now affine maps of the form a*_+b *)
9type sexpr =
10    | Sexpr of int*int
11
12let is_const_sexpr (Sexpr(a, _)) = (a = 0)
13
14let sexpr_id = Sexpr(1, 0)
15
16let const_sexpr n = Sexpr(0, n)
17
18type index = int
19
20let make_id prefix depth = prefix ^ string_of_int depth
21
22type indexing = sexpr list
23
24type const_indexing = int ExtArray.t
25
26let const_ind_iter = ExtArray.iter
27
28let curr_const_ind = function
29    | hd :: _ -> hd
30    | _ -> invalid_arg "curr_const_ind applied to non-empty list"
31
32let init_const_indexing () = ExtArray.make ~buff:1 0 0 
33
34let enter_loop_single indexing n = ExtArray.set indexing n 0
35
36let continue_loop_single indexing n =
37  try
38    ExtArray.set indexing n (ExtArray.get indexing n + 1)
39  with | _ ->
40    invalid_arg "uninitialized loop index" 
41
42let curr_ind = function
43    | hd :: _ -> hd
44    | _ -> invalid_arg "empty indexing stack"
45
46let enter_loop inds = enter_loop_single (curr_ind inds)
47
48let continue_loop inds = continue_loop_single (curr_ind inds)
49
50let enter_loop_opt indexing = Option.iter (enter_loop indexing) 
51
52let continue_loop_opt indexing = Option.iter (continue_loop indexing)
53
54let new_const_ind inds = init_const_indexing () :: inds
55
56let forget_const_ind = function
57        | _ :: inds -> inds
58        | _ -> invalid_arg "empty indexing stack"
59
60let sexpr_of i l = 
61    try
62        List.nth l i
63    with
64                        | Failure _
65      | Invalid_argument _ -> invalid_arg "costLabel.sexpr_of"
66
67let empty_indexing = []
68
69let add_id_indexing ind = sexpr_id :: ind
70
71(* a*_+b is composed with c*_+d by substitution: *)
72(* namely a*_+b ° c*_+d = c*(a*_+b)+d              *)
73let compose_sexpr (Sexpr(a, b)) (Sexpr(c, d)) =
74    Sexpr (a * c, b * c + d)
75               
76let ev_sexpr i (Sexpr(a, b)) = a*i+b
77
78(* i|-->e ° I *)
79let rec compose_index_indexing i s l = match i, l with
80        | 0, s' :: l' -> compose_sexpr s s' :: l'
81        | x, s' :: l' -> s' :: compose_index_indexing (i-1) s l'
82        | _ -> l
83
84
85(* I°J applies every mapping in I to every mapping in J *)
86let rec compose_indexing m n = match m, n with
87        | s1 :: l1, s2 :: l2 -> compose_sexpr s1 s2 :: compose_indexing l1 l2
88        | _ -> n 
89
90let rec compose_const_indexing_i i c = function
91        | [] -> []
92        | s :: l ->
93                let head =
94                        (* if s is constant leave it be. In particular, avoid raising the error *)
95                        if is_const_sexpr s then s else
96                        try
97                          const_sexpr (ev_sexpr (ExtArray.get c i) s) 
98                        with
99                                | Invalid_argument _ ->
100                                        invalid_arg "constant indexing not enough to be applied" in
101          head :: compose_const_indexing_i (i+1) c l
102
103module IndexingSet = Set.Make(struct
104    type t = indexing
105                let compare = compare
106        end)
107
108type t = {
109    name : Atom.t;
110    i : indexing
111}
112
113let comp_index i s lbl =
114        {lbl with i = compose_index_indexing i s lbl.i}
115
116let ev_indexing c lbl =
117    {lbl with i = compose_const_indexing_i 0 c lbl.i}
118
119
120(* if [pretty] is false then a name suitable for labels is given*)
121(* ('P' replaces '+') *)
122let string_of_sexpr pretty prefix i (Sexpr(a, b)) =
123        let plus = if pretty then "+" else "P" in
124        let id = prefix ^ string_of_int i in
125  let a_id_s = if a = 1 then id else string_of_int a ^ id in
126        let b_s = string_of_int b in
127        if a = 0 then b_s else
128        if b = 0 then a_id_s else a_id_s ^ plus ^ b_s
129       
130(* examples:*)
131(* [pretty] true:  (0,i1+1,2i2+2)*)
132(* [pretty] false: _0_i1P1_2i2P2 *)
133let rec string_of_indexing_tl pretty prefix i = function
134        | [] -> if pretty then ")" else ""
135        | hd :: tl ->
136                let sep = if pretty then "," else "_" in
137                let str = string_of_sexpr pretty prefix i hd in
138                sep ^ str ^ string_of_indexing_tl pretty prefix (i+1) tl
139
140let string_of_indexing pretty prefix = function
141        | [] -> ""
142        | hd :: tl ->
143                let start = if pretty then "(" else "_" in
144    let str = string_of_sexpr pretty prefix 0 hd in
145                start ^ str ^ string_of_indexing_tl pretty prefix 1 tl
146               
147let string_of_cost_label ?(pretty = false) lab =
148        lab.name ^ string_of_indexing pretty "i" lab.i
149
150let fresh l universe =
151        {name = Atom.Gen.fresh universe; i = l} 
152
153(* TODO: urgh. Necessary? *)
154type aux_t = t
155                                                       
156(** labels are endowed with a lexicographical ordering *)
157module T : Map.OrderedType with type t = aux_t =
158    struct
159        type t = aux_t
160        let compare = compare (* uses the built-in lexicographical comparison *) 
161    end
162
163module Map = Map.Make(T)   
164module Set = Set.Make(T) 
165(** [constant_map d x] produces a finite map which associates
166    [x] to every element of the set [d]. *)
167
168let indexings_of atom s =
169        let f k accu = if k.name = atom then IndexingSet.add k.i accu else accu in
170        Set.fold f s IndexingSet.empty
171
172let constant_map d x = 
173  Set.fold (fun k accu -> Map.add k x accu) d Map.empty
Note: See TracBrowser for help on using the repository browser.