--- a/src/HOL/Datatype_Examples/Compat.thy Tue Sep 16 19:23:37 2014 +0200
+++ b/src/HOL/Datatype_Examples/Compat.thy Wed Sep 17 08:23:53 2014 +0200
@@ -5,15 +5,15 @@
Tests for compatibility with the old datatype package.
*)
-header \<open> Tests for Compatibility with the Old Datatype Package \<close>
+header {* Tests for Compatibility with the Old Datatype Package *}
theory Compat
imports Main
begin
-subsection \<open> Viewing and Registering New-Style Datatypes as Old-Style Ones \<close>
+subsection {* Viewing and Registering New-Style Datatypes as Old-Style Ones *}
-ML \<open>
+ML {*
fun check_len n xs label =
length xs = n orelse error ("Expected length " ^ string_of_int (length xs) ^ " for " ^ label);
@@ -22,22 +22,22 @@
fun get_descrs thy lens T_name =
(these (Option.map #descr (Old_Datatype_Data.get_info thy T_name)),
- these (Option.map #descr (BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Unfold_Nesting T_name)),
- these (Option.map #descr (BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Keep_Nesting T_name)))
+ these (Option.map #descr (BNF_LFP_Compat.get_info thy [] T_name)),
+ these (Option.map #descr (BNF_LFP_Compat.get_info thy [BNF_LFP_Compat.Keep_Nesting] T_name)))
|> tap (check_lens lens);
-\<close>
+*}
old_datatype 'a old_lst = Old_Nl | Old_Cns 'a "'a old_lst"
-ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name old_lst}; \<close>
+ML {* get_descrs @{theory} (1, 1, 1) @{type_name old_lst} *}
datatype 'a lst = Nl | Cns 'a "'a lst"
-ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name lst}; \<close>
+ML {* get_descrs @{theory} (0, 1, 1) @{type_name lst} *}
datatype_compat lst
-ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name lst}; \<close>
+ML {* get_descrs @{theory} (1, 1, 1) @{type_name lst} *}
datatype 'b w = W | W' "'b w \<times> 'b list"
@@ -45,190 +45,192 @@
datatype_compat w
*)
-ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name w}; \<close>
+ML {* get_descrs @{theory} (0, 1, 1) @{type_name w} *}
datatype ('c, 'b) s = L 'c | R 'b
-ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name s}; \<close>
+ML {* get_descrs @{theory} (0, 1, 1) @{type_name s} *}
datatype 'd x = X | X' "('d x lst, 'd list) s"
-ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name x}; \<close>
+ML {* get_descrs @{theory} (0, 1, 1) @{type_name x} *}
datatype_compat s
-ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name s}; \<close>
-ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name x}; \<close>
+ML {* get_descrs @{theory} (1, 1, 1) @{type_name s} *}
+ML {* get_descrs @{theory} (0, 1, 1) @{type_name x} *}
datatype_compat x
-ML \<open> get_descrs @{theory} (3, 3, 1) @{type_name x}; \<close>
+ML {* get_descrs @{theory} (3, 3, 1) @{type_name x} *}
thm x.induct x.rec
thm compat_x.induct compat_x.rec
datatype 'a tttre = TTTre 'a "'a tttre lst lst lst"
-ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name tttre}; \<close>
+ML {* get_descrs @{theory} (0, 1, 1) @{type_name tttre} *}
datatype_compat tttre
-ML \<open> get_descrs @{theory} (4, 4, 1) @{type_name tttre}; \<close>
+ML {* get_descrs @{theory} (4, 4, 1) @{type_name tttre} *}
thm tttre.induct tttre.rec
thm compat_tttre.induct compat_tttre.rec
datatype 'a ftre = FEmp | FTre "'a \<Rightarrow> 'a ftre lst"
-ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name ftre}; \<close>
+ML {* get_descrs @{theory} (0, 1, 1) @{type_name ftre} *}
datatype_compat ftre
-ML \<open> get_descrs @{theory} (2, 2, 1) @{type_name ftre}; \<close>
+ML {* get_descrs @{theory} (2, 2, 1) @{type_name ftre} *}
thm ftre.induct ftre.rec
thm compat_ftre.induct compat_ftre.rec
datatype 'a btre = BTre 'a "'a btre lst" "'a btre lst"
-ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name btre}; \<close>
+ML {* get_descrs @{theory} (0, 1, 1) @{type_name btre} *}
datatype_compat btre
-ML \<open> get_descrs @{theory} (3, 3, 1) @{type_name btre}; \<close>
+ML {* get_descrs @{theory} (3, 3, 1) @{type_name btre} *}
thm btre.induct btre.rec
thm compat_btre.induct compat_btre.rec
datatype 'a foo = Foo | Foo' 'a "'a bar" and 'a bar = Bar | Bar' 'a "'a foo"
-ML \<open> get_descrs @{theory} (0, 2, 2) @{type_name foo}; \<close>
-ML \<open> get_descrs @{theory} (0, 2, 2) @{type_name bar}; \<close>
+ML {* get_descrs @{theory} (0, 2, 2) @{type_name foo} *}
+ML {* get_descrs @{theory} (0, 2, 2) @{type_name bar} *}
datatype_compat foo bar
-ML \<open> get_descrs @{theory} (2, 2, 2) @{type_name foo}; \<close>
-ML \<open> get_descrs @{theory} (2, 2, 2) @{type_name bar}; \<close>
+ML {* get_descrs @{theory} (2, 2, 2) @{type_name foo} *}
+ML {* get_descrs @{theory} (2, 2, 2) @{type_name bar} *}
datatype 'a tre = Tre 'a "'a tre lst"
-ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name tre}; \<close>
+ML {* get_descrs @{theory} (0, 1, 1) @{type_name tre} *}
datatype_compat tre
-ML \<open> get_descrs @{theory} (2, 2, 1) @{type_name tre}; \<close>
+ML {* get_descrs @{theory} (2, 2, 1) @{type_name tre} *}
thm tre.induct tre.rec
thm compat_tre.induct compat_tre.rec
datatype 'a f = F 'a and 'a g = G 'a
-ML \<open> get_descrs @{theory} (0, 2, 2) @{type_name f}; \<close>
-ML \<open> get_descrs @{theory} (0, 2, 2) @{type_name g}; \<close>
+ML {* get_descrs @{theory} (0, 2, 2) @{type_name f} *}
+ML {* get_descrs @{theory} (0, 2, 2) @{type_name g} *}
datatype h = H "h f" | H'
-ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name h}; \<close>
+ML {* get_descrs @{theory} (0, 1, 1) @{type_name h} *}
datatype_compat f g
-ML \<open> get_descrs @{theory} (2, 2, 2) @{type_name f}; \<close>
-ML \<open> get_descrs @{theory} (2, 2, 2) @{type_name g}; \<close>
-ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name h}; \<close>
+ML {* get_descrs @{theory} (2, 2, 2) @{type_name f} *}
+ML {* get_descrs @{theory} (2, 2, 2) @{type_name g} *}
+ML {* get_descrs @{theory} (0, 1, 1) @{type_name h} *}
datatype_compat h
-ML \<open> get_descrs @{theory} (3, 3, 1) @{type_name h}; \<close>
+ML {* get_descrs @{theory} (3, 3, 1) @{type_name h} *}
thm h.induct h.rec
thm compat_h.induct compat_h.rec
datatype myunit = MyUnity
-ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name myunit}; \<close>
+ML {* get_descrs @{theory} (0, 1, 1) @{type_name myunit} *}
datatype_compat myunit
-ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name myunit}; \<close>
+ML {* get_descrs @{theory} (1, 1, 1) @{type_name myunit} *}
datatype mylist = MyNil | MyCons nat mylist
-ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name mylist}; \<close>
+ML {* get_descrs @{theory} (0, 1, 1) @{type_name mylist} *}
datatype_compat mylist
-ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name mylist}; \<close>
+ML {* get_descrs @{theory} (1, 1, 1) @{type_name mylist} *}
datatype foo' = FooNil | FooCons bar' foo' and bar' = Bar
-ML \<open> get_descrs @{theory} (0, 2, 2) @{type_name foo'}; \<close>
-ML \<open> get_descrs @{theory} (0, 2, 2) @{type_name bar'}; \<close>
+ML {* get_descrs @{theory} (0, 2, 2) @{type_name foo'} *}
+ML {* get_descrs @{theory} (0, 2, 2) @{type_name bar'} *}
datatype_compat bar' foo'
-ML \<open> get_descrs @{theory} (2, 2, 2) @{type_name foo'}; \<close>
-ML \<open> get_descrs @{theory} (2, 2, 2) @{type_name bar'}; \<close>
+ML {* get_descrs @{theory} (2, 2, 2) @{type_name foo'} *}
+ML {* get_descrs @{theory} (2, 2, 2) @{type_name bar'} *}
old_datatype funky = Funky "funky tre" | Funky'
-ML \<open> get_descrs @{theory} (3, 3, 3) @{type_name funky}; \<close>
+ML {* get_descrs @{theory} (3, 3, 3) @{type_name funky} *}
old_datatype fnky = Fnky "nat tre"
-ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name fnky}; \<close>
+ML {* get_descrs @{theory} (1, 1, 1) @{type_name fnky} *}
datatype tree = Tree "tree foo"
-ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name tree}; \<close>
+ML {* get_descrs @{theory} (0, 1, 1) @{type_name tree} *}
datatype_compat tree
-ML \<open> get_descrs @{theory} (3, 3, 1) @{type_name tree}; \<close>
+ML {* get_descrs @{theory} (3, 3, 1) @{type_name tree} *}
thm tree.induct tree.rec
thm compat_tree.induct compat_tree.rec
-subsection \<open> Creating New-Style Datatypes Using Old-Style Interfaces \<close>
+subsection {* Creating New-Style Datatypes Using Old-Style Interfaces *}
-ML \<open>
+ML {*
val l_specs =
[((@{binding l}, [("'a", @{sort type})], NoSyn),
[(@{binding N}, [], NoSyn),
- (@{binding C}, [@{typ 'a}, Type (Sign.full_name @{theory} @{binding l}, [@{typ 'a}])], NoSyn)])];
-\<close>
+ (@{binding C}, [@{typ 'a}, Type (Sign.full_name @{theory} @{binding l}, [@{typ 'a}])],
+ NoSyn)])];
+*}
-setup \<open> snd o BNF_LFP_Compat.add_datatype BNF_LFP_Compat.Unfold_Nesting l_specs; \<close>
+setup {* snd o BNF_LFP_Compat.add_datatype [] l_specs *}
-ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name l}; \<close>
+ML {* get_descrs @{theory} (1, 1, 1) @{type_name l} *}
thm l.exhaust l.map l.induct l.rec l.size
-ML \<open>
+ML {*
val t_specs =
[((@{binding t}, [("'b", @{sort type})], NoSyn),
- [(@{binding T}, [@{typ 'b}, Type (@{type_name l},
- [Type (Sign.full_name @{theory} @{binding t}, [@{typ 'b}])])], NoSyn)])];
-\<close>
+ [(@{binding T}, [@{typ 'b},
+ Type (@{type_name l}, [Type (Sign.full_name @{theory} @{binding t}, [@{typ 'b}])])],
+ NoSyn)])];
+*}
-setup \<open> snd o BNF_LFP_Compat.add_datatype BNF_LFP_Compat.Unfold_Nesting t_specs; \<close>
+setup {* snd o BNF_LFP_Compat.add_datatype [] t_specs *}
-ML \<open> get_descrs @{theory} (2, 2, 1) @{type_name t}; \<close>
+ML {* get_descrs @{theory} (2, 2, 1) @{type_name t} *}
thm t.exhaust t.map t.induct t.rec t.size
thm compat_t.induct compat_t.rec
-ML \<open>
+ML {*
val ft_specs =
[((@{binding ft}, [("'a", @{sort type})], NoSyn),
[(@{binding FT0}, [], NoSyn),
(@{binding FT}, [@{typ 'a} --> Type (Sign.full_name @{theory} @{binding ft}, [@{typ 'a}])],
NoSyn)])];
-\<close>
+*}
-setup \<open> snd o BNF_LFP_Compat.add_datatype BNF_LFP_Compat.Unfold_Nesting ft_specs; \<close>
+setup {* snd o BNF_LFP_Compat.add_datatype [] ft_specs *}
-ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name ft}; \<close>
+ML {* get_descrs @{theory} (1, 1, 1) @{type_name ft} *}
thm ft.exhaust ft.induct ft.rec ft.size
thm compat_ft.induct compat_ft.rec
--- a/src/HOL/Library/refute.ML Tue Sep 16 19:23:37 2014 +0200
+++ b/src/HOL/Library/refute.ML Wed Sep 17 08:23:53 2014 +0200
@@ -416,8 +416,7 @@
fun is_IDT_recursor thy (s, _) =
let
- val rec_names = Symtab.fold (append o #rec_names o snd)
- (BNF_LFP_Compat.get_all thy BNF_LFP_Compat.Unfold_Nesting) []
+ val rec_names = Symtab.fold (append o #rec_names o snd) (BNF_LFP_Compat.get_all thy []) []
in
(* I'm not quite sure if checking the name 's' is sufficient, *)
(* or if we should also check the type 'T'. *)
@@ -690,7 +689,7 @@
(* axiomatic type classes *)
| Type (@{type_name itself}, [T1]) => collect_type_axioms T1 axs
| Type (s, Ts) =>
- (case BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Unfold_Nesting s of
+ (case BNF_LFP_Compat.get_info thy [] s of
SOME _ => (* inductive datatype *)
(* only collect relevant type axioms for the argument types *)
fold collect_type_axioms Ts axs
@@ -819,7 +818,7 @@
| Type (@{type_name prop}, []) => acc
| Type (@{type_name set}, [T1]) => collect_types T1 acc
| Type (s, Ts) =>
- (case BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Unfold_Nesting s of
+ (case BNF_LFP_Compat.get_info thy [] s of
SOME info => (* inductive datatype *)
let
val index = #index info
@@ -1014,7 +1013,7 @@
(* TODO: no warning needed for /positive/ occurrences of IDTs *)
val maybe_spurious = Library.exists (fn
Type (s, _) =>
- (case BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Unfold_Nesting s of
+ (case BNF_LFP_Compat.get_info thy [] s of
SOME info => (* inductive datatype *)
let
val index = #index info
@@ -1740,7 +1739,7 @@
val thy = Proof_Context.theory_of ctxt
val (typs, terms) = model
fun interpret_term (Type (s, Ts)) =
- (case BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Unfold_Nesting s of
+ (case BNF_LFP_Compat.get_info thy [] s of
SOME info => (* inductive datatype *)
let
(* only recursive IDTs have an associated depth *)
@@ -1865,7 +1864,7 @@
HOLogic_empty_set) pairss
end
| Type (s, Ts) =>
- (case BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Unfold_Nesting s of
+ (case BNF_LFP_Compat.get_info thy [] s of
SOME info =>
(case AList.lookup (op =) typs T of
SOME 0 =>
@@ -1931,7 +1930,7 @@
Const (s, T) =>
(case body_type T of
Type (s', Ts') =>
- (case BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Unfold_Nesting s' of
+ (case BNF_LFP_Compat.get_info thy [] s' of
SOME info => (* body type is an inductive datatype *)
let
val index = #index info
@@ -2403,7 +2402,7 @@
end
else
NONE (* not a recursion operator of this datatype *)
- ) (BNF_LFP_Compat.get_all thy BNF_LFP_Compat.Unfold_Nesting) NONE
+ ) (BNF_LFP_Compat.get_all thy []) NONE
| _ => (* head of term is not a constant *)
NONE
end;
@@ -2837,7 +2836,7 @@
in
(case T of
Type (s, Ts) =>
- (case BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Unfold_Nesting s of
+ (case BNF_LFP_Compat.get_info thy [] s of
SOME info => (* inductive datatype *)
let
val (typs, _) = model
@@ -3003,4 +3002,3 @@
in thy' end)));
end;
-
--- a/src/HOL/Nominal/nominal_atoms.ML Tue Sep 16 19:23:37 2014 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML Wed Sep 17 08:23:53 2014 +0200
@@ -100,9 +100,9 @@
val (_,thy1) =
fold_map (fn ak => fn thy =>
let val dt = ((Binding.name ak, [], NoSyn), [(Binding.name ak, [@{typ nat}], NoSyn)])
- val (dt_names, thy1) = BNF_LFP_Compat.add_datatype_dead BNF_LFP_Compat.Unfold_Nesting [dt] thy;
+ val (dt_names, thy1) = BNF_LFP_Compat.add_datatype [BNF_LFP_Compat.Kill_Type_Args] [dt] thy;
- val injects = maps (#inject o BNF_LFP_Compat.the_info thy1 BNF_LFP_Compat.Unfold_Nesting) dt_names;
+ val injects = maps (#inject o BNF_LFP_Compat.the_info thy1 []) dt_names;
val ak_type = Type (Sign.intern_type thy1 ak,[])
val ak_sign = Sign.intern_const thy1 ak
--- a/src/HOL/Nominal/nominal_datatype.ML Tue Sep 16 19:23:37 2014 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Wed Sep 17 08:23:53 2014 +0200
@@ -200,9 +200,9 @@
val new_type_names' = map (fn n => n ^ "_Rep") new_type_names;
- val (full_new_type_names',thy1) = BNF_LFP_Compat.add_datatype_dead BNF_LFP_Compat.Unfold_Nesting dts'' thy;
+ val (full_new_type_names',thy1) = BNF_LFP_Compat.add_datatype [BNF_LFP_Compat.Kill_Type_Args] dts'' thy;
- val {descr, induct, ...} = BNF_LFP_Compat.the_info thy1 BNF_LFP_Compat.Unfold_Nesting (hd full_new_type_names');
+ val {descr, induct, ...} = BNF_LFP_Compat.the_info thy1 [] (hd full_new_type_names');
fun nth_dtyp i = Old_Datatype_Aux.typ_of_dtyp descr (Old_Datatype_Aux.DtRec i);
val big_name = space_implode "_" new_type_names;
--- a/src/HOL/SPARK/Tools/spark_vcs.ML Tue Sep 16 19:23:37 2014 +0200
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML Wed Sep 17 08:23:53 2014 +0200
@@ -173,7 +173,7 @@
fun add_enum_type tyname tyname' thy =
let
- val {case_name, ...} = the (BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Keep_Nesting tyname');
+ val {case_name, ...} = the (BNF_LFP_Compat.get_info thy [BNF_LFP_Compat.Keep_Nesting] tyname');
val cs = map Const (the (BNF_LFP_Compat.get_constrs thy tyname'));
val k = length cs;
val T = Type (tyname', []);
@@ -210,7 +210,7 @@
rtac @{thm subset_antisym} 1 THEN
rtac @{thm subsetI} 1 THEN
Old_Datatype_Aux.exh_tac (K (#exhaust (BNF_LFP_Compat.the_info
- (Proof_Context.theory_of lthy) BNF_LFP_Compat.Keep_Nesting tyname'))) 1 THEN
+ (Proof_Context.theory_of lthy) [BNF_LFP_Compat.Keep_Nesting] tyname'))) 1 THEN
ALLGOALS (asm_full_simp_tac lthy));
val finite_UNIV = Goal.prove lthy [] []
@@ -320,7 +320,7 @@
val tyname = Sign.full_name thy tyb
in
(thy |>
- BNF_LFP_Compat.add_datatype BNF_LFP_Compat.Keep_Nesting
+ BNF_LFP_Compat.add_datatype [BNF_LFP_Compat.Keep_Nesting]
[((tyb, [], NoSyn),
map (fn s => (Binding.name s, [], NoSyn)) els)] |> snd |>
add_enum_type s tyname,
--- a/src/HOL/Statespace/state_fun.ML Tue Sep 16 19:23:37 2014 +0200
+++ b/src/HOL/Statespace/state_fun.ML Wed Sep 17 08:23:53 2014 +0200
@@ -338,7 +338,7 @@
| mkName (TFree (x,_)) = mkUpper (Long_Name.base_name x)
| mkName (TVar ((x,_),_)) = mkUpper (Long_Name.base_name x);
-fun is_datatype thy = is_some o BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Keep_Nesting;
+fun is_datatype thy = is_some o BNF_LFP_Compat.get_info thy [BNF_LFP_Compat.Keep_Nesting];
fun mk_map @{type_name List.list} = Syntax.const @{const_name List.map}
| mk_map n = Syntax.const ("StateFun.map_" ^ Long_Name.base_name n);
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Tue Sep 16 19:23:37 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Wed Sep 17 08:23:53 2014 +0200
@@ -10,25 +10,22 @@
signature BNF_LFP_COMPAT =
sig
- datatype nesting_preference = Keep_Nesting | Unfold_Nesting
+ datatype preference = Keep_Nesting | Include_GFPs | Kill_Type_Args
- val get_all: theory -> nesting_preference -> Old_Datatype_Aux.info Symtab.table
- val get_info: theory -> nesting_preference -> string -> Old_Datatype_Aux.info option
- val the_info: theory -> nesting_preference -> string -> Old_Datatype_Aux.info
+ val get_all: theory -> preference list -> Old_Datatype_Aux.info Symtab.table
+ val get_info: theory -> preference list -> string -> Old_Datatype_Aux.info option
+ val the_info: theory -> preference list -> string -> Old_Datatype_Aux.info
val the_spec: theory -> string -> (string * sort) list * (string * typ list) list
- val the_descr: theory -> nesting_preference -> string list ->
+ val the_descr: theory -> preference list -> string list ->
Old_Datatype_Aux.descr * (string * sort) list * string list * string
* (string list * string list) * (typ list * typ list)
val get_constrs: theory -> string -> (string * typ) list option
- val interpretation: string -> nesting_preference ->
+ val interpretation: string -> preference list ->
(Old_Datatype_Aux.config -> string list -> theory -> theory) -> theory -> theory
val datatype_compat: string list -> local_theory -> local_theory
val datatype_compat_global: string list -> theory -> theory
val datatype_compat_cmd: string list -> local_theory -> local_theory
- val add_datatype: nesting_preference -> Old_Datatype_Aux.spec list -> theory ->
- string list * theory
- val add_datatype_dead: nesting_preference -> Old_Datatype_Aux.spec list -> theory ->
- string list * theory
+ val add_datatype: preference list -> Old_Datatype_Aux.spec list -> theory -> string list * theory
val add_primrec: (binding * typ option * mixfix) list -> (Attrib.binding * term) list ->
local_theory -> (term list * thm list) * local_theory
val add_primrec_global: (binding * typ option * mixfix) list ->
@@ -54,7 +51,7 @@
val compat_N = "compat_";
val rec_split_N = "rec_split_";
-datatype nesting_preference = Keep_Nesting | Unfold_Nesting;
+datatype preference = Keep_Nesting | Include_GFPs | Kill_Type_Args;
fun mk_split_rec_rhs ctxt fpTs Cs (recs as rec1 :: _) =
let
@@ -206,7 +203,7 @@
map (fn (_, (s, Ds, sDss)) => (s, map perm_dtyp Ds, map (apsnd (map perm_dtyp)) sDss)) desc
end;
-fun mk_infos_of_mutually_recursive_new_datatypes nesting_pref check_names fpT_names0 lthy =
+fun mk_infos_of_mutually_recursive_new_datatypes prefs check_names fpT_names0 lthy =
let
val thy = Proof_Context.theory_of lthy;
@@ -214,13 +211,15 @@
fun not_mutually_recursive ss =
error ("{" ^ commas ss ^ "} is not a complete set of mutually recursive datatypes");
- fun lfp_sugar_of s =
+ fun checked_fp_sugar_of s =
(case fp_sugar_of lthy s of
- SOME (fp_sugar as {fp = Least_FP, ...}) => fp_sugar
- | _ => not_datatype s);
+ SOME (fp_sugar as {fp, ...}) =>
+ if member (op =) prefs Include_GFPs orelse fp = Least_FP then fp_sugar else not_datatype s
+ | NONE => not_datatype s);
val fpTs0 as Type (_, var_As) :: _ =
- map (#T o lfp_sugar_of o fst o dest_Type) (#Ts (#fp_res (lfp_sugar_of (hd fpT_names0))));
+ map (#T o checked_fp_sugar_of o fst o dest_Type)
+ (#Ts (#fp_res (checked_fp_sugar_of (hd fpT_names0))));
val fpT_names = map (fst o dest_Type) fpTs0;
val _ = check_names (op =) (fpT_names0, fpT_names) orelse not_mutually_recursive fpT_names0;
@@ -237,11 +236,11 @@
fun mk_typ_descr index (Type (T_name, Ts)) ({ctrs, ...} : ctr_sugar) =
(index, (T_name, map mk_dtyp Ts, map (mk_ctr_descr Ts) ctrs));
- val fp_ctr_sugars = map (#ctr_sugar o lfp_sugar_of) fpT_names;
+ val fp_ctr_sugars = map (#ctr_sugar o checked_fp_sugar_of) fpT_names;
val orig_descr = map3 mk_typ_descr (0 upto nn_fp - 1) fpTs fp_ctr_sugars;
val all_infos = Old_Datatype_Data.get_all thy;
val (orig_descr' :: nested_descrs) =
- if nesting_pref = Keep_Nesting then [orig_descr]
+ if member (op =) prefs Keep_Nesting then [orig_descr]
else fst (Old_Datatype_Aux.unfold_datatypes lthy orig_descr all_infos orig_descr nn_fp);
fun cliquify_descr [] = []
@@ -269,7 +268,7 @@
val fpTs' = Old_Datatype_Aux.get_rec_types descr;
val nn = length fpTs';
- val fp_sugars = map (lfp_sugar_of o fst o dest_Type) fpTs';
+ val fp_sugars = map (checked_fp_sugar_of o fst o dest_Type) fpTs';
val ctr_Tsss = map (map (map (Old_Datatype_Aux.typ_of_dtyp descr) o snd) o #3 o snd) descr;
val kkssss = map (map (map body_rec_indices o snd) o #3 o snd) descr;
@@ -297,8 +296,8 @@
val Xs' = map #X fp_sugars';
val ctrXs_Tsss' = map (map (map substAT) o #ctrXs_Tss) fp_sugars';
val ctrss' = map2 mk_ctr_of fp_sugars' fpTs';
- val {common_co_inducts = [induct], ...} :: _ = fp_sugars';
- val inducts = map (the_single o #co_inducts) fp_sugars';
+ val {common_co_inducts = induct :: _, ...} :: _ = fp_sugars';
+ val inducts = map (hd o #co_inducts) fp_sugars';
val recs = map #co_rec fp_sugars';
val rec_thmss = map #co_rec_thms fp_sugars';
@@ -306,14 +305,14 @@
| is_nested_rec_type _ = false;
val ((lfp_sugar_thms'', (inducts', induct', recs', rec'_thmss)), lthy'') =
- if nesting_pref = Unfold_Nesting andalso
- exists (exists (exists is_nested_rec_type)) ctrXs_Tsss' then
+ if member (op =) prefs Keep_Nesting orelse
+ not (exists (exists (exists is_nested_rec_type)) ctrXs_Tsss') then
+ ((lfp_sugar_thms', (inducts, induct, recs, rec_thmss)), lthy')
+ else
define_split_rec_derive_induct_rec_thms Xs' fpTs' ctrXs_Tsss' ctrss' inducts induct recs
rec_thmss lthy'
|>> `(fn (inducts', induct', _, rec'_thmss) =>
- SOME ((inducts', induct', mk_induct_attrs ctrss'), (rec'_thmss, [])))
- else
- ((lfp_sugar_thms', (inducts, induct, recs, rec_thmss)), lthy');
+ SOME ((inducts', induct', mk_induct_attrs ctrss'), (rec'_thmss, [])));
val rec'_names = map (fst o dest_Const) recs';
val rec'_thms = flat rec'_thmss;
@@ -332,53 +331,58 @@
(nn, b_names, compat_b_names, lfp_sugar_thms'', infos, lthy'')
end;
-fun infos_of_new_datatype_mutual_cluster lthy fpT_name =
- #5 (mk_infos_of_mutually_recursive_new_datatypes Keep_Nesting subset [fpT_name] lthy)
+fun infos_of_new_datatype_mutual_cluster lthy prefs fpT_name =
+ #5 (mk_infos_of_mutually_recursive_new_datatypes prefs subset [fpT_name] lthy)
handle ERROR _ => [];
-fun get_all thy nesting_pref =
+fun get_all thy prefs =
let
val lthy = Proof_Context.init_global thy;
val old_info_tab = Old_Datatype_Data.get_all thy;
val new_T_names = BNF_FP_Def_Sugar.fp_sugars_of_global thy
|> map_filter (try (fn {T = Type (s, _), fp_res_index = 0, ...} => s));
- val new_infos = maps (infos_of_new_datatype_mutual_cluster lthy) new_T_names;
+ val new_infos =
+ maps (infos_of_new_datatype_mutual_cluster lthy (insert (op =) Keep_Nesting prefs))
+ new_T_names;
in
- fold (if nesting_pref = Keep_Nesting then Symtab.update else Symtab.default) new_infos
+ fold (if member (op =) prefs Keep_Nesting then Symtab.update else Symtab.default) new_infos
old_info_tab
end;
-fun get_one get_old get_new thy nesting_pref x =
- let val (get_fst, get_snd) = (get_old thy, get_new thy) |> nesting_pref = Keep_Nesting ? swap in
+fun get_one get_old get_new thy prefs x =
+ let
+ val (get_fst, get_snd) = (get_old thy, get_new thy) |> member (op =) prefs Keep_Nesting ? swap;
+ in
(case get_fst x of NONE => get_snd x | res => res)
end;
-fun get_info_of_new_datatype thy T_name =
+fun get_info_of_new_datatype prefs thy T_name =
let val lthy = Proof_Context.init_global thy in
- AList.lookup (op =) (infos_of_new_datatype_mutual_cluster lthy T_name) T_name
+ AList.lookup (op =) (infos_of_new_datatype_mutual_cluster lthy prefs T_name) T_name
end;
-val get_info = get_one Old_Datatype_Data.get_info get_info_of_new_datatype;
+fun get_info thy prefs =
+ get_one Old_Datatype_Data.get_info (get_info_of_new_datatype prefs) thy prefs;
-fun the_info thy nesting_pref T_name =
- (case get_info thy nesting_pref T_name of
+fun the_info thy prefs T_name =
+ (case get_info thy prefs T_name of
SOME info => info
| NONE => error ("Unknown datatype " ^ quote T_name));
fun the_spec thy T_name =
let
- val {descr, index, ...} = the_info thy Keep_Nesting T_name;
+ val {descr, index, ...} = the_info thy [Keep_Nesting, Include_GFPs] T_name;
val (_, Ds, ctrs0) = the (AList.lookup (op =) descr index);
val tfrees = map Old_Datatype_Aux.dest_DtTFree Ds;
val ctrs = map (apsnd (map (Old_Datatype_Aux.typ_of_dtyp descr))) ctrs0;
in (tfrees, ctrs) end;
-fun the_descr thy nesting_pref (T_names0 as T_name01 :: _) =
+fun the_descr thy prefs (T_names0 as T_name01 :: _) =
let
fun not_mutually_recursive ss =
error ("{" ^ commas ss ^ "} is not a complete set of mutually recursive datatypes");
- val info = the_info thy nesting_pref T_name01;
+ val info = the_info thy prefs T_name01;
val descr = #descr info;
val (_, Ds, _) = the (AList.lookup (op =) descr (#index info));
@@ -420,25 +424,26 @@
map (apsnd mk_ctr_typ) ctrs
end);
-fun old_interpretation_of nesting_pref f config T_names thy =
- if nesting_pref = Unfold_Nesting orelse exists (is_none o fp_sugar_of_global thy) T_names then
+fun old_interpretation_of prefs f config T_names thy =
+ if not (member (op =) prefs Keep_Nesting) orelse
+ exists (is_none o fp_sugar_of_global thy) T_names then
f config T_names thy
else
thy;
-fun new_interpretation_of nesting_pref f (fp_sugars : fp_sugar list) thy =
+fun new_interpretation_of prefs f (fp_sugars : fp_sugar list) thy =
let val T_names = map (fst o dest_Type o #T) fp_sugars in
- if forall (curry (op =) Least_FP o #fp) fp_sugars andalso
- (nesting_pref = Keep_Nesting orelse
+ if (member (op =) prefs Include_GFPs orelse forall (curry (op =) Least_FP o #fp) fp_sugars)
+ andalso (member (op =) prefs Keep_Nesting orelse
exists (is_none o Old_Datatype_Data.get_info thy) T_names) then
f Old_Datatype_Aux.default_config T_names thy
else
thy
end;
-fun interpretation name nesting_pref f =
- let val new_f = new_interpretation_of nesting_pref f in
- Old_Datatype_Data.interpretation (old_interpretation_of nesting_pref f)
+fun interpretation name prefs f =
+ let val new_f = new_interpretation_of prefs f in
+ Old_Datatype_Data.interpretation (old_interpretation_of prefs f)
#> fp_sugars_interpretation name new_f (Local_Theory.background_theory o new_f)
end;
@@ -447,7 +452,7 @@
fun datatype_compat fpT_names lthy =
let
val (nn, b_names, compat_b_names, lfp_sugar_thms, infos, lthy') =
- mk_infos_of_mutually_recursive_new_datatypes Unfold_Nesting eq_set fpT_names lthy;
+ mk_infos_of_mutually_recursive_new_datatypes [] eq_set fpT_names lthy;
val all_notes =
(case lfp_sugar_thms of
@@ -498,12 +503,13 @@
datatype_compat fpT_names lthy
end;
-fun gen_add_datatype live nesting_pref old_specs thy =
+fun add_datatype prefs old_specs thy =
let
val fpT_names = map (Sign.full_name thy o #1 o fst) old_specs;
fun new_type_args_of (s, S) =
- (if live then SOME Binding.empty else NONE, (TFree (s, @{sort type}), S));
+ (if member (op =) prefs Kill_Type_Args then NONE else SOME Binding.empty,
+ (TFree (s, @{sort type}), S));
fun new_ctr_spec_of (b, Ts, mx) = (((Binding.empty, b), map (pair Binding.empty) Ts), mx);
fun new_spec_of ((b, old_tyargs, mx), old_ctr_specs) =
@@ -515,12 +521,9 @@
(fpT_names,
thy
|> map_local_theory (co_datatypes Least_FP construct_lfp (default_ctr_options, new_specs))
- |> nesting_pref = Unfold_Nesting ? perhaps (try (datatype_compat_global fpT_names)))
+ |> not (member (op =) prefs Keep_Nesting) ? perhaps (try (datatype_compat_global fpT_names)))
end;
-val add_datatype = gen_add_datatype true;
-val add_datatype_dead = gen_add_datatype false;
-
val add_primrec = apfst (apsnd flat) ooo BNF_LFP_Rec_Sugar.add_primrec;
val add_primrec_global = apfst (apsnd flat) ooo BNF_LFP_Rec_Sugar.add_primrec_global;
val add_primrec_overloaded = apfst (apsnd flat) oooo BNF_LFP_Rec_Sugar.add_primrec_overloaded;
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Tue Sep 16 19:23:37 2014 +0200
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Wed Sep 17 08:23:53 2014 +0200
@@ -263,7 +263,8 @@
let
val cnstrs = flat (maps
(map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd)
- (Symtab.dest (BNF_LFP_Compat.get_all (Proof_Context.theory_of ctxt) BNF_LFP_Compat.Keep_Nesting)))
+ (Symtab.dest (BNF_LFP_Compat.get_all (Proof_Context.theory_of ctxt)
+ Quickcheck_Common.compat_prefs)))
fun is_constrt (Const (s, T), ts) = (case (AList.lookup (op =) cnstrs s, body_type T) of
(SOME (i, Tname), Type (Tname', _)) => length ts = i andalso Tname = Tname'
| _ => false)
@@ -547,10 +548,11 @@
(@{sort exhaustive}, instantiate_exhaustive_datatype)
val setup_bounded_forall_datatype_interpretation =
- BNF_LFP_Compat.interpretation bounded_forall_plugin BNF_LFP_Compat.Keep_Nesting
+ BNF_LFP_Compat.interpretation bounded_forall_plugin Quickcheck_Common.compat_prefs
(Quickcheck_Common.ensure_sort
(((@{sort type}, @{sort type}), @{sort bounded_forall}),
- (fn thy => BNF_LFP_Compat.the_descr thy BNF_LFP_Compat.Keep_Nesting, instantiate_bounded_forall_datatype)))
+ (fn thy => BNF_LFP_Compat.the_descr thy Quickcheck_Common.compat_prefs,
+ instantiate_bounded_forall_datatype)))
val active = Attrib.setup_config_bool @{binding quickcheck_exhaustive_active} (K true);
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Tue Sep 16 19:23:37 2014 +0200
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Wed Sep 17 08:23:53 2014 +0200
@@ -6,6 +6,7 @@
signature QUICKCHECK_COMMON =
sig
+ val compat_prefs : BNF_LFP_Compat.preference list
val strip_imp : term -> (term list * term)
val reflect_bool : bool -> term
val define_functions : ((term list -> term list) * (Proof.context -> tactic) option)
@@ -46,6 +47,8 @@
(* static options *)
+val compat_prefs = [BNF_LFP_Compat.Keep_Nesting, BNF_LFP_Compat.Include_GFPs]
+
val define_foundationally = false
(* HOLogic's term functions *)
@@ -420,10 +423,10 @@
fun ensure_common_sort_datatype (sort, instantiate) =
ensure_sort (((@{sort typerep}, @{sort term_of}), sort),
- (fn thy => BNF_LFP_Compat.the_descr thy BNF_LFP_Compat.Keep_Nesting, instantiate))
+ (fn thy => BNF_LFP_Compat.the_descr thy compat_prefs, instantiate))
fun datatype_interpretation name =
- BNF_LFP_Compat.interpretation name BNF_LFP_Compat.Keep_Nesting o ensure_common_sort_datatype
+ BNF_LFP_Compat.interpretation name compat_prefs o ensure_common_sort_datatype
(** generic parametric compilation **)
--- a/src/HOL/Tools/TFL/casesplit.ML Tue Sep 16 19:23:37 2014 +0200
+++ b/src/HOL/Tools/TFL/casesplit.ML Wed Sep 17 08:23:53 2014 +0200
@@ -24,7 +24,7 @@
Type(ty_str, _) => ty_str
| TFree(s,_) => error ("Free type: " ^ s)
| TVar((s,i),_) => error ("Free variable: " ^ s)
- val {induct, ...} = BNF_LFP_Compat.the_info thy BNF_LFP_Compat.Keep_Nesting ty_str
+ val {induct, ...} = BNF_LFP_Compat.the_info thy [BNF_LFP_Compat.Keep_Nesting] ty_str
in
cases_thm_of_induct_thm induct
end;
--- a/src/HOL/Tools/TFL/tfl.ML Tue Sep 16 19:23:37 2014 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML Wed Sep 17 08:23:53 2014 +0200
@@ -435,7 +435,7 @@
put_simpset HOL_basic_ss ctxt
addsimps case_rewrites
|> fold (Simplifier.add_cong o #case_cong_weak o snd)
- (Symtab.dest (BNF_LFP_Compat.get_all theory BNF_LFP_Compat.Keep_Nesting))
+ (Symtab.dest (BNF_LFP_Compat.get_all theory [BNF_LFP_Compat.Keep_Nesting]))
val corollaries' = map (Simplifier.simplify case_simpset) corollaries
val extract = Rules.CONTEXT_REWRITE_RULE
(f, [R], @{thm cut_apply}, meta_tflCongs @ context_congs)
--- a/src/HOL/Tools/TFL/thry.ML Tue Sep 16 19:23:37 2014 +0200
+++ b/src/HOL/Tools/TFL/thry.ML Wed Sep 17 08:23:53 2014 +0200
@@ -58,20 +58,20 @@
*---------------------------------------------------------------------------*)
fun match_info thy dtco =
- case (BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Keep_Nesting dtco,
+ case (BNF_LFP_Compat.get_info thy [BNF_LFP_Compat.Keep_Nesting] dtco,
BNF_LFP_Compat.get_constrs thy dtco) of
(SOME {case_name, ... }, SOME constructors) =>
SOME {case_const = Const (case_name, Sign.the_const_type thy case_name), constructors = map Const constructors}
| _ => NONE;
-fun induct_info thy dtco = case BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Keep_Nesting dtco of
+fun induct_info thy dtco = case BNF_LFP_Compat.get_info thy [BNF_LFP_Compat.Keep_Nesting] dtco of
NONE => NONE
| SOME {nchotomy, ...} =>
SOME {nchotomy = nchotomy,
constructors = (map Const o the o BNF_LFP_Compat.get_constrs thy) dtco};
fun extract_info thy =
- let val infos = map snd (Symtab.dest (BNF_LFP_Compat.get_all thy BNF_LFP_Compat.Keep_Nesting))
+ let val infos = map snd (Symtab.dest (BNF_LFP_Compat.get_all thy [BNF_LFP_Compat.Keep_Nesting]))
in {case_congs = map (mk_meta_eq o #case_cong) infos,
case_rewrites = maps (map mk_meta_eq o #case_rewrites) infos}
end;
--- a/src/HOL/Tools/datatype_realizer.ML Tue Sep 16 19:23:37 2014 +0200
+++ b/src/HOL/Tools/datatype_realizer.ML Wed Sep 17 08:23:53 2014 +0200
@@ -233,7 +233,7 @@
else
let
val _ = Old_Datatype_Aux.message config "Adding realizers for induction and case analysis ...";
- val infos = map (BNF_LFP_Compat.the_info thy BNF_LFP_Compat.Unfold_Nesting) names;
+ val infos = map (BNF_LFP_Compat.the_info thy []) names;
val info :: _ = infos;
in
thy
@@ -241,7 +241,6 @@
|> fold_rev (perhaps o try o make_casedists) infos
end;
-val _ = Theory.setup (BNF_LFP_Compat.interpretation extraction_plugin BNF_LFP_Compat.Unfold_Nesting
- add_dt_realizers);
+val _ = Theory.setup (BNF_LFP_Compat.interpretation extraction_plugin [] add_dt_realizers);
end;