# HG changeset patch # User blanchet # Date 1367511944 -7200 # Node ID 142a828838310c7249d63fc7174b3514d7708483 # Parent 55099e63c5ca59a746e75acdec14041ff7d6f1cd removed dead code diff -r 55099e63c5ca -r 142a82883831 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Thu May 02 18:16:28 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Thu May 02 18:25:44 2013 +0200 @@ -51,15 +51,15 @@ * (thm list list * thm list list * Args.src list) val co_datatypes: bool -> (mixfix list -> binding list -> binding list -> binding list -> - binding list list -> (string * sort) list option -> typ list * typ list list -> - BNF_Def.bnf list -> local_theory -> BNF_FP_Util.fp_result * local_theory) -> + binding list list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list -> + local_theory -> BNF_FP_Util.fp_result * local_theory) -> (bool * bool) * (((((binding * (typ * sort)) list * binding) * (binding * binding)) * mixfix) * ((((binding * binding) * (binding * typ) list) * (binding * term) list) * mixfix) list) list -> local_theory -> local_theory val parse_co_datatype_cmd: bool -> (mixfix list -> binding list -> binding list -> binding list -> - binding list list -> (string * sort) list option -> typ list * typ list list -> - BNF_Def.bnf list -> local_theory -> BNF_FP_Util.fp_result * local_theory) -> + binding list list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list -> + local_theory -> BNF_FP_Util.fp_result * local_theory) -> (local_theory -> local_theory) parser end; diff -r 55099e63c5ca -r 142a82883831 src/HOL/BNF/Tools/bnf_fp_util.ML --- a/src/HOL/BNF/Tools/bnf_fp_util.ML Thu May 02 18:16:28 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_util.ML Thu May 02 18:25:44 2013 +0200 @@ -166,8 +166,7 @@ val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list val fp_bnf: (mixfix list -> binding list -> binding list -> binding list -> binding list list -> - (string * sort) list option -> typ list * typ list list -> BNF_Def.bnf list -> local_theory -> - 'a) -> + (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list -> local_theory -> 'a) -> binding list -> mixfix list -> binding list -> binding list -> binding list list -> (string * sort) list -> ((string * sort) * typ) list -> local_theory -> BNF_Def.bnf list * 'a end; @@ -461,13 +460,10 @@ (* 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 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 = +fun fp_sort lhss resBs Ass = (subtract (op =) lhss (filter (fn T => exists (fn Ts => member (op =) Ts T) Ass) resBs)) @ lhss; -fun mk_fp_bnf timer construct_fp resBs bs map_bs rel_bs set_bss sort lhss bnfs deadss livess - unfold_set lthy = +fun mk_fp_bnf timer construct_fp resBs bs sort lhss bnfs deadss livess unfold_set lthy = let val name = mk_common_name (map Binding.name_of bs); fun qualify i = @@ -475,7 +471,7 @@ in Binding.qualify true namei end; val Ass = map (map dest_TFree) livess; - val resDs = (case resBs of NONE => [] | SOME Ts => fold (subtract (op =)) Ass Ts); + val resDs = fold (subtract (op =)) Ass resBs; val Ds = fold (fold Term.add_tfreesT) deadss []; val _ = (case Library.inter (op =) Ds lhss of [] => () @@ -495,7 +491,7 @@ val timer = time (timer "Normalization & sealing of BNFs"); - val res = construct_fp bs map_bs rel_bs set_bss resBs (map TFree resDs, deadss) pre_bnfs lthy''; + val res = construct_fp resBs (map TFree resDs, deadss) pre_bnfs lthy''; val timer = time (timer "FP construction in total"); in @@ -506,14 +502,14 @@ let val timer = time (Timer.startRealTimer ()); val (lhss, rhss) = split_list eqs; - val sort = fp_sort lhss (SOME resBs); + val sort = fp_sort lhss resBs; fun qualify b = Binding.qualify true (Binding.name_of (Binding.prefix_name rawN b)); val ((bnfs, (Dss, Ass)), (unfold_set, lthy')) = apfst (apsnd split_list o split_list) (fold_map2 (fn b => bnf_of_typ Smart_Inline (qualify b) sort) bs rhss (empty_unfolds, lthy)); in - mk_fp_bnf timer (construct_fp mixfixes) (SOME resBs) bs map_bs rel_bs set_bss sort lhss bnfs Dss - Ass unfold_set lthy' + mk_fp_bnf timer (construct_fp mixfixes bs map_bs rel_bs set_bss) resBs bs sort lhss bnfs Dss Ass + unfold_set lthy' end; end; diff -r 55099e63c5ca -r 142a82883831 src/HOL/BNF/Tools/bnf_gfp.ML --- a/src/HOL/BNF/Tools/bnf_gfp.ML Thu May 02 18:16:28 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML Thu May 02 18:25:44 2013 +0200 @@ -10,8 +10,8 @@ signature BNF_GFP = sig val construct_gfp: mixfix list -> binding list -> binding list -> binding list -> - binding list list -> (string * sort) list option -> typ list * typ list list -> - BNF_Def.bnf list -> local_theory -> BNF_FP_Util.fp_result * local_theory + binding list list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list -> + local_theory -> BNF_FP_Util.fp_result * local_theory end; structure BNF_GFP : BNF_GFP = @@ -94,11 +94,9 @@ val allCs' = passiveBs @ activeCs; val Css' = replicate n allCs'; - (* typs *) + (* types *) 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); + map (fn T => if member (op =) deads (TFree T) then SOME (TFree T) else NONE) resBs; 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; diff -r 55099e63c5ca -r 142a82883831 src/HOL/BNF/Tools/bnf_lfp.ML --- a/src/HOL/BNF/Tools/bnf_lfp.ML Thu May 02 18:16:28 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML Thu May 02 18:25:44 2013 +0200 @@ -9,8 +9,8 @@ signature BNF_LFP = sig val construct_lfp: mixfix list -> binding list -> binding list -> binding list -> - binding list list -> (string * sort) list option -> typ list * typ list list -> - BNF_Def.bnf list -> local_theory -> BNF_FP_Util.fp_result * local_theory + binding list list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list -> + local_theory -> BNF_FP_Util.fp_result * local_theory end; structure BNF_LFP : BNF_LFP = @@ -61,11 +61,9 @@ val allCs' = passiveBs @ activeCs; val Css' = replicate n allCs'; - (* typs *) + (* types *) 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); + map (fn T => if member (op =) deads (TFree T) then SOME (TFree T) else NONE) resBs; 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;