src/Tools/code/code_target.ML
changeset 24219 e558fe311376
child 24251 ae3eb1766e56
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/code/code_target.ML	Fri Aug 10 17:04:34 2007 +0200
     1.3 @@ -0,0 +1,2211 @@
     1.4 +(*  Title:      Tools/code/code_target.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Florian Haftmann, TU Muenchen
     1.7 +
     1.8 +Serializer from intermediate language ("Thin-gol")
     1.9 +to target languages (like SML or Haskell).
    1.10 +*)
    1.11 +
    1.12 +signature CODE_TARGET =
    1.13 +sig
    1.14 +  include BASIC_CODE_THINGOL;
    1.15 +
    1.16 +  val add_syntax_class: string -> class
    1.17 +    -> (string * (CodeUnit.const * string) list) option -> theory -> theory;
    1.18 +  val add_syntax_inst: string -> string * class -> bool -> theory -> theory;
    1.19 +  val add_syntax_tycoP: string -> string -> OuterParse.token list
    1.20 +    -> (theory -> theory) * OuterParse.token list;
    1.21 +  val add_syntax_constP: string -> string -> OuterParse.token list
    1.22 +    -> (theory -> theory) * OuterParse.token list;
    1.23 +
    1.24 +  val add_undefined: string -> string -> string -> theory -> theory;
    1.25 +  val add_pretty_list: string -> string -> string -> theory -> theory;
    1.26 +  val add_pretty_list_string: string -> string -> string
    1.27 +    -> string -> string list -> theory -> theory;
    1.28 +  val add_pretty_char: string -> string -> string list -> theory -> theory
    1.29 +  val add_pretty_numeral: string -> bool -> string * typ -> string -> string -> string
    1.30 +    -> string -> string -> theory -> theory;
    1.31 +  val add_pretty_ml_string: string -> string -> string list -> string
    1.32 +    -> string -> string -> theory -> theory;
    1.33 +  val add_pretty_imperative_monad_bind: string -> string -> theory -> theory;
    1.34 +
    1.35 +  type serializer;
    1.36 +  val add_serializer: string * serializer -> theory -> theory;
    1.37 +  val get_serializer: theory -> string -> bool -> string option -> string option -> Args.T list
    1.38 +    -> (theory -> string -> string) -> string list option -> CodeThingol.code -> unit;
    1.39 +  val assert_serializer: theory -> string -> string;
    1.40 +
    1.41 +  val eval_verbose: bool ref;
    1.42 +  val eval_term: theory -> (theory -> string -> string) -> CodeThingol.code
    1.43 +    -> (string * 'a option ref) * CodeThingol.iterm -> string list -> 'a;
    1.44 +  val code_width: int ref;
    1.45 +
    1.46 +  val setup: theory -> theory;
    1.47 +end;
    1.48 +
    1.49 +structure CodeTarget : CODE_TARGET =
    1.50 +struct
    1.51 +
    1.52 +open BasicCodeThingol;
    1.53 +
    1.54 +(** basics **)
    1.55 +
    1.56 +infixr 5 @@;
    1.57 +infixr 5 @|;
    1.58 +fun x @@ y = [x, y];
    1.59 +fun xs @| y = xs @ [y];
    1.60 +val str = PrintMode.with_default Pretty.str;
    1.61 +val concat = Pretty.block o Pretty.breaks;
    1.62 +val brackets = Pretty.enclose "(" ")" o Pretty.breaks;
    1.63 +fun semicolon ps = Pretty.block [concat ps, str ";"];
    1.64 +
    1.65 +
    1.66 +(** syntax **)
    1.67 +
    1.68 +datatype lrx = L | R | X;
    1.69 +
    1.70 +datatype fixity =
    1.71 +    BR
    1.72 +  | NOBR
    1.73 +  | INFX of (int * lrx);
    1.74 +
    1.75 +val APP = INFX (~1, L);
    1.76 +
    1.77 +fun eval_lrx L L = false
    1.78 +  | eval_lrx R R = false
    1.79 +  | eval_lrx _ _ = true;
    1.80 +
    1.81 +fun eval_fxy NOBR NOBR = false
    1.82 +  | eval_fxy BR NOBR = false
    1.83 +  | eval_fxy NOBR BR = false
    1.84 +  | eval_fxy (INFX (pr, lr)) (INFX (pr_ctxt, lr_ctxt)) =
    1.85 +      pr < pr_ctxt
    1.86 +      orelse pr = pr_ctxt
    1.87 +        andalso eval_lrx lr lr_ctxt
    1.88 +      orelse pr_ctxt = ~1
    1.89 +  | eval_fxy _ (INFX _) = false
    1.90 +  | eval_fxy (INFX _) NOBR = false
    1.91 +  | eval_fxy _ _ = true;
    1.92 +
    1.93 +fun gen_brackify _ [p] = p
    1.94 +  | gen_brackify true (ps as _::_) = Pretty.enclose "(" ")" ps
    1.95 +  | gen_brackify false (ps as _::_) = Pretty.block ps;
    1.96 +
    1.97 +fun brackify fxy_ctxt ps =
    1.98 +  gen_brackify (eval_fxy BR fxy_ctxt) (Pretty.breaks ps);
    1.99 +
   1.100 +fun brackify_infix infx fxy_ctxt ps =
   1.101 +  gen_brackify (eval_fxy (INFX infx) fxy_ctxt) (Pretty.breaks ps);
   1.102 +
   1.103 +type class_syntax = string * (string -> string option);
   1.104 +type typ_syntax = int * ((fixity -> itype -> Pretty.T)
   1.105 +  -> fixity -> itype list -> Pretty.T);
   1.106 +type term_syntax = int * ((CodeName.var_ctxt -> fixity -> iterm -> Pretty.T)
   1.107 +  -> CodeName.var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
   1.108 +
   1.109 +
   1.110 +(* user-defined syntax *)
   1.111 +
   1.112 +datatype 'a mixfix =
   1.113 +    Arg of fixity
   1.114 +  | Pretty of Pretty.T;
   1.115 +
   1.116 +fun mk_mixfix prep_arg (fixity_this, mfx) =
   1.117 +  let
   1.118 +    fun is_arg (Arg _) = true
   1.119 +      | is_arg _ = false;
   1.120 +    val i = (length o filter is_arg) mfx;
   1.121 +    fun fillin _ [] [] =
   1.122 +          []
   1.123 +      | fillin pr (Arg fxy :: mfx) (a :: args) =
   1.124 +          (pr fxy o prep_arg) a :: fillin pr mfx args
   1.125 +      | fillin pr (Pretty p :: mfx) args =
   1.126 +          p :: fillin pr mfx args
   1.127 +      | fillin _ [] _ =
   1.128 +          error ("Inconsistent mixfix: too many arguments")
   1.129 +      | fillin _ _ [] =
   1.130 +          error ("Inconsistent mixfix: too less arguments");
   1.131 +  in
   1.132 +    (i, fn pr => fn fixity_ctxt => fn args =>
   1.133 +      gen_brackify (eval_fxy fixity_this fixity_ctxt) (fillin pr mfx args))
   1.134 +  end;
   1.135 +
   1.136 +fun parse_infix prep_arg (x, i) s =
   1.137 +  let
   1.138 +    val l = case x of L => INFX (i, L) | _ => INFX (i, X);
   1.139 +    val r = case x of R => INFX (i, R) | _ => INFX (i, X);
   1.140 +  in
   1.141 +    mk_mixfix prep_arg (INFX (i, x), [Arg l, (Pretty o Pretty.brk) 1, (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r])
   1.142 +  end;
   1.143 +
   1.144 +fun parse_mixfix prep_arg s =
   1.145 +  let
   1.146 +    val sym_any = Scan.one Symbol.is_regular;
   1.147 +    val parse = Scan.optional ($$ "!" >> K true) false -- Scan.repeat (
   1.148 +         ($$ "(" -- $$ "_" -- $$ ")" >> K (Arg NOBR))
   1.149 +      || ($$ "_" >> K (Arg BR))
   1.150 +      || ($$ "/" |-- Scan.repeat ($$ " ") >> (Pretty o Pretty.brk o length))
   1.151 +      || (Scan.repeat1
   1.152 +           (   $$ "'" |-- sym_any
   1.153 +            || Scan.unless ($$ "_" || $$ "/" || $$ "(" |-- $$ "_" |-- $$ ")")
   1.154 +                 sym_any) >> (Pretty o str o implode)));
   1.155 +  in case Scan.finite Symbol.stopper parse (Symbol.explode s)
   1.156 +   of ((_, p as [_]), []) => mk_mixfix prep_arg (NOBR, p)
   1.157 +    | ((b, p as _ :: _ :: _), []) => mk_mixfix prep_arg (if b then NOBR else BR, p)
   1.158 +    | _ => Scan.!! (the_default ("malformed mixfix annotation: " ^ quote s) o snd) Scan.fail ()
   1.159 +  end;
   1.160 +
   1.161 +fun parse_args f args =
   1.162 +  case Scan.read Args.stopper f args
   1.163 +   of SOME x => x
   1.164 +    | NONE => error "Bad serializer arguments";
   1.165 +
   1.166 +
   1.167 +(* generic serializer combinators *)
   1.168 +
   1.169 +fun gen_pr_app pr_app' pr_term const_syntax labelled_name is_cons
   1.170 +      lhs vars fxy (app as ((c, (_, tys)), ts)) =
   1.171 +  case const_syntax c
   1.172 +   of NONE => if lhs andalso not (is_cons c) then
   1.173 +          error ("non-constructor on left hand side of equation: " ^ labelled_name c)
   1.174 +        else brackify fxy (pr_app' lhs vars app)
   1.175 +    | SOME (i, pr) =>
   1.176 +        let
   1.177 +          val k = if i < 0 then length tys else i;
   1.178 +          fun pr' fxy ts = pr (pr_term lhs) vars fxy (ts ~~ curry Library.take k tys);
   1.179 +        in if k = length ts
   1.180 +          then pr' fxy ts
   1.181 +        else if k < length ts
   1.182 +          then case chop k ts of (ts1, ts2) =>
   1.183 +            brackify fxy (pr' APP ts1 :: map (pr_term lhs vars BR) ts2)
   1.184 +          else pr_term lhs vars fxy (CodeThingol.eta_expand app k)
   1.185 +        end;
   1.186 +
   1.187 +fun gen_pr_bind pr_bind' pr_term fxy ((v, pat), ty) vars =
   1.188 +  let
   1.189 +    val vs = case pat
   1.190 +     of SOME pat => CodeThingol.fold_varnames (insert (op =)) pat []
   1.191 +      | NONE => [];
   1.192 +    val vars' = CodeName.intro_vars (the_list v) vars;
   1.193 +    val vars'' = CodeName.intro_vars vs vars';
   1.194 +    val v' = Option.map (CodeName.lookup_var vars') v;
   1.195 +    val pat' = Option.map (pr_term vars'' fxy) pat;
   1.196 +  in (pr_bind' ((v', pat'), ty), vars'') end;
   1.197 +
   1.198 +
   1.199 +(* list, char, string, numeral and monad abstract syntax transformations *)
   1.200 +
   1.201 +fun implode_list c_nil c_cons t =
   1.202 +  let
   1.203 +    fun dest_cons (IConst (c, _) `$ t1 `$ t2) =
   1.204 +          if c = c_cons
   1.205 +          then SOME (t1, t2)
   1.206 +          else NONE
   1.207 +      | dest_cons _ = NONE;
   1.208 +    val (ts, t') = CodeThingol.unfoldr dest_cons t;
   1.209 +  in case t'
   1.210 +   of IConst (c, _) => if c = c_nil then SOME ts else NONE
   1.211 +    | _ => NONE
   1.212 +  end;
   1.213 +
   1.214 +fun decode_char c_nibbles (IConst (c1, _), IConst (c2, _)) =
   1.215 +      let
   1.216 +        fun idx c = find_index (curry (op =) c) c_nibbles;
   1.217 +        fun decode ~1 _ = NONE
   1.218 +          | decode _ ~1 = NONE
   1.219 +          | decode n m = SOME (chr (n * 16 + m));
   1.220 +      in decode (idx c1) (idx c2) end
   1.221 +  | decode_char _ _ = NONE;
   1.222 +
   1.223 +fun implode_string c_char c_nibbles mk_char mk_string ts =
   1.224 +  let
   1.225 +    fun implode_char (IConst (c, _) `$ t1 `$ t2) =
   1.226 +          if c = c_char then decode_char c_nibbles (t1, t2) else NONE
   1.227 +      | implode_char _ = NONE;
   1.228 +    val ts' = map implode_char ts;
   1.229 +  in if forall is_some ts'
   1.230 +    then (SOME o str o mk_string o implode o map_filter I) ts'
   1.231 +    else NONE
   1.232 +  end;
   1.233 +
   1.234 +fun implode_numeral c_bit0 c_bit1 c_pls c_min c_bit =
   1.235 +  let
   1.236 +    fun dest_bit (IConst (c, _)) = if c = c_bit0 then SOME 0
   1.237 +          else if c = c_bit1 then SOME 1
   1.238 +          else NONE
   1.239 +      | dest_bit _ = NONE;
   1.240 +    fun dest_numeral (IConst (c, _)) = if c = c_pls then SOME (IntInf.fromInt 0)
   1.241 +          else if c = c_min then SOME (IntInf.fromInt ~1)
   1.242 +          else NONE
   1.243 +      | dest_numeral (IConst (c, _) `$ t1 `$ t2) =
   1.244 +          if c = c_bit then case (dest_numeral t1, dest_bit t2)
   1.245 +           of (SOME n, SOME b) => SOME (IntInf.fromInt 2 * n + IntInf.fromInt b)
   1.246 +            | _ => NONE
   1.247 +          else NONE
   1.248 +      | dest_numeral _ = NONE;
   1.249 +  in dest_numeral end;
   1.250 +
   1.251 +fun implode_monad c_mbind c_kbind t =
   1.252 +  let
   1.253 +    fun dest_monad (IConst (c, _) `$ t1 `$ t2) =
   1.254 +          if c = c_mbind
   1.255 +            then case CodeThingol.split_abs t2
   1.256 +             of SOME (((v, pat), ty), t') => SOME ((SOME (((SOME v, pat), ty), true), t1), t')
   1.257 +              | NONE => NONE
   1.258 +          else if c = c_kbind
   1.259 +            then SOME ((NONE, t1), t2)
   1.260 +            else NONE
   1.261 +      | dest_monad t = case CodeThingol.split_let t
   1.262 +           of SOME (((pat, ty), tbind), t') => SOME ((SOME (((NONE, SOME pat), ty), false), tbind), t')
   1.263 +            | NONE => NONE;
   1.264 +  in CodeThingol.unfoldr dest_monad t end;
   1.265 +
   1.266 +
   1.267 +(** name auxiliary **)
   1.268 +
   1.269 +val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode;
   1.270 +val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode;
   1.271 +
   1.272 +val dest_name =
   1.273 +  apfst NameSpace.implode o split_last o fst o split_last o NameSpace.explode;
   1.274 +
   1.275 +fun mk_modl_name_tab init_names prefix module_alias code =
   1.276 +  let
   1.277 +    fun nsp_map f = NameSpace.explode #> map f #> NameSpace.implode;
   1.278 +    fun mk_alias name =
   1.279 +     case module_alias name
   1.280 +      of SOME name' => name'
   1.281 +       | NONE => nsp_map (fn name => (the_single o fst)
   1.282 +            (Name.variants [name] init_names)) name;
   1.283 +    fun mk_prefix name =
   1.284 +      case prefix
   1.285 +       of SOME prefix => NameSpace.append prefix name
   1.286 +        | NONE => name;
   1.287 +    val tab =
   1.288 +      Symtab.empty
   1.289 +      |> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name))
   1.290 +           o fst o dest_name o fst)
   1.291 +             code
   1.292 +  in fn name => (the o Symtab.lookup tab) name end;
   1.293 +
   1.294 +
   1.295 +
   1.296 +(** SML/OCaml serializer **)
   1.297 +
   1.298 +datatype ml_def =
   1.299 +    MLFuns of (string * ((iterm list * iterm) list * typscheme)) list
   1.300 +  | MLDatas of (string * ((vname * sort) list * (string * itype list) list)) list
   1.301 +  | MLClass of string * ((class * string) list * (vname * (string * itype) list))
   1.302 +  | MLClassinst of string * ((class * (string * (vname * sort) list))
   1.303 +        * ((class * (string * (string * dict list list))) list
   1.304 +      * (string * iterm) list));
   1.305 +
   1.306 +fun pr_sml tyco_syntax const_syntax labelled_name init_syms deresolv is_cons ml_def =
   1.307 +  let
   1.308 +    val pr_label_classrel = translate_string (fn "." => "__" | c => c) o NameSpace.qualifier;
   1.309 +    val pr_label_classop = NameSpace.base o NameSpace.qualifier;
   1.310 +    fun pr_dicts fxy ds =
   1.311 +      let
   1.312 +        fun pr_dictvar (v, (_, 1)) = first_upper v ^ "_"
   1.313 +          | pr_dictvar (v, (i, _)) = first_upper v ^ string_of_int (i+1) ^ "_";
   1.314 +        fun pr_proj [] p =
   1.315 +              p
   1.316 +          | pr_proj [p'] p =
   1.317 +              brackets [p', p]
   1.318 +          | pr_proj (ps as _ :: _) p =
   1.319 +              brackets [Pretty.enum " o" "(" ")" ps, p];
   1.320 +        fun pr_dictc fxy (DictConst (inst, dss)) =
   1.321 +              brackify fxy ((str o deresolv) inst :: map (pr_dicts BR) dss)
   1.322 +          | pr_dictc fxy (DictVar (classrels, v)) =
   1.323 +              pr_proj (map (str o deresolv) classrels) ((str o pr_dictvar) v)
   1.324 +      in case ds
   1.325 +       of [] => str "()"
   1.326 +        | [d] => pr_dictc fxy d
   1.327 +        | _ :: _ => (Pretty.list "(" ")" o map (pr_dictc NOBR)) ds
   1.328 +      end;
   1.329 +    fun pr_tyvars vs =
   1.330 +      vs
   1.331 +      |> map (fn (v, sort) => map_index (fn (i, _) => DictVar ([], (v, (i, length sort)))) sort)
   1.332 +      |> map (pr_dicts BR);
   1.333 +    fun pr_tycoexpr fxy (tyco, tys) =
   1.334 +      let
   1.335 +        val tyco' = (str o deresolv) tyco
   1.336 +      in case map (pr_typ BR) tys
   1.337 +       of [] => tyco'
   1.338 +        | [p] => Pretty.block [p, Pretty.brk 1, tyco']
   1.339 +        | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco']
   1.340 +      end
   1.341 +    and pr_typ fxy (tyco `%% tys) =
   1.342 +          (case tyco_syntax tyco
   1.343 +           of NONE => pr_tycoexpr fxy (tyco, tys)
   1.344 +            | SOME (i, pr) =>
   1.345 +                if not (i = length tys)
   1.346 +                then error ("Number of argument mismatch in customary serialization: "
   1.347 +                  ^ (string_of_int o length) tys ^ " given, "
   1.348 +                  ^ string_of_int i ^ " expected")
   1.349 +                else pr pr_typ fxy tys)
   1.350 +      | pr_typ fxy (ITyVar v) =
   1.351 +          str ("'" ^ v);
   1.352 +    fun pr_term lhs vars fxy (IConst c) =
   1.353 +          pr_app lhs vars fxy (c, [])
   1.354 +      | pr_term lhs vars fxy (IVar v) =
   1.355 +          str (CodeName.lookup_var vars v)
   1.356 +      | pr_term lhs vars fxy (t as t1 `$ t2) =
   1.357 +          (case CodeThingol.unfold_const_app t
   1.358 +           of SOME c_ts => pr_app lhs vars fxy c_ts
   1.359 +            | NONE =>
   1.360 +                brackify fxy [pr_term lhs vars NOBR t1, pr_term lhs vars BR t2])
   1.361 +      | pr_term lhs vars fxy (t as _ `|-> _) =
   1.362 +          let
   1.363 +            val (binds, t') = CodeThingol.unfold_abs t;
   1.364 +            fun pr ((v, pat), ty) =
   1.365 +              pr_bind NOBR ((SOME v, pat), ty)
   1.366 +              #>> (fn p => concat [str "fn", p, str "=>"]);
   1.367 +            val (ps, vars') = fold_map pr binds vars;
   1.368 +          in brackets (ps @ [pr_term lhs vars' NOBR t']) end
   1.369 +      | pr_term lhs vars fxy (ICase (cases as (_, t0))) = (case CodeThingol.unfold_const_app t0
   1.370 +           of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
   1.371 +                then pr_case vars fxy cases
   1.372 +                else pr_app lhs vars fxy c_ts
   1.373 +            | NONE => pr_case vars fxy cases)
   1.374 +    and pr_app' lhs vars (app as ((c, (iss, tys)), ts)) =
   1.375 +      if is_cons c then let
   1.376 +        val k = length tys
   1.377 +      in if k < 2 then 
   1.378 +        (str o deresolv) c :: map (pr_term lhs vars BR) ts
   1.379 +      else if k = length ts then
   1.380 +        [(str o deresolv) c, Pretty.enum "," "(" ")" (map (pr_term lhs vars NOBR) ts)]
   1.381 +      else [pr_term lhs vars BR (CodeThingol.eta_expand app k)] end else
   1.382 +        (str o deresolv) c
   1.383 +          :: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term lhs vars BR) ts
   1.384 +    and pr_app lhs vars = gen_pr_app pr_app' pr_term const_syntax labelled_name is_cons lhs vars
   1.385 +    and pr_bind' ((NONE, NONE), _) = str "_"
   1.386 +      | pr_bind' ((SOME v, NONE), _) = str v
   1.387 +      | pr_bind' ((NONE, SOME p), _) = p
   1.388 +      | pr_bind' ((SOME v, SOME p), _) = concat [str v, str "as", p]
   1.389 +    and pr_bind fxy = gen_pr_bind pr_bind' (pr_term false) fxy
   1.390 +    and pr_case vars fxy (cases as ((_, [_]), _)) =
   1.391 +          let
   1.392 +            val (binds, t') = CodeThingol.unfold_let (ICase cases);
   1.393 +            fun pr ((pat, ty), t) vars =
   1.394 +              vars
   1.395 +              |> pr_bind NOBR ((NONE, SOME pat), ty)
   1.396 +              |>> (fn p => semicolon [str "val", p, str "=", pr_term false vars NOBR t])
   1.397 +            val (ps, vars') = fold_map pr binds vars;
   1.398 +          in
   1.399 +            Pretty.chunks [
   1.400 +              [str ("let"), Pretty.fbrk, Pretty.chunks ps] |> Pretty.block,
   1.401 +              [str ("in"), Pretty.fbrk, pr_term false vars' NOBR t'] |> Pretty.block,
   1.402 +              str ("end")
   1.403 +            ]
   1.404 +          end
   1.405 +      | pr_case vars fxy (((td, ty), b::bs), _) =
   1.406 +          let
   1.407 +            fun pr delim (pat, t) =
   1.408 +              let
   1.409 +                val (p, vars') = pr_bind NOBR ((NONE, SOME pat), ty) vars;
   1.410 +              in
   1.411 +                concat [str delim, p, str "=>", pr_term false vars' NOBR t]
   1.412 +              end;
   1.413 +          in
   1.414 +            (Pretty.enclose "(" ")" o single o brackify fxy) (
   1.415 +              str "case"
   1.416 +              :: pr_term false vars NOBR td
   1.417 +              :: pr "of" b
   1.418 +              :: map (pr "|") bs
   1.419 +            )
   1.420 +          end
   1.421 +      | pr_case vars fxy ((_, []), _) = str "raise Fail \"empty case\""
   1.422 +    fun pr_def (MLFuns (funns as (funn :: funns'))) =
   1.423 +          let
   1.424 +            val definer =
   1.425 +              let
   1.426 +                fun mk [] [] = "val"
   1.427 +                  | mk (_::_) _ = "fun"
   1.428 +                  | mk [] vs = if (null o filter_out (null o snd)) vs then "val" else "fun";
   1.429 +                fun chk (_, ((ts, _) :: _, (vs, _))) NONE = SOME (mk ts vs)
   1.430 +                  | chk (_, ((ts, _) :: _, (vs, _))) (SOME defi) =
   1.431 +                      if defi = mk ts vs then SOME defi
   1.432 +                      else error ("Mixing simultaneous vals and funs not implemented: "
   1.433 +                        ^ commas (map (labelled_name o fst) funns));
   1.434 +              in the (fold chk funns NONE) end;
   1.435 +            fun pr_funn definer (name, (eqs as eq::eqs', (raw_vs, ty))) =
   1.436 +              let
   1.437 +                val vs = filter_out (null o snd) raw_vs;
   1.438 +                val shift = if null eqs' then I else
   1.439 +                  map (Pretty.block o single o Pretty.block o single);
   1.440 +                fun pr_eq definer (ts, t) =
   1.441 +                  let
   1.442 +                    val consts = map_filter
   1.443 +                      (fn c => if (is_some o const_syntax) c
   1.444 +                        then NONE else (SOME o NameSpace.base o deresolv) c)
   1.445 +                        ((fold o CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []);
   1.446 +                    val vars = init_syms
   1.447 +                      |> CodeName.intro_vars consts
   1.448 +                      |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames)
   1.449 +                           (insert (op =)) ts []);
   1.450 +                  in
   1.451 +                    concat (
   1.452 +                      [str definer, (str o deresolv) name]
   1.453 +                      @ (if null ts andalso null vs
   1.454 +                           andalso not (ty = ITyVar "_")(*for evaluation*)
   1.455 +                         then [str ":", pr_typ NOBR ty]
   1.456 +                         else
   1.457 +                           pr_tyvars vs
   1.458 +                           @ map (pr_term true vars BR) ts)
   1.459 +                   @ [str "=", pr_term false vars NOBR t]
   1.460 +                    )
   1.461 +                  end
   1.462 +              in
   1.463 +                (Pretty.block o Pretty.fbreaks o shift) (
   1.464 +                  pr_eq definer eq
   1.465 +                  :: map (pr_eq "|") eqs'
   1.466 +                )
   1.467 +              end;
   1.468 +            val (ps, p) = split_last (pr_funn definer funn :: map (pr_funn "and") funns');
   1.469 +          in Pretty.chunks (ps @ [Pretty.block ([p, str ";"])]) end
   1.470 +     | pr_def (MLDatas (datas as (data :: datas'))) =
   1.471 +          let
   1.472 +            fun pr_co (co, []) =
   1.473 +                  str (deresolv co)
   1.474 +              | pr_co (co, tys) =
   1.475 +                  concat [
   1.476 +                    str (deresolv co),
   1.477 +                    str "of",
   1.478 +                    Pretty.enum " *" "" "" (map (pr_typ (INFX (2, X))) tys)
   1.479 +                  ];
   1.480 +            fun pr_data definer (tyco, (vs, [])) =
   1.481 +                  concat (
   1.482 +                    str definer
   1.483 +                    :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
   1.484 +                    :: str "="
   1.485 +                    @@ str "EMPTY__" 
   1.486 +                  )
   1.487 +              | pr_data definer (tyco, (vs, cos)) =
   1.488 +                  concat (
   1.489 +                    str definer
   1.490 +                    :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
   1.491 +                    :: str "="
   1.492 +                    :: separate (str "|") (map pr_co cos)
   1.493 +                  );
   1.494 +            val (ps, p) = split_last (pr_data "datatype" data :: map (pr_data "and") datas');
   1.495 +          in Pretty.chunks (ps @ [Pretty.block ([p, str ";"])]) end
   1.496 +     | pr_def (MLClass (class, (superclasses, (v, classops)))) =
   1.497 +          let
   1.498 +            val w = first_upper v ^ "_";
   1.499 +            fun pr_superclass_field (class, classrel) =
   1.500 +              (concat o map str) [
   1.501 +                pr_label_classrel classrel, ":", "'" ^ v, deresolv class
   1.502 +              ];
   1.503 +            fun pr_classop_field (classop, ty) =
   1.504 +              concat [
   1.505 +                (str o pr_label_classop) classop, str ":", pr_typ NOBR ty
   1.506 +              ];
   1.507 +            fun pr_classop_proj (classop, _) =
   1.508 +              semicolon [
   1.509 +                str "fun",
   1.510 +                (str o deresolv) classop,
   1.511 +                Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolv class)],
   1.512 +                str "=",
   1.513 +                str ("#" ^ pr_label_classop classop),
   1.514 +                str w
   1.515 +              ];
   1.516 +            fun pr_superclass_proj (_, classrel) =
   1.517 +              semicolon [
   1.518 +                str "fun",
   1.519 +                (str o deresolv) classrel,
   1.520 +                Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolv class)],
   1.521 +                str "=",
   1.522 +                str ("#" ^ pr_label_classrel classrel),
   1.523 +                str w
   1.524 +              ];
   1.525 +          in
   1.526 +            Pretty.chunks (
   1.527 +              concat [
   1.528 +                str ("type '" ^ v),
   1.529 +                (str o deresolv) class,
   1.530 +                str "=",
   1.531 +                Pretty.enum "," "{" "};" (
   1.532 +                  map pr_superclass_field superclasses @ map pr_classop_field classops
   1.533 +                )
   1.534 +              ]
   1.535 +              :: map pr_superclass_proj superclasses
   1.536 +              @ map pr_classop_proj classops
   1.537 +            )
   1.538 +          end
   1.539 +     | pr_def (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classop_defs)))) =
   1.540 +          let
   1.541 +            fun pr_superclass (_, (classrel, dss)) =
   1.542 +              concat [
   1.543 +                (str o pr_label_classrel) classrel,
   1.544 +                str "=",
   1.545 +                pr_dicts NOBR [DictConst dss]
   1.546 +              ];
   1.547 +            fun pr_classop (classop, t) =
   1.548 +              let
   1.549 +                val consts = map_filter
   1.550 +                  (fn c => if (is_some o const_syntax) c
   1.551 +                    then NONE else (SOME o NameSpace.base o deresolv) c)
   1.552 +                    (CodeThingol.fold_constnames (insert (op =)) t []);
   1.553 +                val vars = CodeName.intro_vars consts init_syms;
   1.554 +              in
   1.555 +                concat [
   1.556 +                  (str o pr_label_classop) classop,
   1.557 +                  str "=",
   1.558 +                  pr_term false vars NOBR t
   1.559 +                ]
   1.560 +              end;
   1.561 +          in
   1.562 +            semicolon ([
   1.563 +              str (if null arity then "val" else "fun"),
   1.564 +              (str o deresolv) inst ] @
   1.565 +              pr_tyvars arity @ [
   1.566 +              str "=",
   1.567 +              Pretty.enum "," "{" "}" (map pr_superclass superarities @ map pr_classop classop_defs),
   1.568 +              str ":",
   1.569 +              pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])
   1.570 +            ])
   1.571 +          end;
   1.572 +  in pr_def ml_def end;
   1.573 +
   1.574 +fun pr_sml_modl name content =
   1.575 +  Pretty.chunks ([
   1.576 +    str ("structure " ^ name ^ " = "),
   1.577 +    str "struct",
   1.578 +    str ""
   1.579 +  ] @ content @ [
   1.580 +    str "",
   1.581 +    str ("end; (*struct " ^ name ^ "*)")
   1.582 +  ]);
   1.583 +
   1.584 +fun pr_ocaml tyco_syntax const_syntax labelled_name init_syms deresolv is_cons ml_def =
   1.585 +  let
   1.586 +    fun pr_dicts fxy ds =
   1.587 +      let
   1.588 +        fun pr_dictvar (v, (_, 1)) = "_" ^ first_upper v
   1.589 +          | pr_dictvar (v, (i, _)) = "_" ^ first_upper v ^ string_of_int (i+1);
   1.590 +        fun pr_proj ps p =
   1.591 +          fold_rev (fn p2 => fn p1 => Pretty.block [p1, str ".", str p2]) ps p
   1.592 +        fun pr_dictc fxy (DictConst (inst, dss)) =
   1.593 +              brackify fxy ((str o deresolv) inst :: map (pr_dicts BR) dss)
   1.594 +          | pr_dictc fxy (DictVar (classrels, v)) =
   1.595 +              pr_proj (map deresolv classrels) ((str o pr_dictvar) v)
   1.596 +      in case ds
   1.597 +       of [] => str "()"
   1.598 +        | [d] => pr_dictc fxy d
   1.599 +        | _ :: _ => (Pretty.list "(" ")" o map (pr_dictc NOBR)) ds
   1.600 +      end;
   1.601 +    fun pr_tyvars vs =
   1.602 +      vs
   1.603 +      |> map (fn (v, sort) => map_index (fn (i, _) => DictVar ([], (v, (i, length sort)))) sort)
   1.604 +      |> map (pr_dicts BR);
   1.605 +    fun pr_tycoexpr fxy (tyco, tys) =
   1.606 +      let
   1.607 +        val tyco' = (str o deresolv) tyco
   1.608 +      in case map (pr_typ BR) tys
   1.609 +       of [] => tyco'
   1.610 +        | [p] => Pretty.block [p, Pretty.brk 1, tyco']
   1.611 +        | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco']
   1.612 +      end
   1.613 +    and pr_typ fxy (tyco `%% tys) =
   1.614 +          (case tyco_syntax tyco
   1.615 +           of NONE => pr_tycoexpr fxy (tyco, tys)
   1.616 +            | SOME (i, pr) =>
   1.617 +                if not (i = length tys)
   1.618 +                then error ("Number of argument mismatch in customary serialization: "
   1.619 +                  ^ (string_of_int o length) tys ^ " given, "
   1.620 +                  ^ string_of_int i ^ " expected")
   1.621 +                else pr pr_typ fxy tys)
   1.622 +      | pr_typ fxy (ITyVar v) =
   1.623 +          str ("'" ^ v);
   1.624 +    fun pr_term lhs vars fxy (IConst c) =
   1.625 +          pr_app lhs vars fxy (c, [])
   1.626 +      | pr_term lhs vars fxy (IVar v) =
   1.627 +          str (CodeName.lookup_var vars v)
   1.628 +      | pr_term lhs vars fxy (t as t1 `$ t2) =
   1.629 +          (case CodeThingol.unfold_const_app t
   1.630 +           of SOME c_ts => pr_app lhs vars fxy c_ts
   1.631 +            | NONE =>
   1.632 +                brackify fxy [pr_term lhs vars NOBR t1, pr_term lhs vars BR t2])
   1.633 +      | pr_term lhs vars fxy (t as _ `|-> _) =
   1.634 +          let
   1.635 +            val (binds, t') = CodeThingol.unfold_abs t;
   1.636 +            fun pr ((v, pat), ty) = pr_bind BR ((SOME v, pat), ty);
   1.637 +            val (ps, vars') = fold_map pr binds vars;
   1.638 +          in brackets (str "fun" :: ps @ str "->" @@ pr_term lhs vars' NOBR t') end
   1.639 +      | pr_term lhs vars fxy (ICase (cases as (_, t0))) = (case CodeThingol.unfold_const_app t0
   1.640 +           of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
   1.641 +                then pr_case vars fxy cases
   1.642 +                else pr_app lhs vars fxy c_ts
   1.643 +            | NONE => pr_case vars fxy cases)
   1.644 +    and pr_app' lhs vars (app as ((c, (iss, tys)), ts)) =
   1.645 +      if is_cons c then
   1.646 +        if length tys = length ts
   1.647 +        then case ts
   1.648 +         of [] => [(str o deresolv) c]
   1.649 +          | [t] => [(str o deresolv) c, pr_term lhs vars BR t]
   1.650 +          | _ => [(str o deresolv) c, Pretty.enum "," "(" ")" (map (pr_term lhs vars NOBR) ts)]
   1.651 +        else [pr_term lhs vars BR (CodeThingol.eta_expand app (length tys))]
   1.652 +      else (str o deresolv) c
   1.653 +        :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term lhs vars BR) ts)
   1.654 +    and pr_app lhs vars = gen_pr_app pr_app' pr_term const_syntax labelled_name is_cons lhs vars
   1.655 +    and pr_bind' ((NONE, NONE), _) = str "_"
   1.656 +      | pr_bind' ((SOME v, NONE), _) = str v
   1.657 +      | pr_bind' ((NONE, SOME p), _) = p
   1.658 +      | pr_bind' ((SOME v, SOME p), _) = brackets [p, str "as", str v]
   1.659 +    and pr_bind fxy = gen_pr_bind pr_bind' (pr_term false) fxy
   1.660 +    and pr_case vars fxy (cases as ((_, [_]), _)) =
   1.661 +          let
   1.662 +            val (binds, t') = CodeThingol.unfold_let (ICase cases);
   1.663 +            fun pr ((pat, ty), t) vars =
   1.664 +              vars
   1.665 +              |> pr_bind NOBR ((NONE, SOME pat), ty)
   1.666 +              |>> (fn p => concat [str "let", p, str "=", pr_term false vars NOBR t, str "in"])
   1.667 +            val (ps, vars') = fold_map pr binds vars;
   1.668 +          in Pretty.chunks (ps @| pr_term false vars' NOBR t') end
   1.669 +      | pr_case vars fxy (((td, ty), b::bs), _) =
   1.670 +          let
   1.671 +            fun pr delim (pat, t) =
   1.672 +              let
   1.673 +                val (p, vars') = pr_bind NOBR ((NONE, SOME pat), ty) vars;
   1.674 +              in concat [str delim, p, str "->", pr_term false vars' NOBR t] end;
   1.675 +          in
   1.676 +            (Pretty.enclose "(" ")" o single o brackify fxy) (
   1.677 +              str "match"
   1.678 +              :: pr_term false vars NOBR td
   1.679 +              :: pr "with" b
   1.680 +              :: map (pr "|") bs
   1.681 +            )
   1.682 +          end
   1.683 +      | pr_case vars fxy ((_, []), _) = str "failwith \"empty case\"";
   1.684 +    fun pr_def (MLFuns (funns as funn :: funns')) =
   1.685 +          let
   1.686 +            fun fish_parm _ (w as SOME _) = w
   1.687 +              | fish_parm (IVar v) NONE = SOME v
   1.688 +              | fish_parm _ NONE = NONE;
   1.689 +            fun fillup_parm _ (_, SOME v) = v
   1.690 +              | fillup_parm x (i, NONE) = x ^ string_of_int i;
   1.691 +            fun fish_parms vars eqs =
   1.692 +              let
   1.693 +                val raw_fished = fold (map2 fish_parm) eqs (replicate (length (hd eqs)) NONE);
   1.694 +                val x = Name.variant (map_filter I raw_fished) "x";
   1.695 +                val fished = map_index (fillup_parm x) raw_fished;
   1.696 +                val vars' = CodeName.intro_vars fished vars;
   1.697 +              in map (CodeName.lookup_var vars') fished end;
   1.698 +            fun pr_eq (ts, t) =
   1.699 +              let
   1.700 +                val consts = map_filter
   1.701 +                  (fn c => if (is_some o const_syntax) c
   1.702 +                    then NONE else (SOME o NameSpace.base o deresolv) c)
   1.703 +                    ((fold o CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []);
   1.704 +                val vars = init_syms
   1.705 +                  |> CodeName.intro_vars consts
   1.706 +                  |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames)
   1.707 +                      (insert (op =)) ts []);
   1.708 +              in concat [
   1.709 +                (Pretty.block o Pretty.commas) (map (pr_term true vars NOBR) ts),
   1.710 +                str "->",
   1.711 +                pr_term false vars NOBR t
   1.712 +              ] end;
   1.713 +            fun pr_eqs [(ts, t)] =
   1.714 +                  let
   1.715 +                    val consts = map_filter
   1.716 +                      (fn c => if (is_some o const_syntax) c
   1.717 +                        then NONE else (SOME o NameSpace.base o deresolv) c)
   1.718 +                        ((fold o CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []);
   1.719 +                    val vars = init_syms
   1.720 +                      |> CodeName.intro_vars consts
   1.721 +                      |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames)
   1.722 +                          (insert (op =)) ts []);
   1.723 +                  in
   1.724 +                    concat (
   1.725 +                      map (pr_term true vars BR) ts
   1.726 +                      @ str "="
   1.727 +                      @@ pr_term false vars NOBR t
   1.728 +                    )
   1.729 +                  end
   1.730 +              | pr_eqs (eqs as (eq as ([_], _)) :: eqs') =
   1.731 +                  Pretty.block (
   1.732 +                    str "="
   1.733 +                    :: Pretty.brk 1
   1.734 +                    :: str "function"
   1.735 +                    :: Pretty.brk 1
   1.736 +                    :: pr_eq eq
   1.737 +                    :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1] o single o pr_eq) eqs'
   1.738 +                  )
   1.739 +              | pr_eqs (eqs as eq :: eqs') =
   1.740 +                  let
   1.741 +                    val consts = map_filter
   1.742 +                      (fn c => if (is_some o const_syntax) c
   1.743 +                        then NONE else (SOME o NameSpace.base o deresolv) c)
   1.744 +                        ((fold o CodeThingol.fold_constnames) (insert (op =)) (map snd eqs) []);
   1.745 +                    val vars = init_syms
   1.746 +                      |> CodeName.intro_vars consts;
   1.747 +                    val dummy_parms = (map str o fish_parms vars o map fst) eqs;
   1.748 +                  in
   1.749 +                    Pretty.block (
   1.750 +                      Pretty.breaks dummy_parms
   1.751 +                      @ Pretty.brk 1
   1.752 +                      :: str "="
   1.753 +                      :: Pretty.brk 1
   1.754 +                      :: str "match"
   1.755 +                      :: Pretty.brk 1
   1.756 +                      :: (Pretty.block o Pretty.commas) dummy_parms
   1.757 +                      :: Pretty.brk 1
   1.758 +                      :: str "with"
   1.759 +                      :: Pretty.brk 1
   1.760 +                      :: pr_eq eq
   1.761 +                      :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1] o single o pr_eq) eqs'
   1.762 +                    )
   1.763 +                  end;
   1.764 +            fun pr_funn definer (name, (eqs, (vs, ty))) =
   1.765 +              concat (
   1.766 +                str definer
   1.767 +                :: (str o deresolv) name
   1.768 +                :: pr_tyvars (filter_out (null o snd) vs)
   1.769 +                @| pr_eqs eqs
   1.770 +              );
   1.771 +            val (ps, p) = split_last (pr_funn "let rec" funn :: map (pr_funn "and") funns');
   1.772 +          in Pretty.chunks (ps @ [Pretty.block ([p, str ";;"])]) end
   1.773 +     | pr_def (MLDatas (datas as (data :: datas'))) =
   1.774 +          let
   1.775 +            fun pr_co (co, []) =
   1.776 +                  str (deresolv co)
   1.777 +              | pr_co (co, tys) =
   1.778 +                  concat [
   1.779 +                    str (deresolv co),
   1.780 +                    str "of",
   1.781 +                    Pretty.enum " *" "" "" (map (pr_typ (INFX (2, X))) tys)
   1.782 +                  ];
   1.783 +            fun pr_data definer (tyco, (vs, [])) =
   1.784 +                  concat (
   1.785 +                    str definer
   1.786 +                    :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
   1.787 +                    :: str "="
   1.788 +                    @@ str "EMPTY_"
   1.789 +                  )
   1.790 +              | pr_data definer (tyco, (vs, cos)) =
   1.791 +                  concat (
   1.792 +                    str definer
   1.793 +                    :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
   1.794 +                    :: str "="
   1.795 +                    :: separate (str "|") (map pr_co cos)
   1.796 +                  );
   1.797 +            val (ps, p) = split_last (pr_data "type" data :: map (pr_data "and") datas');
   1.798 +          in Pretty.chunks (ps @ [Pretty.block ([p, str ";;"])]) end
   1.799 +     | pr_def (MLClass (class, (superclasses, (v, classops)))) =
   1.800 +          let
   1.801 +            val w = "_" ^ first_upper v;
   1.802 +            fun pr_superclass_field (class, classrel) =
   1.803 +              (concat o map str) [
   1.804 +                deresolv classrel, ":", "'" ^ v, deresolv class
   1.805 +              ];
   1.806 +            fun pr_classop_field (classop, ty) =
   1.807 +              concat [
   1.808 +                (str o deresolv) classop, str ":", pr_typ NOBR ty
   1.809 +              ];
   1.810 +            fun pr_classop_proj (classop, _) =
   1.811 +              concat [
   1.812 +                str "let",
   1.813 +                (str o deresolv) classop,
   1.814 +                str w,
   1.815 +                str "=",
   1.816 +                str (w ^ "." ^ deresolv classop ^ ";;")
   1.817 +              ];
   1.818 +          in Pretty.chunks (
   1.819 +            concat [
   1.820 +              str ("type '" ^ v),
   1.821 +              (str o deresolv) class,
   1.822 +              str "=",
   1.823 +              Pretty.enum ";" "{" "};;" (
   1.824 +                map pr_superclass_field superclasses @ map pr_classop_field classops
   1.825 +              )
   1.826 +            ]
   1.827 +            :: map pr_classop_proj classops
   1.828 +          ) end
   1.829 +     | pr_def (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classop_defs)))) =
   1.830 +          let
   1.831 +            fun pr_superclass (_, (classrel, dss)) =
   1.832 +              concat [
   1.833 +                (str o deresolv) classrel,
   1.834 +                str "=",
   1.835 +                pr_dicts NOBR [DictConst dss]
   1.836 +              ];
   1.837 +            fun pr_classop_def (classop, t) =
   1.838 +              let
   1.839 +                val consts = map_filter
   1.840 +                  (fn c => if (is_some o const_syntax) c
   1.841 +                    then NONE else (SOME o NameSpace.base o deresolv) c)
   1.842 +                    (CodeThingol.fold_constnames (insert (op =)) t []);
   1.843 +                val vars = CodeName.intro_vars consts init_syms;
   1.844 +              in
   1.845 +                concat [
   1.846 +                  (str o deresolv) classop,
   1.847 +                  str "=",
   1.848 +                  pr_term false vars NOBR t
   1.849 +                ]
   1.850 +              end;
   1.851 +          in
   1.852 +            concat (
   1.853 +              str "let"
   1.854 +              :: (str o deresolv) inst
   1.855 +              :: pr_tyvars arity
   1.856 +              @ str "="
   1.857 +              @@ (Pretty.enclose "(" ");;" o Pretty.breaks) [
   1.858 +                Pretty.enum ";" "{" "}" (map pr_superclass superarities @ map pr_classop_def classop_defs),
   1.859 +                str ":",
   1.860 +                pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])
   1.861 +              ]
   1.862 +            )
   1.863 +          end;
   1.864 +  in pr_def ml_def end;
   1.865 +
   1.866 +fun pr_ocaml_modl name content =
   1.867 +  Pretty.chunks ([
   1.868 +    str ("module " ^ name ^ " = "),
   1.869 +    str "struct",
   1.870 +    str ""
   1.871 +  ] @ content @ [
   1.872 +    str "",
   1.873 +    str ("end;; (*struct " ^ name ^ "*)")
   1.874 +  ]);
   1.875 +
   1.876 +val code_width = ref 80;
   1.877 +fun code_output p = Pretty.setmp_margin (!code_width) Pretty.output p ^ "\n";
   1.878 +
   1.879 +fun seri_ml pr_def pr_modl module output labelled_name reserved_syms raw_module_alias module_prolog
   1.880 +  (_ : string -> class_syntax option) tyco_syntax const_syntax code =
   1.881 +  let
   1.882 +    val module_alias = if is_some module then K module else raw_module_alias;
   1.883 +    val is_cons = CodeThingol.is_cons code;
   1.884 +    datatype node =
   1.885 +        Def of string * ml_def option
   1.886 +      | Module of string * ((Name.context * Name.context) * node Graph.T);
   1.887 +    val init_names = Name.make_context reserved_syms;
   1.888 +    val init_module = ((init_names, init_names), Graph.empty);
   1.889 +    fun map_node [] f = f
   1.890 +      | map_node (m::ms) f =
   1.891 +          Graph.default_node (m, Module (m, init_module))
   1.892 +          #> Graph.map_node m (fn (Module (dmodlname, (nsp, nodes))) => Module (dmodlname, (nsp, map_node ms f nodes)));
   1.893 +    fun map_nsp_yield [] f (nsp, nodes) =
   1.894 +          let
   1.895 +            val (x, nsp') = f nsp
   1.896 +          in (x, (nsp', nodes)) end
   1.897 +      | map_nsp_yield (m::ms) f (nsp, nodes) =
   1.898 +          let
   1.899 +            val (x, nodes') =
   1.900 +              nodes
   1.901 +              |> Graph.default_node (m, Module (m, init_module))
   1.902 +              |> Graph.map_node_yield m (fn Module (dmodlname, nsp_nodes) => 
   1.903 +                  let
   1.904 +                    val (x, nsp_nodes') = map_nsp_yield ms f nsp_nodes
   1.905 +                  in (x, Module (dmodlname, nsp_nodes')) end)
   1.906 +          in (x, (nsp, nodes')) end;
   1.907 +    val init_syms = CodeName.make_vars reserved_syms;
   1.908 +    val name_modl = mk_modl_name_tab init_names NONE module_alias code;
   1.909 +    fun name_def upper name nsp =
   1.910 +      let
   1.911 +        val (_, base) = dest_name name;
   1.912 +        val base' = if upper then first_upper base else base;
   1.913 +        val ([base''], nsp') = Name.variants [base'] nsp;
   1.914 +      in (base'', nsp') end;
   1.915 +    fun map_nsp_fun f (nsp_fun, nsp_typ) =
   1.916 +      let
   1.917 +        val (x, nsp_fun') = f nsp_fun
   1.918 +      in (x, (nsp_fun', nsp_typ)) end;
   1.919 +    fun map_nsp_typ f (nsp_fun, nsp_typ) =
   1.920 +      let
   1.921 +        val (x, nsp_typ') = f nsp_typ
   1.922 +      in (x, (nsp_fun, nsp_typ')) end;
   1.923 +    fun mk_funs defs =
   1.924 +      fold_map
   1.925 +        (fn (name, CodeThingol.Fun info) =>
   1.926 +              map_nsp_fun (name_def false name) >> (fn base => (base, (name, info)))
   1.927 +          | (name, def) => error ("Function block containing illegal definition: " ^ labelled_name name)
   1.928 +        ) defs
   1.929 +      >> (split_list #> apsnd MLFuns);
   1.930 +    fun mk_datatype defs =
   1.931 +      fold_map
   1.932 +        (fn (name, CodeThingol.Datatype info) =>
   1.933 +              map_nsp_typ (name_def false name) >> (fn base => (base, SOME (name, info)))
   1.934 +          | (name, CodeThingol.Datatypecons _) =>
   1.935 +              map_nsp_fun (name_def true name) >> (fn base => (base, NONE))
   1.936 +          | (name, def) => error ("Datatype block containing illegal definition: " ^ labelled_name name)
   1.937 +        ) defs
   1.938 +      >> (split_list #> apsnd (map_filter I
   1.939 +        #> (fn [] => error ("Datatype block without data definition: " ^ (commas o map (labelled_name o fst)) defs)
   1.940 +             | infos => MLDatas infos)));
   1.941 +    fun mk_class defs =
   1.942 +      fold_map
   1.943 +        (fn (name, CodeThingol.Class info) =>
   1.944 +              map_nsp_typ (name_def false name) >> (fn base => (base, SOME (name, info)))
   1.945 +          | (name, CodeThingol.Classrel _) =>
   1.946 +              map_nsp_fun (name_def false name) >> (fn base => (base, NONE))
   1.947 +          | (name, CodeThingol.Classop _) =>
   1.948 +              map_nsp_fun (name_def false name) >> (fn base => (base, NONE))
   1.949 +          | (name, def) => error ("Class block containing illegal definition: " ^ labelled_name name)
   1.950 +        ) defs
   1.951 +      >> (split_list #> apsnd (map_filter I
   1.952 +        #> (fn [] => error ("Class block without class definition: " ^ (commas o map (labelled_name o fst)) defs)
   1.953 +             | [info] => MLClass info)));
   1.954 +    fun mk_inst [(name, CodeThingol.Classinst info)] =
   1.955 +      map_nsp_fun (name_def false name)
   1.956 +      >> (fn base => ([base], MLClassinst (name, info)));
   1.957 +    fun add_group mk defs nsp_nodes =
   1.958 +      let
   1.959 +        val names as (name :: names') = map fst defs;
   1.960 +        val deps =
   1.961 +          []
   1.962 +          |> fold (fold (insert (op =)) o Graph.imm_succs code) names
   1.963 +          |> subtract (op =) names;
   1.964 +        val (modls, _) = (split_list o map dest_name) names;
   1.965 +        val modl' = (the_single o distinct (op =) o map name_modl) modls
   1.966 +          handle Empty =>
   1.967 +            error ("Illegal mutual dependencies: " ^ commas (map labelled_name names));
   1.968 +        val modl_explode = NameSpace.explode modl';
   1.969 +        fun add_dep name name'' =
   1.970 +          let
   1.971 +            val modl'' = (name_modl o fst o dest_name) name'';
   1.972 +          in if modl' = modl'' then
   1.973 +            map_node modl_explode
   1.974 +              (Graph.add_edge (name, name''))
   1.975 +          else let
   1.976 +            val (common, (diff1::_, diff2::_)) = chop_prefix (op =)
   1.977 +              (modl_explode, NameSpace.explode modl'');
   1.978 +          in
   1.979 +            map_node common
   1.980 +              (fn gr => Graph.add_edge_acyclic (diff1, diff2) gr
   1.981 +                handle Graph.CYCLES _ => error ("Dependency "
   1.982 +                  ^ quote name ^ " -> " ^ quote name''
   1.983 +                  ^ " would result in module dependency cycle"))
   1.984 +          end end;
   1.985 +      in
   1.986 +        nsp_nodes
   1.987 +        |> map_nsp_yield modl_explode (mk defs)
   1.988 +        |-> (fn (base' :: bases', def') =>
   1.989 +           apsnd (map_node modl_explode (Graph.new_node (name, (Def (base', SOME def')))
   1.990 +              #> fold2 (fn name' => fn base' => Graph.new_node (name', (Def (base', NONE)))) names' bases')))
   1.991 +        |> apsnd (fold (fn name => fold (add_dep name) deps) names)
   1.992 +        |> apsnd (fold (map_node modl_explode o Graph.add_edge) (product names names))
   1.993 +      end;
   1.994 +    fun group_defs [(_, CodeThingol.Bot)] =
   1.995 +          I
   1.996 +      | group_defs ((defs as (_, CodeThingol.Fun _)::_)) =
   1.997 +          add_group mk_funs defs
   1.998 +      | group_defs ((defs as (_, CodeThingol.Datatypecons _)::_)) =
   1.999 +          add_group mk_datatype defs
  1.1000 +      | group_defs ((defs as (_, CodeThingol.Datatype _)::_)) =
  1.1001 +          add_group mk_datatype defs
  1.1002 +      | group_defs ((defs as (_, CodeThingol.Class _)::_)) =
  1.1003 +          add_group mk_class defs
  1.1004 +      | group_defs ((defs as (_, CodeThingol.Classrel _)::_)) =
  1.1005 +          add_group mk_class defs
  1.1006 +      | group_defs ((defs as (_, CodeThingol.Classop _)::_)) =
  1.1007 +          add_group mk_class defs
  1.1008 +      | group_defs ((defs as [(_, CodeThingol.Classinst _)])) =
  1.1009 +          add_group mk_inst defs
  1.1010 +      | group_defs defs = error ("Illegal mutual dependencies: " ^
  1.1011 +          (commas o map (labelled_name o fst)) defs)
  1.1012 +    val (_, nodes) =
  1.1013 +      init_module
  1.1014 +      |> fold group_defs (map (AList.make (Graph.get_node code))
  1.1015 +          (rev (Graph.strong_conn code)))
  1.1016 +    fun deresolver prefix name = 
  1.1017 +      let
  1.1018 +        val modl = (fst o dest_name) name;
  1.1019 +        val modl' = (NameSpace.explode o name_modl) modl;
  1.1020 +        val (_, (_, remainder)) = chop_prefix (op =) (prefix, modl');
  1.1021 +        val defname' =
  1.1022 +          nodes
  1.1023 +          |> fold (fn m => fn g => case Graph.get_node g m
  1.1024 +              of Module (_, (_, g)) => g) modl'
  1.1025 +          |> (fn g => case Graph.get_node g name of Def (defname, _) => defname);
  1.1026 +      in
  1.1027 +        NameSpace.implode (remainder @ [defname'])
  1.1028 +      end handle Graph.UNDEF _ =>
  1.1029 +        error ("Unknown definition name: " ^ labelled_name name);
  1.1030 +    fun the_prolog modlname = case module_prolog modlname
  1.1031 +     of NONE => []
  1.1032 +      | SOME p => [p, str ""];
  1.1033 +    fun pr_node prefix (Def (_, NONE)) =
  1.1034 +          NONE
  1.1035 +      | pr_node prefix (Def (_, SOME def)) =
  1.1036 +          SOME (pr_def tyco_syntax const_syntax labelled_name init_syms
  1.1037 +            (deresolver prefix) is_cons def)
  1.1038 +      | pr_node prefix (Module (dmodlname, (_, nodes))) =
  1.1039 +          SOME (pr_modl dmodlname (the_prolog (NameSpace.implode (prefix @ [dmodlname]))
  1.1040 +            @ separate (str "") ((map_filter (pr_node (prefix @ [dmodlname]) o Graph.get_node nodes)
  1.1041 +                o rev o flat o Graph.strong_conn) nodes)));
  1.1042 +    val p = Pretty.chunks (the_prolog "" @ separate (str "") ((map_filter
  1.1043 +      (pr_node [] o Graph.get_node nodes) o rev o flat o Graph.strong_conn) nodes))
  1.1044 +  in output p end;
  1.1045 +
  1.1046 +val eval_verbose = ref false;
  1.1047 +
  1.1048 +fun isar_seri_sml module file =
  1.1049 +  let
  1.1050 +    val output = case file
  1.1051 +     of NONE => use_text "generated code" Output.ml_output (!eval_verbose) o code_output
  1.1052 +      | SOME "-" => writeln o code_output
  1.1053 +      | SOME file => File.write (Path.explode file) o code_output;
  1.1054 +  in
  1.1055 +    parse_args (Scan.succeed ())
  1.1056 +    #> (fn () => seri_ml pr_sml pr_sml_modl module output)
  1.1057 +  end;
  1.1058 +
  1.1059 +fun isar_seri_ocaml module file =
  1.1060 +  let
  1.1061 +    val output = case file
  1.1062 +     of NONE => error "OCaml: no internal compilation"
  1.1063 +      | SOME "-" => writeln o code_output
  1.1064 +      | SOME file => File.write (Path.explode file) o code_output;
  1.1065 +    fun output_file file = File.write (Path.explode file) o code_output;
  1.1066 +    val output_diag = writeln o code_output;
  1.1067 +  in
  1.1068 +    parse_args (Scan.succeed ())
  1.1069 +    #> (fn () => seri_ml pr_ocaml pr_ocaml_modl module output)
  1.1070 +  end;
  1.1071 +
  1.1072 +
  1.1073 +(** Haskell serializer **)
  1.1074 +
  1.1075 +local
  1.1076 +
  1.1077 +fun pr_bind' ((NONE, NONE), _) = str "_"
  1.1078 +  | pr_bind' ((SOME v, NONE), _) = str v
  1.1079 +  | pr_bind' ((NONE, SOME p), _) = p
  1.1080 +  | pr_bind' ((SOME v, SOME p), _) = brackets [str v, str "@", p]
  1.1081 +
  1.1082 +val pr_bind_haskell = gen_pr_bind pr_bind';
  1.1083 +
  1.1084 +in
  1.1085 +
  1.1086 +fun pr_haskell class_syntax tyco_syntax const_syntax labelled_name init_syms
  1.1087 +    deresolv_here deresolv is_cons deriving_show def =
  1.1088 +  let
  1.1089 +    fun class_name class = case class_syntax class
  1.1090 +     of NONE => deresolv class
  1.1091 +      | SOME (class, _) => class;
  1.1092 +    fun classop_name class classop = case class_syntax class
  1.1093 +     of NONE => deresolv_here classop
  1.1094 +      | SOME (_, classop_syntax) => case classop_syntax classop
  1.1095 +         of NONE => (snd o dest_name) classop
  1.1096 +          | SOME classop => classop
  1.1097 +    fun pr_typparms tyvars vs =
  1.1098 +      case maps (fn (v, sort) => map (pair v) sort) vs
  1.1099 +       of [] => str ""
  1.1100 +        | xs => Pretty.block [
  1.1101 +            Pretty.enum "," "(" ")" (
  1.1102 +              map (fn (v, class) => str
  1.1103 +                (class_name class ^ " " ^ CodeName.lookup_var tyvars v)) xs
  1.1104 +            ),
  1.1105 +            str " => "
  1.1106 +          ];
  1.1107 +    fun pr_tycoexpr tyvars fxy (tyco, tys) =
  1.1108 +      brackify fxy (str tyco :: map (pr_typ tyvars BR) tys)
  1.1109 +    and pr_typ tyvars fxy (tycoexpr as tyco `%% tys) =
  1.1110 +          (case tyco_syntax tyco
  1.1111 +           of NONE =>
  1.1112 +                pr_tycoexpr tyvars fxy (deresolv tyco, tys)
  1.1113 +            | SOME (i, pr) =>
  1.1114 +                if not (i = length tys)
  1.1115 +                then error ("Number of argument mismatch in customary serialization: "
  1.1116 +                  ^ (string_of_int o length) tys ^ " given, "
  1.1117 +                  ^ string_of_int i ^ " expected")
  1.1118 +                else pr (pr_typ tyvars) fxy tys)
  1.1119 +      | pr_typ tyvars fxy (ITyVar v) =
  1.1120 +          (str o CodeName.lookup_var tyvars) v;
  1.1121 +    fun pr_typscheme_expr tyvars (vs, tycoexpr) =
  1.1122 +      Pretty.block (pr_typparms tyvars vs @@ pr_tycoexpr tyvars NOBR tycoexpr);
  1.1123 +    fun pr_typscheme tyvars (vs, ty) =
  1.1124 +      Pretty.block (pr_typparms tyvars vs @@ pr_typ tyvars NOBR ty);
  1.1125 +    fun pr_term lhs vars fxy (IConst c) =
  1.1126 +          pr_app lhs vars fxy (c, [])
  1.1127 +      | pr_term lhs vars fxy (t as (t1 `$ t2)) =
  1.1128 +          (case CodeThingol.unfold_const_app t
  1.1129 +           of SOME app => pr_app lhs vars fxy app
  1.1130 +            | _ =>
  1.1131 +                brackify fxy [
  1.1132 +                  pr_term lhs vars NOBR t1,
  1.1133 +                  pr_term lhs vars BR t2
  1.1134 +                ])
  1.1135 +      | pr_term lhs vars fxy (IVar v) =
  1.1136 +          (str o CodeName.lookup_var vars) v
  1.1137 +      | pr_term lhs vars fxy (t as _ `|-> _) =
  1.1138 +          let
  1.1139 +            val (binds, t') = CodeThingol.unfold_abs t;
  1.1140 +            fun pr ((v, pat), ty) = pr_bind BR ((SOME v, pat), ty);
  1.1141 +            val (ps, vars') = fold_map pr binds vars;
  1.1142 +          in brackets (str "\\" :: ps @ str "->" @@ pr_term lhs vars' NOBR t') end
  1.1143 +      | pr_term lhs vars fxy (ICase (cases as (_, t0))) = (case CodeThingol.unfold_const_app t0
  1.1144 +           of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
  1.1145 +                then pr_case vars fxy cases
  1.1146 +                else pr_app lhs vars fxy c_ts
  1.1147 +            | NONE => pr_case vars fxy cases)
  1.1148 +    and pr_app' lhs vars ((c, _), ts) =
  1.1149 +      (str o deresolv) c :: map (pr_term lhs vars BR) ts
  1.1150 +    and pr_app lhs vars = gen_pr_app pr_app' pr_term const_syntax labelled_name is_cons lhs vars
  1.1151 +    and pr_bind fxy = pr_bind_haskell (pr_term false) fxy
  1.1152 +    and pr_case vars fxy (cases as ((_, [_]), _)) =
  1.1153 +          let
  1.1154 +            val (binds, t) = CodeThingol.unfold_let (ICase cases);
  1.1155 +            fun pr ((pat, ty), t) vars =
  1.1156 +              vars
  1.1157 +              |> pr_bind BR ((NONE, SOME pat), ty)
  1.1158 +              |>> (fn p => semicolon [p, str "=", pr_term false vars NOBR t])
  1.1159 +            val (ps, vars') = fold_map pr binds vars;
  1.1160 +          in
  1.1161 +            Pretty.block_enclose (
  1.1162 +              str "let {",
  1.1163 +              concat [str "}", str "in", pr_term false vars' NOBR t]
  1.1164 +            ) ps
  1.1165 +          end
  1.1166 +      | pr_case vars fxy (((td, ty), bs as _ :: _), _) =
  1.1167 +          let
  1.1168 +            fun pr (pat, t) =
  1.1169 +              let
  1.1170 +                val (p, vars') = pr_bind NOBR ((NONE, SOME pat), ty) vars;
  1.1171 +              in semicolon [p, str "->", pr_term false vars' NOBR t] end;
  1.1172 +          in
  1.1173 +            Pretty.block_enclose (
  1.1174 +              concat [str "(case", pr_term false vars NOBR td, str "of", str "{"],
  1.1175 +              str "})"
  1.1176 +            ) (map pr bs)
  1.1177 +          end
  1.1178 +      | pr_case vars fxy ((_, []), _) = str "error \"empty case\"";
  1.1179 +    fun pr_def (name, CodeThingol.Fun (eqs, (vs, ty))) =
  1.1180 +          let
  1.1181 +            val tyvars = CodeName.intro_vars (map fst vs) init_syms;
  1.1182 +            fun pr_eq (ts, t) =
  1.1183 +              let
  1.1184 +                val consts = map_filter
  1.1185 +                  (fn c => if (is_some o const_syntax) c
  1.1186 +                    then NONE else (SOME o NameSpace.base o deresolv) c)
  1.1187 +                    ((fold o CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []);
  1.1188 +                val vars = init_syms
  1.1189 +                  |> CodeName.intro_vars consts
  1.1190 +                  |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames)
  1.1191 +                       (insert (op =)) ts []);
  1.1192 +              in
  1.1193 +                semicolon (
  1.1194 +                  (str o deresolv_here) name
  1.1195 +                  :: map (pr_term true vars BR) ts
  1.1196 +                  @ str "="
  1.1197 +                  @@ pr_term false vars NOBR t
  1.1198 +                )
  1.1199 +              end;
  1.1200 +          in
  1.1201 +            Pretty.chunks (
  1.1202 +              Pretty.block [
  1.1203 +                (str o suffix " ::" o deresolv_here) name,
  1.1204 +                Pretty.brk 1,
  1.1205 +                pr_typscheme tyvars (vs, ty),
  1.1206 +                str ";"
  1.1207 +              ]
  1.1208 +              :: map pr_eq eqs
  1.1209 +            )
  1.1210 +          end
  1.1211 +      | pr_def (name, CodeThingol.Datatype (vs, [])) =
  1.1212 +          let
  1.1213 +            val tyvars = CodeName.intro_vars (map fst vs) init_syms;
  1.1214 +          in
  1.1215 +            semicolon [
  1.1216 +              str "data",
  1.1217 +              pr_typscheme_expr tyvars (vs, (deresolv_here name, map (ITyVar o fst) vs))
  1.1218 +            ]
  1.1219 +          end
  1.1220 +      | pr_def (name, CodeThingol.Datatype (vs, [(co, [ty])])) =
  1.1221 +          let
  1.1222 +            val tyvars = CodeName.intro_vars (map fst vs) init_syms;
  1.1223 +          in
  1.1224 +            semicolon (
  1.1225 +              str "newtype"
  1.1226 +              :: pr_typscheme_expr tyvars (vs, (deresolv_here name, map (ITyVar o fst) vs))
  1.1227 +              :: str "="
  1.1228 +              :: (str o deresolv_here) co
  1.1229 +              :: pr_typ tyvars BR ty
  1.1230 +              :: (if deriving_show name then [str "deriving (Read, Show)"] else [])
  1.1231 +            )
  1.1232 +          end
  1.1233 +      | pr_def (name, CodeThingol.Datatype (vs, co :: cos)) =
  1.1234 +          let
  1.1235 +            val tyvars = CodeName.intro_vars (map fst vs) init_syms;
  1.1236 +            fun pr_co (co, tys) =
  1.1237 +              concat (
  1.1238 +                (str o deresolv_here) co
  1.1239 +                :: map (pr_typ tyvars BR) tys
  1.1240 +              )
  1.1241 +          in
  1.1242 +            semicolon (
  1.1243 +              str "data"
  1.1244 +              :: pr_typscheme_expr tyvars (vs, (deresolv_here name, map (ITyVar o fst) vs))
  1.1245 +              :: str "="
  1.1246 +              :: pr_co co
  1.1247 +              :: map ((fn p => Pretty.block [str "| ", p]) o pr_co) cos
  1.1248 +              @ (if deriving_show name then [str "deriving (Read, Show)"] else [])
  1.1249 +            )
  1.1250 +          end
  1.1251 +      | pr_def (name, CodeThingol.Class (superclasss, (v, classops))) =
  1.1252 +          let
  1.1253 +            val tyvars = CodeName.intro_vars [v] init_syms;
  1.1254 +            fun pr_classop (classop, ty) =
  1.1255 +              semicolon [
  1.1256 +                (str o classop_name name) classop,
  1.1257 +                str "::",
  1.1258 +                pr_typ tyvars NOBR ty
  1.1259 +              ]
  1.1260 +          in
  1.1261 +            Pretty.block_enclose (
  1.1262 +              Pretty.block [
  1.1263 +                str "class ",
  1.1264 +                pr_typparms tyvars [(v, map fst superclasss)],
  1.1265 +                str (deresolv_here name ^ " " ^ CodeName.lookup_var tyvars v),
  1.1266 +                str " where {"
  1.1267 +              ],
  1.1268 +              str "};"
  1.1269 +            ) (map pr_classop classops)
  1.1270 +          end
  1.1271 +      | pr_def (_, CodeThingol.Classinst ((class, (tyco, vs)), (_, classop_defs))) =
  1.1272 +          let
  1.1273 +            val tyvars = CodeName.intro_vars (map fst vs) init_syms;
  1.1274 +            fun pr_instdef (classop, t) =
  1.1275 +                let
  1.1276 +                  val consts = map_filter
  1.1277 +                    (fn c => if (is_some o const_syntax) c
  1.1278 +                      then NONE else (SOME o NameSpace.base o deresolv) c)
  1.1279 +                      (CodeThingol.fold_constnames (insert (op =)) t []);
  1.1280 +                  val vars = init_syms
  1.1281 +                    |> CodeName.intro_vars consts;
  1.1282 +                in
  1.1283 +                  semicolon [
  1.1284 +                    (str o classop_name class) classop,
  1.1285 +                    str "=",
  1.1286 +                    pr_term false vars NOBR t
  1.1287 +                  ]
  1.1288 +                end;
  1.1289 +          in
  1.1290 +            Pretty.block_enclose (
  1.1291 +              Pretty.block [
  1.1292 +                str "instance ",
  1.1293 +                pr_typparms tyvars vs,
  1.1294 +                str (class_name class ^ " "),
  1.1295 +                pr_typ tyvars BR (tyco `%% map (ITyVar o fst) vs),
  1.1296 +                str " where {"
  1.1297 +              ],
  1.1298 +              str "};"
  1.1299 +            ) (map pr_instdef classop_defs)
  1.1300 +          end;
  1.1301 +  in pr_def def end;
  1.1302 +
  1.1303 +fun pretty_haskell_monad c_mbind c_kbind =
  1.1304 +  let
  1.1305 +    fun pretty pr vars fxy [(t, _)] =
  1.1306 +      let
  1.1307 +        val pr_bind = pr_bind_haskell pr;
  1.1308 +        fun pr_mbind (NONE, t) vars =
  1.1309 +              (semicolon [pr vars NOBR t], vars)
  1.1310 +          | pr_mbind (SOME (bind, true), t) vars = vars
  1.1311 +              |> pr_bind NOBR bind
  1.1312 +              |>> (fn p => semicolon [p, str "<-", pr vars NOBR t])
  1.1313 +          | pr_mbind (SOME (bind, false), t) vars = vars
  1.1314 +              |> pr_bind NOBR bind
  1.1315 +              |>> (fn p => semicolon [str "let", p, str "=", pr vars NOBR t]);
  1.1316 +        val (binds, t) = implode_monad c_mbind c_kbind t;
  1.1317 +        val (ps, vars') = fold_map pr_mbind binds vars;
  1.1318 +        fun brack p = if eval_fxy BR fxy then Pretty.block [str "(", p, str ")"] else p;
  1.1319 +      in (brack o Pretty.block_enclose (str "do {", str "}")) (ps @| pr vars' NOBR t) end;
  1.1320 +  in (1, pretty) end;
  1.1321 +
  1.1322 +end; (*local*)
  1.1323 +
  1.1324 +fun seri_haskell module_prefix module destination string_classes labelled_name
  1.1325 +    reserved_syms raw_module_alias module_prolog class_syntax tyco_syntax const_syntax code =
  1.1326 +  let
  1.1327 +    val _ = Option.map File.check destination;
  1.1328 +    val is_cons = CodeThingol.is_cons code;
  1.1329 +    val module_alias = if is_some module then K module else raw_module_alias;
  1.1330 +    val init_names = Name.make_context reserved_syms;
  1.1331 +    val name_modl = mk_modl_name_tab init_names module_prefix module_alias code;
  1.1332 +    fun add_def (name, (def, deps)) =
  1.1333 +      let
  1.1334 +        val (modl, base) = dest_name name;
  1.1335 +        fun name_def base = Name.variants [base] #>> the_single;
  1.1336 +        fun add_fun upper (nsp_fun, nsp_typ) =
  1.1337 +          let
  1.1338 +            val (base', nsp_fun') = name_def (if upper then first_upper base else base) nsp_fun
  1.1339 +          in (base', (nsp_fun', nsp_typ)) end;
  1.1340 +        fun add_typ (nsp_fun, nsp_typ) =
  1.1341 +          let
  1.1342 +            val (base', nsp_typ') = name_def (first_upper base) nsp_typ
  1.1343 +          in (base', (nsp_fun, nsp_typ')) end;
  1.1344 +        val add_name =
  1.1345 +          case def
  1.1346 +           of CodeThingol.Bot => pair base
  1.1347 +            | CodeThingol.Fun _ => add_fun false
  1.1348 +            | CodeThingol.Datatype _ => add_typ
  1.1349 +            | CodeThingol.Datatypecons _ => add_fun true
  1.1350 +            | CodeThingol.Class _ => add_typ
  1.1351 +            | CodeThingol.Classrel _ => pair base
  1.1352 +            | CodeThingol.Classop _ => add_fun false
  1.1353 +            | CodeThingol.Classinst _ => pair base;
  1.1354 +        val modlname' = name_modl modl;
  1.1355 +        fun add_def base' =
  1.1356 +          case def
  1.1357 +           of CodeThingol.Bot => I
  1.1358 +            | CodeThingol.Datatypecons _ =>
  1.1359 +                cons (name, ((NameSpace.append modlname' base', base'), NONE))
  1.1360 +            | CodeThingol.Classrel _ => I
  1.1361 +            | CodeThingol.Classop _ =>
  1.1362 +                cons (name, ((NameSpace.append modlname' base', base'), NONE))
  1.1363 +            | _ => cons (name, ((NameSpace.append modlname' base', base'), SOME def));
  1.1364 +      in
  1.1365 +        Symtab.map_default (modlname', ([], ([], (init_names, init_names))))
  1.1366 +              (apfst (fold (insert (op = : string * string -> bool)) deps))
  1.1367 +        #> `(fn code => add_name ((snd o snd o the o Symtab.lookup code) modlname'))
  1.1368 +        #-> (fn (base', names) =>
  1.1369 +              (Symtab.map_entry modlname' o apsnd) (fn (defs, _) =>
  1.1370 +              (add_def base' defs, names)))
  1.1371 +      end;
  1.1372 +    val code' =
  1.1373 +      fold add_def (AList.make (fn name => (Graph.get_node code name, Graph.imm_succs code name))
  1.1374 +        (Graph.strong_conn code |> flat)) Symtab.empty;
  1.1375 +    val init_syms = CodeName.make_vars reserved_syms;
  1.1376 +    fun deresolv name =
  1.1377 +      (fst o fst o the o AList.lookup (op =) ((fst o snd o the
  1.1378 +        o Symtab.lookup code') ((name_modl o fst o dest_name) name))) name
  1.1379 +        handle Option => error ("Unknown definition name: " ^ labelled_name name);
  1.1380 +    fun deresolv_here name =
  1.1381 +      (snd o fst o the o AList.lookup (op =) ((fst o snd o the
  1.1382 +        o Symtab.lookup code') ((name_modl o fst o dest_name) name))) name
  1.1383 +        handle Option => error ("Unknown definition name: " ^ labelled_name name);
  1.1384 +    fun deriving_show tyco =
  1.1385 +      let
  1.1386 +        fun deriv _ "fun" = false
  1.1387 +          | deriv tycos tyco = member (op =) tycos tyco orelse
  1.1388 +              case the_default CodeThingol.Bot (try (Graph.get_node code) tyco)
  1.1389 +               of CodeThingol.Bot => true
  1.1390 +                | CodeThingol.Datatype (_, cs) => forall (deriv' (tyco :: tycos))
  1.1391 +                    (maps snd cs)
  1.1392 +        and deriv' tycos (tyco `%% tys) = deriv tycos tyco
  1.1393 +              andalso forall (deriv' tycos) tys
  1.1394 +          | deriv' _ (ITyVar _) = true
  1.1395 +      in deriv [] tyco end;
  1.1396 +    fun seri_def qualified = pr_haskell class_syntax tyco_syntax const_syntax labelled_name init_syms
  1.1397 +      deresolv_here (if qualified then deresolv else deresolv_here) is_cons
  1.1398 +      (if string_classes then deriving_show else K false);
  1.1399 +    fun write_module (SOME destination) modlname =
  1.1400 +          let
  1.1401 +            val filename = case modlname
  1.1402 +             of "" => Path.explode "Main.hs"
  1.1403 +              | _ => (Path.ext "hs" o Path.explode o implode o separate "/" o NameSpace.explode) modlname;
  1.1404 +            val pathname = Path.append destination filename;
  1.1405 +            val _ = File.mkdir (Path.dir pathname);
  1.1406 +          in File.write pathname end
  1.1407 +      | write_module NONE _ = writeln;
  1.1408 +    fun seri_module (modlname', (imports, (defs, _))) =
  1.1409 +      let
  1.1410 +        val imports' =
  1.1411 +          imports
  1.1412 +          |> map (name_modl o fst o dest_name)
  1.1413 +          |> distinct (op =)
  1.1414 +          |> remove (op =) modlname';
  1.1415 +        val qualified =
  1.1416 +          imports
  1.1417 +          |> map_filter (try deresolv)
  1.1418 +          |> map NameSpace.base
  1.1419 +          |> has_duplicates (op =);
  1.1420 +        val mk_import = str o (if qualified
  1.1421 +          then prefix "import qualified "
  1.1422 +          else prefix "import ") o suffix ";";
  1.1423 +      in
  1.1424 +        Pretty.chunks (
  1.1425 +          str ("module " ^ modlname' ^ " where {")
  1.1426 +          :: str ""
  1.1427 +          :: map mk_import imports'
  1.1428 +          @ str ""
  1.1429 +          :: separate (str "") ((case module_prolog modlname'
  1.1430 +             of SOME prolog => [prolog]
  1.1431 +              | NONE => [])
  1.1432 +          @ map_filter
  1.1433 +            (fn (name, (_, SOME def)) => SOME (seri_def qualified (name, def))
  1.1434 +              | (_, (_, NONE)) => NONE) defs)
  1.1435 +          @ str ""
  1.1436 +          @@ str "}"
  1.1437 +        )
  1.1438 +        |> code_output
  1.1439 +        |> write_module destination modlname'
  1.1440 +      end;
  1.1441 +  in Symtab.fold (fn modl => fn () => seri_module modl) code' () end;
  1.1442 +
  1.1443 +fun isar_seri_haskell module file =
  1.1444 +  let
  1.1445 +    val destination = case file
  1.1446 +     of NONE => error ("Haskell: no internal compilation")
  1.1447 +      | SOME "-" => NONE
  1.1448 +      | SOME file => SOME (Path.explode file)
  1.1449 +  in
  1.1450 +    parse_args (Scan.option (Args.$$$ "root" -- Args.colon |-- Args.name)
  1.1451 +      -- Scan.optional (Args.$$$ "string_classes" >> K true) false
  1.1452 +      >> (fn (module_prefix, string_classes) =>
  1.1453 +        seri_haskell module_prefix module destination string_classes))
  1.1454 +  end;
  1.1455 +
  1.1456 +
  1.1457 +(** diagnosis serializer **)
  1.1458 +
  1.1459 +fun seri_diagnosis labelled_name _ _ _ _ _ _ code =
  1.1460 +  let
  1.1461 +    val init_names = CodeName.make_vars [];
  1.1462 +    fun pr_fun "fun" = SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
  1.1463 +          brackify_infix (1, R) fxy [
  1.1464 +            pr_typ (INFX (1, X)) ty1,
  1.1465 +            str "->",
  1.1466 +            pr_typ (INFX (1, R)) ty2
  1.1467 +          ])
  1.1468 +      | pr_fun _ = NONE
  1.1469 +    val pr = pr_haskell (K NONE) pr_fun (K NONE) labelled_name init_names I I (K false) (K false);
  1.1470 +  in
  1.1471 +    []
  1.1472 +    |> Graph.fold (fn (name, (def, _)) => case try pr (name, def) of SOME p => cons p | NONE => I) code
  1.1473 +    |> Pretty.chunks2
  1.1474 +    |> code_output
  1.1475 +    |> writeln
  1.1476 +  end;
  1.1477 +
  1.1478 +
  1.1479 +
  1.1480 +(** theory data **)
  1.1481 +
  1.1482 +datatype syntax_expr = SyntaxExpr of {
  1.1483 +  class: (string * (string -> string option)) Symtab.table,
  1.1484 +  inst: unit Symtab.table,
  1.1485 +  tyco: typ_syntax Symtab.table,
  1.1486 +  const: term_syntax Symtab.table
  1.1487 +};
  1.1488 +
  1.1489 +fun mk_syntax_expr ((class, inst), (tyco, const)) =
  1.1490 +  SyntaxExpr { class = class, inst = inst, tyco = tyco, const = const };
  1.1491 +fun map_syntax_expr f (SyntaxExpr { class, inst, tyco, const }) =
  1.1492 +  mk_syntax_expr (f ((class, inst), (tyco, const)));
  1.1493 +fun merge_syntax_expr (SyntaxExpr { class = class1, inst = inst1, tyco = tyco1, const = const1 },
  1.1494 +    SyntaxExpr { class = class2, inst = inst2, tyco = tyco2, const = const2 }) =
  1.1495 +  mk_syntax_expr (
  1.1496 +    (Symtab.join (K snd) (class1, class2),
  1.1497 +       Symtab.join (K snd) (inst1, inst2)),
  1.1498 +    (Symtab.join (K snd) (tyco1, tyco2),
  1.1499 +       Symtab.join (K snd) (const1, const2))
  1.1500 +  );
  1.1501 +
  1.1502 +datatype syntax_modl = SyntaxModl of {
  1.1503 +  alias: string Symtab.table,
  1.1504 +  prolog: Pretty.T Symtab.table
  1.1505 +};
  1.1506 +
  1.1507 +fun mk_syntax_modl (alias, prolog) =
  1.1508 +  SyntaxModl { alias = alias, prolog = prolog };
  1.1509 +fun map_syntax_modl f (SyntaxModl { alias, prolog }) =
  1.1510 +  mk_syntax_modl (f (alias, prolog));
  1.1511 +fun merge_syntax_modl (SyntaxModl { alias = alias1, prolog = prolog1 },
  1.1512 +    SyntaxModl { alias = alias2, prolog = prolog2 }) =
  1.1513 +  mk_syntax_modl (
  1.1514 +    Symtab.join (K snd) (alias1, alias2),
  1.1515 +    Symtab.join (K snd) (prolog1, prolog2)
  1.1516 +  );
  1.1517 +
  1.1518 +type serializer =
  1.1519 +  string option
  1.1520 +  -> string option
  1.1521 +  -> Args.T list
  1.1522 +  -> (string -> string)
  1.1523 +  -> string list
  1.1524 +  -> (string -> string option)
  1.1525 +  -> (string -> Pretty.T option)
  1.1526 +  -> (string -> class_syntax option)
  1.1527 +  -> (string -> typ_syntax option)
  1.1528 +  -> (string -> term_syntax option)
  1.1529 +  -> CodeThingol.code -> unit;
  1.1530 +
  1.1531 +datatype target = Target of {
  1.1532 +  serial: serial,
  1.1533 +  serializer: serializer,
  1.1534 +  syntax_expr: syntax_expr,
  1.1535 +  syntax_modl: syntax_modl,
  1.1536 +  reserved: string list
  1.1537 +};
  1.1538 +
  1.1539 +fun mk_target (serial, ((serializer, reserved), (syntax_expr, syntax_modl))) =
  1.1540 +  Target { serial = serial, reserved = reserved, serializer = serializer, syntax_expr = syntax_expr, syntax_modl = syntax_modl };
  1.1541 +fun map_target f ( Target { serial, serializer, reserved, syntax_expr, syntax_modl } ) =
  1.1542 +  mk_target (f (serial, ((serializer, reserved), (syntax_expr, syntax_modl))));
  1.1543 +fun merge_target target (Target { serial = serial1, serializer = serializer, reserved = reserved1,
  1.1544 +  syntax_expr = syntax_expr1, syntax_modl = syntax_modl1 },
  1.1545 +    Target { serial = serial2, serializer = _, reserved = reserved2,
  1.1546 +      syntax_expr = syntax_expr2, syntax_modl = syntax_modl2 }) =
  1.1547 +  if serial1 = serial2 then
  1.1548 +    mk_target (serial1, ((serializer, merge (op =) (reserved1, reserved2)),
  1.1549 +      (merge_syntax_expr (syntax_expr1, syntax_expr2),
  1.1550 +        merge_syntax_modl (syntax_modl1, syntax_modl2))
  1.1551 +    ))
  1.1552 +  else
  1.1553 +    error ("Incompatible serializers: " ^ quote target);
  1.1554 +
  1.1555 +structure CodeTargetData = TheoryDataFun
  1.1556 +(
  1.1557 +  type T = target Symtab.table;
  1.1558 +  val empty = Symtab.empty;
  1.1559 +  val copy = I;
  1.1560 +  val extend = I;
  1.1561 +  fun merge _ = Symtab.join merge_target;
  1.1562 +);
  1.1563 +
  1.1564 +fun the_serializer (Target { serializer, ... }) = serializer;
  1.1565 +fun the_reserved (Target { reserved, ... }) = reserved;
  1.1566 +fun the_syntax_expr (Target { syntax_expr = SyntaxExpr x, ... }) = x;
  1.1567 +fun the_syntax_modl (Target { syntax_modl = SyntaxModl x, ... }) = x;
  1.1568 +
  1.1569 +fun assert_serializer thy target =
  1.1570 +  case Symtab.lookup (CodeTargetData.get thy) target
  1.1571 +   of SOME data => target
  1.1572 +    | NONE => error ("Unknown code target language: " ^ quote target);
  1.1573 +
  1.1574 +fun add_serializer (target, seri) thy =
  1.1575 +  let
  1.1576 +    val _ = case Symtab.lookup (CodeTargetData.get thy) target
  1.1577 +     of SOME _ => warning ("overwriting existing serializer " ^ quote target)
  1.1578 +      | NONE => ();
  1.1579 +  in
  1.1580 +    thy
  1.1581 +    |> (CodeTargetData.map oo Symtab.map_default)
  1.1582 +          (target, mk_target (serial (), ((seri, []),
  1.1583 +            (mk_syntax_expr ((Symtab.empty, Symtab.empty), (Symtab.empty, Symtab.empty)),
  1.1584 +              mk_syntax_modl (Symtab.empty, Symtab.empty)))))
  1.1585 +          (map_target (fn (serial, ((_, keywords), syntax)) => (serial, ((seri, keywords), syntax))))
  1.1586 +  end;
  1.1587 +
  1.1588 +fun map_seri_data target f thy =
  1.1589 +  let
  1.1590 +    val _ = assert_serializer thy target;
  1.1591 +  in
  1.1592 +    thy
  1.1593 +    |> (CodeTargetData.map o Symtab.map_entry target o map_target) f
  1.1594 +  end;
  1.1595 +
  1.1596 +val target_SML = "SML";
  1.1597 +val target_OCaml = "OCaml";
  1.1598 +val target_Haskell = "Haskell";
  1.1599 +val target_diag = "diag";
  1.1600 +
  1.1601 +fun get_serializer thy target permissive module file args labelled_name = fn cs =>
  1.1602 +  let
  1.1603 +    val data = case Symtab.lookup (CodeTargetData.get thy) target
  1.1604 +     of SOME data => data
  1.1605 +      | NONE => error ("Unknown code target language: " ^ quote target);
  1.1606 +    val seri = the_serializer data;
  1.1607 +    val reserved = the_reserved data;
  1.1608 +    val { alias, prolog } = the_syntax_modl data;
  1.1609 +    val { class, inst, tyco, const } = the_syntax_expr data;
  1.1610 +    val project = if target = target_diag then I
  1.1611 +      else CodeThingol.project_code permissive
  1.1612 +        (Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const) cs;
  1.1613 +    fun check_empty_funs code = case CodeThingol.empty_funs code
  1.1614 +     of [] => code
  1.1615 +      | names => error ("No defining equations for " ^ commas (map (labelled_name thy) names));
  1.1616 +  in
  1.1617 +    project
  1.1618 +    #> check_empty_funs
  1.1619 +    #> seri module file args (labelled_name thy) reserved (Symtab.lookup alias) (Symtab.lookup prolog)
  1.1620 +      (Symtab.lookup class) (Symtab.lookup tyco) (Symtab.lookup const)
  1.1621 +  end;
  1.1622 +
  1.1623 +fun eval_term thy labelled_name code ((ref_name, reff), t) args =
  1.1624 +  let
  1.1625 +    val val_name = "Isabelle_Eval.EVAL.EVAL";
  1.1626 +    val val_name' = "Isabelle_Eval.EVAL";
  1.1627 +    val val_name'_args = space_implode " " (val_name' :: map (enclose "(" ")") args);
  1.1628 +    val seri = get_serializer thy "SML" false (SOME "Isabelle_Eval") NONE [] labelled_name;
  1.1629 +    fun eval code = (
  1.1630 +      reff := NONE;
  1.1631 +      seri (SOME [val_name]) code;
  1.1632 +      use_text "generated code for evaluation" Output.ml_output (!eval_verbose)
  1.1633 +        ("val _ = (" ^ ref_name ^ " := SOME (" ^ val_name'_args ^ "))");
  1.1634 +      case !reff
  1.1635 +       of NONE => error ("Could not retrieve value of ML reference " ^ quote ref_name
  1.1636 +            ^ " (reference probably has been shadowed)")
  1.1637 +        | SOME value => value
  1.1638 +      );
  1.1639 +  in
  1.1640 +    code
  1.1641 +    |> CodeThingol.add_eval_def (val_name, t)
  1.1642 +    |> eval
  1.1643 +  end;
  1.1644 +
  1.1645 +
  1.1646 +
  1.1647 +(** optional pretty serialization **)
  1.1648 +
  1.1649 +local
  1.1650 +
  1.1651 +val pretty : (string * {
  1.1652 +    pretty_char: string -> string,
  1.1653 +    pretty_string: string -> string,
  1.1654 +    pretty_numeral: bool -> IntInf.int -> string,
  1.1655 +    pretty_list: Pretty.T list -> Pretty.T,
  1.1656 +    infix_cons: int * string
  1.1657 +  }) list = [
  1.1658 +  ("SML", { pretty_char = prefix "#" o quote o ML_Syntax.print_char,
  1.1659 +      pretty_string = ML_Syntax.print_string,
  1.1660 +      pretty_numeral = fn unbounded => fn k =>
  1.1661 +        if unbounded then "(" ^ IntInf.toString k ^ " : IntInf.int)"
  1.1662 +        else IntInf.toString k,
  1.1663 +      pretty_list = Pretty.enum "," "[" "]",
  1.1664 +      infix_cons = (7, "::")}),
  1.1665 +  ("OCaml", { pretty_char = fn c => enclose "'" "'"
  1.1666 +        (let val i = ord c
  1.1667 +          in if i < 32 orelse i = 39 orelse i = 92
  1.1668 +            then prefix "\\" (string_of_int i)
  1.1669 +            else c
  1.1670 +          end),
  1.1671 +      pretty_string = (fn _ => error "OCaml: no pretty strings"),
  1.1672 +      pretty_numeral = fn unbounded => fn k => if k >= IntInf.fromInt 0 then
  1.1673 +            if unbounded then
  1.1674 +              "(Big_int.big_int_of_int " ^ IntInf.toString k ^ ")"
  1.1675 +            else IntInf.toString k
  1.1676 +          else
  1.1677 +            if unbounded then
  1.1678 +              "(Big_int.big_int_of_int " ^ (enclose "(" ")" o prefix "-"
  1.1679 +                o IntInf.toString o op ~) k ^ ")"
  1.1680 +            else (enclose "(" ")" o prefix "-" o IntInf.toString o op ~) k,
  1.1681 +      pretty_list = Pretty.enum ";" "[" "]",
  1.1682 +      infix_cons = (6, "::")}),
  1.1683 +  ("Haskell", { pretty_char = fn c => enclose "'" "'"
  1.1684 +        (let val i = ord c
  1.1685 +          in if i < 32 orelse i = 39 orelse i = 92
  1.1686 +            then Library.prefix "\\" (string_of_int i)
  1.1687 +            else c
  1.1688 +          end),
  1.1689 +      pretty_string = ML_Syntax.print_string,
  1.1690 +      pretty_numeral = fn unbounded => fn k => if k >= IntInf.fromInt 0 then
  1.1691 +            IntInf.toString k
  1.1692 +          else
  1.1693 +            (enclose "(" ")" o Library.prefix "-" o IntInf.toString o IntInf.~) k,
  1.1694 +      pretty_list = Pretty.enum "," "[" "]",
  1.1695 +      infix_cons = (5, ":")})
  1.1696 +];
  1.1697 +
  1.1698 +in
  1.1699 +
  1.1700 +fun pr_pretty target = case AList.lookup (op =) pretty target
  1.1701 + of SOME x => x
  1.1702 +  | NONE => error ("Unknown code target language: " ^ quote target);
  1.1703 +
  1.1704 +fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
  1.1705 +  brackify_infix (target_fxy, R) fxy [
  1.1706 +    pr (INFX (target_fxy, X)) t1,
  1.1707 +    str target_cons,
  1.1708 +    pr (INFX (target_fxy, R)) t2
  1.1709 +  ];
  1.1710 +
  1.1711 +fun pretty_list c_nil c_cons target =
  1.1712 +  let
  1.1713 +    val pretty_ops = pr_pretty target;
  1.1714 +    val mk_list = #pretty_list pretty_ops;
  1.1715 +    fun pretty pr vars fxy [(t1, _), (t2, _)] =
  1.1716 +      case Option.map (cons t1) (implode_list c_nil c_cons t2)
  1.1717 +       of SOME ts => mk_list (map (pr vars NOBR) ts)
  1.1718 +        | NONE => default_list (#infix_cons pretty_ops) (pr vars) fxy t1 t2;
  1.1719 +  in (2, pretty) end;
  1.1720 +
  1.1721 +fun pretty_list_string c_nil c_cons c_char c_nibbles target =
  1.1722 +  let
  1.1723 +    val pretty_ops = pr_pretty target;
  1.1724 +    val mk_list = #pretty_list pretty_ops;
  1.1725 +    val mk_char = #pretty_char pretty_ops;
  1.1726 +    val mk_string = #pretty_string pretty_ops;
  1.1727 +    fun pretty pr vars fxy [(t1, _), (t2, _)] =
  1.1728 +      case Option.map (cons t1) (implode_list c_nil c_cons t2)
  1.1729 +       of SOME ts => case implode_string c_char c_nibbles mk_char mk_string ts
  1.1730 +           of SOME p => p
  1.1731 +            | NONE => mk_list (map (pr vars NOBR) ts)
  1.1732 +        | NONE => default_list (#infix_cons pretty_ops) (pr vars) fxy t1 t2;
  1.1733 +  in (2, pretty) end;
  1.1734 +
  1.1735 +fun pretty_char c_char c_nibbles target =
  1.1736 +  let
  1.1737 +    val mk_char = #pretty_char (pr_pretty target);
  1.1738 +    fun pretty _ _ _ [(t1, _), (t2, _)] =
  1.1739 +      case decode_char c_nibbles (t1, t2)
  1.1740 +       of SOME c => (str o mk_char) c
  1.1741 +        | NONE => error "Illegal character expression";
  1.1742 +  in (2, pretty) end;
  1.1743 +
  1.1744 +fun pretty_numeral unbounded c_bit0 c_bit1 c_pls c_min c_bit target =
  1.1745 +  let
  1.1746 +    val mk_numeral = #pretty_numeral (pr_pretty target);
  1.1747 +    fun pretty _ _ _ [(t, _)] =
  1.1748 +      case implode_numeral c_bit0 c_bit1 c_pls c_min c_bit t
  1.1749 +       of SOME k => (str o mk_numeral unbounded) k
  1.1750 +        | NONE => error "Illegal numeral expression";
  1.1751 +  in (1, pretty) end;
  1.1752 +
  1.1753 +fun pretty_ml_string c_char c_nibbles c_nil c_cons target =
  1.1754 +  let
  1.1755 +    val pretty_ops = pr_pretty target;
  1.1756 +    val mk_char = #pretty_char pretty_ops;
  1.1757 +    val mk_string = #pretty_string pretty_ops;
  1.1758 +    fun pretty pr vars fxy [(t, _)] =
  1.1759 +      case implode_list c_nil c_cons t
  1.1760 +       of SOME ts => (case implode_string c_char c_nibbles mk_char mk_string ts
  1.1761 +           of SOME p => p
  1.1762 +            | NONE => error "Illegal ml_string expression")
  1.1763 +        | NONE => error "Illegal ml_string expression";
  1.1764 +  in (1, pretty) end;
  1.1765 +
  1.1766 +val pretty_imperative_monad_bind =
  1.1767 +  let
  1.1768 +    fun pretty (pr : CodeName.var_ctxt -> fixity -> iterm -> Pretty.T)
  1.1769 +          vars fxy [(t1, _), ((v, ty) `|-> t2, _)] =
  1.1770 +            pr vars fxy (ICase (((t1, ty), ([(IVar v, t2)])), IVar ""))
  1.1771 +      | pretty pr vars fxy [(t1, _), (t2, ty2)] =
  1.1772 +          let
  1.1773 +            (*this code suffers from the lack of a proper concept for bindings*)
  1.1774 +            val vs = CodeThingol.fold_varnames cons t2 [];
  1.1775 +            val v = Name.variant vs "x";
  1.1776 +            val vars' = CodeName.intro_vars [v] vars;
  1.1777 +            val var = IVar v;
  1.1778 +            val ty = (hd o fst o CodeThingol.unfold_fun) ty2;
  1.1779 +          in pr vars' fxy (ICase (((t1, ty), ([(var, t2 `$ var)])), IVar "")) end;
  1.1780 +  in (2, pretty) end;
  1.1781 +
  1.1782 +end; (*local*)
  1.1783 +
  1.1784 +(** ML and Isar interface **)
  1.1785 +
  1.1786 +local
  1.1787 +
  1.1788 +fun map_syntax_exprs target =
  1.1789 +  map_seri_data target o apsnd o apsnd o apfst o map_syntax_expr;
  1.1790 +fun map_syntax_modls target =
  1.1791 +  map_seri_data target o apsnd o apsnd o apsnd o map_syntax_modl;
  1.1792 +fun map_reserveds target =
  1.1793 +  map_seri_data target o apsnd o apfst o apsnd;
  1.1794 +
  1.1795 +fun gen_add_syntax_class prep_class prep_const target raw_class raw_syn thy =
  1.1796 +  let
  1.1797 +    val cls = prep_class thy raw_class;
  1.1798 +    val class = CodeName.class thy cls;
  1.1799 +    fun mk_classop (const as (c, _)) = case AxClass.class_of_param thy c
  1.1800 +     of SOME class' => if cls = class' then CodeName.const thy const
  1.1801 +          else error ("Not a class operation for class " ^ quote class ^ ": " ^ quote c)
  1.1802 +      | NONE => error ("Not a class operation: " ^ quote c);
  1.1803 +    fun mk_syntax_ops raw_ops = AList.lookup (op =)
  1.1804 +      ((map o apfst) (mk_classop o prep_const thy) raw_ops);
  1.1805 +  in case raw_syn
  1.1806 +   of SOME (syntax, raw_ops) =>
  1.1807 +      thy
  1.1808 +      |> (map_syntax_exprs target o apfst o apfst)
  1.1809 +           (Symtab.update (class, (syntax, mk_syntax_ops raw_ops)))
  1.1810 +    | NONE =>
  1.1811 +      thy
  1.1812 +      |> (map_syntax_exprs target o apfst o apfst)
  1.1813 +           (Symtab.delete_safe class)
  1.1814 +  end;
  1.1815 +
  1.1816 +fun gen_add_syntax_inst prep_class prep_tyco target (raw_tyco, raw_class) add_del thy =
  1.1817 +  let
  1.1818 +    val inst = CodeName.instance thy (prep_class thy raw_class, prep_tyco thy raw_tyco);
  1.1819 +  in if add_del then
  1.1820 +    thy
  1.1821 +    |> (map_syntax_exprs target o apfst o apsnd)
  1.1822 +        (Symtab.update (inst, ()))
  1.1823 +  else
  1.1824 +    thy
  1.1825 +    |> (map_syntax_exprs target o apfst o apsnd)
  1.1826 +        (Symtab.delete_safe inst)
  1.1827 +  end;
  1.1828 +
  1.1829 +fun gen_add_syntax_tyco prep_tyco target raw_tyco raw_syn thy =
  1.1830 +  let
  1.1831 +    val tyco = prep_tyco thy raw_tyco;
  1.1832 +    val tyco' = if tyco = "fun" then "fun" else CodeName.tyco thy tyco;
  1.1833 +    fun check_args (syntax as (n, _)) = if n <> Sign.arity_number thy tyco
  1.1834 +      then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco)
  1.1835 +      else syntax
  1.1836 +  in case raw_syn
  1.1837 +   of SOME syntax =>
  1.1838 +      thy
  1.1839 +      |> (map_syntax_exprs target o apsnd o apfst)
  1.1840 +           (Symtab.update (tyco', check_args syntax))
  1.1841 +   | NONE =>
  1.1842 +      thy
  1.1843 +      |> (map_syntax_exprs target o apsnd o apfst)
  1.1844 +           (Symtab.delete_safe tyco')
  1.1845 +  end;
  1.1846 +
  1.1847 +fun gen_add_syntax_const prep_const target raw_c raw_syn thy =
  1.1848 +  let
  1.1849 +    val c = prep_const thy raw_c;
  1.1850 +    val c' = CodeName.const thy c;
  1.1851 +    fun check_args (syntax as (n, _)) = if n > (length o fst o strip_type o Sign.the_const_type thy o fst) c
  1.1852 +      then error ("Too many arguments in syntax for constant " ^ (quote o fst) c)
  1.1853 +      else syntax;
  1.1854 +  in case raw_syn
  1.1855 +   of SOME syntax =>
  1.1856 +      thy
  1.1857 +      |> (map_syntax_exprs target o apsnd o apsnd)
  1.1858 +           (Symtab.update (c', check_args syntax))
  1.1859 +   | NONE =>
  1.1860 +      thy
  1.1861 +      |> (map_syntax_exprs target o apsnd o apsnd)
  1.1862 +           (Symtab.delete_safe c')
  1.1863 +  end;
  1.1864 +
  1.1865 +fun cert_class thy class =
  1.1866 +  let
  1.1867 +    val _ = AxClass.get_definition thy class;
  1.1868 +  in class end;
  1.1869 +
  1.1870 +fun read_class thy raw_class =
  1.1871 +  let
  1.1872 +    val class = Sign.intern_class thy raw_class;
  1.1873 +    val _ = AxClass.get_definition thy class;
  1.1874 +  in class end;
  1.1875 +
  1.1876 +fun cert_tyco thy tyco =
  1.1877 +  let
  1.1878 +    val _ = if Sign.declared_tyname thy tyco then ()
  1.1879 +      else error ("No such type constructor: " ^ quote tyco);
  1.1880 +  in tyco end;
  1.1881 +
  1.1882 +fun read_tyco thy raw_tyco =
  1.1883 +  let
  1.1884 +    val tyco = Sign.intern_type thy raw_tyco;
  1.1885 +    val _ = if Sign.declared_tyname thy tyco then ()
  1.1886 +      else error ("No such type constructor: " ^ quote raw_tyco);
  1.1887 +  in tyco end;
  1.1888 +
  1.1889 +fun idfs_of_const thy c =
  1.1890 +  let
  1.1891 +    val c' = (c, Sign.the_const_type thy c);
  1.1892 +    val c'' = CodeUnit.const_of_cexpr thy c';
  1.1893 +  in (c'', CodeName.const thy c'') end;
  1.1894 +
  1.1895 +fun no_bindings x = (Option.map o apsnd)
  1.1896 +  (fn pretty => fn pr => fn vars => pretty (pr vars)) x;
  1.1897 +
  1.1898 +fun gen_add_haskell_monad prep_const c_run c_mbind c_kbind thy =
  1.1899 +  let
  1.1900 +    val c_run' = prep_const thy c_run;
  1.1901 +    val c_mbind' = prep_const thy c_mbind;
  1.1902 +    val c_mbind'' = CodeName.const thy c_mbind';
  1.1903 +    val c_kbind' = prep_const thy c_kbind;
  1.1904 +    val c_kbind'' = CodeName.const thy c_kbind';
  1.1905 +    val pr = pretty_haskell_monad c_mbind'' c_kbind''
  1.1906 +  in
  1.1907 +    thy
  1.1908 +    |> gen_add_syntax_const (K I) target_Haskell c_run' (SOME pr)
  1.1909 +    |> gen_add_syntax_const (K I) target_Haskell c_mbind'
  1.1910 +          (no_bindings (SOME (parse_infix fst (L, 1) ">>=")))
  1.1911 +    |> gen_add_syntax_const (K I) target_Haskell c_kbind'
  1.1912 +          (no_bindings (SOME (parse_infix fst (L, 1) ">>")))
  1.1913 +  end;
  1.1914 +
  1.1915 +fun add_reserved target =
  1.1916 +  let
  1.1917 +    fun add sym syms = if member (op =) syms sym
  1.1918 +      then error ("Reserved symbol " ^ quote sym ^ " already declared")
  1.1919 +      else insert (op =) sym syms
  1.1920 +  in map_reserveds target o add end;
  1.1921 +
  1.1922 +fun add_modl_alias target =
  1.1923 +  map_syntax_modls target o apfst o Symtab.update o apsnd CodeName.check_modulename;
  1.1924 +
  1.1925 +fun add_modl_prolog target =
  1.1926 +  map_syntax_modls target o apsnd o
  1.1927 +    (fn (modl, NONE) => Symtab.delete modl | (modl, SOME prolog) =>
  1.1928 +      Symtab.update (modl, Pretty.str prolog));
  1.1929 +
  1.1930 +fun zip_list (x::xs) f g =
  1.1931 +  f
  1.1932 +  #-> (fn y =>
  1.1933 +    fold_map (fn x => g |-- f >> pair x) xs
  1.1934 +    #-> (fn xys => pair ((x, y) :: xys)));
  1.1935 +
  1.1936 +structure P = OuterParse
  1.1937 +and K = OuterKeyword
  1.1938 +
  1.1939 +fun parse_multi_syntax parse_thing parse_syntax =
  1.1940 +  P.and_list1 parse_thing
  1.1941 +  #-> (fn things => Scan.repeat1 (P.$$$ "(" |-- P.name --
  1.1942 +        (zip_list things parse_syntax (P.$$$ "and")) --| P.$$$ ")"));
  1.1943 +
  1.1944 +val (infixK, infixlK, infixrK) = ("infix", "infixl", "infixr");
  1.1945 +
  1.1946 +fun parse_syntax prep_arg xs =
  1.1947 +  Scan.option ((
  1.1948 +      ((P.$$$ infixK  >> K X)
  1.1949 +        || (P.$$$ infixlK >> K L)
  1.1950 +        || (P.$$$ infixrK >> K R))
  1.1951 +        -- P.nat >> parse_infix prep_arg
  1.1952 +      || Scan.succeed (parse_mixfix prep_arg))
  1.1953 +      -- P.string
  1.1954 +      >> (fn (parse, s) => parse s)) xs;
  1.1955 +
  1.1956 +val (code_classK, code_instanceK, code_typeK, code_constK, code_monadK,
  1.1957 +  code_reservedK, code_modulenameK, code_moduleprologK) =
  1.1958 +  ("code_class", "code_instance", "code_type", "code_const", "code_monad",
  1.1959 +    "code_reserved", "code_modulename", "code_moduleprolog");
  1.1960 +
  1.1961 +in
  1.1962 +
  1.1963 +val parse_syntax = parse_syntax;
  1.1964 +
  1.1965 +val add_syntax_class = gen_add_syntax_class cert_class (K I);
  1.1966 +val add_syntax_inst = gen_add_syntax_inst cert_class cert_tyco;
  1.1967 +val add_syntax_tyco = gen_add_syntax_tyco cert_tyco;
  1.1968 +val add_syntax_const = gen_add_syntax_const (K I);
  1.1969 +
  1.1970 +val add_syntax_class_cmd = gen_add_syntax_class read_class CodeUnit.read_const;
  1.1971 +val add_syntax_inst_cmd = gen_add_syntax_inst read_class read_tyco;
  1.1972 +val add_syntax_tyco_cmd = gen_add_syntax_tyco read_tyco;
  1.1973 +val add_syntax_const_cmd = gen_add_syntax_const CodeUnit.read_const;
  1.1974 +
  1.1975 +fun add_syntax_tycoP target tyco = parse_syntax I >> add_syntax_tyco_cmd target tyco;
  1.1976 +fun add_syntax_constP target c = parse_syntax fst >> (add_syntax_const_cmd target c o no_bindings);
  1.1977 +
  1.1978 +fun add_undefined target undef target_undefined thy =
  1.1979 +  let
  1.1980 +    val (undef', _) = idfs_of_const thy undef;
  1.1981 +    fun pr _ _ _ _ = str target_undefined;
  1.1982 +  in
  1.1983 +    thy
  1.1984 +    |> add_syntax_const target undef' (SOME (~1, pr))
  1.1985 +  end;
  1.1986 +
  1.1987 +fun add_pretty_list target nill cons thy =
  1.1988 +  let
  1.1989 +    val (_, nil'') = idfs_of_const thy nill;
  1.1990 +    val (cons', cons'') = idfs_of_const thy cons;
  1.1991 +    val pr = pretty_list nil'' cons'' target;
  1.1992 +  in
  1.1993 +    thy
  1.1994 +    |> add_syntax_const target cons' (SOME pr)
  1.1995 +  end;
  1.1996 +
  1.1997 +fun add_pretty_list_string target nill cons charr nibbles thy =
  1.1998 +  let
  1.1999 +    val (_, nil'') = idfs_of_const thy nill;
  1.2000 +    val (cons', cons'') = idfs_of_const thy cons;
  1.2001 +    val (_, charr'') = idfs_of_const thy charr;
  1.2002 +    val (_, nibbles'') = split_list (map (idfs_of_const thy) nibbles);
  1.2003 +    val pr = pretty_list_string nil'' cons'' charr'' nibbles'' target;
  1.2004 +  in
  1.2005 +    thy
  1.2006 +    |> add_syntax_const target cons' (SOME pr)
  1.2007 +  end;
  1.2008 +
  1.2009 +fun add_pretty_char target charr nibbles thy =
  1.2010 +  let
  1.2011 +    val (charr', charr'') = idfs_of_const thy charr;
  1.2012 +    val (_, nibbles'') = split_list (map (idfs_of_const thy) nibbles);
  1.2013 +    val pr = pretty_char charr'' nibbles'' target;
  1.2014 +  in
  1.2015 +    thy
  1.2016 +    |> add_syntax_const target charr' (SOME pr)
  1.2017 +  end;
  1.2018 +
  1.2019 +fun add_pretty_numeral target unbounded number_of b0 b1 pls min bit thy =
  1.2020 +  let
  1.2021 +    val number_of' = CodeUnit.const_of_cexpr thy number_of;
  1.2022 +    val (_, b0'') = idfs_of_const thy b0;
  1.2023 +    val (_, b1'') = idfs_of_const thy b1;
  1.2024 +    val (_, pls'') = idfs_of_const thy pls;
  1.2025 +    val (_, min'') = idfs_of_const thy min;
  1.2026 +    val (_, bit'') = idfs_of_const thy bit;
  1.2027 +    val pr = pretty_numeral unbounded b0'' b1'' pls'' min'' bit'' target;
  1.2028 +  in
  1.2029 +    thy
  1.2030 +    |> add_syntax_const target number_of' (SOME pr)
  1.2031 +  end;
  1.2032 +
  1.2033 +fun add_pretty_ml_string target charr nibbles nill cons str thy =
  1.2034 +  let
  1.2035 +    val (_, charr'') = idfs_of_const thy charr;
  1.2036 +    val (_, nibbles'') = split_list (map (idfs_of_const thy) nibbles);
  1.2037 +    val (_, nil'') = idfs_of_const thy nill;
  1.2038 +    val (_, cons'') = idfs_of_const thy cons;
  1.2039 +    val (str', _) = idfs_of_const thy str;
  1.2040 +    val pr = pretty_ml_string charr'' nibbles'' nil'' cons'' target;
  1.2041 +  in
  1.2042 +    thy
  1.2043 +    |> add_syntax_const target str' (SOME pr)
  1.2044 +  end;
  1.2045 +
  1.2046 +fun add_pretty_imperative_monad_bind target bind thy =
  1.2047 +  let
  1.2048 +    val (bind', _) = idfs_of_const thy bind;
  1.2049 +    val pr = pretty_imperative_monad_bind
  1.2050 +  in
  1.2051 +    thy
  1.2052 +    |> add_syntax_const target bind' (SOME pr)
  1.2053 +  end;
  1.2054 +
  1.2055 +val add_haskell_monad = gen_add_haskell_monad CodeUnit.read_const;
  1.2056 +
  1.2057 +val code_classP =
  1.2058 +  OuterSyntax.command code_classK "define code syntax for class" K.thy_decl (
  1.2059 +    parse_multi_syntax P.xname
  1.2060 +      (Scan.option (P.string -- Scan.optional (P.$$$ "where" |-- Scan.repeat1
  1.2061 +        (P.term --| (P.$$$ "\\<equiv>" || P.$$$ "==") -- P.string)) []))
  1.2062 +    >> (Toplevel.theory oo fold) (fn (target, syns) =>
  1.2063 +          fold (fn (raw_class, syn) => add_syntax_class_cmd target raw_class syn) syns)
  1.2064 +  );
  1.2065 +
  1.2066 +val code_instanceP =
  1.2067 +  OuterSyntax.command code_instanceK "define code syntax for instance" K.thy_decl (
  1.2068 +    parse_multi_syntax (P.xname --| P.$$$ "::" -- P.xname)
  1.2069 +      ((P.minus >> K true) || Scan.succeed false)
  1.2070 +    >> (Toplevel.theory oo fold) (fn (target, syns) =>
  1.2071 +          fold (fn (raw_inst, add_del) => add_syntax_inst_cmd target raw_inst add_del) syns)
  1.2072 +  );
  1.2073 +
  1.2074 +val code_typeP =
  1.2075 +  OuterSyntax.command code_typeK "define code syntax for type constructor" K.thy_decl (
  1.2076 +    parse_multi_syntax P.xname (parse_syntax I)
  1.2077 +    >> (Toplevel.theory oo fold) (fn (target, syns) =>
  1.2078 +          fold (fn (raw_tyco, syn) => add_syntax_tyco_cmd target raw_tyco syn) syns)
  1.2079 +  );
  1.2080 +
  1.2081 +val code_constP =
  1.2082 +  OuterSyntax.command code_constK "define code syntax for constant" K.thy_decl (
  1.2083 +    parse_multi_syntax P.term (parse_syntax fst)
  1.2084 +    >> (Toplevel.theory oo fold) (fn (target, syns) =>
  1.2085 +          fold (fn (raw_const, syn) => add_syntax_const_cmd target raw_const (no_bindings syn)) syns)
  1.2086 +  );
  1.2087 +
  1.2088 +val code_monadP =
  1.2089 +  OuterSyntax.command code_monadK "define code syntax for Haskell monads" K.thy_decl (
  1.2090 +    P.term -- P.term -- P.term
  1.2091 +    >> (fn ((raw_run, raw_mbind), raw_kbind) => Toplevel.theory 
  1.2092 +          (add_haskell_monad raw_run raw_mbind raw_kbind))
  1.2093 +  );
  1.2094 +
  1.2095 +val code_reservedP =
  1.2096 +  OuterSyntax.command code_reservedK "declare words as reserved for target language" K.thy_decl (
  1.2097 +    P.name -- Scan.repeat1 P.name
  1.2098 +    >> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds)
  1.2099 +  )
  1.2100 +
  1.2101 +val code_modulenameP =
  1.2102 +  OuterSyntax.command code_modulenameK "alias module to other name" K.thy_decl (
  1.2103 +    P.name -- Scan.repeat1 (P.name -- P.name)
  1.2104 +    >> (fn (target, modlnames) => (Toplevel.theory o fold (add_modl_alias target)) modlnames)
  1.2105 +  )
  1.2106 +
  1.2107 +val code_moduleprologP =
  1.2108 +  OuterSyntax.command code_moduleprologK "add prolog to module" K.thy_decl (
  1.2109 +    P.name -- Scan.repeat1 (P.name -- (P.text >> (fn "-" => NONE | s => SOME s)))
  1.2110 +    >> (fn (target, prologs) => (Toplevel.theory o fold (add_modl_prolog target)) prologs)
  1.2111 +  )
  1.2112 +
  1.2113 +val _ = OuterSyntax.add_keywords [infixK, infixlK, infixrK];
  1.2114 +
  1.2115 +val _ = OuterSyntax.add_parsers [code_classP, code_instanceP, code_typeP, code_constP,
  1.2116 +  code_reservedP, code_modulenameP, code_moduleprologP, code_monadP];
  1.2117 +
  1.2118 +
  1.2119 +(*including serializer defaults*)
  1.2120 +val setup =
  1.2121 +  add_serializer (target_SML, isar_seri_sml)
  1.2122 +  #> add_serializer (target_OCaml, isar_seri_ocaml)
  1.2123 +  #> add_serializer (target_Haskell, isar_seri_haskell)
  1.2124 +  #> add_serializer (target_diag, fn _ => fn _ => fn _ => seri_diagnosis)
  1.2125 +  #> add_syntax_tyco "SML" "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
  1.2126 +      (gen_brackify (case fxy of NOBR => false | _ => eval_fxy (INFX (1, R)) fxy) o Pretty.breaks) [
  1.2127 +        pr_typ (INFX (1, X)) ty1,
  1.2128 +        str "->",
  1.2129 +        pr_typ (INFX (1, R)) ty2
  1.2130 +      ]))
  1.2131 +  #> add_syntax_tyco "OCaml" "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
  1.2132 +      (gen_brackify (case fxy of NOBR => false | _ => eval_fxy (INFX (1, R)) fxy) o Pretty.breaks) [
  1.2133 +        pr_typ (INFX (1, X)) ty1,
  1.2134 +        str "->",
  1.2135 +        pr_typ (INFX (1, R)) ty2
  1.2136 +      ]))
  1.2137 +  #> add_syntax_tyco "Haskell" "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
  1.2138 +      brackify_infix (1, R) fxy [
  1.2139 +        pr_typ (INFX (1, X)) ty1,
  1.2140 +        str "->",
  1.2141 +        pr_typ (INFX (1, R)) ty2
  1.2142 +      ]))
  1.2143 +  #> fold (add_reserved "SML") ML_Syntax.reserved_names
  1.2144 +  #> fold (add_reserved "SML")
  1.2145 +      ["o" (*dictionary projections use it already*), "Fail", "div", "mod" (*standard infixes*)]
  1.2146 +  #> fold (add_reserved "OCaml") [
  1.2147 +      "and", "as", "assert", "begin", "class",
  1.2148 +      "constraint", "do", "done", "downto", "else", "end", "exception",
  1.2149 +      "external", "false", "for", "fun", "function", "functor", "if",
  1.2150 +      "in", "include", "inherit", "initializer", "lazy", "let", "match", "method",
  1.2151 +      "module", "mutable", "new", "object", "of", "open", "or", "private", "rec",
  1.2152 +      "sig", "struct", "then", "to", "true", "try", "type", "val",
  1.2153 +      "virtual", "when", "while", "with"
  1.2154 +    ]
  1.2155 +  #> fold (add_reserved "OCaml") ["failwith", "mod"]
  1.2156 +  #> fold (add_reserved "Haskell") [
  1.2157 +      "hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr",
  1.2158 +      "import", "default", "forall", "let", "in", "class", "qualified", "data",
  1.2159 +      "newtype", "instance", "if", "then", "else", "type", "as", "do", "module"
  1.2160 +    ]
  1.2161 +  #> fold (add_reserved "Haskell") [
  1.2162 +      "Prelude", "Main", "Bool", "Maybe", "Either", "Ordering", "Char", "String", "Int",
  1.2163 +      "Integer", "Float", "Double", "Rational", "IO", "Eq", "Ord", "Enum", "Bounded",
  1.2164 +      "Num", "Real", "Integral", "Fractional", "Floating", "RealFloat", "Monad", "Functor",
  1.2165 +      "AlreadyExists", "ArithException", "ArrayException", "AssertionFailed", "AsyncException",
  1.2166 +      "BlockedOnDeadMVar", "Deadlock", "Denormal", "DivideByZero", "DotNetException", "DynException",
  1.2167 +      "Dynamic", "EOF", "EQ", "EmptyRec", "ErrorCall", "ExitException", "ExitFailure",
  1.2168 +      "ExitSuccess", "False", "GT", "HeapOverflow",
  1.2169 +      "IOError", "IOException", "IllegalOperation",
  1.2170 +      "IndexOutOfBounds", "Just", "Key", "LT", "Left", "LossOfPrecision", "NoMethodError",
  1.2171 +      "NoSuchThing", "NonTermination", "Nothing", "Obj", "OtherError", "Overflow",
  1.2172 +      "PatternMatchFail", "PermissionDenied", "ProtocolError", "RecConError", "RecSelError",
  1.2173 +      "RecUpdError", "ResourceBusy", "ResourceExhausted", "Right", "StackOverflow",
  1.2174 +      "ThreadKilled", "True", "TyCon", "TypeRep", "UndefinedElement", "Underflow",
  1.2175 +      "UnsupportedOperation", "UserError", "abs", "absReal", "acos", "acosh", "all",
  1.2176 +      "and", "any", "appendFile", "asTypeOf", "asciiTab", "asin", "asinh", "atan",
  1.2177 +      "atan2", "atanh", "basicIORun", "blockIO", "boundedEnumFrom", "boundedEnumFromThen",
  1.2178 +      "boundedEnumFromThenTo", "boundedEnumFromTo", "boundedPred", "boundedSucc", "break",
  1.2179 +      "catch", "catchException", "ceiling", "compare", "concat", "concatMap", "const",
  1.2180 +      "cos", "cosh", "curry", "cycle", "decodeFloat", "denominator", "div", "divMod",
  1.2181 +      "doubleToRatio", "doubleToRational", "drop", "dropWhile", "either", "elem",
  1.2182 +      "emptyRec", "encodeFloat", "enumFrom", "enumFromThen", "enumFromThenTo",
  1.2183 +      "enumFromTo", "error", "even", "exp", "exponent", "fail", "filter", "flip",
  1.2184 +      "floatDigits", "floatProperFraction", "floatRadix", "floatRange", "floatToRational",
  1.2185 +      "floor", "fmap", "foldl", "foldl'", "foldl1", "foldr", "foldr1", "fromDouble",
  1.2186 +      "fromEnum", "fromEnum_0", "fromInt", "fromInteger", "fromIntegral", "fromObj",
  1.2187 +      "fromRational", "fst", "gcd", "getChar", "getContents", "getLine", "head",
  1.2188 +      "id", "inRange", "index", "init", "intToRatio", "interact", "ioError", "isAlpha",
  1.2189 +      "isAlphaNum", "isDenormalized", "isDigit", "isHexDigit", "isIEEE", "isInfinite",
  1.2190 +      "isLower", "isNaN", "isNegativeZero", "isOctDigit", "isSpace", "isUpper", "iterate", "iterate'",
  1.2191 +      "last", "lcm", "length", "lex", "lexDigits", "lexLitChar", "lexmatch", "lines", "log",
  1.2192 +      "logBase", "lookup", "loop", "map", "mapM", "mapM_", "max", "maxBound", "maximum",
  1.2193 +      "maybe", "min", "minBound", "minimum", "mod", "negate", "nonnull", "not", "notElem",
  1.2194 +      "null", "numerator", "numericEnumFrom", "numericEnumFromThen", "numericEnumFromThenTo",
  1.2195 +      "numericEnumFromTo", "odd", "or", "otherwise", "pi", "pred", 
  1.2196 +      "print", "product", "properFraction", "protectEsc", "putChar", "putStr", "putStrLn",
  1.2197 +      "quot", "quotRem", "range", "rangeSize", "rationalToDouble", "rationalToFloat",
  1.2198 +      "rationalToRealFloat", "read", "readDec", "readField", "readFieldName", "readFile",
  1.2199 +      "readFloat", "readHex", "readIO", "readInt", "readList", "readLitChar", "readLn",
  1.2200 +      "readOct", "readParen", "readSigned", "reads", "readsPrec", "realFloatToRational",
  1.2201 +      "realToFrac", "recip", "reduce", "rem", "repeat", "replicate", "return", "reverse",
  1.2202 +      "round", "scaleFloat", "scanl", "scanl1", "scanr", "scanr1", "seq", "sequence",
  1.2203 +      "sequence_", "show", "showChar", "showException", "showField", "showList",
  1.2204 +      "showLitChar", "showParen", "showString", "shows", "showsPrec", "significand",
  1.2205 +      "signum", "signumReal", "sin", "sinh", "snd", "span", "splitAt", "sqrt", "subtract",
  1.2206 +      "succ", "sum", "tail", "take", "takeWhile", "takeWhile1", "tan", "tanh", "threadToIOResult",
  1.2207 +      "throw", "toEnum", "toInt", "toInteger", "toObj", "toRational", "truncate", "uncurry",
  1.2208 +      "undefined", "unlines", "unsafeCoerce", "unsafeIndex", "unsafeRangeSize", "until", "unwords",
  1.2209 +      "unzip", "unzip3", "userError", "words", "writeFile", "zip", "zip3", "zipWith", "zipWith3"
  1.2210 +    ] (*due to weird handling of ':', we can't do anything else than to import *all* prelude symbols*);
  1.2211 +
  1.2212 +end; (*local*)
  1.2213 +
  1.2214 +end; (*struct*)