Changeset 1176 for src/joint/Joint.ma


Ignore:
Timestamp:
Sep 3, 2011, 4:17:48 AM (8 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r1171 r1176  
    1 include "ASM/String.ma".
    21include "ASM/I8051.ma".
    32include "common/CostLabel.ma".
    4 include "common/Graphs.ma".
    53include "common/AST.ma".
    64include "common/Registers.ma".
     5include "common/Graphs.ma".
    76
    87record params: Type[1] ≝
    9  { acc_a_reg: Type[0]
     8 { next: Type[0]
     9 
     10 ; acc_a_reg: Type[0]
    1011 ; acc_b_reg: Type[0]
    1112 ; dpl_reg: Type[0]
     
    1314 ; pair_reg: Type[0]
    1415 ; generic_reg: Type[0]
     16 
     17 ; extend_statements: Type[0]
     18 
     19 ; resultT: Type[0]
     20 ; localsT: Type[0]
     21 ; paramsT: Type[0]
    1522 }.
    1623
     
    3138  | joint_instr_store: dpl_reg p → dph_reg p → acc_a_reg p → joint_instruction p globals
    3239  | joint_instr_call_id: ident → nat → joint_instruction p globals
    33   | joint_instr_cond: acc_a_reg p → label → joint_instruction p globals.
     40  | joint_instr_cond: acc_a_reg p → next p → joint_instruction p globals.
    3441
    35 inductive joint_statement (next: Type[0]) (extend: Type[0]) (p:params) (globals: list ident): Type[0] ≝
    36   | joint_st_sequential: joint_instruction p globals → next → joint_statement next extend p globals
    37   | joint_st_goto: label → joint_statement next extend p globals
    38   | joint_st_return: joint_statement next extend p globals
    39   | joint_st_extension: extend → joint_statement next extend p globals.
     42inductive 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
     45  | joint_st_return: joint_statement p globals
     46  | joint_st_extension: extend_statements p → joint_statement p globals.
     47
     48record sem_params_ (preparams: params) (globals: list ident): Type[1] ≝
     49 { pmemoryT: Type[0]
     50 ; lookup: pmemoryT → next preparams → option (joint_statement preparams globals)
     51 }.
     52
     53record joint_internal_function (globals: list ident) (pre) (p:sem_params_ pre globals): Type[0] ≝
     54{ joint_if_luniverse: universe LabelTag;    (*CSC: used only for compilation*)
     55  joint_if_runiverse: universe RegisterTag; (*CSC: used only for compilation*)
     56(*  joint_if_sig: signature;  -- dropped in front end *)
     57  joint_if_result   : resultT pre;
     58  joint_if_params   : paramsT pre;
     59  joint_if_locals   : localsT pre;
     60  joint_if_stacksize: nat;
     61  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 ?
     64}.
     65
     66definition joint_function ≝ λglobals,pre,p. fundef (joint_internal_function globals pre p).
     67
     68record joint_program (globals: list ident) (pre) (p:sem_params_ pre globals) : Type[0] ≝
     69{
     70  joint_pr_vars: list (ident × nat);
     71  joint_pr_functs: list (ident × (joint_function … p));
     72  joint_pr_main: option ident
     73}.
     74
     75(****************************************************************************)
    4076
    4177(* Used in LTL and LIN *) 
Note: See TracChangeset for help on using the changeset viewer.