rename "manual.tex" to "type_system.tex"

fix Makefile clean

5 files changed, 121 insertions, 117 deletions

diff --git a/README b/README
index a380d9bd..2e96dfae 100644
--- a/README
+++ b/README
@@ -167,7 +167,7 @@ l2_parse.ott    Grammar of Sail generated by parser, superset of source language
 l2.ott          Grammar of Sail source
 l2_typ.ott      Grammar of Internal structures used for type annotations
 l2_rules.ott    Rules for type system
-manual.tex      Source of manual
+type_system.tex Source of type system LaTeX document
 
 Relevant make commands:
 make          Builds pdfs for l2 and l2_parse, ml and lem files of grammars
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}