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