Point sail/src makefile at ott file in language/

2 files changed, 2 insertions, 1182 deletions

diff --git a/src/Makefile b/src/Makefile
index d1e29d06..68ad408f 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -49,8 +49,8 @@ all: sail lib doc
 
 full: sail lib power doc test
 
-ast.ml: ast.ott
-	ott -sort false -generate_aux_rules true -o ast.ml -picky_multiple_parses true ast.ott
+ast.ml: ../language/l2.ott
+	ott -sort false -generate_aux_rules true -o ast.ml -picky_multiple_parses true ../language/l2.ott
 
 sail: ast.ml
 	ocamlbuild sail.native
diff --git a/src/ast.ott b/src/ast.ott
deleted file mode 100644
index f08b089b..00000000
--- a/src/ast.ott
+++ /dev/null
@@ -1,1180 +0,0 @@
-%%
-%% Grammar for user language. Generates ./src/ast.ml
-%%
-
-indexvar n , m , i , j ::=
-  {{ phantom }}
-  {{ com Index variables for meta-lists }}
-
-metavar num,numZero,numOne ::=
-  {{ phantom }}
-  {{ lex numeric }}
-  {{ ocaml int }}
-  {{ hol num }}
-  {{ lem integer }}
-  {{ com Numeric literals }}
-
-metavar nat ::=
-  {{ phantom }}
-  {{ lex numeric }}
-  {{ lem nat }}
-
-metavar hex ::=
-  {{ phantom }}
-  {{ lex numeric }}
-  {{ ocaml string }}
-  {{ lem string }}
-  {{ com Bit vector literal, specified by C-style hex number }}
-  
-metavar bin ::=
-  {{ phantom }}
-  {{ lex numeric }}
-  {{ ocaml string }}
-  {{ lem string }}
-  {{ com Bit vector literal, specified by C-style binary number }}  
-
-metavar string ::=
-  {{ phantom }}
-  {{ ocaml string }}
-  {{ lem string }}
-  {{ hol string }}
-  {{ com String literals }}
-
-metavar regexp ::=
-  {{ phantom }}
-  {{ ocaml string }}
-  {{ lem string }}
-  {{ hol string }}
-  {{ com Regular expresions, as a string literal }}
-
-metavar real ::=
-   {{ phantom }}
-  {{ ocaml string }}
-  {{ lem string }}
-  {{ hol string }}
-  {{ com Real number literal }}
-
-embed
-{{ ocaml
-
-type text = string
-
-type l = Parse_ast.l
-
-type 'a annot = l * 'a
-
-type loop = While | Until
-
-}}
-
-embed
-{{ lem
-open import Pervasives
-open import Pervasives_extra
-open import Map
-open import Maybe
-open import Set_extra
-
-type l =
-  | Unknown
-  | Int of string * maybe l (*internal types, functions*)
-  | Range of string * nat * nat * nat * nat
-  | Generated of l (*location for a generated node, where l is the location of the closest original source*)
-
-type annot 'a = l * 'a
-
-val duplicates : forall 'a. list 'a -> list 'a
-
-val set_from_list : forall 'a. list 'a -> set 'a
-
-val subst : forall 'a. list 'a -> list 'a -> bool
-
-}}
-
-metavar x , y , z ::=
-  {{ ocaml text }}
-  {{ lem string }}
-  {{ hol string }}
-  {{ com identifier }}
-  {{ ocamlvar "[[x]]" }}
-  {{ lemvar "[[x]]" }}
-
-metavar ix ::=
-  {{ lex alphanum }}
-  {{ ocaml text }}
-  {{ lem string }}
-  {{ hol string }}
-  {{ com infix identifier }}
-  {{ ocamlvar "[[ix]]" }}
-  {{ lemvar "[[ix]]" }}
-
-
-
-grammar
-
-l :: '' ::=                                     {{ phantom }}
-                                                {{ ocaml Parse_ast.l }}
-                                                {{ lem l }}
-                                                {{ hol unit }}
-  {{ com source location }}
-  |                                             :: :: Unknown
-    {{ ocaml Unknown }}
-    {{ lem Unknown }}
-    {{ hol () }}
-
-annot :: '' ::=
-                                                {{ phantom }}
-                                                {{ ocaml 'a annot }}
-                                                {{ lem annot 'a }}
-                                                {{ hol unit }}
-
-id :: '' ::=
-  {{ com Identifier }}
-  {{ aux _ l }}
-  | x                           :: :: id
-  | ( deinfix x )                       :: D :: deIid {{ com remove infix status }}
-  | bool      		   	 :: M :: bool {{ com built in type identifiers }} {{ ichlo (Id "bool") }}
-  | bit				 :: M :: bit {{ ichlo (Id "bit") }} 
-  | unit			 :: M :: unit {{ ichlo (Id "unit") }}
-  | nat				 :: M :: nat  {{ ichlo (Id "nat") }}
-  | int				 :: M :: int  {{ ichlo (Id "int") }}
-  | string                       :: M :: string {{ tex \ottkw{string} }} {{ ichlo (Id "string") }}
-  | range                        :: M :: range {{ ichlo (Id "range") }}
-  | atom			 :: M :: atom {{ ichlo (Id "atom") }}
-  | vector			 :: M :: vector {{ ichlo (Id "vector") }}
-  | list			 :: M :: list {{ ichlo (Id "list") }}
-%  | set                          :: M :: set {{ ichlo (Id "set") }}
-  | reg                          :: M :: reg {{ ichlo (Id "reg") }}
-  | to_num			 :: M :: tonum {{ com built-in function identifiers }} {{ ichlo (Id "to_num") }}
-  | to_vec			 :: M :: tovec {{ ichlo (Id "to_vec") }}
-  | msb                          :: M :: msb {{ ichlo (Id "msb") }}
-% Note: we have just a single namespace. We don't want the same
-% identifier to be reused as a type name or variable, expression
-% variable, and field name.  We don't enforce any lexical convention
-% on type variables (or variables of other kinds)
-% We don't enforce a lexical convention on infix operators, as some of the 
-% targets use alphabetical infix operators.
-
-% Vector builtins 
-  | vector_access          :: M :: vector_access  {{ ichlo (Id "vector_access") }} 
-  | vector_update          :: M :: vector_update  {{ ichlo (Id "vector_update") }}
-  | vector_update_subrange :: M :: vector_update_subrange {{ ichlo (Id "vector_update_subrange") }}
-  | vector_subrange        :: M :: vector_subrange {{ ichlo (Id "vector_subrange") }}
-  | vector_append        :: M :: vector_append {{ ichlo (Id "vector_append") }}
-
-% Comparison builtins
-  | lteq_atom_atom :: M :: lteq_atom_atom {{ ichlo (Id "lteq_atom_atom") }}
-  | gteq_atom_atom :: M :: gteq_atom_atom {{ ichlo (Id "gteq_atom_atom") }}
-  | lt_atom_atom :: M :: lt_atom_atom {{ ichlo (Id "lt_atom_atom") }}
-  | gt_atom_atom :: M :: gt_atom_atom {{ ichlo (Id "gt_atom_atom") }}
-  
-kid :: '' ::=
-  {{ com kinded IDs: $[[Type]]$, $[[Nat]]$, $[[Order]]$, and $[[Effect]]$ variables }}
-  {{ aux _ l }}
-  | ' x                       :: :: var
- 
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% Kinds and Types                                              %
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-
-grammar
-
-base_kind :: 'BK_' ::=  
-  {{ com base kind}}
-  {{ aux _ l }}
-  | Type                                      :: :: type    {{ com kind of types  }} 
-  | Nat                                       :: :: nat     {{ com kind of natural number size expressions  }} 
-  | Order                                     :: :: order  {{ com kind of vector order specifications  }} 
-
-
-kind :: 'K_' ::=  
-  {{ com kinds}}
-  {{ aux _ l }}
-  | base_kind1 -> ... -> base_kindn            :: :: kind 
-% we'll never use  ...-> Nat , .. Order , .. or Effects
-    
-nexp :: 'Nexp_' ::=  
-  {{ com numeric expression, of kind $[[Nat]]$ }}
-  {{ aux _ l }}
-  | id                                  :: :: id          {{ com abbreviation identifier }}
-  | kid                                 :: :: var         {{ com variable }}
-  | num                                 :: :: constant     {{ com constant }}
-  | nexp1 * nexp2                       :: :: times        {{ com product }}
-  | nexp1 + nexp2                       :: :: sum          {{ com sum }}
-  | nexp1 - nexp2			:: :: minus	   {{ com subtraction }} 
-  | 2** nexp                            :: :: exp         {{ com exponential }}
-  | neg nexp				:: I :: neg	  {{ com for internal use only}}
-  | ( nexp )                            :: S :: paren  {{ ichlo [[nexp]] }}
-
-order :: 'Ord_' ::=  
-  {{ com vector order specifications, of kind $[[Order]]$}}
-  {{ aux _ l }} 
-  | kid                                 :: :: var {{ com variable }} 
-  | inc                                 :: :: inc  {{ com increasing }}
-  | dec                                 :: :: dec  {{ com decreasing }}
-  | ( order )                             :: S :: paren {{ ichlo [[order]] }}
-
-base_effect :: 'BE_' ::=
-  {{ com effect }}
-  {{ aux _ l }}  
-  | rreg                                :: :: rreg {{ com read register }}
-  | wreg                                :: :: wreg {{ com write register }}
-  | rmem                                :: :: rmem {{ com read memory }}
-  | rmemt                               :: :: rmemt {{ com read memory and tag }}
-  | wmem                                :: :: wmem {{ com write memory }}
-  | wmea				                :: :: eamem {{ com signal effective address for writing memory }}
-  | exmem                               :: :: exmem {{ com determine if a store-exclusive (ARM) is going to succeed }}
-  | wmv					                :: :: wmv   {{ com write memory, sending only value }}
-  | wmvt                                :: :: wmvt  {{ com write memory, sending only value and tag }}
-  | barr                                :: :: barr {{ com memory barrier }}
-  | depend				                :: :: depend {{ com dynamic footprint }}
-  | undef                               :: :: undef {{ com undefined-instruction exception }}
-  | unspec                              :: :: unspec {{ com unspecified values }}
-  | nondet                              :: :: nondet {{ com nondeterminism, from $[[nondet]]$ }}
-  | escape                              :: :: escape {{ com potential call of  $[[exit]]$ }}
-  | lset                                :: :: lset {{ com local mutation; not user-writable }}
-  | lret                                :: :: lret {{ com local return; not user-writable }}
-
-effect :: 'Effect_' ::=
-  {{ com effect set, of kind $[[Effect]]$ }}
-  {{ aux _ l }}
- | kid                                 :: :: var
- | { base_effect1 , .. , base_effectn }           :: :: set {{ com effect set }}
- | pure                                 :: M :: pure {{ com sugar for empty effect set }} 
-   {{ lem (Effect_set [])  }} {{icho [[{}]] }}
- | effect1 u+ .. u+ effectn                   :: M :: union {{ com union of sets of effects }} {{ icho [] }}
-   {{ lem (List.foldr effect_union (Effect_aux (Effect_set []) Unknown) [[effect1..effectn]]) }}
-
-embed
-{{ lem
-let effect_union e1 e2 = 
-  match (e1,e2) with
-  | ((Effect_aux (Effect_set els) _),(Effect_aux (Effect_set els2) l)) -> Effect_aux (Effect_set (els++els2)) l
-  end
-}}
-
-grammar
-
-% TODO: are we going to need any effect polymorphism?  Conceivably for built-in maps and folds.  Yes.  But we think we don't need any interesting effect-set expressions, eg effectset-variable union {rreg}. 
-
-typ :: 'Typ_' ::=
-  {{ com type expressions, of kind $[[Type]]$ }}
-  {{ aux _ l }}
-  | _                                           :: :: wild
-    {{ com unspecified type }}
-  | id                                         :: :: id
-    {{ com defined type }}
-  | kid                                         :: :: var
-    {{ com type variable }}
-  | typ1 -> typ2 effectkw effect                        :: :: fn
-    {{ com Function (first-order only in user code) }}
-% 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
-    {{ com Tuple }}
-  | exist kid1 , .. , kidn , n_constraint . typ :: :: exist
-% TODO union in the other kind grammars?  or make a syntax of argument? or glom together the grammars and leave o the typechecker
-  | id < typ_arg1 , .. , typ_argn >                    :: :: app
-  {{ com type constructor application }}
-  | ( typ )                            :: S :: paren {{ ichlo [[typ]] }} 
-%  | range < nexp1, nexp2> :: :: range  {{ com natural numbers [[nexp2]] .. [[nexp2]]+[[nexp1]]-1 }}
-  | [| nexp |]             :: S :: range1 {{ichlo range <[[nexp]], 0> }} {{ com sugar for \texttt{range<0, nexp>} }}
-  | [| nexp : nexp' |]  :: S :: range2 {{ichlo range <[[nexp]],[[nexp']]> }} {{ com sugar for \texttt{range< nexp, nexp'>} }}
-% | atom < nexp > :: :: atom {{ com equivalent to range<nexp,nexp> }}
-  | [: nexp :]            :: S :: atom1 {{ichlo atom <[[nexp]]> }} {{ com sugar for \texttt{atom<nexp>}=\texttt{range<nexp,nexp>} }}
-% use .. not - to avoid ambiguity with nexp -
-% total maps and vectors indexed by finite subranges of nat
-%  | vector nexp1 nexp2 order typ :: :: vector {{ com vector of [[typ]], indexed by natural range }}
-% probably some sugar for vector types, using [ ] similarly to enums:
-% (but with .. not : in the former, to avoid confusion...)
-  | typ [ nexp ]  :: S :: vector2 {{ichlo vector < [[nexp]],0,inc,[[typ]] > }} 
-{{ com sugar for vector indexed by \texttt{[|} $[[nexp]]$ \texttt{|]} }}
-  | typ [ nexp : nexp' ] :: S :: vector3 {{ ichlo vector < [[nexp]],[[nexp']],inc,[[typ]] }} 
-{{ com sugar for vector indexed by \texttt{[|} $[[nexp]]$..$[[nexp']]$ \texttt{|]} }}
-  | typ [ nexp <: nexp' ] :: S :: vector4 {{ ichlo vector < [[nexp]],[[nexp']],inc,[[typ]] }} {{ com sugar for increasing vector }}
-  | typ [ nexp :> nexp' ] :: S :: vector5 {{ ichlo vector < [[nexp]],[[nexp']],dec,[[typ]] }} {{ com sugar for decreasing vector }}
-%  | register [ id ] :: S :: register {{ ichlo (Typ_app Id "lteq_atom_atom") }}
-% ...so bit [ nexp ] etc is just an instance of that
-%  | List < typ > :: :: list {{ com list of [[typ]] }}
-%  | Set < typ >  :: :: set  {{ com finite set of [[typ]] }}
-%  | Reg < typ > :: :: reg  {{ com mutable register components holding [[typ]] }}
-% "reg t" is basically the ML "t ref" 
-% not sure how first-class it should be, though
-% use "reg word32" etc for the types of vanilla registers 
-
- 
-typ_arg :: 'Typ_arg_' ::=
-  {{ com type constructor arguments of all kinds }}
-  {{ aux _ l }} 
-  | nexp       :: :: nexp
-  | typ        :: :: typ
-  | order     :: :: order
-
-% plus more for l-value/r-value pairs, as introduced by the L3 'compound' declarations   ... ref typ
-
-%typ_lib :: 'Typ_lib_' ::=
-%  {{ com library types and syntactic sugar for them }}
-%  {{ aux _ l }} {{ auxparam 'a }}
-% boring base types:
-%%  | unit :: :: unit {{ com unit type with value $()$ }}
-%  | bool :: :: bool {{ com booleans $[[true]]$ and $[[false]]$ }}
-%  | bit :: :: bit  {{ com pure bit values (not mutable bits) }}
-% experimentally trying with two distinct types of bool and bit ...
-%  | nat :: :: nat {{ com natural numbers 0,1,2,... }}
-%  | string :: :: string {{ com UTF8 strings }}
-% finite subranges of nat
-
-parsing
-
-Typ_tup <= Typ_tup
-Typ_fn right Typ_fn
-Typ_fn <= Typ_tup
-%Typ_fn right Typ_app1
-%Typ_tup right Typ_app1
-
-grammar
-
-n_constraint :: 'NC_' ::=
-  {{ com constraint over kind $[[Nat]]$ }}
-  {{ aux _ l }}
-  | nexp = nexp'                                :: :: equal
-  | nexp >= nexp'                               :: :: bounded_ge
-  | nexp '<=' nexp'                             :: :: bounded_le
-  | nexp != nexp'                               :: :: not_equal
-  | kid 'IN' { num1 , ... , numn }              :: :: set
-  | n_constraint \/ n_constraint'               :: :: or
-  | n_constraint /\ n_constraint'               :: :: and
-  | true                                        :: :: true
-  | false                                       :: :: false
-
-% Note only id on the left and constants on the right in a
-% finite-set-bound, as we don't think we need anything more
-
-kinded_id :: 'KOpt_' ::=
-  {{ com optionally kind-annotated identifier }}
-  {{ aux _ l }}
-  | kid	 	    		   	      :: :: none {{ com identifier }}
-  | kind kid				      :: :: kind {{ com kind-annotated variable }}
-
-quant_item :: 'QI_' ::=
-  {{ com kinded identifier or $[[Nat]]$ constraint }}
-  {{ aux _ l }}
-  | kinded_id 	  	 	       	      :: :: id {{ com optionally kinded identifier }}
-  | n_constraint			              :: :: const {{ com $[[Nat]]$ constraint }}
-
-typquant :: 'TypQ_' ::= 
-  {{ com type quantifiers and constraints}}
-  {{ aux _ l }}
-  | forall quant_item1 , ... , quant_itemn . :: :: tq %{{ texlong }}
-% WHY ARE CONSTRAINTS HERE AND NOT IN THE KIND LANGUAGE
-  |                           ::  ::  no_forall     {{ com empty }}
-
-typschm :: 'TypSchm_' ::=
-  {{ com type scheme  }}
-  {{ aux _ l }}
-  |  typquant typ                                                       :: :: ts
-
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% Type definitions                                             %
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-grammar
-%ctor_def :: 'CT_' ::=
-%  {{ com Datatype constructor definition clause }}
-%  {{ aux _ annot }} {{ auxparam 'a }}
-%  | id : typschm                                       :: :: ct
-% but we could get away with disallowing constraints in typschm, we
-% think - if it's useful to do that
-
-%enum_opt :: 'EnumOpt_' ::=
-%  |      :: :: empty
-%  | enum :: :: enum
-
-%% tdefbody :: 'TD_' ::=
-%%   {{ com Type definition bodies }}
-%%   | typschm                                                     :: :: abbrev
-%%     {{ com Type abbreviations }}
-%%   | typquant <| id1 : typ1 ; ... ; idn : typn semi_opt |>     :: :: record
-%%     {{ com Record types }}
-%%   | enumeration_flag_opt '|' ctor_def1 '|' ... '|' ctor_defn            :: :: variant
-%%     {{ com Variant types }}
-%% 
- name_scm_opt :: 'Name_sect_' ::=
-   {{ com optional variable naming-scheme constraint}} 
-   {{ aux _ l }}
-   |                                                   :: :: none
-   | [ name = regexp ]                                 :: :: some
-%% 
-%% type_def :: '' ::=
-%%   {{ com Type definitions }}
-%%   | 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
-
-type_def {{ ocaml 'a type_def }} :: 'TD_' ::=
-  {{ ocaml TD_aux of type_def_aux * 'a annot }}
-  | type_def_aux  :: :: aux
-
-type_def_aux  :: 'TD_' ::=
-  {{ com type definition body }}
-  | typedef id name_scm_opt = typschm                                        :: :: abbrev
-    {{ com type abbreviation }} {{ texlong }}
-  | typedef id name_scm_opt = const struct typquant { typ1 id1 ; ... ; typn idn semi_opt }     :: :: record
-    {{ com struct type definition }} {{ texlong }}
-% 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 name_scm_opt = const union typquant { type_union1 ; ... ; type_unionn semi_opt }   :: :: variant
-    {{ com tagged union type definition}} {{ texlong }}
-
-  | typedef id name_scm_opt = enumerate { id1 ; ... ; idn semi_opt }   :: :: enum
-    {{ com enumeration type definition}} {{ texlong }}
-
-  | typedef  id = register bits [ nexp : nexp' ] { index_range1 : id1 ; ... ; index_rangen : idn } 
-:: :: register {{ com register mutable bitfield type definition }} {{ texlong }}
-
-
-% the D(eprecated) forms here should be removed; they add complexity for no purpose.  The nexp abbreviation form should have better syntax.
-% ; many are shorthands for type\_defs
-kind_def :: 'KD_' ::=
-  {{ com Definition body for elements of kind }}
-  {{ aux _ annot }} {{ auxparam 'a }}
-  | Def kind id name_scm_opt = nexp                                           :: :: nabbrev
-    {{ com $[[Nat]]$-expression abbreviation }}
-%  | Def kind id name_scm_opt = typschm                                        :: D :: abbrev
-%    {{ com type abbreviation }} {{ texlong }}
-%  | Def kind id name_scm_opt = const struct typquant { typ1 id1 ; ... ; typn idn semi_opt }     :: D :: record
-%    {{ com struct type definition }} {{ texlong }}
-%  | Def kind id name_scm_opt = const union typquant { type_union1 ; ... ; type_unionn semi_opt }   :: D :: variant
-%    {{ com union type definition}} {{ texlong }}
-%  | Def kind id name_scm_opt = enumerate { id1 ; ... ; idn semi_opt }   :: D :: enum
-%    {{ com enumeration type definition}} {{ texlong }}
-%
-%  | Def kind id = register bits [ nexp : nexp' ] { index_range1 : id1 ; ... ; index_rangen : idn } 
-%:: D :: register {{ com register mutable bitfield type definition }} {{ texlong }}
-
-
-
-% also sugar [  nexp ] 
-
-type_union :: 'Tu_' ::=
-  {{ com type union constructors }}
-  {{ aux _ l }}
-  | id                                                  :: :: id
-  | typ id                                              :: :: ty_id
-
-index_range :: 'BF_' ::= {{ com index specification, for bitfields in register types}} 
-  {{ aux _ l }}
-  | num :: :: 'single'  {{ com single index }}
-  | num1 '..' num2 :: :: range {{ com index range }}
-  | index_range1 , index_range2 :: :: concat {{ com concatenation of index ranges }}
-
-% 
-
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% Literals                                                     %
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-
-grammar
-
-lit :: 'L_' ::=
-  {{ com literal constant }}
-  {{ aux _ l }}
-  | ( )                                                 :: :: unit  {{ com $() : [[unit]]$ }}
-%Presumably we want to remove bitzero and bitone ?
-  | bitzero                                             :: :: zero {{ com $[[bitzero]] : [[bit]]$ }}
-  | bitone                                              :: :: one {{ com $[[bitone]] : [[bit]]$ }}
-  | true                                                :: :: true  {{ com $[[true]] : [[bool]]$ }}
-  | false                                               :: :: false {{ com $[[false]] : [[bool]]$ }}
-  | num                                         :: :: num  {{ com natural number constant }}
-  | hex                                         :: :: hex  {{ com bit vector constant, C-style }}
-  {{ com hex and bin are constant bit vectors, C-style }}
-  | bin                                         :: :: bin  {{ com bit vector constant, C-style }}
-% Should undefined be of type bit[alpha] or alpha[beta] or just alpha?
-  | string                                              :: :: string {{ com string constant }}
-  | undefined					:: :: undef {{ com undefined-value constant }}
-  | real :: :: real
-  
-semi_opt {{ tex \ottnt{;}^{?} }} :: 'semi_' ::=         {{ phantom }}
-                                                        {{ ocaml bool }}
-                                                        {{ lem bool }}
-                                                        {{ hol bool }}
-  {{ com optional semi-colon }}
-  |                                                     :: :: no  
-    {{ hol F }}
-    {{ ocaml false }}
-    {{ lem false }}
-  | ';'                                                 :: :: yes
-    {{ hol T }}
-    {{ ocaml true }}
-    {{ lem true }}
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% Patterns                                                     %
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-
-pat :: 'P_' ::= 
-  {{ com pattern }}
-  {{ aux _ annot }} {{ auxparam 'a }}
-  | lit                                                 :: :: lit
-    {{ com literal constant pattern }}
-  | _                                                   :: :: wild  
-    {{ com wildcard }}
-  | ( pat as id )                                      :: :: as
-    {{ com named pattern }}
-% ML-style
-%  | ( pat : typ )                                       :: :: typ
-%    {{ com Typed patterns }}
-% C-style
-  | ( typ ) pat                                       :: :: typ
-    {{ com typed pattern }}
-  | id                                      :: :: id
-    {{ com identifier  }}
-  | pat kid :: :: var
-    {{ com bind pattern to type variable }}
-  | id ( pat1 , .. , patn )                                     :: :: app
-    {{ com union constructor pattern }}
-
-% OR?  do we invent something ghastly including a union keyword?  Perhaps not...
-
-%  | <| fpat1 ; ... ; fpatn semi_opt |>                  :: :: record
-%    {{ com Record patterns }}
-% OR
-  | { fpat1 ; ... ; fpatn semi_opt }                  :: :: record
-    {{ com struct pattern }}
-
-%Patterns for vectors
-%Should these be the same since vector syntax has changed, and lists have also changed?
-
-  | [ pat1 , .. , patn  ]                     :: :: vector
-   {{ com vector pattern }}
-
-%  | [ num1 = pat1 , .. , numn = patn ]                     :: :: vector_indexed
-%   {{ com vector pattern (with explicit indices) }}
-
-% cf ntoes for this
-  |  pat1 : .... : patn                                   :: :: vector_concat
-  {{ com concatenated vector pattern }} 
-
-  | ( pat1 , .... , patn )                              :: :: tup
-    {{ com tuple pattern }}
-  | [|| pat1 , .. , patn ||]	                        :: :: list
-    {{ com list pattern }}
-  | ( pat )                                             :: S :: paren
-    {{ ichlo [[pat]] }}
- | pat1 '::' pat2                                      :: :: cons
-   {{ com Cons patterns }}
-
-% XXX Is this still useful?
-fpat :: 'FP_' ::=
-  {{ com field pattern }}
-  {{ aux _ annot }} {{ auxparam 'a }}
-  | id = pat                                            :: :: Fpat
-
-parsing
-P_app <= P_app
-P_app <= P_as
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% Machinery for typing rules                                   %
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-embed
-{{ lem
-
-let rec remove_one i l =
-  match l with
-  | [] -> []
-  | i2::l2 -> if i2 = i then l2 else i2::(remove_one i l2)
-end
-
-let rec remove_from l l2 =
-  match l2 with 
-  | [] -> l
-  | i::l2' -> remove_from (remove_one i l) l2'
-end
-
-let disjoint s1 s2 = Set.null (s1 inter s2)
-
-let rec disjoint_all sets =
-  match sets with
-  | [] -> true
-  | s1::[] -> true
-  | s1::s2::sets -> (disjoint s1 s2) && (disjoint_all (s2::sets))
-end
-}}
-
- 
-grammar 
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% Expressions                                                  %
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-embed
-{{ lem
-
-type tannot = maybe (t * tag * list nec * effect * effect)
-
-}}
-
-grammar
-tannot :: '' ::=
-                                                {{ phantom }}
-                                                {{ ocaml tannot }}
-                                                {{ lem tannot }}
-loop :: loop ::= {{ phantom }}
-  | while ::   :: while 
-  | until ::  :: until 
-
-
-exp :: 'E_' ::=
-  {{ com expression }}
-  {{ aux _ annot }} {{ auxparam 'a }}  
-
-  | { exp1 ; ... ; expn }                               :: :: block {{ com sequential block }}
-% maybe we really should have indentation-sensitive syntax :-)  (given that some of the targets do)
-
-  | nondet { exp1 ; ... ; expn }                        :: :: nondet {{ com nondeterministic block }}
-
-  | id                                                  :: :: id
-    {{ com identifier }}
-
-  | lit                                                 :: :: lit
-    {{ com literal constant }}
-
-  | ( typ ) exp                                         :: :: cast
-    {{ com cast }}
-
-  | id ( exp1 , .. , expn )                                   :: :: app
-    {{ com function application }}
-  | id exp                                               :: S :: tup_app {{ ichlo [[id ( exp ) ]] }} 
-   {{ com funtion application to tuple }}
-
-% Note: fully applied function application only
-
-  | exp1 id exp2                                        :: :: app_infix
-    {{ com infix function application }}
- 
-  | ( exp1 , .... , expn )                              :: :: tuple
-    {{ com tuple }}
-
-  | if exp1 then exp2 else exp3                         :: :: if
-    {{ com conditional }}
-
-  | if exp1 then exp2                                   :: S :: ifnoelse {{ ichlo [[ if exp1 then exp2 else ( ) ]] }}
-  | loop exp1 exp2 :: :: loop
-  | while exp1 do exp2  ::  S :: while        {{ ichlo [[ loop while exp1 exp2 ]] }}
-  | repeat exp1 until exp2 :: S :: until     {{ ichlo [[ loop until exp2 exp1 ]] }}
-  | foreach ( id from exp1 to exp2 by exp3 in order ) exp4  ::   :: for {{ com loop }}
-  | foreach ( id from exp1 to exp2 by exp3 ) exp4           :: S :: forup {{ ichlo [[ foreach id from exp1 to exp2 by exp3 in inc exp4 ]] }}
-  | foreach ( id from exp1 to exp2 ) exp3                   :: S :: forupbyone  {{ ichlo [[ foreach id from exp1 to exp2 by 1 in inc exp4 ]] }}
-  | foreach ( id from exp1 downto exp2 by exp3 ) exp4       :: S :: fordown {{ ichlo [[ foreach id from exp1 to exp2 by exp3 in dec exp4 ]] }}
-  | foreach ( id from exp1 downto exp2 ) exp3               :: S :: fordownbyone  {{ ichlo [[ foreach id from exp1 downto exp2 by 1 in dec exp4 ]] }}
-
-% vectors
-  | [ exp1 , ... , expn ]                             :: :: vector {{ com vector (indexed from 0) }}
-% order comes from global command-line option???
-% here the expi are of type 'a and the result is a vector of 'a, whereas in exp1 : ... : expn 
-% the expi and the result are both of type vector of 'a 
-
-  | [ num1 = exp1 , ... , numn = expn opt_default ]               :: :: vector_indexed {{ com vector (indexed consecutively) }}
-% num1 .. numn must be a consecutive list of naturals
-
-% we pick [ ] not { } for vector literals for consistency with their
-% array-like access syntax, in contrast to the C which has funny
-% syntax for array literals.  We don't have to preserve [ ] for lists
-% as we don't expect to use lists very much. 
-
-  | exp [ exp' ]                                      :: :: vector_access
-  {{ com vector access }}
-
-  | exp [ exp1 '..' exp2 ]                               :: :: vector_subrange
-  {{ com subvector extraction }}
-  % do we want to allow a comma-separated list of such thingies?  
-
-  | [ exp with exp1 = exp2 ]                          :: :: vector_update 
-  {{ com vector functional update }}
-
-  | [ exp with exp1 : exp2 = exp3 ]                   :: :: vector_update_subrange
-  {{ com vector subrange update, with vector}}
-  % do we want a functional update form with a comma-separated list of such?
-
-  | exp : exp2                                        :: :: vector_append
-  {{ com vector concatenation }}
-
-% lists 
-  | [|| exp1 , ..  , expn ||]                           :: :: list
-  {{ com list }}
-  | exp1 '::' exp2                                    :: :: cons
-    {{ com cons }}
-
-
-% const unions
-
-% const structs
-
-% TODO
-
-  | { fexps }                                         :: :: record
-    {{ com struct }}
-  | { exp with fexps }                                :: :: record_update
-    {{ com functional update of struct }}
-  | exp . id                                          :: :: field
-    {{ com field projection from struct  }}
-
-%Expressions for creating and accessing vectors
-
-
-
-%  map : forall 'x 'y ''N.  ('x -> 'y) -> vector ''N 'x -> vector ''N 'y
-%  zip : forall 'x 'y ''N.  vector ''N 'x  -> vector ''N 'y -> vector ''N ('x*'y) 
-%  foldl : forall 'x 'y ''N. ('x 'y -> 'y) -> vector ''N 'x -> 'y -> 'y
-% foldr : forall 'x 'y ''N. ('x 'y -> 'y) -> 'y -> vector ''N 'x -> 'y
-% foldmap : forall 'x 'y 'z ''N. ((x,y) -> (x,z)) -> x -> vector ''N y -> vector ''N z
-%(or unzip)
-
-%  and maybe with nice syntax
-
-  | switch exp { case pexp1  ... case pexpn } :: :: case
-    {{ com pattern matching }}
-%  | ( typ ) exp                                      :: :: Typed
-%    {{ com Type-annotated expressions }}
-  | letbind in exp                                  :: :: let
-    {{ com let expression }}
-
-  | lexp := exp                                      :: :: assign
-    {{ com imperative assignment }}
-
-  | sizeof nexp                                         :: :: sizeof
-  {{ com the value of $[[nexp]]$ at run time }}
-
-  | return exp                                       :: :: return {{ com  return $[[exp]]$ from current function }}
-% this can be used to break out of for loops
-  | exit exp						:: :: exit
-    {{ com halt all current execution }}
-  | throw exp                                  :: :: throw
-  | try exp catch pexp1 .. pexpn             :: :: try
-%, potentially calling a system, trap, or interrupt handler with exp
-  | assert ( exp , exp' )                            :: :: assert
-    {{ com halt with error $[[exp']]$ when not $[[exp]]$ }}
-% exp' is optional?
-  | ( exp )                                             :: S :: paren {{ ichlo [[exp]] }}
-  | ( annot ) exp                                   :: I :: internal_cast {{ com This is an internal cast, generated during type checking that will resolve into a syntactic cast after }}
-  | annot                       :: I :: internal_exp {{ com This is an internal use for passing nexp information  to library functions, postponed for constraint solving }}
-  | sizeof annot             :: I :: sizeof_internal {{ com For sizeof during type checking, to replace nexp with internal n}}
-  | annot , annot'           :: I :: internal_exp_user {{ com This is like the above but the user has specified an implicit parameter for the current function }}
-  | comment string            :: I :: comment {{ com For generated unstructured comments }}
-  | comment exp               :: I :: comment_struc {{ com For generated structured comments }}
-  | let lexp = exp in exp'    :: I :: internal_let {{ com This is an internal node for compilation that demonstrates the scope of a local mutable variable }}
-  | let pat = exp in exp' :: I :: internal_plet {{ com This is an internal node, used to distinguised some introduced lets during processing from original ones }}
-  | return_int ( exp )                                          ::  :: internal_return {{ com For internal use to embed into monad definition }}
-%  | value :: I :: internal_value {{ com For internal use in interpreter to wrap pre-evaluated values when returning an action }}
-  | constraint n_constraint :: :: constraint
-
-%i_direction :: 'I' ::=
-%  | IInc :: :: Inc
-%  | IDec :: :: Dec
-
-%ctor_kind :: 'C_' ::=
-%  | C_Enum nat :: :: Enum
-%  | C_Union    :: :: Union
-
-%reg_form :: 'Form_' ::=
-%  | Reg id tannot i_direction :: :: Reg
-%  | SubReg id reg_form index_range :: :: SubReg
-
-%reg_form_set :: '' ::= {{ phantom }} {{ lem set reg_form }}
-
-%alias_spec_tannot :: '' ::= {{ phantom }} {{ lem alias_spec tannot }} {{ ocaml tannot alias_spec }}
-
-
-lexp :: 'LEXP_' ::= {{ com lvalue expression }}
-    {{ aux _ annot }} {{ auxparam 'a }}
-    | id                                                  :: :: id
-    {{ com identifier }}
-    | id ( exp1 , .. , expn )				  :: :: memory {{ com memory or register write via function call }}
-    | id exp	       	    				  :: S :: mem_tup {{ ichlo [[id (exp)]] }}
-{{ com sugared form of above for explicit tuple $[[exp]]$ }}
-    | ( typ ) id					  :: :: cast
-{{ com cast }}
-    | ( lexp0 , .. , lexpn )                              :: :: tup {{ com multiple (non-memory) assignment }}
-    | lexp [ exp ]  :: ::                                 vector  {{ com vector element }}
-    | lexp [ exp1 '..' exp2 ]  :: ::                         vector_range {{ com subvector }}
-    % maybe comma-sep such lists too
-    | lexp . id :: :: field                        {{ com struct field }}
-
-
-fexp :: 'FE_' ::=
-  {{ com field expression }}
-  {{ aux _ annot }} {{ auxparam 'a }}
-  | id = exp                                            :: :: Fexp
-
-fexps :: 'FES_' ::=
-  {{ com field expression list }}
-  {{ aux _ annot }} {{ auxparam 'a }}
-  | fexp1 ; ... ; fexpn semi_opt                        :: :: Fexps
-
-opt_default :: 'Def_val_' ::=
-  {{ com optional default value for indexed vector expressions }} %, to define a default value for any unspecified positions in a sparse map 
-  {{ aux _ annot }} {{ auxparam 'a }}
-  |                                                     :: :: empty
-  | ; default = exp                                       :: :: dec
-
-pexp :: 'Pat_' ::=
-  {{ com pattern match }}
-  {{ aux _ annot }} {{ auxparam 'a }}
-  | pat -> exp                          :: :: exp
-  | pat when exp1 -> exp                :: :: when
-% apparently could use -> or => for this.
-
-%% % psexp :: 'Pats' ::=
-%% %   {{ com Multi-pattern matches }}
-%% %   {{ aux _ l }}
-%% %   | pat1 ... patn -> exp                                :: :: exp
-
-
-parsing
-
-%P_app right LB_Let_val
-
-%%P_app <= Fun
-
-%%Fun right App
-%%Function right App
-E_case right E_app
-E_let right E_app
-
-%%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 %%%%%%%%%%
-
-tannot_opt :: 'Typ_annot_opt_' ::=
-  {{ com optional type annotation for functions}}
-  {{ aux _ l }} 
-  |                                             :: :: none
-% Currently not optional; one issue, do the type parameters apply over the argument types, or should this be the type of the function and not just the return
-  | typquant typ                                :: :: some 
-
-rec_opt :: 'Rec_' ::=
-  {{ com optional recursive annotation for functions }}
-  {{ aux _ l }}
-  |                                             :: :: nonrec {{ com non-recursive }}
-  | rec                                         :: :: rec {{ com recursive }}
-
-effect_opt :: 'Effect_opt_' ::=
-  {{ com optional effect annotation for functions }}
-  {{ aux _ l }}
-  |                                             :: :: pure {{ com sugar for empty effect set }}
-  | effectkw effect                              :: :: effect
-
-funcl :: 'FCL_' ::=
-  {{ com function clause }}
-  {{ aux _ annot }} {{ auxparam 'a }}
-  | id pat = exp                   :: :: Funcl
-
-
-fundef :: 'FD_' ::=
-  {{ com function definition}}
-  {{ aux _ annot }} {{ auxparam 'a }}
-  | function rec_opt tannot_opt effect_opt funcl1 and ... and funcln :: :: function {{ texlong }}  
-% {{ com function definition }}
-% TODO note that the typ in the tannot_opt is the *result* type, not
-%  the type of the whole function.  The argument type comes from the
-%  pattern in the funcl
-% TODO the above is ok for single functions, but not for mutually
-%  recursive functions - the tannot_opt scopes over all the funcli,
-%  which is ok for the typ_quant part but not for the typ part
-
-letbind :: 'LB_' ::=
-  {{ com let binding }}
-  {{ aux _ annot }} {{ auxparam 'a }}
-%  | let typschm pat = exp                                :: :: val_explicit
-%    {{ com let, explicit type ($[[pat]]$ must be total)}}
-% at the moment, we cannot parse the following, so perhaps we shouldn't keep this form here 
-  | let pat = exp                                    :: :: val
-    {{ com let, implicit type ($[[pat]]$ must be total)}}
-
-val_spec {{ ocaml 'a val_spec }} :: 'VS_' ::=
-   {{ ocaml VS_aux of val_spec_aux * 'a annot }}
-  | val_spec_aux ::  :: aux 
-
-
-val_spec_aux :: 'VS_' ::=
-  {{ com value type specification }} 
-  {{ ocaml  VS_val_spec of typschm * id * string option * bool }}
-  | val typschm id                                  :: S :: val_spec
-    {{ com specify the type of an upcoming definition }}
-    {{ ocaml (VS_val_spec [[typschm]] [[id]] None false) }}
-  | val cast typschm id                             :: S :: cast
-    {{ ocaml  (VS_val_spec [[typschm]] [[id]] None true) }}
-  | val extern typschm id                           :: S :: extern_no_rename
-    {{ com specify the type of an external function }}
-    {{ ocaml  (VS_val_spec [[typschm]] [[id]] (Some [[id]]) false) }}
-  | val extern typschm id = string                  :: S :: extern_spec
-    {{ com specify the type of a function from Lem }}
-    {{ ocaml  (VS_val_spec [[typschm]] [[id]] (Some [[string]]) false) }}
-%where the string must provide an explicit path to the required function but will not be checked
-
-default_spec :: 'DT_' ::=
-  {{ com default kinding or typing assumption }}
-  {{ aux _ l }}
-  | default Order order      :: :: order
-  | default base_kind kid    :: :: kind
-  | default typschm id      :: :: typ
-% The intended semantics of these is that if an id in binding position
-% doesn't have a kind or type annotation, then we look through the
-% default regexps (in order from the beginning) and pick the first
-% assumption for which id matches the regexp, if there is one.
-% Otherwise we try to infer.  Perhaps warn if there are multiple matches.
-% For example, we might often have default Type ['alphanum]
-
-scattered_def :: 'SD_' ::=
-  {{ com scattered function and union type definitions }}
-  {{ aux _ annot }} {{ auxparam 'a }}
-  | scattered function rec_opt tannot_opt effect_opt id   :: :: scattered_function 
-{{ texlong }} {{ com scattered function definition header }}
-
-  | function clause funcl  :: :: scattered_funcl  
-{{ texlong }} {{ com scattered function definition clause }}
-
-  | scattered typedef id name_scm_opt = const union typquant :: :: scattered_variant 
-{{ texlong }} {{ com scattered union definition header }}
-
-  | union id member type_union  :: :: scattered_unioncl 
-{{ texlong }} {{ com scattered union definition member }}
-  | end id  :: :: scattered_end
-{{ texlong }} {{ com scattered definition end }}
-
-reg_id :: 'RI_' ::=
-  {{ aux _ annot }} {{ auxparam 'a }}
-  | id								:: :: id
-
-alias_spec :: 'AL_' ::=
-  {{ com register alias expression forms }}
-%. Other than where noted, each id must refer to an unaliased register of type vector
-  {{ aux _ annot }} {{ auxparam 'a }}
-  | reg_id . id							:: :: subreg
-  | reg_id [ exp ] 						:: :: bit
-  | reg_id [ exp '..' exp' ]					:: :: slice
-  | reg_id : reg_id'  	    					:: :: concat
-
-dec_spec :: 'DEC_' ::=
-  {{ com register declarations }}
-  {{ aux _ annot }} {{ auxparam 'a }}
-  | register typ id                                             :: :: reg
-  | register alias id = alias_spec				:: :: alias
-  | register alias typ id = alias_spec				:: :: typ_alias
-
-dec_comm :: 'DC_' ::= {{ com top-level generated comments }} {{auxparam 'a}}
-  | comment string :: :: comm {{ com generated unstructured comment }}
-  | comment def    :: :: comm_struct {{ com generated structured comment }}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% Top-level definitions                                        %
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-prec :: '' ::=
-   | infix :: :: Infix
-   | infixl :: :: InfixL
-   | infixr :: :: InfixR
-
-def :: 'DEF_' ::=
-  {{ com top-level definition }}
-  {{ auxparam 'a }}
-  | kind_def                                                    :: :: kind
-    {{ com definition of named kind identifiers }}
-  | type_def                                                    :: :: type
-    {{ com type definition }}
-  | fundef                                                   :: :: fundef
-    {{ com function definition }}
-  | letbind                                                   :: :: val
-    {{ com value definition }}
-  | val_spec                                                    :: :: spec
-    {{ com top-level type constraint }}
-  | fix prec num id  :: :: fixity
-    {{ com fixity declaration }}
-  |  overload id [ id1 ; ... ; idn ] :: :: overload
-    {{ com operator overload specification }}
-  | default_spec                                         :: :: default
-    {{ com default kind and type assumptions }}
-  | scattered_def                                        :: :: scattered
-    {{ com scattered function and type definition }}
-  | dec_spec                                            :: :: reg_dec
-    {{ com register declaration }}
-  | dec_comm                                            :: I :: comm
-    {{ com generated comments }}
-
-defs :: '' ::=
-  {{ com definition sequence }}
-  {{ auxparam 'a }}
-  | def1  .. defn                 :: :: Defs
-
-
-
-terminals :: '' ::=
-  | **                                  :: :: starstar
-    {{ tex \ensuremath{\mathop{\mathord{*}\mathord{*} } } }}
-    {{ com \texttt{**} }}
-   | >=                                  :: :: geq
-    {{ tex \ensuremath{\geq} }}
-%     {{ tex \ottsym{\textgreater=} }}
-%     {{ com \texttt{>=} }}
-   | '<='                                        :: :: leq
-    {{ tex \ensuremath{\leq} }}
-%     {{ tex \ottsym{\textless=} }}
-%     {{ com \texttt{<=} }}
-   | ->                                  :: :: arrow
-    {{ tex \ensuremath{\rightarrow} }}
-%     {{ tex \ottsym{-\textgreater} }}
-%     {{ com \texttt{->} }}
-   | ==>                                 :: :: Longrightarrow
-     {{ tex \ensuremath{\Longrightarrow} }}
-     {{ com \texttt{==>} }}
-%   | <|                                  :: :: startrec
-%     {{ tex \ensuremath{\langle|} }}
-%     {{ com \texttt{<|} }}
-%   | |>                                  :: :: endrec
-%     {{ tex \ensuremath{|\rangle} }}
-%     {{ com \texttt{|>} }}
-  | inter                               :: :: inter
-    {{ tex \ensuremath{\cap} }}
-  | u+                                  :: :: uplus
-    {{ tex \ensuremath{\uplus} }}
-  | u-                                  :: :: uminus
-    {{ tex \ensuremath{\setminus} }}
-  | NOTIN                               :: :: notin
-    {{ tex \ensuremath{\not\in} }}
-  | SUBSET                              :: :: subset
-    {{ tex \ensuremath{\subset} }}
-  | NOTEQ                               :: :: noteq
-    {{ tex \ensuremath{\not=} }}
-  | emptyset                            :: :: emptyset
-    {{ tex \ensuremath{\emptyset} }}
-%   | <                                   :: :: lt
-    {{ tex \ensuremath{\langle} }}
-%     {{ tex \ottsym{<} }}
-%   | >                                   :: :: gt
-    {{ tex \ensuremath{\rangle} }}
-%    {{ tex \ottsym{>} }}
-  | lt                                  :: :: mathlt
-    {{ tex < }}
-  | gt                                  :: :: mathgt
-    {{ tex > }} 
-  | ~=                                  :: :: alphaeq
-    {{ tex \ensuremath{\approx} }}
-  | ~< 	   			:: :: consist
-    {{ tex \ensuremath{\precapprox} }}
-  | |-                                  :: :: vdash
-    {{ tex \ensuremath{\vdash} }}
-  | |-t					:: :: vdashT
-    {{ tex \ensuremath{\vdash_t} }}
-  | |-n					:: :: vdashN
-    {{ tex \ensuremath{\vdash_n} }}
-  | |-e					:: :: vdashE
-    {{ tex \ensuremath{\vdash_e} }}
-  | |-o					:: :: vdashO
-    {{ tex \ensuremath{\vdash_o} }}
-  | |-c                                 :: :: vdashC
-    {{ tex \ensuremath{\vdash_c} }}
-  | '                                   :: :: quote
-    {{ tex \ottsym{'} }}
-  | |->                                 :: :: mapsto
-    {{ tex \ensuremath{\mapsto} }}
-  | gives                               :: :: gives
-    {{ tex \ensuremath{\triangleright} }}
-  | ~>                                  :: :: leadsto
-    {{ tex \ensuremath{\leadsto} }}
-  | select				:: :: select
-   {{ tex \ensuremath{\sigma} }}
-  | =>                                  :: :: Rightarrow
-    {{ tex \ensuremath{\Rightarrow} }}
-  | --                                  :: :: dashdash
-    {{ tex \mbox{--} }}
-  | effectkw				:: :: effectkw
-    {{ tex \ottkw{effect} }}
-  | empty                               :: :: empty
-    {{ tex \ensuremath{\epsilon} }}
-  | consistent_increase                 :: :: ci
-    {{ tex \ottkw{consistent\_increase}~ }}
-  | consistent_decrease                 :: :: cd
-    {{ tex \ottkw{consistent\_decrease}~ }}
-  | == :: :: equiv
-    {{ tex \equiv }}
-%   | [| :: :: range_start
-%     {{ tex \mbox{$\ottsym{[\textbar}$} }}       
-%   | |] :: :: range_end       
-%     {{ tex \mbox{$\ottsym{\textbar]}$} }}       
-%   | [|| :: :: list_start
-%     {{ tex \mbox{$\ottsym{[\textbar\textbar}$} }}       
-%   | ||] :: :: list_end       
-%     {{ tex \mbox{$\ottsym{\textbar\textbar]}$} }}       
-
-