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

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

changed representation of indexings to a nameless one implemented with arrays

File size: 2.7 KB
Line 
1module Atom =
2        struct
3                include StringTools
4        end
5
6module StringMap = Map.Make(String)
7
8module Index =
9        struct
10                include StringTools
11        end
12
13(** Simple expressions are for now affine maps of the form a*_+b *)
14type sexpr =
15    | Sexpr of int*int
16
17let sexpr_id = Sexpr(1, 0)
18
19type index = int
20
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
30
31(* a*_+b is composed with c*_+d by substitution: *)
32(* namely a*_+b ° c*_+d = c*(a*_+b)+d              *)
33let compose_sexpr (Sexpr(a, b)) (Sexpr(c, d)) =
34    Sexpr (a * c, b * c + d)
35
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 -> ()
42
43
44(* I°J applies every mapping in I to every mapping in J *)
45let compose_indexing m n =
46        let f i a = compose_index i a n in
47        Array.iteri f m
48
49
50module IndexingSet = Set.Make(struct
51    type t = indexing
52                let compare = compare
53        end)
54
55
56type t = {
57    name : Atom.t;
58    i : indexing
59}
60
61
62(* if [pretty] is false then a name suitable for labels is given*)
63(* ('P' replaces '+') *)
64let string_of_sexpr pretty id (Sexpr(a, b)) =
65        let plus = if pretty then "+" else "P" in
66  let a_id_s = if a = 1 then id else string_of_int a ^ id in
67        let b_s = string_of_int b in
68        if a = 0 then b_s else
69        if b = 0 then a_id_s else a_id_s ^ plus ^ b_s
70       
71(* examples:*)
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
85               
86let string_of_cost_label ?(pretty = false) lab =
87        lab.name ^ string_of_indexing pretty "i" lab.i
88
89let fresh l universe =
90        {name = Atom.Gen.fresh universe; i = l} 
91
92(* TODO: urgh. Necessary? *)
93type aux_t = t
94                                                       
95(** labels are endowed with a lexicographical ordering *)
96module T : Map.OrderedType with type t = aux_t =
97    struct
98        type t = aux_t
99        let compare = compare (* uses the built-in lexicographical comparison *) 
100    end
101
102module Map = Map.Make(T)   
103module Set = Set.Make(T) 
104(** [constant_map d x] produces a finite map which associates
105    [x] to every element of the set [d]. *)
106
107let indexings_of atom s =
108        let f k accu = if k.name = atom then IndexingSet.add k.i accu else accu in
109        Set.fold f s IndexingSet.empty
110
111let constant_map d x = 
112  Set.fold (fun k accu -> Map.add k x accu) d Map.empty
113       
114        (**  **)
Note: See TracBrowser for help on using the repository browser.