source: Deliverables/D2.2/8051-indexed-labels-branch/src/common/costLabel.ml @ 1305

Last change on this file since 1305 was 1305, checked in by tranquil, 9 years ago

added indexes to loop constructors. Branch does not compile atm

File size: 2.7 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 sexpr_id = Sexpr(1, 0)
13
14type index = int
15
16let make_id prefix depth = prefix ^ string_of_int depth
17
18type indexing = sexpr array
19
20let sexpr_of i l = 
21    try
22        l.(i)
23    with
24        | Invalid_argument _ -> invalid_arg("costLabel.sexpr_of")
25
26let id_indexing n = Array.make n sexpr_id
27
28(* a*_+b is composed with c*_+d by substitution: *)
29(* namely a*_+b ° c*_+d = c*(a*_+b)+d              *)
30let compose_sexpr (Sexpr(a, b)) (Sexpr(c, d)) =
31    Sexpr (a * c, b * c + d)
32
33(* i|-->e ° I *)
34let compose_index i s l = 
35  try
36                l.(i) <- compose_sexpr s l.(i)
37        with
38                | Not_found -> ()
39
40
41(* I°J applies every mapping in I to every mapping in J *)
42let compose_indexing m n =
43        let f i a = compose_index i a n in
44        Array.iteri f m
45
46
47module IndexingSet = Set.Make(struct
48    type t = indexing
49                let compare = compare
50        end)
51
52
53type t = {
54    name : Atom.t;
55    i : indexing
56}
57
58
59(* if [pretty] is false then a name suitable for labels is given*)
60(* ('P' replaces '+') *)
61let string_of_sexpr pretty id (Sexpr(a, b)) =
62        let plus = if pretty then "+" else "P" in
63  let a_id_s = if a = 1 then id else string_of_int a ^ id in
64        let b_s = string_of_int b in
65        if a = 0 then b_s else
66        if b = 0 then a_id_s else a_id_s ^ plus ^ b_s
67       
68(* examples:*)
69(* [pretty] true:  (0,i1+1,2i2+2)*)
70(* [pretty] false: _0_i1P1_2i2P2 *)
71let string_of_indexing pretty prefix m = 
72        if Array.length m = 0 then "" else
73        let buff = Buffer.create 16 in
74  Buffer.add_char buff (if pretty then '(' else '_');
75        let sep = if pretty then ',' else '_' in
76        let f i a =
77                if i > 0 then Buffer.add_char buff sep;
78                let str = string_of_sexpr pretty (prefix ^ string_of_int i) a in
79                Buffer.add_string buff str in
80        Array.iteri f m;
81        Buffer.contents buff
82               
83let string_of_cost_label ?(pretty = false) lab =
84        lab.name ^ string_of_indexing pretty "i" lab.i
85
86let fresh l universe =
87        {name = Atom.Gen.fresh universe; i = l} 
88
89(* TODO: urgh. Necessary? *)
90type aux_t = t
91                                                       
92(** labels are endowed with a lexicographical ordering *)
93module T : Map.OrderedType with type t = aux_t =
94    struct
95        type t = aux_t
96        let compare = compare (* uses the built-in lexicographical comparison *) 
97    end
98
99module Map = Map.Make(T)   
100module Set = Set.Make(T) 
101(** [constant_map d x] produces a finite map which associates
102    [x] to every element of the set [d]. *)
103
104let indexings_of atom s =
105        let f k accu = if k.name = atom then IndexingSet.add k.i accu else accu in
106        Set.fold f s IndexingSet.empty
107
108let constant_map d x = 
109  Set.fold (fun k accu -> Map.add k x accu) d Map.empty
110       
111        (**  **)
Note: See TracBrowser for help on using the repository browser.