Changeset 1246 for src/joint/Joint.ma


Ignore:
Timestamp:
Sep 22, 2011, 2:50:44 AM (8 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.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r1245 r1246  
    55include "common/Graphs.ma".
    66
    7 record params_: Type[1] ≝
     7record params__: Type[1] ≝
    88 { acc_a_reg: Type[0]
    99 ; acc_b_reg: Type[0]
     
    2020 }.
    2121
    22 record params: Type[1] ≝
    23  { pars_:> params_
     22record params_: Type[1] ≝
     23 { pars__:> params__
    2424 ; succ: Type[0]
    2525 }.
    2626
    27 inductive joint_instruction (p:params_) (globals: list ident): Type[0] ≝
     27inductive joint_instruction (p:params__) (globals: list ident): Type[0] ≝
    2828  | joint_instr_comment: String → joint_instruction p globals
    2929  | joint_instr_cost_label: costlabel → joint_instruction p globals
     
    4343  | joint_instr_cond: acc_a_reg p → label → joint_instruction p globals.
    4444
    45 inductive joint_statement (p:params) (globals: list ident): Type[0] ≝
     45inductive joint_statement (p:params_) (globals: list ident): Type[0] ≝
    4646  | joint_st_sequential: joint_instruction p globals → succ p → joint_statement p globals
    4747  | joint_st_goto: label → joint_statement p globals
     
    4949  | joint_st_extension: extend_statements p → joint_statement p globals.
    5050
    51 record joint_internal_function (p:params) (globals: list ident) : Type[0] ≝
     51record params (globals: list ident): Type[1] ≝
     52 { pars_:> params_
     53 ; codeT: Type[0]
     54 ; lookup: codeT → label → option (joint_statement pars_ globals)
     55 }.
     56
     57record joint_internal_function (globals: list ident) (p:params globals) : Type[0] ≝
    5258{ joint_if_luniverse: universe LabelTag;    (*CSC: used only for compilation*)
    5359  joint_if_runiverse: universe RegisterTag; (*CSC: used only for compilation*)
     
    5864(*CSC: XXXXX stacksize unused for LTL-...*)
    5965  joint_if_stacksize: nat;
    60   joint_if_lookup   : label → option (joint_statement p globals);
     66  joint_if_code     : codeT … p;
    6167(*CSC: XXXXX entry unused for LIN, but invariant in that case... *)
    62   joint_if_entry    : Σl: label. joint_if_lookup l ≠ None ?;
     68  joint_if_entry    : Σl: label. lookup … joint_if_code l ≠ None ?;
    6369(*CSC: XXXXX exit only used up to RTL (and only for tailcall removal) *)
    64   joint_if_exit     : Σl: label. joint_if_lookup l ≠ None ?
     70  joint_if_exit     : Σl: label. lookup … joint_if_code l ≠ None ?
    6571}.
    6672
     
    7076  λexit: label.
    7177  λp: joint_internal_function pars globals.
    72   λprf: joint_if_lookup … p exit ≠ None ?.
     78  λprf: lookup … (joint_if_code … p) exit ≠ None ?.
    7379   mk_joint_internal_function pars globals
    7480    (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
    7581    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
    76     (joint_if_lookup … p) (joint_if_entry … p) (dp … exit prf).
    77 
     82    (joint_if_code … p) (joint_if_entry … p) (dp … exit prf).
    7883
    7984definition set_luniverse ≝
    80   λp:params.
    8185  λglobals  : list ident.
    82   λint_fun  : joint_internal_function p globals.
     86  λp:params globals.
     87  λint_fun  : joint_internal_function globals p.
    8388  λluniverse: universe LabelTag.
    8489  let runiverse ≝ joint_if_runiverse … int_fun in
     
    8792  let result    ≝ joint_if_result … int_fun in
    8893  let stacksize ≝ joint_if_stacksize … int_fun in
    89   let lookup    ≝ joint_if_lookup … int_fun in
     94  let code      ≝ joint_if_code … int_fun in
    9095  let entry     ≝ joint_if_entry … int_fun in
    9196  let exit      ≝ joint_if_exit … int_fun in
    92     mk_joint_internal_function … globals
     97    mk_joint_internal_function globals p
    9398      luniverse runiverse result params locals
    94       stacksize lookup entry exit.
     99      stacksize code entry exit.
    95100
    96101definition joint_function ≝ λp,globals. fundef (joint_internal_function p globals).
    97102
    98 definition joint_program ≝ λp:params. program (joint_function p) nat.
     103definition joint_program ≝
     104 λp:∀globals.params globals. program (λglobals. joint_function globals (p globals)) nat.
    99105
    100106(****************************************************************************)
Note: See TracChangeset for help on using the changeset viewer.