src/HOL/Tools/record.ML
changeset 35240 663436ed5bd6
parent 35239 0dfec017bc83
child 35262 9ea4445d2ccf
     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