--- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Fri Mar 09 08:45:50 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Fri Mar 09 08:45:53 2007 +0100
@@ -1187,8 +1187,8 @@
@{index_ML CodegenData.add_preproc: "string * (theory -> thm list -> thm list)
-> theory -> theory"} \\
@{index_ML CodegenData.del_preproc: "string -> theory -> theory"} \\
- @{index_ML CodegenData.add_datatype: "string * (((string * sort) list * (string * typ list) list)
- * thm list Susp.T) -> theory -> theory"} \\
+ @{index_ML CodegenData.add_datatype: "string * ((string * sort) list * (string * typ list) list)
+ -> theory -> theory"} \\
@{index_ML CodegenData.del_datatype: "string -> theory -> theory"} \\
@{index_ML CodegenData.get_datatype: "theory -> string
-> ((string * sort) list * (string * typ list) list) option"} \\
@@ -1232,14 +1232,12 @@
\item @{ML CodegenData.del_preproc}~@{text "name"}~@{text "thy"} removes
generic preprcoessor named @{text name} from executable content.
- \item @{ML CodegenData.add_datatype}~@{text "(name, (spec, cert))"}~@{text "thy"} adds
+ \item @{ML CodegenData.add_datatype}~@{text "(name, spec)"}~@{text "thy"} adds
a datatype to executable content, with type constructor
@{text name} and specification @{text spec}; @{text spec} is
a pair consisting of a list of type variable with sort
constraints and a list of constructors with name
- and types of arguments. The addition as datatype
- has to be justified giving a certificate of suspended
- theorems as witnesses for injectiveness and distinctness.
+ and types of arguments.
\item @{ML CodegenData.del_datatype}~@{text "name"}~@{text "thy"}
remove a datatype from executable content, if present.
--- a/src/HOL/Code_Generator.thy Fri Mar 09 08:45:50 2007 +0100
+++ b/src/HOL/Code_Generator.thy Fri Mar 09 08:45:53 2007 +0100
@@ -87,7 +87,9 @@
(Haskell infixl 4 "==")
-text {* boolean expressions *}
+text {* type bool *}
+
+code_datatype True False
lemma [code func]:
shows "(False \<and> x) = False"
@@ -152,18 +154,22 @@
bool true false not
-text {* itself as a code generator datatype *}
+text {* type prop *}
+
+code_datatype Trueprop "prop"
+
+
+text {* type itself *}
-setup {*
- let
- val v = ("'a", []);
- val t = Logic.mk_type (TFree v);
- val Const (c, ty) = t;
- val (_, Type (dtco, _)) = strip_type ty;
- in
- CodegenData.add_datatype (dtco, (([v], [(c, [])]), CodegenData.lazy (fn () => [])))
- end
-*}
+code_datatype "TYPE('a)"
+
+
+text {* prevent unfolding of quantifier definitions *}
+
+lemma [code func]:
+ "Ex = Ex"
+ "All = All"
+ by rule+
text {* code generation for arbitrary as exception *}
--- a/src/HOL/Library/EfficientNat.thy Fri Mar 09 08:45:50 2007 +0100
+++ b/src/HOL/Library/EfficientNat.thy Fri Mar 09 08:45:53 2007 +0100
@@ -159,7 +159,7 @@
(Haskell "!((_) + 1)")
setup {*
- CodegenData.del_datatype "nat"
+ CodegenData.add_datatype ("nat", ([], []))
*}
types_code
--- a/src/HOL/Tools/datatype_codegen.ML Fri Mar 09 08:45:50 2007 +0100
+++ b/src/HOL/Tools/datatype_codegen.ML Fri Mar 09 08:45:53 2007 +0100
@@ -9,8 +9,6 @@
sig
val get_eq: theory -> string -> thm list
val get_eq_datatype: theory -> string -> thm list
- val get_cert: theory -> bool * string -> thm list
- val get_cert_datatype: theory -> string -> thm list
val dest_case_expr: theory -> term
-> ((string * typ) list * ((term * typ) * (term * term) list)) option
val add_datatype_case_const: string -> theory -> theory
@@ -28,7 +26,7 @@
-> (string * (arity * term list)) list option
val prove_codetypes_arities: tactic -> (string * bool) list -> sort
-> (arity list -> (string * term list) list -> theory
- -> ((bstring * Attrib.src list) * term) list * theory)
+ -> ((bstring * Attrib.src list) * term) list * theory)
-> (arity list -> (string * term list) list -> theory -> theory)
-> theory -> theory
@@ -379,35 +377,6 @@
in map mk_dist (sym_product cos) end;
local
- val bool_eq_implies = iffD1;
- val rew_eq = thm "HOL.atomize_eq" |> Thm.symmetric;
- val rew_conj = thm "HOL.atomize_conj" |> Thm.symmetric;
- val not_false_true = iffD2 OF [nth (thms "HOL.simp_thms") 7, TrueI];
- val not_eq_quodlibet = thm "not_eq_quodlibet";
-in
-
-fun get_cert_datatype thy dtco =
- let
- val SOME (vs, cs) = DatatypePackage.get_datatype_spec thy dtco;
- val inject = (#inject o DatatypePackage.the_datatype thy) dtco
- |> map (fn thm => bool_eq_implies OF [thm] )
- |> map (MetaSimplifier.rewrite_rule [rew_eq, rew_conj]);
- val ctxt = ProofContext.init thy;
- val simpset = Simplifier.context ctxt
- (MetaSimplifier.empty_ss addsimprocs [DatatypePackage.distinct_simproc]);
- val cos = map (fn (co, tys) =>
- (Const (co, tys ---> Type (dtco, map TFree vs)), tys)) cs;
- val tac = ALLGOALS (simp_tac simpset)
- THEN ALLGOALS (ProofContext.fact_tac [not_false_true, TrueI]);
- val distinct =
- mk_distinct cos
- |> map (fn t => Goal.prove_global thy [] [] t (K tac))
- |> map (fn thm => not_eq_quodlibet OF [thm])
- in inject @ distinct end
-
-end;
-
-local
val not_sym = thm "HOL.not_sym";
val not_false_true = iffD2 OF [nth (thms "HOL.simp_thms") 7, TrueI];
val refl = thm "refl";
@@ -496,9 +465,6 @@
| get_spec thy (tyco, false) =
TypecopyPackage.get_spec thy tyco;
-fun get_cert thy (true, dtco) = get_cert_datatype thy dtco
- | get_cert thy (false, dtco) = [TypecopyPackage.get_cert thy dtco];
-
local
fun get_eq_thms thy tyco = case DatatypePackage.get_datatype thy tyco
of SOME _ => get_eq_datatype thy tyco
@@ -559,20 +525,20 @@
(* registering code types in code generator *)
-fun codetype_hook specs =
- let
- fun add (dtco, (flag, spec)) thy =
- let
- fun cert thy_ref = (fn () => get_cert (Theory.deref thy_ref) (flag, dtco));
- in
- CodegenData.add_datatype
- (dtco, (spec, CodegenData.lazy (cert (Theory.self_ref thy)))) thy
- end;
- in fold add specs end;
+val codetype_hook =
+ fold (fn (dtco, (_, spec)) => CodegenData.add_datatype (dtco, spec));
(* instrumentalizing the sort algebra *)
+(*fun assume_arities_of_sort thy arities ty_sort =
+ let
+ val pp = Sign.pp thy;
+ val algebra = Sign.classes_of thy
+ |> fold (fn (tyco, asorts, sort) =>
+ Sorts.add_arities pp (tyco, map (fn class => (class, asorts)) sort)) arities;
+ in Sorts.of_sort algebra ty_sort end;
+
fun get_codetypes_arities thy tycos sort =
let
val algebra = Sign.classes_of thy;
@@ -588,7 +554,7 @@
fun typ_of_sort ty =
let
val arities = map (fn (tyco, _) => (tyco, map snd vs, sort)) css;
- in ClassPackage.assume_arities_of_sort thy arities (ty, sort) end;
+ in assume_arities_of_sort thy arities (ty, sort) end;
fun mk_cons tyco (c, tys) =
let
val ts = Name.names Name.context "a" tys;
@@ -598,7 +564,34 @@
then SOME (
map (fn (tyco, cs) => (tyco, (mk_arity tyco, map (mk_cons tyco) cs))) css
) else NONE
- end;
+ end;*)
+
+fun get_codetypes_arities thy tycos sort =
+ let
+ val pp = Sign.pp thy;
+ val algebra = Sign.classes_of thy;
+ val (vs_proto, css_proto) = the_codetypes_mut_specs thy tycos;
+ val vs = map (fn (v, vsort) => (v, Sorts.inter_sort algebra (vsort, sort))) vs_proto;
+ val css = map (fn (tyco, (_, cs)) => (tyco, cs)) css_proto;
+ val algebra' = algebra
+ |> fold (fn (tyco, _) =>
+ Sorts.add_arities pp (tyco, map (fn class => (class, map snd vs)) sort)) css;
+ fun typ_sort_inst ty = CodegenConsts.typ_sort_inst algebra' (Logic.varifyT ty, sort);
+ val venv = Vartab.empty
+ |> fold (fn (v, sort) => Vartab.update_new ((v, 0), sort)) vs
+ |> fold (fn (_, cs) => fold (fn (_, tys) => fold typ_sort_inst tys) cs) css;
+ fun inst (v, _) = (v, (the o Vartab.lookup venv) (v, 0));
+ val vs' = map inst vs;
+ fun mk_arity tyco = (tyco, map snd vs', sort);
+ fun mk_cons tyco (c, tys) =
+ let
+ val tys' = (map o Term.map_type_tfree) (TFree o inst) tys;
+ val ts = Name.names Name.context "a" tys';
+ val ty = (tys' ---> Type (tyco, map TFree vs'));
+ in list_comb (Const (c, ty), map Free ts) end;
+ in
+ map (fn (tyco, cs) => (tyco, (mk_arity tyco, map (mk_cons tyco) cs))) css |> SOME
+ end handle Class_Error => NONE;
fun prove_codetypes_arities tac tycos sort f after_qed thy =
case get_codetypes_arities thy tycos sort
--- a/src/HOL/Tools/typecopy_package.ML Fri Mar 09 08:45:50 2007 +0100
+++ b/src/HOL/Tools/typecopy_package.ML Fri Mar 09 08:45:53 2007 +0100
@@ -22,7 +22,6 @@
type hook = string * info -> theory -> theory
val add_hook: hook -> theory -> theory
val get_spec: theory -> string -> (string * sort) list * (string * typ list) list
- val get_cert: theory -> string -> thm
val get_eq: theory -> string -> thm
val print: theory -> unit
val setup: theory -> theory
@@ -132,26 +131,16 @@
end; (*local*)
-(* equality function equation *)
+(* equality function equation and datatype specification *)
fun get_eq thy tyco =
(#inject o the o get_typecopy_info thy) tyco;
-
-(* datatype specification and certificate *)
-
fun get_spec thy tyco =
let
val SOME { vs, constr, typ, ... } = get_typecopy_info thy tyco
in (vs, [(constr, [typ])]) end;
-local
- val bool_eq_implies = iffD1;
- val rew_eq = thm "HOL.atomize_eq" |> Thm.symmetric;
-in fun get_cert thy tyco =
- MetaSimplifier.rewrite_rule [rew_eq] (bool_eq_implies OF [get_eq thy tyco])
-end; (*local*)
-
(* hook for projection function code *)
--- a/src/Pure/Tools/class_package.ML Fri Mar 09 08:45:50 2007 +0100
+++ b/src/Pure/Tools/class_package.ML Fri Mar 09 08:45:53 2007 +0100
@@ -27,8 +27,6 @@
val instance_sort_cmd: string * string -> theory -> Proof.state
val prove_instance_sort: tactic -> class * sort -> theory -> theory
- val assume_arities_of_sort: theory -> arity list -> typ * sort -> bool
-
(* experimental class target *)
val class_of_locale: theory -> string -> class option
val add_def_in_class: local_theory -> string
@@ -105,17 +103,6 @@
end;
-(* contexts with arity assumptions *)
-
-fun assume_arities_of_sort thy arities ty_sort =
- let
- val pp = Sign.pp thy;
- val algebra = Sign.classes_of thy
- |> fold (fn (tyco, asorts, sort) =>
- Sorts.add_arities pp (tyco, map (fn class => (class, asorts)) sort)) arities;
- in Sorts.of_sort algebra ty_sort end;
-
-
(* instances with implicit parameter handling *)
local
@@ -141,7 +128,7 @@
val _ = case (duplicates (op =) o map #1) arities
of [] => ()
| dupl_tycos => error ("type constructors occur more than once in arities: "
- ^ (commas o map quote) dupl_tycos);
+ ^ (commas o map quote) dupl_tycos);
val super_sort = (Graph.all_succs o #classes o Sorts.rep_algebra o Sign.classes_of) theory
fun get_consts_class tyco ty class =
let
@@ -179,7 +166,6 @@
in fold_map read defs cs end;
val (defs, _) = read_defs raw_defs cs
(fold Sign.primitive_arity arities (Theory.copy theory));
-
fun get_remove_contraint c thy =
let
val ty = Sign.the_const_constraint thy c;
@@ -334,7 +320,6 @@
(* exporting terms and theorems to global toplevel *)
-(*FIXME should also be used when introducing classes*)
fun globalize thy classes =
let
@@ -380,6 +365,7 @@
("default", Method.thms_ctxt_args (Method.METHOD oo default_tac),
"apply some intro/elim rule")]);
+
(* tactical interfaces to locale commands *)
fun prove_interpretation tac prfx_atts expr insts thy =
@@ -431,13 +417,6 @@
local
-fun add_axclass (name, supsort) params axs thy =
- let
- val (c, thy') = thy
- |> AxClass.define_class_i (name, supsort) params axs;
- val {intro, axioms, ...} = AxClass.get_definition thy' c;
- in ((c, (intro, axioms)), thy') end;
-
fun certify_class thy class =
tap (the_class_data thy) (Sign.certify_class thy class);
@@ -454,27 +433,28 @@
(*val subst_classtyvars = Element.map_ctxt {name = I, var = I, term = I,
typ = Term.map_type_tfree subst_classtyvar, fact = I, attrib = I};*)
val other_consts = map (prep_param thy) raw_other_consts;
- val elems = fold_rev (fn Locale.Elem e => cons e | _ => I)
- raw_elems []; (*FIXME make include possible here?*)
+ val (elems, includes) = fold_rev (fn Locale.Elem e => apfst (cons e)
+ | Locale.Expr i => apsnd (cons i)) raw_elems ([], []);
val supclasses = map (prep_class thy) raw_supclasses;
val supsort =
supclasses
|> Sign.certify_sort thy
- |> (fn [] => Sign.defaultS thy | S => S); (*FIXME Why syntax defaultS?*)
- val supexpr = Locale.Merge
- (map (Locale.Locale o #locale o the_class_data thy) supclasses);
- val supparams = (map fst o Locale.parameters_of_expr thy) supexpr;
+ |> (fn [] => Sign.defaultS thy | S => S); (*FIXME Why syntax defaultS?*)
+ val suplocales = map (Locale.Locale o #locale o the_class_data thy) supclasses;
+ val supexpr = Locale.Merge (suplocales @ includes);
+ val supparams = (map fst o Locale.parameters_of_expr thy)
+ (Locale.Merge suplocales);
val supconsts = AList.make
(the o AList.lookup (op =) (param_map thy supclasses)) (map fst supparams);
- (*FIXME include proper*)
(*val elems_constrains = map
(Element.Constrains o apsnd (Term.map_type_tfree subst_classtyvar)) supparams;*)
fun extract_params thy name_locale =
- let
+ let
val params = Locale.parameters_of thy name_locale;
in
(map (fst o fst) params, params
- |> (map o apfst o apsnd o Term.map_type_tfree) (K (TFree (AxClass.param_tyvarname, Sign.defaultS thy)))
+ |> (map o apfst o apsnd o Term.map_type_tfree)
+ (K (TFree (AxClass.param_tyvarname, Sign.defaultS thy)))
|> (map o apsnd) (fork_mixfix true NONE #> fst)
|> chop (length supconsts)
|> snd)
@@ -486,8 +466,8 @@
Const ((fst o the o AList.lookup (op =) consts) c, ty)
| subst t = t;
fun prep_asm ((name, atts), ts) =
- (*FIXME: name handling?*)
- ((NameSpace.base name, map (Attrib.attribute thy) atts), (map o map_aterms) subst ts);
+ ((NameSpace.base name, map (Attrib.attribute thy) atts),
+ (map o map_aterms) subst ts);
in
Locale.global_asms_of thy name_locale
|> map prep_asm
@@ -578,17 +558,24 @@
fun add_def_in_class lthy class ((c, syn), ((name, atts), (rhs, eq))) thy =
let
+ val prfx = (Logic.const_of_class o NameSpace.base) class;
val rhs' = global_term thy [class] rhs;
val (syn', _) = fork_mixfix true NONE syn;
val ty = Term.fastype_of rhs';
+ fun mk_name thy c =
+ let
+ val n1 = Sign.full_name thy c;
+ val n2 = NameSpace.qualifier n1;
+ val n3 = NameSpace.base n1;
+ in NameSpace.implode [n2, prfx, n3] end;
fun add_const (c, ty, syn) =
Sign.add_consts_authentic [(c, ty, syn)]
- #> pair (Sign.full_name thy c, ty);
+ #> pair (mk_name thy c, ty);
fun add_def ((name, atts), prop) thy =
thy
|> PureThy.add_defs_i false [((name, prop), map (Attrib.attribute thy) atts)]
|>> the_single;
- (*val _ = Output.info "------ DEF ------";
+ val _ = Output.info "------ DEF ------";
val _ = Output.info c;
val _ = Output.info name;
val _ = (Output.info o Sign.string_of_term thy) rhs';
@@ -603,12 +590,14 @@
val _ = map print_witness witness;
val _ = (Output.info o string_of_thm) eq';
val eq'' = Element.satisfy_thm witness eq';
- val _ = (Output.info o string_of_thm) eq'';*)
+ val _ = (Output.info o string_of_thm) eq'';
in
thy
- (*|> add_const (c, ty, syn')
+ |> Sign.add_path prfx
+ |> add_const (c, ty, syn')
|-> (fn c => add_def ((name, atts), Logic.mk_equals (Const c, rhs')))
- |-> (fn global_def_thm => tap (fn _ => (Output.info o string_of_thm) global_def_thm))*)
+ |-> (fn global_def_thm => tap (fn _ => (Output.info o string_of_thm) global_def_thm))
+ |> Sign.restore_naming thy
end;
end;
--- a/src/Pure/Tools/codegen_data.ML Fri Mar 09 08:45:50 2007 +0100
+++ b/src/Pure/Tools/codegen_data.ML Fri Mar 09 08:45:53 2007 +0100
@@ -15,9 +15,8 @@
val add_func_legacy: thm -> theory -> theory
val del_func: thm -> theory -> theory
val add_funcl: CodegenConsts.const * thm list Susp.T -> theory -> theory
- val add_datatype: string * (((string * sort) list * (string * typ list) list) * thm list Susp.T)
+ val add_datatype: string * ((string * sort) list * (string * typ list) list)
-> theory -> theory
- val del_datatype: string -> theory -> theory
val add_inline: thm -> theory -> theory
val del_inline: thm -> theory -> theory
val add_inline_proc: string * (theory -> cterm list -> thm list) -> theory -> theory
@@ -28,8 +27,7 @@
val operational_algebra: theory -> (sort -> sort) * Sorts.algebra
val these_funcs: theory -> CodegenConsts.const -> thm list
val tap_typ: theory -> CodegenConsts.const -> typ option
- val get_datatype: theory -> string
- -> ((string * sort) list * (string * typ list) list) option
+ val get_datatype: theory -> string -> ((string * sort) list * (string * typ list) list)
val get_datatype_of_constr: theory -> CodegenConsts.const -> string option
val preprocess_cterm: cterm -> thm
@@ -193,7 +191,7 @@
in (SOME consts, thms) end;
val eq_string = op = : string * string -> bool;
-fun eq_dtyp (((vs1, cs1), _), ((vs2, cs2), _)) =
+fun eq_dtyp ((vs1, cs1), (vs2, cs2)) =
gen_eq_set (eq_pair eq_string (gen_eq_set eq_string)) (vs1, vs2)
andalso gen_eq_set (eq_pair eq_string (eq_list (is_equal o Term.typ_ord))) (cs1, cs2);
fun merge_dtyps (tabs as (tab1, tab2)) =
@@ -210,7 +208,7 @@
datatype spec = Spec of {
funcs: sdthms Consttab.table,
dconstrs: string Consttab.table,
- dtyps: (((string * sort) list * (string * typ list) list) * thm list Susp.T) Symtab.table
+ dtyps: ((string * sort) list * (string * typ list) list) Symtab.table
};
fun mk_spec ((funcs, dconstrs), dtyps) =
@@ -328,15 +326,17 @@
(Pretty.block o Pretty.fbreaks) (
Pretty.str s :: pretty_sdthms ctxt lthms
);
- fun pretty_dtyp (s, cos) =
- (Pretty.block o Pretty.breaks) (
- Pretty.str s
- :: Pretty.str "="
- :: Pretty.separate "|" (map (fn (c, []) => Pretty.str c
- | (c, tys) =>
- (Pretty.block o Pretty.breaks)
- (Pretty.str c :: Pretty.str "of" :: map (Pretty.quote o Sign.pretty_typ thy) tys)) cos)
- )
+ fun pretty_dtyp (s, []) =
+ Pretty.str s
+ | pretty_dtyp (s, cos) =
+ (Pretty.block o Pretty.breaks) (
+ Pretty.str s
+ :: Pretty.str "="
+ :: separate (Pretty.str "|") (map (fn (c, []) => Pretty.str c
+ | (c, tys) =>
+ (Pretty.block o Pretty.breaks)
+ (Pretty.str c :: Pretty.str "of" :: map (Pretty.quote o Sign.pretty_typ thy) tys)) cos)
+ );
val inlines = (#inlines o the_preproc) exec;
val inline_procs = (map fst o #inline_procs o the_preproc) exec;
val preprocs = (map fst o #preprocs o the_preproc) exec;
@@ -346,13 +346,14 @@
|> sort (string_ord o pairself fst);
val dtyps = the_dtyps exec
|> Symtab.dest
- |> map (fn (dtco, ((vs, cos), _)) => (Sign.string_of_typ thy (Type (dtco, map TFree vs)), cos))
+ |> map (fn (dtco, (vs, cos)) => (Sign.string_of_typ thy (Type (dtco, map TFree vs)), cos))
|> sort (string_ord o pairself fst)
in
(Pretty.writeln o Pretty.chunks) [
Pretty.block (
Pretty.str "defining equations:"
- :: map pretty_func funs
+ :: Pretty.fbrk
+ :: (Pretty.fbreaks o map pretty_func) funs
),
Pretty.block (
Pretty.str "inlining theorems:"
@@ -431,77 +432,6 @@
^ CodegenConsts.string_of_const thy c ^ "\n" ^ string_of_thm thm)
in map cert c_thms end;
-fun mk_cos tyco vs cos =
- let
- val dty = Type (tyco, map TFree vs);
- fun mk_co (co, tys) = (Const (co, (tys ---> dty)), map I tys);
- in map mk_co cos end;
-
-fun mk_co_args (co, tys) ctxt =
- let
- val names = Name.invents ctxt "a" (length tys);
- val ctxt' = fold Name.declare names ctxt;
- val vs = map2 (fn v => fn ty => Free (fst (v, 0), I ty)) names tys;
- in (vs, ctxt') end;
-
-fun check_freeness thy cos thms =
- let
- val props = AList.make Drule.plain_prop_of thms;
- fun sym_product [] = []
- | sym_product (x::xs) = map (pair x) xs @ sym_product xs;
- val quodlibet =
- let
- val judg = ObjectLogic.fixed_judgment (the_context ()) "x";
- val [free] = fold_aterms (fn v as Free _ => cons v | _ => I) judg [];
- val judg' = Term.subst_free [(free, Bound 0)] judg;
- val prop = Type ("prop", []);
- val prop' = fastype_of judg';
- in
- Const ("all", (prop' --> prop) --> prop) $ Abs ("P", prop', judg')
- end;
- fun check_inj (co, []) =
- NONE
- | check_inj (co, tys) =
- let
- val ((xs, ys), _) = Name.context
- |> mk_co_args (co, tys)
- ||>> mk_co_args (co, tys);
- val prem = Logic.mk_equals
- (list_comb (co, xs), list_comb (co, ys));
- val concl = Logic.mk_conjunction_list
- (map2 (curry Logic.mk_equals) xs ys);
- val t = Logic.mk_implies (prem, concl);
- in case find_first (curry Term.could_unify t o snd) props
- of SOME (thm, _) => SOME thm
- | NONE => error ("Could not prove injectiveness statement\n"
- ^ Sign.string_of_term thy t
- ^ "\nfor constructor "
- ^ CodegenConsts.string_of_const_typ thy (dest_Const co)
- ^ "\nwith theorems\n" ^ cat_lines (map string_of_thm thms))
- end;
- fun check_dist ((co1, tys1), (co2, tys2)) =
- let
- val ((xs1, xs2), _) = Name.context
- |> mk_co_args (co1, tys1)
- ||>> mk_co_args (co2, tys2);
- val prem = Logic.mk_equals
- (list_comb (co1, xs1), list_comb (co2, xs2));
- val t = Logic.mk_implies (prem, quodlibet);
- in case find_first (curry Term.could_unify t o snd) props
- of SOME (thm, _) => thm
- | NONE => error ("Could not prove distinctness statement\n"
- ^ Sign.string_of_term thy t
- ^ "\nfor constructors "
- ^ CodegenConsts.string_of_const_typ thy (dest_Const co1)
- ^ " and "
- ^ CodegenConsts.string_of_const_typ thy (dest_Const co2)
- ^ "\nwith theorems\n" ^ cat_lines (map string_of_thm thms))
- end;
- in (map_filter check_inj cos, map check_dist (sym_product cos)) end;
-
-fun certify_datatype thy dtco cs thms =
- (op @) (check_freeness thy cs thms);
-
(** operational sort algebra and class discipline **)
@@ -684,37 +614,102 @@
(add_lthms lthms'))) thy
end;
-fun add_datatype (tyco, (vs_cos as (vs, cos), lthms)) thy =
+local
+
+fun consts_of_cos thy tyco vs cos =
+ let
+ val dty = Type (tyco, map TFree vs);
+ fun mk_co (co, tys) = CodegenConsts.norm_of_typ thy (co, tys ---> dty);
+ in map mk_co cos end;
+
+fun co_of_const thy (c, ty) =
let
- val cs = mk_cos tyco vs cos;
- val consts = map (CodegenConsts.norm_of_typ thy o dest_Const o fst) cs;
- val add =
- map_dtyps (Symtab.update_new (tyco,
- (vs_cos, certificate thy (fn thy => certify_datatype thy tyco cs) lthms)))
- #> map_dconstrs (fold (fn c => Consttab.update (c, tyco)) consts)
- in map_exec_purge (SOME consts) add thy end;
+ fun err () = error
+ ("Illegal type for datatype constructor: " ^ Sign.string_of_typ thy ty);
+ val (tys, ty') = strip_type ty;
+ val (tyco, vs) = ((apsnd o map) dest_TFree o dest_Type) ty'
+ handle TYPE _ => err ();
+ val sorts = if has_duplicates (eq_fst op =) vs then err ()
+ else map snd vs;
+ val vs_names = Name.invent_list [] "'a" (length vs);
+ val vs_map = map fst vs ~~ vs_names;
+ val vs' = vs_names ~~ sorts;
+ val tys' = (map o map_type_tfree) (fn (v, sort) =>
+ (TFree ((the o AList.lookup (op =) vs_map) v, sort))) tys
+ handle Option => err ();
+ in (tyco, (vs', (c, tys'))) end;
fun del_datatype tyco thy =
+ case Symtab.lookup ((the_dtyps o get_exec) thy) tyco
+ of SOME (vs, cos) => let
+ val consts = consts_of_cos thy tyco vs cos;
+ val del =
+ map_dtyps (Symtab.delete tyco)
+ #> map_dconstrs (fold Consttab.delete consts)
+ in map_exec_purge (SOME consts) del thy end
+ | NONE => thy;
+
+(*FIXME integrate this auxiliary properly*)
+
+in
+
+fun add_datatype (tyco, (vs_cos as (vs, cos))) thy =
let
- val SOME ((vs, cos), _) = Symtab.lookup ((the_dtyps o get_exec) thy) tyco;
- val cs = mk_cos tyco vs cos;
- val consts = map (CodegenConsts.norm_of_typ thy o dest_Const o fst) cs;
- val del =
- map_dtyps (Symtab.delete tyco)
- #> map_dconstrs (fold Consttab.delete consts)
- in map_exec_purge (SOME consts) del thy end;
+ val consts = consts_of_cos thy tyco vs cos;
+ val add =
+ map_dtyps (Symtab.update_new (tyco, vs_cos))
+ #> map_dconstrs (fold (fn c => Consttab.update (c, tyco)) consts)
+ in
+ thy
+ |> del_datatype tyco
+ |> map_exec_purge (SOME consts) add
+ end;
+
+fun add_datatype_consts cs thy =
+ let
+ val raw_cos = map (co_of_const thy) cs;
+ val (tyco, (vs_names, sorts_cos)) = if (length o distinct (eq_fst op =)) raw_cos = 1
+ then ((fst o hd) raw_cos, ((map fst o fst o snd o hd) raw_cos,
+ map ((apfst o map) snd o snd) raw_cos))
+ else error ("Term constructors not referring to the same type: "
+ ^ commas (map (CodegenConsts.string_of_const_typ thy) cs));
+ val sorts = foldr1 ((uncurry o map2 o curry o Sorts.inter_sort) (Sign.classes_of thy))
+ (map fst sorts_cos);
+ val cos = map snd sorts_cos;
+ val vs = vs_names ~~ sorts;
+ in
+ thy
+ |> add_datatype (tyco, (vs, cos))
+ end;
+
+fun add_datatype_consts_cmd raw_cs thy =
+ let
+ val cs = map (apsnd Logic.unvarifyT o CodegenConsts.typ_of_inst thy
+ o CodegenConsts.read_const thy) raw_cs
+ in
+ thy
+ |> add_datatype_consts cs
+ end;
+
+end; (*local*)
fun add_inline thm thy =
- (map_exec_purge NONE o map_preproc o apfst o apfst) (fold (insert Thm.eq_thm) (CodegenFunc.mk_rew thm)) thy;
+ (map_exec_purge NONE o map_preproc o apfst o apfst)
+ (fold (insert Thm.eq_thm) (CodegenFunc.mk_rew thm)) thy;
+ (*fully applied in order to get right context for mk_rew!*)
fun del_inline thm thy =
- (map_exec_purge NONE o map_preproc o apfst o apfst) (fold (remove Thm.eq_thm) (CodegenFunc.mk_rew thm)) thy ;
+ (map_exec_purge NONE o map_preproc o apfst o apfst)
+ (fold (remove Thm.eq_thm) (CodegenFunc.mk_rew thm)) thy;
+ (*fully applied in order to get right context for mk_rew!*)
fun add_inline_proc (name, f) =
- (map_exec_purge NONE o map_preproc o apfst o apsnd) (AList.update (op =) (name, (serial (), f)));
+ (map_exec_purge NONE o map_preproc o apfst o apsnd)
+ (AList.update (op =) (name, (serial (), f)));
fun del_inline_proc name =
- (map_exec_purge NONE o map_preproc o apfst o apsnd) (delete_force "inline procedure" name);
+ (map_exec_purge NONE o map_preproc o apfst o apsnd)
+ (delete_force "inline procedure" name);
fun add_preproc (name, f) =
(map_exec_purge NONE o map_preproc o apsnd) (AList.update (op =) (name, (serial (), f)));
@@ -774,6 +769,25 @@
end; (*local*)
+fun get_datatype thy tyco =
+ case Symtab.lookup ((the_dtyps o get_exec) thy) tyco
+ of SOME spec => spec
+ | NONE => Sign.arity_number thy tyco
+ |> Name.invents Name.context "'a"
+ |> map (rpair [])
+ |> rpair [];
+
+fun get_datatype_of_constr thy =
+ Consttab.lookup ((the_dcontrs o get_exec) thy);
+
+fun get_datatype_constr thy const =
+ case Consttab.lookup ((the_dcontrs o get_exec) thy) const
+ of SOME tyco => let
+ val (vs, cs) = get_datatype thy tyco;
+ (*FIXME continue here*)
+ in NONE end
+ | NONE => NONE;
+
local
fun get_funcs thy const =
@@ -812,14 +826,6 @@
end; (*local*)
-fun get_datatype thy tyco =
- Symtab.lookup ((the_dtyps o get_exec) thy) tyco
- |> Option.map (fn (spec, thms) => (Susp.force thms; spec));
-
-fun get_datatype_of_constr thy c =
- Consttab.lookup ((the_dcontrs o get_exec) thy) c
- |> (Option.map o tap) (fn dtco => get_datatype thy dtco);
-
(** code attributes **)
@@ -846,15 +852,23 @@
and K = OuterKeyword
val print_codesetupK = "print_codesetup";
+val code_datatypeK = "code_datatype";
in
val print_codesetupP =
- OuterSyntax.improper_command print_codesetupK "print code generator setup of this theory" OuterKeyword.diag
+ OuterSyntax.improper_command print_codesetupK "print code generator setup of this theory" K.diag
(Scan.succeed
(Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep (CodeData.print o Toplevel.theory_of)));
-val _ = OuterSyntax.add_parsers [print_codesetupP];
+val code_datatypeP =
+ OuterSyntax.command code_datatypeK "define set of code datatype constructors" K.thy_decl (
+ Scan.repeat1 P.term
+ >> (Toplevel.theory o add_datatype_consts_cmd)
+ );
+
+
+val _ = OuterSyntax.add_parsers [print_codesetupP, code_datatypeP];
end; (*local*)
--- a/src/Pure/Tools/codegen_package.ML Fri Mar 09 08:45:50 2007 +0100
+++ b/src/Pure/Tools/codegen_package.ML Fri Mar 09 08:45:53 2007 +0100
@@ -148,11 +148,7 @@
let
fun defgen_datatype trns =
let
- val (vs, cos) = case CodegenData.get_datatype thy tyco
- of SOME x => x
- | NONE => (Name.invents Name.context "'a" (Sign.arity_number thy tyco)
- |> map (rpair (Sign.defaultS thy)) , [])
- (*FIXME move to CodegenData*)
+ val (vs, cos) = CodegenData.get_datatype thy tyco;
in
trns
|> fold_map (exprgen_tyvar_sort thy algbr funcgr strct) vs