Ignore:
Timestamp:
Apr 28, 2011, 10:55:47 AM (9 years ago)
Author:
campbell
Message:

Add merging of tries and identifier sets (based on Dominic's earlier code).
Not used at present (I decided to implement the part that would have used it
differently).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVectorTrie.ma

    r761 r779  
    100100  ]
    101101qed.
     102
     103let rec merge (A: Type[0]) (n: nat) (b: BitVectorTrie A n) on b: BitVectorTrie A n → BitVectorTrie A n ≝
     104  match b return λx. λ_. BitVectorTrie A x → BitVectorTrie A x with
     105  [ Stub _ ⇒ λc. c
     106  | Leaf l ⇒ λc. match c with [ Leaf a ⇒ Leaf ? a | _ ⇒ Leaf ? l ]
     107  | Node p l r ⇒
     108    λc.
     109    (match c return λx. λ_. x = (S p) → BitVectorTrie A (S p) with
     110    [ Node p' l' r' ⇒ λprf. Node ? ? (merge ?? l (l'⌈p' ↦ p⌉)) (merge ?? r (r'⌈p' ↦ p⌉))
     111    | Stub _ ⇒ λprf. Node ? p l r
     112    | Leaf _ ⇒ λabsd. ?
     113    ] (refl ? (S p)))
     114  ].
     115  [1:
     116      destruct(absd)
     117  |2,3:
     118      @ injective_S
     119        assumption
     120  ]
     121qed.
Note: See TracChangeset for help on using the changeset viewer.