23 fold_congs: thm list, unfold_congs: thm list, splits: thm list, defs: thm list, |
23 fold_congs: thm list, unfold_congs: thm list, splits: thm list, defs: thm list, |
24 surjective: thm, equality: thm, induct_scheme: thm, induct: thm, cases_scheme: thm, |
24 surjective: thm, equality: thm, induct_scheme: thm, induct: thm, cases_scheme: thm, |
25 cases: thm, simps: thm list, iffs: thm list} |
25 cases: thm, simps: thm list, iffs: thm list} |
26 val get_info: theory -> string -> info option |
26 val get_info: theory -> string -> info option |
27 val the_info: theory -> string -> info |
27 val the_info: theory -> string -> info |
|
28 val get_hierarchy: theory -> (string * typ list) -> (string * (string * typ) list) list |
28 val add_record: bool -> (string * sort) list * binding -> (typ list * string) option -> |
29 val add_record: bool -> (string * sort) list * binding -> (typ list * string) option -> |
29 (binding * typ * mixfix) list -> theory -> theory |
30 (binding * typ * mixfix) list -> theory -> theory |
30 |
31 |
31 val last_extT: typ -> (string * typ list) option |
32 val last_extT: typ -> (string * typ list) option |
32 val dest_recTs: typ -> (string * typ list) list |
33 val dest_recTs: typ -> (string * typ list) list |
612 val get_fieldext = Symtab.lookup o #fieldext o Data.get; |
613 val get_fieldext = Symtab.lookup o #fieldext o Data.get; |
613 |
614 |
614 |
615 |
615 (* parent records *) |
616 (* parent records *) |
616 |
617 |
617 fun add_parents _ NONE parents = parents |
618 local |
618 | add_parents thy (SOME (types, name)) parents = |
619 |
|
620 fun add_parents _ NONE = I |
|
621 | add_parents thy (SOME (types, name)) = |
619 let |
622 let |
620 fun err msg = error (msg ^ " parent record " ^ quote name); |
623 fun err msg = error (msg ^ " parent record " ^ quote name); |
621 |
624 |
622 val {args, parent, fields, extension, induct_scheme, ext_def, ...} = |
625 val {args, parent, ...} = |
623 (case get_info thy name of SOME info => info | NONE => err "Unknown"); |
626 (case get_info thy name of SOME info => info | NONE => err "Unknown"); |
624 val _ = if length types <> length args then err "Bad number of arguments for" else (); |
627 val _ = if length types <> length args then err "Bad number of arguments for" else (); |
625 |
628 |
626 fun bad_inst ((x, S), T) = |
629 fun bad_inst ((x, S), T) = |
627 if Sign.of_sort thy (T, S) then NONE else SOME x |
630 if Sign.of_sort thy (T, S) then NONE else SOME x |
629 val _ = null bads orelse err ("Ill-sorted instantiation of " ^ commas bads ^ " in"); |
632 val _ = null bads orelse err ("Ill-sorted instantiation of " ^ commas bads ^ " in"); |
630 |
633 |
631 val inst = map fst args ~~ types; |
634 val inst = map fst args ~~ types; |
632 val subst = Term.map_type_tfree (the o AList.lookup (op =) inst o fst); |
635 val subst = Term.map_type_tfree (the o AList.lookup (op =) inst o fst); |
633 val parent' = Option.map (apfst (map subst)) parent; |
636 val parent' = Option.map (apfst (map subst)) parent; |
634 val fields' = map (apsnd subst) fields; |
637 in cons (name, inst) #> add_parents thy parent' end; |
635 val extension' = apsnd (map subst) extension; |
638 |
636 in |
639 in |
637 add_parents thy parent' |
640 |
638 (make_parent_info name fields' extension' ext_def induct_scheme :: parents) |
641 fun get_hierarchy thy (name, types) = add_parents thy (SOME (types, name)) []; |
639 end; |
642 |
|
643 fun get_parent_info thy parent = |
|
644 add_parents thy parent [] |> map (fn (name, inst) => |
|
645 let |
|
646 val subst = Term.map_type_tfree (the o AList.lookup (op =) inst o fst); |
|
647 val {fields, extension, induct_scheme, ext_def, ...} = the_info thy name; |
|
648 val fields' = map (apsnd subst) fields; |
|
649 val extension' = apsnd (map subst) extension; |
|
650 in make_parent_info name fields' extension' ext_def induct_scheme end); |
|
651 |
|
652 end; |
640 |
653 |
641 |
654 |
642 |
655 |
643 (** concrete syntax for records **) |
656 (** concrete syntax for records **) |
644 |
657 |
2413 |
2426 |
2414 val parent = Option.map (apfst (map cert_typ)) raw_parent |
2427 val parent = Option.map (apfst (map cert_typ)) raw_parent |
2415 handle ERROR msg => |
2428 handle ERROR msg => |
2416 cat_error msg ("The error(s) above occurred in parent record specification"); |
2429 cat_error msg ("The error(s) above occurred in parent record specification"); |
2417 val parent_args = (case parent of SOME (Ts, _) => Ts | NONE => []); |
2430 val parent_args = (case parent of SOME (Ts, _) => Ts | NONE => []); |
2418 val parents = add_parents thy parent []; |
2431 val parents = get_parent_info thy parent; |
2419 |
2432 |
2420 val bfields = map (prep_field cert_typ) raw_fields; |
2433 val bfields = map (prep_field cert_typ) raw_fields; |
2421 |
2434 |
2422 (* errors *) |
2435 (* errors *) |
2423 |
2436 |