Changeset 2756 for src/ASM/ASMCosts.ma


Ignore:
Timestamp:
Mar 1, 2013, 1:05:21 PM (7 years ago)
Author:
sacerdot
Message:

WARNING: this commit breaks things, sorry, Paolo is going to fix compiler.ma
in a minute...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r2710 r2756  
    1414    mk_abstract_status
    1515      (Status code_memory)
    16       (λs,s'. (execute_1 … s) = s')
     16      (λs. return (execute_1 … s))
     17      ?
    1718      word_deqset
    1819      (program_counter …)
    19       (λs. Some ? (ASM_classify … s))
     20      (ASM_classify …)
    2021      (λpc.lookup_opt … pc cost_labels)
    2122      (next_instruction_properly_relates_program_counters code_memory)
     
    162163          program_counter_after_other pc instruction.
    163164  #code_memory #cost_labels #start_status #classify_assm
    164   change with (Some ? (ASM_classify0 ?) = ?) in classify_assm;
     165  change with (ASM_classify0 ? = ?) in classify_assm;
    165166  destruct (classify_assm)
    166167  @execute_1_and_program_counter_after_other_in_lockstep0 assumption.
Note: See TracChangeset for help on using the changeset viewer.