source: src/ERTL/ERTL.ma @ 1165

Last change on this file since 1165 was 1165, checked in by mulligan, 9 years ago

more changes

File size: 3.6 KB
RevLine 
[733]1include "ASM/I8051.ma".
[1161]2include "LIN/JointLTLLIN.ma".
[733]3include "utilities/BitVectorTrieSet.ma".
4include "utilities/IdentifierTools.ma".
5include "common/Graphs.ma".
[756]6include "common/CostLabel.ma".
7include "common/Registers.ma".
[733]8
[756]9definition registers ≝ list register.
[733]10
[1163]11inductive move_registers: Type[0] ≝
12  | pseudo: register → move_registers
13  | hardware: Register → move_registers.
14
[1161]15definition pre_ertl_statement ≝
[1165]16  joint_statement label register register register register
[1163]17                  (move_registers × move_registers) register.
[1161]18                 
19inductive ertl_statement (globals: list ident): Type[0] ≝
20  | ertl_st_lift_pre: pre_ertl_statement globals → ertl_statement globals
21  | ertl_st_new_frame: label → ertl_statement globals
22  | ertl_st_del_frame: label → ertl_statement globals
[1163]23  | ertl_st_frame_size: register → label → ertl_statement globals.
[1161]24
25(*
[756]26inductive ertl_statement: Type[0] ≝
[759]27  | ertl_st_skip: label → ertl_statement
28  | ertl_st_comment: String → label → ertl_statement
29  | ertl_st_cost: costlabel → label → ertl_statement
[1082]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
[759]33  | ertl_st_new_frame: label → ertl_statement
34  | ertl_st_del_frame: label → ertl_statement
[777]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
[1131]38  | ertl_st_addr: register → register → ident → label → ertl_statement
[777]39  | ertl_st_int: register → Byte → label → ertl_statement
40  | ertl_st_move: register → register → label → ertl_statement
[1138]41  | ertl_st_opaccs: OpAccs → register → register → register → register → label → ertl_statement
[777]42  | ertl_st_op1: Op1 → register → register → label → ertl_statement
43  | ertl_st_op2: Op2 → register → register → register → label → ertl_statement
[759]44  | ertl_st_clear_carry: label → ertl_statement
[1071]45  | ertl_st_set_carry: label → ertl_statement
[777]46  | ertl_st_load: register → register → register → label → ertl_statement
47  | ertl_st_store: register → register → register → label → ertl_statement
[1136]48  | ertl_st_call_id: ident → nat → label → ertl_statement
[1071]49  | ertl_st_cond: register → label → label → ertl_statement
[1107]50  | ertl_st_return: ertl_statement.
[1161]51*)
[733]52
[1161]53definition ertl_statement_graph ≝ λglobals. graph (ertl_statement globals).
[756]54
[1161]55record ertl_internal_function (globals: list ident): Type[0] ≝
[733]56{
[756]57  ertl_if_luniverse: universe LabelTag;
58  ertl_if_runiverse: universe RegisterTag;
59  ertl_if_params: nat;
60  ertl_if_locals: registers;
[782]61  ertl_if_stacksize: nat;
[1161]62  ertl_if_graph: ertl_statement_graph globals;
[1077]63  ertl_if_entry: Σl: label. lookup ? ? ertl_if_graph l ≠ None ?;
64  ertl_if_exit: Σl: label. lookup ? ? ertl_if_graph l ≠ None ?
[733]65}.
66
[1161]67definition ertl_function ≝ λglobals. fundef (ertl_internal_function globals).
[733]68 
[1161]69record ertl_program (globals: list ident): Type[0] ≝
[733]70{
[756]71  ertl_pr_vars: list (ident × nat);
[1161]72  ertl_pr_funcs: list (ident × (ertl_function globals));
[783]73  ertl_pr_main: option ident
[733]74}.
[1161]75
76
77(* XXX: changed from O'Caml
78  | ertl_st_addr_h: register → ident → label → ertl_statement
79  | ertl_st_addr_l: register → ident → label → ertl_statement
80*)
81
82(* XXX: changed from O'Caml
83  | ertl_st_opaccs_a: OpAccs → register → register → register → label → ertl_statement
84  | ertl_st_opaccs_b: OpAccs → register → register → register → label → ertl_statement
85*)
Note: See TracBrowser for help on using the repository browser.