Changeset 1299


Ignore:
Timestamp:
Oct 5, 2011, 9:53:29 PM (8 years ago)
Author:
sacerdot
Message:

Functions from RTL/semantics.ma generalized to work on every graph language
and moved into joint/SemanticUtils.ma.

Location:
src
Files:
1 added
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/semantics.ma

    r1298 r1299  
    1 include "joint/semantics.ma".
     1include "joint/SemanticUtils.ma".
    22(*
    33include "utilities/lists.ma".
     
    88*)
    99include "RTL/RTL.ma". (* CSC: syntax.ma in RTLabs *)
    10 
    11 (*CSC: XXXX; we need to create a brand new chunk per label, so that
    12   pointer operations on labels are not semantically valid!! *)
    13 axiom rtl_pointer_of_label: label → Σp:pointer. ptype p = Code.
    14 axiom rtl_label_of_pointer: pointer → res label.
    15 
    16 (*CSC: XXX This code is cut&paste from joint/semantics.ma, address_of_label.
    17   Maybe there is a better way to organize the code!!! *)
    18 definition rtl_succ_p: label → address → address.
    19  #l #_ generalize in match (refl … (beval_pair_of_pointer (rtl_pointer_of_label l)))
    20  cases (beval_pair_of_pointer (rtl_pointer_of_label l)) in ⊢ (???% → ?)
    21   [ #res #_ @res
    22   | #msg cases (rtl_pointer_of_label l) * * #q #com #off #E1 #E2 destruct ]
    23 qed.
    2410
    2511axiom rtl_pop_frame: unit → res unit.
     
    7460 λglobals.
    7561  mk_more_sem_params2 … rtl_more_sem_params rtl_init_locals
    76    (rtl_fetch_statement …) rtl_fetch_result rtl_fetch_external_args rtl_set_result
     62   (graph_fetch_statement …) rtl_fetch_result rtl_fetch_external_args rtl_set_result
    7763    (rtl_exec_extended …).
    7864
Note: See TracChangeset for help on using the changeset viewer.