tuned;
authorwenzelm
Tue Feb 16 16:40:16 2010 +0100 (2010-02-16)
changeset 351479eb89f41c29d
parent 35146 f7bf73b0d7e5
child 35148 3a34fee2cfcd
tuned;
src/HOL/Tools/record.ML
     1.1 --- a/src/HOL/Tools/record.ML	Tue Feb 16 16:03:06 2010 +0100
     1.2 +++ b/src/HOL/Tools/record.ML	Tue Feb 16 16:40:16 2010 +0100
     1.3 @@ -711,63 +711,6 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun field_update_tr (Const (@{syntax_const "_field_update"}, _) $ Const (name, _) $ arg) =
     1.8 -      Syntax.const (suffix updateN name) $ Abs ("_", dummyT, arg)
     1.9 -  | field_update_tr t = raise TERM ("field_update_tr", [t]);
    1.10 -
    1.11 -fun field_updates_tr (Const (@{syntax_const "_field_updates"}, _) $ t $ u) =
    1.12 -      field_update_tr t :: field_updates_tr u
    1.13 -  | field_updates_tr t = [field_update_tr t];
    1.14 -
    1.15 -fun record_update_tr [t, u] = fold (curry op $) (field_updates_tr u) t
    1.16 -  | record_update_tr ts = raise TERM ("record_update_tr", ts);
    1.17 -
    1.18 -
    1.19 -fun field_tr ((Const (@{syntax_const "_field"}, _) $ Const (name, _) $ arg)) = (name, arg)
    1.20 -  | field_tr t = raise TERM ("field_tr", [t]);
    1.21 -
    1.22 -fun fields_tr (Const (@{syntax_const "_fields"}, _) $ t $ u) = field_tr t :: fields_tr u
    1.23 -  | fields_tr t = [field_tr t];
    1.24 -
    1.25 -fun record_fields_tr more ctxt t =
    1.26 -  let
    1.27 -    val thy = ProofContext.theory_of ctxt;
    1.28 -    fun err msg = raise TERM ("Error in record input: " ^ msg, [t]);
    1.29 -
    1.30 -    fun split_args (field :: fields) ((name, arg) :: fargs) =
    1.31 -          if can (unsuffix name) field
    1.32 -          then
    1.33 -            let val (args, rest) = split_args fields fargs
    1.34 -            in (arg :: args, rest) end
    1.35 -          else err ("expecting field " ^ field ^ " but got " ^ name)
    1.36 -      | split_args [] (fargs as (_ :: _)) = ([], fargs)
    1.37 -      | split_args (_ :: _) [] = err "expecting more fields"
    1.38 -      | split_args _ _ = ([], []);
    1.39 -
    1.40 -    fun mk_ext (fargs as (name, _) :: _) =
    1.41 -          (case get_fieldext thy (Sign.intern_const thy name) of
    1.42 -            SOME (ext, _) =>
    1.43 -              (case get_extfields thy ext of
    1.44 -                SOME fields =>
    1.45 -                  let
    1.46 -                    val (args, rest) = split_args (map fst (but_last fields)) fargs;
    1.47 -                    val more' = mk_ext rest;
    1.48 -                  in
    1.49 -                    (* FIXME authentic syntax *)
    1.50 -                    list_comb (Syntax.const (suffix extN ext), args @ [more'])
    1.51 -                  end
    1.52 -              | NONE => err ("no fields defined for " ^ ext))
    1.53 -          | NONE => err (name ^ " is no proper field"))
    1.54 -      | mk_ext [] = more;
    1.55 -  in mk_ext (fields_tr t) end;
    1.56 -
    1.57 -fun record_tr ctxt [t] = record_fields_tr (Syntax.const @{const_syntax Unity}) ctxt t
    1.58 -  | record_tr _ ts = raise TERM ("record_tr", ts);
    1.59 -
    1.60 -fun record_scheme_tr ctxt [t, more] = record_fields_tr more ctxt t
    1.61 -  | record_scheme_tr _ ts = raise TERM ("record_scheme_tr", ts);
    1.62 -
    1.63 -
    1.64  fun field_type_tr ((Const (@{syntax_const "_field_type"}, _) $ Const (name, _) $ arg)) =
    1.65        (name, arg)
    1.66    | field_type_tr t = raise TERM ("field_type_tr", [t]);
    1.67 @@ -829,6 +772,63 @@
    1.68  fun record_type_scheme_tr ctxt [t, more] = record_field_types_tr more ctxt t
    1.69    | record_type_scheme_tr _ ts = raise TERM ("record_type_scheme_tr", ts);
    1.70  
    1.71 +
    1.72 +fun field_tr ((Const (@{syntax_const "_field"}, _) $ Const (name, _) $ arg)) = (name, arg)
    1.73 +  | field_tr t = raise TERM ("field_tr", [t]);
    1.74 +
    1.75 +fun fields_tr (Const (@{syntax_const "_fields"}, _) $ t $ u) = field_tr t :: fields_tr u
    1.76 +  | fields_tr t = [field_tr t];
    1.77 +
    1.78 +fun record_fields_tr more ctxt t =
    1.79 +  let
    1.80 +    val thy = ProofContext.theory_of ctxt;
    1.81 +    fun err msg = raise TERM ("Error in record input: " ^ msg, [t]);
    1.82 +
    1.83 +    fun split_args (field :: fields) ((name, arg) :: fargs) =
    1.84 +          if can (unsuffix name) field
    1.85 +          then
    1.86 +            let val (args, rest) = split_args fields fargs
    1.87 +            in (arg :: args, rest) end
    1.88 +          else err ("expecting field " ^ field ^ " but got " ^ name)
    1.89 +      | split_args [] (fargs as (_ :: _)) = ([], fargs)
    1.90 +      | split_args (_ :: _) [] = err "expecting more fields"
    1.91 +      | split_args _ _ = ([], []);
    1.92 +
    1.93 +    fun mk_ext (fargs as (name, _) :: _) =
    1.94 +          (case get_fieldext thy (Sign.intern_const thy name) of
    1.95 +            SOME (ext, _) =>
    1.96 +              (case get_extfields thy ext of
    1.97 +                SOME fields =>
    1.98 +                  let
    1.99 +                    val (args, rest) = split_args (map fst (but_last fields)) fargs;
   1.100 +                    val more' = mk_ext rest;
   1.101 +                  in
   1.102 +                    (* FIXME authentic syntax *)
   1.103 +                    list_comb (Syntax.const (suffix extN ext), args @ [more'])
   1.104 +                  end
   1.105 +              | NONE => err ("no fields defined for " ^ ext))
   1.106 +          | NONE => err (name ^ " is no proper field"))
   1.107 +      | mk_ext [] = more;
   1.108 +  in mk_ext (fields_tr t) end;
   1.109 +
   1.110 +fun record_tr ctxt [t] = record_fields_tr (Syntax.const @{const_syntax Unity}) ctxt t
   1.111 +  | record_tr _ ts = raise TERM ("record_tr", ts);
   1.112 +
   1.113 +fun record_scheme_tr ctxt [t, more] = record_fields_tr more ctxt t
   1.114 +  | record_scheme_tr _ ts = raise TERM ("record_scheme_tr", ts);
   1.115 +
   1.116 +
   1.117 +fun field_update_tr (Const (@{syntax_const "_field_update"}, _) $ Const (name, _) $ arg) =
   1.118 +      Syntax.const (suffix updateN name) $ Abs ("_", dummyT, arg)
   1.119 +  | field_update_tr t = raise TERM ("field_update_tr", [t]);
   1.120 +
   1.121 +fun field_updates_tr (Const (@{syntax_const "_field_updates"}, _) $ t $ u) =
   1.122 +      field_update_tr t :: field_updates_tr u
   1.123 +  | field_updates_tr t = [field_update_tr t];
   1.124 +
   1.125 +fun record_update_tr [t, u] = fold (curry op $) (field_updates_tr u) t
   1.126 +  | record_update_tr ts = raise TERM ("record_update_tr", ts);
   1.127 +
   1.128  in
   1.129  
   1.130  val parse_translation =
   1.131 @@ -1429,8 +1429,8 @@
   1.132      (fn thy => fn _ => fn t =>
   1.133        (case t of
   1.134          Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ _ =>
   1.135 -          if quantifier = @{const_name All} orelse
   1.136 -            quantifier = @{const_name all} orelse
   1.137 +          if quantifier = @{const_name all} orelse
   1.138 +            quantifier = @{const_name All} orelse
   1.139              quantifier = @{const_name Ex}
   1.140            then
   1.141              (case rec_id ~1 T of
   1.142 @@ -1554,20 +1554,20 @@
   1.143  
   1.144  (* record_split_tac *)
   1.145  
   1.146 -(*Split all records in the goal, which are quantified by ALL or !!.*)
   1.147 +(*Split all records in the goal, which are quantified by !! or ALL.*)
   1.148  val record_split_tac = CSUBGOAL (fn (cgoal, i) =>
   1.149    let
   1.150      val goal = term_of cgoal;
   1.151  
   1.152      val has_rec = exists_Const
   1.153        (fn (s, Type (_, [Type (_, [T, _]), _])) =>
   1.154 -          (s = @{const_name All} orelse s = @{const_name all}) andalso is_recT T
   1.155 +          (s = @{const_name all} orelse s = @{const_name All}) andalso is_recT T
   1.156          | _ => false);
   1.157  
   1.158      fun is_all t =
   1.159        (case t of
   1.160          Const (quantifier, _) $ _ =>
   1.161 -          if quantifier = @{const_name All} orelse quantifier = @{const_name all} then ~1 else 0
   1.162 +          if quantifier = @{const_name all} orelse quantifier = @{const_name All} then ~1 else 0
   1.163        | _ => 0);
   1.164    in
   1.165      if has_rec goal then