(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

include "joint/Joint.ma".

inductive keyword : Type[0] ≝
  | kwCOMMENT: keyword
  | kwMOVE: keyword
  | kwPOP: keyword
  | kwPUSH: keyword
  | kwADDRESS: keyword
  | kwOPACCS: keyword
  | kwOP1: keyword
  | kwOP2: keyword
  | kwCLEAR_CARRY: keyword
  | kwSET_CARRY: keyword
  | kwLOAD: keyword
  | kwSTORE: keyword
  | kwCOST_LABEL: keyword
  | kwCOND: keyword
  | kwCALL: keyword
  | kwGOTO: keyword
  | kwRETURN: keyword
  | kwTAILCALL: keyword
  | 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
 ; print_nat: nat → string
 ; print_bitvector: ∀n. BitVector n → string }.

record printing_params (string: Type[0]) (P: unserialized_params) : Type[0] ≝
 { 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
 ; print_acc_b_arg: acc_b_arg P → string
 ; print_dpl_reg: dpl_reg P → string   (* low address registers *)
 ; print_dph_reg: dph_reg P → string   (* high address registers *)
 ; print_dpl_arg: dpl_arg P → string   (* low address registers *)
 ; print_dph_arg: dph_arg P → string   (* high address registers *)
 ; print_snd_arg : snd_arg P → string  (* second argument of binary op *)
 ; print_pair_move: pair_move P → string (* argument of move instructions *)
 ; print_call_args: call_args P → string (* arguments of function calls *)
 ; print_call_dest: call_dest P → string (* possible destination of function computation *)
 (* other instructions not fitting in the general framework *)
 ; print_ext_seq : ext_seq P → string
 }.

record print_serialization_params (string: Type[0]) (p:params) : Type[1] ≝
 { print_succ: succ … p → string
 ; print_code_point: code_point p → string
 }.

record code_iteration_params (string: Type[0]) (p:params) (statementT: Type[0])
  (globals) : Type[1] ≝
 { cip_print_serialization_params :> print_serialization_params string p
 ; fold_code:
    ∀A:Type[0]. (code_point p → statementT → A → A) → codeT p globals →
     code_point p → A → A
 ; print_statementT: statementT → string
 }.

definition pm_choose_with_pref:
 ∀A:Type[0]. positive_map A → option Pos → option (Pos × A × (positive_map A)) ≝
 λA,M,n.
  match n with
  [ None ⇒ pm_choose A M
  | Some p ⇒ 
     match pm_try_remove A p M with
     [ None ⇒ pm_choose A M
     | Some res ⇒ let 〈a,M'〉 ≝ res in Some … 〈p,a,M'〉 ]]. 

let rec visit_graph (A:Type[0]) (next: A → option Pos) (B:Type[0])
 (f: Pos → A → B → B) (b:B) (n: option Pos) (M: positive_map A) (x:nat) on x : B ≝
 match x with
 [ O ⇒ b (* Dummy, this should never happen for a large enough value of x *)
 | S y ⇒
    match pm_choose_with_pref A M n with
    [ None ⇒ b
    | Some res ⇒
       let 〈pos,a,M'〉 ≝ res in
        visit_graph A next B f (f pos a b) (next a) M' y ]].

definition print_list:
 ∀string. printing_pass_independent_params string → list string → string ≝
 λstring,pp.
  foldr ?? (print_concat … pp) (print_empty … pp).  

definition print_joint_seq :
 ∀p. ∀globals. ∀string. printing_params string p → joint_seq p globals → string ≝
 λp,globals,string,pp,seq.
  match seq with
  [ COMMENT str ⇒
     print_list … pp [print_keyword … pp kwCOMMENT; print_String … pp str]
  | MOVE pm ⇒
     print_list … pp [print_keyword … pp kwMOVE; print_pair_move … pp pm]
  | POP arg ⇒
     print_list … pp [print_keyword … pp kwPOP; print_acc_a_reg … pp arg]
  | PUSH arg ⇒
     print_list … pp [print_keyword … pp kwPUSH; print_acc_a_arg … pp arg]
  | ADDRESS i Hi offset arg1 arg2 ⇒
     print_list … pp
      [print_keyword … pp kwADDRESS;
       print_ident … pp i;
       print_bitvector … pp … offset;
       print_dpl_reg … pp arg1;
       print_dph_reg … pp arg2]
  | OPACCS opa arg1 arg2 arg3 arg4 ⇒
     print_list … pp
      [print_keyword … pp kwOPACCS;
       print_OpAccs … pp opa;
       print_acc_a_reg … pp arg1;
       print_acc_b_reg … pp arg2;
       print_acc_a_arg … pp arg3;
       print_acc_b_arg … pp arg4]
  | OP1 op1 arg1 arg2 ⇒
     print_list … pp
      [print_keyword … pp kwOP1;
       print_Op1 … pp op1;
       print_acc_a_reg … pp arg1;
       print_acc_a_reg … pp arg2]
  | OP2 op2 arg1 arg2 arg3 ⇒
     print_list … pp
      [print_keyword … pp kwOP2;
       print_Op2 … pp op2;
       print_acc_a_reg … pp arg1;
       print_acc_a_arg … pp arg2;
       print_snd_arg … pp arg3]
  (* int done with generic move *)
  | CLEAR_CARRY ⇒ print_keyword … pp kwCLEAR_CARRY
  | SET_CARRY ⇒ print_keyword … pp kwSET_CARRY
  | LOAD arg1 arg2 arg3 ⇒
     print_list … pp
      [print_keyword … pp kwLOAD;
       print_acc_a_reg … pp arg1;
       print_dpl_arg … pp arg2;
       print_dph_arg … pp arg3]
  | STORE arg1 arg2 arg3 ⇒
     print_list … pp
      [print_keyword … pp kwSTORE;
       print_dpl_arg … pp arg1;
       print_dph_arg … pp arg2;
       print_acc_a_arg … pp arg3]
  | extension_seq ext ⇒ print_ext_seq … pp ext].

definition print_joint_step:
 ∀p,globals. ∀string. printing_params string p → joint_step p globals → string ≝
 λp,globals,string,pp,step.
  match step with
   [ COST_LABEL arg ⇒
      print_list ? pp
       [print_keyword … pp kwCOST_LABEL;
        print_costlabel … pp arg]
   | CALL arg1 arg2 arg3 ⇒
      print_list … pp
       [print_keyword … pp kwCALL;
        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;
        print_call_dest … pp arg3]
   | COND arg1 arg2 ⇒
      print_list … pp
       [print_keyword … pp kwCOND;
        print_acc_a_reg … pp arg1;
        print_label … pp arg2]
   | step_seq seq ⇒ print_joint_seq … pp seq ].

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:
 ∀p:params.∀globals. ∀string. printing_params string p →
  print_serialization_params string p → joint_statement p globals → string ≝
 λp,globals,string,pp,cip,stmt.
  match stmt with
  [ sequential js arg1 ⇒
     print_concat … pp (print_joint_step … pp js) (print_succ … cip arg1)
  | final fin ⇒ print_joint_fin_step … pp fin
  | FCOND has arg1 arg2 arg3 ⇒
     print_list ? pp
      [ print_keyword … pp kwFCOND;
        print_acc_a_reg … pp arg1;
        print_label … pp arg2;
        print_label … pp arg3 ]].

definition graph_print_serialization_params:
 ∀string,graph_params.
  printing_params string (graph_params_to_params graph_params) →
   print_serialization_params string (graph_params_to_params graph_params) ≝
 λstring,gp,pp.
  mk_print_serialization_params … (print_label … pp) (print_label … 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 …
   (graph_print_serialization_params … pp)
   (λA.λf:code_point (graph_params_to_params …) → ?.λM.λinitl.λa.
     visit_graph (joint_statement … gp globals)
     (λstmt. match stmt_implicit_label ?? stmt with
       [ None ⇒ None … | Some label ⇒ match label with [an_identifier p ⇒ Some … p]])
     ? (λn. f (an_identifier … n)) a
     (Some … (word_of_identifier … initl))
     (match M with [an_id_map M' ⇒ M']) (id_map_size … M))
     (print_joint_statement … pp … (graph_print_serialization_params … pp)).

definition lin_print_serialization_params:
 ∀string,lin_params.
  printing_params string (lin_params_to_params lin_params) →
   print_serialization_params string (lin_params_to_params lin_params) ≝
 λstring,gp,pp.
  mk_print_serialization_params … (λ_.print_empty … pp) (print_nat … pp).

definition lin_code_iteration_params:
 ∀string,lin_params,globals.
  printing_params string (lin_params_to_params lin_params) →
   code_iteration_params string (lin_params_to_params lin_params) ? globals ≝
 λstring,lp,globals,pp.
  mk_code_iteration_params ?? (? × (joint_statement ??)) ?
   (lin_print_serialization_params … pp)
   (λA.λf:code_point (lin_params_to_params …) → ?.λM:codeT lp globals.λ_.
    λa.
     \snd (foldl ??
      (λres,x. let 〈pc,res'〉 ≝ res in 〈S pc,f pc x res'〉)
      〈0,a〉 M))
     (λlinstr.
       match \fst linstr with
       [ None ⇒
          print_joint_statement … pp … (lin_print_serialization_params … pp)
           (\snd linstr)
       | Some l ⇒ 
          print_list ? pp
           [ print_label … pp l;
             print_joint_statement … pp … (lin_print_serialization_params … pp)
              (\snd linstr) ]]).

definition print_joint_internal_function:
 ∀p:params. ∀lines. ∀globals. ∀string. code_iteration_params string p lines globals →
  printing_params string p → joint_internal_function p globals → list string
≝ λp,lines,globals,string,cip,pp,f.
   fold_code … cip …
    (λcp.λstmt.λacc.
      print_list ? pp
       [ print_code_point … cip cp;
         print_statementT … cip stmt ]::acc)
    (joint_if_code … f) (joint_if_entry … f) [].

definition print_joint_function:
 ∀p:params. ∀lines. ∀globals. ∀functions. ∀string.
  code_iteration_params string p lines (globals@functions) → printing_params string p →
   joint_function p functions globals → list string ≝
 λp,lines,globals,functions,string,cip,pp,f.
  match f with
  [ Internal f ⇒ print_joint_internal_function … cip … pp f
  | External f ⇒ [] ].

definition print_joint_program:
 ∀p:params. ∀lines. ∀string.
  printing_params string p →
  ∀prog:joint_program p.
   code_iteration_params string p lines (prog_names … prog) →
   list (ident × (list string)) ≝
 λp,lines,string,pp,prog,cip.
  foldr ?? (λf,acc. 〈\fst f,print_joint_function … cip … pp (\snd f)〉 :: acc)
   [] (prog_funct … prog).