Revision 6b4d172f
Added by Xavier Thirioux over 7 years ago
src/dimension.ml  

319  319 
inst_dim_vars := (dim.dim_id, var)::!inst_dim_vars; 
320  320 
var 
321  321  
322 
let rec unify dim1 dim2 = 

323 
let dim1 = repr dim1 in 

324 
let dim2 = repr dim2 in 

325 
if dim1.dim_id = dim2.dim_id then () else 

326 
match dim1.dim_desc, dim2.dim_desc with 

327 
 Dunivar, _ 

328 
 _ , Dunivar > assert false 

329 
 Dvar , Dvar > 

330 
if dim1.dim_id < dim2.dim_id 

331 
then dim2.dim_desc < Dlink dim1 

332 
else dim1.dim_desc < Dlink dim2 

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

334 
dim1.dim_desc < Dlink dim2 

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

336 
dim2.dim_desc < Dlink dim1 

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

338 
begin 

339 
unify i1 i2; 

340 
unify t1 t2; 

341 
unify e1 e2 

342 
end 

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

344 
List.iter2 unify args1 args2 

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

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

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

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

349  
350 
(* unification with the constraint that dim1 is an instance of dim2 *) 

351 
let rec semi_unify dim1 dim2 = 

352 
let dim1 = repr dim1 in 

353 
let dim2 = repr dim2 in 

354 
if dim1.dim_id = dim2.dim_id then () else 

355 
match dim1.dim_desc, dim2.dim_desc with 

356 
 Dunivar, _ 

357 
 _ , Dunivar > assert false 

358 
 Dvar , Dvar > 

359 
if dim1.dim_id < dim2.dim_id 

360 
then dim2.dim_desc < Dlink dim1 

361 
else dim1.dim_desc < Dlink dim2 

362 
 Dvar , _ > raise (Unify (dim1, dim2)) 

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

364 
dim2.dim_desc < Dlink dim1 

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

366 
begin 

367 
semi_unify i1 i2; 

368 
semi_unify t1 t2; 

369 
semi_unify e1 e2 

370 
end 

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

372 
List.iter2 semi_unify args1 args2 

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

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

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

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

322 
(** destructive unification of [dim1] and [dim2]. 

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

324 
if [semi] unification is required, 

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

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

327 
let rec unif dim1 dim2 = 

328 
let dim1 = repr dim1 in 

329 
let dim2 = repr dim2 in 

330 
if dim1.dim_id = dim2.dim_id then () else 

331 
match dim1.dim_desc, dim2.dim_desc with 

332 
 Dunivar, _ 

333 
 _ , Dunivar > assert false 

334 
 Dvar , Dvar > 

335 
if dim1.dim_id < dim2.dim_id 

336 
then dim2.dim_desc < Dlink dim1 

337 
else dim1.dim_desc < Dlink dim2 

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

339 
dim1.dim_desc < Dlink dim2 

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

341 
dim2.dim_desc < Dlink dim1 

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

343 
begin 

344 
unif i1 i2; 

345 
unif t1 t2; 

346 
unif e1 e2 

347 
end 

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

349 
List.iter2 unif args1 args2 

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

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

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

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

354 
in unif dim1 dim2 

377  355  
378  356 
let rec expr_replace_var fvar e = 
379  357 
{ e with dim_desc = expr_replace_desc fvar e.dim_desc } 
Also available in: Unified diff
 refactorization of typing code (simpler subtyping rules)
 simplification of clock calculus (may be still buggy, work in progress)
no impact on unclocked programs.