source: src/joint/joint_printer.ma @ 2982

Last change on this file since 2982 was 2982, checked in by sacerdot, 6 years ago

Pretty priting of LIN implemented.

File size: 11.8 KB
Line 
1(**************************************************************************)
2(*       ___                                                              *)
3(*      ||M||                                                             *)
4(*      ||A||       A project by Andrea Asperti                           *)
5(*      ||T||                                                             *)
6(*      ||I||       Developers:                                           *)
7(*      ||T||         The HELM team.                                      *)
8(*      ||A||         http://helm.cs.unibo.it                             *)
9(*      \   /                                                             *)
10(*       \ /        This file is distributed under the terms of the       *)
11(*        v         GNU General Public License Version 2                  *)
12(*                                                                        *)
13(**************************************************************************)
14
15include "joint/Joint.ma".
16
17inductive keyword : Type[0] ≝
18  | kwCOMMENT: keyword
19  | kwMOVE: keyword
20  | kwPOP: keyword
21  | kwPUSH: keyword
22  | kwADDRESS: keyword
23  | kwOPACCS: keyword
24  | kwOP1: keyword
25  | kwOP2: keyword
26  | kwCLEAR_CARRY: keyword
27  | kwSET_CARRY: keyword
28  | kwLOAD: keyword
29  | kwSTORE: keyword
30  | kwCOST_LABEL: keyword
31  | kwCOND: keyword
32  | kwCALL: keyword
33  | kwGOTO: keyword
34  | kwRETURN: keyword
35  | kwTAILCALL: keyword
36  | kwFCOND: keyword.
37
38record printing_pass_independent_params (string: Type[0]) : Type[0] ≝
39 { print_String: String → string
40 ; print_keyword: keyword → string
41 ; print_concat: string → string → string
42 ; print_empty: string
43 ; print_ident: ident → string
44 ; print_costlabel: costlabel → string
45 ; print_label: label → string
46 ; print_OpAccs: OpAccs → string
47 ; print_Op1: Op1 → string
48 ; print_Op2: Op2 → string
49 ; print_nat: nat → string }.
50
51record printing_params (string: Type[0]) (P: unserialized_params) : Type[0] ≝
52 { print_pass_ind:> printing_pass_independent_params string
53 ; print_acc_a_reg: acc_a_reg P → string
54 ; print_acc_b_reg: acc_b_reg P → string
55 ; print_acc_a_arg: acc_a_arg P → string
56 ; print_acc_b_arg: acc_b_arg P → string
57 ; print_dpl_reg: dpl_reg P → string   (* low address registers *)
58 ; print_dph_reg: dph_reg P → string   (* high address registers *)
59 ; print_dpl_arg: dpl_arg P → string   (* low address registers *)
60 ; print_dph_arg: dph_arg P → string   (* high address registers *)
61 ; print_snd_arg : snd_arg P → string  (* second argument of binary op *)
62 ; print_pair_move: pair_move P → string (* argument of move instructions *)
63 ; print_call_args: call_args P → string (* arguments of function calls *)
64 ; print_call_dest: call_dest P → string (* possible destination of function computation *)
65 (* other instructions not fitting in the general framework *)
66 ; print_ext_seq : ext_seq P → string
67 }.
68
69record print_serialization_params (string: Type[0]) (p:params) : Type[1] ≝
70 { print_succ: succ … p → string
71 ; print_code_point: code_point p → string
72 }.
73
74record code_iteration_params (string: Type[0]) (p:params) (statementT: Type[0])
75  (globals) : Type[1] ≝
76 { cip_print_serialization_params :> print_serialization_params string p
77 ; fold_code:
78    ∀A:Type[0]. (code_point p → statementT → A → A) → codeT p globals → A → A
79 ; print_statementT: statementT → string
80 }.
81
82definition pm_choose_with_pref:
83 ∀A:Type[0]. positive_map A → option Pos → option (Pos × A × (positive_map A)) ≝
84 λA,M,n.
85  match n with
86  [ None ⇒ pm_choose A M
87  | Some p ⇒
88     match pm_try_remove A p M with
89     [ None ⇒ pm_choose A M
90     | Some res ⇒ let 〈a,M'〉 ≝ res in Some … 〈p,a,M'〉 ]].
91
92let rec visit_graph (A:Type[0]) (next: A → option Pos) (B:Type[0])
93 (f: Pos → A → B → B) (b:B) (n: option Pos) (M: positive_map A) (x:nat) on x : B ≝
94 match x with
95 [ O ⇒ b (* Dummy, this should never happen for a large enough value of x *)
96 | S y ⇒
97    match pm_choose_with_pref A M n with
98    [ None ⇒ b
99    | Some res ⇒
100       let 〈pos,a,M'〉 ≝ res in
101        visit_graph A next B f (f pos a b) (next a) M' y ]].
102
103definition print_list:
104 ∀string. printing_pass_independent_params string → list string → string ≝
105 λstring,pp.
106  foldr ?? (print_concat … pp) (print_empty … pp). 
107
108definition print_joint_seq :
109 ∀p. ∀globals. ∀string. printing_params string p → joint_seq p globals → string ≝
110 λp,globals,string,pp,seq.
111  match seq with
112  [ COMMENT str ⇒
113     print_list … pp [print_keyword … pp kwCOMMENT; print_String … pp str]
114  | MOVE pm ⇒
115     print_list … pp [print_keyword … pp kwMOVE; print_pair_move … pp pm]
116  | POP arg ⇒
117     print_list … pp [print_keyword … pp kwPOP; print_acc_a_reg … pp arg]
118  | PUSH arg ⇒
119     print_list … pp [print_keyword … pp kwPUSH; print_acc_a_arg … pp arg]
120  | ADDRESS i Hi arg1 arg2 ⇒
121     print_list … pp
122      [print_keyword … pp kwADDRESS;
123       print_ident … pp i;
124       print_dpl_reg … pp arg1;
125       print_dph_reg … pp arg2]
126  | OPACCS opa arg1 arg2 arg3 arg4 ⇒
127     print_list … pp
128      [print_keyword … pp kwOPACCS;
129       print_OpAccs … pp opa;
130       print_acc_a_reg … pp arg1;
131       print_acc_b_reg … pp arg2;
132       print_acc_a_arg … pp arg3;
133       print_acc_b_arg … pp arg4]
134  | OP1 op1 arg1 arg2 ⇒
135     print_list … pp
136      [print_keyword … pp kwOP1;
137       print_Op1 … pp op1;
138       print_acc_a_reg … pp arg1;
139       print_acc_a_reg … pp arg2]
140  | OP2 op2 arg1 arg2 arg3 ⇒
141     print_list … pp
142      [print_keyword … pp kwOP2;
143       print_Op2 … pp op2;
144       print_acc_a_reg … pp arg1;
145       print_acc_a_arg … pp arg2;
146       print_snd_arg … pp arg3]
147  (* int done with generic move *)
148  | CLEAR_CARRY ⇒ print_keyword … pp kwCLEAR_CARRY
149  | SET_CARRY ⇒ print_keyword … pp kwSET_CARRY
150  | LOAD arg1 arg2 arg3 ⇒
151     print_list … pp
152      [print_keyword … pp kwLOAD;
153       print_acc_a_reg … pp arg1;
154       print_dpl_arg … pp arg2;
155       print_dph_arg … pp arg3]
156  | STORE arg1 arg2 arg3 ⇒
157     print_list … pp
158      [print_keyword … pp kwSTORE;
159       print_dpl_arg … pp arg1;
160       print_dph_arg … pp arg2;
161       print_acc_a_arg … pp arg3]
162  | extension_seq ext ⇒ print_ext_seq … pp ext].
163
164definition print_joint_step:
165 ∀p,globals. ∀string. printing_params string p → joint_step p globals → string ≝
166 λp,globals,string,pp,step.
167  match step with
168   [ COST_LABEL arg ⇒
169      print_list ? pp
170       [print_keyword … pp kwCOST_LABEL;
171        print_costlabel … pp arg]
172   | CALL arg1 arg2 arg3 ⇒
173      print_list … pp
174       [print_keyword … pp kwCALL;
175        match arg1 with
176        [ inl id ⇒ print_ident … pp id
177        | inr arg11_arg12 ⇒
178           print_concat … pp
179            (print_dpl_arg … pp (\fst arg11_arg12))
180            (print_dph_arg … pp (\snd arg11_arg12))];
181        print_call_args … pp arg2;
182        print_call_dest … pp arg3]
183   | COND arg1 arg2 ⇒
184      print_list … pp
185       [print_keyword … pp kwCOND;
186        print_acc_a_reg … pp arg1;
187        print_label … pp arg2]
188   | step_seq seq ⇒ print_joint_seq … pp seq ].
189
190definition print_joint_fin_step:
191 ∀p. ∀string. printing_params string p → joint_fin_step p → string ≝
192 λp,string,pp,fin.
193  match fin with
194   [ GOTO l ⇒
195      print_list ? pp
196       [ print_keyword … pp kwGOTO;
197         print_label … pp l]
198   | RETURN ⇒ print_keyword … pp kwRETURN
199   | TAILCALL has arg1 arg2 ⇒
200      print_list … pp
201       [print_keyword … pp kwTAILCALL;
202        match arg1 with
203        [ inl id ⇒ print_ident … pp id
204        | inr arg11_arg12 ⇒
205           print_concat … pp
206            (print_dpl_arg … pp (\fst arg11_arg12))
207            (print_dph_arg … pp (\snd arg11_arg12))];
208        print_call_args … pp arg2]].
209
210definition print_joint_statement:
211 ∀p:params.∀globals. ∀string. printing_params string p →
212  print_serialization_params string p → joint_statement p globals → string ≝
213 λp,globals,string,pp,cip,stmt.
214  match stmt with
215  [ sequential js arg1 ⇒
216     print_concat … pp (print_joint_step … pp js) (print_succ … cip arg1)
217  | final fin ⇒ print_joint_fin_step … pp fin
218  | FCOND has arg1 arg2 arg3 ⇒
219     print_list ? pp
220      [ print_keyword … pp kwFCOND;
221        print_acc_a_reg … pp arg1;
222        print_label … pp arg2;
223        print_label … pp arg3 ]].
224
225definition graph_print_serialization_params:
226 ∀string,graph_params.
227  printing_params string (graph_params_to_params graph_params) →
228   print_serialization_params string (graph_params_to_params graph_params) ≝
229 λstring,gp,pp.
230  mk_print_serialization_params … (print_label … pp) (print_label … pp).
231
232definition graph_code_iteration_params:
233 ∀string,graph_params,globals.
234  printing_params string (graph_params_to_params graph_params) →
235   code_iteration_params string (graph_params_to_params graph_params) … globals ≝
236 λstring,gp,globals,pp.
237  mk_code_iteration_params …
238   (graph_print_serialization_params … pp)
239   (λA.λf:code_point (graph_params_to_params …) → ?.λM.λa.
240     visit_graph (joint_statement … gp globals)
241     (λstmt. match stmt_implicit_label ?? stmt with
242       [ None ⇒ None … | Some label ⇒ match label with [an_identifier p ⇒ Some … p]])
243     ? (λn. f (an_identifier … n)) a (Some … one)
244     (match M with [an_id_map M' ⇒ M']) (id_map_size … M))
245     (print_joint_statement … pp … (graph_print_serialization_params … pp)).
246
247definition lin_print_serialization_params:
248 ∀string,lin_params.
249  printing_params string (lin_params_to_params lin_params) →
250   print_serialization_params string (lin_params_to_params lin_params) ≝
251 λstring,gp,pp.
252  mk_print_serialization_params … (λ_.print_empty … pp) (print_nat … pp).
253
254definition lin_code_iteration_params:
255 ∀string,lin_params,globals.
256  printing_params string (lin_params_to_params lin_params) →
257   code_iteration_params string (lin_params_to_params lin_params) ? globals ≝
258 λstring,lp,globals,pp.
259  mk_code_iteration_params ?? (? × (joint_statement ??)) ?
260   (lin_print_serialization_params … pp)
261   (λA.λf:code_point (lin_params_to_params …) → ?.λM:codeT lp globals.
262    λa.
263     \snd (foldr ??
264      (λx.λres. let 〈pc,res'〉 ≝ res in 〈S pc,f pc x res'〉)
265      〈0,a〉 M))
266     (λlinstr.
267       match \fst linstr with
268       [ None ⇒
269          print_joint_statement … pp … (lin_print_serialization_params … pp)
270           (\snd linstr)
271       | Some l ⇒
272          print_list ? pp
273           [ print_label … pp l;
274             print_joint_statement … pp … (lin_print_serialization_params … pp)
275              (\snd linstr) ]]).
276
277definition print_joint_internal_function:
278 ∀p:params. ∀lines. ∀globals. ∀string. code_iteration_params string p lines globals →
279  printing_params string p → joint_internal_function p globals → list string
280≝ λp,lines,globals,string,cip,pp,f.
281   fold_code … cip …
282    (λcp.λstmt.λacc.
283      print_list ? pp
284       [ print_code_point … cip cp;
285         print_statementT … cip stmt ]::acc)
286    (joint_if_code … f) [].
287
288definition print_joint_function:
289 ∀p:params. ∀lines. ∀globals. ∀string. code_iteration_params string p lines globals → printing_params string p →
290  joint_function p globals → list string ≝
291 λp,lines,globals,string,cip,pp,f.
292  match f with
293  [ Internal f ⇒ print_joint_internal_function … cip … pp f
294  | External f ⇒ [] ].
295
296definition print_joint_program:
297 ∀p:params. ∀lines. ∀string.
298  printing_params string p →
299  ∀prog:joint_program p.
300   code_iteration_params string p lines (map … (λx. \fst (\fst x)) (prog_vars ?? prog)) →
301   list (ident × (list string)) ≝
302 λp,lines,string,pp,prog,cip.
303  foldr ?? (λf,acc. 〈\fst f,print_joint_function … cip … pp (\snd f)〉 :: acc)
304   [] (prog_funct … prog).
Note: See TracBrowser for help on using the repository browser.