source: src/joint/Joint_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: 10.5 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 ¦ edge is the only explicitly defined coercion):
9
10       _____graph_params___
11      /           ¦        \
12     /         params       \
13    /         /      \      |
14   / stmt_params      local_params
15   \    |                  |
16    inst_params       funct_params
17
18inst_params : types needed to define instructions
19stmt_params : adds successor type needed to define statements
20funct_params : types of result register and parameters of function
21local_params : adds types of local registers
22params : adds type of code and lookup function
23graph_params : is made just of inst_params and local_params, and the coercion
24  to params adds structure common to graph languages *)
25
26record inst_params : Type[1] ≝
27 { acc_a_reg: Type[0] (* registers that will eventually need to be A *)
28 ; acc_b_reg: Type[0] (* registers that will eventually need to be B *)
29 ; acc_a_arg: Type[0] (* arguments that will eventually need to be A *)
30 ; acc_b_arg: Type[0] (* arguments that will eventually need to be B *)
31 ; dpl_reg: Type[0]   (* low address registers *)
32 ; dph_reg: Type[0]   (* high address registers *)
33 ; dpl_arg: Type[0]   (* low address registers *)
34 ; dph_arg: Type[0]   (* high address registers *)
35 ; snd_arg : Type[0]  (* second argument of binary op *)
36 ; operator1 : Type[0] (* = Op1 in all but RTLabs *)
37 ; operator2 : Type[0] (* = Op2 in all but RTLabs *)
38 ; pair_move: Type[0] (* argument of move instructions *)
39 ; call_args: Type[0] (* arguments of function calls *)
40 ; call_dest: Type[0] (* possible destination of function computation *)
41 ; extend_statements: Type[0] (* other statements not fitting in the general framework *)
42 ; ext_forall_labels : (label → Prop) → extend_statements → Prop
43 }.
44 
45inductive joint_instruction (p:inst_params) (globals: list ident): Type[0] ≝
46  | COMMENT: String → joint_instruction p globals
47  | COST_LABEL: costlabel → joint_instruction p globals
48  | MOVE: pair_move p → joint_instruction p globals
49  | POP: acc_a_reg p → joint_instruction p globals
50  | PUSH: acc_a_arg p → joint_instruction p globals
51  | ADDRESS: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_instruction p globals
52  | OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_arg p → acc_b_arg p → joint_instruction p globals
53  | OP1: operator1 p → acc_a_reg p → acc_a_reg p → joint_instruction p globals
54  | OP2: operator2 p → acc_a_reg p → acc_a_arg p → snd_arg p → joint_instruction p globals
55  (* int, clear and set carry can be done with generic move *)
56(*| INT: generic_reg p → Byte → joint_instruction p globals
57  | CLEAR_CARRY: joint_instruction p globals
58  | SET_CARRY: joint_instruction p globals *)
59  | LOAD: acc_a_reg p → dpl_arg p → dph_arg p → joint_instruction p globals
60  | STORE: dpl_arg p → dph_arg p → acc_a_arg p → joint_instruction p globals
61  | CALL_ID: ident → call_args p → call_dest p → joint_instruction p globals
62  | COND: acc_a_reg p → label → joint_instruction p globals
63  | extension: extend_statements p → joint_instruction p globals.
64
65definition inst_forall_labels : ∀p : inst_params.∀globals.
66    (label → Prop) → joint_instruction p globals → Prop ≝
67λp,g,P,inst. match inst with
68  [ COND _ l ⇒ P l
69  | extension ext_s ⇒ ext_forall_labels p P ext_s
70  | _ ⇒ True
71 ].
72
73record stmt_params : Type[1] ≝
74  { inst_pars :> inst_params
75  ; succ : Type[0]
76  ; succ_choice : (succ = label) + (succ = unit)
77  }.
78
79inductive joint_statement (p: stmt_params) (globals: list ident): Type[0] ≝
80  | sequential: joint_instruction p globals → succ p → joint_statement p globals
81  | GOTO: label → joint_statement p globals
82  | RETURN: joint_statement p globals.
83
84(* for all labels in statement. Uses succ_choice to consider the successor of
85   a statement when such successors are labels *)
86definition stmt_forall_labels : ∀p : stmt_params.∀globals.
87    (label → Prop) → joint_statement p globals → Prop.
88*#i_pr#succ#succ_choice#globals#P*
89[#instr cases succ_choice #eq >eq #next
90  [@(inst_forall_labels … P instr ∧ P next)
91  |@(inst_forall_labels … P instr)
92  ]
93|@P
94|@True
95]qed.
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 params : Type[1] ≝
108 { stmt_pars :> stmt_params
109 ; local_pars :> local_params
110 ; codeT: list ident → Type[0]
111 ; lookup: ∀globals.codeT globals → label → option (joint_statement stmt_pars globals)
112 }.
113
114record graph_params : Type[1] ≝
115 { g_inst_pars :> inst_params
116 ; g_local_pars :> local_params
117 }.
118
119definition labels_present : ∀p : params.∀globals.
120  codeT p globals → (joint_statement p globals) → Prop ≝
121λglobals,p,code,s. stmt_forall_labels globals p
122  (λl.lookup … code l ≠ None ?) s.
123
124definition forall_stmts : ∀p : params.∀globals.
125  ∀P: joint_statement p globals → Prop. codeT p globals → Prop ≝
126λglobals,p,P,code. ∀l,s. lookup … code l = Some ? s → P s.
127
128definition code_closed : ∀p : params.∀globals.
129  codeT p globals → Prop ≝ λp,globals,code.
130    forall_stmts … (labels_present … code) code.
131
132include alias "common/Graphs.ma". (* To pick the right lookup *)
133
134
135(* One common instantiation of params via Graphs of joint_statements
136   (all languages but LIN) *)
137definition params_of_graph_params: graph_params → params ≝
138 λgp.
139  let stmt_pars ≝ mk_stmt_params gp label (inl … (refl …)) in
140  mk_params
141   stmt_pars
142   gp
143   (* codeT ≝ *)(λglobals.graph (joint_statement stmt_pars globals))
144   (λglobals.lookup …).
145   
146coercion graph_params_to_params :
147  ∀gp : graph_params.params ≝
148    λgp.params_of_graph_params gp
149    on _gp : graph_params to params.
150
151(* CSC: special case where localsT is a list of registers (RTL and ERTL) *)
152definition rtl_ertl_params ≝ λinst_pars,funct_pars.
153  params_of_graph_params (mk_graph_params inst_pars (mk_local_params funct_pars (list register))).
154
155record joint_internal_function (globals: list ident) (p:params) : Type[0] ≝
156{ joint_if_luniverse: universe LabelTag;    (*CSC: used only for compilation*)
157  joint_if_runiverse: universe RegisterTag; (*CSC: used only for compilation*)
158  (* Paolo: if we want this machinery to work for RTLabs too, we will need the
159     following, right? *)
160(*  joint_if_sig: signature;  -- dropped in front end *)
161  joint_if_result   : resultT p;
162  joint_if_params   : paramsT p;
163  joint_if_locals   : localsT p;
164(*CSC: XXXXX stacksize unused for LTL-...*)
165  joint_if_stacksize: nat;
166  joint_if_code     : codeT p globals ;
167(*CSC: XXXXX entry unused for LIN, but invariant in that case... *)
168  joint_if_entry    : Σl: label. lookup … joint_if_code l ≠ None ?;
169(*CSC: XXXXX exit only used up to RTL (and only for tailcall removal) *)
170  joint_if_exit     : Σl: label. lookup … joint_if_code l ≠ None ?
171}.
172
173definition joint_closed_internal_function ≝
174  λglobals,p.
175    Σdef : joint_internal_function globals p. code_closed … (joint_if_code … def).
176
177(* Currified form *)
178definition set_joint_if_exit ≝
179  λglobals,pars.
180  λexit: label.
181  λp:joint_internal_function globals pars.
182  λprf: lookup … (joint_if_code … p) exit ≠ None ?.
183   mk_joint_internal_function globals pars
184    (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
185    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
186    (joint_if_code … p) (joint_if_entry … p) (mk_Sig … exit prf).
187
188definition set_joint_code ≝
189  λglobals: list ident.
190  λpars: params.
191  λint_fun: joint_internal_function globals pars.
192  λgraph: codeT pars globals.
193  λentry.
194  λexit.
195    mk_joint_internal_function globals pars
196      (joint_if_luniverse … int_fun) (joint_if_runiverse … int_fun) (joint_if_result … int_fun)
197      (joint_if_params … int_fun) (joint_if_locals … int_fun) (joint_if_stacksize … int_fun)
198      graph entry exit.
199
200definition set_joint_if_graph ≝
201  λglobals,pars.
202  λgraph.
203  λp:joint_internal_function globals pars.
204  λentry_prf: lookup … graph (joint_if_entry … p) ≠ None ?.
205  λexit_prf: lookup … graph (joint_if_exit … p) ≠ None ?.
206    set_joint_code globals pars p
207      graph
208      (mk_Sig … (joint_if_entry … p) entry_prf)
209      (mk_Sig … (joint_if_exit … p) exit_prf).
210
211definition set_luniverse ≝
212  λglobals,pars.
213  λp : joint_internal_function globals pars.
214  λluniverse: universe LabelTag.
215   mk_joint_internal_function globals pars
216    luniverse (joint_if_runiverse … p) (joint_if_result … p)
217    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
218    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
219
220definition set_runiverse ≝
221  λglobals,pars.
222  λp : joint_internal_function globals pars.
223  λruniverse: universe RegisterTag.
224   mk_joint_internal_function globals pars
225    (joint_if_luniverse … p) runiverse (joint_if_result … p)
226    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
227    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
228   
229(* Paolo: probably should move these elsewhere *)
230definition graph_dom ≝ λX.λg : graph X.Σl : label.lookup … g l ≠ None ?.
231definition graph_dom_add_incl : ∀X.∀g : graph X.∀l : label.∀x : X.
232  graph_dom ? g → graph_dom ? (add … g l x) ≝ λX,g,l,x,sig_l.
233  mk_Sig … (pi1 ?? sig_l) ?.
234@graph_add_lookup
235@(pi2 … sig_l)
236qed.
237
238(* Specialized for graph_params *)
239definition add_graph ≝
240  λg_pars : graph_params.λglobals.λl:label.λstmt.
241    λp:joint_internal_function globals g_pars.
242   let code ≝ add … (joint_if_code … p) l stmt in
243    mk_joint_internal_function ? g_pars
244     (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
245     (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
246     code
247     (graph_dom_add_incl … (joint_if_entry … p))
248     (graph_dom_add_incl … (joint_if_exit … p)).
249
250definition set_locals ≝
251  λglobals,pars.
252  λp : joint_internal_function globals pars.
253  λlocals.
254   mk_joint_internal_function globals pars
255    (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
256    (joint_if_params … p) locals (joint_if_stacksize … p)
257    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
258
259definition joint_function ≝ λp,globals. fundef (joint_internal_function p globals).
260
261definition joint_program ≝
262 λp:params. program (λglobals. joint_function globals p) nat.
Note: See TracBrowser for help on using the repository browser.