Changeset 1182 for src/joint/Joint.ma


Ignore:
Timestamp:
Sep 5, 2011, 1:23:20 PM (9 years ago)
Author:
mulligan
Message:

changes to semantics: removing parameterised "next" element in joint params (representing labels) as these are actually fixed across ertl, ltl and lin.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r1176 r1182  
    66
    77record params: Type[1] ≝
    8  { next: Type[0]
     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];
    915 
    10  ; acc_a_reg: Type[0]
    11  ; acc_b_reg: Type[0]
    12  ; dpl_reg: Type[0]
    13  ; dph_reg: Type[0]
    14  ; pair_reg: Type[0]
    15  ; generic_reg: Type[0]
     16  extend_statements: Type[0];
    1617 
    17  ; extend_statements: Type[0]
    18  
    19  ; resultT: Type[0]
    20  ; localsT: Type[0]
    21  ; paramsT: Type[0]
    22  }.
     18  resultT: Type[0];
     19  localsT: Type[0];
     20  paramsT: Type[0]
     21}.
    2322
    2423inductive joint_instruction (p:params) (globals: list ident): Type[0] ≝
     
    3837  | joint_instr_store: dpl_reg p → dph_reg p → acc_a_reg p → joint_instruction p globals
    3938  | joint_instr_call_id: ident → nat → joint_instruction p globals
    40   | joint_instr_cond: acc_a_reg p → next p → joint_instruction p globals.
     39  | joint_instr_cond: acc_a_reg p → label → joint_instruction p globals.
    4140
    4241inductive joint_statement (p:params) (globals: list ident): Type[0] ≝
    43   | joint_st_sequential: joint_instruction p globals → next p → joint_statement p globals
    44   | joint_st_goto: next p → joint_statement p globals
     42  | joint_st_sequential: joint_instruction p globals → label → joint_statement p globals
     43  | joint_st_goto: label → joint_statement p globals
    4544  | joint_st_return: joint_statement p globals
    4645  | joint_st_extension: extend_statements p → joint_statement p globals.
     
    4847record sem_params_ (preparams: params) (globals: list ident): Type[1] ≝
    4948 { pmemoryT: Type[0]
    50  ; lookup: pmemoryT → next preparams → option (joint_statement preparams globals)
     49 ; lookup: pmemoryT → label → option (joint_statement preparams globals)
    5150 }.
    5251
     
    6059  joint_if_stacksize: nat;
    6160  joint_if_graph    : pmemoryT … p;
    62   joint_if_entry    : Σl: next pre. lookup … p joint_if_graph l ≠ None ?;
    63   joint_if_exit     : Σl: next pre. lookup … p joint_if_graph l ≠ None ?
     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 ?
    6463}.
    6564
Note: See TracChangeset for help on using the changeset viewer.