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

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

indexing branch is compiling again:

  • clight interpreter updated
  • clight labeller yet to be completed with single-entry loop detection
File size: 3.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
14let const_sexpr n = Sexpr(0, n)
15
16type index = int
17
18let make_id prefix depth = prefix ^ string_of_int depth
19
20type indexing = sexpr list
21
22type const_indexing = int array
23
24(** [enter_loop n indexing] is used to update indexing when one is entering a
25    loop indexed by [n].
26                The function recycles the same constant indexing *)
27let rec enter_loop n indexing = match n with
28        | None -> ()
29        | Some x -> indexing.(x) <- 0
30
31(** [enter_loop n indexing] is used to update indexing when one is continuing a
32    loop indexed by [n]. *)
33let rec continue_loop n indexing = match n with
34        | None -> ()
35        | Some x -> indexing.(x) <- indexing.(x) + 1
36
37let sexpr_of i l = 
38    try
39        List.nth l i
40    with
41                        | Failure _
42      | Invalid_argument _ -> invalid_arg "costLabel.sexpr_of"
43
44let empty_indexing = []
45
46let add_id_indexing ind = sexpr_id :: ind
47
48(* a*_+b is composed with c*_+d by substitution: *)
49(* namely a*_+b ° c*_+d = c*(a*_+b)+d              *)
50let compose_sexpr (Sexpr(a, b)) (Sexpr(c, d)) =
51    Sexpr (a * c, b * c + d)
52               
53let ev_sexpr i (Sexpr(a, b)) = a*i+b
54
55(* i|-->e ° I *)
56let rec compose_index i s l = match i, l with
57        | 0, s' :: l' -> compose_sexpr s s' :: l'
58        | x, s' :: l' -> compose_index (i-1) s l'
59        | _ -> l
60
61
62(* I°J applies every mapping in I to every mapping in J *)
63let rec compose_indexing m n = match m, n with
64        | s1 :: l1, s2 :: l2 -> compose_sexpr s1 s2 :: compose_indexing l1 l2
65        | _ -> n 
66
67let rec compose_const_indexing_i i c = function
68        | [] -> []
69        | s :: l ->
70                const_sexpr (ev_sexpr c.(i) s) :: compose_const_indexing_i (i+1) c l
71
72module IndexingSet = Set.Make(struct
73    type t = indexing
74                let compare = compare
75        end)
76
77type t = {
78    name : Atom.t;
79    i : indexing
80}
81
82let apply_const_indexing c lbl =
83    {lbl with i = compose_const_indexing_i 0 c lbl.i}
84
85
86(* if [pretty] is false then a name suitable for labels is given*)
87(* ('P' replaces '+') *)
88let string_of_sexpr pretty prefix i (Sexpr(a, b)) =
89        let plus = if pretty then "+" else "P" in
90        let id = prefix ^ string_of_int i in
91  let a_id_s = if a = 1 then id else string_of_int a ^ id in
92        let b_s = string_of_int b in
93        if a = 0 then b_s else
94        if b = 0 then a_id_s else a_id_s ^ plus ^ b_s
95       
96(* examples:*)
97(* [pretty] true:  (0,i1+1,2i2+2)*)
98(* [pretty] false: _0_i1P1_2i2P2 *)
99let rec string_of_indexing_tl pretty prefix i = function
100        | [] -> if pretty then ")" else ""
101        | hd :: tl ->
102                let sep = if pretty then "," else "_" in
103                let str = string_of_sexpr pretty prefix i hd in
104                sep ^ str ^ string_of_indexing_tl pretty prefix (i+1) tl
105
106let string_of_indexing pretty prefix = function
107        | [] -> ""
108        | hd :: tl ->
109                let start = if pretty then "(" else "_" in
110    let str = string_of_sexpr pretty prefix 0 hd in
111                start ^ str ^ string_of_indexing_tl pretty prefix 1 tl
112               
113let string_of_cost_label ?(pretty = false) lab =
114        lab.name ^ string_of_indexing pretty "i" lab.i
115
116let fresh l universe =
117        {name = Atom.Gen.fresh universe; i = l} 
118
119(* TODO: urgh. Necessary? *)
120type aux_t = t
121                                                       
122(** labels are endowed with a lexicographical ordering *)
123module T : Map.OrderedType with type t = aux_t =
124    struct
125        type t = aux_t
126        let compare = compare (* uses the built-in lexicographical comparison *) 
127    end
128
129module Map = Map.Make(T)   
130module Set = Set.Make(T) 
131(** [constant_map d x] produces a finite map which associates
132    [x] to every element of the set [d]. *)
133
134let indexings_of atom s =
135        let f k accu = if k.name = atom then IndexingSet.add k.i accu else accu in
136        Set.fold f s IndexingSet.empty
137
138let constant_map d x = 
139  Set.fold (fun k accu -> Map.add k x accu) d Map.empty
140       
141        (**  **)
Note: See TracBrowser for help on using the repository browser.