src/HOL/Record.thy
author wenzelm
Wed Sep 27 19:34:46 2000 +0200 (2000-09-27)
changeset 10093 44584c2b512b
parent 9729 40cfc3dd27da
child 10309 a7f961fb62c6
permissions -rw-r--r--
more symbolic syntax (currently "input");
     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   ""                    :: "id => ident"                                ("_")
    21   ""                    :: "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"             :: "[ident, 'a] => update"                      ("(2_ :=/ _)")
    39   ""                    :: "update => updates"                          ("_")
    40   "_updates"            :: "[update, updates] => updates"               ("_,/ _")
    41   "_record_update"      :: "['a, updates] => 'b"                ("_/(3'(| _ |'))" [900,0] 900)
    42 
    43 syntax (input)   (* FIXME (xsymbols) *)
    44   "_record_type"        :: "field_types => type"                        ("(3\<lparr>_\<rparr>)")
    45   "_record_type_scheme" :: "[field_types, type] => type"        ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)")
    46   "_record"             :: "fields => 'a"                               ("(3\<lparr>_\<rparr>)")
    47   "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
    48   "_record_update"      :: "['a, updates] => 'b"                ("_/(3\<lparr>_\<rparr>)" [900,0] 900)
    49 
    50 
    51 (* type class for record extensions *)
    52 
    53 axclass more < "term"
    54 instance unit :: more
    55   by intro_classes
    56 
    57 
    58 (* initialize the package *)
    59 
    60 setup
    61   RecordPackage.setup
    62 
    63 
    64 end