# HG changeset patch # User haftmann # Date 1169816344 -3600 # Node ID 461130ccfef4b83a514e23bdc446909288ecf144 # Parent 680b04dbd51c8a5a7708c3acab1d5810fdd210a7 clarified code diff -r 680b04dbd51c -r 461130ccfef4 src/Pure/Tools/codegen_consts.ML --- a/src/Pure/Tools/codegen_consts.ML Fri Jan 26 13:59:03 2007 +0100 +++ b/src/Pure/Tools/codegen_consts.ML Fri Jan 26 13:59:04 2007 +0100 @@ -3,7 +3,7 @@ Author: Florian Haftmann, TU Muenchen Identifying constants by name plus normalized type instantantiation schemes. -Convenient data structures for constants. +Convenient data structures for constants. Auxiliary. *) signature CODEGEN_CONSTS = @@ -16,12 +16,15 @@ val typ_of_inst: theory -> const -> string * typ val norm: theory -> const -> const val norm_of_typ: theory -> string * typ -> const + val typ_sort_inst: Sorts.algebra -> typ * sort -> sort Vartab.table -> sort Vartab.table + val typargs: theory -> string * typ -> typ list val find_def: theory -> const -> (string (*theory name*) * thm) option val consts_of: theory -> term -> const list val read_const: theory -> string -> const val string_of_const: theory -> const -> string val raw_string_of_const: const -> string val string_of_const_typ: theory -> string * typ -> string + val string_of_typ: theory -> typ -> string end; structure CodegenConsts: CODEGEN_CONSTS = @@ -43,11 +46,13 @@ (* type instantiations, overloading, dictionary values *) +fun string_of_typ thy = setmp show_sorts true (Sign.string_of_typ thy); + fun inst_of_typ thy (c_ty as (c, ty)) = - (c, Consts.typargs (Sign.consts_of thy) c_ty); + (c, Sign.const_typargs thy c_ty); fun typ_of_inst thy (c_tys as (c, tys)) = - (c, Consts.instance (Sign.consts_of thy) c_tys); + (c, Sign.const_instance thy c_tys); fun find_def thy (c, tys) = let @@ -72,23 +77,43 @@ fun norm thy (c, insts) = let fun disciplined class [ty as Type (tyco, _)] = - (case try (Sorts.mg_domain (Sign.classes_of thy) tyco) [class] - of SOME sorts => (c, [Type (tyco, map (fn v => TVar ((v, 0), [])) - (Name.invents Name.context "'a" (length sorts)))]) - | NONE => error ("no such instance: " ^ quote c ^ ", " ^ quote tyco)) + let + val sorts = Sorts.mg_domain (Sign.classes_of thy) tyco [class]; + val vs = Name.invents Name.context "'a" (length sorts); + in + (c, [Type (tyco, map (fn v => TVar ((v, 0), [])) vs)]) + end | disciplined class _ = (c, [TVar (("'a", 0), [class])]); in case AxClass.class_of_param thy c of SOME class => disciplined class insts - | _ => inst_of_typ thy (c, Sign.the_const_type thy c) + | NONE => inst_of_typ thy (c, Sign.the_const_type thy c) end; fun norm_of_typ thy (c, ty) = - norm thy (c, Consts.typargs (Sign.consts_of thy) (c, ty)); + norm thy (c, Sign.const_typargs thy (c, ty)); fun consts_of thy t = fold_aterms (fn Const c => cons (norm_of_typ thy c) | _ => I) t [] +fun typ_sort_inst algebra = + let + val inters = Sorts.inter_sort algebra; + fun match _ [] = I + | match (TVar (v, S)) S' = Vartab.map_default (v, []) (fn S'' => inters (S, inters (S', S''))) + | match (Type (a, Ts)) S = + fold2 match Ts (Sorts.mg_domain algebra a S) + in uncurry match end; + +fun typargs thy (c_ty as (c, ty)) = + let + val opt_class = AxClass.class_of_param thy c; + val tys = Sign.const_typargs thy (c, ty); + in case (opt_class, tys) + of (SOME _, [Type (_, tys')]) => tys' + | _ => tys + end; + (* reading constants as terms *) @@ -104,7 +129,7 @@ norm_of_typ thy o read_const_typ thy; -(* printing constants *) +(* printing *) fun string_of_const thy (c, tys) = space_implode " " (Sign.extern_const thy c diff -r 680b04dbd51c -r 461130ccfef4 src/Pure/Tools/codegen_data.ML --- a/src/Pure/Tools/codegen_data.ML Fri Jan 26 13:59:03 2007 +0100 +++ b/src/Pure/Tools/codegen_data.ML Fri Jan 26 13:59:04 2007 +0100 @@ -109,7 +109,7 @@ (** code theorems **) -(* pairs of (selected, deleted) function theorems *) +(* pairs of (selected, deleted) defining equations *) type sdthms = thm list Susp.T * thm list; @@ -123,7 +123,7 @@ | matches (_ :: _) [] = false | matches (x :: xs) (y :: ys) = Pattern.matches thy (x, y) andalso matches xs ys; fun drop thm' = not (matches args (args_of thm')) - orelse (warning ("Dropping redundant function theorem\n" ^ string_of_thm thm'); false); + orelse (warning ("Dropping redundant defining equation\n" ^ string_of_thm thm'); false); val (keeps, drops) = List.partition drop sels; in (thm :: keeps, dels |> fold (insert eq_thm) drops |> remove eq_thm thm) end; @@ -353,7 +353,7 @@ in (Pretty.writeln o Pretty.block o Pretty.fbreaks) ([ Pretty.str "code theorems:", - Pretty.str "function theorems:" ] @ + Pretty.str "defining equations:" ] @ map pretty_func funs @ [ Pretty.block ( Pretty.str "inlining theorems:" @@ -418,10 +418,10 @@ val (ty1::tys) = map CodegenFunc.typ_func thms'; fun unify ty env = Sign.typ_unify thy (ty1, ty) env handle Type.TUNIFY => - error ("Type unificaton failed, while unifying function equations\n" + error ("Type unificaton failed, while unifying defining equations\n" ^ (cat_lines o map Display.string_of_thm) thms ^ "\nwith types\n" - ^ (cat_lines o map (Sign.string_of_typ thy)) (ty1 :: tys)); + ^ (cat_lines o map (CodegenConsts.string_of_typ thy)) (ty1 :: tys)); val (env, _) = fold unify tys (Vartab.empty, maxidx) val instT = Vartab.fold (fn (x_i, (sort, ty)) => cons (Thm.ctyp_of thy (TVar (x_i, sort)), Thm.ctyp_of thy ty)) env []; @@ -430,7 +430,7 @@ fun certify_const thy c c_thms = let fun cert (c', thm) = if CodegenConsts.eq_const (c, c') - then thm else error ("Wrong head of function equation,\nexpected constant " + then thm else error ("Wrong head of defining equation,\nexpected constant " ^ CodegenConsts.string_of_const thy c ^ "\n" ^ string_of_thm thm) in map cert c_thms end; @@ -593,7 +593,6 @@ val thy = Thm.theory_of_thm thm; val raw_funcs = CodegenFunc.mk_func thm; val error_warning = if strict_functyp then error else warning #> K NONE; - val string_of_typ = setmp show_sorts true (Sign.string_of_typ thy); fun check_typ_classop class (const as (c, [Type (tyco, _)]), thm) = let val ((_, ty), _) = CodegenFunc.dest_func thm; @@ -611,22 +610,22 @@ in if Sign.typ_instance thy (ty_strongest, ty) then if Sign.typ_instance thy (ty, ty_decl) then SOME (const, thm) - else (warning ("Constraining type\n" ^ string_of_typ ty - ^ "\nof function theorem\n" + else (warning ("Constraining type\n" ^ CodegenConsts.string_of_typ thy ty + ^ "\nof defining equation\n" ^ string_of_thm thm ^ "\nto permitted most general type\n" - ^ string_of_typ ty_decl); + ^ CodegenConsts.string_of_typ thy ty_decl); SOME (const, constrain thm)) - else error_warning ("Type\n" ^ string_of_typ ty - ^ "\nof function theorem\n" + else error_warning ("Type\n" ^ CodegenConsts.string_of_typ thy ty + ^ "\nof defining equation\n" ^ string_of_thm thm ^ "\nis incompatible with permitted least general type\n" - ^ string_of_typ ty_strongest) + ^ CodegenConsts.string_of_typ thy ty_strongest) end | check_typ_classop class ((c, [_]), thm) = (if strict_functyp then error else warning #> K NONE) ("Illegal type for class operation " ^ quote c - ^ "\nin function theorem\n" + ^ "\nin defining equation\n" ^ string_of_thm thm); fun check_typ_fun (const as (c, _), thm) = let @@ -634,11 +633,11 @@ val ty_decl = Sign.the_const_type thy c; in if Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts ty) then SOME (const, thm) - else error_warning ("Type\n" ^ string_of_typ ty - ^ "\nof function theorem\n" + else error_warning ("Type\n" ^ CodegenConsts.string_of_typ thy ty + ^ "\nof defining equation\n" ^ string_of_thm thm ^ "\nis incompatible declared function type\n" - ^ string_of_typ ty_decl) + ^ CodegenConsts.string_of_typ thy ty_decl) end; fun check_typ (const as (c, tys), thm) = case AxClass.class_of_param thy c @@ -758,7 +757,7 @@ |> fold (fn (_, (_, f)) => apply_preproc thy f) ((#preprocs o the_preproc o get_exec) thy) |> map (CodegenFunc.rewrite_func ((#inlines o the_preproc o get_exec) thy)) |> fold (fn (_, (_, f)) => apply_inline_proc thy f) ((#inline_procs o the_preproc o get_exec) thy) -(*FIXME - must check: rewrite rule, function equation, proper constant |> map (snd o check_func false thy) *) +(*FIXME - must check: rewrite rule, defining equation, proper constant |> map (snd o check_func false thy) *) |> sort (cmp_thms thy) |> common_typ_funcs; diff -r 680b04dbd51c -r 461130ccfef4 src/Pure/Tools/codegen_func.ML --- a/src/Pure/Tools/codegen_func.ML Fri Jan 26 13:59:03 2007 +0100 +++ b/src/Pure/Tools/codegen_func.ML Fri Jan 26 13:59:04 2007 +0100 @@ -15,6 +15,7 @@ val dest_func: thm -> (string * typ) * term list val typ_func: thm -> typ + val inst_thm: sort Vartab.table -> thm -> thm val expand_eta: int -> thm -> thm val rewrite_func: thm list -> thm -> thm end; @@ -62,7 +63,7 @@ end; -(* making function theorems *) +(* making defining equations *) val typ_func = lift_thm_thy (fn thy => snd o dest_Const o fst o strip_comb o fst o Logic.dest_equals o ObjectLogic.drop_judgment thy o Drule.plain_prop_of); @@ -83,20 +84,30 @@ ((fold o fold_aterms) (fn Var (v, _) => cons v | _ => I ) args []) - then bad_thm "Repeated variables on left hand side of function equation" thm + then bad_thm "Repeated variables on left hand side of defining equation" thm else () - fun no_abs (Abs _) = bad_thm "Abstraction on left hand side of function equation" thm + fun no_abs (Abs _) = bad_thm "Abstraction on left hand side of defining equation" thm | no_abs (t1 $ t2) = (no_abs t1; no_abs t2) | no_abs _ = (); val _ = map no_abs args; in thm end - | NONE => bad_thm "Not a function equation" thm; + | NONE => bad_thm "Not a defining equation" thm; val mk_func = map (mk_head o assert_func) o mk_rew; (* utilities *) +fun inst_thm tvars' thm = + let + val thy = Thm.theory_of_thm thm; + val tvars = (Term.add_tvars o Thm.prop_of) thm []; + fun mk_inst (tvar as (v, _)) = case Vartab.lookup tvars' v + of SOME sort => SOME (pairself (Thm.ctyp_of thy o TVar) (tvar, (v, sort))) + | NONE => NONE; + val insts = map_filter mk_inst tvars; + in Thm.instantiate (insts, []) thm end; + fun expand_eta k thm = let val thy = Thm.theory_of_thm thm; @@ -139,8 +150,6 @@ val args' = map rewrite ct_args; val lhs' = Thm.symmetric (fold (fn th1 => fn th2 => Thm.combination th2 th1) args' (Thm.reflexive ct_f)); - in - Thm.transitive (Thm.transitive lhs' thm) rhs' - end handle Bind => raise ERROR "rewrite_func" + in Thm.transitive (Thm.transitive lhs' thm) rhs' end; end; diff -r 680b04dbd51c -r 461130ccfef4 src/Pure/Tools/codegen_names.ML --- a/src/Pure/Tools/codegen_names.ML Fri Jan 26 13:59:03 2007 +0100 +++ b/src/Pure/Tools/codegen_names.ML Fri Jan 26 13:59:04 2007 +0100 @@ -340,7 +340,7 @@ val nsp = NameSpace.base name; in case AList.lookup (op =) nsp_mapping nsp of SOME msg => msg ^ " " ^ quote nam - | NONE => error ("illegal shallow name space: " ^ quote nsp) + | NONE => error ("Illegal shallow name space: " ^ quote nsp) end; @@ -378,6 +378,6 @@ fun lookup_var (namemap, _) name = case Symtab.lookup namemap name of SOME name' => name' - | NONE => error ("invalid name in context: " ^ quote name); + | NONE => error ("Invalid name in context: " ^ quote name); end; diff -r 680b04dbd51c -r 461130ccfef4 src/Pure/Tools/codegen_package.ML --- a/src/Pure/Tools/codegen_package.ML Fri Jan 26 13:59:03 2007 +0100 +++ b/src/Pure/Tools/codegen_package.ML Fri Jan 26 13:59:04 2007 +0100 @@ -86,7 +86,7 @@ val _ = Context.add_setup (Code.init #> CodegenPackageData.init); -(* preparing function equations *) +(* preparing defining equations *) fun prep_eqs thy (thms as thm :: _) = let @@ -112,30 +112,27 @@ fun ensure_def thy = CodegenThingol.ensure_def (CodegenNames.labelled_name thy); -fun ensure_def_class thy (algbr as ((_, algebra), _)) funcgr strct class trns = +fun ensure_def_class thy (algbr as ((_, algebra), _)) funcgr strct class = let val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class; val (v, cs) = AxClass.params_of_class thy class; val class' = CodegenNames.class thy class; val classrels' = map (curry (CodegenNames.classrel thy) class) superclasses; val classops' = map (CodegenNames.const thy o CodegenConsts.norm_of_typ thy) cs; - fun defgen_class trns = - trns - |> fold_map (ensure_def_class thy algbr funcgr strct) superclasses - ||>> (fold_map (exprgen_type thy algbr funcgr strct) o map snd) cs - |-> (fn (superclasses, classoptyps) => succeed + val defgen_class = + fold_map (ensure_def_class thy algbr funcgr strct) superclasses + ##>> (fold_map (exprgen_type thy algbr funcgr strct) o map snd) cs + #-> (fn (superclasses, classoptyps) => succeed (CodegenThingol.Class (superclasses ~~ classrels', (unprefix "'" v, classops' ~~ classoptyps)))) in - trns - |> tracing (fn _ => "generating class " ^ quote class) - |> ensure_def thy defgen_class true + tracing (fn _ => "generating class " ^ quote class) + #> ensure_def thy defgen_class true ("generating class " ^ quote class) class' - |> pair class' + #> pair class' end -and ensure_def_classrel thy algbr funcgr strct (subclass, superclass) trns = - trns - |> ensure_def_class thy algbr funcgr strct subclass - |>> (fn _ => CodegenNames.classrel thy (subclass, superclass)) +and ensure_def_classrel thy algbr funcgr strct (subclass, superclass) = + ensure_def_class thy algbr funcgr strct subclass + #>> (fn _ => CodegenNames.classrel thy (subclass, superclass)) and ensure_def_tyco thy algbr funcgr strct tyco trns = let fun defgen_datatype trns = @@ -165,9 +162,7 @@ trns |> fold_map (ensure_def_class thy algbr funcgr strct) (proj_sort sort) |>> (fn sort => (unprefix "'" v, sort)) -and exprgen_type thy algbr funcgr strct (TVar _) trns = - error "TVar encountered in typ during code generation" - | exprgen_type thy algbr funcgr strct (TFree vs) trns = +and exprgen_type thy algbr funcgr strct (TFree vs) trns = trns |> exprgen_tyvar_sort thy algbr funcgr strct vs |>> (fn (v, sort) => ITyVar v) @@ -190,7 +185,7 @@ exception CONSTRAIN of (string * typ) * typ; val timing = ref false; -fun exprgen_dicts thy (algbr as ((proj_sort, algebra), consts)) funcgr strct (ty_ctxt, sort_decl) trns = +fun exprgen_dicts thy (algbr as ((proj_sort, algebra), consts)) funcgr strct (ty_ctxt, sort_decl) = let val pp = Sign.pp thy; datatype typarg = @@ -209,31 +204,25 @@ val typargs = Sorts.of_sort_derivation pp algebra {classrel = classrel, constructor = constructor, variable = variable} (ty_ctxt, proj_sort sort_decl); - fun mk_dict (Global (inst, yss)) trns = - trns - |> ensure_def_inst thy algbr funcgr strct inst - ||>> (fold_map o fold_map) mk_dict yss - |>> (fn (inst, dss) => DictConst (inst, dss)) - | mk_dict (Local (classrels, (v, (k, sort)))) trns = - trns - |> fold_map (ensure_def_classrel thy algbr funcgr strct) classrels - |>> (fn classrels => DictVar (classrels, (unprefix "'" v, (k, length sort)))) + fun mk_dict (Global (inst, yss)) = + ensure_def_inst thy algbr funcgr strct inst + ##>> (fold_map o fold_map) mk_dict yss + #>> (fn (inst, dss) => DictConst (inst, dss)) + | mk_dict (Local (classrels, (v, (k, sort)))) = + fold_map (ensure_def_classrel thy algbr funcgr strct) classrels + #>> (fn classrels => DictVar (classrels, (unprefix "'" v, (k, length sort)))) in - trns - |> fold_map mk_dict typargs + fold_map mk_dict typargs end -and exprgen_dict_parms thy (algbr as (_, consts)) funcgr strct (c, ty_ctxt) trns = +and exprgen_dict_parms thy (algbr as (_, consts)) funcgr strct (c, ty_ctxt) = let val c' = CodegenConsts.norm_of_typ thy (c, ty_ctxt) val idf = CodegenNames.const thy c'; val ty_decl = Consts.the_declaration consts idf; - val insts = (op ~~ o apsnd (map (snd o dest_TVar)) oo pairself) - (curry (Consts.typargs consts) idf) (ty_ctxt, ty_decl); - val _ = if exists not (map (Sign.of_sort thy) insts) - then raise CONSTRAIN ((c, ty_decl), ty_ctxt) else (); + val (tys, tys_decl) = pairself (curry (Consts.typargs consts) idf) (ty_ctxt, ty_decl); + val sorts = map (snd o dest_TVar) tys_decl; in - trns - |> fold_map (exprgen_dicts thy algbr funcgr strct) insts + fold_map (exprgen_dicts thy algbr funcgr strct) (tys ~~ sorts) end and ensure_def_inst thy (algbr as ((_, algebra), _)) funcgr strct (class, tyco) trns = let @@ -326,8 +315,6 @@ and exprgen_term thy algbr funcgr strct (Const (c, ty)) trns = trns |> select_appgen thy algbr funcgr strct ((c, ty), []) - | exprgen_term thy algbr funcgr strct (Var _) trns = - error "Var encountered in term during code generation" | exprgen_term thy algbr funcgr strct (Free (v, ty)) trns = trns |> exprgen_type thy algbr funcgr strct ty @@ -393,9 +380,9 @@ ensure_def_const thy algbr funcgr strct c trns handle CONSTRAIN ((c, ty), ty_decl) => error ( "Constant " ^ c ^ " with most general type\n" - ^ Sign.string_of_typ thy ty + ^ CodegenConsts.string_of_typ thy ty ^ "\noccurs with type\n" - ^ Sign.string_of_typ thy ty_decl); + ^ CodegenConsts.string_of_typ thy ty_decl); fun perhaps_def_const thy algbr funcgr strct c trns = case try (ensure_def_const thy algbr funcgr strct c) trns @@ -406,9 +393,9 @@ exprgen_term thy algbr funcgr strct t trns handle CONSTRAIN ((c, ty), ty_decl) => error ("In term " ^ (quote o Sign.string_of_term thy) t ^ ",\nconstant " ^ c ^ " with most general type\n" - ^ Sign.string_of_typ thy ty + ^ CodegenConsts.string_of_typ thy ty ^ "\noccurs with type\n" - ^ Sign.string_of_typ thy ty_decl); + ^ CodegenConsts.string_of_typ thy ty_decl); (* parametrized application generators, for instantiation in object logic *) @@ -478,14 +465,13 @@ fun add_consts thy f (c1, c2 as (c, tys)) = let - val string_of_typ = setmp show_sorts true (Sign.string_of_typ thy); val _ = case tys of [TVar _] => if is_some (AxClass.class_of_param thy c) - then error ("not a function: " ^ CodegenConsts.string_of_const thy c2) + then error ("Not a function: " ^ CodegenConsts.string_of_const thy c2) else () | _ => (); val _ = if is_some (CodegenData.get_datatype_of_constr thy c2) - then error ("not a function: " ^ CodegenConsts.string_of_const thy c2) + then error ("Not a function: " ^ CodegenConsts.string_of_const thy c2) else (); val funcgr = CodegenFuncgr.make thy [c1, c2]; val ty1 = (f o CodegenFuncgr.typ funcgr) c1; @@ -493,7 +479,7 @@ val _ = if Sign.typ_equiv thy (ty1, ty2) then () else error ("Incompatiable type signatures of " ^ CodegenConsts.string_of_const thy c1 ^ " and " ^ CodegenConsts.string_of_const thy c2 ^ ":\n" - ^ string_of_typ ty1 ^ "\n" ^ string_of_typ ty2); + ^ CodegenConsts.string_of_typ thy ty1 ^ "\n" ^ CodegenConsts.string_of_typ thy ty2); in Consttab.update (c1, c2) end; fun gen_abstyp prep_const prep_typ (raw_abstyp, raw_substtyp) raw_absconsts thy = @@ -501,13 +487,13 @@ val abstyp = Type.no_tvars (prep_typ thy raw_abstyp); val substtyp = Type.no_tvars (prep_typ thy raw_substtyp); val absconsts = (map o pairself) (prep_const thy) raw_absconsts; - val Type (abstyco, tys) = abstyp handle BIND => error ("bad type: " ^ Sign.string_of_typ thy abstyp); - val typarms = map (fst o dest_TFree) tys handle MATCH => error ("bad type: " ^ Sign.string_of_typ thy abstyp); + val Type (abstyco, tys) = abstyp handle BIND => error ("Bad type: " ^ Sign.string_of_typ thy abstyp); + val typarms = map (fst o dest_TFree) tys handle MATCH => error ("Bad type: " ^ Sign.string_of_typ thy abstyp); fun mk_index v = let val k = find_index (fn w => v = w) typarms; in if k = ~1 - then error ("free type variable: " ^ quote v) + then error ("Free type variable: " ^ quote v) else TFree (string_of_int k, []) end; val typpat = map_atyps (fn TFree (v, _) => mk_index v) substtyp; @@ -668,7 +654,7 @@ fun codegen_command thy cmd = case Scan.read OuterLex.stopper (P.!!! code_bareP) ((filter OuterLex.is_proper o OuterSyntax.scan) cmd) of SOME f => (writeln "Now generating code..."; f thy) - | NONE => error ("bad directive " ^ quote cmd); + | NONE => error ("Bad directive " ^ quote cmd); val code_abstypeP = OuterSyntax.command code_abstypeK "axiomatic abstypes for code generation" K.thy_decl ( diff -r 680b04dbd51c -r 461130ccfef4 src/Pure/Tools/codegen_serializer.ML --- a/src/Pure/Tools/codegen_serializer.ML Fri Jan 26 13:59:03 2007 +0100 +++ b/src/Pure/Tools/codegen_serializer.ML Fri Jan 26 13:59:04 2007 +0100 @@ -148,7 +148,7 @@ fun parse_args f args = case Scan.read Args.stopper f args of SOME x => x - | NONE => error "bad serializer arguments"; + | NONE => error "Bad serializer arguments"; (* generic serializer combinators *) @@ -249,7 +249,7 @@ let fun pretty (pr : CodegenNames.var_ctxt -> fixity -> iterm -> Pretty.T) vars fxy [t1, (v, ty) `|-> t2] = pr vars fxy (ICase ((t1, ty), ([(IVar v, t2)]))) - | pretty _ _ _ _ = error "bad arguments for imperative monad bind"; + | pretty _ _ _ _ = error "Bad arguments for imperative monad bind"; in (2, pretty) end; @@ -1007,8 +1007,10 @@ |> fold (fn m => fn g => case Graph.get_node g m of Module (_, (_, g)) => g) modl' |> (fn g => case Graph.get_node g name of Def (defname, _) => defname); - in NameSpace.implode (remainder @ [defname']) end handle Graph.UNDEF _ => - "(raise Fail \"undefined name " ^ name ^ "\")"; + in + NameSpace.implode (remainder @ [defname']) + end handle Graph.UNDEF _ => + error "Unknown name: " ^ quote name; fun the_prolog modlname = case module_prolog modlname of NONE => [] | SOME p => [p, str ""]; @@ -1028,7 +1030,7 @@ let fun output_file file = File.write (Path.explode file) o code_output; val output_diag = writeln o code_output; - val output_internal = use_text "" Output.ml_output false o code_output; + val output_internal = use_text "generated code" Output.ml_output false o code_output; in parse_args ((Args.$$$ "-" >> K output_diag || Args.$$$ "#" >> K output_internal @@ -1596,7 +1598,7 @@ fun eval p = ( reff := NONE; if !eval_verbose then Pretty.writeln p else (); - use_text "" Output.ml_output (!eval_verbose) + use_text "generated code for evaluation" Output.ml_output (!eval_verbose) ((Pretty.output o Pretty.chunks) [p, str ("val _ = (" ^ ref_name ^ " := SOME " ^ val_name' ^ ")") ]);