Theory Datatype_Records

(*  Title:      HOL/Library/Datatype_Records.thy
    Author:     Lars Hupel
*)

section ‹Records based on BNF/datatype machinery›

theory Datatype_Records
imports Main
keywords "datatype_record" :: thy_defn
begin

text ‹
  This theory provides an alternative, stripped-down implementation of records based on the
  machinery of the @{command datatype} package.

  It supports:
   similar declaration syntax as records
   record creation and update syntax (using ⦇ ... ⦈› brackets)
   regular datatype features (e.g. dead type variables etc.)
   ``after-the-fact'' registration of single-free-constructor types as records
›

text ‹
  Caveats:
   there is no compatibility layer; importing this theory will disrupt existing syntax
   extensible records are not supported
›

nonterminal
  ident and
  field_type and
  field_types and
  field and
  fields and
  field_update and
  field_updates

open_bundle datatype_record_syntax
begin

unbundle no record_syntax

syntax
  "_constify"               :: "id => ident"                        (‹_›)
  "_constify"               :: "longid => ident"                    (‹_›)

  "_datatype_field"         :: "ident => 'a => field"               ((‹indent=2 notation=‹infix field value››_ =/ _))
  ""                        :: "field => fields"                    (‹_›)
  "_datatype_fields"        :: "field => fields => fields"          (‹_,/ _›)
  "_datatype_record"        :: "fields => 'a"                       ((‹indent=3 notation=‹mixfix datatype record value››_))
  "_datatype_field_update"  :: "ident => 'a => field_update"        ((‹indent=2 notation=‹infix field update››_ :=/ _))
  ""                        :: "field_update => field_updates"      (‹_›)
  "_datatype_field_updates" :: "field_update => field_updates => field_updates"  (‹_,/ _›)
  "_datatype_record_update" :: "'a => field_updates => 'b"          ((‹open_block notation=‹mixfix datatype record update››_/(3_)) [900, 0] 900)

syntax (ASCII)
  "_datatype_record"        :: "fields => 'a"                       ((‹indent=3 notation=‹mixfix datatype record value››'(| _ |')))
  "_datatype_record_update" :: "'a => field_updates => 'b"          ((‹open_block notation=‹mixfix datatype record update››_/(3'(| _ |'))) [900, 0] 900)

end

named_theorems datatype_record_update

ML_file ‹datatype_records.ML›
setup Datatype_Records.setup

end