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