source: src/RTL/RTL_paolo.ma @ 1635

Last change on this file since 1635 was 1635, checked in by tranquil, 8 years ago
  • lists with binders and monads
  • Joint.ma and other temprarily forked, awaiting feedback from Claudio
  • translation of RTLabs → RTL refactored with new tools
File size: 4.0 KB
Line 
1include "joint/Joint_paolo.ma".
2
3inductive rtl_argument : Type[0] ≝
4  | Reg : register → rtl_argument
5  | Imm : Byte → rtl_argument.
6
7(*CSC: XXX PROBLEM HERE. Tailcalls are not instructions, but statements since they
8  are not sequential. Thus there is a dummy label at the moment in the code.
9  To be fixed once we understand exactly what to do with tail calls. *)
10inductive rtl_statement_extension: Type[0] ≝
11  | rtl_st_ext_stack_address: register → register → rtl_statement_extension
12  | rtl_st_ext_call_ptr: register → register → list rtl_argument → list register → rtl_statement_extension
13  | rtl_st_ext_tailcall_id: ident → list rtl_argument → rtl_statement_extension
14  | rtl_st_ext_tailcall_ptr: register → register → list rtl_argument → rtl_statement_extension.
15
16 
17definition imm_nat : nat → rtl_argument ≝ λn.Imm (nat_to_bv ? n).
18 
19inductive rtl_move : Type[0] ≝
20  | CARRY : bool → rtl_move
21  | REG : register → rtl_argument → rtl_move.
22 
23(* avoid expansion *)
24definition rtl_params : graph_params ≝ mk_graph_params
25  (mk_inst_params
26    (* acc_a_reg ≝ *) register
27    (* acc_b_reg ≝ *) register
28    (* acc_a_arg ≝ *) rtl_argument
29    (* acc_b_arg ≝ *) rtl_argument
30    (* dpl_reg   ≝ *) register
31    (* dph_reg   ≝ *) register
32    (* dpl_arg   ≝ *) rtl_argument
33    (* dph_arg   ≝ *) rtl_argument
34    (* snd_arg   ≝ *) rtl_argument
35    (* operator1 ≝ *) Op1
36    (* operator2 ≝ *) Op2
37    (* pair_move ≝ *) rtl_move
38    (* call_args ≝ *) (list rtl_argument)
39    (* call_dest ≝ *) (list register)
40    (* extend_statements ≝ *) rtl_statement_extension
41    (* ext_forall_labels ≝ *) (λP.λes.True))
42  (mk_local_params
43    (mk_funct_params
44      (* resultT ≝ *) (list register)
45      (* paramsT ≝ *) (list register))
46      (* localsT ≝ *) (list register)).
47   
48definition rtl_instruction ≝ joint_instruction rtl_params.
49definition rtl_statement ≝ joint_statement rtl_params.
50
51
52definition reg_from_nat : ∀globals.register → ℕ → rtl_instruction globals ≝
53  λglobals,r,k.
54  MOVE rtl_params globals (REG r (imm_nat k)).
55
56definition reg_from_byte : ∀globals.register → Byte → rtl_instruction globals ≝
57  λglobals,r,k.
58  MOVE rtl_params globals (REG r (Imm k)).
59
60definition reg_from_reg : ∀globals.register → register → rtl_instruction globals ≝
61  λglobals,r,k.
62  MOVE … (REG r (Reg k)).
63
64definition set_carry : ∀globals.rtl_instruction globals ≝
65  λglobals.MOVE … (CARRY true).
66
67definition clear_carry : ∀globals.rtl_instruction globals ≝
68  λglobals.MOVE … (CARRY false).
69 
70
71definition rtl_internal_function ≝
72  λglobals. joint_internal_function globals rtl_params.
73
74definition rtl_program ≝ joint_program rtl_params.
75
76(************ Same without tail calls ****************)
77
78inductive rtlntc_statement_extension: Type[0] ≝
79  | rtlntc_st_ext_stack_address: register → register → rtlntc_statement_extension
80  | rtlntc_st_ext_call_ptr: register → register → list register → list register → rtlntc_statement_extension.
81
82definition rtlntc_params : graph_params ≝ mk_graph_params
83  (mk_inst_params
84    (* acc_a_reg ≝ *) register
85    (* acc_b_reg ≝ *) register
86    (* acc_a_arg ≝ *) rtl_argument
87    (* acc_b_arg ≝ *) rtl_argument
88    (* dpl_reg   ≝ *) register
89    (* dph_reg   ≝ *) register
90    (* dpl_arg   ≝ *) rtl_argument
91    (* dph_arg   ≝ *) rtl_argument
92    (* snd_arg   ≝ *) rtl_argument
93    (* operator1 ≝ *) Op1
94    (* operator2 ≝ *) Op2
95    (* pair_move ≝ *) rtl_move
96    (* call_args ≝ *) (list rtl_argument)
97    (* call_dest ≝ *) (list register)
98    (* extend_statements ≝ *) rtlntc_statement_extension
99    (* ext_forall_labels ≝ *) (λP.λes.True))
100  (mk_local_params
101    (mk_funct_params
102      (* resultT ≝ *) (list register)
103      (* paramsT ≝ *) (list register))
104      (* localsT ≝ *) (list register)).
105
106definition rtlntc_statement ≝ joint_statement rtlntc_params.
107
108definition rtlntc_internal_function ≝
109  λglobals. joint_internal_function … globals rtlntc_params.
110
111definition rtlntc_program ≝ joint_program rtlntc_params.
Note: See TracBrowser for help on using the repository browser.