src/HOL/Library/datatype_records.ML
author Manuel Eberl <eberlm@in.tum.de>
Mon Mar 26 16:14:16 2018 +0200 (18 months ago)
changeset 67951 655aa11359dc
parent 67611 7929240e44d4
child 68686 7f8db1c4ebec
permissions -rw-r--r--
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
     1 signature DATATYPE_RECORDS = sig
     2   type ctr_options = string -> bool
     3   type ctr_options_cmd = Proof.context -> string -> bool
     4 
     5   val default_ctr_options: ctr_options
     6   val default_ctr_options_cmd: ctr_options_cmd
     7 
     8   val mk_update_defs: string -> local_theory -> local_theory
     9 
    10   val bnf_record: binding -> ctr_options -> (binding option * (typ * sort)) list ->
    11     (binding * typ) list -> local_theory -> local_theory
    12 
    13   val bnf_record_cmd: binding -> ctr_options_cmd ->
    14     (binding option * (string * string option)) list -> (binding * string) list -> local_theory ->
    15     local_theory
    16 
    17   val setup: theory -> theory
    18 end
    19 
    20 structure Datatype_Records : DATATYPE_RECORDS = struct
    21 
    22 type ctr_options = string -> bool
    23 type ctr_options_cmd = Proof.context -> string -> bool
    24 
    25 val default_ctr_options = Plugin_Name.default_filter
    26 val default_ctr_options_cmd = K Plugin_Name.default_filter
    27 
    28 type data = string Symtab.table
    29 
    30 structure Data = Theory_Data
    31 (
    32   type T = data
    33   val empty = Symtab.empty
    34   val merge = Symtab.merge op =
    35   val extend = I
    36 )
    37 
    38 fun mk_update_defs typ_name lthy =
    39   let
    40     val short_name = Long_Name.base_name typ_name
    41 
    42     val {ctrs, casex, selss, ...} = the (Ctr_Sugar.ctr_sugar_of lthy typ_name)
    43     val ctr = case ctrs of [ctr] => ctr | _ => error "BNF_Record.mk_update_defs: expected only single constructor"
    44     val sels = case selss of [sels] => sels | _ => error "BNF_Record.mk_update_defs: expected selectors"
    45     val ctr_dummy = Const (fst (dest_Const ctr), dummyT)
    46     val casex_dummy = Const (fst (dest_Const casex), dummyT)
    47 
    48     val len = length sels
    49 
    50     fun mk_name sel =
    51       Binding.name ("update_" ^ Long_Name.base_name (fst (dest_Const sel)))
    52 
    53     fun mk_t idx =
    54       let
    55         val body =
    56           fold_rev (fn pos => fn t => t $ (if len - pos = idx + 1 then Bound len $ Bound pos else Bound pos)) (0 upto len - 1) ctr_dummy
    57           |> fold_rev (fn idx => fn t => Abs ("x" ^ Value.print_int idx, dummyT, t)) (1 upto len)
    58       in
    59         Abs ("f", dummyT, casex_dummy $ body)
    60       end
    61 
    62     fun define name t =
    63       Local_Theory.define ((name, NoSyn), ((Binding.empty, @{attributes [datatype_record_update, code]}), t)) #> snd
    64 
    65     val lthy' =
    66       Local_Theory.map_background_naming (Name_Space.qualified_path false (Binding.name short_name)) lthy
    67 
    68     fun insert sel =
    69       Symtab.insert op = (fst (dest_Const sel), Local_Theory.full_name lthy' (mk_name sel))
    70   in
    71     lthy'
    72     |> @{fold 2} define (map mk_name sels) (Syntax.check_terms lthy (map mk_t (0 upto len - 1)))
    73     |> Local_Theory.background_theory (Data.map (fold insert sels))
    74     |> Local_Theory.restore_background_naming lthy
    75   end
    76 
    77 fun bnf_record binding opts tyargs args lthy =
    78   let
    79     val constructor =
    80       (((Binding.empty, Binding.map_name (fn c => "make_" ^ c) binding), args), NoSyn)
    81 
    82     val datatyp =
    83       ((tyargs, binding), NoSyn)
    84 
    85     val dtspec =
    86       ((opts, false),
    87        [(((datatyp, [constructor]), (Binding.empty, Binding.empty, Binding.empty)), [])])
    88 
    89     val lthy' =
    90       BNF_FP_Def_Sugar.co_datatypes BNF_Util.Least_FP BNF_LFP.construct_lfp dtspec lthy
    91       |> mk_update_defs (Local_Theory.full_name lthy binding)
    92   in
    93     lthy'
    94   end
    95 
    96 fun bnf_record_cmd binding opts tyargs args lthy =
    97   bnf_record binding (opts lthy)
    98     (map (apsnd (apfst (Syntax.parse_typ lthy) o apsnd (Typedecl.read_constraint lthy))) tyargs)
    99     (map (apsnd (Syntax.parse_typ lthy)) args) lthy
   100 
   101 (* syntax *)
   102 (* copied and adapted from record.ML *)
   103 
   104 val read_const =
   105   dest_Const oo Proof_Context.read_const {proper = true, strict = true}
   106 
   107 fun field_tr ((Const (\<^syntax_const>\<open>_datatype_field\<close>, _) $ Const (name, _) $ arg)) = (name, arg)
   108   | field_tr t = raise TERM ("field_tr", [t]);
   109 
   110 fun fields_tr (Const (\<^syntax_const>\<open>_datatype_fields\<close>, _) $ t $ u) = field_tr t :: fields_tr u
   111   | fields_tr t = [field_tr t];
   112 
   113 fun record_fields_tr ctxt t =
   114   let
   115     val assns = map (apfst (read_const ctxt)) (fields_tr t)
   116 
   117     val typ_name =
   118       snd (fst (hd assns))
   119       |> domain_type
   120       |> dest_Type
   121       |> fst
   122 
   123     val assns' = map (apfst fst) assns
   124 
   125     val {ctrs, selss, ...} = the (Ctr_Sugar.ctr_sugar_of ctxt typ_name)
   126     val ctr = case ctrs of [ctr] => ctr | _ => error "BNF_Record.record_fields_tr: expected only single constructor"
   127     val sels = case selss of [sels] => sels | _ => error "BNF_Record.record_fields_tr: expected selectors"
   128     val ctr_dummy = Const (fst (dest_Const ctr), dummyT)
   129 
   130     fun mk_arg name =
   131       case AList.lookup op = assns' name of
   132         NONE => error ("BNF_Record.record_fields_tr: missing field " ^ name)
   133       | SOME t => t
   134   in
   135     if length assns = length sels then
   136       list_comb (ctr_dummy, map (mk_arg o fst o dest_Const) sels)
   137     else
   138       error ("BNF_Record.record_fields_tr: expected " ^ Value.print_int (length sels) ^ " field(s)")
   139   end
   140 
   141 fun field_update_tr ctxt (Const (\<^syntax_const>\<open>_datatype_field_update\<close>, _) $ Const (name, _) $ arg) =
   142       let
   143         val thy = Proof_Context.theory_of ctxt
   144         val (name, _) = read_const ctxt name
   145       in
   146         case Symtab.lookup (Data.get thy) name of
   147           NONE => raise Fail ("not a valid record field: " ^ name)
   148         | SOME s => Const (s, dummyT) $ Abs (Name.uu_, dummyT, arg)
   149       end
   150   | field_update_tr _ t = raise TERM ("field_update_tr", [@{print} t]);
   151 
   152 fun field_updates_tr ctxt (Const (\<^syntax_const>\<open>_datatype_field_updates\<close>, _) $ t $ u) =
   153       field_update_tr ctxt t :: field_updates_tr ctxt u
   154   | field_updates_tr ctxt t = [field_update_tr ctxt t];
   155 
   156 fun record_tr ctxt [t] = record_fields_tr ctxt t
   157   | record_tr _ ts = raise TERM ("record_tr", ts);
   158 
   159 fun record_update_tr ctxt [t, u] = fold (curry op $) (field_updates_tr ctxt u) t
   160   | record_update_tr _ ts = raise TERM ("record_update_tr", ts);
   161 
   162 val parse_ctr_options =
   163   Scan.optional (@{keyword "("} |-- Parse.list1 (Plugin_Name.parse_filter >> K) --| @{keyword ")"} >>
   164     (fn fs => fold I fs default_ctr_options_cmd)) default_ctr_options_cmd
   165 
   166 val parser =
   167   (parse_ctr_options -- BNF_Util.parse_type_args_named_constrained -- Parse.binding) --
   168     (\<^keyword>\<open>=\<close> |-- Scan.repeat1 (Parse.binding -- (Parse.$$$ "::" |-- Parse.!!! Parse.typ)))
   169 
   170 val _ =
   171   Outer_Syntax.local_theory
   172     @{command_keyword datatype_record}
   173     "Defines a record based on the BNF/datatype machinery"
   174     (parser >> (fn (((ctr_options, tyargs), binding), args) =>
   175       bnf_record_cmd binding ctr_options tyargs args))
   176 
   177 val setup =
   178    (Sign.parse_translation
   179      [(\<^syntax_const>\<open>_datatype_record_update\<close>, record_update_tr),
   180       (\<^syntax_const>\<open>_datatype_record\<close>, record_tr)]);
   181 
   182 end