# HG changeset patch # User blanchet # Date 1346312866 -7200 # Node ID 332e5e661675c84b04419b7a963024d58543e4c7 # Parent f781bbe0d91b76daf283b41c2c0756c0d069e04f have "bnf_of_typ" command seal the BNF diff -r f781bbe0d91b -r 332e5e661675 src/HOL/Codatatype/Tools/bnf_comp.ML --- a/src/HOL/Codatatype/Tools/bnf_comp.ML Wed Aug 29 22:18:33 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_comp.ML Thu Aug 30 09:47:46 2012 +0200 @@ -15,16 +15,16 @@ val rel_unfolds_of: unfold_thms -> thm list val pred_unfolds_of: unfold_thms -> thm list - val default_comp_sort: (string * sort) list list -> (string * sort) list val bnf_of_typ: BNF_Def.const_policy -> binding -> (binding -> binding) -> ((string * sort) list list -> (string * sort) list) -> typ -> unfold_thms * Proof.context -> (BNF_Def.BNF * (typ list * typ list)) * (unfold_thms * Proof.context) val bnf_of_typ_cmd: binding * string -> Proof.context -> Proof.context - val seal_bnf: unfold_thms -> binding -> typ list -> BNF_Def.BNF -> Proof.context -> - BNF_Def.BNF * local_theory + val default_comp_sort: (string * sort) list list -> (string * sort) list val normalize_bnfs: (int -> binding -> binding) -> ''a list list -> ''a list -> (''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 end; structure BNF_Comp : BNF_COMP = @@ -600,6 +600,74 @@ (snd o snd) (permute_bnf I src dest (the (bnf_of lthy raw_bnf)) (empty_unfold, lthy)); +(* Composition pipeline *) + +fun permute_and_kill qualify n src dest bnf = + bnf + |> permute_bnf qualify src dest + #> uncurry (killN_bnf qualify n); + +fun lift_and_permute qualify n src dest bnf = + bnf + |> liftN_bnf qualify n + #> uncurry (permute_bnf qualify src dest); + +fun normalize_bnfs qualify Ass Ds sort bnfs unfold lthy = + let + val before_kill_src = map (fn As => 0 upto (length As - 1)) Ass; + val kill_poss = map (find_indices Ds) Ass; + val live_poss = map2 (subtract (op =)) kill_poss before_kill_src; + val before_kill_dest = map2 append kill_poss live_poss; + val kill_ns = map length kill_poss; + val (inners', (unfold', lthy')) = + fold_map5 (fn i => permute_and_kill (qualify i)) + (if length bnfs = 1 then [0] else (1 upto length bnfs)) + kill_ns before_kill_src before_kill_dest bnfs (unfold, lthy); + + val Ass' = map2 (map o nth) Ass live_poss; + val As = sort Ass'; + val after_lift_dest = replicate (length Ass') (0 upto (length As - 1)); + val old_poss = map (map (fn x => find_index (fn y => x = y) As)) Ass'; + val new_poss = map2 (subtract (op =)) old_poss after_lift_dest; + val after_lift_src = map2 append new_poss old_poss; + val lift_ns = map (fn xs => length As - length xs) Ass'; + in + ((kill_poss, As), fold_map5 (fn i => lift_and_permute (qualify i)) + (if length bnfs = 1 then [0] else (1 upto length bnfs)) + lift_ns after_lift_src after_lift_dest inners' (unfold', lthy')) + end; + +fun default_comp_sort Ass = + Library.sort (Term_Ord.typ_ord o pairself TFree) (fold (fold (insert (op =))) Ass []); + +fun compose_bnf const_policy qualify' b sort outer inners oDs Dss tfreess (unfold, lthy) = + let + val name = Binding.name_of b; + fun qualify i bind = + let val namei = if i > 0 then name ^ string_of_int i else name; + in + if member (op =) (#2 (Binding.dest bind)) (namei, true) then qualify' bind + else qualify' (Binding.prefix_name namei bind) + end; + + val Ass = map (map dest_TFree) tfreess; + val Ds = fold (fold Term.add_tfreesT) (oDs :: Dss) []; + + val ((kill_poss, As), (inners', (unfold', lthy'))) = + normalize_bnfs qualify Ass Ds sort inners unfold lthy; + + val Ds = oDs @ flat (map3 (append oo map o nth) tfreess kill_poss Dss); + val As = map TFree As; + in + apfst (rpair (Ds, As)) (clean_compose_bnf const_policy I b outer inners' (unfold', lthy')) + end; + +fun compose_bnf_cmd (((((b, outer), inners), oDs), Dss), Ass) lthy = (snd o snd) + (compose_bnf Dont_Inline I b default_comp_sort (the (bnf_of lthy outer)) + (map (the o bnf_of lthy) inners) + (map (Syntax.read_typ lthy) oDs) (map (map (Syntax.read_typ lthy)) Dss) + (map (map (Syntax.read_typ lthy)) Ass) (empty_unfold, lthy)); + (* Hide the type of the bound (optimization) and unfold the definitions (nicer to the user) *) fun seal_bnf unfold b Ds bnf lthy = @@ -703,74 +771,6 @@ |> note pred_unfoldN [pred_unfold]) end; -(* Composition pipeline *) - -fun permute_and_kill qualify n src dest bnf = - bnf - |> permute_bnf qualify src dest - #> uncurry (killN_bnf qualify n); - -fun lift_and_permute qualify n src dest bnf = - bnf - |> liftN_bnf qualify n - #> uncurry (permute_bnf qualify src dest); - -fun normalize_bnfs qualify Ass Ds sort bnfs unfold lthy = - let - val before_kill_src = map (fn As => 0 upto (length As - 1)) Ass; - val kill_poss = map (find_indices Ds) Ass; - val live_poss = map2 (subtract (op =)) kill_poss before_kill_src; - val before_kill_dest = map2 append kill_poss live_poss; - val kill_ns = map length kill_poss; - val (inners', (unfold', lthy')) = - fold_map5 (fn i => permute_and_kill (qualify i)) - (if length bnfs = 1 then [0] else (1 upto length bnfs)) - kill_ns before_kill_src before_kill_dest bnfs (unfold, lthy); - - val Ass' = map2 (map o nth) Ass live_poss; - val As = sort Ass'; - val after_lift_dest = replicate (length Ass') (0 upto (length As - 1)); - val old_poss = map (map (fn x => find_index (fn y => x = y) As)) Ass'; - val new_poss = map2 (subtract (op =)) old_poss after_lift_dest; - val after_lift_src = map2 append new_poss old_poss; - val lift_ns = map (fn xs => length As - length xs) Ass'; - in - ((kill_poss, As), fold_map5 (fn i => lift_and_permute (qualify i)) - (if length bnfs = 1 then [0] else (1 upto length bnfs)) - lift_ns after_lift_src after_lift_dest inners' (unfold', lthy')) - end; - -fun default_comp_sort Ass = - Library.sort (Term_Ord.typ_ord o pairself TFree) (fold (fold (insert (op =))) Ass []); - -fun compose_bnf const_policy qualify' b sort outer inners oDs Dss tfreess (unfold, lthy) = - let - val name = Binding.name_of b; - fun qualify i bind = - let val namei = if i > 0 then name ^ string_of_int i else name; - in - if member (op =) (#2 (Binding.dest bind)) (namei, true) then qualify' bind - else qualify' (Binding.prefix_name namei bind) - end; - - val Ass = map (map dest_TFree) tfreess; - val Ds = fold (fold Term.add_tfreesT) (oDs :: Dss) []; - - val ((kill_poss, As), (inners', (unfold', lthy'))) = - normalize_bnfs qualify Ass Ds sort inners unfold lthy; - - val Ds = oDs @ flat (map3 (append oo map o nth) tfreess kill_poss Dss); - val As = map TFree As; - in - apfst (rpair (Ds, As)) (clean_compose_bnf const_policy I b outer inners' (unfold', lthy')) - end; - -fun compose_bnf_cmd (((((b, outer), inners), oDs), Dss), Ass) lthy = (snd o snd) - (compose_bnf Dont_Inline I b default_comp_sort (the (bnf_of lthy outer)) - (map (the o bnf_of lthy) inners) - (map (Syntax.read_typ lthy) oDs) (map (map (Syntax.read_typ lthy)) Dss) - (map (map (Syntax.read_typ lthy)) Ass) (empty_unfold, lthy)); - fun bnf_of_typ _ _ _ _ (T as TFree _) (unfold, lthy) = ((Basic_BNFs.ID_bnf, ([], [T])), (add_to_unfold_opt NONE NONE (SOME Basic_BNFs.ID_rel_def) (SOME Basic_BNFs.ID_pred_def) unfold, lthy)) @@ -823,9 +823,14 @@ end end; -fun bnf_of_typ_cmd (b, rawT) lthy = (snd o snd) - (bnf_of_typ Dont_Inline b I default_comp_sort (Syntax.read_typ lthy rawT) - (empty_unfold, lthy)); +fun bnf_of_typ_cmd (b, rawT) lthy = + let + val ((bnf, (Ds, As)), (unfold, lthy')) = + bnf_of_typ Smart_Inline b I default_comp_sort (Syntax.read_typ lthy rawT) + (empty_unfold, lthy); + in + snd (seal_bnf unfold b Ds bnf lthy') + end; val _ = Outer_Syntax.local_theory @{command_spec "bnf_of_typ"} "parse a type as composition of BNFs"