--- a/src/Pure/Tools/codegen_package.ML Wed Jun 07 16:53:31 2006 +0200
+++ b/src/Pure/Tools/codegen_package.ML Wed Jun 07 16:54:30 2006 +0200
@@ -15,14 +15,6 @@
val add_appconst: xstring * ((int * int) * appgen) -> theory -> theory;
val add_appconst_i: string * ((int * int) * appgen) -> theory -> theory;
- val add_prim_class: xstring -> (string * string)
- -> theory -> theory;
- val add_prim_tyco: xstring -> (string * string)
- -> theory -> theory;
- val add_prim_const: xstring -> (string * string)
- -> theory -> theory;
- val add_prim_i: string -> (string * CodegenThingol.prim list)
- -> theory -> theory;
val add_pretty_list: string -> string -> string * (int * string)
-> theory -> theory;
val add_alias: string * string -> theory -> theory;
@@ -59,7 +51,7 @@
structure ConstNameMangler: NAME_MANGLER;
structure DatatypeconsNameMangler: NAME_MANGLER;
structure CodegenData: THEORY_DATA;
- val mk_tabs: theory -> auxtab;
+ val mk_tabs: theory -> string option -> auxtab;
val alias_get: theory -> string -> string;
val idf_of_name: theory -> string -> string -> string;
val idf_of_const: theory -> auxtab -> string * typ -> string;
@@ -208,7 +200,7 @@
fun re_mangle _ dst = error ("no such datatype constructor: " ^ quote dst);
);
-type auxtab = deftab
+type auxtab = (string option * deftab)
* (InstNameMangler.T * (typ list Symtab.table * ConstNameMangler.T)
* DatatypeconsNameMangler.T);
type eqextr = theory -> auxtab
@@ -497,7 +489,7 @@
let
val (vars, cos) = (fst o the o CodegenTheorems.get_datatypes thy) dtco
in
- SOME (c, (the o AList.lookup (op =) cos) c ---> Type (dtco, map TFree vars))
+ SOME (c, (the o AList.lookup (op =) cos) c ---> Type (dtco, map TFree vars) |> Logic.varifyT)
end
| NONE => NONE;
@@ -516,6 +508,17 @@
(* definition and expression generators *)
+fun check_strict thy f x (tabs as ((SOME target, deftab), tabs')) =
+ thy
+ |> CodegenData.get
+ |> #target_data
+ |> (fn data => (the oo Symtab.lookup) data target)
+ |> f
+ |> (fn tab => Symtab.lookup tab x)
+ |> is_none
+ | check_strict _ _ _ (tabs as ((NONE, _), _)) =
+ false;
+
fun ensure_def_class thy tabs cls trns =
let
fun defgen_class thy (tabs as (_, (insttab, _, _))) cls trns =
@@ -529,7 +532,7 @@
trns
|> debug_msg (fn _ => "trying defgen class declaration for " ^ quote cls)
|> fold_map (ensure_def_class thy tabs) (ClassPackage.the_superclasses thy cls)
- ||>> (exprsgen_type thy tabs o map snd) cs
+ ||>> (fold_map (exprgen_type thy tabs) o map snd) cs
||>> (fold_map o fold_map) (exprgen_tyvar_sort thy tabs) sortctxts
|-> (fn ((supcls, memtypes), sortctxts) => succeed
(Class (supcls, (unprefix "'" v, idfs ~~ (sortctxts ~~ memtypes)))))
@@ -541,22 +544,24 @@
in
trns
|> debug_msg (fn _ => "generating class " ^ quote cls)
- |> ensure_def [("class", defgen_class thy tabs)] ("generating class " ^ quote cls) cls'
+ |> ensure_def (defgen_class thy tabs) true ("generating class " ^ quote cls) cls'
|> pair cls'
end
and ensure_def_tyco thy tabs tyco trns =
let
+ val tyco' = idf_of_name thy nsp_tyco tyco;
+ val strict = check_strict thy #syntax_tyco tyco' tabs;
fun defgen_datatype thy (tabs as (_, (_, _, dtcontab))) dtco trns =
case name_of_idf thy nsp_tyco dtco
of SOME dtco =>
- (case CodegenTheorems.get_datatypes thy dtco
+ (case CodegenTheorems.get_datatypes thy dtco
of SOME ((vars, cos), _) =>
trns
|> debug_msg (fn _ => "trying defgen datatype for " ^ quote dtco)
|> fold_map (exprgen_tyvar_sort thy tabs) vars
- ||>> fold_map (fn (c, ty) =>
- exprsgen_type thy tabs ty
- #-> (fn ty' => pair ((the o idf_of_co thy tabs) (c, dtco), ty'))) cos
+ ||>> fold_map (fn (c, tys) =>
+ fold_map (exprgen_type thy tabs) tys
+ #-> (fn tys' => pair ((the o idf_of_co thy tabs) (c, dtco), tys'))) cos
|-> (fn (vars, cos) => succeed (Datatype
(vars, cos)))
| NONE =>
@@ -565,11 +570,10 @@
| NONE =>
trns
|> fail ("not a type constructor: " ^ quote dtco)
- val tyco' = idf_of_name thy nsp_tyco tyco;
in
trns
|> debug_msg (fn _ => "generating type constructor " ^ quote tyco)
- |> ensure_def [("datatype", defgen_datatype thy tabs)] ("generating type constructor " ^ quote tyco) tyco'
+ |> ensure_def (defgen_datatype thy tabs) strict ("generating type constructor " ^ quote tyco) tyco'
|> pair tyco'
end
and exprgen_tyvar_sort thy tabs (v, sort) trns =
@@ -591,9 +595,7 @@
trns
|> ensure_def_tyco thy tabs tyco
||>> fold_map (exprgen_type thy tabs) tys
- |-> (fn (tyco, tys) => pair (tyco `%% tys))
-and exprsgen_type thy tabs =
- fold_map (exprgen_type thy tabs);
+ |-> (fn (tyco, tys) => pair (tyco `%% tys));
fun exprgen_classlookup thy tabs (ClassPackage.Instance (inst, ls)) trns =
trns
@@ -620,12 +622,16 @@
^ ", actually defining " ^ quote c')
| _ => error ("illegal function equation for " ^ quote c)
end;
+ fun exprgen_eq (args, rhs) trns =
+ trns
+ |> fold_map (exprgen_term thy tabs) args
+ ||>> exprgen_term thy tabs rhs
in
trns
- |> (exprsgen_eqs thy tabs o map dest_eqthm) eq_thms
- ||>> exprsgen_type thy tabs [ty]
+ |> fold_map (exprgen_eq o dest_eqthm) eq_thms
+ ||>> exprgen_type thy tabs ty
||>> fold_map (exprgen_tyvar_sort thy tabs) sortctxt
- |-> (fn ((eqs, [ity]), sortctxt) => (pair o SOME) ((eqs, (sortctxt, ity)), ty))
+ |-> (fn ((eqs, ity), sortctxt) => (pair o SOME) ((eqs, (sortctxt, ity)), ty))
end
| NONE => (NONE, trns)
and ensure_def_inst thy (tabs as (_, (insttab, _, _))) (cls, tyco) trns =
@@ -670,7 +676,7 @@
in
trns
|> debug_msg (fn _ => "generating instance " ^ quote cls ^ " / " ^ quote tyco)
- |> ensure_def [("instance", defgen_inst thy tabs)]
+ |> ensure_def (defgen_inst thy tabs) true
("generating instance " ^ quote cls ^ " / " ^ quote tyco) inst
|> pair inst
end
@@ -682,7 +688,8 @@
trns
|> mk_fun thy tabs (c, ty)
|-> (fn SOME (funn, _) => succeed (Fun funn)
- | NONE => fail ("no defining equations found for " ^ quote c))
+ | NONE => fail ("no defining equations found for " ^
+ (quote o Display.raw_string_of_term o Const) (c, ty)))
| NONE =>
trns
|> fail ("not a constant: " ^ quote c);
@@ -692,7 +699,7 @@
trns
|> debug_msg (fn _ => "trying defgen class member for " ^ quote m)
|> ensure_def_class thy tabs ((the o ClassPackage.lookup_const_class thy) m)
- |-> (fn cls => succeed Undef)
+ |-> (fn cls => succeed Bot)
| _ =>
trns |> fail ("no class member found for " ^ quote m)
fun defgen_datatypecons thy (tabs as (_, (_, _, dtcontab))) co trns =
@@ -701,24 +708,25 @@
trns
|> debug_msg (fn _ => "trying defgen datatype constructor for " ^ quote co)
|> ensure_def_tyco thy tabs dtco
- |-> (fn dtco => succeed Undef)
+ |-> (fn dtco => succeed Bot)
| _ =>
trns
|> fail ("not a datatype constructor: " ^ quote co);
- fun get_defgen idf =
+ fun get_defgen tabs idf strict =
if (is_some oo name_of_idf thy) nsp_const idf
orelse (is_some oo name_of_idf thy) nsp_overl idf
- then ("funs", defgen_funs thy tabs)
+ then defgen_funs thy tabs strict
else if (is_some oo name_of_idf thy) nsp_mem idf
- then ("clsmem", defgen_clsmem thy tabs)
+ then defgen_clsmem thy tabs strict
else if (is_some oo name_of_idf thy) nsp_dtcon idf
- then ("datatypecons", defgen_datatypecons thy tabs)
+ then defgen_datatypecons thy tabs strict
else error ("illegal shallow name space for constant: " ^ quote idf);
val idf = idf_of_const thy tabs (c, ty);
+ val strict = check_strict thy #syntax_const idf tabs;
in
trns
- |> debug_msg (fn _ => "generating constant " ^ quote c)
- |> ensure_def ((single o get_defgen) idf) ("generating constant " ^ quote c) idf
+ |> debug_msg (fn _ => "generating constant " ^ (quote o Display.raw_string_of_term o Const) (c, ty))
+ |> ensure_def (get_defgen tabs idf) strict ("generating constant " ^ quote c) idf
|> pair idf
end
and exprgen_term thy tabs (Const (f, ty)) trns =
@@ -754,20 +762,14 @@
||>> fold_map (exprgen_term thy tabs) ts
|-> (fn (e, es) => pair (e `$$ es))
end
-and exprsgen_term thy tabs =
- fold_map (exprgen_term thy tabs)
-and exprsgen_eqs thy tabs =
- apfst (map (fn (rhs::args) => (args, rhs)))
- oo fold_burrow (exprsgen_term thy tabs)
- o map (fn (args, rhs) => (rhs :: args))
and appgen_default thy tabs ((c, ty), ts) trns =
trns
|> ensure_def_const thy tabs (c, ty)
- ||>> exprsgen_type thy tabs [ty]
+ ||>> exprgen_type thy tabs ty
||>> (fold_map o fold_map) (exprgen_classlookup thy tabs)
(ClassPackage.extract_classlookup thy (c, ty))
||>> fold_map (exprgen_term thy tabs) ts
- |-> (fn (((c, [ty]), ls), es) =>
+ |-> (fn (((c, ty), ls), es) =>
pair (IConst (c, (ls, ty)) `$$ es))
and appgen thy tabs ((f, ty), ts) trns =
case Symtab.lookup ((#appconst o #gens o CodegenData.get) thy) f
@@ -854,14 +856,14 @@
val idf = idf_of_const thy tabs (c, ty);
in
trns
- |> ensure_def [("wfrec", (K o succeed) Undef)] ("generating wfrec") idf
+ |> ensure_def ((K o succeed) Bot) true ("generating wfrec") idf
|> exprgen_type thy tabs ty'
||>> (fold_map o fold_map) (exprgen_classlookup thy tabs)
(ClassPackage.extract_classlookup thy (c, ty))
- ||>> exprsgen_type thy tabs [ty_def]
+ ||>> exprgen_type thy tabs ty_def
||>> exprgen_term thy tabs tf
||>> exprgen_term thy tabs tx
- |-> (fn ((((_, ls), [ty]), tf), tx) => pair (IConst (idf, (ls, ty)) `$ tf `$ tx))
+ |-> (fn ((((_, ls), ty), tf), tx) => pair (IConst (idf, (ls, ty)) `$ tf `$ tx))
end;
fun appgen_datatype_case cos thy tabs (app as ((_, ty), ts)) trns =
@@ -904,7 +906,7 @@
(** theory interface **)
-fun mk_tabs thy =
+fun mk_tabs thy target =
let
fun mk_insttab thy =
InstNameMangler.empty
@@ -968,7 +970,7 @@
val insttab = mk_insttab thy;
val overltabs = mk_overltabs thy;
val dtcontab = mk_dtcontab thy;
- in (Symtab.empty, (insttab, overltabs, dtcontab)) end;
+ in ((target, Symtab.empty), (insttab, overltabs, dtcontab)) end;
fun get_serializer target =
case Symtab.lookup (!serializers) target
@@ -983,7 +985,7 @@
map_module (K CodegenThingol.empty_module) thy
| delete_defs (SOME c) thy =
let
- val tabs = mk_tabs thy;
+ val tabs = mk_tabs thy NONE;
in
map_module (CodegenThingol.purge_module []) thy
end;
@@ -993,12 +995,12 @@
* precondition: improved representation of definitions hidden by customary serializations
*)
-fun expand_module init gen arg thy =
+fun expand_module target init gen arg thy =
thy
|> CodegenTheorems.notify_dirty
|> `(#modl o CodegenData.get)
|> (fn (modl, thy) =>
- (start_transact init (gen thy (mk_tabs thy) arg) modl, thy))
+ (start_transact init (gen thy (mk_tabs thy target) arg) modl, thy))
|-> (fn (x, modl) => map_module (K modl) #> pair x);
fun rename_inconsistent thy =
@@ -1025,18 +1027,16 @@
else add_alias (src, dst) thy
in fold add inconsistent thy end;
-fun codegen_term t thy =
- thy
- |> expand_module NONE exprsgen_term [CodegenTheorems.preprocess_term thy t]
- |-> (fn [t] => pair t);
+fun codegen_term t =
+ expand_module NONE NONE exprgen_term t;
val is_dtcon = has_nsp nsp_dtcon;
fun consts_of_idfs thy =
- map (the o const_of_idf thy (mk_tabs thy));
+ map (the o const_of_idf thy (mk_tabs thy NONE));
fun idfs_of_consts thy =
- map (idf_of_const thy (mk_tabs thy));
+ map (idf_of_const thy (mk_tabs thy NONE));
val get_root_module = (#modl o CodegenData.get);
@@ -1054,7 +1054,9 @@
(** target languages **)
-(* primitive definitions *)
+val ensure_bot = map_module o CodegenThingol.ensure_bot;
+
+(* syntax *)
fun read_typ thy =
Sign.read_typ (thy, K NONE);
@@ -1069,38 +1071,10 @@
fun read_quote get reader gen raw thy =
thy
- |> expand_module ((SOME o get) thy)
+ |> expand_module NONE ((SOME o get) thy)
(fn thy => fn tabs => gen thy tabs o single o reader thy) raw
|-> (fn [x] => pair x);
-fun gen_add_prim prep_name prep_primdef raw_name (target, raw_primdef) thy =
- let
- val _ = if Symtab.defined ((#target_data o CodegenData.get) thy) target
- then () else error ("unknown target language: " ^ quote target);
- val tabs = mk_tabs thy;
- val name = prep_name thy tabs raw_name;
- val primdef = prep_primdef raw_primdef;
- in
- thy
- |> map_module (CodegenThingol.add_prim name (target, primdef))
- end;
-
-val add_prim_i = gen_add_prim ((K o K) I) I;
-val add_prim_class = gen_add_prim
- (fn thy => K (idf_of_name thy nsp_class o Sign.intern_class thy))
- CodegenSerializer.parse_targetdef;
-val add_prim_tyco = gen_add_prim
- (fn thy => K (idf_of_name thy nsp_tyco o Sign.intern_type thy))
- CodegenSerializer.parse_targetdef;
-val add_prim_const = gen_add_prim
- (fn thy => fn tabs => idf_of_const thy tabs o read_const thy)
- CodegenSerializer.parse_targetdef;
-
-val ensure_prim = map_module oo CodegenThingol.ensure_prim;
-
-
-(* syntax *)
-
fun gen_add_syntax_class prep_class class target pretty thy =
thy
|> map_codegen_data
@@ -1136,7 +1110,7 @@
val tyco = prep_tyco thy raw_tyco;
in
thy
- |> ensure_prim tyco target
+ |> ensure_bot tyco
|> reader
|-> (fn pretty => map_codegen_data
(fn (modl, gens, target_data, logic_data) =>
@@ -1151,7 +1125,8 @@
end;
in
CodegenSerializer.parse_syntax (fn thy => no_args_tyco thy raw_tyco)
- (read_quote (fn thy => prep_tyco thy raw_tyco) read_typ exprsgen_type)
+ (read_quote (fn thy => prep_tyco thy raw_tyco) read_typ
+ (fn thy => fn tabs => fold_map (exprgen_type thy tabs)))
#-> (fn reader => pair (mk reader))
end;
@@ -1171,7 +1146,7 @@
fun parse_syntax_const raw_const =
let
fun prep_const thy raw_const =
- idf_of_const thy (mk_tabs thy) (read_const thy raw_const);
+ idf_of_const thy (mk_tabs thy NONE) (read_const thy raw_const);
fun no_args_const thy raw_const =
(length o fst o strip_type o snd o read_const thy) raw_const;
fun mk reader target thy =
@@ -1180,20 +1155,21 @@
val c = prep_const thy raw_const;
in
thy
- |> ensure_prim c target
+ |> ensure_bot c
|> reader
|-> (fn pretty => add_pretty_syntax_const c target pretty)
end;
in
CodegenSerializer.parse_syntax (fn thy => no_args_const thy raw_const)
- (read_quote (fn thy => prep_const thy raw_const) Sign.read_term exprsgen_term)
+ (read_quote (fn thy => prep_const thy raw_const) Sign.read_term
+ (fn thy => fn tabs => fold_map (exprgen_term thy tabs)))
#-> (fn reader => pair (mk reader))
end;
fun add_pretty_list raw_nil raw_cons (target, seri) thy =
let
val _ = get_serializer target;
- val tabs = mk_tabs thy;
+ val tabs = mk_tabs thy NONE;
fun mk_const raw_name =
let
val name = Sign.intern_const thy raw_name;
@@ -1203,7 +1179,6 @@
val pr' = CodegenSerializer.pretty_list nil' cons' seri;
in
thy
- |> ensure_prim cons' target
|> add_pretty_syntax_const cons' target pr'
end;
@@ -1213,15 +1188,16 @@
local
-fun generate_code (SOME raw_consts) thy =
- let
+fun generate_code target (SOME raw_consts) thy =
+ let
val consts = map (read_const thy) raw_consts;
+ val _ = case target of SOME target => (get_serializer target; ()) | _ => ();
in
thy
- |> expand_module NONE (fold_map oo ensure_def_const) consts
+ |> expand_module target NONE (fold_map oo ensure_def_const) consts
|-> (fn cs => pair (SOME cs))
end
- | generate_code NONE thy =
+ | generate_code _ NONE thy =
(NONE, thy);
fun serialize_code target seri raw_consts thy =
@@ -1241,7 +1217,7 @@
) cs module : unit; thy) end;
in
thy
- |> generate_code raw_consts
+ |> generate_code (SOME target) raw_consts
|-> (fn cs => serialize cs)
end;
@@ -1266,9 +1242,10 @@
val generateP =
OuterSyntax.command generateK "generate executable code for constants" K.thy_decl (
- Scan.repeat1 P.term
- >> (fn raw_consts =>
- Toplevel.theory (generate_code (SOME raw_consts) #> snd))
+ Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")")
+ -- Scan.repeat1 P.term
+ >> (fn (target, raw_consts) =>
+ Toplevel.theory (generate_code target (SOME raw_consts) #> snd))
);
val serializeP =
@@ -1284,30 +1261,6 @@
))
);
-val primclassP =
- OuterSyntax.command primclassK "define target-language specific class" K.thy_decl (
- P.xname
- -- Scan.repeat1 (P.name -- P.text)
- >> (fn (raw_class, primdefs) =>
- (Toplevel.theory oo fold) (add_prim_class raw_class) primdefs)
- );
-
-val primtycoP =
- OuterSyntax.command primtycoK "define target-language specific type constructor" K.thy_decl (
- P.xname
- -- Scan.repeat1 (P.name -- P.text)
- >> (fn (raw_tyco, primdefs) =>
- (Toplevel.theory oo fold) (add_prim_tyco raw_tyco) primdefs)
- );
-
-val primconstP =
- OuterSyntax.command primconstK "define target-language specific constant" K.thy_decl (
- P.term
- -- Scan.repeat1 (P.name -- P.text)
- >> (fn (raw_const, primdefs) =>
- (Toplevel.theory oo fold) (add_prim_const raw_const) primdefs)
- );
-
val syntax_classP =
OuterSyntax.command syntax_tycoK "define code syntax for class" K.thy_decl (
Scan.repeat1 (
@@ -1356,8 +1309,7 @@
>> (Toplevel.theory oo fold) add_alias
);
-val _ = OuterSyntax.add_parsers [generateP, serializeP,
- primclassP, primtycoP, primconstP, syntax_tycoP, syntax_constP,
+val _ = OuterSyntax.add_parsers [generateP, serializeP, syntax_tycoP, syntax_constP,
purgeP, aliasP];
end; (* local *)
--- a/src/Pure/Tools/codegen_serializer.ML Wed Jun 07 16:53:31 2006 +0200
+++ b/src/Pure/Tools/codegen_serializer.ML Wed Jun 07 16:54:30 2006 +0200
@@ -20,7 +20,6 @@
* OuterParse.token list;
val parse_syntax: ('b -> int) -> (string -> 'b -> 'a * 'b) -> OuterParse.token list ->
('b -> 'a pretty_syntax * 'b) * OuterParse.token list;
- val parse_targetdef: string -> CodegenThingol.prim list;
val pretty_list: string -> string -> int * string -> CodegenThingol.iexpr pretty_syntax;
val serializers: {
ml: string * (string * string * (string -> bool) -> serializer),
@@ -191,26 +190,6 @@
)
end;
-fun newline_correct s =
- s
- |> Symbol.strip_blanks
- |> space_explode "\n"
- |> map (implode o (fn [] => []
- | (" "::xs) => xs
- | xs => xs) o explode)
- |> space_implode "\n";
-
-fun parse_targetdef s =
- case Scan.finite Symbol.stopper (Scan.repeat (
- ($$ "`" |-- $$ "`" >> (CodegenThingol.Pretty o str))
- || ($$ "`" |-- Scan.repeat1 (Scan.unless ($$ "`") (Scan.one Symbol.not_eof))
- --| $$ "`" >> (fn ["_"] => CodegenThingol.Name | s => error ("malformed antiquote: " ^ implode s)))
- || Scan.repeat1
- (Scan.unless ($$ "`") (Scan.one Symbol.not_eof)) >> (CodegenThingol.Pretty o str o implode)
- )) ((Symbol.explode o Symbol.strip_blanks) s)
- of (p, []) => p
- | (p, ss) => error ("Malformed definition: " ^ quote s ^ " - " ^ commas ss);
-
(* generic abstract serializer *)
@@ -228,16 +207,6 @@
postprocess (class_syntax, tyco_syntax, const_syntax)
select module =
let
- fun pretty_of_prim resolv (name, primdef) =
- let
- fun pr (CodegenThingol.Pretty p) = p
- | pr CodegenThingol.Name = (str o resolv) name;
- in case AList.lookup (op = : string * string -> bool) primdef target
- of NONE => error ("no primitive definition for " ^ quote name)
- | SOME ps => (case map pr ps
- of [] => NONE
- | ps => (SOME o Pretty.block) ps)
- end;
fun from_module' resolv imps ((name_qual, name), defs) =
from_module resolv imps ((name_qual, name), defs)
|> postprocess (resolv name_qual);
@@ -246,7 +215,7 @@
|> debug_msg (fn _ => "selecting submodule...")
|> (if is_some select then (CodegenThingol.project_module o the) select else I)
|> debug_msg (fn _ => "serializing...")
- |> CodegenThingol.serialize (from_defs (pretty_of_prim, (class_syntax : string -> string option, tyco_syntax, const_syntax)))
+ |> CodegenThingol.serialize (from_defs (class_syntax : string -> string option, tyco_syntax, const_syntax))
from_module' validator postproc nspgrp name_root
|> K ()
end;
@@ -660,7 +629,7 @@
in (ml_from_funs, ml_from_datatypes) end;
fun ml_from_defs (is_cons, needs_type)
- (from_prim, (_, tyco_syntax, const_syntax)) resolver prefix defs =
+ (_, tyco_syntax, const_syntax) resolver prefix defs =
let
val resolv = resolver prefix;
val (ml_from_label, ml_from_tyvar, ml_from_sortlookup, ml_from_tycoexpr, ml_from_type, typify, ml_from_expr) =
@@ -721,11 +690,7 @@
]
:: map from_membr_fun membrs)
end
- fun ml_from_def (name, CodegenThingol.Undef) =
- error ("empty definition during serialization: " ^ quote name)
- | ml_from_def (name, CodegenThingol.Prim prim) =
- from_prim resolv (name, prim)
- | ml_from_def (name, CodegenThingol.Typesyn (vs, ty)) =
+ fun ml_from_def (name, CodegenThingol.Typesyn (vs, ty)) =
(map (fn (vname, []) => () | _ =>
error "can't serialize sort constrained type declaration to ML") vs;
Pretty.block [
@@ -867,7 +832,7 @@
local
-fun hs_from_defs with_typs (from_prim, (class_syntax, tyco_syntax, const_syntax))
+fun hs_from_defs with_typs (class_syntax, tyco_syntax, const_syntax)
resolver prefix defs =
let
val resolv = resolver "";
@@ -1002,11 +967,7 @@
hs_from_expr NOBR rhs
]
in Pretty.chunks ((map from_eq o fst o snd o constructive_fun) def) end;
- fun hs_from_def (name, CodegenThingol.Undef) =
- error ("empty statement during serialization: " ^ quote name)
- | hs_from_def (name, CodegenThingol.Prim prim) =
- from_prim resolv_here (name, prim)
- | hs_from_def (name, CodegenThingol.Fun (def as (_, (sctxt, ty)))) =
+ fun hs_from_def (name, CodegenThingol.Fun (def as (_, (sctxt, ty)))) =
let
val body = hs_from_funeqs (name, def);
in if with_typs then
@@ -1038,6 +999,7 @@
(Pretty.block o Pretty.breaks) [
str "data",
hs_from_sctxt_tycoexpr (sctxt, (resolv_here name, map (ITyVar o fst) sctxt)),
+ str "=",
Pretty.block (separate (Pretty.block [Pretty.brk 1, str "| "]) (map mk_cons constrs))
]
end |> SOME
--- a/src/Pure/Tools/codegen_theorems.ML Wed Jun 07 16:53:31 2006 +0200
+++ b/src/Pure/Tools/codegen_theorems.ML Wed Jun 07 16:54:30 2006 +0200
@@ -23,7 +23,6 @@
val proper_name: string -> string;
val common_typ: theory -> (thm -> typ) -> thm list -> thm list;
val preprocess: theory -> thm list -> (typ * thm list) option;
- val preprocess_term: theory -> term -> term;
val get_funs: theory -> string * typ -> (typ * thm list) option;
val get_datatypes: theory -> string
@@ -579,7 +578,7 @@
fun tap_typ thy [] = NONE
| tap_typ thy (thms as (thm::_)) = SOME (extr_typ thy thm, thms);
-fun preprocess' thy extr_ty thms =
+fun preprocess thy thms =
let
fun burrow_thms f [] = []
| burrow_thms f thms =
@@ -587,19 +586,27 @@
|> Conjunction.intr_list
|> f
|> Conjunction.elim_list;
+ fun rewrite_rhs conv thm = (case (Drule.strip_comb o cprop_of) thm
+ of (ct', [ct1, ct2]) => (case term_of ct'
+ of Const ("==", _) =>
+ Thm.equal_elim (combination (combination (reflexive ct') (reflexive ct1)) (conv ct2)) thm
+ | _ => raise ERROR "rewrite_rhs")
+ | _ => raise ERROR "rewrite_rhs");
+ val unfold_thms = Tactic.rewrite true (map (make_eq thy) (the_unfolds thy));
in
thms
|> map (make_eq thy)
|> map (Thm.transfer thy)
|> fold (fn f => f thy) (the_preprocs thy)
- |> map (rewrite_rule (map (make_eq thy) (the_unfolds thy)))
+ |> map (rewrite_rhs unfold_thms)
|> debug_msg (fn _ => "[cg_thm] filter")
|> debug_msg (commas o map string_of_thm)
- |> debug_msg (fn _ => "[cg_thm] extr_typ")
+ |> debug_msg (fn _ => "[cg_thm] common_typ")
|> debug_msg (commas o map string_of_thm)
- |> debug_msg (fn _ => "[cg_thm] common_typ / abs_norm")
+ |> common_typ thy (extr_typ thy)
+ |> debug_msg (fn _ => "[cg_thm] abs_norm")
|> debug_msg (commas o map string_of_thm)
- |> (if extr_ty then common_typ thy (extr_typ thy) #> map (abs_norm thy) else I)
+ |> map (abs_norm thy)
|> burrow_thms (
debug_msg (fn _ => "[cg_thm] canonical tvars")
#> debug_msg (string_of_thm)
@@ -613,27 +620,7 @@
)
|> map Drule.unvarifyT
|> map Drule.unvarify
- end;
-
-fun preprocess thy = preprocess' thy true #> tap_typ thy;
-
-fun preprocess_term thy raw_t =
- let
- val t = Logic.legacy_varify raw_t;
- val x = variant (add_term_names (t, [])) "a";
- val t_eq = Logic.mk_equals (Free (x, fastype_of t), t);
- (*fake definition*)
- val thm_eq = setmp quick_and_dirty true (SkipProof.make_thm thy)
- t_eq;
- fun err ts' = error ("preprocess_term: bad preprocessor; started with "
- ^ (quote o Sign.string_of_term thy) t_eq ^ ", ended up with "
- ^ (quote o commas o map (Sign.string_of_term thy)) ts'
- )
- in case preprocess' thy false [thm_eq]
- of [thm] => (case Drule.plain_prop_of thm
- of t_res as (Const ("==", _) $ Free (x', _) $ t') => if x = x' then t' else err [t_res]
- | t_res => err [t_res])
- | thms => (err o map Drule.plain_prop_of) thms
+ |> tap_typ thy
end;
@@ -709,8 +696,11 @@
fun get_eq thy (c, ty) =
if is_obj_eq thy c
- then case get_datatypes thy ((fst o dest_Type o hd o fst o strip_type) ty)
- of SOME (_, thms) => thms
+ then case strip_type ty
+ of (Type (tyco, _) :: _, _) =>
+ (case get_datatypes thy tyco
+ of SOME (_, thms) => thms
+ | _ => [])
| _ => []
else [];
--- a/src/Pure/Tools/codegen_thingol.ML Wed Jun 07 16:53:31 2006 +0200
+++ b/src/Pure/Tools/codegen_thingol.ML Wed Jun 07 16:54:30 2006 +0200
@@ -62,16 +62,11 @@
val resolve_tycos: (string -> string) -> itype * iexpr list -> itype * iexpr list;
val resolve_consts: (string -> string) -> iexpr -> iexpr;
val eta_expand: (string * (iclasslookup list list * itype)) * iexpr list -> int -> iexpr;
-
type funn = (iexpr list * iexpr) list * (sortcontext * itype);
type datatyp = sortcontext * (string * itype list) list;
- datatype prim =
- Pretty of Pretty.T
- | Name;
datatype def =
- Undef
- | Prim of (string * prim list) list
+ Bot
| Fun of funn
| Typesyn of (vname * sort) list * itype
| Datatype of datatyp
@@ -90,16 +85,15 @@
val pretty_deps: module -> Pretty.T;
val empty_module: module;
val get_def: module -> string -> def;
- val add_prim: string -> (string * prim list) -> module -> module;
- val ensure_prim: string -> string -> module -> module;
val merge_module: module * module -> module;
val diff_module: module * module -> (string * def) list;
val project_module: string list -> module -> module;
val purge_module: string list -> module -> module;
val has_nsp: string -> string -> bool;
+ val ensure_bot: string -> module -> module;
val succeed: 'a -> transact -> 'a transact_fin;
val fail: string -> transact -> 'a transact_fin;
- val ensure_def: (string * (string -> transact -> def transact_fin)) list -> string
+ val ensure_def: (string -> transact -> def transact_fin) -> bool -> string
-> string -> transact -> transact;
val start_transact: string option -> (transact -> 'a * transact) -> module -> 'a * module;
@@ -394,13 +388,8 @@
type funn = (iexpr list * iexpr) list * (sortcontext * itype);
type datatyp = sortcontext * (string * itype list) list;
-datatype prim =
- Pretty of Pretty.T
- | Name;
-
datatype def =
- Undef
- | Prim of (string * prim list) list
+ Bot
| Fun of funn
| Typesyn of (vname * sort) list * itype
| Datatype of datatyp
@@ -415,18 +404,15 @@
datatype node = Def of def | Module of node Graph.T;
type module = node Graph.T;
type transact = Graph.key option * module;
-datatype 'dst transact_res = Succeed of 'dst | Fail of string list * exn option;
-type 'dst transact_fin = 'dst transact_res * module;
+type 'dst transact_fin = 'dst * module;
exception FAIL of string list * exn option;
val eq_def = (op =) : def * def -> bool;
(* simple diagnosis *)
-fun pretty_def Undef =
- Pretty.str "<UNDEF>"
- | pretty_def (Prim prims) =
- Pretty.str ("<PRIM " ^ (commas o map fst) prims ^ ">")
+fun pretty_def Bot =
+ Pretty.str "<Bot>"
| pretty_def (Fun (eqs, (sortctxt, ty))) =
Pretty.enum " |" "" "" (
map (fn (ps, body) =>
@@ -565,6 +551,12 @@
get (Graph.get_node node m) ms
in get (Module modl) modlname end;
+fun is_def modl name =
+ case try (get_def modl) name
+ of NONE => false
+ | SOME Bot => false
+ | _ => true;
+
fun add_def (name, def) =
let
val (modl, base) = dest_name name;
@@ -575,6 +567,46 @@
#> Graph.map_node m (Module o add ms o dest_modl)
in add modl end;
+fun map_def name f =
+ let
+ val (modl, base) = dest_name name;
+ fun mapp [] =
+ Graph.map_node base (Def o f o dest_def)
+ | mapp (m::ms) =
+ Graph.map_node m (Module o mapp ms o dest_modl)
+ in mapp modl end;
+
+fun ensure_bot name =
+ let
+ val (modl, base) = dest_name name;
+ fun ensure [] module =
+ (case try (Graph.get_node module) base
+ of NONE =>
+ module
+ |> Graph.new_node (base, Def Bot)
+ | SOME (Module _) => error ("module already present: " ^ quote name)
+ | _ => module)
+ | ensure (m::ms) module =
+ module
+ |> Graph.default_node (m, Module empty_module)
+ |> Graph.map_node m (Module o ensure ms o dest_modl)
+ in ensure modl end;
+
+fun add_def_incr strict (name, Bot) module =
+ (case try (get_def module) name
+ of NONE => if strict then error "attempted to add Bot to module"
+ else map_def name (K Bot) module
+ | SOME Bot => if strict then error "attempted to add Bot to module"
+ else map_def name (K Bot) module
+ | SOME _ => module)
+ | add_def_incr _ (name, def) module =
+ (case try (get_def module) name
+ of NONE => add_def (name, def) module
+ | SOME Bot => map_def name (K def) module
+ | SOME def' => if eq_def (def, def')
+ then module
+ else error ("tried to overwrite definition " ^ quote name));
+
fun add_dep (name1, name2) modl =
if name1 = name2 then modl
else
@@ -597,90 +629,6 @@
|> Graph.map_node m (Module o add ms o dest_modl);
in add ms modl end;
-fun map_def name f =
- let
- val (modl, base) = dest_name name;
- fun mapp [] =
- Graph.map_node base (Def o f o dest_def)
- | mapp (m::ms) =
- Graph.map_node m (Module o mapp ms o dest_modl)
- in mapp modl end;
-
-fun map_defs f =
- let
- fun mapp (Def def) =
- (Def o f) def
- | mapp (Module modl) =
- (Module o Graph.map_nodes mapp) modl
- in dest_modl o mapp o Module end;
-
-fun fold_defs f =
- let
- fun fol prfix (name, (Def def, _)) =
- f (NameSpace.pack (prfix @ [name]), def)
- | fol prfix (name, (Module modl, _)) =
- Graph.fold (fol (prfix @ [name])) modl
- in Graph.fold (fol []) end;
-
-fun add_deps f modl =
- modl
- |> fold add_dep ([] |> fold_defs (append o f) modl);
-
-fun add_def_incr (name, Undef) module =
- (case try (get_def module) name
- of NONE => (error "attempted to add Undef to module")
- | SOME Undef => (error "attempted to add Undef to module")
- | SOME def' => map_def name (K def') module)
- | add_def_incr (name, def) module =
- (case try (get_def module) name
- of NONE => add_def (name, def) module
- | SOME Undef => map_def name (K def) module
- | SOME def' => if eq_def (def, def')
- then module
- else error ("tried to overwrite definition " ^ name));
-
-fun add_prim name (target, primdef as _::_) =
- let
- val (modl, base) = dest_name name;
- fun add [] module =
- (case try (Graph.get_node module) base
- of NONE =>
- module
- |> Graph.new_node (base, (Def o Prim) [(target, primdef)])
- | SOME (Def (Prim prim)) =>
- if AList.defined (op =) prim target
- then error ("already primitive definition (" ^ target
- ^ ") present for " ^ name)
- else
- module
- |> Graph.map_node base ((K o Def o Prim) (AList.update (op =)
- (target, primdef) prim))
- | _ => error ("already non-primitive definition present for " ^ name))
- | add (m::ms) module =
- module
- |> Graph.default_node (m, Module empty_module)
- |> Graph.map_node m (Module o add ms o dest_modl)
- in add modl end;
-
-fun ensure_prim name target =
- let
- val (modl, base) = dest_name name;
- fun ensure [] module =
- (case try (Graph.get_node module) base
- of NONE =>
- module
- |> Graph.new_node (base, (Def o Prim) [(target, [])])
- | SOME (Def (Prim prim)) =>
- module
- |> Graph.map_node base ((K o Def o Prim) (AList.default (op =)
- (target, []) prim))
- | _ => module)
- | ensure (m::ms) module =
- module
- |> Graph.default_node (m, Module empty_module)
- |> Graph.map_node m (Module o ensure ms o dest_modl)
- in ensure modl end;
-
fun merge_module modl12 =
let
fun join_module _ (Module m1, Module m2) =
@@ -784,10 +732,8 @@
end
) eqs NONE; eqs);
-fun check_prep_def modl Undef =
- Undef
- | check_prep_def modl (d as Prim _) =
- d
+fun check_prep_def modl Bot =
+ Bot
| check_prep_def modl (Fun (eqs, d)) =
Fun (check_funeqs eqs, d)
| check_prep_def modl (d as Typesyn _) =
@@ -837,7 +783,7 @@
fun postprocess_def (name, Datatype (_, constrs)) =
(check_samemodule (name :: map fst constrs);
fold (fn (co, _) =>
- add_def_incr (co, Datatypecons name)
+ add_def_incr true (co, Datatypecons name)
#> add_dep (co, name)
#> add_dep (name, co)
) constrs
@@ -845,7 +791,7 @@
| postprocess_def (name, Class (_, (_, membrs))) =
(check_samemodule (name :: map fst membrs);
fold (fn (m, _) =>
- add_def_incr (m, Classmember name)
+ add_def_incr true (m, Classmember name)
#> add_dep (m, name)
#> add_dep (name, m)
) membrs
@@ -853,57 +799,40 @@
| postprocess_def (name, Classinst (_, memdefs)) =
(check_samemodule (name :: map (fst o fst o snd) memdefs);
fold (fn (_, ((m', _), _)) =>
- add_def_incr (m', Classinstmember)
+ add_def_incr true (m', Classinstmember)
) memdefs
)
| postprocess_def _ =
I;
-fun succeed some (_, modl) = (Succeed some, modl);
-fun fail msg (_, modl) = (Fail ([msg], NONE), modl);
-
-fun check_fail _ (Succeed dst, trns) = (dst, trns)
- | check_fail msg (Fail (msgs, e), _) = raise FAIL (msg::msgs, e);
+fun succeed some (_, modl) = (some, modl);
+fun fail msg (_, modl) = raise FAIL ([msg], NONE);
-fun select_generator _ src [] modl =
- (SOME src, modl) |> fail ("no code generator available")
- | select_generator mk_msg src gens modl =
- let
- fun handle_fail msgs f =
- let
- in
- if ! soft_exc
- then
- (SOME src, modl) |> f
- handle FAIL exc => (Fail exc, modl)
- | e => (Fail (msgs, SOME e), modl)
- else
- (SOME src, modl) |> f
- handle FAIL exc => (Fail exc, modl)
- end;
- fun select msgs [(gname, gen)] =
- handle_fail (msgs @ [mk_msg gname]) (gen src)
- | select msgs ((gname, gen)::gens) =
- let
- val msgs' = msgs @ [mk_msg gname]
- in case handle_fail msgs' (gen src)
- of (Fail (_, NONE), _) =>
- select msgs' gens
- | result => result
- end;
- in select [] gens end;
-
-fun ensure_def defgens msg name (dep, modl) =
+fun ensure_def defgen strict msg name (dep, modl) =
let
- val msg' = case dep
+ val msg' = (case dep
of NONE => msg
- | SOME dep => msg ^ ", with dependency " ^ quote dep;
+ | SOME dep => msg ^ ", with dependency " ^ quote dep)
+ ^ (if strict then " (strict)" else " (non-strict)");
fun add_dp NONE = I
| add_dp (SOME dep) =
debug_msg (fn _ => "adding dependency " ^ quote dep ^ " -> " ^ quote name)
#> add_dep (dep, name);
fun prep_def def modl =
(check_prep_def modl def, modl);
+ fun invoke_generator name defgen modl =
+ if ! soft_exc
+ then
+ defgen name (SOME name, modl)
+ handle FAIL exc =>
+ if strict then raise FAIL exc
+ else (Bot, modl)
+ | e => raise FAIL (["definition generator for " ^ quote name], SOME e)
+ else
+ defgen name (SOME name, modl)
+ handle FAIL exc =>
+ if strict then raise FAIL exc
+ else (Bot, modl);
in
modl
|> (if can (get_def modl) name
@@ -911,19 +840,16 @@
debug_msg (fn _ => "asserting node " ^ quote name)
#> add_dp dep
else
- debug_msg (fn _ => "allocating node " ^ quote name)
- #> add_def (name, Undef)
+ debug_msg (fn _ => "allocating node " ^ quote name ^ (if strict then " (strict)" else " (non-strict)"))
+ #> ensure_bot name
#> add_dp dep
#> debug_msg (fn _ => "creating node " ^ quote name)
- #> select_generator (fn gname => "trying code generator "
- ^ gname ^ " for definition of " ^ quote name) name defgens
- #> debug_msg (fn _ => "checking creation of node " ^ quote name)
- #> check_fail msg'
+ #> invoke_generator name defgen
#-> (fn def => prep_def def)
#-> (fn def =>
debug_msg (fn _ => "addition of " ^ name ^ " := " ^ (Pretty.output o pretty_def) def)
#> debug_msg (fn _ => "adding")
- #> add_def_incr (name, def)
+ #> add_def_incr strict (name, def)
#> debug_msg (fn _ => "postprocessing")
#> postprocess_def (name, def)
#> debug_msg (fn _ => "adding done")
@@ -1049,9 +975,10 @@
fun mk_contents prfx module =
map_filter (seri prfx)
((map (AList.make (Graph.get_node module)) o rev o Graph.strong_conn) module)
- and seri prfx ([(name, Module modl)]) =
+ and seri prfx [(name, Module modl)] =
seri_module (resolver []) (map (resolver []) (imports_of module (prfx @ [name])))
(mk_name prfx name, mk_contents (prfx @ [name]) modl)
+ | seri prfx [(_, Def Bot)] = NONE
| seri prfx ds =
seri_defs sresolver (NameSpace.pack prfx)
(map (fn (name, Def def) => (fst (mk_name prfx name), def)) ds)