Line | |
---|

1 | include "Universes.ma". |
---|

2 | include "Compare.ma". |
---|

3 | include "Maybe.ma". |
---|

4 | |
---|

5 | ninductive Map (A: Type[0]) (B: Type[0]): Type[0] ≝ |
---|

6 | Empty: Map A B |
---|

7 | | Leaf: A → B → Map A B |
---|

8 | | Node: A → B → Map A B → Map A B → Map A B. |
---|

9 | |
---|

10 | (* Greater than or equal to the right, less than to the left. *) |
---|

11 | |
---|

12 | nlet rec insert (A: Type[0]) (B: Type[0]) |
---|

13 | (key: A) (f: A → A → Compare) (value: B) (map: Map A B) on map ≝ |
---|

14 | match map with |
---|

15 | [ Empty ⇒ Leaf … key value |
---|

16 | | Leaf key' value' ⇒ |
---|

17 | match f key key' with |
---|

18 | [ Equal ⇒ Node … key' value' (Empty …) (Leaf … key value) |
---|

19 | | Less ⇒ Node … key' value' (Leaf … key value) (Empty …) |
---|

20 | | Greater ⇒ Node … key' value' (Empty …) (Leaf … key value) |
---|

21 | ] |
---|

22 | | Node key' value' left right ⇒ |
---|

23 | match f key key' with |
---|

24 | [ Equal ⇒ Node A B key' value' left (insert A B key f value right) |
---|

25 | | Less ⇒ Node A B key' value' (insert A B key f value left) right |
---|

26 | | Greater ⇒ Node A B key' value' left (insert A B key f value right) |
---|

27 | ] |
---|

28 | ]. |
---|

29 | |
---|

30 | nlet rec lookup (A: Type[0]) (B: Type[0]) |
---|

31 | (key: A) (f: A → A → Compare) (map: Map A B) on map ≝ |
---|

32 | match map with |
---|

33 | [ Empty ⇒ Nothing ? |
---|

34 | | Leaf key' value' ⇒ |
---|

35 | match f key key' with |
---|

36 | [ Equal ⇒ Just ? value' |
---|

37 | | _ ⇒ Nothing ? |
---|

38 | ] |
---|

39 | | Node key' value' left right ⇒ |
---|

40 | match f key key' with |
---|

41 | [ Equal ⇒ Just ? value' |
---|

42 | | Less ⇒ lookup A B key f left |
---|

43 | | Greater ⇒ lookup A B key f right |
---|

44 | ] |
---|

45 | ]. |
---|

**Note:** See

TracBrowser
for help on using the repository browser.