explicit thm context for error messages
authorhaftmann
Fri Jun 20 21:00:28 2008 +0200 (2008-06-20)
changeset 27304720c8115d723
parent 27303 d6fef33c5c69
child 27305 2dbdfa495982
explicit thm context for error messages
src/Tools/code/code_target.ML
     1.1 --- a/src/Tools/code/code_target.ML	Fri Jun 20 21:00:27 2008 +0200
     1.2 +++ b/src/Tools/code/code_target.ML	Fri Jun 20 21:00:28 2008 +0200
     1.3 @@ -37,11 +37,11 @@
     1.4    val serialize: theory -> string -> string option -> Args.T list
     1.5      -> CodeThingol.program -> string list -> serialization;
     1.6    val compile: serialization -> unit;
     1.7 -  val write: serialization -> unit;
     1.8 +  val export: serialization -> unit;
     1.9    val file: Path.T -> serialization -> unit;
    1.10 -  val string: serialization -> string;
    1.11 +  val string: string list -> serialization -> string;
    1.12  
    1.13 -  val code_of: theory -> string -> string -> string list -> string;
    1.14 +  val code_of: theory -> string -> string -> string list -> string list -> string;
    1.15    val eval_conv: string * (unit -> thm) option ref
    1.16      -> theory -> cterm -> string list -> thm;
    1.17    val eval_term: string * (unit -> 'a) option ref
    1.18 @@ -70,7 +70,7 @@
    1.19  fun enum_default default sep opn cls [] = str default
    1.20    | enum_default default sep opn cls xs = Pretty.enum sep opn cls xs;
    1.21  
    1.22 -datatype destination = Compile | Write | File of Path.T | String;
    1.23 +datatype destination = Compile | Export | File of Path.T | String of string list;
    1.24  type serialization = destination -> string option;
    1.25  
    1.26  val code_width = ref 80; (*FIXME after Pretty module no longer depends on print mode*)
    1.27 @@ -80,9 +80,12 @@
    1.28  
    1.29  (*FIXME why another code_setmp?*)
    1.30  fun compile f = (code_setmp f Compile; ());
    1.31 -fun write f = (code_setmp f Write; ());
    1.32 +fun export f = (code_setmp f Export; ());
    1.33  fun file p f = (code_setmp f (File p); ());
    1.34 -fun string f = the (code_setmp f String);
    1.35 +fun string cs f = the (code_setmp f (String cs));
    1.36 +
    1.37 +fun stmt_names_of_destination (String stmts) = stmts
    1.38 +  | stmt_names_of_destination _ = [];
    1.39  
    1.40  
    1.41  (** generic syntax **)
    1.42 @@ -124,7 +127,7 @@
    1.43  type typ_syntax = int * ((fixity -> itype -> Pretty.T)
    1.44    -> fixity -> itype list -> Pretty.T);
    1.45  type term_syntax = int * ((CodeName.var_ctxt -> fixity -> iterm -> Pretty.T)
    1.46 -  -> CodeName.var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
    1.47 +  -> thm -> bool -> CodeName.var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
    1.48  
    1.49  
    1.50  (** theory data **)
    1.51 @@ -153,7 +156,7 @@
    1.52         Symtab.join (K snd) (const1, const2))
    1.53    );
    1.54  
    1.55 -type serializer = (*FIXME order of arguments*)
    1.56 +type serializer =
    1.57    string option                         (*module name*)
    1.58    -> Args.T list                        (*arguments*)
    1.59    -> (string -> string)                 (*labelled_name*)
    1.60 @@ -297,6 +300,8 @@
    1.61  
    1.62  (* list, char, string, numeral and monad abstract syntax transformations *)
    1.63  
    1.64 +fun nerror thm s = error (s ^ ",\nin equation " ^ Display.string_of_thm thm);
    1.65 +
    1.66  fun implode_list c_nil c_cons t =
    1.67    let
    1.68      fun dest_cons (IConst (c, _) `$ t1 `$ t2) =
    1.69 @@ -330,20 +335,20 @@
    1.70      else NONE
    1.71    end;
    1.72  
    1.73 -fun implode_numeral negative c_pls c_min c_bit0 c_bit1 =
    1.74 +fun implode_numeral thm negative c_pls c_min c_bit0 c_bit1 =
    1.75    let
    1.76      fun dest_bit (IConst (c, _)) = if c = c_bit0 then 0
    1.77            else if c = c_bit1 then 1
    1.78 -          else error "Illegal numeral expression: illegal bit"
    1.79 -      | dest_bit _ = error "Illegal numeral expression: illegal bit";
    1.80 +          else nerror thm "Illegal numeral expression: illegal bit"
    1.81 +      | dest_bit _ = nerror thm "Illegal numeral expression: illegal bit";
    1.82      fun dest_numeral (IConst (c, _)) = if c = c_pls then SOME 0
    1.83            else if c = c_min then
    1.84              if negative then SOME ~1 else NONE
    1.85 -          else error "Illegal numeral expression: illegal leading digit"
    1.86 +          else nerror thm "Illegal numeral expression: illegal leading digit"
    1.87        | dest_numeral (t1 `$ t2) =
    1.88            let val (n, b) = (dest_numeral t2, dest_bit t1)
    1.89            in case n of SOME n => SOME (2 * n + b) | NONE => NONE end
    1.90 -      | dest_numeral _ = error "Illegal numeral expression: illegal term";
    1.91 +      | dest_numeral _ = nerror thm "Illegal numeral expression: illegal term";
    1.92    in dest_numeral #> the_default 0 end;
    1.93  
    1.94  fun implode_monad c_bind t =
    1.95 @@ -364,25 +369,25 @@
    1.96  
    1.97  (* applications and bindings *)
    1.98  
    1.99 -fun gen_pr_app pr_app pr_term syntax_const labelled_name is_cons
   1.100 -      lhs vars fxy (app as ((c, (_, tys)), ts)) =
   1.101 +fun gen_pr_app pr_app pr_term syntax_const is_cons thm pat
   1.102 +    vars fxy (app as ((c, (_, tys)), ts)) =
   1.103    case syntax_const c
   1.104 -   of NONE => if lhs andalso not (is_cons c) then
   1.105 -          error ("Non-constructor on left hand side of equation: " ^ labelled_name c)
   1.106 -        else brackify fxy (pr_app lhs vars app)
   1.107 +   of NONE => if pat andalso not (is_cons c) then
   1.108 +        nerror thm "Non-constructor in pattern "
   1.109 +        else brackify fxy (pr_app thm pat vars app)
   1.110      | SOME (i, pr) =>
   1.111          let
   1.112            val k = if i < 0 then length tys else i;
   1.113 -          fun pr' fxy ts = pr (pr_term lhs) vars fxy (ts ~~ curry Library.take k tys);
   1.114 +          fun pr' fxy ts = pr (pr_term thm pat) thm pat vars fxy (ts ~~ curry Library.take k tys);
   1.115          in if k = length ts
   1.116            then pr' fxy ts
   1.117          else if k < length ts
   1.118            then case chop k ts of (ts1, ts2) =>
   1.119 -            brackify fxy (pr' APP ts1 :: map (pr_term lhs vars BR) ts2)
   1.120 -          else pr_term lhs vars fxy (CodeThingol.eta_expand app k)
   1.121 +            brackify fxy (pr' APP ts1 :: map (pr_term thm pat vars BR) ts2)
   1.122 +          else pr_term thm pat vars fxy (CodeThingol.eta_expand app k)
   1.123          end;
   1.124  
   1.125 -fun gen_pr_bind pr_bind pr_term (fxy : fixity) ((v, pat), ty : itype) vars =
   1.126 +fun gen_pr_bind pr_bind pr_term thm (fxy : fixity) ((v, pat), ty : itype) vars =
   1.127    let
   1.128      val vs = case pat
   1.129       of SOME pat => CodeThingol.fold_varnames (insert (op =)) pat []
   1.130 @@ -390,7 +395,7 @@
   1.131      val vars' = CodeName.intro_vars (the_list v) vars;
   1.132      val vars'' = CodeName.intro_vars vs vars';
   1.133      val v' = Option.map (CodeName.lookup_var vars') v;
   1.134 -    val pat' = Option.map (pr_term true vars'' fxy) pat;
   1.135 +    val pat' = Option.map (pr_term thm true vars'' fxy) pat;
   1.136    in (pr_bind ((v', pat'), ty), vars'') end;
   1.137  
   1.138  
   1.139 @@ -425,12 +430,17 @@
   1.140  (** SML/OCaml serializer **)
   1.141  
   1.142  datatype ml_stmt =
   1.143 -    MLFuns of (string * (typscheme * (iterm list * iterm) list)) list
   1.144 +    MLFuns of (string * (typscheme * ((iterm list * iterm) * thm) list)) list
   1.145    | MLDatas of (string * ((vname * sort) list * (string * itype list) list)) list
   1.146    | MLClass of string * (vname * ((class * string) list * (string * itype) list))
   1.147    | MLClassinst of string * ((class * (string * (vname * sort) list))
   1.148          * ((class * (string * (string * dict list list))) list
   1.149 -      * (string * const) list));
   1.150 +      * ((string * const) * thm) list));
   1.151 +
   1.152 +fun stmt_names_of (MLFuns fs) = map fst fs
   1.153 +  | stmt_names_of (MLDatas ds) = map fst ds
   1.154 +  | stmt_names_of (MLClass (c, _)) = [c]
   1.155 +  | stmt_names_of (MLClassinst (i, _)) = [i];
   1.156  
   1.157  fun pr_sml_stmt syntax_tyco syntax_const labelled_name reserved_names deresolve is_cons =
   1.158    let
   1.159 @@ -469,94 +479,86 @@
   1.160          | [p] => Pretty.block [p, Pretty.brk 1, tyco']
   1.161          | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco']
   1.162        end
   1.163 -    and pr_typ fxy (tyco `%% tys) =
   1.164 -          (case syntax_tyco tyco
   1.165 -           of NONE => pr_tycoexpr fxy (tyco, tys)
   1.166 -            | SOME (i, pr) =>
   1.167 -                if not (i = length tys)
   1.168 -                then error ("Number of argument mismatch in customary serialization: "
   1.169 -                  ^ (string_of_int o length) tys ^ " given, "
   1.170 -                  ^ string_of_int i ^ " expected")
   1.171 -                else pr pr_typ fxy tys)
   1.172 -      | pr_typ fxy (ITyVar v) =
   1.173 -          str ("'" ^ v);
   1.174 -    fun pr_term lhs vars fxy (IConst c) =
   1.175 -          pr_app lhs vars fxy (c, [])
   1.176 -      | pr_term lhs vars fxy (IVar v) =
   1.177 +    and pr_typ fxy (tyco `%% tys) = (case syntax_tyco tyco
   1.178 +         of NONE => pr_tycoexpr fxy (tyco, tys)
   1.179 +          | SOME (i, pr) => pr pr_typ fxy tys)
   1.180 +      | pr_typ fxy (ITyVar v) = str ("'" ^ v);
   1.181 +    fun pr_term thm pat vars fxy (IConst c) =
   1.182 +          pr_app thm pat vars fxy (c, [])
   1.183 +      | pr_term thm pat vars fxy (IVar v) =
   1.184            str (CodeName.lookup_var vars v)
   1.185 -      | pr_term lhs vars fxy (t as t1 `$ t2) =
   1.186 +      | pr_term thm pat vars fxy (t as t1 `$ t2) =
   1.187            (case CodeThingol.unfold_const_app t
   1.188 -           of SOME c_ts => pr_app lhs vars fxy c_ts
   1.189 +           of SOME c_ts => pr_app thm pat vars fxy c_ts
   1.190              | NONE =>
   1.191 -                brackify fxy [pr_term lhs vars NOBR t1, pr_term lhs vars BR t2])
   1.192 -      | pr_term lhs vars fxy (t as _ `|-> _) =
   1.193 +                brackify fxy [pr_term thm pat vars NOBR t1, pr_term thm pat vars BR t2])
   1.194 +      | pr_term thm pat vars fxy (t as _ `|-> _) =
   1.195            let
   1.196              val (binds, t') = CodeThingol.unfold_abs t;
   1.197              fun pr ((v, pat), ty) =
   1.198 -              pr_bind NOBR ((SOME v, pat), ty)
   1.199 +              pr_bind thm NOBR ((SOME v, pat), ty)
   1.200                #>> (fn p => concat [str "fn", p, str "=>"]);
   1.201              val (ps, vars') = fold_map pr binds vars;
   1.202 -          in brackets (ps @ [pr_term lhs vars' NOBR t']) end
   1.203 -      | pr_term lhs vars fxy (ICase (cases as (_, t0))) =
   1.204 +          in brackets (ps @ [pr_term thm pat vars' NOBR t']) end
   1.205 +      | pr_term thm pat vars fxy (ICase (cases as (_, t0))) =
   1.206            (case CodeThingol.unfold_const_app t0
   1.207             of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
   1.208 -                then pr_case vars fxy cases
   1.209 -                else pr_app lhs vars fxy c_ts
   1.210 -            | NONE => pr_case vars fxy cases)
   1.211 -    and pr_app' lhs vars (app as ((c, (iss, tys)), ts)) =
   1.212 +                then pr_case thm vars fxy cases
   1.213 +                else pr_app thm pat vars fxy c_ts
   1.214 +            | NONE => pr_case thm vars fxy cases)
   1.215 +    and pr_app' thm pat vars (app as ((c, (iss, tys)), ts)) =
   1.216        if is_cons c then let
   1.217          val k = length tys
   1.218        in if k < 2 then 
   1.219 -        (str o deresolve) c :: map (pr_term lhs vars BR) ts
   1.220 +        (str o deresolve) c :: map (pr_term thm pat vars BR) ts
   1.221        else if k = length ts then
   1.222 -        [(str o deresolve) c, Pretty.enum "," "(" ")" (map (pr_term lhs vars NOBR) ts)]
   1.223 -      else [pr_term lhs vars BR (CodeThingol.eta_expand app k)] end else
   1.224 +        [(str o deresolve) c, Pretty.enum "," "(" ")" (map (pr_term thm pat vars NOBR) ts)]
   1.225 +      else [pr_term thm pat vars BR (CodeThingol.eta_expand app k)] end else
   1.226          (str o deresolve) c
   1.227 -          :: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term lhs vars BR) ts
   1.228 -    and pr_app lhs vars = gen_pr_app pr_app' pr_term syntax_const
   1.229 -      labelled_name is_cons lhs vars
   1.230 +          :: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term thm pat vars BR) ts
   1.231 +    and pr_app thm pat vars = gen_pr_app pr_app' pr_term syntax_const is_cons thm pat vars
   1.232      and pr_bind' ((NONE, NONE), _) = str "_"
   1.233        | pr_bind' ((SOME v, NONE), _) = str v
   1.234        | pr_bind' ((NONE, SOME p), _) = p
   1.235        | pr_bind' ((SOME v, SOME p), _) = concat [str v, str "as", p]
   1.236 -    and pr_bind fxy = gen_pr_bind pr_bind' pr_term fxy
   1.237 -    and pr_case vars fxy (cases as ((_, [_]), _)) =
   1.238 +    and pr_bind thm = gen_pr_bind pr_bind' pr_term thm
   1.239 +    and pr_case thm vars fxy (cases as ((_, [_]), _)) =
   1.240            let
   1.241              val (binds, t') = CodeThingol.unfold_let (ICase cases);
   1.242              fun pr ((pat, ty), t) vars =
   1.243                vars
   1.244 -              |> pr_bind NOBR ((NONE, SOME pat), ty)
   1.245 -              |>> (fn p => semicolon [str "val", p, str "=", pr_term false vars NOBR t])
   1.246 +              |> pr_bind thm NOBR ((NONE, SOME pat), ty)
   1.247 +              |>> (fn p => semicolon [str "val", p, str "=", pr_term thm false vars NOBR t])
   1.248              val (ps, vars') = fold_map pr binds vars;
   1.249            in
   1.250              Pretty.chunks [
   1.251                [str ("let"), Pretty.fbrk, Pretty.chunks ps] |> Pretty.block,
   1.252 -              [str ("in"), Pretty.fbrk, pr_term false vars' NOBR t'] |> Pretty.block,
   1.253 +              [str ("in"), Pretty.fbrk, pr_term thm false vars' NOBR t'] |> Pretty.block,
   1.254                str ("end")
   1.255              ]
   1.256            end
   1.257 -      | pr_case vars fxy (((td, ty), b::bs), _) =
   1.258 +      | pr_case thm vars fxy (((td, ty), b::bs), _) =
   1.259            let
   1.260              fun pr delim (pat, t) =
   1.261                let
   1.262 -                val (p, vars') = pr_bind NOBR ((NONE, SOME pat), ty) vars;
   1.263 +                val (p, vars') = pr_bind thm NOBR ((NONE, SOME pat), ty) vars;
   1.264                in
   1.265 -                concat [str delim, p, str "=>", pr_term false vars' NOBR t]
   1.266 +                concat [str delim, p, str "=>", pr_term thm false vars' NOBR t]
   1.267                end;
   1.268            in
   1.269              (Pretty.enclose "(" ")" o single o brackify fxy) (
   1.270                str "case"
   1.271 -              :: pr_term false vars NOBR td
   1.272 +              :: pr_term thm false vars NOBR td
   1.273                :: pr "of" b
   1.274                :: map (pr "|") bs
   1.275              )
   1.276            end
   1.277 -      | pr_case vars fxy ((_, []), _) = str "raise Fail \"empty case\""
   1.278 +      | pr_case thm vars fxy ((_, []), _) = str "raise Fail \"empty case\"";
   1.279      fun pr_stmt (MLFuns (funns as (funn :: funns'))) =
   1.280            let
   1.281              val definer =
   1.282                let
   1.283 -                fun no_args _ ((ts, _) :: _) = length ts
   1.284 +                fun no_args _ (((ts, _), _) :: _) = length ts
   1.285                    | no_args ty [] = (length o fst o CodeThingol.unfold_fun) ty;
   1.286                  fun mk 0 [] = "val"
   1.287                    | mk 0 vs = if (null o filter_out (null o snd)) vs
   1.288 @@ -590,7 +592,7 @@
   1.289                      val vs_dict = filter_out (null o snd) vs;
   1.290                      val shift = if null eqs' then I else
   1.291                        map (Pretty.block o single o Pretty.block o single);
   1.292 -                    fun pr_eq definer (ts, t) =
   1.293 +                    fun pr_eq definer ((ts, t), thm) =
   1.294                        let
   1.295                          val consts = map_filter
   1.296                            (fn c => if (is_some o syntax_const) c
   1.297 @@ -607,8 +609,8 @@
   1.298                               then [str ":", pr_typ NOBR ty]
   1.299                               else
   1.300                                 pr_tyvar_dicts vs_dict
   1.301 -                               @ map (pr_term true vars BR) ts)
   1.302 -                       @ [str "=", pr_term false vars NOBR t]
   1.303 +                               @ map (pr_term thm true vars BR) ts)
   1.304 +                       @ [str "=", pr_term thm false vars NOBR t]
   1.305                          )
   1.306                        end
   1.307                    in
   1.308 @@ -697,11 +699,11 @@
   1.309                  str "=",
   1.310                  pr_dicts NOBR [DictConst dss]
   1.311                ];
   1.312 -            fun pr_classparam (classparam, c_inst) =
   1.313 +            fun pr_classparam ((classparam, c_inst), thm) =
   1.314                concat [
   1.315                  (str o pr_label_classparam) classparam,
   1.316                  str "=",
   1.317 -                pr_app false reserved_names NOBR (c_inst, [])
   1.318 +                pr_app thm false reserved_names NOBR (c_inst, [])
   1.319                ];
   1.320            in
   1.321              semicolon ([
   1.322 @@ -757,80 +759,72 @@
   1.323          | [p] => Pretty.block [p, Pretty.brk 1, tyco']
   1.324          | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco']
   1.325        end
   1.326 -    and pr_typ fxy (tyco `%% tys) =
   1.327 -          (case syntax_tyco tyco
   1.328 -           of NONE => pr_tycoexpr fxy (tyco, tys)
   1.329 -            | SOME (i, pr) =>
   1.330 -                if not (i = length tys)
   1.331 -                then error ("Number of argument mismatch in customary serialization: "
   1.332 -                  ^ (string_of_int o length) tys ^ " given, "
   1.333 -                  ^ string_of_int i ^ " expected")
   1.334 -                else pr pr_typ fxy tys)
   1.335 -      | pr_typ fxy (ITyVar v) =
   1.336 -          str ("'" ^ v);
   1.337 -    fun pr_term lhs vars fxy (IConst c) =
   1.338 -          pr_app lhs vars fxy (c, [])
   1.339 -      | pr_term lhs vars fxy (IVar v) =
   1.340 +    and pr_typ fxy (tyco `%% tys) = (case syntax_tyco tyco
   1.341 +         of NONE => pr_tycoexpr fxy (tyco, tys)
   1.342 +          | SOME (i, pr) => pr pr_typ fxy tys)
   1.343 +      | pr_typ fxy (ITyVar v) = str ("'" ^ v);
   1.344 +    fun pr_term thm pat vars fxy (IConst c) =
   1.345 +          pr_app thm pat vars fxy (c, [])
   1.346 +      | pr_term thm pat vars fxy (IVar v) =
   1.347            str (CodeName.lookup_var vars v)
   1.348 -      | pr_term lhs vars fxy (t as t1 `$ t2) =
   1.349 +      | pr_term thm pat vars fxy (t as t1 `$ t2) =
   1.350            (case CodeThingol.unfold_const_app t
   1.351 -           of SOME c_ts => pr_app lhs vars fxy c_ts
   1.352 +           of SOME c_ts => pr_app thm pat vars fxy c_ts
   1.353              | NONE =>
   1.354 -                brackify fxy [pr_term lhs vars NOBR t1, pr_term lhs vars BR t2])
   1.355 -      | pr_term lhs vars fxy (t as _ `|-> _) =
   1.356 +                brackify fxy [pr_term thm pat vars NOBR t1, pr_term thm pat vars BR t2])
   1.357 +      | pr_term thm pat vars fxy (t as _ `|-> _) =
   1.358            let
   1.359              val (binds, t') = CodeThingol.unfold_abs t;
   1.360 -            fun pr ((v, pat), ty) = pr_bind BR ((SOME v, pat), ty);
   1.361 +            fun pr ((v, pat), ty) = pr_bind thm BR ((SOME v, pat), ty);
   1.362              val (ps, vars') = fold_map pr binds vars;
   1.363 -          in brackets (str "fun" :: ps @ str "->" @@ pr_term lhs vars' NOBR t') end
   1.364 -      | pr_term lhs vars fxy (ICase (cases as (_, t0))) = (case CodeThingol.unfold_const_app t0
   1.365 +          in brackets (str "fun" :: ps @ str "->" @@ pr_term thm pat vars' NOBR t') end
   1.366 +      | pr_term thm pat vars fxy (ICase (cases as (_, t0))) = (case CodeThingol.unfold_const_app t0
   1.367             of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
   1.368 -                then pr_case vars fxy cases
   1.369 -                else pr_app lhs vars fxy c_ts
   1.370 -            | NONE => pr_case vars fxy cases)
   1.371 -    and pr_app' lhs vars (app as ((c, (iss, tys)), ts)) =
   1.372 +                then pr_case thm vars fxy cases
   1.373 +                else pr_app thm pat vars fxy c_ts
   1.374 +            | NONE => pr_case thm vars fxy cases)
   1.375 +    and pr_app' thm pat vars (app as ((c, (iss, tys)), ts)) =
   1.376        if is_cons c then
   1.377          if length tys = length ts
   1.378          then case ts
   1.379           of [] => [(str o deresolve) c]
   1.380 -          | [t] => [(str o deresolve) c, pr_term lhs vars BR t]
   1.381 +          | [t] => [(str o deresolve) c, pr_term thm pat vars BR t]
   1.382            | _ => [(str o deresolve) c, Pretty.enum "," "(" ")"
   1.383 -                    (map (pr_term lhs vars NOBR) ts)]
   1.384 -        else [pr_term lhs vars BR (CodeThingol.eta_expand app (length tys))]
   1.385 +                    (map (pr_term thm pat vars NOBR) ts)]
   1.386 +        else [pr_term thm pat vars BR (CodeThingol.eta_expand app (length tys))]
   1.387        else (str o deresolve) c
   1.388 -        :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term lhs vars BR) ts)
   1.389 -    and pr_app lhs vars = gen_pr_app pr_app' pr_term syntax_const
   1.390 -      labelled_name is_cons lhs vars
   1.391 +        :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term thm pat vars BR) ts)
   1.392 +    and pr_app thm pat vars = gen_pr_app pr_app' pr_term syntax_const is_cons thm pat vars
   1.393      and pr_bind' ((NONE, NONE), _) = str "_"
   1.394        | pr_bind' ((SOME v, NONE), _) = str v
   1.395        | pr_bind' ((NONE, SOME p), _) = p
   1.396        | pr_bind' ((SOME v, SOME p), _) = brackets [p, str "as", str v]
   1.397 -    and pr_bind fxy = gen_pr_bind pr_bind' pr_term fxy
   1.398 -    and pr_case vars fxy (cases as ((_, [_]), _)) =
   1.399 +    and pr_bind thm = gen_pr_bind pr_bind' pr_term thm
   1.400 +    and pr_case thm vars fxy (cases as ((_, [_]), _)) =
   1.401            let
   1.402              val (binds, t') = CodeThingol.unfold_let (ICase cases);
   1.403              fun pr ((pat, ty), t) vars =
   1.404                vars
   1.405 -              |> pr_bind NOBR ((NONE, SOME pat), ty)
   1.406 +              |> pr_bind thm NOBR ((NONE, SOME pat), ty)
   1.407                |>> (fn p => concat
   1.408 -                  [str "let", p, str "=", pr_term false vars NOBR t, str "in"])
   1.409 +                  [str "let", p, str "=", pr_term thm false vars NOBR t, str "in"])
   1.410              val (ps, vars') = fold_map pr binds vars;
   1.411 -          in Pretty.chunks (ps @| pr_term false vars' NOBR t') end
   1.412 -      | pr_case vars fxy (((td, ty), b::bs), _) =
   1.413 +          in Pretty.chunks (ps @| pr_term thm false vars' NOBR t') end
   1.414 +      | pr_case thm vars fxy (((td, ty), b::bs), _) =
   1.415            let
   1.416              fun pr delim (pat, t) =
   1.417                let
   1.418 -                val (p, vars') = pr_bind NOBR ((NONE, SOME pat), ty) vars;
   1.419 -              in concat [str delim, p, str "->", pr_term false vars' NOBR t] end;
   1.420 +                val (p, vars') = pr_bind thm NOBR ((NONE, SOME pat), ty) vars;
   1.421 +              in concat [str delim, p, str "->", pr_term thm false vars' NOBR t] end;
   1.422            in
   1.423              (Pretty.enclose "(" ")" o single o brackify fxy) (
   1.424                str "match"
   1.425 -              :: pr_term false vars NOBR td
   1.426 +              :: pr_term thm false vars NOBR td
   1.427                :: pr "with" b
   1.428                :: map (pr "|") bs
   1.429              )
   1.430            end
   1.431 -      | pr_case vars fxy ((_, []), _) = str "failwith \"empty case\"";
   1.432 +      | pr_case thm vars fxy ((_, []), _) = str "failwith \"empty case\"";
   1.433      fun fish_params vars eqs =
   1.434        let
   1.435          fun fish_param _ (w as SOME _) = w
   1.436 @@ -846,7 +840,7 @@
   1.437        in map (CodeName.lookup_var vars') fished3 end;
   1.438      fun pr_stmt (MLFuns (funns as funn :: funns')) =
   1.439            let
   1.440 -            fun pr_eq (ts, t) =
   1.441 +            fun pr_eq ((ts, t), thm) =
   1.442                let
   1.443                  val consts = map_filter
   1.444                    (fn c => if (is_some o syntax_const) c
   1.445 @@ -857,9 +851,9 @@
   1.446                    |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames)
   1.447                        (insert (op =)) ts []);
   1.448                in concat [
   1.449 -                (Pretty.block o Pretty.commas) (map (pr_term true vars NOBR) ts),
   1.450 +                (Pretty.block o Pretty.commas) (map (pr_term thm true vars NOBR) ts),
   1.451                  str "->",
   1.452 -                pr_term false vars NOBR t
   1.453 +                pr_term thm false vars NOBR t
   1.454                ] end;
   1.455              fun pr_eqs name ty [] =
   1.456                    let
   1.457 @@ -874,7 +868,7 @@
   1.458                        @@ str exc_str
   1.459                      )
   1.460                    end
   1.461 -              | pr_eqs _ _ [(ts, t)] =
   1.462 +              | pr_eqs _ _ [((ts, t), thm)] =
   1.463                    let
   1.464                      val consts = map_filter
   1.465                        (fn c => if (is_some o syntax_const) c
   1.466 @@ -886,12 +880,12 @@
   1.467                            (insert (op =)) ts []);
   1.468                    in
   1.469                      concat (
   1.470 -                      map (pr_term true vars BR) ts
   1.471 +                      map (pr_term thm true vars BR) ts
   1.472                        @ str "="
   1.473 -                      @@ pr_term false vars NOBR t
   1.474 +                      @@ pr_term thm false vars NOBR t
   1.475                      )
   1.476                    end
   1.477 -              | pr_eqs _ _ (eqs as (eq as ([_], _)) :: eqs') =
   1.478 +              | pr_eqs _ _ (eqs as (eq as (([_], _), _)) :: eqs') =
   1.479                    Pretty.block (
   1.480                      str "="
   1.481                      :: Pretty.brk 1
   1.482 @@ -907,10 +901,10 @@
   1.483                        (fn c => if (is_some o syntax_const) c
   1.484                          then NONE else (SOME o NameSpace.base o deresolve) c)
   1.485                          ((fold o CodeThingol.fold_constnames)
   1.486 -                          (insert (op =)) (map snd eqs) []);
   1.487 +                          (insert (op =)) (map (snd o fst) eqs) []);
   1.488                      val vars = reserved_names
   1.489                        |> CodeName.intro_vars consts;
   1.490 -                    val dummy_parms = (map str o fish_params vars o map fst) eqs;
   1.491 +                    val dummy_parms = (map str o fish_params vars o map (fst o fst)) eqs;
   1.492                    in
   1.493                      Pretty.block (
   1.494                        Pretty.breaks dummy_parms
   1.495 @@ -1004,11 +998,11 @@
   1.496                  str "=",
   1.497                  pr_dicts NOBR [DictConst dss]
   1.498                ];
   1.499 -            fun pr_classparam_inst (classparam, c_inst) =
   1.500 +            fun pr_classparam_inst ((classparam, c_inst), thm) =
   1.501                concat [
   1.502                  (str o deresolve) classparam,
   1.503                  str "=",
   1.504 -                pr_app false reserved_names NOBR (c_inst, [])
   1.505 +                pr_app thm false reserved_names NOBR (c_inst, [])
   1.506                ];
   1.507            in
   1.508              concat (
   1.509 @@ -1088,7 +1082,7 @@
   1.510        fold_map
   1.511          (fn (name, CodeThingol.Fun stmt) =>
   1.512                map_nsp_fun_yield (mk_name_stmt false name) #>>
   1.513 -                rpair (name, (apsnd o map) fst stmt)
   1.514 +                rpair (name, stmt)
   1.515            | (name, _) =>
   1.516                error ("Function block containing illegal statement: " ^ labelled_name name)
   1.517          ) stmts
   1.518 @@ -1123,7 +1117,7 @@
   1.519               | [stmt] => MLClass stmt)));
   1.520      fun add_inst [(name, CodeThingol.Classinst stmt)] =
   1.521        map_nsp_fun_yield (mk_name_stmt false name)
   1.522 -      #>> (fn base => ([base], MLClassinst (name, (apsnd o apsnd o map) fst stmt)));
   1.523 +      #>> (fn base => ([base], MLClassinst (name, stmt)));
   1.524      fun add_stmts ((stmts as (_, CodeThingol.Fun _)::_)) =
   1.525            add_funs stmts
   1.526        | add_stmts ((stmts as (_, CodeThingol.Datatypecons _)::_)) =
   1.527 @@ -1200,31 +1194,38 @@
   1.528          error ("Unknown statement name: " ^ labelled_name name);
   1.529    in (deresolver, nodes) end;
   1.530  
   1.531 -fun serialize_ml compile pr_module pr_stmt projection module_name labelled_name reserved_names includes raw_module_alias
   1.532 +fun serialize_ml compile pr_module pr_stmt projection raw_module_name labelled_name reserved_names includes raw_module_alias
   1.533    _ syntax_tyco syntax_const program cs destination =
   1.534    let
   1.535      val is_cons = CodeThingol.is_cons program;
   1.536 +    val stmt_names = stmt_names_of_destination destination;
   1.537 +    val module_name = if null stmt_names then raw_module_name else SOME "Code";
   1.538      val (deresolver, nodes) = ml_node_of_program labelled_name module_name
   1.539        reserved_names raw_module_alias program;
   1.540      val reserved_names = CodeName.make_vars reserved_names;
   1.541      fun pr_node prefix (Dummy _) =
   1.542            NONE
   1.543 -      | pr_node prefix (Stmt (_, def)) =
   1.544 -          SOME (pr_stmt syntax_tyco syntax_const labelled_name reserved_names
   1.545 -            (deresolver prefix) is_cons def)
   1.546 +      | pr_node prefix (Stmt (_, stmt)) = if null stmt_names orelse
   1.547 +          (not o null o filter (member (op =) stmt_names) o stmt_names_of) stmt then SOME
   1.548 +            (pr_stmt syntax_tyco syntax_const labelled_name reserved_names
   1.549 +              (deresolver prefix) is_cons stmt)
   1.550 +          else NONE
   1.551        | pr_node prefix (Module (module_name, (_, nodes))) =
   1.552 -          SOME (pr_module module_name (
   1.553 -            separate (str "")
   1.554 -                ((map_filter (pr_node (prefix @ [module_name]) o Graph.get_node nodes)
   1.555 -                o rev o flat o Graph.strong_conn) nodes)));
   1.556 +          let
   1.557 +            val ps = separate (str "")
   1.558 +              ((map_filter (pr_node (prefix @ [module_name]) o Graph.get_node nodes)
   1.559 +                o rev o flat o Graph.strong_conn) nodes)
   1.560 +          in SOME (case destination of String _ => Pretty.chunks ps
   1.561 +           | _ => pr_module module_name ps)
   1.562 +          end;
   1.563      val cs' = map_filter (try (deresolver (if is_some module_name then the_list module_name else [])))
   1.564        cs;
   1.565      val p = Pretty.chunks (separate (str "") (map snd includes @ (map_filter
   1.566        (pr_node [] o Graph.get_node nodes) o rev o flat o Graph.strong_conn) nodes));
   1.567      fun output Compile = K NONE o compile o code_of_pretty
   1.568 -      | output Write = K NONE o code_writeln
   1.569 +      | output Export = K NONE o code_writeln
   1.570        | output (File file) = K NONE o File.write file o code_of_pretty
   1.571 -      | output String = SOME o code_of_pretty;
   1.572 +      | output (String _) = SOME o code_of_pretty;
   1.573    in projection (output destination p) cs' end;
   1.574  
   1.575  end; (*local*)
   1.576 @@ -1242,13 +1243,13 @@
   1.577  
   1.578  (** Haskell serializer **)
   1.579  
   1.580 -val pr_haskell_bind =
   1.581 +fun pr_haskell_bind pr_term =
   1.582    let
   1.583      fun pr_bind ((NONE, NONE), _) = str "_"
   1.584        | pr_bind ((SOME v, NONE), _) = str v
   1.585        | pr_bind ((NONE, SOME p), _) = p
   1.586        | pr_bind ((SOME v, SOME p), _) = brackets [str v, str "@", p];
   1.587 -  in gen_pr_bind pr_bind end;
   1.588 +  in gen_pr_bind pr_bind pr_term end;
   1.589  
   1.590  fun pr_haskell_stmt syntax_class syntax_tyco syntax_const labelled_name
   1.591      init_syms deresolve is_cons contr_classparam_typs deriving_show =
   1.592 @@ -1274,90 +1275,81 @@
   1.593            (map (str o CodeName.lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1;
   1.594      fun pr_tycoexpr tyvars fxy (tyco, tys) =
   1.595        brackify fxy (str tyco :: map (pr_typ tyvars BR) tys)
   1.596 -    and pr_typ tyvars fxy (tycoexpr as tyco `%% tys) =
   1.597 -          (case syntax_tyco tyco
   1.598 -           of NONE =>
   1.599 -                pr_tycoexpr tyvars fxy (deresolve tyco, tys)
   1.600 -            | SOME (i, pr) =>
   1.601 -                if not (i = length tys)
   1.602 -                then error ("Number of argument mismatch in customary serialization: "
   1.603 -                  ^ (string_of_int o length) tys ^ " given, "
   1.604 -                  ^ string_of_int i ^ " expected")
   1.605 -                else pr (pr_typ tyvars) fxy tys)
   1.606 -      | pr_typ tyvars fxy (ITyVar v) =
   1.607 -          (str o CodeName.lookup_var tyvars) v;
   1.608 +    and pr_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case syntax_tyco tyco
   1.609 +         of NONE => pr_tycoexpr tyvars fxy (deresolve tyco, tys)
   1.610 +          | SOME (i, pr) => pr (pr_typ tyvars) fxy tys)
   1.611 +      | pr_typ tyvars fxy (ITyVar v) = (str o CodeName.lookup_var tyvars) v;
   1.612      fun pr_typdecl tyvars (vs, tycoexpr) =
   1.613        Pretty.block (pr_typcontext tyvars vs @| pr_tycoexpr tyvars NOBR tycoexpr);
   1.614      fun pr_typscheme tyvars (vs, ty) =
   1.615        Pretty.block (pr_typforall tyvars vs @ pr_typcontext tyvars vs @| pr_typ tyvars NOBR ty);
   1.616 -    fun pr_term tyvars lhs vars fxy (IConst c) =
   1.617 -          pr_app tyvars lhs vars fxy (c, [])
   1.618 -      | pr_term tyvars lhs vars fxy (t as (t1 `$ t2)) =
   1.619 +    fun pr_term tyvars thm pat vars fxy (IConst c) =
   1.620 +          pr_app tyvars thm pat vars fxy (c, [])
   1.621 +      | pr_term tyvars thm pat vars fxy (t as (t1 `$ t2)) =
   1.622            (case CodeThingol.unfold_const_app t
   1.623 -           of SOME app => pr_app tyvars lhs vars fxy app
   1.624 +           of SOME app => pr_app tyvars thm pat vars fxy app
   1.625              | _ =>
   1.626                  brackify fxy [
   1.627 -                  pr_term tyvars lhs vars NOBR t1,
   1.628 -                  pr_term tyvars lhs vars BR t2
   1.629 +                  pr_term tyvars thm pat vars NOBR t1,
   1.630 +                  pr_term tyvars thm pat vars BR t2
   1.631                  ])
   1.632 -      | pr_term tyvars lhs vars fxy (IVar v) =
   1.633 +      | pr_term tyvars thm pat vars fxy (IVar v) =
   1.634            (str o CodeName.lookup_var vars) v
   1.635 -      | pr_term tyvars lhs vars fxy (t as _ `|-> _) =
   1.636 +      | pr_term tyvars thm pat vars fxy (t as _ `|-> _) =
   1.637            let
   1.638              val (binds, t') = CodeThingol.unfold_abs t;
   1.639 -            fun pr ((v, pat), ty) = pr_bind tyvars BR ((SOME v, pat), ty);
   1.640 +            fun pr ((v, pat), ty) = pr_bind tyvars thm BR ((SOME v, pat), ty);
   1.641              val (ps, vars') = fold_map pr binds vars;
   1.642 -          in brackets (str "\\" :: ps @ str "->" @@ pr_term tyvars lhs vars' NOBR t') end
   1.643 -      | pr_term tyvars lhs vars fxy (ICase (cases as (_, t0))) =
   1.644 +          in brackets (str "\\" :: ps @ str "->" @@ pr_term tyvars thm pat vars' NOBR t') end
   1.645 +      | pr_term tyvars thm pat vars fxy (ICase (cases as (_, t0))) =
   1.646            (case CodeThingol.unfold_const_app t0
   1.647             of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
   1.648 -                then pr_case tyvars vars fxy cases
   1.649 -                else pr_app tyvars lhs vars fxy c_ts
   1.650 -            | NONE => pr_case tyvars vars fxy cases)
   1.651 -    and pr_app' tyvars lhs vars ((c, (_, tys)), ts) = case contr_classparam_typs c
   1.652 -     of [] => (str o deresolve) c :: map (pr_term tyvars lhs vars BR) ts
   1.653 +                then pr_case tyvars thm vars fxy cases
   1.654 +                else pr_app tyvars thm pat vars fxy c_ts
   1.655 +            | NONE => pr_case tyvars thm vars fxy cases)
   1.656 +    and pr_app' tyvars thm pat vars ((c, (_, tys)), ts) = case contr_classparam_typs c
   1.657 +     of [] => (str o deresolve) c :: map (pr_term tyvars thm pat vars BR) ts
   1.658        | fingerprint => let
   1.659            val ts_fingerprint = ts ~~ curry Library.take (length ts) fingerprint;
   1.660            val needs_annotation = forall (fn (_, NONE) => true | (t, SOME _) =>
   1.661              (not o CodeThingol.locally_monomorphic) t) ts_fingerprint;
   1.662 -          fun pr_term_anno (t, NONE) _ = pr_term tyvars lhs vars BR t
   1.663 +          fun pr_term_anno (t, NONE) _ = pr_term tyvars thm pat vars BR t
   1.664              | pr_term_anno (t, SOME _) ty =
   1.665 -                brackets [pr_term tyvars lhs vars NOBR t, str "::", pr_typ tyvars NOBR ty];
   1.666 +                brackets [pr_term tyvars thm pat vars NOBR t, str "::", pr_typ tyvars NOBR ty];
   1.667          in
   1.668            if needs_annotation then
   1.669              (str o deresolve) c :: map2 pr_term_anno ts_fingerprint (curry Library.take (length ts) tys)
   1.670 -          else (str o deresolve) c :: map (pr_term tyvars lhs vars BR) ts
   1.671 +          else (str o deresolve) c :: map (pr_term tyvars thm pat vars BR) ts
   1.672          end
   1.673 -    and pr_app tyvars lhs vars  = gen_pr_app (pr_app' tyvars) (pr_term tyvars) syntax_const
   1.674 -      labelled_name is_cons lhs vars
   1.675 +    and pr_app tyvars = gen_pr_app (pr_app' tyvars) (pr_term tyvars) syntax_const is_cons
   1.676      and pr_bind tyvars = pr_haskell_bind (pr_term tyvars)
   1.677 -    and pr_case tyvars vars fxy (cases as ((_, [_]), _)) =
   1.678 +    and pr_case tyvars thm vars fxy (cases as ((_, [_]), _)) =
   1.679            let
   1.680              val (binds, t) = CodeThingol.unfold_let (ICase cases);
   1.681              fun pr ((pat, ty), t) vars =
   1.682                vars
   1.683 -              |> pr_bind tyvars BR ((NONE, SOME pat), ty)
   1.684 -              |>> (fn p => semicolon [p, str "=", pr_term tyvars false vars NOBR t])
   1.685 +              |> pr_bind tyvars thm BR ((NONE, SOME pat), ty)
   1.686 +              |>> (fn p => semicolon [p, str "=", pr_term tyvars thm false vars NOBR t])
   1.687              val (ps, vars') = fold_map pr binds vars;
   1.688            in
   1.689              Pretty.block_enclose (
   1.690                str "let {",
   1.691 -              concat [str "}", str "in", pr_term tyvars false vars' NOBR t]
   1.692 +              concat [str "}", str "in", pr_term tyvars thm false vars' NOBR t]
   1.693              ) ps
   1.694            end
   1.695 -      | pr_case tyvars vars fxy (((td, ty), bs as _ :: _), _) =
   1.696 +      | pr_case tyvars thm vars fxy (((td, ty), bs as _ :: _), _) =
   1.697            let
   1.698              fun pr (pat, t) =
   1.699                let
   1.700 -                val (p, vars') = pr_bind tyvars NOBR ((NONE, SOME pat), ty) vars;
   1.701 -              in semicolon [p, str "->", pr_term tyvars false vars' NOBR t] end;
   1.702 +                val (p, vars') = pr_bind tyvars thm NOBR ((NONE, SOME pat), ty) vars;
   1.703 +              in semicolon [p, str "->", pr_term tyvars thm false vars' NOBR t] end;
   1.704            in
   1.705              Pretty.block_enclose (
   1.706 -              concat [str "(case", pr_term tyvars false vars NOBR td, str "of", str "{"],
   1.707 +              concat [str "(case", pr_term tyvars thm false vars NOBR td, str "of", str "{"],
   1.708                str "})"
   1.709              ) (map pr bs)
   1.710            end
   1.711 -      | pr_case tyvars vars fxy ((_, []), _) = str "error \"empty case\"";
   1.712 +      | pr_case tyvars thm vars fxy ((_, []), _) = str "error \"empty case\"";
   1.713      fun pr_stmt (name, CodeThingol.Fun ((vs, ty), [])) =
   1.714            let
   1.715              val tyvars = CodeName.intro_vars (map fst vs) init_syms;
   1.716 @@ -1383,7 +1375,7 @@
   1.717        | pr_stmt (name, CodeThingol.Fun ((vs, ty), eqs)) =
   1.718            let
   1.719              val tyvars = CodeName.intro_vars (map fst vs) init_syms;
   1.720 -            fun pr_eq ((ts, t), _) =
   1.721 +            fun pr_eq ((ts, t), thm) =
   1.722                let
   1.723                  val consts = map_filter
   1.724                    (fn c => if (is_some o syntax_const) c
   1.725 @@ -1396,9 +1388,9 @@
   1.726                in
   1.727                  semicolon (
   1.728                    (str o deresolve_base) name
   1.729 -                  :: map (pr_term tyvars true vars BR) ts
   1.730 +                  :: map (pr_term tyvars thm true vars BR) ts
   1.731                    @ str "="
   1.732 -                  @@ pr_term tyvars false vars NOBR t
   1.733 +                  @@ pr_term tyvars thm false vars NOBR t
   1.734                  )
   1.735                end;
   1.736            in
   1.737 @@ -1475,11 +1467,11 @@
   1.738        | pr_stmt (_, CodeThingol.Classinst ((class, (tyco, vs)), (_, classparam_insts))) =
   1.739            let
   1.740              val tyvars = CodeName.intro_vars (map fst vs) init_syms;
   1.741 -            fun pr_instdef ((classparam, c_inst), _) =
   1.742 +            fun pr_instdef ((classparam, c_inst), thm) =
   1.743                semicolon [
   1.744                  (str o classparam_name class) classparam,
   1.745                  str "=",
   1.746 -                pr_app tyvars false init_syms NOBR (c_inst, [])
   1.747 +                pr_app tyvars thm false init_syms NOBR (c_inst, [])
   1.748                ];
   1.749            in
   1.750              Pretty.block_enclose (
   1.751 @@ -1497,9 +1489,9 @@
   1.752  
   1.753  fun pretty_haskell_monad c_bind =
   1.754    let
   1.755 -    fun pretty pr vars fxy [(t, _)] =
   1.756 +    fun pretty pr thm pat vars fxy [(t, _)] =
   1.757        let
   1.758 -        val pr_bind = pr_haskell_bind (K pr);
   1.759 +        val pr_bind = pr_haskell_bind (K (K pr)) thm;
   1.760          fun pr_monad (NONE, t) vars =
   1.761                (semicolon [pr vars NOBR t], vars)
   1.762            | pr_monad (SOME (bind, true), t) vars = vars
   1.763 @@ -1565,10 +1557,12 @@
   1.764          handle Option => error ("Unknown statement name: " ^ labelled_name name);
   1.765    in (deresolver, hs_program) end;
   1.766  
   1.767 -fun serialize_haskell module_prefix module_name string_classes labelled_name
   1.768 +fun serialize_haskell module_prefix raw_module_name string_classes labelled_name
   1.769      reserved_names includes raw_module_alias
   1.770      syntax_class syntax_tyco syntax_const program cs destination =
   1.771    let
   1.772 +    val stmt_names = stmt_names_of_destination destination;
   1.773 +    val module_name = if null stmt_names then raw_module_name else SOME "Code";
   1.774      val (deresolver, hs_program) = haskell_program_of_program labelled_name
   1.775        module_name module_prefix reserved_names raw_module_alias program;
   1.776      val is_cons = CodeThingol.is_cons program;
   1.777 @@ -1599,7 +1593,7 @@
   1.778          str "",
   1.779          str "}"
   1.780        ]);
   1.781 -    fun serialize_module (module_name', (deps, (stmts, _))) =
   1.782 +    fun serialize_module1 (module_name', (deps, (stmts, _))) =
   1.783        let
   1.784          val stmt_names = map fst stmts;
   1.785          val deps' = subtract (op =) stmt_names deps
   1.786 @@ -1625,6 +1619,15 @@
   1.787                  | (_, (_, NONE)) => NONE) stmts)
   1.788            )
   1.789        in pr_module module_name' content end;
   1.790 +    fun serialize_module2 (_, (_, (stmts, _))) = Pretty.chunks (
   1.791 +      separate (str "") (map_filter
   1.792 +        (fn (name, (_, SOME stmt)) => if null stmt_names
   1.793 +              orelse member (op =) stmt_names name
   1.794 +              then SOME (pr_stmt false (name, stmt))
   1.795 +              else NONE
   1.796 +          | (_, (_, NONE)) => NONE) stmts));
   1.797 +    val serialize_module = case destination of String _ => pair "" o serialize_module2
   1.798 +      | _ => serialize_module1;
   1.799      fun write_module destination (modlname, content) =
   1.800        let
   1.801          val filename = case modlname
   1.802 @@ -1635,9 +1638,9 @@
   1.803          val _ = File.mkdir (Path.dir pathname);
   1.804        in File.write pathname (code_of_pretty content) end
   1.805      fun output Compile = error ("Haskell: no internal compilation")
   1.806 -      | output Write = K NONE o map (code_writeln o snd)
   1.807 +      | output Export = K NONE o map (code_writeln o snd)
   1.808        | output (File destination) = K NONE o map (write_module destination)
   1.809 -      | output String = SOME o cat_lines o map (code_of_pretty o snd);
   1.810 +      | output (String _) = SOME o cat_lines o map (code_of_pretty o snd);
   1.811    in
   1.812      output destination (map (uncurry pr_module) includes
   1.813        @ map serialize_module (Symtab.dest hs_program))
   1.814 @@ -1723,7 +1726,7 @@
   1.815    let
   1.816      val pretty_ops = pr_pretty target;
   1.817      val mk_list = #pretty_list pretty_ops;
   1.818 -    fun pretty pr vars fxy [(t1, _), (t2, _)] =
   1.819 +    fun pretty pr thm pat vars fxy [(t1, _), (t2, _)] =
   1.820        case Option.map (cons t1) (implode_list c_nil c_cons t2)
   1.821         of SOME ts => mk_list (map (pr vars NOBR) ts)
   1.822          | NONE => default_list (#infix_cons pretty_ops) (pr vars) fxy t1 t2;
   1.823 @@ -1735,7 +1738,7 @@
   1.824      val mk_list = #pretty_list pretty_ops;
   1.825      val mk_char = #pretty_char pretty_ops;
   1.826      val mk_string = #pretty_string pretty_ops;
   1.827 -    fun pretty pr vars fxy [(t1, _), (t2, _)] =
   1.828 +    fun pretty pr thm pat vars fxy [(t1, _), (t2, _)] =
   1.829        case Option.map (cons t1) (implode_list c_nil c_cons t2)
   1.830         of SOME ts => (case implode_string c_char c_nibbles mk_char mk_string ts
   1.831             of SOME p => p
   1.832 @@ -1746,17 +1749,17 @@
   1.833  fun pretty_char c_char c_nibbles target =
   1.834    let
   1.835      val mk_char = #pretty_char (pr_pretty target);
   1.836 -    fun pretty _ _ _ [(t1, _), (t2, _)] =
   1.837 +    fun pretty _ thm _ _ _ [(t1, _), (t2, _)] =
   1.838        case decode_char c_nibbles (t1, t2)
   1.839         of SOME c => (str o mk_char) c
   1.840 -        | NONE => error "Illegal character expression";
   1.841 +        | NONE => nerror thm "Illegal character expression";
   1.842    in (2, pretty) end;
   1.843  
   1.844  fun pretty_numeral unbounded negative c_pls c_min c_bit0 c_bit1 target =
   1.845    let
   1.846      val mk_numeral = #pretty_numeral (pr_pretty target);
   1.847 -    fun pretty _ _ _ [(t, _)] =
   1.848 -      (str o mk_numeral unbounded o implode_numeral negative c_pls c_min c_bit0 c_bit1) t;
   1.849 +    fun pretty _ thm _ _ _ [(t, _)] =
   1.850 +      (str o mk_numeral unbounded o implode_numeral thm negative c_pls c_min c_bit0 c_bit1) t;
   1.851    in (1, pretty) end;
   1.852  
   1.853  fun pretty_message c_char c_nibbles c_nil c_cons target =
   1.854 @@ -1764,12 +1767,12 @@
   1.855      val pretty_ops = pr_pretty target;
   1.856      val mk_char = #pretty_char pretty_ops;
   1.857      val mk_string = #pretty_string pretty_ops;
   1.858 -    fun pretty pr vars fxy [(t, _)] =
   1.859 +    fun pretty _ thm _ _ _ [(t, _)] =
   1.860        case implode_list c_nil c_cons t
   1.861         of SOME ts => (case implode_string c_char c_nibbles mk_char mk_string ts
   1.862             of SOME p => p
   1.863 -            | NONE => error "Illegal message expression")
   1.864 -        | NONE => error "Illegal message expression";
   1.865 +            | NONE => nerror thm "Illegal message expression")
   1.866 +        | NONE => nerror thm "Illegal message expression";
   1.867    in (1, pretty) end;
   1.868  
   1.869  fun pretty_imperative_monad_bind bind' return' unit' =
   1.870 @@ -1800,26 +1803,21 @@
   1.871            | _ => force t;
   1.872      fun tr_bind ts = (dummy_name, dummy_type)
   1.873        `|-> ICase (((IVar dummy_name, dummy_type), [(unitt, tr_bind' ts)]), dummy_case_term);
   1.874 -    fun pretty pr vars fxy ts = pr vars fxy (tr_bind ts);
   1.875 +    fun pretty pr thm pat vars fxy ts = pr vars fxy (tr_bind ts);
   1.876    in (2, pretty) end;
   1.877  
   1.878 -fun no_bindings x = (Option.map o apsnd)
   1.879 -  (fn pretty => fn pr => fn vars => pretty (pr vars)) x;
   1.880 -
   1.881  end; (*local*)
   1.882  
   1.883  
   1.884 -(** serializer interfaces **)
   1.885 +(** serializer use cases **)
   1.886  
   1.887  (* evaluation *)
   1.888  
   1.889 -fun eval_serializer module [] = serialize_ml
   1.890 -  (use_text (1, "code to be evaluated") Output.ml_output false) 
   1.891 -  (K Pretty.chunks) pr_sml_stmt
   1.892 +fun code_antiq_serializer module [] = serialize_ml (K ()) (K Pretty.chunks) pr_sml_stmt
   1.893    (fn SOME s => fn cs => SOME ("let\n" ^ s ^ "\nin fn () => " ^ enclose "(" ")" (commas cs) ^ " end"))
   1.894    (SOME "Isabelle_Eval");
   1.895  
   1.896 -fun sml_code_of thy program cs = mount_serializer thy (SOME eval_serializer) target_SML NONE [] program cs String
   1.897 +fun sml_code_of thy program cs = mount_serializer thy (SOME code_antiq_serializer) target_SML NONE [] program cs (String [])
   1.898    |> the;
   1.899  
   1.900  fun eval eval'' term_of reff thy ct args =
   1.901 @@ -1843,16 +1841,61 @@
   1.902  fun eval_term reff = eval CodeThingol.eval_term I reff;
   1.903  
   1.904  
   1.905 -(* presentation *)
   1.906 +(* instrumentalization by antiquotation *)
   1.907  
   1.908 -fun code_of thy target module_name cs =
   1.909 +fun ml_code_antiq (ctxt, args) = 
   1.910 +  let
   1.911 +    val thy = Context.theory_of ctxt;
   1.912 +    val (ts, (ctxt', args')) = Scan.repeat1 Args.term (ctxt, args);
   1.913 +    val cs = map (CodeUnit.check_const thy) ts;
   1.914 +    val (cs', program) = CodeThingol.consts_program thy cs;
   1.915 +    val s = sml_code_of thy program cs' ^ " ()";
   1.916 +  in (("codevals", s), (ctxt', args')) end;
   1.917 +
   1.918 +
   1.919 +(* code presentation *)
   1.920 +
   1.921 +fun code_of thy target module_name cs stmt_names =
   1.922    let
   1.923      val (cs', program) = CodeThingol.consts_program thy cs;
   1.924    in
   1.925 -    string (serialize thy target (SOME module_name) [] program cs')
   1.926 +    string stmt_names (serialize thy target (SOME module_name) [] program cs')
   1.927    end;
   1.928  
   1.929  
   1.930 +(* code generation *)
   1.931 +
   1.932 +fun read_const_exprs thy cs =
   1.933 +  let
   1.934 +    val (cs1, cs2) = CodeName.read_const_exprs thy cs;
   1.935 +    val (cs3, program) = CodeThingol.consts_program thy cs2;
   1.936 +    val cs4 = CodeThingol.transitivly_non_empty_funs program (abort_allowed thy);
   1.937 +    val cs5 = map_filter
   1.938 +      (fn (c, c') => if member (op =) cs4 c' then SOME c else NONE) (cs2 ~~ cs3);
   1.939 +  in fold (insert (op =)) cs5 cs1 end;
   1.940 +
   1.941 +fun cached_program thy = 
   1.942 +  let
   1.943 +    val program = CodeThingol.cached_program thy;
   1.944 +  in (CodeThingol.transitivly_non_empty_funs program (abort_allowed thy), program) end
   1.945 +
   1.946 +fun export_code thy cs seris =
   1.947 +  let
   1.948 +    val (cs', program) = if null cs then cached_program thy
   1.949 +      else CodeThingol.consts_program thy cs;
   1.950 +    fun mk_seri_dest dest = case dest
   1.951 +     of NONE => compile
   1.952 +      | SOME "-" => export
   1.953 +      | SOME f => file (Path.explode f)
   1.954 +    val _ = map (fn (((target, module), dest), args) =>
   1.955 +      (mk_seri_dest dest (serialize thy target module args program cs'))) seris;
   1.956 +  in () end;
   1.957 +
   1.958 +fun export_code_cmd raw_cs seris thy = export_code thy (read_const_exprs thy raw_cs) seris;
   1.959 +
   1.960 +
   1.961 +(** serializer data **)
   1.962 +
   1.963  (* infix syntax *)
   1.964  
   1.965  datatype 'a mixfix =
   1.966 @@ -1869,11 +1912,7 @@
   1.967        | fillin pr (Arg fxy :: mfx) (a :: args) =
   1.968            (pr fxy o prep_arg) a :: fillin pr mfx args
   1.969        | fillin pr (Pretty p :: mfx) args =
   1.970 -          p :: fillin pr mfx args
   1.971 -      | fillin _ [] _ =
   1.972 -          error ("Inconsistent mixfix: too many arguments")
   1.973 -      | fillin _ _ [] =
   1.974 -          error ("Inconsistent mixfix: too less arguments");
   1.975 +          p :: fillin pr mfx args;
   1.976    in
   1.977      (i, fn pr => fn fixity_ctxt => fn args =>
   1.978        gen_brackify (fixity fixity_this fixity_ctxt) (fillin pr mfx args))
   1.979 @@ -1960,6 +1999,9 @@
   1.980             (Symtab.delete_safe tyco')
   1.981    end;
   1.982  
   1.983 +fun simple_const_syntax x = (Option.map o apsnd)
   1.984 +  (fn pretty => fn pr => fn thm => fn pat => fn vars => pretty (pr vars)) x;
   1.985 +
   1.986  fun gen_add_syntax_const prep_const target raw_c raw_syn thy =
   1.987    let
   1.988      val c = prep_const thy raw_c;
   1.989 @@ -2019,7 +2061,7 @@
   1.990      |> gen_add_syntax_const (K I) target_Haskell c_run
   1.991            (SOME (pretty_haskell_monad c_bind'))
   1.992      |> gen_add_syntax_const (K I) target_Haskell c_bind
   1.993 -          (no_bindings (SOME (parse_infix fst (L, 1) ">>=")))
   1.994 +          (simple_const_syntax (SOME (parse_infix fst (L, 1) ">>=")))
   1.995    else
   1.996      thy
   1.997      |> gen_add_syntax_const (K I) target c_bind
   1.998 @@ -2097,11 +2139,11 @@
   1.999  val allow_abort_cmd = gen_allow_abort CodeUnit.read_const;
  1.1000  
  1.1001  fun add_syntax_tycoP target tyco = parse_syntax I >> add_syntax_tyco_cmd target tyco;
  1.1002 -fun add_syntax_constP target c = parse_syntax fst >> (add_syntax_const_cmd target c o no_bindings);
  1.1003 +fun add_syntax_constP target c = parse_syntax fst >> (add_syntax_const_cmd target c o simple_const_syntax);
  1.1004  
  1.1005  fun add_undefined target undef target_undefined thy =
  1.1006    let
  1.1007 -    fun pr _ _ _ _ = str target_undefined;
  1.1008 +    fun pr _ _ _ _ _ _ = str target_undefined;
  1.1009    in
  1.1010      thy
  1.1011      |> add_syntax_const target undef (SOME (~1, pr))
  1.1012 @@ -2164,49 +2206,8 @@
  1.1013    end;
  1.1014  
  1.1015  
  1.1016 -(** code generation at a glance **)
  1.1017  
  1.1018 -fun read_const_exprs thy cs =
  1.1019 -  let
  1.1020 -    val (cs1, cs2) = CodeName.read_const_exprs thy cs;
  1.1021 -    val (cs3, program) = CodeThingol.consts_program thy cs2;
  1.1022 -    val cs4 = CodeThingol.transitivly_non_empty_funs program (abort_allowed thy);
  1.1023 -    val cs5 = map_filter
  1.1024 -      (fn (c, c') => if member (op =) cs4 c' then SOME c else NONE) (cs2 ~~ cs3);
  1.1025 -  in fold (insert (op =)) cs5 cs1 end;
  1.1026 -
  1.1027 -fun cached_program thy = 
  1.1028 -  let
  1.1029 -    val program = CodeThingol.cached_program thy;
  1.1030 -  in (CodeThingol.transitivly_non_empty_funs program (abort_allowed thy), program) end
  1.1031 -
  1.1032 -fun code thy cs seris =
  1.1033 -  let
  1.1034 -    val (cs', program) = if null cs
  1.1035 -      then cached_program thy
  1.1036 -      else CodeThingol.consts_program thy cs;
  1.1037 -    fun mk_seri_dest dest = case dest
  1.1038 -     of NONE => compile
  1.1039 -      | SOME "-" => write
  1.1040 -      | SOME f => file (Path.explode f)
  1.1041 -    val _ = map (fn (((target, module), dest), args) =>
  1.1042 -      (mk_seri_dest dest (serialize thy target module args program cs'))) seris;
  1.1043 -  in () end;
  1.1044 -
  1.1045 -fun sml_of thy cs = 
  1.1046 -  let
  1.1047 -    val (cs', program) = CodeThingol.consts_program thy cs;
  1.1048 -  in sml_code_of thy program cs' ^ " ()" end;
  1.1049 -
  1.1050 -fun code_antiq (ctxt, args) = 
  1.1051 -  let
  1.1052 -    val thy = Context.theory_of ctxt;
  1.1053 -    val (ts, (ctxt', args')) = Scan.repeat1 Args.term (ctxt, args);
  1.1054 -    val cs = map (CodeUnit.check_const thy) ts;
  1.1055 -    val s = sml_of thy cs;
  1.1056 -  in (("codevals", s), (ctxt', args')) end;
  1.1057 -
  1.1058 -fun export_code_cmd raw_cs seris thy = code thy (read_const_exprs thy raw_cs) seris;
  1.1059 +(** Isar setup **)
  1.1060  
  1.1061  val (inK, module_nameK, fileK) = ("in", "module_name", "file");
  1.1062  
  1.1063 @@ -2218,9 +2219,6 @@
  1.1064       -- Scan.optional (P.$$$ "(" |-- P.arguments --| P.$$$ ")") []
  1.1065    ) >> (fn (raw_cs, seris) => cmd raw_cs seris));
  1.1066  
  1.1067 -
  1.1068 -(** Isar setup **)
  1.1069 -
  1.1070  val _ = OuterSyntax.keywords [infixK, infixlK, infixrK, inK, module_nameK, fileK];
  1.1071  
  1.1072  val _ =
  1.1073 @@ -2251,7 +2249,7 @@
  1.1074    OuterSyntax.command "code_const" "define code syntax for constant" K.thy_decl (
  1.1075      parse_multi_syntax P.term (parse_syntax fst)
  1.1076      >> (Toplevel.theory oo fold) (fn (target, syns) =>
  1.1077 -          fold (fn (raw_const, syn) => add_syntax_const_cmd target raw_const (no_bindings syn)) syns)
  1.1078 +          fold (fn (raw_const, syn) => add_syntax_const_cmd target raw_const (simple_const_syntax syn)) syns)
  1.1079    );
  1.1080  
  1.1081  val _ =
  1.1082 @@ -2296,7 +2294,7 @@
  1.1083      | NONE => error ("Bad directive " ^ quote cmd)))
  1.1084    handle TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure;
  1.1085  
  1.1086 -val _ = ML_Context.value_antiq "code" code_antiq;
  1.1087 +val _ = ML_Context.value_antiq "code" ml_code_antiq;
  1.1088  
  1.1089  
  1.1090  (* serializer setup, including serializer defaults *)