flesh out sketch of more of our Friday discussion

1 files changed, 808 insertions, 744 deletions

diff --git a/language/l2.ott b/language/l2.ott
index b494cf86..2deac86f 100644
--- a/language/l2.ott
+++ b/language/l2.ott
@@ -155,26 +155,26 @@ metavar ix ::=
 
 grammar
 
-l :: '' ::=					{{ phantom }}
-						{{ ocaml l }}
-						{{ lem l }}
-						{{ hol unit }}
+l :: '' ::=                                     {{ phantom }}
+                                                {{ ocaml l }}
+                                                {{ lem l }}
+                                                {{ hol unit }}
   {{ com Source locations }}
-  | 						:: :: Unknown
+  |                                             :: :: Unknown
     {{ ocaml Unknown }}
     {{ lem Unknown }}
     {{ hol () }}
 
 x_l {{ tex \ottnt{x}^{l} }} , y_l {{ tex \ottnt{y}^{l} }} , z_l {{ tex \ottnt{z}^{l} }} , name :: '' ::=
   {{ com Location-annotated names }}
-  | x l						:: :: X_l
-  | ( ix ) l					:: :: PreX_l
+  | x l                                         :: :: X_l
+  | ( ix ) l                                    :: :: PreX_l
     {{ com Remove infix status }}
 
 ix_l {{ tex \ottnt{ix}^{l} }} :: '' ::=
   {{ com Location-annotated infix names }}
-  | ix l					:: :: SymX_l
-  | ` x ` l					:: :: InX_l
+  | ix l                                        :: :: SymX_l
+  | ` x ` l                                     :: :: InX_l
     {{ com Add infix status }}
 
 embed
@@ -211,16 +211,16 @@ grammar
 id :: '' ::=
   {{ com Not-very-long identifers }}
   {{ aux _ l }}
-  | x				:: :: Id
+  | x                           :: :: Id
 
 
 a :: 'A_' ::=
                                                 {{ aux _ l }}
-						{{ ocaml terminal * text }}
-						{{ lem terminal * string }}
-						{{ hol string }}
+                                                {{ ocaml terminal * text }}
+                                                {{ lem terminal * string }}
+                                                {{ hol string }}
   {{ com Type variables }}
-  | ' x 					:: :: A
+  | ' x                                         :: :: A
     {{ ichlo [[x]] }}
 
 N :: 'N_' ::=
@@ -252,19 +252,19 @@ EFF :: 'EFF_' ::=
 % TODO: better concrete syntax!!!!
 
 
-tnvar :: '' ::=				
-    {{ com Union of type, nexp, endianess and effect variables }}
-    | a					:: :: Av
-    | N					:: :: Nv
-    | EN				:: :: ENv
-    | EFF				:: :: EFFv
+tnvar :: '' ::=                         
+    {{ com variables of the base kinds }}
+    | a                                 :: :: Av
+    | N                                 :: :: Nv
+    | EN                                :: :: ENv
+    | EFF                               :: :: EFFv
 
-tnvars :: '' ::=				{{ phantom }}
-						{{ hol tnvar list }}
-						{{ ocaml tnvar list }}
-						{{ lem list tnvar }}
+tnvars :: '' ::=                                {{ phantom }}
+                                                {{ hol tnvar list }}
+                                                {{ ocaml tnvar list }}
+                                                {{ lem list tnvar }}
   {{ com Type variable lists }}
-  | tnvar1 .. tnvarn		:: :: Tvars
+  | tnvar1 .. tnvarn            :: :: Tvars
     {{ hol [[tnvar1..tnvarn]] }}
     {{ ocaml [[tnvar1..tnvarn]] }}
     {{ lem [[tnvar1..tnvarn]] }}
@@ -285,22 +285,22 @@ kind :: '' ::=
 
     
 nexp :: 'Nexp_' ::=  
-  {{ com Numerical expressions for specifying vector lengths and indexes}}
+  {{ com expressions of kind Nat, for vector lengths }}
   {{ aux _ l }}
   | N                                   :: :: var
   | num                                 :: :: constant
   | nexp1 * nexp2                       :: :: times {{ com must be linear after normalisation... }}
-  | nexp1 + nexp2			:: :: sum
+  | nexp1 + nexp2                       :: :: sum
   | 2 ^ nexp                            :: :: exp
-  | ( nexp )				:: S :: paren  {{ icho [[nexp]] }}
+  | ( nexp )                            :: S :: paren  {{ icho [[nexp]] }}
 
-end :: 'End_' ::=  
+endian :: 'End_' ::=  
   {{ com endianness specifications}}
   {{ aux _ l }}
   | EN                                  :: :: var
   | inc                                 :: :: inc
   | dec                                 :: :: dec
-  | ( end )				:: S :: paren {{ icho [[end]] }}
+  | ( endian )                             :: S :: paren {{ icho [[endian]] }}
 
 effect :: 'Effect_' ::=
   {{ com effect }}
@@ -326,22 +326,22 @@ effects :: 'Effects_' ::=
 
 typ :: 'Typ_' ::=
   {{ com Constructors (of all kinds, not just Type) }}
-  | _						:: :: wild
+  | _                                           :: :: wild
     {{ com Unspecified type }}
-  | a_l						:: :: var
+  | a_l                                         :: :: var
     {{ com Type variables }}
-  | typ1 -> typ2 effects			:: :: fn
+  | typ1 -> typ2 effects                        :: :: fn
     {{ com Function types -- first-order only}}
 % TODO: build first-order restriction into AST or just into type rules? neither - see note
 % TODO: concrete syntax for effects in a function type?  needed only for pp, not in user syntax.
-  | typ1 * .... * typn				:: :: tup
+  | typ1 * .... * typn                          :: :: tup
     {{ com Tuple types }}
-  | nexp					:: :: nexps 
+  | nexp                                        :: :: nexps 
   {{ com here to permit applications to nexps, otherwise not accepted }}
-  | id typ1 .. typn			:: :: app
+  | id typ1 .. typn                     :: :: app
   {{ com Type applications }}
   | ( typ )
-					:: S :: paren {{ icho [[typ]] }}
+                                        :: S :: paren {{ icho [[typ]] }}
 
 % plus more for l-value/r-value pairs, as introduced by the L3 'compound' declarations   ... ref typ
 
@@ -356,11 +356,11 @@ typ_sugar :: 'TypSugar_' ::=
   | nat :: :: nat
   | string :: :: string
 % finite subranges of nat
-  | enum nexp1 nexp2 end :: :: enum  {{ com type of the natural numbers from [[nexp2]] to [[nexp2]]+[[nexp1]]-1, ordered according to [[end]] }}
+  | enum nexp1 nexp2 endian :: :: enum  {{ com natural numbers from [[nexp2]] to [[nexp2]]+[[nexp1]]-1, ordered by [[endian]] }}
   | [ nexp ]             :: :: enum1 {{ com sugar for \texttt{enum nexp 0 inc} }}
   | [ nexp : nexp' ]  :: :: enum2 {{ com sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} }}
 % total maps and vectors indexed by finite subranges of nat
-  | enummap nexp1 nexp2 end typ :: :: enummap 
+  | enummap nexp1 nexp2 endian typ :: :: enummap 
 % probably some sugar for enummap types, using [ ] similarly to enums:
   | typ [ nexp ]  :: :: enummap2
   | typ [ nexp : nexp' ] :: :: enummap3
@@ -380,11 +380,11 @@ Typ_fn <= Typ_tup
 grammar
 
 nexp_constraint :: 'NC_' ::=
-  {{ com Whether a vector is bounded or fixed size }}
+  {{ com contraints over kind Nat }}
   {{ aux _ l }}
-  | nexp = nexp'				:: :: fixed
-  | nexp >= nexp'				:: :: bounded_ge
-  | nexp '<=' nexp'				:: :: bounded_le
+  | nexp = nexp'                                :: :: fixed
+  | nexp >= nexp'                               :: :: bounded_ge
+  | nexp '<=' nexp'                             :: :: bounded_le
   | nexp 'IN' { num1 , ... , numn }               :: :: ad_hoc_nat_set_bounded
 
 % Note only constants in a finite-set-bound, as we don't think we need
@@ -393,16 +393,14 @@ nexp_constraint :: 'NC_' ::=
 
 typquant :: 'TQ_' ::= 
   {{ aux _ l }}
-  | forall tnvar1 .. tnvarn . nexp_constraint1 , .. , nexp_constrainti => 							:: :: Ts
-%TODO add sugar here for no constraints and no constraints-or-tnvars
-%  |  forall tnvar1 ... tnvarn . typ             :: S :: Ts_no_constraint
-%
-% |  typ                                        :: S :: Ts_no_forall
+  | forall tnvar1 ... tnvarn . nexp_constraint1 , ... , nexp_constrainti . :: :: Ts {{ texlong }}
+  | forall tnvar1 ... tnvarn . ::  ::  Ts_no_constraint {{ com sugar }}
+  |                           ::  ::  Ts_no_forall     {{ com sugar }}
 
 typschm :: 'TS_' ::=
     {{ com Type schemes  }}
   {{ aux _ l }}
-  |  typquant typ							:: :: Ts
+  |  typquant typ                                                       :: :: Ts
 
 
 
@@ -413,38 +411,59 @@ typschm :: 'TS_' ::=
 grammar
 ctor_def :: '' ::=
   {{ com Datatype definition clauses }}
-  | x_l : typschm					:: :: Cte
+  | id : typschm                                       :: :: Cte
 % but we could get away with disallowing constraints in typschm, we
 % think - if it's useful to do that
 
-enumeration_flag_opt :: 'Enum_' ::=
+enum_opt :: 'Enum_' ::=
   |      :: :: empty
   | enum :: :: enum
 
 tdefbody :: 'Te_' ::=
   {{ com Type definition bodies }}
-  | typschm							:: :: abbrev
+  | typschm                                                     :: :: abbrev
     {{ com Type abbreviations }}
-  | typquant <| x_l1 : typ1 ; ... ; x_ln : typn semi_opt |>	:: :: record
+  | typquant <| id1 : typ1 ; ... ; idn : typn semi_opt |>     :: :: record
     {{ com Record types }}
-  | enumeration_flag_opt '|' ctor_def1 '|' ... '|' ctor_defn		:: :: variant
+  | enumeration_flag_opt '|' ctor_def1 '|' ... '|' ctor_defn            :: :: variant
     {{ com Variant types }}
 
 naming_scheme_opt {{ tex \ottnt{name}^{?} }} :: 'Name_sect_' ::=
   {{ com Optional variable-naming-scheme specification for variables of defined type }} 
-  |  	 	       		     	 	      :: :: none
-  | [ name = regexp ]  		     	 	      :: :: name
+  |                                                   :: :: none
+  | [ name = regexp ]                                 :: :: name
 
 type_def :: '' ::=
   {{ com Type definitions }}
-  | type x_l : kind naming_scheme_opt = tdefbody  		        	:: :: Td
-%  | enumeration x_l naming_scheme_opt = tdefbody  		        	::   :: Td2
+  | type id : kind naming_scheme_opt = tdefbody                                :: :: Td
+%  | enumeration id naming_scheme_opt = tdefbody                               ::   :: Td2
 % the enumeration is sugar for something that uses an enum flag, where the type system will restrict the tdefbody to be a simple enum...
 
 
 % TODO: do we need mutually recursive type definitions?  
 
 
+%%% OR, IN C STYLE
+
+c_tdefbody :: 'C_Te_' ::=
+  {{ com Type definition bodies }}
+  | typedef id naming_scheme_opt = typschm                                        :: :: abbrev
+    {{ com Type abbreviations }}
+  | typedef id naming_scheme_opt = struct typquant { typ1 id1 ; ... ; typn idn semi_opt }     :: :: record
+    {{ com Struct type definition }}
+% for specifying constructor result types of nat-indexed GADTs, we can
+%  let the typi be function types (as constructors are not allowed to
+%  take parameters of function types)
+% concrete syntax: to be even closer to C, could have a postfix id rather than prefix id = 
+  | typedef id naming_scheme_opt = union typquant { typ1 id1 ; ... ; typn idn semi_opt }   :: :: variant
+    {{ com Union type definition}}
+
+  | typedef id naming_scheme_opt = enum { id1 ; ... ; idn semi_opt }   :: :: enum
+    {{ com Union type definition}}
+
+
+
+
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % Literals                                                     %
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -454,28 +473,28 @@ grammar
 
 lit :: 'L_' ::=
   {{ com Literal constants }}
-  | true						:: :: true
-  | false						:: :: false
-  | num						:: :: num
-  | hex						:: :: hex
+  | true                                                :: :: true
+  | false                                               :: :: false
+  | num                                         :: :: num
+  | hex                                         :: :: hex
   {{ com hex and bin are constant bit vectors, entered as C-style hex or binaries }}
-  | bin						:: :: bin
-  | string						:: :: string
-  | ( )							:: :: unit
-  | bitzero						:: :: zero
+  | bin                                         :: :: bin
+  | string                                              :: :: string
+  | ( )                                                 :: :: unit
+  | bitzero                                             :: :: zero
   {{ com bitzero and bitone are constant bits, if commonly used we will consider overloading 0 and 1 }}
-  | bitone						:: :: one
+  | bitone                                              :: :: one
 
-semi_opt {{ tex \ottnt{;}^{?} }} :: 'semi_' ::=		{{ phantom }}
-							{{ ocaml terminal * bool }}
-							{{ lem (terminal * bool) }}
-							{{ hol bool }}
+semi_opt {{ tex \ottnt{;}^{?} }} :: 'semi_' ::=         {{ phantom }}
+                                                        {{ ocaml terminal * bool }}
+                                                        {{ lem (terminal * bool) }}
+                                                        {{ hol bool }}
   {{ com Optional semi-colons }}
-  |  							:: :: no
+  |                                                     :: :: no
     {{ hol F }}
     {{ ocaml false }}
     {{ lem false }}
-  | ';'							:: :: yes
+  | ';'                                                 :: :: yes
     {{ hol T }}
     {{ ocaml true }}
     {{ lem true }}
@@ -489,40 +508,46 @@ semi_opt {{ tex \ottnt{;}^{?} }} :: 'semi_' ::=		{{ phantom }}
 pat :: 'P_' ::= 
   {{ com Patterns }}
   {{ aux _ l }}
-  | _							:: :: wild  
+  | _                                                   :: :: wild  
     {{ com Wildcards }}
-  | ( pat as x_l )					:: :: as
+  | ( pat as id )                                      :: :: as
     {{ com Named patterns }}
-  | ( pat : typ )					:: :: typ
+  | ( pat : typ )                                       :: :: typ
     {{ com Typed patterns }}
-  | id pat1 .. patn					:: :: app
+  | id pat1 .. patn                                     :: :: app
     {{ com Single variable and constructor patterns }}
-  | <| fpat1 ; ... ; fpatn semi_opt |>			:: :: record
+% OR?  do we invent something ghastly including a union keyword?  Perhaps not...
+
+  | <| fpat1 ; ... ; fpatn semi_opt |>                  :: :: record
     {{ com Record patterns }}
+% OR
+  | struct { fpat1 ; ... ; fpatn semi_opt }                  :: :: c_record
+    {{ com C-style struct patterns }}
+
 %Patterns for vectors
 
-  | [| pat1 ; .. ; patn semi_opt |]			:: :: vector
+  | [| pat1 ; .. ; patn semi_opt |]                     :: :: vector
    {{ com Vector patterns }}
 
-  | [| pat1 .. patn |]	  	 			:: :: vectorC
+  | [| pat1 .. patn |]                                  :: :: vectorC
   {{ com Concatenated vector patterns }} 
 
-  | ( pat1 , .... , patn )				:: :: tup
+  | ( pat1 , .... , patn )                              :: :: tup
     {{ com Tuple patterns }}
-  | [ pat1 ; .. ; patn semi_opt ]			:: :: list
+  | [ pat1 ; .. ; patn semi_opt ]                       :: :: list
     {{ com List patterns }}
-  | ( pat )						:: :: paren
-  | pat1 '::' pat2					:: :: cons
+  | ( pat )                                             :: :: paren
+  | pat1 '::' pat2                                      :: :: cons
     {{ com Cons patterns }}
-  | x_l '+' num                                         :: :: num_add
+  | id '+' num                                         :: :: num_add
     {{ com constant addition patterns }}
-  | lit							:: :: lit
+  | lit                                                 :: :: lit
     {{ com Literal constant patterns }}
 
 fpat :: 'FP' ::=
   {{ com Field patterns }}
   {{ aux _ l }}
-  | id = pat						:: :: Fpat
+  | id = pat                                            :: :: Fpat
 
 parsing
 P_app <= P_app
@@ -536,16 +561,16 @@ P_app <= P_as
 
 grammar
 
-bar_opt {{ tex \ottkw{|}^{?} }} :: 'bar_' ::=		{{ phantom }}
-							{{ ocaml terminal * bool }}
-							{{ lem (terminal * bool) }}
-							{{ hol bool }}
+bar_opt {{ tex \ottkw{|}^{?} }} :: 'bar_' ::=           {{ phantom }}
+                                                        {{ ocaml terminal * bool }}
+                                                        {{ lem (terminal * bool) }}
+                                                        {{ hol bool }}
   {{ com Optional bars }}
-  |  							:: :: no
+  |                                                     :: :: no
     {{ hol F }}
     {{ ocaml false }}
     {{ lem false }}
-  | '|'							:: :: yes
+  | '|'                                                 :: :: yes
     {{ hol T }}
     {{ ocaml true }}
     {{ lem true }}
@@ -553,30 +578,30 @@ bar_opt {{ tex \ottkw{|}^{?} }} :: 'bar_' ::=		{{ phantom }}
 exp :: 'E_' ::=
   {{ com Expressions }}
   {{ aux _ l }}
-  | id							:: :: Ident
+  | id                                                  :: :: Ident
     {{ com Identifiers }}
-  | N							:: :: Nvar
+  | N                                                   :: :: Nvar
     {{ com nexp var, has type num }}
-  | exp1 exp2						:: :: App
+  | exp1 exp2                                           :: :: App
     {{ com Function applications }}
-  | exp1 ix_l exp2					:: :: Infix
+  | exp1 ix_l exp2                                      :: :: Infix
     {{ com Infix applications }}
-  | <| fexps |>						:: :: Record
+  | <| fexps |>                                         :: :: Record
     {{ com Records }}
-  | <| exp with fexps |>				:: :: Recup
+  | <| exp with fexps |>                                :: :: Recup
     {{ com Functional update for records }}
-  | exp . id						:: :: Field
+  | exp . id                                            :: :: Field
     {{ com Field projection for records }}
 
 %Expressions for creating and accessing vectors
-  | [| exp1 ; ..  ; expn semi_opt |]			:: :: Vector
+  | [| exp1 ; ..  ; expn semi_opt |]                    :: :: Vector
   {{ com Vector instantiation }}
 
-  | exp .( nexp ) 					:: :: VAccess
+  | exp .( nexp )                                       :: :: VAccess
   {{ com Vector access }}
 
 % PS '..' or . . ?
-  | exp .( nexp1 '..' nexp2 )      		:: :: VAccessR
+  | exp .( nexp1 '..' nexp2 )                   :: :: VAccessR
   {{ com Subvector extraction }}
 
 
@@ -591,105 +616,155 @@ exp :: 'E_' ::=
 
   | match exp with bar_opt pexp1 '|' ... '|' pexpn l end :: :: Case
     {{ com Pattern matching expressions }}
-  | ( exp : typ )					:: :: Typed
-    {{ com Type-annotated expressions }}
-  | let letbind in exp					:: :: Let
+%  | ( typ ) exp                                      :: :: Typed
+%    {{ com Type-annotated expressions }}
+  | c_letbind in exp                                  :: :: Let
     {{ com Let expressions }}
-  | ( exp1 , .... , expn )				:: :: Tup
+  | ( exp1 , .... , expn )                              :: :: Tup
     {{ com Tuples }}
-  | [ exp1 ; .. ; expn semi_opt ]			:: :: Elist
+  | [ exp1 ; .. ; expn semi_opt ]                       :: :: Elist
     {{ com Lists }}
-  | ( exp )						:: :: Paren
-  | begin exp end					:: :: Begin
-    {{ com Alternate syntax for $\ottnt(exp)$ }}
-  | if exp1 then exp2 else exp3				:: :: If
+  | ( exp )                                             :: S :: Paren {{ ichlo [[exp]] }}
+%  | begin exp end                                       :: :: Begin
+%    {{ com Alternate syntax for $\ottnt(exp)$ }}
+  | if exp1 then exp2 else exp3                         :: :: If
     {{ com Conditionals }}
-  | exp1 '::' exp2					:: :: Cons
+  | exp1 '::' exp2                                      :: :: Cons
     {{ com Cons expressions }}
-  | lit							:: :: Lit
+  | lit                                                 :: :: Lit
     {{ com Literal constants }}
 
 fexp :: 'FE' ::=
   {{ com Field-expressions }}
   {{ aux _ l }}
-  | id = exp 						:: :: Fexp
+  | id = exp                                            :: :: Fexp
 
 fexps :: 'FES' ::=
   {{ com Field-expression lists }}
   {{ aux _ l }}
-  | fexp1 ; ... ; fexpn semi_opt 			:: :: Fexps
+  | fexp1 ; ... ; fexpn semi_opt                        :: :: Fexps
 
 pexp :: 'Pat' ::=
   {{ com Pattern matches }}
   {{ aux _ l }}
-  | pat -> exp					:: :: exp
-
-psexp :: 'Pats' ::=
-  {{ com Multi-pattern matches }}
-  {{ aux _ l }}
-  | pat1 ... patn -> exp 				:: :: exp
-
-tannot_opt_aux :: 'Typ_annot_' ::=
-  {{ com Optional type annotations }}
-  | 							:: :: none
-  | : typ						:: :: some 
+  | pat -> exp                                  :: :: exp
 
-tannot_opt {{ tex \ottnt{tannot}^? }} :: 'Typ_annot_' ::=
-  {{ com location-annotated optional type annotations }}
-  | tannot_opt_aux l					:: :: aux
+%% % psexp :: 'Pats' ::=
+%% %   {{ com Multi-pattern matches }}
+%% %   {{ aux _ l }}
+%% %   | pat1 ... patn -> exp                                :: :: exp
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% Function definitions                                         %
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-funcl :: 'FCL' ::=
-  {{ com Function clauses }}
-  {{ aux _ l }}
-  | x_l pat1 ... patn tannot_opt = exp			:: :: Funcl
-
-letbind :: 'LB_' ::=
-  {{ com Let bindings }}
-  {{ aux _ l }}
-  | pat tannot_opt = exp 				:: :: Let_val
-    {{ com Value bindings }}
-  | funcl						:: :: Let_fun
-    {{ com Function bindings }}
 
 parsing
 
-P_app right LB_Let_val
+%P_app right LB_Let_val
 
-%P_app <= Fun
+%%P_app <= Fun
 
-%Fun right App
-%Function right App
+%%Fun right App
+%%Function right App
 E_Case right E_App
 E_Let right E_App
 
-%Fun <= Field
-%Function <= Field
+%%Fun <= Field
+%%Function <= Field
 E_App <= E_Field
 E_Case <= E_Field
 E_Let <= E_Field
 
 E_App left E_App
 
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Function definitions                                         %
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%% old Lem style %%%%%%
 grammar
+%% % lem_tannot_opt_aux :: 'LEM_Typ_annot_' ::=
+%% %   {{ com Optional type annotations }}
+%% %   |                                                     :: :: none
+%% %   | : typ                                               :: :: some 
+%% % 
+%% % lem_tannot_opt {{ tex \ottnt{tannot}^? }} :: 'LEM_Typ_annot_' ::=
+%% %   {{ com location-annotated optional type annotations }}
+%% %   | tannot_opt_aux l                                    :: :: aux
+%% % 
+%% % lem_funcl :: 'LEM_FCL' ::=
+%% %   {{ com Function clauses }}
+%% %   {{ aux _ l }}
+%% %   | id pat1 ... patn tannot_opt = exp                   :: :: Funcl
+%% % 
+%% % lem_letbind :: 'LEM_LB_' ::=
+%% %   {{ com Let bindings }}
+%% %   {{ aux _ l }}
+%% %   | pat tannot_opt = exp                                :: :: Let_val
+%% %     {{ com Value bindings }}
+%% %   | lem_funcl                                           :: :: Let_fun
+%% %     {{ com Function bindings }}
+%% % 
+%% % 
+%% % grammar
+%% % lem_val_def :: 'LEM_VD' ::= 
+%% %   {{ com Value definitions }}
+%% %   {{ aux _ l }}
+%% %   | let lem_letbind                                     :: :: Let_def
+%% %     {{ com Non-recursive value definitions }}
+%% %   | let rec  lem_funcl1 and ... and lem_funcln          :: :: Let_rec
+%% %     {{ com Recursive function definitions }}
+%% % 
+%% % lem_val_spec :: 'LEM_VS' ::=
+%% %   {{ com Value type specifications }} 
+%% %   {{ aux _ l }}
+%% %   | val x_l : typschm                                           :: :: Val_spec
+
+%%%%% C-ish style %%%%%%%%%%
+
+c_tannot_opt :: 'C_Typ_annot_' ::=
+  {{ com Optional type annotations }}
+  |                                             :: :: none
+  | typ_quant typ                               :: :: some 
 
+c_funcl :: 'C_FCL' ::=
+  {{ com Function clauses }}
+  {{ aux _ l }}
+  | id pat = exp                   :: :: Funcl
+
+c_rec_opt :: '' ::=
+  {{ aux _ l }}
+  |                                             :: :: nonrec
+  | rec                                         :: :: rec
 
+c_effects_opt :: '' ::=
+  {{ aux _ l }}
+  |                                             :: :: pure {{ com sugar for pure }}
+  | effects                                     :: :: nonpure
 
-val_def :: 'VD' ::= 
-  {{ com Value definitions }}
+c_fundef :: 'C_FD' ::=
+  {{ com Function definition}}
+  {{ aux _ l }}
+  | function c_rec_opt c_tannot_opt c_effects_opt c_funcl1 and ... and c_funcln :: :: function {{ texlong }}  {{ com function definition }}
+% TODO note that the typ in the c_tannot_opt is the *result* type, not
+%  the type of the whole function.  The argument type comes from the
+%  pattern in the c_funcl
+% TODO the above is ok for single functions, but not for mutually
+%  recursive functions - the c_tannot_opt scopes over all the c_funcli,
+%  which is ok for the typ_quant part but not for the typ part
+
+c_letbind :: 'LB_' ::=
+  {{ com Let bindings }}
   {{ aux _ l }}
-  | let letbind					:: :: Let_def
-    {{ com Non-recursive value definitions }}
-  | let rec  funcl1 and ... and funcln		:: :: Let_rec
-    {{ com Recursive function definitions }}
+  | typschm id = exp                                :: :: valexp
+    {{ com Value binding }}
+  | let id = exp                                    :: :: valimp
+    {{ com value binding with implicit type }}
+
 
 val_spec :: 'VS' ::=
   {{ com Value type specifications }} 
   {{ aux _ l }}
-  | val x_l : typschm						:: :: Val_spec
+  | val typschm id                                  :: :: Val_spec
+
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % Top-level definitions                                        %
@@ -698,31 +773,20 @@ val_spec :: 'VS' ::=
 def :: 'DEF' ::=
   {{ com Top-level definitions }}
   {{ aux _ l }}
-  | type_def           	       					:: :: Type_def
+  | type_def                                                    :: :: Type_def
     {{ com Type definitions }}
-  | val_def							:: :: Val_def
+  | c_fundef                                                   :: :: Fun_def
+    {{ com Function definitions }}
+  | c_letbind                                                   :: :: Val_def
     {{ com Value definitions }}
-  | val_spec 							:: :: Spec_def
+  | val_spec                                                    :: :: Spec_def
     {{ com Top-level type constraints }}
 
-semisemi_opt {{ tex \ottkw{;;}^? }} :: 'semisemi_' ::=		{{ phantom }}
-								{{ ocaml terminal * bool }}
-								{{ lem (terminal * bool) }}
-								{{ hol bool }}
-  {{ com Optional double-semi-colon }}
-  | 	 							:: :: no
-    {{ hol F }}
-    {{ ocaml false }}
-    {{ lem false }}
-  | ;;								:: :: yes
-    {{ hol T }}
-    {{ ocaml true }}
-    {{ lem true }}
 
 defs :: '' ::=
   {{ com Definition sequences }}
   {{ aux _ l }}
-  | def1 semisemi_opt1 .. defn semisemi_optn			:: :: Defs
+  | def1  .. defn                  :: :: Defs
 
 
 
@@ -730,618 +794,618 @@ defs :: '' ::=
 % Machinery for typing rules                                   %
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-
-
-grammar
-
-
-p :: 'Path_' ::=
-  {{ com Unique paths }}
-  | x1 . .. xn . x				:: :: def
-  | __list					:: :: list	
-    {{ tex \ottkw{\_\_list}  }}
-  | __bool					:: :: bool
-    {{ tex \ottkw{\_\_bool}  }}
-  | __num					:: :: num
-    {{ tex \ottkw{\_\_num}  }}
-  | __set					:: :: set
-    {{ tex \ottkw{\_\_set}  }}
-  | __string					:: :: string
-    {{ tex \ottkw{\_\_string}  }}
-  | __unit					:: :: unit
-    {{ tex \ottkw{\_\_unit}  }}
-  | __bit					:: :: bit
-    {{ tex \ottkw{\_\_bit}  }}
-  | __vector				:: :: vector
-    {{ tex \ottkw{\_\_vector} }}		
-%TODO morally, delete the above - but what are the __ things for?
-% cleaner to declare early in the library?
-
-t_subst {{ tex \ensuremath{\sigma} }} :: '' ::=	{{ phantom }}
-						{{ hol (a # t) list }}
-						{{ lem list (tnvar * t) }}
-  {{ com Type variable substitutions }}
-  | { tnvar1 |-> t1 .. tnvarn |-> tn }			:: :: T_subst
-    {{ ocaml (assert false) }}
-    {{ lem ([[tnvar1 t1 .. tnvarn tn]]) }}
-    {{ hol ([[tnvar1 t1 .. tnvarn tn]]) }}
-
-t , u :: 'T_' ::=
-  {{ com Internal types }}
-  | a						:: :: var
-  | t1 -> t2					:: :: fn
-  | t1 * .... * tn				:: :: tup
-  | p t_args					:: :: app 
-  | ne						:: :: len
-  | t_subst ( t	)				:: M :: subst_app
-    {{ com Multiple substitutions }}
-    {{ ocaml (assert false) }}
-    {{ hol (t_subst_t [[t_subst]] [[t]]) }}
-    {{ lem (t_subst_t [[t_subst]] [[t]]) }}
-  | t_subst ( tnv )			:: M :: var_subst_app
-    {{ com Single variable substitution }}
-    {{ ocaml (assert false) }}
-    {{ hol (t_subst_tnv [[t_subst]] [[tnv]]) }}
-    {{ lem (t_subst_tnv [[t_subst]] [[tnv]]) }}
-  | curry ( t_multi ,  t )			:: M :: multifn
-    {{ com Curried, multiple argument functions }}
-    {{ ocaml (assert false) }}
-    {{ hol (FOLDR T_fn [[t]] [[t_multi]]) }}
-    {{ lem (List.fold_right T_fn [[t_multi]] [[t]]) }}
-
-ne :: 'Ne_' ::=
-  {{ com internal numeric expressions }}
-  | N						:: :: var
-  | nat					:: :: const
-  | ne1 * ne2				:: :: mult
-  | ne1 + ne2				:: :: add
-  | ( - ne )  				:: :: unary
-  | normalize ( ne ) 			:: M :: normalize
-    {{ ocaml (assert false) }}
-    {{ hol ARB }}
-    {{ lem (normalize [[ne]] ) }}
-  | ne1 + ... + nen			:: M :: addmany
-    {{ ocaml (assert false) }}
-    {{ hol ARB }}
-    {{ lem (sumation_nes [[ne1...nen]]) }}
-  | bitlength ( bin )			:: M :: cbin
-    {{ ocaml (asssert false) }}
-    {{ hol ARB }}
-    {{ lem (blength [[bin]]) }}
-  | bitlength ( hex )			:: M :: chex
-    {{ ocaml (assert false) }}
-    {{ hol ARB }}
-    {{ lem (hlength [[hex]]) }}
-  | length ( pat1 ... patn ) 		:: M :: cpat
-    {{ ocaml (assert false) }}
-    {{ hol ARB }}
-    {{ lem (Ne_const (List.length [[pat1...patn]])) }}
-  | length ( exp1 ... expn )		:: M :: cexp
-    {{ hol ARB }}
-    {{ ocaml (assert false) }}
-    {{ lem (Ne_const (List.length [[exp1...expn]])) }}
-
-t_args :: '' ::=
-  {{ com Lists of types }}
-  | t1 .. tn 				:: :: T_args
-  | t_subst ( t_args )				:: M :: T_args_subst_app
-    {{ com Multiple substitutions }}
-    {{ ocaml (assert false) }}
-    {{ hol (t_subst_t_args [[t_subst]] [[t_args]]) }}
-    {{ lem (t_subst_t_args [[t_subst]] [[t_args]]) }}
-
-t_multi :: '' ::=				{{ phantom }}
-						{{ hol t list }}
-						{{ ocaml t list }}
-						{{ lem list t }}
-  {{ com Lists of types }}
-  | ( t1 * .. * tn )				:: :: T_multi
-    {{ hol [[t1..tn]] }}
-    {{ lem [[t1..tn]] }}
-  | t_subst ( t_multi )				:: M :: T_multi_subst_app
-    {{ com Multiple substitutions }}
-    {{ ocaml (assert false) }}
-    {{ hol (MAP (t_subst_t [[t_subst]]) [[t_multi]]) }}
-    {{ lem (List.map (t_subst_t [[t_subst]]) [[t_multi]]) }}
-
-nec :: '' ::=
-  {{ com Numeric expression constraints }}
-  | ne < nec		:: :: lessthan
-  | ne = nec		:: :: eq
-  | ne <= nec		:: :: lteq
-  | ne				:: :: base
-
-parsing
-T_fn right T_fn
-T_tup <= T_multi
-
-embed
-{{ lem
-
-val t_subst_t : list (tnv * t) -> t -> t 
-val t_subst_tnv : list (tnv * t) -> tnv -> t
-val ftv_t : t -> list tnv
-val ftv_tm : list t -> list tnv
-val ftv_s : list (p*tnv) -> list tnv
-val compatible_overlap : list (x*t) -> bool
-
-(*TODO Should this normalize following the implementation? And blength and hlength need a means of implementation*)
-let normalize n = n
-
-let blength (_,bit) = Ne_const 8
-let hlength (_,bit) = Ne_const 8
-
-let rec sumation_nes nes = match nes with
-  | [ a; b] -> Ne_add a b 
-  | x :: y -> Ne_add x (sumation_nes y)
-end
-
-}}
-
-grammar
-
-
-names :: '' ::=					{{ phantom }}
-						{{ hol x set }}
-						{{ lem set x }}
-						{{ ocaml Set.Make(String).t }}
-  {{ com Sets of names }}
-  | { x1 , .. , xn }				:: :: Names
-    {{ hol (LIST_TO_SET [[x1..xn]]) }}
-    {{ lem (set_from_list [[x1..xn]]) }}
-
-semC {{ tex \ensuremath{\mathcal{C} } }} :: '' ::=
-								{{ hol (p#tnv) list }}
-								{{ lem list (p*tnv)  }}
-%   {{ com Typeclass constraint lists }}
-%   | ( p1 tnv1 ) .. ( pn tnvn )					:: :: SemC_concrete
-%     {{ hol ([[p1 tnv1..pn tnvn]]) }}
-%     {{ lem ([[p1 tnv1..pn tnvn]]) }}
-
-env_tag :: '' ::=
-  {{ com Tags for the (non-constructor) value descriptions }}
-%  | method							:: :: method
-%    {{ com Bound to a method }}
-  | val								:: :: spec
-    {{ com Specified with val }}
-  | let								:: :: def
-    {{ com Defined with let or indreln }}
-
-v_desc :: 'V_' ::=
-  {{ com Value descriptions }}
-  | < forall tnvs . t_multi -> p , ( x of names ) >		:: :: constr
-    {{ com Constructors }}
-  | < forall tnvs . semC => t , env_tag >			:: :: val
-    {{ com Values }}
-
-f_desc :: 'F_' ::=
-  | < forall tnvs . p -> t , ( x of names ) >			:: :: field
-    {{ com Fields }}
-
-embed
-{{ hol
-load "fmaptreeTheory";
-val _ = 
-  Hol_datatype 
-    `env_body = <| env_p : x|->p; env_f : x|->f_desc; env_v : x|->v_desc |>`;
-
-val _ = Define `
-  env_union e1 e2 =
-    let i1 = item e1 in
-    let m1 = map e1 in
-    let i2 = item e2 in
-    let m2 = map e2 in
-      FTNode <| env_p:=FUNION i1.env_p i2.env_p; 
-                env_f:=FUNION i1.env_f i2.env_f;
-                env_v:=FUNION i1.env_v i2.env_v |>
-             (FUNION m1 m2)`;
-}}
-{{ lem
-type env =
-  | EnvEmp 
-  | Env of (map x env) * (map x p) * (map x f_desc) * (map x v_desc)
-
-val env_union : env -> env -> env
-let env_union e1 e2 =
-  match (e1,e2) with
-   | (EnvEmp,e2) -> e2
-   | (e1,EnvEmp) -> e1
-   | ((Env Em1 Ep1 Ef1 Ev1),(Env Em2 Ep2 Ef2 Ev2)) ->
-     Env(union_map Em1 Em2) (union_map Ep1 Ep2) (union_map Ef1 Ef2) (union_map Ev1 Ev2)
-end
-
-}}
-
-grammar
-
-xs :: '' ::=					{{ phantom }}
-						{{ hol string list }}
-						{{ lem list string }}
-  | x1 .. xn					:: :: Xs
-    {{ hol [[x1..xn]] }}
-    {{ lem [[x1..xn]] }}
-
-%TODO: no clue what the following are:
-S_c {{ tex {\ensuremath{ {\Sigma}^{\mathcal{C} } } } }} :: '' ::=			{{ phantom }}
-								{{ hol (p#t) list }}
-								{{ lem list (p*t) }}
-  {{ com Typeclass constraints }}
-  | { ( p1 t1 ) , .. , ( pn tn ) }				:: :: S_concrete
-    {{ hol [[p1 t1 .. pn tn]] }}
-    {{ lem [[p1 t1 .. pn tn]] }}
-  | S_c1 union .. union S_cn					:: M :: S_union
-    {{ hol (FLAT [[S_c1..S_cn]]) }}
-    {{ lem (List.flatten [[S_c1..S_cn]]) }}
-    {{ ocaml assert false }}
-
-S_N {{ tex { \ensuremath{ {\Sigma}^{\mathcal{N} } } } }} :: '' ::= {{ phantom }}
-                                                                   {{ hol nec list }}
-                                                                   {{ lem list nec }}
-   {{ com nexp constraint lists }}
-   | { nec1 , .. ,  necn }				:: :: Sn_concrete
-     {{ hol [[nec1 .. necn]] }}
-     {{ lem [[nec1 .. necn]] }}
-   | S_N1 union .. union S_Nn			:: M :: SN_union
-     {{ hol (FLAT [[S_N1..S_Nn]]) }}
-     {{ lem (List.flatten [[S_N1..S_Nn]]) }}
-     {{ ocaml assert false }}
-
-
-E :: '' ::=							{{ phantom }}
-								{{ hol ((string,env_body) fmaptree) }}
-
-
-%TODO: simplify by removing E_m throughout?  And E_p??
-								{{ lem env }}
-  {{ com Environments }}
-  | < E_m , E_p , E_f , E_x >						:: :: E
-    {{ hol (FTNode <|env_p:=[[E_p]]; env_f:=[[E_f]]; env_v:=[[E_x]]|> ([[E_m]])) }}
-    {{ lem (Env [[E_m]] [[E_p]] [[E_f]] [[E_x]]) }}
-  | E1 u+ E2							:: M :: E_union
-    {{ hol (env_union [[E1]] [[E2]]) }}
-    {{ lem (env_union [[E1]] [[E2]]) }}
-    {{ ocaml assert false }}
-  | empty							:: M :: E_empty
-    {{ hol (FTNode <|env_p:=FEMPTY; env_f:=FEMPTY; env_v:=FEMPTY|> FEMPTY) }}
-    {{ lem EnvEmp }}
-    {{ ocaml assert false }}
-
-E_x {{ tex \ottnt{E}^{\textsc{x} } }} :: 'E_x_' ::=		{{ phantom }}
-								{{ hol (x|-> v_desc) }}
-								{{ lem map x v_desc }}
-  {{ com Value environments }}
-  | { x1 |-> v_desc1 , .. , xn |-> v_descn }	:: :: concrete
-    {{ hol (FOLDR (\(k1,k2) E. E |+ (k1,k2)) FEMPTY [[x1 v_desc1 .. xn v_descn]]) }}
-    {{ lem (List.fold_right (fun (x,v) m -> Pmap.add x v m) [[x1 v_desc1 .. xn v_descn]] Pmap.empty) }} 
-  | E_x1 u+ .. u+ E_xn						:: M :: union
-    {{ hol (FOLDR FUNION FEMPTY [[E_x1..E_xn]]) }}
-    {{ lem (List.fold_right union_map [[E_x1..E_xn]] Pmap.empty) }}
-    {{ ocaml (assert false) }}
-
-E_f {{ tex \ottnt{E}^{\textsc{f} } }} :: 'E_f_' ::=		{{ phantom }}
-								{{ hol (x |-> f_desc) }}
-								{{ lem map x f_desc }}
-  {{ com Field environments }}
-  | { x1 |-> f_desc1 , .. , xn |-> f_descn }			:: :: concrete
-    {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[x1 f_desc1 .. xn f_descn]]) }}
-    {{ lem (List.fold_right (fun (x,f) m -> Pmap.add x f m) [[x1 f_desc1 .. xn f_descn]] Pmap.empty) }} 
-  | E_f1 u+ .. u+ E_fn						:: M :: union
-    {{ hol (FOLDR FUNION FEMPTY [[E_f1..E_fn]]) }}
-    {{ lem (List.fold_right union_map [[E_f1..E_fn]] Pmap.empty) }}
-    {{ ocaml (assert false) }}
-
-E_m {{ tex \ottnt{E}^{\textsc{m} } }} :: 'E_m_' ::=		{{ phantom }}
-								{{ hol (string |-> (string,env_body) fmaptree) }}
-								{{ lem map x env }} 
-%  {{ com Module environments }}
-%  | { x1 |-> E1 , .. , xn |-> En }				:: :: concrete
-%    {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[x1 E1 .. xn En]]) }}
-%    {{ lem (List.fold_right (fun (x,e) m -> Pmap.add x e m) [[x1 E1 .. xn En]] Pmap.empty) }} 
-% 
-% _p {{ tex \ottnt{E}^{\textsc{p} } }} :: 'E_p_' ::=		{{ phantom }}
-%        							{{ hol (x |-> p) }}
-%        							{{ lem map x p }}
-%  {{ com Path environments }}
-%  | { x1 |-> p1 , .. , xn |-> pn }				:: :: concrete
-%    {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[x1 p1 .. xn pn]]) }}
-%    {{ lem (List.fold_right (fun (x,p) m -> Pmap.add x p m) [[x1 p1 .. xn pn]] Pmap.empty) }} 
-%  | E_p1 u+ .. u+ E_pn						:: M :: union
-%    {{ hol (FOLDR FUNION FEMPTY [[E_p1..E_pn]]) }}
-%    {{ lem (List.fold_right union_map [[E_p1..E_pn]] Pmap.empty) }}
-% 
-%    {{ ocaml (assert false) }}
- E_l {{ tex \ottnt{E}^{\textsc{l} } }} :: 'E_l_' ::=		{{ phantom }}
-								{{ hol (x |-> t) }}
-								{{ lem map x t }}
-  {{ com Lexical bindings }}
-  | { x1 |-> t1 , .. , xn |-> tn }				:: :: concrete
-    {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[x1 t1 .. xn tn]]) }}
-    {{ lem (List.fold_right (fun (x,t) m -> Pmap.add x t m) [[x1 t1 .. xn tn]] Pmap.empty) }} 
-  | E_l1 u+ .. u+ E_ln						:: M :: union
-    {{ hol (FOLDR FUNION FEMPTY [[E_l1..E_ln]]) }}
-    {{ lem (List.fold_right union_map [[E_l1..E_ln]] Pmap.empty) }}
-   {{ ocaml (assert false) }}
-
-tc_abbrev :: 'Tc_abbrev_' ::=					{{ phantom }}
-								{{ hol t option }}
-								{{ lem option t }}
-								{{ ocaml t option }}
-  {{ com Type abbreviations }}
-  | . t								:: :: some
-    {{ hol (SOME [[t]]) }}
-    {{ lem (Some [[t]]) }}
-  | 								:: :: none
-    {{ hol NONE }}
-    {{ lem None }}
-
-tc_def :: '' ::=
-  {{ com Type and class constructor definitions }} 
-  | tnvs tc_abbrev						:: :: Tc_def
-    {{ com Type constructors }}
-
-TD {{ tex \ensuremath{\Delta} }} :: 'TD_' ::=			{{ phantom }}
-								{{ hol p |-> tc_def }}
-								{{ lem map p tc_def }}
-  {{ com Type constructor definitions }}
-  | { p1 |-> tc_def1 , .. , pn |-> tc_defn }			:: :: concrete
-    {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[p1 tc_def1 .. pn tc_defn]]) }}
-    {{ lem (List.fold_right (fun (p,t) m -> Pmap.add p t m) [[p1 tc_def1 .. pn tc_defn]] Pmap.empty) }} 
-    {{ ocaml (assert false) }}
-  | TD1 u+ TD2							:: M :: union
-    {{ hol (FUNION [[TD1]] [[TD2]]) }}
-    {{ lem (union_map [[TD1]] [[TD2]]) }}
-    {{ ocaml (assert false) }}
-
-
-
-D :: 'D_' ::=							{{ phantom }}
-								{{ hol ((p |-> tc_def) # (p |-> x list) # (inst list)) }}
-                                                                {{ lem tdefs}}
-  {{ com Global type definition store }}
-  | < TD , TC , I >							:: :: concrete
-    {{ hol ([[TD]], [[TC]], [[I]]) }}
-    {{ lem (D [[TD]] [[TC]] [[I]]) }}
-  | D1 u+ D2							:: M :: union
-    {{ hol (case ([[D1]],[[D2]]) of ((x1,x2,x3),(y1,y2,y3)) => (FUNION x1 y1, FUNION x2 y2, x3 ++ y3)) }}
-    {{ lem (union_tcdefs [[D1]] [[D2]]) }}
-    {{ ocaml (assert false) }}
-  | empty							:: M :: empty
-    {{ hol (FEMPTY, FEMPTY, []) }}
-    {{ lem DEmp }}
-    {{ ocaml assert false }}
-
-parsing
-E_union left E_union
-
-embed
-{{ lem
-type tdefs =
-  | DEmp
-  | D of (map p tc_def) * (map p (list x)) * (set inst)
-
-val union_tcdefs : tdefs -> tdefs -> tdefs
-
-}}
+%% %% 
+%% %% 
+%% %% grammar
+%% %% 
+%% %% 
+%% %% p :: 'Path_' ::=
+%% %%   {{ com Unique paths }}
+%% %%   | x1 . .. xn . x                              :: :: def
+%% %%   | __list                                      :: :: list      
+%% %%     {{ tex \ottkw{\_\_list}  }}
+%% %%   | __bool                                      :: :: bool
+%% %%     {{ tex \ottkw{\_\_bool}  }}
+%% %%   | __num                                       :: :: num
+%% %%     {{ tex \ottkw{\_\_num}  }}
+%% %%   | __set                                       :: :: set
+%% %%     {{ tex \ottkw{\_\_set}  }}
+%% %%   | __string                                    :: :: string
+%% %%     {{ tex \ottkw{\_\_string}  }}
+%% %%   | __unit                                      :: :: unit
+%% %%     {{ tex \ottkw{\_\_unit}  }}
+%% %%   | __bit                                       :: :: bit
+%% %%     {{ tex \ottkw{\_\_bit}  }}
+%% %%   | __vector                            :: :: vector
+%% %%     {{ tex \ottkw{\_\_vector} }}                
+%% %% %TODO morally, delete the above - but what are the __ things for?
+%% %% % cleaner to declare early in the library?
+%% %% 
+%% %% t_subst {{ tex \ensuremath{\sigma} }} :: '' ::= {{ phantom }}
+%% %%                                                 {{ hol (a # t) list }}
+%% %%                                                 {{ lem list (tnvar * t) }}
+%% %%   {{ com Type variable substitutions }}
+%% %%   | { tnvar1 |-> t1 .. tnvarn |-> tn }                  :: :: T_subst
+%% %%     {{ ocaml (assert false) }}
+%% %%     {{ lem ([[tnvar1 t1 .. tnvarn tn]]) }}
+%% %%     {{ hol ([[tnvar1 t1 .. tnvarn tn]]) }}
+%% %% 
+%% %% t , u :: 'T_' ::=
+%% %%   {{ com Internal types }}
+%% %%   | a                                           :: :: var
+%% %%   | t1 -> t2                                    :: :: fn
+%% %%   | t1 * .... * tn                              :: :: tup
+%% %%   | p t_args                                    :: :: app 
+%% %%   | ne                                          :: :: len
+%% %%   | t_subst ( t )                               :: M :: subst_app
+%% %%     {{ com Multiple substitutions }}
+%% %%     {{ ocaml (assert false) }}
+%% %%     {{ hol (t_subst_t [[t_subst]] [[t]]) }}
+%% %%     {{ lem (t_subst_t [[t_subst]] [[t]]) }}
+%% %%   | t_subst ( tnv )                     :: M :: var_subst_app
+%% %%     {{ com Single variable substitution }}
+%% %%     {{ ocaml (assert false) }}
+%% %%     {{ hol (t_subst_tnv [[t_subst]] [[tnv]]) }}
+%% %%     {{ lem (t_subst_tnv [[t_subst]] [[tnv]]) }}
+%% %%   | curry ( t_multi ,  t )                      :: M :: multifn
+%% %%     {{ com Curried, multiple argument functions }}
+%% %%     {{ ocaml (assert false) }}
+%% %%     {{ hol (FOLDR T_fn [[t]] [[t_multi]]) }}
+%% %%     {{ lem (List.fold_right T_fn [[t_multi]] [[t]]) }}
+%% %% 
+%% %% ne :: 'Ne_' ::=
+%% %%   {{ com internal numeric expressions }}
+%% %%   | N                                           :: :: var
+%% %%   | nat                                 :: :: const
+%% %%   | ne1 * ne2                           :: :: mult
+%% %%   | ne1 + ne2                           :: :: add
+%% %%   | ( - ne )                            :: :: unary
+%% %%   | normalize ( ne )                    :: M :: normalize
+%% %%     {{ ocaml (assert false) }}
+%% %%     {{ hol ARB }}
+%% %%     {{ lem (normalize [[ne]] ) }}
+%% %%   | ne1 + ... + nen                     :: M :: addmany
+%% %%     {{ ocaml (assert false) }}
+%% %%     {{ hol ARB }}
+%% %%     {{ lem (sumation_nes [[ne1...nen]]) }}
+%% %%   | bitlength ( bin )                   :: M :: cbin
+%% %%     {{ ocaml (asssert false) }}
+%% %%     {{ hol ARB }}
+%% %%     {{ lem (blength [[bin]]) }}
+%% %%   | bitlength ( hex )                   :: M :: chex
+%% %%     {{ ocaml (assert false) }}
+%% %%     {{ hol ARB }}
+%% %%     {{ lem (hlength [[hex]]) }}
+%% %%   | length ( pat1 ... patn )            :: M :: cpat
+%% %%     {{ ocaml (assert false) }}
+%% %%     {{ hol ARB }}
+%% %%     {{ lem (Ne_const (List.length [[pat1...patn]])) }}
+%% %%   | length ( exp1 ... expn )            :: M :: cexp
+%% %%     {{ hol ARB }}
+%% %%     {{ ocaml (assert false) }}
+%% %%     {{ lem (Ne_const (List.length [[exp1...expn]])) }}
+%% %% 
+%% %% t_args :: '' ::=
+%% %%   {{ com Lists of types }}
+%% %%   | t1 .. tn                            :: :: T_args
+%% %%   | t_subst ( t_args )                          :: M :: T_args_subst_app
+%% %%     {{ com Multiple substitutions }}
+%% %%     {{ ocaml (assert false) }}
+%% %%     {{ hol (t_subst_t_args [[t_subst]] [[t_args]]) }}
+%% %%     {{ lem (t_subst_t_args [[t_subst]] [[t_args]]) }}
+%% %% 
+%% %% t_multi :: '' ::=                               {{ phantom }}
+%% %%                                                 {{ hol t list }}
+%% %%                                                 {{ ocaml t list }}
+%% %%                                                 {{ lem list t }}
+%% %%   {{ com Lists of types }}
+%% %%   | ( t1 * .. * tn )                            :: :: T_multi
+%% %%     {{ hol [[t1..tn]] }}
+%% %%     {{ lem [[t1..tn]] }}
+%% %%   | t_subst ( t_multi )                         :: M :: T_multi_subst_app
+%% %%     {{ com Multiple substitutions }}
+%% %%     {{ ocaml (assert false) }}
+%% %%     {{ hol (MAP (t_subst_t [[t_subst]]) [[t_multi]]) }}
+%% %%     {{ lem (List.map (t_subst_t [[t_subst]]) [[t_multi]]) }}
+%% %% 
+%% %% nec :: '' ::=
+%% %%   {{ com Numeric expression constraints }}
+%% %%   | ne < nec            :: :: lessthan
+%% %%   | ne = nec            :: :: eq
+%% %%   | ne <= nec           :: :: lteq
+%% %%   | ne                          :: :: base
+%% %% 
+%% %% parsing
+%% %% T_fn right T_fn
+%% %% T_tup <= T_multi
+%% %% 
+%% %% embed
+%% %% {{ lem
+%% %% 
+%% %% val t_subst_t : list (tnv * t) -> t -> t 
+%% %% val t_subst_tnv : list (tnv * t) -> tnv -> t
+%% %% val ftv_t : t -> list tnv
+%% %% val ftv_tm : list t -> list tnv
+%% %% val ftv_s : list (p*tnv) -> list tnv
+%% %% val compatible_overlap : list (x*t) -> bool
+%% %% 
+%% %% (*TODO Should this normalize following the implementation? And blength and hlength need a means of implementation*)
+%% %% let normalize n = n
+%% %% 
+%% %% let blength (_,bit) = Ne_const 8
+%% %% let hlength (_,bit) = Ne_const 8
+%% %% 
+%% %% let rec sumation_nes nes = match nes with
+%% %%   | [ a; b] -> Ne_add a b 
+%% %%   | x :: y -> Ne_add x (sumation_nes y)
+%% %% end
+%% %% 
+%% %% }}
+%% %% 
+%% %% grammar
+%% %% 
+%% %% 
+%% %% names :: '' ::=                                 {{ phantom }}
+%% %%                                                 {{ hol x set }}
+%% %%                                                 {{ lem set x }}
+%% %%                                                 {{ ocaml Set.Make(String).t }}
+%% %%   {{ com Sets of names }}
+%% %%   | { x1 , .. , xn }                            :: :: Names
+%% %%     {{ hol (LIST_TO_SET [[x1..xn]]) }}
+%% %%     {{ lem (set_from_list [[x1..xn]]) }}
+%% %% 
+%% %% semC {{ tex \ensuremath{\mathcal{C} } }} :: '' ::=
+%% %%                                                                 {{ hol (p#tnv) list }}
+%% %%                                                                 {{ lem list (p*tnv)  }}
+%% %% %   {{ com Typeclass constraint lists }}
+%% %% %   | ( p1 tnv1 ) .. ( pn tnvn )                                        :: :: SemC_concrete
+%% %% %     {{ hol ([[p1 tnv1..pn tnvn]]) }}
+%% %% %     {{ lem ([[p1 tnv1..pn tnvn]]) }}
+%% %% 
+%% %% env_tag :: '' ::=
+%% %%   {{ com Tags for the (non-constructor) value descriptions }}
+%% %% %  | method                                                     :: :: method
+%% %% %    {{ com Bound to a method }}
+%% %%   | val                                                         :: :: spec
+%% %%     {{ com Specified with val }}
+%% %%   | let                                                         :: :: def
+%% %%     {{ com Defined with let or indreln }}
+%% %% 
+%% %% v_desc :: 'V_' ::=
+%% %%   {{ com Value descriptions }}
+%% %%   | < forall tnvs . t_multi -> p , ( x of names ) >             :: :: constr
+%% %%     {{ com Constructors }}
+%% %%   | < forall tnvs . semC => t , env_tag >                       :: :: val
+%% %%     {{ com Values }}
+%% %% 
+%% %% f_desc :: 'F_' ::=
+%% %%   | < forall tnvs . p -> t , ( x of names ) >                   :: :: field
+%% %%     {{ com Fields }}
+%% %% 
+%% %% embed
+%% %% {{ hol
+%% %% load "fmaptreeTheory";
+%% %% val _ = 
+%% %%   Hol_datatype 
+%% %%     `env_body = <| env_p : x|->p; env_f : x|->f_desc; env_v : x|->v_desc |>`;
+%% %% 
+%% %% val _ = Define `
+%% %%   env_union e1 e2 =
+%% %%     let i1 = item e1 in
+%% %%     let m1 = map e1 in
+%% %%     let i2 = item e2 in
+%% %%     let m2 = map e2 in
+%% %%       FTNode <| env_p:=FUNION i1.env_p i2.env_p; 
+%% %%                 env_f:=FUNION i1.env_f i2.env_f;
+%% %%                 env_v:=FUNION i1.env_v i2.env_v |>
+%% %%              (FUNION m1 m2)`;
+%% %% }}
+%% %% {{ lem
+%% %% type env =
+%% %%   | EnvEmp 
+%% %%   | Env of (map x env) * (map x p) * (map x f_desc) * (map x v_desc)
+%% %% 
+%% %% val env_union : env -> env -> env
+%% %% let env_union e1 e2 =
+%% %%   match (e1,e2) with
+%% %%    | (EnvEmp,e2) -> e2
+%% %%    | (e1,EnvEmp) -> e1
+%% %%    | ((Env Em1 Ep1 Ef1 Ev1),(Env Em2 Ep2 Ef2 Ev2)) ->
+%% %%      Env(union_map Em1 Em2) (union_map Ep1 Ep2) (union_map Ef1 Ef2) (union_map Ev1 Ev2)
+%% %% end
+%% %% 
+%% %% }}
+%% %% 
+%% %% grammar
+%% %% 
+%% %% xs :: '' ::=                                    {{ phantom }}
+%% %%                                                 {{ hol string list }}
+%% %%                                                 {{ lem list string }}
+%% %%   | x1 .. xn                                    :: :: Xs
+%% %%     {{ hol [[x1..xn]] }}
+%% %%     {{ lem [[x1..xn]] }}
+%% %% 
+%% %% %TODO: no clue what the following are:
+%% %% S_c {{ tex {\ensuremath{ {\Sigma}^{\mathcal{C} } } } }} :: '' ::=                       {{ phantom }}
+%% %%                                                                 {{ hol (p#t) list }}
+%% %%                                                                 {{ lem list (p*t) }}
+%% %%   {{ com Typeclass constraints }}
+%% %%   | { ( p1 t1 ) , .. , ( pn tn ) }                              :: :: S_concrete
+%% %%     {{ hol [[p1 t1 .. pn tn]] }}
+%% %%     {{ lem [[p1 t1 .. pn tn]] }}
+%% %%   | S_c1 union .. union S_cn                                    :: M :: S_union
+%% %%     {{ hol (FLAT [[S_c1..S_cn]]) }}
+%% %%     {{ lem (List.flatten [[S_c1..S_cn]]) }}
+%% %%     {{ ocaml assert false }}
+%% %% 
+%% %% S_N {{ tex { \ensuremath{ {\Sigma}^{\mathcal{N} } } } }} :: '' ::= {{ phantom }}
+%% %%                                                                    {{ hol nec list }}
+%% %%                                                                    {{ lem list nec }}
+%% %%    {{ com nexp constraint lists }}
+%% %%    | { nec1 , .. ,  necn }                              :: :: Sn_concrete
+%% %%      {{ hol [[nec1 .. necn]] }}
+%% %%      {{ lem [[nec1 .. necn]] }}
+%% %%    | S_N1 union .. union S_Nn                   :: M :: SN_union
+%% %%      {{ hol (FLAT [[S_N1..S_Nn]]) }}
+%% %%      {{ lem (List.flatten [[S_N1..S_Nn]]) }}
+%% %%      {{ ocaml assert false }}
+%% %% 
+%% %% 
+%% %% E :: '' ::=                                                     {{ phantom }}
+%% %%                                                                 {{ hol ((string,env_body) fmaptree) }}
+%% %% 
+%% %% 
+%% %% %TODO: simplify by removing E_m throughout?  And E_p??
+%% %%                                                                 {{ lem env }}
+%% %%   {{ com Environments }}
+%% %%   | < E_m , E_p , E_f , E_x >                                           :: :: E
+%% %%     {{ hol (FTNode <|env_p:=[[E_p]]; env_f:=[[E_f]]; env_v:=[[E_x]]|> ([[E_m]])) }}
+%% %%     {{ lem (Env [[E_m]] [[E_p]] [[E_f]] [[E_x]]) }}
+%% %%   | E1 u+ E2                                                    :: M :: E_union
+%% %%     {{ hol (env_union [[E1]] [[E2]]) }}
+%% %%     {{ lem (env_union [[E1]] [[E2]]) }}
+%% %%     {{ ocaml assert false }}
+%% %%   | empty                                                       :: M :: E_empty
+%% %%     {{ hol (FTNode <|env_p:=FEMPTY; env_f:=FEMPTY; env_v:=FEMPTY|> FEMPTY) }}
+%% %%     {{ lem EnvEmp }}
+%% %%     {{ ocaml assert false }}
+%% %% 
+%% %% E_x {{ tex \ottnt{E}^{\textsc{x} } }} :: 'E_x_' ::=             {{ phantom }}
+%% %%                                                                 {{ hol (x|-> v_desc) }}
+%% %%                                                                 {{ lem map x v_desc }}
+%% %%   {{ com Value environments }}
+%% %%   | { x1 |-> v_desc1 , .. , xn |-> v_descn }    :: :: concrete
+%% %%     {{ hol (FOLDR (\(k1,k2) E. E |+ (k1,k2)) FEMPTY [[x1 v_desc1 .. xn v_descn]]) }}
+%% %%     {{ lem (List.fold_right (fun (x,v) m -> Pmap.add x v m) [[x1 v_desc1 .. xn v_descn]] Pmap.empty) }} 
+%% %%   | E_x1 u+ .. u+ E_xn                                          :: M :: union
+%% %%     {{ hol (FOLDR FUNION FEMPTY [[E_x1..E_xn]]) }}
+%% %%     {{ lem (List.fold_right union_map [[E_x1..E_xn]] Pmap.empty) }}
+%% %%     {{ ocaml (assert false) }}
+%% %% 
+%% %% E_f {{ tex \ottnt{E}^{\textsc{f} } }} :: 'E_f_' ::=             {{ phantom }}
+%% %%                                                                 {{ hol (x |-> f_desc) }}
+%% %%                                                                 {{ lem map x f_desc }}
+%% %%   {{ com Field environments }}
+%% %%   | { x1 |-> f_desc1 , .. , xn |-> f_descn }                    :: :: concrete
+%% %%     {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[x1 f_desc1 .. xn f_descn]]) }}
+%% %%     {{ lem (List.fold_right (fun (x,f) m -> Pmap.add x f m) [[x1 f_desc1 .. xn f_descn]] Pmap.empty) }} 
+%% %%   | E_f1 u+ .. u+ E_fn                                          :: M :: union
+%% %%     {{ hol (FOLDR FUNION FEMPTY [[E_f1..E_fn]]) }}
+%% %%     {{ lem (List.fold_right union_map [[E_f1..E_fn]] Pmap.empty) }}
+%% %%     {{ ocaml (assert false) }}
+%% %% 
+%% %% E_m {{ tex \ottnt{E}^{\textsc{m} } }} :: 'E_m_' ::=             {{ phantom }}
+%% %%                                                                 {{ hol (string |-> (string,env_body) fmaptree) }}
+%% %%                                                                 {{ lem map x env }} 
+%% %% %  {{ com Module environments }}
+%% %% %  | { x1 |-> E1 , .. , xn |-> En }                             :: :: concrete
+%% %% %    {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[x1 E1 .. xn En]]) }}
+%% %% %    {{ lem (List.fold_right (fun (x,e) m -> Pmap.add x e m) [[x1 E1 .. xn En]] Pmap.empty) }} 
+%% %% % 
+%% %% % _p {{ tex \ottnt{E}^{\textsc{p} } }} :: 'E_p_' ::=            {{ phantom }}
+%% %% %                                                               {{ hol (x |-> p) }}
+%% %% %                                                               {{ lem map x p }}
+%% %% %  {{ com Path environments }}
+%% %% %  | { x1 |-> p1 , .. , xn |-> pn }                             :: :: concrete
+%% %% %    {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[x1 p1 .. xn pn]]) }}
+%% %% %    {{ lem (List.fold_right (fun (x,p) m -> Pmap.add x p m) [[x1 p1 .. xn pn]] Pmap.empty) }} 
+%% %% %  | E_p1 u+ .. u+ E_pn                                         :: M :: union
+%% %% %    {{ hol (FOLDR FUNION FEMPTY [[E_p1..E_pn]]) }}
+%% %% %    {{ lem (List.fold_right union_map [[E_p1..E_pn]] Pmap.empty) }}
+%% %% % 
+%% %% %    {{ ocaml (assert false) }}
+%% %%  E_l {{ tex \ottnt{E}^{\textsc{l} } }} :: 'E_l_' ::=            {{ phantom }}
+%% %%                                                                 {{ hol (x |-> t) }}
+%% %%                                                                 {{ lem map x t }}
+%% %%   {{ com Lexical bindings }}
+%% %%   | { x1 |-> t1 , .. , xn |-> tn }                              :: :: concrete
+%% %%     {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[x1 t1 .. xn tn]]) }}
+%% %%     {{ lem (List.fold_right (fun (x,t) m -> Pmap.add x t m) [[x1 t1 .. xn tn]] Pmap.empty) }} 
+%% %%   | E_l1 u+ .. u+ E_ln                                          :: M :: union
+%% %%     {{ hol (FOLDR FUNION FEMPTY [[E_l1..E_ln]]) }}
+%% %%     {{ lem (List.fold_right union_map [[E_l1..E_ln]] Pmap.empty) }}
+%% %%    {{ ocaml (assert false) }}
+%% %% 
+%% %% tc_abbrev :: 'Tc_abbrev_' ::=                                   {{ phantom }}
+%% %%                                                                 {{ hol t option }}
+%% %%                                                                 {{ lem option t }}
+%% %%                                                                 {{ ocaml t option }}
+%% %%   {{ com Type abbreviations }}
+%% %%   | . t                                                         :: :: some
+%% %%     {{ hol (SOME [[t]]) }}
+%% %%     {{ lem (Some [[t]]) }}
+%% %%   |                                                             :: :: none
+%% %%     {{ hol NONE }}
+%% %%     {{ lem None }}
+%% %% 
+%% %% tc_def :: '' ::=
+%% %%   {{ com Type and class constructor definitions }} 
+%% %%   | tnvs tc_abbrev                                              :: :: Tc_def
+%% %%     {{ com Type constructors }}
+%% %% 
+%% %% TD {{ tex \ensuremath{\Delta} }} :: 'TD_' ::=                   {{ phantom }}
+%% %%                                                                 {{ hol p |-> tc_def }}
+%% %%                                                                 {{ lem map p tc_def }}
+%% %%   {{ com Type constructor definitions }}
+%% %%   | { p1 |-> tc_def1 , .. , pn |-> tc_defn }                    :: :: concrete
+%% %%     {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[p1 tc_def1 .. pn tc_defn]]) }}
+%% %%     {{ lem (List.fold_right (fun (p,t) m -> Pmap.add p t m) [[p1 tc_def1 .. pn tc_defn]] Pmap.empty) }} 
+%% %%     {{ ocaml (assert false) }}
+%% %%   | TD1 u+ TD2                                                  :: M :: union
+%% %%     {{ hol (FUNION [[TD1]] [[TD2]]) }}
+%% %%     {{ lem (union_map [[TD1]] [[TD2]]) }}
+%% %%     {{ ocaml (assert false) }}
+%% %% 
+%% %% 
+%% %% 
+%% %% D :: 'D_' ::=                                                   {{ phantom }}
+%% %%                                                                 {{ hol ((p |-> tc_def) # (p |-> x list) # (inst list)) }}
+%% %%                                                                 {{ lem tdefs}}
+%% %%   {{ com Global type definition store }}
+%% %%   | < TD , TC , I >                                                     :: :: concrete
+%% %%     {{ hol ([[TD]], [[TC]], [[I]]) }}
+%% %%     {{ lem (D [[TD]] [[TC]] [[I]]) }}
+%% %%   | D1 u+ D2                                                    :: M :: union
+%% %%     {{ hol (case ([[D1]],[[D2]]) of ((x1,x2,x3),(y1,y2,y3)) => (FUNION x1 y1, FUNION x2 y2, x3 ++ y3)) }}
+%% %%     {{ lem (union_tcdefs [[D1]] [[D2]]) }}
+%% %%     {{ ocaml (assert false) }}
+%% %%   | empty                                                       :: M :: empty
+%% %%     {{ hol (FEMPTY, FEMPTY, []) }}
+%% %%     {{ lem DEmp }}
+%% %%     {{ ocaml assert false }}
+%% %% 
+%% %% parsing
+%% %% E_union left E_union
+%% %% 
+%% %% embed
+%% %% {{ lem
+%% %% type tdefs =
+%% %%   | DEmp
+%% %%   | D of (map p tc_def) * (map p (list x)) * (set inst)
+%% %% 
+%% %% val union_tcdefs : tdefs -> tdefs -> tdefs
+%% %% 
+%% %% }}
 
 grammar
 
 terminals :: '' ::=
-  | >=					:: :: geq
+  | >=                                  :: :: geq
     {{ tex \ensuremath{\geq} }}
     {{ com \texttt{>=} }}
-  | '<='					:: :: leq
+  | '<='                                        :: :: leq
     {{ tex \ensuremath{\leq} }}
     {{ com \texttt{<=} }}
-  | ->					:: :: arrow
+  | ->                                  :: :: arrow
     {{ tex \ensuremath{\rightarrow} }}
     {{ com \texttt{->} }}
-  | ==> 				:: :: Longrightarrow
+  | ==>                                 :: :: Longrightarrow
     {{ tex \ensuremath{\Longrightarrow} }}
     {{ com \texttt{==>} }}
-  | <|					:: :: startrec
+  | <|                                  :: :: startrec
     {{ tex \ensuremath{\langle|} }}
     {{ com \texttt{<|} }}
-  | |>					:: :: endrec
+  | |>                                  :: :: endrec
     {{ tex \ensuremath{|\rangle} }}
     {{ com \texttt{|>} }}
-  | inter				:: :: inter
+  | inter                               :: :: inter
     {{ tex \ensuremath{\cap} }}
-  | union				:: :: union
-    {{ tex \ensuremath{\cup} }}
-  | u+					:: :: uplus
+%  | union                               :: :: union
+%    {{ tex \ensuremath{\cup} }}
+  | u+                                  :: :: uplus
     {{ tex \ensuremath{\uplus} }}
-  | NOTIN 				:: :: notin
+  | NOTIN                               :: :: notin
     {{ tex \ensuremath{\not\in} }}
-  | SUBSET				:: :: subset
+  | SUBSET                              :: :: subset
     {{ tex \ensuremath{\subset} }}
-  | NOTEQ				:: :: noteq
+  | NOTEQ                               :: :: noteq
     {{ tex \ensuremath{\not=} }}
-  | emptyset				:: :: emptyset
+  | emptyset                            :: :: emptyset
     {{ tex \ensuremath{\emptyset} }}
-  | < 					:: :: lt
+  | <                                   :: :: lt
     {{ tex \ensuremath{\langle} }}
-  | > 					:: :: gt
+  | >                                   :: :: gt
     {{ tex \ensuremath{\rangle} }}
-  | |-					:: :: vdash
+  | |-                                  :: :: vdash
     {{ tex \ensuremath{\vdash} }}
-  | '					:: :: quote
+  | '                                   :: :: quote
     {{ tex \mbox{'} }}
-  | |-> 				:: :: mapsto
+  | |->                                 :: :: mapsto
     {{ tex \ensuremath{\mapsto} }}
-  | gives				:: :: gives
+  | gives                               :: :: gives
     {{ tex \ensuremath{\triangleright} }}
-  | ~>					:: :: leadsto
+  | ~>                                  :: :: leadsto
     {{ tex \ensuremath{\leadsto} }}
-  | => 					:: :: Rightarrow
+  | =>                                  :: :: Rightarrow
     {{ tex \ensuremath{\Rightarrow} }}
-  | --					:: :: dashdash
+  | --                                  :: :: dashdash
     {{ tex \mbox{--} }}
-  | empty				:: :: empty
+  | empty                               :: :: empty
     {{ tex \ensuremath{\epsilon} }}
  
 
 formula :: formula_ ::=
-  | judgement							:: :: judgement
+  | judgement                                                   :: :: judgement
 
-  | formula1 .. formulan					:: :: dots
+  | formula1 .. formulan                                        :: :: dots
 
-%   | E_m ( x ) gives E						:: :: lookup_m
+%   | E_m ( x ) gives E                                         :: :: lookup_m
 %     {{ com Module lookup }}
 %     {{ hol (FLOOKUP [[E_m]] [[x]] = SOME [[E]]) }}
 %     {{ lem (Pmap.find [[x]] [[E_m]]) = [[E]] }} 
 % 
-%   | E_p ( x ) gives p						:: :: lookup_p
+%   | E_p ( x ) gives p                                         :: :: lookup_p
 %     {{ com Path lookup }}
 %     {{ hol (FLOOKUP [[E_p]] [[x]] = SOME [[p]]) }}
 %     {{ lem Pmap.find [[x]] [[E_p]] = [[p]] }} 
 
-  | E_f ( x ) gives f_desc					:: :: lookup_f
-    {{ com Field lookup }}
-    {{ hol (FLOOKUP [[E_f]] [[x]] = SOME [[f_desc]]) }}
-    {{ lem Pmap.find [[x]] [[E_f]] = [[f_desc]] }} 
-
-  | E_x ( x ) gives v_desc					:: :: lookup_v
-    {{ com Value lookup }}
-    {{ hol (FLOOKUP [[E_x]] [[x]] = SOME [[v_desc]]) }}
-    {{ lem Pmap.find [[x]] [[E_x]] = [[v_desc]] }} 
-
-  | E_l ( x ) gives t						:: :: lookup_l
-    {{ com Lexical binding lookup }}
-    {{ hol (FLOOKUP [[E_l]] [[x]] = SOME [[t]]) }}
-    {{ lem Pmap.find [[x]] [[E_l]] = [[t]] }} 
-
-%   | TD ( p ) gives tc_def					:: :: lookup_tc
-%     {{ com Type constructor lookup }}
-%     {{ hol (FLOOKUP [[TD]] [[p]] = SOME [[tc_def]]) }}
-%     {{ lem Pmap.find [[p]] [[TD]] = [[tc_def]] }} 
-% 
-%   | TC ( p ) gives xs						:: :: lookup_class
-%     {{ com Type constructor lookup }}
-%     {{ hol (FLOOKUP [[TC]] [[p]] = SOME [[xs]]) }}
-%     {{ lem Pmap.find [[p]] [[TC]] = [[xs]] }} 
-
-  | dom ( E_m1 ) inter dom ( E_m2 ) = emptyset			:: :: E_m_disjoint
-    {{ hol (DISJOINT (FDOM [[E_m1]]) (FDOM [[E_m2]])) }}
-    {{ lem disjoint (Pmap.domain [[E_m1]]) (Pmap.domain [[E_m2]]) }} 
-
-  | dom ( E_x1 ) inter dom ( E_x2 ) = emptyset			:: :: E_x_disjoint
-    {{ hol (DISJOINT (FDOM [[E_x1]]) (FDOM [[E_x2]])) }}
-    {{ lem disjoint (Pmap.domain [[E_x1]]) (Pmap.domain [[E_x2]])  }} 
-    
-  | dom ( E_f1 ) inter dom ( E_f2 ) = emptyset			:: :: E_f_disjoint
-    {{ hol (DISJOINT (FDOM [[E_f1]]) (FDOM [[E_f2]])) }}
-    {{ lem disjoint (Pmap.domain [[E_f1]]) (Pmap.domain [[E_f2]]) }} 
-
-%   | dom ( E_p1 ) inter dom ( E_p2 ) = emptyset			:: :: E_p_disjoint
-%     {{ hol (DISJOINT (FDOM [[E_p1]]) (FDOM [[E_p2]])) }}
-%     {{ lem disjoint (Pmap.domain [[E_p1]]) (Pmap.domain [[E_p2]]) }} 
-% 
-  | disjoint doms ( E_l1 , .... , E_ln )			:: :: E_l_disjoint
-    {{ hol (FOLDR (\E b. case b of NONE => NONE | SOME s => if DISJOINT (FDOM
-E) s then SOME (FDOM E UNION s) else NONE) (SOME {}) [[E_l1....E_ln]] <> NONE) }}
-    {{ lem disjoint_all (List.map Pmap.domain [[E_l1 .... E_ln]]) }}
-    {{ com Pairwise disjoint domains }}
-
-  | disjoint doms ( E_x1 , .... , E_xn )			:: :: E_x_disjoint_many
-    {{ hol (FOLDR (\E b. case b of NONE => NONE | SOME s => if DISJOINT (FDOM
-E) s then SOME (FDOM E UNION s) else NONE) (SOME {}) [[E_x1....E_xn]] <> NONE) }}
-    {{ lem disjoint_all (List.map Pmap.domain [[E_x1 .... E_xn]]) }}
-    {{ com Pairwise disjoint domains }}
-
-  | compatible overlap ( x1 |-> t1 , .. , xn |-> tn )		:: :: E_l_compat
-    {{ hol (!__n __m. MEM __m [[x1 t1 .. xn tn]] /\ MEM __n [[x1 t1..xn tn]] /\ (FST __m  = FST __n) ==> (SND __m = SND __n)) }}
-    {{ lem (compatible_overlap [[x1 t1 .. xn tn]]) }} 
-    {{ com $(\ottnt{x}_i = \ottnt{x}_j) \ensuremath{\Longrightarrow} (\ottnt{t}_i = \ottnt{t}_j)$ }}
-
-  | duplicates ( tnvs ) = emptyset				:: :: no_dups_tnvs
-    {{ hol (ALL_DISTINCT [[tnvs]]) }}
-    {{ lem (duplicates [[tnvs]]) = [ ] }} 
-
-  | duplicates ( x1 , .. , xn )	= emptyset			:: :: no_dups
-    {{ hol (ALL_DISTINCT [[x1..xn]]) }}
-    {{ lem (duplicates [[x1..xn]]) = [ ] }} 
-
-  | x NOTIN dom ( E_l )						:: :: notin_dom_l
-    {{ hol ([[x]] NOTIN FDOM [[E_l]]) }}
-    {{ lem Pervasives.not (Pmap.mem [[x]] [[E_l]]) }} 
-
-  | x NOTIN dom ( E_x )						:: :: notin_dom_v
-    {{ hol ([[x]] NOTIN FDOM [[E_x]]) }}
-    {{ lem Pervasives.not (Pmap.mem [[x]] [[E_x]]) }} 
-
-  | x NOTIN dom ( E_f )						:: :: notin_dom_f
-    {{ hol ([[x]] NOTIN FDOM [[E_f]]) }}
-    {{ lem Pervasives.not (Pmap.mem [[x]] [[E_f]]) }} 
-
-%   | p NOTIN dom ( TC )						:: :: notin_dom_tc
-%     {{ hol ([[p]] NOTIN FDOM [[TC]]) }}
-%     {{ lem Pervasives.not (Pmap.mem [[p]] [[TC]]) }} 
-
-  | p NOTIN dom ( TD )						:: :: notin_dom_td
-    {{ hol ([[p]] NOTIN FDOM [[TD]]) }}
-    {{ lem Pervasives.not (Pmap.mem [[p]] [[TD]]) }} 
-
-  | FV ( t ) SUBSET tnvs						:: :: FV_t
-    {{ com Free type variables }}
-    {{ hol (LIST_TO_SET (ftv_t [[t]]) SUBSET LIST_TO_SET [[tnvs]]) }}
-    {{ lem subst (ftv_t [[t]]) [[tnvs]]  }} 
-
-  | FV ( t_multi ) SUBSET tnvs					:: :: FV_t_multi
-    {{ com Free type variables }}
-    {{ hol (LIST_TO_SET (FLAT (MAP ftv_t [[t_multi]])) SUBSET LIST_TO_SET [[tnvs]]) }}
-    {{ lem subst (ftv_tm [[t_multi]]) [[tnvs]]  }} 
-
-  | FV ( semC ) SUBSET tnvs					:: :: FV_semC
-    {{ com Free type variables }}
-    {{ hol (LIST_TO_SET (MAP SND [[semC]]) SUBSET LIST_TO_SET [[tnvs]]) }}
-    {{ lem subst (ftv_s [[semC]]) [[tnvs]] }} 
-
-  | inst 'IN' I							:: :: inst_in
-    {{ hol (MEM [[inst]] [[I]]) }}
-    {{ lem ([[inst]] IN [[I]]) }}
-
-  | ( p t ) NOTIN I						:: :: notin_I
-    {{ hol (~?__semC__. MEM (Inst __semC__ [[p]] [[t]]) [[I]]) }}
-    {{ lem (Pervasives.not ((Inst [] [[p]] [[t]]) IN [[I]])) }}
-
-  | E_l1 = E_l2							:: :: E_l_eqn
-    {{ ichl ([[E_l1]] = [[E_l2]]) }}
-
-  | E_x1 = E_x2							:: :: E_x_eqn
-    {{ ichl ([[E_x1]] = [[E_x2]]) }}
-
-  | E_f1 = E_f2							:: :: E_f_eqn
-    {{ ichl ([[E_f1]] = [[E_f2]]) }}
-
-  | E1 = E2							:: :: E_eqn
-    {{ ichl ([[E1]] = [[E2]]) }}
-
-  | TD1 = TD2							:: :: TD_eqn
-    {{ ichl ([[TD1]] = [[TD2]]) }}
-
-  | TC1 = TC2							:: :: TC_eqn
-    {{ ichl ([[TC1]] = [[TC2]]) }}
-
-  | I1 = I2							:: :: I_eqn
-    {{ ichl ([[I1]] = [[I2]]) }}
-
-  | names1 = names2						:: :: names_eq
-    {{ ichl ([[names1]] = [[names2]]) }}
-
-  | t1 = t2							:: :: t_eq
-    {{ ichl ([[t1]] = [[t2]]) }}
-
-  | t_subst1 = t_subst2						:: :: t_subst_eq
-    {{ ichl ([[t_subst1]] = [[t_subst2]]) }}
-
-  | p1 = p2							:: :: p_eq
-    {{ ichl ([[p1]] = [[p2]]) }}
-
-  | xs1 = xs2							:: :: xs_eq
-    {{ ichl ([[xs1]] = [[xs2]]) }}
-
-  | tnvs1 = tnvs2							:: :: tnvs_eq
-    {{ ichl ([[tnvs1]] = [[tnvs2]]) }}
+%% %%   | E_f ( x ) gives f_desc                                      :: :: lookup_f
+%% %%     {{ com Field lookup }}
+%% %%     {{ hol (FLOOKUP [[E_f]] [[x]] = SOME [[f_desc]]) }}
+%% %%     {{ lem Pmap.find [[x]] [[E_f]] = [[f_desc]] }} 
+%% %% 
+%% %%   | E_x ( x ) gives v_desc                                      :: :: lookup_v
+%% %%     {{ com Value lookup }}
+%% %%     {{ hol (FLOOKUP [[E_x]] [[x]] = SOME [[v_desc]]) }}
+%% %%     {{ lem Pmap.find [[x]] [[E_x]] = [[v_desc]] }} 
+%% %% 
+%% %%   | E_l ( x ) gives t                                           :: :: lookup_l
+%% %%     {{ com Lexical binding lookup }}
+%% %%     {{ hol (FLOOKUP [[E_l]] [[x]] = SOME [[t]]) }}
+%% %%     {{ lem Pmap.find [[x]] [[E_l]] = [[t]] }} 
+%% %% 
+%% %% %   | TD ( p ) gives tc_def                                     :: :: lookup_tc
+%% %% %     {{ com Type constructor lookup }}
+%% %% %     {{ hol (FLOOKUP [[TD]] [[p]] = SOME [[tc_def]]) }}
+%% %% %     {{ lem Pmap.find [[p]] [[TD]] = [[tc_def]] }} 
+%% %% % 
+%% %% %   | TC ( p ) gives xs                                         :: :: lookup_class
+%% %% %     {{ com Type constructor lookup }}
+%% %% %     {{ hol (FLOOKUP [[TC]] [[p]] = SOME [[xs]]) }}
+%% %% %     {{ lem Pmap.find [[p]] [[TC]] = [[xs]] }} 
+%% %% 
+%% %%   | dom ( E_m1 ) inter dom ( E_m2 ) = emptyset                  :: :: E_m_disjoint
+%% %%     {{ hol (DISJOINT (FDOM [[E_m1]]) (FDOM [[E_m2]])) }}
+%% %%     {{ lem disjoint (Pmap.domain [[E_m1]]) (Pmap.domain [[E_m2]]) }} 
+%% %% 
+%% %%   | dom ( E_x1 ) inter dom ( E_x2 ) = emptyset                  :: :: E_x_disjoint
+%% %%     {{ hol (DISJOINT (FDOM [[E_x1]]) (FDOM [[E_x2]])) }}
+%% %%     {{ lem disjoint (Pmap.domain [[E_x1]]) (Pmap.domain [[E_x2]])  }} 
+%% %%     
+%% %%   | dom ( E_f1 ) inter dom ( E_f2 ) = emptyset                  :: :: E_f_disjoint
+%% %%     {{ hol (DISJOINT (FDOM [[E_f1]]) (FDOM [[E_f2]])) }}
+%% %%     {{ lem disjoint (Pmap.domain [[E_f1]]) (Pmap.domain [[E_f2]]) }} 
+%% %% 
+%% %% %   | dom ( E_p1 ) inter dom ( E_p2 ) = emptyset                        :: :: E_p_disjoint
+%% %% %     {{ hol (DISJOINT (FDOM [[E_p1]]) (FDOM [[E_p2]])) }}
+%% %% %     {{ lem disjoint (Pmap.domain [[E_p1]]) (Pmap.domain [[E_p2]]) }} 
+%% %% % 
+%% %%   | disjoint doms ( E_l1 , .... , E_ln )                        :: :: E_l_disjoint
+%% %%     {{ hol (FOLDR (\E b. case b of NONE => NONE | SOME s => if DISJOINT (FDOM
+%% %% E) s then SOME (FDOM E UNION s) else NONE) (SOME {}) [[E_l1....E_ln]] <> NONE) }}
+%% %%     {{ lem disjoint_all (List.map Pmap.domain [[E_l1 .... E_ln]]) }}
+%% %%     {{ com Pairwise disjoint domains }}
+%% %% 
+%% %%   | disjoint doms ( E_x1 , .... , E_xn )                        :: :: E_x_disjoint_many
+%% %%     {{ hol (FOLDR (\E b. case b of NONE => NONE | SOME s => if DISJOINT (FDOM
+%% %% E) s then SOME (FDOM E UNION s) else NONE) (SOME {}) [[E_x1....E_xn]] <> NONE) }}
+%% %%     {{ lem disjoint_all (List.map Pmap.domain [[E_x1 .... E_xn]]) }}
+%% %%     {{ com Pairwise disjoint domains }}
+%% %% 
+%% %%   | compatible overlap ( x1 |-> t1 , .. , xn |-> tn )           :: :: E_l_compat
+%% %%     {{ hol (!__n __m. MEM __m [[x1 t1 .. xn tn]] /\ MEM __n [[x1 t1..xn tn]] /\ (FST __m  = FST __n) ==> (SND __m = SND __n)) }}
+%% %%     {{ lem (compatible_overlap [[x1 t1 .. xn tn]]) }} 
+%% %%     {{ com $(\ottnt{x}_i = \ottnt{x}_j) \ensuremath{\Longrightarrow} (\ottnt{t}_i = \ottnt{t}_j)$ }}
+%% %% 
+%% %%   | duplicates ( tnvs ) = emptyset                              :: :: no_dups_tnvs
+%% %%     {{ hol (ALL_DISTINCT [[tnvs]]) }}
+%% %%     {{ lem (duplicates [[tnvs]]) = [ ] }} 
+%% %% 
+%% %%   | duplicates ( x1 , .. , xn ) = emptyset                      :: :: no_dups
+%% %%     {{ hol (ALL_DISTINCT [[x1..xn]]) }}
+%% %%     {{ lem (duplicates [[x1..xn]]) = [ ] }} 
+%% %% 
+%% %%   | x NOTIN dom ( E_l )                                         :: :: notin_dom_l
+%% %%     {{ hol ([[x]] NOTIN FDOM [[E_l]]) }}
+%% %%     {{ lem Pervasives.not (Pmap.mem [[x]] [[E_l]]) }} 
+%% %% 
+%% %%   | x NOTIN dom ( E_x )                                         :: :: notin_dom_v
+%% %%     {{ hol ([[x]] NOTIN FDOM [[E_x]]) }}
+%% %%     {{ lem Pervasives.not (Pmap.mem [[x]] [[E_x]]) }} 
+%% %% 
+%% %%   | x NOTIN dom ( E_f )                                         :: :: notin_dom_f
+%% %%     {{ hol ([[x]] NOTIN FDOM [[E_f]]) }}
+%% %%     {{ lem Pervasives.not (Pmap.mem [[x]] [[E_f]]) }} 
+%% %% 
+%% %% %   | p NOTIN dom ( TC )                                                :: :: notin_dom_tc
+%% %% %     {{ hol ([[p]] NOTIN FDOM [[TC]]) }}
+%% %% %     {{ lem Pervasives.not (Pmap.mem [[p]] [[TC]]) }} 
+%% %% 
+%% %%   | p NOTIN dom ( TD )                                          :: :: notin_dom_td
+%% %%     {{ hol ([[p]] NOTIN FDOM [[TD]]) }}
+%% %%     {{ lem Pervasives.not (Pmap.mem [[p]] [[TD]]) }} 
+%% %% 
+%% %%   | FV ( t ) SUBSET tnvs                                                :: :: FV_t
+%% %%     {{ com Free type variables }}
+%% %%     {{ hol (LIST_TO_SET (ftv_t [[t]]) SUBSET LIST_TO_SET [[tnvs]]) }}
+%% %%     {{ lem subst (ftv_t [[t]]) [[tnvs]]  }} 
+%% %% 
+%% %%   | FV ( t_multi ) SUBSET tnvs                                  :: :: FV_t_multi
+%% %%     {{ com Free type variables }}
+%% %%     {{ hol (LIST_TO_SET (FLAT (MAP ftv_t [[t_multi]])) SUBSET LIST_TO_SET [[tnvs]]) }}
+%% %%     {{ lem subst (ftv_tm [[t_multi]]) [[tnvs]]  }} 
+%% %% 
+%% %%   | FV ( semC ) SUBSET tnvs                                     :: :: FV_semC
+%% %%     {{ com Free type variables }}
+%% %%     {{ hol (LIST_TO_SET (MAP SND [[semC]]) SUBSET LIST_TO_SET [[tnvs]]) }}
+%% %%     {{ lem subst (ftv_s [[semC]]) [[tnvs]] }} 
+%% %% 
+%% %%   | inst 'IN' I                                                 :: :: inst_in
+%% %%     {{ hol (MEM [[inst]] [[I]]) }}
+%% %%     {{ lem ([[inst]] IN [[I]]) }}
+%% %% 
+%% %%   | ( p t ) NOTIN I                                             :: :: notin_I
+%% %%     {{ hol (~?__semC__. MEM (Inst __semC__ [[p]] [[t]]) [[I]]) }}
+%% %%     {{ lem (Pervasives.not ((Inst [] [[p]] [[t]]) IN [[I]])) }}
+%% %% 
+%% %%   | E_l1 = E_l2                                                 :: :: E_l_eqn
+%% %%     {{ ichl ([[E_l1]] = [[E_l2]]) }}
+%% %% 
+%% %%   | E_x1 = E_x2                                                 :: :: E_x_eqn
+%% %%     {{ ichl ([[E_x1]] = [[E_x2]]) }}
+%% %% 
+%% %%   | E_f1 = E_f2                                                 :: :: E_f_eqn
+%% %%     {{ ichl ([[E_f1]] = [[E_f2]]) }}
+%% %% 
+%% %%   | E1 = E2                                                     :: :: E_eqn
+%% %%     {{ ichl ([[E1]] = [[E2]]) }}
+%% %% 
+%% %%   | TD1 = TD2                                                   :: :: TD_eqn
+%% %%     {{ ichl ([[TD1]] = [[TD2]]) }}
+%% %% 
+%% %%   | TC1 = TC2                                                   :: :: TC_eqn
+%% %%     {{ ichl ([[TC1]] = [[TC2]]) }}
+%% %% 
+%% %%   | I1 = I2                                                     :: :: I_eqn
+%% %%     {{ ichl ([[I1]] = [[I2]]) }}
+%% %% 
+%% %%   | names1 = names2                                             :: :: names_eq
+%% %%     {{ ichl ([[names1]] = [[names2]]) }}
+%% %% 
+%% %%   | t1 = t2                                                     :: :: t_eq
+%% %%     {{ ichl ([[t1]] = [[t2]]) }}
+%% %% 
+%% %%   | t_subst1 = t_subst2                                         :: :: t_subst_eq
+%% %%     {{ ichl ([[t_subst1]] = [[t_subst2]]) }}
+%% %% 
+%% %%   | p1 = p2                                                     :: :: p_eq
+%% %%     {{ ichl ([[p1]] = [[p2]]) }}
+%% %% 
+%% %%   | xs1 = xs2                                                   :: :: xs_eq
+%% %%     {{ ichl ([[xs1]] = [[xs2]]) }}
+%% %% 
+%% %%   | tnvs1 = tnvs2                                                       :: :: tnvs_eq
+%% %%     {{ ichl ([[tnvs1]] = [[tnvs2]]) }}
 
 % Substitutions and freevars are not correctly generated for the OCaml ast.ml
 %substitutions
@@ -1883,7 +1947,7 @@ E) s then SOME (FDOM E UNION s) else NONE) (SOME {}) [[E_x1....E_xn]] <> NONE) }
 %% % TD,E,E_l |- exp1 exp2 : t2 gives S_c1 union S_c2, S_N1 union S_N2
 %% % 
 %% % %TODO t1 and t1 should be t1 and t'1 so that constraints from any vectors can be extracted and added to S_N
-%% % % 		Same for t2
+%% % %          Same for t2
 %% % :check_exp_aux: TD,E,E_l |- (ix) : t1 -> t2 -> t3 gives S_c1,S_N1
 %% % TD,E,E_l |- exp1 : t1 gives S_c2,S_N2
 %% % TD,E,E_l |- exp2 : t2 gives S_c3,S_N3