Changeset 1168


Ignore:
Timestamp:
Sep 2, 2011, 11:36:15 AM (8 years ago)
Author:
sacerdot
Message:

Joint statements parameterized over a record.

Location:
src
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r1165 r1168  
    11include "ASM/I8051.ma".
    2 include "LIN/JointLTLLIN.ma".
     2include "joint/Joint.ma".
    33include "utilities/BitVectorTrieSet.ma".
    44include "utilities/IdentifierTools.ma".
     
    1313  | hardware: Register → move_registers.
    1414
    15 definition pre_ertl_statement ≝
    16   joint_statement label register register register register
    17                   (move_registers × move_registers) register.
     15definition ertl_params: params ≝
     16 mk_params register register register register (move_registers × move_registers) register.
     17
     18definition pre_ertl_statement ≝ joint_statement label ertl_params.
    1819                 
    1920inductive ertl_statement (globals: list ident): Type[0] ≝
     
    2223  | ertl_st_del_frame: label → ertl_statement globals
    2324  | ertl_st_frame_size: register → label → ertl_statement globals.
    24 
    25 (*
    26 inductive ertl_statement: Type[0] ≝
    27   | ertl_st_skip: label → ertl_statement
    28   | ertl_st_comment: String → label → ertl_statement
    29   | ertl_st_cost: costlabel → label → ertl_statement
    30   | ertl_st_get_hdw: register → Register → label → ertl_statement
    31   | ertl_st_set_hdw: Register → register → label → ertl_statement
    32   | ertl_st_hdw_to_hdw: Register → Register → label → ertl_statement
    33   | ertl_st_new_frame: label → ertl_statement
    34   | ertl_st_del_frame: label → ertl_statement
    35   | ertl_st_frame_size: register → label → ertl_statement
    36   | ertl_st_pop: register → label → ertl_statement
    37   | ertl_st_push: register → label → ertl_statement
    38   | ertl_st_addr: register → register → ident → label → ertl_statement
    39   | ertl_st_int: register → Byte → label → ertl_statement
    40   | ertl_st_move: register → register → label → ertl_statement
    41   | ertl_st_opaccs: OpAccs → register → register → register → register → label → ertl_statement
    42   | ertl_st_op1: Op1 → register → register → label → ertl_statement
    43   | ertl_st_op2: Op2 → register → register → register → label → ertl_statement
    44   | ertl_st_clear_carry: label → ertl_statement
    45   | ertl_st_set_carry: label → ertl_statement
    46   | ertl_st_load: register → register → register → label → ertl_statement
    47   | ertl_st_store: register → register → register → label → ertl_statement
    48   | ertl_st_call_id: ident → nat → label → ertl_statement
    49   | ertl_st_cond: register → label → label → ertl_statement
    50   | ertl_st_return: ertl_statement.
    51 *)
    5225
    5326definition ertl_statement_graph ≝ λglobals. graph (ertl_statement globals).
  • src/ERTL/ERTLToLTL.ma

    r1166 r1168  
    5151    sub.
    5252
    53 definition get_stack ≝
     53definition get_stack:
     54 ∀globals. ertl_internal_function globals → graph (ltl_statement globals) → Register → Byte → label →
     55  ltl_statement globals × (graph (ltl_statement globals)) × (universe LabelTag)
     56
    5457  λglobals: list ident.
    5558  λint_fun.
     
    6063    let off ≝ adjust_off globals int_fun off in
    6164    let luniv ≝ ertl_if_luniverse globals int_fun in
    62     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ??????? globals (joint_instr_move … globals (from_acc r)) l) in
    63     ?.
    64    
    65     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_load globals) l) in
    66     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
    67     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in
    68     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in
    69     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
    70     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in
    71       〈joint_st_sequential ? globals (joint_instr_int globals RegisterA off) l, 〈graph, luniv〉〉.
     65    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc r)) l) in
     66    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_load … globals it it it) l) in
     67    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in
     68    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it RegisterSPH) l) in
     69    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterA (zero ?)) l) in
     70    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
     71    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it RegisterSPL) l) in
     72      〈joint_st_sequential ? ltl_params globals (joint_instr_int ? globals RegisterA off) l, graph, luniv〉.
    7273
    7374definition set_stack ≝
  • src/LIN/LIN.ma

    r1167 r1168  
    1 include "Joint/JointLTLLIN.ma".
    2  
    3 inductive pre_lin_statement (globals: list ident): Type[0] ≝
    4   | lin_st_lift_joint: joint_statement unit Register Register Register Register Register registers_move globals → pre_lin_statement globals.
     1include "joint/Joint.ma".
     2
     3definition lin_params: params ≝
     4 mk_params unit unit unit unit registers_move Register.
     5
     6definition pre_lin_statement ≝
     7 λglobals: list ident. joint_statement unit lin_params globals.
    58
    69definition lin_statement ≝
  • src/LIN/LINToASM.ma

    r1149 r1168  
    3535      match instr' with
    3636      [ joint_instr_cost_label lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
    37       | joint_instr_cond_acc lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
     37      | joint_instr_cond lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
    3838      | _ ⇒ set_empty ?
    3939      ]
  • src/LTL/LTL.ma

    r1166 r1168  
    11include "common/Graphs.ma".
    22include "utilities/IdentifierTools.ma".
    3 include "LIN/JointLTLLIN.ma".
     3include "joint/Joint.ma".
    44
    5 inductive ltl_statement (globals: list ident): Type[0] ≝
    6   ltl_st_lift_joint: joint_statement label Register Register Register Register Register registers_move globals → ltl_statement globals.
     5definition ltl_params: params ≝
     6 mk_params unit unit unit unit registers_move Register.
     7
     8definition ltl_statement ≝ λglobals: list ident. joint_statement label ltl_params globals.
    79 
    810definition ltl_statement_graph ≝ λglobals. graph (ltl_statement globals).
Note: See TracChangeset for help on using the changeset viewer.