2223 | read_parent (SOME raw_T) ctxt = |
2223 | read_parent (SOME raw_T) ctxt = |
2224 (case Proof_Context.read_typ_abbrev ctxt raw_T of |
2224 (case Proof_Context.read_typ_abbrev ctxt raw_T of |
2225 Type (name, Ts) => (SOME (Ts, name), fold Variable.declare_typ Ts ctxt) |
2225 Type (name, Ts) => (SOME (Ts, name), fold Variable.declare_typ Ts ctxt) |
2226 | T => error ("Bad parent record specification: " ^ Syntax.string_of_typ ctxt T)); |
2226 | T => error ("Bad parent record specification: " ^ Syntax.string_of_typ ctxt T)); |
2227 |
2227 |
2228 fun prep_field prep (x, T, mx) = (x, prep T, mx) |
2228 fun read_fields raw_fields ctxt = |
2229 handle ERROR msg => |
2229 let |
2230 cat_error msg ("The error(s) above occurred in record field " ^ Binding.print x); |
2230 val Ts = Syntax.read_typs ctxt (map (fn (_, raw_T, _) => raw_T) raw_fields); |
2231 |
2231 val fields = map2 (fn (x, _, mx) => fn T => (x, T, mx)) raw_fields Ts; |
2232 fun read_field raw_field ctxt = |
2232 val ctxt' = fold Variable.declare_typ Ts ctxt; |
2233 let val field as (_, T, _) = prep_field (Syntax.read_typ ctxt) raw_field |
2233 in (fields, ctxt') end; |
2234 in (field, Variable.declare_typ T ctxt) end; |
|
2235 |
2234 |
2236 in |
2235 in |
2237 |
2236 |
2238 fun add_record (params, binding) raw_parent raw_fields thy = |
2237 fun add_record (params, binding) raw_parent raw_fields thy = |
2239 let |
2238 let |
2250 handle ERROR msg => |
2249 handle ERROR msg => |
2251 cat_error msg ("The error(s) above occurred in parent record specification"); |
2250 cat_error msg ("The error(s) above occurred in parent record specification"); |
2252 val parent_args = (case parent of SOME (Ts, _) => Ts | NONE => []); |
2251 val parent_args = (case parent of SOME (Ts, _) => Ts | NONE => []); |
2253 val parents = get_parent_info thy parent; |
2252 val parents = get_parent_info thy parent; |
2254 |
2253 |
2255 val bfields = map (prep_field cert_typ) raw_fields; |
2254 val bfields = |
|
2255 raw_fields |> map (fn (x, raw_T, mx) => (x, cert_typ raw_T, mx) |
|
2256 handle ERROR msg => |
|
2257 cat_error msg ("The error(s) above occurred in record field " ^ Binding.print x)); |
|
2258 |
2256 |
2259 |
2257 (* errors *) |
2260 (* errors *) |
2258 |
2261 |
2259 val name = Sign.full_name thy binding; |
2262 val name = Sign.full_name thy binding; |
2260 val err_dup_record = |
2263 val err_dup_record = |
2291 let |
2294 let |
2292 val ctxt = Proof_Context.init_global thy; |
2295 val ctxt = Proof_Context.init_global thy; |
2293 val params = map (apsnd (Typedecl.read_constraint ctxt)) raw_params; |
2296 val params = map (apsnd (Typedecl.read_constraint ctxt)) raw_params; |
2294 val ctxt1 = fold (Variable.declare_typ o TFree) params ctxt; |
2297 val ctxt1 = fold (Variable.declare_typ o TFree) params ctxt; |
2295 val (parent, ctxt2) = read_parent raw_parent ctxt1; |
2298 val (parent, ctxt2) = read_parent raw_parent ctxt1; |
2296 val (fields, ctxt3) = fold_map read_field raw_fields ctxt2; |
2299 val (fields, ctxt3) = read_fields raw_fields ctxt2; |
2297 val params' = map (Proof_Context.check_tfree ctxt3) params; |
2300 val params' = map (Proof_Context.check_tfree ctxt3) params; |
2298 in thy |> add_record (params', binding) parent fields end; |
2301 in thy |> add_record (params', binding) parent fields end; |
2299 |
2302 |
2300 end; |
2303 end; |
2301 |
2304 |