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.