src/Tools/Code/code_ml.ML
changeset 47609 b3dab1892cda
parent 47576 b32aae03e3d6
child 48003 1d11af40b106
     1.1 --- a/src/Tools/Code/code_ml.ML	Thu Apr 19 18:24:40 2012 +0200
     1.2 +++ b/src/Tools/Code/code_ml.ML	Thu Apr 19 19:18:11 2012 +0200
     1.3 @@ -39,9 +39,6 @@
     1.4    | ML_Datas of (string * ((vname * sort) list * ((string * vname list) * itype list) list)) list
     1.5    | ML_Class of string * (vname * ((class * string) list * (string * itype) list));
     1.6  
     1.7 -fun stmt_name_of_binding (ML_Function (name, _)) = name
     1.8 -  | stmt_name_of_binding (ML_Instance (name, _)) = name;
     1.9 -
    1.10  fun print_product _ [] = NONE
    1.11    | print_product print [x] = SOME (print x)
    1.12    | print_product print xs = (SOME o enum " *" "" "") (map print xs);
    1.13 @@ -55,16 +52,16 @@
    1.14  
    1.15  fun print_sml_stmt tyco_syntax const_syntax reserved is_cons deresolve =
    1.16    let
    1.17 -    fun print_tyco_expr fxy (tyco, []) = (str o deresolve) tyco
    1.18 -      | print_tyco_expr fxy (tyco, [ty]) =
    1.19 +    fun print_tyco_expr (tyco, []) = (str o deresolve) tyco
    1.20 +      | print_tyco_expr (tyco, [ty]) =
    1.21            concat [print_typ BR ty, (str o deresolve) tyco]
    1.22 -      | print_tyco_expr fxy (tyco, tys) =
    1.23 +      | print_tyco_expr (tyco, tys) =
    1.24            concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco]
    1.25      and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco
    1.26 -         of NONE => print_tyco_expr fxy (tyco, tys)
    1.27 -          | SOME (i, print) => print print_typ fxy tys)
    1.28 +         of NONE => print_tyco_expr (tyco, tys)
    1.29 +          | SOME (_, print) => print print_typ fxy tys)
    1.30        | print_typ fxy (ITyVar v) = str ("'" ^ v);
    1.31 -    fun print_dicttyp (class, ty) = print_tyco_expr NOBR (class, [ty]);
    1.32 +    fun print_dicttyp (class, ty) = print_tyco_expr (class, [ty]);
    1.33      fun print_typscheme_prefix (vs, p) = enum " ->" "" ""
    1.34        (map_filter (fn (v, sort) =>
    1.35          (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);
    1.36 @@ -129,7 +126,7 @@
    1.37      and print_case is_pseudo_fun some_thm vars fxy (cases as ((_, [_]), _)) =
    1.38            let
    1.39              val (binds, body) = Code_Thingol.unfold_let (ICase cases);
    1.40 -            fun print_match ((pat, ty), t) vars =
    1.41 +            fun print_match ((pat, _), t) vars =
    1.42                vars
    1.43                |> print_bind is_pseudo_fun some_thm NOBR pat
    1.44                |>> (fn p => semicolon [str "val", p, str "=",
    1.45 @@ -170,7 +167,7 @@
    1.46        in
    1.47          concat (
    1.48            str definer
    1.49 -          :: print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs)
    1.50 +          :: print_tyco_expr (tyco, map (ITyVar o fst) vs)
    1.51            :: str "="
    1.52            :: separate (str "|") (map print_co cos)
    1.53          )
    1.54 @@ -236,7 +233,7 @@
    1.55                  (map print_super_instance super_instances
    1.56                    @ map print_classparam_instance classparam_instances)
    1.57                :: str ":"
    1.58 -              @@ print_tyco_expr NOBR (class, [tyco `%% map (ITyVar o fst) vs])
    1.59 +              @@ print_tyco_expr (class, [tyco `%% map (ITyVar o fst) vs])
    1.60              ))
    1.61            end;
    1.62      fun print_stmt (ML_Exc (name, (vs_ty, n))) = pair
    1.63 @@ -276,7 +273,7 @@
    1.64            end
    1.65       | print_stmt (ML_Datas [(tyco, (vs, []))]) =
    1.66            let
    1.67 -            val ty_p = print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs);
    1.68 +            val ty_p = print_tyco_expr (tyco, map (ITyVar o fst) vs);
    1.69            in
    1.70              pair
    1.71              [concat [str "type", ty_p]]
    1.72 @@ -359,16 +356,16 @@
    1.73  
    1.74  fun print_ocaml_stmt tyco_syntax const_syntax reserved is_cons deresolve =
    1.75    let
    1.76 -    fun print_tyco_expr fxy (tyco, []) = (str o deresolve) tyco
    1.77 -      | print_tyco_expr fxy (tyco, [ty]) =
    1.78 +    fun print_tyco_expr (tyco, []) = (str o deresolve) tyco
    1.79 +      | print_tyco_expr (tyco, [ty]) =
    1.80            concat [print_typ BR ty, (str o deresolve) tyco]
    1.81 -      | print_tyco_expr fxy (tyco, tys) =
    1.82 +      | print_tyco_expr (tyco, tys) =
    1.83            concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco]
    1.84      and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco
    1.85 -         of NONE => print_tyco_expr fxy (tyco, tys)
    1.86 +         of NONE => print_tyco_expr (tyco, tys)
    1.87            | SOME (_, print) => print print_typ fxy tys)
    1.88        | print_typ fxy (ITyVar v) = str ("'" ^ v);
    1.89 -    fun print_dicttyp (class, ty) = print_tyco_expr NOBR (class, [ty]);
    1.90 +    fun print_dicttyp (class, ty) = print_tyco_expr (class, [ty]);
    1.91      fun print_typscheme_prefix (vs, p) = enum " ->" "" ""
    1.92        (map_filter (fn (v, sort) =>
    1.93          (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);
    1.94 @@ -465,7 +462,7 @@
    1.95        in
    1.96          concat (
    1.97            str definer
    1.98 -          :: print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs)
    1.99 +          :: print_tyco_expr (tyco, map (ITyVar o fst) vs)
   1.100            :: str "="
   1.101            :: separate (str "|") (map print_co cos)
   1.102          )
   1.103 @@ -576,7 +573,7 @@
   1.104                  enum_default "()" ";" "{" "}" (map print_super_instance super_instances
   1.105                    @ map print_classparam_instance classparam_instances),
   1.106                  str ":",
   1.107 -                print_tyco_expr NOBR (class, [tyco `%% map (ITyVar o fst) vs])
   1.108 +                print_tyco_expr (class, [tyco `%% map (ITyVar o fst) vs])
   1.109                ]
   1.110              ))
   1.111            end;
   1.112 @@ -616,7 +613,7 @@
   1.113            end
   1.114       | print_stmt (ML_Datas [(tyco, (vs, []))]) =
   1.115            let
   1.116 -            val ty_p = print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs);
   1.117 +            val ty_p = print_tyco_expr (tyco, map (ITyVar o fst) vs);
   1.118            in
   1.119              pair
   1.120              [concat [str "type", ty_p]]