src/HOL/Record.thy
author wenzelm
Thu Mar 11 13:20:35 1999 +0100 (1999-03-11)
changeset 6349 f7750d816c21
parent 5732 8712391bbf3d
child 7357 d0e16da40ea2
permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
     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 Record = Datatype +
    10 
    11 
    12 (* concrete syntax *)
    13 
    14 nonterminals
    15   ident field_type field_types field fields update updates
    16 
    17 syntax
    18   (*field names*)
    19   ""                	:: "id => ident"                    		("_")
    20   ""                	:: "longid => ident"                		("_")
    21 
    22   (*record types*)
    23   "_field_type"         :: "[ident, type] => field_type"           	("(2_ ::/ _)")
    24   ""               	:: "field_type => field_types"              	("_")
    25   "_field_types"	:: "[field_type, field_types] => field_types"   ("_,/ _")
    26   "_record_type"	:: "field_types => type"                   	("(3'(| _ |'))")
    27   "_record_type_scheme"	:: "[field_types, type] => type"	("(3'(| _,/ (2... ::/ _) |'))")
    28 
    29   (*records*)
    30   "_field"          	:: "[ident, 'a] => field"           		("(2_ =/ _)")
    31   ""                	:: "field => fields"                		("_")
    32   "_fields"         	:: "[field, fields] => fields"      		("_,/ _")
    33   "_record"         	:: "fields => 'a"                   		("(3'(| _ |'))")
    34   "_record_scheme"  	:: "[fields, 'a] => 'a"             	("(3'(| _,/ (2... =/ _) |'))")
    35 
    36   (*record updates*)
    37   "_update"	    	:: "[ident, 'a] => update"           		("(2_ :=/ _)")
    38   ""                	:: "update => updates"               		("_")
    39   "_updates"        	:: "[update, updates] => updates"    		("_,/ _")
    40   "_record_update"  	:: "['a, updates] => 'b"               	("_/(3'(| _ |'))" [900,0] 900)
    41 
    42 
    43 (* type class for record extensions *)
    44 
    45 axclass more < term
    46 instance unit :: more
    47 
    48 
    49 (* initialize the package *)
    50 
    51 setup
    52   RecordPackage.setup
    53 
    54 
    55 end