and matching .ott

2 files changed, 53 insertions, 49 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