Code_Printer.tuplify
authorhaftmann
Tue Aug 31 13:15:35 2010 +0200 (2010-08-31)
changeset 38922ec2a8efd8990
parent 38921 15f8cffdbf5d
child 38923 79d7f2b4cf71
Code_Printer.tuplify
src/Tools/Code/code_eval.ML
src/Tools/Code/code_ml.ML
src/Tools/Code/code_printer.ML
src/Tools/Code/code_scala.ML
     1.1 --- a/src/Tools/Code/code_eval.ML	Tue Aug 31 13:08:58 2010 +0200
     1.2 +++ b/src/Tools/Code/code_eval.ML	Tue Aug 31 13:15:35 2010 +0200
     1.3 @@ -150,7 +150,7 @@
     1.4    let
     1.5      val k = Code.args_number thy const;
     1.6      fun pr pr' fxy ts = Code_Printer.brackify fxy
     1.7 -      (const' :: the_list (Code_ML.print_tuple pr' Code_Printer.BR (map fst ts)));
     1.8 +      (const' :: the_list (Code_Printer.tuplify pr' Code_Printer.BR (map fst ts)));
     1.9    in
    1.10      thy
    1.11      |> Code_Target.add_syntax_const target const (SOME (Code_Printer.simple_const_syntax (k, pr)))
     2.1 --- a/src/Tools/Code/code_ml.ML	Tue Aug 31 13:08:58 2010 +0200
     2.2 +++ b/src/Tools/Code/code_ml.ML	Tue Aug 31 13:15:35 2010 +0200
     2.3 @@ -8,8 +8,6 @@
     2.4  sig
     2.5    val target_SML: string
     2.6    val target_OCaml: string
     2.7 -  val print_tuple: (Code_Printer.fixity -> 'a -> Pretty.T)
     2.8 -    -> Code_Printer.fixity -> 'a list -> Pretty.T option
     2.9    val setup: theory -> theory
    2.10  end;
    2.11  
    2.12 @@ -54,9 +52,9 @@
    2.13    | print_product print [x] = SOME (print x)
    2.14    | print_product print xs = (SOME o enum " *" "" "") (map print xs);
    2.15  
    2.16 -fun print_tuple _ _ [] = NONE
    2.17 -  | print_tuple print fxy [x] = SOME (print fxy x)
    2.18 -  | print_tuple print _ xs = SOME (enum "," "(" ")" (map (print NOBR) xs));
    2.19 +fun tuplify _ _ [] = NONE
    2.20 +  | tuplify print fxy [x] = SOME (print fxy x)
    2.21 +  | tuplify print _ xs = SOME (enum "," "(" ")" (map (print NOBR) xs));
    2.22  
    2.23  
    2.24  (** SML serializer **)
    2.25 @@ -92,7 +90,7 @@
    2.26              | classrels => brackets
    2.27                  [enum " o" "(" ")" (map (str o deresolve) classrels), v_p]
    2.28            end
    2.29 -    and print_dicts is_pseudo_fun = print_tuple (print_dict is_pseudo_fun);
    2.30 +    and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
    2.31      val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
    2.32        (map_index (fn (i, _) => DictVar ([], (v, (i, length sort)))) sort));
    2.33      fun print_term is_pseudo_fun some_thm vars fxy (IConst c) =
    2.34 @@ -125,7 +123,7 @@
    2.35          let val k = length function_typs in
    2.36            if k < 2 orelse length ts = k
    2.37            then (str o deresolve) c
    2.38 -            :: the_list (print_tuple (print_term is_pseudo_fun some_thm vars) BR ts)
    2.39 +            :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
    2.40            else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)]
    2.41          end
    2.42        else if is_pseudo_fun c
    2.43 @@ -393,7 +391,7 @@
    2.44              else "_" ^ first_upper v ^ string_of_int (i+1))
    2.45            |> fold_rev (fn classrel => fn p =>
    2.46                 Pretty.block [p, str ".", (str o deresolve) classrel]) classrels
    2.47 -    and print_dicts is_pseudo_fun = print_tuple (print_dict is_pseudo_fun);
    2.48 +    and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
    2.49      val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
    2.50        (map_index (fn (i, _) => DictVar ([], (v, (i, length sort)))) sort));
    2.51      fun print_term is_pseudo_fun some_thm vars fxy (IConst c) =
    2.52 @@ -423,7 +421,7 @@
    2.53          let val k = length tys in
    2.54            if length ts = k
    2.55            then (str o deresolve) c
    2.56 -            :: the_list (print_tuple (print_term is_pseudo_fun some_thm vars) BR ts)
    2.57 +            :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
    2.58            else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)]
    2.59          end
    2.60        else if is_pseudo_fun c
     3.1 --- a/src/Tools/Code/code_printer.ML	Tue Aug 31 13:08:58 2010 +0200
     3.2 +++ b/src/Tools/Code/code_printer.ML	Tue Aug 31 13:15:35 2010 +0200
     3.3 @@ -68,6 +68,8 @@
     3.4    val brackify_infix: int * lrx -> fixity -> Pretty.T * Pretty.T * Pretty.T -> Pretty.T
     3.5    val brackify_block: fixity -> Pretty.T -> Pretty.T list -> Pretty.T -> Pretty.T
     3.6    val applify: string -> string -> ('a -> Pretty.T) -> fixity -> Pretty.T -> 'a list -> Pretty.T
     3.7 +  val tuplify: (fixity -> 'a -> Pretty.T) -> fixity -> 'a list -> Pretty.T option
     3.8 +
     3.9  
    3.10    type tyco_syntax
    3.11    type simple_const_syntax
    3.12 @@ -244,6 +246,10 @@
    3.13        (if (fixity BR fxy_ctxt) then enclose "(" ")" else Pretty.block)
    3.14          (p @@ enum "," opn cls (map f ps));
    3.15  
    3.16 +fun tuplify _ _ [] = NONE
    3.17 +  | tuplify print fxy [x] = SOME (print fxy x)
    3.18 +  | tuplify print _ xs = SOME (enum "," "(" ")" (map (print NOBR) xs));
    3.19 +
    3.20  
    3.21  (* generic syntax *)
    3.22  
     4.1 --- a/src/Tools/Code/code_scala.ML	Tue Aug 31 13:08:58 2010 +0200
     4.2 +++ b/src/Tools/Code/code_scala.ML	Tue Aug 31 13:15:35 2010 +0200
     4.3 @@ -171,8 +171,8 @@
     4.4                else aux_params vars1 (map (fst o fst) eqs);
     4.5              val vars2 = intro_vars params vars1;
     4.6              val (tys', ty') = Code_Thingol.unfold_fun_n (length params) ty;
     4.7 -            fun print_tuple [p] = p
     4.8 -              | print_tuple ps = enum "," "(" ")" ps;
     4.9 +            fun tuplify [p] = p
    4.10 +              | tuplify ps = enum "," "(" ")" ps;
    4.11              fun print_rhs vars' ((_, t), (some_thm, _)) =
    4.12                print_term tyvars false some_thm vars' NOBR t;
    4.13              fun print_clause (eq as ((ts, _), (some_thm, _))) =
    4.14 @@ -181,7 +181,7 @@
    4.15                    (insert (op =)) ts []) vars1;
    4.16                in
    4.17                  concat [str "case",
    4.18 -                  print_tuple (map (print_term tyvars true some_thm vars' NOBR) ts),
    4.19 +                  tuplify (map (print_term tyvars true some_thm vars' NOBR) ts),
    4.20                    str "=>", print_rhs vars' eq]
    4.21                end;
    4.22              val head = print_defhead tyvars vars2 name vs params tys' ty';
    4.23 @@ -189,7 +189,7 @@
    4.24              concat [head, print_rhs vars2 (hd eqs)]
    4.25            else
    4.26              Pretty.block_enclose
    4.27 -              (concat [head, print_tuple (map (str o lookup_var vars2) params),
    4.28 +              (concat [head, tuplify (map (str o lookup_var vars2) params),
    4.29                  str "match", str "{"], str "}")
    4.30                (map print_clause eqs)
    4.31            end;