source: src/joint/Joint.ma @ 1908

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

Files ported to new version of the standard library.

File size: 7.3 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 ; call_args: Type[0]
15 ; call_dest: Type[0]
16 
17 ; extend_statements: Type[0]
18 }.
19
20record params_: Type[1] ≝
21 { pars__:> params__
22 ; succ: Type[0]
23 }.
24
25(* One common instantiation of params via Graphs of joint_statements
26   (all languages but LIN) *)
27definition graph_params_ : params__ → params_ ≝
28 λpars__. mk_params_ pars__ label.
29
30inductive joint_instruction (p:params__) (globals: list ident): Type[0] ≝
31  | COMMENT: String → joint_instruction p globals
32  | COST_LABEL: costlabel → joint_instruction p globals
33  | INT: generic_reg p → Byte → joint_instruction p globals
34  | MOVE: pair_reg p → joint_instruction p globals
35  | POP: acc_a_reg p → joint_instruction p globals
36  | PUSH: acc_a_reg p → joint_instruction p globals
37  | ADDRESS: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_instruction p globals
38  | OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_reg p → acc_b_reg p → joint_instruction p globals
39  | OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_instruction p globals
40  | OP2: Op2 → acc_a_reg p → acc_a_reg p → generic_reg p → joint_instruction p globals
41  | CLEAR_CARRY: joint_instruction p globals
42  | SET_CARRY: joint_instruction p globals
43  | LOAD: acc_a_reg p → dpl_reg p → dph_reg p → joint_instruction p globals
44  | STORE: dpl_reg p → dph_reg p → acc_a_reg p → joint_instruction p globals
45  | CALL_ID: ident → call_args p → call_dest p → joint_instruction p globals
46  | COND: acc_a_reg p → label → joint_instruction p globals
47  | extension: extend_statements p → joint_instruction p globals.
48
49inductive joint_statement (p:params_) (globals: list ident): Type[0] ≝
50  | sequential: joint_instruction p globals → succ p → joint_statement p globals
51  | GOTO: label → joint_statement p globals
52  | RETURN: joint_statement p globals.
53
54record params0: Type[1] ≝
55 { pars__' :> params__
56 ; resultT: Type[0]
57 ; paramsT: Type[0]
58 }.
59
60record params1 : Type[1] ≝
61 { pars0 :> params0
62 ; localsT: Type[0]
63 }.
64
65record params (globals: list ident): Type[1] ≝
66 { succ_ : Type[0]
67 ; pars1 :> params1
68 ; codeT: Type[0]
69 ; lookup: codeT → label → option (joint_statement (mk_params_ pars1 succ_) globals)
70 }.
71 
72definition params__of_params: ∀globals. params globals → params_ ≝
73 λglobals,pars. mk_params_ pars (succ_ … pars).
74coercion params__of_params: ∀globals.∀p: params globals. params_ ≝ params__of_params
75 on _p: params ? to params_.
76
77include alias "common/Graphs.ma". (* To pick the right lookup *)
78
79(* One common instantiation of params via Graphs of joint_statements
80   (all languages but LIN) *)
81definition graph_params: params1 → ∀globals: list ident. params globals ≝
82 λpars1,globals.
83  mk_params globals label pars1
84   (graph (joint_statement (graph_params_ pars1) globals)) (lookup …).
85
86
87(* CSC: special case where localsT is a list of register (RTL and ERTL) *)
88definition rtl_ertl_params1 ≝ λpars0. mk_params1 pars0 (list register).
89definition rtl_ertl_params ≝ λpars0. graph_params (rtl_ertl_params1 pars0).
90
91record joint_internal_function (globals: list ident) (p:params globals) : Type[0] ≝
92{ joint_if_luniverse: universe LabelTag;    (*CSC: used only for compilation*)
93  joint_if_runiverse: universe RegisterTag; (*CSC: used only for compilation*)
94(*  joint_if_sig: signature;  -- dropped in front end *)
95  joint_if_result   : resultT p;
96  joint_if_params   : paramsT p;
97  joint_if_locals   : localsT p;
98(*CSC: XXXXX stacksize unused for LTL-...*)
99  joint_if_stacksize: nat;
100  joint_if_code     : codeT … p;
101(*CSC: XXXXX entry unused for LIN, but invariant in that case... *)
102  joint_if_entry    : Σl: label. lookup … joint_if_code l ≠ None ?;
103(*CSC: XXXXX exit only used up to RTL (and only for tailcall removal) *)
104  joint_if_exit     : Σl: label. lookup … joint_if_code l ≠ None ?
105}.
106
107(* Currified form *)
108definition set_joint_if_exit ≝
109  λglobals,pars.
110  λexit: label.
111  λp:joint_internal_function globals pars.
112  λprf: lookup … (joint_if_code … p) exit ≠ None ?.
113   mk_joint_internal_function globals pars
114    (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
115    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
116    (joint_if_code … p) (joint_if_entry … p) (mk_Sig … exit prf).
117
118definition set_joint_code ≝
119  λglobals: list ident.
120  λpars: params globals.
121  λint_fun: joint_internal_function globals pars.
122  λgraph: codeT … pars.
123  λentry.
124  λexit.
125    mk_joint_internal_function globals pars
126      (joint_if_luniverse … int_fun) (joint_if_runiverse … int_fun) (joint_if_result … int_fun)
127      (joint_if_params … int_fun) (joint_if_locals … int_fun) (joint_if_stacksize … int_fun)
128      graph entry exit.
129
130definition set_joint_if_graph ≝
131  λglobals,pars.
132  λgraph.
133  λp:joint_internal_function globals pars.
134  λentry_prf: lookup … graph (joint_if_entry … p) ≠ None ?.
135  λexit_prf: lookup … graph (joint_if_exit … p) ≠ None ?.
136    set_joint_code globals pars p graph
137      (mk_Sig … (joint_if_entry … p) entry_prf) (mk_Sig … (joint_if_exit … p) exit_prf).
138
139definition set_luniverse ≝
140  λglobals,pars.
141  λp : joint_internal_function globals pars.
142  λluniverse: universe LabelTag.
143   mk_joint_internal_function globals pars
144    luniverse (joint_if_runiverse … p) (joint_if_result … p)
145    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
146    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
147
148definition set_runiverse ≝
149  λglobals,pars.
150  λp : joint_internal_function globals pars.
151  λruniverse: universe RegisterTag.
152   mk_joint_internal_function globals pars
153    (joint_if_luniverse … p) runiverse (joint_if_result … p)
154    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
155    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
156
157(* Specialized for graph_params *)
158definition add_graph ≝
159  λpars1,globals.λl:label.λstmt.λp:joint_internal_function globals (graph_params pars1 globals).
160   let code ≝ add … (joint_if_code ?? p) l stmt in
161    mk_joint_internal_function … (graph_params … globals)
162     (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
163     (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
164     code (pi1 ?? (joint_if_entry … p)) (pi1 … (joint_if_exit … p)).
165  normalize nodelta;
166  [ cases (joint_if_entry … p) | cases (joint_if_exit … p)]
167  #LBL #LBL_PRF @graph_add_lookup @LBL_PRF
168qed.
169
170definition set_locals ≝
171  λglobals,pars.
172  λp : joint_internal_function globals pars.
173  λlocals.
174   mk_joint_internal_function globals pars
175    (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
176    (joint_if_params … p) locals (joint_if_stacksize … p)
177    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
178
179definition joint_function ≝ λp,globals. fundef (joint_internal_function p globals).
180
181definition joint_program ≝
182 λp:∀globals.params globals. program (λglobals. joint_function globals (p globals)) nat.
Note: See TracBrowser for help on using the repository browser.