Merge remote-tracking branch 'origin/sail2' into c_fixes

9 files changed, 0 insertions, 4000 deletions

diff --git a/language/Makefile b/language/Makefile
deleted file mode 100644
index 759523b7..00000000
--- a/language/Makefile
+++ /dev/null
@@ -1,54 +0,0 @@
-#OTT=../../../rsem/ott/bin/ott
-# this is the binary that gets rebuilt by make in ott/src:
-OTT=../../ott/src/ott
-OTTLIB=$(dir $(shell which ott))../hol
-
-.PHONY: all
-all: l2.ml l2_parse.ml l2.lem l2_parse2.ml l2_parse2_parser.mly
-
-docs: l2.pdf l2_parse.pdf 
-
-%.pdf: %.tex
-	pdflatex $<
-
-%Theory.uo: %Script.sml
-	Holmake --qof -I $(OTTLIB) $@
-
-type_system.pdf: doc_in.tex type_system.tex
-	pdflatex type_system.tex
-	pdflatex type_system.tex
-
-l2.tex: l2.ott  l2_rules.ott # l2_terminals_non_tt.ott  l2_typ.ott l2_rules.ott
-	$(OTT) -sort false -generate_aux_rules false -o $@ -picky_multiple_parses true $^
-
-doc_in.tex: l2.ott primitive_doc.ott l2_terminals_tt.ott l2_typ.ott l2_rules.ott
-	$(OTT) -sort false -generate_aux_rules false -tex_wrap false -o $@ -picky_multiple_parses true $^
-
-%.tex: %.ott
-	$(OTT) -sort false -generate_aux_rules false -o $@ -picky_multiple_parses true $^
-
-%.ml: %.ott
-	$(OTT) -sort false -generate_aux_rules true -o $@ -picky_multiple_parses true $^
-
-%Script.sml: %.ott
-	$(OTT) -sort false -generate_aux_rules true -o $@ -picky_multiple_parses true $^
-
-l2.lem: l2.ott
-	$(OTT) -sort false -generate_aux_rules true -o $@ -picky_multiple_parses true $^
-
-ROOT=l2_parse2
-# generate the ocaml AST type, ocamllex lexer, menhir parser, and ocaml pretty printers for the AST, all from the Ott soruce
-$(ROOT)_ast.ml  $(ROOT)_lexer.mll $(ROOT)_parser.mly $(ROOT)_parser_pp.ml $(ROOT)_ast.tex : $(ROOT).ott Makefile
-	$(OTT) -quotient_rules false -generate_aux_rules false -i $(ROOT).ott  -o $(ROOT)_parser.mly -o $(ROOT)_lexer.mll -o $(ROOT)_ast.ml -o $(ROOT).tex
-
-
-clean:
-	rm -rf *~
-	rm -rf *.uo *.ui *.sig *.sml .HOLMK
-	rm -f *.aux *.log *.dvi *.ps *.pdf *.toc
-	rm -rf l2.pdf l2_parse.pdf 
-	rm -rf l2.tex doc_in.tex
-
-realclean:
-	$(MAKE) clean
-	rm -rf l2.ml l2_parse.ml l2.lem
diff --git a/language/l2_parse.ott b/language/l2_parse.ott
deleted file mode 100644
index 49df4908..00000000
--- a/language/l2_parse.ott
+++ /dev/null
@@ -1,1407 +0,0 @@
-indexvar n , i , j , k ::=
-  {{ phantom }}
-  {{ com Index variables for meta-lists }}
-
-metavar num ::=
-  {{ phantom }}
-  {{ lex numeric }}
-  {{ ocaml int }}
-  {{ hol num }}
-  {{ lem integer }}
-  {{ com Numeric literals }}
-
-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 }}
-
-embed
-{{ ocaml
-
-type l =
-  | Unknown
-  | Int of string * l option
-  | Generated of l
-  | Range of Lexing.position * Lexing.position
-
-type 'a annot = l * 'a
-
-exception Parse_error_locn of l * string
-
-}}
-
-embed
-{{ lem
-open import Map
-open import Maybe
-open import Pervasives
-
-type l =
-  | Unknown
-  | Trans of string * maybe l
-  | Range of nat * nat
-
-val duplicates : forall 'a. list 'a -> list 'a
-
-val union_map : forall 'a 'b. map 'a 'b -> map 'a 'b -> map 'a 'b
-
-val set_from_list : forall 'a. list 'a -> set 'a
-
-val subst : forall 'a. list 'a -> list 'a -> bool
-
-}}
-
-metavar x , y , z ::=
-  {{ ocaml string }}
-  {{ lem string }}
-  {{ hol string }}
-  {{ com identifier }}
-  {{ ocamlvar "[[x]]" }}
-  {{ lemvar "[[x]]" }}
-
-metavar ix ::=
-  {{ lex alphanum }}
-  {{ ocaml string }}
-  {{ lem string }}
-  {{ hol string }}
-  {{ com infix identifier }}
-  {{ ocamlvar "[[ix]]" }}
-  {{ lemvar "[[ix]]" }}
-
-
-
-grammar
-
-l :: '' ::=                                     {{ phantom }}
-                                                {{ ocaml l }}
-                                                {{ lem l }}
-                                                {{ hol unit }}
-  {{ com Source location }}
-  |                                             :: :: Unknown
-    {{ ocaml Unknown }}
-    {{ lem Unknown }}
-    {{ hol () }}
-
-
-id :: '' ::=
-  {{ com Identifier }}
-  {{ aux _ l }}
-  | x                           :: :: id
-  | ( deinfix x )                       :: :: deIid {{ com remove infix status }}
-
-
-kid :: '' ::=
-  {{ com identifiers with kind, ticked to differntiate from program variables }}
-  {{ aux _ l }}
-  | ' x                       :: :: var
-
-% 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. 
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% 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  }} 
-  | Effect                                    :: :: effect {{ com kind of effect sets  }} 
-
-kind :: 'K_' ::=  
-  {{ com kinds}}
-  {{ aux _ l }}
-  | base_kind1 -> ... -> base_kindn            :: :: kind 
-% we'll never use  ...-> Nat
-
-base_effect :: 'BE_' ::=
-  {{ com effect }}
-  {{ aux _ l }}  
-  | rreg                                :: :: rreg {{ com read register }}
-  | wreg                                :: :: wreg {{ com write register }}
-  | rmem                                :: :: rmem {{ com read memory }}
-  | wmem                                :: :: wmem {{ com write memory }}
-  | wmv					:: :: wmv {{ com write memory value }}
-  | eamem				:: :: eamem {{ com address for write signaled }}
-  | barr                                :: :: barr {{ com memory barrier }}
-  | depend				:: :: depend {{ com dynmically dependent footprint }}
-  | undef                               :: :: undef {{ com undefined-instruction exception }}
-  | unspec                              :: :: unspec {{ com unspecified values }}
-  | nondet                              :: :: nondet {{ com nondeterminism from intra-instruction parallelism }}
-  | escape                              :: :: escape
-
-atyp :: 'ATyp_' ::=
-  {{ com expressions of all kinds, to be translated to types, nats, orders, and effects after parsing }}
-  {{ aux _ l }}
-  | id                                  :: :: id          {{ com identifier }}
-  | kid                                 :: :: var         {{ com ticked variable }}
-  | num                                 :: :: constant     {{ com constant }}
-  | atyp1 * atyp2                       :: :: times        {{ com product }}
-  | atyp1 + atyp2                       :: :: sum          {{ com sum }}
-  | atyp1 - atyp2                        :: :: minus	     {{ com subtraction }}
-  | 2** atyp                            :: :: exp         {{ com exponential }}
-  | neg atyp				:: :: neg	  {{ com Internal (but not M as I want a datatype constructor) negative nexp }}
-  | ( atyp )                            :: S :: paren  {{ icho [[atyp]] }}
-
-  | inc                                 :: :: inc  {{ com increasing (little-endian) }}
-  | dec                                 :: :: dec  {{ com decreasing (big-endian) }}
-  | defaultOrd                          :: :: default_ord {{ com default order for increasing or decreasing signficant bits }}
-  | { base_effect1 , .. , base_effectn }           :: :: set {{ com effect set }}
-  | pure                                 :: M :: pure {{ com sugar for empty effect set }} {{ icho [] }}
-  | atyp1 -> atyp2 effect atyp3                        :: :: fn
-    {{ com Function type (first-order only in user code), last atyp is an effect }}
-  | ( atyp1 , .... , atypn )                        :: :: tup
-    {{ com Tuple type }}
-  | id < atyp1 , .. , atypn >                    :: :: app
-  {{ com type constructor application }}
-
-
-% 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
-%  | enum nexp1 nexp2 order :: :: enum  {{ com natural numbers [[atyp2]] .. [[atyp2]]+[[atyp1]]-1, ordered by order }}
-%  | [ nexp ]             :: :: enum1 {{ com sugar for \texttt{enum nexp 0 inc} }}
-%  | [ nexp : nexp' ]  :: :: enum2 {{ com sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} }}
-% use .. not - to avoid ambiguity with nexp -
-% total maps and vectors indexed by finite subranges of nat
-%  | vector nexp1 nexp2 order atyp :: :: vector {{ com vector of [[atyp]], indexed by natural range }}
-% probably some sugar for vector types, using [ ] similarly to enums:
-% (but with .. not : in the former, to avoid confusion...)
-%  | atyp [ nexp ]  :: :: vector2 {{ com sugar for vector indexed by [ [[atyp]] ] }}
-%  | atyp [ nexp : nexp' ] :: :: vector3 {{ com sugar for vector indexed by [ [[atyp]]..[[atyp']] ] }}
-% ...so bit [ nexp ] etc is just an instance of that
-%  | list atyp :: :: list {{ com list of [[atyp]] }}
-%  | set atyp  :: :: set  {{ com finite set of [[atyp]] }}
-%  | reg atyp  :: :: reg  {{ com mutable register components holding [[atyp]] }}
-% "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 
-
-parsing
-
-ATyp_tup <= ATyp_tup
-ATyp_fn right ATyp_fn
-ATyp_fn <= ATyp_tup
-
-grammar
-
-n_constraint :: 'NC_' ::=
-  {{ com constraint over kind $[[Nat]]$ }}
-  {{ aux _ l }}
-  | atyp = atyp'                                :: :: fixed
-  | atyp >= atyp'                               :: :: bounded_ge
-  | atyp '<=' atyp'                             :: :: bounded_le
-  | kid 'IN' { num1 , ... , numn }               :: :: nat_set_bounded
-
-% 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 Either a kinded identifier or a nexp constraint for a typquant }}
-  {{ aux _ l }}
-  | kinded_id 	  	 	       	      :: :: id {{ com An optionally kinded identifier }}
-  | n_constraint			      :: :: const {{ com A constraint for this type }}
-
-typquant :: 'TypQ_' ::= 
-  {{ com type quantifiers and constraints}}
-  {{ aux _ l }}
-  | forall quant_item1 , ... , quant_itemn . :: :: tq {{ texlong }}
-  |                           ::  ::  no_forall     {{ com sugar, omitting quantifier and constraints }}
-
-typschm :: 'TypSchm_' ::=
-  {{ com type scheme  }}
-  {{ aux _ l }}
-  |  typquant atyp                                                       :: :: ts
-
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% Type definitions                                             %
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-grammar
-%ctor_def :: 'CT_' ::=
-%  {{ com Datatype constructor definition clause }}
-%  {{ aux _ l }}
-%  | id : typschm                                       :: :: ct
-% but we could get away with disallowing constraints in typschm, we
-% think - if it's useful to do that
-
- name_scm_opt :: 'Name_sect_' ::=
-   {{ com Optional variable-naming-scheme specification for variables of defined type }} 
-   {{ aux _ l }}
-   |                                                   :: :: none
-   | [ name = regexp ]                                 :: :: some
-
-type_union :: 'Tu_' ::=
-  {{ com Type union constructors }}
-  {{ aux _ l }}
-  | id                                                  :: :: id
-  | atyp id                                             :: :: ty_id
-
-type_def :: 'TD_' ::=
-  {{ com Type definition body }}
-  {{ aux _ l }}
-  | typedef id name_scm_opt = typschm                                        :: :: abbrev
-    {{ com type abbreviation }} {{ texlong }}
-  | typedef id name_scm_opt = const struct typquant { atyp1 id1 ; ... ; atypn idn semi_opt }     :: :: record
-    {{ com struct type definition }} {{ texlong }}
-  | typedef id name_scm_opt = const union typquant { type_union1 ; ... ; type_unionn semi_opt }   :: :: variant
-    {{ com union type definition}} {{ texlong }}
-  | typedef id name_scm_opt = enumerate { id1 ; ... ; idn semi_opt }   :: :: enum
-    {{ com enumeration type definition}} {{ texlong }}
-
-  | typedef id = register bits [ atyp : atyp' ] { index_range1 : id1 ; ... ; index_rangen : idn } 
-:: :: register {{ com register mutable bitfield type definition }} {{ texlong }}
-
-kind_def :: 'KD_' ::=
-  {{ com Definition body for elements of kind; many are shorthands for type\_defs }}
-  {{ aux _ l }}
-  | Def kind id name_scm_opt = typschm                                        :: :: abbrev
-    {{ com type abbreviation }} {{ texlong }}
-  | Def kind id name_scm_opt = const struct typquant { atyp1 id1 ; ... ; atypn idn semi_opt }     :: :: record
-    {{ com struct type definition }} {{ texlong }}
-  | Def kind id name_scm_opt = const union typquant { type_union1 ; ... ; type_unionn semi_opt }   :: :: variant
-    {{ com union type definition}} {{ texlong }}
-  | Def kind id name_scm_opt = enumerate { id1 ; ... ; idn semi_opt }   :: :: enum
-    {{ com enumeration type definition}} {{ texlong }}
-
-  | Def kind id = register bits [ atyp : atyp' ] { index_range1 : id1 ; ... ; index_rangen : idn } 
-:: :: register {{ com register mutable bitfield type definition }} {{ texlong }}
-
-
-% also sugar [  nexp ] 
-
-
-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 }}
-  | undefined					:: :: undef {{ com undefined value }}
-  | string                                              :: :: string {{ com string constant }}
-
-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 _ l }}
-  | lit                                                 :: :: lit
-    {{ com literal constant pattern }}
-  | _                                                   :: :: wild  
-    {{ com wildcard }}
-  | ( pat as id )                                      :: :: as
-    {{ com named pattern }}
-  | ( atyp ) pat                                       :: :: typ
-    {{ com typed pattern }}
-
-  | id                                      :: :: id
-    {{ com identifier  }}
-
-  | id ( pat1 , .. , patn )                                     :: :: app
-    {{ com union constructor pattern }}
-
-  | { fpat1 ; ... ; fpatn semi_opt }                  :: :: record
-    {{ com struct pattern }}
-
-  | [ pat1 , .. , patn  ]                     :: :: vector
-   {{ com vector pattern }}
-
-  | [ num1 = pat1 , .. , numn = patn  ]                     :: :: vector_indexed
-   {{ com vector pattern (with explicit indices) }}
-
-  |  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]] }}
-
-fpat :: 'FP_' ::=
-  {{ com Field pattern }}
-  {{ aux _ l }}
-  | id = pat                                            :: :: Fpat
-
-parsing
-P_app <= P_app
-P_app <= P_as
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% Expressions                                                  %
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-
-
-grammar
-
-exp :: 'E_' ::=
-  {{ com Expression }}
-  {{ aux _ l }}
-
-  | { exp1 ; ... ; expn }                               :: :: block {{ com block (parsing conflict with structs?) }}
-% maybe we really should have indentation-sensitive syntax :-)  (given that some of the targets do)
-
-  | nondet { exp1 ; ... ; expn }                        :: :: nondet {{ com block that can evaluate the contained expressions in any ordering }}
-
-  | id                                                  :: :: id
-    {{ com identifier }}
-
-  | lit                                                 :: :: lit
-    {{ com literal constant }}
-
-  | ( atyp ) exp                                         :: :: cast
-    {{ com cast }}
-
-
-  | id exp                                               :: S :: tup_app {{ ichlo [[id ( exp ) ]] }} {{ com No extra parens needed when exp is a tuple }}
-  | id ( exp1 , .. , expn )                                   :: :: app
-    {{ com function application }}
-% 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 {{ icho [[ if exp1 then exp2 else unit ]] }}
-
-  | foreach id from exp1 to exp2 by exp3 in atyp 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  {{ icho [[ foreach id from exp1 to exp2 by 1 exp4 ]] }}
-  | foreach id from exp1 downto exp2 by exp3 exp4       :: S :: fordown {{ icho [[ foreach id from exp1 to exp2 by ( - exp3 ) exp4 ]] }}
-  | foreach id from exp1 downto exp2 exp3               :: S :: fordownbyone  {{ icho [[ foreach id from exp1 downto exp2 by 1 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 
-
-  | [ exp1 , ... , 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 exp1 ; .. ; expn }                                :: :: 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 }}
-  | letbind in exp                                  :: :: let
-    {{ com let expression }}
-
-  | exp := exp'                                      :: :: assign
-    {{ com imperative assignment }}
-
-  | sizeof atyp                                         :: :: sizeof
-  | exit exp						:: :: exit
-  | return exp                                          :: :: return
-  | assert ( exp , exp' )                               :: :: assert
-
-  | ( exp )                                             :: S :: paren {{ ichlo [[exp]] }}
-
-
-lexp :: 'LEXP_' ::= {{ com lvalue expression, can't occur out of the parser }}
-    {{ aux _ l }}
-%    {{ aux _ annot }} {{ auxparam 'a }}
-    | id                                                  :: :: id
-    {{ com identifier }}
-    | id ( exp1 , .. , expn )				  :: :: mem
-    | id exp	       	    				  :: S :: mem_tup {{ ichlo [[id (exp)]] }}
-    | 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 _ l }} 
-%  {{ aux _ annot }} {{ auxparam 'a }}
-  | id = exp                                            :: :: Fexp
-
-fexps :: 'FES_' ::=
-  {{ com Field-expression list }}
-  {{ aux _ l }}
-%  {{ aux _ annot }} {{ auxparam 'a }}
-  | fexp1 ; ... ; fexpn semi_opt                        :: :: Fexps
-
-opt_default :: 'Def_val_' ::=
-  {{ com Optional default value for indexed vectors, to define a defualt value for any unspecified positions in a sparse map }}
-  {{ aux _ l }} 
-  |                                                     :: :: empty
-  | ; default = exp                                       :: :: dec
-
-pexp :: 'Pat_' ::=
-  {{ com Pattern match }}
-  {{ aux _ l }}
-%  {{ aux _ annot }} {{ auxparam 'a }}
-  | pat -> exp                                  :: :: exp
-% 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 }}
-%  {{ aux _ annot }} {{ auxparam 'a }}
-  |                                             :: :: none
-  | typquant atyp                               :: :: 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 }}
-%  {{ aux _ annot }} {{ auxparam 'a }}
-  |                                             :: :: pure {{ com sugar for empty effect set }}
-  | effectkw atyp                                     :: :: effect
-
-funcl :: 'FCL_' ::=
-  {{ com Function clause }}
-  {{ aux _ l }}
-%  {{ aux _ annot }} {{ auxparam 'a }}
-  | id pat = exp                   :: :: Funcl
-
-
-fundef :: 'FD_' ::=
-  {{ com Function definition}}
-  {{ aux _ l }}
-%  {{ 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 _ l }}
-%  {{ aux _ annot }} {{ auxparam 'a }}
-  | let typschm pat = exp                                :: :: val_explicit
-    {{ com value binding, explicit type ([[pat]] must be total)}}
-  | let pat = exp                                    :: :: val_implicit
-    {{ com value binding, implicit type ([[pat]] must be total)}}
-
-
-val_spec :: 'VS_' ::=
-  {{ com Value type specification }} 
-  {{ aux _ l }}
-%  {{ aux _ annot }} {{ auxparam 'a }}
-  | val typschm id                                  :: :: val_spec
-  | val extern typschm id                           :: :: extern_no_rename
-  | val extern typschm id = string                  :: :: extern_spec
-
-default_typing_spec :: 'DT_' ::=
-  {{ com Default kinding or typing assumption, and default order for literal vectors and vector shorthands }}
-  {{ aux _ l }}
-%  {{ aux _ annot }} {{ auxparam 'a }}
-  | default base_kind kid    :: :: kind
-  | default base_kind atyp   :: :: order
-  | 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 Function and type union definitions that can be spread across
-         a file. Each one must end in $[[end id]]$ }}
-  {{ aux _ l }} 
-  | scattered function rec_opt tannot_opt effect_opt id   :: :: scattered_function {{ texlong }} {{ com scattered function definition header }}
-
-  | function clause funcl  :: :: scattered_funcl  
-{{ 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 {{ com scattered union definition member }}
-  | end id  :: :: scattered_end
-{{ com scattered definition end }}
-
-dec_spec :: 'DEC_' ::=
-  {{ com Register declarations }}
-  {{ aux _ l }}
-  | register atyp id                                             :: :: reg
-  | register alias id = exp	      	 			 :: :: alias
-  | register alias atyp id = exp	  			 :: :: typ_alias
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% Top-level definitions                                        %
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-def :: 'DEF_' ::=
-  {{ com Top-level definition }}
-  | 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 }}
-  | default_typing_spec                                         :: :: default
-    {{ com default kind and type assumptions }}
-  | scattered_def					:: :: scattered
-    {{ com scattered definition }} 
-  | dec_spec                                            :: :: reg_dec
-    {{ com register declaration }}
-
-defs :: '' ::=
-  {{ com Definition sequence }}
-  | def1  .. defn                 :: :: Defs
-
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% Machinery for typing rules                                   %
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%% %% 
-%% %% 
-%% %% grammar
-%% %% 
-%% %% 
-%% %% p :: 'Path_' ::=
-%% %%   {{ com Unique paths }}
-%% %%   | x1 . .. xn . x                              :: :: def
-%% %%   | __list                                      :: :: list      
-%% %%     {{ tex \ottkw{\_\_list}  }}
-%% %%   | __bool                                      :: :: bool
-%% %%     {{ tex \ottkw{\_\_bool}  }}
-%% %%   | __num                                       :: :: num
-%% %%     {{ tex \ottkw{\_\_num}  }}
-%% %%   | __set                                       :: :: set
-%% %%     {{ tex \ottkw{\_\_set}  }}
-%% %%   | __string                                    :: :: string
-%% %%     {{ tex \ottkw{\_\_string}  }}
-%% %%   | __unit                                      :: :: unit
-%% %%     {{ tex \ottkw{\_\_unit}  }}
-%% %%   | __bit                                       :: :: bit
-%% %%     {{ tex \ottkw{\_\_bit}  }}
-%% %%   | __vector                            :: :: vector
-%% %%     {{ tex \ottkw{\_\_vector} }}                
-%% %% %TODO morally, delete the above - but what are the __ things for?
-%% %% % cleaner to declare early in the library?
-%% %% 
-%% %% t_subst {{ tex \ensuremath{\sigma} }} :: '' ::= {{ phantom }}
-%% %%                                                 {{ hol (a # t) list }}
-%% %%                                                 {{ lem list (tnvar * t) }}
-%% %%   {{ com Type variable substitutions }}
-%% %%   | { tnvar1 |-> t1 .. tnvarn |-> tn }                  :: :: T_subst
-%% %%     {{ ocaml (assert false) }}
-%% %%     {{ lem ([[tnvar1 t1 .. tnvarn tn]]) }}
-%% %%     {{ hol ([[tnvar1 t1 .. tnvarn tn]]) }}
-%% %% 
-%% %% t , u :: 'T_' ::=
-%% %%   {{ com Internal types }}
-%% %%   | a                                           :: :: var
-%% %%   | t1 -> t2                                    :: :: fn
-%% %%   | t1 * .... * tn                              :: :: tup
-%% %%   | p t_args                                    :: :: app 
-%% %%   | ne                                          :: :: len
-%% %%   | t_subst ( t )                               :: M :: subst_app
-%% %%     {{ com Multiple substitutions }}
-%% %%     {{ ocaml (assert false) }}
-%% %%     {{ hol (t_subst_t [[t_subst]] [[t]]) }}
-%% %%     {{ lem (t_subst_t [[t_subst]] [[t]]) }}
-%% %%   | t_subst ( tnv )                     :: M :: var_subst_app
-%% %%     {{ com Single variable substitution }}
-%% %%     {{ ocaml (assert false) }}
-%% %%     {{ hol (t_subst_tnv [[t_subst]] [[tnv]]) }}
-%% %%     {{ lem (t_subst_tnv [[t_subst]] [[tnv]]) }}
-%% %%   | curry ( t_multi ,  t )                      :: M :: multifn
-%% %%     {{ com Curried, multiple argument functions }}
-%% %%     {{ ocaml (assert false) }}
-%% %%     {{ hol (FOLDR T_fn [[t]] [[t_multi]]) }}
-%% %%     {{ lem (List.fold_right T_fn [[t_multi]] [[t]]) }}
-%% %% 
-%% %% ne :: 'Ne_' ::=
-%% %%   {{ com internal numeric expressions }}
-%% %%   | N                                           :: :: var
-%% %%   | nat                                 :: :: const
-%% %%   | ne1 * ne2                           :: :: mult
-%% %%   | ne1 + ne2                           :: :: add
-%% %%   | ( - ne )                            :: :: unary
-%% %%   | normalize ( ne )                    :: M :: normalize
-%% %%     {{ ocaml (assert false) }}
-%% %%     {{ hol ARB }}
-%% %%     {{ lem (normalize [[ne]] ) }}
-%% %%   | ne1 + ... + nen                     :: M :: addmany
-%% %%     {{ ocaml (assert false) }}
-%% %%     {{ hol ARB }}
-%% %%     {{ lem (sumation_nes [[ne1...nen]]) }}
-%% %%   | bitlength ( bin )                   :: M :: cbin
-%% %%     {{ ocaml (asssert false) }}
-%% %%     {{ hol ARB }}
-%% %%     {{ lem (blength [[bin]]) }}
-%% %%   | bitlength ( hex )                   :: M :: chex
-%% %%     {{ ocaml (assert false) }}
-%% %%     {{ hol ARB }}
-%% %%     {{ lem (hlength [[hex]]) }}
-%% %%   | length ( pat1 ... patn )            :: M :: cpat
-%% %%     {{ ocaml (assert false) }}
-%% %%     {{ hol ARB }}
-%% %%     {{ lem (Ne_const (List.length [[pat1...patn]])) }}
-%% %%   | length ( exp1 ... expn )            :: M :: cexp
-%% %%     {{ hol ARB }}
-%% %%     {{ ocaml (assert false) }}
-%% %%     {{ lem (Ne_const (List.length [[exp1...expn]])) }}
-%% %% 
-%% %% t_args :: '' ::=
-%% %%   {{ com Lists of types }}
-%% %%   | t1 .. tn                            :: :: T_args
-%% %%   | t_subst ( t_args )                          :: M :: T_args_subst_app
-%% %%     {{ com Multiple substitutions }}
-%% %%     {{ ocaml (assert false) }}
-%% %%     {{ hol (t_subst_t_args [[t_subst]] [[t_args]]) }}
-%% %%     {{ lem (t_subst_t_args [[t_subst]] [[t_args]]) }}
-%% %% 
-%% %% t_multi :: '' ::=                               {{ phantom }}
-%% %%                                                 {{ hol t list }}
-%% %%                                                 {{ ocaml t list }}
-%% %%                                                 {{ lem list t }}
-%% %%   {{ com Lists of types }}
-%% %%   | ( t1 * .. * tn )                            :: :: T_multi
-%% %%     {{ hol [[t1..tn]] }}
-%% %%     {{ lem [[t1..tn]] }}
-%% %%   | t_subst ( t_multi )                         :: M :: T_multi_subst_app
-%% %%     {{ com Multiple substitutions }}
-%% %%     {{ ocaml (assert false) }}
-%% %%     {{ hol (MAP (t_subst_t [[t_subst]]) [[t_multi]]) }}
-%% %%     {{ lem (List.map (t_subst_t [[t_subst]]) [[t_multi]]) }}
-%% %% 
-%% %% nec :: '' ::=
-%% %%   {{ com Numeric expression constraints }}
-%% %%   | ne < nec            :: :: lessthan
-%% %%   | ne = nec            :: :: eq
-%% %%   | ne <= nec           :: :: lteq
-%% %%   | ne                          :: :: base
-%% %% 
-%% %% parsing
-%% %% T_fn right T_fn
-%% %% T_tup <= T_multi
-%% %% 
-%% %% embed
-%% %% {{ lem
-%% %% 
-%% %% val t_subst_t : list (tnv * t) -> t -> t 
-%% %% val t_subst_tnv : list (tnv * t) -> tnv -> t
-%% %% val ftv_t : t -> list tnv
-%% %% val ftv_tm : list t -> list tnv
-%% %% val ftv_s : list (p*tnv) -> list tnv
-%% %% val compatible_overlap : list (x*t) -> bool
-%% %% 
-%% %% (*TODO Should this normalize following the implementation? And blength and hlength need a means of implementation*)
-%% %% let normalize n = n
-%% %% 
-%% %% let blength (_,bit) = Ne_const 8
-%% %% let hlength (_,bit) = Ne_const 8
-%% %% 
-%% %% let rec sumation_nes nes = match nes with
-%% %%   | [ a; b] -> Ne_add a b 
-%% %%   | x :: y -> Ne_add x (sumation_nes y)
-%% %% end
-%% %% 
-%% %% }}
-%% %% 
-%% %% grammar
-%% %% 
-%% %% 
-%% %% names :: '' ::=                                 {{ phantom }}
-%% %%                                                 {{ hol x set }}
-%% %%                                                 {{ lem set x }}
-%% %%                                                 {{ ocaml Set.Make(String).t }}
-%% %%   {{ com Sets of names }}
-%% %%   | { x1 , .. , xn }                            :: :: Names
-%% %%     {{ hol (LIST_TO_SET [[x1..xn]]) }}
-%% %%     {{ lem (set_from_list [[x1..xn]]) }}
-%% %% 
-%% %% semC {{ tex \ensuremath{\mathcal{C} } }} :: '' ::=
-%% %%                                                                 {{ hol (p#tnv) list }}
-%% %%                                                                 {{ lem list (p*tnv)  }}
-%% %% %   {{ com Typeclass constraint lists }}
-%% %% %   | ( p1 tnv1 ) .. ( pn tnvn )                                        :: :: SemC_concrete
-%% %% %     {{ hol ([[p1 tnv1..pn tnvn]]) }}
-%% %% %     {{ lem ([[p1 tnv1..pn tnvn]]) }}
-%% %% 
-%% %% env_tag :: '' ::=
-%% %%   {{ com Tags for the (non-constructor) value descriptions }}
-%% %% %  | method                                                     :: :: method
-%% %% %    {{ com Bound to a method }}
-%% %%   | val                                                         :: :: spec
-%% %%     {{ com Specified with val }}
-%% %%   | let                                                         :: :: def
-%% %%     {{ com Defined with let or indreln }}
-%% %% 
-%% %% v_desc :: 'V_' ::=
-%% %%   {{ com Value descriptions }}
-%% %%   | < forall tnvs . t_multi -> p , ( x of names ) >             :: :: constr
-%% %%     {{ com Constructors }}
-%% %%   | < forall tnvs . semC => t , env_tag >                       :: :: val
-%% %%     {{ com Values }}
-%% %% 
-%% %% f_desc :: 'F_' ::=
-%% %%   | < forall tnvs . p -> t , ( x of names ) >                   :: :: field
-%% %%     {{ com Fields }}
-%% %% 
-%% %% embed
-%% %% {{ hol
-%% %% load "fmaptreeTheory";
-%% %% val _ = 
-%% %%   Hol_datatype 
-%% %%     `env_body = <| env_p : x|->p; env_f : x|->f_desc; env_v : x|->v_desc |>`;
-%% %% 
-%% %% val _ = Define `
-%% %%   env_union e1 e2 =
-%% %%     let i1 = item e1 in
-%% %%     let m1 = map e1 in
-%% %%     let i2 = item e2 in
-%% %%     let m2 = map e2 in
-%% %%       FTNode <| env_p:=FUNION i1.env_p i2.env_p; 
-%% %%                 env_f:=FUNION i1.env_f i2.env_f;
-%% %%                 env_v:=FUNION i1.env_v i2.env_v |>
-%% %%              (FUNION m1 m2)`;
-%% %% }}
-%% %% {{ lem
-%% %% type env =
-%% %%   | EnvEmp 
-%% %%   | Env of (map x env) * (map x p) * (map x f_desc) * (map x v_desc)
-%% %% 
-%% %% val env_union : env -> env -> env
-%% %% let env_union e1 e2 =
-%% %%   match (e1,e2) with
-%% %%    | (EnvEmp,e2) -> e2
-%% %%    | (e1,EnvEmp) -> e1
-%% %%    | ((Env Em1 Ep1 Ef1 Ev1),(Env Em2 Ep2 Ef2 Ev2)) ->
-%% %%      Env(union_map Em1 Em2) (union_map Ep1 Ep2) (union_map Ef1 Ef2) (union_map Ev1 Ev2)
-%% %% end
-%% %% 
-%% %% }}
-%% %% 
-%% %% grammar
-%% %% 
-%% %% xs :: '' ::=                                    {{ phantom }}
-%% %%                                                 {{ hol string list }}
-%% %%                                                 {{ lem list string }}
-%% %%   | x1 .. xn                                    :: :: Xs
-%% %%     {{ hol [[x1..xn]] }}
-%% %%     {{ lem [[x1..xn]] }}
-%% %% 
-%% %% %TODO: no clue what the following are:
-%% %% S_c {{ tex {\ensuremath{ {\Sigma}^{\mathcal{C} } } } }} :: '' ::=                       {{ phantom }}
-%% %%                                                                 {{ hol (p#t) list }}
-%% %%                                                                 {{ lem list (p*t) }}
-%% %%   {{ com Typeclass constraints }}
-%% %%   | { ( p1 t1 ) , .. , ( pn tn ) }                              :: :: S_concrete
-%% %%     {{ hol [[p1 t1 .. pn tn]] }}
-%% %%     {{ lem [[p1 t1 .. pn tn]] }}
-%% %%   | S_c1 union .. union S_cn                                    :: M :: S_union
-%% %%     {{ hol (FLAT [[S_c1..S_cn]]) }}
-%% %%     {{ lem (List.flatten [[S_c1..S_cn]]) }}
-%% %%     {{ ocaml assert false }}
-%% %% 
-%% %% S_N {{ tex { \ensuremath{ {\Sigma}^{\mathcal{N} } } } }} :: '' ::= {{ phantom }}
-%% %%                                                                    {{ hol nec list }}
-%% %%                                                                    {{ lem list nec }}
-%% %%    {{ com nexp constraint lists }}
-%% %%    | { nec1 , .. ,  necn }                              :: :: Sn_concrete
-%% %%      {{ hol [[nec1 .. necn]] }}
-%% %%      {{ lem [[nec1 .. necn]] }}
-%% %%    | S_N1 union .. union S_Nn                   :: M :: SN_union
-%% %%      {{ hol (FLAT [[S_N1..S_Nn]]) }}
-%% %%      {{ lem (List.flatten [[S_N1..S_Nn]]) }}
-%% %%      {{ ocaml assert false }}
-%% %% 
-%% %% 
-%% %% E :: '' ::=                                                     {{ phantom }}
-%% %%                                                                 {{ hol ((string,env_body) fmaptree) }}
-%% %% 
-%% %% 
-%% %% %TODO: simplify by removing E_m throughout?  And E_p??
-%% %%                                                                 {{ lem env }}
-%% %%   {{ com Environments }}
-%% %%   | < E_m , E_p , E_f , E_x >                                           :: :: E
-%% %%     {{ hol (FTNode <|env_p:=[[E_p]]; env_f:=[[E_f]]; env_v:=[[E_x]]|> ([[E_m]])) }}
-%% %%     {{ lem (Env [[E_m]] [[E_p]] [[E_f]] [[E_x]]) }}
-%% %%   | E1 u+ E2                                                    :: M :: E_union
-%% %%     {{ hol (env_union [[E1]] [[E2]]) }}
-%% %%     {{ lem (env_union [[E1]] [[E2]]) }}
-%% %%     {{ ocaml assert false }}
-%% %%   | empty                                                       :: M :: E_empty
-%% %%     {{ hol (FTNode <|env_p:=FEMPTY; env_f:=FEMPTY; env_v:=FEMPTY|> FEMPTY) }}
-%% %%     {{ lem EnvEmp }}
-%% %%     {{ ocaml assert false }}
-%% %% 
-%% %% E_x {{ tex \ottnt{E}^{\textsc{x} } }} :: 'E_x_' ::=             {{ phantom }}
-%% %%                                                                 {{ hol (x|-> v_desc) }}
-%% %%                                                                 {{ lem map x v_desc }}
-%% %%   {{ com Value environments }}
-%% %%   | { x1 |-> v_desc1 , .. , xn |-> v_descn }    :: :: concrete
-%% %%     {{ hol (FOLDR (\(k1,k2) E. E |+ (k1,k2)) FEMPTY [[x1 v_desc1 .. xn v_descn]]) }}
-%% %%     {{ lem (List.fold_right (fun (x,v) m -> Pmap.add x v m) [[x1 v_desc1 .. xn v_descn]] Pmap.empty) }} 
-%% %%   | E_x1 u+ .. u+ E_xn                                          :: M :: union
-%% %%     {{ hol (FOLDR FUNION FEMPTY [[E_x1..E_xn]]) }}
-%% %%     {{ lem (List.fold_right union_map [[E_x1..E_xn]] Pmap.empty) }}
-%% %%     {{ ocaml (assert false) }}
-%% %% 
-%% %% E_f {{ tex \ottnt{E}^{\textsc{f} } }} :: 'E_f_' ::=             {{ phantom }}
-%% %%                                                                 {{ hol (x |-> f_desc) }}
-%% %%                                                                 {{ lem map x f_desc }}
-%% %%   {{ com Field environments }}
-%% %%   | { x1 |-> f_desc1 , .. , xn |-> f_descn }                    :: :: concrete
-%% %%     {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[x1 f_desc1 .. xn f_descn]]) }}
-%% %%     {{ lem (List.fold_right (fun (x,f) m -> Pmap.add x f m) [[x1 f_desc1 .. xn f_descn]] Pmap.empty) }} 
-%% %%   | E_f1 u+ .. u+ E_fn                                          :: M :: union
-%% %%     {{ hol (FOLDR FUNION FEMPTY [[E_f1..E_fn]]) }}
-%% %%     {{ lem (List.fold_right union_map [[E_f1..E_fn]] Pmap.empty) }}
-%% %%     {{ ocaml (assert false) }}
-%% %% 
-%% %% E_m {{ tex \ottnt{E}^{\textsc{m} } }} :: 'E_m_' ::=             {{ phantom }}
-%% %%                                                                 {{ hol (string |-> (string,env_body) fmaptree) }}
-%% %%                                                                 {{ lem map x env }} 
-%% %% %  {{ com Module environments }}
-%% %% %  | { x1 |-> E1 , .. , xn |-> En }                             :: :: concrete
-%% %% %    {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[x1 E1 .. xn En]]) }}
-%% %% %    {{ lem (List.fold_right (fun (x,e) m -> Pmap.add x e m) [[x1 E1 .. xn En]] Pmap.empty) }} 
-%% %% % 
-%% %% % _p {{ tex \ottnt{E}^{\textsc{p} } }} :: 'E_p_' ::=            {{ phantom }}
-%% %% %                                                               {{ hol (x |-> p) }}
-%% %% %                                                               {{ lem map x p }}
-%% %% %  {{ com Path environments }}
-%% %% %  | { x1 |-> p1 , .. , xn |-> pn }                             :: :: concrete
-%% %% %    {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[x1 p1 .. xn pn]]) }}
-%% %% %    {{ lem (List.fold_right (fun (x,p) m -> Pmap.add x p m) [[x1 p1 .. xn pn]] Pmap.empty) }} 
-%% %% %  | E_p1 u+ .. u+ E_pn                                         :: M :: union
-%% %% %    {{ hol (FOLDR FUNION FEMPTY [[E_p1..E_pn]]) }}
-%% %% %    {{ lem (List.fold_right union_map [[E_p1..E_pn]] Pmap.empty) }}
-%% %% % 
-%% %% %    {{ ocaml (assert false) }}
-%% %%  E_l {{ tex \ottnt{E}^{\textsc{l} } }} :: 'E_l_' ::=            {{ phantom }}
-%% %%                                                                 {{ hol (x |-> t) }}
-%% %%                                                                 {{ lem map x t }}
-%% %%   {{ com Lexical bindings }}
-%% %%   | { x1 |-> t1 , .. , xn |-> tn }                              :: :: concrete
-%% %%     {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[x1 t1 .. xn tn]]) }}
-%% %%     {{ lem (List.fold_right (fun (x,t) m -> Pmap.add x t m) [[x1 t1 .. xn tn]] Pmap.empty) }} 
-%% %%   | E_l1 u+ .. u+ E_ln                                          :: M :: union
-%% %%     {{ hol (FOLDR FUNION FEMPTY [[E_l1..E_ln]]) }}
-%% %%     {{ lem (List.fold_right union_map [[E_l1..E_ln]] Pmap.empty) }}
-%% %%    {{ ocaml (assert false) }}
-%% %% 
-%% %% tc_abbrev :: 'Tc_abbrev_' ::=                                   {{ phantom }}
-%% %%                                                                 {{ hol t option }}
-%% %%                                                                 {{ lem option t }}
-%% %%                                                                 {{ ocaml t option }}
-%% %%   {{ com Type abbreviations }}
-%% %%   | . t                                                         :: :: some
-%% %%     {{ hol (SOME [[t]]) }}
-%% %%     {{ lem (Some [[t]]) }}
-%% %%   |                                                             :: :: none
-%% %%     {{ hol NONE }}
-%% %%     {{ lem None }}
-%% %% 
-%% %% tc_def :: '' ::=
-%% %%   {{ com Type and class constructor definitions }} 
-%% %%   | tnvs tc_abbrev                                              :: :: Tc_def
-%% %%     {{ com Type constructors }}
-%% %% 
-%% %% TD {{ tex \ensuremath{\Delta} }} :: 'TD_' ::=                   {{ phantom }}
-%% %%                                                                 {{ hol p |-> tc_def }}
-%% %%                                                                 {{ lem map p tc_def }}
-%% %%   {{ com Type constructor definitions }}
-%% %%   | { p1 |-> tc_def1 , .. , pn |-> tc_defn }                    :: :: concrete
-%% %%     {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[p1 tc_def1 .. pn tc_defn]]) }}
-%% %%     {{ lem (List.fold_right (fun (p,t) m -> Pmap.add p t m) [[p1 tc_def1 .. pn tc_defn]] Pmap.empty) }} 
-%% %%     {{ ocaml (assert false) }}
-%% %%   | TD1 u+ TD2                                                  :: M :: union
-%% %%     {{ hol (FUNION [[TD1]] [[TD2]]) }}
-%% %%     {{ lem (union_map [[TD1]] [[TD2]]) }}
-%% %%     {{ ocaml (assert false) }}
-%% %% 
-%% %% 
-%% %% 
-%% %% D :: 'D_' ::=                                                   {{ phantom }}
-%% %%                                                                 {{ hol ((p |-> tc_def) # (p |-> x list) # (inst list)) }}
-%% %%                                                                 {{ lem tdefs}}
-%% %%   {{ com Global type definition store }}
-%% %%   | < TD , TC , I >                                                     :: :: concrete
-%% %%     {{ hol ([[TD]], [[TC]], [[I]]) }}
-%% %%     {{ lem (D [[TD]] [[TC]] [[I]]) }}
-%% %%   | D1 u+ D2                                                    :: M :: union
-%% %%     {{ hol (case ([[D1]],[[D2]]) of ((x1,x2,x3),(y1,y2,y3)) => (FUNION x1 y1, FUNION x2 y2, x3 ++ y3)) }}
-%% %%     {{ lem (union_tcdefs [[D1]] [[D2]]) }}
-%% %%     {{ ocaml (assert false) }}
-%% %%   | empty                                                       :: M :: empty
-%% %%     {{ hol (FEMPTY, FEMPTY, []) }}
-%% %%     {{ lem DEmp }}
-%% %%     {{ ocaml assert false }}
-%% %% 
-%% %% parsing
-%% %% E_union left E_union
-%% %% 
-%% %% embed
-%% %% {{ lem
-%% %% type tdefs =
-%% %%   | DEmp
-%% %%   | D of (map p tc_def) * (map p (list x)) * (set inst)
-%% %% 
-%% %% val union_tcdefs : tdefs -> tdefs -> tdefs
-%% %% 
-%% %% }}
-
-grammar
-
-terminals :: '' ::=
-  | **                                  :: :: starstar
-    {{ tex \ensuremath{\mathop{\mathord{*}\mathord{*} } } }}
-    {{ com \texttt{**} }}
-  | >=                                  :: :: geq
-    {{ tex \ensuremath{\geq} }}
-    {{ com \texttt{>=} }}
-  | '<='                                        :: :: leq
-    {{ tex \ensuremath{\leq} }}
-    {{ com \texttt{<=} }}
-  | ->                                  :: :: arrow
-    {{ tex \ensuremath{\rightarrow} }}
-    {{ 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} }}
-%  | union                               :: :: union
-%    {{ tex \ensuremath{\cup} }}
-  | u+                                  :: :: uplus
-    {{ tex \ensuremath{\uplus} }}
-  | 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} }}
-  | >                                   :: :: gt
-    {{ tex \ensuremath{\rangle} }}
-  | |-                                  :: :: vdash
-    {{ tex \ensuremath{\vdash} }}
-  | '                                   :: :: quote
-    {{ tex \mbox{'} }}
-  | |->                                 :: :: mapsto
-    {{ tex \ensuremath{\mapsto} }}
-  | gives                               :: :: gives
-    {{ tex \ensuremath{\triangleright} }}
-  | ~>                                  :: :: leadsto
-    {{ tex \ensuremath{\leadsto} }}
-  | =>                                  :: :: Rightarrow
-    {{ tex \ensuremath{\Rightarrow} }}
-  | --                                  :: :: dashdash
-    {{ tex \mbox{--} }}
-  | empty                               :: :: empty
-    {{ tex \ensuremath{\epsilon} }}
-  | effectkw			        :: :: effectkw
-    {{ tex \ottkw{effect} }}
- 
-
-formula :: formula_ ::=
-  | judgement                                                   :: :: judgement
-
-  | formula1 .. formulan                                        :: :: dots
-
-%   | E_m ( x ) gives E                                         :: :: lookup_m
-%     {{ com Module lookup }}
-%     {{ hol (FLOOKUP [[E_m]] [[x]] = SOME [[E]]) }}
-%     {{ lem (Pmap.find [[x]] [[E_m]]) = [[E]] }} 
-% 
-%   | E_p ( x ) gives p                                         :: :: lookup_p
-%     {{ com Path lookup }}
-%     {{ hol (FLOOKUP [[E_p]] [[x]] = SOME [[p]]) }}
-%     {{ lem Pmap.find [[x]] [[E_p]] = [[p]] }} 
-
-%% %%   | E_f ( x ) gives f_desc                                      :: :: lookup_f
-%% %%     {{ com Field lookup }}
-%% %%     {{ hol (FLOOKUP [[E_f]] [[x]] = SOME [[f_desc]]) }}
-%% %%     {{ lem Pmap.find [[x]] [[E_f]] = [[f_desc]] }} 
-%% %% 
-%% %%   | E_x ( x ) gives v_desc                                      :: :: lookup_v
-%% %%     {{ com Value lookup }}
-%% %%     {{ hol (FLOOKUP [[E_x]] [[x]] = SOME [[v_desc]]) }}
-%% %%     {{ lem Pmap.find [[x]] [[E_x]] = [[v_desc]] }} 
-%% %% 
-%% %%   | E_l ( x ) gives t                                           :: :: lookup_l
-%% %%     {{ com Lexical binding lookup }}
-%% %%     {{ hol (FLOOKUP [[E_l]] [[x]] = SOME [[t]]) }}
-%% %%     {{ lem Pmap.find [[x]] [[E_l]] = [[t]] }} 
-%% %% 
-%% %% %   | TD ( p ) gives tc_def                                     :: :: lookup_tc
-%% %% %     {{ com Type constructor lookup }}
-%% %% %     {{ hol (FLOOKUP [[TD]] [[p]] = SOME [[tc_def]]) }}
-%% %% %     {{ lem Pmap.find [[p]] [[TD]] = [[tc_def]] }} 
-%% %% % 
-%% %% %   | TC ( p ) gives xs                                         :: :: lookup_class
-%% %% %     {{ com Type constructor lookup }}
-%% %% %     {{ hol (FLOOKUP [[TC]] [[p]] = SOME [[xs]]) }}
-%% %% %     {{ lem Pmap.find [[p]] [[TC]] = [[xs]] }} 
-%% %% 
-%% %%   | dom ( E_m1 ) inter dom ( E_m2 ) = emptyset                  :: :: E_m_disjoint
-%% %%     {{ hol (DISJOINT (FDOM [[E_m1]]) (FDOM [[E_m2]])) }}
-%% %%     {{ lem disjoint (Pmap.domain [[E_m1]]) (Pmap.domain [[E_m2]]) }} 
-%% %% 
-%% %%   | dom ( E_x1 ) inter dom ( E_x2 ) = emptyset                  :: :: E_x_disjoint
-%% %%     {{ hol (DISJOINT (FDOM [[E_x1]]) (FDOM [[E_x2]])) }}
-%% %%     {{ lem disjoint (Pmap.domain [[E_x1]]) (Pmap.domain [[E_x2]])  }} 
-%% %%     
-%% %%   | dom ( E_f1 ) inter dom ( E_f2 ) = emptyset                  :: :: E_f_disjoint
-%% %%     {{ hol (DISJOINT (FDOM [[E_f1]]) (FDOM [[E_f2]])) }}
-%% %%     {{ lem disjoint (Pmap.domain [[E_f1]]) (Pmap.domain [[E_f2]]) }} 
-%% %% 
-%% %% %   | dom ( E_p1 ) inter dom ( E_p2 ) = emptyset                        :: :: E_p_disjoint
-%% %% %     {{ hol (DISJOINT (FDOM [[E_p1]]) (FDOM [[E_p2]])) }}
-%% %% %     {{ lem disjoint (Pmap.domain [[E_p1]]) (Pmap.domain [[E_p2]]) }} 
-%% %% % 
-%% %%   | disjoint doms ( E_l1 , .... , E_ln )                        :: :: E_l_disjoint
-%% %%     {{ hol (FOLDR (\E b. case b of NONE => NONE | SOME s => if DISJOINT (FDOM
-%% %% E) s then SOME (FDOM E UNION s) else NONE) (SOME {}) [[E_l1....E_ln]] <> NONE) }}
-%% %%     {{ lem disjoint_all (List.map Pmap.domain [[E_l1 .... E_ln]]) }}
-%% %%     {{ com Pairwise disjoint domains }}
-%% %% 
-%% %%   | disjoint doms ( E_x1 , .... , E_xn )                        :: :: E_x_disjoint_many
-%% %%     {{ hol (FOLDR (\E b. case b of NONE => NONE | SOME s => if DISJOINT (FDOM
-%% %% E) s then SOME (FDOM E UNION s) else NONE) (SOME {}) [[E_x1....E_xn]] <> NONE) }}
-%% %%     {{ lem disjoint_all (List.map Pmap.domain [[E_x1 .... E_xn]]) }}
-%% %%     {{ com Pairwise disjoint domains }}
-%% %% 
-%% %%   | compatible overlap ( x1 |-> t1 , .. , xn |-> tn )           :: :: E_l_compat
-%% %%     {{ hol (!__n __m. MEM __m [[x1 t1 .. xn tn]] /\ MEM __n [[x1 t1..xn tn]] /\ (FST __m  = FST __n) ==> (SND __m = SND __n)) }}
-%% %%     {{ lem (compatible_overlap [[x1 t1 .. xn tn]]) }} 
-%% %%     {{ com $(\ottnt{x}_i = \ottnt{x}_j) \ensuremath{\Longrightarrow} (\ottnt{t}_i = \ottnt{t}_j)$ }}
-%% %% 
-%% %%   | duplicates ( tnvs ) = emptyset                              :: :: no_dups_tnvs
-%% %%     {{ hol (ALL_DISTINCT [[tnvs]]) }}
-%% %%     {{ lem (duplicates [[tnvs]]) = [ ] }} 
-%% %% 
-%% %%   | duplicates ( x1 , .. , xn ) = emptyset                      :: :: no_dups
-%% %%     {{ hol (ALL_DISTINCT [[x1..xn]]) }}
-%% %%     {{ lem (duplicates [[x1..xn]]) = [ ] }} 
-%% %% 
-%% %%   | x NOTIN dom ( E_l )                                         :: :: notin_dom_l
-%% %%     {{ hol ([[x]] NOTIN FDOM [[E_l]]) }}
-%% %%     {{ lem Pervasives.not (Pmap.mem [[x]] [[E_l]]) }} 
-%% %% 
-%% %%   | x NOTIN dom ( E_x )                                         :: :: notin_dom_v
-%% %%     {{ hol ([[x]] NOTIN FDOM [[E_x]]) }}
-%% %%     {{ lem Pervasives.not (Pmap.mem [[x]] [[E_x]]) }} 
-%% %% 
-%% %%   | x NOTIN dom ( E_f )                                         :: :: notin_dom_f
-%% %%     {{ hol ([[x]] NOTIN FDOM [[E_f]]) }}
-%% %%     {{ lem Pervasives.not (Pmap.mem [[x]] [[E_f]]) }} 
-%% %% 
-%% %% %   | p NOTIN dom ( TC )                                                :: :: notin_dom_tc
-%% %% %     {{ hol ([[p]] NOTIN FDOM [[TC]]) }}
-%% %% %     {{ lem Pervasives.not (Pmap.mem [[p]] [[TC]]) }} 
-%% %% 
-%% %%   | p NOTIN dom ( TD )                                          :: :: notin_dom_td
-%% %%     {{ hol ([[p]] NOTIN FDOM [[TD]]) }}
-%% %%     {{ lem Pervasives.not (Pmap.mem [[p]] [[TD]]) }} 
-%% %% 
-%% %%   | FV ( t ) SUBSET tnvs                                                :: :: FV_t
-%% %%     {{ com Free type variables }}
-%% %%     {{ hol (LIST_TO_SET (ftv_t [[t]]) SUBSET LIST_TO_SET [[tnvs]]) }}
-%% %%     {{ lem subst (ftv_t [[t]]) [[tnvs]]  }} 
-%% %% 
-%% %%   | FV ( t_multi ) SUBSET tnvs                                  :: :: FV_t_multi
-%% %%     {{ com Free type variables }}
-%% %%     {{ hol (LIST_TO_SET (FLAT (MAP ftv_t [[t_multi]])) SUBSET LIST_TO_SET [[tnvs]]) }}
-%% %%     {{ lem subst (ftv_tm [[t_multi]]) [[tnvs]]  }} 
-%% %% 
-%% %%   | FV ( semC ) SUBSET tnvs                                     :: :: FV_semC
-%% %%     {{ com Free type variables }}
-%% %%     {{ hol (LIST_TO_SET (MAP SND [[semC]]) SUBSET LIST_TO_SET [[tnvs]]) }}
-%% %%     {{ lem subst (ftv_s [[semC]]) [[tnvs]] }} 
-%% %% 
-%% %%   | inst 'IN' I                                                 :: :: inst_in
-%% %%     {{ hol (MEM [[inst]] [[I]]) }}
-%% %%     {{ lem ([[inst]] IN [[I]]) }}
-%% %% 
-%% %%   | ( p t ) NOTIN I                                             :: :: notin_I
-%% %%     {{ hol (~?__semC__. MEM (Inst __semC__ [[p]] [[t]]) [[I]]) }}
-%% %%     {{ lem (Pervasives.not ((Inst [] [[p]] [[t]]) IN [[I]])) }}
-%% %% 
-%% %%   | E_l1 = E_l2                                                 :: :: E_l_eqn
-%% %%     {{ ichl ([[E_l1]] = [[E_l2]]) }}
-%% %% 
-%% %%   | E_x1 = E_x2                                                 :: :: E_x_eqn
-%% %%     {{ ichl ([[E_x1]] = [[E_x2]]) }}
-%% %% 
-%% %%   | E_f1 = E_f2                                                 :: :: E_f_eqn
-%% %%     {{ ichl ([[E_f1]] = [[E_f2]]) }}
-%% %% 
-%% %%   | E1 = E2                                                     :: :: E_eqn
-%% %%     {{ ichl ([[E1]] = [[E2]]) }}
-%% %% 
-%% %%   | TD1 = TD2                                                   :: :: TD_eqn
-%% %%     {{ ichl ([[TD1]] = [[TD2]]) }}
-%% %% 
-%% %%   | TC1 = TC2                                                   :: :: TC_eqn
-%% %%     {{ ichl ([[TC1]] = [[TC2]]) }}
-%% %% 
-%% %%   | I1 = I2                                                     :: :: I_eqn
-%% %%     {{ ichl ([[I1]] = [[I2]]) }}
-%% %% 
-%% %%   | names1 = names2                                             :: :: names_eq
-%% %%     {{ ichl ([[names1]] = [[names2]]) }}
-%% %% 
-%% %%   | t1 = t2                                                     :: :: t_eq
-%% %%     {{ ichl ([[t1]] = [[t2]]) }}
-%% %% 
-%% %%   | t_subst1 = t_subst2                                         :: :: t_subst_eq
-%% %%     {{ ichl ([[t_subst1]] = [[t_subst2]]) }}
-%% %% 
-%% %%   | p1 = p2                                                     :: :: p_eq
-%% %%     {{ ichl ([[p1]] = [[p2]]) }}
-%% %% 
-%% %%   | xs1 = xs2                                                   :: :: xs_eq
-%% %%     {{ ichl ([[xs1]] = [[xs2]]) }}
-%% %% 
-%% %%   | tnvs1 = tnvs2                                                       :: :: tnvs_eq
-%% %%     {{ ichl ([[tnvs1]] = [[tnvs2]]) }}
-
diff --git a/language/l2_parse2.ott b/language/l2_parse2.ott
deleted file mode 100644
index 0f8dc8e7..00000000
--- a/language/l2_parse2.ott
+++ /dev/null
@@ -1,1424 +0,0 @@
-indexvar n , i , j , k ::=
-  {{ phantom }}
-  {{ com Index variables for meta-lists }}
-
-metavar num ::=
-  {{ phantom }}
-  {{ lex numeric }}
-  {{ ocaml int }}
-  {{ hol num }}
-  {{ lem integer }}
-  {{ com Numeric literals }}
-  {{ ocamllex ['0'-'9']+  }}
-
-metavar hex ::=
-  {{ phantom }}
-  {{ lex numeric }}
-  {{ ocaml string }}
-  {{ lem string }}
-{{ ocamllex '0''x'['0'-'9' 'A' - 'F' 'a'-'f' '_']+  }}
-  {{ com Bit vector literal, specified by C-style hex number }}
-  
-metavar bin ::=
-  {{ phantom }}
-  {{ lex numeric }}
-  {{ ocaml string }}
-  {{ lem string }}
-{{ ocamllex '\'' ['0' '1'     ' ']* '\''  }}
-  {{ com Bit vector literal, specified by C-style binary number }}  
-
-metavar string ::=
-  {{ phantom }}
-  {{ ocaml string }}
-  {{ lem string }}
-  {{ hol string }}
-  {{ ocamllex "a"  }} {{ phantom }}
-  {{ com String literals }}
-
-metavar regexp ::=
-  {{ phantom }}
-  {{ ocaml string }}
-  {{ lem string }}
-  {{ hol string }}
-  {{ ocamllex "a"  }} {{ phantom }}
-  {{ com Regular expresions, as a string literal }}
-
-embed
-{{ ocaml
-
-type l =
-  | Unknown
-  | Int of string * l option
-  | Generated of l
-  | Range of Lexing.position * Lexing.position
-
-type 'a annot = l * 'a
-
-exception Parse_error_locn of l * string
-
-}}
-
-embed
-{{ lem
-open import Map
-open import Maybe
-open import Pervasives
-
-type l =
-  | Unknown
-  | Trans of string * maybe l
-  | Range of nat * nat
-
-val duplicates : forall 'a. list 'a -> list 'a
-
-val union_map : forall 'a 'b. map 'a 'b -> map 'a 'b -> map 'a 'b
-
-val set_from_list : forall 'a. list 'a -> set 'a
-
-val subst : forall 'a. list 'a -> list 'a -> bool
-
-}}
-
-metavar x , y , z ::=
-  {{ ocaml string }}
-  {{ lem string }}
-  {{ hol string }}
-  {{ com identifier }}
-  {{ ocamlvar "[[x]]" }}
-  {{ lemvar "[[x]]" }}
-  {{ ocamllex "a"  }} {{ phantom }}
-
-metavar ix ::=
-  {{ lex alphanum }}
-  {{ ocaml string }}
-  {{ lem string }}
-  {{ hol string }}
-  {{ com infix identifier }}
-  {{ ocamlvar "[[ix]]" }}
-  {{ lemvar "[[ix]]" }}
-  {{ ocamllex "a"  }} {{ phantom }}
-
-
-grammar
-
-l :: '' ::=                                     {{ phantom }}
-                                                {{ ocaml l }}
-                                                {{ lem l }}
-                                                {{ hol unit }}
-  {{ com Source location }}
-  |                                             :: :: Unknown
-    {{ ocaml Unknown }}
-    {{ lem Unknown }}
-    {{ hol () }}
-
-
-id :: '' ::=
-  {{ com Identifier }}
-  {{ aux _ l }}
-  | x                           :: :: id
-  | op x                        :: :: deIid {{ com remove infix status }}
-
-
-kid :: '' ::=
-  {{ com identifiers with kind, ticked to differntiate from program variables }}
-  {{ aux _ l }}
-  | ' x                       :: :: var
-
-% 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. 
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% 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  }} 
-  | Effect                                    :: :: effect {{ com kind of effect sets  }} 
-
-kind :: 'K_' ::=  
-  {{ com kinds}}
-  {{ aux _ l }}
-  | base_kind1 -> ... -> base_kindn            :: :: kind 
-% we'll never use  ...-> Nat
-
-base_effect :: 'BE_' ::=
-  {{ com effect }}
-  {{ aux _ l }}  
-  | rreg                                :: :: rreg {{ com read register }}
-  | wreg                                :: :: wreg {{ com write register }}
-  | rmem                                :: :: rmem {{ com read memory }}
-  | wmem                                :: :: wmem {{ com write memory }}
-  | wmv					:: :: wmv {{ com write memory value }}
-  | eamem				:: :: eamem {{ com address for write signaled }}
-  | barr                                :: :: barr {{ com memory barrier }}
-  | depend				:: :: depend {{ com dynmically dependent footprint }}
-  | undef                               :: :: undef {{ com undefined-instruction exception }}
-  | unspec                              :: :: unspec {{ com unspecified values }}
-  | nondet                              :: :: nondet {{ com nondeterminism from intra-instruction parallelism }}
-  | escape                              :: :: escape
-
-
-
-atomic_typ :: 'ATyp_' ::= 
-  {{ quotient-with atyp }}
-  | id :: :: id
-  | kid :: :: var
-  | num :: :: constant
-  | dec :: :: dec
-  | inc :: :: inc
-  | id ( atyp1 , ... , atypn ) :: :: app
-  | ( atyp ) :: S :: paren {{ ocaml [[atyp]] }} 
-  | ( atyp1 , .... , atypn ) :: :: tup
-  | {| num_list |} :: S :: existential_set {{ ocaml   
-    { let v = mk_kid "n" $startpos $endpos in
-      let atom_id = mk_id (Id "atom") $startpos $endpos in
-      let atom_of_v = mk_typ (ATyp_app (atom_id, [mk_typ (ATyp_var v) $startpos $endpos])) $startpos $endpos in
-      mk_typ (ATyp_exist ([v], NC_aux (NC_set (v, [[num_list]]), loc $startpos($2) $endpos($2)), atom_of_v)) $startpos $endpos } }}
-  | { kid_list .  atyp } :: S :: existential_true {{ ocaml
-    { mk_typ (ATyp_exist ([[kid_list]], NC_aux (NC_true, loc $startpos $endpos), [[atyp]])) $startpos $endpos } }}
-  | { kid_list ,  nc . atyp } :: :: exist 
-  | { base_effect1 , .. , base_effectn }           :: :: set {{ com effect set }}
-  | pure                                 :: M :: pure {{ com sugar for empty effect set }} {{ icho [] }}
-
-
-atyp :: 'ATyp_' ::= 
-  {{ com expressions of all kinds, to be translated to types, nats, orders, and effects after parsing }}
-  {{ aux _ l }}
-  | atomic_typ                          :: S :: atomic {{ ocaml [[atomic_typ]] }} {{ quotient-remove }}
-  | atyp1 * atyp2                       :: :: times        {{ com product }}
-  | atyp1 + atyp2                       :: :: sum          {{ com sum }}
-  | atyp1 - atyp2                        :: :: minus	     {{ com subtraction }}
-  | 2** atyp                            :: :: exp         {{ com exponential }}
-  | neg atyp				:: :: neg	  {{ com Internal (but not M as I want a datatype constructor) negative nexp }}
-  | atyp1 -> atyp2 effect atyp3                        :: :: fn
-    {{ com Function type (first-order only in user code), last atyp is an effect }}
-
-
-% 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
-%  | enum nexp1 nexp2 order :: :: enum  {{ com natural numbers [[atyp2]] .. [[atyp2]]+[[atyp1]]-1, ordered by order }}
-%  | [ nexp ]             :: :: enum1 {{ com sugar for \texttt{enum nexp 0 inc} }}
-%  | [ nexp : nexp' ]  :: :: enum2 {{ com sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} }}
-% use .. not - to avoid ambiguity with nexp -
-% total maps and vectors indexed by finite subranges of nat
-%  | vector nexp1 nexp2 order atyp :: :: vector {{ com vector of [[atyp]], indexed by natural range }}
-% probably some sugar for vector types, using [ ] similarly to enums:
-% (but with .. not : in the former, to avoid confusion...)
-%  | atyp [ nexp ]  :: :: vector2 {{ com sugar for vector indexed by [ [[atyp]] ] }}
-%  | atyp [ nexp : nexp' ] :: :: vector3 {{ com sugar for vector indexed by [ [[atyp]]..[[atyp']] ] }}
-% ...so bit [ nexp ] etc is just an instance of that
-%  | list atyp :: :: list {{ com list of [[atyp]] }}
-%  | set atyp  :: :: set  {{ com finite set of [[atyp]] }}
-%  | reg atyp  :: :: reg  {{ com mutable register components holding [[atyp]] }}
-% "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 
-
-% parsing
-% 
-% ATyp_tup <= ATyp_tup
-% ATyp_fn right ATyp_fn
-% ATyp_fn <= ATyp_tup
-
-grammar
-
-n_constraint :: 'NC_' ::=
-  {{ com constraint over kind $[[Nat]]$ }}
-  {{ aux _ l }}
-  | atyp = atyp'                                :: :: fixed
-  | atyp >= atyp'                               :: :: bounded_ge
-  | atyp '<=' atyp'                             :: :: bounded_le
-  | kid 'IN' { num1 , ... , numn }               :: :: nat_set_bounded
-
-% 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 Either a kinded identifier or a nexp constraint for a typquant }}
-  {{ aux _ l }}
-  | kinded_id 	  	 	       	      :: :: id {{ com An optionally kinded identifier }}
-  | n_constraint			      :: :: const {{ com A constraint for this type }}
-
-typquant :: 'TypQ_' ::= 
-  {{ com type quantifiers and constraints}}
-  {{ aux _ l }}
-  | forall quant_item1 , ... , quant_itemn . :: :: tq {{ texlong }}
-  |                           ::  ::  no_forall     {{ com sugar, omitting quantifier and constraints }}
-
-typschm :: 'TypSchm_' ::=
-  {{ com type scheme  }}
-  {{ aux _ l }}
-  |  typquant atyp                                                       :: :: ts
-
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% Type definitions                                             %
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-grammar
-%ctor_def :: 'CT_' ::=
-%  {{ com Datatype constructor definition clause }}
-%  {{ aux _ l }}
-%  | id : typschm                                       :: :: ct
-% but we could get away with disallowing constraints in typschm, we
-% think - if it's useful to do that
-
- name_scm_opt :: 'Name_sect_' ::=
-   {{ com Optional variable-naming-scheme specification for variables of defined type }} 
-   {{ aux _ l }}
-   |                                                   :: :: none
-   | [ name = regexp ]                                 :: :: some
-
-type_union :: 'Tu_' ::=
-  {{ com Type union constructors }}
-  {{ aux _ l }}
-  | id                                                  :: :: id
-  | atyp id                                             :: :: ty_id
-
-type_def :: 'TD_' ::=
-  {{ com Type definition body }}
-  {{ aux _ l }}
-  | typedef id name_scm_opt = typschm                                        :: :: abbrev
-    {{ com type abbreviation }} {{ texlong }}
-  | typedef id name_scm_opt = const struct typquant { atyp1 id1 ; ... ; atypn idn semi_opt }     :: :: record
-    {{ com struct type definition }} {{ texlong }}
-  | typedef id name_scm_opt = const union typquant { type_union1 ; ... ; type_unionn semi_opt }   :: :: variant
-    {{ com union type definition}} {{ texlong }}
-  | typedef id name_scm_opt = enumerate { id1 ; ... ; idn semi_opt }   :: :: enum
-    {{ com enumeration type definition}} {{ texlong }}
-
-  | typedef id = register bits [ atyp : atyp' ] { index_range1 : id1 ; ... ; index_rangen : idn } 
-:: :: register {{ com register mutable bitfield type definition }} {{ texlong }}
-
-kind_def :: 'KD_' ::=
-  {{ com Definition body for elements of kind; many are shorthands for type\_defs }}
-  {{ aux _ l }}
-  | Def kind id name_scm_opt = typschm                                        :: :: abbrev
-    {{ com type abbreviation }} {{ texlong }}
-  | Def kind id name_scm_opt = const struct typquant { atyp1 id1 ; ... ; atypn idn semi_opt }     :: :: record
-    {{ com struct type definition }} {{ texlong }}
-  | Def kind id name_scm_opt = const union typquant { type_union1 ; ... ; type_unionn semi_opt }   :: :: variant
-    {{ com union type definition}} {{ texlong }}
-  | Def kind id name_scm_opt = enumerate { id1 ; ... ; idn semi_opt }   :: :: enum
-    {{ com enumeration type definition}} {{ texlong }}
-
-  | Def kind id = register bits [ atyp : atyp' ] { index_range1 : id1 ; ... ; index_rangen : idn } 
-:: :: register {{ com register mutable bitfield type definition }} {{ texlong }}
-
-
-% also sugar [  nexp ] 
-
-
-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 }}
-  | undefined					:: :: undef {{ com undefined value }}
-  | string                                              :: :: string {{ com string constant }}
-
-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 _ l }}
-  | lit                                                 :: :: lit
-    {{ com literal constant pattern }}
-  | _                                                   :: :: wild  
-    {{ com wildcard }}
-  | ( pat as id )                                      :: :: as
-    {{ com named pattern }}
-  | ( atyp ) pat                                       :: :: typ
-    {{ com typed pattern }}
-
-  | id                                      :: :: id
-    {{ com identifier  }}
-
-  | id ( pat1 , .. , patn )                                     :: :: app
-    {{ com union constructor pattern }}
-
-  | { fpat1 ; ... ; fpatn semi_opt }                  :: :: record
-    {{ com struct pattern }}
-
-  | [ pat1 , .. , patn  ]                     :: :: vector
-   {{ com vector pattern }}
-
-  | [ num1 = pat1 , .. , numn = patn  ]                     :: :: vector_indexed
-   {{ com vector pattern (with explicit indices) }}
-
-  |  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]] }}
-
-fpat :: 'FP_' ::=
-  {{ com Field pattern }}
-  {{ aux _ l }}
-  | id = pat                                            :: :: Fpat
-
-parsing
-P_app <= P_app
-P_app <= P_as
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% Expressions                                                  %
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-
-
-grammar
-
-exp :: 'E_' ::=
-  {{ com Expression }}
-  {{ aux _ l }}
-
-  | { exp1 ; ... ; expn }                               :: :: block {{ com block (parsing conflict with structs?) }}
-% maybe we really should have indentation-sensitive syntax :-)  (given that some of the targets do)
-
-  | nondet { exp1 ; ... ; expn }                        :: :: nondet {{ com block that can evaluate the contained expressions in any ordering }}
-
-  | id                                                  :: :: id
-    {{ com identifier }}
-
-  | lit                                                 :: :: lit
-    {{ com literal constant }}
-
-  | ( atyp ) exp                                         :: :: cast
-    {{ com cast }}
-
-
-  | id exp                                               :: S :: tup_app {{ ichlo [[id]] ( [[exp]] ) }} {{ com No extra parens needed when exp is a tuple }}
-  | id ( exp1 , .. , expn )                                   :: :: app
-    {{ com function application }}
-% 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 {{ icho [[ if exp1 then exp2 else unit ]] }}
-
-  | foreach id from exp1 to exp2 by exp3 in atyp 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  {{ icho [[ foreach id from exp1 to exp2 by 1 exp4 ]] }}
-  | foreach id from exp1 downto exp2 by exp3 exp4       :: S :: fordown {{ icho [[ foreach id from exp1 to exp2 by ( - exp3 ) exp4 ]] }}
-  | foreach id from exp1 downto exp2 exp3               :: S :: fordownbyone  {{ icho [[ foreach id from exp1 downto exp2 by 1 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 
-
-  | [ exp1 , ... , 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 exp1 ; .. ; expn }                                :: :: 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 }}
-  | letbind in exp                                  :: :: let
-    {{ com let expression }}
-
-  | exp := exp'                                      :: :: assign
-    {{ com imperative assignment }}
-
-  | sizeof atyp                                         :: :: sizeof
-  | exit exp						:: :: exit
-  | return exp                                          :: :: return
-  | assert ( exp , exp' )                               :: :: assert
-
-  | ( exp )                                             :: S :: paren {{ ichlo [[exp]] }}
-
-
-lexp :: 'LEXP_' ::= {{ com lvalue expression, can't occur out of the parser }}
-    {{ aux _ l }}
-%    {{ aux _ annot }} {{ auxparam 'a }}
-    | id                                                  :: :: id
-    {{ com identifier }}
-    | id ( exp1 , .. , expn )				  :: :: mem
-    | id exp	       	    				  :: S :: mem_tup {{ ichlo [[id (exp)]] }}
-    | 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 _ l }} 
-%  {{ aux _ annot }} {{ auxparam 'a }}
-  | id = exp                                            :: :: Fexp
-
-fexps :: 'FES_' ::=
-  {{ com Field-expression list }}
-  {{ aux _ l }}
-%  {{ aux _ annot }} {{ auxparam 'a }}
-  | fexp1 ; ... ; fexpn semi_opt                        :: :: Fexps
-
-opt_default :: 'Def_val_' ::=
-  {{ com Optional default value for indexed vectors, to define a defualt value for any unspecified positions in a sparse map }}
-  {{ aux _ l }} 
-  |                                                     :: :: empty
-  | ; default = exp                                       :: :: dec
-
-pexp :: 'Pat_' ::=
-  {{ com Pattern match }}
-  {{ aux _ l }}
-%  {{ aux _ annot }} {{ auxparam 'a }}
-  | pat -> exp                                  :: :: exp
-% 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 }}
-%  {{ aux _ annot }} {{ auxparam 'a }}
-  |                                             :: :: none
-  | typquant atyp                               :: :: 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 }}
-%  {{ aux _ annot }} {{ auxparam 'a }}
-  |                                             :: :: pure {{ com sugar for empty effect set }}
-  | effectkw atyp                                     :: :: effect
-
-funcl :: 'FCL_' ::=
-  {{ com Function clause }}
-  {{ aux _ l }}
-%  {{ aux _ annot }} {{ auxparam 'a }}
-  | id pat = exp                   :: :: Funcl
-
-
-fundef :: 'FD_' ::=
-  {{ com Function definition}}
-  {{ aux _ l }}
-%  {{ 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 _ l }}
-%  {{ aux _ annot }} {{ auxparam 'a }}
-  | let typschm pat = exp                                :: :: val_explicit
-    {{ com value binding, explicit type ([[pat]] must be total)}}
-  | let pat = exp                                    :: :: val_implicit
-    {{ com value binding, implicit type ([[pat]] must be total)}}
-
-
-val_spec :: 'VS_' ::=
-  {{ com Value type specification }} 
-  {{ aux _ l }}
-%  {{ aux _ annot }} {{ auxparam 'a }}
-  | val typschm id                                  :: :: val_spec
-  | val extern typschm id                           :: :: extern_no_rename
-  | val extern typschm id = string                  :: :: extern_spec
-
-default_typing_spec :: 'DT_' ::=
-  {{ com Default kinding or typing assumption, and default order for literal vectors and vector shorthands }}
-  {{ aux _ l }}
-%  {{ aux _ annot }} {{ auxparam 'a }}
-  | default base_kind kid    :: :: kind
-  | default base_kind atyp   :: :: order
-  | 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 Function and type union definitions that can be spread across
-         a file. Each one must end in $[[end id]]$ }}
-  {{ aux _ l }} 
-  | scattered function rec_opt tannot_opt effect_opt id   :: :: scattered_function {{ texlong }} {{ com scattered function definition header }}
-
-  | function clause funcl  :: :: scattered_funcl  
-{{ 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 {{ com scattered union definition member }}
-  | end id  :: :: scattered_end
-{{ com scattered definition end }}
-
-dec_spec :: 'DEC_' ::=
-  {{ com Register declarations }}
-  {{ aux _ l }}
-  | register atyp id                                             :: :: reg
-  | register alias id = exp	      	 			 :: :: alias
-  | register alias atyp id = exp	  			 :: :: typ_alias
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% Top-level definitions                                        %
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-def :: 'DEF_' ::=
-  {{ com Top-level definition }}
-  | 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 }}
-  | default_typing_spec                                         :: :: default
-    {{ com default kind and type assumptions }}
-  | scattered_def					:: :: scattered
-    {{ com scattered definition }} 
-  | dec_spec                                            :: :: reg_dec
-    {{ com register declaration }}
-
-defs :: '' ::=
-  {{ com Definition sequence }}
-  | def1  .. defn                 :: :: Defs
-
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% Machinery for typing rules                                   %
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%% %% 
-%% %% 
-%% %% grammar
-%% %% 
-%% %% 
-%% %% p :: 'Path_' ::=
-%% %%   {{ com Unique paths }}
-%% %%   | x1 . .. xn . x                              :: :: def
-%% %%   | __list                                      :: :: list      
-%% %%     {{ tex \ottkw{\_\_list}  }}
-%% %%   | __bool                                      :: :: bool
-%% %%     {{ tex \ottkw{\_\_bool}  }}
-%% %%   | __num                                       :: :: num
-%% %%     {{ tex \ottkw{\_\_num}  }}
-%% %%   | __set                                       :: :: set
-%% %%     {{ tex \ottkw{\_\_set}  }}
-%% %%   | __string                                    :: :: string
-%% %%     {{ tex \ottkw{\_\_string}  }}
-%% %%   | __unit                                      :: :: unit
-%% %%     {{ tex \ottkw{\_\_unit}  }}
-%% %%   | __bit                                       :: :: bit
-%% %%     {{ tex \ottkw{\_\_bit}  }}
-%% %%   | __vector                            :: :: vector
-%% %%     {{ tex \ottkw{\_\_vector} }}                
-%% %% %TODO morally, delete the above - but what are the __ things for?
-%% %% % cleaner to declare early in the library?
-%% %% 
-%% %% t_subst {{ tex \ensuremath{\sigma} }} :: '' ::= {{ phantom }}
-%% %%                                                 {{ hol (a # t) list }}
-%% %%                                                 {{ lem list (tnvar * t) }}
-%% %%   {{ com Type variable substitutions }}
-%% %%   | { tnvar1 |-> t1 .. tnvarn |-> tn }                  :: :: T_subst
-%% %%     {{ ocaml (assert false) }}
-%% %%     {{ lem ([[tnvar1 t1 .. tnvarn tn]]) }}
-%% %%     {{ hol ([[tnvar1 t1 .. tnvarn tn]]) }}
-%% %% 
-%% %% t , u :: 'T_' ::=
-%% %%   {{ com Internal types }}
-%% %%   | a                                           :: :: var
-%% %%   | t1 -> t2                                    :: :: fn
-%% %%   | t1 * .... * tn                              :: :: tup
-%% %%   | p t_args                                    :: :: app 
-%% %%   | ne                                          :: :: len
-%% %%   | t_subst ( t )                               :: M :: subst_app
-%% %%     {{ com Multiple substitutions }}
-%% %%     {{ ocaml (assert false) }}
-%% %%     {{ hol (t_subst_t [[t_subst]] [[t]]) }}
-%% %%     {{ lem (t_subst_t [[t_subst]] [[t]]) }}
-%% %%   | t_subst ( tnv )                     :: M :: var_subst_app
-%% %%     {{ com Single variable substitution }}
-%% %%     {{ ocaml (assert false) }}
-%% %%     {{ hol (t_subst_tnv [[t_subst]] [[tnv]]) }}
-%% %%     {{ lem (t_subst_tnv [[t_subst]] [[tnv]]) }}
-%% %%   | curry ( t_multi ,  t )                      :: M :: multifn
-%% %%     {{ com Curried, multiple argument functions }}
-%% %%     {{ ocaml (assert false) }}
-%% %%     {{ hol (FOLDR T_fn [[t]] [[t_multi]]) }}
-%% %%     {{ lem (List.fold_right T_fn [[t_multi]] [[t]]) }}
-%% %% 
-%% %% ne :: 'Ne_' ::=
-%% %%   {{ com internal numeric expressions }}
-%% %%   | N                                           :: :: var
-%% %%   | nat                                 :: :: const
-%% %%   | ne1 * ne2                           :: :: mult
-%% %%   | ne1 + ne2                           :: :: add
-%% %%   | ( - ne )                            :: :: unary
-%% %%   | normalize ( ne )                    :: M :: normalize
-%% %%     {{ ocaml (assert false) }}
-%% %%     {{ hol ARB }}
-%% %%     {{ lem (normalize [[ne]] ) }}
-%% %%   | ne1 + ... + nen                     :: M :: addmany
-%% %%     {{ ocaml (assert false) }}
-%% %%     {{ hol ARB }}
-%% %%     {{ lem (sumation_nes [[ne1...nen]]) }}
-%% %%   | bitlength ( bin )                   :: M :: cbin
-%% %%     {{ ocaml (asssert false) }}
-%% %%     {{ hol ARB }}
-%% %%     {{ lem (blength [[bin]]) }}
-%% %%   | bitlength ( hex )                   :: M :: chex
-%% %%     {{ ocaml (assert false) }}
-%% %%     {{ hol ARB }}
-%% %%     {{ lem (hlength [[hex]]) }}
-%% %%   | length ( pat1 ... patn )            :: M :: cpat
-%% %%     {{ ocaml (assert false) }}
-%% %%     {{ hol ARB }}
-%% %%     {{ lem (Ne_const (List.length [[pat1...patn]])) }}
-%% %%   | length ( exp1 ... expn )            :: M :: cexp
-%% %%     {{ hol ARB }}
-%% %%     {{ ocaml (assert false) }}
-%% %%     {{ lem (Ne_const (List.length [[exp1...expn]])) }}
-%% %% 
-%% %% t_args :: '' ::=
-%% %%   {{ com Lists of types }}
-%% %%   | t1 .. tn                            :: :: T_args
-%% %%   | t_subst ( t_args )                          :: M :: T_args_subst_app
-%% %%     {{ com Multiple substitutions }}
-%% %%     {{ ocaml (assert false) }}
-%% %%     {{ hol (t_subst_t_args [[t_subst]] [[t_args]]) }}
-%% %%     {{ lem (t_subst_t_args [[t_subst]] [[t_args]]) }}
-%% %% 
-%% %% t_multi :: '' ::=                               {{ phantom }}
-%% %%                                                 {{ hol t list }}
-%% %%                                                 {{ ocaml t list }}
-%% %%                                                 {{ lem list t }}
-%% %%   {{ com Lists of types }}
-%% %%   | ( t1 * .. * tn )                            :: :: T_multi
-%% %%     {{ hol [[t1..tn]] }}
-%% %%     {{ lem [[t1..tn]] }}
-%% %%   | t_subst ( t_multi )                         :: M :: T_multi_subst_app
-%% %%     {{ com Multiple substitutions }}
-%% %%     {{ ocaml (assert false) }}
-%% %%     {{ hol (MAP (t_subst_t [[t_subst]]) [[t_multi]]) }}
-%% %%     {{ lem (List.map (t_subst_t [[t_subst]]) [[t_multi]]) }}
-%% %% 
-%% %% nec :: '' ::=
-%% %%   {{ com Numeric expression constraints }}
-%% %%   | ne < nec            :: :: lessthan
-%% %%   | ne = nec            :: :: eq
-%% %%   | ne <= nec           :: :: lteq
-%% %%   | ne                          :: :: base
-%% %% 
-%% %% parsing
-%% %% T_fn right T_fn
-%% %% T_tup <= T_multi
-%% %% 
-%% %% embed
-%% %% {{ lem
-%% %% 
-%% %% val t_subst_t : list (tnv * t) -> t -> t 
-%% %% val t_subst_tnv : list (tnv * t) -> tnv -> t
-%% %% val ftv_t : t -> list tnv
-%% %% val ftv_tm : list t -> list tnv
-%% %% val ftv_s : list (p*tnv) -> list tnv
-%% %% val compatible_overlap : list (x*t) -> bool
-%% %% 
-%% %% (*TODO Should this normalize following the implementation? And blength and hlength need a means of implementation*)
-%% %% let normalize n = n
-%% %% 
-%% %% let blength (_,bit) = Ne_const 8
-%% %% let hlength (_,bit) = Ne_const 8
-%% %% 
-%% %% let rec sumation_nes nes = match nes with
-%% %%   | [ a; b] -> Ne_add a b 
-%% %%   | x :: y -> Ne_add x (sumation_nes y)
-%% %% end
-%% %% 
-%% %% }}
-%% %% 
-%% %% grammar
-%% %% 
-%% %% 
-%% %% names :: '' ::=                                 {{ phantom }}
-%% %%                                                 {{ hol x set }}
-%% %%                                                 {{ lem set x }}
-%% %%                                                 {{ ocaml Set.Make(String).t }}
-%% %%   {{ com Sets of names }}
-%% %%   | { x1 , .. , xn }                            :: :: Names
-%% %%     {{ hol (LIST_TO_SET [[x1..xn]]) }}
-%% %%     {{ lem (set_from_list [[x1..xn]]) }}
-%% %% 
-%% %% semC {{ tex \ensuremath{\mathcal{C} } }} :: '' ::=
-%% %%                                                                 {{ hol (p#tnv) list }}
-%% %%                                                                 {{ lem list (p*tnv)  }}
-%% %% %   {{ com Typeclass constraint lists }}
-%% %% %   | ( p1 tnv1 ) .. ( pn tnvn )                                        :: :: SemC_concrete
-%% %% %     {{ hol ([[p1 tnv1..pn tnvn]]) }}
-%% %% %     {{ lem ([[p1 tnv1..pn tnvn]]) }}
-%% %% 
-%% %% env_tag :: '' ::=
-%% %%   {{ com Tags for the (non-constructor) value descriptions }}
-%% %% %  | method                                                     :: :: method
-%% %% %    {{ com Bound to a method }}
-%% %%   | val                                                         :: :: spec
-%% %%     {{ com Specified with val }}
-%% %%   | let                                                         :: :: def
-%% %%     {{ com Defined with let or indreln }}
-%% %% 
-%% %% v_desc :: 'V_' ::=
-%% %%   {{ com Value descriptions }}
-%% %%   | < forall tnvs . t_multi -> p , ( x of names ) >             :: :: constr
-%% %%     {{ com Constructors }}
-%% %%   | < forall tnvs . semC => t , env_tag >                       :: :: val
-%% %%     {{ com Values }}
-%% %% 
-%% %% f_desc :: 'F_' ::=
-%% %%   | < forall tnvs . p -> t , ( x of names ) >                   :: :: field
-%% %%     {{ com Fields }}
-%% %% 
-%% %% embed
-%% %% {{ hol
-%% %% load "fmaptreeTheory";
-%% %% val _ = 
-%% %%   Hol_datatype 
-%% %%     `env_body = <| env_p : x|->p; env_f : x|->f_desc; env_v : x|->v_desc |>`;
-%% %% 
-%% %% val _ = Define `
-%% %%   env_union e1 e2 =
-%% %%     let i1 = item e1 in
-%% %%     let m1 = map e1 in
-%% %%     let i2 = item e2 in
-%% %%     let m2 = map e2 in
-%% %%       FTNode <| env_p:=FUNION i1.env_p i2.env_p; 
-%% %%                 env_f:=FUNION i1.env_f i2.env_f;
-%% %%                 env_v:=FUNION i1.env_v i2.env_v |>
-%% %%              (FUNION m1 m2)`;
-%% %% }}
-%% %% {{ lem
-%% %% type env =
-%% %%   | EnvEmp 
-%% %%   | Env of (map x env) * (map x p) * (map x f_desc) * (map x v_desc)
-%% %% 
-%% %% val env_union : env -> env -> env
-%% %% let env_union e1 e2 =
-%% %%   match (e1,e2) with
-%% %%    | (EnvEmp,e2) -> e2
-%% %%    | (e1,EnvEmp) -> e1
-%% %%    | ((Env Em1 Ep1 Ef1 Ev1),(Env Em2 Ep2 Ef2 Ev2)) ->
-%% %%      Env(union_map Em1 Em2) (union_map Ep1 Ep2) (union_map Ef1 Ef2) (union_map Ev1 Ev2)
-%% %% end
-%% %% 
-%% %% }}
-%% %% 
-%% %% grammar
-%% %% 
-%% %% xs :: '' ::=                                    {{ phantom }}
-%% %%                                                 {{ hol string list }}
-%% %%                                                 {{ lem list string }}
-%% %%   | x1 .. xn                                    :: :: Xs
-%% %%     {{ hol [[x1..xn]] }}
-%% %%     {{ lem [[x1..xn]] }}
-%% %% 
-%% %% %TODO: no clue what the following are:
-%% %% S_c {{ tex {\ensuremath{ {\Sigma}^{\mathcal{C} } } } }} :: '' ::=                       {{ phantom }}
-%% %%                                                                 {{ hol (p#t) list }}
-%% %%                                                                 {{ lem list (p*t) }}
-%% %%   {{ com Typeclass constraints }}
-%% %%   | { ( p1 t1 ) , .. , ( pn tn ) }                              :: :: S_concrete
-%% %%     {{ hol [[p1 t1 .. pn tn]] }}
-%% %%     {{ lem [[p1 t1 .. pn tn]] }}
-%% %%   | S_c1 union .. union S_cn                                    :: M :: S_union
-%% %%     {{ hol (FLAT [[S_c1..S_cn]]) }}
-%% %%     {{ lem (List.flatten [[S_c1..S_cn]]) }}
-%% %%     {{ ocaml assert false }}
-%% %% 
-%% %% S_N {{ tex { \ensuremath{ {\Sigma}^{\mathcal{N} } } } }} :: '' ::= {{ phantom }}
-%% %%                                                                    {{ hol nec list }}
-%% %%                                                                    {{ lem list nec }}
-%% %%    {{ com nexp constraint lists }}
-%% %%    | { nec1 , .. ,  necn }                              :: :: Sn_concrete
-%% %%      {{ hol [[nec1 .. necn]] }}
-%% %%      {{ lem [[nec1 .. necn]] }}
-%% %%    | S_N1 union .. union S_Nn                   :: M :: SN_union
-%% %%      {{ hol (FLAT [[S_N1..S_Nn]]) }}
-%% %%      {{ lem (List.flatten [[S_N1..S_Nn]]) }}
-%% %%      {{ ocaml assert false }}
-%% %% 
-%% %% 
-%% %% E :: '' ::=                                                     {{ phantom }}
-%% %%                                                                 {{ hol ((string,env_body) fmaptree) }}
-%% %% 
-%% %% 
-%% %% %TODO: simplify by removing E_m throughout?  And E_p??
-%% %%                                                                 {{ lem env }}
-%% %%   {{ com Environments }}
-%% %%   | < E_m , E_p , E_f , E_x >                                           :: :: E
-%% %%     {{ hol (FTNode <|env_p:=[[E_p]]; env_f:=[[E_f]]; env_v:=[[E_x]]|> ([[E_m]])) }}
-%% %%     {{ lem (Env [[E_m]] [[E_p]] [[E_f]] [[E_x]]) }}
-%% %%   | E1 u+ E2                                                    :: M :: E_union
-%% %%     {{ hol (env_union [[E1]] [[E2]]) }}
-%% %%     {{ lem (env_union [[E1]] [[E2]]) }}
-%% %%     {{ ocaml assert false }}
-%% %%   | empty                                                       :: M :: E_empty
-%% %%     {{ hol (FTNode <|env_p:=FEMPTY; env_f:=FEMPTY; env_v:=FEMPTY|> FEMPTY) }}
-%% %%     {{ lem EnvEmp }}
-%% %%     {{ ocaml assert false }}
-%% %% 
-%% %% E_x {{ tex \ottnt{E}^{\textsc{x} } }} :: 'E_x_' ::=             {{ phantom }}
-%% %%                                                                 {{ hol (x|-> v_desc) }}
-%% %%                                                                 {{ lem map x v_desc }}
-%% %%   {{ com Value environments }}
-%% %%   | { x1 |-> v_desc1 , .. , xn |-> v_descn }    :: :: concrete
-%% %%     {{ hol (FOLDR (\(k1,k2) E. E |+ (k1,k2)) FEMPTY [[x1 v_desc1 .. xn v_descn]]) }}
-%% %%     {{ lem (List.fold_right (fun (x,v) m -> Pmap.add x v m) [[x1 v_desc1 .. xn v_descn]] Pmap.empty) }} 
-%% %%   | E_x1 u+ .. u+ E_xn                                          :: M :: union
-%% %%     {{ hol (FOLDR FUNION FEMPTY [[E_x1..E_xn]]) }}
-%% %%     {{ lem (List.fold_right union_map [[E_x1..E_xn]] Pmap.empty) }}
-%% %%     {{ ocaml (assert false) }}
-%% %% 
-%% %% E_f {{ tex \ottnt{E}^{\textsc{f} } }} :: 'E_f_' ::=             {{ phantom }}
-%% %%                                                                 {{ hol (x |-> f_desc) }}
-%% %%                                                                 {{ lem map x f_desc }}
-%% %%   {{ com Field environments }}
-%% %%   | { x1 |-> f_desc1 , .. , xn |-> f_descn }                    :: :: concrete
-%% %%     {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[x1 f_desc1 .. xn f_descn]]) }}
-%% %%     {{ lem (List.fold_right (fun (x,f) m -> Pmap.add x f m) [[x1 f_desc1 .. xn f_descn]] Pmap.empty) }} 
-%% %%   | E_f1 u+ .. u+ E_fn                                          :: M :: union
-%% %%     {{ hol (FOLDR FUNION FEMPTY [[E_f1..E_fn]]) }}
-%% %%     {{ lem (List.fold_right union_map [[E_f1..E_fn]] Pmap.empty) }}
-%% %%     {{ ocaml (assert false) }}
-%% %% 
-%% %% E_m {{ tex \ottnt{E}^{\textsc{m} } }} :: 'E_m_' ::=             {{ phantom }}
-%% %%                                                                 {{ hol (string |-> (string,env_body) fmaptree) }}
-%% %%                                                                 {{ lem map x env }} 
-%% %% %  {{ com Module environments }}
-%% %% %  | { x1 |-> E1 , .. , xn |-> En }                             :: :: concrete
-%% %% %    {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[x1 E1 .. xn En]]) }}
-%% %% %    {{ lem (List.fold_right (fun (x,e) m -> Pmap.add x e m) [[x1 E1 .. xn En]] Pmap.empty) }} 
-%% %% % 
-%% %% % _p {{ tex \ottnt{E}^{\textsc{p} } }} :: 'E_p_' ::=            {{ phantom }}
-%% %% %                                                               {{ hol (x |-> p) }}
-%% %% %                                                               {{ lem map x p }}
-%% %% %  {{ com Path environments }}
-%% %% %  | { x1 |-> p1 , .. , xn |-> pn }                             :: :: concrete
-%% %% %    {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[x1 p1 .. xn pn]]) }}
-%% %% %    {{ lem (List.fold_right (fun (x,p) m -> Pmap.add x p m) [[x1 p1 .. xn pn]] Pmap.empty) }} 
-%% %% %  | E_p1 u+ .. u+ E_pn                                         :: M :: union
-%% %% %    {{ hol (FOLDR FUNION FEMPTY [[E_p1..E_pn]]) }}
-%% %% %    {{ lem (List.fold_right union_map [[E_p1..E_pn]] Pmap.empty) }}
-%% %% % 
-%% %% %    {{ ocaml (assert false) }}
-%% %%  E_l {{ tex \ottnt{E}^{\textsc{l} } }} :: 'E_l_' ::=            {{ phantom }}
-%% %%                                                                 {{ hol (x |-> t) }}
-%% %%                                                                 {{ lem map x t }}
-%% %%   {{ com Lexical bindings }}
-%% %%   | { x1 |-> t1 , .. , xn |-> tn }                              :: :: concrete
-%% %%     {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[x1 t1 .. xn tn]]) }}
-%% %%     {{ lem (List.fold_right (fun (x,t) m -> Pmap.add x t m) [[x1 t1 .. xn tn]] Pmap.empty) }} 
-%% %%   | E_l1 u+ .. u+ E_ln                                          :: M :: union
-%% %%     {{ hol (FOLDR FUNION FEMPTY [[E_l1..E_ln]]) }}
-%% %%     {{ lem (List.fold_right union_map [[E_l1..E_ln]] Pmap.empty) }}
-%% %%    {{ ocaml (assert false) }}
-%% %% 
-%% %% tc_abbrev :: 'Tc_abbrev_' ::=                                   {{ phantom }}
-%% %%                                                                 {{ hol t option }}
-%% %%                                                                 {{ lem option t }}
-%% %%                                                                 {{ ocaml t option }}
-%% %%   {{ com Type abbreviations }}
-%% %%   | . t                                                         :: :: some
-%% %%     {{ hol (SOME [[t]]) }}
-%% %%     {{ lem (Some [[t]]) }}
-%% %%   |                                                             :: :: none
-%% %%     {{ hol NONE }}
-%% %%     {{ lem None }}
-%% %% 
-%% %% tc_def :: '' ::=
-%% %%   {{ com Type and class constructor definitions }} 
-%% %%   | tnvs tc_abbrev                                              :: :: Tc_def
-%% %%     {{ com Type constructors }}
-%% %% 
-%% %% TD {{ tex \ensuremath{\Delta} }} :: 'TD_' ::=                   {{ phantom }}
-%% %%                                                                 {{ hol p |-> tc_def }}
-%% %%                                                                 {{ lem map p tc_def }}
-%% %%   {{ com Type constructor definitions }}
-%% %%   | { p1 |-> tc_def1 , .. , pn |-> tc_defn }                    :: :: concrete
-%% %%     {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[p1 tc_def1 .. pn tc_defn]]) }}
-%% %%     {{ lem (List.fold_right (fun (p,t) m -> Pmap.add p t m) [[p1 tc_def1 .. pn tc_defn]] Pmap.empty) }} 
-%% %%     {{ ocaml (assert false) }}
-%% %%   | TD1 u+ TD2                                                  :: M :: union
-%% %%     {{ hol (FUNION [[TD1]] [[TD2]]) }}
-%% %%     {{ lem (union_map [[TD1]] [[TD2]]) }}
-%% %%     {{ ocaml (assert false) }}
-%% %% 
-%% %% 
-%% %% 
-%% %% D :: 'D_' ::=                                                   {{ phantom }}
-%% %%                                                                 {{ hol ((p |-> tc_def) # (p |-> x list) # (inst list)) }}
-%% %%                                                                 {{ lem tdefs}}
-%% %%   {{ com Global type definition store }}
-%% %%   | < TD , TC , I >                                                     :: :: concrete
-%% %%     {{ hol ([[TD]], [[TC]], [[I]]) }}
-%% %%     {{ lem (D [[TD]] [[TC]] [[I]]) }}
-%% %%   | D1 u+ D2                                                    :: M :: union
-%% %%     {{ hol (case ([[D1]],[[D2]]) of ((x1,x2,x3),(y1,y2,y3)) => (FUNION x1 y1, FUNION x2 y2, x3 ++ y3)) }}
-%% %%     {{ lem (union_tcdefs [[D1]] [[D2]]) }}
-%% %%     {{ ocaml (assert false) }}
-%% %%   | empty                                                       :: M :: empty
-%% %%     {{ hol (FEMPTY, FEMPTY, []) }}
-%% %%     {{ lem DEmp }}
-%% %%     {{ ocaml assert false }}
-%% %% 
-%% %% parsing
-%% %% E_union left E_union
-%% %% 
-%% %% embed
-%% %% {{ lem
-%% %% type tdefs =
-%% %%   | DEmp
-%% %%   | D of (map p tc_def) * (map p (list x)) * (set inst)
-%% %% 
-%% %% val union_tcdefs : tdefs -> tdefs -> tdefs
-%% %% 
-%% %% }}
-
-grammar
-
-terminals :: '' ::=
-  | **                                  :: :: starstar
-    {{ tex \ensuremath{\mathop{\mathord{*}\mathord{*} } } }}
-    {{ com \texttt{**} }}
-  | >=                                  :: :: geq
-    {{ tex \ensuremath{\geq} }}
-    {{ com \texttt{>=} }}
-  | '<='                                        :: :: leq
-    {{ tex \ensuremath{\leq} }}
-    {{ com \texttt{<=} }}
-  | ->                                  :: :: arrow
-    {{ tex \ensuremath{\rightarrow} }}
-    {{ 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} }}
-%  | union                               :: :: union
-%    {{ tex \ensuremath{\cup} }}
-  | u+                                  :: :: uplus
-    {{ tex \ensuremath{\uplus} }}
-  | 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} }}
-  | >                                   :: :: gt
-    {{ tex \ensuremath{\rangle} }}
-  | |-                                  :: :: vdash
-    {{ tex \ensuremath{\vdash} }}
-  | '                                   :: :: quote
-    {{ tex \mbox{'} }}
-  | |->                                 :: :: mapsto
-    {{ tex \ensuremath{\mapsto} }}
-  | gives                               :: :: gives
-    {{ tex \ensuremath{\triangleright} }}
-  | ~>                                  :: :: leadsto
-    {{ tex \ensuremath{\leadsto} }}
-  | =>                                  :: :: Rightarrow
-    {{ tex \ensuremath{\Rightarrow} }}
-  | --                                  :: :: dashdash
-    {{ tex \mbox{--} }}
-  | empty                               :: :: empty
-    {{ tex \ensuremath{\epsilon} }}
-  | effectkw			        :: :: effectkw
-    {{ tex \ottkw{effect} }}
- 
-
-formula :: formula_ ::=
-  | judgement                                                   :: :: judgement
-
-  | formula1 .. formulan                                        :: :: dots
-
-%   | E_m ( x ) gives E                                         :: :: lookup_m
-%     {{ com Module lookup }}
-%     {{ hol (FLOOKUP [[E_m]] [[x]] = SOME [[E]]) }}
-%     {{ lem (Pmap.find [[x]] [[E_m]]) = [[E]] }} 
-% 
-%   | E_p ( x ) gives p                                         :: :: lookup_p
-%     {{ com Path lookup }}
-%     {{ hol (FLOOKUP [[E_p]] [[x]] = SOME [[p]]) }}
-%     {{ lem Pmap.find [[x]] [[E_p]] = [[p]] }} 
-
-%% %%   | E_f ( x ) gives f_desc                                      :: :: lookup_f
-%% %%     {{ com Field lookup }}
-%% %%     {{ hol (FLOOKUP [[E_f]] [[x]] = SOME [[f_desc]]) }}
-%% %%     {{ lem Pmap.find [[x]] [[E_f]] = [[f_desc]] }} 
-%% %% 
-%% %%   | E_x ( x ) gives v_desc                                      :: :: lookup_v
-%% %%     {{ com Value lookup }}
-%% %%     {{ hol (FLOOKUP [[E_x]] [[x]] = SOME [[v_desc]]) }}
-%% %%     {{ lem Pmap.find [[x]] [[E_x]] = [[v_desc]] }} 
-%% %% 
-%% %%   | E_l ( x ) gives t                                           :: :: lookup_l
-%% %%     {{ com Lexical binding lookup }}
-%% %%     {{ hol (FLOOKUP [[E_l]] [[x]] = SOME [[t]]) }}
-%% %%     {{ lem Pmap.find [[x]] [[E_l]] = [[t]] }} 
-%% %% 
-%% %% %   | TD ( p ) gives tc_def                                     :: :: lookup_tc
-%% %% %     {{ com Type constructor lookup }}
-%% %% %     {{ hol (FLOOKUP [[TD]] [[p]] = SOME [[tc_def]]) }}
-%% %% %     {{ lem Pmap.find [[p]] [[TD]] = [[tc_def]] }} 
-%% %% % 
-%% %% %   | TC ( p ) gives xs                                         :: :: lookup_class
-%% %% %     {{ com Type constructor lookup }}
-%% %% %     {{ hol (FLOOKUP [[TC]] [[p]] = SOME [[xs]]) }}
-%% %% %     {{ lem Pmap.find [[p]] [[TC]] = [[xs]] }} 
-%% %% 
-%% %%   | dom ( E_m1 ) inter dom ( E_m2 ) = emptyset                  :: :: E_m_disjoint
-%% %%     {{ hol (DISJOINT (FDOM [[E_m1]]) (FDOM [[E_m2]])) }}
-%% %%     {{ lem disjoint (Pmap.domain [[E_m1]]) (Pmap.domain [[E_m2]]) }} 
-%% %% 
-%% %%   | dom ( E_x1 ) inter dom ( E_x2 ) = emptyset                  :: :: E_x_disjoint
-%% %%     {{ hol (DISJOINT (FDOM [[E_x1]]) (FDOM [[E_x2]])) }}
-%% %%     {{ lem disjoint (Pmap.domain [[E_x1]]) (Pmap.domain [[E_x2]])  }} 
-%% %%     
-%% %%   | dom ( E_f1 ) inter dom ( E_f2 ) = emptyset                  :: :: E_f_disjoint
-%% %%     {{ hol (DISJOINT (FDOM [[E_f1]]) (FDOM [[E_f2]])) }}
-%% %%     {{ lem disjoint (Pmap.domain [[E_f1]]) (Pmap.domain [[E_f2]]) }} 
-%% %% 
-%% %% %   | dom ( E_p1 ) inter dom ( E_p2 ) = emptyset                        :: :: E_p_disjoint
-%% %% %     {{ hol (DISJOINT (FDOM [[E_p1]]) (FDOM [[E_p2]])) }}
-%% %% %     {{ lem disjoint (Pmap.domain [[E_p1]]) (Pmap.domain [[E_p2]]) }} 
-%% %% % 
-%% %%   | disjoint doms ( E_l1 , .... , E_ln )                        :: :: E_l_disjoint
-%% %%     {{ hol (FOLDR (\E b. case b of NONE => NONE | SOME s => if DISJOINT (FDOM
-%% %% E) s then SOME (FDOM E UNION s) else NONE) (SOME {}) [[E_l1....E_ln]] <> NONE) }}
-%% %%     {{ lem disjoint_all (List.map Pmap.domain [[E_l1 .... E_ln]]) }}
-%% %%     {{ com Pairwise disjoint domains }}
-%% %% 
-%% %%   | disjoint doms ( E_x1 , .... , E_xn )                        :: :: E_x_disjoint_many
-%% %%     {{ hol (FOLDR (\E b. case b of NONE => NONE | SOME s => if DISJOINT (FDOM
-%% %% E) s then SOME (FDOM E UNION s) else NONE) (SOME {}) [[E_x1....E_xn]] <> NONE) }}
-%% %%     {{ lem disjoint_all (List.map Pmap.domain [[E_x1 .... E_xn]]) }}
-%% %%     {{ com Pairwise disjoint domains }}
-%% %% 
-%% %%   | compatible overlap ( x1 |-> t1 , .. , xn |-> tn )           :: :: E_l_compat
-%% %%     {{ hol (!__n __m. MEM __m [[x1 t1 .. xn tn]] /\ MEM __n [[x1 t1..xn tn]] /\ (FST __m  = FST __n) ==> (SND __m = SND __n)) }}
-%% %%     {{ lem (compatible_overlap [[x1 t1 .. xn tn]]) }} 
-%% %%     {{ com $(\ottnt{x}_i = \ottnt{x}_j) \ensuremath{\Longrightarrow} (\ottnt{t}_i = \ottnt{t}_j)$ }}
-%% %% 
-%% %%   | duplicates ( tnvs ) = emptyset                              :: :: no_dups_tnvs
-%% %%     {{ hol (ALL_DISTINCT [[tnvs]]) }}
-%% %%     {{ lem (duplicates [[tnvs]]) = [ ] }} 
-%% %% 
-%% %%   | duplicates ( x1 , .. , xn ) = emptyset                      :: :: no_dups
-%% %%     {{ hol (ALL_DISTINCT [[x1..xn]]) }}
-%% %%     {{ lem (duplicates [[x1..xn]]) = [ ] }} 
-%% %% 
-%% %%   | x NOTIN dom ( E_l )                                         :: :: notin_dom_l
-%% %%     {{ hol ([[x]] NOTIN FDOM [[E_l]]) }}
-%% %%     {{ lem Pervasives.not (Pmap.mem [[x]] [[E_l]]) }} 
-%% %% 
-%% %%   | x NOTIN dom ( E_x )                                         :: :: notin_dom_v
-%% %%     {{ hol ([[x]] NOTIN FDOM [[E_x]]) }}
-%% %%     {{ lem Pervasives.not (Pmap.mem [[x]] [[E_x]]) }} 
-%% %% 
-%% %%   | x NOTIN dom ( E_f )                                         :: :: notin_dom_f
-%% %%     {{ hol ([[x]] NOTIN FDOM [[E_f]]) }}
-%% %%     {{ lem Pervasives.not (Pmap.mem [[x]] [[E_f]]) }} 
-%% %% 
-%% %% %   | p NOTIN dom ( TC )                                                :: :: notin_dom_tc
-%% %% %     {{ hol ([[p]] NOTIN FDOM [[TC]]) }}
-%% %% %     {{ lem Pervasives.not (Pmap.mem [[p]] [[TC]]) }} 
-%% %% 
-%% %%   | p NOTIN dom ( TD )                                          :: :: notin_dom_td
-%% %%     {{ hol ([[p]] NOTIN FDOM [[TD]]) }}
-%% %%     {{ lem Pervasives.not (Pmap.mem [[p]] [[TD]]) }} 
-%% %% 
-%% %%   | FV ( t ) SUBSET tnvs                                                :: :: FV_t
-%% %%     {{ com Free type variables }}
-%% %%     {{ hol (LIST_TO_SET (ftv_t [[t]]) SUBSET LIST_TO_SET [[tnvs]]) }}
-%% %%     {{ lem subst (ftv_t [[t]]) [[tnvs]]  }} 
-%% %% 
-%% %%   | FV ( t_multi ) SUBSET tnvs                                  :: :: FV_t_multi
-%% %%     {{ com Free type variables }}
-%% %%     {{ hol (LIST_TO_SET (FLAT (MAP ftv_t [[t_multi]])) SUBSET LIST_TO_SET [[tnvs]]) }}
-%% %%     {{ lem subst (ftv_tm [[t_multi]]) [[tnvs]]  }} 
-%% %% 
-%% %%   | FV ( semC ) SUBSET tnvs                                     :: :: FV_semC
-%% %%     {{ com Free type variables }}
-%% %%     {{ hol (LIST_TO_SET (MAP SND [[semC]]) SUBSET LIST_TO_SET [[tnvs]]) }}
-%% %%     {{ lem subst (ftv_s [[semC]]) [[tnvs]] }} 
-%% %% 
-%% %%   | inst 'IN' I                                                 :: :: inst_in
-%% %%     {{ hol (MEM [[inst]] [[I]]) }}
-%% %%     {{ lem ([[inst]] IN [[I]]) }}
-%% %% 
-%% %%   | ( p t ) NOTIN I                                             :: :: notin_I
-%% %%     {{ hol (~?__semC__. MEM (Inst __semC__ [[p]] [[t]]) [[I]]) }}
-%% %%     {{ lem (Pervasives.not ((Inst [] [[p]] [[t]]) IN [[I]])) }}
-%% %% 
-%% %%   | E_l1 = E_l2                                                 :: :: E_l_eqn
-%% %%     {{ ichl ([[E_l1]] = [[E_l2]]) }}
-%% %% 
-%% %%   | E_x1 = E_x2                                                 :: :: E_x_eqn
-%% %%     {{ ichl ([[E_x1]] = [[E_x2]]) }}
-%% %% 
-%% %%   | E_f1 = E_f2                                                 :: :: E_f_eqn
-%% %%     {{ ichl ([[E_f1]] = [[E_f2]]) }}
-%% %% 
-%% %%   | E1 = E2                                                     :: :: E_eqn
-%% %%     {{ ichl ([[E1]] = [[E2]]) }}
-%% %% 
-%% %%   | TD1 = TD2                                                   :: :: TD_eqn
-%% %%     {{ ichl ([[TD1]] = [[TD2]]) }}
-%% %% 
-%% %%   | TC1 = TC2                                                   :: :: TC_eqn
-%% %%     {{ ichl ([[TC1]] = [[TC2]]) }}
-%% %% 
-%% %%   | I1 = I2                                                     :: :: I_eqn
-%% %%     {{ ichl ([[I1]] = [[I2]]) }}
-%% %% 
-%% %%   | names1 = names2                                             :: :: names_eq
-%% %%     {{ ichl ([[names1]] = [[names2]]) }}
-%% %% 
-%% %%   | t1 = t2                                                     :: :: t_eq
-%% %%     {{ ichl ([[t1]] = [[t2]]) }}
-%% %% 
-%% %%   | t_subst1 = t_subst2                                         :: :: t_subst_eq
-%% %%     {{ ichl ([[t_subst1]] = [[t_subst2]]) }}
-%% %% 
-%% %%   | p1 = p2                                                     :: :: p_eq
-%% %%     {{ ichl ([[p1]] = [[p2]]) }}
-%% %% 
-%% %%   | xs1 = xs2                                                   :: :: xs_eq
-%% %%     {{ ichl ([[xs1]] = [[xs2]]) }}
-%% %% 
-%% %%   | tnvs1 = tnvs2                                                       :: :: tnvs_eq
-%% %%     {{ ichl ([[tnvs1]] = [[tnvs2]]) }}
-
diff --git a/language/l2_rules.ott b/language/l2_rules.ott
deleted file mode 100644
index 9e1b79fb..00000000
--- a/language/l2_rules.ott
+++ /dev/null
@@ -1,424 +0,0 @@
-
-
-grammar
-
-mut :: 'mut_' ::=
-  |  immutable :: :: immutable
-  |  mutable :: :: mutable
-
-lvar :: 'lvar_' ::=
-  | register typ :: :: register
-  | enum typ     :: :: enum
-  | local mut typ :: :: local
-  | union typquant typ :: :: union
-  | unbound :: :: unbound
-  
-
-
-G {{ tex \Gamma }}, D {{ tex \Delta }} :: 'G_' ::=  {{ com Type environment }} 
-   | empty                              :: :: empty {{ tex \epsilon }} {{ com Empty context }}
-   | G , x1 : typ1 , .. , xn : typn     :: :: type_list  {{ com List of variables and their types }}
-%   | G , x1 : k1 , .. , xn : kn         :: :: kind_list  {{ com List of variables and their kinds }}
-   | G , kid1 , .. , kidn               :: :: kid_list
-%   | G , quant_item1 , .. , quant_itemn :: :: quant_list
-%   | G , { nec1 , .. , necn }           :: :: constraint_list {{ com Constraints }}
-   | G , G1 .. Gn                       :: :: merge {{ com Merge or disjoint union }}
-   | G , id : lvar                       :: :: add_local
-
-
-formula :: formula_ ::=
-  | judgement                                                   :: :: judgement
-  | formula1 .. formulan                                        :: :: dots
-  | G ( id ) = lvar                                             :: :: lookup_id
-  | G ( typ1 , id ) = typ2                                      :: :: lookup_record_field
-  | G ( typ1 ) = typ2                                           :: :: lookup_typ
-  |  nexp = length [|| exp , exp1 , .. , expn ||]               :: :: vector_length
-  | order_inc                                                   :: :: default_order_inc
-  | order_dec                                                   :: :: default_order_dec
-  |  G |= nexp1 <= nexp2  :: :: prove_lteq
-
-defns
-  declarative :: '' ::=
-
-defn
- G |- typ1  ~< typ2   :: :: subtype :: subtype_
- {{ com $[[typ1]]$ is a subtype of $[[typ2]]$  }}
- {{ tex [[G]] \vdash [[typ1]]  \preccurlyeq [[typ2]] }}
-by
-
-
------------------ :: refl
-G |- typ ~< typ
-
---------------------- :: wild
-G |- _ ~< _
-
-
-
-------------- :: id
-G |- id ~< id
-
-G |- typ1 ~< typ'1 .. G |- typn ~< typ'n
---------------------------------------------------- :: tuple
-G |- (typ1 , .. , typn ) ~< (typ'1, .. , typ'n)
-
-
-defn
-G |-l lit => typ  :: :: infer_lit :: infer_lit_
-{{ com Infer that type of $[[lit]]$ is $[[typ]]$ }}
-{{ tex [[G]] \vdash_l [[lit]] \Rightarrow [[typ]] }}
-by
-
-
------------------------------ :: unit
-G |-l () => unit
-
--------------------- :: zero
-G |-l bitzero => bit
-
--------------------- :: one
-G |-l bitone => bit
-
-
----------------------- :: num
-G |-l num => atom < num >
-
-
----------------------- :: true
-G |-l true => bool
-
-
----------------------- :: false
-G |-l false => bool
-
-defn
-G |- lexp := exp => typ -| D :: :: bind_assignment :: bind_assignment_
-{{ com Bind assignment returning updated environment  }}
-{{ tex [[G]] \vdash [[lexp]] := [[exp]] \Rightarrow [[typ]] \dashv [[D]] }}
-by
-
-
-G |- exp => typ
-G |- id <= typ -| D
-------------------------------- :: id
-G |- id := exp => unit -| D
-
-defn
-G |- pat <= typ -| D :: :: bind_pat :: bind_pat_
-{{ tex [[G]] \vdash [[pat]] \Leftarrow [[typ]] \dashv [[D]] }}
-by
-
-G |- lit <= typ
--------------------     :: lit
-G |- lit <= typ -| G
-
-%% FIXME do add_local
-G(id) = local mutable typ'
----------------------- :: local
-G |- id <= typ -| G
-
-G(id) = unbound
----------------------- :: unbound
-G |- id <= typ -| G
-
-
-G(id) = enum typ'
-G |- typ' ~< typ
----------------------- :: enum
-G |- id <= typ -| G
-
-
----------------------- :: wild
-G |- _ <= typ -| G
-
-
-%% FIXME Should be fold?
-G |- pat1 <= typ1 -| G1 .. G |- patn <= typn -| Gn
-------------------------------------------------------- :: tup
-G |- (pat1 , .. , patn ) <= (typ1 , .. , typn ) -| G , G1 .. Gn
-
-
-
-defn
-G |- pat => typ -| D :: :: infer_pat :: infer_pat_
-{{ tex [[G]] \vdash [[pat]] \Leftarrow [[typ]] \dashv [[D]] }}
-by
-
-G(id) = enum typ 
--------------------- ::  id
-G |- id => typ -| G
-
-
-G |- pat <= typ -| D
-------------------------------- :: typ
-G |- (typ) pat => typ -| D
-
-
-G |-l lit => typ
------------------------  :: lit
-G |- lit => typ -| G
-
-
-defn
-G |-i id => typ :: :: infer_id :: infer_id_
-{{ com Infer type of indentifier }}
-{{ tex [[G]] \vdash_i [[id]] \Rightarrow [[typ]] }}
-by
-
-
-G(id) = local mut typ
----------------------- :: local
-G |-i id => typ
-
-
-G(id) = enum typ
----------------------- :: enum
-G |-i id => typ
-
-
-G(id) = register typ
----------------------- :: register
-G |-i id => typ
-
-
-G(id) = union typquant typ
-------------------------------------- :: union
-G |-i id => typ
-
-defn
-G |-f exp . id => typ :: :: infer_field :: infer_field_
-{{ tex [[G]] \vdash_f [[exp]] . [[id]] \Rightarrow [[typ]] }}
-by
-
-
-G |- exp => typ1
-G ( typ1 ) = register [ id2 ]
-G ( id2 ) = (base,top,ranges)
-ranges ( id ) = vec_typ
----------------------------- :: register
-G |-f exp . id => vec_typ
-
-
-
-G |- exp => typ1
-G ( typ1 , id ) = typ
----------------------------- :: record
-G |-f exp . id => typ
-
-
-defn
-G |- exp1 => n_constraint :: :: infer_flow :: infer_flow_
-by
-
-
-G |- x => atom < nexp1 >
-G |- y => atom < nexp2 >
----------------------------- :: lteq
-G |- :E_app: lteq_atom_atom ( x , y ) =>  nexp1 <= nexp2
-
-
-G |- x => atom < nexp1 >
-G |- y => atom < nexp2 >
----------------------------- :: gteq
-G |- :E_app: gteq_atom_atom ( x , y ) =>  nexp1 >= nexp2
-
-G |- x => atom < nexp1 >
-G |- y => atom < nexp2 >
----------------------------- :: lt
-G |- :E_app: lt_atom_atom ( x , y ) =>  nexp1 + numOne <= nexp2
-
-G |- x => atom < nexp1 >
-G |- y => atom < nexp2 >
----------------------------- :: gt
-G |- :E_app: lteq_atom_atom ( x , y ) =>  nexp1 >= nexp2 + numOne
-
-
-G |- id => range <nexp1 , nexp2 >
-G |- y => atom < nexp >
-------------------------------------------------------------------------------- :: lt_range_atom
-G |- :E_app: lt_range_atom ( id , y ) => range < nexp1 , min (nexp - 1 , nexp2 ) >
-
-
-
-
-defn
- G |- exp => typ :: :: infer_exp :: infer_exp_
-{{ com Infer that type of $[[exp]]$ is $[[typ]]$ }}
-{{ tex [[G]] \vdash [[exp]] \Rightarrow [[typ]]  }}
-by
-
-
-G |- exp1 <= unit ... G |- expn <= unit
------------------------------------------- :: nondet
-G |- nondet { exp1 ; ... ; expn } => unit
-
-
-G |-i id => typ
----------------- :: id
-G |- id => typ
-
-
-G |-l lit => typ
----------------- :: lit
-G |- lit => typ
-
-
------------------------------------ :: sizeof
-G |- sizeof nexp => atom < nexp >
-
-
--------------------------------------------- :: constraint
-G |- constraint n_constraint => bool
-
-G |-f exp . id => typ
------------------------- :: field
-G |- exp . id => typ
-
-
-G |- exp1 => typ1 .... G |- expn => typn
----------------------------------------------------------- :: tuple
-G |- ( exp1 , .... , expn ) => (typ1 , .... , typn )
-
-
-
-
-G |- lexp := exp => typ -| D
--------------------- :: assign
-G |- lexp := exp => typ
-
-
-
----------------------------- :: record_update
-G |- lexp . id := exp => typ
-
-
-G |- exp <= typ
------------------------ :: cast
-G |- ( typ ) exp => typ
-
-
-
-G |- :E_app: id ( exp1 , exp2 ) => typ
--------------------------------- :: app_infix
-G |- exp1 id exp2 => typ
-
-
---------------------------------------- :: app
-G |- :E_app: id (exp1 , .. , expn ) => typ
-
-
-
-G |- exp1 => bool
-G |- exp2 => unit
-------------------------------- :: while_loop
-G |- while exp1 do exp2 => unit
-
-G |- exp1 => unit
-G |- exp2 => bool
-------------------------------- :: until_loop
-G |- repeat exp1 until exp2 => unit
-
-G |- exp1 => range <nexp1,nexp1'>
-G |- exp2 => range <nexp2,nexp2'>
-G |= nexp1' <= nexp2
-G |- exp3 <= int
-G |- exp4 => unit
------------------------------------------------------------------------ :: for_inc
-G |-  foreach ( id from exp1 to exp2 by exp3 in inc ) exp4 => unit
-
-G |- exp1 => range <nexp1,nexp1'>
-G |- exp2 => range <nexp2,nexp2'>
-G |= nexp2' <= nexp1
-G |- exp3 <= int
-G |- exp4 => unit
------------------------------------------------------------------------ :: for_dec
-G |-  foreach ( id from exp1 to exp2 by exp3 in dec ) exp4 => unit
-
-
-G |- foreach ( id from exp1 to exp2 by exp3 in inc) exp4 => typ
------------------------------------------------------------------------ :: forup
-G |- foreach ( id from exp1 to exp2 by exp3 ) exp4 => typ
-
-
-G |- foreach ( id from exp1 to exp2 by numOne in inc) exp3 => typ
------------------------------------------------------------------------ :: forupbyone
-G |- foreach ( id from exp1 to exp2 ) exp3 => typ
-
-
-G |- foreach ( id from exp1 to exp2 by exp3 in dec) exp4   => typ
---------------------------------------------------------------------------- :: fordown
-G |- foreach ( id from exp1 downto exp2 by exp3 ) exp4   => typ
-
-G |- foreach ( id from exp1 to exp2 by numOne in dec) exp3  => typ
-------------------------------------------------------------------------- :: fordownbyone
-G |- foreach ( id from exp1 downto exp2 ) exp3  => typ
-
-
-G |- exp1 => n_constraint
-%G , flows , constrs |- exp2 => typ
-%G , flows , negate constrs |- exp3 <= typ
--------------------------------------------- :: if
-G |- if exp1 then exp2 else exp3 => typ
-
-G |- :E_app: vector_access ( exp , exp' ) => typ
------------------------------- :: vector_access
-G |- exp [ exp' ] => typ
-
-
-G |- :E_app: vector_subrange ( exp , exp1 , exp2 ) => typ
---------------------------- :: vector_subrange
-G |- exp [ exp1 .. exp2 ] => typ
-
-
-G |- :E_app: vector_update ( exp , exp1 , exp2 ) => typ
----------------------------------- :: vector_update
-G |- :E_vector_update: [ exp with exp1 = exp2] => typ
-
-
-G |- :E_app: vector_update_subrange ( exp , exp1 , exp2 , exp3 ) => typ
------------------------------------------- ::  vector_update_subrange
-G |- :E_vector_update_subrange: [  exp with exp1 : exp2 = exp3 ] => typ
-
-
-G |- :E_app: vector_append ( exp1 , exp2 ) => typ
------------------------------------ ::   vector_append
-G |- exp1 : exp2  => typ
-
-
-order_inc
-G |- exp => typ
-G |- exp1 <= typ .. G |- expn <= typ
-nexp = length [|| exp , exp1 , .. , expn ||]
--------------------------------------------- :: vector_inc
-G |- [|| exp , exp1 , .. , expn ||] => typ [ numZero <: nexp ]
-
-order_dec
-G |- exp => typ
-G |- exp1 <= typ .. G |- expn <= typ
-nexp = length [|| exp , exp1 , .. , expn ||]
--------------------------------------------- :: vector_dec
-G |- [|| exp , exp1 , .. , expn ||] => typ [ nexp :> numZero ]
-
-
-G |- exp1 <= bool
-G |- exp2 <= string
------------------------------------ :: assert
-G |- assert (exp1, exp2 ) => unit
-
-
-defn
- G |- exp <= typ :: :: check_exp :: check_exp_
-{{ com Check that type of $[[exp]]$ is $[[typ]]$ }}
-{{ tex [[G]] \vdash [[exp]] \Leftarrow [[typ]]  }}
-by
-
-
-G |- exp1 <= unit ... G |- expn <= unit
-G |- exp <= typ
------------------------------------ :: block
-G |- { exp1; ... ; expn ; exp } <= typ
-
-
-
- 
-
diff --git a/language/l2_terminals_non_tt.ott b/language/l2_terminals_non_tt.ott
deleted file mode 100644
index 2c466b8b..00000000
--- a/language/l2_terminals_non_tt.ott
+++ /dev/null
@@ -1,31 +0,0 @@
-grammar 
-terminals :: '' ::=
-  | <                                   :: :: lt
-    {{ tex \ensuremath{\langle} }}
-%    {{ tex \ottsym{<} }}
-  | >                                   :: :: gt
-    {{ tex \ensuremath{\rangle} }}
-%    {{ tex \ottsym{>} }}
-
-%   | [| :: :: 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]}$} }}       
-
-  | ->                                  :: :: arrow
-    {{ tex \ensuremath{\rightarrow} }}
-%    {{ tex \ottsym{-\textgreater} }}
-    {{ com \texttt{->} }}
-
-  | >=                                  :: :: geq
-    {{ tex \ensuremath{\geq} }}
-%    {{ tex \ottsym{\textgreater=} }}
-    {{ com \texttt{>=} }}
-  | '<='                                        :: :: leq
-    {{ tex \ensuremath{\leq} }}
-%    {{ tex \ottsym{\textless=} }}
-    {{ com \texttt{<=} }}
diff --git a/language/l2_terminals_tt.ott b/language/l2_terminals_tt.ott
deleted file mode 100644
index c6bc8d34..00000000
--- a/language/l2_terminals_tt.ott
+++ /dev/null
@@ -1,31 +0,0 @@
-grammar 
-terminals :: '' ::=
-  | <                                   :: :: lt
-%    {{ tex \ensuremath{\langle} }}
-    {{ tex \ottsym{<} }}
-  | >                                   :: :: gt
-%    {{ tex \ensuremath{\rangle} }}
-    {{ tex \ottsym{>} }}
-
-  | [| :: :: 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]}$} }}       
-
-  | ->                                  :: :: arrow
-%    {{ tex \ensuremath{\rightarrow} }}
-    {{ tex \ottsym{-\textgreater} }}
-    {{ com \texttt{->} }}
-
-  | >=                                  :: :: geq
-%    {{ tex \ensuremath{\geq} }}
-    {{ tex \ottsym{\textgreater=} }}
-    {{ com \texttt{>=} }}
-  | '<='                                        :: :: leq
-%    {{ tex \ensuremath{\leq} }}
-    {{ tex \ottsym{\textless=} }}
-    {{ com \texttt{<=} }}
diff --git a/language/l2_typ.ott b/language/l2_typ.ott
deleted file mode 100644
index 43077d60..00000000
--- a/language/l2_typ.ott
+++ /dev/null
@@ -1,382 +0,0 @@
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% 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 
-
-k :: 'Ki_' ::=
-{{ com Internal kinds }}
-   | K_Typ                                             :: :: typ
-   | K_Nat                                             :: :: nat
-   | K_Ord                                             :: :: ord
-   | K_Efct                                             :: :: efct
-   | K_Lam ( k0 .. kn -> k' )                  :: :: ctor
-   | K_infer                                           :: :: infer {{ com Representing an unknown kind, inferred by context }}
-
-t , u :: 'T_' ::=                                
-{{ com Internal types }}
-   | x                                            :: :: id
-   | ' x                                          :: :: var
-   | t1 -> t2 effect                        :: :: fn 
-   | ( t1 , .... , tn )                           :: :: tup
-   | x < t_args >                           :: :: app 
-   | t |-> t1                                   :: :: abbrev
-   | register < t_arg >                  :: S :: reg_app {{ ichlo T_app "register" [[t_arg]] }}
-   | range < ne ne' > 			  :: S :: range_app {{ ichlo T_app "range" [[ [ ne ; ne' ] ]] }}
-   | atom < ne >    			  :: S :: atom_app {{ ichlo T_app "atom" [ [[ne]] ] }}
-   | vector < ne ne' order t >           :: S :: vector_app {{ ichlo T_app "vector" [[ [ ne; ne'; ord; t ] ]] }} 
-   | list < t >      	     		 :: S :: list_app {{ ichlo T_app "list" [[t]] }}
-   | reg < t >				 :: S :: box_app {{ ichlo T_app "reg" [[t]] }}
-   | implicit < ne >                      :: S :: implicit_app {{ ichlo T_app "implicit" [[ne]] }}
-   | bit      	     	   	       	          :: S :: bit_typ {{ ichlo T_id "bit" }}
-   | string                                    :: S :: string_typ {{ ichlo T_id "string" }}
-   | unit                                       :: S :: unit_typ {{ ichlo T_id "unit" }} 
-   | t [ t_arg1 / tid1 .. t_argn / tidn ]  :: M :: subst {{ ichlo "todo" }}
-
-optx :: '' ::= {{ phantom }} {{ lem maybe string }} {{ ocaml string option }}
-  | x                                            ::  :: optx_x
-  {{ lem (Just [[x]]) }} {{ ocaml (Some [[x]]) }}
-  |                                              :: :: optx_none
-  {{ lem Nothing }} {{ ocaml None }}
-
-
-tag :: 'Tag_' ::=                                 
-{{ com Data indicating where the identifier arises and thus information necessary in compilation }}
-   | None                                 :: :: empty
-   | Intro                                :: :: intro {{ com Denotes an assignment and lexp that introduces a binding }}
-   | Set                                  :: :: set {{ com Denotes an expression that mutates a local variable }}
-   | Tuple                                :: :: tuple_assign {{ com Denotes an assignment with a tuple lexp }}
-   | Global				  :: :: global {{ com Globally let-bound or enumeration based value/variable }} 
-   | Ctor                                 :: :: ctor {{ com Data constructor from a type union }}
-   | Extern optx                          :: :: extern {{ com External function, specied only with a val statement }}
-   | Default                              :: :: default {{ com Type has come from default declaration, identifier may not be bound locally }}
-   | Spec				  :: :: spec
-   | Enum num				  :: :: enum
-   | Alias				  :: :: alias
-   | Unknown_path optx			  :: :: unknown {{ com Tag to distinguish an unknown path from a non-analysis non deterministic path}}
-
-ne :: 'Ne_' ::=
- {{ com internal numeric expressions }}
-   | x                                   :: :: id
-   | ' x                                 :: :: var
-   | num                                 :: :: const
-   | infinity                            :: :: inf
-   | ne1 * ne2                           :: :: mult
-   | ne1 + ... + nen                     :: :: add
-   | ne1 - ne2 	 		       :: :: minus
-   | 2 ** ne				 :: :: exp
-   | ( - ne )                            :: :: unary
-   | zero   				 :: S :: zero
-     {{ lem (Ne_const 0) }}
-   | one				 :: S :: one
-     {{ lem (Ne_const 1) }}
-   | bitlength ( bin )                   :: M :: cbin
-     {{ ocaml (asssert false) }}
-     {{ hol ARB }}
-     {{ lem (blength [[bin]]) }}
-   | bitlength ( hex )                   :: M :: chex
-     {{ ocaml (assert false) }}
-     {{ hol ARB }}
-     {{ lem (hlength [[hex]]) }}
-   | count ( num0 ... numi )                :: M :: length {{ichlo "todo" }}
-   | length ( pat1 ... patn )            :: M :: cpat
-     {{ ocaml (assert false) }}
-     {{ hol ARB }}
-     {{ lem (Ne_const (List.length [[pat1...patn]])) }}
-   | length ( exp1 ... expn )            :: M :: cexp
-     {{ hol ARB }}
-     {{ ocaml (assert false) }}
-     {{ lem (Ne_const (List.length [[exp1...expn]])) }}
- 
- t_arg :: 't_arg_' ::=  
- {{ com Argument to type constructors }}
- | t :: :: typ
- | ne :: :: nexp
- | effect :: :: effect
- | order :: :: order
- | fresh :: M :: freshvar {{ lem T_arg (T_var "fresh") }}
-
- t_args :: '' ::=   {{ lem list t_arg }}
-  {{ com Arguments to type constructors }}
-   | t_arg1 ... t_argn                            :: :: T_args
-
- nec :: 'Nec_' ::=
-   {{ com Numeric expression constraints }}
-   | ne <= ne'            :: :: lteq
-   | ne = ne'            :: :: eq
-   | ne >= ne'           :: :: gteq
-   | ' x 'IN' { num1 , ... , numn } :: :: in
-   | nec0 .. necn -> nec'0 ... nec'm :: :: cond
-   | nec0 ... necn                   :: :: branch
-
-S_N {{ tex {\Sigma^{\textsc{N} } } }} :: '' ::= {{ phantom }}
-                                                                    {{ hol nec list }}
-                                                                    {{ lem list nec }}
-    {{ com nexp constraint lists }}
-    | { nec1 , .. ,  necn }                              :: :: Sn_concrete
-      {{ hol [[nec1 .. necn]] }}
-      {{ lem [[nec1 .. necn]] }}
-   | S_N1 u+ .. u+ S_Nn                                                    :: M :: SN_union
-     {{ hol (FOLDR FUNION FEMPTY [[S_N1..S_Nn]]) }}
-     {{ lem (List.foldr (++) [] [[S_N1..S_Nn]]) }}
-     {{ ocaml (assert false) }}
-   | consistent_increase ne1 ne'1 ... nen ne'n                    :: M :: SN_increasing
-     {{ com Generates constraints from  pairs of constraints, where the first of each pair is always larger than the sum of the previous pair }}
-     {{ ocaml (assert false) }}
-     {{ ichl todo }}
-   | consistent_decrease ne1 ne'1 ... nen ne'n                      :: M :: SN_decreasing
-     {{ com Generates constraints from  pairs of constraints, where the first of each pair is always smaller than the difference of the previous pair }}
-     {{ ocaml assert false }}
-     {{ ichl todo }}
-   | resolve ( S_N )                                                :: :: resolution
-     {{ lem [[S_N]] (* Write constraint solver *) }}
- 
-
- E_d {{ tex {\ottnt{E}^{\textsc{d} } } }} :: 'E_d_' ::=  {{ phantom }}
-                                                         {{ lem definition_env }}
- {{ com Environments storing top level information, such as defined abbreviations, records, enumerations, and kinds }}
- | < E_k , E_a , E_r , E_e >	     	       		    	 :: :: base
-   {{ hol arb }}
-   {{ lem (Denv [[E_k]] [[E_r]] [[E_e]]) }}
- | empty       	     					 :: :: empty
-   {{ hol arb }}
-   {{ lem DenvEmp }}
- | E_d u+ E_d'						 :: :: union
-   {{ hol arb }}
-   {{ lem (denv_union [[E_d]] [[E_d']]) }}
- 
- kinf :: 'kinf_' ::=
-   {{ com Whether a kind is default or from a local binding }}
-   | k                                        :: :: k
-   | k default                                :: :: def
-
- tid :: 'tid_' ::=
-   {{ com A type identifier or type variable }}
-   | id                                      :: :: id
-   | kid                                     :: :: var
-
- E_k {{ tex {\ottnt{E}^{\textsc{k} } } }} :: 'E_k_' ::=             {{ phantom }}
-                                                                 {{ hol (tid-> kinf) }}
-                                                                 {{ lem (map tid kinf) }}
-   {{ com Kind environments }}
-   | { tid1 |-> kinf1 , .. , tidn |-> kinfn }    :: :: concrete
-     {{ hol (FOLDR (\(k1,k2) E. E |+ (k1,k2)) FEMPTY [[tid1 kinf1 .. tidn kinfn]]) }}
-     {{ lem (List.foldr (fun (x,v) m -> Map.insert x v m) Map.empty [[tid1 kinf1 .. tidn kinfn]]) }} 
-   | E_k1 u+ .. u+ E_kn                                          :: M :: union
-     {{ com In a unioning kinf, {k default} u {k} results in {k} (i.e. the default is locally forgotten) }} 
-     {{ hol (FOLDR FUNION FEMPTY [[E_k1..E_kn]]) }}
-     {{ lem (List.foldr (union) Map.empty [[E_k1..E_kn]]) }}
-     {{ ocaml (assert false) }}
-   | E_k u- E_k1 .. E_kn                                            :: M :: multi_set_minus
-     {{ hol arb }} 
-     {{ lem (Map.fromList (remove_from (Set_extra.toList (Map.toSet [[E_k]]))
-                                       (Set_extra.toList (Map.toSet (List.foldr (union) Map.empty [[E_k1..E_kn]]))))) }} 
-     {{ ocaml assert false }}
-
- tinf :: 'tinf_' ::=                                                 
-    {{ com Type variables, type, and constraints, bound to an identifier }}
-    | t                                                 :: :: typ
-    | E_k , S_N , tag , t         :: :: quant_typ                                                             
-
-tinflist :: 'tinfs_' ::=
-  {{ com In place so that a list of tinfs can be referred to without the dot form }}
-  | empty :: :: empty
-  | tinf1 ... tinfn  :: :: ls
-
-conformsto :: 'conformsto_' ::=
-  {{ com how much conformance does overloading need }}
- | full :: :: full
- | parm :: :: parm
-
-widenvec :: 'widenvec_' ::=
-  | vectors :: :: widen
-  | none    :: :: dont
-  | _       :: :: dontcare
-
-widennum :: 'widennum_' ::=
-  | nums  :: :: widen
-  | none  :: :: dont
-  | _     :: :: dontcare
-
-widening :: 'widening_' ::=
-  {{ com Should we widen vector start locations, should we widen atoms and ranges }}
-  | ( widennum , widenvec ) :: :: w
-
- E_a {{ tex \ottnt{E}^{\textsc{a} } }} :: 'E_a_' ::=   {{ phantom }}
-                                                                            {{ hol tid |-> tinf}}
-                                                                            {{ lem map tid tinf }} 
-   | { tid1 |-> tinf1 , .. , tidn |-> tinfn } :: :: concrete
-   | E_a1 u+ .. u+ E_an	               :: :: union
-
- field_typs :: 'FT_' ::=     {{ phantom }}
-                             {{ lem list (id * t) }}
- {{ com Record fields }}
- | id1 : t1 , .. , idn : tn :: :: fields
-   {{ lem [[id1 t1..idn tn]] }}
-
- E_r {{ tex \ottnt{E}^{\textsc{r} } }} :: 'E_r_' ::=             {{ phantom }}
-                                                                 {{ hol (id*t) |-> tinf) }}
-                                                                 {{ lem map (list (id*t)) tinf }}
-   {{ com Record environments }}
-   | { { field_typs1 } |-> tinf1 , .. , { field_typsn } |-> tinfn }                    :: :: concrete
-     {{ hol (FOLDR (\x E. E |+ x) FEMPTY) }}
-     {{ lem (List.foldr (fun (x,f) m -> Map.insert x f m) Map.empty [[field_typs1 tinf1..field_typsn tinfn]]) }} 
-   | E_r1 u+ .. u+ E_rn                                          :: M :: union
-     {{ hol (FOLDR FUNION FEMPTY [[E_r1..E_rn]]) }}
-     {{ lem (List.foldr (union) Map.empty [[E_r1..E_rn]]) }}
-     {{ ocaml (assert false) }}
-
-  enumerate_map :: '' ::=                                        {{ phantom }}
-                                                                 {{ lem (list (nat*id)) }}
-   | { num1 |-> id1 ... numn |-> idn }                           :: :: enum_map
-    {{ lem [[num1 id1...numn idn]] }}
-
-  E_e {{ tex \ottnt{E}^{\textsc{e} } }} :: 'E_e_' ::=            {{ phantom }}
-                                                                 {{ lem (map t (list (nat*id))) }}
-   {{ com Enumeration environments }}
-   | { t1 |-> enumerate_map1 , .. , tn |-> enumerate_mapn }     :: :: base
-     {{ lem (List.foldr (fun (x,f) m -> Map.insert x f m) Map.empty [[t1 enumerate_map1..tn enumerate_mapn]]) }} 
-   | E_e1 u+ .. u+ E_en                                         :: :: union
-     {{ lem (List.foldr (union) Map.empty [[E_e1..E_en]]) }}
-
-    
-embed
-{{ lem
- type definition_env =
-   | DenvEmp
-   | Denv of (map tid kinf) * (map (list (id*t)) tinf) * (map t (list (nat*id)))
-
-}}
-
-grammar
-
- E_t {{ tex {\ottnt{E}^{\textsc{t} } } }} :: 'E_t_' ::=          {{ phantom }}
-                                                                 {{ hol (id |-> tinf) }}
-                                                                 {{ lem map id tinf }}
-   {{ com Type environments }}
-   | { id1 |-> tinf1 , .. , idn |-> tinfn }                    :: :: base
-     {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[id1 tinf1 .. idn tinfn]]) }}
-     {{ lem (List.foldr (fun (x,f) m -> Map.insert x f m) Map.empty [[id1 tinf1 .. idn tinfn]]) }} 
-   | { id |-> overload tinf conformsto : tinf1 , ... , tinfn }        :: :: overload
-   | ( E_t1 u+ .... u+ E_tn )                                         :: M :: union
-     {{ hol (FOLDR FUNION FEMPTY [[E_t1....E_tn]]) }}
-     {{ lem (List.foldr (union) Map.empty [[E_t1....E_tn]]) }}
-     {{ ocaml (assert false) }}
-   | u+ E_t1 .. E_tn                                            :: M :: multi_union
-     {{ hol arb }}
-     {{ lem (List.foldr (union) Map.empty [[E_t1..E_tn]]) }}
-     {{ ocaml assert false }}
-   | E_t u- id1 .. idn                                            :: M :: multi_set_minus
-     {{ hol arb }} 
-     {{ lem (Map.fromList (remove_from (Set_extra.toList (Map.toSet [[E_t]]))
-                                       (Set_extra.toList (Map.toSet (List.foldr (union) Map.empty [[id1..idn]]))))) }} 
-     {{ ocaml assert false }}
-   | ( E_t1 inter .... inter E_tn )                                  :: M :: intersect
-     {{ hol arb }}
-     {{ lem (List.foldr (fun a b -> (Map.fromList (Set_extra.toList ((Map.toSet a) inter (Map.toSet b)))))  Map.empty [[E_t1....E_tn]]) }} 
-     {{ ocaml (assert false) }}
-   | inter E_t1 .. E_tn                                            :: M :: multi_inter
-     {{ hol arb }}
-     {{ lem (List.foldr (fun a b -> (Map.fromList (Set_extra.toList ((Map.toSet a) inter (Map.toSet b))))) Map.empty [[E_t1..E_tn]]) }}
-     {{ ocaml assert false }}
-
-
-ts :: ts_ ::=                                     {{ phantom }}
-                                                  {{ lem list t }}
-  | t1 , .. , tn :: :: lst 
-
-embed
-{{ lem
-let blength (bit) = Ne_const 8
-let hlength (bit) = Ne_const 8
-
- type env =
-   | EnvEmp 
-   | Env of (map id tinf) * definition_env
-
- type inf = 
-   | Iemp
-   | Inf of (list nec) * effect
-
- val denv_union : definition_env -> definition_env -> definition_env
- let denv_union de1 de2 = 
-  match (de1,de2) with
-   | (DenvEmp,de2) -> de2
-   | (de1,DenvEmp) -> de1
-   | ((Denv ke1 re1 ee1),(Denv ke2 re2 ee2)) ->
-      Denv (ke1 union ke2) (re1 union re2) (ee1 union ee2)
-   end
-
- val env_union : env -> env -> env
- let env_union e1 e2 =
-   match (e1,e2) with
-    | (EnvEmp,e2) -> e2
-    | (e1,EnvEmp) -> e1
-    | ((Env te1 de1),(Env te2 de2)) ->
-      Env (te1 union te2) (denv_union de1 de2)
- end
-
-let inf_union i1 i2 =
-  match (i1,i2) with 
- | (Iemp,i2) -> i2
- | (i1,Iemp) -> i1
- | (Inf n1 e1,Inf n2 e2) -> (Inf (n1++n2) (effect_union e1 e2))
- end
-
-let fresh_kid denv = Var "x" (*TODO When strings can be manipulated, this should actually build a fresh string*)
-
-}}
-
-grammar
-
- E :: '' ::=                                                     
-                                                                 {{ hol ((string,env_body) fmaptree) }}
-                                                                 {{ lem env }}
- {{ com Definition environment and lexical environment }}
- | < E_t , E_d >                                           :: :: E
-  {{ hol arb }}
-  {{ lem (Env [[E_t]] [[E_d]])  }}
- | empty                                                       :: M :: E_empty
-   {{ hol arb }}
-   {{ lem EnvEmp }}
-   {{ ocaml assert false }}
- | E u+ E'                                                      :: :: E_union
-   {{ lem (env_union [[E]] [[E']]) }}
-
- I :: '' ::=                                                     {{ lem inf }}
-  {{ com Information given by type checking an expression }}
-  | < S_N , effect >                                      :: :: I
-    {{ lem (Inf [[S_N]] [[effect]]) }}
-  | Ie                                                           :: :: Iempty {{ com Empty constraints, effect }} {{ tex {\ottnt{I}_{\epsilon} } }}
-    {{ lem Iemp }}
-  | ( I1 u+ I2 ) :: :: singleunion {{ tex [[I1]] [[u+]] [[I2]] }}
-  | I1 u+ .. u+ In                                               :: :: Iunion {{ com Unions the constraints and effect }}
-    {{ lem (List.foldr inf_union Iemp [[I1..In]]) }}
-
diff --git a/language/primitive_doc.ott b/language/primitive_doc.ott
deleted file mode 100644
index a53f62fe..00000000
--- a/language/primitive_doc.ott
+++ /dev/null
@@ -1,130 +0,0 @@
-grammar 
-
-built_in_types :: '' ::=
-  {{ com Type  Kind }}
-  | bit : Typ :: :: bitDesc
-  | unit : Typ :: :: unitDesc
-  | forall Nat 'n. Nat 'm. range <'n, 'm> : Nat -> Nat -> Typ :: :: rangeDesc
-  | forall Nat 'n. atom <'n> : Nat -> Typ :: :: atomDesc {{ com singleton number, instead of range$< 'n,'n >$ }}
-  | forall Nat 'n, Nat 'm, Order 'o, Typ 't. vector < 'n, 'm, 'o, 't > : Nat -> Nat -> Order -> Typ :: :: vectorDesc
-  | forall Typ 'a. option < 'a > : Typ -> Typ :: :: optCtors
-  | forall Typ 't. register < 't > : Typ -> Typ :: :: registerDec
-  | forall Typ 't. reg < 't > : Typ -> Typ :: :: regDec
-    {{ com internal reference cell }}
-  | forall Nat 'n . implicit <'n> : Nat -> Typ :: :: implicitDesc
-    {{ com To add to a function val specification indicating that n relies on call site expected value }}
-
-built_in_type_abbreviations :: '' ::=
-  | bool => bit :: :: boolDesc
-  | nat => [| 0 '..' pos_infinity |] :: :: natDesc
-  | int  => [| neg_infinity '..' pos_infinity |] :: :: intDesc 
-  | uint8 => [| 0 '..' 2**8 |] :: :: uinteightDesc
-  | uint16 => [| 0 '..' 2**16 |] :: :: uintsixteenDesc
-  | uint32 => [| 0 '..' 2**32 |] :: :: uintthirtytwoDesc
-  | uint64 => [| 0 '..' 2**64 |] :: :: uintsixtyfourDesc
-
-
-functions :: '' ::=
-  {{ com Built-in functions: all have effect pure, all order polymorphic }}
-  | val forall Typ 'a  . 'a -> unit : ignore :: :: ignore
-  | val forall Typ 'a . 'a -> option < 'a > : Some :: :: some
-  | val forall Typ 'a . unit -> option < 'a > : None :: :: none
-  | val ( [: 'n :] , [: 'm :] ) -> [| 'n + 'm |] : + :: :: plusbase
-  {{ com arithmetic addition }}
-  | val forall Nat 'n . ( bit [ 'n ] , bit ['n] ) -> bit [ 'n ] : + :: :: plusvec
-  {{ com unsigned vector addition }}
-  | val forall Nat 'n . ( bit [ 'n ] , bit [ 'n ]) -> ( bit [ 'n ] , bit , bit ) : + :: :: plusoverflow
-  {{ com unsigned vector addition with overflow, carry out }}
-  | val forall Nat 'n . ( bit [ 'n ] , bit ['n] ) -> bit [ 'n ] : +_s :: :: plusvecS
-  {{ com signed vector addition }}
-  | val forall Nat 'n . (bit [ 'n ] , bit [ 'n ] ) -> ( bit [ 'n ] , bit , bit ) : +_s :: :: plusoverflowS
-  {{ com signed vector addition with overflow, carry out }}
-  | val ( [| 'n '..' 'm |] , [| 'o '..' 'p |] ) -> [| 'n - 'o '..' 'm - 'p |] : - :: :: minusbase
-  {{ com arithmetic subtraction }}
-  | val forall Nat 'n . ( bit [ 'n ] , bit ['n] ) -> bit [ 'n ] : - :: :: minusvec
-  {{ com unsigned vector subtraction }}
-  | val forall Nat 'n . ( bit [ 'n ] , bit [ 'n ] ) -> ( bit [ 'n ] , bit , bit ) : - :: :: minusoverflow
-  {{ com unsigned vector subtraction with overflow, carry out }}
-  | val forall Nat 'n . ( bit [ 'n ] , bit ['n] ) -> bit [ 'n ] : -_s :: :: minusvecS
-  {{ com signed vector subtraction }}
-  | val forall Nat 'n . (bit [ 'n ] , bit [ 'n ] ) -> ( bit [ 'n ] , bit , bit ) : -_s :: :: minusoverflowS
-  {{ com signed vector subtraction with overflow, carry out }}
-  | val ( [| 'n '..' 'm |] , [| 'o '..' 'p |] ) -> [| 'n * 'o '..' 'm * 'p |] : * :: :: multbase
-  {{ com arithmetic multiplication }}
-  | val forall Nat 'n . ( bit [ 'n ] , bit ['n] ) -> bit [ 2*'n ] : * :: :: multvec
-  {{ com unsigned vector multiplication }}
-  | val forall Nat 'n . ( bit [ 'n ] , bit ['n] ) -> bit [ 2*'n ] : *_s :: :: multvecS
-  {{ com signed vector multiplication }}
-  | val ( [| 'n '..' 'm |] , [| 1 '..' 'p |] ) -> [| 0 '..' 'p - 1 |] : mod :: :: modbase
-  {{ com arithmetic modulo }}
-  | val forall Nat 'n . ( bit [ 'n ] , bit [ 'n ] ) -> bit [ 'n ] : mod :: :: modvec
-  {{ com unsigned vector modulo }}
-  | val ( [| 'n '..' 'm |] , [| 1 '..' 'p |] ) -> [| 'q '..' 'r |] : quot :: :: quotbase
-  {{ com arithmetic integer division }}
-  | val forall Nat 'n , Nat 'm . ( bit [ 'n ] , bit [ 'm ] ) -> bit [ 'n ] : quot :: :: quotvec
-  {{ com unsigned vector division }}
-  | val forall Nat 'n , Nat 'm . ( bit [ 'n ] , bit [ 'm ] ) -> bit [ 'n ] : quot_s :: :: quotvecS
-  {{ com signed vector division }}
-  | val forall Typ 'a , Nat 'n . ( 'a [' n]  -> [: 'n :] ) : length :: :: len
-  | val forall Typ 'a , Nat 'n , Nat 'm , 'n <= 'm . ( implicit < 'm > , 'a [ 'n ] ) -> 'a [ 'm ] : mask :: :: mask
-  {{ com reduce size of vector, dropping MSBits. Type system supplies implicit parameter, uses may require a cast }}
-  | val forall Nat 'n . ( bit [ 'n ] , bit [ 'n ] ) -> bit : == :: :: vecEQ
-  {{ com vector equality }}
-  | val forall Typ 'a , Typ 'b . ( 'a , 'b ) -> bit : == :: :: EQ
-  | val forall Typ 'a , Typ 'b . ( 'a , 'b ) -> bit : !=  :: :: NEQ
-  | val ( [| 'n '..' 'm |] , [| 'o '..' 'p |] ) -> bit : < :: :: ltbase
-  | val forall Nat 'n . ( bit [ 'n ] , bit ['n] ) -> bit : < :: :: ltvec
-  {{ com unsigned less than }}
-  | val forall Nat 'n . ( bit [ 'n ] , bit ['n] ) -> bit : <_s :: :: ltvecS
-  | val ( [| 'n '..' 'm |] , [| 'o '..' 'p |] ) -> bit : > :: :: gtbase
-  | val forall Nat 'n . ( bit [ 'n ] , bit ['n] ) -> bit : > :: :: gtvec
-  {{ com unsigned greater than }}
-  | val forall Nat 'n . ( bit [ 'n ] , bit ['n] ) -> bit : >_s :: :: gtvecS
- | val ( [| 'n '..' 'm |] , [| 'o '..' 'p |] ) -> bit : <= :: :: lteqbase
-  | val forall Nat 'n . ( bit [ 'n ] , bit ['n] ) -> bit : <= :: :: lteqvec
-  {{ com unsigned less than or eq }}
-  | val forall Nat 'n . ( bit [ 'n ] , bit ['n] ) -> bit : <=_s :: :: lteqvecS
-  | val ( [| 'n '..' 'm |] , [| 'o '..' 'p |] ) -> bit : >= :: :: gteqbase
-  | val forall Nat 'n . ( bit [ 'n ] , bit ['n] ) -> bit : >= :: :: gteqvec
-  {{ com unsigned greater than or eq }}
-  | val forall Nat 'n . ( bit [ 'n ] , bit ['n] ) -> bit : >=_s :: :: gteqvecS
-  | val bit -> bit : ~ :: :: neg
-  {{ com bit negation }}
-  | val forall Nat 'n . bit [ 'n ] -> bit [ 'n ] : ~ :: :: negvec
-  {{ com bitwise negation }}
-  | val ( bit , bit ) -> bit : | :: :: or
-  {{ com bitwise or }}
-  | val forall Nat 'n . ( bit [ 'n ] , bit [ 'n ] ) -> bit [ 'n ] : | :: :: orvec
-  | val ( bit , bit ) -> bit : & :: :: and
-  {{ com bitwise and }}
-  | val forall Nat 'n . ( bit [ 'n ] , bit [ 'n ] ) -> bit [ 'n ] : & :: :: andvec
-  | val ( bit , bit ) -> bit : ^ :: :: xor
-  {{ com bitwise xor }}
-  | val forall Nat 'n . ( bit [ 'n ] , bit [ 'n ] ) -> bit [ 'n ] : '^' :: :: xorvec
-  | val forall Nat 'n . ( bit ,  [| 'n |] ) -> bit [ 'n ] : '^^' :: :: duplicate
-  {{ com duplicate bit into a vector }}
-  | val forall Nat 'n , Nat 'm , 'm <= 'n . ( bit [ 'n ] , [| 'm |] ) -> bit [ 'n ] : << :: :: lshift
-  {{ com left shift }}
-  | val forall Nat 'n , Nat 'm , 'm <= 'n . ( bit [ 'n ] , [| 'm |] ) -> bit [ 'n ] : >> :: :: rshift
-  {{ com right shift }}
-  | val forall Nat 'n , Nat 'm , 'm <= 'n . ( bit [ 'n ] , [| 'm |] ) -> bit [ 'n ] : <<< :: :: rotate
-  {{ com rotate }}
-
-
-functions_with_coercions :: '' ::=
-  | val forall Nat 'n . (bit [ 'n ] , bit [ 'n ]) -> [| 2 ** 'n |] : + :: :: plusvecRange
-  | val forall Nat 'n, Nat 'o, Nat 'p. ( bit [ 'n ] , [| 'o '..' 'p |] ) -> bit [ 'n ] : + :: :: plusvecrange
-  | val forall Nat 'n, Nat 'o, Nat 'p. ( [| 'o '..' 'p |] , bit ['n] ) -> bit [ 'n ] : + :: :: plusrangevec
-  | val forall Nat 'n, Nat 'o, Nat 'p. ( bit [ 'n ] , [| 'o '..' 'p |] ) -> [| 'o '..' 'p + 2** 'n |] : + :: :: plusvecrangeRange
-  | val forall Nat 'n ( bit [ 'n ] , bit ) -> bit [ 'n ] : + :: :: plusvecbit
-  | val forall Nat 'n ( bit , bit [ 'n ]  ) -> bit [ 'n ] : + :: :: plusbitvec
-  | val forall Nat 'n . (bit [ 'n ] , bit [ 'n ]) -> [| 2 ** 'n |] : +_s :: :: plusvecRangeS
-  | val forall Nat 'n, Nat 'o, Nat 'p. ( bit [ 'n ] , [| 'o '..' 'p |] ) -> bit [ 'n ] : +_s :: :: plusvecrangeS
-  | val forall Nat 'n, Nat 'o, Nat 'p. ( [| 'o '..' 'p |] , bit ['n] ) -> bit [ 'n ] : +_s :: :: plusrangevecS
-  | val forall Nat 'n, Nat 'o, Nat 'p. ( bit [ 'n ] , [| 'o '..' 'p |] ) -> [| 'o '..' 'p + 2** 'n |] : +_s :: :: plusvecrangeRangeS
-  | val forall Nat 'n ( bit [ 'n ] , bit ) -> bit [ 'n ] : +_s :: :: plusvecbitS
-  | val forall Nat 'n ( bit , bit [ 'n ]  ) -> bit [ 'n ] : +_s :: :: plusbitvecS
-  | val forall Nat 'n, Nat 'o, Nat 'p. ( bit [ 'n ] , [| 'o '..' 'p |] ) -> bit [ 'n ] : - :: :: minusvecrange
-  | val forall Nat 'n, Nat 'o, Nat 'p. ( [| 'o '..' 'p |] , bit ['n] ) -> bit [ 'n ] : - :: :: minusrangevec
-  | val forall Nat 'n, Nat 'o, Nat 'p. ( bit [ 'n ] , [| 'o '..' 'p |] ) -> [| 'o '..' 'p + 2** 'n |] : - :: :: minusvecrangeRange
-
diff --git a/language/type_system.tex b/language/type_system.tex
deleted file mode 100644
index afb9fb88..00000000
--- a/language/type_system.tex
+++ /dev/null
@@ -1,117 +0,0 @@
-\documentclass[11pt]{article}
-
-\usepackage{amsmath,amssymb,supertabular,geometry,fullpage}
-\geometry{a4paper,twoside,landscape,left=10.5mm,right=10.5mm,top=20mm,bottom=30mm}
-\usepackage{color}
-
-\begin{document}
-
-\input{doc_in}
-
-\title{Sail Type System}
-\author{Kathryn E Gray, Gabriel Kerneis, Peter Sewell}
-
-\maketitle
-
-\tableofcontents
-
-\newpage
-
-\section{Sail syntax}
-
-\ottgrammartabular{
-\ottl\ottinterrule
-\ottannot\ottinterrule
-\ottid\ottinterrule
-\ottkid\ottinterrule
-\ottbaseXXkind\ottinterrule
-\ottkind\ottinterrule
-\ottnexp\ottinterrule
-\ottorder\ottinterrule
-\ottbaseXXeffect\ottinterrule
-\otteffect\ottinterrule
-\otttyp\ottinterrule
-\otttypXXarg\ottinterrule
-\ottnXXconstraint\ottinterrule
-\ottkindedXXid\ottinterrule
-\ottquantXXitem\ottinterrule
-\otttypquant\ottinterrule
-\otttypschm\ottinterrule
-\ottnameXXscmXXopt\ottinterrule
-\otttypeXXdef\ottinterrule
-\otttypeXXunion\ottinterrule
-\ottindexXXrange\ottinterrule
-\ottlit\ottinterrule
-\ottsemiXXopt\ottinterrule
-\ottpat\ottinterrule
-\ottfpat\ottinterrule
-\ottexp\ottinterrule
-\ottlexp\ottinterrule
-\ottfexp\ottinterrule
-\ottfexps\ottinterrule
-\ottoptXXdefault\ottinterrule
-\ottpexp\ottinterrule
-\otttannotXXopt\ottinterrule
-\ottrecXXopt\ottinterrule
-\otteffectXXopt\ottinterrule
-\ottfuncl\ottinterrule
-\ottfundef\ottinterrule
-\ottletbind\ottinterrule
-\ottvalXXspec\ottinterrule
-\ottdefaultXXspec\ottinterrule
-\ottscatteredXXdef\ottinterrule
-\ottregXXid\ottinterrule
-\ottaliasXXspec\ottinterrule
-\ottdecXXspec\ottinterrule
-\ottdef\ottinterrule
-\ottdefs\ottinterrule}
-
-\newpage
-\section{Sail primitive types and functions}
-
-\ottgrammartabular{
-\ottbuiltXXinXXtypes\ottinterrule}
-
-\ottgrammartabular{
-\ottbuiltXXinXXtypeXXabbreviations\ottinterrule
-\ottfunctions\ottinterrule
-\ottfunctionsXXwithXXcoercions\ottinterrule}
-\newpage
-
-\section{Sail type system}
-
-\subsection{Internal type syntax}
-
-\ottgrammartabular{
-\ottk\ottinterrule
-\ottt\ottinterrule
-\ottoptx\ottinterrule
-\otttag\ottinterrule
-\ottne\ottinterrule
-\otttXXarg\ottinterrule
-\otttXXargs\ottinterrule
-\ottnec\ottinterrule
-\ottSXXN\ottinterrule
-\ottEXXd\ottinterrule
-\ottkinf\ottinterrule
-\otttid\ottinterrule
-\ottEXXk\ottinterrule
-\otttinf\ottinterrule
-\ottEXXa\ottinterrule
-\ottfieldXXtyps\ottinterrule
-\ottEXXr\ottinterrule
-\ottenumerateXXmap\ottinterrule
-\ottEXXe\ottinterrule
-\ottEXXt\ottinterrule
-\ottts\ottinterrule
-\ottE\ottinterrule
-\ottI\ottinterrule
-\ottformula\ottinterrule}
-
-
-\subsection{ Type relations }
-\ottdefnss
-
-\section{Sail operational semantics \{TODO\}}
-
-\end{document}