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

include "Universes.ma".
include "Compare.ma".
include "Maybe.ma".

ninductive Map (A: Type[0]) (B: Type[0]): Type[0] ≝
  Empty: Map A B
| Leaf: A → B → Map A B
| Node: A → B → Map A B → Map A B → Map A B.

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

nlet rec insert (A: Type[0]) (B: Type[0])
                (key: A) (f: A → A → Compare) (value: B) (map: Map A B) on map ≝
  match map with
    [ Empty ⇒ Leaf … key value
    | Leaf key' value' ⇒
      match f key key' with
        [ Equal ⇒ Node … key' value' (Empty …) (Leaf … key value)
        | Less ⇒ Node … key' value' (Leaf … key value) (Empty …)
        | Greater ⇒ Node … key' value' (Empty …) (Leaf … key value)
        ]
    | Node key' value' left right ⇒
      match f key key' with
        [ Equal ⇒ Node A B key' value' left (insert A B key f value right)
        | Less ⇒ Node A B key' value' (insert A B key f value left) right
        | Greater ⇒ Node A B key' value' left (insert A B key f value right)
        ]
    ].
    
nlet rec lookup (A: Type[0]) (B: Type[0])
                (key: A) (f: A → A → Compare) (map: Map A B) on map ≝
  match map with
    [ Empty ⇒ Nothing ?
    | Leaf key' value' ⇒
      match f key key' with
        [ Equal ⇒ Just ? value'
        | _ ⇒ Nothing ?
        ]
    | Node key' value' left right ⇒
      match f key key' with
        [ Equal ⇒ Just ? value'
        | Less ⇒ lookup A B key f left
        | Greater ⇒ lookup A B key f right
        ]
    ].