Revision ca7ff3f7
Added by LĂ©lio Brun over 1 year ago
src/utils/dimension.ml  

11  11  
12  12 
open Format 
13  13  
14 
type dim_expr = 

15 
{mutable dim_desc: dim_desc; 

16 
dim_loc: Location.t; 

17 
dim_id: int} 

14 
type dim_expr = { 

15 
mutable dim_desc : dim_desc; 

16 
dim_loc : Location.t; 

17 
dim_id : int; 

18 
} 

18  19  
19  20 
and dim_desc = 
20 
 Dbool of bool 

21 
 Dint of int


22 
 Dident of Utils.ident 

23 
 Dappl of Utils.ident * dim_expr list 

24 
 Dite of dim_expr * dim_expr * dim_expr 

25 
 Dlink of dim_expr 

26 
 Dvar 

27 
 Dunivar 

21 
 Dbool of bool


22 
 Dint of int


23 
 Dident of Utils.ident


24 
 Dappl of Utils.ident * dim_expr list


25 
 Dite of dim_expr * dim_expr * dim_expr


26 
 Dlink of dim_expr


27 
 Dvar


28 
 Dunivar


28  29  
29  30 
exception Unify of dim_expr * dim_expr 
31  
30  32 
exception InvalidDimension 
31  33  
32  34 
let new_id = ref (1) 
33  35  
34  36 
let mkdim loc dim = 
35  37 
incr new_id; 
36 
{ dim_loc = loc; 

37 
dim_id = !new_id; 

38 
dim_desc = dim;} 

38 
{ dim_loc = loc; dim_id = !new_id; dim_desc = dim } 

39  39  
40  40 
let mkdim_var () = 
41  41 
incr new_id; 
42 
{ dim_loc = Location.dummy_loc; 

43 
dim_id = !new_id; 

44 
dim_desc = Dvar;} 

42 
{ dim_loc = Location.dummy_loc; dim_id = !new_id; dim_desc = Dvar } 

45  43  
46  44 
let mkdim_ident loc id = 
47  45 
incr new_id; 
48 
{ dim_loc = loc; 

49 
dim_id = !new_id; 

50 
dim_desc = Dident id;} 

46 
{ dim_loc = loc; dim_id = !new_id; dim_desc = Dident id } 

51  47  
52  48 
let mkdim_bool loc b = 
53  49 
incr new_id; 
54 
{ dim_loc = loc; 

55 
dim_id = !new_id; 

56 
dim_desc = Dbool b;} 

50 
{ dim_loc = loc; dim_id = !new_id; dim_desc = Dbool b } 

57  51  
58  52 
let mkdim_int loc i = 
59  53 
incr new_id; 
60 
{ dim_loc = loc; 

61 
dim_id = !new_id; 

62 
dim_desc = Dint i;} 

54 
{ dim_loc = loc; dim_id = !new_id; dim_desc = Dint i } 

63  55  
64  56 
let mkdim_appl loc f args = 
65  57 
incr new_id; 
66 
{ dim_loc = loc; 

67 
dim_id = !new_id; 

68 
dim_desc = Dappl (f, args);} 

58 
{ dim_loc = loc; dim_id = !new_id; dim_desc = Dappl (f, args) } 

69  59  
70  60 
let mkdim_ite loc i t e = 
71  61 
incr new_id; 
72 
{ dim_loc = loc; 

73 
dim_id = !new_id; 

74 
dim_desc = Dite (i, t, e);} 

62 
{ dim_loc = loc; dim_id = !new_id; dim_desc = Dite (i, t, e) } 

75  63  
76  64 
let rec pp_dimension fmt dim = 
77 
(*fprintf fmt "<%d>" (Obj.magic dim: int);*) 

78 
match dim.dim_desc with 

79 
 Dident id > 

80 
fprintf fmt "%s" id 

81 
 Dint i > 

82 
fprintf fmt "%d" i 

83 
 Dbool b > 

84 
fprintf fmt "%B" b 

85 
 Dite (i, t, e) > 

86 
fprintf fmt "if %a then %a else %a" 

87 
pp_dimension i pp_dimension t pp_dimension e 

88 
 Dappl (f, [arg]) > 

89 
fprintf fmt "(%s%a)" f pp_dimension arg 

90 
 Dappl (f, [arg1; arg2]) > 

91 
fprintf fmt "(%a%s%a)" pp_dimension arg1 f pp_dimension arg2 

92 
 Dappl (_, _) > assert false 

93 
 Dlink dim' > fprintf fmt "%a" pp_dimension dim' 

94 
 Dvar > fprintf fmt "_%s" (Utils.name_of_dimension dim.dim_id) 

95 
 Dunivar > fprintf fmt "'%s" (Utils.name_of_dimension dim.dim_id) 

65 
(*fprintf fmt "<%d>" (Obj.magic dim: int);*) 

66 
match dim.dim_desc with 

67 
 Dident id > 

68 
fprintf fmt "%s" id 

69 
 Dint i > 

70 
fprintf fmt "%d" i 

71 
 Dbool b > 

72 
fprintf fmt "%B" b 

73 
 Dite (i, t, e) > 

74 
fprintf fmt "if %a then %a else %a" pp_dimension i pp_dimension t 

75 
pp_dimension e 

76 
 Dappl (f, [ arg ]) > 

77 
fprintf fmt "(%s%a)" f pp_dimension arg 

78 
 Dappl (f, [ arg1; arg2 ]) > 

79 
fprintf fmt "(%a%s%a)" pp_dimension arg1 f pp_dimension arg2 

80 
 Dappl (_, _) > 

81 
assert false 

82 
 Dlink dim' > 

83 
fprintf fmt "%a" pp_dimension dim' 

84 
 Dvar > 

85 
fprintf fmt "_%s" (Utils.name_of_dimension dim.dim_id) 

86 
 Dunivar > 

87 
fprintf fmt "'%s" (Utils.name_of_dimension dim.dim_id) 

96  88  
97  89 
let rec multi_dimension_product loc dim_list = 
98 
match dim_list with 

99 
 [] > mkdim_int loc 1 

100 
 [d] > d 

101 
 d::q > mkdim_appl loc "*" [d; multi_dimension_product loc q] 

90 
match dim_list with 

91 
 [] > 

92 
mkdim_int loc 1 

93 
 [ d ] > 

94 
d 

95 
 d :: q > 

96 
mkdim_appl loc "*" [ d; multi_dimension_product loc q ] 

102  97  
103  98 
(* Builds a dimension expr representing 0<=d *) 
104 
let check_bound loc d = 

105 
mkdim_appl loc "<=" [mkdim_int loc 0; d] 

99 
let check_bound loc d = mkdim_appl loc "<=" [ mkdim_int loc 0; d ] 

106  100  
107  101 
(* Builds a dimension expr representing 0<=i<d *) 
108  102 
let check_access loc d i = 
109 
mkdim_appl loc "&&" 

110 
[mkdim_appl loc "<=" [mkdim_int loc 0; i]; 

111 
mkdim_appl loc "<" [i; d]] 

103 
mkdim_appl loc "&&" 

104 
[ mkdim_appl loc "<=" [ mkdim_int loc 0; i ]; mkdim_appl loc "<" [ i; d ] ] 

112  105  
113 
let rec repr dim = 

114 
match dim.dim_desc with 

115 
 Dlink dim' > repr dim' 

116 
 _ > dim 

106 
let rec repr dim = match dim.dim_desc with Dlink dim' > repr dim'  _ > dim 

117  107  
118  108 
let rec is_eq_dimension d1 d2 = 
119  109 
let d1 = repr d1 in 
120  110 
let d2 = repr d2 in 
121 
d1.dim_id = d2.dim_id  

111 
d1.dim_id = d2.dim_id 

112 
 

122  113 
match d1.dim_desc, d2.dim_desc with 
123  114 
 Dappl (f1, args1), Dappl (f2, args2) > 
124 
f1 = f2 && List.length args1 = List.length args2 && List.for_all2 is_eq_dimension args1 args2 

115 
f1 = f2 

116 
&& List.length args1 = List.length args2 

117 
&& List.for_all2 is_eq_dimension args1 args2 

125  118 
 Dite (c1, t1, e1), Dite (c2, t2, e2) > 
126  119 
is_eq_dimension c1 c2 && is_eq_dimension t1 t2 && is_eq_dimension e1 e2 
127 
 Dint i1 , Dint i2 > i1 = i2 

128 
 Dbool b1 , Dbool b2 > b1 = b2 

129 
 Dident id1, Dident id2 > id1 = id2 

130 
 _ > false 

120 
 Dint i1, Dint i2 > 

121 
i1 = i2 

122 
 Dbool b1, Dbool b2 > 

123 
b1 = b2 

124 
 Dident id1, Dident id2 > 

125 
id1 = id2 

126 
 _ > 

127 
false 

131  128  
132  129 
let is_dimension_const dim = 
133 
match (repr dim).dim_desc with 

134 
 Dint _ 

135 
 Dbool _ > true 

136 
 _ > false 

130 
match (repr dim).dim_desc with Dint _  Dbool _ > true  _ > false 

137  131  
138  132 
let size_const_dimension dim = 
139  133 
match (repr dim).dim_desc with 
140 
 Dint i > i 

141 
 Dbool b > if b then 1 else 0 

142 
 _ > (Format.eprintf "internal error: size_const_dimension %a@." pp_dimension dim; assert false) 

134 
 Dint i > 

135 
i 

136 
 Dbool b > 

137 
if b then 1 else 0 

138 
 _ > 

139 
Format.eprintf "internal error: size_const_dimension %a@." pp_dimension dim; 

140 
assert false 

143  141  
144  142 
let rec is_polymorphic dim = 
145  143 
match dim.dim_desc with 
146 
 Dident _ 

147 
 Dint _ 

148 
 Dbool _ 

149 
 Dvar > false 

150 
 Dite (i, t, e) > 

151 
is_polymorphic i  is_polymorphic t  is_polymorphic e 

152 
 Dappl (_, args) > List.exists is_polymorphic args 

153 
 Dlink dim' > is_polymorphic dim' 

154 
 Dunivar > true 

144 
 Dident _  Dint _  Dbool _  Dvar > 

145 
false 

146 
 Dite (i, t, e) > 

147 
is_polymorphic i  is_polymorphic t  is_polymorphic e 

148 
 Dappl (_, args) > 

149 
List.exists is_polymorphic args 

150 
 Dlink dim' > 

151 
is_polymorphic dim' 

152 
 Dunivar > 

153 
true 

155  154  
156  155 
(* Normalizes a dimension expression, i.e. canonicalize all polynomial 
157 
subexpressions, where unsupported operations (eg. '/') are treated 

158 
as variables. 

159 
*) 

156 
subexpressions, where unsupported operations (eg. '/') are treated as 

157 
variables. *) 

160  158  
161  159 
let rec factors dim = 
162  160 
match dim.dim_desc with 
163 
 Dappl (f, args) when f = "*" > List.flatten (List.map factors args) 

164 
 _ > [dim] 

161 
 Dappl (f, args) when f = "*" > 

162 
List.flatten (List.map factors args) 

163 
 _ > 

164 
[ dim ] 

165  165  
166  166 
let rec factors_constant fs = 
167  167 
match fs with 
168 
 [] > 1 

169 
 f::q > 

168 
 [] > 

169 
1 

170 
 f :: q > ( 

170  171 
match f.dim_desc with 
171 
 Dint i > i * (factors_constant q) 

172 
 _ > factors_constant q 

172 
 Dint i > 

173 
i * factors_constant q 

174 
 _ > 

175 
factors_constant q) 

173  176  
174  177 
let norm_factors fs = 
175  178 
let k = factors_constant fs in 
176  179 
let nk = List.filter (fun d > not (is_dimension_const d)) fs in 
177 
(k, List.sort compare nk)


180 
k, List.sort compare nk


178  181  
179  182 
let rec terms dim = 
180 
match dim.dim_desc with 

181 
 Dappl (f, args) when f = "+" > List.flatten (List.map terms args) 

182 
 _ > [dim] 

183  
184 
let normalize dim = 

185 
dim 

186 
(* 

187 
let rec unnormalize loc l = 

188 
let l = List.sort (fun (k, l) (k', l') > compare l l') (List.map (fun (k, l) > (k, List.sort compare l)) l) in 

189 
match l with 

190 
 [] > mkdim_int loc 0 

191 
 t::q > 

192 
List.fold_left (fun res (k, l) > mkdim_appl loc "+" res (mkdim_appl loc "*" (mkdim_int loc k) l)) t q 

193 
*) 

194 
let copy copy_dim_vars dim = 

195 
let rec cp dim = 

196  183 
match dim.dim_desc with 
197 
 Dbool _ 

198 
 Dint _ > dim 

199 
 Dident id > mkdim_ident dim.dim_loc id 

200 
 Dite (c, t, e) > mkdim_ite dim.dim_loc (cp c) (cp t) (cp e) 

201 
 Dappl (id, args) > mkdim_appl dim.dim_loc id (List.map cp args) 

202 
 Dlink dim' > cp dim' 

203 
 Dunivar > assert false 

204 
 Dvar > 

205 
try 

206 
List.assoc dim.dim_id !copy_dim_vars 

207 
with Not_found > 

208 
let var = mkdim dim.dim_loc Dvar in 

209 
copy_dim_vars := (dim.dim_id, var)::!copy_dim_vars; 

210 
var 

211 
in cp dim 

184 
 Dappl (f, args) when f = "+" > 

185 
List.flatten (List.map terms args) 

186 
 _ > 

187 
[ dim ] 

188  
189 
let normalize dim = dim 

212  190  
213 
(* Partially evaluates a 'simple' dimension expr [dim], i.e. an expr containing only int and bool 

214 
constructs, with conditionals. [eval_const] is a typing environment for static values. [eval_op] is an evaluation env for basic operators. The argument [dim] is modified inplace. 

215 
*) 

191 
(* let rec unnormalize loc l = let l = List.sort (fun (k, l) (k', l') > compare 

192 
l l') (List.map (fun (k, l) > (k, List.sort compare l)) l) in match l with  

193 
[] > mkdim_int loc 0  t::q > List.fold_left (fun res (k, l) > mkdim_appl 

194 
loc "+" res (mkdim_appl loc "*" (mkdim_int loc k) l)) t q *) 

195 
let copy copy_dim_vars dim = 

196 
let rec cp dim = 

197 
match dim.dim_desc with 

198 
 Dbool _  Dint _ > 

199 
dim 

200 
 Dident id > 

201 
mkdim_ident dim.dim_loc id 

202 
 Dite (c, t, e) > 

203 
mkdim_ite dim.dim_loc (cp c) (cp t) (cp e) 

204 
 Dappl (id, args) > 

205 
mkdim_appl dim.dim_loc id (List.map cp args) 

206 
 Dlink dim' > 

207 
cp dim' 

208 
 Dunivar > 

209 
assert false 

210 
 Dvar > ( 

211 
try List.assoc dim.dim_id !copy_dim_vars 

212 
with Not_found > 

213 
let var = mkdim dim.dim_loc Dvar in 

214 
copy_dim_vars := (dim.dim_id, var) :: !copy_dim_vars; 

215 
var) 

216 
in 

217 
cp dim 

218  
219 
(* Partially evaluates a 'simple' dimension expr [dim], i.e. an expr containing 

220 
only int and bool constructs, with conditionals. [eval_const] is a typing 

221 
environment for static values. [eval_op] is an evaluation env for basic 

222 
operators. The argument [dim] is modified inplace. *) 

216  223 
let rec eval eval_op eval_const dim = 
217  224 
match dim.dim_desc with 
218 
 Dbool _ 

219 
 Dint _ > () 

220 
 Dident id > 

221 
(match eval_const id with 

222 
 Some val_dim > dim.dim_desc < Dlink val_dim 

223 
 None > (Format.eprintf "invalid %a@." pp_dimension dim; raise InvalidDimension)) 

224 
 Dite (c, t, e) > 

225 
begin 

226 
eval eval_op eval_const c; 

227 
eval eval_op eval_const t; 

228 
eval eval_op eval_const e; 

229 
match (repr c).dim_desc with 

230 
 Dbool b > dim.dim_desc < Dlink (if b then t else e) 

231 
 _ > () 

232 
end 

225 
 Dbool _  Dint _ > 

226 
() 

227 
 Dident id > ( 

228 
match eval_const id with 

229 
 Some val_dim > 

230 
dim.dim_desc < Dlink val_dim 

231 
 None > 

232 
Format.eprintf "invalid %a@." pp_dimension dim; 

233 
raise InvalidDimension) 

234 
 Dite (c, t, e) > ( 

235 
eval eval_op eval_const c; 

236 
eval eval_op eval_const t; 

237 
eval eval_op eval_const e; 

238 
match (repr c).dim_desc with 

239 
 Dbool b > 

240 
dim.dim_desc < Dlink (if b then t else e) 

241 
 _ > 

242 
()) 

233  243 
 Dappl (id, args) > 
234 
begin 

235 
List.iter (eval eval_op eval_const) args; 

236 
if List.for_all is_dimension_const args 

237 
then dim.dim_desc < Env.lookup_value eval_op id (List.map (fun d > (repr d).dim_desc) args) 

238 
end 

244 
List.iter (eval eval_op eval_const) args; 

245 
if List.for_all is_dimension_const args then 

246 
dim.dim_desc < 

247 
Env.lookup_value eval_op id (List.map (fun d > (repr d).dim_desc) args) 

239  248 
 Dlink dim' > 
240 
begin


241 
eval eval_op eval_const dim';


242 
dim.dim_desc < Dlink (repr dim')


243 
end


244 
 Dvar > ()


245 
 Dunivar > assert false


249 
eval eval_op eval_const dim';


250 
dim.dim_desc < Dlink (repr dim')


251 
 Dvar >


252 
()


253 
 Dunivar >


254 
assert false


246  255  
247  256 
let uneval const univar = 
248  257 
let univar = repr univar in 
249  258 
match univar.dim_desc with 
250 
 Dunivar > univar.dim_desc < Dident const 

251 
 _ > assert false 

259 
 Dunivar > 

260 
univar.dim_desc < Dident const 

261 
 _ > 

262 
assert false 

252  263  
253  264 
(** [occurs dvar dim] returns true if the dimension variable [dvar] occurs in 
254  265 
dimension expression [dim]. False otherwise. *) 
255  266 
let rec occurs dvar dim = 
256  267 
let dim = repr dim in 
257  268 
match dim.dim_desc with 
258 
 Dvar > dim.dim_id = dvar.dim_id 

259 
 Dident _ 

260 
 Dint _ 

261 
 Dbool _ 

262 
 Dunivar > false 

263 
 Dite (i, t, e) > 

264 
occurs dvar i  occurs dvar t  occurs dvar e 

265 
 Dappl (_, args) > List.exists (occurs dvar) args 

266 
 Dlink _ > assert false 

267  
268 
(* Promote monomorphic dimension variables to polymorphic variables. 

269 
Generalize by sideeffects *) 

269 
 Dvar > 

270 
dim.dim_id = dvar.dim_id 

271 
 Dident _  Dint _  Dbool _  Dunivar > 

272 
false 

273 
 Dite (i, t, e) > 

274 
occurs dvar i  occurs dvar t  occurs dvar e 

275 
 Dappl (_, args) > 

276 
List.exists (occurs dvar) args 

277 
 Dlink _ > 

278 
assert false 

279  
280 
(* Promote monomorphic dimension variables to polymorphic variables. Generalize 

281 
by sideeffects *) 

270  282 
let rec generalize dim = 
271  283 
match dim.dim_desc with 
272 
 Dvar > dim.dim_desc < Dunivar 

273 
 Dident _ 

274 
 Dint _ 

275 
 Dbool _ 

276 
 Dunivar > () 

277 
 Dite (i, t, e) > 

278 
generalize i; generalize t; generalize e 

279 
 Dappl (_, args) > List.iter generalize args 

280 
 Dlink dim' > generalize dim' 

281  
282 
(* Instantiate polymorphic dimension variables to monomorphic variables. 

283 
Also duplicates the whole term structure (but the constant subterms). 

284 
*) 

284 
 Dvar > 

285 
dim.dim_desc < Dunivar 

286 
 Dident _  Dint _  Dbool _  Dunivar > 

287 
() 

288 
 Dite (i, t, e) > 

289 
generalize i; 

290 
generalize t; 

291 
generalize e 

292 
 Dappl (_, args) > 

293 
List.iter generalize args 

294 
 Dlink dim' > 

295 
generalize dim' 

296  
297 
(* Instantiate polymorphic dimension variables to monomorphic variables. Also 

298 
duplicates the whole term structure (but the constant subterms). *) 

285  299 
let rec instantiate inst_dim_vars dim = 
286  300 
let dim = repr dim in 
287  301 
match dim.dim_desc with 
288 
 Dvar 

289 
 Dident _ 

290 
 Dint _ 

291 
 Dbool _ > dim 

292 
 Dite (i, t, e) > 

293 
mkdim_ite dim.dim_loc 

294 
(instantiate inst_dim_vars i) 

295 
(instantiate inst_dim_vars t) 

296 
(instantiate inst_dim_vars e) 

297 
 Dappl (f, args) > mkdim_appl dim.dim_loc f (List.map (instantiate inst_dim_vars) args) 

298 
 Dlink _ > assert false (*mkdim dim.dim_loc (Dlink (instantiate inst_dim_vars dim'))*) 

299 
 Dunivar > 

300 
try 

301 
List.assoc dim.dim_id !inst_dim_vars 

302 
with Not_found > 

303 
let var = mkdim dim.dim_loc Dvar in 

304 
inst_dim_vars := (dim.dim_id, var)::!inst_dim_vars; 

305 
var 

306  
307 
(** destructive unification of [dim1] and [dim2]. 

308 
Raises [Unify (t1,t2)] if the types are not unifiable. 

309 
if [semi] unification is required, 

310 
[dim1] should furthermore be an instance of [dim2] *) 

311 
let unify ?(semi=false) dim1 dim2 = 

302 
 Dvar  Dident _  Dint _  Dbool _ > 

303 
dim 

304 
 Dite (i, t, e) > 

305 
mkdim_ite dim.dim_loc 

306 
(instantiate inst_dim_vars i) 

307 
(instantiate inst_dim_vars t) 

308 
(instantiate inst_dim_vars e) 

309 
 Dappl (f, args) > 

310 
mkdim_appl dim.dim_loc f (List.map (instantiate inst_dim_vars) args) 

311 
 Dlink _ > 

312 
assert false (*mkdim dim.dim_loc (Dlink (instantiate inst_dim_vars dim'))*) 

313 
 Dunivar > ( 

314 
try List.assoc dim.dim_id !inst_dim_vars 

315 
with Not_found > 

316 
let var = mkdim dim.dim_loc Dvar in 

317 
inst_dim_vars := (dim.dim_id, var) :: !inst_dim_vars; 

318 
var) 

319  
320 
(** destructive unification of [dim1] and [dim2]. Raises [Unify (t1,t2)] if the 

321 
types are not unifiable. if [semi] unification is required, [dim1] should 

322 
furthermore be an instance of [dim2] *) 

323 
let unify ?(semi = false) dim1 dim2 = 

312  324 
let rec unif dim1 dim2 = 
313  325 
let dim1 = repr dim1 in 
314  326 
let dim2 = repr dim2 in 
315 
if dim1.dim_id = dim2.dim_id then () else 

327 
if dim1.dim_id = dim2.dim_id then () 

328 
else 

316  329 
match dim1.dim_desc, dim2.dim_desc with 
317 
 Dunivar, _ 

318 
 _ , Dunivar > assert false 

319 
 Dvar , Dvar > 

320 
if dim1.dim_id < dim2.dim_id 

321 
then dim2.dim_desc < Dlink dim1 

322 
else dim1.dim_desc < Dlink dim2 

323 
 Dvar , _ when (not semi) && not (occurs dim1 dim2) > 

324 
dim1.dim_desc < Dlink dim2 

325 
 _ , Dvar when not (occurs dim2 dim1) > 

326 
dim2.dim_desc < Dlink dim1 

327 
 Dite(i1, t1, e1), Dite(i2, t2, e2) > 

328 
begin 

329 
unif i1 i2; 

330 
unif t1 t2; 

331 
unif e1 e2 

332 
end 

333 
 Dappl(f1, args1), Dappl(f2, args2) when f1 = f2 && List.length args1 = List.length args2 > 

334 
List.iter2 unif args1 args2 

335 
 Dbool b1, Dbool b2 when b1 = b2 > () 

336 
 Dint i1 , Dint i2 when i1 = i2 > () 

337 
 Dident id1, Dident id2 when id1 = id2 > () 

338 
 _ > raise (Unify (dim1, dim2)) 

339 
in unif dim1 dim2 

340  
341 
let rec rename fnode fvar e = 

342 
{ e with dim_desc = expr_replace_var_desc fnode fvar e.dim_desc } 

330 
 Dunivar, _  _, Dunivar > 

331 
assert false 

332 
 Dvar, Dvar > 

333 
if dim1.dim_id < dim2.dim_id then dim2.dim_desc < Dlink dim1 

334 
else dim1.dim_desc < Dlink dim2 

335 
 Dvar, _ when (not semi) && not (occurs dim1 dim2) > 

336 
dim1.dim_desc < Dlink dim2 

337 
 _, Dvar when not (occurs dim2 dim1) > 

338 
dim2.dim_desc < Dlink dim1 

339 
 Dite (i1, t1, e1), Dite (i2, t2, e2) > 

340 
unif i1 i2; 

341 
unif t1 t2; 

342 
unif e1 e2 

343 
 Dappl (f1, args1), Dappl (f2, args2) 

344 
when f1 = f2 && List.length args1 = List.length args2 > 

345 
List.iter2 unif args1 args2 

346 
 Dbool b1, Dbool b2 when b1 = b2 > 

347 
() 

348 
 Dint i1, Dint i2 when i1 = i2 > 

349 
() 

350 
 Dident id1, Dident id2 when id1 = id2 > 

351 
() 

352 
 _ > 

353 
raise (Unify (dim1, dim2)) 

354 
in 

355 
unif dim1 dim2 

356  
357 
let rec rename fnode fvar e = 

358 
{ e with dim_desc = expr_replace_var_desc fnode fvar e.dim_desc } 

359  
343  360 
and expr_replace_var_desc fnode fvar e = 
344  361 
let re = rename fnode fvar in 
345  362 
match e with 
346 
 Dvar 

347 
 Dunivar 

348 
 Dbool _ 

349 
 Dint _ > e 

350 
 Dident v > Dident (fvar v) 

351 
 Dappl (id, el) > Dappl (fnode id, List.map re el) 

352 
 Dite (g,t,e) > Dite (re g, re t, re e) 

353 
 Dlink e > Dlink (re e) 

354  
355 
let rec expr_replace_expr fvar e = 

356 
{ e with dim_desc = expr_replace_expr_desc fvar e.dim_desc } 

363 
 Dvar  Dunivar  Dbool _  Dint _ > 

364 
e 

365 
 Dident v > 

366 
Dident (fvar v) 

367 
 Dappl (id, el) > 

368 
Dappl (fnode id, List.map re el) 

369 
 Dite (g, t, e) > 

370 
Dite (re g, re t, re e) 

371 
 Dlink e > 

372 
Dlink (re e) 

373  
374 
let rec expr_replace_expr fvar e = 

375 
{ e with dim_desc = expr_replace_expr_desc fvar e.dim_desc } 

376  
357  377 
and expr_replace_expr_desc fvar e = 
358  378 
let re = expr_replace_expr fvar in 
359  379 
match e with 
360 
 Dvar 

361 
 Dunivar 

362 
 Dbool _ 

363 
 Dint _ > e 

364 
 Dident v > (fvar v).dim_desc 

365 
 Dappl (id, el) > Dappl (id, List.map re el) 

366 
 Dite (g,t,e) > Dite (re g, re t, re e) 

367 
 Dlink e > Dlink (re e) 

380 
 Dvar  Dunivar  Dbool _  Dint _ > 

381 
e 

382 
 Dident v > 

383 
(fvar v).dim_desc 

384 
 Dappl (id, el) > 

385 
Dappl (id, List.map re el) 

386 
 Dite (g, t, e) > 

387 
Dite (re g, re t, re e) 

388 
 Dlink e > 

389 
Dlink (re e) 
Also available in: Unified diff
reformatting