source: src/RTL/RTL.ma @ 1239

Last change on this file since 1239 was 1239, checked in by sacerdot, 9 years ago

RTLAbstoRTL ported to new datatypes.

Note: RTL syntax/semantics is not (yet?) an instance of Joint.

File size: 2.5 KB
RevLine 
[754]1include "basics/list.ma".
2include "common/Registers.ma".
3include "common/AST.ma".
4include "common/Graphs.ma".
5include "common/CostLabel.ma".
6
7definition registers ≝ list register.
8
9inductive rtl_statement: Type[0] ≝
10  | rtl_st_skip: label → rtl_statement
[782]11  | rtl_st_cost: costlabel → label → rtl_statement
[1115]12                (* ldest, hdest, symbol, next *)
[754]13  | rtl_st_addr: register → register → ident → label → rtl_statement
[1115]14                (* ldest, hdest, next *)
[782]15  | rtl_st_stack_addr: register → register → label → rtl_statement
[754]16  | rtl_st_int: register → Byte → label → rtl_statement
[1115]17                (* dest, src, next *)
[754]18  | rtl_st_move: register → register → label → rtl_statement
[1064]19  | rtl_st_clear_carry: label → rtl_statement
[1115]20                (* op, acc dest, bacc dest, acc src, bacc src, next *)
[1061]21  | rtl_st_opaccs: OpAccs → register → register → register → register → label → rtl_statement
[1115]22                (* op, dest, src, next *)
[1061]23  | rtl_st_op1: Op1 → register → register → label → rtl_statement
[1115]24                (* op, dest, src1, src2, next *)
[1061]25  | rtl_st_op2: Op2 → register → register → register → label → rtl_statement
[754]26  | rtl_st_load: register → register → register → label → rtl_statement
27  | rtl_st_store: register → register → register → label → rtl_statement
28  | rtl_st_call_id: ident → registers → registers → label → rtl_statement
29  | rtl_st_call_ptr: register → register → registers → registers → label → rtl_statement
30  | rtl_st_tailcall_id: ident → registers → rtl_statement
31  | rtl_st_tailcall_ptr: register → register → registers → rtl_statement
[1066]32  | rtl_st_cond: register → label → label → rtl_statement
[1060]33  | rtl_st_set_carry: label → rtl_statement
[1106]34  | rtl_st_return: rtl_statement.
[754]35 
36definition rtl_statement_graph ≝ graph rtl_statement.
37
38record rtl_internal_function: Type[0] ≝
39{
40  rtl_if_luniverse: universe LabelTag;
41  rtl_if_runiverse: universe RegisterTag;
[1068]42(*  rtl_if_sig: signature;  -- dropped in front end *)
[1071]43  rtl_if_result   : registers;
44  rtl_if_params   : registers;
45  rtl_if_locals   : registers;
[754]46  rtl_if_stacksize: nat;
[1071]47  rtl_if_graph    : rtl_statement_graph;
48  rtl_if_entry    : Σl: label. lookup ? ? rtl_if_graph l ≠ None ?;
49  rtl_if_exit     : Σl: label. lookup ? ? rtl_if_graph l ≠ None ?
[754]50}.
51
[1068]52definition rtl_function_definition ≝ fundef rtl_internal_function.
[1239]53
54definition rtl_program: Type[0] ≝ program (λ_.rtl_function_definition) nat.
Note: See TracBrowser for help on using the repository browser.