Changeset 2847


Ignore:
Timestamp:
Mar 12, 2013, 10:20:26 AM (4 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/joint_printer.ma

    r2846 r2847  
    3636  | kwFCOND: keyword.
    3737
     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
    3850record 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
    4053 ; print_acc_b_reg: acc_b_reg P → string
    4154 ; print_acc_a_arg: acc_a_arg P → string
     
    5164 (* other instructions not fitting in the general framework *)
    5265 ; 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
    6366 }.
    6467
     
    7174 }.
    7275
    73 definition print_list: ∀string,P. printing_params string P → list string → string ≝
    74  λstring,P,pp.
     76definition 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
     85definition print_list:
     86 ∀string. printing_pass_independent_params string → list string → string ≝
     87 λstring,pp.
    7588  foldr ?? (print_concat … pp) (print_empty … pp). 
    7689
     
    136149  match step with
    137150   [ COST_LABEL arg ⇒
    138       print_list pp
     151      print_list ? pp
    139152       [print_keyword … pp kwCOST_LABEL;
    140153        print_costlabel … pp arg]
    141154   | CALL arg1 arg2 arg3 ⇒
    142       print_list ?? pp
     155      print_list pp
    143156       [print_keyword … pp kwCALL;
    144157        match arg1 with
     
    157170   | step_seq seq ⇒ print_joint_seq … pp seq ].
    158171
    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.*)
     172definition 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]].
    167191
    168192definition print_joint_statement:
     
    175199  | final fin ⇒ print_joint_fin_step … pp fin
    176200  | FCOND has arg1 arg2 arg3 ⇒
    177      print_list pp
     201     print_list ? pp
    178202      [ print_keyword … pp kwFCOND;
    179203        print_acc_a_reg … pp arg1;
Note: See TracChangeset for help on using the changeset viewer.