Last change
on this file since 1128 was
1127,
checked in by mulligan, 9 years ago

interference graphs axiomatised, more added to ertl

File size:
535 bytes

Line  

1  include "ERTL/ERTL.ma". 

2  

3  let rec assoc_list_find 

4  (A: Type[0]) (B: Type[0]) (eq_a: A → A → bool) (to_find: A) 

5  (def: B) (l: list (A × B)) 

6  on l ≝ 

7  match l with 

8  [ nil ⇒ def 

9   cons hd tl ⇒ 

10  if eq_a (\fst hd) to_find then 

11  \snd hd 

12  else 

13  assoc_list_find A B eq_a to_find def tl 

14  ]. 

15  

16  definition lookup ≝ 

17  λuses. 

18  λr. 

19  assoc_list_find register nat (eq_identifier ?) uses 0 r. 

20  

21  definition count ≝ 

22  λr. 

23  λuses. 

24  (r, 

25  

26  let count r uses = Register.Map.add r (lookup uses r + 1) uses 

Note: See
TracBrowser
for help on using the repository browser.