src/Tools/Code/code_ml.ML
changeset 38922 ec2a8efd8990
parent 38921 15f8cffdbf5d
child 38923 79d7f2b4cf71
     1.1 --- a/src/Tools/Code/code_ml.ML	Tue Aug 31 13:08:58 2010 +0200
     1.2 +++ b/src/Tools/Code/code_ml.ML	Tue Aug 31 13:15:35 2010 +0200
     1.3 @@ -8,8 +8,6 @@
     1.4  sig
     1.5    val target_SML: string
     1.6    val target_OCaml: string
     1.7 -  val print_tuple: (Code_Printer.fixity -> 'a -> Pretty.T)
     1.8 -    -> Code_Printer.fixity -> 'a list -> Pretty.T option
     1.9    val setup: theory -> theory
    1.10  end;
    1.11  
    1.12 @@ -54,9 +52,9 @@
    1.13    | print_product print [x] = SOME (print x)
    1.14    | print_product print xs = (SOME o enum " *" "" "") (map print xs);
    1.15  
    1.16 -fun print_tuple _ _ [] = NONE
    1.17 -  | print_tuple print fxy [x] = SOME (print fxy x)
    1.18 -  | print_tuple print _ xs = SOME (enum "," "(" ")" (map (print NOBR) xs));
    1.19 +fun tuplify _ _ [] = NONE
    1.20 +  | tuplify print fxy [x] = SOME (print fxy x)
    1.21 +  | tuplify print _ xs = SOME (enum "," "(" ")" (map (print NOBR) xs));
    1.22  
    1.23  
    1.24  (** SML serializer **)
    1.25 @@ -92,7 +90,7 @@
    1.26              | classrels => brackets
    1.27                  [enum " o" "(" ")" (map (str o deresolve) classrels), v_p]
    1.28            end
    1.29 -    and print_dicts is_pseudo_fun = print_tuple (print_dict is_pseudo_fun);
    1.30 +    and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
    1.31      val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
    1.32        (map_index (fn (i, _) => DictVar ([], (v, (i, length sort)))) sort));
    1.33      fun print_term is_pseudo_fun some_thm vars fxy (IConst c) =
    1.34 @@ -125,7 +123,7 @@
    1.35          let val k = length function_typs in
    1.36            if k < 2 orelse length ts = k
    1.37            then (str o deresolve) c
    1.38 -            :: the_list (print_tuple (print_term is_pseudo_fun some_thm vars) BR ts)
    1.39 +            :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
    1.40            else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)]
    1.41          end
    1.42        else if is_pseudo_fun c
    1.43 @@ -393,7 +391,7 @@
    1.44              else "_" ^ first_upper v ^ string_of_int (i+1))
    1.45            |> fold_rev (fn classrel => fn p =>
    1.46                 Pretty.block [p, str ".", (str o deresolve) classrel]) classrels
    1.47 -    and print_dicts is_pseudo_fun = print_tuple (print_dict is_pseudo_fun);
    1.48 +    and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
    1.49      val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
    1.50        (map_index (fn (i, _) => DictVar ([], (v, (i, length sort)))) sort));
    1.51      fun print_term is_pseudo_fun some_thm vars fxy (IConst c) =
    1.52 @@ -423,7 +421,7 @@
    1.53          let val k = length tys in
    1.54            if length ts = k
    1.55            then (str o deresolve) c
    1.56 -            :: the_list (print_tuple (print_term is_pseudo_fun some_thm vars) BR ts)
    1.57 +            :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
    1.58            else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)]
    1.59          end
    1.60        else if is_pseudo_fun c