# HG changeset patch # User wenzelm # Date 1266323742 -3600 # Node ID 8b8302da3a550912999061fce6312b896f7f4c35 # Parent 7b2538c987e75353c9c26a3ba95cb08511206572 tuned; diff -r 7b2538c987e7 -r 8b8302da3a55 src/HOL/Record.thy --- a/src/HOL/Record.thy Tue Feb 16 13:26:21 2010 +0100 +++ b/src/HOL/Record.thy Tue Feb 16 13:35:42 2010 +0100 @@ -425,17 +425,17 @@ "_constify" :: "id => ident" ("_") "_constify" :: "longid => ident" ("_") - "_field_type" :: "[ident, type] => field_type" ("(2_ ::/ _)") + "_field_type" :: "ident => type => field_type" ("(2_ ::/ _)") "" :: "field_type => field_types" ("_") - "_field_types" :: "[field_type, field_types] => field_types" ("_,/ _") + "_field_types" :: "field_type => field_types => field_types" ("_,/ _") "_record_type" :: "field_types => type" ("(3'(| _ |'))") - "_record_type_scheme" :: "[field_types, type] => type" ("(3'(| _,/ (2... ::/ _) |'))") + "_record_type_scheme" :: "field_types => type => type" ("(3'(| _,/ (2... ::/ _) |'))") - "_field" :: "[ident, 'a] => field" ("(2_ =/ _)") + "_field" :: "ident => 'a => field" ("(2_ =/ _)") "" :: "field => fields" ("_") - "_fields" :: "[field, fields] => fields" ("_,/ _") + "_fields" :: "field => fields => fields" ("_,/ _") "_record" :: "fields => 'a" ("(3'(| _ |'))") - "_record_scheme" :: "[fields, 'a] => 'a" ("(3'(| _,/ (2... =/ _) |'))") + "_record_scheme" :: "fields => 'a => 'a" ("(3'(| _,/ (2... =/ _) |'))") "_update_name" :: idt "_update" :: "ident => 'a => update" ("(2_ :=/ _)") diff -r 7b2538c987e7 -r 8b8302da3a55 src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Tue Feb 16 13:26:21 2010 +0100 +++ b/src/HOL/Tools/record.ML Tue Feb 16 13:35:42 2010 +0100 @@ -270,11 +270,9 @@ val Trueprop = HOLogic.mk_Trueprop; fun All xs t = Term.list_all_free (xs, t); -infix 9 $$; infix 0 :== ===; infixr 0 ==>; -val op $$ = Term.list_comb; val op :== = Primitive_Defs.mk_defpair; val op === = Trueprop o HOLogic.mk_eq; val op ==> = Logic.mk_implies; @@ -586,9 +584,9 @@ 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 (Symtab.update_new (name, thm) extsplit) splits - extfields fieldext; + val data = + make_record_data records sel_upd equalities extinjects + (Symtab.update_new (name, thm) extsplit) splits extfields fieldext; in Records_Data.put data thy end; @@ -598,9 +596,9 @@ 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 (Symtab.update_new (name, thmP) splits) - extfields fieldext; + val data = + make_record_data records sel_upd equalities extinjects extsplit + (Symtab.update_new (name, thmP) splits) extfields fieldext; in Records_Data.put data thy end; val get_splits = Symtab.lookup o #splits o Records_Data.get; @@ -619,8 +617,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_record_data records sel_upd equalities extinjects extsplit splits (Symtab.update_new (name, fields) extfields) fieldext; in Records_Data.put data thy end; @@ -701,7 +698,8 @@ fun decode_type thy t = let - fun get_sort xs n = AList.lookup (op =) xs (n: indexname) |> the_default (Sign.defaultS thy); + fun get_sort env xi = + the_default (Sign.defaultS thy) (AList.lookup (op =) env (xi: indexname)); val map_sort = Sign.intern_sort thy; in Syntax.typ_of_term (get_sort (Syntax.term_sorts map_sort t)) map_sort t @@ -711,6 +709,8 @@ (* parse translations *) +local + fun gen_field_tr mark sfx (t as Const (c, _) $ Const (name, _) $ arg) = if c = mark then Syntax.const (suffix sfx name) $ Abs ("_", dummyT, arg) else raise TERM ("gen_field_tr: " ^ mark, [t]) @@ -721,17 +721,20 @@ else [gen_field_tr mark sfx tm] | gen_fields_tr _ mark sfx tm = [gen_field_tr mark sfx tm]; +in fun record_update_tr [t, u] = fold (curry op $) (gen_fields_tr @{syntax_const "_updates"} @{syntax_const "_update"} updateN u) t | record_update_tr ts = raise TERM ("record_update_tr", ts); -fun update_name_tr (Free (x, T) :: ts) = Free (suffix updateN x, T) $$ ts - | update_name_tr (Const (x, T) :: ts) = Const (suffix updateN x, T) $$ ts +end; + +fun update_name_tr (Free (x, T) :: ts) = list_comb (Free (suffix updateN x, T), ts) + | update_name_tr (Const (x, T) :: ts) = list_comb (Const (suffix updateN x, T), ts) | update_name_tr (((c as Const (@{syntax_const "_constrain"}, _)) $ t $ ty) :: ts) = (* FIXME @{type_syntax} *) - (c $ update_name_tr [t] $ (Syntax.const "fun" $ ty $ Syntax.const "dummy")) $$ ts + list_comb (c $ update_name_tr [t] $ (Syntax.const "fun" $ ty $ Syntax.const "dummy"), ts) | update_name_tr ts = raise TERM ("update_name_tr", ts); fun dest_ext_field mark (t as (Const (c, _) $ Const (name, _) $ arg)) = @@ -2091,15 +2094,18 @@ val upd_specs = map mk_upd_spec (fields_more ~~ lastN updator_thms); (*derived operations*) - val make_spec = Const (full (Binding.name makeN), all_types ---> recT0) $$ all_vars :== - mk_rec (all_vars @ [HOLogic.unit]) 0; - val fields_spec = Const (full (Binding.name fields_selN), types ---> Type extension) $$ vars :== - mk_rec (all_vars @ [HOLogic.unit]) parent_len; + val make_spec = + list_comb (Const (full (Binding.name makeN), all_types ---> recT0), all_vars) :== + mk_rec (all_vars @ [HOLogic.unit]) 0; + val fields_spec = + list_comb (Const (full (Binding.name fields_selN), types ---> Type extension), vars) :== + mk_rec (all_vars @ [HOLogic.unit]) parent_len; val extend_spec = Const (full (Binding.name extendN), recT0 --> moreT --> rec_schemeT0) $ r_unit0 $ more :== - mk_rec ((map (mk_sel r_unit0) all_fields) @ [more]) 0; - val truncate_spec = Const (full (Binding.name truncateN), rec_schemeT0 --> recT0) $ r0 :== - mk_rec ((map (mk_sel r0) all_fields) @ [HOLogic.unit]) 0; + mk_rec ((map (mk_sel r_unit0) all_fields) @ [more]) 0; + val truncate_spec = + Const (full (Binding.name truncateN), rec_schemeT0 --> recT0) $ r0 :== + mk_rec ((map (mk_sel r0) all_fields) @ [HOLogic.unit]) 0; (* 2st stage: defs_thy *)