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