Ignore:
Timestamp:
Dec 15, 2010, 6:38:59 PM (9 years ago)
Author:
mulligan
Message:
  • README updated
  • Test and DoTest? fixed to work on assembly_program
  • assembly function for labelled programs avoided because of efficiency issues
File:
1 edited

Legend:

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

    r425 r431  
    431431nqed.
    432432
    433 ndefinition assembly: assembly_program → Maybe (List Byte × (BitVectorTrie String sixteen)) ≝
     433ndefinition assembly0: assembly_program → Maybe (List Byte × (BitVectorTrie String sixteen)) ≝
    434434  λp.
    435435    let 〈preamble, instr_list〉 ≝ p in
     
    508508          ) in
    509509        Just (List ? × (BitVectorTrie ? ?)) 〈flat_list, costs〉.
    510   ##[##2,3,4,5,6: nnormalize; //;
     510  ##[##2,3,4,5,6: nnormalize; @;
    511511  ##| nwhd in ⊢ (? (? ? ? %));
    512512      ncases (less_than_b (nat_of_bitvector eight ?) two_hundred_and_fifty_six)
    513         [ nnormalize; //;
     513        [ nnormalize; @;
    514514      ##| nnormalize;
    515515          nelim not_implemented;
     
    518518nqed.
    519519
    520 (*
    521 ndefinition assembly: List instruction → List Byte ≝
    522  fold_right … (λi,l. assembly1 i @ l) [].
    523 *)
     520ndefinition assembly: assembly_program → Maybe (List Byte × (BitVectorTrie String sixteen)) ≝
     521 λp: assembly_program.
     522  Just ? (〈fold_right ?? (λi,l.
     523   match i with [ Instruction i ⇒ assembly1 i @ l | _ ⇒ l] ) [ ] (second ?? p), Stub …〉).
Note: See TracChangeset for help on using the changeset viewer.