# HG changeset patch # User wenzelm # Date 1266334816 -3600 # Node ID 9eb89f41c29d0dff9640b5c1f0c2c384ea9c577d # Parent f7bf73b0d7e5a4ffeeadec893d0b4ebf882eefc9 tuned; diff -r f7bf73b0d7e5 -r 9eb89f41c29d src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Tue Feb 16 16:03:06 2010 +0100 +++ b/src/HOL/Tools/record.ML Tue Feb 16 16:40:16 2010 +0100 @@ -711,63 +711,6 @@ local -fun field_update_tr (Const (@{syntax_const "_field_update"}, _) $ Const (name, _) $ arg) = - Syntax.const (suffix updateN name) $ Abs ("_", dummyT, arg) - | field_update_tr t = raise TERM ("field_update_tr", [t]); - -fun field_updates_tr (Const (@{syntax_const "_field_updates"}, _) $ t $ u) = - field_update_tr t :: field_updates_tr u - | field_updates_tr t = [field_update_tr t]; - -fun record_update_tr [t, u] = fold (curry op $) (field_updates_tr u) t - | record_update_tr ts = raise TERM ("record_update_tr", ts); - - -fun field_tr ((Const (@{syntax_const "_field"}, _) $ Const (name, _) $ arg)) = (name, arg) - | field_tr t = raise TERM ("field_tr", [t]); - -fun fields_tr (Const (@{syntax_const "_fields"}, _) $ t $ u) = field_tr t :: fields_tr u - | fields_tr t = [field_tr t]; - -fun record_fields_tr more ctxt t = - let - val thy = ProofContext.theory_of ctxt; - fun err msg = raise TERM ("Error in record input: " ^ msg, [t]); - - fun split_args (field :: fields) ((name, arg) :: fargs) = - if can (unsuffix name) field - then - let val (args, rest) = split_args fields fargs - in (arg :: args, rest) end - else err ("expecting field " ^ field ^ " but got " ^ name) - | split_args [] (fargs as (_ :: _)) = ([], fargs) - | split_args (_ :: _) [] = err "expecting more fields" - | split_args _ _ = ([], []); - - fun mk_ext (fargs as (name, _) :: _) = - (case get_fieldext thy (Sign.intern_const thy name) of - SOME (ext, _) => - (case get_extfields thy ext of - SOME fields => - let - val (args, rest) = split_args (map fst (but_last fields)) fargs; - val more' = mk_ext rest; - in - (* FIXME authentic syntax *) - list_comb (Syntax.const (suffix extN ext), args @ [more']) - end - | NONE => err ("no fields defined for " ^ ext)) - | NONE => err (name ^ " is no proper field")) - | mk_ext [] = more; - in mk_ext (fields_tr t) end; - -fun record_tr ctxt [t] = record_fields_tr (Syntax.const @{const_syntax Unity}) ctxt t - | record_tr _ ts = raise TERM ("record_tr", ts); - -fun record_scheme_tr ctxt [t, more] = record_fields_tr more ctxt t - | record_scheme_tr _ ts = raise TERM ("record_scheme_tr", ts); - - fun field_type_tr ((Const (@{syntax_const "_field_type"}, _) $ Const (name, _) $ arg)) = (name, arg) | field_type_tr t = raise TERM ("field_type_tr", [t]); @@ -829,6 +772,63 @@ fun record_type_scheme_tr ctxt [t, more] = record_field_types_tr more ctxt t | record_type_scheme_tr _ ts = raise TERM ("record_type_scheme_tr", ts); + +fun field_tr ((Const (@{syntax_const "_field"}, _) $ Const (name, _) $ arg)) = (name, arg) + | field_tr t = raise TERM ("field_tr", [t]); + +fun fields_tr (Const (@{syntax_const "_fields"}, _) $ t $ u) = field_tr t :: fields_tr u + | fields_tr t = [field_tr t]; + +fun record_fields_tr more ctxt t = + let + val thy = ProofContext.theory_of ctxt; + fun err msg = raise TERM ("Error in record input: " ^ msg, [t]); + + fun split_args (field :: fields) ((name, arg) :: fargs) = + if can (unsuffix name) field + then + let val (args, rest) = split_args fields fargs + in (arg :: args, rest) end + else err ("expecting field " ^ field ^ " but got " ^ name) + | split_args [] (fargs as (_ :: _)) = ([], fargs) + | split_args (_ :: _) [] = err "expecting more fields" + | split_args _ _ = ([], []); + + fun mk_ext (fargs as (name, _) :: _) = + (case get_fieldext thy (Sign.intern_const thy name) of + SOME (ext, _) => + (case get_extfields thy ext of + SOME fields => + let + val (args, rest) = split_args (map fst (but_last fields)) fargs; + val more' = mk_ext rest; + in + (* FIXME authentic syntax *) + list_comb (Syntax.const (suffix extN ext), args @ [more']) + end + | NONE => err ("no fields defined for " ^ ext)) + | NONE => err (name ^ " is no proper field")) + | mk_ext [] = more; + in mk_ext (fields_tr t) end; + +fun record_tr ctxt [t] = record_fields_tr (Syntax.const @{const_syntax Unity}) ctxt t + | record_tr _ ts = raise TERM ("record_tr", ts); + +fun record_scheme_tr ctxt [t, more] = record_fields_tr more ctxt t + | record_scheme_tr _ ts = raise TERM ("record_scheme_tr", ts); + + +fun field_update_tr (Const (@{syntax_const "_field_update"}, _) $ Const (name, _) $ arg) = + Syntax.const (suffix updateN name) $ Abs ("_", dummyT, arg) + | field_update_tr t = raise TERM ("field_update_tr", [t]); + +fun field_updates_tr (Const (@{syntax_const "_field_updates"}, _) $ t $ u) = + field_update_tr t :: field_updates_tr u + | field_updates_tr t = [field_update_tr t]; + +fun record_update_tr [t, u] = fold (curry op $) (field_updates_tr u) t + | record_update_tr ts = raise TERM ("record_update_tr", ts); + in val parse_translation = @@ -1429,8 +1429,8 @@ (fn thy => fn _ => fn t => (case t of Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ _ => - if quantifier = @{const_name All} orelse - quantifier = @{const_name all} orelse + if quantifier = @{const_name all} orelse + quantifier = @{const_name All} orelse quantifier = @{const_name Ex} then (case rec_id ~1 T of @@ -1554,20 +1554,20 @@ (* record_split_tac *) -(*Split all records in the goal, which are quantified by ALL or !!.*) +(*Split all records in the goal, which are quantified by !! or ALL.*) val record_split_tac = CSUBGOAL (fn (cgoal, i) => let val goal = term_of cgoal; val has_rec = exists_Const (fn (s, Type (_, [Type (_, [T, _]), _])) => - (s = @{const_name All} orelse s = @{const_name all}) andalso is_recT T + (s = @{const_name all} orelse s = @{const_name All}) andalso is_recT T | _ => false); fun is_all t = (case t of Const (quantifier, _) $ _ => - if quantifier = @{const_name All} orelse quantifier = @{const_name all} then ~1 else 0 + if quantifier = @{const_name all} orelse quantifier = @{const_name All} then ~1 else 0 | _ => 0); in if has_rec goal then