source: src/joint/Joint.ma @ 1275

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

RTL ported to joint syntax, but:

  1. bug discovered: opaccs should have taken four registers
  2. push/pop should not be present in RTL :-(

ERTLToLTL and RTLtoERTL not working ATM

File size: 6.7 KB
Line 
1include "ASM/I8051.ma".
2include "common/CostLabel.ma".
3include "common/AST.ma".
4include "common/Registers.ma".
5include "utilities/sigma.ma". (* CSC: Only for Sigma type projections *)
6include "common/Graphs.ma".
7
8record params__: Type[1] ≝
9 { acc_a_reg: Type[0]
10 ; acc_b_reg: Type[0]
11 ; dpl_reg: Type[0]
12 ; dph_reg: Type[0]
13 ; pair_reg: Type[0]
14 ; generic_reg: Type[0]
15 ; call_args: Type[0]
16 ; call_dest: Type[0]
17 
18 ; extend_statements: Type[0]
19 
20 ; resultT: Type[0]
21 ; localsT: Type[0]
22 ; paramsT: Type[0]
23 }.
24
25record params_: Type[1] ≝
26 { pars__:> params__
27 ; succ: Type[0]
28 }.
29
30inductive joint_instruction (p:params__) (globals: list ident): Type[0] ≝
31  | joint_instr_comment: String → joint_instruction p globals
32  | joint_instr_cost_label: costlabel → joint_instruction p globals
33  | joint_instr_int: generic_reg p → Byte → joint_instruction p globals
34  | joint_instr_move: pair_reg p → joint_instruction p globals
35  | joint_instr_pop: acc_a_reg p → joint_instruction p globals
36  | joint_instr_push: acc_a_reg p → joint_instruction p globals
37  | joint_instr_address: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_instruction p globals
38  | joint_instr_opaccs: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_reg p → acc_b_reg p → joint_instruction p globals
39  | joint_instr_op1: Op1 → acc_a_reg p → acc_a_reg p → joint_instruction p globals
40  | joint_instr_op2: Op2 → acc_a_reg p → acc_a_reg p → generic_reg p → joint_instruction p globals
41  | joint_instr_clear_carry: joint_instruction p globals
42  | joint_instr_set_carry: joint_instruction p globals
43  | joint_instr_load: acc_a_reg p → dpl_reg p → dph_reg p → joint_instruction p globals
44  | joint_instr_store: dpl_reg p → dph_reg p → acc_a_reg p → joint_instruction p globals
45  | joint_instr_call_id: ident → call_args p → call_dest p → joint_instruction p globals
46  | joint_instr_cond: acc_a_reg p → label → joint_instruction p globals
47  | joint_instr_extension: extend_statements p → joint_instruction p globals.
48
49inductive joint_statement (p:params_) (globals: list ident): Type[0] ≝
50  | joint_st_sequential: joint_instruction p globals → succ p → joint_statement p globals
51  | joint_st_goto: label → joint_statement p globals
52  | joint_st_return: joint_statement p globals.
53
54
55record params (globals: list ident): Type[1] ≝
56 { pars_:> params_
57 ; codeT: Type[0]
58 ; lookup: codeT → label → option (joint_statement pars_ globals)
59 }.
60
61include alias "common/Graphs.ma". (* To pick the right lookup *)
62
63(* One common instantiation of params via Graphs of joint_statements *)
64definition graph_params: params_ → ∀globals: list ident. params globals ≝
65 λparams_,globals. mk_params globals params_ (graph (joint_statement params_ globals)) (lookup …).
66
67record joint_internal_function (globals: list ident) (p:params globals) : Type[0] ≝
68{ joint_if_luniverse: universe LabelTag;    (*CSC: used only for compilation*)
69  joint_if_runiverse: universe RegisterTag; (*CSC: used only for compilation*)
70(*  joint_if_sig: signature;  -- dropped in front end *)
71  joint_if_result   : resultT p;
72  joint_if_params   : paramsT p;
73  joint_if_locals   : localsT p;
74(*CSC: XXXXX stacksize unused for LTL-...*)
75  joint_if_stacksize: nat;
76  joint_if_code     : codeT … p;
77(*CSC: XXXXX entry unused for LIN, but invariant in that case... *)
78  joint_if_entry    : Σl: label. lookup … joint_if_code l ≠ None ?;
79(*CSC: XXXXX exit only used up to RTL (and only for tailcall removal) *)
80  joint_if_exit     : Σl: label. lookup … joint_if_code l ≠ None ?
81}.
82
83(* Currified form *)
84definition set_joint_if_exit ≝
85  λglobals,pars.
86  λexit: label.
87  λp:joint_internal_function globals pars.
88  λprf: lookup … (joint_if_code … p) exit ≠ None ?.
89   mk_joint_internal_function globals pars
90    (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
91    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
92    (joint_if_code … p) (joint_if_entry … p) (dp … exit prf).
93
94definition set_joint_if_graph ≝
95  λglobals,pars.
96  λgraph.
97  λp:joint_internal_function globals pars.
98  λentry_prf: lookup … graph (joint_if_entry … p) ≠ None ?.
99  λexit_prf: lookup … graph (joint_if_exit … p) ≠ None ?.
100   mk_joint_internal_function globals pars
101    (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
102    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
103    graph (dp … (joint_if_entry … p) entry_prf) (dp … (joint_if_exit … p) exit_prf).
104
105definition set_luniverse ≝
106  λglobals,pars.
107  λp : joint_internal_function globals pars.
108  λluniverse: universe LabelTag.
109   mk_joint_internal_function globals pars
110    luniverse (joint_if_runiverse … p) (joint_if_result … p)
111    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
112    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
113
114definition set_runiverse ≝
115  λglobals,pars.
116  λp : joint_internal_function globals pars.
117  λruniverse: universe RegisterTag.
118   mk_joint_internal_function globals pars
119    (joint_if_luniverse … p) runiverse (joint_if_result … p)
120    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
121    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
122
123(* Specialized for graph_params *)
124definition add_graph ≝
125  λpars_,globals.λl:label.λstmt.λp:joint_internal_function globals (graph_params pars_ globals).
126   let code ≝ add … (joint_if_code ?? p) l stmt in
127    mk_joint_internal_function … (graph_params pars_ globals)
128     (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
129     (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
130     code (pi1 ?? (joint_if_entry … p)) (pi1 … (joint_if_exit … p)).
131  normalize nodelta;
132  [ cases (joint_if_entry … p) | cases (joint_if_exit … p)]
133  #LBL #LBL_PRF @graph_add_lookup @LBL_PRF
134qed.
135
136definition set_locals ≝
137  λglobals,pars.
138  λp : joint_internal_function globals pars.
139  λlocals.
140   mk_joint_internal_function globals pars
141    (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
142    (joint_if_params … p) locals (joint_if_stacksize … p)
143    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
144
145definition joint_function ≝ λp,globals. fundef (joint_internal_function p globals).
146
147definition joint_program ≝
148 λp:∀globals.params globals. program (λglobals. joint_function globals (p globals)) nat.
149
150(****************************************************************************)
151
152(* Used in LTL and LIN *) 
153inductive registers_move: Type[0] ≝
154 | from_acc: Register → registers_move
155 | to_acc: Register → registers_move.
Note: See TracBrowser for help on using the repository browser.