Changeset 2286 for src/joint/Traces.ma


Ignore:
Timestamp:
Aug 2, 2012, 3:18:11 PM (8 years ago)
Author:
tranquil
Message:

Big update!

  • merge of all _paolo variants
  • reorganised some depends (in particular, Register and thus back-end laguages no longer have fake ASM dependency)
  • split I8051.ma spawning new BackEndOps?.ma

compiler.ma broken at the moment, but not by these changes as far as I can tell

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Traces.ma

    r2186 r2286  
    1 include "joint/semantics_paolo.ma".
     1include "joint/semantics.ma".
    22
    33record evaluation_params : Type[1] ≝
     
    55 ; sparams:> sem_params
    66 ; exit: cpointer
    7  ; ev_genv: genv globals sparams
     7 ; ev_genv: genv sparams globals
    88 ; io_env : state sparams → ∀o:io_out.res (io_in o)
    99 } .
     
    5858   (* as_pc_of ≝ *) (pc …)
    5959   (* as_classifier ≝ *)
    60     (λs,cl.∃stmt.fetch_statement ? p … (ev_genv p) (pc … s) = return stmt
     60    (λs,cl.∃fn,stmt.fetch_statement ? p … (ev_genv p) (pc … s) = return 〈fn,stmt〉
    6161     stmt_classifier … stmt = cl)
    6262   (* as_label_of_pc ≝ *)
    6363    (λpc.
    6464      match fetch_statement ? p … (ev_genv p) pc with
    65       [ OK stmt ⇒ cost_label_of_stmt … stmt
     65      [ OK fn_stmt ⇒ cost_label_of_stmt … (\snd fn_stmt)
    6666      | _ ⇒ None ?
    6767      ])
     
    6969    (λs1,s2.
    7070      (* Paolo: considering sequential calls, tailcalls must be classified as cl_return *)
    71       ∃stp,nxt.fetch_statement ? p … (ev_genv p) (pc … s1) = return (sequential ?? stp nxt)
     71      ∃fn,stp,nxt.fetch_statement ? p … (ev_genv p) (pc … s1) = return 〈fn,sequential ?? stp nxt〉
    7272      succ_pc p p (pc … s1) nxt = return pc … s2)
    7373   (* as_final ≝ *) (λs.is_final (globals ?) p (ev_genv p) (exit p) s ≠ None ?).
Note: See TracChangeset for help on using the changeset viewer.