src/Tools/code/code_target.ML
changeset 27103 d8549f4d900b
parent 27024 fcab2dd46872
child 27304 720c8115d723
     1.1 --- a/src/Tools/code/code_target.ML	Tue Jun 10 15:30:01 2008 +0200
     1.2 +++ b/src/Tools/code/code_target.ML	Tue Jun 10 15:30:06 2008 +0200
     1.3 @@ -28,24 +28,28 @@
     1.4    val add_pretty_message: string -> string -> string list -> string
     1.5      -> string -> string -> theory -> theory;
     1.6  
     1.7 -  val allow_exception: string -> theory -> theory;
     1.8 +  val allow_abort: string -> theory -> theory;
     1.9  
    1.10    type serialization;
    1.11    type serializer;
    1.12 -  val add_serializer: string * serializer -> theory -> theory;
    1.13 -  val assert_serializer: theory -> string -> string;
    1.14 -  val serialize: theory -> string -> bool -> string option -> Args.T list
    1.15 -    -> CodeThingol.code -> string list option -> serialization;
    1.16 +  val add_target: string * serializer -> theory -> theory;
    1.17 +  val assert_target: theory -> string -> string;
    1.18 +  val serialize: theory -> string -> string option -> Args.T list
    1.19 +    -> CodeThingol.program -> string list -> serialization;
    1.20    val compile: serialization -> unit;
    1.21    val write: serialization -> unit;
    1.22    val file: Path.T -> serialization -> unit;
    1.23    val string: serialization -> string;
    1.24 -  val sml_of: theory -> CodeThingol.code -> string list -> string;
    1.25 -  val eval: theory -> (string * (unit -> 'a) option ref)
    1.26 -    -> CodeThingol.code -> CodeThingol.iterm * CodeThingol.itype -> string list -> 'a;
    1.27 -  val target_code_width: int ref;
    1.28 +
    1.29 +  val code_of: theory -> string -> string -> string list -> string;
    1.30 +  val eval_conv: string * (unit -> thm) option ref
    1.31 +    -> theory -> cterm -> string list -> thm;
    1.32 +  val eval_term: string * (unit -> 'a) option ref
    1.33 +    -> theory -> term -> string list -> 'a;
    1.34 +  val shell_command: string (*theory name*) -> string (*cg expr*) -> unit;
    1.35  
    1.36    val setup: theory -> theory;
    1.37 +  val code_width: int ref;
    1.38  end;
    1.39  
    1.40  structure CodeTarget : CODE_TARGET =
    1.41 @@ -69,16 +73,16 @@
    1.42  datatype destination = Compile | Write | File of Path.T | String;
    1.43  type serialization = destination -> string option;
    1.44  
    1.45 -val target_code_width = ref 80; (*FIXME after Pretty module no longer depends on print mode*)
    1.46 -fun target_code_setmp f = PrintMode.setmp [] (Pretty.setmp_margin (!target_code_width) f);
    1.47 -fun target_code_of_pretty p = target_code_setmp Pretty.string_of p ^ "\n";
    1.48 -fun target_code_writeln p = Pretty.setmp_margin (!target_code_width) Pretty.writeln p;
    1.49 +val code_width = ref 80; (*FIXME after Pretty module no longer depends on print mode*)
    1.50 +fun code_setmp f = PrintMode.setmp [] (Pretty.setmp_margin (!code_width) f);
    1.51 +fun code_of_pretty p = code_setmp Pretty.string_of p ^ "\n";
    1.52 +fun code_writeln p = Pretty.setmp_margin (!code_width) Pretty.writeln p;
    1.53  
    1.54 -(*FIXME why another target_code_setmp?*)
    1.55 -fun compile f = (target_code_setmp f Compile; ());
    1.56 -fun write f = (target_code_setmp f Write; ());
    1.57 -fun file p f = (target_code_setmp f (File p); ());
    1.58 -fun string f = the (target_code_setmp f String);
    1.59 +(*FIXME why another code_setmp?*)
    1.60 +fun compile f = (code_setmp f Compile; ());
    1.61 +fun write f = (code_setmp f Write; ());
    1.62 +fun file p f = (code_setmp f (File p); ());
    1.63 +fun string f = the (code_setmp f String);
    1.64  
    1.65  
    1.66  (** generic syntax **)
    1.67 @@ -125,13 +129,12 @@
    1.68  
    1.69  (** theory data **)
    1.70  
    1.71 -val target_diag = "diag";
    1.72  val target_SML = "SML";
    1.73  val target_OCaml = "OCaml";
    1.74  val target_Haskell = "Haskell";
    1.75  
    1.76  datatype name_syntax_table = NameSyntaxTable of {
    1.77 -  class: (string * (string -> string option)) Symtab.table,
    1.78 +  class: class_syntax Symtab.table,
    1.79    inst: unit Symtab.table,
    1.80    tyco: typ_syntax Symtab.table,
    1.81    const: term_syntax Symtab.table
    1.82 @@ -160,7 +163,7 @@
    1.83    -> (string -> class_syntax option)
    1.84    -> (string -> typ_syntax option)
    1.85    -> (string -> term_syntax option)
    1.86 -  -> CodeThingol.code                   (*program*)
    1.87 +  -> CodeThingol.program
    1.88    -> string list                        (*selected statements*)
    1.89    -> serialization;
    1.90  
    1.91 @@ -209,12 +212,14 @@
    1.92  fun the_name_syntax (Target { name_syntax_table = NameSyntaxTable x, ... }) = x;
    1.93  fun the_module_alias (Target { module_alias , ... }) = module_alias;
    1.94  
    1.95 -fun assert_serializer thy target =
    1.96 +val abort_allowed = snd o CodeTargetData.get;
    1.97 +
    1.98 +fun assert_target thy target =
    1.99    case Symtab.lookup (fst (CodeTargetData.get thy)) target
   1.100     of SOME data => target
   1.101      | NONE => error ("Unknown code target language: " ^ quote target);
   1.102  
   1.103 -fun add_serializer (target, seri) thy =
   1.104 +fun add_target (target, seri) thy =
   1.105    let
   1.106      val _ = case Symtab.lookup (fst (CodeTargetData.get thy)) target
   1.107       of SOME _ => warning ("Overwriting existing serializer " ^ quote target)
   1.108 @@ -228,48 +233,59 @@
   1.109            ((map_target o apfst o apsnd o K) seri)
   1.110    end;
   1.111  
   1.112 -fun map_seri_data target f thy =
   1.113 +fun map_target_data target f thy =
   1.114    let
   1.115 -    val _ = assert_serializer thy target;
   1.116 +    val _ = assert_target thy target;
   1.117    in
   1.118      thy
   1.119      |> (CodeTargetData.map o apfst o Symtab.map_entry target o map_target) f
   1.120    end;
   1.121  
   1.122 -fun map_adaptions target =
   1.123 -  map_seri_data target o apsnd o apfst;
   1.124 +fun map_reserved target =
   1.125 +  map_target_data target o apsnd o apfst o apfst;
   1.126 +fun map_includes target =
   1.127 +  map_target_data target o apsnd o apfst o apsnd;
   1.128  fun map_name_syntax target =
   1.129 -  map_seri_data target o apsnd o apsnd o apfst o map_name_syntax_table;
   1.130 +  map_target_data target o apsnd o apsnd o apfst o map_name_syntax_table;
   1.131  fun map_module_alias target =
   1.132 -  map_seri_data target o apsnd o apsnd o apsnd;
   1.133 +  map_target_data target o apsnd o apsnd o apsnd;
   1.134  
   1.135 -fun get_serializer get_seri thy target permissive =
   1.136 +fun invoke_serializer thy abortable serializer reserved includes 
   1.137 +    module_alias class inst tyco const module args program1 cs1 =
   1.138    let
   1.139 -    val (seris, exc) = CodeTargetData.get thy;
   1.140 -    val data = case Symtab.lookup seris target
   1.141 +    val hidden = Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const;
   1.142 +    val cs2 = subtract (op =) hidden cs1;
   1.143 +    val program2 = Graph.subgraph (not o member (op =) hidden) program1;
   1.144 +    val all_cs = Graph.all_succs program2 cs2;
   1.145 +    val program3 = Graph.subgraph (member (op =) all_cs) program2;
   1.146 +    val empty_funs = filter_out (member (op =) abortable)
   1.147 +      (CodeThingol.empty_funs program3);
   1.148 +    val _ = if null empty_funs then () else error ("No defining equations for "
   1.149 +      ^ commas (map (CodeName.labelled_name thy) empty_funs));
   1.150 +  in
   1.151 +    serializer module args (CodeName.labelled_name thy) reserved includes
   1.152 +      (Symtab.lookup module_alias) (Symtab.lookup class)
   1.153 +      (Symtab.lookup tyco) (Symtab.lookup const)
   1.154 +      program3 cs2
   1.155 +  end;
   1.156 +
   1.157 +fun mount_serializer thy alt_serializer target =
   1.158 +  let
   1.159 +    val (targets, abortable) = CodeTargetData.get thy;
   1.160 +    val data = case Symtab.lookup targets target
   1.161       of SOME data => data
   1.162        | NONE => error ("Unknown code target language: " ^ quote target);
   1.163 -    val seri = get_seri data;
   1.164 +    val serializer = the_default (the_serializer data) alt_serializer;
   1.165      val reserved = the_reserved data;
   1.166      val includes = Symtab.dest (the_includes data);
   1.167 -    val alias = the_module_alias data;
   1.168 +    val module_alias = the_module_alias data;
   1.169      val { class, inst, tyco, const } = the_name_syntax data;
   1.170 -    val project = if target = target_diag then K I
   1.171 -      else CodeThingol.project_code permissive
   1.172 -        (Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const);
   1.173 -    fun check_empty_funs code = case filter_out (member (op =) exc)
   1.174 -        (CodeThingol.empty_funs code)
   1.175 -     of [] => code
   1.176 -      | names => error ("No defining equations for "
   1.177 -          ^ commas (map (CodeName.labelled_name thy) names));
   1.178 -  in fn module => fn args => fn code => fn cs =>
   1.179 -    seri module args (CodeName.labelled_name thy) reserved includes
   1.180 -      (Symtab.lookup alias) (Symtab.lookup class)
   1.181 -      (Symtab.lookup tyco) (Symtab.lookup const)
   1.182 -        ((check_empty_funs o project cs) code) (these cs)
   1.183 +  in
   1.184 +    invoke_serializer thy abortable serializer reserved
   1.185 +      includes module_alias class inst tyco const
   1.186    end;
   1.187  
   1.188 -val serialize = get_serializer the_serializer;
   1.189 +fun serialize thy = mount_serializer thy NONE;
   1.190  
   1.191  fun parse_args f args =
   1.192    case Scan.read Args.stopper f args
   1.193 @@ -277,39 +293,7 @@
   1.194      | NONE => error "Bad serializer arguments";
   1.195  
   1.196  
   1.197 -(** generic output combinators **)
   1.198 -
   1.199 -(* applications and bindings *)
   1.200 -
   1.201 -fun gen_pr_app pr_app' pr_term const_syntax labelled_name is_cons
   1.202 -      lhs vars fxy (app as ((c, (_, tys)), ts)) =
   1.203 -  case const_syntax c
   1.204 -   of NONE => if lhs andalso not (is_cons c) then
   1.205 -          error ("Non-constructor on left hand side of equation: " ^ labelled_name c)
   1.206 -        else brackify fxy (pr_app' lhs vars app)
   1.207 -    | SOME (i, pr) =>
   1.208 -        let
   1.209 -          val k = if i < 0 then length tys else i;
   1.210 -          fun pr' fxy ts = pr (pr_term lhs) vars fxy (ts ~~ curry Library.take k tys);
   1.211 -        in if k = length ts
   1.212 -          then pr' fxy ts
   1.213 -        else if k < length ts
   1.214 -          then case chop k ts of (ts1, ts2) =>
   1.215 -            brackify fxy (pr' APP ts1 :: map (pr_term lhs vars BR) ts2)
   1.216 -          else pr_term lhs vars fxy (CodeThingol.eta_expand app k)
   1.217 -        end;
   1.218 -
   1.219 -fun gen_pr_bind pr_bind' pr_term fxy ((v, pat), ty) vars =
   1.220 -  let
   1.221 -    val vs = case pat
   1.222 -     of SOME pat => CodeThingol.fold_varnames (insert (op =)) pat []
   1.223 -      | NONE => [];
   1.224 -    val vars' = CodeName.intro_vars (the_list v) vars;
   1.225 -    val vars'' = CodeName.intro_vars vs vars';
   1.226 -    val v' = Option.map (CodeName.lookup_var vars') v;
   1.227 -    val pat' = Option.map (pr_term true vars'' fxy) pat;
   1.228 -  in (pr_bind' ((v', pat'), ty), vars'') end;
   1.229 -
   1.230 +(** generic code combinators **)
   1.231  
   1.232  (* list, char, string, numeral and monad abstract syntax transformations *)
   1.233  
   1.234 @@ -359,7 +343,7 @@
   1.235        | dest_numeral (t1 `$ t2) =
   1.236            let val (n, b) = (dest_numeral t2, dest_bit t1)
   1.237            in case n of SOME n => SOME (2 * n + b) | NONE => NONE end
   1.238 -      | dest_numeral _ = error "Illegal numeral expression: illegal constant";
   1.239 +      | dest_numeral _ = error "Illegal numeral expression: illegal term";
   1.240    in dest_numeral #> the_default 0 end;
   1.241  
   1.242  fun implode_monad c_bind t =
   1.243 @@ -378,6 +362,38 @@
   1.244    in CodeThingol.unfoldr dest_monad t end;
   1.245  
   1.246  
   1.247 +(* applications and bindings *)
   1.248 +
   1.249 +fun gen_pr_app pr_app pr_term syntax_const labelled_name is_cons
   1.250 +      lhs vars fxy (app as ((c, (_, tys)), ts)) =
   1.251 +  case syntax_const c
   1.252 +   of NONE => if lhs andalso not (is_cons c) then
   1.253 +          error ("Non-constructor on left hand side of equation: " ^ labelled_name c)
   1.254 +        else brackify fxy (pr_app lhs vars app)
   1.255 +    | SOME (i, pr) =>
   1.256 +        let
   1.257 +          val k = if i < 0 then length tys else i;
   1.258 +          fun pr' fxy ts = pr (pr_term lhs) vars fxy (ts ~~ curry Library.take k tys);
   1.259 +        in if k = length ts
   1.260 +          then pr' fxy ts
   1.261 +        else if k < length ts
   1.262 +          then case chop k ts of (ts1, ts2) =>
   1.263 +            brackify fxy (pr' APP ts1 :: map (pr_term lhs vars BR) ts2)
   1.264 +          else pr_term lhs vars fxy (CodeThingol.eta_expand app k)
   1.265 +        end;
   1.266 +
   1.267 +fun gen_pr_bind pr_bind pr_term (fxy : fixity) ((v, pat), ty : itype) vars =
   1.268 +  let
   1.269 +    val vs = case pat
   1.270 +     of SOME pat => CodeThingol.fold_varnames (insert (op =)) pat []
   1.271 +      | NONE => [];
   1.272 +    val vars' = CodeName.intro_vars (the_list v) vars;
   1.273 +    val vars'' = CodeName.intro_vars vs vars';
   1.274 +    val v' = Option.map (CodeName.lookup_var vars') v;
   1.275 +    val pat' = Option.map (pr_term true vars'' fxy) pat;
   1.276 +  in (pr_bind ((v', pat'), ty), vars'') end;
   1.277 +
   1.278 +
   1.279  (* name auxiliary *)
   1.280  
   1.281  val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode;
   1.282 @@ -386,30 +402,29 @@
   1.283  val dest_name =
   1.284    apfst NameSpace.implode o split_last o fst o split_last o NameSpace.explode;
   1.285  
   1.286 -fun mk_modl_name_tab init_names prefix module_alias code =
   1.287 +fun mk_name_module reserved_names module_prefix module_alias program =
   1.288    let
   1.289 -    fun nsp_map f = NameSpace.explode #> map f #> NameSpace.implode;
   1.290 -    fun mk_alias name =
   1.291 -     case module_alias name
   1.292 -      of SOME name' => name'
   1.293 -       | NONE => nsp_map (fn name => (the_single o fst)
   1.294 -            (Name.variants [name] init_names)) name;
   1.295 -    fun mk_prefix name =
   1.296 -      case prefix
   1.297 -       of SOME prefix => NameSpace.append prefix name
   1.298 -        | NONE => name;
   1.299 +    fun mk_alias name = case module_alias name
   1.300 +     of SOME name' => name'
   1.301 +      | NONE => name
   1.302 +          |> NameSpace.explode
   1.303 +          |> map (fn name => (the_single o fst) (Name.variants [name] reserved_names))
   1.304 +          |> NameSpace.implode;
   1.305 +    fun mk_prefix name = case module_prefix
   1.306 +     of SOME module_prefix => NameSpace.append module_prefix name
   1.307 +      | NONE => name;
   1.308      val tab =
   1.309        Symtab.empty
   1.310        |> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name))
   1.311             o fst o dest_name o fst)
   1.312 -             code
   1.313 -  in fn name => (the o Symtab.lookup tab) name end;
   1.314 +             program
   1.315 +  in the o Symtab.lookup tab end;
   1.316  
   1.317  
   1.318  
   1.319  (** SML/OCaml serializer **)
   1.320  
   1.321 -datatype ml_def =
   1.322 +datatype ml_stmt =
   1.323      MLFuns of (string * (typscheme * (iterm list * iterm) list)) list
   1.324    | MLDatas of (string * ((vname * sort) list * (string * itype list) list)) list
   1.325    | MLClass of string * (vname * ((class * string) list * (string * itype) list))
   1.326 @@ -417,7 +432,7 @@
   1.327          * ((class * (string * (string * dict list list))) list
   1.328        * (string * const) list));
   1.329  
   1.330 -fun pr_sml tyco_syntax const_syntax labelled_name init_syms deresolv is_cons ml_def =
   1.331 +fun pr_sml_stmt syntax_tyco syntax_const labelled_name reserved_names deresolve is_cons =
   1.332    let
   1.333      val pr_label_classrel = translate_string (fn "." => "__" | c => c)
   1.334        o NameSpace.qualifier;
   1.335 @@ -432,30 +447,30 @@
   1.336                brackets [p', p]
   1.337            | pr_proj (ps as _ :: _) p =
   1.338                brackets [Pretty.enum " o" "(" ")" ps, p];
   1.339 -        fun pr_dictc fxy (DictConst (inst, dss)) =
   1.340 -              brackify fxy ((str o deresolv) inst :: map (pr_dicts BR) dss)
   1.341 -          | pr_dictc fxy (DictVar (classrels, v)) =
   1.342 -              pr_proj (map (str o deresolv) classrels) ((str o pr_dictvar) v)
   1.343 +        fun pr_dict fxy (DictConst (inst, dss)) =
   1.344 +              brackify fxy ((str o deresolve) inst :: map (pr_dicts BR) dss)
   1.345 +          | pr_dict fxy (DictVar (classrels, v)) =
   1.346 +              pr_proj (map (str o deresolve) classrels) ((str o pr_dictvar) v)
   1.347        in case ds
   1.348         of [] => str "()"
   1.349 -        | [d] => pr_dictc fxy d
   1.350 -        | _ :: _ => (Pretty.list "(" ")" o map (pr_dictc NOBR)) ds
   1.351 +        | [d] => pr_dict fxy d
   1.352 +        | _ :: _ => (Pretty.list "(" ")" o map (pr_dict NOBR)) ds
   1.353        end;
   1.354 -    fun pr_tyvars vs =
   1.355 +    fun pr_tyvar_dicts vs =
   1.356        vs
   1.357        |> map (fn (v, sort) => map_index (fn (i, _) =>
   1.358             DictVar ([], (v, (i, length sort)))) sort)
   1.359        |> map (pr_dicts BR);
   1.360      fun pr_tycoexpr fxy (tyco, tys) =
   1.361        let
   1.362 -        val tyco' = (str o deresolv) tyco
   1.363 +        val tyco' = (str o deresolve) tyco
   1.364        in case map (pr_typ BR) tys
   1.365         of [] => tyco'
   1.366          | [p] => Pretty.block [p, Pretty.brk 1, tyco']
   1.367          | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco']
   1.368        end
   1.369      and pr_typ fxy (tyco `%% tys) =
   1.370 -          (case tyco_syntax tyco
   1.371 +          (case syntax_tyco tyco
   1.372             of NONE => pr_tycoexpr fxy (tyco, tys)
   1.373              | SOME (i, pr) =>
   1.374                  if not (i = length tys)
   1.375 @@ -484,7 +499,7 @@
   1.376            in brackets (ps @ [pr_term lhs vars' NOBR t']) end
   1.377        | pr_term lhs vars fxy (ICase (cases as (_, t0))) =
   1.378            (case CodeThingol.unfold_const_app t0
   1.379 -           of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
   1.380 +           of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
   1.381                  then pr_case vars fxy cases
   1.382                  else pr_app lhs vars fxy c_ts
   1.383              | NONE => pr_case vars fxy cases)
   1.384 @@ -492,13 +507,13 @@
   1.385        if is_cons c then let
   1.386          val k = length tys
   1.387        in if k < 2 then 
   1.388 -        (str o deresolv) c :: map (pr_term lhs vars BR) ts
   1.389 +        (str o deresolve) c :: map (pr_term lhs vars BR) ts
   1.390        else if k = length ts then
   1.391 -        [(str o deresolv) c, Pretty.enum "," "(" ")" (map (pr_term lhs vars NOBR) ts)]
   1.392 +        [(str o deresolve) c, Pretty.enum "," "(" ")" (map (pr_term lhs vars NOBR) ts)]
   1.393        else [pr_term lhs vars BR (CodeThingol.eta_expand app k)] end else
   1.394 -        (str o deresolv) c
   1.395 +        (str o deresolve) c
   1.396            :: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term lhs vars BR) ts
   1.397 -    and pr_app lhs vars = gen_pr_app pr_app' pr_term const_syntax
   1.398 +    and pr_app lhs vars = gen_pr_app pr_app' pr_term syntax_const
   1.399        labelled_name is_cons lhs vars
   1.400      and pr_bind' ((NONE, NONE), _) = str "_"
   1.401        | pr_bind' ((SOME v, NONE), _) = str v
   1.402 @@ -537,7 +552,7 @@
   1.403              )
   1.404            end
   1.405        | pr_case vars fxy ((_, []), _) = str "raise Fail \"empty case\""
   1.406 -    fun pr_def (MLFuns (funns as (funn :: funns'))) =
   1.407 +    fun pr_stmt (MLFuns (funns as (funn :: funns'))) =
   1.408            let
   1.409              val definer =
   1.410                let
   1.411 @@ -553,46 +568,45 @@
   1.412                        else error ("Mixing simultaneous vals and funs not implemented: "
   1.413                          ^ commas (map (labelled_name o fst) funns));
   1.414                in the (fold chk funns NONE) end;
   1.415 -            fun pr_funn definer (name, ((raw_vs, ty), [])) =
   1.416 +            fun pr_funn definer (name, ((vs, ty), [])) =
   1.417                    let
   1.418 -                    val vs = filter_out (null o snd) raw_vs;
   1.419 -                    val n = length vs + (length o fst o CodeThingol.unfold_fun) ty;
   1.420 +                    val vs_dict = filter_out (null o snd) vs;
   1.421 +                    val n = length vs_dict + (length o fst o CodeThingol.unfold_fun) ty;
   1.422                      val exc_str =
   1.423                        (ML_Syntax.print_string o NameSpace.base o NameSpace.qualifier) name;
   1.424                    in
   1.425                      concat (
   1.426                        str definer
   1.427 -                      :: (str o deresolv) name
   1.428 +                      :: (str o deresolve) name
   1.429                        :: map str (replicate n "_")
   1.430                        @ str "="
   1.431                        :: str "raise"
   1.432                        :: str "(Fail"
   1.433 -                      :: str exc_str
   1.434 -                      @@ str ")"
   1.435 +                      @@ str (exc_str ^ ")")
   1.436                      )
   1.437                    end
   1.438 -              | pr_funn definer (name, ((raw_vs, ty), eqs as eq :: eqs')) =
   1.439 +              | pr_funn definer (name, ((vs, ty), eqs as eq :: eqs')) =
   1.440                    let
   1.441 -                    val vs = filter_out (null o snd) raw_vs;
   1.442 +                    val vs_dict = filter_out (null o snd) vs;
   1.443                      val shift = if null eqs' then I else
   1.444                        map (Pretty.block o single o Pretty.block o single);
   1.445                      fun pr_eq definer (ts, t) =
   1.446                        let
   1.447                          val consts = map_filter
   1.448 -                          (fn c => if (is_some o const_syntax) c
   1.449 -                            then NONE else (SOME o NameSpace.base o deresolv) c)
   1.450 +                          (fn c => if (is_some o syntax_const) c
   1.451 +                            then NONE else (SOME o NameSpace.base o deresolve) c)
   1.452                              ((fold o CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []);
   1.453 -                        val vars = init_syms
   1.454 +                        val vars = reserved_names
   1.455                            |> CodeName.intro_vars consts
   1.456                            |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames)
   1.457                                 (insert (op =)) ts []);
   1.458                        in
   1.459                          concat (
   1.460 -                          [str definer, (str o deresolv) name]
   1.461 -                          @ (if null ts andalso null vs
   1.462 +                          [str definer, (str o deresolve) name]
   1.463 +                          @ (if null ts andalso null vs_dict
   1.464                               then [str ":", pr_typ NOBR ty]
   1.465                               else
   1.466 -                               pr_tyvars vs
   1.467 +                               pr_tyvar_dicts vs_dict
   1.468                                 @ map (pr_term true vars BR) ts)
   1.469                         @ [str "=", pr_term false vars NOBR t]
   1.470                          )
   1.471 @@ -605,13 +619,13 @@
   1.472                    end;
   1.473              val (ps, p) = split_last (pr_funn definer funn :: map (pr_funn "and") funns');
   1.474            in Pretty.chunks (ps @ [Pretty.block ([p, str ";"])]) end
   1.475 -     | pr_def (MLDatas (datas as (data :: datas'))) =
   1.476 +     | pr_stmt (MLDatas (datas as (data :: datas'))) =
   1.477            let
   1.478              fun pr_co (co, []) =
   1.479 -                  str (deresolv co)
   1.480 +                  str (deresolve co)
   1.481                | pr_co (co, tys) =
   1.482                    concat [
   1.483 -                    str (deresolv co),
   1.484 +                    str (deresolve co),
   1.485                      str "of",
   1.486                      Pretty.enum " *" "" "" (map (pr_typ (INFX (2, X))) tys)
   1.487                    ];
   1.488 @@ -632,12 +646,12 @@
   1.489              val (ps, p) = split_last
   1.490                (pr_data "datatype" data :: map (pr_data "and") datas');
   1.491            in Pretty.chunks (ps @ [Pretty.block ([p, str ";"])]) end
   1.492 -     | pr_def (MLClass (class, (v, (superclasses, classparams)))) =
   1.493 +     | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) =
   1.494            let
   1.495              val w = first_upper v ^ "_";
   1.496              fun pr_superclass_field (class, classrel) =
   1.497                (concat o map str) [
   1.498 -                pr_label_classrel classrel, ":", "'" ^ v, deresolv class
   1.499 +                pr_label_classrel classrel, ":", "'" ^ v, deresolve class
   1.500                ];
   1.501              fun pr_classparam_field (classparam, ty) =
   1.502                concat [
   1.503 @@ -646,8 +660,8 @@
   1.504              fun pr_classparam_proj (classparam, _) =
   1.505                semicolon [
   1.506                  str "fun",
   1.507 -                (str o deresolv) classparam,
   1.508 -                Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolv class)],
   1.509 +                (str o deresolve) classparam,
   1.510 +                Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolve class)],
   1.511                  str "=",
   1.512                  str ("#" ^ pr_label_classparam classparam),
   1.513                  str w
   1.514 @@ -655,8 +669,8 @@
   1.515              fun pr_superclass_proj (_, classrel) =
   1.516                semicolon [
   1.517                  str "fun",
   1.518 -                (str o deresolv) classrel,
   1.519 -                Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolv class)],
   1.520 +                (str o deresolve) classrel,
   1.521 +                Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolve class)],
   1.522                  str "=",
   1.523                  str ("#" ^ pr_label_classrel classrel),
   1.524                  str w
   1.525 @@ -665,7 +679,7 @@
   1.526              Pretty.chunks (
   1.527                concat [
   1.528                  str ("type '" ^ v),
   1.529 -                (str o deresolv) class,
   1.530 +                (str o deresolve) class,
   1.531                  str "=",
   1.532                  Pretty.enum "," "{" "};" (
   1.533                    map pr_superclass_field superclasses @ map pr_classparam_field classparams
   1.534 @@ -675,7 +689,7 @@
   1.535                @ map pr_classparam_proj classparams
   1.536              )
   1.537            end
   1.538 -     | pr_def (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) =
   1.539 +     | pr_stmt (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) =
   1.540            let
   1.541              fun pr_superclass (_, (classrel, dss)) =
   1.542                concat [
   1.543 @@ -687,13 +701,13 @@
   1.544                concat [
   1.545                  (str o pr_label_classparam) classparam,
   1.546                  str "=",
   1.547 -                pr_app false init_syms NOBR (c_inst, [])
   1.548 +                pr_app false reserved_names NOBR (c_inst, [])
   1.549                ];
   1.550            in
   1.551              semicolon ([
   1.552                str (if null arity then "val" else "fun"),
   1.553 -              (str o deresolv) inst ] @
   1.554 -              pr_tyvars arity @ [
   1.555 +              (str o deresolve) inst ] @
   1.556 +              pr_tyvar_dicts arity @ [
   1.557                str "=",
   1.558                Pretty.enum "," "{" "}"
   1.559                  (map pr_superclass superarities @ map pr_classparam classparam_insts),
   1.560 @@ -701,20 +715,19 @@
   1.561                pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])
   1.562              ])
   1.563            end;
   1.564 -  in pr_def ml_def end;
   1.565 +  in pr_stmt end;
   1.566  
   1.567 -fun pr_sml_modl name content =
   1.568 -  Pretty.chunks ([
   1.569 -    str ("structure " ^ name ^ " = "),
   1.570 -    str "struct",
   1.571 -    str ""
   1.572 -  ] @ content @ [
   1.573 -    str "",
   1.574 -    str ("end; (*struct " ^ name ^ "*)")
   1.575 -  ]);
   1.576 +fun pr_sml_module name content =
   1.577 +  Pretty.chunks (
   1.578 +    str ("structure " ^ name ^ " = ")
   1.579 +    :: str "struct"
   1.580 +    :: str ""
   1.581 +    :: content
   1.582 +    @ str ""
   1.583 +    @@ str ("end; (*struct " ^ name ^ "*)")
   1.584 +  );
   1.585  
   1.586 -fun pr_ocaml tyco_syntax const_syntax labelled_name
   1.587 -    init_syms deresolv is_cons ml_def =
   1.588 +fun pr_ocaml_stmt syntax_tyco syntax_const labelled_name reserved_names deresolve is_cons =
   1.589    let
   1.590      fun pr_dicts fxy ds =
   1.591        let
   1.592 @@ -722,30 +735,30 @@
   1.593            | pr_dictvar (v, (i, _)) = "_" ^ first_upper v ^ string_of_int (i+1);
   1.594          fun pr_proj ps p =
   1.595            fold_rev (fn p2 => fn p1 => Pretty.block [p1, str ".", str p2]) ps p
   1.596 -        fun pr_dictc fxy (DictConst (inst, dss)) =
   1.597 -              brackify fxy ((str o deresolv) inst :: map (pr_dicts BR) dss)
   1.598 -          | pr_dictc fxy (DictVar (classrels, v)) =
   1.599 -              pr_proj (map deresolv classrels) ((str o pr_dictvar) v)
   1.600 +        fun pr_dict fxy (DictConst (inst, dss)) =
   1.601 +              brackify fxy ((str o deresolve) inst :: map (pr_dicts BR) dss)
   1.602 +          | pr_dict fxy (DictVar (classrels, v)) =
   1.603 +              pr_proj (map deresolve classrels) ((str o pr_dictvar) v)
   1.604        in case ds
   1.605         of [] => str "()"
   1.606 -        | [d] => pr_dictc fxy d
   1.607 -        | _ :: _ => (Pretty.list "(" ")" o map (pr_dictc NOBR)) ds
   1.608 +        | [d] => pr_dict fxy d
   1.609 +        | _ :: _ => (Pretty.list "(" ")" o map (pr_dict NOBR)) ds
   1.610        end;
   1.611 -    fun pr_tyvars vs =
   1.612 +    fun pr_tyvar_dicts vs =
   1.613        vs
   1.614        |> map (fn (v, sort) => map_index (fn (i, _) =>
   1.615             DictVar ([], (v, (i, length sort)))) sort)
   1.616        |> map (pr_dicts BR);
   1.617      fun pr_tycoexpr fxy (tyco, tys) =
   1.618        let
   1.619 -        val tyco' = (str o deresolv) tyco
   1.620 +        val tyco' = (str o deresolve) tyco
   1.621        in case map (pr_typ BR) tys
   1.622         of [] => tyco'
   1.623          | [p] => Pretty.block [p, Pretty.brk 1, tyco']
   1.624          | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco']
   1.625        end
   1.626      and pr_typ fxy (tyco `%% tys) =
   1.627 -          (case tyco_syntax tyco
   1.628 +          (case syntax_tyco tyco
   1.629             of NONE => pr_tycoexpr fxy (tyco, tys)
   1.630              | SOME (i, pr) =>
   1.631                  if not (i = length tys)
   1.632 @@ -771,7 +784,7 @@
   1.633              val (ps, vars') = fold_map pr binds vars;
   1.634            in brackets (str "fun" :: ps @ str "->" @@ pr_term lhs vars' NOBR t') end
   1.635        | pr_term lhs vars fxy (ICase (cases as (_, t0))) = (case CodeThingol.unfold_const_app t0
   1.636 -           of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
   1.637 +           of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
   1.638                  then pr_case vars fxy cases
   1.639                  else pr_app lhs vars fxy c_ts
   1.640              | NONE => pr_case vars fxy cases)
   1.641 @@ -779,14 +792,14 @@
   1.642        if is_cons c then
   1.643          if length tys = length ts
   1.644          then case ts
   1.645 -         of [] => [(str o deresolv) c]
   1.646 -          | [t] => [(str o deresolv) c, pr_term lhs vars BR t]
   1.647 -          | _ => [(str o deresolv) c, Pretty.enum "," "(" ")"
   1.648 +         of [] => [(str o deresolve) c]
   1.649 +          | [t] => [(str o deresolve) c, pr_term lhs vars BR t]
   1.650 +          | _ => [(str o deresolve) c, Pretty.enum "," "(" ")"
   1.651                      (map (pr_term lhs vars NOBR) ts)]
   1.652          else [pr_term lhs vars BR (CodeThingol.eta_expand app (length tys))]
   1.653 -      else (str o deresolv) c
   1.654 +      else (str o deresolve) c
   1.655          :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term lhs vars BR) ts)
   1.656 -    and pr_app lhs vars = gen_pr_app pr_app' pr_term const_syntax
   1.657 +    and pr_app lhs vars = gen_pr_app pr_app' pr_term syntax_const
   1.658        labelled_name is_cons lhs vars
   1.659      and pr_bind' ((NONE, NONE), _) = str "_"
   1.660        | pr_bind' ((SOME v, NONE), _) = str v
   1.661 @@ -818,28 +831,28 @@
   1.662              )
   1.663            end
   1.664        | pr_case vars fxy ((_, []), _) = str "failwith \"empty case\"";
   1.665 -    fun pr_def (MLFuns (funns as funn :: funns')) =
   1.666 +    fun fish_params vars eqs =
   1.667 +      let
   1.668 +        fun fish_param _ (w as SOME _) = w
   1.669 +          | fish_param (IVar v) NONE = SOME v
   1.670 +          | fish_param _ NONE = NONE;
   1.671 +        fun fillup_param _ (_, SOME v) = v
   1.672 +          | fillup_param x (i, NONE) = x ^ string_of_int i;
   1.673 +        val fished1 = fold (map2 fish_param) eqs (replicate (length (hd eqs)) NONE);
   1.674 +        val x = Name.variant (map_filter I fished1) "x";
   1.675 +        val fished2 = map_index (fillup_param x) fished1;
   1.676 +        val (fished3, _) = Name.variants fished2 Name.context;
   1.677 +        val vars' = CodeName.intro_vars fished3 vars;
   1.678 +      in map (CodeName.lookup_var vars') fished3 end;
   1.679 +    fun pr_stmt (MLFuns (funns as funn :: funns')) =
   1.680            let
   1.681 -            fun fish_parm _ (w as SOME _) = w
   1.682 -              | fish_parm (IVar v) NONE = SOME v
   1.683 -              | fish_parm _ NONE = NONE;
   1.684 -            fun fillup_parm _ (_, SOME v) = v
   1.685 -              | fillup_parm x (i, NONE) = x ^ string_of_int i;
   1.686 -            fun fish_parms vars eqs =
   1.687 -              let
   1.688 -                val fished1 = fold (map2 fish_parm) eqs (replicate (length (hd eqs)) NONE);
   1.689 -                val x = Name.variant (map_filter I fished1) "x";
   1.690 -                val fished2 = map_index (fillup_parm x) fished1;
   1.691 -                val (fished3, _) = Name.variants fished2 Name.context;
   1.692 -                val vars' = CodeName.intro_vars fished3 vars;
   1.693 -              in map (CodeName.lookup_var vars') fished3 end;
   1.694              fun pr_eq (ts, t) =
   1.695                let
   1.696                  val consts = map_filter
   1.697 -                  (fn c => if (is_some o const_syntax) c
   1.698 -                    then NONE else (SOME o NameSpace.base o deresolv) c)
   1.699 +                  (fn c => if (is_some o syntax_const) c
   1.700 +                    then NONE else (SOME o NameSpace.base o deresolve) c)
   1.701                      ((fold o CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []);
   1.702 -                val vars = init_syms
   1.703 +                val vars = reserved_names
   1.704                    |> CodeName.intro_vars consts
   1.705                    |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames)
   1.706                        (insert (op =)) ts []);
   1.707 @@ -864,10 +877,10 @@
   1.708                | pr_eqs _ _ [(ts, t)] =
   1.709                    let
   1.710                      val consts = map_filter
   1.711 -                      (fn c => if (is_some o const_syntax) c
   1.712 -                        then NONE else (SOME o NameSpace.base o deresolv) c)
   1.713 +                      (fn c => if (is_some o syntax_const) c
   1.714 +                        then NONE else (SOME o NameSpace.base o deresolve) c)
   1.715                          ((fold o CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []);
   1.716 -                    val vars = init_syms
   1.717 +                    val vars = reserved_names
   1.718                        |> CodeName.intro_vars consts
   1.719                        |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames)
   1.720                            (insert (op =)) ts []);
   1.721 @@ -891,13 +904,13 @@
   1.722                | pr_eqs _ _ (eqs as eq :: eqs') =
   1.723                    let
   1.724                      val consts = map_filter
   1.725 -                      (fn c => if (is_some o const_syntax) c
   1.726 -                        then NONE else (SOME o NameSpace.base o deresolv) c)
   1.727 +                      (fn c => if (is_some o syntax_const) c
   1.728 +                        then NONE else (SOME o NameSpace.base o deresolve) c)
   1.729                          ((fold o CodeThingol.fold_constnames)
   1.730                            (insert (op =)) (map snd eqs) []);
   1.731 -                    val vars = init_syms
   1.732 +                    val vars = reserved_names
   1.733                        |> CodeName.intro_vars consts;
   1.734 -                    val dummy_parms = (map str o fish_parms vars o map fst) eqs;
   1.735 +                    val dummy_parms = (map str o fish_params vars o map fst) eqs;
   1.736                    in
   1.737                      Pretty.block (
   1.738                        Pretty.breaks dummy_parms
   1.739 @@ -918,20 +931,20 @@
   1.740              fun pr_funn definer (name, ((vs, ty), eqs)) =
   1.741                concat (
   1.742                  str definer
   1.743 -                :: (str o deresolv) name
   1.744 -                :: pr_tyvars (filter_out (null o snd) vs)
   1.745 +                :: (str o deresolve) name
   1.746 +                :: pr_tyvar_dicts (filter_out (null o snd) vs)
   1.747                  @| pr_eqs name ty eqs
   1.748                );
   1.749              val (ps, p) = split_last
   1.750                (pr_funn "let rec" funn :: map (pr_funn "and") funns');
   1.751            in Pretty.chunks (ps @ [Pretty.block ([p, str ";;"])]) end
   1.752 -     | pr_def (MLDatas (datas as (data :: datas'))) =
   1.753 +     | pr_stmt (MLDatas (datas as (data :: datas'))) =
   1.754            let
   1.755              fun pr_co (co, []) =
   1.756 -                  str (deresolv co)
   1.757 +                  str (deresolve co)
   1.758                | pr_co (co, tys) =
   1.759                    concat [
   1.760 -                    str (deresolv co),
   1.761 +                    str (deresolve co),
   1.762                      str "of",
   1.763                      Pretty.enum " *" "" "" (map (pr_typ (INFX (2, X))) tys)
   1.764                    ];
   1.765 @@ -952,29 +965,29 @@
   1.766              val (ps, p) = split_last
   1.767                (pr_data "type" data :: map (pr_data "and") datas');
   1.768            in Pretty.chunks (ps @ [Pretty.block ([p, str ";;"])]) end
   1.769 -     | pr_def (MLClass (class, (v, (superclasses, classparams)))) =
   1.770 +     | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) =
   1.771            let
   1.772              val w = "_" ^ first_upper v;
   1.773              fun pr_superclass_field (class, classrel) =
   1.774                (concat o map str) [
   1.775 -                deresolv classrel, ":", "'" ^ v, deresolv class
   1.776 +                deresolve classrel, ":", "'" ^ v, deresolve class
   1.777                ];
   1.778              fun pr_classparam_field (classparam, ty) =
   1.779                concat [
   1.780 -                (str o deresolv) classparam, str ":", pr_typ NOBR ty
   1.781 +                (str o deresolve) classparam, str ":", pr_typ NOBR ty
   1.782                ];
   1.783              fun pr_classparam_proj (classparam, _) =
   1.784                concat [
   1.785                  str "let",
   1.786 -                (str o deresolv) classparam,
   1.787 +                (str o deresolve) classparam,
   1.788                  str w,
   1.789                  str "=",
   1.790 -                str (w ^ "." ^ deresolv classparam ^ ";;")
   1.791 +                str (w ^ "." ^ deresolve classparam ^ ";;")
   1.792                ];
   1.793            in Pretty.chunks (
   1.794              concat [
   1.795                str ("type '" ^ v),
   1.796 -              (str o deresolv) class,
   1.797 +              (str o deresolve) class,
   1.798                str "=",
   1.799                enum_default "();;" ";" "{" "};;" (
   1.800                  map pr_superclass_field superclasses
   1.801 @@ -983,25 +996,25 @@
   1.802              ]
   1.803              :: map pr_classparam_proj classparams
   1.804            ) end
   1.805 -     | pr_def (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) =
   1.806 +     | pr_stmt (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) =
   1.807            let
   1.808              fun pr_superclass (_, (classrel, dss)) =
   1.809                concat [
   1.810 -                (str o deresolv) classrel,
   1.811 +                (str o deresolve) classrel,
   1.812                  str "=",
   1.813                  pr_dicts NOBR [DictConst dss]
   1.814                ];
   1.815              fun pr_classparam_inst (classparam, c_inst) =
   1.816                concat [
   1.817 -                (str o deresolv) classparam,
   1.818 +                (str o deresolve) classparam,
   1.819                  str "=",
   1.820 -                pr_app false init_syms NOBR (c_inst, [])
   1.821 +                pr_app false reserved_names NOBR (c_inst, [])
   1.822                ];
   1.823            in
   1.824              concat (
   1.825                str "let"
   1.826 -              :: (str o deresolv) inst
   1.827 -              :: pr_tyvars arity
   1.828 +              :: (str o deresolve) inst
   1.829 +              :: pr_tyvar_dicts arity
   1.830                @ str "="
   1.831                @@ (Pretty.enclose "(" ");;" o Pretty.breaks) [
   1.832                  enum_default "()" ";" "{" "}" (map pr_superclass superarities
   1.833 @@ -1011,33 +1024,37 @@
   1.834                ]
   1.835              )
   1.836            end;
   1.837 -  in pr_def ml_def end;
   1.838 +  in pr_stmt end;
   1.839 +
   1.840 +fun pr_ocaml_module name content =
   1.841 +  Pretty.chunks (
   1.842 +    str ("module " ^ name ^ " = ")
   1.843 +    :: str "struct"
   1.844 +    :: str ""
   1.845 +    :: content
   1.846 +    @ str ""
   1.847 +    @@ str ("end;; (*struct " ^ name ^ "*)")
   1.848 +  );
   1.849  
   1.850 -fun pr_ocaml_modl name content =
   1.851 -  Pretty.chunks ([
   1.852 -    str ("module " ^ name ^ " = "),
   1.853 -    str "struct",
   1.854 -    str ""
   1.855 -  ] @ content @ [
   1.856 -    str "",
   1.857 -    str ("end;; (*struct " ^ name ^ "*)")
   1.858 -  ]);
   1.859 +local
   1.860 +
   1.861 +datatype ml_node =
   1.862 +    Dummy of string
   1.863 +  | Stmt of string * ml_stmt
   1.864 +  | Module of string * ((Name.context * Name.context) * ml_node Graph.T);
   1.865  
   1.866 -fun seri_ml internal output_cont pr_def pr_modl module labelled_name reserved_syms includes raw_module_alias
   1.867 -  (_ : string -> class_syntax option) tyco_syntax const_syntax code cs seri_dest =
   1.868 +in
   1.869 +
   1.870 +fun ml_node_of_program labelled_name module_name reserved_names raw_module_alias program =
   1.871    let
   1.872 -    val module_alias = if is_some module then K module else raw_module_alias;
   1.873 -    val is_cons = CodeThingol.is_cons code;
   1.874 -    datatype node =
   1.875 -        Def of string * ml_def option
   1.876 -      | Module of string * ((Name.context * Name.context) * node Graph.T);
   1.877 -    val init_names = Name.make_context reserved_syms;
   1.878 -    val init_module = ((init_names, init_names), Graph.empty);
   1.879 +    val module_alias = if is_some module_name then K module_name else raw_module_alias;
   1.880 +    val reserved_names = Name.make_context reserved_names;
   1.881 +    val empty_module = ((reserved_names, reserved_names), Graph.empty);
   1.882      fun map_node [] f = f
   1.883        | map_node (m::ms) f =
   1.884 -          Graph.default_node (m, Module (m, init_module))
   1.885 -          #> Graph.map_node m (fn (Module (dmodlname, (nsp, nodes))) =>
   1.886 -               Module (dmodlname, (nsp, map_node ms f nodes)));
   1.887 +          Graph.default_node (m, Module (m, empty_module))
   1.888 +          #> Graph.map_node m (fn (Module (module_name, (nsp, nodes))) =>
   1.889 +               Module (module_name, (nsp, map_node ms f nodes)));
   1.890      fun map_nsp_yield [] f (nsp, nodes) =
   1.891            let
   1.892              val (x, nsp') = f nsp
   1.893 @@ -1046,193 +1063,202 @@
   1.894            let
   1.895              val (x, nodes') =
   1.896                nodes
   1.897 -              |> Graph.default_node (m, Module (m, init_module))
   1.898 -              |> Graph.map_node_yield m (fn Module (dmodlname, nsp_nodes) => 
   1.899 +              |> Graph.default_node (m, Module (m, empty_module))
   1.900 +              |> Graph.map_node_yield m (fn Module (d_module_name, nsp_nodes) => 
   1.901                    let
   1.902                      val (x, nsp_nodes') = map_nsp_yield ms f nsp_nodes
   1.903 -                  in (x, Module (dmodlname, nsp_nodes')) end)
   1.904 +                  in (x, Module (d_module_name, nsp_nodes')) end)
   1.905            in (x, (nsp, nodes')) end;
   1.906 -    val init_syms = CodeName.make_vars reserved_syms;
   1.907 -    val name_modl = mk_modl_name_tab init_names NONE module_alias code;
   1.908 -    fun name_def upper name nsp =
   1.909 +    fun map_nsp_fun_yield f (nsp_fun, nsp_typ) =
   1.910 +      let
   1.911 +        val (x, nsp_fun') = f nsp_fun
   1.912 +      in (x, (nsp_fun', nsp_typ)) end;
   1.913 +    fun map_nsp_typ_yield f (nsp_fun, nsp_typ) =
   1.914 +      let
   1.915 +        val (x, nsp_typ') = f nsp_typ
   1.916 +      in (x, (nsp_fun, nsp_typ')) end;
   1.917 +    val mk_name_module = mk_name_module reserved_names NONE module_alias program;
   1.918 +    fun mk_name_stmt upper name nsp =
   1.919        let
   1.920          val (_, base) = dest_name name;
   1.921          val base' = if upper then first_upper base else base;
   1.922          val ([base''], nsp') = Name.variants [base'] nsp;
   1.923        in (base'', nsp') end;
   1.924 -    fun map_nsp_fun f (nsp_fun, nsp_typ) =
   1.925 -      let
   1.926 -        val (x, nsp_fun') = f nsp_fun
   1.927 -      in (x, (nsp_fun', nsp_typ)) end;
   1.928 -    fun map_nsp_typ f (nsp_fun, nsp_typ) =
   1.929 -      let
   1.930 -        val (x, nsp_typ') = f nsp_typ
   1.931 -      in (x, (nsp_fun, nsp_typ')) end;
   1.932 -    fun mk_funs defs =
   1.933 +    fun add_funs stmts =
   1.934        fold_map
   1.935 -        (fn (name, CodeThingol.Fun info) =>
   1.936 -              map_nsp_fun (name_def false name) >>
   1.937 -                (fn base => (base, (name, (apsnd o map) fst info)))
   1.938 -          | (name, def) =>
   1.939 +        (fn (name, CodeThingol.Fun stmt) =>
   1.940 +              map_nsp_fun_yield (mk_name_stmt false name) #>>
   1.941 +                rpair (name, (apsnd o map) fst stmt)
   1.942 +          | (name, _) =>
   1.943                error ("Function block containing illegal statement: " ^ labelled_name name)
   1.944 -        ) defs
   1.945 -      >> (split_list #> apsnd MLFuns);
   1.946 -    fun mk_datatype defs =
   1.947 +        ) stmts
   1.948 +      #>> (split_list #> apsnd MLFuns);
   1.949 +    fun add_datatypes stmts =
   1.950        fold_map
   1.951 -        (fn (name, CodeThingol.Datatype info) =>
   1.952 -              map_nsp_typ (name_def false name) >> (fn base => (base, SOME (name, info)))
   1.953 +        (fn (name, CodeThingol.Datatype stmt) =>
   1.954 +              map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, stmt))
   1.955            | (name, CodeThingol.Datatypecons _) =>
   1.956 -              map_nsp_fun (name_def true name) >> (fn base => (base, NONE))
   1.957 -          | (name, def) =>
   1.958 +              map_nsp_fun_yield (mk_name_stmt true name) #>> rpair NONE
   1.959 +          | (name, _) =>
   1.960                error ("Datatype block containing illegal statement: " ^ labelled_name name)
   1.961 -        ) defs
   1.962 -      >> (split_list #> apsnd (map_filter I
   1.963 +        ) stmts
   1.964 +      #>> (split_list #> apsnd (map_filter I
   1.965          #> (fn [] => error ("Datatype block without data statement: "
   1.966 -                  ^ (commas o map (labelled_name o fst)) defs)
   1.967 -             | infos => MLDatas infos)));
   1.968 -    fun mk_class defs =
   1.969 +                  ^ (commas o map (labelled_name o fst)) stmts)
   1.970 +             | stmts => MLDatas stmts)));
   1.971 +    fun add_class stmts =
   1.972        fold_map
   1.973          (fn (name, CodeThingol.Class info) =>
   1.974 -              map_nsp_typ (name_def false name) >> (fn base => (base, SOME (name, info)))
   1.975 +              map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, info))
   1.976            | (name, CodeThingol.Classrel _) =>
   1.977 -              map_nsp_fun (name_def false name) >> (fn base => (base, NONE))
   1.978 +              map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE
   1.979            | (name, CodeThingol.Classparam _) =>
   1.980 -              map_nsp_fun (name_def false name) >> (fn base => (base, NONE))
   1.981 -          | (name, def) =>
   1.982 +              map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE
   1.983 +          | (name, _) =>
   1.984                error ("Class block containing illegal statement: " ^ labelled_name name)
   1.985 -        ) defs
   1.986 -      >> (split_list #> apsnd (map_filter I
   1.987 +        ) stmts
   1.988 +      #>> (split_list #> apsnd (map_filter I
   1.989          #> (fn [] => error ("Class block without class statement: "
   1.990 -                  ^ (commas o map (labelled_name o fst)) defs)
   1.991 -             | [info] => MLClass info)));
   1.992 -    fun mk_inst [(name, CodeThingol.Classinst info)] =
   1.993 -      map_nsp_fun (name_def false name)
   1.994 -      >> (fn base => ([base], MLClassinst (name, (apsnd o apsnd o map) fst info)));
   1.995 -    fun add_group mk defs nsp_nodes =
   1.996 +                  ^ (commas o map (labelled_name o fst)) stmts)
   1.997 +             | [stmt] => MLClass stmt)));
   1.998 +    fun add_inst [(name, CodeThingol.Classinst stmt)] =
   1.999 +      map_nsp_fun_yield (mk_name_stmt false name)
  1.1000 +      #>> (fn base => ([base], MLClassinst (name, (apsnd o apsnd o map) fst stmt)));
  1.1001 +    fun add_stmts ((stmts as (_, CodeThingol.Fun _)::_)) =
  1.1002 +          add_funs stmts
  1.1003 +      | add_stmts ((stmts as (_, CodeThingol.Datatypecons _)::_)) =
  1.1004 +          add_datatypes stmts
  1.1005 +      | add_stmts ((stmts as (_, CodeThingol.Datatype _)::_)) =
  1.1006 +          add_datatypes stmts
  1.1007 +      | add_stmts ((stmts as (_, CodeThingol.Class _)::_)) =
  1.1008 +          add_class stmts
  1.1009 +      | add_stmts ((stmts as (_, CodeThingol.Classrel _)::_)) =
  1.1010 +          add_class stmts
  1.1011 +      | add_stmts ((stmts as (_, CodeThingol.Classparam _)::_)) =
  1.1012 +          add_class stmts
  1.1013 +      | add_stmts ((stmts as [(_, CodeThingol.Classinst _)])) =
  1.1014 +          add_inst stmts
  1.1015 +      | add_stmts stmts = error ("Illegal mutual dependencies: " ^
  1.1016 +          (commas o map (labelled_name o fst)) stmts);
  1.1017 +    fun add_stmts' stmts nsp_nodes =
  1.1018        let
  1.1019 -        val names as (name :: names') = map fst defs;
  1.1020 +        val names as (name :: names') = map fst stmts;
  1.1021          val deps =
  1.1022            []
  1.1023 -          |> fold (fold (insert (op =)) o Graph.imm_succs code) names
  1.1024 +          |> fold (fold (insert (op =)) o Graph.imm_succs program) names
  1.1025            |> subtract (op =) names;
  1.1026 -        val (modls, _) = (split_list o map dest_name) names;
  1.1027 -        val modl' = (the_single o distinct (op =) o map name_modl) modls
  1.1028 +        val (module_names, _) = (split_list o map dest_name) names;
  1.1029 +        val module_name = (the_single o distinct (op =) o map mk_name_module) module_names
  1.1030            handle Empty =>
  1.1031              error ("Different namespace prefixes for mutual dependencies:\n"
  1.1032                ^ commas (map labelled_name names)
  1.1033                ^ "\n"
  1.1034 -              ^ commas (map (NameSpace.qualifier o NameSpace.qualifier) names));
  1.1035 -        val modl_explode = NameSpace.explode modl';
  1.1036 -        fun add_dep name name'' =
  1.1037 +              ^ commas module_names);
  1.1038 +        val module_name_path = NameSpace.explode module_name;
  1.1039 +        fun add_dep name name' =
  1.1040            let
  1.1041 -            val modl'' = (name_modl o fst o dest_name) name'';
  1.1042 -          in if modl' = modl'' then
  1.1043 -            map_node modl_explode
  1.1044 -              (Graph.add_edge (name, name''))
  1.1045 +            val module_name' = (mk_name_module o fst o dest_name) name';
  1.1046 +          in if module_name = module_name' then
  1.1047 +            map_node module_name_path (Graph.add_edge (name, name'))
  1.1048            else let
  1.1049              val (common, (diff1::_, diff2::_)) = chop_prefix (op =)
  1.1050 -              (modl_explode, NameSpace.explode modl'');
  1.1051 +              (module_name_path, NameSpace.explode module_name');
  1.1052            in
  1.1053              map_node common
  1.1054 -              (fn gr => Graph.add_edge_acyclic (diff1, diff2) gr
  1.1055 +              (fn node => Graph.add_edge_acyclic (diff1, diff2) node
  1.1056                  handle Graph.CYCLES _ => error ("Dependency "
  1.1057 -                  ^ quote name ^ " -> " ^ quote name''
  1.1058 +                  ^ quote name ^ " -> " ^ quote name'
  1.1059                    ^ " would result in module dependency cycle"))
  1.1060            end end;
  1.1061        in
  1.1062          nsp_nodes
  1.1063 -        |> map_nsp_yield modl_explode (mk defs)
  1.1064 -        |-> (fn (base' :: bases', def') =>
  1.1065 -           apsnd (map_node modl_explode (Graph.new_node (name, (Def (base', SOME def')))
  1.1066 +        |> map_nsp_yield module_name_path (add_stmts stmts)
  1.1067 +        |-> (fn (base' :: bases', stmt') =>
  1.1068 +           apsnd (map_node module_name_path (Graph.new_node (name, (Stmt (base', stmt')))
  1.1069                #> fold2 (fn name' => fn base' =>
  1.1070 -                   Graph.new_node (name', (Def (base', NONE)))) names' bases')))
  1.1071 +                   Graph.new_node (name', (Dummy base'))) names' bases')))
  1.1072          |> apsnd (fold (fn name => fold (add_dep name) deps) names)
  1.1073 -        |> apsnd (fold_product (curry (map_node modl_explode o Graph.add_edge)) names names)
  1.1074 +        |> apsnd (fold_product (curry (map_node module_name_path o Graph.add_edge)) names names)
  1.1075        end;
  1.1076 -    fun group_defs ((defs as (_, CodeThingol.Fun _)::_)) =
  1.1077 -          add_group mk_funs defs
  1.1078 -      | group_defs ((defs as (_, CodeThingol.Datatypecons _)::_)) =
  1.1079 -          add_group mk_datatype defs
  1.1080 -      | group_defs ((defs as (_, CodeThingol.Datatype _)::_)) =
  1.1081 -          add_group mk_datatype defs
  1.1082 -      | group_defs ((defs as (_, CodeThingol.Class _)::_)) =
  1.1083 -          add_group mk_class defs
  1.1084 -      | group_defs ((defs as (_, CodeThingol.Classrel _)::_)) =
  1.1085 -          add_group mk_class defs
  1.1086 -      | group_defs ((defs as (_, CodeThingol.Classparam _)::_)) =
  1.1087 -          add_group mk_class defs
  1.1088 -      | group_defs ((defs as [(_, CodeThingol.Classinst _)])) =
  1.1089 -          add_group mk_inst defs
  1.1090 -      | group_defs defs = error ("Illegal mutual dependencies: " ^
  1.1091 -          (commas o map (labelled_name o fst)) defs)
  1.1092 -    val (_, nodes) =
  1.1093 -      init_module
  1.1094 -      |> fold group_defs (map (AList.make (Graph.get_node code))
  1.1095 -          (rev (Graph.strong_conn code)))
  1.1096 +    val (_, nodes) = empty_module
  1.1097 +      |> fold add_stmts' (map (AList.make (Graph.get_node program))
  1.1098 +          (rev (Graph.strong_conn program)));
  1.1099      fun deresolver prefix name = 
  1.1100        let
  1.1101 -        val modl = (fst o dest_name) name;
  1.1102 -        val modl' = (NameSpace.explode o name_modl) modl;
  1.1103 -        val (_, (_, remainder)) = chop_prefix (op =) (prefix, modl');
  1.1104 -        val defname' =
  1.1105 +        val module_name = (fst o dest_name) name;
  1.1106 +        val module_name' = (NameSpace.explode o mk_name_module) module_name;
  1.1107 +        val (_, (_, remainder)) = chop_prefix (op =) (prefix, module_name');
  1.1108 +        val stmt_name =
  1.1109            nodes
  1.1110 -          |> fold (fn m => fn g => case Graph.get_node g m
  1.1111 -              of Module (_, (_, g)) => g) modl'
  1.1112 -          |> (fn g => case Graph.get_node g name of Def (defname, _) => defname);
  1.1113 +          |> fold (fn name => fn node => case Graph.get_node node name
  1.1114 +              of Module (_, (_, node)) => node) module_name'
  1.1115 +          |> (fn node => case Graph.get_node node name of Stmt (stmt_name, _) => stmt_name
  1.1116 +               | Dummy stmt_name => stmt_name);
  1.1117        in
  1.1118 -        NameSpace.implode (remainder @ [defname'])
  1.1119 +        NameSpace.implode (remainder @ [stmt_name])
  1.1120        end handle Graph.UNDEF _ =>
  1.1121          error ("Unknown statement name: " ^ labelled_name name);
  1.1122 -    fun pr_node prefix (Def (_, NONE)) =
  1.1123 +  in (deresolver, nodes) end;
  1.1124 +
  1.1125 +fun serialize_ml compile pr_module pr_stmt projection module_name labelled_name reserved_names includes raw_module_alias
  1.1126 +  _ syntax_tyco syntax_const program cs destination =
  1.1127 +  let
  1.1128 +    val is_cons = CodeThingol.is_cons program;
  1.1129 +    val (deresolver, nodes) = ml_node_of_program labelled_name module_name
  1.1130 +      reserved_names raw_module_alias program;
  1.1131 +    val reserved_names = CodeName.make_vars reserved_names;
  1.1132 +    fun pr_node prefix (Dummy _) =
  1.1133            NONE
  1.1134 -      | pr_node prefix (Def (_, SOME def)) =
  1.1135 -          SOME (pr_def tyco_syntax const_syntax labelled_name init_syms
  1.1136 +      | pr_node prefix (Stmt (_, def)) =
  1.1137 +          SOME (pr_stmt syntax_tyco syntax_const labelled_name reserved_names
  1.1138              (deresolver prefix) is_cons def)
  1.1139 -      | pr_node prefix (Module (dmodlname, (_, nodes))) =
  1.1140 -          SOME (pr_modl dmodlname (
  1.1141 +      | pr_node prefix (Module (module_name, (_, nodes))) =
  1.1142 +          SOME (pr_module module_name (
  1.1143              separate (str "")
  1.1144 -                ((map_filter (pr_node (prefix @ [dmodlname]) o Graph.get_node nodes)
  1.1145 +                ((map_filter (pr_node (prefix @ [module_name]) o Graph.get_node nodes)
  1.1146                  o rev o flat o Graph.strong_conn) nodes)));
  1.1147 +    val cs' = map_filter (try (deresolver (if is_some module_name then the_list module_name else [])))
  1.1148 +      cs;
  1.1149      val p = Pretty.chunks (separate (str "") (map snd includes @ (map_filter
  1.1150        (pr_node [] o Graph.get_node nodes) o rev o flat o Graph.strong_conn) nodes));
  1.1151 -    val deresolv = try (deresolver (if is_some module then the_list module else []));
  1.1152 -    val output = case seri_dest
  1.1153 -     of Compile => K NONE o internal o target_code_of_pretty
  1.1154 -      | Write => K NONE o target_code_writeln
  1.1155 -      | File file => K NONE o File.write file o target_code_of_pretty
  1.1156 -      | String => SOME o target_code_of_pretty;
  1.1157 -  in output_cont (map_filter deresolv cs, output p) end;
  1.1158 +    fun output Compile = K NONE o compile o code_of_pretty
  1.1159 +      | output Write = K NONE o code_writeln
  1.1160 +      | output (File file) = K NONE o File.write file o code_of_pretty
  1.1161 +      | output String = SOME o code_of_pretty;
  1.1162 +  in projection (output destination p) cs' end;
  1.1163 +
  1.1164 +end; (*local*)
  1.1165  
  1.1166 -fun isar_seri_sml module =
  1.1167 +fun isar_seri_sml module_name =
  1.1168    parse_args (Scan.succeed ())
  1.1169 -  #> (fn () => seri_ml (use_text (1, "generated code") Output.ml_output false) snd pr_sml pr_sml_modl module);
  1.1170 +  #> (fn () => serialize_ml (use_text (1, "generated code") Output.ml_output false)
  1.1171 +      pr_sml_module pr_sml_stmt K module_name);
  1.1172  
  1.1173 -fun isar_seri_ocaml module =
  1.1174 +fun isar_seri_ocaml module_name =
  1.1175    parse_args (Scan.succeed ())
  1.1176 -  #> (fn () => seri_ml (fn _ => error "OCaml: no internal compilation") snd pr_ocaml pr_ocaml_modl module)
  1.1177 +  #> (fn () => serialize_ml (fn _ => error "OCaml: no internal compilation")
  1.1178 +      pr_ocaml_module pr_ocaml_stmt K module_name);
  1.1179  
  1.1180  
  1.1181  (** Haskell serializer **)
  1.1182  
  1.1183 -local
  1.1184 -
  1.1185 -fun pr_bind' ((NONE, NONE), _) = str "_"
  1.1186 -  | pr_bind' ((SOME v, NONE), _) = str v
  1.1187 -  | pr_bind' ((NONE, SOME p), _) = p
  1.1188 -  | pr_bind' ((SOME v, SOME p), _) = brackets [str v, str "@", p]
  1.1189 -
  1.1190 -val pr_bind_haskell = gen_pr_bind pr_bind';
  1.1191 +val pr_haskell_bind =
  1.1192 +  let
  1.1193 +    fun pr_bind ((NONE, NONE), _) = str "_"
  1.1194 +      | pr_bind ((SOME v, NONE), _) = str v
  1.1195 +      | pr_bind ((NONE, SOME p), _) = p
  1.1196 +      | pr_bind ((SOME v, SOME p), _) = brackets [str v, str "@", p];
  1.1197 +  in gen_pr_bind pr_bind end;
  1.1198  
  1.1199 -in
  1.1200 -
  1.1201 -fun pr_haskell class_syntax tyco_syntax const_syntax labelled_name
  1.1202 -    init_syms deresolv_here deresolv is_cons contr_classparam_typs deriving_show def =
  1.1203 +fun pr_haskell_stmt syntax_class syntax_tyco syntax_const labelled_name
  1.1204 +    init_syms deresolve is_cons contr_classparam_typs deriving_show =
  1.1205    let
  1.1206 -    fun class_name class = case class_syntax class
  1.1207 -     of NONE => deresolv class
  1.1208 +    val deresolve_base = NameSpace.base o deresolve;
  1.1209 +    fun class_name class = case syntax_class class
  1.1210 +     of NONE => deresolve class
  1.1211        | SOME (class, _) => class;
  1.1212 -    fun classparam_name class classparam = case class_syntax class
  1.1213 -     of NONE => deresolv_here classparam
  1.1214 +    fun classparam_name class classparam = case syntax_class class
  1.1215 +     of NONE => deresolve_base classparam
  1.1216        | SOME (_, classparam_syntax) => case classparam_syntax classparam
  1.1217           of NONE => (snd o dest_name) classparam
  1.1218            | SOME classparam => classparam;
  1.1219 @@ -1249,9 +1275,9 @@
  1.1220      fun pr_tycoexpr tyvars fxy (tyco, tys) =
  1.1221        brackify fxy (str tyco :: map (pr_typ tyvars BR) tys)
  1.1222      and pr_typ tyvars fxy (tycoexpr as tyco `%% tys) =
  1.1223 -          (case tyco_syntax tyco
  1.1224 +          (case syntax_tyco tyco
  1.1225             of NONE =>
  1.1226 -                pr_tycoexpr tyvars fxy (deresolv tyco, tys)
  1.1227 +                pr_tycoexpr tyvars fxy (deresolve tyco, tys)
  1.1228              | SOME (i, pr) =>
  1.1229                  if not (i = length tys)
  1.1230                  then error ("Number of argument mismatch in customary serialization: "
  1.1231 @@ -1284,12 +1310,12 @@
  1.1232            in brackets (str "\\" :: ps @ str "->" @@ pr_term tyvars lhs vars' NOBR t') end
  1.1233        | pr_term tyvars lhs vars fxy (ICase (cases as (_, t0))) =
  1.1234            (case CodeThingol.unfold_const_app t0
  1.1235 -           of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
  1.1236 +           of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
  1.1237                  then pr_case tyvars vars fxy cases
  1.1238                  else pr_app tyvars lhs vars fxy c_ts
  1.1239              | NONE => pr_case tyvars vars fxy cases)
  1.1240      and pr_app' tyvars lhs vars ((c, (_, tys)), ts) = case contr_classparam_typs c
  1.1241 -     of [] => (str o deresolv) c :: map (pr_term tyvars lhs vars BR) ts
  1.1242 +     of [] => (str o deresolve) c :: map (pr_term tyvars lhs vars BR) ts
  1.1243        | fingerprint => let
  1.1244            val ts_fingerprint = ts ~~ curry Library.take (length ts) fingerprint;
  1.1245            val needs_annotation = forall (fn (_, NONE) => true | (t, SOME _) =>
  1.1246 @@ -1299,12 +1325,12 @@
  1.1247                  brackets [pr_term tyvars lhs vars NOBR t, str "::", pr_typ tyvars NOBR ty];
  1.1248          in
  1.1249            if needs_annotation then
  1.1250 -            (str o deresolv) c :: map2 pr_term_anno ts_fingerprint (curry Library.take (length ts) tys)
  1.1251 -          else (str o deresolv) c :: map (pr_term tyvars lhs vars BR) ts
  1.1252 +            (str o deresolve) c :: map2 pr_term_anno ts_fingerprint (curry Library.take (length ts) tys)
  1.1253 +          else (str o deresolve) c :: map (pr_term tyvars lhs vars BR) ts
  1.1254          end
  1.1255 -    and pr_app tyvars lhs vars  = gen_pr_app (pr_app' tyvars) (pr_term tyvars) const_syntax
  1.1256 +    and pr_app tyvars lhs vars  = gen_pr_app (pr_app' tyvars) (pr_term tyvars) syntax_const
  1.1257        labelled_name is_cons lhs vars
  1.1258 -    and pr_bind tyvars = pr_bind_haskell (pr_term tyvars)
  1.1259 +    and pr_bind tyvars = pr_haskell_bind (pr_term tyvars)
  1.1260      and pr_case tyvars vars fxy (cases as ((_, [_]), _)) =
  1.1261            let
  1.1262              val (binds, t) = CodeThingol.unfold_let (ICase cases);
  1.1263 @@ -1332,20 +1358,20 @@
  1.1264              ) (map pr bs)
  1.1265            end
  1.1266        | pr_case tyvars vars fxy ((_, []), _) = str "error \"empty case\"";
  1.1267 -    fun pr_def (name, CodeThingol.Fun ((vs, ty), [])) =
  1.1268 +    fun pr_stmt (name, CodeThingol.Fun ((vs, ty), [])) =
  1.1269            let
  1.1270              val tyvars = CodeName.intro_vars (map fst vs) init_syms;
  1.1271              val n = (length o fst o CodeThingol.unfold_fun) ty;
  1.1272            in
  1.1273              Pretty.chunks [
  1.1274                Pretty.block [
  1.1275 -                (str o suffix " ::" o deresolv_here) name,
  1.1276 +                (str o suffix " ::" o deresolve_base) name,
  1.1277                  Pretty.brk 1,
  1.1278                  pr_typscheme tyvars (vs, ty),
  1.1279                  str ";"
  1.1280                ],
  1.1281                concat (
  1.1282 -                (str o deresolv_here) name
  1.1283 +                (str o deresolve_base) name
  1.1284                  :: map str (replicate n "_")
  1.1285                  @ str "="
  1.1286                  :: str "error"
  1.1287 @@ -1354,14 +1380,14 @@
  1.1288                )
  1.1289              ]
  1.1290            end
  1.1291 -      | pr_def (name, CodeThingol.Fun ((vs, ty), eqs)) =
  1.1292 +      | pr_stmt (name, CodeThingol.Fun ((vs, ty), eqs)) =
  1.1293            let
  1.1294              val tyvars = CodeName.intro_vars (map fst vs) init_syms;
  1.1295              fun pr_eq ((ts, t), _) =
  1.1296                let
  1.1297                  val consts = map_filter
  1.1298 -                  (fn c => if (is_some o const_syntax) c
  1.1299 -                    then NONE else (SOME o NameSpace.base o deresolv) c)
  1.1300 +                  (fn c => if (is_some o syntax_const) c
  1.1301 +                    then NONE else (SOME o NameSpace.base o deresolve) c)
  1.1302                      ((fold o CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []);
  1.1303                  val vars = init_syms
  1.1304                    |> CodeName.intro_vars consts
  1.1305 @@ -1369,7 +1395,7 @@
  1.1306                         (insert (op =)) ts []);
  1.1307                in
  1.1308                  semicolon (
  1.1309 -                  (str o deresolv_here) name
  1.1310 +                  (str o deresolve_base) name
  1.1311                    :: map (pr_term tyvars true vars BR) ts
  1.1312                    @ str "="
  1.1313                    @@ pr_term tyvars false vars NOBR t
  1.1314 @@ -1378,7 +1404,7 @@
  1.1315            in
  1.1316              Pretty.chunks (
  1.1317                Pretty.block [
  1.1318 -                (str o suffix " ::" o deresolv_here) name,
  1.1319 +                (str o suffix " ::" o deresolve_base) name,
  1.1320                  Pretty.brk 1,
  1.1321                  pr_typscheme tyvars (vs, ty),
  1.1322                  str ";"
  1.1323 @@ -1386,47 +1412,47 @@
  1.1324                :: map pr_eq eqs
  1.1325              )
  1.1326            end
  1.1327 -      | pr_def (name, CodeThingol.Datatype (vs, [])) =
  1.1328 +      | pr_stmt (name, CodeThingol.Datatype (vs, [])) =
  1.1329            let
  1.1330              val tyvars = CodeName.intro_vars (map fst vs) init_syms;
  1.1331            in
  1.1332              semicolon [
  1.1333                str "data",
  1.1334 -              pr_typdecl tyvars (vs, (deresolv_here name, map (ITyVar o fst) vs))
  1.1335 +              pr_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs))
  1.1336              ]
  1.1337            end
  1.1338 -      | pr_def (name, CodeThingol.Datatype (vs, [(co, [ty])])) =
  1.1339 +      | pr_stmt (name, CodeThingol.Datatype (vs, [(co, [ty])])) =
  1.1340            let
  1.1341              val tyvars = CodeName.intro_vars (map fst vs) init_syms;
  1.1342            in
  1.1343              semicolon (
  1.1344                str "newtype"
  1.1345 -              :: pr_typdecl tyvars (vs, (deresolv_here name, map (ITyVar o fst) vs))
  1.1346 +              :: pr_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs))
  1.1347                :: str "="
  1.1348 -              :: (str o deresolv_here) co
  1.1349 +              :: (str o deresolve_base) co
  1.1350                :: pr_typ tyvars BR ty
  1.1351                :: (if deriving_show name then [str "deriving (Read, Show)"] else [])
  1.1352              )
  1.1353            end
  1.1354 -      | pr_def (name, CodeThingol.Datatype (vs, co :: cos)) =
  1.1355 +      | pr_stmt (name, CodeThingol.Datatype (vs, co :: cos)) =
  1.1356            let
  1.1357              val tyvars = CodeName.intro_vars (map fst vs) init_syms;
  1.1358              fun pr_co (co, tys) =
  1.1359                concat (
  1.1360 -                (str o deresolv_here) co
  1.1361 +                (str o deresolve_base) co
  1.1362                  :: map (pr_typ tyvars BR) tys
  1.1363                )
  1.1364            in
  1.1365              semicolon (
  1.1366                str "data"
  1.1367 -              :: pr_typdecl tyvars (vs, (deresolv_here name, map (ITyVar o fst) vs))
  1.1368 +              :: pr_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs))
  1.1369                :: str "="
  1.1370                :: pr_co co
  1.1371                :: map ((fn p => Pretty.block [str "| ", p]) o pr_co) cos
  1.1372                @ (if deriving_show name then [str "deriving (Read, Show)"] else [])
  1.1373              )
  1.1374            end
  1.1375 -      | pr_def (name, CodeThingol.Class (v, (superclasses, classparams))) =
  1.1376 +      | pr_stmt (name, CodeThingol.Class (v, (superclasses, classparams))) =
  1.1377            let
  1.1378              val tyvars = CodeName.intro_vars [v] init_syms;
  1.1379              fun pr_classparam (classparam, ty) =
  1.1380 @@ -1440,13 +1466,13 @@
  1.1381                Pretty.block [
  1.1382                  str "class ",
  1.1383                  Pretty.block (pr_typcontext tyvars [(v, map fst superclasses)]),
  1.1384 -                str (deresolv_here name ^ " " ^ CodeName.lookup_var tyvars v),
  1.1385 +                str (deresolve_base name ^ " " ^ CodeName.lookup_var tyvars v),
  1.1386                  str " where {"
  1.1387                ],
  1.1388                str "};"
  1.1389              ) (map pr_classparam classparams)
  1.1390            end
  1.1391 -      | pr_def (_, CodeThingol.Classinst ((class, (tyco, vs)), (_, classparam_insts))) =
  1.1392 +      | pr_stmt (_, CodeThingol.Classinst ((class, (tyco, vs)), (_, classparam_insts))) =
  1.1393            let
  1.1394              val tyvars = CodeName.intro_vars (map fst vs) init_syms;
  1.1395              fun pr_instdef ((classparam, c_inst), _) =
  1.1396 @@ -1467,13 +1493,13 @@
  1.1397                str "};"
  1.1398              ) (map pr_instdef classparam_insts)
  1.1399            end;
  1.1400 -  in pr_def def end;
  1.1401 +  in pr_stmt end;
  1.1402  
  1.1403  fun pretty_haskell_monad c_bind =
  1.1404    let
  1.1405      fun pretty pr vars fxy [(t, _)] =
  1.1406        let
  1.1407 -        val pr_bind = pr_bind_haskell (K pr);
  1.1408 +        val pr_bind = pr_haskell_bind (K pr);
  1.1409          fun pr_monad (NONE, t) vars =
  1.1410                (semicolon [pr vars NOBR t], vars)
  1.1411            | pr_monad (SOME (bind, true), t) vars = vars
  1.1412 @@ -1488,74 +1514,70 @@
  1.1413        in (brack o Pretty.block_enclose (str "do {", str "}")) (ps @| pr vars' NOBR t) end;
  1.1414    in (1, pretty) end;
  1.1415  
  1.1416 -end; (*local*)
  1.1417 -
  1.1418 -fun seri_haskell module_prefix module string_classes labelled_name
  1.1419 -    reserved_syms includes raw_module_alias
  1.1420 -    class_syntax tyco_syntax const_syntax code cs seri_dest =
  1.1421 +fun haskell_program_of_program labelled_name module_name module_prefix reserved_names raw_module_alias program =
  1.1422    let
  1.1423 -    val is_cons = CodeThingol.is_cons code;
  1.1424 -    val contr_classparam_typs = CodeThingol.contr_classparam_typs code;
  1.1425 -    val module_alias = if is_some module then K module else raw_module_alias;
  1.1426 -    val init_names = Name.make_context reserved_syms;
  1.1427 -    val name_modl = mk_modl_name_tab init_names module_prefix module_alias code;
  1.1428 -    fun add_def (name, (def, deps)) =
  1.1429 +    val module_alias = if is_some module_name then K module_name else raw_module_alias;
  1.1430 +    val reserved_names = Name.make_context reserved_names;
  1.1431 +    val mk_name_module = mk_name_module reserved_names module_prefix module_alias program;
  1.1432 +    fun add_stmt (name, (stmt, deps)) =
  1.1433        let
  1.1434 -        val (modl, base) = dest_name name;
  1.1435 -        val name_def = yield_singleton Name.variants;
  1.1436 +        val (module_name, base) = dest_name name;
  1.1437 +        val module_name' = mk_name_module module_name;
  1.1438 +        val mk_name_stmt = yield_singleton Name.variants;
  1.1439          fun add_fun upper (nsp_fun, nsp_typ) =
  1.1440            let
  1.1441              val (base', nsp_fun') =
  1.1442 -              name_def (if upper then first_upper base else base) nsp_fun
  1.1443 +              mk_name_stmt (if upper then first_upper base else base) nsp_fun
  1.1444            in (base', (nsp_fun', nsp_typ)) end;
  1.1445          fun add_typ (nsp_fun, nsp_typ) =
  1.1446            let
  1.1447 -            val (base', nsp_typ') = name_def (first_upper base) nsp_typ
  1.1448 +            val (base', nsp_typ') = mk_name_stmt (first_upper base) nsp_typ
  1.1449            in (base', (nsp_fun, nsp_typ')) end;
  1.1450 -        val add_name =
  1.1451 -          case def
  1.1452 -           of CodeThingol.Fun _ => add_fun false
  1.1453 -            | CodeThingol.Datatype _ => add_typ
  1.1454 -            | CodeThingol.Datatypecons _ => add_fun true
  1.1455 -            | CodeThingol.Class _ => add_typ
  1.1456 -            | CodeThingol.Classrel _ => pair base
  1.1457 -            | CodeThingol.Classparam _ => add_fun false
  1.1458 -            | CodeThingol.Classinst _ => pair base;
  1.1459 -        val modlname' = name_modl modl;
  1.1460 -        fun add_def base' =
  1.1461 -          case def
  1.1462 -           of CodeThingol.Datatypecons _ =>
  1.1463 -                cons (name, ((NameSpace.append modlname' base', base'), NONE))
  1.1464 -            | CodeThingol.Classrel _ => I
  1.1465 -            | CodeThingol.Classparam _ =>
  1.1466 -                cons (name, ((NameSpace.append modlname' base', base'), NONE))
  1.1467 -            | _ => cons (name, ((NameSpace.append modlname' base', base'), SOME def));
  1.1468 +        val add_name = case stmt
  1.1469 +         of CodeThingol.Fun _ => add_fun false
  1.1470 +          | CodeThingol.Datatype _ => add_typ
  1.1471 +          | CodeThingol.Datatypecons _ => add_fun true
  1.1472 +          | CodeThingol.Class _ => add_typ
  1.1473 +          | CodeThingol.Classrel _ => pair base
  1.1474 +          | CodeThingol.Classparam _ => add_fun false
  1.1475 +          | CodeThingol.Classinst _ => pair base;
  1.1476 +        fun add_stmt' base' = case stmt
  1.1477 +         of CodeThingol.Datatypecons _ =>
  1.1478 +              cons (name, (NameSpace.append module_name' base', NONE))
  1.1479 +          | CodeThingol.Classrel _ => I
  1.1480 +          | CodeThingol.Classparam _ =>
  1.1481 +              cons (name, (NameSpace.append module_name' base', NONE))
  1.1482 +          | _ => cons (name, (NameSpace.append module_name' base', SOME stmt));
  1.1483        in
  1.1484 -        Symtab.map_default (modlname', ([], ([], (init_names, init_names))))
  1.1485 +        Symtab.map_default (module_name', ([], ([], (reserved_names, reserved_names))))
  1.1486                (apfst (fold (insert (op = : string * string -> bool)) deps))
  1.1487 -        #> `(fn code => add_name ((snd o snd o the o Symtab.lookup code) modlname'))
  1.1488 +        #> `(fn program => add_name ((snd o snd o the o Symtab.lookup program) module_name'))
  1.1489          #-> (fn (base', names) =>
  1.1490 -              (Symtab.map_entry modlname' o apsnd) (fn (defs, _) =>
  1.1491 -              (add_def base' defs, names)))
  1.1492 +              (Symtab.map_entry module_name' o apsnd) (fn (stmts, _) =>
  1.1493 +              (add_stmt' base' stmts, names)))
  1.1494        end;
  1.1495 -    val code' =
  1.1496 -      fold add_def (AList.make (fn name =>
  1.1497 -        (Graph.get_node code name, Graph.imm_succs code name))
  1.1498 -        (Graph.strong_conn code |> flat)) Symtab.empty;
  1.1499 -    val init_syms = CodeName.make_vars reserved_syms;
  1.1500 -    fun deresolv name =
  1.1501 -      (fst o fst o the o AList.lookup (op =) ((fst o snd o the
  1.1502 -        o Symtab.lookup code') ((name_modl o fst o dest_name) name))) name
  1.1503 +    val hs_program = fold add_stmt (AList.make (fn name =>
  1.1504 +      (Graph.get_node program name, Graph.imm_succs program name))
  1.1505 +      (Graph.strong_conn program |> flat)) Symtab.empty;
  1.1506 +    fun deresolver name =
  1.1507 +      (fst o the o AList.lookup (op =) ((fst o snd o the
  1.1508 +        o Symtab.lookup hs_program) ((mk_name_module o fst o dest_name) name))) name
  1.1509          handle Option => error ("Unknown statement name: " ^ labelled_name name);
  1.1510 -    fun deresolv_here name =
  1.1511 -      (snd o fst o the o AList.lookup (op =) ((fst o snd o the
  1.1512 -        o Symtab.lookup code') ((name_modl o fst o dest_name) name))) name
  1.1513 -        handle Option => error ("Unknown statement name: " ^ labelled_name name);
  1.1514 +  in (deresolver, hs_program) end;
  1.1515 +
  1.1516 +fun serialize_haskell module_prefix module_name string_classes labelled_name
  1.1517 +    reserved_names includes raw_module_alias
  1.1518 +    syntax_class syntax_tyco syntax_const program cs destination =
  1.1519 +  let
  1.1520 +    val (deresolver, hs_program) = haskell_program_of_program labelled_name
  1.1521 +      module_name module_prefix reserved_names raw_module_alias program;
  1.1522 +    val is_cons = CodeThingol.is_cons program;
  1.1523 +    val contr_classparam_typs = CodeThingol.contr_classparam_typs program;
  1.1524      fun deriving_show tyco =
  1.1525        let
  1.1526          fun deriv _ "fun" = false
  1.1527            | deriv tycos tyco = member (op =) tycos tyco orelse
  1.1528 -              case try (Graph.get_node code) tyco
  1.1529 +              case try (Graph.get_node program) tyco
  1.1530                  of SOME (CodeThingol.Datatype (_, cs)) => forall (deriv' (tyco :: tycos))
  1.1531                      (maps snd cs)
  1.1532                   | NONE => true
  1.1533 @@ -1563,45 +1585,46 @@
  1.1534                andalso forall (deriv' tycos) tys
  1.1535            | deriv' _ (ITyVar _) = true
  1.1536        in deriv [] tyco end;
  1.1537 -    fun seri_def qualified = pr_haskell class_syntax tyco_syntax
  1.1538 -      const_syntax labelled_name init_syms
  1.1539 -      deresolv_here (if qualified then deresolv else deresolv_here) is_cons
  1.1540 -      contr_classparam_typs
  1.1541 +    val reserved_names = CodeName.make_vars reserved_names;
  1.1542 +    fun pr_stmt qualified = pr_haskell_stmt syntax_class syntax_tyco
  1.1543 +      syntax_const labelled_name reserved_names
  1.1544 +      (if qualified then deresolver else NameSpace.base o deresolver)
  1.1545 +      is_cons contr_classparam_typs
  1.1546        (if string_classes then deriving_show else K false);
  1.1547 -    fun assemble_module (modulename, content) =
  1.1548 -      (modulename, Pretty.chunks [
  1.1549 -        str ("module " ^ modulename ^ " where {"),
  1.1550 +    fun pr_module name content =
  1.1551 +      (name, Pretty.chunks [
  1.1552 +        str ("module " ^ name ^ " where {"),
  1.1553          str "",
  1.1554          content,
  1.1555          str "",
  1.1556          str "}"
  1.1557        ]);
  1.1558 -    fun seri_module (modlname', (imports, (defs, _))) =
  1.1559 +    fun serialize_module (module_name', (deps, (stmts, _))) =
  1.1560        let
  1.1561 -        val imports' =
  1.1562 -          imports
  1.1563 -          |> map (name_modl o fst o dest_name)
  1.1564 +        val stmt_names = map fst stmts;
  1.1565 +        val deps' = subtract (op =) stmt_names deps
  1.1566            |> distinct (op =)
  1.1567 -          |> remove (op =) modlname';
  1.1568 -        val qualified = is_none module andalso
  1.1569 -          imports @ map fst defs
  1.1570 -          |> distinct (op =)
  1.1571 -          |> map_filter (try deresolv)
  1.1572 +          |> map_filter (try deresolver);
  1.1573 +        val qualified = is_none module_name andalso
  1.1574 +          map deresolver stmt_names @ deps'
  1.1575            |> map NameSpace.base
  1.1576            |> has_duplicates (op =);
  1.1577 -        val mk_import = str o (if qualified
  1.1578 +        val imports = deps'
  1.1579 +          |> map NameSpace.qualifier
  1.1580 +          |> distinct (op =);
  1.1581 +        fun pr_import_include (name, _) = str ("import " ^ name ^ ";");
  1.1582 +        val pr_import_module = str o (if qualified
  1.1583            then prefix "import qualified "
  1.1584            else prefix "import ") o suffix ";";
  1.1585 -        fun import_include (name, _) = str ("import " ^ name ^ ";");
  1.1586          val content = Pretty.chunks (
  1.1587 -            map mk_import imports'
  1.1588 -            @ map import_include includes
  1.1589 +            map pr_import_include includes
  1.1590 +            @ map pr_import_module imports
  1.1591              @ str ""
  1.1592              :: separate (str "") (map_filter
  1.1593 -              (fn (name, (_, SOME def)) => SOME (seri_def qualified (name, def))
  1.1594 -                | (_, (_, NONE)) => NONE) defs)
  1.1595 +              (fn (name, (_, SOME stmt)) => SOME (pr_stmt qualified (name, stmt))
  1.1596 +                | (_, (_, NONE)) => NONE) stmts)
  1.1597            )
  1.1598 -      in assemble_module (modlname', content) end;
  1.1599 +      in pr_module module_name' content end;
  1.1600      fun write_module destination (modlname, content) =
  1.1601        let
  1.1602          val filename = case modlname
  1.1603 @@ -1610,46 +1633,21 @@
  1.1604                  o NameSpace.explode) modlname;
  1.1605          val pathname = Path.append destination filename;
  1.1606          val _ = File.mkdir (Path.dir pathname);
  1.1607 -      in File.write pathname (target_code_of_pretty content) end
  1.1608 -    val output = case seri_dest
  1.1609 -     of Compile => error ("Haskell: no internal compilation")
  1.1610 -      | Write => K NONE o map (target_code_writeln o snd)
  1.1611 -      | File destination => K NONE o map (write_module destination)
  1.1612 -      | String => SOME o cat_lines o map (target_code_of_pretty o snd);
  1.1613 -  in output (map assemble_module includes
  1.1614 -    @ map seri_module (Symtab.dest code'))
  1.1615 +      in File.write pathname (code_of_pretty content) end
  1.1616 +    fun output Compile = error ("Haskell: no internal compilation")
  1.1617 +      | output Write = K NONE o map (code_writeln o snd)
  1.1618 +      | output (File destination) = K NONE o map (write_module destination)
  1.1619 +      | output String = SOME o cat_lines o map (code_of_pretty o snd);
  1.1620 +  in
  1.1621 +    output destination (map (uncurry pr_module) includes
  1.1622 +      @ map serialize_module (Symtab.dest hs_program))
  1.1623    end;
  1.1624  
  1.1625  fun isar_seri_haskell module =
  1.1626    parse_args (Scan.option (Args.$$$ "root" -- Args.colon |-- Args.name)
  1.1627      -- Scan.optional (Args.$$$ "string_classes" >> K true) false
  1.1628      >> (fn (module_prefix, string_classes) =>
  1.1629 -      seri_haskell module_prefix module string_classes));
  1.1630 -
  1.1631 -
  1.1632 -(** diagnosis serializer **)
  1.1633 -
  1.1634 -fun seri_diagnosis labelled_name _ _ _ _ _ _ code _ _ =
  1.1635 -  let
  1.1636 -    val init_names = CodeName.make_vars [];
  1.1637 -    fun pr_fun "fun" = SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
  1.1638 -          brackify_infix (1, R) fxy [
  1.1639 -            pr_typ (INFX (1, X)) ty1,
  1.1640 -            str "->",
  1.1641 -            pr_typ (INFX (1, R)) ty2
  1.1642 -          ])
  1.1643 -      | pr_fun _ = NONE
  1.1644 -    val pr = pr_haskell (K NONE) pr_fun (K NONE) labelled_name init_names
  1.1645 -      I I (K false) (K []) (K false);
  1.1646 -  in
  1.1647 -    []
  1.1648 -    |> Graph.fold (fn (name, (def, _)) =>
  1.1649 -          case try pr (name, def) of SOME p => cons p | NONE => I) code
  1.1650 -    |> Pretty.chunks2
  1.1651 -    |> target_code_of_pretty
  1.1652 -    |> writeln
  1.1653 -    |> K NONE
  1.1654 -  end;
  1.1655 +      serialize_haskell module_prefix module string_classes));
  1.1656  
  1.1657  
  1.1658  (** optional pretty serialization **)
  1.1659 @@ -1811,25 +1809,48 @@
  1.1660  end; (*local*)
  1.1661  
  1.1662  
  1.1663 -(** user interfaces **)
  1.1664 +(** serializer interfaces **)
  1.1665  
  1.1666  (* evaluation *)
  1.1667  
  1.1668 -fun eval_seri module args =
  1.1669 -  seri_ml (use_text (1, "generated code") Output.ml_output false)
  1.1670 -    (fn (cs, SOME s) => "let\n" ^ s ^ "\nin fn () => " ^ enclose "(" ")" (commas cs) ^ " end")
  1.1671 -    pr_sml (K Pretty.chunks) (SOME "Isabelle_Eval");
  1.1672 +fun eval_serializer module [] = serialize_ml
  1.1673 +  (use_text (1, "code to be evaluated") Output.ml_output false) 
  1.1674 +  (K Pretty.chunks) pr_sml_stmt
  1.1675 +  (fn SOME s => fn cs => SOME ("let\n" ^ s ^ "\nin fn () => " ^ enclose "(" ")" (commas cs) ^ " end"))
  1.1676 +  (SOME "Isabelle_Eval");
  1.1677  
  1.1678 -fun sml_of thy code cs = get_serializer (K eval_seri) thy target_SML false NONE [] code (SOME cs) String;
  1.1679 +fun sml_code_of thy program cs = mount_serializer thy (SOME eval_serializer) target_SML NONE [] program cs String
  1.1680 +  |> the;
  1.1681  
  1.1682 -fun eval thy (ref_name, reff) code (t, ty) args =
  1.1683 +fun eval eval'' term_of reff thy ct args =
  1.1684    let
  1.1685 -    val _ = if CodeThingol.contains_dictvar t then
  1.1686 -      error "Term to be evaluated constains free dictionaries" else ();
  1.1687 -    val code' = CodeThingol.add_value_stmt (t, ty) code;
  1.1688 -    val value_code = sml_of thy code' [CodeName.value_name] ;
  1.1689 -    val sml_code = space_implode " " (value_code :: "()" :: map (enclose "(" ")") args);
  1.1690 -  in ML_Context.evaluate Output.ml_output false (ref_name, reff) sml_code end;
  1.1691 +    val _ = if null (term_frees (term_of ct)) then () else error ("Term "
  1.1692 +      ^ quote (Syntax.string_of_term_global thy (term_of ct))
  1.1693 +      ^ " to be evaluated contains free variables");
  1.1694 +    fun eval' program ((vs, ty), t) deps =
  1.1695 +      let
  1.1696 +        val _ = if CodeThingol.contains_dictvar t then
  1.1697 +          error "Term to be evaluated constains free dictionaries" else ();
  1.1698 +        val program' = program
  1.1699 +          |> Graph.new_node (CodeName.value_name, CodeThingol.Fun (([], ty), [(([], t), Drule.dummy_thm)]))
  1.1700 +          |> fold (curry Graph.add_edge CodeName.value_name) deps;
  1.1701 +        val value_code = sml_code_of thy program' [CodeName.value_name] ;
  1.1702 +        val sml_code = space_implode " " (value_code :: "()" :: map (enclose "(" ")") args);
  1.1703 +      in ML_Context.evaluate Output.ml_output false reff sml_code end;
  1.1704 +  in eval'' thy (fn t => (t, eval')) ct end;
  1.1705 +
  1.1706 +fun eval_conv reff = eval CodeThingol.eval_conv Thm.term_of reff;
  1.1707 +fun eval_term reff = eval CodeThingol.eval_term I reff;
  1.1708 +
  1.1709 +
  1.1710 +(* presentation *)
  1.1711 +
  1.1712 +fun code_of thy target module_name cs =
  1.1713 +  let
  1.1714 +    val (cs', program) = CodeThingol.consts_program thy cs;
  1.1715 +  in
  1.1716 +    string (serialize thy target (SOME module_name) [] program cs')
  1.1717 +  end;
  1.1718  
  1.1719  
  1.1720  (* infix syntax *)
  1.1721 @@ -1877,11 +1898,7 @@
  1.1722      val _ = AxClass.get_info thy class;
  1.1723    in class end;
  1.1724  
  1.1725 -fun read_class thy raw_class =
  1.1726 -  let
  1.1727 -    val class = Sign.intern_class thy raw_class;
  1.1728 -    val _ = AxClass.get_info thy class;
  1.1729 -  in class end;
  1.1730 +fun read_class thy = cert_class thy o Sign.intern_class thy;
  1.1731  
  1.1732  fun cert_tyco thy tyco =
  1.1733    let
  1.1734 @@ -1889,12 +1906,7 @@
  1.1735        else error ("No such type constructor: " ^ quote tyco);
  1.1736    in tyco end;
  1.1737  
  1.1738 -fun read_tyco thy raw_tyco =
  1.1739 -  let
  1.1740 -    val tyco = Sign.intern_type thy raw_tyco;
  1.1741 -    val _ = if Sign.declared_tyname thy tyco then ()
  1.1742 -      else error ("No such type constructor: " ^ quote raw_tyco);
  1.1743 -  in tyco end;
  1.1744 +fun read_tyco thy = cert_tyco thy o Sign.intern_type thy;
  1.1745  
  1.1746  fun gen_add_syntax_class prep_class prep_const target raw_class raw_syn thy =
  1.1747    let
  1.1748 @@ -1971,7 +1983,7 @@
  1.1749      fun add sym syms = if member (op =) syms sym
  1.1750        then error ("Reserved symbol " ^ quote sym ^ " already declared")
  1.1751        else insert (op =) sym syms
  1.1752 -  in map_adaptions target o apfst o add end;
  1.1753 +  in map_reserved target o add end;
  1.1754  
  1.1755  fun add_include target =
  1.1756    let
  1.1757 @@ -1983,39 +1995,39 @@
  1.1758            in Symtab.update (name, str content) incls end
  1.1759        | add (name, NONE) incls =
  1.1760            Symtab.delete name incls;
  1.1761 -  in map_adaptions target o apsnd o add end;
  1.1762 +  in map_includes target o add end;
  1.1763  
  1.1764 -fun add_modl_alias target =
  1.1765 +fun add_module_alias target =
  1.1766    map_module_alias target o Symtab.update o apsnd CodeName.check_modulename;
  1.1767  
  1.1768 -fun add_monad target c_run c_bind c_return_unit thy =
  1.1769 +fun add_monad target raw_c_run raw_c_bind raw_c_return_unit thy =
  1.1770    let
  1.1771 -    val c_run' = CodeUnit.read_const thy c_run;
  1.1772 -    val c_bind' = CodeUnit.read_const thy c_bind;
  1.1773 -    val c_bind'' = CodeName.const thy c_bind';
  1.1774 -    val c_return_unit'' = (Option.map o pairself)
  1.1775 -      (CodeName.const thy o CodeUnit.read_const thy) c_return_unit;
  1.1776 +    val c_run = CodeUnit.read_const thy raw_c_run;
  1.1777 +    val c_bind = CodeUnit.read_const thy raw_c_bind;
  1.1778 +    val c_bind' = CodeName.const thy c_bind;
  1.1779 +    val c_return_unit' = (Option.map o pairself)
  1.1780 +      (CodeName.const thy o CodeUnit.read_const thy) raw_c_return_unit;
  1.1781      val is_haskell = target = target_Haskell;
  1.1782 -    val _ = if is_haskell andalso is_some c_return_unit''
  1.1783 +    val _ = if is_haskell andalso is_some c_return_unit'
  1.1784        then error ("No unit entry may be given for Haskell monad")
  1.1785        else ();
  1.1786 -    val _ = if not is_haskell andalso is_none c_return_unit''
  1.1787 +    val _ = if not is_haskell andalso is_none c_return_unit'
  1.1788        then error ("Unit entry must be given for SML/OCaml monad")
  1.1789        else ();
  1.1790    in if target = target_Haskell then
  1.1791      thy
  1.1792 -    |> gen_add_syntax_const (K I) target_Haskell c_run'
  1.1793 -          (SOME (pretty_haskell_monad c_bind''))
  1.1794 -    |> gen_add_syntax_const (K I) target_Haskell c_bind'
  1.1795 +    |> gen_add_syntax_const (K I) target_Haskell c_run
  1.1796 +          (SOME (pretty_haskell_monad c_bind'))
  1.1797 +    |> gen_add_syntax_const (K I) target_Haskell c_bind
  1.1798            (no_bindings (SOME (parse_infix fst (L, 1) ">>=")))
  1.1799    else
  1.1800      thy
  1.1801 -    |> gen_add_syntax_const (K I) target c_bind'
  1.1802 -          (SOME (pretty_imperative_monad_bind c_bind''
  1.1803 -            ((fst o the) c_return_unit'') ((snd o the) c_return_unit'')))
  1.1804 +    |> gen_add_syntax_const (K I) target c_bind
  1.1805 +          (SOME (pretty_imperative_monad_bind c_bind'
  1.1806 +            ((fst o the) c_return_unit') ((snd o the) c_return_unit')))
  1.1807    end;
  1.1808  
  1.1809 -fun gen_allow_exception prep_cs raw_c thy =
  1.1810 +fun gen_allow_abort prep_cs raw_c thy =
  1.1811    let
  1.1812      val c = prep_cs thy raw_c;
  1.1813      val c' = CodeName.const thy c;
  1.1814 @@ -2028,7 +2040,7 @@
  1.1815      #-> (fn xys => pair ((x, y) :: xys)));
  1.1816  
  1.1817  
  1.1818 -(* conrete syntax *)
  1.1819 +(* concrete syntax *)
  1.1820  
  1.1821  structure P = OuterParse
  1.1822  and K = OuterKeyword
  1.1823 @@ -2076,13 +2088,13 @@
  1.1824  val add_syntax_inst = gen_add_syntax_inst cert_class cert_tyco;
  1.1825  val add_syntax_tyco = gen_add_syntax_tyco cert_tyco;
  1.1826  val add_syntax_const = gen_add_syntax_const (K I);
  1.1827 -val allow_exception = gen_allow_exception (K I);
  1.1828 +val allow_abort = gen_allow_abort (K I);
  1.1829  
  1.1830  val add_syntax_class_cmd = gen_add_syntax_class read_class CodeUnit.read_const;
  1.1831  val add_syntax_inst_cmd = gen_add_syntax_inst read_class read_tyco;
  1.1832  val add_syntax_tyco_cmd = gen_add_syntax_tyco read_tyco;
  1.1833  val add_syntax_const_cmd = gen_add_syntax_const CodeUnit.read_const;
  1.1834 -val allow_exception_cmd = gen_allow_exception CodeUnit.read_const;
  1.1835 +val allow_abort_cmd = gen_allow_abort CodeUnit.read_const;
  1.1836  
  1.1837  fun add_syntax_tycoP target tyco = parse_syntax I >> add_syntax_tyco_cmd target tyco;
  1.1838  fun add_syntax_constP target c = parse_syntax fst >> (add_syntax_const_cmd target c o no_bindings);
  1.1839 @@ -2152,9 +2164,64 @@
  1.1840    end;
  1.1841  
  1.1842  
  1.1843 -(* Isar commands *)
  1.1844 +(** code generation at a glance **)
  1.1845 +
  1.1846 +fun read_const_exprs thy cs =
  1.1847 +  let
  1.1848 +    val (cs1, cs2) = CodeName.read_const_exprs thy cs;
  1.1849 +    val (cs3, program) = CodeThingol.consts_program thy cs2;
  1.1850 +    val cs4 = CodeThingol.transitivly_non_empty_funs program (abort_allowed thy);
  1.1851 +    val cs5 = map_filter
  1.1852 +      (fn (c, c') => if member (op =) cs4 c' then SOME c else NONE) (cs2 ~~ cs3);
  1.1853 +  in fold (insert (op =)) cs5 cs1 end;
  1.1854 +
  1.1855 +fun cached_program thy = 
  1.1856 +  let
  1.1857 +    val program = CodeThingol.cached_program thy;
  1.1858 +  in (CodeThingol.transitivly_non_empty_funs program (abort_allowed thy), program) end
  1.1859 +
  1.1860 +fun code thy cs seris =
  1.1861 +  let
  1.1862 +    val (cs', program) = if null cs
  1.1863 +      then cached_program thy
  1.1864 +      else CodeThingol.consts_program thy cs;
  1.1865 +    fun mk_seri_dest dest = case dest
  1.1866 +     of NONE => compile
  1.1867 +      | SOME "-" => write
  1.1868 +      | SOME f => file (Path.explode f)
  1.1869 +    val _ = map (fn (((target, module), dest), args) =>
  1.1870 +      (mk_seri_dest dest (serialize thy target module args program cs'))) seris;
  1.1871 +  in () end;
  1.1872  
  1.1873 -val _ = OuterSyntax.keywords [infixK, infixlK, infixrK];
  1.1874 +fun sml_of thy cs = 
  1.1875 +  let
  1.1876 +    val (cs', program) = CodeThingol.consts_program thy cs;
  1.1877 +  in sml_code_of thy program cs' ^ " ()" end;
  1.1878 +
  1.1879 +fun code_antiq (ctxt, args) = 
  1.1880 +  let
  1.1881 +    val thy = Context.theory_of ctxt;
  1.1882 +    val (ts, (ctxt', args')) = Scan.repeat1 Args.term (ctxt, args);
  1.1883 +    val cs = map (CodeUnit.check_const thy) ts;
  1.1884 +    val s = sml_of thy cs;
  1.1885 +  in (("codevals", s), (ctxt', args')) end;
  1.1886 +
  1.1887 +fun export_code_cmd raw_cs seris thy = code thy (read_const_exprs thy raw_cs) seris;
  1.1888 +
  1.1889 +val (inK, module_nameK, fileK) = ("in", "module_name", "file");
  1.1890 +
  1.1891 +fun code_exprP cmd =
  1.1892 +  (Scan.repeat P.term
  1.1893 +  -- Scan.repeat (P.$$$ inK |-- P.name
  1.1894 +     -- Scan.option (P.$$$ module_nameK |-- P.name)
  1.1895 +     -- Scan.option (P.$$$ fileK |-- P.name)
  1.1896 +     -- Scan.optional (P.$$$ "(" |-- P.arguments --| P.$$$ ")") []
  1.1897 +  ) >> (fn (raw_cs, seris) => cmd raw_cs seris));
  1.1898 +
  1.1899 +
  1.1900 +(** Isar setup **)
  1.1901 +
  1.1902 +val _ = OuterSyntax.keywords [infixK, infixlK, infixrK, inK, module_nameK, fileK];
  1.1903  
  1.1904  val _ =
  1.1905    OuterSyntax.command "code_class" "define code syntax for class" K.thy_decl (
  1.1906 @@ -2211,22 +2278,33 @@
  1.1907  val _ =
  1.1908    OuterSyntax.command "code_modulename" "alias module to other name" K.thy_decl (
  1.1909      P.name -- Scan.repeat1 (P.name -- P.name)
  1.1910 -    >> (fn (target, modlnames) => (Toplevel.theory o fold (add_modl_alias target)) modlnames)
  1.1911 +    >> (fn (target, modlnames) => (Toplevel.theory o fold (add_module_alias target)) modlnames)
  1.1912 +  );
  1.1913 +
  1.1914 +val _ =
  1.1915 +  OuterSyntax.command "code_abort" "permit constant to be implemented as program abort" K.thy_decl (
  1.1916 +    Scan.repeat1 P.term >> (Toplevel.theory o fold allow_abort_cmd)
  1.1917    );
  1.1918  
  1.1919  val _ =
  1.1920 -  OuterSyntax.command "code_exception" "permit exceptions for constant" K.thy_decl (
  1.1921 -    Scan.repeat1 P.term >> (Toplevel.theory o fold allow_exception_cmd)
  1.1922 -  );
  1.1923 +  OuterSyntax.command "export_code" "generate executable code for constants"
  1.1924 +    K.diag (P.!!! (code_exprP export_code_cmd) >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
  1.1925 +
  1.1926 +fun shell_command thyname cmd = Toplevel.program (fn _ =>
  1.1927 +  (use_thy thyname; case Scan.read OuterLex.stopper (P.!!! (code_exprP export_code_cmd)) ((filter OuterLex.is_proper o OuterSyntax.scan) cmd)
  1.1928 +   of SOME f => (writeln "Now generating code..."; f (theory thyname))
  1.1929 +    | NONE => error ("Bad directive " ^ quote cmd)))
  1.1930 +  handle TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure;
  1.1931 +
  1.1932 +val _ = ML_Context.value_antiq "code" code_antiq;
  1.1933  
  1.1934  
  1.1935  (* serializer setup, including serializer defaults *)
  1.1936  
  1.1937  val setup =
  1.1938 -  add_serializer (target_SML, isar_seri_sml)
  1.1939 -  #> add_serializer (target_OCaml, isar_seri_ocaml)
  1.1940 -  #> add_serializer (target_Haskell, isar_seri_haskell)
  1.1941 -  #> add_serializer (target_diag, fn _ => fn _=> seri_diagnosis)
  1.1942 +  add_target (target_SML, isar_seri_sml)
  1.1943 +  #> add_target (target_OCaml, isar_seri_ocaml)
  1.1944 +  #> add_target (target_Haskell, isar_seri_haskell)
  1.1945    #> add_syntax_tyco "SML" "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
  1.1946        brackify_infix (1, R) fxy [
  1.1947          pr_typ (INFX (1, X)) ty1,