Changeset 2847
- Timestamp:
- Mar 12, 2013, 10:20:26 AM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/joint/joint_printer.ma
r2846 r2847 36 36 | kwFCOND: keyword. 37 37 38 record 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 38 50 record printing_params (string: Type[0]) (P: unserialized_params) : Type[0] ≝ 39 { print_acc_a_reg: acc_a_reg P → string 51 { print_pass_ind:> printing_pass_independent_params string 52 ; print_acc_a_reg: acc_a_reg P → string 40 53 ; print_acc_b_reg: acc_b_reg P → string 41 54 ; print_acc_a_arg: acc_a_arg P → string … … 51 64 (* other instructions not fitting in the general framework *) 52 65 ; print_ext_seq : ext_seq P → string 53 ; print_String: String → string54 ; print_keyword: keyword → string55 ; print_concat: string → string → string56 ; print_empty: string57 ; print_ident: ident → string58 ; print_costlabel: costlabel → string59 ; print_label: label → string60 ; print_OpAccs: OpAccs → string61 ; print_Op1: Op1 → string62 ; print_Op2: Op2 → string63 66 }. 64 67 … … 71 74 }. 72 75 73 definition print_list: ∀string,P. printing_params string P → list string → string ≝ 74 λstring,P,pp. 76 definition graph_code_iteration_params: 77 ∀string,graph_params,globals. 78 printing_params string (graph_params_to_params graph_params) → 79 code_iteration_params string (graph_params_to_params graph_params) globals ≝ 80 λstring,gp,globals,pp. 81 mk_code_iteration_params ??? 82 (λA.λf:code_point (graph_params_to_params …) → ?. 83 graph_fold … (λn. f (an_identifier … n)) …) (print_label … pp). 84 85 definition print_list: 86 ∀string. printing_pass_independent_params string → list string → string ≝ 87 λstring,pp. 75 88 foldr ?? (print_concat … pp) (print_empty … pp). 76 89 … … 136 149 match step with 137 150 [ COST_LABEL arg ⇒ 138 print_list …pp151 print_list ? pp 139 152 [print_keyword … pp kwCOST_LABEL; 140 153 print_costlabel … pp arg] 141 154 | CALL arg1 arg2 arg3 ⇒ 142 print_list ??pp155 print_list … pp 143 156 [print_keyword … pp kwCALL; 144 157 match arg1 with … … 157 170 | step_seq seq ⇒ print_joint_seq … pp seq ]. 158 171 159 axiom print_joint_fin_step: 160 ∀p. ∀string. printing_params string p → joint_fin_step p → string. (* 161 inductive 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.*) 172 definition print_joint_fin_step: 173 ∀p. ∀string. printing_params string p → joint_fin_step p → string ≝ 174 λp,string,pp,fin. 175 match fin with 176 [ GOTO l ⇒ 177 print_list ? pp 178 [ print_keyword … pp kwGOTO; 179 print_label … pp l] 180 | RETURN ⇒ print_keyword … pp kwRETURN 181 | TAILCALL has arg1 arg2 ⇒ 182 print_list … pp 183 [print_keyword … pp kwTAILCALL; 184 match arg1 with 185 [ inl id ⇒ print_ident … pp id 186 | inr arg11_arg12 ⇒ 187 print_concat … pp 188 (print_dpl_arg … pp (\fst arg11_arg12)) 189 (print_dph_arg … pp (\snd arg11_arg12))]; 190 print_call_args … pp arg2]]. 167 191 168 192 definition print_joint_statement: … … 175 199 | final fin ⇒ print_joint_fin_step … pp fin 176 200 | FCOND has arg1 arg2 arg3 ⇒ 177 print_list …pp201 print_list ? pp 178 202 [ print_keyword … pp kwFCOND; 179 203 print_acc_a_reg … pp arg1;
Note: See TracChangeset
for help on using the changeset viewer.