Ignore:
Timestamp:
Dec 13, 2010, 6:03:05 PM (9 years ago)
Author:
mulligan
Message:

Got a few more cases working.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/Map.ma

    r410 r414  
    11include "Universes.ma".
    22include "Compare.ma".
     3include "Maybe.ma".
    34
    45ninductive Map (A: Type[0]) (B: Type[0]): Type[0] ≝
     
    78| Node: A → B → Map A B → Map A B → Map A B.
    89
     10(* Greater than or equal to the right, less than to the left.  *)
     11
    912nlet 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
    1114  match map with
    12     [ Empty ⇒ Leaf key value
     15    [ Empty ⇒ Leaf key value
    1316    | Leaf key' value' ⇒
    1417      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)
    1821        ]
    19     | Node key' value'
     22    | Node key' value' left right
    2023      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)
    2427        ]
    2528    ].
     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 TracChangeset for help on using the changeset viewer.