src/HOL/Library/Datatype_Records.thy
author haftmann
Fri Mar 22 19:18:08 2019 +0000 (3 months ago)
changeset 69946 494934c30f38
parent 69913 ca515cf61651
permissions -rw-r--r--
improved code equations taken over from AFP
lars@67618
     1
(*  Title:      HOL/Library/Datatype_Records.thy
lars@67618
     2
    Author:     Lars Hupel
lars@67618
     3
*)
lars@67618
     4
lars@67611
     5
section \<open>Records based on BNF/datatype machinery\<close>
lars@67611
     6
lars@67611
     7
theory Datatype_Records
lars@67611
     8
imports Main
wenzelm@69913
     9
keywords "datatype_record" :: thy_defn
lars@67611
    10
begin
lars@67611
    11
lars@67618
    12
text \<open>
lars@67618
    13
  This theory provides an alternative, stripped-down implementation of records based on the
lars@67618
    14
  machinery of the @{command datatype} package.
lars@67618
    15
lars@67618
    16
  It supports:
lars@67618
    17
  \<^item> similar declaration syntax as records
lars@67618
    18
  \<^item> record creation and update syntax (using \<open>\<lparr> ... \<rparr>\<close> brackets)
lars@67618
    19
  \<^item> regular datatype features (e.g. dead type variables etc.)
lars@67618
    20
  \<^item> ``after-the-fact'' registration of single-free-constructor types as records
lars@67618
    21
\<close>
lars@67618
    22
lars@67618
    23
text \<open>
lars@67618
    24
  Caveats:
lars@67618
    25
  \<^item> there is no compatibility layer; importing this theory will disrupt existing syntax
lars@67618
    26
  \<^item> extensible records are not supported
lars@67618
    27
\<close>
lars@67618
    28
lars@67611
    29
no_syntax
lars@67611
    30
  "_constify"           :: "id => ident"                        ("_")
lars@67611
    31
  "_constify"           :: "longid => ident"                    ("_")
lars@67611
    32
lars@67611
    33
  "_field_type"         :: "ident => type => field_type"        ("(2_ ::/ _)")
lars@67611
    34
  ""                    :: "field_type => field_types"          ("_")
lars@67611
    35
  "_field_types"        :: "field_type => field_types => field_types"    ("_,/ _")
lars@67611
    36
  "_record_type"        :: "field_types => type"                ("(3\<lparr>_\<rparr>)")
lars@67611
    37
  "_record_type_scheme" :: "field_types => type => type"        ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)")
lars@67611
    38
lars@67611
    39
  "_field"              :: "ident => 'a => field"               ("(2_ =/ _)")
lars@67611
    40
  ""                    :: "field => fields"                    ("_")
lars@67611
    41
  "_fields"             :: "field => fields => fields"          ("_,/ _")
lars@67611
    42
  "_record"             :: "fields => 'a"                       ("(3\<lparr>_\<rparr>)")
lars@67611
    43
  "_record_scheme"      :: "fields => 'a => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
lars@67611
    44
lars@67611
    45
  "_field_update"       :: "ident => 'a => field_update"        ("(2_ :=/ _)")
lars@67611
    46
  ""                    :: "field_update => field_updates"      ("_")
lars@67611
    47
  "_field_updates"      :: "field_update => field_updates => field_updates"  ("_,/ _")
lars@67611
    48
  "_record_update"      :: "'a => field_updates => 'b"          ("_/(3\<lparr>_\<rparr>)" [900, 0] 900)
lars@67611
    49
lars@67611
    50
no_syntax (ASCII)
lars@67611
    51
  "_record_type"        :: "field_types => type"                ("(3'(| _ |'))")
lars@67611
    52
  "_record_type_scheme" :: "field_types => type => type"        ("(3'(| _,/ (2... ::/ _) |'))")
lars@67611
    53
  "_record"             :: "fields => 'a"                       ("(3'(| _ |'))")
lars@67611
    54
  "_record_scheme"      :: "fields => 'a => 'a"                 ("(3'(| _,/ (2... =/ _) |'))")
lars@67611
    55
  "_record_update"      :: "'a => field_updates => 'b"          ("_/(3'(| _ |'))" [900, 0] 900)
lars@67611
    56
lars@67611
    57
(* copied and adapted from Record.thy *)
lars@67611
    58
lars@67611
    59
nonterminal
lars@67611
    60
  field and
lars@67611
    61
  fields and
lars@67611
    62
  field_update and
lars@67611
    63
  field_updates
lars@67611
    64
lars@67611
    65
syntax
lars@67611
    66
  "_constify"               :: "id => ident"                        ("_")
lars@67611
    67
  "_constify"               :: "longid => ident"                    ("_")
lars@67611
    68
lars@67611
    69
  "_datatype_field"         :: "ident => 'a => field"               ("(2_ =/ _)")
lars@67611
    70
  ""                        :: "field => fields"                    ("_")
lars@67611
    71
  "_datatype_fields"        :: "field => fields => fields"          ("_,/ _")
lars@67611
    72
  "_datatype_record"        :: "fields => 'a"                       ("(3\<lparr>_\<rparr>)")
lars@67611
    73
  "_datatype_field_update"  :: "ident => 'a => field_update"        ("(2_ :=/ _)")
lars@67611
    74
  ""                        :: "field_update => field_updates"      ("_")
lars@67611
    75
  "_datatype_field_updates" :: "field_update => field_updates => field_updates"  ("_,/ _")
lars@67611
    76
  "_datatype_record_update" :: "'a => field_updates => 'b"          ("_/(3\<lparr>_\<rparr>)" [900, 0] 900)
lars@67611
    77
lars@67611
    78
syntax (ASCII)
lars@67611
    79
  "_datatype_record"        :: "fields => 'a"                       ("(3'(| _ |'))")
lars@67611
    80
  "_datatype_record_scheme" :: "fields => 'a => 'a"                 ("(3'(| _,/ (2... =/ _) |'))")
lars@67611
    81
  "_datatype_record_update" :: "'a => field_updates => 'b"          ("_/(3'(| _ |'))" [900, 0] 900)
lars@67611
    82
lars@67611
    83
named_theorems datatype_record_update
lars@67611
    84
wenzelm@69605
    85
ML_file \<open>datatype_records.ML\<close>
lars@67611
    86
setup \<open>Datatype_Records.setup\<close>
lars@67611
    87
lars@67611
    88
end