diff options
Diffstat (limited to 'language')
| -rw-r--r-- | language/Makefile | 22 | ||||
| -rw-r--r-- | language/l2.lem | 103 | ||||
| -rw-r--r-- | language/l2.ml | 107 | ||||
| -rw-r--r-- | language/type_system.tex (renamed from language/manual.tex) | 4 |
4 files changed, 120 insertions, 116 deletions
diff --git a/language/Makefile b/language/Makefile index 1420ab1f..c297829c 100644 --- a/language/Makefile +++ b/language/Makefile @@ -4,7 +4,9 @@ OTT=../../../github/ott/src/ott OTTLIB=$(dir $(shell which ott))../hol .PHONY: all -all: l2.pdf l2_parse.pdf l2.ml l2_parse.ml l2.lem +all: l2.ml l2_parse.ml l2.lem + +docs: l2.pdf l2_parse.pdf %.pdf: %.tex pdflatex $< @@ -12,9 +14,9 @@ all: l2.pdf l2_parse.pdf l2.ml l2_parse.ml l2.lem %Theory.uo: %Script.sml Holmake --qof -I $(OTTLIB) $@ -manual.pdf: doc_in.tex manual.tex - pdflatex manual.tex - pdflatex manual.tex +type_system.pdf: doc_in.tex type_system.tex + pdflatex type_system.tex + pdflatex type_system.tex l2.tex: l2.ott l2_typ.ott l2_rules.ott $(OTT) -sort false -generate_aux_rules false -o $@ -picky_multiple_parses true $^ @@ -36,7 +38,11 @@ l2.lem: l2.ott l2_typ.ott clean: rm -rf *~ - -rm -rf *.uo *.ui *.sig *.sml .HOLMK - -rm -f *.aux *.log *.dvi *.ps *.pdf - rm -rf l2.pdf l2_parse.pdf l2.ml l2_parse.ml l2.lem - rm -rf l2.tex doc_in.tex
\ No newline at end of file + rm -rf *.uo *.ui *.sig *.sml .HOLMK + rm -f *.aux *.log *.dvi *.ps *.pdf *.toc + rm -rf l2.pdf l2_parse.pdf + rm -rf l2.tex doc_in.tex + +realclean: + $(MAKE) clean + rm -rf l2.ml l2_parse.ml l2.lem
\ No newline at end of file diff --git a/language/l2.lem b/language/l2.lem index 2d375340..40b23099 100644 --- a/language/l2.lem +++ b/language/l2.lem @@ -34,11 +34,11 @@ type base_kind = | BK_aux of base_kind_aux * l -type kid_aux = (* variables with kind, ticked to differentiate from program variables *) +type kid_aux = (* kinded IDs: Type, Nat, Order, and Effect variables *) | Var of x -type id_aux = (* Identifier *) +type id_aux = (* identifier *) | Id of x | DeIid of x (* remove infix status *) @@ -59,8 +59,8 @@ type kind = | K_aux of kind_aux * l -type nexp_aux = (* expression of kind Nat, for vector sizes and origins *) - | Nexp_id of id (* identifier, bound by \texttt{def Nat x = nexp} *) +type nexp_aux = (* numeric expression, of kind Nat *) + | Nexp_id of id (* abbreviation identifier *) | Nexp_var of kid (* variable *) | Nexp_constant of integer (* constant *) | Nexp_times of nexp * nexp (* product *) @@ -84,10 +84,10 @@ type base_effect_aux = (* effect *) | BE_depend (* dynamic footprint *) | BE_undef (* undefined-instruction exception *) | BE_unspec (* unspecified values *) - | BE_nondet (* nondeterminism from intra-instruction parallelism *) - | BE_escape (* Tracking of expressions and functions that might call exit *) - | BE_lset (* Local mutation happend; not user-writable *) - | BE_lret (* Local return happened; not user-writable *) + | BE_nondet (* nondeterminism, from nondet *) + | BE_escape (* potential call of exit *) + | BE_lset (* local mutation; not user-writable *) + | BE_lret (* local return; not user-writable *) type base_effect = @@ -96,11 +96,11 @@ type base_effect = type order_aux = (* vector order specifications, of kind Order *) | Ord_var of kid (* variable *) - | Ord_inc (* increasing (little-endian) *) - | Ord_dec (* decreasing (big-endian) *) + | Ord_inc (* increasing *) + | Ord_dec (* decreasing *) -type effect_aux = (* effect set, of kind Effects *) +type effect_aux = (* effect set, of kind Effect *) | Effect_var of kid | Effect_set of list base_effect (* effect set *) @@ -152,7 +152,7 @@ type typquant_aux = (* type quantifiers and constraints *) | TypQ_no_forall (* empty *) -type lit_aux = (* Literal constant *) +type lit_aux = (* literal constant *) | L_unit (* $() : unit$ *) | L_zero (* $bitzero : bit$ *) | L_one (* $bitone : bit$ *) @@ -161,26 +161,26 @@ type lit_aux = (* Literal constant *) | L_num of integer (* natural number constant *) | L_hex of string (* bit vector constant, C-style *) | L_bin of string (* bit vector constant, C-style *) - | L_undef (* constant representing undefined values *) | L_string of string (* string constant *) + | L_undef (* undefined-value constant *) type typquant = | TypQ_aux of typquant_aux * l -type typ_aux = (* Type expressions, of kind $Type$ *) - | Typ_wild (* Unspecified type *) - | Typ_id of id (* Defined type *) - | Typ_var of kid (* Type variable *) - | Typ_fn of typ * typ * effect (* Function type (first-order only in user code) *) - | Typ_tup of list typ (* Tuple type *) +type typ_aux = (* type expressions, of kind $Type$ *) + | Typ_wild (* unspecified type *) + | Typ_id of id (* defined type *) + | Typ_var of kid (* type variable *) + | Typ_fn of typ * typ * effect (* Function (first-order only in user code) *) + | Typ_tup of list typ (* Tuple *) | Typ_app of id * list typ_arg (* type constructor application *) and typ = | Typ_aux of typ_aux * l -and typ_arg_aux = (* Type constructor arguments of all kinds *) +and typ_arg_aux = (* type constructor arguments of all kinds *) | Typ_arg_nexp of nexp | Typ_arg_typ of typ | Typ_arg_order of order @@ -198,7 +198,7 @@ type typschm_aux = (* type scheme *) | TypSchm_ts of typquant * typ -type pat_aux 'a = (* Pattern *) +type pat_aux 'a = (* pattern *) | P_lit of lit (* literal constant pattern *) | P_wild (* wildcard *) | P_as of (pat 'a) * id (* named pattern *) @@ -215,7 +215,7 @@ type pat_aux 'a = (* Pattern *) and pat 'a = | P_aux of (pat_aux 'a) * annot 'a -and fpat_aux 'a = (* Field pattern *) +and fpat_aux 'a = (* field pattern *) | FP_Fpat of id * (pat 'a) and fpat 'a = @@ -230,7 +230,7 @@ type reg_id_aux 'a = | RI_id of id -type exp_aux 'a = (* Expression *) +type exp_aux 'a = (* expression *) | E_block of list (exp 'a) (* sequential block *) | E_nondet of list (exp 'a) (* nondeterministic block *) | E_id of id (* identifier *) @@ -285,32 +285,32 @@ and lexp_aux 'a = (* lvalue expression *) and lexp 'a = | LEXP_aux of (lexp_aux 'a) * annot 'a -and fexp_aux 'a = (* Field-expression *) +and fexp_aux 'a = (* field expression *) | FE_Fexp of id * (exp 'a) and fexp 'a = | FE_aux of (fexp_aux 'a) * annot 'a -and fexps_aux 'a = (* Field-expression list *) +and fexps_aux 'a = (* field expression list *) | FES_Fexps of list (fexp 'a) * bool and fexps 'a = | FES_aux of (fexps_aux 'a) * annot 'a -and opt_default_aux 'a = (* Optional default value for indexed vectors, to define a default value for any unspecified positions in a sparse map *) +and opt_default_aux 'a = (* optional default value for indexed vector expressions *) | Def_val_empty | Def_val_dec of (exp 'a) and opt_default 'a = | Def_val_aux of (opt_default_aux 'a) * annot 'a -and pexp_aux 'a = (* Pattern match *) +and pexp_aux 'a = (* pattern match *) | Pat_exp of (pat 'a) * (exp 'a) and pexp 'a = | Pat_aux of (pexp_aux 'a) * annot 'a -and letbind_aux 'a = (* Let binding *) +and letbind_aux 'a = (* let binding *) | LB_val_explicit of typschm * (pat 'a) * (exp 'a) (* let, explicit type ((pat 'a) must be total) *) | LB_val_implicit of (pat 'a) * (exp 'a) (* let, implicit type ((pat 'a) must be total) *) @@ -322,35 +322,35 @@ type reg_id 'a = | RI_aux of (reg_id_aux 'a) * annot 'a -type type_union_aux = (* Type union constructors *) +type type_union_aux = (* type union constructors *) | Tu_id of id | Tu_ty_id of typ * id -type name_scm_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *) +type name_scm_opt_aux = (* optional variable naming-scheme constraint *) | Name_sect_none | Name_sect_some of string -type effect_opt_aux = (* Optional effect annotation for functions *) +type effect_opt_aux = (* optional effect annotation for functions *) | Effect_opt_pure (* sugar for empty effect set *) | Effect_opt_effect of effect -type funcl_aux 'a = (* Function clause *) +type funcl_aux 'a = (* function clause *) | FCL_Funcl of id * (pat 'a) * (exp 'a) -type rec_opt_aux = (* Optional recursive annotation for functions *) +type rec_opt_aux = (* optional recursive annotation for functions *) | Rec_nonrec (* non-recursive *) | Rec_rec (* recursive *) -type tannot_opt_aux = (* Optional type annotation for functions *) +type tannot_opt_aux = (* optional type annotation for functions *) | Typ_annot_opt_some of typquant * typ -type alias_spec_aux 'a = (* Register alias expression forms *) +type alias_spec_aux 'a = (* register alias expression forms *) | AL_subreg of (reg_id 'a) * id | AL_bit of (reg_id 'a) * (exp 'a) | AL_slice of (reg_id 'a) * (exp 'a) * (exp 'a) @@ -394,28 +394,28 @@ type alias_spec 'a = | AL_aux of (alias_spec_aux 'a) * annot 'a -type default_spec_aux 'a = (* Default kinding or typing assumption *) - | DT_kind of base_kind * kid +type default_spec_aux 'a = (* default kinding or typing assumption *) | DT_order of order + | DT_kind of base_kind * kid | DT_typ of typschm * id -type type_def_aux 'a = (* Type definition body *) +type type_def_aux 'a = (* type definition body *) | TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *) | TD_record of id * name_scm_opt * typquant * list (typ * id) * bool (* struct type definition *) - | TD_variant of id * name_scm_opt * typquant * list type_union * bool (* union type definition *) + | TD_variant of id * name_scm_opt * typquant * list type_union * bool (* tagged union type definition *) | TD_enum of id * name_scm_opt * list id * bool (* enumeration type definition *) | TD_register of id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *) -type val_spec_aux 'a = (* Value type specification *) - | VS_val_spec of typschm * id - | VS_extern_no_rename of typschm * id - | VS_extern_spec of typschm * id * string (* Specify the type and id of a function from Lem, where the string must provide an explicit path to the required function but will not be checked *) +type val_spec_aux 'a = (* value type specification *) + | VS_val_spec of typschm * id (* specify the type of an upcoming definition *) + | VS_extern_no_rename of typschm * id (* specify the type of an external function *) + | VS_extern_spec of typschm * id * string (* specify the type of a function from Lem *) -type kind_def_aux 'a = (* Definition body for elements of kind; many are shorthands for type\_defs *) - | KD_nabbrev of kind * id * name_scm_opt * nexp (* nexp abbreviation *) +type kind_def_aux 'a = (* Definition body for elements of kind *) + | KD_nabbrev of kind * id * name_scm_opt * nexp (* Nat-expression abbreviation *) | KD_abbrev of kind * id * name_scm_opt * typschm (* type abbreviation *) | KD_record of kind * id * name_scm_opt * typquant * list (typ * id) * bool (* struct type definition *) | KD_variant of kind * id * name_scm_opt * typquant * list type_union * bool (* union type definition *) @@ -423,8 +423,7 @@ type kind_def_aux 'a = (* Definition body for elements of kind; many are shorth | KD_register of kind * id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *) -type scattered_def_aux 'a = (* Function and type union definitions that can be spread across - a file. Each one must end in $id$ *) +type scattered_def_aux 'a = (* scattered function and union type definitions *) | SD_scattered_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *) | SD_scattered_funcl of (funcl 'a) (* scattered function definition clause *) | SD_scattered_variant of id * name_scm_opt * typquant (* scattered union definition header *) @@ -432,11 +431,11 @@ type scattered_def_aux 'a = (* Function and type union definitions that can be | SD_scattered_end of id (* scattered definition end *) -type fundef_aux 'a = (* Function definition *) +type fundef_aux 'a = (* function definition *) | FD_function of rec_opt * tannot_opt * effect_opt * list (funcl 'a) -type dec_spec_aux 'a = (* Register declarations *) +type dec_spec_aux 'a = (* register declarations *) | DEC_reg of typ * id | DEC_alias of id * (alias_spec 'a) | DEC_typ_alias of typ * id * (alias_spec 'a) @@ -470,11 +469,11 @@ type dec_spec 'a = | DEC_aux of (dec_spec_aux 'a) * annot 'a -type dec_comm 'a = (* Top-level generated comments *) +type dec_comm 'a = (* top-level generated comments *) | DC_comm of string (* generated unstructured comment *) | DC_comm_struct of (def 'a) (* generated structured comment *) -and def 'a = (* Top-level definition *) +and def 'a = (* top-level definition *) | DEF_kind of (kind_def 'a) (* definition of named kind identifiers *) | DEF_type of (type_def 'a) (* type definition *) | DEF_fundef of (fundef 'a) (* function definition *) @@ -486,7 +485,7 @@ and def 'a = (* Top-level definition *) | DEF_comm of (dec_comm 'a) (* generated comments *) -type defs 'a = (* Definition sequence *) +type defs 'a = (* definition sequence *) | Defs of list (def 'a) diff --git a/language/l2.ml b/language/l2.ml index 4043c8e6..538cd234 100644 --- a/language/l2.ml +++ b/language/l2.ml @@ -25,13 +25,13 @@ base_kind = type -id_aux = (* Identifier *) +id_aux = (* identifier *) Id of x | DeIid of x (* remove infix status *) type -kid_aux = (* variables with kind, ticked to differentiate from program variables *) +kid_aux = (* kinded IDs: _, _, _, and _ variables *) Var of x @@ -56,8 +56,8 @@ kind = type -nexp_aux = (* expression of kind _, for vector sizes and origins *) - Nexp_id of id (* identifier, bound by \texttt{def Nat x = nexp} *) +nexp_aux = (* numeric expression, of kind _ *) + Nexp_id of id (* abbreviation identifier *) | Nexp_var of kid (* variable *) | Nexp_constant of int (* constant *) | Nexp_times of nexp * nexp (* product *) @@ -82,10 +82,10 @@ base_effect_aux = (* effect *) | BE_depend (* dynamic footprint *) | BE_undef (* undefined-instruction exception *) | BE_unspec (* unspecified values *) - | BE_nondet (* nondeterminism from intra-instruction parallelism *) - | BE_escape (* Tracking of expressions and functions that might call exit *) - | BE_lset (* Local mutation happend; not user-writable *) - | BE_lret (* Local return happened; not user-writable *) + | BE_nondet (* nondeterminism, from _ *) + | BE_escape (* potential call of _ *) + | BE_lset (* local mutation; not user-writable *) + | BE_lret (* local return; not user-writable *) type @@ -94,14 +94,14 @@ base_effect = type -order_aux = (* vector order specifications, of kind Order *) +order_aux = (* vector order specifications, of kind _ *) Ord_var of kid (* variable *) - | Ord_inc (* increasing (little-endian) *) - | Ord_dec (* decreasing (big-endian) *) + | Ord_inc (* increasing *) + | Ord_dec (* decreasing *) type -effect_aux = (* effect set, of kind Effects *) +effect_aux = (* effect set, of kind _ *) Effect_var of kid | Effect_set of (base_effect) list (* effect set *) @@ -158,7 +158,7 @@ typquant_aux = (* type quantifiers and constraints *) type -lit_aux = (* Literal constant *) +lit_aux = (* literal constant *) L_unit (* $() : _$ *) | L_zero (* $_ : _$ *) | L_one (* $_ : _$ *) @@ -167,8 +167,8 @@ lit_aux = (* Literal constant *) | L_num of int (* natural number constant *) | L_hex of string (* bit vector constant, C-style *) | L_bin of string (* bit vector constant, C-style *) - | L_undef (* constant representing undefined values *) | L_string of string (* string constant *) + | L_undef (* undefined-value constant *) type @@ -177,18 +177,18 @@ typquant = type -typ_aux = (* Type expressions, of kind $_$ *) - Typ_wild (* Unspecified type *) - | Typ_id of id (* Defined type *) - | Typ_var of kid (* Type variable *) - | Typ_fn of typ * typ * effect (* Function type (first-order only in user code) *) - | Typ_tup of (typ) list (* Tuple type *) +typ_aux = (* type expressions, of kind $_$ *) + Typ_wild (* unspecified type *) + | Typ_id of id (* defined type *) + | Typ_var of kid (* type variable *) + | Typ_fn of typ * typ * effect (* Function (first-order only in user code) *) + | Typ_tup of (typ) list (* Tuple *) | Typ_app of id * (typ_arg) list (* type constructor application *) and typ = Typ_aux of typ_aux * l -and typ_arg_aux = (* Type constructor arguments of all kinds *) +and typ_arg_aux = (* type constructor arguments of all kinds *) Typ_arg_nexp of nexp | Typ_arg_typ of typ | Typ_arg_order of order @@ -209,7 +209,7 @@ typschm_aux = (* type scheme *) type -'a pat_aux = (* Pattern *) +'a pat_aux = (* pattern *) P_lit of lit (* literal constant pattern *) | P_wild (* wildcard *) | P_as of 'a pat * id (* named pattern *) @@ -226,7 +226,7 @@ type and 'a pat = P_aux of 'a pat_aux * 'a annot -and 'a fpat_aux = (* Field pattern *) +and 'a fpat_aux = (* field pattern *) FP_Fpat of id * 'a pat and 'a fpat = @@ -244,7 +244,7 @@ type type -'a exp_aux = (* Expression *) +'a exp_aux = (* expression *) E_block of ('a exp) list (* sequential block *) | E_nondet of ('a exp) list (* nondeterministic block *) | E_id of id (* identifier *) @@ -299,32 +299,32 @@ and 'a lexp_aux = (* lvalue expression *) and 'a lexp = LEXP_aux of 'a lexp_aux * 'a annot -and 'a fexp_aux = (* Field-expression *) +and 'a fexp_aux = (* field expression *) FE_Fexp of id * 'a exp and 'a fexp = FE_aux of 'a fexp_aux * 'a annot -and 'a fexps_aux = (* Field-expression list *) +and 'a fexps_aux = (* field expression list *) FES_Fexps of ('a fexp) list * bool and 'a fexps = FES_aux of 'a fexps_aux * 'a annot -and 'a opt_default_aux = (* Optional default value for indexed vectors, to define a default value for any unspecified positions in a sparse map *) +and 'a opt_default_aux = (* optional default value for indexed vector expressions *) Def_val_empty | Def_val_dec of 'a exp and 'a opt_default = Def_val_aux of 'a opt_default_aux * 'a annot -and 'a pexp_aux = (* Pattern match *) +and 'a pexp_aux = (* pattern match *) Pat_exp of 'a pat * 'a exp and 'a pexp = Pat_aux of 'a pexp_aux * 'a annot -and 'a letbind_aux = (* Let binding *) +and 'a letbind_aux = (* let binding *) LB_val_explicit of typschm * 'a pat * 'a exp (* let, explicit type ('a pat must be total) *) | LB_val_implicit of 'a pat * 'a exp (* let, implicit type ('a pat must be total) *) @@ -338,41 +338,41 @@ type type -type_union_aux = (* Type union constructors *) +type_union_aux = (* type union constructors *) Tu_id of id | Tu_ty_id of typ * id type -name_scm_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *) +name_scm_opt_aux = (* optional variable naming-scheme constraint *) Name_sect_none | Name_sect_some of string type -effect_opt_aux = (* Optional effect annotation for functions *) +effect_opt_aux = (* optional effect annotation for functions *) Effect_opt_pure (* sugar for empty effect set *) | Effect_opt_effect of effect type -'a funcl_aux = (* Function clause *) +'a funcl_aux = (* function clause *) FCL_Funcl of id * 'a pat * 'a exp type -rec_opt_aux = (* Optional recursive annotation for functions *) +rec_opt_aux = (* optional recursive annotation for functions *) Rec_nonrec (* non-recursive *) | Rec_rec (* recursive *) type -tannot_opt_aux = (* Optional type annotation for functions *) +tannot_opt_aux = (* optional type annotation for functions *) Typ_annot_opt_some of typquant * typ type -'a alias_spec_aux = (* Register alias expression forms *) +'a alias_spec_aux = (* register alias expression forms *) AL_subreg of 'a reg_id * id | AL_bit of 'a reg_id * 'a exp | AL_slice of 'a reg_id * 'a exp * 'a exp @@ -425,31 +425,31 @@ type type -'a default_spec_aux = (* Default kinding or typing assumption *) - DT_kind of base_kind * kid - | DT_order of order +'a default_spec_aux = (* default kinding or typing assumption *) + DT_order of order + | DT_kind of base_kind * kid | DT_typ of typschm * id type -'a type_def_aux = (* Type definition body *) +'a type_def_aux = (* type definition body *) TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *) | TD_record of id * name_scm_opt * typquant * ((typ * id)) list * bool (* struct type definition *) - | TD_variant of id * name_scm_opt * typquant * (type_union) list * bool (* union type definition *) + | TD_variant of id * name_scm_opt * typquant * (type_union) list * bool (* tagged union type definition *) | TD_enum of id * name_scm_opt * (id) list * bool (* enumeration type definition *) | TD_register of id * nexp * nexp * ((index_range * id)) list (* register mutable bitfield type definition *) type -'a val_spec_aux = (* Value type specification *) - VS_val_spec of typschm * id - | VS_extern_no_rename of typschm * id - | VS_extern_spec of typschm * id * string (* Specify the type and id of a function from Lem, where the string must provide an explicit path to the required function but will not be checked *) +'a val_spec_aux = (* value type specification *) + VS_val_spec of typschm * id (* specify the type of an upcoming definition *) + | VS_extern_no_rename of typschm * id (* specify the type of an external function *) + | VS_extern_spec of typschm * id * string (* specify the type of a function from Lem *) type -'a kind_def_aux = (* Definition body for elements of kind; many are shorthands for type\_defs *) - KD_nabbrev of kind * id * name_scm_opt * nexp (* nexp abbreviation *) +'a kind_def_aux = (* Definition body for elements of kind *) + KD_nabbrev of kind * id * name_scm_opt * nexp (* _-expression abbreviation *) | KD_abbrev of kind * id * name_scm_opt * typschm (* type abbreviation *) | KD_record of kind * id * name_scm_opt * typquant * ((typ * id)) list * bool (* struct type definition *) | KD_variant of kind * id * name_scm_opt * typquant * (type_union) list * bool (* union type definition *) @@ -458,8 +458,7 @@ type type -'a scattered_def_aux = (* Function and type union definitions that can be spread across - a file. Each one must end in $_$ *) +'a scattered_def_aux = (* scattered function and union type definitions *) SD_scattered_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *) | SD_scattered_funcl of 'a funcl (* scattered function definition clause *) | SD_scattered_variant of id * name_scm_opt * typquant (* scattered union definition header *) @@ -468,12 +467,12 @@ type type -'a fundef_aux = (* Function definition *) +'a fundef_aux = (* function definition *) FD_function of rec_opt * tannot_opt * effect_opt * ('a funcl) list type -'a dec_spec_aux = (* Register declarations *) +'a dec_spec_aux = (* register declarations *) DEC_reg of typ * id | DEC_alias of id * 'a alias_spec | DEC_typ_alias of typ * id * 'a alias_spec @@ -515,11 +514,11 @@ type type -'a dec_comm = (* Top-level generated comments *) +'a dec_comm = (* top-level generated comments *) DC_comm of string (* generated unstructured comment *) | DC_comm_struct of 'a def (* generated structured comment *) -and 'a def = (* Top-level definition *) +and 'a def = (* top-level definition *) DEF_kind of 'a kind_def (* definition of named kind identifiers *) | DEF_type of 'a type_def (* type definition *) | DEF_fundef of 'a fundef (* function definition *) @@ -532,7 +531,7 @@ and 'a def = (* Top-level definition *) type -'a defs = (* Definition sequence *) +'a defs = (* definition sequence *) Defs of ('a def) list diff --git a/language/manual.tex b/language/type_system.tex index 5d4b9d6a..afb9fb88 100644 --- a/language/manual.tex +++ b/language/type_system.tex @@ -8,7 +8,7 @@ \input{doc_in} -\title{Sail Manual} +\title{Sail Type System} \author{Kathryn E Gray, Gabriel Kerneis, Peter Sewell} \maketitle @@ -114,4 +114,4 @@ \section{Sail operational semantics \{TODO\}} -\end{document}
\ No newline at end of file +\end{document} |