Changeset 2858


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

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

Files:
7 edited

Legend:

Unmodified
Added
Removed
  • driver/backendPrinter.ml

    r2856 r2858  
    4444let string_of_pos n = string_of_int (Extracted.Glue.int_of_matitapos n)
    4545
     46let print_ident n = "fun_" ^ string_of_pos n
     47
    4648let printing_pass_independent_params =
    4749 { Extracted.Joint_printer.print_String =
     
    5052 ; print_concat = (fun s1 s2 -> s1 ^ " " ^ s2)
    5153 ; print_empty = ""
    52  ; print_newline = "\n"
    53  ; print_ident = (fun n -> "fun_" ^ string_of_pos n)
     54 ; print_ident = print_ident
    5455 ; print_costlabel = (fun n -> "k_" ^ string_of_pos n)
    5556 ; print_label = (fun n -> "l_" ^ string_of_pos n)
     
    135136 }
    136137
    137 let print_LTL_program =
    138  Extracted.LTL_printer.print_LTL_program joint_LTL_LIN_printing_params
     138let rec list_of_matitalist =
     139 function
     140    Extracted.List.Nil -> []
     141  | Extracted.List.Cons (hd,tl) -> hd :: list_of_matitalist tl
     142
     143let print_graph l =
     144 let l = list_of_matitalist l in
     145  String.concat "\n\n"
     146   (List.map
     147     (fun {Extracted.Types.fst=ident; snd=commands} ->
     148       let commands = list_of_matitalist commands in
     149       print_ident ident ^ ":\n" ^
     150       String.concat "\n" commands
     151     )
     152    l)
     153
     154let print_LTL_program program =
     155 let res =
     156  Extracted.LTL_printer.print_LTL_program joint_LTL_LIN_printing_params program
     157 in
     158  "\n" ^ print_graph res ^ "\n"
  • extracted/joint_printer.ml

    r2854 r2858  
    390390                                                                 'string ->
    391391                                                                 'string);
    392                                                   print_newline : 'string;
    393392                                                  print_empty : 'string;
    394393                                                  print_ident : (AST.ident ->
     
    408407(** val printing_pass_independent_params_rect_Type4 :
    409408    ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
    410     -> 'a1 -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) ->
    411     (Graphs.label -> 'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 ->
    412     'a1) -> (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1
    413     printing_pass_independent_params -> 'a2 **)
     409    -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
     410    'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
     411    (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params
     412    -> 'a2 **)
    414413let rec printing_pass_independent_params_rect_Type4 h_mk_printing_pass_independent_params x_263 =
    415414  let { print_String = print_String0; print_keyword = print_keyword0;
    416     print_concat = print_concat0; print_newline = print_newline0;
    417     print_empty = print_empty0; print_ident = print_ident0; print_costlabel =
    418     print_costlabel0; print_label = print_label0; print_OpAccs =
    419     print_OpAccs0; print_Op1 = print_Op3; print_Op2 = print_Op4 } = x_263
     415    print_concat = print_concat0; print_empty = print_empty0; print_ident =
     416    print_ident0; print_costlabel = print_costlabel0; print_label =
     417    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
     418    print_Op2 = print_Op4 } = x_263
    420419  in
    421420  h_mk_printing_pass_independent_params print_String0 print_keyword0
    422     print_concat0 print_newline0 print_empty0 print_ident0 print_costlabel0
    423     print_label0 print_OpAccs0 print_Op3 print_Op4
     421    print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
     422    print_OpAccs0 print_Op3 print_Op4
    424423
    425424(** val printing_pass_independent_params_rect_Type5 :
    426425    ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
    427     -> 'a1 -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) ->
    428     (Graphs.label -> 'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 ->
    429     'a1) -> (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1
    430     printing_pass_independent_params -> 'a2 **)
     426    -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
     427    'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
     428    (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params
     429    -> 'a2 **)
    431430let rec printing_pass_independent_params_rect_Type5 h_mk_printing_pass_independent_params x_265 =
    432431  let { print_String = print_String0; print_keyword = print_keyword0;
    433     print_concat = print_concat0; print_newline = print_newline0;
    434     print_empty = print_empty0; print_ident = print_ident0; print_costlabel =
    435     print_costlabel0; print_label = print_label0; print_OpAccs =
    436     print_OpAccs0; print_Op1 = print_Op3; print_Op2 = print_Op4 } = x_265
     432    print_concat = print_concat0; print_empty = print_empty0; print_ident =
     433    print_ident0; print_costlabel = print_costlabel0; print_label =
     434    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
     435    print_Op2 = print_Op4 } = x_265
    437436  in
    438437  h_mk_printing_pass_independent_params print_String0 print_keyword0
    439     print_concat0 print_newline0 print_empty0 print_ident0 print_costlabel0
    440     print_label0 print_OpAccs0 print_Op3 print_Op4
     438    print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
     439    print_OpAccs0 print_Op3 print_Op4
    441440
    442441(** val printing_pass_independent_params_rect_Type3 :
    443442    ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
    444     -> 'a1 -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) ->
    445     (Graphs.label -> 'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 ->
    446     'a1) -> (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1
    447     printing_pass_independent_params -> 'a2 **)
     443    -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
     444    'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
     445    (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params
     446    -> 'a2 **)
    448447let rec printing_pass_independent_params_rect_Type3 h_mk_printing_pass_independent_params x_267 =
    449448  let { print_String = print_String0; print_keyword = print_keyword0;
    450     print_concat = print_concat0; print_newline = print_newline0;
    451     print_empty = print_empty0; print_ident = print_ident0; print_costlabel =
    452     print_costlabel0; print_label = print_label0; print_OpAccs =
    453     print_OpAccs0; print_Op1 = print_Op3; print_Op2 = print_Op4 } = x_267
     449    print_concat = print_concat0; print_empty = print_empty0; print_ident =
     450    print_ident0; print_costlabel = print_costlabel0; print_label =
     451    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
     452    print_Op2 = print_Op4 } = x_267
    454453  in
    455454  h_mk_printing_pass_independent_params print_String0 print_keyword0
    456     print_concat0 print_newline0 print_empty0 print_ident0 print_costlabel0
    457     print_label0 print_OpAccs0 print_Op3 print_Op4
     455    print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
     456    print_OpAccs0 print_Op3 print_Op4
    458457
    459458(** val printing_pass_independent_params_rect_Type2 :
    460459    ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
    461     -> 'a1 -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) ->
    462     (Graphs.label -> 'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 ->
    463     'a1) -> (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1
    464     printing_pass_independent_params -> 'a2 **)
     460    -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
     461    'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
     462    (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params
     463    -> 'a2 **)
    465464let rec printing_pass_independent_params_rect_Type2 h_mk_printing_pass_independent_params x_269 =
    466465  let { print_String = print_String0; print_keyword = print_keyword0;
    467     print_concat = print_concat0; print_newline = print_newline0;
    468     print_empty = print_empty0; print_ident = print_ident0; print_costlabel =
    469     print_costlabel0; print_label = print_label0; print_OpAccs =
    470     print_OpAccs0; print_Op1 = print_Op3; print_Op2 = print_Op4 } = x_269
     466    print_concat = print_concat0; print_empty = print_empty0; print_ident =
     467    print_ident0; print_costlabel = print_costlabel0; print_label =
     468    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
     469    print_Op2 = print_Op4 } = x_269
    471470  in
    472471  h_mk_printing_pass_independent_params print_String0 print_keyword0
    473     print_concat0 print_newline0 print_empty0 print_ident0 print_costlabel0
    474     print_label0 print_OpAccs0 print_Op3 print_Op4
     472    print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
     473    print_OpAccs0 print_Op3 print_Op4
    475474
    476475(** val printing_pass_independent_params_rect_Type1 :
    477476    ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
    478     -> 'a1 -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) ->
    479     (Graphs.label -> 'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 ->
    480     'a1) -> (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1
    481     printing_pass_independent_params -> 'a2 **)
     477    -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
     478    'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
     479    (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params
     480    -> 'a2 **)
    482481let rec printing_pass_independent_params_rect_Type1 h_mk_printing_pass_independent_params x_271 =
    483482  let { print_String = print_String0; print_keyword = print_keyword0;
    484     print_concat = print_concat0; print_newline = print_newline0;
    485     print_empty = print_empty0; print_ident = print_ident0; print_costlabel =
    486     print_costlabel0; print_label = print_label0; print_OpAccs =
    487     print_OpAccs0; print_Op1 = print_Op3; print_Op2 = print_Op4 } = x_271
     483    print_concat = print_concat0; print_empty = print_empty0; print_ident =
     484    print_ident0; print_costlabel = print_costlabel0; print_label =
     485    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
     486    print_Op2 = print_Op4 } = x_271
    488487  in
    489488  h_mk_printing_pass_independent_params print_String0 print_keyword0
    490     print_concat0 print_newline0 print_empty0 print_ident0 print_costlabel0
    491     print_label0 print_OpAccs0 print_Op3 print_Op4
     489    print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
     490    print_OpAccs0 print_Op3 print_Op4
    492491
    493492(** val printing_pass_independent_params_rect_Type0 :
    494493    ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
    495     -> 'a1 -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) ->
    496     (Graphs.label -> 'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 ->
    497     'a1) -> (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1
    498     printing_pass_independent_params -> 'a2 **)
     494    -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
     495    'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
     496    (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params
     497    -> 'a2 **)
    499498let rec printing_pass_independent_params_rect_Type0 h_mk_printing_pass_independent_params x_273 =
    500499  let { print_String = print_String0; print_keyword = print_keyword0;
    501     print_concat = print_concat0; print_newline = print_newline0;
    502     print_empty = print_empty0; print_ident = print_ident0; print_costlabel =
    503     print_costlabel0; print_label = print_label0; print_OpAccs =
    504     print_OpAccs0; print_Op1 = print_Op3; print_Op2 = print_Op4 } = x_273
     500    print_concat = print_concat0; print_empty = print_empty0; print_ident =
     501    print_ident0; print_costlabel = print_costlabel0; print_label =
     502    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
     503    print_Op2 = print_Op4 } = x_273
    505504  in
    506505  h_mk_printing_pass_independent_params print_String0 print_keyword0
    507     print_concat0 print_newline0 print_empty0 print_ident0 print_costlabel0
    508     print_label0 print_OpAccs0 print_Op3 print_Op4
     506    print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
     507    print_OpAccs0 print_Op3 print_Op4
    509508
    510509(** val print_String :
     
    523522  xxx.print_concat
    524523
    525 (** val print_newline : 'a1 printing_pass_independent_params -> 'a1 **)
    526 let rec print_newline xxx =
    527   xxx.print_newline
    528 
    529524(** val print_empty : 'a1 printing_pass_independent_params -> 'a1 **)
    530525let rec print_empty xxx =
     
    563558(** val printing_pass_independent_params_inv_rect_Type4 :
    564559    'a1 printing_pass_independent_params -> ((String.string -> 'a1) ->
    565     (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> (AST.ident ->
    566     'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
     560    (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
     561    (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
    567562    (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2
    568563    -> 'a1) -> __ -> 'a2) -> 'a2 **)
     
    572567(** val printing_pass_independent_params_inv_rect_Type3 :
    573568    'a1 printing_pass_independent_params -> ((String.string -> 'a1) ->
    574     (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> (AST.ident ->
    575     'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
     569    (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
     570    (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
    576571    (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2
    577572    -> 'a1) -> __ -> 'a2) -> 'a2 **)
     
    581576(** val printing_pass_independent_params_inv_rect_Type2 :
    582577    'a1 printing_pass_independent_params -> ((String.string -> 'a1) ->
    583     (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> (AST.ident ->
    584     'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
     578    (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
     579    (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
    585580    (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2
    586581    -> 'a1) -> __ -> 'a2) -> 'a2 **)
     
    590585(** val printing_pass_independent_params_inv_rect_Type1 :
    591586    'a1 printing_pass_independent_params -> ((String.string -> 'a1) ->
    592     (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> (AST.ident ->
    593     'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
     587    (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
     588    (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
    594589    (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2
    595590    -> 'a1) -> __ -> 'a2) -> 'a2 **)
     
    599594(** val printing_pass_independent_params_inv_rect_Type0 :
    600595    'a1 printing_pass_independent_params -> ((String.string -> 'a1) ->
    601     (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> (AST.ident ->
    602     'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
     596    (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
     597    (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) ->
    603598    (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2
    604599    -> 'a1) -> __ -> 'a2) -> 'a2 **)
     
    612607  Logic.eq_rect_Type2 x
    613608    (let { print_String = a0; print_keyword = a10; print_concat = a2;
    614        print_newline = a3; print_empty = a4; print_ident = a5;
    615        print_costlabel = a6; print_label = a7; print_OpAccs = a8; print_Op1 =
    616        a9; print_Op2 = a100 } = x
     609       print_empty = a3; print_ident = a4; print_costlabel = a5;
     610       print_label = a6; print_OpAccs = a7; print_Op1 = a8; print_Op2 =
     611       a9 } = x
    617612     in
    618     Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __)) y
     613    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __)) y
    619614
    620615type 'string printing_params = { print_pass_ind : 'string
     
    10481043    Obj.magic (fun _ dH -> dH __ __ __)) y
    10491044
     1045(** val pm_choose_with_pref :
     1046    'a1 PositiveMap.positive_map -> Positive.pos Types.option ->
     1047    ((Positive.pos, 'a1) Types.prod, 'a1 PositiveMap.positive_map) Types.prod
     1048    Types.option **)
     1049let pm_choose_with_pref m = function
     1050| Types.None -> PositiveMap.pm_choose m
     1051| Types.Some p ->
     1052  (match PositiveMap.pm_try_remove p m with
     1053   | Types.None -> PositiveMap.pm_choose m
     1054   | Types.Some res ->
     1055     let { Types.fst = a; Types.snd = m' } = res in
     1056     Types.Some { Types.fst = { Types.fst = p; Types.snd = a }; Types.snd =
     1057     m' })
     1058
     1059(** val visit_graph :
     1060    ('a1 -> Positive.pos Types.option) -> (Positive.pos -> 'a1 -> 'a2 -> 'a2)
     1061    -> 'a2 -> Positive.pos Types.option -> 'a1 PositiveMap.positive_map ->
     1062    Nat.nat -> 'a2 **)
     1063let rec visit_graph next f b n m = function
     1064| Nat.O -> b
     1065| Nat.S y ->
     1066  (match pm_choose_with_pref m n with
     1067   | Types.None -> b
     1068   | Types.Some res ->
     1069     let { Types.fst = eta2; Types.snd = m' } = res in
     1070     let { Types.fst = pos; Types.snd = a } = eta2 in
     1071     visit_graph next f (f pos a b) (next a) m' y)
     1072
    10501073(** val graph_code_iteration_params :
    10511074    Joint.graph_params -> AST.ident List.list -> 'a1 printing_params -> 'a1
    10521075    code_iteration_params **)
    10531076let graph_code_iteration_params gp globals pp =
    1054   { fold_code = (fun _ f ->
    1055     Obj.magic (Graphs.graph_fold (fun n -> Obj.magic f n))); print_succ =
    1056     (Obj.magic pp.print_pass_ind.print_label); print_code_point =
    1057     (Obj.magic pp.print_pass_ind.print_label) }
     1077  { fold_code = (fun _ f m a ->
     1078    visit_graph (fun stmt ->
     1079      match Joint.stmt_implicit_label (Joint.gp_to_p__o__stmt_pars gp)
     1080              globals stmt with
     1081      | Types.None -> Types.None
     1082      | Types.Some label -> let p = label in Types.Some p) (fun n ->
     1083      Obj.magic f n) a Types.None (let m' = Obj.magic m in m')
     1084      (Identifiers.id_map_size PreIdentifiers.LabelTag (Obj.magic m)));
     1085    print_succ = (Obj.magic pp.print_pass_ind.print_label);
     1086    print_code_point = (Obj.magic pp.print_pass_ind.print_label) }
    10581087
    10591088(** val print_list :
     
    11851214(** val print_joint_internal_function :
    11861215    Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> 'a1
    1187     printing_params -> Joint.joint_internal_function -> 'a1 **)
     1216    printing_params -> Joint.joint_internal_function -> 'a1 List.list **)
    11881217let print_joint_internal_function p globals cip pp f =
    1189   fold_code0 p globals cip (fun cp stmt acc ->
    1190     print_list pp.print_pass_ind (List.Cons ((cip.print_code_point cp),
    1191       (List.Cons ((print_joint_statement p globals pp cip stmt), (List.Cons
    1192       (pp.print_pass_ind.print_newline, (List.Cons (acc, List.Nil)))))))))
    1193     f.Joint.joint_if_code pp.print_pass_ind.print_empty
     1218  fold_code0 p globals cip (fun cp stmt acc -> List.Cons
     1219    ((print_list pp.print_pass_ind (List.Cons ((cip.print_code_point cp),
     1220       (List.Cons ((print_joint_statement p globals pp cip stmt),
     1221       List.Nil))))), acc)) f.Joint.joint_if_code List.Nil
    11941222
    11951223(** val print_joint_function :
    11961224    Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> 'a1
    1197     printing_params -> Joint.joint_function -> 'a1 **)
     1225    printing_params -> Joint.joint_function -> 'a1 List.list **)
    11981226let print_joint_function p globals cip pp = function
    11991227| AST.Internal f0 ->
    12001228  print_joint_internal_function p globals cip pp (Types.pi1 f0)
    1201 | AST.External f0 -> pp.print_pass_ind.print_empty
     1229| AST.External f0 -> List.Nil
    12021230
    12031231(** val print_joint_program :
    12041232    Joint.params -> 'a1 printing_params -> Joint.joint_program -> 'a1
    1205     code_iteration_params -> 'a1 **)
     1233    code_iteration_params -> (AST.ident, 'a1 List.list) Types.prod List.list **)
    12061234let print_joint_program p pp prog cip =
    1207   List.foldr (fun f ->
    1208     pp.print_pass_ind.print_concat
    1209       (print_joint_function p
    1210         (List.map (fun x -> x.Types.fst.Types.fst) prog.AST.prog_vars) cip pp
    1211         f.Types.snd)) pp.print_pass_ind.print_empty prog.AST.prog_funct
    1212 
     1235  List.foldr (fun f acc -> List.Cons ({ Types.fst = f.Types.fst; Types.snd =
     1236    (print_joint_function p
     1237      (List.map (fun x -> x.Types.fst.Types.fst) prog.AST.prog_vars) cip pp
     1238      f.Types.snd) }, acc)) List.Nil prog.AST.prog_funct
     1239
  • extracted/joint_printer.mli

    r2854 r2858  
    191191                                                                 'string ->
    192192                                                                 'string);
    193                                                   print_newline : 'string;
    194193                                                  print_empty : 'string;
    195194                                                  print_ident : (AST.ident ->
     
    209208val printing_pass_independent_params_rect_Type4 :
    210209  ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
    211   -> 'a1 -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) ->
    212   (Graphs.label -> 'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 ->
    213   'a1) -> (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1
    214   printing_pass_independent_params -> 'a2
     210  -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
     211  'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
     212  (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params ->
     213  'a2
    215214
    216215val printing_pass_independent_params_rect_Type5 :
    217216  ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
    218   -> 'a1 -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) ->
    219   (Graphs.label -> 'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 ->
    220   'a1) -> (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1
    221   printing_pass_independent_params -> 'a2
     217  -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
     218  'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
     219  (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params ->
     220  'a2
    222221
    223222val printing_pass_independent_params_rect_Type3 :
    224223  ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
    225   -> 'a1 -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) ->
    226   (Graphs.label -> 'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 ->
    227   'a1) -> (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1
    228   printing_pass_independent_params -> 'a2
     224  -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
     225  'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
     226  (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params ->
     227  'a2
    229228
    230229val printing_pass_independent_params_rect_Type2 :
    231230  ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
    232   -> 'a1 -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) ->
    233   (Graphs.label -> 'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 ->
    234   'a1) -> (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1
    235   printing_pass_independent_params -> 'a2
     231  -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
     232  'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
     233  (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params ->
     234  'a2
    236235
    237236val printing_pass_independent_params_rect_Type1 :
    238237  ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
    239   -> 'a1 -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) ->
    240   (Graphs.label -> 'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 ->
    241   'a1) -> (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1
    242   printing_pass_independent_params -> 'a2
     238  -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
     239  'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
     240  (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params ->
     241  'a2
    243242
    244243val printing_pass_independent_params_rect_Type0 :
    245244  ((String.string -> 'a1) -> (keyword -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1
    246   -> 'a1 -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) ->
    247   (Graphs.label -> 'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 ->
    248   'a1) -> (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1
    249   printing_pass_independent_params -> 'a2
     245  -> (AST.ident -> 'a1) -> (CostLabel.costlabel -> 'a1) -> (Graphs.label ->
     246  'a1) -> (BackEndOps.opAccs -> 'a1) -> (BackEndOps.op1 -> 'a1) ->
     247  (BackEndOps.op2 -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params ->
     248  'a2
    250249
    251250val print_String :
     
    256255val print_concat : 'a1 printing_pass_independent_params -> 'a1 -> 'a1 -> 'a1
    257256
    258 val print_newline : 'a1 printing_pass_independent_params -> 'a1
    259 
    260257val print_empty : 'a1 printing_pass_independent_params -> 'a1
    261258
     
    276273val printing_pass_independent_params_inv_rect_Type4 :
    277274  'a1 printing_pass_independent_params -> ((String.string -> 'a1) -> (keyword
    278   -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> (AST.ident -> 'a1) ->
     275  -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
    279276  (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) -> (BackEndOps.opAccs
    280277  -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2 -> 'a1) -> __ -> 'a2)
     
    283280val printing_pass_independent_params_inv_rect_Type3 :
    284281  'a1 printing_pass_independent_params -> ((String.string -> 'a1) -> (keyword
    285   -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> (AST.ident -> 'a1) ->
     282  -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
    286283  (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) -> (BackEndOps.opAccs
    287284  -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2 -> 'a1) -> __ -> 'a2)
     
    290287val printing_pass_independent_params_inv_rect_Type2 :
    291288  'a1 printing_pass_independent_params -> ((String.string -> 'a1) -> (keyword
    292   -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> (AST.ident -> 'a1) ->
     289  -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
    293290  (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) -> (BackEndOps.opAccs
    294291  -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2 -> 'a1) -> __ -> 'a2)
     
    297294val printing_pass_independent_params_inv_rect_Type1 :
    298295  'a1 printing_pass_independent_params -> ((String.string -> 'a1) -> (keyword
    299   -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> (AST.ident -> 'a1) ->
     296  -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
    300297  (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) -> (BackEndOps.opAccs
    301298  -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2 -> 'a1) -> __ -> 'a2)
     
    304301val printing_pass_independent_params_inv_rect_Type0 :
    305302  'a1 printing_pass_independent_params -> ((String.string -> 'a1) -> (keyword
    306   -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> (AST.ident -> 'a1) ->
     303  -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> (AST.ident -> 'a1) ->
    307304  (CostLabel.costlabel -> 'a1) -> (Graphs.label -> 'a1) -> (BackEndOps.opAccs
    308305  -> 'a1) -> (BackEndOps.op1 -> 'a1) -> (BackEndOps.op2 -> 'a1) -> __ -> 'a2)
     
    545542  code_iteration_params -> __
    546543
     544val pm_choose_with_pref :
     545  'a1 PositiveMap.positive_map -> Positive.pos Types.option ->
     546  ((Positive.pos, 'a1) Types.prod, 'a1 PositiveMap.positive_map) Types.prod
     547  Types.option
     548
     549val visit_graph :
     550  ('a1 -> Positive.pos Types.option) -> (Positive.pos -> 'a1 -> 'a2 -> 'a2)
     551  -> 'a2 -> Positive.pos Types.option -> 'a1 PositiveMap.positive_map ->
     552  Nat.nat -> 'a2
     553
    547554val graph_code_iteration_params :
    548555  Joint.graph_params -> AST.ident List.list -> 'a1 printing_params -> 'a1
     
    569576val print_joint_internal_function :
    570577  Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> 'a1
    571   printing_params -> Joint.joint_internal_function -> 'a1
     578  printing_params -> Joint.joint_internal_function -> 'a1 List.list
    572579
    573580val print_joint_function :
    574581  Joint.params -> AST.ident List.list -> 'a1 code_iteration_params -> 'a1
    575   printing_params -> Joint.joint_function -> 'a1
     582  printing_params -> Joint.joint_function -> 'a1 List.list
    576583
    577584val print_joint_program :
    578585  Joint.params -> 'a1 printing_params -> Joint.joint_program -> 'a1
    579   code_iteration_params -> 'a1
    580 
     586  code_iteration_params -> (AST.ident, 'a1 List.list) Types.prod List.list
     587
  • extracted/lTL_printer.ml

    r2854 r2858  
    112112
    113113(** val print_LTL_program :
    114     'a1 Joint_printer.printing_params -> LTL.ltl_program -> 'a1 **)
     114    'a1 Joint_printer.printing_params -> LTL.ltl_program -> (AST.ident, 'a1
     115    List.list) Types.prod List.list **)
    115116let print_LTL_program pp prog =
    116117  Joint_printer.print_joint_program (Joint.graph_params_to_params LTL.lTL) pp
  • extracted/lTL_printer.mli

    r2854 r2858  
    112112
    113113val print_LTL_program :
    114   'a1 Joint_printer.printing_params -> LTL.ltl_program -> 'a1
     114  'a1 Joint_printer.printing_params -> LTL.ltl_program -> (AST.ident, 'a1
     115  List.list) Types.prod List.list
    115116
  • 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.