--- 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
--- 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;
--- 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;
--- 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;
--- 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 (
--- 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' ^ ")")
]);