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 is_const_sexpr (Sexpr(a, _)) = (a = 0) |
---|
13 | |
---|
14 | let sexpr_id = Sexpr(1, 0) |
---|
15 | |
---|
16 | let const_sexpr n = Sexpr(0, n) |
---|
17 | |
---|
18 | type index = int |
---|
19 | |
---|
20 | let make_id prefix depth = prefix ^ string_of_int depth |
---|
21 | |
---|
22 | type indexing = sexpr list |
---|
23 | |
---|
24 | type const_indexing = int ExtArray.t |
---|
25 | |
---|
26 | let const_ind_iter = ExtArray.iter |
---|
27 | |
---|
28 | let curr_const_ind = function |
---|
29 | | hd :: _ -> hd |
---|
30 | | _ -> invalid_arg "curr_const_ind applied to non-empty list" |
---|
31 | |
---|
32 | let init_const_indexing () = ExtArray.make ~buff:1 0 0 |
---|
33 | |
---|
34 | let enter_loop_single indexing n = ExtArray.set indexing n 0 |
---|
35 | |
---|
36 | let 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 | |
---|
42 | let curr_ind = function |
---|
43 | | hd :: _ -> hd |
---|
44 | | _ -> invalid_arg "empty indexing stack" |
---|
45 | |
---|
46 | let enter_loop inds = enter_loop_single (curr_ind inds) |
---|
47 | |
---|
48 | let continue_loop inds = continue_loop_single (curr_ind inds) |
---|
49 | |
---|
50 | let enter_loop_opt indexing = Option.iter (enter_loop indexing) |
---|
51 | |
---|
52 | let continue_loop_opt indexing = Option.iter (continue_loop indexing) |
---|
53 | |
---|
54 | let new_const_ind inds = init_const_indexing () :: inds |
---|
55 | |
---|
56 | let forget_const_ind = function |
---|
57 | | _ :: inds -> inds |
---|
58 | | _ -> invalid_arg "empty indexing stack" |
---|
59 | |
---|
60 | let sexpr_of i l = |
---|
61 | try |
---|
62 | List.nth l i |
---|
63 | with |
---|
64 | | Failure _ |
---|
65 | | Invalid_argument _ -> invalid_arg "costLabel.sexpr_of" |
---|
66 | |
---|
67 | let empty_indexing = [] |
---|
68 | |
---|
69 | let 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 *) |
---|
73 | let compose_sexpr (Sexpr(a, b)) (Sexpr(c, d)) = |
---|
74 | Sexpr (a * c, b * c + d) |
---|
75 | |
---|
76 | let ev_sexpr i (Sexpr(a, b)) = a*i+b |
---|
77 | |
---|
78 | (* i|-->e ° I *) |
---|
79 | let 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 *) |
---|
86 | let 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 | |
---|
90 | let 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 | |
---|
103 | module IndexingSet = Set.Make(struct |
---|
104 | type t = indexing |
---|
105 | let compare = compare |
---|
106 | end) |
---|
107 | |
---|
108 | type t = { |
---|
109 | name : Atom.t; |
---|
110 | i : indexing |
---|
111 | } |
---|
112 | |
---|
113 | let comp_index i s lbl = |
---|
114 | {lbl with i = compose_index_indexing i s lbl.i} |
---|
115 | |
---|
116 | let 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 '+') *) |
---|
122 | let 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 *) |
---|
133 | let 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 | |
---|
140 | let 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 | |
---|
147 | let string_of_cost_label ?(pretty = false) lab = |
---|
148 | lab.name ^ string_of_indexing pretty "i" lab.i |
---|
149 | |
---|
150 | let fresh l universe = |
---|
151 | {name = Atom.Gen.fresh universe; i = l} |
---|
152 | |
---|
153 | (* TODO: urgh. Necessary? *) |
---|
154 | type aux_t = t |
---|
155 | |
---|
156 | (** labels are endowed with a lexicographical ordering *) |
---|
157 | module 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 | |
---|
163 | module Map = Map.Make(T) |
---|
164 | module 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 | |
---|
168 | let 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 | |
---|
172 | let constant_map d x = |
---|
173 | Set.fold (fun k accu -> Map.add k x accu) d Map.empty |
---|