Changeset 1280 for src/joint

Timestamp:

Sep 28, 2011, 2:43:37 AM (8 years ago)

Author:

sacerdot

Message:

Some progress in the porting of RTLAbstoRTL to the joint syntax:

1) common code with RTLtoERTL factorized out in joint/TranslateUtils.ma
2) this required yet another refactoring of the parameters in Joint.ma
3) RTLtoERTL ported to the new parameters; LTLtoLIN and LINtoASM are

probably broken but easily fixable a.t.m. RTLAbstoRTL still in progress,
but the difficult part is almost done.

Location:

src/joint

Files:

• Joint.ma (modified) (4 diffs)
• TranslateUtils.ma (added)

src/joint/Joint.ma

@@ -17 +17 @@
  
  ; extend_statements: Type[0]
- 
- ; resultT: Type[0]
- ; localsT: Type[0]
- ; paramsT: Type[0]
  }.
 
@@ -27 +23 @@
  ; succ: Type[0]
  }.
+
+(* One common instantiation of params via Graphs of joint_statements
+   (all languages but LIN) *)
+definition graph_params_ : params__ → params_ ≝
+ λpars__. mk_params_ pars__ label.
 
 inductive joint_instruction (p:params__) (globals: list ident): Type[0] ≝
@@ -52 +53 @@
   | joint_st_return: joint_statement p globals.
 
+record params0: Type[1] ≝
+ { pars__' :> params__
+ ; resultT: Type[0]
+ ; paramsT: Type[0]
+ }.
+
+record params1 : Type[1] ≝
+ { pars0 :> params0
+ ; localsT: Type[0]
+ }.
 
 record params (globals: list ident): Type[1] ≝
- { pars_:> params_
+ { succ_ : Type[0]
+ ; pars1 :> params1
  ; codeT: Type[0]
- ; lookup: codeT → label → option (joint_statement pars_ globals)
+ ; lookup: codeT → label → option (joint_statement (mk_params_ pars1 succ_) globals)
  }.
+ 
+definition params__of_params: ∀globals. params globals → params_ ≝
+ λglobals,pars. mk_params_ pars (succ_ … pars).
+coercion params__of_params: ∀globals.∀p: params globals. params_ ≝ params__of_params
+ on _p: params ? to params_.
 
 include alias "common/Graphs.ma". (* To pick the right lookup *)
 
-(* One common instantiation of params via Graphs of joint_statements *)
-definition graph_params: params_ → ∀globals: list ident. params globals ≝
- λparams_,globals. mk_params globals params_ (graph (joint_statement params_ globals)) (lookup …).
+(* One common instantiation of params via Graphs of joint_statements
+   (all languages but LIN) *)
+definition graph_params: params1 → ∀globals: list ident. params globals ≝
+ λpars1,globals.
+  mk_params globals label pars1
+   (graph (joint_statement (graph_params_ pars1) globals)) (lookup …).
+
+
+(* CSC: special case where localsT is a list of register (RTL and ERTL) *)
+definition rtl_ertl_params1 ≝ λpars0. mk_params1 pars0 (list register).
+definition rtl_ertl_params ≝ λpars0. graph_params (rtl_ertl_params1 pars0).
 
 record joint_internal_function (globals: list ident) (p:params globals) : Type[0] ≝
@@ -123 +148 @@
 (* Specialized for graph_params *)
 definition add_graph ≝
-  λpars_,globals.λl:label.λstmt.λp:joint_internal_function globals (graph_params pars_ globals).
+  λpars1,globals.λl:label.λstmt.λp:joint_internal_function globals (graph_params pars1 globals).
    let code ≝ add … (joint_if_code ?? p) l stmt in
-    mk_joint_internal_function … (graph_params pars_ globals)
+    mk_joint_internal_function … (graph_params … globals)
      (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
      (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)