Ignore:
Timestamp:
Dec 5, 2010, 11:54:59 PM (9 years ago)
Author:
sacerdot
Message:

1) notation for cast fixed
2) ambiguity reduced: Empty => VEmpty, Cons => VCons
3) DoTest? modified to pretty-print the execution trace.

This should make debugging easier.

File:
1 edited

Legend:

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

    r357 r374  
    1212       : A ≝
    1313  (match b return λx.λ_. x = n → A with
    14     [ Empty ⇒
     14    [ VEmpty ⇒
    1515      (match t return λx.λ_. Z = x → A with
    1616        [ Leaf l ⇒ λ_.l
     
    1818        | Stub s ⇒ λ_.a
    1919        ])
    20     | Cons o hd tl ⇒
     20    | VCons o hd tl ⇒
    2121      match t return λx.λ_. (S o) = x → A with
    2222        [ Leaf l ⇒ λK.⊥
    2323        | Node h l r ⇒
    2424           match hd with
    25              [ true ⇒ λK. lookup A h (tl⌈h ↦ o⌉) r a
    26              | false ⇒ λK. lookup A h (tl⌈h ↦ o⌉) l a
     25             [ true ⇒ λK. lookup A h (tl⌈o ↦ h⌉) r a
     26             | false ⇒ λK. lookup A h (tl⌈o ↦ h⌉) l a
    2727             ]
    2828        | Stub s ⇒ λ_. a
     
    3636       : BitVectorTrie A n ≝
    3737   match b with
    38     [ Empty ⇒ Leaf A a
    39     | Cons o hd tl ⇒
     38    [ VEmpty ⇒ Leaf A a
     39    | VCons o hd tl ⇒
    4040      match hd with
    4141        [ true ⇒  Node A o (Stub A o) (prepare_trie_for_insertion A o tl a)
     
    4848                 BitVectorTrie A n → BitVectorTrie A n ≝
    4949  (match b with
    50     [ Empty ⇒ λ_. Leaf A a
    51     | Cons o hd tl ⇒ λt.
     50    [ VEmpty ⇒ λ_. Leaf A a
     51    | VCons o hd tl ⇒ λt.
    5252          match t return λy.λ_. S o = y → BitVectorTrie A (S o) with
    5353            [ Leaf l ⇒ λprf.⊥
    5454            | Node p l r ⇒ λprf.
    5555               match hd with
    56                 [ true ⇒  Node A o (l⌈o ↦ p⌉) (insert A o tl a (r⌈o ↦ p⌉))
    57                 | false ⇒ Node A o (insert A o tl a (l⌈o ↦ p⌉)) (r⌈o ↦ p⌉)
     56                [ true ⇒  Node A o (l⌈p ↦ o⌉) (insert A o tl a (r⌈p ↦ o⌉))
     57                | false ⇒ Node A o (insert A o tl a (l⌈p ↦ o⌉)) (r⌈p ↦ o⌉)
    5858                ]
    59             | Stub p ⇒ λprf. (prepare_trie_for_insertion A ? (Cons ? o hd tl) a)
     59            | Stub p ⇒ λprf. (prepare_trie_for_insertion A ? (hd:::tl) a)
    6060            ] (refl ? (S o))
    6161    ]).
Note: See TracChangeset for help on using the changeset viewer.