src/HOL/Tools/record.ML
changeset 35136 34206672b168
parent 35135 1667fd3b051d
child 35137 405bb7e38057
     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