Changeset 833 for src/ASM/Assembly.ma


Ignore:
Timestamp:
May 24, 2011, 11:19:53 PM (8 years ago)
Author:
sacerdot
Message:

Bug fixed to make the file compile.
But the type of the assembly function is no more right.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r832 r833  
    636636  ].
    637637
    638 check lookup.
    639 
    640638definition assembly ≝
    641639  λp.
     
    653651        let lookup_labels ≝ λx. lookup ? ? x labels (zero ?) in
    654652        let lookup_datalabels ≝ λx. lookup ? ? x datalabels (zero ?) in
    655         let to_flatten ≝ map ? ? (λx. assembly_1_pseudoinstruction p pc lookup_labels lookup_datalabels x) instr_list in
    656         (*
    657           foldr ? ? (λx. λy.
     653        let to_flatten ≝
     654         map ? ? (λx. assembly_1_pseudoinstruction p pc lookup_labels lookup_datalabels (\snd x)) instr_list
     655        in
     656         foldr ? ? (λx. λy.
    658657            match y with
    659658            [ None ⇒ None ?
     
    663662              | Some x ⇒ Some ? (x @ lst)
    664663              ]
    665             ]) (Some ? [ ]) to_flatten *) ?
    666       ]
    667     ].
    668    
    669 (*
    670         if  then (* 65536 *)
    671           None ?
    672         else
    673           let flat_list ≝ flatten ? (
    674             map ? ? (
    675               assembly_1_pseudoinstruction (
    676                 λx. lookup ? ? x labels (zero ?))
    677                   (λx. lookup ? ? x datalabels (zero ?))
    678                   (address_of labels)) instr_list) in
    679           Some (list ? × (BitVectorTrie ? ?)) 〈flat_list, costs〉
    680 *)
    681 
    682 (*
    683   [2,3,4,5,6:
    684     normalize; %;
    685   | whd in ⊢ (? (? ? ? %));
    686       cases (split bool 8 8 (lookup Word 16 trgt labels (zero 16)))
    687       # high
    688       # low
    689       whd in ⊢ (? (? ? ? %))
    690       cases (eq_bv 8 high (zero 8))
    691       [ normalize
    692         %
    693       | elim not_implemented;
    694       ]
    695   ]
    696 qed. *)
    697 
    698 
     664            ]) (Some ? [ ]) to_flatten ]].
    699665
    700666definition assembly_unlabelled_program: assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
Note: See TracChangeset for help on using the changeset viewer.