1 | module Atom = |
---|
2 | struct |
---|
3 | include StringTools |
---|
4 | end |
---|
5 | |
---|
6 | module StringMap = Map.Make(String) |
---|
7 | |
---|
8 | (** Simple expressions are for now affine maps of the form a*_+b *) |
---|
9 | type sexpr = |
---|
10 | | Sexpr of int*int |
---|
11 | |
---|
12 | let sexpr_id = Sexpr(1, 0) |
---|
13 | |
---|
14 | let const_sexpr n = Sexpr(0, n) |
---|
15 | |
---|
16 | type index = int |
---|
17 | |
---|
18 | let make_id prefix depth = prefix ^ string_of_int depth |
---|
19 | |
---|
20 | type indexing = sexpr list |
---|
21 | |
---|
22 | type 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 *) |
---|
27 | let rec enter_loop n indexing = match n with |
---|
28 | | None -> () |
---|
29 | | Some x -> try indexing.(x) <- 0 with | _ -> assert false |
---|
30 | |
---|
31 | (** [enter_loop n indexing] is used to update indexing when one is continuing a |
---|
32 | loop indexed by [n]. *) |
---|
33 | let rec continue_loop n indexing = match n with |
---|
34 | | None -> () |
---|
35 | | Some x -> try indexing.(x) <- indexing.(x) + 1 with | _ -> assert false |
---|
36 | |
---|
37 | let sexpr_of i l = |
---|
38 | try |
---|
39 | List.nth l i |
---|
40 | with |
---|
41 | | Failure _ |
---|
42 | | Invalid_argument _ -> invalid_arg "costLabel.sexpr_of" |
---|
43 | |
---|
44 | let empty_indexing = [] |
---|
45 | |
---|
46 | let 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 *) |
---|
50 | let compose_sexpr (Sexpr(a, b)) (Sexpr(c, d)) = |
---|
51 | Sexpr (a * c, b * c + d) |
---|
52 | |
---|
53 | let ev_sexpr i (Sexpr(a, b)) = a*i+b |
---|
54 | |
---|
55 | (* i|-->e ° I *) |
---|
56 | let 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 *) |
---|
63 | let 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 | |
---|
67 | let rec compose_const_indexing_i i c = function |
---|
68 | | [] -> [] |
---|
69 | | s :: l -> |
---|
70 | try |
---|
71 | const_sexpr (ev_sexpr c.(i) s) :: compose_const_indexing_i (i+1) c l |
---|
72 | with |
---|
73 | | Invalid_argument _ -> assert false |
---|
74 | |
---|
75 | module IndexingSet = Set.Make(struct |
---|
76 | type t = indexing |
---|
77 | let compare = compare |
---|
78 | end) |
---|
79 | |
---|
80 | type t = { |
---|
81 | name : Atom.t; |
---|
82 | i : indexing |
---|
83 | } |
---|
84 | |
---|
85 | let apply_const_indexing c lbl = |
---|
86 | {lbl with i = compose_const_indexing_i 0 c lbl.i} |
---|
87 | |
---|
88 | |
---|
89 | (* if [pretty] is false then a name suitable for labels is given*) |
---|
90 | (* ('P' replaces '+') *) |
---|
91 | let string_of_sexpr pretty prefix i (Sexpr(a, b)) = |
---|
92 | let plus = if pretty then "+" else "P" in |
---|
93 | let id = prefix ^ string_of_int i in |
---|
94 | let a_id_s = if a = 1 then id else string_of_int a ^ id in |
---|
95 | let b_s = string_of_int b in |
---|
96 | if a = 0 then b_s else |
---|
97 | if b = 0 then a_id_s else a_id_s ^ plus ^ b_s |
---|
98 | |
---|
99 | (* examples:*) |
---|
100 | (* [pretty] true: (0,i1+1,2i2+2)*) |
---|
101 | (* [pretty] false: _0_i1P1_2i2P2 *) |
---|
102 | let rec string_of_indexing_tl pretty prefix i = function |
---|
103 | | [] -> if pretty then ")" else "" |
---|
104 | | hd :: tl -> |
---|
105 | let sep = if pretty then "," else "_" in |
---|
106 | let str = string_of_sexpr pretty prefix i hd in |
---|
107 | sep ^ str ^ string_of_indexing_tl pretty prefix (i+1) tl |
---|
108 | |
---|
109 | let string_of_indexing pretty prefix = function |
---|
110 | | [] -> "" |
---|
111 | | hd :: tl -> |
---|
112 | let start = if pretty then "(" else "_" in |
---|
113 | let str = string_of_sexpr pretty prefix 0 hd in |
---|
114 | start ^ str ^ string_of_indexing_tl pretty prefix 1 tl |
---|
115 | |
---|
116 | let string_of_cost_label ?(pretty = false) lab = |
---|
117 | lab.name ^ string_of_indexing pretty "i" lab.i |
---|
118 | |
---|
119 | let fresh l universe = |
---|
120 | {name = Atom.Gen.fresh universe; i = l} |
---|
121 | |
---|
122 | (* TODO: urgh. Necessary? *) |
---|
123 | type aux_t = t |
---|
124 | |
---|
125 | (** labels are endowed with a lexicographical ordering *) |
---|
126 | module T : Map.OrderedType with type t = aux_t = |
---|
127 | struct |
---|
128 | type t = aux_t |
---|
129 | let compare = compare (* uses the built-in lexicographical comparison *) |
---|
130 | end |
---|
131 | |
---|
132 | module Map = Map.Make(T) |
---|
133 | module Set = Set.Make(T) |
---|
134 | (** [constant_map d x] produces a finite map which associates |
---|
135 | [x] to every element of the set [d]. *) |
---|
136 | |
---|
137 | let indexings_of atom s = |
---|
138 | let f k accu = if k.name = atom then IndexingSet.add k.i accu else accu in |
---|
139 | Set.fold f s IndexingSet.empty |
---|
140 | |
---|
141 | let constant_map d x = |
---|
142 | Set.fold (fun k accu -> Map.add k x accu) d Map.empty |
---|
143 | |
---|
144 | (** **) |
---|