Changeset 1233 for src/joint/Joint.ma


Ignore:
Timestamp:
Sep 21, 2011, 11:57:20 AM (9 years ago)
Author:
sacerdot
Message:

1) Ported to Brian's new dependent type for fullexec
2) Universe level raised for fullexec and related stuff to accomodate the

joint semantics

3) Improved joint syntax and semantics
4) Code for LTLToLin simplified

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r1228 r1233  
    55include "common/Graphs.ma".
    66
     7record params_: Type[1] ≝
     8 { acc_a_reg: Type[0]
     9 ; acc_b_reg: Type[0]
     10 ; dpl_reg: Type[0]
     11 ; dph_reg: Type[0]
     12 ; pair_reg: Type[0]
     13 ; generic_reg: Type[0]
     14 
     15 ; extend_statements: Type[0]
     16 
     17 ; resultT: Type[0]
     18 ; localsT: Type[0]
     19 ; paramsT: Type[0]
     20 }.
     21
    722record params: Type[1] ≝
    8 {
    9   acc_a_reg: Type[0];
    10   acc_b_reg: Type[0];
    11   dpl_reg: Type[0];
    12   dph_reg: Type[0];
    13   pair_reg: Type[0];
    14   generic_reg: Type[0];
    15  
    16   extend_statements: Type[0];
    17  
    18   resultT: Type[0];
    19   localsT: Type[0];
    20   paramsT: Type[0]
    21 }.
     23 { pars_:> params_
     24 ; succ: Type[0]
     25 }.
    2226
    23 inductive joint_instruction (p:params) (globals: list ident): Type[0] ≝
     27inductive joint_instruction (p:params_) (globals: list ident): Type[0] ≝
    2428  | joint_instr_comment: String → joint_instruction p globals
    2529  | joint_instr_cost_label: costlabel → joint_instruction p globals
     
    4044
    4145inductive joint_statement (p:params) (globals: list ident): Type[0] ≝
    42   | joint_st_sequential: joint_instruction p globals → label → joint_statement p globals
     46  | joint_st_sequential: joint_instruction p globals → succ p → joint_statement p globals
    4347  | joint_st_goto: label → joint_statement p globals
    4448  | joint_st_return: joint_statement p globals
    4549  | joint_st_extension: extend_statements p → joint_statement p globals.
    4650
    47 record sem_params_ (preparams: params) (globals: list ident): Type[1] ≝
    48  { pmemoryT: Type[0]
    49  ; lookup: pmemoryT → label → option (joint_statement preparams globals)
    50  }.
    51 
    52 record joint_internal_function (globals: list ident) (pre) (p:sem_params_ pre globals): Type[0] ≝
     51record joint_internal_function (p:params) (globals: list ident) : Type[0] ≝
    5352{ joint_if_luniverse: universe LabelTag;    (*CSC: used only for compilation*)
    5453  joint_if_runiverse: universe RegisterTag; (*CSC: used only for compilation*)
    5554(*  joint_if_sig: signature;  -- dropped in front end *)
    56   joint_if_result   : resultT pre;
    57   joint_if_params   : paramsT pre;
    58   joint_if_locals   : localsT pre;
     55  joint_if_result   : resultT p;
     56  joint_if_params   : paramsT p;
     57  joint_if_locals   : localsT p;
    5958  joint_if_stacksize: nat;
    60   joint_if_graph    : pmemoryT … p;
    61   joint_if_entry    : Σl: label. lookup … p joint_if_graph l ≠ None ?;
    62   joint_if_exit     : Σl: label. lookup … p joint_if_graph l ≠ None ?
     59  joint_if_lookup   : label → option (joint_statement p globals);
     60  joint_if_entry    : Σl: label. joint_if_lookup l ≠ None ?;
     61  joint_if_exit     : Σl: label. joint_if_lookup l ≠ None ?
    6362}.
    6463
    6564definition set_luniverse ≝
     65  λp:params.
    6666  λglobals  : list ident.
    67   λpre.
    68   λp: sem_params_ pre globals.
    69   λint_fun  : joint_internal_function globals … p.
     67  λint_fun  : joint_internal_function p globals.
    7068  λluniverse: universe LabelTag.
    7169  let runiverse ≝ joint_if_runiverse … int_fun in
     
    7472  let result    ≝ joint_if_result … int_fun in
    7573  let stacksize ≝ joint_if_stacksize … int_fun in
    76   let graph     ≝ joint_if_graph … int_fun in
     74  let lookup    ≝ joint_if_lookup … int_fun in
    7775  let entry     ≝ joint_if_entry … int_fun in
    7876  let exit      ≝ joint_if_exit … int_fun in
    79     mk_joint_internal_function globals ? p
     77    mk_joint_internal_function … globals
    8078      luniverse runiverse result params locals
    81       stacksize graph entry exit.
     79      stacksize lookup entry exit.
    8280
    83 definition joint_function ≝ λglobals,pre,p. fundef (joint_internal_function globals pre p).
     81definition joint_function ≝ λp,globals. fundef (joint_internal_function p globals).
    8482
    85 definition joint_program ≝
    86   λglobals: list ident.
    87   λpre.
    88   λp: sem_params_ pre globals.
    89     program (λx. joint_function globals pre p) nat.
     83definition joint_program ≝ λp:params. program (joint_function p) nat.
    9084
    9185(****************************************************************************)
Note: See TracChangeset for help on using the changeset viewer.