source: Deliverables/D4.1/Matita/Map.ma @ 414

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

Got a few more cases working.

File size: 1.5 KB
Line 
1include "Universes.ma".
2include "Compare.ma".
3include "Maybe.ma".
4
5ninductive 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
12nlet 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   
30nlet 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.