--- a/src/HOL/Tools/record.ML Tue Jul 27 20:16:03 2010 +0200
+++ b/src/HOL/Tools/record.ML Tue Jul 27 20:16:14 2010 +0200
@@ -7,9 +7,13 @@
Extensible records with structural subtyping.
*)
-signature BASIC_RECORD =
+signature RECORD =
sig
- type record_info =
+ val print_type_abbr: bool Unsynchronized.ref
+ val print_type_as_fields: bool Unsynchronized.ref
+ val timing: bool Unsynchronized.ref
+
+ type info =
{args: (string * sort) list,
parent: (typ list * string) option,
fields: (string * typ) list,
@@ -19,30 +23,11 @@
fold_congs: thm list, unfold_congs: thm list, splits: thm list, defs: thm list,
surjective: thm, equality: thm, induct_scheme: thm, induct: thm, cases_scheme: thm,
cases: thm, simps: thm list, iffs: thm list}
- val get_record: theory -> string -> record_info option
- val the_record: theory -> string -> record_info
- val record_simproc: simproc
- val record_eq_simproc: simproc
- val record_upd_simproc: simproc
- val record_split_simproc: (term -> int) -> simproc
- val record_ex_sel_eq_simproc: simproc
- val record_split_tac: int -> tactic
- val record_split_simp_tac: thm list -> (term -> int) -> int -> tactic
- val record_split_name: string
- val record_split_wrapper: string * wrapper
- val print_record_type_abbr: bool Unsynchronized.ref
- val print_record_type_as_fields: bool Unsynchronized.ref
-end;
-
-signature RECORD =
-sig
- include BASIC_RECORD
- val timing: bool Unsynchronized.ref
- val updateN: string
- val ext_typeN: string
- val extN: string
- val makeN: string
- val moreN: string
+ val get_info: theory -> string -> info option
+ val the_info: theory -> string -> info
+ val add_record: bool -> (string * sort) list * binding -> (typ list * string) option ->
+ (binding * typ * mixfix) list -> theory -> theory
+
val last_extT: typ -> (string * typ list) option
val dest_recTs: typ -> (string * typ list) list
val get_extT_fields: theory -> typ -> (string * typ) list * (string * typ)
@@ -51,13 +36,20 @@
val get_extension: theory -> string -> (string * typ list) option
val get_extinjects: theory -> thm list
val get_simpset: theory -> simpset
- val print_records: theory -> unit
+ val simproc: simproc
+ val eq_simproc: simproc
+ val upd_simproc: simproc
+ val split_simproc: (term -> int) -> simproc
+ val ex_sel_eq_simproc: simproc
+ val split_tac: int -> tactic
+ val split_simp_tac: thm list -> (term -> int) -> int -> tactic
+ val split_wrapper: string * wrapper
+
+ val updateN: string
+ val ext_typeN: string
+ val extN: string
val read_typ: Proof.context -> string -> (string * sort) list -> typ * (string * sort) list
val cert_typ: Proof.context -> typ -> (string * sort) list -> typ * (string * sort) list
- val add_record: bool -> (string * sort) list * binding -> (typ list * string) option ->
- (binding * typ * mixfix) list -> theory -> theory
- val add_record_cmd: bool -> (string * string option) list * binding -> string option ->
- (binding * string * mixfix) list -> theory -> theory
val setup: theory -> theory
end;
@@ -339,9 +331,9 @@
(** record info **)
-(* type record_info and parent_info *)
-
-type record_info =
+(* type info and parent_info *)
+
+type info =
{args: (string * sort) list,
parent: (typ list * string) option,
fields: (string * typ) list,
@@ -372,11 +364,11 @@
simps: thm list,
iffs: thm list};
-fun make_record_info args parent fields extension
+fun make_info args parent fields extension
ext_induct ext_inject ext_surjective ext_split ext_def
select_convs update_convs select_defs update_defs fold_congs unfold_congs splits defs
surjective equality induct_scheme induct cases_scheme cases
- simps iffs : record_info =
+ simps iffs : info =
{args = args, parent = parent, fields = fields, extension = extension,
ext_induct = ext_induct, ext_inject = ext_inject, ext_surjective = ext_surjective,
ext_split = ext_split, ext_def = ext_def, select_convs = select_convs,
@@ -399,8 +391,8 @@
(* theory data *)
-type record_data =
- {records: record_info Symtab.table,
+type data =
+ {records: info Symtab.table,
sel_upd:
{selectors: (int * bool) Symtab.table,
updates: string Symtab.table,
@@ -415,17 +407,17 @@
extfields: (string * typ) list Symtab.table, (*maps extension to its fields*)
fieldext: (string * typ list) Symtab.table}; (*maps field to its extension*)
-fun make_record_data
+fun make_data
records sel_upd equalities extinjects extsplit splits extfields fieldext =
{records = records, sel_upd = sel_upd,
equalities = equalities, extinjects=extinjects, extsplit = extsplit, splits = splits,
- extfields = extfields, fieldext = fieldext }: record_data;
+ extfields = extfields, fieldext = fieldext }: data;
structure Records_Data = Theory_Data
(
- type T = record_data;
+ type T = data;
val empty =
- make_record_data Symtab.empty
+ make_data Symtab.empty
{selectors = Symtab.empty, updates = Symtab.empty,
simpset = HOL_basic_ss, defset = HOL_basic_ss,
foldcong = HOL_basic_ss, unfoldcong = HOL_basic_ss}
@@ -454,7 +446,7 @@
splits = splits2,
extfields = extfields2,
fieldext = fieldext2}) =
- make_record_data
+ make_data
(Symtab.merge (K true) (recs1, recs2))
{selectors = Symtab.merge (K true) (sels1, sels2),
updates = Symtab.merge (K true) (upds1, upds2),
@@ -472,32 +464,13 @@
(Symtab.merge (K true) (fieldext1, fieldext2));
);
-fun print_records thy =
- let
- val {records = recs, ...} = Records_Data.get thy;
- val prt_typ = Syntax.pretty_typ_global thy;
-
- fun pretty_parent NONE = []
- | pretty_parent (SOME (Ts, name)) =
- [Pretty.block [prt_typ (Type (name, Ts)), Pretty.str " +"]];
-
- fun pretty_field (c, T) = Pretty.block
- [Pretty.str (Sign.extern_const thy c), Pretty.str " ::",
- Pretty.brk 1, Pretty.quote (prt_typ T)];
-
- fun pretty_record (name, {args, parent, fields, ...}: record_info) =
- Pretty.block (Pretty.fbreaks (Pretty.block
- [prt_typ (Type (name, map TFree args)), Pretty.str " = "] ::
- pretty_parent parent @ map pretty_field fields));
- in map pretty_record (Symtab.dest recs) |> Pretty.chunks |> Pretty.writeln end;
-
(* access 'records' *)
-val get_record = Symtab.lookup o #records o Records_Data.get;
-
-fun the_record thy name =
- (case get_record thy name of
+val get_info = Symtab.lookup o #records o Records_Data.get;
+
+fun the_info thy name =
+ (case get_info thy name of
SOME info => info
| NONE => error ("Unknown record type " ^ quote name));
@@ -505,7 +478,7 @@
let
val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
Records_Data.get thy;
- val data = make_record_data (Symtab.update (name, info) records)
+ val data = make_data (Symtab.update (name, info) records)
sel_upd equalities extinjects extsplit splits extfields fieldext;
in Records_Data.put data thy end;
@@ -538,7 +511,7 @@
val {records, sel_upd = {selectors, updates, simpset, defset, foldcong, unfoldcong},
equalities, extinjects, extsplit, splits, extfields, fieldext} = Records_Data.get thy;
- val data = make_record_data records
+ val data = make_data records
{selectors = fold Symtab.update_new sels selectors,
updates = fold Symtab.update_new upds updates,
simpset = Simplifier.addsimps (simpset, simps),
@@ -551,11 +524,11 @@
(* access 'equalities' *)
-fun add_record_equalities name thm thy =
+fun add_equalities name thm thy =
let
val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
Records_Data.get thy;
- val data = make_record_data records sel_upd
+ val data = make_data records sel_upd
(Symtab.update_new (name, thm) equalities) extinjects extsplit splits extfields fieldext;
in Records_Data.put data thy end;
@@ -569,7 +542,7 @@
val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
Records_Data.get thy;
val data =
- make_record_data records sel_upd equalities (insert Thm.eq_thm_prop thm extinjects)
+ make_data records sel_upd equalities (insert Thm.eq_thm_prop thm extinjects)
extsplit splits extfields fieldext;
in Records_Data.put data thy end;
@@ -583,19 +556,19 @@
val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
Records_Data.get thy;
val data =
- make_record_data records sel_upd equalities extinjects
+ make_data records sel_upd equalities extinjects
(Symtab.update_new (name, thm) extsplit) splits extfields fieldext;
in Records_Data.put data thy end;
(* access 'splits' *)
-fun add_record_splits name thmP thy =
+fun add_splits name thmP thy =
let
val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
Records_Data.get thy;
val data =
- make_record_data records sel_upd equalities extinjects extsplit
+ make_data records sel_upd equalities extinjects extsplit
(Symtab.update_new (name, thmP) splits) extfields fieldext;
in Records_Data.put data thy end;
@@ -615,7 +588,7 @@
val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
Records_Data.get thy;
val data =
- make_record_data records sel_upd equalities extinjects extsplit splits
+ make_data records sel_upd equalities extinjects extsplit splits
(Symtab.update_new (name, fields) extfields) fieldext;
in Records_Data.put data thy end;
@@ -655,7 +628,7 @@
val fieldext' =
fold (fn field => Symtab.update_new (field, extname_types)) fields fieldext;
val data =
- make_record_data records sel_upd equalities extinjects
+ make_data records sel_upd equalities extinjects
extsplit splits extfields fieldext';
in Records_Data.put data thy end;
@@ -670,7 +643,7 @@
fun err msg = error (msg ^ " parent record " ^ quote name);
val {args, parent, fields, extension, induct_scheme, ext_def, ...} =
- (case get_record thy name of SOME info => info | NONE => err "Unknown");
+ (case get_info thy name of SOME info => info | NONE => err "Unknown");
val _ = if length types <> length args then err "Bad number of arguments for" else ();
fun bad_inst ((x, S), T) =
@@ -837,8 +810,8 @@
(* print translations *)
-val print_record_type_abbr = Unsynchronized.ref true;
-val print_record_type_as_fields = Unsynchronized.ref true;
+val print_type_abbr = Unsynchronized.ref true;
+val print_type_as_fields = Unsynchronized.ref true;
local
@@ -886,7 +859,7 @@
val _ = null fields andalso raise Match;
val u = foldr1 field_types_tr' (map (field_type_tr' o apsnd term_of_type) fields);
in
- if not (! print_record_type_as_fields) orelse null fields then raise Match
+ if not (! print_type_as_fields) orelse null fields then raise Match
else if moreT = HOLogic.unitT then Syntax.const @{syntax_const "_record_type"} $ u
else Syntax.const @{syntax_const "_record_type_scheme"} $ u $ term_of_type moreT
end;
@@ -906,7 +879,7 @@
fun match rT T = Type.raw_match (varifyT rT, T) Vartab.empty;
in
- if ! print_record_type_abbr then
+ if ! print_type_abbr then
(case last_extT T of
SOME (name, _) =>
if name = last_ext then
@@ -1175,7 +1148,7 @@
in
-(* record_simproc *)
+(* simproc *)
(*
Simplify selections of an record update:
@@ -1191,7 +1164,7 @@
- If X is a more-selector we have to make sure that S is not in the updated
subrecord.
*)
-val record_simproc =
+val simproc =
Simplifier.simproc @{theory HOL} "record_simp" ["x"]
(fn thy => fn _ => fn t =>
(case t of
@@ -1255,7 +1228,7 @@
end;
-(* record_upd_simproc *)
+(* upd_simproc *)
(*Simplify multiple updates:
(1) "N_update y (M_update g (N_update x (M_update f r))) =
@@ -1265,7 +1238,7 @@
In both cases "more" updates complicate matters: for this reason
we omit considering further updates if doing so would introduce
both a more update and an update to a field within it.*)
-val record_upd_simproc =
+val upd_simproc =
Simplifier.simproc @{theory HOL} "record_upd_simp" ["x"]
(fn thy => fn _ => fn t =>
let
@@ -1363,7 +1336,7 @@
in
if simp then
SOME
- (prove_unfold_defs thy noops' [record_simproc]
+ (prove_unfold_defs thy noops' [simproc]
(list_all (vars, Logic.mk_equals (lhs, rhs))))
else NONE
end);
@@ -1371,7 +1344,7 @@
end;
-(* record_eq_simproc *)
+(* eq_simproc *)
(*Look up the most specific record-equality.
@@ -1379,13 +1352,13 @@
Testing equality of records boils down to the test of equality of all components.
Therefore the complexity is: #components * complexity for single component.
Especially if a record has a lot of components it may be better to split up
- the record first and do simplification on that (record_split_simp_tac).
+ the record first and do simplification on that (split_simp_tac).
e.g. r(|lots of updates|) = x
- record_eq_simproc record_split_simp_tac
+ eq_simproc split_simp_tac
Complexity: #components * #updates #updates
*)
-val record_eq_simproc =
+val eq_simproc =
Simplifier.simproc @{theory HOL} "record_eq_simp" ["r = s"]
(fn thy => fn _ => fn t =>
(case t of Const (@{const_name "op ="}, Type (_, [T, _])) $ _ $ _ =>
@@ -1398,14 +1371,14 @@
| _ => NONE));
-(* record_split_simproc *)
+(* split_simproc *)
(*Split quantified occurrences of records, for which P holds. P can peek on the
subterm starting at the quantified occurrence of the record (including the quantifier):
P t = 0: do not split
P t = ~1: completely split
P t > 0: split up to given bound of record extensions.*)
-fun record_split_simproc P =
+fun split_simproc P =
Simplifier.simproc @{theory HOL} "record_split_simp" ["x"]
(fn thy => fn _ => fn t =>
(case t of
@@ -1427,20 +1400,20 @@
@{const_name all} => all_thm
| @{const_name All} => All_thm RS eq_reflection
| @{const_name Ex} => Ex_thm RS eq_reflection
- | _ => error "record_split_simproc"))
+ | _ => error "split_simproc"))
else NONE
end)
else NONE
| _ => NONE));
-val record_ex_sel_eq_simproc =
- Simplifier.simproc @{theory HOL} "record_ex_sel_eq_simproc" ["Ex t"]
+val ex_sel_eq_simproc =
+ Simplifier.simproc @{theory HOL} "ex_sel_eq_simproc" ["Ex t"]
(fn thy => fn ss => fn t =>
let
fun prove prop =
prove_global true thy [] prop
(fn _ => simp_tac (Simplifier.inherit_context ss (get_simpset thy)
- addsimps @{thms simp_thms} addsimprocs [record_split_simproc (K ~1)]) 1);
+ addsimps @{thms simp_thms} addsimprocs [split_simproc (K ~1)]) 1);
fun mkeq (lr, Teq, (sel, Tsel), x) i =
if is_selector thy sel then
@@ -1474,7 +1447,7 @@
end);
-(* record_split_simp_tac *)
+(* split_simp_tac *)
(*Split (and simplify) all records in the goal for which P holds.
For quantified occurrences of a record
@@ -1483,7 +1456,7 @@
P t = 0: do not split
P t = ~1: completely split
P t > 0: split up to given bound of record extensions.*)
-fun record_split_simp_tac thms P = CSUBGOAL (fn (cgoal, i) =>
+fun split_simp_tac thms P = CSUBGOAL (fn (cgoal, i) =>
let
val thy = Thm.theory_of_cterm cgoal;
@@ -1525,7 +1498,7 @@
else NONE
end));
- val simprocs = if has_rec goal then [record_split_simproc P] else [];
+ val simprocs = if has_rec goal then [split_simproc P] else [];
val thms' = K_comp_convs @ thms;
in
EVERY split_frees_tacs THEN
@@ -1533,10 +1506,10 @@
end);
-(* record_split_tac *)
+(* split_tac *)
(*Split all records in the goal, which are quantified by !! or ALL.*)
-val record_split_tac = CSUBGOAL (fn (cgoal, i) =>
+val split_tac = CSUBGOAL (fn (cgoal, i) =>
let
val goal = term_of cgoal;
@@ -1550,15 +1523,15 @@
| is_all _ = 0;
in
if has_rec goal then
- Simplifier.full_simp_tac (HOL_basic_ss addsimprocs [record_split_simproc is_all]) i
+ Simplifier.full_simp_tac (HOL_basic_ss addsimprocs [split_simproc is_all]) i
else no_tac
end);
(* wrapper *)
-val record_split_name = "record_split_tac";
-val record_split_wrapper = (record_split_name, fn tac => record_split_tac ORELSE' tac);
+val split_name = "record_split_tac";
+val split_wrapper = (split_name, fn tac => split_tac ORELSE' tac);
@@ -1842,9 +1815,9 @@
in Thm.implies_elim thm' thm end;
-(* record_definition *)
-
-fun record_definition (alphas, binding) parent (parents: parent_info list) raw_fields thy =
+(* definition *)
+
+fun definition (alphas, binding) parent (parents: parent_info list) raw_fields thy =
let
val prefix = Binding.name_of binding;
val name = Sign.full_name thy binding;
@@ -2342,7 +2315,7 @@
((Binding.name "iffs", iffs), [iff_add])];
val info =
- make_record_info alphas parent fields extension
+ make_info alphas parent fields extension
ext_induct ext_inject ext_surjective ext_split ext_def
sel_convs' upd_convs' sel_defs' upd_defs' fold_congs' unfold_congs' splits' derived_defs'
surjective' equality' induct_scheme' induct' cases_scheme' cases' simps' iffs';
@@ -2351,10 +2324,10 @@
thms_thy'
|> put_record name info
|> put_sel_upd names full_moreN depth sel_upd_simps sel_upd_defs (fold_congs', unfold_congs')
- |> add_record_equalities extension_id equality'
+ |> add_equalities extension_id equality'
|> add_extinjects ext_inject
|> add_extsplit extension_name ext_split
- |> add_record_splits extension_id (split_meta', split_object', split_ex', induct_scheme')
+ |> add_splits extension_id (split_meta', split_object', split_ex', induct_scheme')
|> add_extfields extension_name (fields @ [(full_moreN, moreT)])
|> add_fieldext (extension_name, snd extension) (names @ [full_moreN])
|> Sign.restore_naming thy;
@@ -2408,7 +2381,7 @@
val name = Sign.full_name thy binding;
val err_dup_record =
- if is_none (get_record thy name) then []
+ if is_none (get_info thy name) then []
else ["Duplicate definition of record " ^ quote name];
val spec_frees = fold Term.add_tfreesT (parent_args @ map #2 bfields) [];
@@ -2433,7 +2406,7 @@
err_dup_record @ err_extra_frees @ err_no_fields @ err_dup_fields @ err_bad_fields;
val _ = if null errs then () else error (cat_lines errs);
in
- thy |> record_definition (params, binding) parent parents bfields
+ thy |> definition (params, binding) parent parents bfields
end
handle ERROR msg => cat_error msg ("Failed to define record " ^ quote (Binding.str_of binding));
@@ -2456,7 +2429,7 @@
Sign.add_trfuns ([], parse_translation, [], []) #>
Sign.add_advanced_trfuns ([], advanced_parse_translation, [], []) #>
Simplifier.map_simpset (fn ss =>
- ss addsimprocs [record_simproc, record_upd_simproc, record_eq_simproc]);
+ ss addsimprocs [simproc, upd_simproc, eq_simproc]);
(* outer syntax *)
@@ -2469,6 +2442,3 @@
>> (fn (x, (y, z)) => Toplevel.theory (add_record_cmd false x y z)));
end;
-
-structure Basic_Record: BASIC_RECORD = Record;
-open Basic_Record;