Ignore:
Timestamp:
Mar 27, 2013, 6:05:41 PM (7 years ago)
Author:
sacerdot
Message:

Pretty priting of LIN implemented.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/joint_printer.ma

    r2859 r2982  
    4646 ; print_OpAccs: OpAccs → string
    4747 ; print_Op1: Op1 → string
    48  ; print_Op2: Op2 → string }.
     48 ; print_Op2: Op2 → string
     49 ; print_nat: nat → string }.
    4950
    5051record printing_params (string: Type[0]) (P: unserialized_params) : Type[0] ≝
     
    6667 }.
    6768
    68 record code_iteration_params (string: Type[0]) (p:params) (globals) : Type[1] ≝
    69  { fold_code:
    70     ∀A:Type[0].
    71      (code_point p → joint_statement p globals → A → A) →
    72       codeT p globals → A → A
    73  ; print_succ: succ … p → string
     69record print_serialization_params (string: Type[0]) (p:params) : Type[1] ≝
     70 { print_succ: succ … p → string
    7471 ; print_code_point: code_point p → string
     72 }.
     73
     74record code_iteration_params (string: Type[0]) (p:params) (statementT: Type[0])
     75  (globals) : Type[1] ≝
     76 { cip_print_serialization_params :> print_serialization_params string p
     77 ; fold_code:
     78    ∀A:Type[0]. (code_point p → statementT → A → A) → codeT p globals → A → A
     79 ; print_statementT: statementT → string
    7580 }.
    7681
     
    95100       let 〈pos,a,M'〉 ≝ res in
    96101        visit_graph A next B f (f pos a b) (next a) M' y ]].
    97 
    98 definition graph_code_iteration_params:
    99  ∀string,graph_params,globals.
    100   printing_params string (graph_params_to_params graph_params) →
    101    code_iteration_params string (graph_params_to_params graph_params) globals ≝
    102  λstring,gp,globals,pp.
    103   mk_code_iteration_params ???
    104    (λA.λf:code_point (graph_params_to_params …) → ?.λM.λa.
    105      visit_graph (joint_statement … gp globals)
    106      (λstmt. match stmt_implicit_label ?? stmt with
    107        [ None ⇒ None … | Some label ⇒ match label with [an_identifier p ⇒ Some … p]])
    108      ? (λn. f (an_identifier … n)) a (Some … one)
    109      (match M with [an_id_map M' ⇒ M']) (id_map_size … M))
    110    (print_label … pp) (print_label … pp).
    111102
    112103definition print_list:
     
    219210definition print_joint_statement:
    220211 ∀p:params.∀globals. ∀string. printing_params string p →
    221   code_iteration_params string p globals → joint_statement p globals → string ≝
     212  print_serialization_params string p → joint_statement p globals → string ≝
    222213 λp,globals,string,pp,cip,stmt.
    223214  match stmt with
     
    232223        print_label … pp arg3 ]].
    233224
     225definition graph_print_serialization_params:
     226 ∀string,graph_params.
     227  printing_params string (graph_params_to_params graph_params) →
     228   print_serialization_params string (graph_params_to_params graph_params) ≝
     229 λstring,gp,pp.
     230  mk_print_serialization_params … (print_label … pp) (print_label … pp).
     231
     232definition graph_code_iteration_params:
     233 ∀string,graph_params,globals.
     234  printing_params string (graph_params_to_params graph_params) →
     235   code_iteration_params string (graph_params_to_params graph_params) … globals ≝
     236 λstring,gp,globals,pp.
     237  mk_code_iteration_params …
     238   (graph_print_serialization_params … pp)
     239   (λA.λf:code_point (graph_params_to_params …) → ?.λM.λa.
     240     visit_graph (joint_statement … gp globals)
     241     (λstmt. match stmt_implicit_label ?? stmt with
     242       [ None ⇒ None … | Some label ⇒ match label with [an_identifier p ⇒ Some … p]])
     243     ? (λn. f (an_identifier … n)) a (Some … one)
     244     (match M with [an_id_map M' ⇒ M']) (id_map_size … M))
     245     (print_joint_statement … pp … (graph_print_serialization_params … pp)).
     246
     247definition lin_print_serialization_params:
     248 ∀string,lin_params.
     249  printing_params string (lin_params_to_params lin_params) →
     250   print_serialization_params string (lin_params_to_params lin_params) ≝
     251 λstring,gp,pp.
     252  mk_print_serialization_params … (λ_.print_empty … pp) (print_nat … pp).
     253
     254definition lin_code_iteration_params:
     255 ∀string,lin_params,globals.
     256  printing_params string (lin_params_to_params lin_params) →
     257   code_iteration_params string (lin_params_to_params lin_params) ? globals ≝
     258 λstring,lp,globals,pp.
     259  mk_code_iteration_params ?? (? × (joint_statement ??)) ?
     260   (lin_print_serialization_params … pp)
     261   (λA.λf:code_point (lin_params_to_params …) → ?.λM:codeT lp globals.
     262    λa.
     263     \snd (foldr ??
     264      (λx.λres. let 〈pc,res'〉 ≝ res in 〈S pc,f pc x res'〉)
     265      〈0,a〉 M))
     266     (λlinstr.
     267       match \fst linstr with
     268       [ None ⇒
     269          print_joint_statement … pp … (lin_print_serialization_params … pp)
     270           (\snd linstr)
     271       | Some l ⇒
     272          print_list ? pp
     273           [ print_label … pp l;
     274             print_joint_statement … pp … (lin_print_serialization_params … pp)
     275              (\snd linstr) ]]).
     276
    234277definition print_joint_internal_function:
    235  ∀p:params. ∀globals. ∀string. code_iteration_params string p globals →
     278 ∀p:params. ∀lines. ∀globals. ∀string. code_iteration_params string p lines globals →
    236279  printing_params string p → joint_internal_function p globals → list string
    237 ≝ λp,globals,string,cip,pp,f.
     280≝ λp,lines,globals,string,cip,pp,f.
    238281   fold_code … cip …
    239282    (λcp.λstmt.λacc.
    240       print_list pp
     283      print_list ? pp
    241284       [ print_code_point … cip cp;
    242          print_joint_statement … pp cip stmt ]::acc)
     285         print_statementT … cip stmt ]::acc)
    243286    (joint_if_code … f) [].
    244287
    245288definition print_joint_function:
    246  ∀p:params. ∀globals. ∀string. code_iteration_params string p globals → printing_params string p →
     289 ∀p:params. ∀lines. ∀globals. ∀string. code_iteration_params string p lines globals → printing_params string p →
    247290  joint_function p globals → list string ≝
    248  λp,globals,string,cip,pp,f.
     291 λp,lines,globals,string,cip,pp,f.
    249292  match f with
    250293  [ Internal f ⇒ print_joint_internal_function … cip … pp f
     
    252295
    253296definition print_joint_program:
    254  ∀p:params. ∀string.
     297 ∀p:params. ∀lines. ∀string.
    255298  printing_params string p →
    256299  ∀prog:joint_program p.
    257    code_iteration_params string p (map … (λx. \fst (\fst x)) (prog_vars ?? prog)) →
     300   code_iteration_params string p lines (map … (λx. \fst (\fst x)) (prog_vars ?? prog)) →
    258301   list (ident × (list string)) ≝
    259  λp,string,pp,prog,cip.
     302 λp,lines,string,pp,prog,cip.
    260303  foldr ?? (λf,acc. 〈\fst f,print_joint_function … cip … pp (\snd f)〉 :: acc)
    261304   [] (prog_funct … prog).
Note: See TracChangeset for help on using the changeset viewer.