1.1 --- a/src/HOL/Tools/record.ML Mon Feb 15 20:32:21 2010 +0100
1.2 +++ b/src/HOL/Tools/record.ML Mon Feb 15 22:24:19 2010 +0100
1.3 @@ -42,10 +42,10 @@
1.4 val print_records: theory -> unit
1.5 val read_typ: Proof.context -> string -> (string * sort) list -> typ * (string * sort) list
1.6 val cert_typ: Proof.context -> typ -> (string * sort) list -> typ * (string * sort) list
1.7 - val add_record: bool -> string list * string -> string option -> (string * string * mixfix) list
1.8 - -> theory -> theory
1.9 - val add_record_i: bool -> string list * string -> (typ list * string) option
1.10 - -> (string * typ * mixfix) list -> theory -> theory
1.11 + val add_record: bool -> string list * binding -> (typ list * string) option ->
1.12 + (binding * typ * mixfix) list -> theory -> theory
1.13 + val add_record_cmd: bool -> string list * binding -> string option ->
1.14 + (binding * string * mixfix) list -> theory -> theory
1.15 val setup: theory -> theory
1.16 end;
1.17
1.18 @@ -189,7 +189,7 @@
1.19 val meta_allE = @{thm Pure.meta_allE};
1.20 val prop_subst = @{thm prop_subst};
1.21 val K_record_comp = @{thm K_record_comp};
1.22 -val K_comp_convs = [@{thm o_apply}, K_record_comp]
1.23 +val K_comp_convs = [@{thm o_apply}, K_record_comp];
1.24 val o_assoc = @{thm o_assoc};
1.25 val id_apply = @{thm id_apply};
1.26 val id_o_apps = [@{thm id_apply}, @{thm id_o}, @{thm o_id}];
1.27 @@ -830,7 +830,8 @@
1.28 in
1.29 (case try (unsuffix sfx) name_field of
1.30 SOME name =>
1.31 - apfst (cons (Syntax.const mark $ Syntax.free name $ t)) (gen_field_upds_tr' mark sfx u)
1.32 + apfst (cons (Syntax.const mark $ Syntax.free name $ t))
1.33 + (gen_field_upds_tr' mark sfx u)
1.34 | NONE => ([], tm))
1.35 end
1.36 | gen_field_upds_tr' _ _ tm = ([], tm);
1.37 @@ -883,9 +884,12 @@
1.38 val name_sfx = suffix extN name;
1.39 val unit = fn Const (@{const_syntax Product_Type.Unity}, _) => true | _ => false;
1.40 fun tr' ctxt ts =
1.41 - record_tr' @{syntax_const "_fields"} @{syntax_const "_field"}
1.42 - @{syntax_const "_record"} @{syntax_const "_record_scheme"} unit ctxt
1.43 - (list_comb (Syntax.const name_sfx, ts));
1.44 + record_tr'
1.45 + @{syntax_const "_fields"}
1.46 + @{syntax_const "_field"}
1.47 + @{syntax_const "_record"}
1.48 + @{syntax_const "_record_scheme"}
1.49 + unit ctxt (list_comb (Syntax.const name_sfx, ts));
1.50 in (name_sfx, tr') end;
1.51
1.52 fun print_translation names =
1.53 @@ -993,8 +997,11 @@
1.54 let
1.55 val name_sfx = suffix ext_typeN name;
1.56 fun tr' ctxt ts =
1.57 - record_type_tr' @{syntax_const "_field_types"} @{syntax_const "_field_type"}
1.58 - @{syntax_const "_record_type"} @{syntax_const "_record_type_scheme"}
1.59 + record_type_tr'
1.60 + @{syntax_const "_field_types"}
1.61 + @{syntax_const "_field_type"}
1.62 + @{syntax_const "_record_type"}
1.63 + @{syntax_const "_record_type_scheme"}
1.64 ctxt (list_comb (Syntax.const name_sfx, ts));
1.65 in (name_sfx, tr') end;
1.66
1.67 @@ -1003,8 +1010,11 @@
1.68 let
1.69 val name_sfx = suffix ext_typeN name;
1.70 val default_tr' =
1.71 - record_type_tr' @{syntax_const "_field_types"} @{syntax_const "_field_type"}
1.72 - @{syntax_const "_record_type"} @{syntax_const "_record_type_scheme"};
1.73 + record_type_tr'
1.74 + @{syntax_const "_field_types"}
1.75 + @{syntax_const "_field_type"}
1.76 + @{syntax_const "_record_type"}
1.77 + @{syntax_const "_record_type_scheme"};
1.78 fun tr' ctxt ts =
1.79 record_type_abbr_tr' default_tr' abbr alphas zeta lastExt schemeT ctxt
1.80 (list_comb (Syntax.const name_sfx, ts));
1.81 @@ -1828,17 +1838,19 @@
1.82
1.83 (* record_definition *)
1.84
1.85 -fun record_definition (args, bname) parent (parents: parent_info list) raw_fields thy =
1.86 +fun record_definition (args, b) parent (parents: parent_info list) raw_fields thy =
1.87 let
1.88 val external_names = Name_Space.external_names (Sign.naming_of thy);
1.89
1.90 val alphas = map fst args;
1.91 - val name = Sign.full_bname thy bname;
1.92 - val full = Sign.full_bname_path thy bname;
1.93 +
1.94 + val base_name = Binding.name_of b; (* FIXME include qualifier etc. (!?) *)
1.95 + val name = Sign.full_name thy b;
1.96 + val full = Sign.full_name_path thy base_name;
1.97 val base = Long_Name.base_name;
1.98
1.99 - val (bfields, field_syntax) =
1.100 - split_list (map (fn (x, T, mx) => ((x, T), mx)) raw_fields);
1.101 + val bfields = map (fn (x, T, _) => (x, T)) raw_fields;
1.102 + val field_syntax = map #3 raw_fields;
1.103
1.104 val parent_fields = maps #fields parents;
1.105 val parent_chunks = map (length o #fields) parents;
1.106 @@ -1851,14 +1863,14 @@
1.107
1.108 val fields = map (apfst full) bfields;
1.109 val names = map fst fields;
1.110 - val extN = full bname;
1.111 + val extN = full b;
1.112 val types = map snd fields;
1.113 val alphas_fields = fold Term.add_tfree_namesT types [];
1.114 val alphas_ext = inter (op =) alphas_fields alphas;
1.115 val len = length fields;
1.116 val variants =
1.117 Name.variant_list (moreN :: rN :: (rN ^ "'") :: wN :: parent_variants)
1.118 - (map fst bfields);
1.119 + (map (Binding.name_of o fst) bfields);
1.120 val vars = ListPair.map Free (variants, types);
1.121 val named_vars = names ~~ vars;
1.122 val idxms = 0 upto len;
1.123 @@ -1873,8 +1885,8 @@
1.124 val zeta = Name.variant alphas "'z";
1.125 val moreT = TFree (zeta, HOLogic.typeS);
1.126 val more = Free (moreN, moreT);
1.127 - val full_moreN = full moreN;
1.128 - val bfields_more = bfields @ [(moreN, moreT)];
1.129 + val full_moreN = full (Binding.name moreN);
1.130 + val bfields_more = bfields @ [(Binding.name moreN, moreT)];
1.131 val fields_more = fields @ [(full_moreN, moreT)];
1.132 val named_vars_more = named_vars @ [(full_moreN, more)];
1.133 val all_vars_more = all_vars @ [more];
1.134 @@ -1885,7 +1897,7 @@
1.135
1.136 val (extension_thy, extT, ext_induct, ext_inject, ext_split, ext_def) =
1.137 thy
1.138 - |> Sign.add_path bname
1.139 + |> Sign.add_path base_name
1.140 |> extension_definition extN fields alphas_ext zeta moreT more vars;
1.141
1.142 val _ = timing_msg "record preparing definitions";
1.143 @@ -1952,8 +1964,8 @@
1.144
1.145 (* prepare declarations *)
1.146
1.147 - val sel_decls = map (mk_selC rec_schemeT0) bfields_more;
1.148 - val upd_decls = map (mk_updC updateN rec_schemeT0) bfields_more;
1.149 + val sel_decls = map (mk_selC rec_schemeT0 o apfst Binding.name_of) bfields_more;
1.150 + val upd_decls = map (mk_updC updateN rec_schemeT0 o apfst Binding.name_of) bfields_more;
1.151 val make_decl = (makeN, all_types ---> recT0);
1.152 val fields_decl = (fields_selN, types ---> Type extension);
1.153 val extend_decl = (extendN, recT0 --> moreT --> rec_schemeT0);
1.154 @@ -1964,8 +1976,8 @@
1.155
1.156 (*record (scheme) type abbreviation*)
1.157 val recordT_specs =
1.158 - [(Binding.name (suffix schemeN bname), alphas @ [zeta], rec_schemeT0, Syntax.NoSyn),
1.159 - (Binding.name bname, alphas, recT0, Syntax.NoSyn)];
1.160 + [(Binding.suffix_name schemeN b, alphas @ [zeta], rec_schemeT0, Syntax.NoSyn),
1.161 + (b, alphas, recT0, Syntax.NoSyn)];
1.162
1.163 val ext_defs = ext_def :: map #extdef parents;
1.164
1.165 @@ -2030,14 +2042,14 @@
1.166 val upd_specs = map mk_upd_spec (fields_more ~~ lastN updator_thms);
1.167
1.168 (*derived operations*)
1.169 - val make_spec = Const (full makeN, all_types ---> recT0) $$ all_vars :==
1.170 + val make_spec = Const (full (Binding.name makeN), all_types ---> recT0) $$ all_vars :==
1.171 mk_rec (all_vars @ [HOLogic.unit]) 0;
1.172 - val fields_spec = Const (full fields_selN, types ---> Type extension) $$ vars :==
1.173 + val fields_spec = Const (full (Binding.name fields_selN), types ---> Type extension) $$ vars :==
1.174 mk_rec (all_vars @ [HOLogic.unit]) parent_len;
1.175 val extend_spec =
1.176 - Const (full extendN, recT0-->moreT-->rec_schemeT0) $ r_unit0 $ more :==
1.177 + Const (full (Binding.name extendN), recT0 --> moreT --> rec_schemeT0) $ r_unit0 $ more :==
1.178 mk_rec ((map (mk_sel r_unit0) all_fields) @ [more]) 0;
1.179 - val truncate_spec = Const (full truncateN, rec_schemeT0 --> recT0) $ r0 :==
1.180 + val truncate_spec = Const (full (Binding.name truncateN), rec_schemeT0 --> recT0) $ r0 :==
1.181 mk_rec ((map (mk_sel r0) all_fields) @ [HOLogic.unit]) 0;
1.182
1.183
1.184 @@ -2050,7 +2062,7 @@
1.185 ([], [], adv_ext_tr's @ adv_record_type_tr's @ adv_record_type_abbr_tr's, [])
1.186 |> Sign.parent_path
1.187 |> Sign.add_tyabbrs_i recordT_specs
1.188 - |> Sign.add_path bname
1.189 + |> Sign.add_path base_name
1.190 |> Sign.add_consts_i
1.191 (map2 (fn (x, T) => fn mx => (Binding.name x, T, mx))
1.192 sel_decls (field_syntax @ [Syntax.NoSyn]))
1.193 @@ -2347,10 +2359,13 @@
1.194
1.195 (*We do all preparations and error checks here, deferring the real
1.196 work to record_definition.*)
1.197 -fun gen_add_record prep_typ prep_raw_parent quiet_mode (params, bname) raw_parent raw_fields thy =
1.198 +fun gen_add_record prep_typ prep_raw_parent quiet_mode
1.199 + (params, b) raw_parent raw_fields thy =
1.200 let
1.201 val _ = Theory.requires thy "Record" "record definitions";
1.202 - val _ = if quiet_mode then () else writeln ("Defining record " ^ quote bname ^ " ...");
1.203 + val _ =
1.204 + if quiet_mode then ()
1.205 + else writeln ("Defining record " ^ quote (Binding.name_of b) ^ " ...");
1.206
1.207 val ctxt = ProofContext.init thy;
1.208
1.209 @@ -2371,10 +2386,12 @@
1.210
1.211 (* fields *)
1.212
1.213 - fun prep_field (c, raw_T, mx) env =
1.214 - let val (T, env') = prep_typ ctxt raw_T env handle ERROR msg =>
1.215 - cat_error msg ("The error(s) above occured in record field " ^ quote c)
1.216 - in ((c, T, mx), env') end;
1.217 + fun prep_field (x, raw_T, mx) env =
1.218 + let
1.219 + val (T, env') =
1.220 + prep_typ ctxt raw_T env handle ERROR msg =>
1.221 + cat_error msg ("The error(s) above occured in record field " ^ quote (Binding.str_of x));
1.222 + in ((x, T, mx), env') end;
1.223
1.224 val (bfields, envir) = fold_map prep_field raw_fields init_env;
1.225 val envir_names = map fst envir;
1.226 @@ -2388,7 +2405,7 @@
1.227
1.228 (* errors *)
1.229
1.230 - val name = Sign.full_bname thy bname;
1.231 + val name = Sign.full_name thy b;
1.232 val err_dup_record =
1.233 if is_none (get_record thy name) then []
1.234 else ["Duplicate definition of record " ^ quote name];
1.235 @@ -2406,12 +2423,12 @@
1.236 val err_no_fields = if null bfields then ["No fields present"] else [];
1.237
1.238 val err_dup_fields =
1.239 - (case duplicates (op =) (map #1 bfields) of
1.240 + (case duplicates Binding.eq_name (map #1 bfields) of
1.241 [] => []
1.242 - | dups => ["Duplicate field(s) " ^ commas_quote dups]);
1.243 + | dups => ["Duplicate field(s) " ^ commas_quote (map Binding.str_of dups)]);
1.244
1.245 val err_bad_fields =
1.246 - if forall (not_equal moreN o #1) bfields then []
1.247 + if forall (not_equal moreN o Binding.name_of o #1) bfields then []
1.248 else ["Illegal field name " ^ quote moreN];
1.249
1.250 val err_dup_sorts =
1.251 @@ -2425,12 +2442,12 @@
1.252
1.253 val _ = if null errs then () else error (cat_lines errs);
1.254 in
1.255 - thy |> record_definition (args, bname) parent parents bfields
1.256 + thy |> record_definition (args, b) parent parents bfields
1.257 end
1.258 - handle ERROR msg => cat_error msg ("Failed to define record " ^ quote bname);
1.259 -
1.260 -val add_record = gen_add_record read_typ read_raw_parent;
1.261 -val add_record_i = gen_add_record cert_typ (K I);
1.262 + handle ERROR msg => cat_error msg ("Failed to define record " ^ quote (Binding.str_of b));
1.263 +
1.264 +val add_record = gen_add_record cert_typ (K I);
1.265 +val add_record_cmd = gen_add_record read_typ read_raw_parent;
1.266
1.267
1.268 (* setup theory *)
1.269 @@ -2446,13 +2463,11 @@
1.270
1.271 local structure P = OuterParse and K = OuterKeyword in
1.272
1.273 -val record_decl =
1.274 - P.type_args -- P.name --
1.275 - (P.$$$ "=" |-- Scan.option (P.typ --| P.$$$ "+") -- Scan.repeat1 P.const);
1.276 -
1.277 val _ =
1.278 OuterSyntax.command "record" "define extensible record" K.thy_decl
1.279 - (record_decl >> (fn (x, (y, z)) => Toplevel.theory (add_record false x y z)));
1.280 + (P.type_args -- P.binding --
1.281 + (P.$$$ "=" |-- Scan.option (P.typ --| P.$$$ "+") -- Scan.repeat1 P.const_binding)
1.282 + >> (fn (x, (y, z)) => Toplevel.theory (add_record_cmd false x y z)));
1.283
1.284 end;
1.285