Changeset 2475 for src/ASM


Ignore:
Timestamp:
Nov 19, 2012, 5:13:21 PM (8 years ago)
Author:
campbell
Message:

Get compiler.ma and correctness.ma checking again. Note that the back-end
is in a state of flux at the moment, so is axiomatised out.

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1964 r2475  
    1313      word_deqset
    1414      (program_counter …)
    15       (λs,class. ASM_classify … s = class)
     15      (λs. ASM_classify … s)
    1616      (λpc.lookup_opt ?? pc cost_labels)
    1717      (next_instruction_properly_relates_program_counters code_memory)
     18      ?
    1819      ?.
    19   cases daemon (* XXX: is final predicate *)
     20  cases daemon (* XXX: is final predicate, call ident function *)
    2021qed.
    2122
  • src/ASM/ASMCostsSplit.ma

    r2001 r2475  
    2222    | Some lbl ⇒ λlookup_refl.
    2323      let cost ≝ block_cost code_memory program_counter cost_labels in
    24         cic:/matita/cerco/common/Identifiers/add.fix(0,2,2) ?? cost_mapping lbl cost
     24        cic:/matita/cerco/common/Identifiers/add.fix(0,2,3) ?? cost_mapping lbl cost
    2525    ] (refl … (lookup_opt … program_counter cost_labels))
    2626  ] (refl … program_size).
Note: See TracChangeset for help on using the changeset viewer.