1.1 --- a/src/HOL/Tools/record.ML Fri Feb 19 21:31:14 2010 +0100
1.2 +++ b/src/HOL/Tools/record.ML Fri Feb 19 22:06:01 2010 +0100
1.3 @@ -842,96 +842,6 @@
1.4 val print_record_type_abbr = Unsynchronized.ref true;
1.5 val print_record_type_as_fields = Unsynchronized.ref true;
1.6
1.7 -local
1.8 -
1.9 -fun field_updates_tr' ctxt (tm as Const (c, _) $ k $ u) =
1.10 - let
1.11 - val extern = Consts.extern (ProofContext.consts_of ctxt);
1.12 - val t =
1.13 - (case k of
1.14 - Abs (_, _, Abs (_, _, t) $ Bound 0) =>
1.15 - if null (loose_bnos t) then t else raise Match
1.16 - | Abs (_, _, t) =>
1.17 - if null (loose_bnos t) then t else raise Match
1.18 - | _ => raise Match);
1.19 - in
1.20 - (case try (unprefix Syntax.constN) c |> Option.map extern of
1.21 - SOME update_name =>
1.22 - (case try (unsuffix updateN) update_name of
1.23 - SOME name =>
1.24 - apfst (cons (Syntax.const @{syntax_const "_field_update"} $ Syntax.free name $ t))
1.25 - (field_updates_tr' ctxt u)
1.26 - | NONE => ([], tm))
1.27 - | NONE => ([], tm))
1.28 - end
1.29 - | field_updates_tr' _ tm = ([], tm);
1.30 -
1.31 -fun record_update_tr' ctxt tm =
1.32 - (case field_updates_tr' ctxt tm of
1.33 - ([], _) => raise Match
1.34 - | (ts, u) =>
1.35 - Syntax.const @{syntax_const "_record_update"} $ u $
1.36 - foldr1 (fn (v, w) => Syntax.const @{syntax_const "_field_updates"} $ v $ w) (rev ts));
1.37 -
1.38 -in
1.39 -
1.40 -fun field_update_tr' name =
1.41 - let
1.42 - val update_name = Syntax.constN ^ name ^ updateN;
1.43 - fun tr' ctxt [t, u] = record_update_tr' ctxt (Syntax.const update_name $ t $ u)
1.44 - | tr' _ _ = raise Match;
1.45 - in (update_name, tr') end;
1.46 -
1.47 -end;
1.48 -
1.49 -
1.50 -local
1.51 -
1.52 -(* FIXME Syntax.free (??) *)
1.53 -fun field_tr' (c, t) = Syntax.const @{syntax_const "_field"} $ Syntax.const c $ t;
1.54 -fun fields_tr' (t, u) = Syntax.const @{syntax_const "_fields"} $ t $ u;
1.55 -
1.56 -fun record_tr' ctxt t =
1.57 - let
1.58 - val thy = ProofContext.theory_of ctxt;
1.59 - val extern = Consts.extern (ProofContext.consts_of ctxt);
1.60 -
1.61 - fun strip_fields t =
1.62 - (case strip_comb t of
1.63 - (Const (ext, _), args as (_ :: _)) =>
1.64 - (case try (unprefix Syntax.constN o unsuffix extN) ext of
1.65 - SOME ext' =>
1.66 - (case get_extfields thy ext' of
1.67 - SOME fields =>
1.68 - (let
1.69 - val f :: fs = but_last (map fst fields);
1.70 - val fields' = extern f :: map Long_Name.base_name fs;
1.71 - val (args', more) = split_last args;
1.72 - in (fields' ~~ args') @ strip_fields more end
1.73 - handle Library.UnequalLengths => [("", t)])
1.74 - | NONE => [("", t)])
1.75 - | NONE => [("", t)])
1.76 - | _ => [("", t)]);
1.77 -
1.78 - val (fields, (_, more)) = split_last (strip_fields t);
1.79 - val _ = null fields andalso raise Match;
1.80 - val u = foldr1 fields_tr' (map field_tr' fields);
1.81 - in
1.82 - case more of
1.83 - Const (@{const_syntax Unity}, _) => Syntax.const @{syntax_const "_record"} $ u
1.84 - | _ => Syntax.const @{syntax_const "_record_scheme"} $ u $ more
1.85 - end;
1.86 -
1.87 -in
1.88 -
1.89 -fun record_ext_tr' name =
1.90 - let
1.91 - val ext_name = Syntax.constN ^ name ^ extN;
1.92 - fun tr' ctxt ts = record_tr' ctxt (list_comb (Syntax.const ext_name, ts));
1.93 - in (ext_name, tr') end;
1.94 -
1.95 -end;
1.96 -
1.97
1.98 local
1.99
1.100 @@ -1053,6 +963,97 @@
1.101 end;
1.102
1.103
1.104 +local
1.105 +
1.106 +(* FIXME Syntax.free (??) *)
1.107 +fun field_tr' (c, t) = Syntax.const @{syntax_const "_field"} $ Syntax.const c $ t;
1.108 +fun fields_tr' (t, u) = Syntax.const @{syntax_const "_fields"} $ t $ u;
1.109 +
1.110 +fun record_tr' ctxt t =
1.111 + let
1.112 + val thy = ProofContext.theory_of ctxt;
1.113 + val extern = Consts.extern (ProofContext.consts_of ctxt);
1.114 +
1.115 + fun strip_fields t =
1.116 + (case strip_comb t of
1.117 + (Const (ext, _), args as (_ :: _)) =>
1.118 + (case try (unprefix Syntax.constN o unsuffix extN) ext of
1.119 + SOME ext' =>
1.120 + (case get_extfields thy ext' of
1.121 + SOME fields =>
1.122 + (let
1.123 + val f :: fs = but_last (map fst fields);
1.124 + val fields' = extern f :: map Long_Name.base_name fs;
1.125 + val (args', more) = split_last args;
1.126 + in (fields' ~~ args') @ strip_fields more end
1.127 + handle Library.UnequalLengths => [("", t)])
1.128 + | NONE => [("", t)])
1.129 + | NONE => [("", t)])
1.130 + | _ => [("", t)]);
1.131 +
1.132 + val (fields, (_, more)) = split_last (strip_fields t);
1.133 + val _ = null fields andalso raise Match;
1.134 + val u = foldr1 fields_tr' (map field_tr' fields);
1.135 + in
1.136 + case more of
1.137 + Const (@{const_syntax Unity}, _) => Syntax.const @{syntax_const "_record"} $ u
1.138 + | _ => Syntax.const @{syntax_const "_record_scheme"} $ u $ more
1.139 + end;
1.140 +
1.141 +in
1.142 +
1.143 +fun record_ext_tr' name =
1.144 + let
1.145 + val ext_name = Syntax.constN ^ name ^ extN;
1.146 + fun tr' ctxt ts = record_tr' ctxt (list_comb (Syntax.const ext_name, ts));
1.147 + in (ext_name, tr') end;
1.148 +
1.149 +end;
1.150 +
1.151 +
1.152 +local
1.153 +
1.154 +fun field_updates_tr' ctxt (tm as Const (c, _) $ k $ u) =
1.155 + let
1.156 + val extern = Consts.extern (ProofContext.consts_of ctxt);
1.157 + val t =
1.158 + (case k of
1.159 + Abs (_, _, Abs (_, _, t) $ Bound 0) =>
1.160 + if null (loose_bnos t) then t else raise Match
1.161 + | Abs (_, _, t) =>
1.162 + if null (loose_bnos t) then t else raise Match
1.163 + | _ => raise Match);
1.164 + in
1.165 + (case try (unprefix Syntax.constN) c |> Option.map extern of
1.166 + SOME update_name =>
1.167 + (case try (unsuffix updateN) update_name of
1.168 + SOME name =>
1.169 + apfst (cons (Syntax.const @{syntax_const "_field_update"} $ Syntax.free name $ t))
1.170 + (field_updates_tr' ctxt u)
1.171 + | NONE => ([], tm))
1.172 + | NONE => ([], tm))
1.173 + end
1.174 + | field_updates_tr' _ tm = ([], tm);
1.175 +
1.176 +fun record_update_tr' ctxt tm =
1.177 + (case field_updates_tr' ctxt tm of
1.178 + ([], _) => raise Match
1.179 + | (ts, u) =>
1.180 + Syntax.const @{syntax_const "_record_update"} $ u $
1.181 + foldr1 (fn (v, w) => Syntax.const @{syntax_const "_field_updates"} $ v $ w) (rev ts));
1.182 +
1.183 +in
1.184 +
1.185 +fun field_update_tr' name =
1.186 + let
1.187 + val update_name = Syntax.constN ^ name ^ updateN;
1.188 + fun tr' ctxt [t, u] = record_update_tr' ctxt (Syntax.const update_name $ t $ u)
1.189 + | tr' _ _ = raise Match;
1.190 + in (update_name, tr') end;
1.191 +
1.192 +end;
1.193 +
1.194 +
1.195
1.196 (** record simprocs **)
1.197
1.198 @@ -1567,11 +1568,9 @@
1.199 (s = @{const_name all} orelse s = @{const_name All}) andalso is_recT T
1.200 | _ => false);
1.201
1.202 - fun is_all t = (* FIXME *)
1.203 - (case t of
1.204 - Const (quantifier, _) $ _ =>
1.205 - if quantifier = @{const_name all} orelse quantifier = @{const_name All} then ~1 else 0
1.206 - | _ => 0);
1.207 + fun is_all (Const (@{const_name all}, _) $ _) = ~1
1.208 + | is_all (Const (@{const_name All}, _) $ _) = ~1
1.209 + | is_all _ = 0;
1.210 in
1.211 if has_rec goal then
1.212 Simplifier.full_simp_tac (HOL_basic_ss addsimprocs [record_split_simproc is_all]) i