src/Tools/Code/code_ml.ML
changeset 33992 bf22ff4f3d19
parent 33636 a9bb3f063773
child 34028 1e6206763036
     1.1 --- a/src/Tools/Code/code_ml.ML	Fri Dec 04 18:19:32 2009 +0100
     1.2 +++ b/src/Tools/Code/code_ml.ML	Fri Dec 04 18:19:32 2009 +0100
     1.3 @@ -21,6 +21,9 @@
     1.4  infixr 5 @@;
     1.5  infixr 5 @|;
     1.6  
     1.7 +
     1.8 +(** generic **)
     1.9 +
    1.10  val target_SML = "SML";
    1.11  val target_OCaml = "OCaml";
    1.12  val target_Eval = "Eval";
    1.13 @@ -32,7 +35,7 @@
    1.14        * ((string * const) * (thm * bool)) list));
    1.15  
    1.16  datatype ml_stmt =
    1.17 -    ML_Exc of string * int
    1.18 +    ML_Exc of string * (typscheme * int)
    1.19    | ML_Val of ml_binding
    1.20    | ML_Funs of ml_binding list * string list
    1.21    | ML_Datas of (string * ((vname * sort) list * (string * itype list) list)) list
    1.22 @@ -47,130 +50,144 @@
    1.23    | stmt_names_of (ML_Datas ds) = map fst ds
    1.24    | stmt_names_of (ML_Class (name, _)) = [name];
    1.25  
    1.26 +fun print_product _ [] = NONE
    1.27 +  | print_product print [x] = SOME (print x)
    1.28 +  | print_product print xs = (SOME o Pretty.enum " *" "" "") (map print xs);
    1.29  
    1.30 -(** SML serailizer **)
    1.31 +fun print_tuple _ _ [] = NONE
    1.32 +  | print_tuple print fxy [x] = SOME (print fxy x)
    1.33 +  | print_tuple print _ xs = SOME (Pretty.list "(" ")" (map (print NOBR) xs));
    1.34  
    1.35 -fun pr_sml_stmt labelled_name syntax_tyco syntax_const reserved deresolve is_cons =
    1.36 +
    1.37 +(** SML serializer **)
    1.38 +
    1.39 +fun print_sml_stmt labelled_name syntax_tyco syntax_const reserved is_cons deresolve =
    1.40    let
    1.41 -    fun pr_dicts is_pseudo_fun fxy ds =
    1.42 -      let
    1.43 -        fun pr_dictvar (v, (_, 1)) = first_upper v ^ "_"
    1.44 -          | pr_dictvar (v, (i, _)) = first_upper v ^ string_of_int (i+1) ^ "_";
    1.45 -        fun pr_proj [] p =
    1.46 -              p
    1.47 -          | pr_proj [p'] p =
    1.48 -              brackets [p', p]
    1.49 -          | pr_proj (ps as _ :: _) p =
    1.50 -              brackets [Pretty.enum " o" "(" ")" ps, p];
    1.51 -        fun pr_dict fxy (DictConst (inst, dss)) =
    1.52 -              brackify fxy ((str o deresolve) inst ::
    1.53 -                (if is_pseudo_fun inst then [str "()"]
    1.54 -                else map (pr_dicts is_pseudo_fun BR) dss))
    1.55 -          | pr_dict fxy (DictVar (classrels, v)) =
    1.56 -              pr_proj (map (str o deresolve) classrels) ((str o pr_dictvar) v)
    1.57 -      in case ds
    1.58 -       of [] => str "()"
    1.59 -        | [d] => pr_dict fxy d
    1.60 -        | _ :: _ => (Pretty.list "(" ")" o map (pr_dict NOBR)) ds
    1.61 -      end;
    1.62 -    fun pr_tyvar_dicts is_pseudo_fun vs =
    1.63 -      vs
    1.64 -      |> map (fn (v, sort) => map_index (fn (i, _) =>
    1.65 -           DictVar ([], (v, (i, length sort)))) sort)
    1.66 -      |> map (pr_dicts is_pseudo_fun BR);
    1.67 -    fun pr_tycoexpr fxy (tyco, tys) =
    1.68 -      let
    1.69 -        val tyco' = (str o deresolve) tyco
    1.70 -      in case map (pr_typ BR) tys
    1.71 -       of [] => tyco'
    1.72 -        | [p] => Pretty.block [p, Pretty.brk 1, tyco']
    1.73 -        | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco']
    1.74 -      end
    1.75 -    and pr_typ fxy (tyco `%% tys) = (case syntax_tyco tyco
    1.76 -         of NONE => pr_tycoexpr fxy (tyco, tys)
    1.77 -          | SOME (i, pr) => pr pr_typ fxy tys)
    1.78 -      | pr_typ fxy (ITyVar v) = str ("'" ^ v);
    1.79 -    fun pr_term is_pseudo_fun thm vars fxy (IConst c) =
    1.80 -          pr_app is_pseudo_fun thm vars fxy (c, [])
    1.81 -      | pr_term is_pseudo_fun thm vars fxy (IVar NONE) =
    1.82 +    fun print_tyco_expr fxy (tyco, []) = (str o deresolve) tyco
    1.83 +      | print_tyco_expr fxy (tyco, [ty]) =
    1.84 +          concat [print_typ BR ty, (str o deresolve) tyco]
    1.85 +      | print_tyco_expr fxy (tyco, tys) =
    1.86 +          concat [Pretty.list "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco]
    1.87 +    and print_typ fxy (tyco `%% tys) = (case syntax_tyco tyco
    1.88 +         of NONE => print_tyco_expr fxy (tyco, tys)
    1.89 +          | SOME (i, print) => print print_typ fxy tys)
    1.90 +      | print_typ fxy (ITyVar v) = str ("'" ^ v);
    1.91 +    fun print_dicttyp (class, ty) = print_tyco_expr NOBR (class, [ty]);
    1.92 +    fun print_typscheme_prefix (vs, p) = Pretty.enum " ->" "" ""
    1.93 +      (map_filter (fn (v, sort) =>
    1.94 +        (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);
    1.95 +    fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty);
    1.96 +    fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty);
    1.97 +    fun print_dict is_pseudo_fun fxy (DictConst (inst, dss)) =
    1.98 +          brackify fxy ((str o deresolve) inst ::
    1.99 +            (if is_pseudo_fun inst then [str "()"]
   1.100 +            else map_filter (print_dicts is_pseudo_fun BR) dss))
   1.101 +      | print_dict is_pseudo_fun fxy (DictVar (classrels, (v, (i, k)))) =
   1.102 +          let
   1.103 +            val v_p = str (if k = 1 then first_upper v ^ "_"
   1.104 +              else first_upper v ^ string_of_int (i+1) ^ "_");
   1.105 +          in case classrels
   1.106 +           of [] => v_p
   1.107 +            | [classrel] => brackets [(str o deresolve) classrel, v_p]
   1.108 +            | classrels => brackets
   1.109 +                [Pretty.enum " o" "(" ")" (map (str o deresolve) classrels), v_p]
   1.110 +          end
   1.111 +    and print_dicts is_pseudo_fun = print_tuple (print_dict is_pseudo_fun);
   1.112 +    val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
   1.113 +      (map_index (fn (i, _) => DictVar ([], (v, (i, length sort)))) sort));
   1.114 +    fun print_term is_pseudo_fun thm vars fxy (IConst c) =
   1.115 +          print_app is_pseudo_fun thm vars fxy (c, [])
   1.116 +      | print_term is_pseudo_fun thm vars fxy (IVar NONE) =
   1.117            str "_"
   1.118 -      | pr_term is_pseudo_fun thm vars fxy (IVar (SOME v)) =
   1.119 +      | print_term is_pseudo_fun thm vars fxy (IVar (SOME v)) =
   1.120            str (lookup_var vars v)
   1.121 -      | pr_term is_pseudo_fun thm vars fxy (t as t1 `$ t2) =
   1.122 +      | print_term is_pseudo_fun thm vars fxy (t as t1 `$ t2) =
   1.123            (case Code_Thingol.unfold_const_app t
   1.124 -           of SOME c_ts => pr_app is_pseudo_fun thm vars fxy c_ts
   1.125 -            | NONE => brackify fxy
   1.126 -               [pr_term is_pseudo_fun thm vars NOBR t1, pr_term is_pseudo_fun thm vars BR t2])
   1.127 -      | pr_term is_pseudo_fun thm vars fxy (t as _ `|=> _) =
   1.128 +           of SOME c_ts => print_app is_pseudo_fun thm vars fxy c_ts
   1.129 +            | NONE => brackify fxy [print_term is_pseudo_fun thm vars NOBR t1,
   1.130 +                print_term is_pseudo_fun thm vars BR t2])
   1.131 +      | print_term is_pseudo_fun thm vars fxy (t as _ `|=> _) =
   1.132            let
   1.133              val (binds, t') = Code_Thingol.unfold_pat_abs t;
   1.134 -            fun pr (pat, ty) =
   1.135 -              pr_bind is_pseudo_fun thm NOBR pat
   1.136 +            fun print_abs (pat, ty) =
   1.137 +              print_bind is_pseudo_fun thm NOBR pat
   1.138                #>> (fn p => concat [str "fn", p, str "=>"]);
   1.139 -            val (ps, vars') = fold_map pr binds vars;
   1.140 -          in brackets (ps @ [pr_term is_pseudo_fun thm vars' NOBR t']) end
   1.141 -      | pr_term is_pseudo_fun thm vars fxy (ICase (cases as (_, t0))) =
   1.142 +            val (ps, vars') = fold_map print_abs binds vars;
   1.143 +          in brackets (ps @ [print_term is_pseudo_fun thm vars' NOBR t']) end
   1.144 +      | print_term is_pseudo_fun thm vars fxy (ICase (cases as (_, t0))) =
   1.145            (case Code_Thingol.unfold_const_app t0
   1.146             of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
   1.147 -                then pr_case is_pseudo_fun thm vars fxy cases
   1.148 -                else pr_app is_pseudo_fun thm vars fxy c_ts
   1.149 -            | NONE => pr_case is_pseudo_fun thm vars fxy cases)
   1.150 -    and pr_app' is_pseudo_fun thm vars (app as ((c, ((_, iss), tys)), ts)) =
   1.151 +                then print_case is_pseudo_fun thm vars fxy cases
   1.152 +                else print_app is_pseudo_fun thm vars fxy c_ts
   1.153 +            | NONE => print_case is_pseudo_fun thm vars fxy cases)
   1.154 +    and print_app_expr is_pseudo_fun thm vars (app as ((c, ((_, iss), tys)), ts)) =
   1.155        if is_cons c then
   1.156 -        let
   1.157 -          val k = length tys
   1.158 -        in if k < 2 then 
   1.159 -          (str o deresolve) c :: map (pr_term is_pseudo_fun thm vars BR) ts
   1.160 -        else if k = length ts then
   1.161 -          [(str o deresolve) c, Pretty.enum "," "(" ")" (map (pr_term is_pseudo_fun thm vars NOBR) ts)]
   1.162 -        else [pr_term is_pseudo_fun thm vars BR (Code_Thingol.eta_expand k app)] end
   1.163 +        let val k = length tys in
   1.164 +          if k < 2 orelse length ts = k
   1.165 +          then (str o deresolve) c
   1.166 +            :: the_list (print_tuple (print_term is_pseudo_fun thm vars) BR ts)
   1.167 +          else [print_term is_pseudo_fun thm vars BR (Code_Thingol.eta_expand k app)]
   1.168 +        end
   1.169        else if is_pseudo_fun c
   1.170          then (str o deresolve) c @@ str "()"
   1.171 -      else
   1.172 -        (str o deresolve) c
   1.173 -          :: (map (pr_dicts is_pseudo_fun BR) o filter_out null) iss @ map (pr_term is_pseudo_fun thm vars BR) ts
   1.174 -    and pr_app is_pseudo_fun thm vars = gen_pr_app (pr_app' is_pseudo_fun) (pr_term is_pseudo_fun)
   1.175 -      syntax_const thm vars
   1.176 -    and pr_bind is_pseudo_fun = gen_pr_bind (pr_term is_pseudo_fun)
   1.177 -    and pr_case is_pseudo_fun thm vars fxy (cases as ((_, [_]), _)) =
   1.178 +      else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) iss
   1.179 +        @ map (print_term is_pseudo_fun thm vars BR) ts
   1.180 +    and print_app is_pseudo_fun thm vars = gen_print_app (print_app_expr is_pseudo_fun)
   1.181 +      (print_term is_pseudo_fun) syntax_const thm vars
   1.182 +    and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)
   1.183 +    and print_case is_pseudo_fun thm vars fxy (cases as ((_, [_]), _)) =
   1.184            let
   1.185              val (binds, body) = Code_Thingol.unfold_let (ICase cases);
   1.186 -            fun pr ((pat, ty), t) vars =
   1.187 +            fun print_match ((pat, ty), t) vars =
   1.188                vars
   1.189 -              |> pr_bind is_pseudo_fun thm NOBR pat
   1.190 -              |>> (fn p => semicolon [str "val", p, str "=", pr_term is_pseudo_fun thm vars NOBR t])
   1.191 -            val (ps, vars') = fold_map pr binds vars;
   1.192 +              |> print_bind is_pseudo_fun thm NOBR pat
   1.193 +              |>> (fn p => semicolon [str "val", p, str "=",
   1.194 +                    print_term is_pseudo_fun thm vars NOBR t])
   1.195 +            val (ps, vars') = fold_map print_match binds vars;
   1.196            in
   1.197              Pretty.chunks [
   1.198 -              [str ("let"), Pretty.fbrk, Pretty.chunks ps] |> Pretty.block,
   1.199 -              [str ("in"), Pretty.fbrk, pr_term is_pseudo_fun thm vars' NOBR body] |> Pretty.block,
   1.200 +              Pretty.block [str ("let"), Pretty.fbrk, Pretty.chunks ps],
   1.201 +              Pretty.block [str ("in"), Pretty.fbrk, print_term is_pseudo_fun thm vars' NOBR body],
   1.202                str ("end")
   1.203              ]
   1.204            end
   1.205 -      | pr_case is_pseudo_fun thm vars fxy (((t, ty), clause :: clauses), _) =
   1.206 +      | print_case is_pseudo_fun thm vars fxy (((t, ty), clause :: clauses), _) =
   1.207            let
   1.208 -            fun pr delim (pat, body) =
   1.209 +            fun print_select delim (pat, body) =
   1.210                let
   1.211 -                val (p, vars') = pr_bind is_pseudo_fun thm NOBR pat vars;
   1.212 +                val (p, vars') = print_bind is_pseudo_fun thm NOBR pat vars;
   1.213                in
   1.214 -                concat [str delim, p, str "=>", pr_term is_pseudo_fun thm vars' NOBR body]
   1.215 +                concat [str delim, p, str "=>", print_term is_pseudo_fun thm vars' NOBR body]
   1.216                end;
   1.217            in
   1.218              brackets (
   1.219                str "case"
   1.220 -              :: pr_term is_pseudo_fun thm vars NOBR t
   1.221 -              :: pr "of" clause
   1.222 -              :: map (pr "|") clauses
   1.223 +              :: print_term is_pseudo_fun thm vars NOBR t
   1.224 +              :: print_select "of" clause
   1.225 +              :: map (print_select "|") clauses
   1.226              )
   1.227            end
   1.228 -      | pr_case is_pseudo_fun thm vars fxy ((_, []), _) =
   1.229 +      | print_case is_pseudo_fun thm vars fxy ((_, []), _) =
   1.230            (concat o map str) ["raise", "Fail", "\"empty case\""];
   1.231 -    fun pr_binding is_pseudo_fun needs_typ definer (ML_Function (name, ((vs, ty), eqs as eq :: eqs'))) =
   1.232 +    fun print_val_decl print_typscheme (name, typscheme) = concat
   1.233 +      [str "val", str (deresolve name), str ":", print_typscheme typscheme];
   1.234 +    fun print_datatype_decl definer (tyco, (vs, cos)) =
   1.235 +      let
   1.236 +        fun print_co (co, []) = str (deresolve co)
   1.237 +          | print_co (co, tys) = concat [str (deresolve co), str "of",
   1.238 +              Pretty.enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];
   1.239 +      in
   1.240 +        concat (
   1.241 +          str definer
   1.242 +          :: print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs)
   1.243 +          :: str "="
   1.244 +          :: separate (str "|") (map print_co cos)
   1.245 +        )
   1.246 +      end;
   1.247 +    fun print_def is_pseudo_fun needs_typ definer
   1.248 +          (ML_Function (name, (vs_ty as (vs, ty), eq :: eqs))) =
   1.249            let
   1.250 -            val vs_dict = filter_out (null o snd) vs;
   1.251 -            val shift = if null eqs' then I else
   1.252 -              map (Pretty.block o single o Pretty.block o single);
   1.253 -            fun pr_eq definer ((ts, t), (thm, _)) =
   1.254 +            fun print_eqn definer ((ts, t), (thm, _)) =
   1.255                let
   1.256                  val consts = fold Code_Thingol.add_constnames (t :: ts) [];
   1.257                  val vars = reserved
   1.258 @@ -179,157 +196,158 @@
   1.259                    |> intro_vars ((fold o Code_Thingol.fold_varnames)
   1.260                         (insert (op =)) ts []);
   1.261                  val prolog = if needs_typ then
   1.262 -                  concat [str definer, (str o deresolve) name, str ":", pr_typ NOBR ty]
   1.263 +                  concat [str definer, (str o deresolve) name, str ":", print_typ NOBR ty]
   1.264                      else Pretty.strs [definer, deresolve name];
   1.265                in
   1.266                  concat (
   1.267                    prolog
   1.268                    :: (if is_pseudo_fun name then [str "()"]
   1.269 -                      else pr_tyvar_dicts is_pseudo_fun vs_dict
   1.270 -                        @ map (pr_term is_pseudo_fun thm vars BR) ts)
   1.271 +                      else print_dict_args vs
   1.272 +                        @ map (print_term is_pseudo_fun thm vars BR) ts)
   1.273                    @ str "="
   1.274 -                  @@ pr_term is_pseudo_fun thm vars NOBR t
   1.275 +                  @@ print_term is_pseudo_fun thm vars NOBR t
   1.276                  )
   1.277                end
   1.278 -          in
   1.279 -            (Pretty.block o Pretty.fbreaks o shift) (
   1.280 -              pr_eq definer eq
   1.281 -              :: map (pr_eq "|") eqs'
   1.282 -            )
   1.283 +            val shift = if null eqs then I else
   1.284 +              map (Pretty.block o single o Pretty.block o single);
   1.285 +          in pair
   1.286 +            (print_val_decl print_typscheme (name, vs_ty))
   1.287 +            ((Pretty.block o Pretty.fbreaks o shift) (
   1.288 +              print_eqn definer eq
   1.289 +              :: map (print_eqn "|") eqs
   1.290 +            ))
   1.291            end
   1.292 -      | pr_binding is_pseudo_fun _ definer (ML_Instance (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) =
   1.293 +      | print_def is_pseudo_fun _ definer
   1.294 +          (ML_Instance (inst, ((class, (tyco, vs)), (superinsts, classparams)))) =
   1.295            let
   1.296 -            fun pr_superclass (_, (classrel, dss)) =
   1.297 +            fun print_superinst (_, (classrel, dss)) =
   1.298                concat [
   1.299                  (str o Long_Name.base_name o deresolve) classrel,
   1.300                  str "=",
   1.301 -                pr_dicts is_pseudo_fun NOBR [DictConst dss]
   1.302 +                print_dict is_pseudo_fun NOBR (DictConst dss)
   1.303                ];
   1.304 -            fun pr_classparam ((classparam, c_inst), (thm, _)) =
   1.305 +            fun print_classparam ((classparam, c_inst), (thm, _)) =
   1.306                concat [
   1.307                  (str o Long_Name.base_name o deresolve) classparam,
   1.308                  str "=",
   1.309 -                pr_app (K false) thm reserved NOBR (c_inst, [])
   1.310 +                print_app (K false) thm reserved NOBR (c_inst, [])
   1.311                ];
   1.312 -          in
   1.313 -            concat (
   1.314 +          in pair
   1.315 +            (print_val_decl print_dicttypscheme
   1.316 +              (inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
   1.317 +            (concat (
   1.318                str definer
   1.319                :: (str o deresolve) inst
   1.320                :: (if is_pseudo_fun inst then [str "()"]
   1.321 -                  else pr_tyvar_dicts is_pseudo_fun arity)
   1.322 +                  else print_dict_args vs)
   1.323                @ str "="
   1.324 -              :: Pretty.enum "," "{" "}"
   1.325 -                (map pr_superclass superarities @ map pr_classparam classparam_insts)
   1.326 +              :: Pretty.list "{" "}"
   1.327 +                (map print_superinst superinsts @ map print_classparam classparams)
   1.328                :: str ":"
   1.329 -              @@ pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])
   1.330 -            )
   1.331 +              @@ print_tyco_expr NOBR (class, [tyco `%% map (ITyVar o fst) vs])
   1.332 +            ))
   1.333            end;
   1.334 -    fun pr_stmt (ML_Exc (name, n)) =
   1.335 -          (concat o map str) (
   1.336 +    fun print_stmt (ML_Exc (name, (vs_ty, n))) = pair
   1.337 +          [print_val_decl print_typscheme (name, vs_ty)]
   1.338 +          ((semicolon o map str) (
   1.339              (if n = 0 then "val" else "fun")
   1.340              :: deresolve name
   1.341              :: replicate n "_"
   1.342              @ "="
   1.343              :: "raise"
   1.344              :: "Fail"
   1.345 -            @@ (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name ^ ";"
   1.346 -          )
   1.347 -      | pr_stmt (ML_Val binding) =
   1.348 -          semicolon [pr_binding (K false) true "val" binding]
   1.349 -      | pr_stmt (ML_Funs (binding :: bindings, pseudo_funs)) =
   1.350 +            @@ (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name
   1.351 +          ))
   1.352 +      | print_stmt (ML_Val binding) =
   1.353            let
   1.354 -            val pr_binding' = pr_binding (member (op =) pseudo_funs) false;
   1.355 -            fun pr_pseudo_fun name = concat [
   1.356 +            val (sig_p, p) = print_def (K false) true "val" binding
   1.357 +          in pair
   1.358 +            [sig_p]
   1.359 +            (semicolon [p])
   1.360 +          end
   1.361 +      | print_stmt (ML_Funs (binding :: bindings, pseudo_funs)) =
   1.362 +          let
   1.363 +            val print_def' = print_def (member (op =) pseudo_funs) false;
   1.364 +            fun print_pseudo_fun name = concat [
   1.365                  str "val",
   1.366                  (str o deresolve) name,
   1.367                  str "=",
   1.368                  (str o deresolve) name,
   1.369                  str "();"
   1.370                ];
   1.371 -            val (ps, p) = split_last
   1.372 -              (pr_binding' "fun" binding :: map (pr_binding' "and") bindings);
   1.373 -            val pseudo_ps = map pr_pseudo_fun pseudo_funs;
   1.374 -          in Pretty.chunks (ps @ Pretty.block ([p, str ";"]) :: pseudo_ps) end
   1.375 -     | pr_stmt (ML_Datas (datas as (data :: datas'))) =
   1.376 +            val (sig_ps, (ps, p)) = (apsnd split_last o split_list)
   1.377 +              (print_def' "fun" binding :: map (print_def' "and") bindings);
   1.378 +            val pseudo_ps = map print_pseudo_fun pseudo_funs;
   1.379 +          in pair
   1.380 +            sig_ps
   1.381 +            (Pretty.chunks (ps @ semicolon [p] :: pseudo_ps))
   1.382 +          end
   1.383 +     | print_stmt (ML_Datas [(tyco, (vs, []))]) =
   1.384 +          let
   1.385 +            val ty_p = print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs);
   1.386 +          in
   1.387 +            pair
   1.388 +            [concat [str "type", ty_p]]
   1.389 +            (concat [str "datatype", ty_p, str "=", str "EMPTY__"])
   1.390 +          end
   1.391 +     | print_stmt (ML_Datas (data :: datas)) = 
   1.392            let
   1.393 -            fun pr_co (co, []) =
   1.394 -                  str (deresolve co)
   1.395 -              | pr_co (co, tys) =
   1.396 -                  concat [
   1.397 -                    str (deresolve co),
   1.398 -                    str "of",
   1.399 -                    Pretty.enum " *" "" "" (map (pr_typ (INFX (2, X))) tys)
   1.400 -                  ];
   1.401 -            fun pr_data definer (tyco, (vs, [])) =
   1.402 -                  concat (
   1.403 -                    str definer
   1.404 -                    :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
   1.405 -                    :: str "="
   1.406 -                    @@ str "EMPTY__" 
   1.407 -                  )
   1.408 -              | pr_data definer (tyco, (vs, cos)) =
   1.409 -                  concat (
   1.410 -                    str definer
   1.411 -                    :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
   1.412 -                    :: str "="
   1.413 -                    :: separate (str "|") (map pr_co cos)
   1.414 -                  );
   1.415 -            val (ps, p) = split_last
   1.416 -              (pr_data "datatype" data :: map (pr_data "and") datas');
   1.417 -          in Pretty.chunks (ps @| Pretty.block ([p, str ";"])) end
   1.418 -     | pr_stmt (ML_Class (class, (v, (superclasses, classparams)))) =
   1.419 +            val sig_ps = print_datatype_decl "datatype" data
   1.420 +              :: map (print_datatype_decl "and") datas;
   1.421 +            val (ps, p) = split_last sig_ps;
   1.422 +          in pair
   1.423 +            sig_ps
   1.424 +            (Pretty.chunks (ps @| semicolon [p]))
   1.425 +          end
   1.426 +     | print_stmt (ML_Class (class, (v, (superclasses, classparams)))) =
   1.427            let
   1.428 -            val w = first_upper v ^ "_";
   1.429 -            fun pr_superclass_field (class, classrel) =
   1.430 -              (concat o map str) [
   1.431 -                deresolve classrel, ":", "'" ^ v, deresolve class
   1.432 -              ];
   1.433 -            fun pr_classparam_field (classparam, ty) =
   1.434 -              concat [
   1.435 -                (str o deresolve) classparam, str ":", pr_typ NOBR ty
   1.436 -              ];
   1.437 -            fun pr_classparam_proj (classparam, _) =
   1.438 -              semicolon [
   1.439 -                str "fun",
   1.440 -                (str o deresolve) classparam,
   1.441 -                Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolve class)],
   1.442 -                str "=",
   1.443 -                str ("#" ^ deresolve classparam),
   1.444 -                str w
   1.445 -              ];
   1.446 -            fun pr_superclass_proj (_, classrel) =
   1.447 -              semicolon [
   1.448 -                str "fun",
   1.449 -                (str o deresolve) classrel,
   1.450 -                Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolve class)],
   1.451 -                str "=",
   1.452 -                str ("#" ^ deresolve classrel),
   1.453 -                str w
   1.454 -              ];
   1.455 -          in
   1.456 -            Pretty.chunks (
   1.457 +            fun print_field s p = concat [str s, str ":", p];
   1.458 +            fun print_proj s p = semicolon
   1.459 +              (map str ["val", s, "=", "#" ^ s, ":"] @| p);
   1.460 +            fun print_superclass_decl (superclass, classrel) =
   1.461 +              print_val_decl print_dicttypscheme
   1.462 +                (classrel, ([(v, [class])], (superclass, ITyVar v)));
   1.463 +            fun print_superclass_field (superclass, classrel) =
   1.464 +              print_field (deresolve classrel) (print_dicttyp (superclass, ITyVar v));
   1.465 +            fun print_superclass_proj (superclass, classrel) =
   1.466 +              print_proj (deresolve classrel)
   1.467 +                (print_dicttypscheme ([(v, [class])], (superclass, ITyVar v)));
   1.468 +            fun print_classparam_decl (classparam, ty) =
   1.469 +              print_val_decl print_typscheme
   1.470 +                (classparam, ([(v, [class])], ty));
   1.471 +            fun print_classparam_field (classparam, ty) =
   1.472 +              print_field (deresolve classparam) (print_typ NOBR ty);
   1.473 +            fun print_classparam_proj (classparam, ty) =
   1.474 +              print_proj (deresolve classparam)
   1.475 +                (print_typscheme ([(v, [class])], ty));
   1.476 +          in pair
   1.477 +            (concat [str "type", print_dicttyp (class, ITyVar v)]
   1.478 +              :: map print_superclass_decl superclasses
   1.479 +              @ map print_classparam_decl classparams)
   1.480 +            (Pretty.chunks (
   1.481                concat [
   1.482                  str ("type '" ^ v),
   1.483                  (str o deresolve) class,
   1.484                  str "=",
   1.485 -                Pretty.enum "," "{" "};" (
   1.486 -                  map pr_superclass_field superclasses @ map pr_classparam_field classparams
   1.487 +                Pretty.list "{" "};" (
   1.488 +                  map print_superclass_field superclasses
   1.489 +                  @ map print_classparam_field classparams
   1.490                  )
   1.491                ]
   1.492 -              :: map pr_superclass_proj superclasses
   1.493 -              @ map pr_classparam_proj classparams
   1.494 -            )
   1.495 +              :: map print_superclass_proj superclasses
   1.496 +              @ map print_classparam_proj classparams
   1.497 +            ))
   1.498            end;
   1.499 -  in pr_stmt end;
   1.500 +  in print_stmt end;
   1.501  
   1.502 -fun pr_sml_module name content =
   1.503 -  Pretty.chunks (
   1.504 -    str ("structure " ^ name ^ " = ")
   1.505 -    :: str "struct"
   1.506 -    :: str ""
   1.507 -    :: content
   1.508 -    @ str ""
   1.509 -    @@ str ("end; (*struct " ^ name ^ "*)")
   1.510 +fun print_sml_module name some_decls body = Pretty.chunks2 (
   1.511 +    Pretty.chunks (
   1.512 +      str ("structure " ^ name ^ (if is_some some_decls then " : sig" else " ="))
   1.513 +      :: (the_list o Option.map (Pretty.indent 2 o Pretty.chunks)) some_decls
   1.514 +      @| (if is_some some_decls then str "end = struct" else str "struct")
   1.515 +    )
   1.516 +    :: body
   1.517 +    @| str ("end; (*struct " ^ name ^ "*)")
   1.518    );
   1.519  
   1.520  val literals_sml = Literals {
   1.521 @@ -338,118 +356,127 @@
   1.522    literal_numeral = fn unbounded => fn k =>
   1.523      if unbounded then "(" ^ string_of_int k ^ " : IntInf.int)"
   1.524      else string_of_int k,
   1.525 -  literal_list = Pretty.enum "," "[" "]",
   1.526 +  literal_list = Pretty.list "[" "]",
   1.527    infix_cons = (7, "::")
   1.528  };
   1.529  
   1.530  
   1.531  (** OCaml serializer **)
   1.532  
   1.533 -fun pr_ocaml_stmt labelled_name syntax_tyco syntax_const reserved deresolve is_cons =
   1.534 +fun print_ocaml_stmt labelled_name syntax_tyco syntax_const reserved is_cons deresolve =
   1.535    let
   1.536 -    fun pr_dicts is_pseudo_fun fxy ds =
   1.537 -      let
   1.538 -        fun pr_dictvar (v, (_, 1)) = "_" ^ first_upper v
   1.539 -          | pr_dictvar (v, (i, _)) = "_" ^ first_upper v ^ string_of_int (i+1);
   1.540 -        fun pr_proj ps p =
   1.541 -          fold_rev (fn p2 => fn p1 => Pretty.block [p1, str ".", str p2]) ps p
   1.542 -        fun pr_dict fxy (DictConst (inst, dss)) =
   1.543 -              brackify fxy ((str o deresolve) inst ::
   1.544 -                (if is_pseudo_fun inst then [str "()"]
   1.545 -                else map (pr_dicts is_pseudo_fun BR) dss))
   1.546 -          | pr_dict fxy (DictVar (classrels, v)) =
   1.547 -              pr_proj (map deresolve classrels) ((str o pr_dictvar) v)
   1.548 -      in case ds
   1.549 -       of [] => str "()"
   1.550 -        | [d] => pr_dict fxy d
   1.551 -        | _ :: _ => (Pretty.list "(" ")" o map (pr_dict NOBR)) ds
   1.552 -      end;
   1.553 -    fun pr_tyvar_dicts is_pseudo_fun vs =
   1.554 -      vs
   1.555 -      |> map (fn (v, sort) => map_index (fn (i, _) =>
   1.556 -           DictVar ([], (v, (i, length sort)))) sort)
   1.557 -      |> map (pr_dicts is_pseudo_fun BR);
   1.558 -    fun pr_tycoexpr fxy (tyco, tys) =
   1.559 -      let
   1.560 -        val tyco' = (str o deresolve) tyco
   1.561 -      in case map (pr_typ BR) tys
   1.562 -       of [] => tyco'
   1.563 -        | [p] => Pretty.block [p, Pretty.brk 1, tyco']
   1.564 -        | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco']
   1.565 -      end
   1.566 -    and pr_typ fxy (tyco `%% tys) = (case syntax_tyco tyco
   1.567 -         of NONE => pr_tycoexpr fxy (tyco, tys)
   1.568 -          | SOME (i, pr) => pr pr_typ fxy tys)
   1.569 -      | pr_typ fxy (ITyVar v) = str ("'" ^ v);
   1.570 -    fun pr_term is_pseudo_fun thm vars fxy (IConst c) =
   1.571 -          pr_app is_pseudo_fun thm vars fxy (c, [])
   1.572 -      | pr_term is_pseudo_fun thm vars fxy (IVar NONE) =
   1.573 +    fun print_tyco_expr fxy (tyco, []) = (str o deresolve) tyco
   1.574 +      | print_tyco_expr fxy (tyco, [ty]) =
   1.575 +          concat [print_typ BR ty, (str o deresolve) tyco]
   1.576 +      | print_tyco_expr fxy (tyco, tys) =
   1.577 +          concat [Pretty.list "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco]
   1.578 +    and print_typ fxy (tyco `%% tys) = (case syntax_tyco tyco
   1.579 +         of NONE => print_tyco_expr fxy (tyco, tys)
   1.580 +          | SOME (i, print) => print print_typ fxy tys)
   1.581 +      | print_typ fxy (ITyVar v) = str ("'" ^ v);
   1.582 +    fun print_dicttyp (class, ty) = print_tyco_expr NOBR (class, [ty]);
   1.583 +    fun print_typscheme_prefix (vs, p) = Pretty.enum " ->" "" ""
   1.584 +      (map_filter (fn (v, sort) =>
   1.585 +        (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);
   1.586 +    fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty);
   1.587 +    fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty);
   1.588 +    fun print_dict is_pseudo_fun fxy (DictConst (inst, dss)) =
   1.589 +          brackify fxy ((str o deresolve) inst ::
   1.590 +            (if is_pseudo_fun inst then [str "()"]
   1.591 +            else map_filter (print_dicts is_pseudo_fun BR) dss))
   1.592 +      | print_dict is_pseudo_fun fxy (DictVar (classrels, (v, (i, k)))) =
   1.593 +          str (if k = 1 then "_" ^ first_upper v
   1.594 +            else "_" ^ first_upper v ^ string_of_int (i+1))
   1.595 +          |> fold_rev (fn classrel => fn p =>
   1.596 +               Pretty.block [p, str ".", (str o deresolve) classrel]) classrels
   1.597 +    and print_dicts is_pseudo_fun = print_tuple (print_dict is_pseudo_fun);
   1.598 +    val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
   1.599 +      (map_index (fn (i, _) => DictVar ([], (v, (i, length sort)))) sort));
   1.600 +    fun print_term is_pseudo_fun thm vars fxy (IConst c) =
   1.601 +          print_app is_pseudo_fun thm vars fxy (c, [])
   1.602 +      | print_term is_pseudo_fun thm vars fxy (IVar NONE) =
   1.603            str "_"
   1.604 -      | pr_term is_pseudo_fun thm vars fxy (IVar (SOME v)) =
   1.605 +      | print_term is_pseudo_fun thm vars fxy (IVar (SOME v)) =
   1.606            str (lookup_var vars v)
   1.607 -      | pr_term is_pseudo_fun thm vars fxy (t as t1 `$ t2) =
   1.608 +      | print_term is_pseudo_fun thm vars fxy (t as t1 `$ t2) =
   1.609            (case Code_Thingol.unfold_const_app t
   1.610 -           of SOME c_ts => pr_app is_pseudo_fun thm vars fxy c_ts
   1.611 -            | NONE =>
   1.612 -                brackify fxy [pr_term is_pseudo_fun thm vars NOBR t1, pr_term is_pseudo_fun thm vars BR t2])
   1.613 -      | pr_term is_pseudo_fun thm vars fxy (t as _ `|=> _) =
   1.614 +           of SOME c_ts => print_app is_pseudo_fun thm vars fxy c_ts
   1.615 +            | NONE => brackify fxy [print_term is_pseudo_fun thm vars NOBR t1,
   1.616 +                print_term is_pseudo_fun thm vars BR t2])
   1.617 +      | print_term is_pseudo_fun thm vars fxy (t as _ `|=> _) =
   1.618            let
   1.619              val (binds, t') = Code_Thingol.unfold_pat_abs t;
   1.620 -            val (ps, vars') = fold_map (pr_bind is_pseudo_fun thm BR o fst) binds vars;
   1.621 -          in brackets (str "fun" :: ps @ str "->" @@ pr_term is_pseudo_fun thm vars' NOBR t') end
   1.622 -      | pr_term is_pseudo_fun thm vars fxy (ICase (cases as (_, t0))) = (case Code_Thingol.unfold_const_app t0
   1.623 +            val (ps, vars') = fold_map (print_bind is_pseudo_fun thm BR o fst) binds vars;
   1.624 +          in brackets (str "fun" :: ps @ str "->" @@ print_term is_pseudo_fun thm vars' NOBR t') end
   1.625 +      | print_term is_pseudo_fun thm vars fxy (ICase (cases as (_, t0))) =
   1.626 +          (case Code_Thingol.unfold_const_app t0
   1.627             of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
   1.628 -                then pr_case is_pseudo_fun thm vars fxy cases
   1.629 -                else pr_app is_pseudo_fun thm vars fxy c_ts
   1.630 -            | NONE => pr_case is_pseudo_fun thm vars fxy cases)
   1.631 -    and pr_app' is_pseudo_fun thm vars (app as ((c, ((_, iss), tys)), ts)) =
   1.632 +                then print_case is_pseudo_fun thm vars fxy cases
   1.633 +                else print_app is_pseudo_fun thm vars fxy c_ts
   1.634 +            | NONE => print_case is_pseudo_fun thm vars fxy cases)
   1.635 +    and print_app_expr is_pseudo_fun thm vars (app as ((c, ((_, iss), tys)), ts)) =
   1.636        if is_cons c then
   1.637 -        if length tys = length ts
   1.638 -        then case ts
   1.639 -         of [] => [(str o deresolve) c]
   1.640 -          | [t] => [(str o deresolve) c, pr_term is_pseudo_fun thm vars BR t]
   1.641 -          | _ => [(str o deresolve) c, Pretty.enum "," "(" ")"
   1.642 -                    (map (pr_term is_pseudo_fun thm vars NOBR) ts)]
   1.643 -        else [pr_term is_pseudo_fun thm vars BR (Code_Thingol.eta_expand (length tys) app)]
   1.644 +        let val k = length tys in
   1.645 +          if length ts = k
   1.646 +          then (str o deresolve) c
   1.647 +            :: the_list (print_tuple (print_term is_pseudo_fun thm vars) BR ts)
   1.648 +          else [print_term is_pseudo_fun thm vars BR (Code_Thingol.eta_expand k app)]
   1.649 +        end
   1.650        else if is_pseudo_fun c
   1.651          then (str o deresolve) c @@ str "()"
   1.652 -      else (str o deresolve) c
   1.653 -        :: ((map (pr_dicts is_pseudo_fun BR) o filter_out null) iss @ map (pr_term is_pseudo_fun thm vars BR) ts)
   1.654 -    and pr_app is_pseudo_fun = gen_pr_app (pr_app' is_pseudo_fun) (pr_term is_pseudo_fun)
   1.655 -      syntax_const
   1.656 -    and pr_bind is_pseudo_fun = gen_pr_bind (pr_term is_pseudo_fun)
   1.657 -    and pr_case is_pseudo_fun thm vars fxy (cases as ((_, [_]), _)) =
   1.658 +      else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) iss
   1.659 +        @ map (print_term is_pseudo_fun thm vars BR) ts
   1.660 +    and print_app is_pseudo_fun thm vars = gen_print_app (print_app_expr is_pseudo_fun)
   1.661 +      (print_term is_pseudo_fun) syntax_const thm vars
   1.662 +    and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)
   1.663 +    and print_case is_pseudo_fun thm vars fxy (cases as ((_, [_]), _)) =
   1.664            let
   1.665              val (binds, body) = Code_Thingol.unfold_let (ICase cases);
   1.666 -            fun pr ((pat, ty), t) vars =
   1.667 +            fun print_let ((pat, ty), t) vars =
   1.668                vars
   1.669 -              |> pr_bind is_pseudo_fun thm NOBR pat
   1.670 +              |> print_bind is_pseudo_fun thm NOBR pat
   1.671                |>> (fn p => concat
   1.672 -                  [str "let", p, str "=", pr_term is_pseudo_fun thm vars NOBR t, str "in"])
   1.673 -            val (ps, vars') = fold_map pr binds vars;
   1.674 +                  [str "let", p, str "=", print_term is_pseudo_fun thm vars NOBR t, str "in"])
   1.675 +            val (ps, vars') = fold_map print_let binds vars;
   1.676            in
   1.677              brackify_block fxy (Pretty.chunks ps) []
   1.678 -              (pr_term is_pseudo_fun thm vars' NOBR body)
   1.679 +              (print_term is_pseudo_fun thm vars' NOBR body)
   1.680            end
   1.681 -      | pr_case is_pseudo_fun thm vars fxy (((t, ty), clause :: clauses), _) =
   1.682 +      | print_case is_pseudo_fun thm vars fxy (((t, ty), clause :: clauses), _) =
   1.683            let
   1.684 -            fun pr delim (pat, body) =
   1.685 +            fun print_select delim (pat, body) =
   1.686                let
   1.687 -                val (p, vars') = pr_bind is_pseudo_fun thm NOBR pat vars;
   1.688 -              in concat [str delim, p, str "->", pr_term is_pseudo_fun thm vars' NOBR body] end;
   1.689 +                val (p, vars') = print_bind is_pseudo_fun thm NOBR pat vars;
   1.690 +              in concat [str delim, p, str "->", print_term is_pseudo_fun thm vars' NOBR body] end;
   1.691            in
   1.692              brackets (
   1.693                str "match"
   1.694 -              :: pr_term is_pseudo_fun thm vars NOBR t
   1.695 -              :: pr "with" clause
   1.696 -              :: map (pr "|") clauses
   1.697 +              :: print_term is_pseudo_fun thm vars NOBR t
   1.698 +              :: print_select "with" clause
   1.699 +              :: map (print_select "|") clauses
   1.700              )
   1.701            end
   1.702 -      | pr_case is_pseudo_fun thm vars fxy ((_, []), _) =
   1.703 +      | print_case is_pseudo_fun thm vars fxy ((_, []), _) =
   1.704            (concat o map str) ["failwith", "\"empty case\""];
   1.705 -    fun pr_binding is_pseudo_fun needs_typ definer (ML_Function (name, ((vs, ty), eqs))) =
   1.706 +    fun print_val_decl print_typscheme (name, typscheme) = concat
   1.707 +      [str "val", str (deresolve name), str ":", print_typscheme typscheme];
   1.708 +    fun print_datatype_decl definer (tyco, (vs, cos)) =
   1.709 +      let
   1.710 +        fun print_co (co, []) = str (deresolve co)
   1.711 +          | print_co (co, tys) = concat [str (deresolve co), str "of",
   1.712 +              Pretty.enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];
   1.713 +      in
   1.714 +        concat (
   1.715 +          str definer
   1.716 +          :: print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs)
   1.717 +          :: str "="
   1.718 +          :: separate (str "|") (map print_co cos)
   1.719 +        )
   1.720 +      end;
   1.721 +    fun print_def is_pseudo_fun needs_typ definer
   1.722 +          (ML_Function (name, (vs_ty as (vs, ty), eqs))) =
   1.723            let
   1.724 -            fun pr_eq ((ts, t), (thm, _)) =
   1.725 +            fun print_eqn ((ts, t), (thm, _)) =
   1.726                let
   1.727                  val consts = fold Code_Thingol.add_constnames (t :: ts) [];
   1.728                  val vars = reserved
   1.729 @@ -459,11 +486,11 @@
   1.730                        (insert (op =)) ts []);
   1.731                in concat [
   1.732                  (Pretty.block o Pretty.commas)
   1.733 -                  (map (pr_term is_pseudo_fun thm vars NOBR) ts),
   1.734 +                  (map (print_term is_pseudo_fun thm vars NOBR) ts),
   1.735                  str "->",
   1.736 -                pr_term is_pseudo_fun thm vars NOBR t
   1.737 +                print_term is_pseudo_fun thm vars NOBR t
   1.738                ] end;
   1.739 -            fun pr_eqs is_pseudo [((ts, t), (thm, _))] =
   1.740 +            fun print_eqns is_pseudo [((ts, t), (thm, _))] =
   1.741                    let
   1.742                      val consts = fold Code_Thingol.add_constnames (t :: ts) [];
   1.743                      val vars = reserved
   1.744 @@ -474,22 +501,22 @@
   1.745                    in
   1.746                      concat (
   1.747                        (if is_pseudo then [str "()"]
   1.748 -                        else map (pr_term is_pseudo_fun thm vars BR) ts)
   1.749 +                        else map (print_term is_pseudo_fun thm vars BR) ts)
   1.750                        @ str "="
   1.751 -                      @@ pr_term is_pseudo_fun thm vars NOBR t
   1.752 +                      @@ print_term is_pseudo_fun thm vars NOBR t
   1.753                      )
   1.754                    end
   1.755 -              | pr_eqs _ (eqs as (eq as (([_], _), _)) :: eqs') =
   1.756 +              | print_eqns _ ((eq as (([_], _), _)) :: eqs) =
   1.757                    Pretty.block (
   1.758                      str "="
   1.759                      :: Pretty.brk 1
   1.760                      :: str "function"
   1.761                      :: Pretty.brk 1
   1.762 -                    :: pr_eq eq
   1.763 +                    :: print_eqn eq
   1.764                      :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1]
   1.765 -                          o single o pr_eq) eqs'
   1.766 +                          o single o print_eqn) eqs
   1.767                    )
   1.768 -              | pr_eqs _ (eqs as eq :: eqs') =
   1.769 +              | print_eqns _ (eqs as eq :: eqs') =
   1.770                    let
   1.771                      val consts = fold Code_Thingol.add_constnames (map (snd o fst) eqs) [];
   1.772                      val vars = reserved
   1.773 @@ -508,142 +535,143 @@
   1.774                        :: Pretty.brk 1
   1.775                        :: str "with"
   1.776                        :: Pretty.brk 1
   1.777 -                      :: pr_eq eq
   1.778 +                      :: print_eqn eq
   1.779                        :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1]
   1.780 -                           o single o pr_eq) eqs'
   1.781 +                           o single o print_eqn) eqs'
   1.782                      )
   1.783                    end;
   1.784              val prolog = if needs_typ then
   1.785 -              concat [str definer, (str o deresolve) name, str ":", pr_typ NOBR ty]
   1.786 +              concat [str definer, (str o deresolve) name, str ":", print_typ NOBR ty]
   1.787                  else Pretty.strs [definer, deresolve name];
   1.788 -          in
   1.789 -            concat (
   1.790 +          in pair
   1.791 +            (print_val_decl print_typscheme (name, vs_ty))
   1.792 +            (concat (
   1.793                prolog
   1.794 -              :: pr_tyvar_dicts is_pseudo_fun (filter_out (null o snd) vs)
   1.795 -              @| pr_eqs (is_pseudo_fun name) eqs
   1.796 -            )
   1.797 +              :: print_dict_args vs
   1.798 +              @| print_eqns (is_pseudo_fun name) eqs
   1.799 +            ))
   1.800            end
   1.801 -      | pr_binding is_pseudo_fun _ definer (ML_Instance (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) =
   1.802 +      | print_def is_pseudo_fun _ definer (ML_Instance (inst, ((class, (tyco, vs)), (superinsts, classparams)))) =
   1.803            let
   1.804 -            fun pr_superclass (_, (classrel, dss)) =
   1.805 +            fun print_superinst (_, (classrel, dss)) =
   1.806                concat [
   1.807                  (str o deresolve) classrel,
   1.808                  str "=",
   1.809 -                pr_dicts is_pseudo_fun NOBR [DictConst dss]
   1.810 +                print_dict is_pseudo_fun NOBR (DictConst dss)
   1.811                ];
   1.812 -            fun pr_classparam_inst ((classparam, c_inst), (thm, _)) =
   1.813 +            fun print_classparam ((classparam, c_inst), (thm, _)) =
   1.814                concat [
   1.815                  (str o deresolve) classparam,
   1.816                  str "=",
   1.817 -                pr_app (K false) thm reserved NOBR (c_inst, [])
   1.818 +                print_app (K false) thm reserved NOBR (c_inst, [])
   1.819                ];
   1.820 -          in
   1.821 -            concat (
   1.822 +          in pair
   1.823 +            (print_val_decl print_dicttypscheme
   1.824 +              (inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
   1.825 +            (concat (
   1.826                str definer
   1.827                :: (str o deresolve) inst
   1.828 -              :: pr_tyvar_dicts is_pseudo_fun arity
   1.829 +              :: print_dict_args vs
   1.830                @ str "="
   1.831                @@ brackets [
   1.832 -                enum_default "()" ";" "{" "}" (map pr_superclass superarities
   1.833 -                  @ map pr_classparam_inst classparam_insts),
   1.834 +                enum_default "()" ";" "{" "}" (map print_superinst superinsts
   1.835 +                  @ map print_classparam classparams),
   1.836                  str ":",
   1.837 -                pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])
   1.838 +                print_tyco_expr NOBR (class, [tyco `%% map (ITyVar o fst) vs])
   1.839                ]
   1.840 -            )
   1.841 +            ))
   1.842            end;
   1.843 -     fun pr_stmt (ML_Exc (name, n)) =
   1.844 -          (concat o map str) (
   1.845 +     fun print_stmt (ML_Exc (name, (vs_ty, n))) = pair
   1.846 +          [print_val_decl print_typscheme (name, vs_ty)]
   1.847 +          ((doublesemicolon o map str) (
   1.848              "let"
   1.849              :: deresolve name
   1.850              :: replicate n "_"
   1.851              @ "="
   1.852              :: "failwith"
   1.853 -            @@ (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name ^ ";;"
   1.854 -          )
   1.855 -      | pr_stmt (ML_Val binding) =
   1.856 -           Pretty.block [pr_binding (K false) true "let" binding, str ";;"]
   1.857 -      | pr_stmt (ML_Funs (binding :: bindings, pseudo_funs)) =
   1.858 +            @@ (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name
   1.859 +          ))
   1.860 +      | print_stmt (ML_Val binding) =
   1.861            let
   1.862 -            val pr_binding' = pr_binding (member (op =) pseudo_funs) false;
   1.863 -            fun pr_pseudo_fun name = concat [
   1.864 +            val (sig_p, p) = print_def (K false) true "let" binding
   1.865 +          in pair
   1.866 +            [sig_p]
   1.867 +            (doublesemicolon [p])
   1.868 +          end
   1.869 +      | print_stmt (ML_Funs (binding :: bindings, pseudo_funs)) =
   1.870 +          let
   1.871 +            val print_def' = print_def (member (op =) pseudo_funs) false;
   1.872 +            fun print_pseudo_fun name = concat [
   1.873                  str "let",
   1.874                  (str o deresolve) name,
   1.875                  str "=",
   1.876                  (str o deresolve) name,
   1.877                  str "();;"
   1.878                ];
   1.879 -            val (ps, p) = split_last
   1.880 -              (pr_binding' "let rec" binding :: map (pr_binding' "and") bindings);
   1.881 -            val pseudo_ps = map pr_pseudo_fun pseudo_funs;
   1.882 -          in Pretty.chunks (ps @ Pretty.block ([p, str ";;"]) :: pseudo_ps) end
   1.883 -     | pr_stmt (ML_Datas (datas as (data :: datas'))) =
   1.884 +            val (sig_ps, (ps, p)) = (apsnd split_last o split_list)
   1.885 +              (print_def' "let rec" binding :: map (print_def' "and") bindings);
   1.886 +            val pseudo_ps = map print_pseudo_fun pseudo_funs;
   1.887 +          in pair
   1.888 +            sig_ps
   1.889 +            (Pretty.chunks (ps @ doublesemicolon [p] :: pseudo_ps))
   1.890 +          end
   1.891 +     | print_stmt (ML_Datas [(tyco, (vs, []))]) =
   1.892 +          let
   1.893 +            val ty_p = print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs);
   1.894 +          in
   1.895 +            pair
   1.896 +            [concat [str "type", ty_p]]
   1.897 +            (concat [str "type", ty_p, str "=", str "EMPTY__"])
   1.898 +          end
   1.899 +     | print_stmt (ML_Datas (data :: datas)) = 
   1.900            let
   1.901 -            fun pr_co (co, []) =
   1.902 -                  str (deresolve co)
   1.903 -              | pr_co (co, tys) =
   1.904 -                  concat [
   1.905 -                    str (deresolve co),
   1.906 -                    str "of",
   1.907 -                    Pretty.enum " *" "" "" (map (pr_typ (INFX (2, X))) tys)
   1.908 -                  ];
   1.909 -            fun pr_data definer (tyco, (vs, [])) =
   1.910 -                  concat (
   1.911 -                    str definer
   1.912 -                    :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
   1.913 -                    :: str "="
   1.914 -                    @@ str "EMPTY_"
   1.915 -                  )
   1.916 -              | pr_data definer (tyco, (vs, cos)) =
   1.917 -                  concat (
   1.918 -                    str definer
   1.919 -                    :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
   1.920 -                    :: str "="
   1.921 -                    :: separate (str "|") (map pr_co cos)
   1.922 -                  );
   1.923 -            val (ps, p) = split_last
   1.924 -              (pr_data "type" data :: map (pr_data "and") datas');
   1.925 -          in Pretty.chunks (ps @| Pretty.block ([p, str ";;"])) end
   1.926 -     | pr_stmt (ML_Class (class, (v, (superclasses, classparams)))) =
   1.927 +            val sig_ps = print_datatype_decl "type" data
   1.928 +              :: map (print_datatype_decl "and") datas;
   1.929 +            val (ps, p) = split_last sig_ps;
   1.930 +          in pair
   1.931 +            sig_ps
   1.932 +            (Pretty.chunks (ps @| doublesemicolon [p]))
   1.933 +          end
   1.934 +     | print_stmt (ML_Class (class, (v, (superclasses, classparams)))) =
   1.935            let
   1.936 +            fun print_field s p = concat [str s, str ":", p];
   1.937 +            fun print_superclass_field (superclass, classrel) =
   1.938 +              print_field (deresolve classrel) (print_dicttyp (superclass, ITyVar v));
   1.939 +            fun print_classparam_decl (classparam, ty) =
   1.940 +              print_val_decl print_typscheme
   1.941 +                (classparam, ([(v, [class])], ty));
   1.942 +            fun print_classparam_field (classparam, ty) =
   1.943 +              print_field (deresolve classparam) (print_typ NOBR ty);
   1.944              val w = "_" ^ first_upper v;
   1.945 -            fun pr_superclass_field (class, classrel) =
   1.946 -              (concat o map str) [
   1.947 -                deresolve classrel, ":", "'" ^ v, deresolve class
   1.948 -              ];
   1.949 -            fun pr_classparam_field (classparam, ty) =
   1.950 -              concat [
   1.951 -                (str o deresolve) classparam, str ":", pr_typ NOBR ty
   1.952 -              ];
   1.953 -            fun pr_classparam_proj (classparam, _) =
   1.954 -              concat [
   1.955 -                str "let",
   1.956 -                (str o deresolve) classparam,
   1.957 -                str w,
   1.958 +            fun print_classparam_proj (classparam, _) =
   1.959 +              (concat o map str) ["let", deresolve classparam, w, "=",
   1.960 +                w ^ "." ^ deresolve classparam ^ ";;"];
   1.961 +            val type_decl_p = concat [
   1.962 +                str ("type '" ^ v),
   1.963 +                (str o deresolve) class,
   1.964                  str "=",
   1.965 -                str (w ^ "." ^ deresolve classparam ^ ";;")
   1.966 +                enum_default "unit" ";" "{" "}" (
   1.967 +                  map print_superclass_field superclasses
   1.968 +                  @ map print_classparam_field classparams
   1.969 +                )
   1.970                ];
   1.971 -          in Pretty.chunks (
   1.972 -            concat [
   1.973 -              str ("type '" ^ v),
   1.974 -              (str o deresolve) class,
   1.975 -              str "=",
   1.976 -              enum_default "unit;;" ";" "{" "};;" (
   1.977 -                map pr_superclass_field superclasses
   1.978 -                @ map pr_classparam_field classparams
   1.979 -              )
   1.980 -            ]
   1.981 -            :: map pr_classparam_proj classparams
   1.982 -          ) end;
   1.983 - in pr_stmt end;
   1.984 +          in pair
   1.985 +            (type_decl_p :: map print_classparam_decl classparams)
   1.986 +            (Pretty.chunks (
   1.987 +              doublesemicolon [type_decl_p]
   1.988 +              :: map print_classparam_proj classparams
   1.989 +            ))
   1.990 +          end;
   1.991 +  in print_stmt end;
   1.992  
   1.993 -fun pr_ocaml_module name content =
   1.994 -  Pretty.chunks (
   1.995 -    str ("module " ^ name ^ " = ")
   1.996 -    :: str "struct"
   1.997 -    :: str ""
   1.998 -    :: content
   1.999 -    @ str ""
  1.1000 -    @@ str ("end;; (*struct " ^ name ^ "*)")
  1.1001 +fun print_ocaml_module name some_decls body = Pretty.chunks2 (
  1.1002 +    Pretty.chunks (
  1.1003 +      str ("module " ^ name ^ (if is_some some_decls then " : sig" else " ="))
  1.1004 +      :: (the_list o Option.map (Pretty.indent 2 o Pretty.chunks)) some_decls
  1.1005 +      @| (if is_some some_decls then str "end = struct" else str "struct")
  1.1006 +    )
  1.1007 +    :: body
  1.1008 +    @| str ("end;; (*struct " ^ name ^ "*)")
  1.1009    );
  1.1010  
  1.1011  val literals_ocaml = let
  1.1012 @@ -736,8 +764,8 @@
  1.1013                  | _ => (eqs, NONE)
  1.1014                else (eqs, NONE)
  1.1015            in (ML_Function (name, (tysm, eqs')), is_value) end
  1.1016 -      | ml_binding_of_stmt (name, Code_Thingol.Classinst (stmt as ((_, (_, arity)), _))) =
  1.1017 -          (ML_Instance (name, stmt), if null arity then SOME (name, false) else NONE)
  1.1018 +      | ml_binding_of_stmt (name, Code_Thingol.Classinst (stmt as ((_, (_, vs)), _))) =
  1.1019 +          (ML_Instance (name, stmt), if forall (null o snd) vs then SOME (name, false) else NONE)
  1.1020        | ml_binding_of_stmt (name, _) =
  1.1021            error ("Binding block containing illegal statement: " ^ labelled_name name)
  1.1022      fun add_fun (name, stmt) =
  1.1023 @@ -745,7 +773,8 @@
  1.1024          val (binding, some_value_name) = ml_binding_of_stmt (name, stmt);
  1.1025          val ml_stmt = case binding
  1.1026           of ML_Function (name, ((vs, ty), [])) =>
  1.1027 -              ML_Exc (name, (length o filter_out (null o snd)) vs + (length o fst o Code_Thingol.unfold_fun) ty)
  1.1028 +              ML_Exc (name, ((vs, ty),
  1.1029 +                (length o filter_out (null o snd)) vs + (length o fst o Code_Thingol.unfold_fun) ty))
  1.1030            | _ => case some_value_name
  1.1031               of NONE => ML_Funs ([binding], [])
  1.1032                | SOME (name, true) => ML_Funs ([binding], [name])
  1.1033 @@ -869,34 +898,35 @@
  1.1034          error ("Unknown statement name: " ^ labelled_name name);
  1.1035    in (deresolver, nodes) end;
  1.1036  
  1.1037 -fun serialize_ml target compile pr_module pr_stmt raw_module_name labelled_name reserved includes raw_module_alias
  1.1038 -  _ syntax_tyco syntax_const program stmt_names destination =
  1.1039 +fun serialize_ml target compile print_module print_stmt raw_module_name with_signatures labelled_name
  1.1040 +  reserved includes raw_module_alias _ syntax_tyco syntax_const program stmt_names destination =
  1.1041    let
  1.1042      val is_cons = Code_Thingol.is_cons program;
  1.1043 -    val present_stmt_names = Code_Target.stmt_names_of_destination destination;
  1.1044 -    val is_present = not (null present_stmt_names);
  1.1045 -    val module_name = if is_present then SOME "Code" else raw_module_name;
  1.1046 +    val presentation_stmt_names = Code_Target.stmt_names_of_destination destination;
  1.1047 +    val is_presentation = not (null presentation_stmt_names);
  1.1048 +    val module_name = if is_presentation then SOME "Code" else raw_module_name;
  1.1049      val (deresolver, nodes) = ml_node_of_program labelled_name module_name
  1.1050        reserved raw_module_alias program;
  1.1051      val reserved = make_vars reserved;
  1.1052 -    fun pr_node prefix (Dummy _) =
  1.1053 +    fun print_node prefix (Dummy _) =
  1.1054            NONE
  1.1055 -      | pr_node prefix (Stmt (_, stmt)) = if is_present andalso
  1.1056 -          (null o filter (member (op =) present_stmt_names) o stmt_names_of) stmt
  1.1057 +      | print_node prefix (Stmt (_, stmt)) = if is_presentation andalso
  1.1058 +          (null o filter (member (op =) presentation_stmt_names) o stmt_names_of) stmt
  1.1059            then NONE
  1.1060 -          else SOME
  1.1061 -            (pr_stmt labelled_name syntax_tyco syntax_const reserved
  1.1062 -              (deresolver prefix) is_cons stmt)
  1.1063 -      | pr_node prefix (Module (module_name, (_, nodes))) =
  1.1064 -          separate (str "")
  1.1065 -            ((map_filter (pr_node (prefix @ [module_name]) o Graph.get_node nodes)
  1.1066 -              o rev o flat o Graph.strong_conn) nodes)
  1.1067 -          |> (if is_present then Pretty.chunks else pr_module module_name)
  1.1068 -          |> SOME;
  1.1069 +          else SOME (print_stmt labelled_name syntax_tyco syntax_const reserved is_cons (deresolver prefix) stmt)
  1.1070 +      | print_node prefix (Module (module_name, (_, nodes))) =
  1.1071 +          let
  1.1072 +            val (decls, body) = print_nodes (prefix @ [module_name]) nodes;
  1.1073 +            val p = if is_presentation then Pretty.chunks2 body
  1.1074 +              else print_module module_name (if with_signatures then SOME decls else NONE) body;
  1.1075 +          in SOME ([], p) end
  1.1076 +    and print_nodes prefix nodes = (map_filter (print_node prefix o Graph.get_node nodes)
  1.1077 +        o rev o flat o Graph.strong_conn) nodes
  1.1078 +      |> split_list
  1.1079 +      |> (fn (decls, body) => (flat decls, body))
  1.1080      val stmt_names' = (map o try)
  1.1081        (deresolver (if is_some module_name then the_list module_name else [])) stmt_names;
  1.1082 -    val p = Pretty.chunks (separate (str "") (map snd includes @ (map_filter
  1.1083 -      (pr_node [] o Graph.get_node nodes) o rev o flat o Graph.strong_conn) nodes));
  1.1084 +    val p = Pretty.chunks2 (map snd includes @ snd (print_nodes [] nodes));
  1.1085    in
  1.1086      Code_Target.mk_serialization target
  1.1087        (case compile of SOME compile => SOME (compile o Code_Target.code_of_pretty) | NONE => NONE)
  1.1088 @@ -909,9 +939,16 @@
  1.1089  
  1.1090  (** ML (system language) code for evaluation and instrumentalization **)
  1.1091  
  1.1092 -fun eval_code_of some_target thy = Code_Target.serialize_custom thy (the_default target_Eval some_target,
  1.1093 -    (fn _ => fn [] => serialize_ml target_SML (SOME (K ())) (K Pretty.chunks) pr_sml_stmt (SOME ""),
  1.1094 -  literals_sml));
  1.1095 +val eval_struct_name = "Code"
  1.1096 +
  1.1097 +fun eval_code_of some_target with_struct thy =
  1.1098 +  let
  1.1099 +    val target = the_default target_Eval some_target;
  1.1100 +    val serialize = if with_struct then fn _ => fn [] =>
  1.1101 +        serialize_ml target_SML (SOME (K ())) print_sml_module print_sml_stmt (SOME eval_struct_name) true
  1.1102 +      else fn _ => fn [] => 
  1.1103 +        serialize_ml target_SML (SOME (K ())) ((K o K) Pretty.chunks2) print_sml_stmt (SOME eval_struct_name) true;
  1.1104 +  in Code_Target.serialize_custom thy (target, (serialize, literals_sml)) end;
  1.1105  
  1.1106  
  1.1107  (* evaluation *)
  1.1108 @@ -928,7 +965,7 @@
  1.1109            |> Graph.new_node (value_name,
  1.1110                Code_Thingol.Fun (Term.dummy_patternN, (([], ty), [(([], t), (Drule.dummy_thm, true))])))
  1.1111            |> fold (curry Graph.add_edge value_name) deps;
  1.1112 -        val (value_code, [SOME value_name']) = eval_code_of some_target thy naming program' [value_name];
  1.1113 +        val (value_code, [SOME value_name']) = eval_code_of some_target false thy naming program' [value_name];
  1.1114          val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name'
  1.1115            ^ space_implode " " (map (enclose "(" ")") args) ^ " end";
  1.1116        in ML_Context.evaluate ctxt false reff sml_code end;
  1.1117 @@ -952,7 +989,7 @@
  1.1118    let
  1.1119      val (consts', (naming, program)) = Code_Thingol.consts_program thy consts;
  1.1120      val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos;
  1.1121 -    val (ml_code, target_names) = eval_code_of NONE thy naming program (consts' @ tycos');
  1.1122 +    val (ml_code, target_names) = eval_code_of NONE true thy naming program (consts' @ tycos');
  1.1123      val (consts'', tycos'') = chop (length consts') target_names;
  1.1124      val consts_map = map2 (fn const => fn NONE =>
  1.1125          error ("Constant " ^ (quote o Code.string_of_const thy) const
  1.1126 @@ -970,7 +1007,7 @@
  1.1127      val tycos' = fold (insert (op =)) new_tycos tycos;
  1.1128      val consts' = fold (insert (op =)) new_consts consts;
  1.1129      val (struct_name', ctxt') = if struct_name = ""
  1.1130 -      then ML_Antiquote.variant "Code" ctxt
  1.1131 +      then ML_Antiquote.variant eval_struct_name ctxt
  1.1132        else (struct_name, ctxt);
  1.1133      val acc_code = Lazy.lazy (delayed_code (ProofContext.theory_of ctxt) tycos' consts');
  1.1134    in CodeAntiqData.put ((tycos', consts'), (false, (struct_name', acc_code))) ctxt' end;
  1.1135 @@ -998,9 +1035,8 @@
  1.1136  fun print_code struct_name is_first print_it ctxt =
  1.1137    let
  1.1138      val (_, (_, (struct_code_name, acc_code))) = CodeAntiqData.get ctxt;
  1.1139 -    val (raw_ml_code, (tycos_map, consts_map)) = Lazy.force acc_code;
  1.1140 -    val ml_code = if is_first then "\nstructure " ^ struct_code_name
  1.1141 -        ^ " =\nstruct\n\n" ^ raw_ml_code ^ "\nend;\n\n"
  1.1142 +    val (ml_code, (tycos_map, consts_map)) = Lazy.force acc_code;
  1.1143 +    val ml_code = if is_first then ml_code
  1.1144        else "";
  1.1145      val all_struct_name = Long_Name.append struct_name struct_code_name;
  1.1146    in (ml_code, print_it all_struct_name tycos_map consts_map) end;
  1.1147 @@ -1038,31 +1074,31 @@
  1.1148        >> ml_code_datatype_antiq);
  1.1149  
  1.1150  fun isar_seri_sml module_name =
  1.1151 -  Code_Target.parse_args (Scan.succeed ())
  1.1152 -  #> (fn () => serialize_ml target_SML
  1.1153 +  Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
  1.1154 +  >> (fn with_signatures => serialize_ml target_SML
  1.1155        (SOME (use_text ML_Env.local_context (1, "generated code") false))
  1.1156 -      pr_sml_module pr_sml_stmt module_name);
  1.1157 +      print_sml_module print_sml_stmt module_name with_signatures));
  1.1158  
  1.1159  fun isar_seri_ocaml module_name =
  1.1160 -  Code_Target.parse_args (Scan.succeed ())
  1.1161 -  #> (fn () => serialize_ml target_OCaml NONE
  1.1162 -      pr_ocaml_module pr_ocaml_stmt module_name);
  1.1163 +  Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
  1.1164 +  >> (fn with_signatures => serialize_ml target_OCaml NONE
  1.1165 +      print_ocaml_module print_ocaml_stmt module_name with_signatures));
  1.1166  
  1.1167  val setup =
  1.1168    Code_Target.add_target (target_SML, (isar_seri_sml, literals_sml))
  1.1169    #> Code_Target.add_target (target_OCaml, (isar_seri_ocaml, literals_ocaml))
  1.1170    #> Code_Target.extend_target (target_Eval, (target_SML, K I))
  1.1171 -  #> Code_Target.add_syntax_tyco target_SML "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
  1.1172 +  #> Code_Target.add_syntax_tyco target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
  1.1173        brackify_infix (1, R) fxy [
  1.1174 -        pr_typ (INFX (1, X)) ty1,
  1.1175 +        print_typ (INFX (1, X)) ty1,
  1.1176          str "->",
  1.1177 -        pr_typ (INFX (1, R)) ty2
  1.1178 +        print_typ (INFX (1, R)) ty2
  1.1179        ]))
  1.1180 -  #> Code_Target.add_syntax_tyco target_OCaml "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
  1.1181 +  #> Code_Target.add_syntax_tyco target_OCaml "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
  1.1182        brackify_infix (1, R) fxy [
  1.1183 -        pr_typ (INFX (1, X)) ty1,
  1.1184 +        print_typ (INFX (1, X)) ty1,
  1.1185          str "->",
  1.1186 -        pr_typ (INFX (1, R)) ty2
  1.1187 +        print_typ (INFX (1, R)) ty2
  1.1188        ]))
  1.1189    #> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names
  1.1190    #> fold (Code_Target.add_reserved target_SML)