Ignore:
Timestamp:
Apr 19, 2011, 12:22:32 PM (9 years ago)
Author:
campbell
Message:

Enforce the use of declared identifiers/registers in Cminor/RTLabs.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVectorTrie.ma

    r726 r761  
    11include "basics/types.ma".
    22
     3include "utilities/option.ma".
    34include "ASM/BitVector.ma".
    45
     
    7576  ]
    7677qed.
     78
     79let rec update (A: Type[0]) (n: nat) (b: BitVector n) (a: A) on b: BitVectorTrie A n → option (BitVectorTrie A n) ≝
     80  (match b with
     81    [ VEmpty ⇒ λt. match t return λy.λ_. O = y → option (BitVectorTrie A O) with
     82                   [ Leaf _ ⇒ λ_. Some ? (Leaf A a)
     83                   | Stub _ ⇒ λ_. None ?
     84                   | Node _ _ _ ⇒ λprf. ⊥
     85                   ] (refl ? O)
     86    | VCons o hd tl ⇒ λt.
     87          match t return λy.λ_. S o = y → option (BitVectorTrie A (S o)) with
     88            [ Leaf l ⇒ λprf.⊥
     89            | Node p l r ⇒ λprf.
     90               match hd with
     91                [ true ⇒  option_map ?? (λv. Node A o (l⌈p ↦ o⌉) v) (update A o tl a (r⌈p ↦ o⌉))
     92                | false ⇒ option_map ?? (λv. Node A o v (r⌈p ↦ o⌉)) (update A o tl a (l⌈p ↦ o⌉))
     93                ]
     94            | Stub p ⇒ λprf. None ?
     95            ] (refl ? (S o))
     96    ]).
     97  [ 1,2: destruct
     98  |*:
     99    @ injective_S @sym_eq @prf
     100  ]
     101qed.
Note: See TracChangeset for help on using the changeset viewer.