Changeset 414 for Deliverables/D4.1/Matita/Map.ma
 Timestamp:
 Dec 13, 2010, 6:03:05 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Map.ma
r410 r414 1 1 include "Universes.ma". 2 2 include "Compare.ma". 3 include "Maybe.ma". 3 4 4 5 ninductive Map (A: Type[0]) (B: Type[0]): Type[0] ≝ … … 7 8  Node: A → B → Map A B → Map A B → Map A B. 8 9 10 (* Greater than or equal to the right, less than to the left. *) 11 9 12 nlet rec insert (A: Type[0]) (B: Type[0]) 10 (key: A) (f: A → A → Compare) (value: B) (map: Map A B) ≝13 (key: A) (f: A → A → Compare) (value: B) (map: Map A B) on map ≝ 11 14 match map with 12 [ Empty ⇒ Leaf key value15 [ Empty ⇒ Leaf … key value 13 16  Leaf key' value' ⇒ 14 17 match f key key' with 15 [ Equal ⇒ ?16  Less ⇒ ?17  Greater ⇒ ?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) 18 21 ] 19  Node key' value' ⇒22  Node key' value' left right ⇒ 20 23 match f key key' with 21 [ Equal ⇒ ?22  Less ⇒ ?23  Greater ?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) 24 27 ] 25 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 TracChangeset
for help on using the changeset viewer.