Changeset 2847

Timestamp:

Mar 12, 2013, 10:20:26 AM (8 years ago)

Author:

sacerdot

Message:

...

File:

• src/joint/joint_printer.ma (modified) (6 diffs)

src/joint/joint_printer.ma

@@ -36 +36 @@
   | kwFCOND: keyword.
 
+record printing_pass_independent_params (string: Type[0]) : Type[0] ≝
+ { print_String: String → string
+ ; print_keyword: keyword → string
+ ; print_concat: string → string → string
+ ; print_empty: string
+ ; print_ident: ident → string
+ ; print_costlabel: costlabel → string
+ ; print_label: label → string
+ ; print_OpAccs: OpAccs → string
+ ; print_Op1: Op1 → string
+ ; print_Op2: Op2 → string }.
+
 record printing_params (string: Type[0]) (P: unserialized_params) : Type[0] ≝
- { print_acc_a_reg: acc_a_reg P → string 
+ { print_pass_ind:> printing_pass_independent_params string
+ ; print_acc_a_reg: acc_a_reg P → string 
  ; print_acc_b_reg: acc_b_reg P → string
  ; print_acc_a_arg: acc_a_arg P → string
@@ -51 +64 @@
  (* other instructions not fitting in the general framework *)
  ; print_ext_seq : ext_seq P → string
- ; print_String: String → string
- ; print_keyword: keyword → string
- ; print_concat: string → string → string
- ; print_empty: string
- ; print_ident: ident → string
- ; print_costlabel: costlabel → string
- ; print_label: label → string
- ; print_OpAccs: OpAccs → string
- ; print_Op1: Op1 → string
- ; print_Op2: Op2 → string
  }.
 
@@ -71 +74 @@
  }.
 
-definition print_list: ∀string,P. printing_params string P → list string → string ≝
- λstring,P,pp.
+definition graph_code_iteration_params:
+ ∀string,graph_params,globals.
+  printing_params string (graph_params_to_params graph_params) →
+   code_iteration_params string (graph_params_to_params graph_params) globals ≝
+ λstring,gp,globals,pp.
+  mk_code_iteration_params ???
+   (λA.λf:code_point (graph_params_to_params …) → ?.
+     graph_fold … (λn. f (an_identifier … n)) …) (print_label … pp).
+
+definition print_list:
+ ∀string. printing_pass_independent_params string → list string → string ≝
+ λstring,pp.
   foldr ?? (print_concat … pp) (print_empty … pp).  
 
@@ -136 +149 @@
   match step with
    [ COST_LABEL arg ⇒
-      print_list … pp
+      print_list ? pp
        [print_keyword … pp kwCOST_LABEL;
         print_costlabel … pp arg]
    | CALL arg1 arg2 arg3 ⇒
-      print_list ?? pp
+      print_list … pp
        [print_keyword … pp kwCALL;
         match arg1 with
@@ -157 +170 @@
    | step_seq seq ⇒ print_joint_seq … pp seq ].
 
-axiom print_joint_fin_step:
- ∀p. ∀string. printing_params string p → joint_fin_step p → string. (*
-inductive joint_fin_step (p: unserialized_params): Type[0] ≝
-  | GOTO: label → joint_fin_step p
-  | RETURN: joint_fin_step p
-  | TAILCALL :
-    has_tailcalls p → (ident + (dpl_arg p × (dph_arg p))) →
-    call_args p → joint_fin_step p.*)
+definition print_joint_fin_step:
+ ∀p. ∀string. printing_params string p → joint_fin_step p → string ≝
+ λp,string,pp,fin.
+  match fin with
+   [ GOTO l ⇒
+      print_list ? pp
+       [ print_keyword … pp kwGOTO;
+         print_label … pp l]
+   | RETURN ⇒ print_keyword … pp kwRETURN
+   | TAILCALL has arg1 arg2 ⇒
+      print_list … pp
+       [print_keyword … pp kwTAILCALL;
+        match arg1 with
+        [ inl id ⇒ print_ident … pp id
+        | inr arg11_arg12 ⇒
+           print_concat … pp
+            (print_dpl_arg … pp (\fst arg11_arg12))
+            (print_dph_arg … pp (\snd arg11_arg12))];
+        print_call_args … pp arg2]].
 
 definition print_joint_statement:
@@ -175 +199 @@
   | final fin ⇒ print_joint_fin_step … pp fin
   | FCOND has arg1 arg2 arg3 ⇒
-     print_list … pp
+     print_list ? pp
       [ print_keyword … pp kwFCOND;
         print_acc_a_reg … pp arg1;