Small clean up of ott files, start of environments for formal representation of kind and type system

2 files changed, 93 insertions, 363 deletions

diff --git a/language/l2.ott b/language/l2.ott
index 6ce1f140..81671276 100644
--- a/language/l2.ott
+++ b/language/l2.ott
@@ -1,4 +1,4 @@
-indexvar n , i , j , k ::=
+indexvar n , i , j ::=
   {{ phantom }}
   {{ com Index variables for meta-lists }}
 
@@ -916,34 +916,9 @@ defs :: '' ::=
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % Machinery for typing rules                                   %
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ 
+grammar 
 
-%% %% 
-%% %% 
-%% %% 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) }}
@@ -953,13 +928,23 @@ defs :: '' ::=
 %% %%     {{ 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
+
+k :: 'Ki_' ::=
+{{ com Internal kinds }}
+   | K_Typ                                             :: :: typ
+   | K_Nat                                             :: :: nat
+   | K_Ord                                             :: :: ord
+   | K_Efct                                            :: :: efct
+   | K_Val                                             :: :: val {{ com Representing values, for use in identifier checks }}
+   | K_Lam ( k0 .. kn -> k' )                           :: :: ctor
+   | K_infer                                           :: :: infer {{ com Representing an unknown kind, inferred by context }}
+
+t , u :: 'T_' ::=                                {{ phantom }}
+{{ com Internal types }}
+   | id                                           :: :: var
+   | t1 -> t2                                    :: :: fn
+   | t1 * .... * tn                              :: :: tup
+   | id t_args                                    :: :: app 
 %% %%   | t_subst ( t )                               :: M :: subst_app
 %% %%     {{ com Multiple substitutions }}
 %% %%     {{ ocaml (assert false) }}
@@ -1148,19 +1133,6 @@ defs :: '' ::=
 %% %%     {{ 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 }}
@@ -1174,81 +1146,46 @@ defs :: '' ::=
 %% %%      {{ 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) }}
-%% %% 
+ E :: '' ::=                                                     {{ phantom }}
+                                                                 {{ hol ((string,env_body) fmaptree) }}
+                                                                 {{ lem env }}
+ {{ com Environments }}
+ | < E_t , E_k >                                           :: :: E
+  {{ hol arb }}
+  {{ lem (Env [[E_k]] [[E_t]]) }}
+ | E1 u+ E2                                                    :: M :: E_union
+  {{ hol (env_union [[E1]] [[E2]]) }}
+  {{ lem (env_union [[E1]] [[E2]]) }}
+  {{ ocaml assert false }}
+ | empty                                                       :: M :: E_empty
+   {{ hol arb }}
+   {{ lem EnvEmp }}
+   {{ ocaml assert false }}
+ 
+ E_k {{ tex \ottnt{E}^{\textsc{k} } }} :: 'E_k_' ::=             {{ phantom }}
+                                                                 {{ hol (id-> k) }}
+                                                                 {{ lem map id k }}
+   {{ com Kind environments }}
+   | { id1 |-> k1 , .. , idn |-> kn }    :: :: concrete
+     {{ hol (FOLDR (\(k1,k2) E. E |+ (k1,k2)) FEMPTY [[id1 k1 .. idn kn]]) }}
+     {{ lem (List.fold_right (fun (x,v) m -> Pmap.add x v m) [[id1 k1 .. idn kn]] Pmap.empty) }} 
+   | E_k1 u+ .. u+ E_kn                                          :: M :: union
+     {{ hol (FOLDR FUNION FEMPTY [[E_k1..E_kn]]) }}
+     {{ lem (List.fold_right union_map [[E_k1..E_kn]] Pmap.empty) }}
+     {{ ocaml (assert false) }}
+ 
+ E_t {{ tex \ottnt{E}^{\textsc{t} } }} :: 'E_t_' ::=             {{ phantom }}
+                                                                 {{ hol (id |-> t) }}
+                                                                 {{ lem map x f_desc }}
+   {{ com Type environments }}
+   | { id1 |-> t1 , .. , idn |-> tn }                    :: :: concrete
+     {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[id1 t1 .. idn tn]]) }}
+     {{ lem (List.fold_right (fun (x,f) m -> Pmap.add x f m) [[id1 t1 .. idn tn]] Pmap.empty) }} 
+   | E_t1 u+ .. u+ E_tn                                          :: M :: union
+     {{ hol (FOLDR FUNION FEMPTY [[E_t1..E_tn]]) }}
+     {{ lem (List.fold_right union_map [[E_t1..E_tn]] Pmap.empty) }}
+     {{ ocaml (assert false) }}
+
 %% %% tc_abbrev :: 'Tc_abbrev_' ::=                                   {{ phantom }}
 %% %%                                                                 {{ hol t option }}
 %% %%                                                                 {{ lem option t }}
@@ -1375,63 +1312,33 @@ formula :: formula_ ::=
 
   | 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]] }} 
-%% %% 
+   | E_k ( id ) gives k                                      :: :: lookup_k
+     {{ com Kind lookup }}
+     {{ hol (FLOOKUP [[E_k]] [[id]] = SOME [[k]]) }}
+     {{ lem Pmap.find [[id]] [[E_k]] = [[k]] }} 
+
+   | E_t ( id ) gives t                                      :: :: lookup_t
+     {{ com Type lookup }}
+     {{ hol (FLOOKUP [[E_t]] [[id]] = SOME [[t]]) }}
+     {{ lem Pmap.find [[id]] [[E_t]] = [[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 }}
-%% %% 
+
+   | dom ( E_t1 ) inter dom ( E_t2 ) = emptyset                  :: :: E_t_disjoint
+     {{ hol (DISJOINT (FDOM [[E_t1]]) (FDOM [[E_t2]])) }}
+     {{ lem disjoint (Pmap.domain [[E_t1]]) (Pmap.domain [[E_t2]])  }} 
+   
+   | dom ( E_k1 ) inter dom ( E_k2 ) = emptyset                  :: :: E_k_disjoint
+     {{ hol (DISJOINT (FDOM [[E_f1]]) (FDOM [[E_f2]])) }}
+     {{ lem disjoint (Pmap.domain [[E_f1]]) (Pmap.domain [[E_f2]]) }} 
+
 %% %%   | 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) }}
@@ -1450,26 +1357,15 @@ formula :: formula_ ::=
 %% %%   | 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]]) }} 
-%% %% 
+
+   | id NOTIN dom ( E_k )                                         :: :: notin_dom_k
+     {{ hol ([[id]] NOTIN FDOM [[E_k]]) }}
+     {{ lem Pervasives.not (Pmap.mem [[id]] [[E_k]]) }} 
+
 %% %%   | 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 }}
@@ -1540,6 +1436,9 @@ formula :: formula_ ::=
 %freevars
 %t a :: ftv
 
+defns 
+translate_ast :: '' ::=
+
 %% % 
 %% % 
 %% % defns
diff --git a/language/l2_parse.ott b/language/l2_parse.ott
index 4cdb0a53..e06752a0 100644
--- a/language/l2_parse.ott
+++ b/language/l2_parse.ott
@@ -136,43 +136,6 @@ id :: '' ::=
 % targets use alphabetical infix operators. 
 
 
-%% 
-%% x_l {{ tex \ottnt{x}^{l} }} , y_l {{ tex \ottnt{y}^{l} }} , z_l {{ tex \ottnt{z}^{l} }} , name :: '' ::=
-%%   {{ com Location-annotated names }}
-%%   | x l                                         :: :: X_l
-%%   | ( ix ) l                                    :: :: PreX_l
-%%     {{ com Remove infix status }}
-%% 
-%% ix_l {{ tex \ottnt{ix}^{l} }} :: '' ::=
-%%   {{ com Location-annotated infix names }}
-%%   | ix l                                        :: :: SymX_l
-%%   | ` x ` l                                     :: :: InX_l
-%%     {{ com Add infix status }}
-%% 
-%% embed
-%% {{ ocaml
-%% let xl_to_l = function
-%%   | X_l(_,l) -> l
-%%   | PreX_l(_,_,_,l) -> l
-%% 
-%% let ixl_to_l = function
-%%   | SymX_l(_,l) -> l
-%%   | InX_l(_,_,_,l) -> l
-%% }}
-%% {{ lem
-%% 
-%% (*let xl_to_l = function
-%%   | X_l(_,l) -> l
-%%   | PreX_l(_,_,l) -> l
-%% end
-%% 
-%% let ixl_to_l = function
-%%   | SymX_l(_,l) -> l
-%%   | InX_l(_,_,_,l) -> l
-%% end*)
-%% 
-%% }}
-
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % Kinds and Types                                              %
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -181,72 +144,6 @@ id :: '' ::=
 grammar
 
 
-% a :: 'A_' ::=
-%                                                 {{ aux _ l }}
-%                                                 {{ ocaml terminal * text }}
-%                                                 {{ lem terminal * string }}
-%                                                 {{ hol string }}
-%   {{ com Type variables }}
-%   | ' x                                         :: :: A
-%     {{ ichlo [[x]] }}
-% 
-% N :: 'N_' ::=
-%                                                    {{ aux _ l }}
-%                                                    {{ ocaml terminal * text }}
-%                                                    {{ lem terminal * string }}
-%                                                    {{ hol string }}
-%     {{ com numeric variables }} 
-%     | ' ' x                                        :: :: N
-%       {{ ichlo [[x]] }}
-% 
-% EN :: 'EN_' ::=
-%                                                    {{ aux _ l }}
-%                                                    {{ ocaml terminal * text }}
-%                                                    {{ lem terminal * string }}
-%                                                    {{ hol string }}
-%     {{ com endianness variables }} 
-%     | ' ' ' x                                     :: :: EN
-%       {{ ichlo [[x]] }}
-% 
-% EFF :: 'EFF_' ::=
-%                                                    {{ aux _ l }}
-%                                                    {{ ocaml terminal * text }}
-%                                                    {{ lem terminal * string }}
-%                                                    {{ hol string }}
-%     {{ com effect set variables }} 
-%     | ' ' ' ' x                                     :: :: EFF
-%       {{ ichlo [[x]] }}
-% % TODO: better concrete syntax!!!!
-% 
-% 
-% tnvar :: '' ::=                         
-%     {{ com variables of the base kinds }}
-%     | a                                 :: :: Av
-%     | N                                 :: :: Nv
-%     | EN                                :: :: ENv
-%     | EFF                               :: :: EFFv
-% 
-% tnvars :: '' ::=                                {{ phantom }}
-%                                                 {{ hol tnvar list }}
-%                                                 {{ ocaml tnvar list }}
-%                                                 {{ lem list tnvar }}
-%   {{ com Type variable lists }}
-%   | tnvar1 .. tnvarn            :: :: Tvars
-%     {{ hol [[tnvar1..tnvarn]] }}
-%     {{ ocaml [[tnvar1..tnvarn]] }}
-%     {{ lem [[tnvar1..tnvarn]] }}
-%     
-% 
-% ids :: '' ::=                                {{ phantom }}
-%                                                 {{ hol id list }}
-%                                                 {{ ocaml id list }}
-%                                                 {{ lem list id }}
-%   {{ com Type variable lists }}
-%   | id1 .. idn            :: :: Tvars
-%     {{ hol [[id1..idn]] }}
-%     {{ ocaml [[id1..idn]] }}
-%     {{ lem [[id1..idn]] }}
-    
 
 base_kind :: 'BK_' ::=  
   {{ com base kind}}
@@ -274,33 +171,27 @@ efct :: 'Effect_' ::=
   | nondet                              :: :: nondet {{ com nondeterminism from intra-instruction parallelism }}
 
 atyp :: 'ATyp_' ::=
-  {{ com expression of all kinds }}
+  {{ com expressions of all kinds, to be translated to types, nats, orders, and effects after parsing }}
   {{ aux _ l }}
   | id                                  :: :: id          {{ com identifier }}
   | num                                 :: :: constant     {{ com constant }}
   | atyp1 * atyp2                       :: :: times        {{ com product }}
-%{{ com must be linear after normalisation... except for the type of *, ahem }}
   | atyp1 + atyp2                       :: :: sum          {{ com sum }}
   | 2 ** atyp                            :: :: exp         {{ com exponential }}
   | ( atyp )                            :: S :: paren  {{ icho [[atyp]] }}
 
   | inc                                 :: :: inc  {{ com increasing (little-endian) }}
   | dec                                 :: :: dec  {{ com decreasing (big-endian) }}
- | effect id                            :: :: efid
- | effect { efct1 , .. , efctn }           :: :: set {{ com effect set }}
- | pure                                 :: M :: pure {{ com sugar for empty effect set }} {{ icho [] }}
-
-% TODO: are we going to need any effect polymorphism?  Conceivably for built-in maps and folds.  Yes.  But we think we don't need any interesting effect-set expressions, eg effectset-variable union {rreg}. 
+  | effect id                            :: :: efid
+  | effect { efct1 , .. , efctn }           :: :: set {{ com effect set }}
+  | pure                                 :: M :: pure {{ com sugar for empty effect set }} {{ icho [] }}
 
   | _                                           :: :: wild
     {{ com Unspecified type }}
   | atyp1 -> atyp2 atyp3                        :: :: fn
-    {{ com Function type (first-order only in user code) }}
-% TODO: build first-order restriction into AST or just into type rules? neither - see note
-% TODO: concrete syntax for effects in a function type?  needed only for pp, not in user syntax.
+    {{ com Function type (first-order only in user code), last atyp is an effect }}
   | atyp1 * .... * atypn                          :: :: tup
     {{ com Tuple type }}
-% TODO union in the other kind grammars?  or make a syntax of argument? or glom together the grammars and leave o the typechecker
   | id atyp1 .. atypn                     :: :: app
   {{ com type constructor application }}
 
@@ -341,15 +232,12 @@ parsing
 ATyp_tup <= ATyp_tup
 ATyp_fn right ATyp_fn
 ATyp_fn <= ATyp_tup
-%Typ_fn right Typ_app1
-%Typ_tup right Typ_app1
 
 grammar
 
 nexp_constraint :: 'NC_' ::=
   {{ com constraint over kind $[[Nat]]$ }}
   {{ aux _ l }}
-%  {{ aux _ annot }} {{ auxparam 'a }}
   | atyp = atyp'                                :: :: fixed
   | atyp >= atyp'                               :: :: bounded_ge
   | atyp '<=' atyp'                             :: :: bounded_le
@@ -372,16 +260,12 @@ quant_item :: 'QI_' ::=
 
 typquant :: 'TypQ_' ::= 
   {{ com type quantifiers and constraints}}
-%  {{ aux _ annot }} {{ auxparam 'a }}
   {{ aux _ l }}
   | forall quant_item1 , ... , quant_itemn . :: :: tq {{ texlong }}
-
-% WHY ARE CONSTRAINTS HERE AND NOT IN THE KIND LANGUAGE
   |                           ::  ::  no_forall     {{ com sugar, omitting quantifier and constraints }}
 
 typschm :: 'TypSchm_' ::=
   {{ com type scheme  }}
-%  {{ aux _ annot }} {{ auxparam 'a }}
   {{ aux _ l }}
   |  typquant atyp                                                       :: :: ts
 
@@ -395,58 +279,26 @@ grammar
 ctor_def :: 'CT_' ::=
   {{ com Datatype constructor definition clause }}
   {{ aux _ l }}
-%  {{ aux _ annot }} {{ auxparam 'a }}
   | id : typschm                                       :: :: ct
 % but we could get away with disallowing constraints in typschm, we
 % think - if it's useful to do that
 
-%enum_opt :: 'EnumOpt_' ::=
-%  |      :: :: empty
-%  | enum :: :: enum
-
-%% tdefbody :: 'TD_' ::=
-%%   {{ com Type definition bodies }}
-%%   | typschm                                                     :: :: abbrev
-%%     {{ com Type abbreviations }}
-%%   | typquant <| id1 : atyp1 ; ... ; idn : atypn semi_opt |>     :: :: record
-%%     {{ com Record types }}
-%%   | enumeration_flag_opt '|' ctor_def1 '|' ... '|' ctor_defn            :: :: variant
-%%     {{ com Variant types }}
-%% 
  naming_scheme_opt :: 'Name_sect_' ::=
    {{ com Optional variable-naming-scheme specification for variables of defined type }} 
    {{ aux _ l }}
    |                                                   :: :: none
    | [ name = regexp ]                                 :: :: some
-%% 
-%% type_def :: '' ::=
-%%   {{ com Type definitions }}
-%%   | type id : kind naming_scheme_opt = tdefbody                                :: :: Td
-%% %  | enumeration id naming_scheme_opt = tdefbody                               ::   :: Td2
-%% % the enumeration is sugar for something that uses an enum flag, where the type system will restrict the tdefbody to be a simple enum...
-%% 
-
-% TODO: do we need mutually recursive type definitions?  
-
-
-%%% OR, IN C STYLE
 
 type_def :: 'TD_' ::=
   {{ com Type definition body }}
   {{ aux _ l }}
-%  {{ aux _ annot }} {{ auxparam 'a }}
   | typedef id naming_scheme_opt = typschm                                        :: :: abbrev
     {{ com type abbreviation }} {{ texlong }}
   | typedef id naming_scheme_opt = const struct typquant { atyp1 id1 ; ... ; atypn idn semi_opt }     :: :: record
     {{ com struct type definition }} {{ texlong }}
-% for specifying constructor result types of nat-indexed GADTs, we can
-%  let the typi be function types (as constructors are not allowed to
-%  take parameters of function types)
-% concrete syntax: to be even closer to C, could have a postfix id rather than prefix id = 
   | typedef id naming_scheme_opt = const union typquant { atyp1 id1 ; ... ; atypn idn semi_opt }   :: :: variant
     {{ com union type definition}} {{ texlong }}
-
-  | typedef id naming_scheme_opt = enum { id1 ; ... ; idn semi_opt }   :: :: enum
+  | typedef id naming_scheme_opt = enumerate { id1 ; ... ; idn semi_opt }   :: :: enum
     {{ com enumeration type definition}} {{ texlong }}
 
   | typedef  id = register bits [ atyp : atyp' ] { index_range1 : id1 ; ... ; index_rangen : idn } 
@@ -510,45 +362,30 @@ semi_opt {{ tex \ottnt{;}^{?} }} :: 'semi_' ::=         {{ phantom }}
 pat :: 'P_' ::= 
   {{ com Pattern }}
   {{ aux _ l }}
-%  {{ aux _ annot }} {{ auxparam 'a }}
   | lit                                                 :: :: lit
     {{ com literal constant pattern }}
   | _                                                   :: :: wild  
     {{ com wildcard }}
   | ( pat as id )                                      :: :: as
     {{ com named pattern }}
-% ML-style
-%  | ( pat : typ )                                       :: :: typ
-%    {{ com Typed patterns }}
-% C-style
   | ( < atyp > pat )                                       :: :: typ
     {{ com typed pattern }}
 
   | id                                      :: :: id
     {{ com identifier  }}
 
-%
   | id pat1 .. patn                                     :: :: app
     {{ com union constructor pattern }}
 
-% OR?  do we invent something ghastly including a union keyword?  Perhaps not...
-
-%  | <| fpat1 ; ... ; fpatn semi_opt |>                  :: :: record
-%    {{ com Record patterns }}
-% OR
   | { fpat1 ; ... ; fpatn semi_opt }                  :: :: record
     {{ com struct pattern }}
 
-%Patterns for vectors
-%Should these be the same since vector syntax has changed, and lists have also changed?
-
   | [ pat1 , .. , patn  ]                     :: :: vector
    {{ com vector pattern }}
 
   | [ num1 = pat1 , .. , numn = patn  ]                     :: :: vector_indexed
    {{ com vector pattern (with explicit indices) }}
 
-% cf ntoes for this
   |  pat1 : .... : patn                                   :: :: vector_concat
   {{ com concatenated vector pattern }} 
 
@@ -558,15 +395,10 @@ pat :: 'P_' ::=
     {{ com list pattern }}
   | ( pat )                                             :: S :: paren
 {{ ichlo [[pat]] }}
-%  | pat1 '::' pat2                                      :: :: cons
-%    {{ com Cons patterns }}
-%  | id '+' num                                         :: :: num_add
-%    {{ com constant addition patterns }}
 
 fpat :: 'FP_' ::=
   {{ com Field pattern }}
   {{ aux _ l }}
-%  {{ aux _ annot }} {{ auxparam 'a }}
   | id = pat                                            :: :: Fpat
 
 parsing
@@ -584,7 +416,6 @@ grammar
 exp :: 'E_' ::=
   {{ com Expression }}
   {{ aux _ l }}
-%  {{ aux _ annot }} {{ auxparam 'a }}  
 
   | { exp1 ; ... ; expn }                               :: :: block {{ com block (parsing conflict with structs?) }}
 % maybe we really should have indentation-sensitive syntax :-)  (given that some of the targets do)