--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Tue Sep 09 20:51:36 2014 +0200
@@ -2,6 +2,7 @@
Author: Dmitriy Traytel, TU Muenchen
Author: Jasmin Blanchette, TU Muenchen
Author: Martin Desharnais, TU Muenchen
+ Author: Stefan Berghofer, TU Muenchen
Copyright 2012, 2013, 2014
Shared library for the datatype and codatatype constructions.
@@ -187,6 +188,7 @@
BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory -> 'a) ->
binding list -> (string * sort) list -> (string * sort) list -> ((string * sort) * typ) list ->
local_theory -> (BNF_Def.bnf list * BNF_Comp.absT_info list) * 'a
+ val fp_antiquote_setup: binding -> theory -> theory
end;
structure BNF_FP_Util : BNF_FP_UTIL =
@@ -630,4 +632,29 @@
timer; ((pre_bnfs, absT_infos), res)
end;
+fun fp_antiquote_setup binding =
+ Thy_Output.antiquotation binding (Args.type_name {proper = true, strict = true})
+ (fn {source = src, context = ctxt, ...} => fn fcT_name =>
+ (case Ctr_Sugar.ctr_sugar_of ctxt fcT_name of
+ NONE => error ("Not a known freely generated type name: " ^ quote fcT_name)
+ | SOME {T = T0, ctrs = ctrs0, ...} =>
+ let
+ val freezeT = Term.map_atyps (fn TVar ((s, _), S) => TFree (s, S) | T => T);
+
+ val T = freezeT T0;
+ val ctrs = map (Term.map_types freezeT) ctrs0;
+
+ val pretty_typ_bracket = Syntax.pretty_typ (Config.put pretty_priority 1001 ctxt);
+ fun pretty_ctr ctr =
+ Pretty.block (Pretty.breaks (Syntax.pretty_term ctxt ctr ::
+ map pretty_typ_bracket (binder_types (fastype_of ctr))));
+ val pretty_co_datatype =
+ Pretty.block (Pretty.keyword1 (Binding.name_of binding) :: Pretty.brk 1 ::
+ Syntax.pretty_typ ctxt T :: Pretty.str " =" :: Pretty.brk 1 ::
+ flat (separate [Pretty.brk 1, Pretty.str "| "] (map (single o pretty_ctr) ctrs)));
+ in
+ Thy_Output.output ctxt
+ (Thy_Output.maybe_pretty_source (K (K pretty_co_datatype)) ctxt src [()])
+ end));
+
end;
--- a/src/HOL/Tools/BNF/bnf_gfp.ML Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Tue Sep 09 20:51:36 2014 +0200
@@ -2530,4 +2530,6 @@
Outer_Syntax.local_theory @{command_spec "codatatype"} "define coinductive datatypes"
(parse_co_datatype_cmd Greatest_FP construct_gfp);
+val _ = Theory.setup (fp_antiquote_setup @{binding codatatype});
+
end;
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Tue Sep 09 20:51:36 2014 +0200
@@ -1817,4 +1817,6 @@
Outer_Syntax.local_theory @{command_spec "datatype_new"} "define inductive datatypes"
(parse_co_datatype_cmd Least_FP construct_lfp);
+val _ = Theory.setup (fp_antiquote_setup @{binding datatype});
+
end;
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Tue Sep 09 20:51:36 2014 +0200
@@ -1088,6 +1088,6 @@
-- parse_sel_default_eqs
>> free_constructors_cmd);
-val _ = Context.>> (Context.map_theory Ctr_Sugar_Interpretation.init);
+val _ = Theory.setup Ctr_Sugar_Interpretation.init;
end;
--- a/src/HOL/Tools/Old_Datatype/old_datatype_data.ML Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_data.ML Tue Sep 09 20:51:36 2014 +0200
@@ -235,33 +235,6 @@
-(** document antiquotation **)
-
-val antiq_setup =
- Thy_Output.antiquotation @{binding datatype} (Args.type_name {proper = true, strict = true})
- (fn {source = src, context = ctxt, ...} => fn dtco =>
- let
- val thy = Proof_Context.theory_of ctxt;
- val (vs, cos) = the_spec thy dtco;
- val ty = Type (dtco, map TFree vs);
- val pretty_typ_bracket = Syntax.pretty_typ (Config.put pretty_priority 1001 ctxt);
- fun pretty_constr (co, tys) =
- Pretty.block (Pretty.breaks
- (Syntax.pretty_term ctxt (Const (co, tys ---> ty)) ::
- map pretty_typ_bracket tys));
- val pretty_datatype =
- Pretty.block
- (Pretty.keyword1 "datatype" :: Pretty.brk 1 ::
- Syntax.pretty_typ ctxt ty ::
- Pretty.str " =" :: Pretty.brk 1 ::
- flat (separate [Pretty.brk 1, Pretty.str "| "] (map (single o pretty_constr) cos)));
- in
- Thy_Output.output ctxt
- (Thy_Output.maybe_pretty_source (K (K pretty_datatype)) ctxt src [()])
- end);
-
-
-
(** abstract theory extensions relative to a datatype characterisation **)
structure Datatype_Interpretation = Interpretation
@@ -284,7 +257,7 @@
(** setup theory **)
-val _ = Theory.setup (antiq_setup #> Datatype_Interpretation.init);
+val _ = Theory.setup Datatype_Interpretation.init;
open Old_Datatype_Aux;