# HG changeset patch # User traytel # Date 1346940382 -7200 # Node ID 073d7d1b748874f6f7d51a2585d12133d07b6cee # Parent 83fdea0c477911bf6059574d18f76e13cc68ba1d respect order of/additional type variables supplied by the user in fixed point constructions; diff -r 83fdea0c4779 -r 073d7d1b7488 src/HOL/Codatatype/Examples/Misc_Codata.thy --- a/src/HOL/Codatatype/Examples/Misc_Codata.thy Thu Sep 06 12:21:33 2012 +0200 +++ b/src/HOL/Codatatype/Examples/Misc_Codata.thy Thu Sep 06 16:06:22 2012 +0200 @@ -53,15 +53,10 @@ and ('a, 'b) trm = Factor "('a, 'b) factor" | Prod "('a, 'b) factor" "('a, 'b) trm" and ('a, 'b) factor = C 'a | V 'b | Paren "('a, 'b) exp" -codata_raw some_killing: 'A = "'a \ 'b \ ('A + 'B)" - and in_here: 'B = "'b \ 'a + 'c" - -(* FIXME codata ('a, 'b, 'c) some_killing = SK "'a \ 'b \ ('a, 'b, 'c) some_killing + ('a, 'b, 'c) in_here" - and ('a, 'b, 'c) in_here = + and ('a, 'b, 'c) in_here = IH1 'b 'a | IH2 'c -*) codata_raw some_killing': 'a = "'b \ 'd \ ('a + 'c)" and in_here': 'c = "'d + 'e" @@ -69,7 +64,7 @@ codata_raw some_killing'': 'a = "'b \ 'c" and in_here'': 'c = "'d \ 'b + 'e" -codata_raw less_killing: 'a = "'b \ 'c" +codata ('b, 'c) less_killing = LK "'b \ 'c" codata 'b cps = CPS1 'b | CPS2 "'b \ 'b cps" @@ -95,6 +90,14 @@ and ('c, 'e, 'g) ind_wit = IW1 | IW2 'c +codata ('b, 'a) bar = BAR "'a \ 'b" +codata ('a, 'b, 'c, 'd) foo = FOO "'d + 'b \ 'c + 'a" + +codata 'a dead_foo = A +(* FIXME: handle unknown type constructors using DEADID? +codata ('a, 'b) use_dead_foo = Y "'a" "'b dead_foo" +*) + (* SLOW, MEMORY-HUNGRY codata ('a, 'c) D1 = A1 "('a, 'c) D2" | B1 "'a list" and ('a, 'c) D2 = A2 "('a, 'c) D3" | B2 "'c list" diff -r 83fdea0c4779 -r 073d7d1b7488 src/HOL/Codatatype/Examples/Misc_Data.thy --- a/src/HOL/Codatatype/Examples/Misc_Data.thy Thu Sep 06 12:21:33 2012 +0200 +++ b/src/HOL/Codatatype/Examples/Misc_Data.thy Thu Sep 06 16:06:22 2012 +0200 @@ -51,15 +51,10 @@ and ('a, 'b) trm = Factor "('a, 'b) factor" | Prod "('a, 'b) factor" "('a, 'b) trm" and ('a, 'b) factor = C 'a | V 'b | Paren "('a, 'b) exp" -data_raw some_killing: 'A = "'a \ 'b \ ('A + 'B)" - and in_here: 'B = "'b \ 'a + 'c" - -(* FIXME data ('a, 'b, 'c) some_killing = SK "'a \ 'b \ ('a, 'b, 'c) some_killing + ('a, 'b, 'c) in_here" and ('a, 'b, 'c) in_here = IH1 'b 'a | IH2 'c -*) data 'b nofail1 = NF11 "'b nofail1 \ 'b" | NF12 'b data 'b nofail2 = NF2 "('b nofail2 \ 'b \ 'b nofail2 \ 'b) list" @@ -150,4 +145,11 @@ and s8 = S8 nat *) +data ('a, 'b) bar = BAR "'b \ 'a" +data ('a, 'b, 'c, 'd) foo = FOO "'d + 'b \ 'c + 'a" + +data 'a dead_foo = A +(* FIXME: handle unknown type constructors using DEADID? +data ('a, 'b) use_dead_foo = Y "'a" "'b dead_foo" +*) end diff -r 83fdea0c4779 -r 073d7d1b7488 src/HOL/Codatatype/Tools/bnf_comp.ML --- a/src/HOL/Codatatype/Tools/bnf_comp.ML Thu Sep 06 12:21:33 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_comp.ML Thu Sep 06 16:06:22 2012 +0200 @@ -23,7 +23,7 @@ (''a list list -> ''a list) -> BNF_Def.BNF list -> unfold_thms -> Proof.context -> (int list list * ''a list) * (BNF_Def.BNF list * (unfold_thms * Proof.context)) val seal_bnf: unfold_thms -> binding -> typ list -> BNF_Def.BNF -> Proof.context -> - BNF_Def.BNF * local_theory + (BNF_Def.BNF * typ list) * local_theory end; structure BNF_Comp : BNF_COMP = @@ -656,6 +656,7 @@ val bd_repT = fst (dest_relT (fastype_of bnf_bd)); val bdT_bind = Binding.suffix_name ("_" ^ bdTN) b; val params = fold Term.add_tfreesT Ds []; + val deads = map TFree params; val ((bdT_name, (bdT_glob_info, bdT_loc_info)), (lthy', lthy)) = lthy @@ -666,7 +667,7 @@ val phi = Proof_Context.export_morphism lthy lthy'; val bnf_bd' = mk_dir_image bnf_bd - (Const (#Abs_name bdT_glob_info, bd_repT --> Type (bdT_name, map TFree params))) + (Const (#Abs_name bdT_glob_info, bd_repT --> Type (bdT_name, deads))) val set_def = Morphism.thm phi (the (#set_def bdT_loc_info)); val Abs_inject = Morphism.thm phi (#Abs_inject bdT_loc_info); @@ -701,8 +702,8 @@ fun wit_tac _ = mk_simple_wit_tac (map unfold_defs (wit_thms_of_bnf bnf)); - val (bnf', lthy') = bnf_def Hardly_Inline (K Derive_All_Facts) I tacs wit_tac NONE - ((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits) lthy; + val (bnf', lthy') = bnf_def Hardly_Inline (K Derive_All_Facts) I tacs wit_tac (SOME deads) + ((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits) lthy; val defs' = filter_refl (map_def_of_bnf bnf' :: set_defs_of_bnf bnf'); val unfold_defs' = unfold_defs o Local_Defs.unfold lthy' defs'; @@ -723,7 +724,7 @@ |> map (fn (thmN, thms) => ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); in - (bnf', lthy' |> Local_Theory.notes notes |> snd) + ((bnf', deads), lthy' |> Local_Theory.notes notes |> snd) end; fun bnf_of_typ _ _ _ _ (T as TFree _) (unfold, lthy) = diff -r 83fdea0c4779 -r 073d7d1b7488 src/HOL/Codatatype/Tools/bnf_fp_util.ML --- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML Thu Sep 06 12:21:33 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML Thu Sep 06 16:06:22 2012 +0200 @@ -103,12 +103,12 @@ val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list - val fp_bnf: (binding list -> mixfix list -> (string * sort) list -> typ list list -> - BNF_Def.BNF list -> local_theory -> 'a) -> + val fp_bnf: (mixfix list -> (string * sort) list option -> binding list -> + typ list * typ list list -> BNF_Def.BNF list -> local_theory -> 'a) -> binding list -> mixfix list -> (string * sort) list -> ((string * sort) * typ) list -> local_theory -> 'a - val fp_bnf_cmd: (binding list -> mixfix list -> (string * sort) list -> typ list list -> - BNF_Def.BNF list -> local_theory -> 'a) -> + val fp_bnf_cmd: (mixfix list -> (string * sort) list option -> binding list -> + typ list * typ list list -> BNF_Def.BNF list -> local_theory -> 'a) -> binding list * (string list * string list) -> local_theory -> 'a end; @@ -272,10 +272,12 @@ (* FIXME: because of "@ lhss", the output could contain type variables that are not in the input; also, "fp_sort" should put the "resBs" first and in the order in which they appear *) -fun fp_sort lhss Ass = Library.sort (Term_Ord.typ_ord o pairself TFree) - (subtract (op =) lhss (fold (fold (insert (op =))) Ass [])) @ lhss; +fun fp_sort lhss NONE Ass = Library.sort (Term_Ord.typ_ord o pairself TFree) + (subtract (op =) lhss (fold (fold (insert (op =))) Ass [])) @ lhss + | fp_sort lhss (SOME resBs) Ass = + (subtract (op =) lhss (filter (fn T => exists (fn Ts => member (op =) Ts T) Ass) resBs)) @ lhss; -fun mk_fp_bnf timer construct bs mixfixes resBs sort lhss bnfs deadss livess unfold lthy = +fun mk_fp_bnf timer construct resBs bs sort lhss bnfs deadss livess unfold lthy = let val name = fold_rev (fn b => fn s => Binding.name_of b ^ s) bs ""; fun qualify i bind = @@ -286,8 +288,8 @@ end; val Ass = map (map dest_TFree) livess; - val resDs = fold (subtract (op =)) Ass resBs; - val Ds = fold (fold Term.add_tfreesT) deadss resDs; + val resDs = (case resBs of NONE => [] | SOME Ts => fold (subtract (op =)) Ass Ts); + val Ds = fold (fold Term.add_tfreesT) deadss []; val _ = (case Library.inter (op =) Ds lhss of [] => () | A :: _ => error ("Nonadmissible type recursion (cannot take fixed point of dead type \ @@ -300,12 +302,13 @@ val Dss = map3 (append oo map o nth) livess kill_poss deadss; - val (bnfs'', lthy'') = - fold_map3 (seal_bnf unfold') (map (Binding.suffix_name "BNF") bs) Dss bnfs' lthy'; + val ((bnfs'', deadss), lthy'') = + fold_map3 (seal_bnf unfold') (map (Binding.suffix_name "BNF") bs) Dss bnfs' lthy' + |>> split_list; val timer = time (timer "Normalization & sealing of BNFs"); - val res = construct bs mixfixes resDs Dss bnfs'' lthy''; + val res = construct resBs bs (map TFree resDs, deadss) bnfs'' lthy''; val timer = time (timer "FP construction in total"); in @@ -316,25 +319,25 @@ let val timer = time (Timer.startRealTimer ()); val (lhss, rhss) = split_list eqs; - val sort = fp_sort lhss; + val sort = fp_sort lhss (SOME resBs); val ((bnfs, (Dss, Ass)), (unfold, lthy')) = apfst (apsnd split_list o split_list) (fold_map2 (fn b => bnf_of_typ Smart_Inline (Binding.suffix_name "RAW" b) I sort) bs rhss (empty_unfold, lthy)); in - mk_fp_bnf timer construct bs mixfixes resBs sort lhss bnfs Dss Ass unfold lthy' + mk_fp_bnf timer (construct mixfixes) (SOME resBs) bs sort lhss bnfs Dss Ass unfold lthy' end; fun fp_bnf_cmd construct (bs, (raw_lhss, raw_bnfs)) lthy = let val timer = time (Timer.startRealTimer ()); val lhss = map (dest_TFree o Syntax.read_typ lthy) raw_lhss; - val sort = fp_sort lhss; + val sort = fp_sort lhss NONE; val ((bnfs, (Dss, Ass)), (unfold, lthy')) = apfst (apsnd split_list o split_list) (fold_map2 (fn b => fn rawT => (bnf_of_typ Smart_Inline (Binding.suffix_name "RAW" b) I sort (Syntax.read_typ lthy rawT))) - bs raw_bnfs (empty_unfold, lthy)); + bs raw_bnfs (empty_unfold, lthy)); in - mk_fp_bnf timer construct bs (map (K NoSyn) bs) [] sort lhss bnfs Dss Ass unfold lthy' + mk_fp_bnf timer (construct (map (K NoSyn) bs)) NONE bs sort lhss bnfs Dss Ass unfold lthy' end; end; diff -r 83fdea0c4779 -r 073d7d1b7488 src/HOL/Codatatype/Tools/bnf_gfp.ML --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML Thu Sep 06 12:21:33 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML Thu Sep 06 16:06:22 2012 +0200 @@ -9,8 +9,8 @@ signature BNF_GFP = sig - val bnf_gfp: binding list -> mixfix list -> (string * sort) list -> typ list list -> - BNF_Def.BNF list -> local_theory -> + val bnf_gfp: mixfix list -> (string * sort) list option -> binding list -> + typ list * typ list list -> BNF_Def.BNF list -> local_theory -> (term list * term list * term list * term list * thm list * thm list * thm list) * local_theory end; @@ -53,7 +53,7 @@ ((i, I), nth (nth lwitss i) nwit) :: maps (tree_to_coind_wits lwitss) subtrees; (*all bnfs have the same lives*) -fun bnf_gfp bs mixfixes resDs Dss_insts bnfs lthy = +fun bnf_gfp mixfixes resBs bs (resDs, Dss) bnfs lthy = let val timer = time (Timer.startRealTimer ()); @@ -66,8 +66,7 @@ (* TODO: check if m, n etc are sane *) - val Dss = map (fn Ds => map TFree (fold Term.add_tfreesT Ds [])) Dss_insts; - val deads = fold (union (op =)) Dss (map TFree resDs); + val deads = fold (union (op =)) Dss resDs; val names_lthy = fold Variable.declare_typ deads lthy; (* tvars *) @@ -92,8 +91,16 @@ val Css' = replicate n allCs'; (* typs *) + val dead_poss = + (case resBs of + NONE => map SOME deads @ replicate m NONE + | SOME Ts => map (fn T => if member (op =) deads (TFree T) then SOME (TFree T) else NONE) Ts); + fun mk_param NONE passive = (hd passive, tl passive) + | mk_param (SOME a) passive = (a, passive); + val mk_params = fold_map mk_param dead_poss #> fst; + fun mk_FTs Ts = map2 (fn Ds => mk_T_of_bnf Ds Ts) Dss bnfs; - val (params, params') = `(map Term.dest_TFree) (deads @ passiveAs); + val (params, params') = `(map Term.dest_TFree) (mk_params passiveAs); val FTsAs = mk_FTs allAs; val FTsBs = mk_FTs allBs; val FTsCs = mk_FTs allCs; @@ -1912,7 +1919,7 @@ (*transforms defined frees into consts*) val phi = Proof_Context.export_morphism lthy_old lthy; fun mk_unfs passive = - map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ (deads @ passive)) o + map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ (mk_params passive)) o Morphism.term phi) unf_frees; val unfs = mk_unfs passiveAs; val unf's = mk_unfs passiveBs; diff -r 83fdea0c4779 -r 073d7d1b7488 src/HOL/Codatatype/Tools/bnf_lfp.ML --- a/src/HOL/Codatatype/Tools/bnf_lfp.ML Thu Sep 06 12:21:33 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML Thu Sep 06 16:06:22 2012 +0200 @@ -8,8 +8,8 @@ signature BNF_LFP = sig - val bnf_lfp: binding list -> mixfix list -> (string * sort) list -> typ list list -> - BNF_Def.BNF list -> local_theory -> + val bnf_lfp: mixfix list -> (string * sort) list option -> binding list -> + typ list * typ list list -> BNF_Def.BNF list -> local_theory -> (term list * term list * term list * term list * thm list * thm list * thm list) * local_theory end; @@ -24,7 +24,7 @@ open BNF_LFP_Tactics (*all bnfs have the same lives*) -fun bnf_lfp bs mixfixes resDs Dss_insts bnfs lthy = +fun bnf_lfp mixfixes resBs bs (resDs, Dss) bnfs lthy = let val timer = time (Timer.startRealTimer ()); val live = live_of_bnf (hd bnfs); @@ -35,8 +35,7 @@ (* TODO: check if m, n etc are sane *) - val Dss = map (fn Ds => map TFree (fold Term.add_tfreesT Ds [])) Dss_insts; - val deads = fold (union (op =)) Dss (map TFree resDs); + val deads = fold (union (op =)) Dss resDs; val names_lthy = fold Variable.declare_typ deads lthy; (* tvars *) @@ -58,8 +57,16 @@ val Css' = replicate n allCs'; (* typs *) + val dead_poss = + (case resBs of + NONE => map SOME deads @ replicate m NONE + | SOME Ts => map (fn T => if member (op =) deads (TFree T) then SOME (TFree T) else NONE) Ts); + fun mk_param NONE passive = (hd passive, tl passive) + | mk_param (SOME a) passive = (a, passive); + val mk_params = fold_map mk_param dead_poss #> fst; + fun mk_FTs Ts = map2 (fn Ds => mk_T_of_bnf Ds Ts) Dss bnfs; - val (params, params') = `(map Term.dest_TFree) (deads @ passiveAs); + val (params, params') = `(map Term.dest_TFree) (mk_params passiveAs); val FTsAs = mk_FTs allAs; val FTsBs = mk_FTs allBs; val FTsCs = mk_FTs allCs; @@ -1019,7 +1026,7 @@ (*transforms defined frees into consts*) val phi = Proof_Context.export_morphism lthy_old lthy; fun mk_flds passive = - map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ (deads @ passive)) o + map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ (mk_params passive)) o Morphism.term phi) fld_frees; val flds = mk_flds passiveAs; val fld's = mk_flds passiveBs;