src/HOL/Tools/record.ML
changeset 35149 eee63670b5aa
parent 35148 3a34fee2cfcd
child 35232 f588e1169c8b
     1.1 --- a/src/HOL/Tools/record.ML	Tue Feb 16 16:42:18 2010 +0100
     1.2 +++ b/src/HOL/Tools/record.ML	Tue Feb 16 20:41:52 2010 +0100
     1.3 @@ -632,20 +632,20 @@
     1.4      val midx = maxidx_of_typs (moreT :: Ts);
     1.5      val varifyT = varifyT midx;
     1.6      val {records, extfields, ...} = Records_Data.get thy;
     1.7 -    val (flds, (more, _)) = split_last (Symtab.lookup_list extfields name);
     1.8 +    val (fields, (more, _)) = split_last (Symtab.lookup_list extfields name);
     1.9      val args = map varifyT (snd (#extension (the (Symtab.lookup records recname))));
    1.10  
    1.11 -    val subst = fold (Sign.typ_match thy) (but_last args ~~ but_last Ts) (Vartab.empty);
    1.12 -    val flds' = map (apsnd (Envir.norm_type subst o varifyT)) flds;
    1.13 -  in (flds', (more, moreT)) end;
    1.14 +    val subst = fold (Sign.typ_match thy) (but_last args ~~ but_last Ts) Vartab.empty;
    1.15 +    val fields' = map (apsnd (Envir.norm_type subst o varifyT)) fields;
    1.16 +  in (fields', (more, moreT)) end;
    1.17  
    1.18  fun get_recT_fields thy T =
    1.19    let
    1.20 -    val (root_flds, (root_more, root_moreT)) = get_extT_fields thy T;
    1.21 -    val (rest_flds, rest_more) =
    1.22 +    val (root_fields, (root_more, root_moreT)) = get_extT_fields thy T;
    1.23 +    val (rest_fields, rest_more) =
    1.24        if is_recT root_moreT then get_recT_fields thy root_moreT
    1.25        else ([], (root_more, root_moreT));
    1.26 -  in (root_flds @ rest_flds, rest_more) end;
    1.27 +  in (root_fields @ rest_fields, rest_more) end;
    1.28  
    1.29  
    1.30  (* access 'fieldext' *)
    1.31 @@ -848,7 +848,9 @@
    1.32  val print_record_type_abbr = Unsynchronized.ref true;
    1.33  val print_record_type_as_fields = Unsynchronized.ref true;
    1.34  
    1.35 -fun gen_field_upds_tr' mark sfx (tm as Const (name_field, _) $ k $ u) =
    1.36 +local
    1.37 +
    1.38 +fun field_updates_tr' (tm as Const (c, _) $ k $ u) =
    1.39        let
    1.40          val t =
    1.41            (case k of
    1.42 @@ -858,78 +860,139 @@
    1.43                if null (loose_bnos t) then t else raise Match
    1.44            | _ => raise Match);
    1.45        in
    1.46 -        (case try (unsuffix sfx) name_field of
    1.47 +        (case try (unsuffix updateN) c of
    1.48            SOME name =>
    1.49 -            apfst (cons (Syntax.const mark $ Syntax.free name $ t))
    1.50 -              (gen_field_upds_tr' mark sfx u)
    1.51 +            (* FIXME check wrt. record data (??) *)
    1.52 +            (* FIXME early extern (!??) *)
    1.53 +            apfst (cons (Syntax.const @{syntax_const "_field_update"} $ Syntax.free name $ t))
    1.54 +              (field_updates_tr' u)
    1.55          | NONE => ([], tm))
    1.56        end
    1.57 -  | gen_field_upds_tr' _ _ tm = ([], tm);
    1.58 +  | field_updates_tr' tm = ([], tm);
    1.59  
    1.60  fun record_update_tr' tm =
    1.61 -  (case gen_field_upds_tr' @{syntax_const "_field_update"} updateN tm of
    1.62 +  (case field_updates_tr' tm of
    1.63      ([], _) => raise Match
    1.64    | (ts, u) =>
    1.65        Syntax.const @{syntax_const "_record_update"} $ u $
    1.66          foldr1 (fn (v, w) => Syntax.const @{syntax_const "_field_updates"} $ v $ w) (rev ts));
    1.67  
    1.68 -fun gen_field_tr' sfx tr' name =
    1.69 -  let val name_sfx = suffix sfx name
    1.70 -  in (name_sfx, fn [t, u] => tr' (Syntax.const name_sfx $ t $ u) | _ => raise Match) end;
    1.71 -
    1.72 -fun record_tr' sep mark record record_scheme unit ctxt t =
    1.73 +in
    1.74 +
    1.75 +fun field_update_tr' name =
    1.76 +  let
    1.77 +    (* FIXME authentic syntax *)
    1.78 +    val update_name = suffix updateN name;
    1.79 +    fun tr' [t, u] = record_update_tr' (Syntax.const update_name $ t $ u)
    1.80 +      | tr' _ = raise Match;
    1.81 +  in (update_name, tr') end;
    1.82 +
    1.83 +end;
    1.84 +
    1.85 +
    1.86 +local
    1.87 +
    1.88 +(* FIXME early extern (!??) *)
    1.89 +(* FIXME Syntax.free (??) *)
    1.90 +fun field_tr' (c, t) = Syntax.const @{syntax_const "_field"} $ Syntax.const c $ t;
    1.91 +
    1.92 +fun fields_tr' (t, u) = Syntax.const @{syntax_const "_fields"} $ t $ u;
    1.93 +
    1.94 +fun record_tr' ctxt t =
    1.95    let
    1.96      val thy = ProofContext.theory_of ctxt;
    1.97  
    1.98 -    fun field_lst t =
    1.99 +    fun strip_fields t =
   1.100        (case strip_comb t of
   1.101          (Const (ext, _), args as (_ :: _)) =>
   1.102 -          (case try (unsuffix extN) (Sign.intern_const thy ext) of
   1.103 +          (case try (unsuffix extN) (Sign.intern_const thy ext) of  (* FIXME authentic syntax *)
   1.104              SOME ext' =>
   1.105                (case get_extfields thy ext' of
   1.106 -                SOME flds =>
   1.107 +                SOME fields =>
   1.108                   (let
   1.109 -                    val f :: fs = but_last (map fst flds);
   1.110 -                    val flds' = Sign.extern_const thy f :: map Long_Name.base_name fs;
   1.111 +                    val f :: fs = but_last (map fst fields);
   1.112 +                    val fields' = Sign.extern_const thy f :: map Long_Name.base_name fs;
   1.113                      val (args', more) = split_last args;
   1.114 -                  in (flds' ~~ args') @ field_lst more end
   1.115 +                  in (fields' ~~ args') @ strip_fields more end
   1.116                    handle Library.UnequalLengths => [("", t)])
   1.117                | NONE => [("", t)])
   1.118            | NONE => [("", t)])
   1.119         | _ => [("", t)]);
   1.120  
   1.121 -    val (flds, (_, more)) = split_last (field_lst t);
   1.122 -    val _ = if null flds then raise Match else ();
   1.123 -    val flds' = map (fn (n, t) => Syntax.const mark $ Syntax.const n $ t) flds;
   1.124 -    val flds'' = foldr1 (fn (x, y) => Syntax.const sep $ x $ y) flds';
   1.125 +    val (fields, (_, more)) = split_last (strip_fields t);
   1.126 +    val _ = null fields andalso raise Match;
   1.127 +    val u = foldr1 fields_tr' (map field_tr' fields);
   1.128    in
   1.129 -    if unit more
   1.130 -    then Syntax.const record $ flds''
   1.131 -    else Syntax.const record_scheme $ flds'' $ more
   1.132 +    case more of
   1.133 +      Const (@{const_syntax Unity}, _) => Syntax.const @{syntax_const "_record"} $ u
   1.134 +    | _ => Syntax.const @{syntax_const "_record_scheme"} $ u $ more
   1.135    end;
   1.136  
   1.137 -fun gen_record_tr' name =
   1.138 +in
   1.139 +
   1.140 +fun record_ext_tr' name =
   1.141 +  let
   1.142 +    val ext_name = suffix extN name;
   1.143 +    fun tr' ctxt ts = record_tr' ctxt (list_comb (Syntax.const ext_name, ts));
   1.144 +  in (ext_name, tr') end;
   1.145 +
   1.146 +end;
   1.147 +
   1.148 +
   1.149 +local
   1.150 +
   1.151 +(* FIXME early extern (!??) *)
   1.152 +(* FIXME Syntax.free (??) *)
   1.153 +fun field_type_tr' (c, t) = Syntax.const @{syntax_const "_field_type"} $ Syntax.const c $ t;
   1.154 +
   1.155 +fun field_types_tr' (t, u) = Syntax.const @{syntax_const "_field_types"} $ t $ u;
   1.156 +
   1.157 +fun record_type_tr' ctxt t =
   1.158    let
   1.159 -    val name_sfx = suffix extN name;
   1.160 -    val unit = fn Const (@{const_syntax Product_Type.Unity}, _) => true | _ => false;
   1.161 -    fun tr' ctxt ts =
   1.162 -      record_tr'
   1.163 -        @{syntax_const "_fields"}
   1.164 -        @{syntax_const "_field"}
   1.165 -        @{syntax_const "_record"}
   1.166 -        @{syntax_const "_record_scheme"}
   1.167 -        unit ctxt (list_comb (Syntax.const name_sfx, ts));
   1.168 -  in (name_sfx, tr') end;
   1.169 -
   1.170 -fun print_translation names =
   1.171 -  map (gen_field_tr' updateN record_update_tr') names;
   1.172 -
   1.173 -
   1.174 -(* record_type_abbr_tr' *)
   1.175 +    val thy = ProofContext.theory_of ctxt;
   1.176 +
   1.177 +    val T = decode_type thy t;
   1.178 +    val varifyT = varifyT (Term.maxidx_of_typ T);
   1.179 +
   1.180 +    val term_of_type = Syntax.term_of_typ (! Syntax.show_sorts) o Sign.extern_typ thy;
   1.181 +
   1.182 +    fun strip_fields T =
   1.183 +      (case T of
   1.184 +        Type (ext, args) =>
   1.185 +          (case try (unsuffix ext_typeN) ext of
   1.186 +            SOME ext' =>
   1.187 +              (case get_extfields thy ext' of
   1.188 +                SOME fields =>
   1.189 +                  (case get_fieldext thy (fst (hd fields)) of
   1.190 +                    SOME (_, alphas) =>
   1.191 +                     (let
   1.192 +                        val f :: fs = but_last fields;
   1.193 +                        val fields' =
   1.194 +                          apfst (Sign.extern_const thy) f :: map (apfst Long_Name.base_name) fs;
   1.195 +                        val (args', more) = split_last args;
   1.196 +                        val alphavars = map varifyT (but_last alphas);
   1.197 +                        val subst = fold (Sign.typ_match thy) (alphavars ~~ args') Vartab.empty;
   1.198 +                        val fields'' = (map o apsnd) (Envir.norm_type subst o varifyT) fields';
   1.199 +                      in fields'' @ strip_fields more end
   1.200 +                      handle Type.TYPE_MATCH => [("", T)]
   1.201 +                        | Library.UnequalLengths => [("", T)])
   1.202 +                  | NONE => [("", T)])
   1.203 +              | NONE => [("", T)])
   1.204 +          | NONE => [("", T)])
   1.205 +      | _ => [("", T)]);
   1.206 +
   1.207 +    val (fields, (_, moreT)) = split_last (strip_fields T);
   1.208 +    val _ = null fields andalso raise Match;
   1.209 +    val u = foldr1 field_types_tr' (map (field_type_tr' o apsnd term_of_type) fields);
   1.210 +  in
   1.211 +    if not (! print_record_type_as_fields) orelse null fields then raise Match
   1.212 +    else if moreT = HOLogic.unitT then Syntax.const @{syntax_const "_record_type"} $ u
   1.213 +    else Syntax.const @{syntax_const "_record_type_scheme"} $ u $ term_of_type moreT
   1.214 +  end;
   1.215  
   1.216  (*try to reconstruct the record name type abbreviation from
   1.217    the (nested) extension types*)
   1.218 -fun record_type_abbr_tr' default_tr' abbr alphas zeta last_ext schemeT ctxt tm =
   1.219 +fun record_type_abbr_tr' abbr alphas zeta last_ext schemeT ctxt tm =
   1.220    let
   1.221      val thy = ProofContext.theory_of ctxt;
   1.222  
   1.223 @@ -966,88 +1029,34 @@
   1.224        (case last_extT T of
   1.225          SOME (name, _) =>
   1.226            if name = last_ext then
   1.227 -           (let val subst = match schemeT T in
   1.228 +            let val subst = match schemeT T in
   1.229                if HOLogic.is_unitT (Envir.norm_type subst (varifyT (TFree (zeta, Sign.defaultS thy))))
   1.230                then mk_type_abbr subst abbr alphas
   1.231                else mk_type_abbr subst (suffix schemeN abbr) (alphas @ [zeta])
   1.232 -            end handle Type.TYPE_MATCH => default_tr' ctxt tm)
   1.233 +            end handle Type.TYPE_MATCH => record_type_tr' ctxt tm
   1.234            else raise Match (*give print translation of specialised record a chance*)
   1.235        | _ => raise Match)
   1.236 -    else default_tr' ctxt tm
   1.237 +    else record_type_tr' ctxt tm
   1.238    end;
   1.239  
   1.240 -fun record_type_tr' sep mark record record_scheme ctxt t =
   1.241 +in
   1.242 +
   1.243 +fun record_ext_type_tr' name =
   1.244    let
   1.245 -    val thy = ProofContext.theory_of ctxt;
   1.246 -
   1.247 -    val T = decode_type thy t;
   1.248 -    val varifyT = varifyT (Term.maxidx_of_typ T);
   1.249 -
   1.250 -    fun term_of_type T = Syntax.term_of_typ (! Syntax.show_sorts) (Sign.extern_typ thy T);
   1.251 -
   1.252 -    fun field_lst T =
   1.253 -      (case T of
   1.254 -        Type (ext, args) =>
   1.255 -          (case try (unsuffix ext_typeN) ext of
   1.256 -            SOME ext' =>
   1.257 -              (case get_extfields thy ext' of
   1.258 -                SOME flds =>
   1.259 -                  (case get_fieldext thy (fst (hd flds)) of
   1.260 -                    SOME (_, alphas) =>
   1.261 -                     (let
   1.262 -                        val f :: fs = but_last flds;
   1.263 -                        val flds' = apfst (Sign.extern_const thy) f ::
   1.264 -                          map (apfst Long_Name.base_name) fs;
   1.265 -                        val (args', more) = split_last args;
   1.266 -                        val alphavars = map varifyT (but_last alphas);
   1.267 -                        val subst = fold2 (curry (Sign.typ_match thy)) alphavars args' Vartab.empty;
   1.268 -                        val flds'' = (map o apsnd) (Envir.norm_type subst o varifyT) flds';
   1.269 -                      in flds'' @ field_lst more end
   1.270 -                      handle Type.TYPE_MATCH => [("", T)]
   1.271 -                        | Library.UnequalLengths => [("", T)])
   1.272 -                  | NONE => [("", T)])
   1.273 -              | NONE => [("", T)])
   1.274 -          | NONE => [("", T)])
   1.275 -      | _ => [("", T)]);
   1.276 -
   1.277 -    val (flds, (_, moreT)) = split_last (field_lst T);
   1.278 -    val flds' = map (fn (n, T) => Syntax.const mark $ Syntax.const n $ term_of_type T) flds;
   1.279 -    val flds'' =
   1.280 -      foldr1 (fn (x, y) => Syntax.const sep $ x $ y) flds'
   1.281 -        handle Empty => raise Match;
   1.282 -  in
   1.283 -    if not (! print_record_type_as_fields) orelse null flds then raise Match
   1.284 -    else if moreT = HOLogic.unitT then Syntax.const record $ flds''
   1.285 -    else Syntax.const record_scheme $ flds'' $ term_of_type moreT
   1.286 -  end;
   1.287 -
   1.288 -
   1.289 -fun gen_record_type_tr' name =
   1.290 +    val ext_type_name = suffix ext_typeN name;
   1.291 +    fun tr' ctxt ts =
   1.292 +      record_type_tr' ctxt (list_comb (Syntax.const ext_type_name, ts));
   1.293 +  in (ext_type_name, tr') end;
   1.294 +
   1.295 +fun record_ext_type_abbr_tr' abbr alphas zeta last_ext schemeT name =
   1.296    let
   1.297 -    val name_sfx = suffix ext_typeN name;
   1.298 +    val ext_type_name = suffix ext_typeN name;
   1.299      fun tr' ctxt ts =
   1.300 -      record_type_tr'
   1.301 -        @{syntax_const "_field_types"}
   1.302 -        @{syntax_const "_field_type"}
   1.303 -        @{syntax_const "_record_type"}
   1.304 -        @{syntax_const "_record_type_scheme"}
   1.305 -        ctxt (list_comb (Syntax.const name_sfx, ts));
   1.306 -  in (name_sfx, tr') end;
   1.307 -
   1.308 -
   1.309 -fun gen_record_type_abbr_tr' abbr alphas zeta last_ext schemeT name =
   1.310 -  let
   1.311 -    val name_sfx = suffix ext_typeN name;
   1.312 -    val default_tr' =
   1.313 -      record_type_tr'
   1.314 -        @{syntax_const "_field_types"}
   1.315 -        @{syntax_const "_field_type"}
   1.316 -        @{syntax_const "_record_type"}
   1.317 -        @{syntax_const "_record_type_scheme"};
   1.318 -    fun tr' ctxt ts =
   1.319 -      record_type_abbr_tr' default_tr' abbr alphas zeta last_ext schemeT ctxt
   1.320 -        (list_comb (Syntax.const name_sfx, ts));
   1.321 -  in (name_sfx, tr') end;
   1.322 +      record_type_abbr_tr' abbr alphas zeta last_ext schemeT ctxt
   1.323 +        (list_comb (Syntax.const ext_type_name, ts));
   1.324 +  in (ext_type_name, tr') end;
   1.325 +
   1.326 +end;
   1.327  
   1.328  
   1.329  
   1.330 @@ -1970,25 +1979,24 @@
   1.331  
   1.332  
   1.333      (* prepare print translation functions *)
   1.334 -
   1.335 -    val field_tr's =
   1.336 -      print_translation (distinct (op =) (maps external_names (full_moreN :: names)));
   1.337 -
   1.338 -    val adv_ext_tr's =
   1.339 -      let val trnames = external_names extN
   1.340 -      in map (gen_record_tr') trnames end;
   1.341 -
   1.342 -    val adv_record_type_abbr_tr's =
   1.343 +    (* FIXME authentic syntax *)
   1.344 +
   1.345 +    val field_update_tr's =
   1.346 +      map field_update_tr' (distinct (op =) (maps external_names (full_moreN :: names)));
   1.347 +
   1.348 +    val record_ext_tr's = map record_ext_tr' (external_names extN);
   1.349 +
   1.350 +    val record_ext_type_abbr_tr's =
   1.351        let
   1.352          val trnames = external_names (hd extension_names);
   1.353          val last_ext = unsuffix ext_typeN (fst extension);
   1.354 -      in map (gen_record_type_abbr_tr' name alphas zeta last_ext rec_schemeT0) trnames end;
   1.355 -
   1.356 -    val adv_record_type_tr's =
   1.357 +      in map (record_ext_type_abbr_tr' name alphas zeta last_ext rec_schemeT0) trnames end;
   1.358 +
   1.359 +    val record_ext_type_tr's =
   1.360        let
   1.361 +        (*avoid conflict with record_type_abbr_tr's*)
   1.362          val trnames = if parent_len > 0 then external_names extN else [];
   1.363 -        (*avoid conflict with adv_record_type_abbr_tr's*)
   1.364 -      in map (gen_record_type_tr') trnames end;
   1.365 +      in map record_ext_type_tr' trnames end;
   1.366  
   1.367  
   1.368      (* prepare declarations *)
   1.369 @@ -2005,8 +2013,8 @@
   1.370  
   1.371      (*record (scheme) type abbreviation*)
   1.372      val recordT_specs =
   1.373 -      [(Binding.suffix_name schemeN b, alphas @ [zeta], rec_schemeT0, Syntax.NoSyn),
   1.374 -        (b, alphas, recT0, Syntax.NoSyn)];
   1.375 +      [(Binding.suffix_name schemeN b, alphas @ [zeta], rec_schemeT0, NoSyn),
   1.376 +        (b, alphas, recT0, NoSyn)];
   1.377  
   1.378      val ext_defs = ext_def :: map #ext_def parents;
   1.379  
   1.380 @@ -2089,16 +2097,15 @@
   1.381  
   1.382      fun mk_defs () =
   1.383        extension_thy
   1.384 -      |> Sign.add_trfuns ([], [], field_tr's, [])
   1.385 +      |> Sign.add_trfuns ([], [], field_update_tr's, [])
   1.386        |> Sign.add_advanced_trfuns
   1.387 -          ([], [], adv_ext_tr's @ adv_record_type_tr's @ adv_record_type_abbr_tr's, [])
   1.388 +        ([], [], record_ext_tr's @ record_ext_type_tr's @ record_ext_type_abbr_tr's, [])
   1.389        |> Sign.parent_path
   1.390        |> Sign.add_tyabbrs_i recordT_specs
   1.391        |> Sign.add_path base_name
   1.392        |> Sign.add_consts_i
   1.393 -          (map2 (fn (x, T) => fn mx => (Binding.name x, T, mx))
   1.394 -            sel_decls (field_syntax @ [Syntax.NoSyn]))
   1.395 -      |> (Sign.add_consts_i o map (fn (x, T) => (Binding.name x, T, Syntax.NoSyn)))
   1.396 +          (map2 (fn (x, T) => fn mx => (Binding.name x, T, mx)) sel_decls (field_syntax @ [NoSyn]))
   1.397 +      |> (Sign.add_consts_i o map (fn (x, T) => (Binding.name x, T, NoSyn)))
   1.398            (upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
   1.399        |> (PureThy.add_defs false o map (Thm.no_attributes o apfst (Binding.conceal o Binding.name)))
   1.400          sel_specs