source: src/joint/joint_printer.ma @ 2846

Last change on this file since 2846 was 2846, checked in by sacerdot, 7 years ago

Pretty printing of joint programs.

File size: 8.0 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_params (string: Type[0]) (P: unserialized_params) : Type[0] ≝
39 { print_acc_a_reg: acc_a_reg P → string
40 ; print_acc_b_reg: acc_b_reg P → string
41 ; print_acc_a_arg: acc_a_arg P → string
42 ; print_acc_b_arg: acc_b_arg P → string
43 ; print_dpl_reg: dpl_reg P → string   (* low address registers *)
44 ; print_dph_reg: dph_reg P → string   (* high address registers *)
45 ; print_dpl_arg: dpl_arg P → string   (* low address registers *)
46 ; print_dph_arg: dph_arg P → string   (* high address registers *)
47 ; print_snd_arg : snd_arg P → string  (* second argument of binary op *)
48 ; print_pair_move: pair_move P → string (* argument of move instructions *)
49 ; print_call_args: call_args P → string (* arguments of function calls *)
50 ; print_call_dest: call_dest P → string (* possible destination of function computation *)
51 (* other instructions not fitting in the general framework *)
52 ; print_ext_seq : ext_seq P → string
53 ; print_String: String → string
54 ; print_keyword: keyword → string
55 ; print_concat: string → string → string
56 ; print_empty: string
57 ; print_ident: ident → string
58 ; print_costlabel: costlabel → string
59 ; print_label: label → string
60 ; print_OpAccs: OpAccs → string
61 ; print_Op1: Op1 → string
62 ; print_Op2: Op2 → string
63 }.
64
65record code_iteration_params (string: Type[0]) (p:params) (globals) : Type[1] ≝
66 { fold_code:
67    ∀A:Type[0].
68     (code_point p → joint_statement p globals → A → A) →
69      codeT p globals → A → A
70 ; print_succ: succ … p → string
71 }.
72
73definition print_list: ∀string,P. printing_params string P → list string → string ≝
74 λstring,P,pp.
75  foldr ?? (print_concat … pp) (print_empty … pp). 
76
77definition print_joint_seq :
78 ∀p. ∀globals. ∀string. printing_params string p → joint_seq p globals → string ≝
79 λp,globals,string,pp,seq.
80  match seq with
81  [ COMMENT str ⇒
82     print_list … pp [print_keyword … pp kwCOMMENT; print_String … pp str]
83  | MOVE pm ⇒
84     print_list … pp [print_keyword … pp kwMOVE; print_pair_move … pp pm]
85  | POP arg ⇒
86     print_list … pp [print_keyword … pp kwPOP; print_acc_a_reg … pp arg]
87  | PUSH arg ⇒
88     print_list … pp [print_keyword … pp kwPUSH; print_acc_a_arg … pp arg]
89  | ADDRESS i Hi arg1 arg2 ⇒
90     print_list … pp
91      [print_keyword … pp kwADDRESS;
92       print_ident … pp i;
93       print_dpl_reg … pp arg1;
94       print_dph_reg … pp arg2]
95  | OPACCS opa arg1 arg2 arg3 arg4 ⇒
96     print_list … pp
97      [print_keyword … pp kwOPACCS;
98       print_OpAccs … pp opa;
99       print_acc_a_reg … pp arg1;
100       print_acc_b_reg … pp arg2;
101       print_acc_a_arg … pp arg3;
102       print_acc_b_arg … pp arg4]
103  | OP1 op1 arg1 arg2 ⇒
104     print_list … pp
105      [print_keyword … pp kwOP1;
106       print_Op1 … pp op1;
107       print_acc_a_reg … pp arg1;
108       print_acc_a_reg … pp arg2]
109  | OP2 op2 arg1 arg2 arg3 ⇒
110     print_list … pp
111      [print_keyword … pp kwOP2;
112       print_Op2 … pp op2;
113       print_acc_a_reg … pp arg1;
114       print_acc_a_arg … pp arg2;
115       print_snd_arg … pp arg3]
116  (* int done with generic move *)
117  | CLEAR_CARRY ⇒ print_keyword … pp kwCLEAR_CARRY
118  | SET_CARRY ⇒ print_keyword … pp kwSET_CARRY
119  | LOAD arg1 arg2 arg3 ⇒
120     print_list … pp
121      [print_keyword … pp kwLOAD;
122       print_acc_a_reg … pp arg1;
123       print_dpl_arg … pp arg2;
124       print_dph_arg … pp arg3]
125  | STORE arg1 arg2 arg3 ⇒
126     print_list … pp
127      [print_keyword … pp kwSTORE;
128       print_dpl_arg … pp arg1;
129       print_dph_arg … pp arg2;
130       print_acc_a_arg … pp arg3]
131  | extension_seq ext ⇒ print_ext_seq … pp ext].
132
133definition print_joint_step:
134 ∀p,globals. ∀string. printing_params string p → joint_step p globals → string ≝
135 λp,globals,string,pp,step.
136  match step with
137   [ COST_LABEL arg ⇒
138      print_list … pp
139       [print_keyword … pp kwCOST_LABEL;
140        print_costlabel … pp arg]
141   | CALL arg1 arg2 arg3 ⇒
142      print_list ?? pp
143       [print_keyword … pp kwCALL;
144        match arg1 with
145        [ inl id ⇒ print_ident … pp id
146        | inr arg11_arg12 ⇒
147           print_concat … pp
148            (print_dpl_arg … pp (\fst arg11_arg12))
149            (print_dph_arg … pp (\snd arg11_arg12))];
150        print_call_args … pp arg2;
151        print_call_dest … pp arg3]
152   | COND arg1 arg2 ⇒
153      print_list … pp
154       [print_keyword … pp kwCOND;
155        print_acc_a_reg … pp arg1;
156        print_label … pp arg2]
157   | step_seq seq ⇒ print_joint_seq … pp seq ].
158
159axiom print_joint_fin_step:
160 ∀p. ∀string. printing_params string p → joint_fin_step p → string. (*
161inductive joint_fin_step (p: unserialized_params): Type[0] ≝
162  | GOTO: label → joint_fin_step p
163  | RETURN: joint_fin_step p
164  | TAILCALL :
165    has_tailcalls p → (ident + (dpl_arg p × (dph_arg p))) →
166    call_args p → joint_fin_step p.*)
167
168definition print_joint_statement:
169 ∀p:params.∀globals. ∀string. printing_params string p →
170  code_iteration_params string p globals → joint_statement p globals → string ≝
171 λp,globals,string,pp,cip,stmt.
172  match stmt with
173  [ sequential js arg1 ⇒
174     print_concat … pp (print_joint_step … pp js) (print_succ … cip arg1)
175  | final fin ⇒ print_joint_fin_step … pp fin
176  | FCOND has arg1 arg2 arg3 ⇒
177     print_list … pp
178      [ print_keyword … pp kwFCOND;
179        print_acc_a_reg … pp arg1;
180        print_label … pp arg2;
181        print_label … pp arg3 ]].
182
183definition print_joint_internal_function:
184 ∀p:params. ∀globals. ∀string. code_iteration_params string p globals →
185  printing_params string p → joint_internal_function p globals → string
186≝ λp,globals,string,cip,pp,f.
187   fold_code … cip … (λcp.λstmt. print_concat … pp (print_joint_statement … pp cip stmt))
188    (joint_if_code … f) (print_empty … pp).
189
190definition print_joint_function:
191 ∀p:params. ∀globals. ∀string. code_iteration_params string p globals → printing_params string p →
192  joint_function p globals → string ≝
193 λp,globals,string,cip,pp,f.
194  match f with
195  [ Internal f ⇒ print_joint_internal_function … cip … pp f
196  | External f ⇒ print_empty … pp ].
197
198definition print_joint_program:
199 ∀p:params. ∀string.
200  printing_params string p →
201  ∀prog:joint_program p.
202   code_iteration_params string p (map … (λx. \fst (\fst x)) (prog_vars ?? prog)) → string ≝
203 λp,string,pp,prog,cip.
204  foldr ?? (λf. print_concat … pp (print_joint_function … cip … pp (\snd f)))
205   (print_empty … pp) (prog_funct … prog).
Note: See TracBrowser for help on using the repository browser.