major refactorings in code generator modules
authorhaftmann
Tue Jun 10 15:30:06 2008 +0200 (2008-06-10)
changeset 27103d8549f4d900b
parent 27102 a98cd7450204
child 27104 791607529f6d
major refactorings in code generator modules
doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
doc-src/IsarRef/Thy/HOL_Specific.thy
doc-src/IsarRef/Thy/document/HOL_Specific.tex
lib/Tools/codegen
src/HOL/Code_Setup.thy
src/HOL/IsaMakefile
src/HOL/Library/Eval.thy
src/HOL/Library/Eval_Witness.thy
src/HOL/ex/ExecutableContent.thy
src/HOL/ex/Quickcheck.thy
src/Tools/code/code_funcgr.ML
src/Tools/code/code_name.ML
src/Tools/code/code_package.ML
src/Tools/code/code_target.ML
src/Tools/code/code_thingol.ML
src/Tools/nbe.ML
     1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Tue Jun 10 15:30:01 2008 +0200
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Tue Jun 10 15:30:06 2008 +0200
     1.3 @@ -7,9 +7,7 @@
     1.4  uses "../../../antiquote_setup.ML"
     1.5  begin
     1.6  
     1.7 -ML {*
     1.8 -CodeTarget.target_code_width := 74;
     1.9 -*}
    1.10 +ML {* CodeTarget.code_width := 74 *}
    1.11  
    1.12  (*>*)
    1.13  
     2.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Jun 10 15:30:01 2008 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Jun 10 15:30:06 2008 +0200
     2.3 @@ -915,7 +915,7 @@
     2.4      @{command_def (HOL) "code_reserved"} & : & \isartrans{theory}{theory} \\
     2.5      @{command_def (HOL) "code_include"} & : & \isartrans{theory}{theory} \\
     2.6      @{command_def (HOL) "code_modulename"} & : & \isartrans{theory}{theory} \\
     2.7 -    @{command_def (HOL) "code_exception"} & : & \isartrans{theory}{theory} \\
     2.8 +    @{command_def (HOL) "code_abort"} & : & \isartrans{theory}{theory} \\
     2.9      @{command_def (HOL) "print_codesetup"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
    2.10      @{attribute_def (HOL) code} & : & \isaratt \\
    2.11    \end{matharray}
    2.12 @@ -1069,9 +1069,9 @@
    2.13    \item [@{command (HOL) "code_modulename"}] declares aliasings from
    2.14    one module name onto another.
    2.15  
    2.16 -  \item [@{command (HOL) "code_exception"}] declares constants which
    2.17 -  are not required to have a definition by a defining equations; these
    2.18 -  are mapped on exceptions instead.
    2.19 +  \item [@{command (HOL) "code_abort"}] declares constants which
    2.20 +  are not required to have a definition by a defining equations;
    2.21 +  if needed these are implemented by program abort instead.
    2.22  
    2.23    \item [@{attribute (HOL) code}~@{text func}] explicitly selects (or
    2.24    with option ``@{text "del:"}'' deselects) a defining equation for
     3.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue Jun 10 15:30:01 2008 +0200
     3.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue Jun 10 15:30:06 2008 +0200
     3.3 @@ -919,7 +919,7 @@
     3.4      \indexdef{HOL}{command}{code\_reserved}\hypertarget{command.HOL.code-reserved}{\hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}}} & : & \isartrans{theory}{theory} \\
     3.5      \indexdef{HOL}{command}{code\_include}\hypertarget{command.HOL.code-include}{\hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}}} & : & \isartrans{theory}{theory} \\
     3.6      \indexdef{HOL}{command}{code\_modulename}\hypertarget{command.HOL.code-modulename}{\hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}}} & : & \isartrans{theory}{theory} \\
     3.7 -    \indexdef{HOL}{command}{code\_exception}\hypertarget{command.HOL.code-exception}{\hyperlink{command.HOL.code-exception}{\mbox{\isa{\isacommand{code{\isacharunderscore}exception}}}}} & : & \isartrans{theory}{theory} \\
     3.8 +    \indexdef{HOL}{command}{code\_abort}\hypertarget{command.HOL.code-abort}{\hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}} & : & \isartrans{theory}{theory} \\
     3.9      \indexdef{HOL}{command}{print\_codesetup}\hypertarget{command.HOL.print-codesetup}{\hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
    3.10      \indexdef{HOL}{attribute}{code}\hypertarget{attribute.HOL.code}{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}} & : & \isaratt \\
    3.11    \end{matharray}
    3.12 @@ -1070,9 +1070,9 @@
    3.13    \item [\hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}}] declares aliasings from
    3.14    one module name onto another.
    3.15  
    3.16 -  \item [\hyperlink{command.HOL.code-exception}{\mbox{\isa{\isacommand{code{\isacharunderscore}exception}}}}] declares constants which
    3.17 -  are not required to have a definition by a defining equations; these
    3.18 -  are mapped on exceptions instead.
    3.19 +  \item [\hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}] declares constants which
    3.20 +  are not required to have a definition by a defining equations;
    3.21 +  if needed these are implemented by program abort instead.
    3.22  
    3.23    \item [\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}~\isa{func}] explicitly selects (or
    3.24    with option ``\isa{{\isachardoublequote}del{\isacharcolon}{\isachardoublequote}}'' deselects) a defining equation for
     4.1 --- a/lib/Tools/codegen	Tue Jun 10 15:30:01 2008 +0200
     4.2 +++ b/lib/Tools/codegen	Tue Jun 10 15:30:06 2008 +0200
     4.3 @@ -35,6 +35,6 @@
     4.4  ## main
     4.5  
     4.6  CMD=$(echo $CMD | sed -e 's/\\/\\\\"/g; s/"/\\\"/g')
     4.7 -FULL_CMD="CodePackage.codegen_shell_command \"$THY\" \"$CMD\";"
     4.8 +FULL_CMD="CodeTarget.shell_command \"$THY\" \"$CMD\";"
     4.9  
    4.10  "$ISABELLE" -q -e "$FULL_CMD" "$IMAGE" || exit 1
     5.1 --- a/src/HOL/Code_Setup.thy	Tue Jun 10 15:30:01 2008 +0200
     5.2 +++ b/src/HOL/Code_Setup.thy	Tue Jun 10 15:30:06 2008 +0200
     5.3 @@ -126,8 +126,18 @@
     5.4  
     5.5  subsection {* Evaluation oracle *}
     5.6  
     5.7 +ML {*
     5.8 +structure Eval_Method =
     5.9 +struct
    5.10 +
    5.11 +val eval_ref : (unit -> bool) option ref = ref NONE;
    5.12 +
    5.13 +end;
    5.14 +*}
    5.15 +
    5.16  oracle eval_oracle ("term") = {* fn thy => fn t => 
    5.17 -  if CodePackage.satisfies thy (HOLogic.dest_Trueprop t) [] 
    5.18 +  if CodeTarget.eval_term ("Eval_Method.eval_ref", Eval_Method.eval_ref) thy
    5.19 +    (HOLogic.dest_Trueprop t) [] 
    5.20    then t
    5.21    else HOLogic.Trueprop $ HOLogic.true_const (*dummy*)
    5.22  *}
     6.1 --- a/src/HOL/IsaMakefile	Tue Jun 10 15:30:01 2008 +0200
     6.2 +++ b/src/HOL/IsaMakefile	Tue Jun 10 15:30:06 2008 +0200
     6.3 @@ -89,7 +89,7 @@
     6.4    $(SRC)/Provers/quasi.ML $(SRC)/Provers/splitter.ML			\
     6.5    $(SRC)/Provers/trancl.ML $(SRC)/Tools/Metis/metis.ML			\
     6.6    $(SRC)/Tools/code/code_funcgr.ML $(SRC)/Tools/code/code_name.ML	\
     6.7 -  $(SRC)/Tools/code/code_package.ML $(SRC)/Tools/code/code_target.ML	\
     6.8 +  $(SRC)/Tools/code/code_target.ML	\
     6.9    $(SRC)/Tools/code/code_thingol.ML $(SRC)/Tools/nbe.ML $(SRC)/Tools/atomize_elim.ML \
    6.10    $(SRC)/Tools/random_word.ML $(SRC)/Tools/rat.ML Tools/TFL/casesplit.ML ATP_Linkup.thy	\
    6.11    Arith_Tools.thy Code_Setup.thy Datatype.thy 			\
     7.1 --- a/src/HOL/Library/Eval.thy	Tue Jun 10 15:30:01 2008 +0200
     7.2 +++ b/src/HOL/Library/Eval.thy	Tue Jun 10 15:30:06 2008 +0200
     7.3 @@ -244,7 +244,7 @@
     7.4  fun eval_term thy t =
     7.5    t 
     7.6    |> Eval.mk_term_of (fastype_of t)
     7.7 -  |> (fn t => CodePackage.eval_term ("Eval.eval_ref", eval_ref) thy t [])
     7.8 +  |> (fn t => CodeTarget.eval_term ("Eval.eval_ref", eval_ref) thy t [])
     7.9    |> Code.postprocess_term thy;
    7.10  
    7.11  val evaluators = [
     8.1 --- a/src/HOL/Library/Eval_Witness.thy	Tue Jun 10 15:30:01 2008 +0200
     8.2 +++ b/src/HOL/Library/Eval_Witness.thy	Tue Jun 10 15:30:06 2008 +0200
     8.3 @@ -46,6 +46,15 @@
     8.4  instance bool :: ml_equiv ..
     8.5  instance list :: (ml_equiv) ml_equiv ..
     8.6  
     8.7 +ML {*
     8.8 +structure Eval_Witness_Method =
     8.9 +struct
    8.10 +
    8.11 +val eval_ref : (unit -> bool) option ref = ref NONE;
    8.12 +
    8.13 +end;
    8.14 +*}
    8.15 +
    8.16  oracle eval_witness_oracle ("term * string list") = {* fn thy => fn (goal, ws) => 
    8.17  let
    8.18    fun check_type T = 
    8.19 @@ -59,7 +68,7 @@
    8.20      | dest_exs _ _ = sys_error "dest_exs";
    8.21    val t = dest_exs (length ws) (HOLogic.dest_Trueprop goal);
    8.22  in
    8.23 -  if CodePackage.satisfies thy t ws
    8.24 +  if CodeTarget.eval_term ("Eval_Witness_Method.eval_ref", Eval_Witness_Method.eval_ref) thy t ws
    8.25    then goal
    8.26    else HOLogic.Trueprop $ HOLogic.true_const (*dummy*)
    8.27  end
     9.1 --- a/src/HOL/ex/ExecutableContent.thy	Tue Jun 10 15:30:01 2008 +0200
     9.2 +++ b/src/HOL/ex/ExecutableContent.thy	Tue Jun 10 15:30:06 2008 +0200
     9.3 @@ -34,4 +34,9 @@
     9.4  lemma [code func, code func del]: "(Eval.term_of \<Colon> index \<Rightarrow> term) = Eval.term_of" ..
     9.5  declare fast_bv_to_nat_helper.simps [code func del]
     9.6  
     9.7 +setup {*
     9.8 +  Code.del_funcs
     9.9 +    (AxClass.param_of_inst @{theory} (@{const_name "Eval.term_of"}, @{type_name "env"}))
    9.10 +*}
    9.11 +
    9.12  end
    10.1 --- a/src/HOL/ex/Quickcheck.thy	Tue Jun 10 15:30:01 2008 +0200
    10.2 +++ b/src/HOL/ex/Quickcheck.thy	Tue Jun 10 15:30:06 2008 +0200
    10.3 @@ -250,7 +250,7 @@
    10.4  
    10.5  fun compile_generator_expr thy prop tys =
    10.6    let
    10.7 -    val f = CodePackage.eval_term ("Quickcheck.eval_ref", eval_ref) thy
    10.8 +    val f = CodeTarget.eval_term ("Quickcheck.eval_ref", eval_ref) thy
    10.9        (mk_generator_expr thy prop tys) [];
   10.10    in f #> Random_Engine.run #> (Option.map o map) (Code.postprocess_term thy) end;
   10.11  
    11.1 --- a/src/Tools/code/code_funcgr.ML	Tue Jun 10 15:30:01 2008 +0200
    11.2 +++ b/src/Tools/code/code_funcgr.ML	Tue Jun 10 15:30:06 2008 +0200
    11.3 @@ -14,7 +14,6 @@
    11.4    val all: T -> string list
    11.5    val pretty: theory -> T -> Pretty.T
    11.6    val make: theory -> string list -> T
    11.7 -  val make_consts: theory -> string list -> string list * T
    11.8    val eval_conv: theory -> (term -> term * (T -> term -> thm)) -> cterm -> thm
    11.9    val eval_term: theory -> (term -> term * (T -> term -> 'a)) -> term -> 'a
   11.10    val timing: bool ref
   11.11 @@ -219,12 +218,6 @@
   11.12  
   11.13  val ensure_consts = ensure_consts;
   11.14  
   11.15 -fun check_consts thy consts funcgr =
   11.16 -  let
   11.17 -    val algebra = Code.coregular_algebra thy;
   11.18 -    fun try_const const funcgr = (const, ensure_consts thy algebra [const] funcgr);
   11.19 -  in fold_map try_const consts funcgr end;
   11.20 -
   11.21  fun proto_eval thy cterm_of evaluator_fr evaluator proto_ct funcgr =
   11.22    let
   11.23      val ct = cterm_of proto_ct;
   11.24 @@ -278,13 +271,63 @@
   11.25  fun make thy =
   11.26    Funcgr.change thy o ensure_consts thy (Code.coregular_algebra thy);
   11.27  
   11.28 -fun make_consts thy =
   11.29 -  Funcgr.change_yield thy o check_consts thy;
   11.30 -
   11.31  fun eval_conv thy f =
   11.32    fst o Funcgr.change_yield thy o proto_eval_conv thy f;
   11.33  
   11.34  fun eval_term thy f =
   11.35    fst o Funcgr.change_yield thy o proto_eval_term thy f;
   11.36  
   11.37 +
   11.38 +(** diagnostic commands **)
   11.39 +
   11.40 +fun code_depgr thy [] = make thy []
   11.41 +  | code_depgr thy consts =
   11.42 +      let
   11.43 +        val gr = make thy consts;
   11.44 +        val select = Graph.all_succs gr consts;
   11.45 +      in
   11.46 +        gr
   11.47 +        |> Graph.subgraph (member (op =) select) 
   11.48 +        |> Graph.map_nodes ((apsnd o map) (AxClass.overload thy))
   11.49 +      end;
   11.50 +
   11.51 +fun code_thms thy = Pretty.writeln o pretty thy o code_depgr thy;
   11.52 +
   11.53 +fun code_deps thy consts =
   11.54 +  let
   11.55 +    val gr = code_depgr thy consts;
   11.56 +    fun mk_entry (const, (_, (_, parents))) =
   11.57 +      let
   11.58 +        val name = CodeUnit.string_of_const thy const;
   11.59 +        val nameparents = map (CodeUnit.string_of_const thy) parents;
   11.60 +      in { name = name, ID = name, dir = "", unfold = true,
   11.61 +        path = "", parents = nameparents }
   11.62 +      end;
   11.63 +    val prgr = Graph.fold ((fn x => fn xs => xs @ [x]) o mk_entry) gr [];
   11.64 +  in Present.display_graph prgr end;
   11.65 +
   11.66 +local
   11.67 +
   11.68 +structure P = OuterParse
   11.69 +and K = OuterKeyword
   11.70 +
   11.71 +fun code_thms_cmd thy = code_thms thy o op @ o CodeName.read_const_exprs thy;
   11.72 +fun code_deps_cmd thy = code_deps thy o op @ o CodeName.read_const_exprs thy;
   11.73 +
   11.74 +in
   11.75 +
   11.76 +val _ =
   11.77 +  OuterSyntax.improper_command "code_thms" "print system of defining equations for code" OuterKeyword.diag
   11.78 +    (Scan.repeat P.term
   11.79 +      >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
   11.80 +        o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of)));
   11.81 +
   11.82 +val _ =
   11.83 +  OuterSyntax.improper_command "code_deps" "visualize dependencies of defining equations for code" OuterKeyword.diag
   11.84 +    (Scan.repeat P.term
   11.85 +      >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
   11.86 +        o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));
   11.87 +
   11.88 +end;
   11.89 +
   11.90  end; (*struct*)
    12.1 --- a/src/Tools/code/code_name.ML	Tue Jun 10 15:30:01 2008 +0200
    12.2 +++ b/src/Tools/code/code_name.ML	Tue Jun 10 15:30:06 2008 +0200
    12.3 @@ -10,10 +10,13 @@
    12.4  
    12.5  signature CODE_NAME =
    12.6  sig
    12.7 +  val read_const_exprs: theory -> string list -> string list * string list
    12.8 +
    12.9    val purify_var: string -> string
   12.10    val purify_tvar: string -> string
   12.11    val purify_sym: string -> string
   12.12    val check_modulename: string -> string
   12.13 +
   12.14    type var_ctxt;
   12.15    val make_vars: string list -> var_ctxt;
   12.16    val intro_vars: string list -> var_ctxt -> var_ctxt;
   12.17 @@ -38,6 +41,31 @@
   12.18  structure CodeName: CODE_NAME =
   12.19  struct
   12.20  
   12.21 +(** constant expressions **)
   12.22 +
   12.23 +fun read_const_exprs thy =
   12.24 +  let
   12.25 +    fun consts_of some_thyname =
   12.26 +      let
   12.27 +        val thy' = case some_thyname
   12.28 +         of SOME thyname => ThyInfo.the_theory thyname thy
   12.29 +          | NONE => thy;
   12.30 +        val raw_cs = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
   12.31 +          ((snd o #constants o Consts.dest o #consts o Sign.rep_sg) thy') [];
   12.32 +        val cs = map (CodeUnit.subst_alias thy') raw_cs;
   12.33 +        fun belongs_here c =
   12.34 +          not (exists (fn thy'' => Sign.declared_const thy'' c) (Theory.parents_of thy'))
   12.35 +      in case some_thyname
   12.36 +       of NONE => cs
   12.37 +        | SOME thyname => filter belongs_here cs
   12.38 +      end;
   12.39 +    fun read_const_expr "*" = ([], consts_of NONE)
   12.40 +      | read_const_expr s = if String.isSuffix ".*" s
   12.41 +          then ([], consts_of (SOME (unsuffix ".*" s)))
   12.42 +          else ([CodeUnit.read_const thy s], []);
   12.43 +  in pairself flat o split_list o map read_const_expr end;
   12.44 +
   12.45 +
   12.46  (** purification **)
   12.47  
   12.48  fun purify_name upper lower =
   12.49 @@ -98,7 +126,6 @@
   12.50    | NONE => error ("Invalid name in context: " ^ quote name);
   12.51  
   12.52  
   12.53 -
   12.54  (** global names (identifiers) **)
   12.55  
   12.56  (* identifier categories *)
    13.1 --- a/src/Tools/code/code_package.ML	Tue Jun 10 15:30:01 2008 +0200
    13.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.3 @@ -1,357 +0,0 @@
    13.4 -(*  Title:      Tools/code/code_package.ML
    13.5 -    ID:         $Id$
    13.6 -    Author:     Florian Haftmann, TU Muenchen
    13.7 -
    13.8 -Code generator interfaces and Isar setup.
    13.9 -*)
   13.10 -
   13.11 -signature CODE_PACKAGE =
   13.12 -sig
   13.13 -  val source_of: theory -> string -> string -> string list -> string;
   13.14 -  val evaluate_conv: theory
   13.15 -    -> (term -> term * (CodeThingol.code -> CodeThingol.typscheme * CodeThingol.iterm
   13.16 -       -> string list -> thm))
   13.17 -    -> cterm -> thm;
   13.18 -  val evaluate_term: theory
   13.19 -    -> (term -> term * (CodeThingol.code -> CodeThingol.typscheme * CodeThingol.iterm
   13.20 -       -> string list -> 'a))
   13.21 -    -> term -> 'a;
   13.22 -  val eval_conv: string * (unit -> thm) option ref
   13.23 -    -> theory -> cterm -> string list -> thm;
   13.24 -  val eval_term: string * (unit -> 'a) option ref
   13.25 -    -> theory -> term -> string list -> 'a;
   13.26 -  val satisfies: theory -> term -> string list -> bool;
   13.27 -  val satisfies_ref: (unit -> bool) option ref;
   13.28 -  val codegen_shell_command: string (*theory name*) -> string (*cg expr*) -> unit;
   13.29 -end;
   13.30 -
   13.31 -structure CodePackage : CODE_PACKAGE =
   13.32 -struct
   13.33 -
   13.34 -(** code theorems **)
   13.35 -
   13.36 -fun code_depgr thy [] = CodeFuncgr.make thy []
   13.37 -  | code_depgr thy consts =
   13.38 -      let
   13.39 -        val gr = CodeFuncgr.make thy consts;
   13.40 -        val select = Graph.all_succs gr consts;
   13.41 -      in
   13.42 -        gr
   13.43 -        |> Graph.subgraph (member (op =) select) 
   13.44 -        |> Graph.map_nodes ((apsnd o map) (AxClass.overload thy))
   13.45 -      end;
   13.46 -
   13.47 -fun code_thms thy =
   13.48 -  Pretty.writeln o CodeFuncgr.pretty thy o code_depgr thy;
   13.49 -
   13.50 -fun code_deps thy consts =
   13.51 -  let
   13.52 -    val gr = code_depgr thy consts;
   13.53 -    fun mk_entry (const, (_, (_, parents))) =
   13.54 -      let
   13.55 -        val name = CodeUnit.string_of_const thy const;
   13.56 -        val nameparents = map (CodeUnit.string_of_const thy) parents;
   13.57 -      in { name = name, ID = name, dir = "", unfold = true,
   13.58 -        path = "", parents = nameparents }
   13.59 -      end;
   13.60 -    val prgr = Graph.fold ((fn x => fn xs => xs @ [x]) o mk_entry) gr [];
   13.61 -  in Present.display_graph prgr end;
   13.62 -
   13.63 -
   13.64 -(** code generation interfaces **)
   13.65 -
   13.66 -(* code data *)
   13.67 -
   13.68 -structure Program = CodeDataFun
   13.69 -(
   13.70 -  type T = CodeThingol.code;
   13.71 -  val empty = CodeThingol.empty_code;
   13.72 -  fun merge _ = CodeThingol.merge_code;
   13.73 -  fun purge _ NONE _ = CodeThingol.empty_code
   13.74 -    | purge NONE _ _ = CodeThingol.empty_code
   13.75 -    | purge (SOME thy) (SOME cs) code =
   13.76 -        let
   13.77 -          val cs_exisiting =
   13.78 -            map_filter (CodeName.const_rev thy) (Graph.keys code);
   13.79 -          val dels = (Graph.all_preds code
   13.80 -              o map (CodeName.const thy)
   13.81 -              o filter (member (op =) cs_exisiting)
   13.82 -            ) cs;
   13.83 -        in Graph.del_nodes dels code end;
   13.84 -);
   13.85 -
   13.86 -(* generic generation combinators *)
   13.87 -
   13.88 -val ensure_const = CodeThingol.ensure_const;
   13.89 -
   13.90 -fun perhaps_const thy algbr funcgr c trns =
   13.91 -  case try (CodeThingol.ensure_const thy algbr funcgr c) trns
   13.92 -   of SOME (c, trns) => (SOME c, trns)
   13.93 -    | NONE => (NONE, trns);
   13.94 -
   13.95 -fun generate thy funcgr f x =
   13.96 -  Program.change_yield thy (CodeThingol.transact thy funcgr
   13.97 -    (fn thy => fn funcgr => fn algbr => f thy funcgr algbr x));
   13.98 -
   13.99 -(* export_code functionality *)
  13.100 -
  13.101 -fun code thy permissive cs seris =
  13.102 -  let
  13.103 -    val code = Program.get thy;
  13.104 -    fun mk_seri_dest file = case file
  13.105 -     of NONE => CodeTarget.compile
  13.106 -      | SOME "-" => CodeTarget.write
  13.107 -      | SOME f => CodeTarget.file (Path.explode f)
  13.108 -    val _ = map (fn (((target, module), file), args) =>
  13.109 -      (mk_seri_dest file (CodeTarget.serialize thy target permissive module args code cs))) seris;
  13.110 -  in () end;
  13.111 -
  13.112 -(* code retrieval *)
  13.113 -
  13.114 -fun source_of thy target module_name cs =
  13.115 -  let
  13.116 -    val (cs', _) = generate thy (CodeFuncgr.make thy cs)
  13.117 -      (fold_map ooo ensure_const) cs;
  13.118 -    val code = Program.get thy;
  13.119 -  in
  13.120 -    CodeTarget.string
  13.121 -      (CodeTarget.serialize thy target false (SOME module_name) [] code (SOME cs'))
  13.122 -  end;
  13.123 -
  13.124 -(* evaluation machinery *)
  13.125 -
  13.126 -fun evaluate eval_kind thy evaluator =
  13.127 -  let
  13.128 -    fun evaluator'' evaluator''' funcgr t =
  13.129 -      let
  13.130 -        val ((code, (vs_ty_t, deps)), _) =
  13.131 -          generate thy funcgr CodeThingol.ensure_value t;
  13.132 -      in evaluator''' code vs_ty_t deps end;
  13.133 -    fun evaluator' t =
  13.134 -      let
  13.135 -        val (t', evaluator''') = evaluator t;
  13.136 -      in (t', evaluator'' evaluator''') end;
  13.137 -  in eval_kind thy evaluator' end
  13.138 -
  13.139 -fun evaluate_conv thy = evaluate CodeFuncgr.eval_conv thy;
  13.140 -fun evaluate_term thy = evaluate CodeFuncgr.eval_term thy;
  13.141 -
  13.142 -fun eval_ml reff args thy code ((vs, ty), t) deps =
  13.143 -  CodeTarget.eval thy reff code (t, ty) args;
  13.144 -
  13.145 -fun eval evaluate term_of reff thy ct args =
  13.146 -  let
  13.147 -    val _ = if null (term_frees (term_of ct)) then () else error ("Term "
  13.148 -      ^ quote (Syntax.string_of_term_global thy (term_of ct))
  13.149 -      ^ " to be evaluated contains free variables");
  13.150 -  in evaluate thy (fn t => (t, eval_ml reff args thy)) ct end;
  13.151 -
  13.152 -fun eval_conv reff = eval evaluate_conv Thm.term_of reff;
  13.153 -fun eval_term reff = eval evaluate_term I reff;
  13.154 -
  13.155 -val satisfies_ref : (unit -> bool) option ref = ref NONE;
  13.156 -
  13.157 -val satisfies = eval_term ("CodePackage.satisfies_ref", satisfies_ref);
  13.158 -
  13.159 -(* code antiquotation *)
  13.160 -
  13.161 -fun code_antiq (ctxt, args) = 
  13.162 -  let
  13.163 -    val thy = Context.theory_of ctxt;
  13.164 -    val (ts, (ctxt', args')) = Scan.repeat1 Args.term (ctxt, args);
  13.165 -    val cs = map (CodeUnit.check_const thy) ts;
  13.166 -    val (cs', code') = generate thy (CodeFuncgr.make thy cs)
  13.167 -      (fold_map ooo ensure_const) cs;
  13.168 -    val code'' = CodeTarget.sml_of thy code' cs' ^ " ()";
  13.169 -  in (("codevals", code''), (ctxt', args')) end;
  13.170 -
  13.171 -
  13.172 -(* const expressions *)
  13.173 -
  13.174 -local
  13.175 -
  13.176 -fun consts_of thy some_thyname =
  13.177 -  let
  13.178 -    val this_thy = Option.map ThyInfo.get_theory some_thyname |> the_default thy;
  13.179 -    val raw_cs = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
  13.180 -      ((snd o #constants o Consts.dest o #consts o Sign.rep_sg) this_thy) [];
  13.181 -    val cs = map (CodeUnit.subst_alias thy) raw_cs;
  13.182 -    fun belongs_here thyname c =
  13.183 -      not (exists (fn thy' => Sign.declared_const thy' c) (Theory.parents_of this_thy))
  13.184 -  in case some_thyname
  13.185 -   of NONE => cs
  13.186 -    | SOME thyname => filter (belongs_here thyname) cs
  13.187 -  end;
  13.188 -
  13.189 -fun read_const_expr thy "*" = ([], consts_of thy NONE)
  13.190 -  | read_const_expr thy s = if String.isSuffix ".*" s
  13.191 -      then ([], consts_of thy (SOME (unsuffix ".*" s)))
  13.192 -      else ([CodeUnit.read_const thy s], []);
  13.193 -
  13.194 -in
  13.195 -
  13.196 -fun read_const_exprs thy select exprs =
  13.197 -  case (pairself flat o split_list o map (read_const_expr thy)) exprs
  13.198 -   of (consts, []) => (false, consts)
  13.199 -    | (consts, consts') => (true, consts @ select consts');
  13.200 -
  13.201 -end; (*local*)
  13.202 -
  13.203 -fun filter_generatable thy consts =
  13.204 -  let
  13.205 -    val (consts', funcgr) = CodeFuncgr.make_consts thy consts;
  13.206 -    val (consts'', _) = generate thy funcgr (fold_map ooo perhaps_const) consts';
  13.207 -    val consts''' = map_filter (fn (const, SOME _) => SOME const | (_, NONE) => NONE)
  13.208 -      (consts' ~~ consts'');
  13.209 -  in consts''' end;
  13.210 -
  13.211 -fun generate_const_exprs thy raw_cs =
  13.212 -  let
  13.213 -    val (perm1, cs) = read_const_exprs thy
  13.214 -      (filter_generatable thy) raw_cs;
  13.215 -    val (perm2, cs') = case generate thy (CodeFuncgr.make thy cs)
  13.216 -      (fold_map ooo ensure_const) cs
  13.217 -     of ([], _) => (true, NONE)
  13.218 -      | (cs, _) => (false, SOME cs);
  13.219 -  in (perm1 orelse perm2, cs') end;
  13.220 -
  13.221 -
  13.222 -(** code properties **)
  13.223 -
  13.224 -fun mk_codeprops thy all_cs sel_cs =
  13.225 -  let
  13.226 -    fun select (thmref, thm) = case try (Thm.unvarify o Drule.zero_var_indexes) thm
  13.227 -     of NONE => NONE
  13.228 -      | SOME thm => let
  13.229 -          val t = (ObjectLogic.drop_judgment thy o Thm.prop_of) thm;
  13.230 -          val cs = fold_aterms (fn Const (c, ty) =>
  13.231 -            cons (AxClass.unoverload_const thy (c, ty)) | _ => I) t [];
  13.232 -        in if exists (member (op =) sel_cs) cs
  13.233 -          andalso forall (member (op =) all_cs) cs
  13.234 -          then SOME (thmref, thm) else NONE end;
  13.235 -    fun mk_codeprop (thmref, thm) =
  13.236 -      let
  13.237 -        val t = ObjectLogic.drop_judgment thy (Thm.prop_of thm);
  13.238 -        val ty_judg = fastype_of t;
  13.239 -        val tfrees1 = fold_aterms (fn Const (c, ty) =>
  13.240 -          Term.add_tfreesT ty | _ => I) t [];
  13.241 -        val vars = Term.add_frees t [];
  13.242 -        val tfrees2 = fold (Term.add_tfreesT o snd) vars [];
  13.243 -        val tfrees' = subtract (op =) tfrees2 tfrees1 |> map TFree;
  13.244 -        val ty = map Term.itselfT tfrees' @ map snd vars ---> ty_judg;
  13.245 -        val tfree_vars = map Logic.mk_type tfrees';
  13.246 -        val c = Facts.string_of_ref thmref
  13.247 -          |> NameSpace.explode
  13.248 -          |> (fn [x] => [x] | (x::xs) => xs)
  13.249 -          |> space_implode "_"
  13.250 -        val propdef = (((c, ty), tfree_vars @ map Free vars), t);
  13.251 -      in if c = "" then NONE else SOME (thmref, propdef) end;
  13.252 -  in
  13.253 -    Facts.dest_static (PureThy.facts_of thy)
  13.254 -    |> maps Facts.selections
  13.255 -    |> map_filter select
  13.256 -    |> map_filter mk_codeprop
  13.257 -  end;
  13.258 -
  13.259 -fun add_codeprops all_cs sel_cs thy =
  13.260 -  let
  13.261 -    val codeprops = mk_codeprops thy all_cs sel_cs;
  13.262 -    fun lift_name_yield f x = (Name.context, x) |> f ||> snd;
  13.263 -    fun add (thmref, (((raw_c, ty), ts), t)) (names, thy) =
  13.264 -      let
  13.265 -        val _ = warning ("Adding theorem " ^ quote (Facts.string_of_ref thmref)
  13.266 -          ^ " as code property " ^ quote raw_c);
  13.267 -        val ([raw_c'], names') = Name.variants [raw_c] names;
  13.268 -        val (const as Const (c, _), thy') = thy |> Sign.declare_const [] (raw_c', ty, NoSyn);
  13.269 -        val eq = Logic.mk_equals (list_comb (const, ts), t);
  13.270 -        val ([def], thy'') = thy' |> PureThy.add_defs_i false [((Thm.def_name raw_c', eq), [])];
  13.271 -      in ((c, def), (names', thy'')) end;
  13.272 -  in
  13.273 -    thy
  13.274 -    |> Sign.sticky_prefix "codeprop"
  13.275 -    |> lift_name_yield (fold_map add codeprops)
  13.276 -    ||> Sign.restore_naming thy
  13.277 -    |-> (fn c_thms => fold (Code.add_func o snd) c_thms #> pair c_thms)
  13.278 -  end;
  13.279 -
  13.280 -
  13.281 -(** interfaces and Isar setup **)
  13.282 -
  13.283 -local
  13.284 -
  13.285 -structure P = OuterParse
  13.286 -and K = OuterKeyword
  13.287 -
  13.288 -fun code_cmd raw_cs seris thy =
  13.289 -  let
  13.290 -    val (permissive, cs) = generate_const_exprs thy raw_cs;
  13.291 -    val _ = code thy permissive cs seris;
  13.292 -  in () end;
  13.293 -
  13.294 -fun code_thms_cmd thy =
  13.295 -  code_thms thy o snd o read_const_exprs thy (fst o CodeFuncgr.make_consts thy);
  13.296 -
  13.297 -fun code_deps_cmd thy =
  13.298 -  code_deps thy o snd o read_const_exprs thy (fst o CodeFuncgr.make_consts thy);
  13.299 -
  13.300 -fun code_props_cmd raw_cs seris thy =
  13.301 -  let
  13.302 -    val (_, all_cs) = generate_const_exprs thy ["*"];
  13.303 -    val (permissive, cs) = generate_const_exprs thy raw_cs;
  13.304 -    val (c_thms, thy') = add_codeprops (map (the o CodeName.const_rev thy) (these all_cs))
  13.305 -      (map (the o CodeName.const_rev thy) (these cs)) thy;
  13.306 -    val prop_cs = (filter_generatable thy' o map fst) c_thms;
  13.307 -    val _ = if null seris then () else (generate thy' (CodeFuncgr.make thy' prop_cs)
  13.308 -      (fold_map ooo ensure_const) prop_cs; ());
  13.309 -    val _ = if null seris then () else code thy' permissive
  13.310 -      (SOME (map (CodeName.const thy') prop_cs)) seris;
  13.311 -  in thy' end;
  13.312 -
  13.313 -val (inK, module_nameK, fileK) = ("in", "module_name", "file");
  13.314 -
  13.315 -fun code_exprP cmd =
  13.316 -  (Scan.repeat P.term
  13.317 -  -- Scan.repeat (P.$$$ inK |-- P.name
  13.318 -     -- Scan.option (P.$$$ module_nameK |-- P.name)
  13.319 -     -- Scan.option (P.$$$ fileK |-- P.name)
  13.320 -     -- Scan.optional (P.$$$ "(" |-- P.arguments --| P.$$$ ")") []
  13.321 -  ) >> (fn (raw_cs, seris) => cmd raw_cs seris));
  13.322 -
  13.323 -val _ = OuterSyntax.keywords [inK, module_nameK, fileK];
  13.324 -
  13.325 -val (codeK, code_thmsK, code_depsK, code_propsK) =
  13.326 -  ("export_code", "code_thms", "code_deps", "code_props");
  13.327 -
  13.328 -in
  13.329 -
  13.330 -val _ =
  13.331 -  OuterSyntax.command codeK "generate executable code for constants"
  13.332 -    K.diag (P.!!! (code_exprP code_cmd) >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
  13.333 -
  13.334 -fun codegen_shell_command thyname cmd = Toplevel.program (fn _ =>
  13.335 -  (use_thy thyname; case Scan.read OuterLex.stopper (P.!!! (code_exprP code_cmd)) ((filter OuterLex.is_proper o OuterSyntax.scan) cmd)
  13.336 -   of SOME f => (writeln "Now generating code..."; f (theory thyname))
  13.337 -    | NONE => error ("Bad directive " ^ quote cmd)))
  13.338 -  handle TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure;
  13.339 -
  13.340 -val _ =
  13.341 -  OuterSyntax.improper_command code_thmsK "print system of defining equations for code" OuterKeyword.diag
  13.342 -    (Scan.repeat P.term
  13.343 -      >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
  13.344 -        o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of)));
  13.345 -
  13.346 -val _ =
  13.347 -  OuterSyntax.improper_command code_depsK "visualize dependencies of defining equations for code" OuterKeyword.diag
  13.348 -    (Scan.repeat P.term
  13.349 -      >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
  13.350 -        o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));
  13.351 -
  13.352 -val _ =
  13.353 -  OuterSyntax.command code_propsK "generate characteristic properties for executable constants"
  13.354 -    K.thy_decl (P.!!! (code_exprP code_props_cmd) >> Toplevel.theory);
  13.355 -
  13.356 -val _ = ML_Context.value_antiq "code" code_antiq;
  13.357 -
  13.358 -end; (*local*)
  13.359 -
  13.360 -end; (*struct*)
    14.1 --- a/src/Tools/code/code_target.ML	Tue Jun 10 15:30:01 2008 +0200
    14.2 +++ b/src/Tools/code/code_target.ML	Tue Jun 10 15:30:06 2008 +0200
    14.3 @@ -28,24 +28,28 @@
    14.4    val add_pretty_message: string -> string -> string list -> string
    14.5      -> string -> string -> theory -> theory;
    14.6  
    14.7 -  val allow_exception: string -> theory -> theory;
    14.8 +  val allow_abort: string -> theory -> theory;
    14.9  
   14.10    type serialization;
   14.11    type serializer;
   14.12 -  val add_serializer: string * serializer -> theory -> theory;
   14.13 -  val assert_serializer: theory -> string -> string;
   14.14 -  val serialize: theory -> string -> bool -> string option -> Args.T list
   14.15 -    -> CodeThingol.code -> string list option -> serialization;
   14.16 +  val add_target: string * serializer -> theory -> theory;
   14.17 +  val assert_target: theory -> string -> string;
   14.18 +  val serialize: theory -> string -> string option -> Args.T list
   14.19 +    -> CodeThingol.program -> string list -> serialization;
   14.20    val compile: serialization -> unit;
   14.21    val write: serialization -> unit;
   14.22    val file: Path.T -> serialization -> unit;
   14.23    val string: serialization -> string;
   14.24 -  val sml_of: theory -> CodeThingol.code -> string list -> string;
   14.25 -  val eval: theory -> (string * (unit -> 'a) option ref)
   14.26 -    -> CodeThingol.code -> CodeThingol.iterm * CodeThingol.itype -> string list -> 'a;
   14.27 -  val target_code_width: int ref;
   14.28 +
   14.29 +  val code_of: theory -> string -> string -> string list -> string;
   14.30 +  val eval_conv: string * (unit -> thm) option ref
   14.31 +    -> theory -> cterm -> string list -> thm;
   14.32 +  val eval_term: string * (unit -> 'a) option ref
   14.33 +    -> theory -> term -> string list -> 'a;
   14.34 +  val shell_command: string (*theory name*) -> string (*cg expr*) -> unit;
   14.35  
   14.36    val setup: theory -> theory;
   14.37 +  val code_width: int ref;
   14.38  end;
   14.39  
   14.40  structure CodeTarget : CODE_TARGET =
   14.41 @@ -69,16 +73,16 @@
   14.42  datatype destination = Compile | Write | File of Path.T | String;
   14.43  type serialization = destination -> string option;
   14.44  
   14.45 -val target_code_width = ref 80; (*FIXME after Pretty module no longer depends on print mode*)
   14.46 -fun target_code_setmp f = PrintMode.setmp [] (Pretty.setmp_margin (!target_code_width) f);
   14.47 -fun target_code_of_pretty p = target_code_setmp Pretty.string_of p ^ "\n";
   14.48 -fun target_code_writeln p = Pretty.setmp_margin (!target_code_width) Pretty.writeln p;
   14.49 +val code_width = ref 80; (*FIXME after Pretty module no longer depends on print mode*)
   14.50 +fun code_setmp f = PrintMode.setmp [] (Pretty.setmp_margin (!code_width) f);
   14.51 +fun code_of_pretty p = code_setmp Pretty.string_of p ^ "\n";
   14.52 +fun code_writeln p = Pretty.setmp_margin (!code_width) Pretty.writeln p;
   14.53  
   14.54 -(*FIXME why another target_code_setmp?*)
   14.55 -fun compile f = (target_code_setmp f Compile; ());
   14.56 -fun write f = (target_code_setmp f Write; ());
   14.57 -fun file p f = (target_code_setmp f (File p); ());
   14.58 -fun string f = the (target_code_setmp f String);
   14.59 +(*FIXME why another code_setmp?*)
   14.60 +fun compile f = (code_setmp f Compile; ());
   14.61 +fun write f = (code_setmp f Write; ());
   14.62 +fun file p f = (code_setmp f (File p); ());
   14.63 +fun string f = the (code_setmp f String);
   14.64  
   14.65  
   14.66  (** generic syntax **)
   14.67 @@ -125,13 +129,12 @@
   14.68  
   14.69  (** theory data **)
   14.70  
   14.71 -val target_diag = "diag";
   14.72  val target_SML = "SML";
   14.73  val target_OCaml = "OCaml";
   14.74  val target_Haskell = "Haskell";
   14.75  
   14.76  datatype name_syntax_table = NameSyntaxTable of {
   14.77 -  class: (string * (string -> string option)) Symtab.table,
   14.78 +  class: class_syntax Symtab.table,
   14.79    inst: unit Symtab.table,
   14.80    tyco: typ_syntax Symtab.table,
   14.81    const: term_syntax Symtab.table
   14.82 @@ -160,7 +163,7 @@
   14.83    -> (string -> class_syntax option)
   14.84    -> (string -> typ_syntax option)
   14.85    -> (string -> term_syntax option)
   14.86 -  -> CodeThingol.code                   (*program*)
   14.87 +  -> CodeThingol.program
   14.88    -> string list                        (*selected statements*)
   14.89    -> serialization;
   14.90  
   14.91 @@ -209,12 +212,14 @@
   14.92  fun the_name_syntax (Target { name_syntax_table = NameSyntaxTable x, ... }) = x;
   14.93  fun the_module_alias (Target { module_alias , ... }) = module_alias;
   14.94  
   14.95 -fun assert_serializer thy target =
   14.96 +val abort_allowed = snd o CodeTargetData.get;
   14.97 +
   14.98 +fun assert_target thy target =
   14.99    case Symtab.lookup (fst (CodeTargetData.get thy)) target
  14.100     of SOME data => target
  14.101      | NONE => error ("Unknown code target language: " ^ quote target);
  14.102  
  14.103 -fun add_serializer (target, seri) thy =
  14.104 +fun add_target (target, seri) thy =
  14.105    let
  14.106      val _ = case Symtab.lookup (fst (CodeTargetData.get thy)) target
  14.107       of SOME _ => warning ("Overwriting existing serializer " ^ quote target)
  14.108 @@ -228,48 +233,59 @@
  14.109            ((map_target o apfst o apsnd o K) seri)
  14.110    end;
  14.111  
  14.112 -fun map_seri_data target f thy =
  14.113 +fun map_target_data target f thy =
  14.114    let
  14.115 -    val _ = assert_serializer thy target;
  14.116 +    val _ = assert_target thy target;
  14.117    in
  14.118      thy
  14.119      |> (CodeTargetData.map o apfst o Symtab.map_entry target o map_target) f
  14.120    end;
  14.121  
  14.122 -fun map_adaptions target =
  14.123 -  map_seri_data target o apsnd o apfst;
  14.124 +fun map_reserved target =
  14.125 +  map_target_data target o apsnd o apfst o apfst;
  14.126 +fun map_includes target =
  14.127 +  map_target_data target o apsnd o apfst o apsnd;
  14.128  fun map_name_syntax target =
  14.129 -  map_seri_data target o apsnd o apsnd o apfst o map_name_syntax_table;
  14.130 +  map_target_data target o apsnd o apsnd o apfst o map_name_syntax_table;
  14.131  fun map_module_alias target =
  14.132 -  map_seri_data target o apsnd o apsnd o apsnd;
  14.133 +  map_target_data target o apsnd o apsnd o apsnd;
  14.134  
  14.135 -fun get_serializer get_seri thy target permissive =
  14.136 +fun invoke_serializer thy abortable serializer reserved includes 
  14.137 +    module_alias class inst tyco const module args program1 cs1 =
  14.138    let
  14.139 -    val (seris, exc) = CodeTargetData.get thy;
  14.140 -    val data = case Symtab.lookup seris target
  14.141 +    val hidden = Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const;
  14.142 +    val cs2 = subtract (op =) hidden cs1;
  14.143 +    val program2 = Graph.subgraph (not o member (op =) hidden) program1;
  14.144 +    val all_cs = Graph.all_succs program2 cs2;
  14.145 +    val program3 = Graph.subgraph (member (op =) all_cs) program2;
  14.146 +    val empty_funs = filter_out (member (op =) abortable)
  14.147 +      (CodeThingol.empty_funs program3);
  14.148 +    val _ = if null empty_funs then () else error ("No defining equations for "
  14.149 +      ^ commas (map (CodeName.labelled_name thy) empty_funs));
  14.150 +  in
  14.151 +    serializer module args (CodeName.labelled_name thy) reserved includes
  14.152 +      (Symtab.lookup module_alias) (Symtab.lookup class)
  14.153 +      (Symtab.lookup tyco) (Symtab.lookup const)
  14.154 +      program3 cs2
  14.155 +  end;
  14.156 +
  14.157 +fun mount_serializer thy alt_serializer target =
  14.158 +  let
  14.159 +    val (targets, abortable) = CodeTargetData.get thy;
  14.160 +    val data = case Symtab.lookup targets target
  14.161       of SOME data => data
  14.162        | NONE => error ("Unknown code target language: " ^ quote target);
  14.163 -    val seri = get_seri data;
  14.164 +    val serializer = the_default (the_serializer data) alt_serializer;
  14.165      val reserved = the_reserved data;
  14.166      val includes = Symtab.dest (the_includes data);
  14.167 -    val alias = the_module_alias data;
  14.168 +    val module_alias = the_module_alias data;
  14.169      val { class, inst, tyco, const } = the_name_syntax data;
  14.170 -    val project = if target = target_diag then K I
  14.171 -      else CodeThingol.project_code permissive
  14.172 -        (Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const);
  14.173 -    fun check_empty_funs code = case filter_out (member (op =) exc)
  14.174 -        (CodeThingol.empty_funs code)
  14.175 -     of [] => code
  14.176 -      | names => error ("No defining equations for "
  14.177 -          ^ commas (map (CodeName.labelled_name thy) names));
  14.178 -  in fn module => fn args => fn code => fn cs =>
  14.179 -    seri module args (CodeName.labelled_name thy) reserved includes
  14.180 -      (Symtab.lookup alias) (Symtab.lookup class)
  14.181 -      (Symtab.lookup tyco) (Symtab.lookup const)
  14.182 -        ((check_empty_funs o project cs) code) (these cs)
  14.183 +  in
  14.184 +    invoke_serializer thy abortable serializer reserved
  14.185 +      includes module_alias class inst tyco const
  14.186    end;
  14.187  
  14.188 -val serialize = get_serializer the_serializer;
  14.189 +fun serialize thy = mount_serializer thy NONE;
  14.190  
  14.191  fun parse_args f args =
  14.192    case Scan.read Args.stopper f args
  14.193 @@ -277,39 +293,7 @@
  14.194      | NONE => error "Bad serializer arguments";
  14.195  
  14.196  
  14.197 -(** generic output combinators **)
  14.198 -
  14.199 -(* applications and bindings *)
  14.200 -
  14.201 -fun gen_pr_app pr_app' pr_term const_syntax labelled_name is_cons
  14.202 -      lhs vars fxy (app as ((c, (_, tys)), ts)) =
  14.203 -  case const_syntax c
  14.204 -   of NONE => if lhs andalso not (is_cons c) then
  14.205 -          error ("Non-constructor on left hand side of equation: " ^ labelled_name c)
  14.206 -        else brackify fxy (pr_app' lhs vars app)
  14.207 -    | SOME (i, pr) =>
  14.208 -        let
  14.209 -          val k = if i < 0 then length tys else i;
  14.210 -          fun pr' fxy ts = pr (pr_term lhs) vars fxy (ts ~~ curry Library.take k tys);
  14.211 -        in if k = length ts
  14.212 -          then pr' fxy ts
  14.213 -        else if k < length ts
  14.214 -          then case chop k ts of (ts1, ts2) =>
  14.215 -            brackify fxy (pr' APP ts1 :: map (pr_term lhs vars BR) ts2)
  14.216 -          else pr_term lhs vars fxy (CodeThingol.eta_expand app k)
  14.217 -        end;
  14.218 -
  14.219 -fun gen_pr_bind pr_bind' pr_term fxy ((v, pat), ty) vars =
  14.220 -  let
  14.221 -    val vs = case pat
  14.222 -     of SOME pat => CodeThingol.fold_varnames (insert (op =)) pat []
  14.223 -      | NONE => [];
  14.224 -    val vars' = CodeName.intro_vars (the_list v) vars;
  14.225 -    val vars'' = CodeName.intro_vars vs vars';
  14.226 -    val v' = Option.map (CodeName.lookup_var vars') v;
  14.227 -    val pat' = Option.map (pr_term true vars'' fxy) pat;
  14.228 -  in (pr_bind' ((v', pat'), ty), vars'') end;
  14.229 -
  14.230 +(** generic code combinators **)
  14.231  
  14.232  (* list, char, string, numeral and monad abstract syntax transformations *)
  14.233  
  14.234 @@ -359,7 +343,7 @@
  14.235        | dest_numeral (t1 `$ t2) =
  14.236            let val (n, b) = (dest_numeral t2, dest_bit t1)
  14.237            in case n of SOME n => SOME (2 * n + b) | NONE => NONE end
  14.238 -      | dest_numeral _ = error "Illegal numeral expression: illegal constant";
  14.239 +      | dest_numeral _ = error "Illegal numeral expression: illegal term";
  14.240    in dest_numeral #> the_default 0 end;
  14.241  
  14.242  fun implode_monad c_bind t =
  14.243 @@ -378,6 +362,38 @@
  14.244    in CodeThingol.unfoldr dest_monad t end;
  14.245  
  14.246  
  14.247 +(* applications and bindings *)
  14.248 +
  14.249 +fun gen_pr_app pr_app pr_term syntax_const labelled_name is_cons
  14.250 +      lhs vars fxy (app as ((c, (_, tys)), ts)) =
  14.251 +  case syntax_const c
  14.252 +   of NONE => if lhs andalso not (is_cons c) then
  14.253 +          error ("Non-constructor on left hand side of equation: " ^ labelled_name c)
  14.254 +        else brackify fxy (pr_app lhs vars app)
  14.255 +    | SOME (i, pr) =>
  14.256 +        let
  14.257 +          val k = if i < 0 then length tys else i;
  14.258 +          fun pr' fxy ts = pr (pr_term lhs) vars fxy (ts ~~ curry Library.take k tys);
  14.259 +        in if k = length ts
  14.260 +          then pr' fxy ts
  14.261 +        else if k < length ts
  14.262 +          then case chop k ts of (ts1, ts2) =>
  14.263 +            brackify fxy (pr' APP ts1 :: map (pr_term lhs vars BR) ts2)
  14.264 +          else pr_term lhs vars fxy (CodeThingol.eta_expand app k)
  14.265 +        end;
  14.266 +
  14.267 +fun gen_pr_bind pr_bind pr_term (fxy : fixity) ((v, pat), ty : itype) vars =
  14.268 +  let
  14.269 +    val vs = case pat
  14.270 +     of SOME pat => CodeThingol.fold_varnames (insert (op =)) pat []
  14.271 +      | NONE => [];
  14.272 +    val vars' = CodeName.intro_vars (the_list v) vars;
  14.273 +    val vars'' = CodeName.intro_vars vs vars';
  14.274 +    val v' = Option.map (CodeName.lookup_var vars') v;
  14.275 +    val pat' = Option.map (pr_term true vars'' fxy) pat;
  14.276 +  in (pr_bind ((v', pat'), ty), vars'') end;
  14.277 +
  14.278 +
  14.279  (* name auxiliary *)
  14.280  
  14.281  val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode;
  14.282 @@ -386,30 +402,29 @@
  14.283  val dest_name =
  14.284    apfst NameSpace.implode o split_last o fst o split_last o NameSpace.explode;
  14.285  
  14.286 -fun mk_modl_name_tab init_names prefix module_alias code =
  14.287 +fun mk_name_module reserved_names module_prefix module_alias program =
  14.288    let
  14.289 -    fun nsp_map f = NameSpace.explode #> map f #> NameSpace.implode;
  14.290 -    fun mk_alias name =
  14.291 -     case module_alias name
  14.292 -      of SOME name' => name'
  14.293 -       | NONE => nsp_map (fn name => (the_single o fst)
  14.294 -            (Name.variants [name] init_names)) name;
  14.295 -    fun mk_prefix name =
  14.296 -      case prefix
  14.297 -       of SOME prefix => NameSpace.append prefix name
  14.298 -        | NONE => name;
  14.299 +    fun mk_alias name = case module_alias name
  14.300 +     of SOME name' => name'
  14.301 +      | NONE => name
  14.302 +          |> NameSpace.explode
  14.303 +          |> map (fn name => (the_single o fst) (Name.variants [name] reserved_names))
  14.304 +          |> NameSpace.implode;
  14.305 +    fun mk_prefix name = case module_prefix
  14.306 +     of SOME module_prefix => NameSpace.append module_prefix name
  14.307 +      | NONE => name;
  14.308      val tab =
  14.309        Symtab.empty
  14.310        |> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name))
  14.311             o fst o dest_name o fst)
  14.312 -             code
  14.313 -  in fn name => (the o Symtab.lookup tab) name end;
  14.314 +             program
  14.315 +  in the o Symtab.lookup tab end;
  14.316  
  14.317  
  14.318  
  14.319  (** SML/OCaml serializer **)
  14.320  
  14.321 -datatype ml_def =
  14.322 +datatype ml_stmt =
  14.323      MLFuns of (string * (typscheme * (iterm list * iterm) list)) list
  14.324    | MLDatas of (string * ((vname * sort) list * (string * itype list) list)) list
  14.325    | MLClass of string * (vname * ((class * string) list * (string * itype) list))
  14.326 @@ -417,7 +432,7 @@
  14.327          * ((class * (string * (string * dict list list))) list
  14.328        * (string * const) list));
  14.329  
  14.330 -fun pr_sml tyco_syntax const_syntax labelled_name init_syms deresolv is_cons ml_def =
  14.331 +fun pr_sml_stmt syntax_tyco syntax_const labelled_name reserved_names deresolve is_cons =
  14.332    let
  14.333      val pr_label_classrel = translate_string (fn "." => "__" | c => c)
  14.334        o NameSpace.qualifier;
  14.335 @@ -432,30 +447,30 @@
  14.336                brackets [p', p]
  14.337            | pr_proj (ps as _ :: _) p =
  14.338                brackets [Pretty.enum " o" "(" ")" ps, p];
  14.339 -        fun pr_dictc fxy (DictConst (inst, dss)) =
  14.340 -              brackify fxy ((str o deresolv) inst :: map (pr_dicts BR) dss)
  14.341 -          | pr_dictc fxy (DictVar (classrels, v)) =
  14.342 -              pr_proj (map (str o deresolv) classrels) ((str o pr_dictvar) v)
  14.343 +        fun pr_dict fxy (DictConst (inst, dss)) =
  14.344 +              brackify fxy ((str o deresolve) inst :: map (pr_dicts BR) dss)
  14.345 +          | pr_dict fxy (DictVar (classrels, v)) =
  14.346 +              pr_proj (map (str o deresolve) classrels) ((str o pr_dictvar) v)
  14.347        in case ds
  14.348         of [] => str "()"
  14.349 -        | [d] => pr_dictc fxy d
  14.350 -        | _ :: _ => (Pretty.list "(" ")" o map (pr_dictc NOBR)) ds
  14.351 +        | [d] => pr_dict fxy d
  14.352 +        | _ :: _ => (Pretty.list "(" ")" o map (pr_dict NOBR)) ds
  14.353        end;
  14.354 -    fun pr_tyvars vs =
  14.355 +    fun pr_tyvar_dicts vs =
  14.356        vs
  14.357        |> map (fn (v, sort) => map_index (fn (i, _) =>
  14.358             DictVar ([], (v, (i, length sort)))) sort)
  14.359        |> map (pr_dicts BR);
  14.360      fun pr_tycoexpr fxy (tyco, tys) =
  14.361        let
  14.362 -        val tyco' = (str o deresolv) tyco
  14.363 +        val tyco' = (str o deresolve) tyco
  14.364        in case map (pr_typ BR) tys
  14.365         of [] => tyco'
  14.366          | [p] => Pretty.block [p, Pretty.brk 1, tyco']
  14.367          | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco']
  14.368        end
  14.369      and pr_typ fxy (tyco `%% tys) =
  14.370 -          (case tyco_syntax tyco
  14.371 +          (case syntax_tyco tyco
  14.372             of NONE => pr_tycoexpr fxy (tyco, tys)
  14.373              | SOME (i, pr) =>
  14.374                  if not (i = length tys)
  14.375 @@ -484,7 +499,7 @@
  14.376            in brackets (ps @ [pr_term lhs vars' NOBR t']) end
  14.377        | pr_term lhs vars fxy (ICase (cases as (_, t0))) =
  14.378            (case CodeThingol.unfold_const_app t0
  14.379 -           of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
  14.380 +           of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
  14.381                  then pr_case vars fxy cases
  14.382                  else pr_app lhs vars fxy c_ts
  14.383              | NONE => pr_case vars fxy cases)
  14.384 @@ -492,13 +507,13 @@
  14.385        if is_cons c then let
  14.386          val k = length tys
  14.387        in if k < 2 then 
  14.388 -        (str o deresolv) c :: map (pr_term lhs vars BR) ts
  14.389 +        (str o deresolve) c :: map (pr_term lhs vars BR) ts
  14.390        else if k = length ts then
  14.391 -        [(str o deresolv) c, Pretty.enum "," "(" ")" (map (pr_term lhs vars NOBR) ts)]
  14.392 +        [(str o deresolve) c, Pretty.enum "," "(" ")" (map (pr_term lhs vars NOBR) ts)]
  14.393        else [pr_term lhs vars BR (CodeThingol.eta_expand app k)] end else
  14.394 -        (str o deresolv) c
  14.395 +        (str o deresolve) c
  14.396            :: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term lhs vars BR) ts
  14.397 -    and pr_app lhs vars = gen_pr_app pr_app' pr_term const_syntax
  14.398 +    and pr_app lhs vars = gen_pr_app pr_app' pr_term syntax_const
  14.399        labelled_name is_cons lhs vars
  14.400      and pr_bind' ((NONE, NONE), _) = str "_"
  14.401        | pr_bind' ((SOME v, NONE), _) = str v
  14.402 @@ -537,7 +552,7 @@
  14.403              )
  14.404            end
  14.405        | pr_case vars fxy ((_, []), _) = str "raise Fail \"empty case\""
  14.406 -    fun pr_def (MLFuns (funns as (funn :: funns'))) =
  14.407 +    fun pr_stmt (MLFuns (funns as (funn :: funns'))) =
  14.408            let
  14.409              val definer =
  14.410                let
  14.411 @@ -553,46 +568,45 @@
  14.412                        else error ("Mixing simultaneous vals and funs not implemented: "
  14.413                          ^ commas (map (labelled_name o fst) funns));
  14.414                in the (fold chk funns NONE) end;
  14.415 -            fun pr_funn definer (name, ((raw_vs, ty), [])) =
  14.416 +            fun pr_funn definer (name, ((vs, ty), [])) =
  14.417                    let
  14.418 -                    val vs = filter_out (null o snd) raw_vs;
  14.419 -                    val n = length vs + (length o fst o CodeThingol.unfold_fun) ty;
  14.420 +                    val vs_dict = filter_out (null o snd) vs;
  14.421 +                    val n = length vs_dict + (length o fst o CodeThingol.unfold_fun) ty;
  14.422                      val exc_str =
  14.423                        (ML_Syntax.print_string o NameSpace.base o NameSpace.qualifier) name;
  14.424                    in
  14.425                      concat (
  14.426                        str definer
  14.427 -                      :: (str o deresolv) name
  14.428 +                      :: (str o deresolve) name
  14.429                        :: map str (replicate n "_")
  14.430                        @ str "="
  14.431                        :: str "raise"
  14.432                        :: str "(Fail"
  14.433 -                      :: str exc_str
  14.434 -                      @@ str ")"
  14.435 +                      @@ str (exc_str ^ ")")
  14.436                      )
  14.437                    end
  14.438 -              | pr_funn definer (name, ((raw_vs, ty), eqs as eq :: eqs')) =
  14.439 +              | pr_funn definer (name, ((vs, ty), eqs as eq :: eqs')) =
  14.440                    let
  14.441 -                    val vs = filter_out (null o snd) raw_vs;
  14.442 +                    val vs_dict = filter_out (null o snd) vs;
  14.443                      val shift = if null eqs' then I else
  14.444                        map (Pretty.block o single o Pretty.block o single);
  14.445                      fun pr_eq definer (ts, t) =
  14.446                        let
  14.447                          val consts = map_filter
  14.448 -                          (fn c => if (is_some o const_syntax) c
  14.449 -                            then NONE else (SOME o NameSpace.base o deresolv) c)
  14.450 +                          (fn c => if (is_some o syntax_const) c
  14.451 +                            then NONE else (SOME o NameSpace.base o deresolve) c)
  14.452                              ((fold o CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []);
  14.453 -                        val vars = init_syms
  14.454 +                        val vars = reserved_names
  14.455                            |> CodeName.intro_vars consts
  14.456                            |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames)
  14.457                                 (insert (op =)) ts []);
  14.458                        in
  14.459                          concat (
  14.460 -                          [str definer, (str o deresolv) name]
  14.461 -                          @ (if null ts andalso null vs
  14.462 +                          [str definer, (str o deresolve) name]
  14.463 +                          @ (if null ts andalso null vs_dict
  14.464                               then [str ":", pr_typ NOBR ty]
  14.465                               else
  14.466 -                               pr_tyvars vs
  14.467 +                               pr_tyvar_dicts vs_dict
  14.468                                 @ map (pr_term true vars BR) ts)
  14.469                         @ [str "=", pr_term false vars NOBR t]
  14.470                          )
  14.471 @@ -605,13 +619,13 @@
  14.472                    end;
  14.473              val (ps, p) = split_last (pr_funn definer funn :: map (pr_funn "and") funns');
  14.474            in Pretty.chunks (ps @ [Pretty.block ([p, str ";"])]) end
  14.475 -     | pr_def (MLDatas (datas as (data :: datas'))) =
  14.476 +     | pr_stmt (MLDatas (datas as (data :: datas'))) =
  14.477            let
  14.478              fun pr_co (co, []) =
  14.479 -                  str (deresolv co)
  14.480 +                  str (deresolve co)
  14.481                | pr_co (co, tys) =
  14.482                    concat [
  14.483 -                    str (deresolv co),
  14.484 +                    str (deresolve co),
  14.485                      str "of",
  14.486                      Pretty.enum " *" "" "" (map (pr_typ (INFX (2, X))) tys)
  14.487                    ];
  14.488 @@ -632,12 +646,12 @@
  14.489              val (ps, p) = split_last
  14.490                (pr_data "datatype" data :: map (pr_data "and") datas');
  14.491            in Pretty.chunks (ps @ [Pretty.block ([p, str ";"])]) end
  14.492 -     | pr_def (MLClass (class, (v, (superclasses, classparams)))) =
  14.493 +     | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) =
  14.494            let
  14.495              val w = first_upper v ^ "_";
  14.496              fun pr_superclass_field (class, classrel) =
  14.497                (concat o map str) [
  14.498 -                pr_label_classrel classrel, ":", "'" ^ v, deresolv class
  14.499 +                pr_label_classrel classrel, ":", "'" ^ v, deresolve class
  14.500                ];
  14.501              fun pr_classparam_field (classparam, ty) =
  14.502                concat [
  14.503 @@ -646,8 +660,8 @@
  14.504              fun pr_classparam_proj (classparam, _) =
  14.505                semicolon [
  14.506                  str "fun",
  14.507 -                (str o deresolv) classparam,
  14.508 -                Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolv class)],
  14.509 +                (str o deresolve) classparam,
  14.510 +                Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolve class)],
  14.511                  str "=",
  14.512                  str ("#" ^ pr_label_classparam classparam),
  14.513                  str w
  14.514 @@ -655,8 +669,8 @@
  14.515              fun pr_superclass_proj (_, classrel) =
  14.516                semicolon [
  14.517                  str "fun",
  14.518 -                (str o deresolv) classrel,
  14.519 -                Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolv class)],
  14.520 +                (str o deresolve) classrel,
  14.521 +                Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolve class)],
  14.522                  str "=",
  14.523                  str ("#" ^ pr_label_classrel classrel),
  14.524                  str w
  14.525 @@ -665,7 +679,7 @@
  14.526              Pretty.chunks (
  14.527                concat [
  14.528                  str ("type '" ^ v),
  14.529 -                (str o deresolv) class,
  14.530 +                (str o deresolve) class,
  14.531                  str "=",
  14.532                  Pretty.enum "," "{" "};" (
  14.533                    map pr_superclass_field superclasses @ map pr_classparam_field classparams
  14.534 @@ -675,7 +689,7 @@
  14.535                @ map pr_classparam_proj classparams
  14.536              )
  14.537            end
  14.538 -     | pr_def (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) =
  14.539 +     | pr_stmt (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) =
  14.540            let
  14.541              fun pr_superclass (_, (classrel, dss)) =
  14.542                concat [
  14.543 @@ -687,13 +701,13 @@
  14.544                concat [
  14.545                  (str o pr_label_classparam) classparam,
  14.546                  str "=",
  14.547 -                pr_app false init_syms NOBR (c_inst, [])
  14.548 +                pr_app false reserved_names NOBR (c_inst, [])
  14.549                ];
  14.550            in
  14.551              semicolon ([
  14.552                str (if null arity then "val" else "fun"),
  14.553 -              (str o deresolv) inst ] @
  14.554 -              pr_tyvars arity @ [
  14.555 +              (str o deresolve) inst ] @
  14.556 +              pr_tyvar_dicts arity @ [
  14.557                str "=",
  14.558                Pretty.enum "," "{" "}"
  14.559                  (map pr_superclass superarities @ map pr_classparam classparam_insts),
  14.560 @@ -701,20 +715,19 @@
  14.561                pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])
  14.562              ])
  14.563            end;
  14.564 -  in pr_def ml_def end;
  14.565 +  in pr_stmt end;
  14.566  
  14.567 -fun pr_sml_modl name content =
  14.568 -  Pretty.chunks ([
  14.569 -    str ("structure " ^ name ^ " = "),
  14.570 -    str "struct",
  14.571 -    str ""
  14.572 -  ] @ content @ [
  14.573 -    str "",
  14.574 -    str ("end; (*struct " ^ name ^ "*)")
  14.575 -  ]);
  14.576 +fun pr_sml_module name content =
  14.577 +  Pretty.chunks (
  14.578 +    str ("structure " ^ name ^ " = ")
  14.579 +    :: str "struct"
  14.580 +    :: str ""
  14.581 +    :: content
  14.582 +    @ str ""
  14.583 +    @@ str ("end; (*struct " ^ name ^ "*)")
  14.584 +  );
  14.585  
  14.586 -fun pr_ocaml tyco_syntax const_syntax labelled_name
  14.587 -    init_syms deresolv is_cons ml_def =
  14.588 +fun pr_ocaml_stmt syntax_tyco syntax_const labelled_name reserved_names deresolve is_cons =
  14.589    let
  14.590      fun pr_dicts fxy ds =
  14.591        let
  14.592 @@ -722,30 +735,30 @@
  14.593            | pr_dictvar (v, (i, _)) = "_" ^ first_upper v ^ string_of_int (i+1);
  14.594          fun pr_proj ps p =
  14.595            fold_rev (fn p2 => fn p1 => Pretty.block [p1, str ".", str p2]) ps p
  14.596 -        fun pr_dictc fxy (DictConst (inst, dss)) =
  14.597 -              brackify fxy ((str o deresolv) inst :: map (pr_dicts BR) dss)
  14.598 -          | pr_dictc fxy (DictVar (classrels, v)) =
  14.599 -              pr_proj (map deresolv classrels) ((str o pr_dictvar) v)
  14.600 +        fun pr_dict fxy (DictConst (inst, dss)) =
  14.601 +              brackify fxy ((str o deresolve) inst :: map (pr_dicts BR) dss)
  14.602 +          | pr_dict fxy (DictVar (classrels, v)) =
  14.603 +              pr_proj (map deresolve classrels) ((str o pr_dictvar) v)
  14.604        in case ds
  14.605         of [] => str "()"
  14.606 -        | [d] => pr_dictc fxy d
  14.607 -        | _ :: _ => (Pretty.list "(" ")" o map (pr_dictc NOBR)) ds
  14.608 +        | [d] => pr_dict fxy d
  14.609 +        | _ :: _ => (Pretty.list "(" ")" o map (pr_dict NOBR)) ds
  14.610        end;
  14.611 -    fun pr_tyvars vs =
  14.612 +    fun pr_tyvar_dicts vs =
  14.613        vs
  14.614        |> map (fn (v, sort) => map_index (fn (i, _) =>
  14.615             DictVar ([], (v, (i, length sort)))) sort)
  14.616        |> map (pr_dicts BR);
  14.617      fun pr_tycoexpr fxy (tyco, tys) =
  14.618        let
  14.619 -        val tyco' = (str o deresolv) tyco
  14.620 +        val tyco' = (str o deresolve) tyco
  14.621        in case map (pr_typ BR) tys
  14.622         of [] => tyco'
  14.623          | [p] => Pretty.block [p, Pretty.brk 1, tyco']
  14.624          | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco']
  14.625        end
  14.626      and pr_typ fxy (tyco `%% tys) =
  14.627 -          (case tyco_syntax tyco
  14.628 +          (case syntax_tyco tyco
  14.629             of NONE => pr_tycoexpr fxy (tyco, tys)
  14.630              | SOME (i, pr) =>
  14.631                  if not (i = length tys)
  14.632 @@ -771,7 +784,7 @@
  14.633              val (ps, vars') = fold_map pr binds vars;
  14.634            in brackets (str "fun" :: ps @ str "->" @@ pr_term lhs vars' NOBR t') end
  14.635        | pr_term lhs vars fxy (ICase (cases as (_, t0))) = (case CodeThingol.unfold_const_app t0
  14.636 -           of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
  14.637 +           of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
  14.638                  then pr_case vars fxy cases
  14.639                  else pr_app lhs vars fxy c_ts
  14.640              | NONE => pr_case vars fxy cases)
  14.641 @@ -779,14 +792,14 @@
  14.642        if is_cons c then
  14.643          if length tys = length ts
  14.644          then case ts
  14.645 -         of [] => [(str o deresolv) c]
  14.646 -          | [t] => [(str o deresolv) c, pr_term lhs vars BR t]
  14.647 -          | _ => [(str o deresolv) c, Pretty.enum "," "(" ")"
  14.648 +         of [] => [(str o deresolve) c]
  14.649 +          | [t] => [(str o deresolve) c, pr_term lhs vars BR t]
  14.650 +          | _ => [(str o deresolve) c, Pretty.enum "," "(" ")"
  14.651                      (map (pr_term lhs vars NOBR) ts)]
  14.652          else [pr_term lhs vars BR (CodeThingol.eta_expand app (length tys))]
  14.653 -      else (str o deresolv) c
  14.654 +      else (str o deresolve) c
  14.655          :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term lhs vars BR) ts)
  14.656 -    and pr_app lhs vars = gen_pr_app pr_app' pr_term const_syntax
  14.657 +    and pr_app lhs vars = gen_pr_app pr_app' pr_term syntax_const
  14.658        labelled_name is_cons lhs vars
  14.659      and pr_bind' ((NONE, NONE), _) = str "_"
  14.660        | pr_bind' ((SOME v, NONE), _) = str v
  14.661 @@ -818,28 +831,28 @@
  14.662              )
  14.663            end
  14.664        | pr_case vars fxy ((_, []), _) = str "failwith \"empty case\"";
  14.665 -    fun pr_def (MLFuns (funns as funn :: funns')) =
  14.666 +    fun fish_params vars eqs =
  14.667 +      let
  14.668 +        fun fish_param _ (w as SOME _) = w
  14.669 +          | fish_param (IVar v) NONE = SOME v
  14.670 +          | fish_param _ NONE = NONE;
  14.671 +        fun fillup_param _ (_, SOME v) = v
  14.672 +          | fillup_param x (i, NONE) = x ^ string_of_int i;
  14.673 +        val fished1 = fold (map2 fish_param) eqs (replicate (length (hd eqs)) NONE);
  14.674 +        val x = Name.variant (map_filter I fished1) "x";
  14.675 +        val fished2 = map_index (fillup_param x) fished1;
  14.676 +        val (fished3, _) = Name.variants fished2 Name.context;
  14.677 +        val vars' = CodeName.intro_vars fished3 vars;
  14.678 +      in map (CodeName.lookup_var vars') fished3 end;
  14.679 +    fun pr_stmt (MLFuns (funns as funn :: funns')) =
  14.680            let
  14.681 -            fun fish_parm _ (w as SOME _) = w
  14.682 -              | fish_parm (IVar v) NONE = SOME v
  14.683 -              | fish_parm _ NONE = NONE;
  14.684 -            fun fillup_parm _ (_, SOME v) = v
  14.685 -              | fillup_parm x (i, NONE) = x ^ string_of_int i;
  14.686 -            fun fish_parms vars eqs =
  14.687 -              let
  14.688 -                val fished1 = fold (map2 fish_parm) eqs (replicate (length (hd eqs)) NONE);
  14.689 -                val x = Name.variant (map_filter I fished1) "x";
  14.690 -                val fished2 = map_index (fillup_parm x) fished1;
  14.691 -                val (fished3, _) = Name.variants fished2 Name.context;
  14.692 -                val vars' = CodeName.intro_vars fished3 vars;
  14.693 -              in map (CodeName.lookup_var vars') fished3 end;
  14.694              fun pr_eq (ts, t) =
  14.695                let
  14.696                  val consts = map_filter
  14.697 -                  (fn c => if (is_some o const_syntax) c
  14.698 -                    then NONE else (SOME o NameSpace.base o deresolv) c)
  14.699 +                  (fn c => if (is_some o syntax_const) c
  14.700 +                    then NONE else (SOME o NameSpace.base o deresolve) c)
  14.701                      ((fold o CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []);
  14.702 -                val vars = init_syms
  14.703 +                val vars = reserved_names
  14.704                    |> CodeName.intro_vars consts
  14.705                    |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames)
  14.706                        (insert (op =)) ts []);
  14.707 @@ -864,10 +877,10 @@
  14.708                | pr_eqs _ _ [(ts, t)] =
  14.709                    let
  14.710                      val consts = map_filter
  14.711 -                      (fn c => if (is_some o const_syntax) c
  14.712 -                        then NONE else (SOME o NameSpace.base o deresolv) c)
  14.713 +                      (fn c => if (is_some o syntax_const) c
  14.714 +                        then NONE else (SOME o NameSpace.base o deresolve) c)
  14.715                          ((fold o CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []);
  14.716 -                    val vars = init_syms
  14.717 +                    val vars = reserved_names
  14.718                        |> CodeName.intro_vars consts
  14.719                        |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames)
  14.720                            (insert (op =)) ts []);
  14.721 @@ -891,13 +904,13 @@
  14.722                | pr_eqs _ _ (eqs as eq :: eqs') =
  14.723                    let
  14.724                      val consts = map_filter
  14.725 -                      (fn c => if (is_some o const_syntax) c
  14.726 -                        then NONE else (SOME o NameSpace.base o deresolv) c)
  14.727 +                      (fn c => if (is_some o syntax_const) c
  14.728 +                        then NONE else (SOME o NameSpace.base o deresolve) c)
  14.729                          ((fold o CodeThingol.fold_constnames)
  14.730                            (insert (op =)) (map snd eqs) []);
  14.731 -                    val vars = init_syms
  14.732 +                    val vars = reserved_names
  14.733                        |> CodeName.intro_vars consts;
  14.734 -                    val dummy_parms = (map str o fish_parms vars o map fst) eqs;
  14.735 +                    val dummy_parms = (map str o fish_params vars o map fst) eqs;
  14.736                    in
  14.737                      Pretty.block (
  14.738                        Pretty.breaks dummy_parms
  14.739 @@ -918,20 +931,20 @@
  14.740              fun pr_funn definer (name, ((vs, ty), eqs)) =
  14.741                concat (
  14.742                  str definer
  14.743 -                :: (str o deresolv) name
  14.744 -                :: pr_tyvars (filter_out (null o snd) vs)
  14.745 +                :: (str o deresolve) name
  14.746 +                :: pr_tyvar_dicts (filter_out (null o snd) vs)
  14.747                  @| pr_eqs name ty eqs
  14.748                );
  14.749              val (ps, p) = split_last
  14.750                (pr_funn "let rec" funn :: map (pr_funn "and") funns');
  14.751            in Pretty.chunks (ps @ [Pretty.block ([p, str ";;"])]) end
  14.752 -     | pr_def (MLDatas (datas as (data :: datas'))) =
  14.753 +     | pr_stmt (MLDatas (datas as (data :: datas'))) =
  14.754            let
  14.755              fun pr_co (co, []) =
  14.756 -                  str (deresolv co)
  14.757 +                  str (deresolve co)
  14.758                | pr_co (co, tys) =
  14.759                    concat [
  14.760 -                    str (deresolv co),
  14.761 +                    str (deresolve co),
  14.762                      str "of",
  14.763                      Pretty.enum " *" "" "" (map (pr_typ (INFX (2, X))) tys)
  14.764                    ];
  14.765 @@ -952,29 +965,29 @@
  14.766              val (ps, p) = split_last
  14.767                (pr_data "type" data :: map (pr_data "and") datas');
  14.768            in Pretty.chunks (ps @ [Pretty.block ([p, str ";;"])]) end
  14.769 -     | pr_def (MLClass (class, (v, (superclasses, classparams)))) =
  14.770 +     | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) =
  14.771            let
  14.772              val w = "_" ^ first_upper v;
  14.773              fun pr_superclass_field (class, classrel) =
  14.774                (concat o map str) [
  14.775 -                deresolv classrel, ":", "'" ^ v, deresolv class
  14.776 +                deresolve classrel, ":", "'" ^ v, deresolve class
  14.777                ];
  14.778              fun pr_classparam_field (classparam, ty) =
  14.779                concat [
  14.780 -                (str o deresolv) classparam, str ":", pr_typ NOBR ty
  14.781 +                (str o deresolve) classparam, str ":", pr_typ NOBR ty
  14.782                ];
  14.783              fun pr_classparam_proj (classparam, _) =
  14.784                concat [
  14.785                  str "let",
  14.786 -                (str o deresolv) classparam,
  14.787 +                (str o deresolve) classparam,
  14.788                  str w,
  14.789                  str "=",
  14.790 -                str (w ^ "." ^ deresolv classparam ^ ";;")
  14.791 +                str (w ^ "." ^ deresolve classparam ^ ";;")
  14.792                ];
  14.793            in Pretty.chunks (
  14.794              concat [
  14.795                str ("type '" ^ v),
  14.796 -              (str o deresolv) class,
  14.797 +              (str o deresolve) class,
  14.798                str "=",
  14.799                enum_default "();;" ";" "{" "};;" (
  14.800                  map pr_superclass_field superclasses
  14.801 @@ -983,25 +996,25 @@
  14.802              ]
  14.803              :: map pr_classparam_proj classparams
  14.804            ) end
  14.805 -     | pr_def (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) =
  14.806 +     | pr_stmt (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) =
  14.807            let
  14.808              fun pr_superclass (_, (classrel, dss)) =
  14.809                concat [
  14.810 -                (str o deresolv) classrel,
  14.811 +                (str o deresolve) classrel,
  14.812                  str "=",
  14.813                  pr_dicts NOBR [DictConst dss]
  14.814                ];
  14.815              fun pr_classparam_inst (classparam, c_inst) =
  14.816                concat [
  14.817 -                (str o deresolv) classparam,
  14.818 +                (str o deresolve) classparam,
  14.819                  str "=",
  14.820 -                pr_app false init_syms NOBR (c_inst, [])
  14.821 +                pr_app false reserved_names NOBR (c_inst, [])
  14.822                ];
  14.823            in
  14.824              concat (
  14.825                str "let"
  14.826 -              :: (str o deresolv) inst
  14.827 -              :: pr_tyvars arity
  14.828 +              :: (str o deresolve) inst
  14.829 +              :: pr_tyvar_dicts arity
  14.830                @ str "="
  14.831                @@ (Pretty.enclose "(" ");;" o Pretty.breaks) [
  14.832                  enum_default "()" ";" "{" "}" (map pr_superclass superarities
  14.833 @@ -1011,33 +1024,37 @@
  14.834                ]
  14.835              )
  14.836            end;
  14.837 -  in pr_def ml_def end;
  14.838 +  in pr_stmt end;
  14.839 +
  14.840 +fun pr_ocaml_module name content =
  14.841 +  Pretty.chunks (
  14.842 +    str ("module " ^ name ^ " = ")
  14.843 +    :: str "struct"
  14.844 +    :: str ""
  14.845 +    :: content
  14.846 +    @ str ""
  14.847 +    @@ str ("end;; (*struct " ^ name ^ "*)")
  14.848 +  );
  14.849  
  14.850 -fun pr_ocaml_modl name content =
  14.851 -  Pretty.chunks ([
  14.852 -    str ("module " ^ name ^ " = "),
  14.853 -    str "struct",
  14.854 -    str ""
  14.855 -  ] @ content @ [
  14.856 -    str "",
  14.857 -    str ("end;; (*struct " ^ name ^ "*)")
  14.858 -  ]);
  14.859 +local
  14.860 +
  14.861 +datatype ml_node =
  14.862 +    Dummy of string
  14.863 +  | Stmt of string * ml_stmt
  14.864 +  | Module of string * ((Name.context * Name.context) * ml_node Graph.T);
  14.865  
  14.866 -fun seri_ml internal output_cont pr_def pr_modl module labelled_name reserved_syms includes raw_module_alias
  14.867 -  (_ : string -> class_syntax option) tyco_syntax const_syntax code cs seri_dest =
  14.868 +in
  14.869 +
  14.870 +fun ml_node_of_program labelled_name module_name reserved_names raw_module_alias program =
  14.871    let
  14.872 -    val module_alias = if is_some module then K module else raw_module_alias;
  14.873 -    val is_cons = CodeThingol.is_cons code;
  14.874 -    datatype node =
  14.875 -        Def of string * ml_def option
  14.876 -      | Module of string * ((Name.context * Name.context) * node Graph.T);
  14.877 -    val init_names = Name.make_context reserved_syms;
  14.878 -    val init_module = ((init_names, init_names), Graph.empty);
  14.879 +    val module_alias = if is_some module_name then K module_name else raw_module_alias;
  14.880 +    val reserved_names = Name.make_context reserved_names;
  14.881 +    val empty_module = ((reserved_names, reserved_names), Graph.empty);
  14.882      fun map_node [] f = f
  14.883        | map_node (m::ms) f =
  14.884 -          Graph.default_node (m, Module (m, init_module))
  14.885 -          #> Graph.map_node m (fn (Module (dmodlname, (nsp, nodes))) =>
  14.886 -               Module (dmodlname, (nsp, map_node ms f nodes)));
  14.887 +          Graph.default_node (m, Module (m, empty_module))
  14.888 +          #> Graph.map_node m (fn (Module (module_name, (nsp, nodes))) =>
  14.889 +               Module (module_name, (nsp, map_node ms f nodes)));
  14.890      fun map_nsp_yield [] f (nsp, nodes) =
  14.891            let
  14.892              val (x, nsp') = f nsp
  14.893 @@ -1046,193 +1063,202 @@
  14.894            let
  14.895              val (x, nodes') =
  14.896                nodes
  14.897 -              |> Graph.default_node (m, Module (m, init_module))
  14.898 -              |> Graph.map_node_yield m (fn Module (dmodlname, nsp_nodes) => 
  14.899 +              |> Graph.default_node (m, Module (m, empty_module))
  14.900 +              |> Graph.map_node_yield m (fn Module (d_module_name, nsp_nodes) => 
  14.901                    let
  14.902                      val (x, nsp_nodes') = map_nsp_yield ms f nsp_nodes
  14.903 -                  in (x, Module (dmodlname, nsp_nodes')) end)
  14.904 +                  in (x, Module (d_module_name, nsp_nodes')) end)
  14.905            in (x, (nsp, nodes')) end;
  14.906 -    val init_syms = CodeName.make_vars reserved_syms;
  14.907 -    val name_modl = mk_modl_name_tab init_names NONE module_alias code;
  14.908 -    fun name_def upper name nsp =
  14.909 +    fun map_nsp_fun_yield f (nsp_fun, nsp_typ) =
  14.910 +      let
  14.911 +        val (x, nsp_fun') = f nsp_fun
  14.912 +      in (x, (nsp_fun', nsp_typ)) end;
  14.913 +    fun map_nsp_typ_yield f (nsp_fun, nsp_typ) =
  14.914 +      let
  14.915 +        val (x, nsp_typ') = f nsp_typ
  14.916 +      in (x, (nsp_fun, nsp_typ')) end;
  14.917 +    val mk_name_module = mk_name_module reserved_names NONE module_alias program;
  14.918 +    fun mk_name_stmt upper name nsp =
  14.919        let
  14.920          val (_, base) = dest_name name;
  14.921          val base' = if upper then first_upper base else base;
  14.922          val ([base''], nsp') = Name.variants [base'] nsp;
  14.923        in (base'', nsp') end;
  14.924 -    fun map_nsp_fun f (nsp_fun, nsp_typ) =
  14.925 -      let
  14.926 -        val (x, nsp_fun') = f nsp_fun
  14.927 -      in (x, (nsp_fun', nsp_typ)) end;
  14.928 -    fun map_nsp_typ f (nsp_fun, nsp_typ) =
  14.929 -      let
  14.930 -        val (x, nsp_typ') = f nsp_typ
  14.931 -      in (x, (nsp_fun, nsp_typ')) end;
  14.932 -    fun mk_funs defs =
  14.933 +    fun add_funs stmts =
  14.934        fold_map
  14.935 -        (fn (name, CodeThingol.Fun info) =>
  14.936 -              map_nsp_fun (name_def false name) >>
  14.937 -                (fn base => (base, (name, (apsnd o map) fst info)))
  14.938 -          | (name, def) =>
  14.939 +        (fn (name, CodeThingol.Fun stmt) =>
  14.940 +              map_nsp_fun_yield (mk_name_stmt false name) #>>
  14.941 +                rpair (name, (apsnd o map) fst stmt)
  14.942 +          | (name, _) =>
  14.943                error ("Function block containing illegal statement: " ^ labelled_name name)
  14.944 -        ) defs
  14.945 -      >> (split_list #> apsnd MLFuns);
  14.946 -    fun mk_datatype defs =
  14.947 +        ) stmts
  14.948 +      #>> (split_list #> apsnd MLFuns);
  14.949 +    fun add_datatypes stmts =
  14.950        fold_map
  14.951 -        (fn (name, CodeThingol.Datatype info) =>
  14.952 -              map_nsp_typ (name_def false name) >> (fn base => (base, SOME (name, info)))
  14.953 +        (fn (name, CodeThingol.Datatype stmt) =>
  14.954 +              map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, stmt))
  14.955            | (name, CodeThingol.Datatypecons _) =>
  14.956 -              map_nsp_fun (name_def true name) >> (fn base => (base, NONE))
  14.957 -          | (name, def) =>
  14.958 +              map_nsp_fun_yield (mk_name_stmt true name) #>> rpair NONE
  14.959 +          | (name, _) =>
  14.960                error ("Datatype block containing illegal statement: " ^ labelled_name name)
  14.961 -        ) defs
  14.962 -      >> (split_list #> apsnd (map_filter I
  14.963 +        ) stmts
  14.964 +      #>> (split_list #> apsnd (map_filter I
  14.965          #> (fn [] => error ("Datatype block without data statement: "
  14.966 -                  ^ (commas o map (labelled_name o fst)) defs)
  14.967 -             | infos => MLDatas infos)));
  14.968 -    fun mk_class defs =
  14.969 +                  ^ (commas o map (labelled_name o fst)) stmts)
  14.970 +             | stmts => MLDatas stmts)));
  14.971 +    fun add_class stmts =
  14.972        fold_map
  14.973          (fn (name, CodeThingol.Class info) =>
  14.974 -              map_nsp_typ (name_def false name) >> (fn base => (base, SOME (name, info)))
  14.975 +              map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, info))
  14.976            | (name, CodeThingol.Classrel _) =>
  14.977 -              map_nsp_fun (name_def false name) >> (fn base => (base, NONE))
  14.978 +              map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE
  14.979            | (name, CodeThingol.Classparam _) =>
  14.980 -              map_nsp_fun (name_def false name) >> (fn base => (base, NONE))
  14.981 -          | (name, def) =>
  14.982 +              map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE
  14.983 +          | (name, _) =>
  14.984                error ("Class block containing illegal statement: " ^ labelled_name name)
  14.985 -        ) defs
  14.986 -      >> (split_list #> apsnd (map_filter I
  14.987 +        ) stmts
  14.988 +      #>> (split_list #> apsnd (map_filter I
  14.989          #> (fn [] => error ("Class block without class statement: "
  14.990 -                  ^ (commas o map (labelled_name o fst)) defs)
  14.991 -             | [info] => MLClass info)));
  14.992 -    fun mk_inst [(name, CodeThingol.Classinst info)] =
  14.993 -      map_nsp_fun (name_def false name)
  14.994 -      >> (fn base => ([base], MLClassinst (name, (apsnd o apsnd o map) fst info)));
  14.995 -    fun add_group mk defs nsp_nodes =
  14.996 +                  ^ (commas o map (labelled_name o fst)) stmts)
  14.997 +             | [stmt] => MLClass stmt)));
  14.998 +    fun add_inst [(name, CodeThingol.Classinst stmt)] =
  14.999 +      map_nsp_fun_yield (mk_name_stmt false name)
 14.1000 +      #>> (fn base => ([base], MLClassinst (name, (apsnd o apsnd o map) fst stmt)));
 14.1001 +    fun add_stmts ((stmts as (_, CodeThingol.Fun _)::_)) =
 14.1002 +          add_funs stmts
 14.1003 +      | add_stmts ((stmts as (_, CodeThingol.Datatypecons _)::_)) =
 14.1004 +          add_datatypes stmts
 14.1005 +      | add_stmts ((stmts as (_, CodeThingol.Datatype _)::_)) =
 14.1006 +          add_datatypes stmts
 14.1007 +      | add_stmts ((stmts as (_, CodeThingol.Class _)::_)) =
 14.1008 +          add_class stmts
 14.1009 +      | add_stmts ((stmts as (_, CodeThingol.Classrel _)::_)) =
 14.1010 +          add_class stmts
 14.1011 +      | add_stmts ((stmts as (_, CodeThingol.Classparam _)::_)) =
 14.1012 +          add_class stmts
 14.1013 +      | add_stmts ((stmts as [(_, CodeThingol.Classinst _)])) =
 14.1014 +          add_inst stmts
 14.1015 +      | add_stmts stmts = error ("Illegal mutual dependencies: " ^
 14.1016 +          (commas o map (labelled_name o fst)) stmts);
 14.1017 +    fun add_stmts' stmts nsp_nodes =
 14.1018        let
 14.1019 -        val names as (name :: names') = map fst defs;
 14.1020 +        val names as (name :: names') = map fst stmts;
 14.1021          val deps =
 14.1022            []
 14.1023 -          |> fold (fold (insert (op =)) o Graph.imm_succs code) names
 14.1024 +          |> fold (fold (insert (op =)) o Graph.imm_succs program) names
 14.1025            |> subtract (op =) names;
 14.1026 -        val (modls, _) = (split_list o map dest_name) names;
 14.1027 -        val modl' = (the_single o distinct (op =) o map name_modl) modls
 14.1028 +        val (module_names, _) = (split_list o map dest_name) names;
 14.1029 +        val module_name = (the_single o distinct (op =) o map mk_name_module) module_names
 14.1030            handle Empty =>
 14.1031              error ("Different namespace prefixes for mutual dependencies:\n"
 14.1032                ^ commas (map labelled_name names)
 14.1033                ^ "\n"
 14.1034 -              ^ commas (map (NameSpace.qualifier o NameSpace.qualifier) names));
 14.1035 -        val modl_explode = NameSpace.explode modl';
 14.1036 -        fun add_dep name name'' =
 14.1037 +              ^ commas module_names);
 14.1038 +        val module_name_path = NameSpace.explode module_name;
 14.1039 +        fun add_dep name name' =
 14.1040            let
 14.1041 -            val modl'' = (name_modl o fst o dest_name) name'';
 14.1042 -          in if modl' = modl'' then
 14.1043 -            map_node modl_explode
 14.1044 -              (Graph.add_edge (name, name''))
 14.1045 +            val module_name' = (mk_name_module o fst o dest_name) name';
 14.1046 +          in if module_name = module_name' then
 14.1047 +            map_node module_name_path (Graph.add_edge (name, name'))
 14.1048            else let
 14.1049              val (common, (diff1::_, diff2::_)) = chop_prefix (op =)
 14.1050 -              (modl_explode, NameSpace.explode modl'');
 14.1051 +              (module_name_path, NameSpace.explode module_name');
 14.1052            in
 14.1053              map_node common
 14.1054 -              (fn gr => Graph.add_edge_acyclic (diff1, diff2) gr
 14.1055 +              (fn node => Graph.add_edge_acyclic (diff1, diff2) node
 14.1056                  handle Graph.CYCLES _ => error ("Dependency "
 14.1057 -                  ^ quote name ^ " -> " ^ quote name''
 14.1058 +                  ^ quote name ^ " -> " ^ quote name'
 14.1059                    ^ " would result in module dependency cycle"))
 14.1060            end end;
 14.1061        in
 14.1062          nsp_nodes
 14.1063 -        |> map_nsp_yield modl_explode (mk defs)
 14.1064 -        |-> (fn (base' :: bases', def') =>
 14.1065 -           apsnd (map_node modl_explode (Graph.new_node (name, (Def (base', SOME def')))
 14.1066 +        |> map_nsp_yield module_name_path (add_stmts stmts)
 14.1067 +        |-> (fn (base' :: bases', stmt') =>
 14.1068 +           apsnd (map_node module_name_path (Graph.new_node (name, (Stmt (base', stmt')))
 14.1069                #> fold2 (fn name' => fn base' =>
 14.1070 -                   Graph.new_node (name', (Def (base', NONE)))) names' bases')))
 14.1071 +                   Graph.new_node (name', (Dummy base'))) names' bases')))
 14.1072          |> apsnd (fold (fn name => fold (add_dep name) deps) names)
 14.1073 -        |> apsnd (fold_product (curry (map_node modl_explode o Graph.add_edge)) names names)
 14.1074 +        |> apsnd (fold_product (curry (map_node module_name_path o Graph.add_edge)) names names)
 14.1075        end;
 14.1076 -    fun group_defs ((defs as (_, CodeThingol.Fun _)::_)) =
 14.1077 -          add_group mk_funs defs
 14.1078 -      | group_defs ((defs as (_, CodeThingol.Datatypecons _)::_)) =
 14.1079 -          add_group mk_datatype defs
 14.1080 -      | group_defs ((defs as (_, CodeThingol.Datatype _)::_)) =
 14.1081 -          add_group mk_datatype defs
 14.1082 -      | group_defs ((defs as (_, CodeThingol.Class _)::_)) =
 14.1083 -          add_group mk_class defs
 14.1084 -      | group_defs ((defs as (_, CodeThingol.Classrel _)::_)) =
 14.1085 -          add_group mk_class defs
 14.1086 -      | group_defs ((defs as (_, CodeThingol.Classparam _)::_)) =
 14.1087 -          add_group mk_class defs
 14.1088 -      | group_defs ((defs as [(_, CodeThingol.Classinst _)])) =
 14.1089 -          add_group mk_inst defs
 14.1090 -      | group_defs defs = error ("Illegal mutual dependencies: " ^
 14.1091 -          (commas o map (labelled_name o fst)) defs)
 14.1092 -    val (_, nodes) =
 14.1093 -      init_module
 14.1094 -      |> fold group_defs (map (AList.make (Graph.get_node code))
 14.1095 -          (rev (Graph.strong_conn code)))
 14.1096 +    val (_, nodes) = empty_module
 14.1097 +      |> fold add_stmts' (map (AList.make (Graph.get_node program))
 14.1098 +          (rev (Graph.strong_conn program)));
 14.1099      fun deresolver prefix name = 
 14.1100        let
 14.1101 -        val modl = (fst o dest_name) name;
 14.1102 -        val modl' = (NameSpace.explode o name_modl) modl;
 14.1103 -        val (_, (_, remainder)) = chop_prefix (op =) (prefix, modl');
 14.1104 -        val defname' =
 14.1105 +        val module_name = (fst o dest_name) name;
 14.1106 +        val module_name' = (NameSpace.explode o mk_name_module) module_name;
 14.1107 +        val (_, (_, remainder)) = chop_prefix (op =) (prefix, module_name');
 14.1108 +        val stmt_name =
 14.1109            nodes
 14.1110 -          |> fold (fn m => fn g => case Graph.get_node g m
 14.1111 -              of Module (_, (_, g)) => g) modl'
 14.1112 -          |> (fn g => case Graph.get_node g name of Def (defname, _) => defname);
 14.1113 +          |> fold (fn name => fn node => case Graph.get_node node name
 14.1114 +              of Module (_, (_, node)) => node) module_name'
 14.1115 +          |> (fn node => case Graph.get_node node name of Stmt (stmt_name, _) => stmt_name
 14.1116 +               | Dummy stmt_name => stmt_name);
 14.1117        in
 14.1118 -        NameSpace.implode (remainder @ [defname'])
 14.1119 +        NameSpace.implode (remainder @ [stmt_name])
 14.1120        end handle Graph.UNDEF _ =>
 14.1121          error ("Unknown statement name: " ^ labelled_name name);
 14.1122 -    fun pr_node prefix (Def (_, NONE)) =
 14.1123 +  in (deresolver, nodes) end;
 14.1124 +
 14.1125 +fun serialize_ml compile pr_module pr_stmt projection module_name labelled_name reserved_names includes raw_module_alias
 14.1126 +  _ syntax_tyco syntax_const program cs destination =
 14.1127 +  let
 14.1128 +    val is_cons = CodeThingol.is_cons program;
 14.1129 +    val (deresolver, nodes) = ml_node_of_program labelled_name module_name
 14.1130 +      reserved_names raw_module_alias program;
 14.1131 +    val reserved_names = CodeName.make_vars reserved_names;
 14.1132 +    fun pr_node prefix (Dummy _) =
 14.1133            NONE
 14.1134 -      | pr_node prefix (Def (_, SOME def)) =
 14.1135 -          SOME (pr_def tyco_syntax const_syntax labelled_name init_syms
 14.1136 +      | pr_node prefix (Stmt (_, def)) =
 14.1137 +          SOME (pr_stmt syntax_tyco syntax_const labelled_name reserved_names
 14.1138              (deresolver prefix) is_cons def)
 14.1139 -      | pr_node prefix (Module (dmodlname, (_, nodes))) =
 14.1140 -          SOME (pr_modl dmodlname (
 14.1141 +      | pr_node prefix (Module (module_name, (_, nodes))) =
 14.1142 +          SOME (pr_module module_name (
 14.1143              separate (str "")
 14.1144 -                ((map_filter (pr_node (prefix @ [dmodlname]) o Graph.get_node nodes)
 14.1145 +                ((map_filter (pr_node (prefix @ [module_name]) o Graph.get_node nodes)
 14.1146                  o rev o flat o Graph.strong_conn) nodes)));
 14.1147 +    val cs' = map_filter (try (deresolver (if is_some module_name then the_list module_name else [])))
 14.1148 +      cs;
 14.1149      val p = Pretty.chunks (separate (str "") (map snd includes @ (map_filter
 14.1150        (pr_node [] o Graph.get_node nodes) o rev o flat o Graph.strong_conn) nodes));
 14.1151 -    val deresolv = try (deresolver (if is_some module then the_list module else []));
 14.1152 -    val output = case seri_dest
 14.1153 -     of Compile => K NONE o internal o target_code_of_pretty
 14.1154 -      | Write => K NONE o target_code_writeln
 14.1155 -      | File file => K NONE o File.write file o target_code_of_pretty
 14.1156 -      | String => SOME o target_code_of_pretty;
 14.1157 -  in output_cont (map_filter deresolv cs, output p) end;
 14.1158 +    fun output Compile = K NONE o compile o code_of_pretty
 14.1159 +      | output Write = K NONE o code_writeln
 14.1160 +      | output (File file) = K NONE o File.write file o code_of_pretty
 14.1161 +      | output String = SOME o code_of_pretty;
 14.1162 +  in projection (output destination p) cs' end;
 14.1163 +
 14.1164 +end; (*local*)
 14.1165  
 14.1166 -fun isar_seri_sml module =
 14.1167 +fun isar_seri_sml module_name =
 14.1168    parse_args (Scan.succeed ())
 14.1169 -  #> (fn () => seri_ml (use_text (1, "generated code") Output.ml_output false) snd pr_sml pr_sml_modl module);
 14.1170 +  #> (fn () => serialize_ml (use_text (1, "generated code") Output.ml_output false)
 14.1171 +      pr_sml_module pr_sml_stmt K module_name);
 14.1172  
 14.1173 -fun isar_seri_ocaml module =
 14.1174 +fun isar_seri_ocaml module_name =
 14.1175    parse_args (Scan.succeed ())
 14.1176 -  #> (fn () => seri_ml (fn _ => error "OCaml: no internal compilation") snd pr_ocaml pr_ocaml_modl module)
 14.1177 +  #> (fn () => serialize_ml (fn _ => error "OCaml: no internal compilation")
 14.1178 +      pr_ocaml_module pr_ocaml_stmt K module_name);
 14.1179  
 14.1180  
 14.1181  (** Haskell serializer **)
 14.1182  
 14.1183 -local
 14.1184 -
 14.1185 -fun pr_bind' ((NONE, NONE), _) = str "_"
 14.1186 -  | pr_bind' ((SOME v, NONE), _) = str v
 14.1187 -  | pr_bind' ((NONE, SOME p), _) = p
 14.1188 -  | pr_bind' ((SOME v, SOME p), _) = brackets [str v, str "@", p]
 14.1189 -
 14.1190 -val pr_bind_haskell = gen_pr_bind pr_bind';
 14.1191 +val pr_haskell_bind =
 14.1192 +  let
 14.1193 +    fun pr_bind ((NONE, NONE), _) = str "_"
 14.1194 +      | pr_bind ((SOME v, NONE), _) = str v
 14.1195 +      | pr_bind ((NONE, SOME p), _) = p
 14.1196 +      | pr_bind ((SOME v, SOME p), _) = brackets [str v, str "@", p];
 14.1197 +  in gen_pr_bind pr_bind end;
 14.1198  
 14.1199 -in
 14.1200 -
 14.1201 -fun pr_haskell class_syntax tyco_syntax const_syntax labelled_name
 14.1202 -    init_syms deresolv_here deresolv is_cons contr_classparam_typs deriving_show def =
 14.1203 +fun pr_haskell_stmt syntax_class syntax_tyco syntax_const labelled_name
 14.1204 +    init_syms deresolve is_cons contr_classparam_typs deriving_show =
 14.1205    let
 14.1206 -    fun class_name class = case class_syntax class
 14.1207 -     of NONE => deresolv class
 14.1208 +    val deresolve_base = NameSpace.base o deresolve;
 14.1209 +    fun class_name class = case syntax_class class
 14.1210 +     of NONE => deresolve class
 14.1211        | SOME (class, _) => class;
 14.1212 -    fun classparam_name class classparam = case class_syntax class
 14.1213 -     of NONE => deresolv_here classparam
 14.1214 +    fun classparam_name class classparam = case syntax_class class
 14.1215 +     of NONE => deresolve_base classparam
 14.1216        | SOME (_, classparam_syntax) => case classparam_syntax classparam
 14.1217           of NONE => (snd o dest_name) classparam
 14.1218            | SOME classparam => classparam;
 14.1219 @@ -1249,9 +1275,9 @@
 14.1220      fun pr_tycoexpr tyvars fxy (tyco, tys) =
 14.1221        brackify fxy (str tyco :: map (pr_typ tyvars BR) tys)
 14.1222      and pr_typ tyvars fxy (tycoexpr as tyco `%% tys) =
 14.1223 -          (case tyco_syntax tyco
 14.1224 +          (case syntax_tyco tyco
 14.1225             of NONE =>
 14.1226 -                pr_tycoexpr tyvars fxy (deresolv tyco, tys)
 14.1227 +                pr_tycoexpr tyvars fxy (deresolve tyco, tys)
 14.1228              | SOME (i, pr) =>
 14.1229                  if not (i = length tys)
 14.1230                  then error ("Number of argument mismatch in customary serialization: "
 14.1231 @@ -1284,12 +1310,12 @@
 14.1232            in brackets (str "\\" :: ps @ str "->" @@ pr_term tyvars lhs vars' NOBR t') end
 14.1233        | pr_term tyvars lhs vars fxy (ICase (cases as (_, t0))) =
 14.1234            (case CodeThingol.unfold_const_app t0
 14.1235 -           of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
 14.1236 +           of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
 14.1237                  then pr_case tyvars vars fxy cases
 14.1238                  else pr_app tyvars lhs vars fxy c_ts
 14.1239              | NONE => pr_case tyvars vars fxy cases)
 14.1240      and pr_app' tyvars lhs vars ((c, (_, tys)), ts) = case contr_classparam_typs c
 14.1241 -     of [] => (str o deresolv) c :: map (pr_term tyvars lhs vars BR) ts
 14.1242 +     of [] => (str o deresolve) c :: map (pr_term tyvars lhs vars BR) ts
 14.1243        | fingerprint => let
 14.1244            val ts_fingerprint = ts ~~ curry Library.take (length ts) fingerprint;
 14.1245            val needs_annotation = forall (fn (_, NONE) => true | (t, SOME _) =>
 14.1246 @@ -1299,12 +1325,12 @@
 14.1247                  brackets [pr_term tyvars lhs vars NOBR t, str "::", pr_typ tyvars NOBR ty];
 14.1248          in
 14.1249            if needs_annotation then
 14.1250 -            (str o deresolv) c :: map2 pr_term_anno ts_fingerprint (curry Library.take (length ts) tys)
 14.1251 -          else (str o deresolv) c :: map (pr_term tyvars lhs vars BR) ts
 14.1252 +            (str o deresolve) c :: map2 pr_term_anno ts_fingerprint (curry Library.take (length ts) tys)
 14.1253 +          else (str o deresolve) c :: map (pr_term tyvars lhs vars BR) ts
 14.1254          end
 14.1255 -    and pr_app tyvars lhs vars  = gen_pr_app (pr_app' tyvars) (pr_term tyvars) const_syntax
 14.1256 +    and pr_app tyvars lhs vars  = gen_pr_app (pr_app' tyvars) (pr_term tyvars) syntax_const
 14.1257        labelled_name is_cons lhs vars
 14.1258 -    and pr_bind tyvars = pr_bind_haskell (pr_term tyvars)
 14.1259 +    and pr_bind tyvars = pr_haskell_bind (pr_term tyvars)
 14.1260      and pr_case tyvars vars fxy (cases as ((_, [_]), _)) =
 14.1261            let
 14.1262              val (binds, t) = CodeThingol.unfold_let (ICase cases);
 14.1263 @@ -1332,20 +1358,20 @@
 14.1264              ) (map pr bs)
 14.1265            end
 14.1266        | pr_case tyvars vars fxy ((_, []), _) = str "error \"empty case\"";
 14.1267 -    fun pr_def (name, CodeThingol.Fun ((vs, ty), [])) =
 14.1268 +    fun pr_stmt (name, CodeThingol.Fun ((vs, ty), [])) =
 14.1269            let
 14.1270              val tyvars = CodeName.intro_vars (map fst vs) init_syms;
 14.1271              val n = (length o fst o CodeThingol.unfold_fun) ty;
 14.1272            in
 14.1273              Pretty.chunks [
 14.1274                Pretty.block [
 14.1275 -                (str o suffix " ::" o deresolv_here) name,
 14.1276 +                (str o suffix " ::" o deresolve_base) name,
 14.1277                  Pretty.brk 1,
 14.1278                  pr_typscheme tyvars (vs, ty),
 14.1279                  str ";"
 14.1280                ],
 14.1281                concat (
 14.1282 -                (str o deresolv_here) name
 14.1283 +                (str o deresolve_base) name
 14.1284                  :: map str (replicate n "_")
 14.1285                  @ str "="
 14.1286                  :: str "error"
 14.1287 @@ -1354,14 +1380,14 @@
 14.1288                )
 14.1289              ]
 14.1290            end
 14.1291 -      | pr_def (name, CodeThingol.Fun ((vs, ty), eqs)) =
 14.1292 +      | pr_stmt (name, CodeThingol.Fun ((vs, ty), eqs)) =
 14.1293            let
 14.1294              val tyvars = CodeName.intro_vars (map fst vs) init_syms;
 14.1295              fun pr_eq ((ts, t), _) =
 14.1296                let
 14.1297                  val consts = map_filter
 14.1298 -                  (fn c => if (is_some o const_syntax) c
 14.1299 -                    then NONE else (SOME o NameSpace.base o deresolv) c)
 14.1300 +                  (fn c => if (is_some o syntax_const) c
 14.1301 +                    then NONE else (SOME o NameSpace.base o deresolve) c)
 14.1302                      ((fold o CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []);
 14.1303                  val vars = init_syms
 14.1304                    |> CodeName.intro_vars consts
 14.1305 @@ -1369,7 +1395,7 @@
 14.1306                         (insert (op =)) ts []);
 14.1307                in
 14.1308                  semicolon (
 14.1309 -                  (str o deresolv_here) name
 14.1310 +                  (str o deresolve_base) name
 14.1311                    :: map (pr_term tyvars true vars BR) ts
 14.1312                    @ str "="
 14.1313                    @@ pr_term tyvars false vars NOBR t
 14.1314 @@ -1378,7 +1404,7 @@
 14.1315            in
 14.1316              Pretty.chunks (
 14.1317                Pretty.block [
 14.1318 -                (str o suffix " ::" o deresolv_here) name,
 14.1319 +                (str o suffix " ::" o deresolve_base) name,
 14.1320                  Pretty.brk 1,
 14.1321                  pr_typscheme tyvars (vs, ty),
 14.1322                  str ";"
 14.1323 @@ -1386,47 +1412,47 @@
 14.1324                :: map pr_eq eqs
 14.1325              )
 14.1326            end
 14.1327 -      | pr_def (name, CodeThingol.Datatype (vs, [])) =
 14.1328 +      | pr_stmt (name, CodeThingol.Datatype (vs, [])) =
 14.1329            let
 14.1330              val tyvars = CodeName.intro_vars (map fst vs) init_syms;
 14.1331            in
 14.1332              semicolon [
 14.1333                str "data",
 14.1334 -              pr_typdecl tyvars (vs, (deresolv_here name, map (ITyVar o fst) vs))
 14.1335 +              pr_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs))
 14.1336              ]
 14.1337            end
 14.1338 -      | pr_def (name, CodeThingol.Datatype (vs, [(co, [ty])])) =
 14.1339 +      | pr_stmt (name, CodeThingol.Datatype (vs, [(co, [ty])])) =
 14.1340            let
 14.1341              val tyvars = CodeName.intro_vars (map fst vs) init_syms;
 14.1342            in
 14.1343              semicolon (
 14.1344                str "newtype"
 14.1345 -              :: pr_typdecl tyvars (vs, (deresolv_here name, map (ITyVar o fst) vs))
 14.1346 +              :: pr_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs))
 14.1347                :: str "="
 14.1348 -              :: (str o deresolv_here) co
 14.1349 +              :: (str o deresolve_base) co
 14.1350                :: pr_typ tyvars BR ty
 14.1351                :: (if deriving_show name then [str "deriving (Read, Show)"] else [])
 14.1352              )
 14.1353            end
 14.1354 -      | pr_def (name, CodeThingol.Datatype (vs, co :: cos)) =
 14.1355 +      | pr_stmt (name, CodeThingol.Datatype (vs, co :: cos)) =
 14.1356            let
 14.1357              val tyvars = CodeName.intro_vars (map fst vs) init_syms;
 14.1358              fun pr_co (co, tys) =
 14.1359                concat (
 14.1360 -                (str o deresolv_here) co
 14.1361 +                (str o deresolve_base) co
 14.1362                  :: map (pr_typ tyvars BR) tys
 14.1363                )
 14.1364            in
 14.1365              semicolon (
 14.1366                str "data"
 14.1367 -              :: pr_typdecl tyvars (vs, (deresolv_here name, map (ITyVar o fst) vs))
 14.1368 +              :: pr_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs))
 14.1369                :: str "="
 14.1370                :: pr_co co
 14.1371                :: map ((fn p => Pretty.block [str "| ", p]) o pr_co) cos
 14.1372                @ (if deriving_show name then [str "deriving (Read, Show)"] else [])
 14.1373              )
 14.1374            end
 14.1375 -      | pr_def (name, CodeThingol.Class (v, (superclasses, classparams))) =
 14.1376 +      | pr_stmt (name, CodeThingol.Class (v, (superclasses, classparams))) =
 14.1377            let
 14.1378              val tyvars = CodeName.intro_vars [v] init_syms;
 14.1379              fun pr_classparam (classparam, ty) =
 14.1380 @@ -1440,13 +1466,13 @@
 14.1381                Pretty.block [
 14.1382                  str "class ",
 14.1383                  Pretty.block (pr_typcontext tyvars [(v, map fst superclasses)]),
 14.1384 -                str (deresolv_here name ^ " " ^ CodeName.lookup_var tyvars v),
 14.1385 +                str (deresolve_base name ^ " " ^ CodeName.lookup_var tyvars v),
 14.1386                  str " where {"
 14.1387                ],
 14.1388                str "};"
 14.1389              ) (map pr_classparam classparams)
 14.1390            end
 14.1391 -      | pr_def (_, CodeThingol.Classinst ((class, (tyco, vs)), (_, classparam_insts))) =
 14.1392 +      | pr_stmt (_, CodeThingol.Classinst ((class, (tyco, vs)), (_, classparam_insts))) =
 14.1393            let
 14.1394              val tyvars = CodeName.intro_vars (map fst vs) init_syms;
 14.1395              fun pr_instdef ((classparam, c_inst), _) =
 14.1396 @@ -1467,13 +1493,13 @@
 14.1397                str "};"
 14.1398              ) (map pr_instdef classparam_insts)
 14.1399            end;
 14.1400 -  in pr_def def end;
 14.1401 +  in pr_stmt end;
 14.1402  
 14.1403  fun pretty_haskell_monad c_bind =
 14.1404    let
 14.1405      fun pretty pr vars fxy [(t, _)] =
 14.1406        let
 14.1407 -        val pr_bind = pr_bind_haskell (K pr);
 14.1408 +        val pr_bind = pr_haskell_bind (K pr);
 14.1409          fun pr_monad (NONE, t) vars =
 14.1410                (semicolon [pr vars NOBR t], vars)
 14.1411            | pr_monad (SOME (bind, true), t) vars = vars
 14.1412 @@ -1488,74 +1514,70 @@
 14.1413        in (brack o Pretty.block_enclose (str "do {", str "}")) (ps @| pr vars' NOBR t) end;
 14.1414    in (1, pretty) end;
 14.1415  
 14.1416 -end; (*local*)
 14.1417 -
 14.1418 -fun seri_haskell module_prefix module string_classes labelled_name
 14.1419 -    reserved_syms includes raw_module_alias
 14.1420 -    class_syntax tyco_syntax const_syntax code cs seri_dest =
 14.1421 +fun haskell_program_of_program labelled_name module_name module_prefix reserved_names raw_module_alias program =
 14.1422    let
 14.1423 -    val is_cons = CodeThingol.is_cons code;
 14.1424 -    val contr_classparam_typs = CodeThingol.contr_classparam_typs code;
 14.1425 -    val module_alias = if is_some module then K module else raw_module_alias;
 14.1426 -    val init_names = Name.make_context reserved_syms;
 14.1427 -    val name_modl = mk_modl_name_tab init_names module_prefix module_alias code;
 14.1428 -    fun add_def (name, (def, deps)) =
 14.1429 +    val module_alias = if is_some module_name then K module_name else raw_module_alias;
 14.1430 +    val reserved_names = Name.make_context reserved_names;
 14.1431 +    val mk_name_module = mk_name_module reserved_names module_prefix module_alias program;
 14.1432 +    fun add_stmt (name, (stmt, deps)) =
 14.1433        let
 14.1434 -        val (modl, base) = dest_name name;
 14.1435 -        val name_def = yield_singleton Name.variants;
 14.1436 +        val (module_name, base) = dest_name name;
 14.1437 +        val module_name' = mk_name_module module_name;
 14.1438 +        val mk_name_stmt = yield_singleton Name.variants;
 14.1439          fun add_fun upper (nsp_fun, nsp_typ) =
 14.1440            let
 14.1441              val (base', nsp_fun') =
 14.1442 -              name_def (if upper then first_upper base else base) nsp_fun
 14.1443 +              mk_name_stmt (if upper then first_upper base else base) nsp_fun
 14.1444            in (base', (nsp_fun', nsp_typ)) end;
 14.1445          fun add_typ (nsp_fun, nsp_typ) =
 14.1446            let
 14.1447 -            val (base', nsp_typ') = name_def (first_upper base) nsp_typ
 14.1448 +            val (base', nsp_typ') = mk_name_stmt (first_upper base) nsp_typ
 14.1449            in (base', (nsp_fun, nsp_typ')) end;
 14.1450 -        val add_name =
 14.1451 -          case def
 14.1452 -           of CodeThingol.Fun _ => add_fun false
 14.1453 -            | CodeThingol.Datatype _ => add_typ
 14.1454 -            | CodeThingol.Datatypecons _ => add_fun true
 14.1455 -            | CodeThingol.Class _ => add_typ
 14.1456 -            | CodeThingol.Classrel _ => pair base
 14.1457 -            | CodeThingol.Classparam _ => add_fun false
 14.1458 -            | CodeThingol.Classinst _ => pair base;
 14.1459 -        val modlname' = name_modl modl;
 14.1460 -        fun add_def base' =
 14.1461 -          case def
 14.1462 -           of CodeThingol.Datatypecons _ =>
 14.1463 -                cons (name, ((NameSpace.append modlname' base', base'), NONE))
 14.1464 -            | CodeThingol.Classrel _ => I
 14.1465 -            | CodeThingol.Classparam _ =>
 14.1466 -                cons (name, ((NameSpace.append modlname' base', base'), NONE))
 14.1467 -            | _ => cons (name, ((NameSpace.append modlname' base', base'), SOME def));
 14.1468 +        val add_name = case stmt
 14.1469 +         of CodeThingol.Fun _ => add_fun false
 14.1470 +          | CodeThingol.Datatype _ => add_typ
 14.1471 +          | CodeThingol.Datatypecons _ => add_fun true
 14.1472 +          | CodeThingol.Class _ => add_typ
 14.1473 +          | CodeThingol.Classrel _ => pair base
 14.1474 +          | CodeThingol.Classparam _ => add_fun false
 14.1475 +          | CodeThingol.Classinst _ => pair base;
 14.1476 +        fun add_stmt' base' = case stmt
 14.1477 +         of CodeThingol.Datatypecons _ =>
 14.1478 +              cons (name, (NameSpace.append module_name' base', NONE))
 14.1479 +          | CodeThingol.Classrel _ => I
 14.1480 +          | CodeThingol.Classparam _ =>
 14.1481 +              cons (name, (NameSpace.append module_name' base', NONE))
 14.1482 +          | _ => cons (name, (NameSpace.append module_name' base', SOME stmt));
 14.1483        in
 14.1484 -        Symtab.map_default (modlname', ([], ([], (init_names, init_names))))
 14.1485 +        Symtab.map_default (module_name', ([], ([], (reserved_names, reserved_names))))
 14.1486                (apfst (fold (insert (op = : string * string -> bool)) deps))
 14.1487 -        #> `(fn code => add_name ((snd o snd o the o Symtab.lookup code) modlname'))
 14.1488 +        #> `(fn program => add_name ((snd o snd o the o Symtab.lookup program) module_name'))
 14.1489          #-> (fn (base', names) =>
 14.1490 -              (Symtab.map_entry modlname' o apsnd) (fn (defs, _) =>
 14.1491 -              (add_def base' defs, names)))
 14.1492 +              (Symtab.map_entry module_name' o apsnd) (fn (stmts, _) =>
 14.1493 +              (add_stmt' base' stmts, names)))
 14.1494        end;
 14.1495 -    val code' =
 14.1496 -      fold add_def (AList.make (fn name =>
 14.1497 -        (Graph.get_node code name, Graph.imm_succs code name))
 14.1498 -        (Graph.strong_conn code |> flat)) Symtab.empty;
 14.1499 -    val init_syms = CodeName.make_vars reserved_syms;
 14.1500 -    fun deresolv name =
 14.1501 -      (fst o fst o the o AList.lookup (op =) ((fst o snd o the
 14.1502 -        o Symtab.lookup code') ((name_modl o fst o dest_name) name))) name
 14.1503 +    val hs_program = fold add_stmt (AList.make (fn name =>
 14.1504 +      (Graph.get_node program name, Graph.imm_succs program name))
 14.1505 +      (Graph.strong_conn program |> flat)) Symtab.empty;
 14.1506 +    fun deresolver name =
 14.1507 +      (fst o the o AList.lookup (op =) ((fst o snd o the
 14.1508 +        o Symtab.lookup hs_program) ((mk_name_module o fst o dest_name) name))) name
 14.1509          handle Option => error ("Unknown statement name: " ^ labelled_name name);
 14.1510 -    fun deresolv_here name =
 14.1511 -      (snd o fst o the o AList.lookup (op =) ((fst o snd o the
 14.1512 -        o Symtab.lookup code') ((name_modl o fst o dest_name) name))) name
 14.1513 -        handle Option => error ("Unknown statement name: " ^ labelled_name name);
 14.1514 +  in (deresolver, hs_program) end;
 14.1515 +
 14.1516 +fun serialize_haskell module_prefix module_name string_classes labelled_name
 14.1517 +    reserved_names includes raw_module_alias
 14.1518 +    syntax_class syntax_tyco syntax_const program cs destination =
 14.1519 +  let
 14.1520 +    val (deresolver, hs_program) = haskell_program_of_program labelled_name
 14.1521 +      module_name module_prefix reserved_names raw_module_alias program;
 14.1522 +    val is_cons = CodeThingol.is_cons program;
 14.1523 +    val contr_classparam_typs = CodeThingol.contr_classparam_typs program;
 14.1524      fun deriving_show tyco =
 14.1525        let
 14.1526          fun deriv _ "fun" = false
 14.1527            | deriv tycos tyco = member (op =) tycos tyco orelse
 14.1528 -              case try (Graph.get_node code) tyco
 14.1529 +              case try (Graph.get_node program) tyco
 14.1530                  of SOME (CodeThingol.Datatype (_, cs)) => forall (deriv' (tyco :: tycos))
 14.1531                      (maps snd cs)
 14.1532                   | NONE => true
 14.1533 @@ -1563,45 +1585,46 @@
 14.1534                andalso forall (deriv' tycos) tys
 14.1535            | deriv' _ (ITyVar _) = true
 14.1536        in deriv [] tyco end;
 14.1537 -    fun seri_def qualified = pr_haskell class_syntax tyco_syntax
 14.1538 -      const_syntax labelled_name init_syms
 14.1539 -      deresolv_here (if qualified then deresolv else deresolv_here) is_cons
 14.1540 -      contr_classparam_typs
 14.1541 +    val reserved_names = CodeName.make_vars reserved_names;
 14.1542 +    fun pr_stmt qualified = pr_haskell_stmt syntax_class syntax_tyco
 14.1543 +      syntax_const labelled_name reserved_names
 14.1544 +      (if qualified then deresolver else NameSpace.base o deresolver)
 14.1545 +      is_cons contr_classparam_typs
 14.1546        (if string_classes then deriving_show else K false);
 14.1547 -    fun assemble_module (modulename, content) =
 14.1548 -      (modulename, Pretty.chunks [
 14.1549 -        str ("module " ^ modulename ^ " where {"),
 14.1550 +    fun pr_module name content =
 14.1551 +      (name, Pretty.chunks [
 14.1552 +        str ("module " ^ name ^ " where {"),
 14.1553          str "",
 14.1554          content,
 14.1555          str "",
 14.1556          str "}"
 14.1557        ]);
 14.1558 -    fun seri_module (modlname', (imports, (defs, _))) =
 14.1559 +    fun serialize_module (module_name', (deps, (stmts, _))) =
 14.1560        let
 14.1561 -        val imports' =
 14.1562 -          imports
 14.1563 -          |> map (name_modl o fst o dest_name)
 14.1564 +        val stmt_names = map fst stmts;
 14.1565 +        val deps' = subtract (op =) stmt_names deps
 14.1566            |> distinct (op =)
 14.1567 -          |> remove (op =) modlname';
 14.1568 -        val qualified = is_none module andalso
 14.1569 -          imports @ map fst defs
 14.1570 -          |> distinct (op =)
 14.1571 -          |> map_filter (try deresolv)
 14.1572 +          |> map_filter (try deresolver);
 14.1573 +        val qualified = is_none module_name andalso
 14.1574 +          map deresolver stmt_names @ deps'
 14.1575            |> map NameSpace.base
 14.1576            |> has_duplicates (op =);
 14.1577 -        val mk_import = str o (if qualified
 14.1578 +        val imports = deps'
 14.1579 +          |> map NameSpace.qualifier
 14.1580 +          |> distinct (op =);
 14.1581 +        fun pr_import_include (name, _) = str ("import " ^ name ^ ";");
 14.1582 +        val pr_import_module = str o (if qualified
 14.1583            then prefix "import qualified "
 14.1584            else prefix "import ") o suffix ";";
 14.1585 -        fun import_include (name, _) = str ("import " ^ name ^ ";");
 14.1586          val content = Pretty.chunks (
 14.1587 -            map mk_import imports'
 14.1588 -            @ map import_include includes
 14.1589 +            map pr_import_include includes
 14.1590 +            @ map pr_import_module imports
 14.1591              @ str ""
 14.1592              :: separate (str "") (map_filter
 14.1593 -              (fn (name, (_, SOME def)) => SOME (seri_def qualified (name, def))
 14.1594 -                | (_, (_, NONE)) => NONE) defs)
 14.1595 +              (fn (name, (_, SOME stmt)) => SOME (pr_stmt qualified (name, stmt))
 14.1596 +                | (_, (_, NONE)) => NONE) stmts)
 14.1597            )
 14.1598 -      in assemble_module (modlname', content) end;
 14.1599 +      in pr_module module_name' content end;
 14.1600      fun write_module destination (modlname, content) =
 14.1601        let
 14.1602          val filename = case modlname
 14.1603 @@ -1610,46 +1633,21 @@
 14.1604                  o NameSpace.explode) modlname;
 14.1605          val pathname = Path.append destination filename;
 14.1606          val _ = File.mkdir (Path.dir pathname);
 14.1607 -      in File.write pathname (target_code_of_pretty content) end
 14.1608 -    val output = case seri_dest
 14.1609 -     of Compile => error ("Haskell: no internal compilation")
 14.1610 -      | Write => K NONE o map (target_code_writeln o snd)
 14.1611 -      | File destination => K NONE o map (write_module destination)
 14.1612 -      | String => SOME o cat_lines o map (target_code_of_pretty o snd);
 14.1613 -  in output (map assemble_module includes
 14.1614 -    @ map seri_module (Symtab.dest code'))
 14.1615 +      in File.write pathname (code_of_pretty content) end
 14.1616 +    fun output Compile = error ("Haskell: no internal compilation")
 14.1617 +      | output Write = K NONE o map (code_writeln o snd)
 14.1618 +      | output (File destination) = K NONE o map (write_module destination)
 14.1619 +      | output String = SOME o cat_lines o map (code_of_pretty o snd);
 14.1620 +  in
 14.1621 +    output destination (map (uncurry pr_module) includes
 14.1622 +      @ map serialize_module (Symtab.dest hs_program))
 14.1623    end;
 14.1624  
 14.1625  fun isar_seri_haskell module =
 14.1626    parse_args (Scan.option (Args.$$$ "root" -- Args.colon |-- Args.name)
 14.1627      -- Scan.optional (Args.$$$ "string_classes" >> K true) false
 14.1628      >> (fn (module_prefix, string_classes) =>
 14.1629 -      seri_haskell module_prefix module string_classes));
 14.1630 -
 14.1631 -
 14.1632 -(** diagnosis serializer **)
 14.1633 -
 14.1634 -fun seri_diagnosis labelled_name _ _ _ _ _ _ code _ _ =
 14.1635 -  let
 14.1636 -    val init_names = CodeName.make_vars [];
 14.1637 -    fun pr_fun "fun" = SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
 14.1638 -          brackify_infix (1, R) fxy [
 14.1639 -            pr_typ (INFX (1, X)) ty1,
 14.1640 -            str "->",
 14.1641 -            pr_typ (INFX (1, R)) ty2
 14.1642 -          ])
 14.1643 -      | pr_fun _ = NONE
 14.1644 -    val pr = pr_haskell (K NONE) pr_fun (K NONE) labelled_name init_names
 14.1645 -      I I (K false) (K []) (K false);
 14.1646 -  in
 14.1647 -    []
 14.1648 -    |> Graph.fold (fn (name, (def, _)) =>
 14.1649 -          case try pr (name, def) of SOME p => cons p | NONE => I) code
 14.1650 -    |> Pretty.chunks2
 14.1651 -    |> target_code_of_pretty
 14.1652 -    |> writeln
 14.1653 -    |> K NONE
 14.1654 -  end;
 14.1655 +      serialize_haskell module_prefix module string_classes));
 14.1656  
 14.1657  
 14.1658  (** optional pretty serialization **)
 14.1659 @@ -1811,25 +1809,48 @@
 14.1660  end; (*local*)
 14.1661  
 14.1662  
 14.1663 -(** user interfaces **)
 14.1664 +(** serializer interfaces **)
 14.1665  
 14.1666  (* evaluation *)
 14.1667  
 14.1668 -fun eval_seri module args =
 14.1669 -  seri_ml (use_text (1, "generated code") Output.ml_output false)
 14.1670 -    (fn (cs, SOME s) => "let\n" ^ s ^ "\nin fn () => " ^ enclose "(" ")" (commas cs) ^ " end")
 14.1671 -    pr_sml (K Pretty.chunks) (SOME "Isabelle_Eval");
 14.1672 +fun eval_serializer module [] = serialize_ml
 14.1673 +  (use_text (1, "code to be evaluated") Output.ml_output false) 
 14.1674 +  (K Pretty.chunks) pr_sml_stmt
 14.1675 +  (fn SOME s => fn cs => SOME ("let\n" ^ s ^ "\nin fn () => " ^ enclose "(" ")" (commas cs) ^ " end"))
 14.1676 +  (SOME "Isabelle_Eval");
 14.1677  
 14.1678 -fun sml_of thy code cs = get_serializer (K eval_seri) thy target_SML false NONE [] code (SOME cs) String;
 14.1679 +fun sml_code_of thy program cs = mount_serializer thy (SOME eval_serializer) target_SML NONE [] program cs String
 14.1680 +  |> the;
 14.1681  
 14.1682 -fun eval thy (ref_name, reff) code (t, ty) args =
 14.1683 +fun eval eval'' term_of reff thy ct args =
 14.1684    let
 14.1685 -    val _ = if CodeThingol.contains_dictvar t then
 14.1686 -      error "Term to be evaluated constains free dictionaries" else ();
 14.1687 -    val code' = CodeThingol.add_value_stmt (t, ty) code;
 14.1688 -    val value_code = sml_of thy code' [CodeName.value_name] ;
 14.1689 -    val sml_code = space_implode " " (value_code :: "()" :: map (enclose "(" ")") args);
 14.1690 -  in ML_Context.evaluate Output.ml_output false (ref_name, reff) sml_code end;
 14.1691 +    val _ = if null (term_frees (term_of ct)) then () else error ("Term "
 14.1692 +      ^ quote (Syntax.string_of_term_global thy (term_of ct))
 14.1693 +      ^ " to be evaluated contains free variables");
 14.1694 +    fun eval' program ((vs, ty), t) deps =
 14.1695 +      let
 14.1696 +        val _ = if CodeThingol.contains_dictvar t then
 14.1697 +          error "Term to be evaluated constains free dictionaries" else ();
 14.1698 +        val program' = program
 14.1699 +          |> Graph.new_node (CodeName.value_name, CodeThingol.Fun (([], ty), [(([], t), Drule.dummy_thm)]))
 14.1700 +          |> fold (curry Graph.add_edge CodeName.value_name) deps;
 14.1701 +        val value_code = sml_code_of thy program' [CodeName.value_name] ;
 14.1702 +        val sml_code = space_implode " " (value_code :: "()" :: map (enclose "(" ")") args);
 14.1703 +      in ML_Context.evaluate Output.ml_output false reff sml_code end;
 14.1704 +  in eval'' thy (fn t => (t, eval')) ct end;
 14.1705 +
 14.1706 +fun eval_conv reff = eval CodeThingol.eval_conv Thm.term_of reff;
 14.1707 +fun eval_term reff = eval CodeThingol.eval_term I reff;
 14.1708 +
 14.1709 +
 14.1710 +(* presentation *)
 14.1711 +
 14.1712 +fun code_of thy target module_name cs =
 14.1713 +  let
 14.1714 +    val (cs', program) = CodeThingol.consts_program thy cs;
 14.1715 +  in
 14.1716 +    string (serialize thy target (SOME module_name) [] program cs')
 14.1717 +  end;
 14.1718  
 14.1719  
 14.1720  (* infix syntax *)
 14.1721 @@ -1877,11 +1898,7 @@
 14.1722      val _ = AxClass.get_info thy class;
 14.1723    in class end;
 14.1724  
 14.1725 -fun read_class thy raw_class =
 14.1726 -  let
 14.1727 -    val class = Sign.intern_class thy raw_class;
 14.1728 -    val _ = AxClass.get_info thy class;
 14.1729 -  in class end;
 14.1730 +fun read_class thy = cert_class thy o Sign.intern_class thy;
 14.1731  
 14.1732  fun cert_tyco thy tyco =
 14.1733    let
 14.1734 @@ -1889,12 +1906,7 @@
 14.1735        else error ("No such type constructor: " ^ quote tyco);
 14.1736    in tyco end;
 14.1737  
 14.1738 -fun read_tyco thy raw_tyco =
 14.1739 -  let
 14.1740 -    val tyco = Sign.intern_type thy raw_tyco;
 14.1741 -    val _ = if Sign.declared_tyname thy tyco then ()
 14.1742 -      else error ("No such type constructor: " ^ quote raw_tyco);
 14.1743 -  in tyco end;
 14.1744 +fun read_tyco thy = cert_tyco thy o Sign.intern_type thy;
 14.1745  
 14.1746  fun gen_add_syntax_class prep_class prep_const target raw_class raw_syn thy =
 14.1747    let
 14.1748 @@ -1971,7 +1983,7 @@
 14.1749      fun add sym syms = if member (op =) syms sym
 14.1750        then error ("Reserved symbol " ^ quote sym ^ " already declared")
 14.1751        else insert (op =) sym syms
 14.1752 -  in map_adaptions target o apfst o add end;
 14.1753 +  in map_reserved target o add end;
 14.1754  
 14.1755  fun add_include target =
 14.1756    let
 14.1757 @@ -1983,39 +1995,39 @@
 14.1758            in Symtab.update (name, str content) incls end
 14.1759        | add (name, NONE) incls =
 14.1760            Symtab.delete name incls;
 14.1761 -  in map_adaptions target o apsnd o add end;
 14.1762 +  in map_includes target o add end;
 14.1763  
 14.1764 -fun add_modl_alias target =
 14.1765 +fun add_module_alias target =
 14.1766    map_module_alias target o Symtab.update o apsnd CodeName.check_modulename;
 14.1767  
 14.1768 -fun add_monad target c_run c_bind c_return_unit thy =
 14.1769 +fun add_monad target raw_c_run raw_c_bind raw_c_return_unit thy =
 14.1770    let
 14.1771 -    val c_run' = CodeUnit.read_const thy c_run;
 14.1772 -    val c_bind' = CodeUnit.read_const thy c_bind;
 14.1773 -    val c_bind'' = CodeName.const thy c_bind';
 14.1774 -    val c_return_unit'' = (Option.map o pairself)
 14.1775 -      (CodeName.const thy o CodeUnit.read_const thy) c_return_unit;
 14.1776 +    val c_run = CodeUnit.read_const thy raw_c_run;
 14.1777 +    val c_bind = CodeUnit.read_const thy raw_c_bind;
 14.1778 +    val c_bind' = CodeName.const thy c_bind;
 14.1779 +    val c_return_unit' = (Option.map o pairself)
 14.1780 +      (CodeName.const thy o CodeUnit.read_const thy) raw_c_return_unit;
 14.1781      val is_haskell = target = target_Haskell;
 14.1782 -    val _ = if is_haskell andalso is_some c_return_unit''
 14.1783 +    val _ = if is_haskell andalso is_some c_return_unit'
 14.1784        then error ("No unit entry may be given for Haskell monad")
 14.1785        else ();
 14.1786 -    val _ = if not is_haskell andalso is_none c_return_unit''
 14.1787 +    val _ = if not is_haskell andalso is_none c_return_unit'
 14.1788        then error ("Unit entry must be given for SML/OCaml monad")
 14.1789        else ();
 14.1790    in if target = target_Haskell then
 14.1791      thy
 14.1792 -    |> gen_add_syntax_const (K I) target_Haskell c_run'
 14.1793 -          (SOME (pretty_haskell_monad c_bind''))
 14.1794 -    |> gen_add_syntax_const (K I) target_Haskell c_bind'
 14.1795 +    |> gen_add_syntax_const (K I) target_Haskell c_run
 14.1796 +          (SOME (pretty_haskell_monad c_bind'))
 14.1797 +    |> gen_add_syntax_const (K I) target_Haskell c_bind
 14.1798            (no_bindings (SOME (parse_infix fst (L, 1) ">>=")))
 14.1799    else
 14.1800      thy
 14.1801 -    |> gen_add_syntax_const (K I) target c_bind'
 14.1802 -          (SOME (pretty_imperative_monad_bind c_bind''
 14.1803 -            ((fst o the) c_return_unit'') ((snd o the) c_return_unit'')))
 14.1804 +    |> gen_add_syntax_const (K I) target c_bind
 14.1805 +          (SOME (pretty_imperative_monad_bind c_bind'
 14.1806 +            ((fst o the) c_return_unit') ((snd o the) c_return_unit')))
 14.1807    end;
 14.1808  
 14.1809 -fun gen_allow_exception prep_cs raw_c thy =
 14.1810 +fun gen_allow_abort prep_cs raw_c thy =
 14.1811    let
 14.1812      val c = prep_cs thy raw_c;
 14.1813      val c' = CodeName.const thy c;
 14.1814 @@ -2028,7 +2040,7 @@
 14.1815      #-> (fn xys => pair ((x, y) :: xys)));
 14.1816  
 14.1817  
 14.1818 -(* conrete syntax *)
 14.1819 +(* concrete syntax *)
 14.1820  
 14.1821  structure P = OuterParse
 14.1822  and K = OuterKeyword
 14.1823 @@ -2076,13 +2088,13 @@
 14.1824  val add_syntax_inst = gen_add_syntax_inst cert_class cert_tyco;
 14.1825  val add_syntax_tyco = gen_add_syntax_tyco cert_tyco;
 14.1826  val add_syntax_const = gen_add_syntax_const (K I);
 14.1827 -val allow_exception = gen_allow_exception (K I);
 14.1828 +val allow_abort = gen_allow_abort (K I);
 14.1829  
 14.1830  val add_syntax_class_cmd = gen_add_syntax_class read_class CodeUnit.read_const;
 14.1831  val add_syntax_inst_cmd = gen_add_syntax_inst read_class read_tyco;
 14.1832  val add_syntax_tyco_cmd = gen_add_syntax_tyco read_tyco;
 14.1833  val add_syntax_const_cmd = gen_add_syntax_const CodeUnit.read_const;
 14.1834 -val allow_exception_cmd = gen_allow_exception CodeUnit.read_const;
 14.1835 +val allow_abort_cmd = gen_allow_abort CodeUnit.read_const;
 14.1836  
 14.1837  fun add_syntax_tycoP target tyco = parse_syntax I >> add_syntax_tyco_cmd target tyco;
 14.1838  fun add_syntax_constP target c = parse_syntax fst >> (add_syntax_const_cmd target c o no_bindings);
 14.1839 @@ -2152,9 +2164,64 @@
 14.1840    end;
 14.1841  
 14.1842  
 14.1843 -(* Isar commands *)
 14.1844 +(** code generation at a glance **)
 14.1845 +
 14.1846 +fun read_const_exprs thy cs =
 14.1847 +  let
 14.1848 +    val (cs1, cs2) = CodeName.read_const_exprs thy cs;
 14.1849 +    val (cs3, program) = CodeThingol.consts_program thy cs2;
 14.1850 +    val cs4 = CodeThingol.transitivly_non_empty_funs program (abort_allowed thy);
 14.1851 +    val cs5 = map_filter
 14.1852 +      (fn (c, c') => if member (op =) cs4 c' then SOME c else NONE) (cs2 ~~ cs3);
 14.1853 +  in fold (insert (op =)) cs5 cs1 end;
 14.1854 +
 14.1855 +fun cached_program thy = 
 14.1856 +  let
 14.1857 +    val program = CodeThingol.cached_program thy;
 14.1858 +  in (CodeThingol.transitivly_non_empty_funs program (abort_allowed thy), program) end
 14.1859 +
 14.1860 +fun code thy cs seris =
 14.1861 +  let
 14.1862 +    val (cs', program) = if null cs
 14.1863 +      then cached_program thy
 14.1864 +      else CodeThingol.consts_program thy cs;
 14.1865 +    fun mk_seri_dest dest = case dest
 14.1866 +     of NONE => compile
 14.1867 +      | SOME "-" => write
 14.1868 +      | SOME f => file (Path.explode f)
 14.1869 +    val _ = map (fn (((target, module), dest), args) =>
 14.1870 +      (mk_seri_dest dest (serialize thy target module args program cs'))) seris;
 14.1871 +  in () end;
 14.1872  
 14.1873 -val _ = OuterSyntax.keywords [infixK, infixlK, infixrK];
 14.1874 +fun sml_of thy cs = 
 14.1875 +  let
 14.1876 +    val (cs', program) = CodeThingol.consts_program thy cs;
 14.1877 +  in sml_code_of thy program cs' ^ " ()" end;
 14.1878 +
 14.1879 +fun code_antiq (ctxt, args) = 
 14.1880 +  let
 14.1881 +    val thy = Context.theory_of ctxt;
 14.1882 +    val (ts, (ctxt', args')) = Scan.repeat1 Args.term (ctxt, args);
 14.1883 +    val cs = map (CodeUnit.check_const thy) ts;
 14.1884 +    val s = sml_of thy cs;
 14.1885 +  in (("codevals", s), (ctxt', args')) end;
 14.1886 +
 14.1887 +fun export_code_cmd raw_cs seris thy = code thy (read_const_exprs thy raw_cs) seris;
 14.1888 +
 14.1889 +val (inK, module_nameK, fileK) = ("in", "module_name", "file");
 14.1890 +
 14.1891 +fun code_exprP cmd =
 14.1892 +  (Scan.repeat P.term
 14.1893 +  -- Scan.repeat (P.$$$ inK |-- P.name
 14.1894 +     -- Scan.option (P.$$$ module_nameK |-- P.name)
 14.1895 +     -- Scan.option (P.$$$ fileK |-- P.name)
 14.1896 +     -- Scan.optional (P.$$$ "(" |-- P.arguments --| P.$$$ ")") []
 14.1897 +  ) >> (fn (raw_cs, seris) => cmd raw_cs seris));
 14.1898 +
 14.1899 +
 14.1900 +(** Isar setup **)
 14.1901 +
 14.1902 +val _ = OuterSyntax.keywords [infixK, infixlK, infixrK, inK, module_nameK, fileK];
 14.1903  
 14.1904  val _ =
 14.1905    OuterSyntax.command "code_class" "define code syntax for class" K.thy_decl (
 14.1906 @@ -2211,22 +2278,33 @@
 14.1907  val _ =
 14.1908    OuterSyntax.command "code_modulename" "alias module to other name" K.thy_decl (
 14.1909      P.name -- Scan.repeat1 (P.name -- P.name)
 14.1910 -    >> (fn (target, modlnames) => (Toplevel.theory o fold (add_modl_alias target)) modlnames)
 14.1911 +    >> (fn (target, modlnames) => (Toplevel.theory o fold (add_module_alias target)) modlnames)
 14.1912 +  );
 14.1913 +
 14.1914 +val _ =
 14.1915 +  OuterSyntax.command "code_abort" "permit constant to be implemented as program abort" K.thy_decl (
 14.1916 +    Scan.repeat1 P.term >> (Toplevel.theory o fold allow_abort_cmd)
 14.1917    );
 14.1918  
 14.1919  val _ =
 14.1920 -  OuterSyntax.command "code_exception" "permit exceptions for constant" K.thy_decl (
 14.1921 -    Scan.repeat1 P.term >> (Toplevel.theory o fold allow_exception_cmd)
 14.1922 -  );
 14.1923 +  OuterSyntax.command "export_code" "generate executable code for constants"
 14.1924 +    K.diag (P.!!! (code_exprP export_code_cmd) >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
 14.1925 +
 14.1926 +fun shell_command thyname cmd = Toplevel.program (fn _ =>
 14.1927 +  (use_thy thyname; case Scan.read OuterLex.stopper (P.!!! (code_exprP export_code_cmd)) ((filter OuterLex.is_proper o OuterSyntax.scan) cmd)
 14.1928 +   of SOME f => (writeln "Now generating code..."; f (theory thyname))
 14.1929 +    | NONE => error ("Bad directive " ^ quote cmd)))
 14.1930 +  handle TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure;
 14.1931 +
 14.1932 +val _ = ML_Context.value_antiq "code" code_antiq;
 14.1933  
 14.1934  
 14.1935  (* serializer setup, including serializer defaults *)
 14.1936  
 14.1937  val setup =
 14.1938 -  add_serializer (target_SML, isar_seri_sml)
 14.1939 -  #> add_serializer (target_OCaml, isar_seri_ocaml)
 14.1940 -  #> add_serializer (target_Haskell, isar_seri_haskell)
 14.1941 -  #> add_serializer (target_diag, fn _ => fn _=> seri_diagnosis)
 14.1942 +  add_target (target_SML, isar_seri_sml)
 14.1943 +  #> add_target (target_OCaml, isar_seri_ocaml)
 14.1944 +  #> add_target (target_Haskell, isar_seri_haskell)
 14.1945    #> add_syntax_tyco "SML" "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
 14.1946        brackify_infix (1, R) fxy [
 14.1947          pr_typ (INFX (1, X)) ty1,
    15.1 --- a/src/Tools/code/code_thingol.ML	Tue Jun 10 15:30:01 2008 +0200
    15.2 +++ b/src/Tools/code/code_thingol.ML	Tue Jun 10 15:30:06 2008 +0200
    15.3 @@ -71,25 +71,20 @@
    15.4      | Classinst of (class * (string * (vname * sort) list))
    15.5            * ((class * (string * (string * dict list list))) list
    15.6          * ((string * const) * thm) list);
    15.7 -  type code = stmt Graph.T;
    15.8 -  val empty_code: code;
    15.9 -  val merge_code: code * code -> code;
   15.10 -  val project_code: bool (*delete empty funs*)
   15.11 -    -> string list (*hidden*) -> string list option (*selected*)
   15.12 -    -> code -> code;
   15.13 -  val empty_funs: code -> string list;
   15.14 -  val is_cons: code -> string -> bool;
   15.15 -  val contr_classparam_typs: code -> string -> itype option list;
   15.16 +  type program = stmt Graph.T;
   15.17 +  val empty_funs: program -> string list;
   15.18 +  val transitivly_non_empty_funs: program -> string list -> string list;
   15.19 +  val is_cons: program -> string -> bool;
   15.20 +  val contr_classparam_typs: program -> string -> itype option list;
   15.21  
   15.22 -  type transact;
   15.23 -  val ensure_const: theory -> (sort -> sort) * Sorts.algebra -> CodeFuncgr.T
   15.24 -    -> string -> transact -> string * transact;
   15.25 -  val ensure_value: theory -> (sort -> sort) * Sorts.algebra -> CodeFuncgr.T
   15.26 -    -> term -> transact -> (code * ((typscheme * iterm) * string list)) * transact;
   15.27 -  val transact: theory -> CodeFuncgr.T
   15.28 -    -> (theory -> (sort -> sort) * Sorts.algebra -> CodeFuncgr.T
   15.29 -      -> transact -> 'a * transact) -> code -> 'a * code;
   15.30 -  val add_value_stmt: iterm * itype -> code -> code;
   15.31 +  val consts_program: theory -> string list -> string list * program;
   15.32 +  val cached_program: theory -> program;
   15.33 +  val eval_conv: theory
   15.34 +    -> (term -> term * (program -> typscheme * iterm -> string list -> thm))
   15.35 +    -> cterm -> thm;
   15.36 +  val eval_term: theory
   15.37 +    -> (term -> term * (program -> typscheme * iterm -> string list -> 'a))
   15.38 +    -> term -> 'a;
   15.39  end;
   15.40  
   15.41  structure CodeThingol: CODE_THINGOL =
   15.42 @@ -256,7 +251,7 @@
   15.43  
   15.44  
   15.45  
   15.46 -(** definitions, transactions **)
   15.47 +(** statements, abstract programs **)
   15.48  
   15.49  type typscheme = (vname * sort) list * itype;
   15.50  datatype stmt =
   15.51 @@ -271,62 +266,25 @@
   15.52          * ((class * (string * (string * dict list list))) list
   15.53        * ((string * const) * thm) list);
   15.54  
   15.55 -type code = stmt Graph.T;
   15.56 -
   15.57 -
   15.58 -(* abstract code *)
   15.59 -
   15.60 -val empty_code = Graph.empty : code; (*read: "depends on"*)
   15.61 -
   15.62 -fun ensure_node name = Graph.default_node (name, NoStmt);
   15.63 +type program = stmt Graph.T;
   15.64  
   15.65 -fun add_def_incr (name, NoStmt) code =
   15.66 -      (case the_default NoStmt (try (Graph.get_node code) name)
   15.67 -       of NoStmt => error "Attempted to add NoStmt to code"
   15.68 -        | _ => code)
   15.69 -  | add_def_incr (name, def) code =
   15.70 -      (case try (Graph.get_node code) name
   15.71 -       of NONE => Graph.new_node (name, def) code
   15.72 -        | SOME NoStmt => Graph.map_node name (K def) code
   15.73 -        | SOME _ => error ("Tried to overwrite statement " ^ quote name));
   15.74 -
   15.75 -fun add_dep (NONE, _) = I
   15.76 -  | add_dep (SOME name1, name2) =
   15.77 -      if name1 = name2 then I else Graph.add_edge (name1, name2);
   15.78 -
   15.79 -val merge_code : code * code -> code = Graph.merge (K true);
   15.80 +fun empty_funs program =
   15.81 +  Graph.fold (fn (name, (Fun (_, []), _)) => cons name
   15.82 +               | _ => I) program [];
   15.83  
   15.84 -fun project_code delete_empty_funs hidden raw_selected code =
   15.85 +fun transitivly_non_empty_funs program names_ignored =
   15.86    let
   15.87 -    fun is_empty_fun name = case Graph.get_node code name
   15.88 -     of Fun (_, []) => true
   15.89 -      | _ => false;
   15.90 -    val names = subtract (op =) hidden (Graph.keys code);
   15.91 -    val deleted = Graph.all_preds code (filter is_empty_fun names);
   15.92 -    val selected = case raw_selected
   15.93 -     of NONE => names |> subtract (op =) deleted 
   15.94 -      | SOME sel => sel
   15.95 -          |> delete_empty_funs ? subtract (op =) deleted
   15.96 -          |> subtract (op =) hidden
   15.97 -          |> Graph.all_succs code
   15.98 -          |> delete_empty_funs ? subtract (op =) deleted
   15.99 -          |> subtract (op =) hidden;
  15.100 -  in
  15.101 -    code
  15.102 -    |> Graph.subgraph (member (op =) selected)
  15.103 -  end;
  15.104 +    val names_empty = empty_funs program;
  15.105 +    val names_delete = Graph.all_preds program (subtract (op =) names_ignored names_empty)
  15.106 +  in subtract (op =) names_delete (Graph.keys program) end;
  15.107  
  15.108 -fun empty_funs code =
  15.109 -  Graph.fold (fn (name, (Fun (_, []), _)) => cons name
  15.110 -               | _ => I) code [];
  15.111 -
  15.112 -fun is_cons code name = case Graph.get_node code name
  15.113 +fun is_cons program name = case Graph.get_node program name
  15.114   of Datatypecons _ => true
  15.115    | _ => false;
  15.116  
  15.117 -fun contr_classparam_typs code name = case Graph.get_node code name
  15.118 +fun contr_classparam_typs program name = case Graph.get_node program name
  15.119   of Classparam class => let
  15.120 -        val Class (_, (_, params)) = Graph.get_node code class;
  15.121 +        val Class (_, (_, params)) = Graph.get_node program class;
  15.122          val SOME ty = AList.lookup (op =) params name;
  15.123          val (tys, res_ty) = unfold_fun ty;
  15.124          fun no_tyvar (_ `%% tys) = forall no_tyvar tys
  15.125 @@ -338,35 +296,28 @@
  15.126    | _ => [];
  15.127  
  15.128  
  15.129 -(* transaction protocol *)
  15.130 +(** translation kernel **)
  15.131  
  15.132 -type transact = Graph.key option * code;
  15.133 +type transaction = Graph.key option * program;
  15.134  
  15.135 -fun ensure_stmt stmtgen name (dep, code) =
  15.136 +fun ensure_stmt stmtgen name (dep, program) =
  15.137    let
  15.138 -    fun add_def false =
  15.139 -          ensure_node name
  15.140 -          #> add_dep (dep, name)
  15.141 +    val add_dep = case dep of NONE => I | SOME dep => Graph.add_edge (dep, name);
  15.142 +    fun add_stmt false =
  15.143 +          Graph.default_node (name, NoStmt)
  15.144 +          #> add_dep
  15.145            #> curry stmtgen (SOME name)
  15.146            ##> snd
  15.147 -          #-> (fn def => add_def_incr (name, def))
  15.148 -      | add_def true =
  15.149 -          add_dep (dep, name);
  15.150 +          #-> (fn stmt => Graph.map_node name (K stmt))
  15.151 +      | add_stmt true =
  15.152 +          add_dep;
  15.153    in
  15.154 -    code
  15.155 -    |> add_def (can (Graph.get_node code) name)
  15.156 +    program
  15.157 +    |> add_stmt (can (Graph.get_node program) name)
  15.158      |> pair dep
  15.159      |> pair name
  15.160    end;
  15.161  
  15.162 -fun transact thy funcgr f code =
  15.163 -  (NONE, code)
  15.164 -  |> f thy (Code.operational_algebra thy) funcgr
  15.165 -  |-> (fn x => fn (_, code) => (x, code));
  15.166 -
  15.167 -
  15.168 -(* translation kernel *)
  15.169 -
  15.170  fun not_wellsorted thy thm ty sort e =
  15.171    let
  15.172      val err_class = Sorts.class_error (Syntax.pp_global thy) e;
  15.173 @@ -624,12 +575,56 @@
  15.174    | NONE => exprgen_app_default thy algbr funcgr thm ((c, ty), ts);
  15.175  
  15.176  
  15.177 -(** evaluation **)
  15.178 +(** generated programs **)
  15.179 +
  15.180 +(* store *)
  15.181 +
  15.182 +structure Program = CodeDataFun
  15.183 +(
  15.184 +  type T = program;
  15.185 +  val empty = Graph.empty;
  15.186 +  fun merge _ = Graph.merge (K true);
  15.187 +  fun purge _ NONE _ = Graph.empty
  15.188 +    | purge NONE _ _ = Graph.empty
  15.189 +    | purge (SOME thy) (SOME cs) program =
  15.190 +        let
  15.191 +          val cs_exisiting =
  15.192 +            map_filter (CodeName.const_rev thy) (Graph.keys program);
  15.193 +          val dels = (Graph.all_preds program
  15.194 +              o map (CodeName.const thy)
  15.195 +              o filter (member (op =) cs_exisiting)
  15.196 +            ) cs;
  15.197 +        in Graph.del_nodes dels program end;
  15.198 +);
  15.199 +
  15.200 +val cached_program = Program.get;
  15.201  
  15.202 -fun add_value_stmt (t, ty) code =
  15.203 -  code
  15.204 -  |> Graph.new_node (CodeName.value_name, Fun (([], ty), [(([], t), Drule.dummy_thm)]))
  15.205 -  |> fold (curry Graph.add_edge CodeName.value_name) (Graph.keys code);
  15.206 +fun transact f program =
  15.207 +  (NONE, program)
  15.208 +  |> f
  15.209 +  |-> (fn x => fn (_, program) => (x, program));
  15.210 +
  15.211 +fun generate thy funcgr f x =
  15.212 +  Program.change_yield thy (transact (f thy (Code.operational_algebra thy) funcgr x));
  15.213 +
  15.214 +
  15.215 +(* program generation *)
  15.216 +
  15.217 +fun consts_program thy cs =
  15.218 +  let
  15.219 +    fun project_consts cs program =
  15.220 +      let
  15.221 +        val cs_all = Graph.all_succs program cs;
  15.222 +      in (cs, Graph.subgraph (member (op =) cs_all) program) end;
  15.223 +    fun generate_consts thy algebra funcgr =
  15.224 +      fold_map (ensure_const thy algebra funcgr);
  15.225 +  in
  15.226 +    generate thy (CodeFuncgr.make thy cs) generate_consts cs
  15.227 +    |-> project_consts
  15.228 +  end;
  15.229 +
  15.230 +
  15.231 +(* value evaluation *)
  15.232  
  15.233  fun ensure_value thy algbr funcgr t = 
  15.234    let
  15.235 @@ -641,20 +636,36 @@
  15.236        ##>> exprgen_typ thy algbr funcgr ty
  15.237        ##>> exprgen_term thy algbr funcgr NONE t
  15.238        #>> (fn ((vs, ty), t) => Fun ((vs, ty), [(([], t), Drule.dummy_thm)]));
  15.239 -    fun term_value (dep, code1) =
  15.240 +    fun term_value (dep, program1) =
  15.241        let
  15.242          val Fun ((vs, ty), [(([], t), _)]) =
  15.243 -          Graph.get_node code1 CodeName.value_name;
  15.244 -        val deps = Graph.imm_succs code1 CodeName.value_name;
  15.245 -        val code2 = Graph.del_nodes [CodeName.value_name] code1;
  15.246 -        val code3 = project_code false [] (SOME deps) code2;
  15.247 -      in ((code3, (((vs, ty), t), deps)), (dep, code2)) end;
  15.248 +          Graph.get_node program1 CodeName.value_name;
  15.249 +        val deps = Graph.imm_succs program1 CodeName.value_name;
  15.250 +        val program2 = Graph.del_nodes [CodeName.value_name] program1;
  15.251 +        val deps_all = Graph.all_succs program2 deps;
  15.252 +        val program3 = Graph.subgraph (member (op =) deps_all) program2;
  15.253 +      in ((program3, (((vs, ty), t), deps)), (dep, program2)) end;
  15.254    in
  15.255      ensure_stmt stmt_value CodeName.value_name
  15.256      #> snd
  15.257      #> term_value
  15.258    end;
  15.259  
  15.260 +fun eval eval_kind thy evaluator =
  15.261 +  let
  15.262 +    fun evaluator'' evaluator''' funcgr t =
  15.263 +      let
  15.264 +        val ((program, (vs_ty_t, deps)), _) = generate thy funcgr ensure_value t;
  15.265 +      in evaluator''' program vs_ty_t deps end;
  15.266 +    fun evaluator' t =
  15.267 +      let
  15.268 +        val (t', evaluator''') = evaluator t;
  15.269 +      in (t', evaluator'' evaluator''') end;
  15.270 +  in eval_kind thy evaluator' end
  15.271 +
  15.272 +fun eval_conv thy = eval CodeFuncgr.eval_conv thy;
  15.273 +fun eval_term thy = eval CodeFuncgr.eval_term thy;
  15.274 +
  15.275  end; (*struct*)
  15.276  
  15.277  
    16.1 --- a/src/Tools/nbe.ML	Tue Jun 10 15:30:01 2008 +0200
    16.2 +++ b/src/Tools/nbe.ML	Tue Jun 10 15:30:06 2008 +0200
    16.3 @@ -277,14 +277,14 @@
    16.4        #-> fold (fn (name, univ) => (Graph.map_node name o apfst) (K (SOME univ))))
    16.5    end;
    16.6  
    16.7 -fun ensure_stmts code =
    16.8 +fun ensure_stmts program =
    16.9    let
   16.10      fun add_stmts names (gr, (maxidx, idx_tab)) = if exists ((can o Graph.get_node) gr) names
   16.11        then (gr, (maxidx, idx_tab))
   16.12        else (gr, (maxidx, idx_tab))
   16.13 -        |> compile_stmts (map (fn name => ((name, Graph.get_node code name),
   16.14 -          Graph.imm_succs code name)) names);
   16.15 -  in fold_rev add_stmts (Graph.strong_conn code) end;
   16.16 +        |> compile_stmts (map (fn name => ((name, Graph.get_node program name),
   16.17 +          Graph.imm_succs program name)) names);
   16.18 +  in fold_rev add_stmts (Graph.strong_conn program) end;
   16.19  
   16.20  
   16.21  (** evaluation **)
   16.22 @@ -364,9 +364,9 @@
   16.23  
   16.24  (* compilation, evaluation and reification *)
   16.25  
   16.26 -fun compile_eval thy code vs_ty_t deps =
   16.27 +fun compile_eval thy program vs_ty_t deps =
   16.28    let
   16.29 -    val (gr, (_, idx_tab)) = Nbe_Functions.change thy (ensure_stmts code);
   16.30 +    val (gr, (_, idx_tab)) = Nbe_Functions.change thy (ensure_stmts program);
   16.31    in
   16.32      vs_ty_t
   16.33      |> eval_term gr deps
   16.34 @@ -375,7 +375,7 @@
   16.35  
   16.36  (* evaluation with type reconstruction *)
   16.37  
   16.38 -fun eval thy t code vs_ty_t deps =
   16.39 +fun eval thy t program vs_ty_t deps =
   16.40    let
   16.41      fun subst_const f = map_aterms (fn t as Term.Const (c, ty) => Term.Const (f c, ty)
   16.42        | t => t);
   16.43 @@ -395,7 +395,7 @@
   16.44          ^ setmp show_types true (Syntax.string_of_term_global thy) t);
   16.45      val string_of_term = setmp show_types true (Syntax.string_of_term_global thy);
   16.46    in
   16.47 -    compile_eval thy code vs_ty_t deps
   16.48 +    compile_eval thy program vs_ty_t deps
   16.49      |> tracing (fn t => "Normalized:\n" ^ string_of_term t)
   16.50      |> subst_triv_consts
   16.51      |> type_frees
   16.52 @@ -408,14 +408,14 @@
   16.53  
   16.54  (* evaluation oracle *)
   16.55  
   16.56 -exception Norm of term * CodeThingol.code
   16.57 +exception Norm of term * CodeThingol.program
   16.58    * (CodeThingol.typscheme * CodeThingol.iterm) * string list;
   16.59  
   16.60 -fun norm_oracle (thy, Norm (t, code, vs_ty_t, deps)) =
   16.61 -  Logic.mk_equals (t, eval thy t code vs_ty_t deps);
   16.62 +fun norm_oracle (thy, Norm (t, program, vs_ty_t, deps)) =
   16.63 +  Logic.mk_equals (t, eval thy t program vs_ty_t deps);
   16.64  
   16.65 -fun norm_invoke thy t code vs_ty_t deps =
   16.66 -  Thm.invoke_oracle_i thy "HOL.norm" (thy, Norm (t, code, vs_ty_t, deps));
   16.67 +fun norm_invoke thy t program vs_ty_t deps =
   16.68 +  Thm.invoke_oracle_i thy "HOL.norm" (thy, Norm (t, program, vs_ty_t, deps));
   16.69    (*FIXME get rid of hardwired theory name*)
   16.70  
   16.71  fun add_triv_classes thy =
   16.72 @@ -430,15 +430,15 @@
   16.73  fun norm_conv ct =
   16.74    let
   16.75      val thy = Thm.theory_of_cterm ct;
   16.76 -    fun evaluator' t code vs_ty_t deps = norm_invoke thy t code vs_ty_t deps;
   16.77 +    fun evaluator' t program vs_ty_t deps = norm_invoke thy t program vs_ty_t deps;
   16.78      fun evaluator t = (add_triv_classes thy t, evaluator' t);
   16.79 -  in CodePackage.evaluate_conv thy evaluator ct end;
   16.80 +  in CodeThingol.eval_conv thy evaluator ct end;
   16.81  
   16.82  fun norm_term thy t =
   16.83    let
   16.84 -    fun evaluator' t code vs_ty_t deps = eval thy t code vs_ty_t deps;
   16.85 +    fun evaluator' t program vs_ty_t deps = eval thy t program vs_ty_t deps;
   16.86      fun evaluator t = (add_triv_classes thy t, evaluator' t);
   16.87 -  in (Code.postprocess_term thy o CodePackage.evaluate_term thy evaluator) t end;
   16.88 +  in (Code.postprocess_term thy o CodeThingol.eval_term thy evaluator) t end;
   16.89  
   16.90  (* evaluation command *)
   16.91