7 Codatatype construction. |
7 Codatatype construction. |
8 *) |
8 *) |
9 |
9 |
10 signature BNF_GFP = |
10 signature BNF_GFP = |
11 sig |
11 sig |
12 val bnf_gfp: binding list -> mixfix list -> (string * sort) list -> typ list list -> |
12 val bnf_gfp: mixfix list -> (string * sort) list option -> binding list -> |
13 BNF_Def.BNF list -> local_theory -> |
13 typ list * typ list list -> BNF_Def.BNF list -> local_theory -> |
14 (term list * term list * term list * term list * thm list * thm list * thm list) * local_theory |
14 (term list * term list * term list * term list * thm list * thm list * thm list) * local_theory |
15 end; |
15 end; |
16 |
16 |
17 structure BNF_GFP : BNF_GFP = |
17 structure BNF_GFP : BNF_GFP = |
18 struct |
18 struct |
51 fun tree_to_coind_wits _ (Leaf j) = [] |
51 fun tree_to_coind_wits _ (Leaf j) = [] |
52 | tree_to_coind_wits lwitss (Node ((i, nwit, I), subtrees)) = |
52 | tree_to_coind_wits lwitss (Node ((i, nwit, I), subtrees)) = |
53 ((i, I), nth (nth lwitss i) nwit) :: maps (tree_to_coind_wits lwitss) subtrees; |
53 ((i, I), nth (nth lwitss i) nwit) :: maps (tree_to_coind_wits lwitss) subtrees; |
54 |
54 |
55 (*all bnfs have the same lives*) |
55 (*all bnfs have the same lives*) |
56 fun bnf_gfp bs mixfixes resDs Dss_insts bnfs lthy = |
56 fun bnf_gfp mixfixes resBs bs (resDs, Dss) bnfs lthy = |
57 let |
57 let |
58 val timer = time (Timer.startRealTimer ()); |
58 val timer = time (Timer.startRealTimer ()); |
59 |
59 |
60 val live = live_of_bnf (hd bnfs); |
60 val live = live_of_bnf (hd bnfs); |
61 val n = length bnfs; (*active*) |
61 val n = length bnfs; (*active*) |
64 val ls = 1 upto m; |
64 val ls = 1 upto m; |
65 val b = Binding.name (fold_rev (fn b => fn s => Binding.name_of b ^ s) bs ""); |
65 val b = Binding.name (fold_rev (fn b => fn s => Binding.name_of b ^ s) bs ""); |
66 |
66 |
67 (* TODO: check if m, n etc are sane *) |
67 (* TODO: check if m, n etc are sane *) |
68 |
68 |
69 val Dss = map (fn Ds => map TFree (fold Term.add_tfreesT Ds [])) Dss_insts; |
69 val deads = fold (union (op =)) Dss resDs; |
70 val deads = fold (union (op =)) Dss (map TFree resDs); |
|
71 val names_lthy = fold Variable.declare_typ deads lthy; |
70 val names_lthy = fold Variable.declare_typ deads lthy; |
72 |
71 |
73 (* tvars *) |
72 (* tvars *) |
74 val ((((((((passiveAs, activeAs), allAs)), (passiveBs, activeBs)), |
73 val ((((((((passiveAs, activeAs), allAs)), (passiveBs, activeBs)), |
75 (passiveCs, activeCs)), passiveXs), passiveYs), idxT) = names_lthy |
74 (passiveCs, activeCs)), passiveXs), passiveYs), idxT) = names_lthy |
90 val allCs = passiveAs @ activeCs; |
89 val allCs = passiveAs @ activeCs; |
91 val allCs' = passiveBs @ activeCs; |
90 val allCs' = passiveBs @ activeCs; |
92 val Css' = replicate n allCs'; |
91 val Css' = replicate n allCs'; |
93 |
92 |
94 (* typs *) |
93 (* typs *) |
|
94 val dead_poss = |
|
95 (case resBs of |
|
96 NONE => map SOME deads @ replicate m NONE |
|
97 | SOME Ts => map (fn T => if member (op =) deads (TFree T) then SOME (TFree T) else NONE) Ts); |
|
98 fun mk_param NONE passive = (hd passive, tl passive) |
|
99 | mk_param (SOME a) passive = (a, passive); |
|
100 val mk_params = fold_map mk_param dead_poss #> fst; |
|
101 |
95 fun mk_FTs Ts = map2 (fn Ds => mk_T_of_bnf Ds Ts) Dss bnfs; |
102 fun mk_FTs Ts = map2 (fn Ds => mk_T_of_bnf Ds Ts) Dss bnfs; |
96 val (params, params') = `(map Term.dest_TFree) (deads @ passiveAs); |
103 val (params, params') = `(map Term.dest_TFree) (mk_params passiveAs); |
97 val FTsAs = mk_FTs allAs; |
104 val FTsAs = mk_FTs allAs; |
98 val FTsBs = mk_FTs allBs; |
105 val FTsBs = mk_FTs allBs; |
99 val FTsCs = mk_FTs allCs; |
106 val FTsCs = mk_FTs allCs; |
100 val ATs = map HOLogic.mk_setT passiveAs; |
107 val ATs = map HOLogic.mk_setT passiveAs; |
101 val BTs = map HOLogic.mk_setT activeAs; |
108 val BTs = map HOLogic.mk_setT activeAs; |
1910 ||> `Local_Theory.restore; |
1917 ||> `Local_Theory.restore; |
1911 |
1918 |
1912 (*transforms defined frees into consts*) |
1919 (*transforms defined frees into consts*) |
1913 val phi = Proof_Context.export_morphism lthy_old lthy; |
1920 val phi = Proof_Context.export_morphism lthy_old lthy; |
1914 fun mk_unfs passive = |
1921 fun mk_unfs passive = |
1915 map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ (deads @ passive)) o |
1922 map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ (mk_params passive)) o |
1916 Morphism.term phi) unf_frees; |
1923 Morphism.term phi) unf_frees; |
1917 val unfs = mk_unfs passiveAs; |
1924 val unfs = mk_unfs passiveAs; |
1918 val unf's = mk_unfs passiveBs; |
1925 val unf's = mk_unfs passiveBs; |
1919 val unf_defs = map ((fn thm => thm RS fun_cong) o Morphism.thm phi) unf_def_frees; |
1926 val unf_defs = map ((fn thm => thm RS fun_cong) o Morphism.thm phi) unf_def_frees; |
1920 |
1927 |