src/HOL/Record.thy
author wenzelm
Tue Aug 07 22:37:30 2001 +0200 (2001-08-07)
changeset 11473 4546d8d39221
parent 10641 d1533f63c738
child 11489 1fd5469c195e
permissions -rw-r--r--
fix problem with user translations by making field names appear as consts;
     1 (*  Title:      HOL/Record.thy
     2     ID:         $Id$
     3     Author:     Wolfgang Naraschewski and Markus Wenzel, TU Muenchen
     4 
     5 Extensible records with structural subtyping in HOL.  See
     6 Tools/record_package.ML for the actual implementation.
     7 *)
     8 
     9 theory Record = Datatype
    10 files "Tools/record_package.ML":
    11 
    12 
    13 (* concrete syntax *)
    14 
    15 nonterminals
    16   ident field_type field_types field fields update updates
    17 
    18 syntax
    19   (*field names*)
    20   "_field_name"         :: "id => ident"                                ("_")
    21   "_field_name"         :: "longid => ident"                            ("_")
    22 
    23   (*record types*)
    24   "_field_type"         :: "[ident, type] => field_type"                ("(2_ ::/ _)")
    25   ""                    :: "field_type => field_types"                  ("_")
    26   "_field_types"        :: "[field_type, field_types] => field_types"   ("_,/ _")
    27   "_record_type"        :: "field_types => type"                        ("(3'(| _ |'))")
    28   "_record_type_scheme" :: "[field_types, type] => type"        ("(3'(| _,/ (2... ::/ _) |'))")
    29 
    30   (*records*)
    31   "_field"              :: "[ident, 'a] => field"                       ("(2_ =/ _)")
    32   ""                    :: "field => fields"                            ("_")
    33   "_fields"             :: "[field, fields] => fields"                  ("_,/ _")
    34   "_record"             :: "fields => 'a"                               ("(3'(| _ |'))")
    35   "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3'(| _,/ (2... =/ _) |'))")
    36 
    37   (*record updates*)
    38   "_update_name"        :: idt
    39   "_update"             :: "[ident, 'a] => update"                      ("(2_ :=/ _)")
    40   ""                    :: "update => updates"                          ("_")
    41   "_updates"            :: "[update, updates] => updates"               ("_,/ _")
    42   "_record_update"      :: "['a, updates] => 'b"                ("_/(3'(| _ |'))" [900,0] 900)
    43 
    44 syntax (xsymbols)
    45   "_record_type"        :: "field_types => type"                        ("(3\<lparr>_\<rparr>)")
    46   "_record_type_scheme" :: "[field_types, type] => type"        ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)")
    47   "_record"             :: "fields => 'a"                               ("(3\<lparr>_\<rparr>)")
    48   "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
    49   "_record_update"      :: "['a, updates] => 'b"                ("_/(3\<lparr>_\<rparr>)" [900,0] 900)
    50 
    51 parse_translation {*
    52   let
    53     fun update_name_tr (Free (x, T) :: ts) =
    54           Term.list_comb (Free (suffix RecordPackage.updateN x, T), ts)
    55       | update_name_tr (Const (x, T) :: ts) =
    56           Term.list_comb (Const (suffix RecordPackage.updateN x, T), ts)
    57       | update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) =
    58           Term.list_comb (c $ update_name_tr [t] $
    59             (Syntax.const "fun" $ ty $ Syntax.const "dummy"), ts)
    60       | update_name_tr ts = raise TERM ("update_name_tr", ts);
    61   in [("_update_name", update_name_tr)] end
    62 *}
    63 
    64 
    65 (* type class for record extensions *)
    66 
    67 axclass more < "term"
    68 instance unit :: more ..
    69 
    70 
    71 (* initialize the package *)
    72 
    73 setup
    74   RecordPackage.setup
    75 
    76 
    77 end