# HG changeset patch # User blanchet # Date 1410935033 -7200 # Node ID 04ac60da613e3afe344ce9e1798a75b21fcc1d46 # Parent c9f374b64d994d8eebca5f72375eda8fd87f1238 support (finite values of) codatatypes in Quickcheck diff -r c9f374b64d99 -r 04ac60da613e src/HOL/Datatype_Examples/Compat.thy --- 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 \ Tests for Compatibility with the Old Datatype Package \ +header {* Tests for Compatibility with the Old Datatype Package *} theory Compat imports Main begin -subsection \ Viewing and Registering New-Style Datatypes as Old-Style Ones \ +subsection {* Viewing and Registering New-Style Datatypes as Old-Style Ones *} -ML \ +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); -\ +*} old_datatype 'a old_lst = Old_Nl | Old_Cns 'a "'a old_lst" -ML \ get_descrs @{theory} (1, 1, 1) @{type_name old_lst}; \ +ML {* get_descrs @{theory} (1, 1, 1) @{type_name old_lst} *} datatype 'a lst = Nl | Cns 'a "'a lst" -ML \ get_descrs @{theory} (0, 1, 1) @{type_name lst}; \ +ML {* get_descrs @{theory} (0, 1, 1) @{type_name lst} *} datatype_compat lst -ML \ get_descrs @{theory} (1, 1, 1) @{type_name lst}; \ +ML {* get_descrs @{theory} (1, 1, 1) @{type_name lst} *} datatype 'b w = W | W' "'b w \ 'b list" @@ -45,190 +45,192 @@ datatype_compat w *) -ML \ get_descrs @{theory} (0, 1, 1) @{type_name w}; \ +ML {* get_descrs @{theory} (0, 1, 1) @{type_name w} *} datatype ('c, 'b) s = L 'c | R 'b -ML \ get_descrs @{theory} (0, 1, 1) @{type_name s}; \ +ML {* get_descrs @{theory} (0, 1, 1) @{type_name s} *} datatype 'd x = X | X' "('d x lst, 'd list) s" -ML \ get_descrs @{theory} (0, 1, 1) @{type_name x}; \ +ML {* get_descrs @{theory} (0, 1, 1) @{type_name x} *} datatype_compat s -ML \ get_descrs @{theory} (1, 1, 1) @{type_name s}; \ -ML \ get_descrs @{theory} (0, 1, 1) @{type_name x}; \ +ML {* get_descrs @{theory} (1, 1, 1) @{type_name s} *} +ML {* get_descrs @{theory} (0, 1, 1) @{type_name x} *} datatype_compat x -ML \ get_descrs @{theory} (3, 3, 1) @{type_name x}; \ +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 \ get_descrs @{theory} (0, 1, 1) @{type_name tttre}; \ +ML {* get_descrs @{theory} (0, 1, 1) @{type_name tttre} *} datatype_compat tttre -ML \ get_descrs @{theory} (4, 4, 1) @{type_name tttre}; \ +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 \ 'a ftre lst" -ML \ get_descrs @{theory} (0, 1, 1) @{type_name ftre}; \ +ML {* get_descrs @{theory} (0, 1, 1) @{type_name ftre} *} datatype_compat ftre -ML \ get_descrs @{theory} (2, 2, 1) @{type_name ftre}; \ +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 \ get_descrs @{theory} (0, 1, 1) @{type_name btre}; \ +ML {* get_descrs @{theory} (0, 1, 1) @{type_name btre} *} datatype_compat btre -ML \ get_descrs @{theory} (3, 3, 1) @{type_name btre}; \ +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 \ get_descrs @{theory} (0, 2, 2) @{type_name foo}; \ -ML \ get_descrs @{theory} (0, 2, 2) @{type_name bar}; \ +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 \ get_descrs @{theory} (2, 2, 2) @{type_name foo}; \ -ML \ get_descrs @{theory} (2, 2, 2) @{type_name bar}; \ +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 \ get_descrs @{theory} (0, 1, 1) @{type_name tre}; \ +ML {* get_descrs @{theory} (0, 1, 1) @{type_name tre} *} datatype_compat tre -ML \ get_descrs @{theory} (2, 2, 1) @{type_name tre}; \ +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 \ get_descrs @{theory} (0, 2, 2) @{type_name f}; \ -ML \ get_descrs @{theory} (0, 2, 2) @{type_name g}; \ +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 \ get_descrs @{theory} (0, 1, 1) @{type_name h}; \ +ML {* get_descrs @{theory} (0, 1, 1) @{type_name h} *} datatype_compat f g -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}; \ +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 \ get_descrs @{theory} (3, 3, 1) @{type_name h}; \ +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 \ get_descrs @{theory} (0, 1, 1) @{type_name myunit}; \ +ML {* get_descrs @{theory} (0, 1, 1) @{type_name myunit} *} datatype_compat myunit -ML \ get_descrs @{theory} (1, 1, 1) @{type_name myunit}; \ +ML {* get_descrs @{theory} (1, 1, 1) @{type_name myunit} *} datatype mylist = MyNil | MyCons nat mylist -ML \ get_descrs @{theory} (0, 1, 1) @{type_name mylist}; \ +ML {* get_descrs @{theory} (0, 1, 1) @{type_name mylist} *} datatype_compat mylist -ML \ get_descrs @{theory} (1, 1, 1) @{type_name mylist}; \ +ML {* get_descrs @{theory} (1, 1, 1) @{type_name mylist} *} datatype foo' = FooNil | FooCons bar' foo' and bar' = Bar -ML \ get_descrs @{theory} (0, 2, 2) @{type_name foo'}; \ -ML \ get_descrs @{theory} (0, 2, 2) @{type_name bar'}; \ +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 \ get_descrs @{theory} (2, 2, 2) @{type_name foo'}; \ -ML \ get_descrs @{theory} (2, 2, 2) @{type_name bar'}; \ +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 \ get_descrs @{theory} (3, 3, 3) @{type_name funky}; \ +ML {* get_descrs @{theory} (3, 3, 3) @{type_name funky} *} old_datatype fnky = Fnky "nat tre" -ML \ get_descrs @{theory} (1, 1, 1) @{type_name fnky}; \ +ML {* get_descrs @{theory} (1, 1, 1) @{type_name fnky} *} datatype tree = Tree "tree foo" -ML \ get_descrs @{theory} (0, 1, 1) @{type_name tree}; \ +ML {* get_descrs @{theory} (0, 1, 1) @{type_name tree} *} datatype_compat tree -ML \ get_descrs @{theory} (3, 3, 1) @{type_name tree}; \ +ML {* get_descrs @{theory} (3, 3, 1) @{type_name tree} *} thm tree.induct tree.rec thm compat_tree.induct compat_tree.rec -subsection \ Creating New-Style Datatypes Using Old-Style Interfaces \ +subsection {* Creating New-Style Datatypes Using Old-Style Interfaces *} -ML \ +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)])]; -\ + (@{binding C}, [@{typ 'a}, Type (Sign.full_name @{theory} @{binding l}, [@{typ 'a}])], + NoSyn)])]; +*} -setup \ snd o BNF_LFP_Compat.add_datatype BNF_LFP_Compat.Unfold_Nesting l_specs; \ +setup {* snd o BNF_LFP_Compat.add_datatype [] l_specs *} -ML \ get_descrs @{theory} (1, 1, 1) @{type_name l}; \ +ML {* get_descrs @{theory} (1, 1, 1) @{type_name l} *} thm l.exhaust l.map l.induct l.rec l.size -ML \ +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)])]; -\ + [(@{binding T}, [@{typ 'b}, + Type (@{type_name l}, [Type (Sign.full_name @{theory} @{binding t}, [@{typ 'b}])])], + NoSyn)])]; +*} -setup \ snd o BNF_LFP_Compat.add_datatype BNF_LFP_Compat.Unfold_Nesting t_specs; \ +setup {* snd o BNF_LFP_Compat.add_datatype [] t_specs *} -ML \ get_descrs @{theory} (2, 2, 1) @{type_name t}; \ +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 \ +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)])]; -\ +*} -setup \ snd o BNF_LFP_Compat.add_datatype BNF_LFP_Compat.Unfold_Nesting ft_specs; \ +setup {* snd o BNF_LFP_Compat.add_datatype [] ft_specs *} -ML \ get_descrs @{theory} (1, 1, 1) @{type_name ft}; \ +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 diff -r c9f374b64d99 -r 04ac60da613e src/HOL/Library/refute.ML --- 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; - diff -r c9f374b64d99 -r 04ac60da613e src/HOL/Nominal/nominal_atoms.ML --- 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 diff -r c9f374b64d99 -r 04ac60da613e src/HOL/Nominal/nominal_datatype.ML --- 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; diff -r c9f374b64d99 -r 04ac60da613e src/HOL/SPARK/Tools/spark_vcs.ML --- 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, diff -r c9f374b64d99 -r 04ac60da613e src/HOL/Statespace/state_fun.ML --- 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); diff -r c9f374b64d99 -r 04ac60da613e src/HOL/Tools/BNF/bnf_lfp_compat.ML --- 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; diff -r c9f374b64d99 -r 04ac60da613e src/HOL/Tools/Quickcheck/exhaustive_generators.ML --- 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); diff -r c9f374b64d99 -r 04ac60da613e src/HOL/Tools/Quickcheck/quickcheck_common.ML --- 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 **) diff -r c9f374b64d99 -r 04ac60da613e src/HOL/Tools/TFL/casesplit.ML --- 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; diff -r c9f374b64d99 -r 04ac60da613e src/HOL/Tools/TFL/tfl.ML --- 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) diff -r c9f374b64d99 -r 04ac60da613e src/HOL/Tools/TFL/thry.ML --- 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; diff -r c9f374b64d99 -r 04ac60da613e src/HOL/Tools/datatype_realizer.ML --- 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;