remove obsolete files from language directory.

1 files changed, 0 insertions, 1424 deletions

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]]) }}
-