101 |
101 |
102 ML Local_Theory.exit_global |
102 ML Local_Theory.exit_global |
103 |
103 |
104 (* TODO: replace with proper thing *) |
104 (* TODO: replace with proper thing *) |
105 ML {* |
105 ML {* |
106 fun is_atom ty = Binding.name_of ty = "name" |
106 fun is_atom ty = ty = "name" |
107 *} |
107 *} |
108 |
108 |
109 ML {* |
109 ML {* @{term "A \<union> B"} *} |
110 fun fv_constr lthy prefix (((name, anno_tys), bds), syn) = |
110 |
|
111 (* TODO: After variant_frees, check that the new names correspond to the ones given by user *) |
|
112 ML {* |
|
113 fun fv_constr lthy prefix dt_names (((name, anno_tys), bds), syn) = |
111 let |
114 let |
112 fun prepare_name (NONE, ty) = ("", ty) |
115 fun prepare_name (NONE, ty) = ("", ty) |
113 | prepare_name (SOME n, ty) = (n, ty); |
116 | prepare_name (SOME n, ty) = (n, ty); |
114 val vars = map Free (Variable.variant_frees lthy [] (map prepare_name anno_tys)); |
117 val vars = map Free (Variable.variant_frees lthy [] (map prepare_name anno_tys)); |
115 val var_strs = map (Syntax.string_of_term lthy) vars; |
118 val var_strs = map (Syntax.string_of_term lthy) vars; |
116 in |
119 fun fv_var (t as Free (s, (ty as Type (tyS, _)))) = |
117 prefix ^ " (" ^ (Binding.name_of name) ^ " " ^ (implode (separate " " var_strs)) ^ ") = " |
120 if is_atom tyS then HOLogic.mk_set ty [t] else |
|
121 if tyS mem dt_names then Free ("fv_" ^ tyS, dummyT) $ t else |
|
122 @{term "{}"} |
|
123 val fv_eq = |
|
124 if null vars then HOLogic.mk_set @{typ atom} [] |
|
125 else foldr1 (HOLogic.mk_binop @{const_name union}) (map fv_var vars) |
|
126 val fv_eq_str = Syntax.string_of_term lthy fv_eq |
|
127 in |
|
128 prefix ^ " (" ^ (Binding.name_of name) ^ " " ^ (implode (separate " " var_strs)) ^ ") = " ^ fv_eq_str |
118 end |
129 end |
119 *} |
130 *} |
120 |
131 |
121 ML {* |
132 ML {* |
122 fun single_dt lthy (((s2, s3), syn), constrs) = |
133 fun single_dt lthy (((s2, s3), syn), constrs) = |
128 |> separate "\n" |
139 |> separate "\n" |
129 |> implode |
140 |> implode |
130 *} |
141 *} |
131 |
142 |
132 ML {* |
143 ML {* |
133 fun fv_dt lthy (((s2, s3), syn), constrs) = |
144 fun fv_dt lthy dt_names (((s2, s3), syn), constrs) = |
134 map (fv_constr lthy ("fv_" ^ Binding.name_of s3)) constrs |
145 map (fv_constr lthy ("fv_" ^ Binding.name_of s3) dt_names) constrs |
135 |> separate "\n" |
146 |> separate "\n" |
136 |> implode |
147 |> implode |
137 *} |
148 *} |
138 |
149 |
139 ML {* fun single_fun_eq lthy (at, s) = |
150 ML {* fun single_fun_eq lthy (at, s) = |
147 |> separate "\n" |
158 |> separate "\n" |
148 |> implode |
159 |> implode |
149 *} |
160 *} |
150 |
161 |
151 ML {* |
162 ML {* |
|
163 fun dt_name (((s2, s3), syn), constrs) = Binding.name_of s3 |
|
164 *} |
|
165 |
|
166 ML {* |
152 fun print_dts (dts, (funs, feqs)) lthy = |
167 fun print_dts (dts, (funs, feqs)) lthy = |
153 let |
168 let |
154 val _ = warning (implode (separate "\n" (map (single_dt lthy) dts))); |
169 val _ = warning (implode (separate "\n" (map (single_dt lthy) dts))); |
155 val _ = warning (implode (separate "\n" (map single_fun_fix funs))); |
170 val _ = warning (implode (separate "\n" (map single_fun_fix funs))); |
156 val _ = warning (implode (separate "\n" (map (single_fun_eq lthy) feqs))); |
171 val _ = warning (implode (separate "\n" (map (single_fun_eq lthy) feqs))); |
157 val _ = warning (implode (separate "\n" (map (fv_dt lthy) dts))); |
172 val _ = warning (implode (separate "\n" (map (fv_dt lthy (map dt_name dts)) dts))); |
158 in |
173 in |
159 lthy |
174 lthy |
160 end |
175 end |
161 *} |
176 *} |
162 |
177 |