Changeset 1479 for src/ASM


Ignore:
Timestamp:
Nov 2, 2011, 8:27:30 AM (8 years ago)
Author:
boender
Message:
  • added insert_lookup_opt
  • assembly compiles now
Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r1459 r1479  
    10001000definition jump_expansion': pseudo_assembly_program → policy_type ≝
    10011001 λprogram.λpc.
    1002   let policy ≝ jump_expansion_internal (\snd program) in
     1002  let policy ≝ jump_expansion_internal (\snd program) (|\snd program|) in
    10031003  let 〈n,j〉 ≝ lookup ? ? pc policy 〈0, long_jump〉 in
    10041004    j.
  • src/ASM/BitVectorTrie.ma

    r1474 r1479  
    464464qed.
    465465
     466lemma insert_lookup_opt:
     467 ∀A:Type[0].∀v,a:A.∀n.∀c,b:BitVector n.∀t:BitVectorTrie A n.
     468   lookup_opt … b (insert … c v t) = Some A a → lookup_opt … b t = Some A a ∨ a = v.
     469 #A #v #a #n #c elim c -c; -n;
     470 [ #b #t #Hl normalize in Hl; %2 destruct (Hl) @refl
     471 | #n #hd #tl #Hind #b cases (BitVector_Sn … b) #hd' * #tl' #Heq >Heq
     472   #t cases (BitVectorTrie_Sn … t)
     473   [ * #l * #r #Heq2 >Heq2 cases hd cases hd' #H normalize in H; normalize
     474     [1,4: @(Hind tl' ? H)
     475     |2,3: %1 @H
     476     ]
     477   | #Heq2 >Heq2 cases hd cases hd' #H normalize in H; normalize
     478     [1,4: lapply (refl ? (eq_bv ? tl' tl)) cases (eq_bv ? tl' tl) in ⊢ (???% → %) #Heq3
     479       [1,3: >(eq_bv_eq … Heq3) in H; >lookup_opt_prepare_trie_for_insertion_hit #X destruct (X) %2 //
     480       |2,4: >(lookup_opt_prepare_trie_for_insertion_miss) in H
     481         [1,3: #X %1 //
     482         |2,4: >Heq3 //
     483         ]
     484       ]
     485     |2,3: destruct (H)
     486     ]
     487qed.
     488
    466489lemma forall_insert_inv1:
    467490  ∀A.∀n.∀b.∀a.∀t.∀P.
Note: See TracChangeset for help on using the changeset viewer.