Ignore:
Timestamp:
Jan 20, 2011, 6:10:07 PM (9 years ago)
Author:
mulligan
Message:

Moved over to standard library.

File:
1 edited

Legend:

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

    r437 r465  
    1010     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
    1111      [ ADDR11 w ⇒ λ_.
    12          let 〈v1,v2〉 ≝ split ? (S (S (S Z))) (S (S (S (S (S (S (S (S Z)))))))) w in
     12         let 〈v1,v2〉 ≝ split ? (S (S (S O))) (S (S (S (S (S (S (S (S O)))))))) w in
    1313          [ (v1 @@ [[true; false; false; false; true]]) ; v2 ]
    1414      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
     
    3030     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
    3131      [ ADDR11 w ⇒ λ_.
    32          let 〈v1,v2〉 ≝ split ?  (S (S (S Z))) (S (S (S (S (S (S (S (S Z)))))))) w in
     32         let 〈v1,v2〉 ≝ split ?  (S (S (S O))) (S (S (S (S (S (S (S (S O)))))))) w in
    3333          [ (v1 @@ [[false; false; false; false; true]]) ; v2 ]
    3434      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
    3535  | ANL addrs ⇒
    3636     match addrs with
    37       [ Left addrs ⇒ match addrs with
    38          [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     37      [ inl addrs ⇒ match addrs with
     38         [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    3939           match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
    4040            [ REGISTER r ⇒ λ_.[ ([[false;true;false;true;true]]) @@ r ]
     
    4343            | DATA b1 ⇒ λ_. [ ([[false;true;false;true;false;true;false;false]]) ; b1 ]
    4444            | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
    45          | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     45         | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    4646            let b1 ≝
    4747             match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
     
    5353             | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
    5454         ]
    55       | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     55      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    5656         match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with
    5757          [ BIT_ADDR b1 ⇒ λ_.[ ([[true;false;false;false;false;false;true;false]]) ; b1 ]
     
    157157           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr3) in
    158158         match addrs with
    159           [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     159          [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    160160             match addr2 return λx. bool_to_Prop (is_in ? [[direct;data]] x) → ? with
    161161              [ DIRECT b1 ⇒ λ_.
     
    164164                 [ ([[true; false; true; true; false; true; false; false]]); b1; b3 ]
    165165              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
    166           | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     166          | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    167167             let b2 ≝
    168168              match addr2 return λx. bool_to_Prop (is_in ? [[data]] x) → ? with
    169169               [ DATA b2 ⇒ λ_. b2
    170170               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
    171              match addr1 return λx. bool_to_Prop (is_in ? [[register;indirect]] x) → List Byte with
     171             match addr1 return λx. bool_to_Prop (is_in ? [[register;indirect]] x) → list Byte with
    172172              [ REGISTER r⇒ λ_.
    173173                 [ ([[true; false; true; true; true]]) @@ r; b2; b3 ]
     
    193193     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
    194194      [ ADDR16 w ⇒ λ_.
    195          let 〈b1,b2〉 ≝ split ? (S (S (S (S (S (S (S (S Z)))))))) (S (S (S (S (S (S (S (S Z)))))))) w in
     195         let 〈b1,b2〉 ≝ split ? (S (S (S (S (S (S (S (S O)))))))) (S (S (S (S (S (S (S (S O)))))))) w in
    196196          [ ([[false;false;false;true;false;false;true;false]]); b1; b2 ]         
    197197      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
     
    199199     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
    200200      [ ADDR16 w ⇒ λ_.
    201          let 〈b1,b2〉 ≝ split ? (S (S (S (S (S (S (S (S Z)))))))) (S (S (S (S (S (S (S (S Z)))))))) w in
     201         let 〈b1,b2〉 ≝ split ? (S (S (S (S (S (S (S (S O)))))))) (S (S (S (S (S (S (S (S O)))))))) w in
    202202          [ ([[false;false;false;false;false;false;true;false]]); b1; b2 ]         
    203203      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
    204204  | MOV addrs ⇒
    205205     match addrs with
    206       [ Left addrs ⇒
     206      [ inl addrs ⇒
    207207         match addrs with
    208           [ Left addrs ⇒
     208          [ inl addrs ⇒
    209209             match addrs with
    210               [ Left addrs ⇒
     210              [ inl addrs ⇒
    211211                 match addrs with
    212                   [ Left addrs ⇒
     212                  [ inl addrs ⇒
    213213                     match addrs with
    214                       [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     214                      [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    215215                         match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
    216216                          [ REGISTER r ⇒ λ_.[ ([[true;true;true;false;true]]) @@ r ]
     
    219219                          | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;false;false]]) ; b1 ]
    220220                          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
    221                       | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     221                      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    222222                         match addr1 return λx. bool_to_Prop (is_in ? [[register;indirect]] x) → ? with
    223223                          [ REGISTER r ⇒ λ_.
     
    234234                              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
    235235                          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
    236                   | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     236                  | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    237237                     let b1 ≝
    238238                      match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
     
    246246                      | DATA b2 ⇒ λ_. [ ([[false;true;true;true;false;true;false;true]]); b1; b2 ]
    247247                      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
    248               | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     248              | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    249249                 match addr2 return λx. bool_to_Prop (is_in ? [[data16]] x) → ? with
    250250                  [ DATA16 w ⇒ λ_.
    251                      let 〈b1,b2〉 ≝ split ? (S (S (S (S (S (S (S (S Z)))))))) (S (S (S (S (S (S (S (S Z)))))))) w in
     251                     let 〈b1,b2〉 ≝ split ? (S (S (S (S (S (S (S (S O)))))))) (S (S (S (S (S (S (S (S O)))))))) w in
    252252                      [ ([[true;false;false;true;false;false;false;false]]); b1; b2]
    253253                  | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
    254           | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     254          | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    255255             match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
    256256              [ BIT_ADDR b1 ⇒ λ_.
    257257                 [ ([[true;false;true;false;false;false;true;false]]); b1 ]
    258258              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
    259       | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     259      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    260260         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
    261261          [ BIT_ADDR b1 ⇒ λ_.
     
    271271  | MOVX addrs ⇒
    272272     match addrs with
    273       [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     273      [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    274274         match addr2 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with
    275275          [ EXT_INDIRECT i1 ⇒ λ_.
     
    278278             [ ([[true;true;true;false;false;false;false;false]]) ]
    279279          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
    280       | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     280      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    281281         match addr1 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with
    282282          [ EXT_INDIRECT i1 ⇒ λ_.
     
    291291  | ORL addrs ⇒
    292292     match addrs with
    293       [ Left addrs ⇒
     293      [ inl addrs ⇒
    294294         match addrs with
    295           [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     295          [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    296296             match addr2 return λx. bool_to_Prop (is_in ? [[register;data;direct;indirect]] x) → ? with
    297297             [ REGISTER r ⇒ λ_.[ ([[false;true;false;false;true]]) @@ r ]
     
    300300             | DATA b1 ⇒ λ_. [ ([[false;true;false;false;false;true;false;false]]) ; b1 ]
    301301             | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
    302           | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     302          | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    303303            let b1 ≝
    304304              match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
     
    311311                 [ ([[false;true;false;false;false;false;true;true]]); b1; b2 ]
    312312              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
    313       | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in     
     313      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in     
    314314         match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with
    315315          [ BIT_ADDR b1 ⇒ λ_.
     
    381381  | XRL addrs ⇒
    382382     match addrs with
    383       [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     383      [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    384384         match addr2 return λx. bool_to_Prop (is_in ? [[data;register;direct;indirect]] x) → ? with
    385385          [ REGISTER r ⇒ λ_.
     
    392392             [ ([[false;true;true;false;false;true;false;false]]); b1]
    393393          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
    394       | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     394      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    395395         let b1 ≝
    396396          match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
     
    419419      ].
    420420
    421 ndefinition address_of: BitVectorTrie (BitVector eight) eight → String → addressing_mode ≝
    422     λmap: BitVectorTrie (BitVector eight) eight.
     421ndefinition address_of: BitVectorTrie (BitVector 8) 8 → String → addressing_mode ≝
     422    λmap: BitVectorTrie (BitVector 8) 8.
    423423    λstring: String.
    424424      let address ≝ lookup … (bitvector_of_string … string) map (zero ?) in
    425425      let address_bv ≝ nat_of_bitvector ? address in
    426         if less_than_b address_bv two_hundred_and_fifty_six then
     426        if leb address_bv 256 then
    427427          RELATIVE address
    428428        else
     
    431431nqed.
    432432
    433 ndefinition assembly: assembly_program → Maybe (List Byte × (BitVectorTrie String sixteen)) ≝
     433ndefinition assembly: assembly_program → option (list Byte × (BitVectorTrie String 16)) ≝
    434434  λp.
    435435    let 〈preamble, instr_list〉 ≝ p in
    436436    let 〈datalabels, ignore〉 ≝
    437       fold_left ((BitVectorTrie (BitVector sixteen) sixteen) × Nat) ? (
     437      foldl ((BitVectorTrie (BitVector 16) 16) × nat) ? (
    438438        λt. λpreamble.
    439439          let 〈datalabels, addr〉 ≝ t in
    440440          let 〈name, size〉 ≝ preamble in
    441           let addr_sixteen ≝ bitvector_of_nat sixteen addr in
     441          let addr_sixteen ≝ bitvector_of_nat 16 addr in
    442442            〈insert ? ? (bitvector_of_string ? name) addr_sixteen datalabels, addr + size〉)
    443               〈(Stub ? ?), Z〉 preamble in
     443              〈(Stub ? ?), O〉 preamble in
    444444    let 〈pc_labels, costs〉 ≝
    445       fold_left ((Nat × (BitVectorTrie ? ?)) × (BitVectorTrie ? ?)) ? (
     445      foldl ((nat × (BitVectorTrie ? ?)) × (BitVectorTrie ? ?)) ? (
    446446        λt. λi.
    447447          let 〈pc_labels, costs〉 ≝ t in
     
    450450              [ Instruction instr ⇒
    451451                let code_memory ≝ load_code_memory (assembly1 instr) in
    452                 let 〈instr_pc', ignore〉 ≝ fetch code_memory (zero sixteen) in
     452                let 〈instr_pc', ignore〉 ≝ fetch code_memory (zero 16) in
    453453                let 〈instr', program_counter'〉 ≝ instr_pc' in
    454454                let program_counter_n' ≝ nat_of_bitvector ? program_counter' in
     
    456456              | Label label ⇒
    457457                let program_counter_bv ≝ bitvector_of_nat ? program_counter in
    458                   〈〈program_counter, (insert ? ? (bitvector_of_string eight label) program_counter_bv labels)〉, costs〉
     458                  〈〈program_counter, (insert ? ? (bitvector_of_string 8 label) program_counter_bv labels)〉, costs〉
    459459              | Cost cost ⇒
    460460                let program_counter_bv ≝ bitvector_of_nat ? program_counter in
    461461                  〈pc_labels, (insert ? ? program_counter_bv cost costs)〉
    462462              | Jmp jmp ⇒
    463                   〈〈program_counter + three, labels〉, costs〉
     463                  〈〈program_counter + 3, labels〉, costs〉
    464464              | Call call ⇒
    465                   〈〈program_counter + three, labels〉, costs〉
     465                  〈〈program_counter + 3, labels〉, costs〉
    466466              | Mov dptr trgt ⇒ t
    467467              | WithLabel jmp ⇒
    468                 let fake_addr ≝ RELATIVE (zero eight) in
     468                let fake_addr ≝ RELATIVE (zero 8) in
    469469                let fake_jump ≝ assembly_jump jmp (λx: String. fake_addr) in
    470470                let code_memory ≝ load_code_memory (assembly1 fake_jump) in
    471                 let 〈instr_pc', ignore〉 ≝ fetch code_memory (zero sixteen) in
     471                let 〈instr_pc', ignore〉 ≝ fetch code_memory (zero 16) in
    472472                let 〈instr', program_counter'〉 ≝ instr_pc' in
    473                 let program_counter_n' ≝ nat_of_bitvector sixteen program_counter' in
     473                let program_counter_n' ≝ nat_of_bitvector 16 program_counter' in
    474474                  〈〈program_counter + program_counter_n', labels〉, costs〉
    475475              ]
    476           ) 〈〈Z, (Stub ? ?)〉, (Stub ? ?)〉 instr_list in
     476          ) 〈〈O, (Stub ? ?)〉, (Stub ? ?)〉 instr_list in
    477477    let 〈program_counter, labels〉 ≝ pc_labels in
    478       if greater_than_b program_counter
    479                         sixty_five_thousand_five_hundred_and_thirty_six then
    480         Nothing ?
     478      if gtb program_counter (2^16) then
     479        None ?
    481480      else
    482481        let flat_list ≝
     
    489488                  | Call call ⇒
    490489                    let pc_offset ≝ lookup ? ? (bitvector_of_string ? call) labels (zero ?) in
    491                     let pc_offset_pad ≝ (zero eight) @@ pc_offset in
     490                    let pc_offset_pad ≝ (zero 8) @@ pc_offset in
    492491                    let address ≝ ADDR16 pc_offset_pad in
    493492                      assembly1 (LCALL ? address)
     
    495494                    let pc_offset ≝ lookup ? ? (bitvector_of_string ? trgt) datalabels (zero ?) in
    496495                    let address ≝ DATA16 pc_offset in
    497                       assembly1 (MOV ? (Left ? ? (Left ? ? (Right ? ? 〈DPTR, address〉))))
     496                      assembly1 (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉))))
    498497                  | Instruction instr ⇒ assembly1 instr
    499498                  | Jmp jmp ⇒
    500499                    let pc_offset ≝ lookup ? ? (bitvector_of_string ? jmp) labels (zero ?) in
    501                     let pc_offset_pad ≝ (zero eight) @@ pc_offset in
     500                    let pc_offset_pad ≝ (zero 8) @@ pc_offset in
    502501                    let address ≝ ADDR16 pc_offset_pad in
    503502                      assembly1 (LJMP ? address)
     
    507506            ) instr_list
    508507          ) in
    509         Just (List ? × (BitVectorTrie ? ?)) 〈flat_list, costs〉.
     508        Some (list ? × (BitVectorTrie ? ?)) 〈flat_list, costs〉.
    510509  ##[##2,3,4,5,6: nnormalize; @;
    511510  ##| nwhd in ⊢ (? (? ? ? %));
    512       ncases (less_than_b (nat_of_bitvector eight ?) two_hundred_and_fifty_six)
     511      ncases (leb (nat_of_bitvector 8 ?) 256)
    513512        [ nnormalize; @;
    514513      ##| nnormalize;
     
    518517nqed.
    519518
    520 ndefinition assembly_unlabelled_program: List instruction → Maybe (List Byte × (BitVectorTrie String sixteen)) ≝
    521  λp.Just ? (〈fold_right ?? (λi,l. assembly1 i @ l) [ ] p, Stub …〉).
     519ndefinition assembly_unlabelled_program: list instruction → option (list Byte × (BitVectorTrie String 16)) ≝
     520 λp.Some ? (〈foldr ?? (λi,l. assembly1 i @ l) [ ] p, Stub …〉).
Note: See TracChangeset for help on using the changeset viewer.