Theory Datatype_Records
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