Changeset 2858 for src


Ignore:
Timestamp:
Mar 13, 2013, 12:52:16 AM (7 years ago)
Author:
sacerdot
Message:

Trying to pretty print the code graph in visit order.
Slightly bugged ATM, IKD why.

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/LTL/LTL_printer.ma

    r2848 r2858  
    1717
    1818definition print_LTL_program:
    19  ∀string. printing_params string LTL → ltl_program → string ≝
     19 ∀string. printing_params string LTL → ltl_program →
     20  list (ident × (list string)) ≝
    2021 λstring,pp,prog. print_joint_program … pp prog (graph_code_iteration_params … pp).
  • src/joint/joint_printer.ma

    r2853 r2858  
    4040 ; print_keyword: keyword → string
    4141 ; print_concat: string → string → string
    42  ; print_newline: string
    4342 ; print_empty: string
    4443 ; print_ident: ident → string
     
    7675 }.
    7776
     77definition pm_choose_with_pref:
     78 ∀A:Type[0]. positive_map A → option Pos → option (Pos × A × (positive_map A)) ≝
     79 λA,M,n.
     80  match n with
     81  [ None ⇒ pm_choose A M
     82  | Some p ⇒
     83     match pm_try_remove A p M with
     84     [ None ⇒ pm_choose A M
     85     | Some res ⇒ let 〈a,M'〉 ≝ res in Some … 〈p,a,M'〉 ]].
     86
     87let rec visit_graph (A:Type[0]) (next: A → option Pos) (B:Type[0])
     88 (f: Pos → A → B → B) (b:B) (n: option Pos) (M: positive_map A) (x:nat) on x : B ≝
     89 match x with
     90 [ O ⇒ b (* Dummy, this should never happen for a large enough value of x *)
     91 | S y ⇒
     92    match pm_choose_with_pref A M n with
     93    [ None ⇒ b
     94    | Some res ⇒
     95       let 〈pos,a,M'〉 ≝ res in
     96        visit_graph A next B f (f pos a b) (next a) M' y ]].
     97
    7898definition graph_code_iteration_params:
    7999 ∀string,graph_params,globals.
     
    82102 λstring,gp,globals,pp.
    83103  mk_code_iteration_params ???
    84    (λA.λf:code_point (graph_params_to_params …) → ?.
    85      graph_fold … (λn. f (an_identifier … n)) …)
     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 (None …)
     109     (match M with [an_id_map M' ⇒ M']) (id_map_size … M))
    86110   (print_label … pp) (print_label … pp).
    87111
     
    210234definition print_joint_internal_function:
    211235 ∀p:params. ∀globals. ∀string. code_iteration_params string p globals →
    212   printing_params string p → joint_internal_function p globals → string
     236  printing_params string p → joint_internal_function p globals → list string
    213237≝ λp,globals,string,cip,pp,f.
    214238   fold_code … cip …
     
    216240      print_list … pp
    217241       [ print_code_point … cip cp;
    218          print_joint_statement … pp cip stmt;
    219          print_newline … pp;
    220          acc])
    221     (joint_if_code … f) (print_empty … pp).
     242         print_joint_statement … pp cip stmt ]::acc)
     243    (joint_if_code … f) [].
    222244
    223245definition print_joint_function:
    224246 ∀p:params. ∀globals. ∀string. code_iteration_params string p globals → printing_params string p →
    225   joint_function p globals → string ≝
     247  joint_function p globals → list string ≝
    226248 λp,globals,string,cip,pp,f.
    227249  match f with
    228250  [ Internal f ⇒ print_joint_internal_function … cip … pp f
    229   | External f ⇒ print_empty … pp ].
     251  | External f ⇒ [] ].
    230252
    231253definition print_joint_program:
     
    233255  printing_params string p →
    234256  ∀prog:joint_program p.
    235    code_iteration_params string p (map … (λx. \fst (\fst x)) (prog_vars ?? prog)) → string ≝
     257   code_iteration_params string p (map … (λx. \fst (\fst x)) (prog_vars ?? prog)) →
     258   list (ident × (list string)) ≝
    236259 λp,string,pp,prog,cip.
    237   foldr ?? (λf. print_concat … pp (print_joint_function … cip … pp (\snd f)))
    238    (print_empty … pp) (prog_funct … prog).
     260  foldr ?? (λf,acc. 〈\fst f,print_joint_function … cip … pp (\snd f)〉 :: acc)
     261   [] (prog_funct … prog).
Note: See TracChangeset for help on using the changeset viewer.