source: src/joint/Joint_paolo.ma @ 1640

Last change on this file since 1640 was 1640, checked in by tranquil, 8 years ago
  • finished fork of semantics.ma
  • unification of Errors under the monad notations brings problems in type checking when res and IO are used together. Needs a lot of annotations, and may break the pre-fork material
File size: 12.0 KB
Line 
1include "ASM/I8051.ma".
2include "common/CostLabel.ma".
3include "common/AST.ma".
4include "common/Registers.ma".
5include "common/Graphs.ma".
6
7(* Here is the structure of parameter records (downward edges are coercions,
8   the ↓ edges are the only explicitly defined coercions). lin_params and
9   graph_params are simple wrappers of unserialized_params, and the coercions
10   from them to params instantiate the missing bits with values for linarized
11   programs and graph programs respectively.
12
13        lin_params      graph_params
14          |       \_____ /____   |
15          |             /     \  |
16          \_______     /      ↓  ↓
17                  \   _\____ params
18                   \_/  \      |
19                    / \  \     ↓
20              _____/   unserialized_params
21             /      _______/   |
22            /      /           |
23     stmt_params  /   local_params
24        |      __/             |
25    inst_params       funct_params
26
27inst_params : types needed to define instructions
28stmt_params : adds successor type needed to define statements
29funct_params : types of result register and parameters of function
30local_params : adds types of local registers
31params : adds type of code and lookup function
32graph_params : is made just of inst_params and local_params, and the coercion
33  to params adds structure common to graph languages *)
34
35record inst_params : Type[1] ≝
36 { acc_a_reg: Type[0] (* registers that will eventually need to be A *)
37 ; acc_b_reg: Type[0] (* registers that will eventually need to be B *)
38 ; acc_a_arg: Type[0] (* arguments that will eventually need to be A *)
39 ; acc_b_arg: Type[0] (* arguments that will eventually need to be B *)
40 ; dpl_reg: Type[0]   (* low address registers *)
41 ; dph_reg: Type[0]   (* high address registers *)
42 ; dpl_arg: Type[0]   (* low address registers *)
43 ; dph_arg: Type[0]   (* high address registers *)
44 ; snd_arg : Type[0]  (* second argument of binary op *)
45 ; pair_move: Type[0] (* argument of move instructions *)
46 ; call_args: Type[0] (* arguments of function calls *)
47 ; call_dest: Type[0] (* possible destination of function computation *)
48 ; extend_statements: Type[0] (* other statements not fitting in the general framework *)
49 ; ext_forall_labels : (label → Prop) → extend_statements → Prop
50 }.
51 
52inductive joint_instruction (p:inst_params) (globals: list ident): Type[0] ≝
53  | COMMENT: String → joint_instruction p globals
54  | COST_LABEL: costlabel → joint_instruction p globals
55  | MOVE: pair_move p → joint_instruction p globals
56  | POP: acc_a_reg p → joint_instruction p globals
57  | PUSH: acc_a_arg p → joint_instruction p globals
58  | ADDRESS: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_instruction p globals
59  | OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_arg p → acc_b_arg p → joint_instruction p globals
60  | OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_instruction p globals
61  | OP2: Op2 → acc_a_reg p → acc_a_arg p → snd_arg p → joint_instruction p globals
62  (* int done with generic move *)
63(*| INT: generic_reg p → Byte → joint_instruction p globals *)
64  | CLEAR_CARRY: joint_instruction p globals
65  | SET_CARRY: joint_instruction p globals
66  | LOAD: acc_a_reg p → dpl_arg p → dph_arg p → joint_instruction p globals
67  | STORE: dpl_arg p → dph_arg p → acc_a_arg p → joint_instruction p globals
68  | CALL_ID: ident → call_args p → call_dest p → joint_instruction p globals
69  | COND: acc_a_reg p → label → joint_instruction p globals
70  | extension: extend_statements p → joint_instruction p globals.
71
72(* Paolo: to be moved elsewhere *)
73
74notation "r ← a1 .op. a2" with precedence 50 for
75  @{'op2 $op $r $a1 $a2}.
76notation "r ← . op . a" with precedence 50 for
77  @{'op1 $op $r $a}.
78notation "r ← a" with precedence 50 for
79  @{'mov $r $a}. (* to be set in individual languages *)
80notation "❮r, s❯ ← a1 . op . a2" with precedence 50 for
81  @{'opaccs $op $r $s $a1 $a2}.
82
83interpretation "op2" 'op2 op r a1 a2 = (OP2 ? ? op r a1 a2).
84interpretation "op1" 'op1 op r a = (OP1 ? ? op r a).
85interpretation "opaccs" 'opaccs op r s a1 a2 = (OPACCS ? ? op r s a1 a2).
86
87
88
89definition inst_forall_labels : ∀p : inst_params.∀globals.
90    (label → Prop) → joint_instruction p globals → Prop ≝
91λp,g,P,inst. match inst with
92  [ COND _ l ⇒ P l
93  | extension ext_s ⇒ ext_forall_labels p P ext_s
94  | _ ⇒ True
95 ].
96
97record funct_params : Type[1] ≝
98  { resultT : Type[0]
99  ; paramsT : Type[0]
100  }.
101 
102record local_params : Type[1] ≝
103 { funct_pars :> funct_params
104 ; localsT: Type[0]
105 }.
106
107record unserialized_params : Type[1] ≝
108 { u_inst_pars :> inst_params
109 ; u_local_pars :> local_params
110 }.
111
112record stmt_params : Type[1] ≝
113  { unserialized_pars :> unserialized_params
114  ; succ : Type[0]
115  ; succ_forall_labels : (label → Prop) → succ → Prop
116  }.
117
118inductive joint_statement (p: stmt_params) (globals: list ident): Type[0] ≝
119  | sequential: joint_instruction p globals → succ p → joint_statement p globals
120  | GOTO: label → joint_statement p globals
121  | RETURN: joint_statement p globals.
122
123record params : Type[1] ≝
124 { stmt_pars :> stmt_params
125 ; codeT: list ident → Type[0]
126 ; lookup: ∀globals.codeT globals → label → option (joint_statement stmt_pars globals)
127 }.
128
129
130(* for all labels in statement. Uses succ_choice to consider the successor of
131   a statement when such successors are labels *)
132definition stmt_forall_labels : ∀p : stmt_params.∀globals.
133    (label → Prop) → joint_statement p globals → Prop ≝
134  λp,g,P,stmt. match stmt with
135  [ sequential inst next ⇒ inst_forall_labels p g P inst ∧ succ_forall_labels p P next
136  | GOTO l ⇒ P l
137  | RETURN ⇒ True
138  ].
139
140record lin_params : Type[1] ≝
141  { l_u_pars :> unserialized_params }.
142
143include "utilities/option.ma".
144
145definition lin_params_to_params ≝
146  λlp : lin_params. mk_params
147    (mk_stmt_params lp unit (λ_.λ_.True))
148    (* codeT ≝ *)(λglobals.list ((option label) × (joint_statement ? globals)))
149    (* lookup ≝ *)(λglobals,code,lbl.find ??
150        (λl_stmt. let 〈lbl_opt, stmt〉 ≝ l_stmt in
151          ! lbl' ← lbl_opt ;
152          if eq_identifier … lbl lbl' then return stmt else None ?) code).
153
154coercion lp_to_p : ∀lp : lin_params.params ≝ lin_params_to_params
155  on _lp : lin_params to params.
156
157record graph_params : Type[1] ≝
158  { g_u_pars :> unserialized_params }.
159
160include alias "common/Graphs.ma". (* To pick the right lookup *)
161
162(* One common instantiation of params via Graphs of joint_statements
163   (all languages but LIN) *)
164definition graph_params_to_params ≝
165  λgp : graph_params. mk_params
166    (mk_stmt_params gp label (λP.P))
167    (* codeT ≝ *)(λglobals.graph (joint_statement ? globals))
168    (* lookup ≝ *)(λglobals.lookup …).
169   
170coercion gp_to_p : ∀gp:graph_params.params ≝ λgp.graph_params_to_params gp
171on _gp : graph_params to params.
172   
173
174definition labels_present : ∀p : params.∀globals.
175  codeT p globals → (joint_statement p globals) → Prop ≝
176λglobals,p,code,s. stmt_forall_labels globals p
177  (λl.lookup … code l ≠ None ?) s.
178
179definition forall_stmts : ∀p : params.∀globals.
180  ∀P: joint_statement p globals → Prop. codeT p globals → Prop ≝
181λglobals,p,P,code. ∀l,s. lookup … code l = Some ? s → P s.
182
183definition code_closed : ∀p : params.∀globals.
184  codeT p globals → Prop ≝ λp,globals,code.
185    forall_stmts … (labels_present … code) code.
186
187(* CSC: special case where localsT is a list of registers (RTL and ERTL) *)
188definition rtl_ertl_params : ?→?→params ≝ λinst_pars,funct_pars.
189  (mk_graph_params (mk_unserialized_params inst_pars (mk_local_params funct_pars (list register)))).
190
191record joint_internal_function (globals: list ident) (p:params) : Type[0] ≝
192{ joint_if_luniverse: universe LabelTag;    (*CSC: used only for compilation*)
193  joint_if_runiverse: universe RegisterTag; (*CSC: used only for compilation*)
194  (* Paolo: if we want this machinery to work for RTLabs too, we will need the
195     following, right? *)
196(*  joint_if_sig: signature;  -- dropped in front end *)
197  joint_if_result   : resultT p;
198  joint_if_params   : paramsT p;
199  joint_if_locals   : localsT p;
200(*CSC: XXXXX stacksize unused for LTL-...*)
201  joint_if_stacksize: nat;
202  joint_if_code     : codeT p globals ;
203(*CSC: XXXXX entry unused for LIN, but invariant in that case... *)
204  joint_if_entry    : Σl: label. lookup … joint_if_code l ≠ None ?;
205(*CSC: XXXXX exit only used up to RTL (and only for tailcall removal) *)
206  joint_if_exit     : Σl: label. lookup … joint_if_code l ≠ None ?
207}.
208
209definition joint_closed_internal_function ≝
210  λglobals,p.
211    Σdef : joint_internal_function globals p. code_closed … (joint_if_code … def).
212
213(* Currified form *)
214definition set_joint_if_exit ≝
215  λglobals,pars.
216  λexit: label.
217  λp:joint_internal_function globals pars.
218  λprf: lookup … (joint_if_code … p) exit ≠ None ?.
219   mk_joint_internal_function globals pars
220    (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
221    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
222    (joint_if_code … p) (joint_if_entry … p) (mk_Sig … exit prf).
223
224definition set_joint_code ≝
225  λglobals: list ident.
226  λpars: params.
227  λint_fun: joint_internal_function globals pars.
228  λgraph: codeT pars globals.
229  λentry.
230  λexit.
231    mk_joint_internal_function globals pars
232      (joint_if_luniverse … int_fun) (joint_if_runiverse … int_fun) (joint_if_result … int_fun)
233      (joint_if_params … int_fun) (joint_if_locals … int_fun) (joint_if_stacksize … int_fun)
234      graph entry exit.
235
236definition set_joint_if_graph ≝
237  λglobals,pars.
238  λgraph.
239  λp:joint_internal_function globals pars.
240  λentry_prf: lookup … graph (joint_if_entry … p) ≠ None ?.
241  λexit_prf: lookup … graph (joint_if_exit … p) ≠ None ?.
242    set_joint_code globals pars p
243      graph
244      (mk_Sig … (joint_if_entry … p) entry_prf)
245      (mk_Sig … (joint_if_exit … p) exit_prf).
246
247definition set_luniverse ≝
248  λglobals,pars.
249  λp : joint_internal_function globals pars.
250  λluniverse: universe LabelTag.
251   mk_joint_internal_function globals pars
252    luniverse (joint_if_runiverse … p) (joint_if_result … p)
253    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
254    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
255
256definition set_runiverse ≝
257  λglobals,pars.
258  λp : joint_internal_function globals pars.
259  λruniverse: universe RegisterTag.
260   mk_joint_internal_function globals pars
261    (joint_if_luniverse … p) runiverse (joint_if_result … p)
262    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
263    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
264   
265(* Paolo: probably should move these elsewhere *)
266definition graph_dom ≝ λX.λg : graph X.Σl : label.lookup … g l ≠ None ?.
267definition graph_dom_add_incl : ∀X.∀g : graph X.∀l : label.∀x : X.
268  graph_dom ? g → graph_dom ? (add … g l x) ≝ λX,g,l,x,sig_l.
269  mk_Sig … (pi1 ?? sig_l) ?.
270@graph_add_lookup
271@(pi2 … sig_l)
272qed.
273
274(* Specialized for graph_params *)
275definition add_graph ≝
276  λg_pars : graph_params.λglobals.λl:label.λstmt.
277    λp:joint_internal_function globals g_pars.
278   let code ≝ add … (joint_if_code … p) l stmt in
279    mk_joint_internal_function ? g_pars
280     (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
281     (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
282     code
283     (graph_dom_add_incl … (joint_if_entry … p))
284     (graph_dom_add_incl … (joint_if_exit … p)).
285
286definition set_locals ≝
287  λglobals,pars.
288  λp : joint_internal_function globals pars.
289  λlocals.
290   mk_joint_internal_function globals pars
291    (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
292    (joint_if_params … p) locals (joint_if_stacksize … p)
293    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
294
295definition joint_function ≝ λp,globals. fundef (joint_internal_function p globals).
296
297definition joint_program ≝
298 λp:params. program (λglobals. joint_function globals p) nat.
Note: See TracBrowser for help on using the repository browser.