Changeset 1182 for src/joint

Timestamp:

Sep 5, 2011, 1:23:20 PM (10 years ago)

Author:

mulligan

Message:

changes to semantics: removing parameterised "next" element in joint params (representing labels) as these are actually fixed across ertl, ltl and lin.

Location:

src/joint

Files:

• Joint.ma (modified) (4 diffs)
• semantics.ma (modified) (3 diffs)

src/joint/Joint.ma

@@ -6 +6 @@
 
 record params: Type[1] ≝
- { next: Type[0]
+{ 
+  acc_a_reg: Type[0];
+  acc_b_reg: Type[0];
+  dpl_reg: Type[0];
+  dph_reg: Type[0];
+  pair_reg: Type[0];
+  generic_reg: Type[0];
  
- ; acc_a_reg: Type[0]
- ; acc_b_reg: Type[0]
- ; dpl_reg: Type[0]
- ; dph_reg: Type[0]
- ; pair_reg: Type[0]
- ; generic_reg: Type[0]
+  extend_statements: Type[0];
  
- ; extend_statements: Type[0]
- 
- ; resultT: Type[0]
- ; localsT: Type[0]
- ; paramsT: Type[0]
- }.
+  resultT: Type[0];
+  localsT: Type[0];
+  paramsT: Type[0]
+}.
 
 inductive joint_instruction (p:params) (globals: list ident): Type[0] ≝
@@ -38 +37 @@
   | joint_instr_store: dpl_reg p → dph_reg p → acc_a_reg p → joint_instruction p globals
   | joint_instr_call_id: ident → nat → joint_instruction p globals
-  | joint_instr_cond: acc_a_reg p → next p → joint_instruction p globals.
+  | joint_instr_cond: acc_a_reg p → label → joint_instruction p globals.
 
 inductive joint_statement (p:params) (globals: list ident): Type[0] ≝
-  | joint_st_sequential: joint_instruction p globals → next p → joint_statement p globals
-  | joint_st_goto: next p → joint_statement p globals
+  | joint_st_sequential: joint_instruction p globals → label → joint_statement p globals
+  | joint_st_goto: label → joint_statement p globals
   | joint_st_return: joint_statement p globals
   | joint_st_extension: extend_statements p → joint_statement p globals.
@@ -48 +47 @@
 record sem_params_ (preparams: params) (globals: list ident): Type[1] ≝
  { pmemoryT: Type[0]
- ; lookup: pmemoryT → next preparams → option (joint_statement preparams globals)
+ ; lookup: pmemoryT → label → option (joint_statement preparams globals)
  }.
 
@@ -60 +59 @@
   joint_if_stacksize: nat;
   joint_if_graph    : pmemoryT … p;
-  joint_if_entry    : Σl: next pre. lookup … p joint_if_graph l ≠ None ?;
-  joint_if_exit     : Σl: next pre. lookup … p joint_if_graph l ≠ None ?
+  joint_if_entry    : Σl: label. lookup … p joint_if_graph l ≠ None ?;
+  joint_if_exit     : Σl: label. lookup … p joint_if_graph l ≠ None ?
 }.
 

src/joint/semantics.ma

@@ -37 +37 @@
 *)
 (* CSC: ??? *)
-axiom address_of_label: ∀p. mem → next p → address.
-axiom address_chunks_of_label: ∀p. mem → next p → Byte × Byte.
+axiom address_of_label: mem → label → address.
+axiom address_chunks_of_label: mem → label → Byte × Byte.
 axiom label_of_address_chunks: Byte → Byte → label.
 axiom address_of_address_chunks: Byte → Byte → address.
@@ -106 +106 @@
 
 (* CSC: was build_state in RTL *)
-definition goto: ∀p:sem_params. next p → state p → state p ≝
+definition goto: ∀p:sem_params. label → state p → state p ≝
  λp,l,st. set_pc … (address_of_label … (m … st) l) st.
 
@@ -188 +188 @@
    (λv. bind ?? (Byte_of_val v) (λv. OK ? 〈st,v〉)).
 
-definition save_ra : ∀p. state p → next p → res (state p) ≝
+definition save_ra : ∀p. state p → label → res (state p) ≝
  λp,st,l.
   let 〈addrl,addrh〉 ≝ address_chunks_of_label … (m … st) l in