|
Last change
on this file since 1165 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.
