and matching .ott

3 files changed, 259 insertions, 240 deletions

diff --git a/language/Makefile b/language/Makefile
index f1607d23..595a09e8 100644
--- a/language/Makefile
+++ b/language/Makefile
@@ -8,7 +8,7 @@ l2.pdf: l2.tex
 l2Theory.uo: l2Script.sml
 	Holmake --qof -I $(OTTLIB) l2Theory.uo
 
-l2.tex ../src/ast.ml l2Script.sml: l2.ott
+l2.tex ../src/ast.ml l2Script.sml: l2.ott ../../../rsem/ott/src/ott
 	ott -sort false -generate_aux_rules false -o l2.tex  -picky_multiple_parses true l2.ott
 	ott -sort false -generate_aux_rules true -ocaml_include_terminals true -o ../src/ast.ml -o l2Script.sml -picky_multiple_parses true l2.ott
 
@@ -21,6 +21,6 @@ l2.lem: l2.ott
 
 clean:
 	rm -rf *~
-	-rm -rf *.uo *.ui l2Theory.sig l2Theory.sml l2.tex l2Script.sml l2.aux l2.log l2.dvi l2.ps l2_unwrapped.tex .HOLMK 
+	-rm -rf *.uo *.ui l2Theory.sig l2Theory.sml l2.tex l2Script.sml l2.aux l2.log l2.dvi l2.ps l2_unwrapped.tex .HOLMK  l2.ml
 #l2.sys l2 library/lib_cache
 
diff --git a/language/l2.ott b/language/l2.ott
index e25d7547..1cc9b3fd 100644
--- a/language/l2.ott
+++ b/language/l2.ott
@@ -49,26 +49,30 @@ metavar regexp ::=
 embed
 {{ ocaml
 
-type text = Ulib.Text.t
 
-type l =
+
+type text = string (* was Ulib.Text.t *)
+
+type 'a l = 'a
+(*
   | Unknown
   | Trans of string * l option
   | Range of Lexing.position * Lexing.position
-
-exception Parse_error_locn of l * string
+*)
+exception Parse_error_locn of string l * string
 
 type ml_comment = 
-  | Chars of Ulib.Text.t
+  | Chars of text
   | Comment of ml_comment list
 
 type lex_skip =
   | Com of ml_comment
-  | Ws of Ulib.Text.t
+  | Ws of text
   | Nl
 
 type lex_skips = lex_skip list option
 
+(*
 let pp_lex_skips ppf sk = 
   match sk with
     | None -> ()
@@ -89,7 +93,7 @@ let combine_lex_skips s1 s2 =
     | (None,_) -> s2
     | (_,None) -> s1
     | (Some(s1),Some(s2)) -> Some(s2@s1)
-
+*)
 type terminal = lex_skips
 
 }}
@@ -156,9 +160,9 @@ metavar ix ::=
 grammar
 
 l :: '' ::=                                     {{ phantom }}
-                                                {{ ocaml l }}
+                                                {{ ocaml 'a l }}
                                                 {{ lem l }}
-                                                {{ hol unit }}
+                                                {{ hol unit }} 
   {{ com Source location }}
   |                                             :: :: Unknown
     {{ ocaml Unknown }}
@@ -167,7 +171,7 @@ l :: '' ::=                                     {{ phantom }}
 
 id :: '' ::=
   {{ com Identifier }}
-  {{ aux _ l }}
+  {{ aux _ l }}  {{ auxparam 'a }}
   | x                           :: :: id
   | ( x )                       :: :: deIid {{ com remove infix status }}
 % Note: we have just a single namespace. We don't want the same
@@ -224,7 +228,7 @@ grammar
 
 
 % a :: 'A_' ::=
-%                                                 {{ aux _ l }}
+%                                                 {{ aux _ l }}  {{ auxparam 'a }}
 %                                                 {{ ocaml terminal * text }}
 %                                                 {{ lem terminal * string }}
 %                                                 {{ hol string }}
@@ -233,7 +237,7 @@ grammar
 %     {{ ichlo [[x]] }}
 % 
 % N :: 'N_' ::=
-%                                                    {{ aux _ l }}
+%                                                    {{ aux _ l }}  {{ auxparam 'a }}
 %                                                    {{ ocaml terminal * text }}
 %                                                    {{ lem terminal * string }}
 %                                                    {{ hol string }}
@@ -242,7 +246,7 @@ grammar
 %       {{ ichlo [[x]] }}
 % 
 % EN :: 'EN_' ::=
-%                                                    {{ aux _ l }}
+%                                                    {{ aux _ l }}  {{ auxparam 'a }}
 %                                                    {{ ocaml terminal * text }}
 %                                                    {{ lem terminal * string }}
 %                                                    {{ hol string }}
@@ -251,7 +255,7 @@ grammar
 %       {{ ichlo [[x]] }}
 % 
 % EFF :: 'EFF_' ::=
-%                                                    {{ aux _ l }}
+%                                                    {{ aux _ l }}  {{ auxparam 'a }}
 %                                                    {{ ocaml terminal * text }}
 %                                                    {{ lem terminal * string }}
 %                                                    {{ hol string }}
@@ -292,7 +296,7 @@ grammar
 
 base_kind :: 'BK_' ::=  
   {{ com base kind}}
-  {{ aux _ l }}
+  {{ aux _ l }}  {{ auxparam 'a }}
   | Type                                       :: :: type    {{ com kind of types  }} 
   | Nat                                        :: :: nat     {{ com kind of natural number size expressions  }} 
   | Order                                     :: :: order  {{ com kind of vector order specifications  }} 
@@ -300,14 +304,14 @@ base_kind :: 'BK_' ::=
 
 kind :: 'K_' ::=  
   {{ com kinds}}
-  {{ aux _ l }}
+  {{ aux _ l }}  {{ auxparam 'a }}
   | base_kind1 -> ... -> base_kindn            :: :: kind 
 % we'll never use  ...-> Nat
 
     
 nexp :: 'Nexp_' ::=  
   {{ com expression of kind $[[Nat]]$, for vector sizes and origins }}
-  {{ aux _ l }}
+  {{ aux _ l }}  {{ auxparam 'a }}
   | id                                  :: :: id          {{ com identifier }}
   | num                                 :: :: constant     {{ com constant }}
   | nexp1 * nexp2                       :: :: times        {{ com product }}
@@ -318,7 +322,7 @@ nexp :: 'Nexp_' ::=
 
 order :: 'Ord_' ::=  
   {{ com vector order specifications, of kind $[[Order]]$}}
-  {{ aux _ l }}
+  {{ aux _ l }}  {{ auxparam 'a }}
   | id                                  :: :: id  {{ com identifier }}
   | inc                                 :: :: inc  {{ com increasing (little-endian) }}
   | dec                                 :: :: dec  {{ com decreasing (big-endian) }}
@@ -326,7 +330,7 @@ order :: 'Ord_' ::=
 
 effect :: 'Effect_' ::=
   {{ com effect }}
-  {{ aux _ l }} 
+  {{ aux _ l }}  {{ auxparam 'a }}
   | rreg                                :: :: rreg {{ com read register }}
   | wreg                                :: :: wreg {{ com write register }}
   | rmem                                :: :: rmem {{ com read memory }}
@@ -338,7 +342,7 @@ effect :: 'Effect_' ::=
 
 effects :: 'Effects_' ::=
   {{ com effect set, of kind $[[Effects]]$ }}
-  {{ aux _ l }}
+  {{ aux _ l }}  {{ auxparam 'a }}
  | id                                  :: :: var
  | { effect1 , .. , effectn }           :: :: set {{ com effect set }}
  | pure                                 :: M :: pure {{ com sugar for empty effect set }} {{ icho [] }}
@@ -347,7 +351,7 @@ effects :: 'Effects_' ::=
 
 
 typ :: 'Typ_' ::=
-  {{ com Type expressions, of kind $[[Type]]$ }}
+  {{ com Type expressions, of kind $[[Type]]$ }} {{ aux _ l }}  {{ auxparam 'a }} 
   | _                                           :: :: wild
     {{ com Unspecified type }}
   | id                                         :: :: var
@@ -364,7 +368,7 @@ typ :: 'Typ_' ::=
   | ( typ )                            :: S :: paren {{ icho [[typ]] }} 
 
 typ_arg :: 'Typ_arg_' ::=
-  {{ com Type constructor arguments of all kinds }}
+  {{ com Type constructor arguments of all kinds }} {{ aux _ l}}
   | nexp       :: :: nexp
   | typ        :: :: typ
   | order     :: :: order
@@ -374,7 +378,7 @@ typ_arg :: 'Typ_arg_' ::=
 
 typ_lib :: 'Typ_lib_' ::=
   {{ com library types and syntactic sugar for them }}
-  {{ aux _ l }}
+  {{ aux _ l }}  {{ auxparam 'a }}
 % boring base types:
   | unit :: :: unit {{ com unit type with value $()$ }}
   | bool :: :: bool {{ com booleans $[[true]]$ and $[[false]]$ }}
@@ -413,7 +417,7 @@ grammar
 
 nexp_constraint :: 'NC_' ::=
   {{ com constraint over kind $[[Nat]]$ }}
-  {{ aux _ l }}
+  {{ aux _ l }}  {{ auxparam 'a }}
   | nexp = nexp'                                :: :: fixed
   | nexp >= nexp'                               :: :: bounded_ge
   | nexp '<=' nexp'                             :: :: bounded_le
@@ -423,13 +427,13 @@ nexp_constraint :: 'NC_' ::=
 % finite-set-bound, as we don't think we need anything more
 
 kinded_id :: 'KOpt_' ::=
-  {{ com optionally kind-annotated identifier }}
+  {{ com optionally kind-annotated identifier }} {{ aux _ l }}  {{ auxparam 'a }}
   | id	 	    		   	      :: :: none {{ com identifier }}
   | kind id				      :: :: kind {{ com kind-annotated variable }}
   | ( kinded_id ) 			      :: S :: paren {{ icho [[kinded_id]] }}
 
 typquant :: 'TypQ_' ::= 
-  {{ aux _ l }} {{ com type quantifiers and constraints}}
+  {{ aux _ l }}  {{ auxparam 'a }} {{ com type quantifiers and constraints}}
   | forall kinded_id1 ... kinded_idn . nexp_constraint1 , ... , nexp_constrainti . :: :: tq {{ texlong }}
 
 % WHY ARE CONSTRAINTS HERE AND NOT IN THE KIND LANGUAGE
@@ -439,7 +443,7 @@ typquant :: 'TypQ_' ::=
 
 typschm :: 'TypSchm_' ::=
     {{ com type scheme  }}
-  {{ aux _ l }}
+  {{ aux _ l }}  {{ auxparam 'a }}
   |  typquant typ                                                       :: :: ts
 
 
@@ -559,7 +563,7 @@ semi_opt {{ tex \ottnt{;}^{?} }} :: 'semi_' ::=         {{ phantom }}
 
 pat :: 'P_' ::= 
   {{ com Pattern }}
-  {{ aux _ l }}
+  {{ aux _ l }}  {{ auxparam 'a }}
   | lit                                                 :: :: lit
     {{ com literal constant pattern }}
   | _                                                   :: :: wild  
@@ -614,7 +618,7 @@ pat :: 'P_' ::=
 
 fpat :: 'FP_' ::=
   {{ com Field pattern }}
-  {{ aux _ l }}
+  {{ aux _ l }}  {{ auxparam 'a }}
   | id = pat                                            :: :: Fpat
 
 parsing
@@ -631,7 +635,7 @@ grammar
 
 exp :: 'E_' ::=
   {{ com Expression }}
-  {{ aux _ l }}  
+  {{ aux _ l }}  {{ 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)
@@ -746,23 +750,23 @@ lexp :: 'LEXP_' ::= {{ com lvalue expression }}
 
 fexp :: 'FE_' ::=
   {{ com Field-expression }}
-  {{ aux _ l }}
+  {{ aux _ l }}  {{ auxparam 'a }}
   | id = exp                                            :: :: Fexp
 
 fexps :: 'FES_' ::=
   {{ com Field-expression list }}
-  {{ aux _ l }}
+  {{ aux _ l }}  {{ auxparam 'a }}
   | fexp1 ; ... ; fexpn semi_opt                        :: :: Fexps
 
 pexp :: 'Pat_' ::=
   {{ com Pattern match }}
-  {{ aux _ l }}
+  {{ aux _ l }}  {{ auxparam 'a }}
   | pat -> exp                                  :: :: exp
 % apparently could use -> or => for this.
 
 %% % psexp :: 'Pats' ::=
 %% %   {{ com Multi-pattern matches }}
-%% %   {{ aux _ l }}
+%% %   {{ aux _ l }}  {{ auxparam 'a }}
 %% %   | pat1 ... patn -> exp                                :: :: exp
 
 
@@ -803,12 +807,12 @@ grammar
 %% % 
 %% % lem_funcl :: 'LEM_FCL' ::=
 %% %   {{ com Function clauses }}
-%% %   {{ aux _ l }}
+%% %   {{ aux _ l }}  {{ auxparam 'a }}
 %% %   | id pat1 ... patn tannot_opt = exp                   :: :: Funcl
 %% % 
 %% % lem_letbind :: 'LEM_LB_' ::=
 %% %   {{ com Let bindings }}
-%% %   {{ aux _ l }}
+%% %   {{ aux _ l }}  {{ auxparam 'a }}
 %% %   | pat tannot_opt = exp                                :: :: Let_val
 %% %     {{ com Value bindings }}
 %% %   | lem_funcl                                           :: :: Let_fun
@@ -818,7 +822,7 @@ grammar
 %% % grammar
 %% % lem_val_def :: 'LEM_VD' ::= 
 %% %   {{ com Value definitions }}
-%% %   {{ aux _ l }}
+%% %   {{ aux _ l }}  {{ auxparam 'a }}
 %% %   | let lem_letbind                                     :: :: Let_def
 %% %     {{ com Non-recursive value definitions }}
 %% %   | let rec  lem_funcl1 and ... and lem_funcln          :: :: Let_rec
@@ -826,7 +830,7 @@ grammar
 %% % 
 %% % lem_val_spec :: 'LEM_VS' ::=
 %% %   {{ com Value type specifications }} 
-%% %   {{ aux _ l }}
+%% %   {{ aux _ l }}  {{ auxparam 'a }}
 %% %   | val x_l : typschm                                           :: :: Val_spec
 
 %%%%% C-ish style %%%%%%%%%%
@@ -837,24 +841,24 @@ tannot_opt :: 'Typ_annot_opt_' ::=
   | typ_quant typ                               :: :: some 
 
 rec_opt :: 'Rec_' ::=
-  {{ aux _ l }} {{ com Optional recursive annotation for functions }}
+  {{ aux _ l }}  {{ auxparam 'a }} {{ com Optional recursive annotation for functions }}
   |                                             :: :: nonrec {{ com non-recursive }}
   | rec                                         :: :: rec {{ com recursive }}
 
 effects_opt :: 'Effects_opt_' ::=
-  {{ aux _ l }} {{ com Optional effect annotation for functions }}
+  {{ aux _ l }}  {{ auxparam 'a }} {{ com Optional effect annotation for functions }}
   |                                             :: :: pure {{ com sugar for empty effect set }}
   | effects                                     :: :: effects
 
 funcl :: 'FCL_' ::=
   {{ com Function clause }}
-  {{ aux _ l }}
+  {{ aux _ l }}  {{ auxparam 'a }}
   | id pat = exp                   :: :: Funcl
 
 
 fundef :: 'FD_' ::=
   {{ com Function definition}}
-  {{ aux _ l }}
+  {{ aux _ l }}  {{ auxparam 'a }}
   | function rec_opt tannot_opt effects_opt funcl1 and ... and funcln :: :: function {{ texlong }}  
 % {{ com function definition }}
 % TODO note that the typ in the tannot_opt is the *result* type, not
@@ -866,7 +870,7 @@ fundef :: 'FD_' ::=
 
 letbind :: 'LB_' ::=
   {{ com Let binding }}
-  {{ aux _ l }}
+  {{ aux _ l }}  {{ auxparam 'a }}
   | typschm pat = exp                                :: :: val_explicit
     {{ com value binding, explicit type ([[pat]] must be total)}}
   | let pat = exp                                    :: :: val_implicit
@@ -875,12 +879,12 @@ letbind :: 'LB_' ::=
 
 val_spec :: 'VS_' ::=
   {{ com Value type specification }} 
-  {{ aux _ l }}
+  {{ aux _ l }}  {{ auxparam 'a }}
   | val typschm id                                  :: :: val_spec
 
 default_typing_spec :: 'DT_' ::=
   {{ com Default kinding or typing assumption }}
-  {{ aux _ l }}
+  {{ aux _ l }}  {{ auxparam 'a }}
   | default base_kind id    :: :: kind
   | default typschm id      :: :: typ
 % The intended semantics of these is that if an id in binding position
@@ -896,7 +900,7 @@ default_typing_spec :: 'DT_' ::=
 
 def :: 'DEF_' ::=
   {{ com Top-level definition }}
-  {{ aux _ l }}
+  {{ aux _ l }}  {{ auxparam 'a }}
   | type_def                                                    :: :: type
     {{ com type definition }}
   | fundef                                                   :: :: fundef
@@ -923,7 +927,7 @@ def :: 'DEF_' ::=
 
 defs :: '' ::=
   {{ com Definition sequence }}
-%  {{ aux _ l }}
+%  {{ aux _ l }}  {{ auxparam 'a }} 
   | def1  .. defn                 :: :: Defs
 
 
diff --git a/src/ast.ml b/src/ast.ml
index 5a307aa5..09008f05 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -1,26 +1,30 @@
 (* generated by Ott 0.22 from: l2.ott *)
 
 
-type text = Ulib.Text.t
 
-type l =
+
+type text = string (* was Ulib.Text.t *)
+
+type 'a l = 'a
+(*
   | Unknown
   | Trans of string * l option
   | Range of Lexing.position * Lexing.position
-
-exception Parse_error_locn of l * string
+*)
+exception Parse_error_locn of string l * string
 
 type ml_comment = 
-  | Chars of Ulib.Text.t
+  | Chars of text
   | Comment of ml_comment list
 
 type lex_skip =
   | Com of ml_comment
-  | Ws of Ulib.Text.t
+  | Ws of text
   | Nl
 
 type lex_skips = lex_skip list option
 
+(*
 let pp_lex_skips ppf sk = 
   match sk with
     | None -> ()
@@ -41,7 +45,7 @@ let combine_lex_skips s1 s2 =
     | (None,_) -> s2
     | (_,None) -> s1
     | (Some(s1),Some(s2)) -> Some(s2@s1)
-
+*)
 type terminal = lex_skips
 
 
@@ -49,31 +53,36 @@ type x = terminal * text (* identifier *)
 type ix = terminal * text (* infix identifier *)
 
 type 
-id_aux =  (* Identifier *)
+'a base_kind_aux =  (* base kind *)
+   BK_type of terminal (* kind of types *)
+ | BK_nat of terminal (* kind of natural number size expressions *)
+ | BK_order of terminal (* kind of vector order specifications *)
+ | BK_effects of terminal (* kind of effect sets *)
+
+
+type 
+'a id_aux =  (* Identifier *)
    Id of x
  | DeIid of terminal * x * terminal (* remove infix status *)
 
 
 type 
-base_kind_aux =  (* base kind *)
-   BK_type of terminal (* kind of types *)
- | BK_nat of terminal (* kind of natural number size expressions *)
- | BK_order of terminal (* kind of vector order specifications *)
- | BK_effects of terminal (* kind of effect sets *)
+'a base_kind = 
+   BK_aux of 'a base_kind_aux * 'a l
 
 
 type 
-id = 
-   Id_aux of id_aux * l
+'a id = 
+   Id_aux of 'a id_aux * 'a l
 
 
 type 
-base_kind = 
-   BK_aux of base_kind_aux * l
+'a kind_aux =  (* kinds *)
+   K_kind of ('a base_kind * terminal) list
 
 
 type 
-effect_aux =  (* effect *)
+'a effect_aux =  (* effect *)
    Effect_rreg of terminal (* read register *)
  | Effect_wreg of terminal (* write register *)
  | Effect_rmem of terminal (* read memory *)
@@ -84,104 +93,110 @@ effect_aux =  (* effect *)
 
 
 type 
-nexp_aux =  (* expression of kind $_$, for vector sizes and origins *)
-   Nexp_id of id (* identifier *)
+'a nexp_aux =  (* expression of kind $_$, for vector sizes and origins *)
+   Nexp_id of 'a id (* identifier *)
  | Nexp_constant of terminal * int (* constant *)
- | Nexp_times of nexp * terminal * nexp (* product *)
- | Nexp_sum of nexp * terminal * nexp (* sum *)
- | Nexp_exp of terminal * terminal * nexp (* exponential *)
+ | Nexp_times of 'a nexp * terminal * 'a nexp (* product *)
+ | Nexp_sum of 'a nexp * terminal * 'a nexp (* sum *)
+ | Nexp_exp of terminal * terminal * 'a nexp (* exponential *)
 
-and nexp = 
-   Nexp_aux of nexp_aux * l
+and 'a nexp = 
+   Nexp_aux of 'a nexp_aux * 'a l
 
 
 type 
-kind_aux =  (* kinds *)
-   K_kind of (base_kind * terminal) list
+'a kind = 
+   K_aux of 'a kind_aux * 'a l
 
 
 type 
-effect = 
-   Effect_aux of effect_aux * l
+'a effect = 
+   Effect_aux of 'a effect_aux * 'a l
 
 
 type 
-nexp_constraint_aux =  (* constraint over kind $_$ *)
-   NC_fixed of nexp * terminal * nexp
- | NC_bounded_ge of nexp * terminal * nexp
- | NC_bounded_le of nexp * terminal * nexp
- | NC_nat_set_bounded of id * terminal * terminal * (terminal * int * terminal) list * terminal
+'a nexp_constraint_aux =  (* constraint over kind $_$ *)
+   NC_fixed of 'a nexp * terminal * 'a nexp
+ | NC_bounded_ge of 'a nexp * terminal * 'a nexp
+ | NC_bounded_le of 'a nexp * terminal * 'a nexp
+ | NC_nat_set_bounded of 'a id * terminal * terminal * (terminal * int * terminal) list * terminal
 
 
 type 
-kind = 
-   K_aux of kind_aux * l
+'a kinded_id_aux =  (* optionally kind-annotated identifier *)
+   KOpt_none of 'a id (* identifier *)
+ | KOpt_kind of 'a kind * 'a id (* kind-annotated variable *)
 
 
 type 
-effects_aux =  (* effect set, of kind $_$ *)
-   Effects_var of id
- | Effects_set of terminal * (effect * terminal) list * terminal (* effect set *)
+'a order_aux =  (* vector order specifications, of kind $_$ *)
+   Ord_id of 'a id (* identifier *)
+ | Ord_inc of terminal (* increasing (little-endian) *)
+ | Ord_dec of terminal (* decreasing (big-endian) *)
 
 
 type 
-order_aux =  (* vector order specifications, of kind $_$ *)
-   Ord_id of id (* identifier *)
- | Ord_inc of terminal (* increasing (little-endian) *)
- | Ord_dec of terminal (* decreasing (big-endian) *)
+'a effects_aux =  (* effect set, of kind $_$ *)
+   Effects_var of 'a id
+ | Effects_set of terminal * ('a effect * terminal) list * terminal (* effect set *)
 
 
 type 
-nexp_constraint = 
-   NC_aux of nexp_constraint_aux * l
+'a nexp_constraint = 
+   NC_aux of 'a nexp_constraint_aux * 'a l
 
 
 type 
-kinded_id =  (* optionally kind-annotated identifier *)
-   KOpt_none of id (* identifier *)
- | KOpt_kind of kind * id (* kind-annotated variable *)
+'a kinded_id = 
+   KOpt_aux of 'a kinded_id_aux * 'a l
 
 
 type 
-effects = 
-   Effects_aux of effects_aux * l
+'a order = 
+   Ord_aux of 'a order_aux * 'a l
 
 
 type 
-order = 
-   Ord_aux of order_aux * l
+'a effects = 
+   Effects_aux of 'a effects_aux * 'a l
 
 
 type 
-typquant_aux =  (* type quantifiers and constraints *)
-   TypQ_tq of terminal * (kinded_id) list * terminal * (nexp_constraint * terminal) list * terminal
- | TypQ_no_constraint of terminal * (kinded_id) list * terminal (* sugar, omitting constraints *)
+'a typquant_aux =  (* type quantifiers and constraints *)
+   TypQ_tq of terminal * ('a kinded_id) list * terminal * ('a nexp_constraint * terminal) list * terminal
+ | TypQ_no_constraint of terminal * ('a kinded_id) list * terminal (* sugar, omitting constraints *)
  | TypQ_no_forall (* sugar, omitting quantifier and constraints *)
 
 
 type 
-typ =  (* Type expressions, of kind $_$ *)
+'a typ_aux =  (* Type expressions, of kind $_$ *)
    Typ_wild of terminal (* Unspecified type *)
- | Typ_var of id (* Type variable *)
- | Typ_fn of typ * terminal * typ * effects (* Function type (first-order only in user code) *)
- | Typ_tup of (typ * terminal) list (* Tuple type *)
- | Typ_app of id * (typ_arg) list (* type constructor application *)
+ | Typ_var of 'a id (* Type variable *)
+ | Typ_fn of 'a typ * terminal * 'a typ * 'a effects (* Function type (first-order only in user code) *)
+ | Typ_tup of ('a typ * terminal) list (* Tuple type *)
+ | Typ_app of 'a id * (typ_arg) list (* type constructor application *)
+
+and 'a typ = 
+   Typ_aux of 'a typ_aux * 'a l
+
+and typ_arg_aux =  (* Type constructor arguments of all kinds *)
+   Typ_arg_nexp of 'a nexp
+ | Typ_arg_typ of 'a typ
+ | Typ_arg_order of 'a order
+ | Typ_arg_effects of 'a effects
 
-and typ_arg =  (* Type constructor arguments of all kinds *)
-   Typ_arg_nexp of nexp
- | Typ_arg_typ of typ
- | Typ_arg_order of order
- | Typ_arg_effects of effects
+and typ_arg = 
+   Typ_arg_aux of typ_arg_aux * 'a l
 
 
 type 
-typquant = 
-   TypQ_aux of typquant_aux * l
+'a typquant = 
+   TypQ_aux of 'a typquant_aux * 'a l
 
 
 type 
-typschm_aux =  (* type scheme *)
-   TypSchm_ts of typquant * typ
+'a typschm_aux =  (* type scheme *)
+   TypSchm_ts of 'a typquant * 'a typ
 
 
 type 
@@ -198,131 +213,131 @@ lit =  (* Literal constant *)
 
 
 type 
-typschm = 
-   TypSchm_aux of typschm_aux * l
+'a typschm = 
+   TypSchm_aux of 'a typschm_aux * 'a l
 
 
 type 
-pat_aux =  (* Pattern *)
+'a pat_aux =  (* Pattern *)
    P_lit of lit (* literal constant pattern *)
  | P_wild of terminal (* wildcard *)
- | P_as of terminal * pat * terminal * id * terminal (* named pattern *)
- | P_typ of terminal * typ * pat * terminal (* typed pattern *)
- | P_id of id (* identifier *)
- | P_app of id * (pat) list (* union constructor pattern *)
- | P_record of terminal * (fpat * terminal) list * terminal * bool * terminal (* struct pattern *)
- | P_vector of terminal * (pat * terminal) list * terminal (* vector pattern *)
- | P_vector_indexed of terminal * ((terminal * int * terminal * pat) * terminal) list * terminal (* vector pattern (with explicit indices) *)
- | P_vector_concat of (pat * terminal) list (* concatenated vector pattern *)
- | P_tup of terminal * (pat * terminal) list * terminal (* tuple pattern *)
- | P_list of terminal * (pat * terminal) list * terminal (* list pattern *)
+ | P_as of terminal * 'a pat * terminal * 'a id * terminal (* named pattern *)
+ | P_typ of terminal * 'a typ * 'a pat * terminal (* typed pattern *)
+ | P_id of 'a id (* identifier *)
+ | P_app of 'a id * ('a pat) list (* union constructor pattern *)
+ | P_record of terminal * ('a fpat * terminal) list * terminal * bool * terminal (* struct pattern *)
+ | P_vector of terminal * ('a pat * terminal) list * terminal (* vector pattern *)
+ | P_vector_indexed of terminal * ((terminal * int * terminal * 'a pat) * terminal) list * terminal (* vector pattern (with explicit indices) *)
+ | P_vector_concat of ('a pat * terminal) list (* concatenated vector pattern *)
+ | P_tup of terminal * ('a pat * terminal) list * terminal (* tuple pattern *)
+ | P_list of terminal * ('a pat * terminal) list * terminal (* list pattern *)
 
-and pat = 
-   P_aux of pat_aux * l
+and 'a pat = 
+   P_aux of 'a pat_aux * 'a l
 
-and fpat_aux =  (* Field pattern *)
-   FP_Fpat of id * terminal * pat
+and 'a fpat_aux =  (* Field pattern *)
+   FP_Fpat of 'a id * terminal * 'a pat
 
-and fpat = 
-   FP_aux of fpat_aux * l
+and 'a fpat = 
+   FP_aux of 'a fpat_aux * 'a l
 
 
 type 
-exp_aux =  (* Expression *)
-   E_block of terminal * (exp * terminal) list * terminal (* block (parsing conflict with structs?) *)
- | E_id of id (* identifier *)
+'a exp_aux =  (* Expression *)
+   E_block of terminal * ('a exp * terminal) list * terminal (* block (parsing conflict with structs?) *)
+ | E_id of 'a id (* identifier *)
  | E_lit of lit (* literal constant *)
- | E_cast of terminal * typ * terminal * exp (* cast *)
- | E_app of exp * (exp) list (* function application *)
- | E_app_infix of exp * id * exp (* infix function application *)
- | E_tuple of terminal * (exp * terminal) list * terminal (* tuple *)
- | E_if of terminal * exp * terminal * exp * terminal * exp (* conditional *)
- | E_vector of terminal * (exp * terminal) list * terminal (* vector (indexed from 0) *)
- | E_vector_indexed of terminal * ((terminal * int * terminal * exp) * terminal) list * terminal (* vector (indexed consecutively) *)
- | E_vector_access of exp * terminal * exp * terminal (* vector access *)
- | E_vector_subrange of exp * terminal * exp * terminal * exp * terminal (* subvector extraction *)
- | E_vector_update of terminal * exp * terminal * exp * terminal * exp * terminal (* vector functional update *)
- | E_vector_update_subrange of terminal * exp * terminal * exp * terminal * exp * terminal * exp * terminal (* vector subrange update (with vector) *)
- | E_list of terminal * (exp * terminal) list * terminal (* list *)
- | E_cons of exp * terminal * exp (* cons *)
- | E_record of terminal * fexps * terminal (* struct *)
- | E_record_update of terminal * exp * terminal * fexps * terminal (* functional update of struct *)
- | E_field of exp * terminal * id (* field projection from struct *)
- | E_case of terminal * exp * terminal * ((terminal * pexp)) list * terminal (* pattern matching *)
- | E_let of letbind * terminal * exp (* let expression *)
- | E_assign of lexp * terminal * exp (* imperative assignment *)
-
-and exp = 
-   E_aux of exp_aux * l
+ | E_cast of terminal * 'a typ * terminal * 'a exp (* cast *)
+ | E_app of 'a exp * ('a exp) list (* function application *)
+ | E_app_infix of 'a exp * 'a id * 'a exp (* infix function application *)
+ | E_tuple of terminal * ('a exp * terminal) list * terminal (* tuple *)
+ | E_if of terminal * 'a exp * terminal * 'a exp * terminal * 'a exp (* conditional *)
+ | E_vector of terminal * ('a exp * terminal) list * terminal (* vector (indexed from 0) *)
+ | E_vector_indexed of terminal * ((terminal * int * terminal * 'a exp) * terminal) list * terminal (* vector (indexed consecutively) *)
+ | E_vector_access of 'a exp * terminal * 'a exp * terminal (* vector access *)
+ | E_vector_subrange of 'a exp * terminal * 'a exp * terminal * 'a exp * terminal (* subvector extraction *)
+ | E_vector_update of terminal * 'a exp * terminal * 'a exp * terminal * 'a exp * terminal (* vector functional update *)
+ | E_vector_update_subrange of terminal * 'a exp * terminal * 'a exp * terminal * 'a exp * terminal * 'a exp * terminal (* vector subrange update (with vector) *)
+ | E_list of terminal * ('a exp * terminal) list * terminal (* list *)
+ | E_cons of 'a exp * terminal * 'a exp (* cons *)
+ | E_record of terminal * 'a fexps * terminal (* struct *)
+ | E_record_update of terminal * 'a exp * terminal * 'a fexps * terminal (* functional update of struct *)
+ | E_field of 'a exp * terminal * 'a id (* field projection from struct *)
+ | E_case of terminal * 'a exp * terminal * ((terminal * 'a pexp)) list * terminal (* pattern matching *)
+ | E_let of 'a letbind * terminal * 'a exp (* let expression *)
+ | E_assign of lexp * terminal * 'a exp (* imperative assignment *)
+
+and 'a exp = 
+   E_aux of 'a exp_aux * 'a l
 
 and lexp =  (* lvalue expression *)
-   LEXP_id of id (* identifier *)
- | LEXP_vector of lexp * terminal * exp * terminal (* vector element *)
- | LEXP_vector_range of lexp * terminal * exp * terminal * exp * terminal (* subvector *)
- | LEXP_field of lexp * terminal * id (* struct field *)
+   LEXP_id of 'a id (* identifier *)
+ | LEXP_vector of lexp * terminal * 'a exp * terminal (* vector element *)
+ | LEXP_vector_range of lexp * terminal * 'a exp * terminal * 'a exp * terminal (* subvector *)
+ | LEXP_field of lexp * terminal * 'a id (* struct field *)
 
-and fexp_aux =  (* Field-expression *)
-   FE_Fexp of id * terminal * exp
+and 'a fexp_aux =  (* Field-expression *)
+   FE_Fexp of 'a id * terminal * 'a exp
 
-and fexp = 
-   FE_aux of fexp_aux * l
+and 'a fexp = 
+   FE_aux of 'a fexp_aux * 'a l
 
-and fexps_aux =  (* Field-expression list *)
-   FES_Fexps of (fexp * terminal) list * terminal * bool
+and 'a fexps_aux =  (* Field-expression list *)
+   FES_Fexps of ('a fexp * terminal) list * terminal * bool
 
-and fexps = 
-   FES_aux of fexps_aux * l
+and 'a fexps = 
+   FES_aux of 'a fexps_aux * 'a l
 
-and pexp_aux =  (* Pattern match *)
-   Pat_exp of pat * terminal * exp
+and 'a pexp_aux =  (* Pattern match *)
+   Pat_exp of 'a pat * terminal * 'a exp
 
-and pexp = 
-   Pat_aux of pexp_aux * l
+and 'a pexp = 
+   Pat_aux of 'a pexp_aux * 'a l
 
-and letbind_aux =  (* Let binding *)
-   LB_val_explicit of typschm * pat * terminal * exp (* value binding, explicit type (pat must be total) *)
- | LB_val_implicit of terminal * pat * terminal * exp (* value binding, implicit type (pat must be total) *)
+and 'a letbind_aux =  (* Let binding *)
+   LB_val_explicit of 'a typschm * 'a pat * terminal * 'a exp (* value binding, explicit type ('a pat must be total) *)
+ | LB_val_implicit of terminal * 'a pat * terminal * 'a exp (* value binding, implicit type ('a pat must be total) *)
 
-and letbind = 
-   LB_aux of letbind_aux * l
+and 'a letbind = 
+   LB_aux of 'a letbind_aux * 'a l
 
 
 type 
-rec_opt_aux =  (* Optional recursive annotation for functions *)
+'a rec_opt_aux =  (* Optional recursive annotation for functions *)
    Rec_nonrec (* non-recursive *)
  | Rec_rec of terminal (* recursive *)
 
 
 type 
-effects_opt_aux =  (* Optional effect annotation for functions *)
+'a effects_opt_aux =  (* Optional effect annotation for functions *)
    Effects_opt_pure (* sugar for empty effect set *)
- | Effects_opt_effects of effects
+ | Effects_opt_effects of 'a effects
 
 
 type 
-funcl_aux =  (* Function clause *)
-   FCL_Funcl of id * pat * terminal * exp
+'a funcl_aux =  (* Function clause *)
+   FCL_Funcl of 'a id * 'a pat * terminal * 'a exp
 
 
 type 
 tannot_opt =  (* Optional type annotation for functions *)
    Typ_annot_opt_none
- | Typ_annot_opt_some of terminal * typ
+ | Typ_annot_opt_some of terminal * 'a typ
 
 
 type 
-rec_opt = 
-   Rec_aux of rec_opt_aux * l
+'a rec_opt = 
+   Rec_aux of 'a rec_opt_aux * 'a l
 
 
 type 
-effects_opt = 
-   Effects_opt_aux of effects_opt_aux * l
+'a effects_opt = 
+   Effects_opt_aux of 'a effects_opt_aux * 'a l
 
 
 type 
-funcl = 
-   FCL_aux of funcl_aux * l
+'a funcl = 
+   FCL_aux of 'a funcl_aux * 'a l
 
 
 type 
@@ -339,96 +354,96 @@ index_range =  (* index specification, for bitfields in register types *)
 
 
 type 
-fundef_aux =  (* Function definition *)
-   FD_function of terminal * rec_opt * tannot_opt * effects_opt * (funcl * terminal) list
+'a fundef_aux =  (* Function definition *)
+   FD_function of terminal * 'a rec_opt * tannot_opt * 'a effects_opt * ('a funcl * terminal) list
 
 
 type 
-val_spec_aux =  (* Value type specification *)
-   VS_val_spec of terminal * typschm * id
+'a val_spec_aux =  (* Value type specification *)
+   VS_val_spec of terminal * 'a typschm * 'a id
 
 
 type 
-default_typing_spec_aux =  (* Default kinding or typing assumption *)
-   DT_kind of terminal * base_kind * id
- | DT_typ of terminal * typschm * id
+'a default_typing_spec_aux =  (* Default kinding or typing assumption *)
+   DT_kind of terminal * 'a base_kind * 'a id
+ | DT_typ of terminal * 'a typschm * 'a id
 
 
 type 
 type_def =  (* Type definition body *)
-   TD_abbrev of terminal * id * naming_scheme_opt * terminal * typschm (* type abbreviation *)
- | TD_record of terminal * id * naming_scheme_opt * terminal * terminal * terminal * typquant * terminal * ((typ * id) * terminal) list * terminal * bool * terminal (* struct type definition *)
- | TD_variant of terminal * id * naming_scheme_opt * terminal * terminal * terminal * typquant * terminal * ((typ * id) * terminal) list * terminal * bool * terminal (* union type definition *)
- | TD_enum of terminal * id * naming_scheme_opt * terminal * terminal * terminal * (id * terminal) list * terminal * bool * terminal (* enumeration type definition *)
- | TD_register of terminal * id * terminal * terminal * terminal * terminal * nexp * terminal * nexp * terminal * terminal * ((index_range * terminal * id) * terminal) list * terminal (* register mutable bitfield type definition *)
+   TD_abbrev of terminal * 'a id * naming_scheme_opt * terminal * 'a typschm (* type abbreviation *)
+ | TD_record of terminal * 'a id * naming_scheme_opt * terminal * terminal * terminal * 'a typquant * terminal * (('a typ * 'a id) * terminal) list * terminal * bool * terminal (* struct type definition *)
+ | TD_variant of terminal * 'a id * naming_scheme_opt * terminal * terminal * terminal * 'a typquant * terminal * (('a typ * 'a id) * terminal) list * terminal * bool * terminal (* union type definition *)
+ | TD_enum of terminal * 'a id * naming_scheme_opt * terminal * terminal * terminal * ('a id * terminal) list * terminal * bool * terminal (* enumeration type definition *)
+ | TD_register of terminal * 'a id * terminal * terminal * terminal * terminal * 'a nexp * terminal * 'a nexp * terminal * terminal * ((index_range * terminal * 'a id) * terminal) list * terminal (* register mutable bitfield type definition *)
 
 
 type 
-fundef = 
-   FD_aux of fundef_aux * l
+'a fundef = 
+   FD_aux of 'a fundef_aux * 'a l
 
 
 type 
-val_spec = 
-   VS_aux of val_spec_aux * l
+'a val_spec = 
+   VS_aux of 'a val_spec_aux * 'a l
 
 
 type 
-default_typing_spec = 
-   DT_aux of default_typing_spec_aux * l
+'a default_typing_spec = 
+   DT_aux of 'a default_typing_spec_aux * 'a l
 
 
 type 
-def_aux =  (* Top-level definition *)
+'a def_aux =  (* Top-level definition *)
    DEF_type of type_def (* type definition *)
- | DEF_fundef of fundef (* function definition *)
- | DEF_val of letbind (* value definition *)
- | DEF_spec of val_spec (* top-level type constraint *)
- | DEF_default of default_typing_spec (* default kind and type assumptions *)
- | DEF_reg_dec of terminal * typ * id (* register declaration *)
- | DEF_scattered_function of terminal * terminal * rec_opt * tannot_opt * effects_opt * id (* scattered function definition header *)
- | DEF_scattered_funcl of terminal * terminal * funcl (* scattered function definition clause *)
- | DEF_scattered_variant of terminal * terminal * id * naming_scheme_opt * terminal * terminal * terminal * typquant (* scattered union definition header *)
- | DEF_scattered_unioncl of terminal * id * terminal * typ * id (* scattered union definition member *)
- | DEF_scattered_end of terminal * id (* scattered definition end *)
+ | DEF_fundef of 'a fundef (* function definition *)
+ | DEF_val of 'a letbind (* value definition *)
+ | DEF_spec of 'a val_spec (* top-level type constraint *)
+ | DEF_default of 'a default_typing_spec (* default kind and type assumptions *)
+ | DEF_reg_dec of terminal * 'a typ * 'a id (* register declaration *)
+ | DEF_scattered_function of terminal * terminal * 'a rec_opt * tannot_opt * 'a effects_opt * 'a id (* scattered function definition header *)
+ | DEF_scattered_funcl of terminal * terminal * 'a funcl (* scattered function definition clause *)
+ | DEF_scattered_variant of terminal * terminal * 'a id * naming_scheme_opt * terminal * terminal * terminal * 'a typquant (* scattered union definition header *)
+ | DEF_scattered_unioncl of terminal * 'a id * terminal * 'a typ * 'a id (* scattered union definition member *)
+ | DEF_scattered_end of terminal * 'a id (* scattered definition end *)
 
 
 type 
-typ_lib_aux =  (* library types and syntactic sugar for them *)
+'a typ_lib_aux =  (* library types and syntactic sugar for them *)
    Typ_lib_unit of terminal (* unit type with value $()$ *)
  | Typ_lib_bool of terminal (* booleans $_$ and $_$ *)
  | Typ_lib_bit of terminal (* pure bit values (not mutable bits) *)
  | Typ_lib_nat of terminal (* natural numbers 0,1,2,... *)
  | Typ_lib_string of terminal * Ulib.UTF8.t (* UTF8 strings *)
- | Typ_lib_enum of terminal * nexp * nexp * order (* natural numbers nexp .. nexp+nexp-1, ordered by order *)
- | Typ_lib_enum1 of terminal * nexp * terminal (* sugar for \texttt{enum nexp 0 inc} *)
- | Typ_lib_enum2 of terminal * nexp * terminal * nexp * terminal (* sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} *)
- | Typ_lib_vector of terminal * nexp * nexp * order * typ (* vector of typ, indexed by natural range *)
- | Typ_lib_vector2 of typ * terminal * nexp * terminal (* sugar for vector indexed by [ nexp ] *)
- | Typ_lib_vector3 of typ * terminal * nexp * terminal * nexp * terminal (* sugar for vector indexed by [ nexp..nexp ] *)
- | Typ_lib_list of terminal * typ (* list of typ *)
- | Typ_lib_set of terminal * typ (* finite set of typ *)
- | Typ_lib_reg of terminal * typ (* mutable register components holding typ *)
+ | Typ_lib_enum of terminal * 'a nexp * 'a nexp * 'a order (* natural numbers 'a nexp .. 'a nexp+'a nexp-1, ordered by 'a order *)
+ | Typ_lib_enum1 of terminal * 'a nexp * terminal (* sugar for \texttt{enum nexp 0 inc} *)
+ | Typ_lib_enum2 of terminal * 'a nexp * terminal * 'a nexp * terminal (* sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} *)
+ | Typ_lib_vector of terminal * 'a nexp * 'a nexp * 'a order * 'a typ (* vector of 'a typ, indexed by natural range *)
+ | Typ_lib_vector2 of 'a typ * terminal * 'a nexp * terminal (* sugar for vector indexed by [ 'a nexp ] *)
+ | Typ_lib_vector3 of 'a typ * terminal * 'a nexp * terminal * 'a nexp * terminal (* sugar for vector indexed by [ 'a nexp..'a nexp ] *)
+ | Typ_lib_list of terminal * 'a typ (* list of 'a typ *)
+ | Typ_lib_set of terminal * 'a typ (* finite set of 'a typ *)
+ | Typ_lib_reg of terminal * 'a typ (* mutable register components holding 'a typ *)
 
 
 type 
-def = 
-   DEF_aux of def_aux * l
+'a def = 
+   DEF_aux of 'a def_aux * 'a l
 
 
 type 
-typ_lib = 
-   Typ_lib_aux of typ_lib_aux * l
+'a typ_lib = 
+   Typ_lib_aux of 'a typ_lib_aux * 'a l
 
 
 type 
 ctor_def =  (* Datatype constructor definition clause *)
-   CT_ct of id * terminal * typschm
+   CT_ct of 'a id * terminal * 'a typschm
 
 
 type 
 defs =  (* Definition sequence *)
-   Defs of (def) list
+   Defs of ('a def) list