Changeset 2910 for src/ASM/ASMCosts.ma


Ignore:
Timestamp:
Mar 19, 2013, 11:19:32 PM (7 years ago)
Author:
sacerdot
Message:

Abstract statuses for ASM and OC completed.
A simple test program can now be run in every pass of the compiler, always
showing the same behaviour (up to initialization).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r2907 r2910  
    2525qed.
    2626
     27definition OC_as_call_ident:
     28 ∀prog:labelled_object_code.∀cm. (Σs:Status cm. OC_classify … s = cl_call) → ident
     29
     30 λprog,cm,s0.
     31  let pc ≝ program_counter ?? (execute_1' cm s0) in
     32  match lookup_opt ?? pc (symboltable prog) with
     33  [ None ⇒ ⊥ | Some id ⇒ id ].
     34cases daemon (*CSC: we need a specification of the symboltable for this *)
     35qed.
     36
    2737definition OC_abstract_status: labelled_object_code → abstract_status ≝
    2838 λprog.
     
    3747      (next_instruction_properly_relates_program_counters code_memory)
    3848      (λst. as_result_of_finaladdr … st (final_pc prog))
    39       ?
     49      (OC_as_call_ident prog …)
    4050      ?.
    41   #x cases daemon (* XXX: (tail)call_ident function *)
     51 * #st whd in ⊢ (??%? → ?); cases current_instruction [7: *] normalize
     52 try (#x #y #abs) try (#x #abs) try #abs destruct
    4253qed.
    4354
Note: See TracChangeset for help on using the changeset viewer.