Changeset 2754 for src/ASM/Assembly.ma


Ignore:
Timestamp:
Mar 1, 2013, 10:26:31 AM (7 years ago)
Author:
sacerdot
Message:
  1. WARNING: I commented out one of James's function used in compiler.ma because it was undefined (partial commit). To be restored.
  2. The type of labelled_object_code programs now has a symbol table, used to generate the intensional events function call/return.
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2707 r2754  
    808808    ∀sigma: Word → Word.
    809809    ∀policy: Word → bool.
    810       Σres:list Byte × (BitVectorTrie costlabel 16).
     810      Σres:labelled_object_code.
    811811       sigma_policy_specification p sigma policy →
    812812       let 〈preamble,instr_list〉 ≝ p in
     
    871871    in
    872872     〈reverse … revcode,
    873       fold … (λppc.λcost.λpc_to_costs. insert … (sigma ppc) cost pc_to_costs) ppc_to_costs (Stub ??)〉.
     873      〈fold … (λppc.λcost.λpc_to_costs. insert … (sigma ppc) cost pc_to_costs) ppc_to_costs (Stub ??),
     874       foldl ??
     875        (λsymboltable,newident_oldident.
     876          let ppc ≝ lookup_labels (\fst newident_oldident) in
     877           insert … (sigma ppc) (\snd newident_oldident) symboltable) (Stub ??) (\snd preamble)〉〉.
    874878  [ cases (foldl_strong ? (λx.Σy.?) ???) in p1; #ignore_revcode #Hfold #EQignore_revcode
    875879    >EQignore_revcode in Hfold; #Hfold #sigma_pol_ok #instr_list_ok
     
    10281032
    10291033definition assembly_unlabelled_program:
    1030     assembly_program → option (list Byte × (BitVectorTrie Identifier 16))
     1034    assembly_program → option labelled_object_code
    10311035  λp.
    1032     Some … (〈foldr … (λi,l. assembly1 i @ l) [ ] p, Stub …〉).
     1036    Some … (〈foldr … (λi,l. assembly1 i @ l) [ ] p, 〈Stub …, Stub …〉〉).
Note: See TracChangeset for help on using the changeset viewer.