Changeset 1311 for Deliverables/D3.3/id-lookup-branch/ERTL/ERTL.ma

Timestamp:

Oct 6, 2011, 6:45:54 PM (10 years ago)

Author:

campbell

Message:

Merge trunk to invariants branch, sorting out the handling of temporaries
in Clight/toCminor.

Location:

Deliverables/D3.3/id-lookup-branch

Files:

• . (modified) (1 prop)
• ERTL/ERTL.ma (modified) (2 diffs)

Deliverables/D3.3/id-lookup-branch/ERTL/ERTL.ma

@@ -1 @@
-include "ASM/I8051.ma".
 include "joint/Joint.ma".
-include "utilities/BitVectorTrieSet.ma".
-include "utilities/IdentifierTools.ma".
-include "common/Graphs.ma".
-include "common/CostLabel.ma".
-include "common/Registers.ma".
-
-definition registers ≝ list register.
 
 inductive move_registers: Type[0] ≝
@@ -14 +6 @@
                   
 inductive ertl_statement_extension: Type[0] ≝
-  | ertl_st_ext_new_frame: label → ertl_statement_extension
-  | ertl_st_ext_del_frame: label → ertl_statement_extension
-  | ertl_st_ext_frame_size: register → label → ertl_statement_extension.
+  | ertl_st_ext_new_frame: ertl_statement_extension
+  | ertl_st_ext_del_frame: ertl_statement_extension
+  | ertl_st_ext_frame_size: register → ertl_statement_extension.
 
-definition ertl_params: params ≝
- mk_params
-   register register register register
-     (move_registers × move_registers) register
-       ertl_statement_extension unit (list register) nat.
+definition ertl_params__: params__ ≝
+ mk_params__ register register register register (move_registers × move_registers)
+  register nat unit ertl_statement_extension.
+definition ertl_params_: params_ ≝ graph_params_ ertl_params__.
+definition ertl_params0: params0 ≝ mk_params0 ertl_params__ unit nat.
+definition ertl_params1: params1 ≝ rtl_ertl_params1 ertl_params0.
+definition ertl_params: ∀globals. params globals ≝ rtl_ertl_params ertl_params0.
 
-definition ertl_statement ≝ joint_statement ertl_params.
+definition ertl_statement ≝ joint_statement ertl_params_.
 
-definition ertl_statement_graph ≝ λglobals. graph (ertl_statement globals).
+definition ertl_internal_function ≝
+  λglobals.joint_internal_function … (ertl_params globals).
 
-record ertl_internal_function (globals: list ident): Type[0] ≝
-{
-  ertl_if_luniverse: universe LabelTag;
-  ertl_if_runiverse: universe RegisterTag;
-  ertl_if_params: nat;
-  ertl_if_locals: registers;
-  ertl_if_stacksize: nat;
-  ertl_if_graph: ertl_statement_graph globals;
-  ertl_if_entry: Σl: label. lookup ? ? ertl_if_graph l ≠ None ?;
-  ertl_if_exit: Σl: label. lookup ? ? ertl_if_graph l ≠ None ?
-}.
-
-definition set_luniverse ≝
-  λglobals  : list ident.
-  λint_fun  : ertl_internal_function globals.
-  λluniverse: universe LabelTag.
-  let runiverse ≝ ertl_if_runiverse globals int_fun in
-  let params    ≝ ertl_if_params globals int_fun in
-  let locals    ≝ ertl_if_locals globals int_fun in
-  let stacksize ≝ ertl_if_stacksize globals int_fun in
-  let graph     ≝ ertl_if_graph globals int_fun in
-  let entry     ≝ ertl_if_entry globals int_fun in
-  let exit      ≝ ertl_if_exit globals int_fun in
-    mk_ertl_internal_function globals
-      luniverse runiverse params locals
-      stacksize graph entry exit.
-
-definition ertl_function ≝ λglobals. fundef (ertl_internal_function globals).
-  
-record ertl_program (globals: list ident): Type[0] ≝
-{
-  ertl_pr_vars: list (ident × nat);
-  ertl_pr_funcs: list (ident × (ertl_function globals));
-  ertl_pr_main: option ident
-}.
-
-
-(* XXX: changed from O'Caml
-  | ertl_st_addr_h: register → ident → label → ertl_statement
-  | ertl_st_addr_l: register → ident → label → ertl_statement
-*)
-
-(* XXX: changed from O'Caml
-  | ertl_st_opaccs_a: OpAccs → register → register → register → label → ertl_statement
-  | ertl_st_opaccs_b: OpAccs → register → register → register → label → ertl_statement
-*)
+definition ertl_program ≝ joint_program ertl_params.