source: src/joint/Joint.ma @ 1245

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

RTLtoERTL and LINToASM: porting to new Joint data type in progress.
However, it seems better to go back to a Joint representation where
the "mapping" from label to internal functions is more concrete.
To be done.

File size: 4.4 KB
Line 
1include "ASM/I8051.ma".
2include "common/CostLabel.ma".
3include "common/AST.ma".
4include "common/Registers.ma".
5include "common/Graphs.ma".
6
7record params_: Type[1] ≝
8 { acc_a_reg: Type[0]
9 ; acc_b_reg: Type[0]
10 ; dpl_reg: Type[0]
11 ; dph_reg: Type[0]
12 ; pair_reg: Type[0]
13 ; generic_reg: Type[0]
14 
15 ; extend_statements: Type[0]
16 
17 ; resultT: Type[0]
18 ; localsT: Type[0]
19 ; paramsT: Type[0]
20 }.
21
22record params: Type[1] ≝
23 { pars_:> params_
24 ; succ: Type[0]
25 }.
26
27inductive joint_instruction (p:params_) (globals: list ident): Type[0] ≝
28  | joint_instr_comment: String → joint_instruction p globals
29  | joint_instr_cost_label: costlabel → joint_instruction p globals
30  | joint_instr_int: generic_reg p → Byte → joint_instruction p globals
31  | joint_instr_move: pair_reg p → joint_instruction p globals
32  | joint_instr_pop: acc_a_reg p → joint_instruction p globals
33  | joint_instr_push: acc_a_reg p → joint_instruction p globals
34  | joint_instr_address: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_instruction p globals
35  | joint_instr_opaccs: OpAccs → acc_a_reg p → acc_b_reg p → joint_instruction p globals
36  | joint_instr_op1: Op1 → acc_a_reg p → joint_instruction p globals
37  | joint_instr_op2: Op2 → acc_a_reg p → generic_reg p → joint_instruction p globals
38  | joint_instr_clear_carry: joint_instruction p globals
39  | joint_instr_set_carry: joint_instruction p globals
40  | joint_instr_load: acc_a_reg p → dpl_reg p → dph_reg p → joint_instruction p globals
41  | joint_instr_store: dpl_reg p → dph_reg p → acc_a_reg p → joint_instruction p globals
42  | joint_instr_call_id: ident → nat → joint_instruction p globals
43  | joint_instr_cond: acc_a_reg p → label → joint_instruction p globals.
44
45inductive joint_statement (p:params) (globals: list ident): Type[0] ≝
46  | joint_st_sequential: joint_instruction p globals → succ p → joint_statement p globals
47  | joint_st_goto: label → joint_statement p globals
48  | joint_st_return: joint_statement p globals
49  | joint_st_extension: extend_statements p → joint_statement p globals.
50
51record joint_internal_function (p:params) (globals: list ident) : Type[0] ≝
52{ joint_if_luniverse: universe LabelTag;    (*CSC: used only for compilation*)
53  joint_if_runiverse: universe RegisterTag; (*CSC: used only for compilation*)
54(*  joint_if_sig: signature;  -- dropped in front end *)
55  joint_if_result   : resultT p;
56  joint_if_params   : paramsT p;
57  joint_if_locals   : localsT p;
58(*CSC: XXXXX stacksize unused for LTL-...*)
59  joint_if_stacksize: nat;
60  joint_if_lookup   : label → option (joint_statement p globals);
61(*CSC: XXXXX entry unused for LIN, but invariant in that case... *)
62  joint_if_entry    : Σl: label. joint_if_lookup l ≠ None ?;
63(*CSC: XXXXX exit only used up to RTL (and only for tailcall removal) *)
64  joint_if_exit     : Σl: label. joint_if_lookup l ≠ None ?
65}.
66
67(* Currified form *)
68definition set_joint_if_exit ≝
69  λpars,globals.
70  λexit: label.
71  λp: joint_internal_function pars globals.
72  λprf: joint_if_lookup … p exit ≠ None ?.
73   mk_joint_internal_function pars globals
74    (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
75    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
76    (joint_if_lookup … p) (joint_if_entry … p) (dp … exit prf).
77
78
79definition set_luniverse ≝
80  λp:params.
81  λglobals  : list ident.
82  λint_fun  : joint_internal_function p globals.
83  λluniverse: universe LabelTag.
84  let runiverse ≝ joint_if_runiverse … int_fun in
85  let params    ≝ joint_if_params … int_fun in
86  let locals    ≝ joint_if_locals … int_fun in
87  let result    ≝ joint_if_result … int_fun in
88  let stacksize ≝ joint_if_stacksize … int_fun in
89  let lookup    ≝ joint_if_lookup … int_fun in
90  let entry     ≝ joint_if_entry … int_fun in
91  let exit      ≝ joint_if_exit … int_fun in
92    mk_joint_internal_function … globals
93      luniverse runiverse result params locals
94      stacksize lookup entry exit.
95
96definition joint_function ≝ λp,globals. fundef (joint_internal_function p globals).
97
98definition joint_program ≝ λp:params. program (joint_function p) nat.
99
100(****************************************************************************)
101
102(* Used in LTL and LIN *) 
103inductive registers_move: Type[0] ≝
104 | from_acc: Register → registers_move
105 | to_acc: Register → registers_move.
Note: See TracBrowser for help on using the repository browser.