source: src/ERTL/uses.ma @ 1151

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

interference graphs axiomatised, more added to ertl

File size: 535 bytes
Line 
1include "ERTL/ERTL.ma".
2
3let 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     
16definition lookup ≝
17  λuses.
18  λr.
19    assoc_list_find register nat (eq_identifier ?) uses 0 r.
20
21definition count ≝
22  λr.
23  λuses.
24    (r,
25
26let count r uses = Register.Map.add r (lookup uses r + 1) uses
Note: See TracBrowser for help on using the repository browser.