Generate ast.ml from ott file and update makefile.

Fix until loop not being counted as sugar

3 files changed, 1187 insertions, 583 deletions

diff --git a/src/Makefile b/src/Makefile
index d0001868..d1e29d06 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -49,15 +49,18 @@ all: sail lib doc
 
 full: sail lib power doc test
 
-sail:
+ast.ml: ast.ott
+	ott -sort false -generate_aux_rules true -o ast.ml -picky_multiple_parses true ast.ott
+
+sail: ast.ml
 	ocamlbuild sail.native
 
 sail.native: sail
 
-sail.byte: 
+sail.byte:
 	ocamlbuild -cflag -g sail.byte
 
-interpreter: 
+interpreter:
 	ocamlbuild lem_interp/extract.cmxa
 	ocamlbuild lem_interp/extract.cma
 
@@ -238,6 +241,7 @@ clean:
 	-rm -rf tex-doc
 	-rm -rf lem lib
 	-rm -rf sail.docdir
+	-rm -f ast.ml
 
 doc:
 	ocamlbuild sail.docdir/index.html
diff --git a/src/ast.ml b/src/ast.ml
deleted file mode 100644
index ec1d4d34..00000000
--- a/src/ast.ml
+++ /dev/null
@@ -1,580 +0,0 @@
-(**************************************************************************)
-(*     Sail                                                               *)
-(*                                                                        *)
-(*  Copyright (c) 2013-2017                                               *)
-(*    Kathyrn Gray                                                        *)
-(*    Shaked Flur                                                         *)
-(*    Stephen Kell                                                        *)
-(*    Gabriel Kerneis                                                     *)
-(*    Robert Norton-Wright                                                *)
-(*    Christopher Pulte                                                   *)
-(*    Peter Sewell                                                        *)
-(*                                                                        *)
-(*  All rights reserved.                                                  *)
-(*                                                                        *)
-(*  This software was developed by the University of Cambridge Computer   *)
-(*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  *)
-(*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   *)
-(*                                                                        *)
-(*  Redistribution and use in source and binary forms, with or without    *)
-(*  modification, are permitted provided that the following conditions    *)
-(*  are met:                                                              *)
-(*  1. Redistributions of source code must retain the above copyright     *)
-(*     notice, this list of conditions and the following disclaimer.      *)
-(*  2. Redistributions in binary form must reproduce the above copyright  *)
-(*     notice, this list of conditions and the following disclaimer in    *)
-(*     the documentation and/or other materials provided with the         *)
-(*     distribution.                                                      *)
-(*                                                                        *)
-(*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    *)
-(*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     *)
-(*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       *)
-(*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   *)
-(*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          *)
-(*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      *)
-(*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      *)
-(*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   *)
-(*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    *)
-(*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    *)
-(*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    *)
-(*  SUCH DAMAGE.                                                          *)
-(**************************************************************************)
-
-(* generated by Ott 0.25 from: l2.ott *)
-
-type text = string
-
-type l = Parse_ast.l
-
-type 'a annot = l * 'a
-
-
-type x = text (* identifier *)
-type ix = text (* infix identifier *)
-
-type
-base_kind_aux =  (* base kind *)
-   BK_type (* kind of types *)
- | BK_nat (* kind of natural number size expressions *)
- | BK_order (* kind of vector order specifications *)
-
-
-type
-base_kind =
-   BK_aux of base_kind_aux * l
-
-
-type
-id_aux =  (* Identifier *)
-   Id of x
- | DeIid of x (* remove infix status *)
-
-
-type
-kid_aux =  (* variables with kind, ticked to differntiate from program variables *)
-   Var of x
-
-
-type
-kind_aux =  (* kinds *)
-   K_kind of (base_kind) list
-
-
-type
-id =
-   Id_aux of id_aux * l
-
-
-type
-kid =
-   Kid_aux of kid_aux * l
-
-
-type
-kind =
-   K_aux of kind_aux * l
-
-
-type
-nexp_aux =  (* expression of kind Nat, for vector sizes and origins *)
-   Nexp_id of id (* identifier, bound by def Nat x = nexp *)
- | Nexp_var of kid (* variable *)
- | Nexp_constant of int (* constant *)
- | Nexp_times of nexp * nexp (* product *)
- | Nexp_sum of nexp * nexp (* sum *)
- | Nexp_minus of nexp * nexp (* subtraction *)
- | Nexp_exp of nexp (* exponential *)
- | Nexp_neg of nexp (* For internal use *)
-
-and nexp =
-   Nexp_aux of nexp_aux * l
-
-
-type
-base_effect_aux =  (* effect *)
-   BE_rreg (* read register *)
- | BE_wreg (* write register *)
- | BE_rmem (* read memory *)
- | BE_rmemt (* read memory tagged *)
- | BE_wmem (* write memory *)
- | BE_eamem (* signal effective address for writing memory *)
- | BE_exmem (* determine if a store-exclusive (ARM) is going to succeed *)
- | BE_wmv (* write memory, sending only value *)
- | BE_wmvt (* write memory, sending only value and tag *)
- | BE_barr (* memory barrier *)
- | BE_depend (* dynamic footprint *)
- | BE_undef (* undefined-instruction exception *)
- | BE_unspec (* unspecified values *)
- | BE_nondet (* nondeterminism from intra-instruction parallelism *)
- | BE_escape (* Tracking of expressions and functions that might call exit *)
- | BE_lset (* Local mutation happend; not user-writable *)
- | BE_lret (* Local return happened; not user-writable *)
-
-
-type
-base_effect =
-   BE_aux of base_effect_aux * l
-
-
-type
-order_aux =  (* vector order specifications, of kind Order *)
-   Ord_var of kid (* variable *)
- | Ord_inc (* increasing (little-endian) *)
- | Ord_dec (* decreasing (big-endian) *)
-
-
-type
-effect_aux =  (* effect set, of kind Effects *)
-   Effect_var of kid
- | Effect_set of (base_effect) list (* effect set *)
-
-
-type
-order =
-   Ord_aux of order_aux * l
-
-
-type
-effect =
-   Effect_aux of effect_aux * l
-
-
-type
-kinded_id_aux =  (* optionally kind-annotated identifier *)
-   KOpt_none of kid (* identifier *)
- | KOpt_kind of kind * kid (* kind-annotated variable *)
-
-
-type
-n_constraint_aux =  (* constraint over kind $_$ *)
-   NC_equal of nexp * nexp
- | NC_bounded_ge of nexp * nexp
- | NC_bounded_le of nexp * nexp
- | NC_not_equal of nexp * nexp
- | NC_set of kid * (int) list
- | NC_or of n_constraint * n_constraint
- | NC_and of n_constraint * n_constraint
- | NC_true
- | NC_false
-
-and
-n_constraint =
-   NC_aux of n_constraint_aux * l
-
-type
-kinded_id =
-   KOpt_aux of kinded_id_aux * l
-
-type
-quant_item_aux =  (* Either a kinded identifier or a nexp constraint for a typquant *)
-   QI_id of kinded_id (* An optionally kinded identifier *)
- | QI_const of n_constraint (* A constraint for this type *)
-
-
-type
-quant_item =
-   QI_aux of quant_item_aux * l
-
-
-type
-typquant_aux =  (* type quantifiers and constraints *)
-   TypQ_tq of (quant_item) list
- | TypQ_no_forall (* sugar, omitting quantifier and constraints *)
-
-
-type
-lit_aux =  (* Literal constant *)
-   L_unit (* $() : _$ *)
- | L_zero (* $_ : _$ *)
- | L_one (* $_ : _$ *)
- | L_true (* $_ : _$ *)
- | L_false (* $_ : _$ *)
- | L_num of int (* natural number constant *)
- | L_hex of string (* bit vector constant, C-style *)
- | L_bin of string (* bit vector constant, C-style *)
- | L_undef (* constant representing undefined values *)
- | L_string of string (* string constant *)
- | L_real of string
-
-type
-typquant =
-   TypQ_aux of typquant_aux * l
-
-type
-typ_aux =  (* Type expressions, of kind $_$ *)
-   Typ_wild (* Unspecified type *)
- | Typ_id of id (* Defined type *)
- | Typ_var of kid (* Type variable *)
- | Typ_fn of typ * typ * effect (* Function type (first-order only in user code) *)
- | Typ_tup of (typ) list (* Tuple type *)
- | Typ_app of id * (typ_arg) list (* type constructor application *)
- | Typ_exist of kid list * n_constraint * typ
-
-and typ =
-   Typ_aux of typ_aux * l
-
-and typ_arg_aux =  (* Type constructor arguments of all kinds *)
-   Typ_arg_nexp of nexp
- | Typ_arg_typ of typ
- | Typ_arg_order of order
-
-and typ_arg =
-   Typ_arg_aux of typ_arg_aux * l
-
-
-type
-lit =
-   L_aux of lit_aux * l
-
-
-type
-typschm_aux =  (* type scheme *)
-   TypSchm_ts of typquant * typ
-
-
-type
-'a pat_aux =  (* Pattern *)
-   P_lit of lit (* literal constant pattern *)
- | P_wild (* wildcard *)
- | P_as of 'a pat * id (* named pattern *)
- | P_typ of typ * 'a pat (* typed pattern *)
- | P_id of id (* identifier *)
- | P_var of 'a pat * kid (* bind pattern to type variable *)
- | P_app of id * ('a pat) list (* union constructor pattern *)
- | P_record of ('a fpat) list * bool (* struct pattern *)
- | P_vector of ('a pat) list (* vector pattern *)
- | P_vector_concat of ('a pat) list (* concatenated vector pattern *)
- | P_tup of ('a pat) list (* tuple pattern *)
- | P_list of ('a pat) list (* list pattern *)
- | P_cons of 'a pat * 'a pat
-
-and 'a pat =
-   P_aux of 'a pat_aux * 'a annot
-
-and 'a fpat_aux =  (* Field pattern *)
-   FP_Fpat of id * 'a pat
-
-and 'a fpat =
-   FP_aux of 'a fpat_aux * 'a annot
-
-
-type
-typschm =
-   TypSchm_aux of typschm_aux * l
-
-
-type
-'a reg_id_aux =
-   RI_id of id
-
-type loop = While | Until
-
-type
-'a exp_aux =  (* Expression *)
-   E_block of ('a exp) list (* block *)
- | E_nondet of ('a exp) list (* nondeterminisitic block, expressions evaluate in an unspecified order, or concurrently *)
- | E_id of id (* identifier *)
- | E_lit of lit (* literal constant *)
- | E_cast of typ * 'a exp (* cast *)
- | E_app of id * ('a exp) list (* function application *)
- | E_app_infix of 'a exp * id * 'a exp (* infix function application *)
- | E_tuple of ('a exp) list (* tuple *)
- | E_if of 'a exp * 'a exp * 'a exp (* conditional *)
- | E_for of id * 'a exp * 'a exp * 'a exp * order * 'a exp (* for loop *)
- | E_loop of loop * 'a exp * 'a exp
- | E_vector of ('a exp) list (* vector (indexed from 0) *)
- | E_vector_access of 'a exp * 'a exp (* vector access *)
- | E_vector_subrange of 'a exp * 'a exp * 'a exp (* subvector extraction *)
- | E_vector_update of 'a exp * 'a exp * 'a exp (* vector functional update *)
- | E_vector_update_subrange of 'a exp * 'a exp * 'a exp * 'a exp (* vector subrange update (with vector) *)
- | E_vector_append of 'a exp * 'a exp (* vector concatenation *)
- | E_list of ('a exp) list (* list *)
- | E_cons of 'a exp * 'a exp (* cons *)
- | E_record of 'a fexps (* struct *)
- | E_record_update of 'a exp * 'a fexps (* functional update of struct *)
- | E_field of 'a exp * id (* field projection from struct *)
- | E_case of 'a exp * ('a pexp) list (* pattern matching *)
- | E_let of 'a letbind * 'a exp (* let expression *)
- | E_assign of 'a lexp * 'a exp (* imperative assignment *)
- | E_sizeof of nexp (* Expression to return the value of the nexp variable or expression at run time *)
- | E_constraint of n_constraint (* Expression to evaluate the n_constraint at run time *)
- | E_exit of 'a exp (* expression to halt all current execution, potentially calling a system, trap, or interrupt handler with exp *)
- | E_throw of 'a exp
- | E_try of 'a exp * ('a pexp) list
- | E_return of 'a exp (* expression to end current function execution and return the value of exp from the function; this can be used to break out of for loops *)
- | E_assert of 'a exp * 'a exp (* expression to halt with error, when the first expression is false, reporting the optional string as an error *)
- | E_internal_cast of 'a annot * 'a exp (* This is an internal cast, generated during type checking that will resolve into a syntactic cast after *)
- | E_internal_exp of 'a annot (* This is an internal use for passing nexp information  to library functions, postponed for constraint solving *)
- | E_sizeof_internal of 'a annot (* For sizeof during type checking, to replace nexp with internal n *)
- | E_internal_exp_user of 'a annot * 'a annot (* This is like the above but the user has specified an implicit parameter for the current function *)
- | E_comment of string (* For generated unstructured comments *)
- | E_comment_struc of 'a exp (* For generated structured comments *)
- | E_internal_let of 'a lexp * 'a exp * 'a exp (* This is an internal node for compilation that demonstrates the scope of a local mutable variable *)
- | E_internal_plet of 'a pat * 'a exp * 'a exp (* This is an internal node, used to distinguised some introduced lets during processing from original ones *)
- | E_internal_return of 'a exp (* For internal use to embed into monad definition *)
-
-and 'a exp =
-   E_aux of 'a exp_aux * 'a annot
-
-and 'a lexp_aux =  (* lvalue expression *)
-   LEXP_id of id (* identifier *)
- | LEXP_memory of id * ('a exp) list (* memory write via function call *)
- | LEXP_cast of typ * id
- | LEXP_tup of ('a lexp) list (* set multiple at a time, a check will ensure it's not memory *)
- | LEXP_vector of 'a lexp * 'a exp (* vector element *)
- | LEXP_vector_range of 'a lexp * 'a exp * 'a exp (* subvector *)
- | LEXP_field of 'a lexp * id (* struct field *)
-
-and 'a lexp =
-   LEXP_aux of 'a lexp_aux * 'a annot
-
-and 'a fexp_aux =  (* Field-expression *)
-   FE_Fexp of id * 'a exp
-
-and 'a fexp =
-   FE_aux of 'a fexp_aux * 'a annot
-
-and 'a fexps_aux =  (* Field-expression list *)
-   FES_Fexps of ('a fexp) list * bool
-
-and 'a fexps =
-   FES_aux of 'a fexps_aux * 'a annot
-
-and 'a opt_default_aux =  (* Optional default value for indexed vectors, to define a defualt value for any unspecified positions in a sparse map *)
-   Def_val_empty
- | Def_val_dec of 'a exp
-
-and 'a opt_default =
-   Def_val_aux of 'a opt_default_aux * 'a annot
-
-and 'a pexp_aux =  (* Pattern match *)
-  Pat_exp of 'a pat * 'a exp
-| Pat_when of 'a pat * 'a exp * 'a exp
-
-and 'a pexp =
-   Pat_aux of 'a pexp_aux * 'a annot
-
-and 'a letbind_aux =  (* Let binding *)
-   LB_val of 'a pat * 'a exp (* value binding, implicit type ('a pat must be total) *)
-
-and 'a letbind =
-   LB_aux of 'a letbind_aux * 'a annot
-
-
-type
-'a reg_id =
-   RI_aux of 'a reg_id_aux * 'a annot
-
-
-type
-type_union_aux =  (* Type union constructors *)
-   Tu_id of id
- | Tu_ty_id of typ * id
-
-
-type
-name_scm_opt_aux =  (* Optional variable-naming-scheme specification for variables of defined type *)
-   Name_sect_none
- | Name_sect_some of string
-
-
-type
-effect_opt_aux =  (* Optional effect annotation for functions *)
-   Effect_opt_pure (* sugar for empty effect set *)
- | Effect_opt_effect of effect
-
-
-type
-'a funcl_aux =  (* Function clause *)
-   FCL_Funcl of id * 'a pat * 'a exp
-
-
-type
-rec_opt_aux =  (* Optional recursive annotation for functions *)
-   Rec_nonrec (* non-recursive *)
- | Rec_rec (* recursive *)
-
-
-type
-tannot_opt_aux =  (* Optional type annotation for functions *)
-   Typ_annot_opt_some of typquant * typ
- | Typ_annot_opt_none
-
-type
-'a alias_spec_aux =  (* Register alias expression forms. Other than where noted, each id must refer to an unaliased register of type vector *)
-   AL_subreg of 'a reg_id * id
- | AL_bit of 'a reg_id * 'a exp
- | AL_slice of 'a reg_id * 'a exp * 'a exp
- | AL_concat of 'a reg_id * 'a reg_id
-
-
-type
-type_union =
-   Tu_aux of type_union_aux * l
-
-
-type
-index_range_aux =  (* index specification, for bitfields in register types *)
-   BF_single of int (* single index *)
- | BF_range of int * int (* index range *)
- | BF_concat of index_range * index_range (* concatenation of index ranges *)
-
-and index_range =
-   BF_aux of index_range_aux * l
-
-
-type
-name_scm_opt =
-   Name_sect_aux of name_scm_opt_aux * l
-
-
-type
-effect_opt =
-   Effect_opt_aux of effect_opt_aux * l
-
-
-type
-'a funcl =
-   FCL_aux of 'a funcl_aux * 'a annot
-
-
-type
-rec_opt =
-   Rec_aux of rec_opt_aux * l
-
-
-type
-tannot_opt =
-   Typ_annot_opt_aux of tannot_opt_aux * l
-
-
-type
-'a alias_spec =
-   AL_aux of 'a alias_spec_aux * 'a annot
-
-
-type
-default_spec_aux =  (* Default kinding or typing assumption *)
-   DT_kind of base_kind * kid
- | DT_order of order
- | DT_typ of typschm * id
-
-
-type
-type_def_aux =  (* Type definition body *)
-   TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *)
- | TD_record of id * name_scm_opt * typquant * ((typ * id)) list * bool (* struct type definition *)
- | TD_variant of id * name_scm_opt * typquant * (type_union) list * bool (* union type definition *)
- | TD_enum of id * name_scm_opt * (id) list * bool (* enumeration type definition *)
- | TD_register of id * nexp * nexp * ((index_range * id)) list (* register mutable bitfield type definition *)
-
-
-type
-val_spec_aux =  (* Value type specification *)
-   VS_val_spec of typschm * id * string option * bool
-
-type
-'a kind_def_aux =  (* Definition body for elements of kind; many are shorthands for type\_defs *)
-   KD_nabbrev of kind * id * name_scm_opt * nexp (* nexp abbreviation *)
-
-type
-'a scattered_def_aux =  (* Function and type union definitions that can be spread across
-         a file. Each one must end in $_$ *)
-   SD_scattered_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *)
- | SD_scattered_funcl of 'a funcl (* scattered function definition clause *)
- | SD_scattered_variant of id * name_scm_opt * typquant (* scattered union definition header *)
- | SD_scattered_unioncl of id * type_union (* scattered union definition member *)
- | SD_scattered_end of id (* scattered definition end *)
-
-
-type
-'a fundef_aux =  (* Function definition *)
-   FD_function of rec_opt * tannot_opt * effect_opt * ('a funcl) list
-
-
-type
-'a dec_spec_aux =  (* Register declarations *)
-   DEC_reg of typ * id
- | DEC_alias of id * 'a alias_spec
- | DEC_typ_alias of typ * id * 'a alias_spec
-
-
-type default_spec =
-   DT_aux of default_spec_aux * l
-
-
-type
-'a type_def =
-   TD_aux of type_def_aux * 'a annot
-
-
-type
-'a val_spec =
-   VS_aux of val_spec_aux * 'a annot
-
-
-type
-'a kind_def =
-   KD_aux of 'a kind_def_aux * 'a annot
-
-
-type
-'a scattered_def =
-   SD_aux of 'a scattered_def_aux * 'a annot
-
-
-type
-'a fundef =
-   FD_aux of 'a fundef_aux * 'a annot
-
-
-type
-'a dec_spec =
-   DEC_aux of 'a dec_spec_aux * 'a annot
-
-type prec = Infix | InfixL | InfixR
-
-type
-'a dec_comm =  (* Top-level generated comments *)
-   DC_comm of string (* generated unstructured comment *)
- | DC_comm_struct of 'a def (* generated structured comment *)
-
-and 'a def =  (* Top-level definition *)
-   DEF_kind of 'a kind_def (* definition of named kind identifiers *)
- | DEF_type of 'a type_def (* type definition *)
- | DEF_fundef of 'a fundef (* function definition *)
- | DEF_val of 'a letbind (* value definition *)
- | DEF_spec of 'a val_spec (* top-level type constraint *)
- | DEF_fixity of prec * int * id (* fixity declaration *)
- | DEF_overload of id * id list (* operator overload specification *)
- | DEF_default of default_spec (* default kind and type assumptions *)
- | DEF_scattered of 'a scattered_def (* scattered function and type definition *)
- | DEF_reg_dec of 'a dec_spec (* register declaration *)
- | DEF_comm of 'a dec_comm (* generated comments *)
-
-type
-'a defs =  (* Definition sequence *)
-   Defs of ('a def) list
-
-
-
diff --git a/src/ast.ott b/src/ast.ott
new file mode 100644
index 00000000..f08b089b
--- /dev/null
+++ b/src/ast.ott
@@ -0,0 +1,1180 @@
+%%
+%% 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]}$} }}       
+
+