Changeset 1246 for src/joint

Timestamp:

Sep 22, 2011, 2:50:44 AM (9 years ago)

Author:

sacerdot

Message:

Yet another change to Joint.ma to accomodate all passes.
The concrete memory representation for the code of internal functions is
back, at the price of more complexity in the definition of the parameters.

Note: I do not understand any more the well_formed_P invariant for LIN code.
Moreover, the invariant does not seem to hold for code produced using LTLToLin.

Location:

src/joint

Files:

• Joint.ma (modified) (7 diffs)
• semantics.ma (modified) (1 diff)

src/joint/Joint.ma

@@ -5 +5 @@
 include "common/Graphs.ma".
 
-record params_: Type[1] ≝
+record params__: Type[1] ≝
  { acc_a_reg: Type[0]
  ; acc_b_reg: Type[0]
@@ -20 +20 @@
  }.
 
-record params: Type[1] ≝
- { pars_:> params_
+record params_: Type[1] ≝
+ { pars__:> params__
  ; succ: Type[0]
  }.
 
-inductive joint_instruction (p:params_) (globals: list ident): Type[0] ≝
+inductive joint_instruction (p:params__) (globals: list ident): Type[0] ≝
   | joint_instr_comment: String → joint_instruction p globals
   | joint_instr_cost_label: costlabel → joint_instruction p globals
@@ -43 +43 @@
   | joint_instr_cond: acc_a_reg p → label → joint_instruction p globals.
 
-inductive joint_statement (p:params) (globals: list ident): Type[0] ≝
+inductive joint_statement (p:params_) (globals: list ident): Type[0] ≝
   | joint_st_sequential: joint_instruction p globals → succ p → joint_statement p globals
   | joint_st_goto: label → joint_statement p globals
@@ -49 +49 @@
   | joint_st_extension: extend_statements p → joint_statement p globals.
 
-record joint_internal_function (p:params) (globals: list ident) : Type[0] ≝
+record params (globals: list ident): Type[1] ≝
+ { pars_:> params_
+ ; codeT: Type[0]
+ ; lookup: codeT → label → option (joint_statement pars_ globals)
+ }.
+
+record joint_internal_function (globals: list ident) (p:params globals) : Type[0] ≝
 { joint_if_luniverse: universe LabelTag;    (*CSC: used only for compilation*)
   joint_if_runiverse: universe RegisterTag; (*CSC: used only for compilation*)
@@ -58 +64 @@
 (*CSC: XXXXX stacksize unused for LTL-...*)
   joint_if_stacksize: nat;
-  joint_if_lookup   : label → option (joint_statement p globals);
+  joint_if_code     : codeT … p;
 (*CSC: XXXXX entry unused for LIN, but invariant in that case... *)
-  joint_if_entry    : Σl: label. joint_if_lookup l ≠ None ?;
+  joint_if_entry    : Σl: label. lookup … joint_if_code l ≠ None ?;
 (*CSC: XXXXX exit only used up to RTL (and only for tailcall removal) *)
-  joint_if_exit     : Σl: label. joint_if_lookup l ≠ None ?
+  joint_if_exit     : Σl: label. lookup … joint_if_code l ≠ None ?
 }.
 
@@ -70 +76 @@
   λexit: label.
   λp: joint_internal_function pars globals.
-  λprf: joint_if_lookup … p exit ≠ None ?.
+  λprf: lookup … (joint_if_code … p) exit ≠ None ?.
    mk_joint_internal_function pars 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)
-    (joint_if_lookup … p) (joint_if_entry … p) (dp … exit prf).
-
+    (joint_if_code … p) (joint_if_entry … p) (dp … exit prf).
 
 definition set_luniverse ≝
-  λp:params.
   λglobals  : list ident.
-  λint_fun  : joint_internal_function p globals.
+  λp:params globals.
+  λint_fun  : joint_internal_function globals p.
   λluniverse: universe LabelTag.
   let runiverse ≝ joint_if_runiverse … int_fun in
@@ -87 +92 @@
   let result    ≝ joint_if_result … int_fun in
   let stacksize ≝ joint_if_stacksize … int_fun in
-  let lookup    ≝ joint_if_lookup … int_fun in
+  let code      ≝ joint_if_code … int_fun in
   let entry     ≝ joint_if_entry … int_fun in
   let exit      ≝ joint_if_exit … int_fun in
-    mk_joint_internal_function … globals
+    mk_joint_internal_function globals p
       luniverse runiverse result params locals
-      stacksize lookup entry exit.
+      stacksize code entry exit.
 
 definition joint_function ≝ λp,globals. fundef (joint_internal_function p globals).
 
-definition joint_program ≝ λp:params. program (joint_function p) nat.
+definition joint_program ≝
+ λp:∀globals.params globals. program (λglobals. joint_function globals (p globals)) nat.
 
 (****************************************************************************)

src/joint/semantics.ma

@@ -206 +206 @@
 axiom BadFunction : String.
 
-(*CSC: move elsewhere *)
+(*CSC: move elsewhere, also in LIN.ma *)
 definition pi1: ∀A.∀P:A → Prop. (Σx:A. P x) → A ≝
  λA,P,c. match c with [ dp w _ ⇒ w ].