First addition of lexer and parser for L2, based on Lem parser and lexer.

Not complete, does not compile

2 files changed, 1173 insertions, 0 deletions

diff --git a/src/lexer.mll b/src/lexer.mll
new file mode 100644
index 00000000..551544c7
--- /dev/null
+++ b/src/lexer.mll
@@ -0,0 +1,210 @@
+(**************************************************************************)
+(*                        Lem                                             *)
+(*                                                                        *)
+(*          Dominic Mulligan, University of Cambridge                     *)
+(*          Francesco Zappa Nardelli, INRIA Paris-Rocquencourt            *)
+(*          Gabriel Kerneis, University of Cambridge                      *)
+(*          Kathy Gray, University of Cambridge                           *)
+(*          Peter Boehm, University of Cambridge (while working on Lem)   *)
+(*          Peter Sewell, University of Cambridge                         *)
+(*          Scott Owens, University of Kent                               *)
+(*          Thomas Tuerk, University of Cambridge                         *)
+(*                                                                        *)
+(*  The Lem sources are copyright 2010-2013                               *)
+(*  by the UK authors above and Institut National de Recherche en         *)
+(*  Informatique et en Automatique (INRIA).                               *)
+(*                                                                        *)
+(*  All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli}   *)
+(*  are distributed under the license below.  The former are distributed  *)
+(*  under the LGPLv2, as in the LICENSE file.                             *)
+(*                                                                        *)
+(*                                                                        *)
+(*  Redistribution and use in source and binary forms, with or without    *)
+(*  modification, are permitted provided that the following conditions    *)
+(*  are met:                                                              *)
+(*  1. Redistributions of source code must retain the above copyright     *)
+(*  notice, this list of conditions and the following disclaimer.         *)
+(*  2. Redistributions in binary form must reproduce the above copyright  *)
+(*  notice, this list of conditions and the following disclaimer in the   *)
+(*  documentation and/or other materials provided with the distribution.  *)
+(*  3. The names of the authors may not be used to endorse or promote     *)
+(*  products derived from this software without specific prior written    *)
+(*  permission.                                                           *)
+(*                                                                        *)
+(*  THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS    *)
+(*  OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED     *)
+(*  WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE    *)
+(*  ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY       *)
+(*  DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL    *)
+(*  DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE     *)
+(*  GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS         *)
+(*  INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER  *)
+(*  IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR       *)
+(*  OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN   *)
+(*  IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.                         *)
+(**************************************************************************)
+
+{
+open Parser
+module M = Map.Make(String)
+exception LexError of char * Lexing.position
+
+let (^^^) = Ulib.Text.(^^^)
+let r = Ulib.Text.of_latin1
+(* Available as Scanf.unescaped since OCaml 4.0 but 3.12 is still common *)
+let unescaped s = Scanf.sscanf ("\"" ^ s ^ "\"") "%S%!" (fun x -> x)
+
+let kw_table = 
+  List.fold_left
+    (fun r (x,y) -> M.add x y r)
+    M.empty
+    [
+     ("and",                     (fun x -> And(x)));
+     ("as",                      (fun x -> As(x)));
+     ("case",			 (fun x -> Case(x)));
+     ("const",			 (fun x -> Const(x)));
+     ("default",		 (fun x -> Default(x)));
+     ("enum",			 (fun x -> Enum(x)));
+     ("else",                    (fun x -> Else(x)));
+     ("false",                   (fun x -> False(x)));
+     ("forall",                  (fun x -> Forall(x)));
+     ("function",                (fun x -> Function_(x)));
+     ("if",                      (fun x -> If_(x)));
+     ("in",			 (fun x -> In(x)));
+     ("IN",                      (fun x -> IN(x,r"IN")));     
+     ("let",                     (fun x -> Let_(x)));
+     ("rec",			 (fun x -> Rec(x)));
+     ("register",		 (fun x -> Register(x)));
+     ("struct",                  (fun x -> Struct(x)));
+     ("switch",			 (fun x -> Switch(x)));
+     ("then",                    (fun x -> Then(x)));
+     ("true",                    (fun x -> True(x)));
+     ("type",                    (fun x -> Type(x)));
+     ("typedef",		 (fun x -> Typedef(x)));
+     ("union",			 (fun x -> Union(x)))
+     ("with",                    (fun x -> With(x)));
+     ("val",                     (fun x -> Val(x)));
+]
+
+}
+
+let ws = [' ''\t']+
+let letter = ['a'-'z''A'-'Z']
+let digit = ['0'-'9']
+let binarydigit = ['0'-'1']
+let hexdigit = ['0'-'9''A'-'F''a'-'f']
+let alphanum = letter|digit
+let startident = letter|'_'
+let ident = alphanum|['_''\'']
+let oper_char = ['!''$''%''&''*''+''-''.''/'':''<''=''>''?''@''^''|''~']
+let safe_com1 = [^'*''('')''\n']
+let safe_com2 = [^'*''(''\n']
+let com_help = "("*safe_com2 | "*"*"("+safe_com2 | "*"*safe_com1
+let com_body = com_help*"*"*
+let escape_sequence = ('\\' ['\\''\"''\'''n''t''b''r']) | ('\\' digit digit digit) | ('\\' 'x' hexdigit hexdigit)
+
+rule token skips = parse
+  | ws as i
+    { token (Ast.Ws(Ulib.Text.of_latin1 i)::skips) lexbuf }
+  | "\n"
+    { Lexing.new_line lexbuf;
+      token (Ast.Nl::skips) lexbuf } 
+  
+  | "&"					{ (Amp(Some(skips),r"&")) }
+  | "@"					{ (At(Some(skips),r"@")) }
+  | "|"                                 { (Bar(Some(skips))) }
+  | "^"					{ (Carrot(Some(skips),r"^")) }
+  | ":"                                 { (Colon(Some(skips))) }
+  | ","                                 { (Comma(Some(skips))) }
+  | "."                                 { (Dot(Some(skips))) }
+  | "\"					{ (Div(Some(skips),r"\")) }
+  | "="                                 { (Eq(Some(skips),r"=")) }
+  | "!"					{ (Excl(Some(skips),r"!")) }
+  | ">"					{ (Gt(Some(skips),r">")) }
+  | "<"					{ (Lt(Some(skips),r"<")) }
+  | "+"					{ (Plus(Some(skips),r"+")) }
+  | ";"                                 { (Semi(Some(skips))) }
+  | "*"                                 { (Star(Some(skips),r"*")) }
+  | "~"					{ (Tilde(Some(skips),r"~")) }
+  | "_"                                 { (Under(Some(skips))) }
+  | "{"                                 { (Lcurly(Some(skips))) }
+  | "}"                                 { (Rcurly(Some(skips))) }
+  | "("                                 { (Lparen(Some(skips))) }
+  | ")"                                 { (Rparen(Some(skips))) }
+  | "["                                 { (Lsquare(Some(skips))) }
+  | "]"                                 { (Rsquare(Some(skips))) }
+  | "&&" as i                           { (AmpAmp(Some(skips),Ulib.Text.of_latin1 i)) }
+  | "->"                                { (Arrow(Some(skips))) }
+  | "||"                                { (BarBar(Some(skips))) }
+  | "|>"                                { (BarGt(Some(skips))) }
+  | "|]"				{ (BarSquare(Some(skips))) }
+  | "::" as i                           { (ColonColon(Some(skips),Ulib.Text.of_latin1 i)) }
+  | ".."				{ (DotDot(Some(skips)) }  
+  | "=="				{ (EqEq(Some(skips),r"==")) }
+  | "!="				{ (ExclEq(Some(skips),r"!=")) }
+  | ">="				{ (GtEq(Some(skips),r">=")) }
+  | ">=+"				{ (GtEqPlus(Some(skips),r">=+")) }
+  | ">>"				{ (GtGt(Some(skips),r">>")) }
+  | ">>>"				{ (GtGtGt(Some(skips),r">>")) }
+  | ">+"				{ (GtPlus(Some(skips),r">+")) }
+  | "<="				{ (LtEq(Some(skips),r"<=")) }
+  | "<=+"				{ (LtEqPlus(Some(skips),r"<=+")) }
+  | "<<"				{ (LtLt(Some(skips),r"<<")) }
+  | "<<<"				{ (LtLtLt(Some(skips),r"<<<")) }
+  | "<+"				{ (LtPlus(Some(skips),r"<+")) }
+  | "**"				{ (StarStar(Some(skips),r"**")) }
+
+  | "(*"                           
+    { token (Ast.Com(Ast.Comment(comment lexbuf))::skips) lexbuf }
+
+  | startident ident* as i              { if M.mem i kw_table then
+                                            (M.find i kw_table) (Some(skips))
+                                          else
+                                            Id(Some(skips), Ulib.Text.of_latin1 i) }
+
+  | "\\\\" ([^' ' '\t' '\n']+ as i)     { (Id(Some(skips), Ulib.Text.of_latin1 i)) } 
+
+  | ['!''?''~'] oper_char* as i         { (Id(Some(skips), Ulib.Text.of_latin1 i)) }
+
+  | "**" oper_char* as i                { (StarStar(Some(skips), Ulib.Text.of_latin1 i)) }
+  | ['/''%'] oper_char* as i         { (Id(Some(skips), Ulib.Text.of_latin1 i)) }
+  | "*" oper_char+ as i         { (Id(Some(skips), Ulib.Text.of_latin1 i)) }
+  | ['+''-'] oper_char* as i            { (Id(Some(skips), Ulib.Text.of_latin1 i)) }
+  | ">=" oper_char+ as i   		{ (Id(Some(skips), Ulib.Text.of_latin1 i)) }
+  | ['@''^'] oper_char* as i            { (Id(Some(skips), Ulib.Text.of_latin1 i)) }
+  | ['=''<''>''|''&''$'] oper_char* as i { (Id(Some(skips), Ulib.Text.of_latin1 i)) }
+  | digit+ as i                         { (Num(Some(skips),int_of_string i)) }
+  | "0b" (binarydigit+ as i)		{ (Bin(Some(skips), i)) }
+  | "0x" (hexdigit+ as i) 		{ (Hex(Some(skips), i)) }
+  | '"'                                 { (String(Some(skips),
+                                           string (Lexing.lexeme_start_p lexbuf) (Buffer.create 10) lexbuf)) }
+  | eof                                 { (Eof(Some(skips))) }
+  | _  as c                             { raise (LexError(c, Lexing.lexeme_start_p lexbuf)) }
+
+
+and comment = parse
+  | (com_body "("* as i) "(*"           { let c1 = comment lexbuf in
+                                          let c2 = comment lexbuf in
+                                            Ast.Chars(Ulib.Text.of_latin1 i) :: Ast.Comment(c1) :: c2}
+  | (com_body as i) "*)"                { [Ast.Chars(Ulib.Text.of_latin1 i)] }
+  | com_body "("* "\n" as i             { Lexing.new_line lexbuf; 
+                                          (Ast.Chars(Ulib.Text.of_latin1 i) :: comment lexbuf) }
+  | _  as c                             { raise (LexError(c, Lexing.lexeme_start_p lexbuf)) }
+  | eof                                 { [] }
+
+and string pos b = parse
+  | ([^'"''\n''\\']*'\n' as i)          { Lexing.new_line lexbuf;
+                                          Buffer.add_string b i;
+                                          string pos b lexbuf }
+  | ([^'"''\n''\\']* as i)              { Buffer.add_string b i; string pos b lexbuf }
+  | escape_sequence as i                { Buffer.add_string b i; string pos b lexbuf }
+  | '\\' '\n' ws                        { Lexing.new_line lexbuf; string pos b lexbuf }
+  | '\\'                                { raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos,
+                                            "illegal backslash escape in string"))) }
+  | '"'                                 { let s = unescaped(Buffer.contents b) in
+                                          try Ulib.UTF8.validate s; s
+                                          with Ulib.UTF8.Malformed_code ->
+                                            raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos,
+                                              "String literal is not valid utf8"))) }
+  | eof                                 { raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos,
+                                            "String literal not terminated"))) }
diff --git a/src/parser.mly b/src/parser.mly
new file mode 100644
index 00000000..c352b830
--- /dev/null
+++ b/src/parser.mly
@@ -0,0 +1,963 @@
+/**************************************************************************/
+/*                        Lem                                             */
+/*                                                                        */
+/*          Dominic Mulligan, University of Cambridge                     */
+/*          Francesco Zappa Nardelli, INRIA Paris-Rocquencourt            */
+/*          Gabriel Kerneis, University of Cambridge                      */
+/*          Kathy Gray, University of Cambridge                           */
+/*          Peter Boehm, University of Cambridge (while working on Lem)   */
+/*          Peter Sewell, University of Cambridge                         */
+/*          Scott Owens, University of Kent                               */
+/*          Thomas Tuerk, University of Cambridge                         */
+/*                                                                        */
+/*  The Lem sources are copyright 2010-2013                               */
+/*  by the UK authors above and Institut National de Recherche en         */
+/*  Informatique et en Automatique (INRIA).                               */
+/*                                                                        */
+/*  All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli}   */
+/*  are distributed under the license below.  The former are distributed  */
+/*  under the LGPLv2, as in the LICENSE file.                             */
+/*                                                                        */
+/*                                                                        */
+/*  Redistribution and use in source and binary forms, with or without    */
+/*  modification, are permitted provided that the following conditions    */
+/*  are met:                                                              */
+/*  1. Redistributions of source code must retain the above copyright     */
+/*  notice, this list of conditions and the following disclaimer.         */
+/*  2. Redistributions in binary form must reproduce the above copyright  */
+/*  notice, this list of conditions and the following disclaimer in the   */
+/*  documentation and/or other materials provided with the distribution.  */
+/*  3. The names of the authors may not be used to endorse or promote     */
+/*  products derived from this software without specific prior written    */
+/*  permission.                                                           */
+/*                                                                        */
+/*  THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS    */
+/*  OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED     */
+/*  WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE    */
+/*  ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY       */
+/*  DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL    */
+/*  DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE     */
+/*  GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS         */
+/*  INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER  */
+/*  IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR       */
+/*  OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN   */
+/*  IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.                         */
+/**************************************************************************/
+
+%{
+(* 
+   *)
+let r = Ulib.Text.of_latin1
+
+open Ast
+
+let loc () = Range(Parsing.symbol_start_pos(),Parsing.symbol_end_pos())
+let locn m n = Range(Parsing.rhs_start_pos m,Parsing.rhs_end_pos n)
+
+(*let tloc t = Typ_l(t,loc ())
+let nloc n = Length_l(n,loc ())
+let lloc l = Lit_l(l,loc ())
+let ploc p = Pat_l(p,loc ())
+let eloc e = Expr_l(e,loc ())
+let lbloc lb = Letbind(lb,loc ())
+let dloc d = Def_l(d,loc ())
+let irloc ir = Rule_l(ir,loc())
+let reclloc fcl = Rec_l(fcl,loc())*)
+
+let pat_to_let p =
+  match p with
+    | Pat_l(P_app(Id([],v,_),(arg::args as a)),_) ->
+        Some((v,a))
+    | _ ->
+        None
+
+let pat_to_letfun p =
+  match p with
+    | Pat_l(P_app(Id([],v,_),(arg::args as a)),_) ->
+        (v,a)
+    | Pat_l(_,l) -> 
+        raise (Parse_error_locn(l,"Bad pattern for let binding of a function"))
+
+let get_target (s1,n) =
+  if Ulib.Text.compare n (r"hol") = 0 then
+    Target_hol(s1)
+  else if Ulib.Text.compare n (r"ocaml") = 0 then
+    Target_ocaml(s1)
+  else if Ulib.Text.compare n (r"coq") = 0 then
+    Target_coq(s1)
+  else if Ulib.Text.compare n (r"isabelle") = 0 then
+    Target_isa(s1)
+  else if Ulib.Text.compare n (r"tex") = 0 then
+    Target_tex(s1)
+  else
+    raise (Parse_error_locn(loc (),"Expected substitution target in {hol; isabelle; ocaml; coq; tex}, given " ^ Ulib.Text.to_string n))
+
+let build_fexp (Expr_l(e,_)) l =
+  match e with
+    | Infix(Expr_l(Ident(i), l'),SymX_l((stx,op),l''),e2) when Ulib.Text.compare op (r"=") = 0 ->
+        Fexp(i, stx, e2, l)
+    | _ ->
+        raise (Parse_error_locn(l,"Invalid record field assignment (should be id = exp)"))
+
+let mod_cap n =
+  if not (Name.starts_with_upper_letter (Name.strip_lskip (Name.from_x n))) then
+    raise (Parse_error_locn(Ast.xl_to_l n, "Module name must begin with an upper-case letter"))
+  else
+    ()
+
+let space = Ulib.Text.of_latin1 " "
+let star = Ulib.Text.of_latin1 "*"
+
+let mk_pre_x_l sk1 (sk2,id) sk3 l =
+  if (sk2 = None || sk2 = Some []) && (sk3 = None || sk3 = Some []) then
+    PreX_l(sk1,(None,id),None,l)
+  else if (sk2 = Some [Ws space] && 
+           sk3 = Some [Ws space] && 
+           (Ulib.Text.left id 1 = star ||
+            Ulib.Text.right id 1 = star)) then
+    PreX_l(sk1,(None,id),None,l)
+  else
+    raise (Parse_error_locn(l, "illegal whitespace in parenthesised infix name"))
+
+
+%}
+
+%{
+(*Terminals with no content*)
+}%
+
+%token <Ast.terminal> And As Case Const Default Enum Else False Forall Function_
+%token <Ast.terminal> If_ In IN Let_ Rec Register Struct Switch Then True 
+%token <Ast.terminal> Type Typedef Union With Val
+
+%token <Ast.terminal> Arrow Bar Colon Comma Dot Eof Semi Under
+%token <Ast.terminal> Lcurly Rcurly Lparen Rparen Lsquare Rsquare
+%token <Ast.terminal> BarBar BarGt BarSquare DotDot LtBar SquareBar 
+
+
+%{
+(*Terminals with content*)
+}%
+
+%token <Ast.terminal * Ulib.Text.t> Id
+%token <Ast.terminal * int> Num
+%token <Ast.terminal * string> String Bin Hex
+
+%token <Ast.terminal * Ulib.Text.t> Amp At Carrot  Div Eq Excl Gt Lt Plus Star Tilde
+%token <Ast.terminal * Ulib.Text.t> AmpAmp ColonColon EqEq ExclEq GtEq GtEqPlus GtGt 
+%token <Ast.terminal * Ulib.Text.t> GtGtGt GtPlus LtEq LtEqPlus LtLt LtLtLt LtPlus StarStar 
+%token <Ast.terminal * Ulib.Text.t> SquareBar BarSquare 
+
+%start file
+%type <Ast.defs> defs
+%type <Ast.typ> typ
+%type <Ast.pat> pat
+%type <Ast.exp> exp
+%type <Ast.defs * Ast.terminal> file
+
+
+%%
+
+x:
+  | X
+    { X_l($1, loc ()) }
+  | Lparen Eq Rparen
+    { mk_pre_x_l $1 $2 $3 (loc ()) }
+  | Lparen IN Rparen
+    { mk_pre_x_l $1 $2 $3 (loc ()) }
+  | Lparen MEM Rparen
+    { mk_pre_x_l $1 $2 $3 (loc ()) }
+  | Lparen MinusMinusGt Rparen
+    { mk_pre_x_l $1 $2 $3 (loc ()) }
+  | Lparen AmpAmp Rparen
+    { mk_pre_x_l $1 $2 $3 (loc ()) }
+  | Lparen BarBar Rparen
+    { mk_pre_x_l $1 $2 $3 (loc ()) }
+  | Lparen ColonColon Rparen
+    { mk_pre_x_l $1 $2 $3 (loc ()) }
+  | Lparen Star Rparen
+    { mk_pre_x_l $1 $2 $3 (loc ()) }
+  | Lparen Plus Rparen
+    { mk_pre_x_l $1 $2 $3 (loc ()) }
+  | Lparen GtEq Rparen
+    { mk_pre_x_l $1 $2 $3 (loc ()) }
+  | Lparen PlusX Rparen
+    { mk_pre_x_l $1 $2 $3 (loc ()) }
+  | Lparen StarX Rparen
+    { mk_pre_x_l $1 $2 $3 (loc ()) }
+  | Lparen GtEqX Rparen
+    { mk_pre_x_l $1 $2 $3 (loc ()) }
+  | Lparen EqualX Rparen
+    { mk_pre_x_l $1 $2 $3 (loc ()) }
+  | Lparen StarstarX Rparen
+    { mk_pre_x_l $1 $2 $3 (loc ()) }
+  | Lparen At Rparen
+    { mk_pre_x_l $1 $2 $3 (loc ()) }
+  | Lparen AtX Rparen
+    { mk_pre_x_l $1 $2 $3 (loc ()) }
+
+id:
+  | id_help
+    { Id(fst $1, snd $1, loc ()) }
+
+id_help:
+  | x
+    { ([],$1) }
+  | x Dot id_help
+    { let (l,last) = $3 in
+        (($1,$2)::l, last) }
+
+tnvar:
+  | Tyvar
+    { Avl(A_l((fst $1, snd $1), loc ())) }
+  | Nvar
+    { Nvl(N_l((fst $1, snd $1), loc ())) }
+
+atomic_typ:
+  | Under
+    { tloc (Typ_wild($1)) }
+  | Tyvar
+    { tloc (Typ_var(A_l((fst $1, snd $1), loc()))) }
+  | id
+    { tloc (Typ_app($1,[])) }
+  | Lparen typ Rparen
+    { tloc (Typ_paren($1,$2,$3)) }
+
+appt_typ :
+  | atomic_typ
+    { $1 }
+  | atomic_nexp
+    { tloc (Typ_Nexps($1)) }
+
+atomic_typs:
+  | appt_typ
+    { [$1] }
+  | appt_typ atomic_typs
+    { $1::$2 }
+
+app_typ:
+  | atomic_typ
+    { $1 }
+  | id atomic_typs
+    { tloc (Typ_app($1,$2)) }
+  
+star_typ_list:
+  | app_typ
+    { [($1,None)] }
+  | app_typ Star star_typ_list
+    { ($1,fst $2)::$3 }
+
+star_typ:
+  | star_typ_list
+    { match $1 with
+        | [] -> assert false
+        | [(t,None)] -> t
+        | [(t,Some _)] -> assert false
+        | ts -> tloc (Typ_tup(ts)) }
+
+typ:
+  | star_typ
+    { $1 }
+  | star_typ Arrow typ
+    { tloc (Typ_fn($1,$2,$3)) }
+
+atomic_nexp:
+   | Nvar
+     { nloc (Nexp_var (fst $1, snd $1)) }
+   | Num
+     { nloc (Nexp_constant(fst $1, snd $1)) }
+   | Lparen nexp Rparen
+     { nloc (Nexp_paren($1,$2,$3)) }
+
+star_nexp:
+   | atomic_nexp
+     { $1 }
+   | atomic_nexp Star star_nexp
+     { nloc (Nexp_times($1, fst $2, $3)) }
+
+nexp:
+   | star_nexp
+     { $1 }
+   | star_nexp Plus nexp
+     { nloc (Nexp_sum($1,fst $2,$3)) }
+
+lit:
+  | True
+    { lloc (L_true($1)) }
+  | False
+    { lloc (L_false($1)) }
+  | Num
+    { lloc (L_num(fst $1, snd $1)) }
+  | String
+    { lloc (L_string(fst $1, snd $1)) }
+  | Lparen Rparen
+    { lloc (L_unit($1,$2)) }
+  | HashZero
+    { lloc (L_zero($1)) }
+  | HashOne
+    { lloc (L_one($1)) }
+  | Bin
+    { lloc (L_bin(fst $1, snd $1)) }
+  | Hex
+    { lloc (L_hex(fst $1, snd $1)) }
+
+atomic_pat:
+  | Under
+    { ploc (P_wild($1)) }
+  | id
+    { ploc (P_app($1,[])) }
+  | Lparen pat Colon typ Rparen
+    { ploc (P_typ($1,$2,$3,$4,$5)) }
+  | LtBar fpats BarGt
+    { ploc (P_record($1,fst $2,fst (snd $2),snd (snd $2),$3)) }
+  | BraceBar semi_pats_atomic BarBrace
+    { ploc (P_vector($1,fst $2,fst (snd $2),snd (snd $2),$3)) }
+  | BraceBar atomic_pats_two BarBrace
+    { ploc (P_vectorC($1, $2, $3)) }
+  | Lparen comma_pats Rparen
+    { ploc (P_tup($1,$2,$3)) }
+  | Lparen pat Rparen
+    { ploc (P_paren($1,$2,$3)) }
+  | Lsquare semi_pats Rsquare
+    { ploc (P_list($1,fst $2,fst (snd $2),snd (snd $2),$3)) }
+  | lit
+    { ploc (P_lit($1)) }
+  | Lparen pat As x Rparen
+    { ploc (P_as($1,$2,$3,$4,$5)) }
+  | x Plus Num
+    { ploc (P_num_add($1,fst $2,fst $3, snd $3)) }
+
+atomic_pats:
+  | atomic_pat
+    { [$1] }
+  | atomic_pat atomic_pats
+    { $1::$2 }
+
+atomic_pats_two:
+  | atomic_pat atomic_pat
+    { [$1;$2] }
+  | atomic_pat atomic_pats_two
+    { $1::$2 }
+
+app_pat:
+  | atomic_pat
+    { $1 }
+  | id atomic_pats
+    { ploc (P_app($1,$2)) }
+
+pat:
+  | app_pat
+    { $1 }
+  | app_pat ColonColon pat
+    { ploc (P_cons($1,fst $2,$3)) } 
+
+semi_pats_atomic:
+  | atomic_pat
+    { ([($1,None)], (None,false))}
+  | atomic_pat Semi
+    { ([($1,None)], ($2,true)) }
+  | atomic_pat Semi semi_pats_atomic
+    { (($1,$2)::fst $3, snd $3) }    
+
+semi_pats_help:
+  | pat
+    { ([($1,None)], (None,false)) }
+  | pat Semi
+    { ([($1,None)], ($2,true)) }
+  | pat Semi semi_pats_help
+    { (($1,$2)::fst $3, snd $3) }
+
+semi_pats:
+  |
+    { ([], (None, false)) }
+  | semi_pats_help
+    { $1 }
+
+comma_pats:
+  | pat Comma pat
+    { [($1,$2);($3,None)] }
+  | pat Comma comma_pats
+    { ($1,$2)::$3 }
+
+fpat:
+  | id Eq pat
+    { Fpat($1,fst $2,$3,loc ()) }
+
+fpats:
+  | fpat
+    { ([($1,None)], (None,false)) }
+  | fpat Semi
+    { ([($1,None)], ($2,true)) }
+  | fpat Semi fpats
+    { (($1,$2)::fst $3, snd $3) }
+
+atomic_exp:
+  | LtBar fexps BarGt
+    { eloc (Record($1,$2,$3)) }
+  | LtBar at_exp With fexps BarGt
+    { eloc (Recup($1,$2,$3,$4,$5)) }
+  | Lparen exp Colon typ Rparen
+    { eloc (Typed($1,$2,$3,$4,$5)) }
+  | BraceBar semi_exps BarBrace
+    { eloc (Vector($1,fst $2, fst (snd $2), snd (snd $2), $3)) }
+  | Lsquare semi_exps Rsquare
+    { eloc (Elist($1,fst $2,fst (snd $2), snd (snd $2), $3)) }
+  | Lparen comma_exps Rparen
+    { eloc (Tup($1,$2,$3)) }
+  | Lparen exp Rparen
+    { eloc (Paren($1,$2,$3)) }
+  | Begin_ exp End
+    { eloc (Begin($1,$2,$3)) }
+  | lit
+    { eloc (Lit($1)) }
+  | Nvar
+    { eloc (Nvar($1)) }
+  | Lcurly exp Bar exp Rcurly
+    { eloc (Setcomp($1,$2,$3,$4,$5)) }
+  | Lcurly exp Bar Forall quant_bindings Bar exp Rcurly
+    { eloc (Setcomp_binding($1,$2,$3,$4,$5,$6,$7,$8)) }
+  | Lcurly semi_exps Rcurly
+    { eloc (Set($1,fst $2,fst (snd $2), snd (snd $2),$3)) }
+  | Lsquare exp Bar Forall quant_bindings Bar exp Rsquare
+    { eloc (Listcomp($1,$2,$3,$4,$5,$6,$7,$8)) }
+  | Function_ patexps End
+    { eloc (Function($1,None,false,$2,$3)) }
+  | Function_ Bar patexps End
+    { eloc (Function($1,$2,true,$3,$4)) }
+  | Match exp With patexps End
+    { eloc (Case($1,$2,$3,None,false,$4,locn 4 4,$5)) }
+  | Match exp With Bar patexps End
+    { eloc (Case($1,$2,$3,$4,true,$5,locn 5 5,$6)) }
+  | Do id do_exps In exp End
+    { eloc (Do($1,$2,$3,$4,$5,$6)) }
+
+field_exp:
+  | atomic_exp
+    { $1 }
+  | atomic_exp Dot id
+    { eloc (Field($1,$2,$3)) }
+  | atomic_exp DotBrace nexp Rsquare
+    { eloc (VAccess($1,$2,$3,$4)) }
+  | atomic_exp DotBrace nexp Dot Dot nexp Rsquare
+    { eloc (VAccessR($1,$2,$3,$4,$6,$7)) }
+  | id DotBrace nexp Rsquare
+    { eloc (VAccess((eloc (Ident ($1))),$2,$3,$4)) }
+  | id DotBrace nexp Dot Dot nexp Rsquare
+    { eloc (VAccessR((eloc (Ident ($1))),$2,$3,$4,$6,$7)) }
+  | id
+    { eloc (Ident($1)) }
+
+app_exp:
+  | field_exp
+    { $1 }
+  | app_exp field_exp
+    { eloc (App($1,$2)) }
+
+right_atomic_exp:
+  | Forall quant_bindings Dot exp
+    { eloc (Quant(Q_forall($1), $2,$3,$4)) }
+  | Exists quant_bindings Dot exp
+    { eloc (Quant(Q_exists($1), $2,$3,$4)) }
+  | If_ exp Then exp Else exp
+    { eloc (If($1,$2,$3,$4,$5,$6)) }
+  | Fun_ patsexp
+    { eloc (Fun($1,$2)) }
+  | Let_ letbind In exp
+    { eloc (Let($1,$2,$3,$4)) }
+
+starstar_exp:
+  | app_exp
+    { $1 }
+  | app_exp StarstarX starstar_exp
+    { eloc (Infix($1, SymX_l($2, locn 2 2), $3)) }
+
+starstar_right_atomic_exp:
+  | right_atomic_exp
+    { $1 }
+  | app_exp StarstarX starstar_right_atomic_exp
+    { eloc (Infix($1, SymX_l($2, locn 2 2), $3)) }
+
+star_exp:
+  | starstar_exp
+    { $1 }
+  | star_exp Star starstar_exp
+    { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) }
+  | star_exp StarX starstar_exp
+    { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) }
+
+star_right_atomic_exp:
+  | starstar_right_atomic_exp
+    { $1 }
+  | star_exp Star starstar_right_atomic_exp
+    { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) }
+  | star_exp StarX starstar_right_atomic_exp
+    { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) }
+
+plus_exp:
+  | star_exp
+    { $1 }
+  | plus_exp Plus star_exp
+    { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) }
+  | plus_exp PlusX star_exp
+    { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) }
+
+plus_right_atomic_exp:
+  | star_right_atomic_exp
+    { $1 }
+  | plus_exp Plus star_right_atomic_exp
+    { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) }
+  | plus_exp PlusX star_right_atomic_exp
+    { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) }
+
+cons_exp:
+  | plus_exp
+    { $1 }
+  | plus_exp ColonColon cons_exp
+    { eloc (Cons($1,fst $2,$3)) }
+
+cons_right_atomic_exp:
+  | plus_right_atomic_exp
+    { $1 }
+  | plus_exp ColonColon cons_right_atomic_exp
+    { eloc (Cons($1,fst $2,$3)) }
+
+at_exp:
+  | cons_exp
+    { $1 }
+  | cons_exp At at_exp
+    { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) }
+  | cons_exp AtX at_exp
+    { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) }
+
+at_right_atomic_exp:
+  | cons_right_atomic_exp
+    { $1 }
+  | cons_exp At at_right_atomic_exp
+    { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) }
+  | cons_exp AtX at_right_atomic_exp
+    { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) }
+
+eq_exp:
+  | at_exp
+    { $1 }
+  | eq_exp Eq at_exp
+    { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) }
+  | eq_exp EqualX at_exp
+    { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) }
+  | eq_exp GtEq at_exp
+    { eloc (Infix ($1,SymX_l($2, locn 2 2), $3)) }
+  | eq_exp GtEqX at_exp
+    { eloc (Infix ($1,SymX_l($2, locn 2 2), $3)) }
+  | eq_exp IN at_exp
+    { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) }
+  | eq_exp MEM at_exp
+    { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) }
+
+eq_right_atomic_exp:
+  | at_right_atomic_exp
+    { $1 }
+  | eq_exp Eq at_right_atomic_exp
+    { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) }
+  | eq_exp EqualX at_right_atomic_exp
+    { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) }
+  | eq_exp IN at_right_atomic_exp
+    { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) }
+  | eq_exp MEM at_right_atomic_exp
+    { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) }
+
+and_exp:
+  | eq_exp
+    { $1 }
+  | eq_exp AmpAmp and_exp
+    { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) }
+
+and_right_atomic_exp:
+  | eq_right_atomic_exp
+    { $1 }
+  | eq_exp AmpAmp and_right_atomic_exp
+    { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) }
+
+or_exp:
+  | and_exp
+    { $1 }
+  | and_exp BarBar or_exp
+    { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) }
+
+or_right_atomic_exp:
+  | and_right_atomic_exp
+    { $1 }
+  | and_exp BarBar or_right_atomic_exp
+    { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) }
+
+imp_exp:
+  | or_exp
+    { $1 }
+  | or_exp MinusMinusGt imp_exp
+    { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) }
+
+imp_right_atomic_exp:
+  | or_right_atomic_exp
+    { $1 }
+  | or_exp MinusMinusGt imp_right_atomic_exp
+    { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) }
+
+exp:
+  | imp_right_atomic_exp
+    { $1 }
+  | imp_exp
+    { $1 }
+
+comma_exps:
+  | exp Comma exp
+    { [($1,$2);($3,None)] }
+  | exp Comma comma_exps
+    { ($1,$2)::$3 }
+ 
+semi_exps_help:
+  | exp
+    { ([($1,None)], (None,false)) }
+  | exp Semi
+    { ([($1,None)], ($2,true)) }
+  | exp Semi semi_exps_help
+    { (($1,$2)::fst $3, snd $3) }
+
+semi_exps:
+  |
+    { ([], (None, false)) }
+  | semi_exps_help
+    { $1 }
+
+quant_bindings:
+  | x
+    { [Qb_var($1)] }
+  | Lparen pat IN exp Rparen
+    { [Qb_restr($1,$2,fst $3,$4,$5)] }
+  | Lparen pat MEM exp Rparen
+    { [Qb_list_restr($1,$2,fst $3,$4,$5)] }
+  | x quant_bindings
+    { Qb_var($1)::$2 }
+  | Lparen pat IN exp Rparen quant_bindings
+    { Qb_restr($1,$2,fst $3,$4,$5)::$6 }
+  | Lparen pat MEM exp Rparen quant_bindings
+    { Qb_list_restr($1,$2,fst $3,$4,$5)::$6 }
+
+patsexp:
+  | atomic_pats1 Arrow exp
+    { Patsexp($1,$2,$3,loc ()) }
+
+opt_typ_annot:
+  | 
+    { Typ_annot_none }
+  | Colon typ
+    { Typ_annot_some($1,$2) }
+
+atomic_pats1:
+  | atomic_pat
+    { [$1] }
+  | atomic_pat atomic_pats1
+    { $1::$2 }
+
+patexps:
+  | pat Arrow exp
+    { [(Patexp($1,$2,$3,loc ()),None)] }
+  | pat Arrow exp Bar patexps
+    { (Patexp($1,$2,$3,locn 1 3),$4)::$5 }
+
+fexp:
+  | id Eq exp
+    { Fexp($1,fst $2,$3,loc()) }
+
+fexps:
+  | fexps_help
+    { Fexps(fst $1, fst (snd $1), snd (snd $1), loc ()) }
+
+fexps_help:
+  | fexp
+    { ([($1,None)], (None,false)) }
+  | fexp Semi
+    { ([($1,None)], ($2,true)) }
+  | fexp Semi fexps_help
+    { (($1,$2)::fst $3, snd $3) }
+
+letbind:
+  | pat opt_typ_annot Eq exp
+    { match pat_to_let $1 with
+        | Some((v,pats)) ->
+            lbloc (Let_fun(Funcl(v,pats,$2,fst $3,$4)))
+        | None ->
+            lbloc (Let_val($1,$2,fst $3,$4)) }
+
+do_exps:
+  | 
+    { [] }
+  | pat LeftArrow exp Semi do_exps
+    { ($1,$2,$3,$4)::$5 }
+
+funcl: 
+  | x atomic_pats1 opt_typ_annot Eq exp
+    { reclloc (Funcl($1,$2,$3,fst $4,$5)) }
+
+funcls:
+  | x atomic_pats1 opt_typ_annot Eq exp
+    { [(reclloc (Funcl($1,$2,$3,fst $4,$5)),None)] }
+  | funcl And funcls
+    { ($1,$2)::$3 }
+
+xs:
+  |
+    { [] }
+  | x xs
+    { $1::$2 }
+
+exps:
+  |
+    { [] }
+  | field_exp exps
+    { $1::$2 }
+ 
+x_opt:
+  |
+      { X_l_none }
+  | x Colon
+      { X_l_some ($1, $2) }
+
+indreln_clause:
+  | x_opt Forall xs Dot exp EqEqGt x exps
+    { irloc (Rule($1,$2,$3,$4,$5,$6,$7,$8)) }
+
+
+and_indreln_clauses:
+  | indreln_clause
+    { [($1,None)] }
+  | indreln_clause And and_indreln_clauses
+    { ($1,$2)::$3 }
+
+tnvs:
+  |
+    { [] }
+  | tnvar tnvs
+    { $1::$2 }
+
+c:
+  | id tnvar
+    { C($1,$2) }
+
+cs:
+  | c
+    { [($1,None)] }
+  | c Comma cs
+    { ($1,$2)::$3 }
+
+c2:
+  | id typ
+    { 
+      match $2 with
+        | Typ_l(Typ_var(a_l),_) ->
+            C($1,Avl(a_l)) 
+        | _ -> 
+          raise (Parse_error_locn(loc (),"Invalid class constraint"))
+    }
+
+cs2:
+  | c2
+    { [($1, None)] }
+  | c2 Comma cs2
+    { ($1,$2)::$3 }
+
+range:
+  | nexp Eq nexp
+    { Range_l(Fixed($1,(fst $2),$3), loc () ) }
+  | nexp GtEq nexp
+    { Range_l(Bounded($1,(fst $2),$3), loc () ) }
+
+ranges:
+  | range
+    { [($1,None)] }
+  | range Comma ranges 
+    { ($1,$2)::$3 }
+
+typschm:
+  | typ
+    { Ts(C_pre_empty, $1) }
+  | Forall tnvs Dot typ
+    { Ts(C_pre_forall($1,$2,$3,Cs_empty),$4) }
+  | Forall tnvs Dot cs EqGt typ
+    { Ts(C_pre_forall($1,$2,$3,Cs_classes($4,$5)), $6) }
+  | Forall tnvs Dot ranges EqGt typ
+    { Ts(C_pre_forall($1,$2,$3,Cs_lengths($4,$5)), $6) }
+  | Forall tnvs Dot cs Semi ranges EqGt typ
+    { Ts(C_pre_forall($1,$2,$3,Cs_both($4,$5,$6,$7)),$8) }
+
+
+insttyp:
+  | typ
+    { $1 }
+  | nexp
+    { tloc (Typ_Nexps($1)) }
+
+instschm:
+  | Lparen id insttyp Rparen
+    { Is(C_pre_empty, $1,$2,$3,$4) }
+  | Forall tnvs Dot Lparen id insttyp Rparen
+    { Is(C_pre_forall($1,$2,$3,Cs_empty),$4,$5,$6,$7) }
+  | Forall tnvs Dot cs2 EqGt Lparen id insttyp Rparen
+    { Is(C_pre_forall($1,$2,$3,Cs_classes($4,$5)),$6,$7,$8,$9) }
+
+val_spec:
+  | Val x Colon typschm
+    { Val_spec($1,$2,$3,$4) }
+
+class_val_spec:
+  | Val x Colon typ
+    { ($1,$2,$3,$4) }
+
+class_val_specs:
+  | class_val_spec
+    { [(fun (a,b,c,d) -> (a,b,c,d,loc())) $1] }
+  | class_val_spec class_val_specs
+    { ((fun (a,b,c,d) -> (a,b,c,d,loc())) $1)::$2 }
+
+targets:
+  | X
+    { [(get_target $1,None)] }
+  | X Semi targets
+    { (get_target $1, $2)::$3 }
+
+targets_opt:
+  |
+    { None }
+  | Lcurly Rcurly
+    { Some(Targets_concrete($1,[],$2)) }
+  | Lcurly targets Rcurly
+    { Some(Targets_concrete($1,$2,$3)) }
+    
+lemma_typ:
+  | Lemma
+    { Lemma_lemma $1 }
+  | Theorem
+    { Lemma_theorem $1 }
+  | Assert
+    { Lemma_assert $1 }
+
+lemma: 
+  | lemma_typ targets_opt Lparen exp Rparen
+    { Lemma_unnamed ($1, $2, $3, $4, $5) }
+  | lemma_typ targets_opt x Colon Lparen exp Rparen
+    { Lemma_named ($1, $2, $3, $4, $5, $6, $7) }
+
+val_def:  
+  | Let_ targets_opt letbind
+    { Let_def($1,$2,$3) }
+  | Let_ Rec targets_opt funcls
+    { Let_rec($1,$2,$3,$4) }
+  | Let_ Inline targets_opt letbind
+    { Let_inline($1,$2,$3,$4) }
+
+val_defs:
+  | val_def
+    { [($1,loc())] }
+  | val_def val_defs
+    { ($1,loc ())::$2 }
+
+def:
+  | Type tds
+    { dloc (Type_def($1,$2)) }
+  | val_def
+    { dloc (Val_def($1)) }
+  | Rename targets_opt id Eq x
+    { dloc (Ident_rename($1,$2,$3,fst $4,$5)) }
+  | Module_ x Eq Struct defs End
+    { mod_cap $2; dloc (Module($1,$2,fst $3,$4,$5,$6)) }
+  | Module_ x Eq id
+    { mod_cap $2; dloc (Rename($1,$2,fst $3,$4)) }
+  | Open_ id
+    { dloc (Open($1,$2)) }
+  | Indreln targets_opt and_indreln_clauses
+    { dloc (Indreln($1,$2,$3)) }
+  | val_spec
+    { dloc (Spec_def($1)) }
+  | Class_ Lparen x tnvar Rparen class_val_specs End
+    { dloc (Class($1,$2,$3,$4,$5,$6,$7)) }
+  | Inst instschm val_defs End
+    { dloc (Instance($1,$2,$3,$4)) }
+  | lemma
+    { dloc (Lemma $1) }
+
+xtyp:
+  | x Colon typ
+    { ($1,$2,$3) }
+   
+xtyps:
+  | xtyp
+    { ([($1,None)], (None, false)) }
+  | xtyp Semi
+    { ([($1,None)], ($2, true)) }
+  | xtyp Semi xtyps
+    { (($1,$2)::fst $3, snd $3) }
+
+ctor_texp:
+  | x Of star_typ_list
+    { Cte($1,$2,$3) }
+  | x
+    { Cte($1,None,[]) }
+
+ctor_single_texp:
+  | x Of star_typ_list
+    { Cte($1,$2,$3) }
+    
+ctor_texps:
+  | ctor_texp
+    { [($1,None)] }
+  | ctor_texp Bar ctor_texps
+    { ($1,$2)::$3 }
+
+texp:
+  | typ
+    { Te_abbrev($1) }
+  | LtBar xtyps BarGt
+    { Te_record($1,fst $2, fst (snd $2), snd (snd $2), $3) }    
+  | Bar ctor_texps
+    { Te_variant($1,true,$2) }
+  | ctor_texp Bar ctor_texps
+    { Te_variant(None,false,($1,$2)::$3) }
+  | ctor_single_texp
+    { Te_variant(None,false,[($1,None)]) }
+
+name_sect:
+  | Lsquare x Eq String Rsquare
+    { Name_sect_name($1,$2,fst $3,(fst $4),(snd $4),$5) }
+ 
+td:
+  | x tnvs
+    { Td_opaque($1,$2,Name_sect_none) }
+  | x tnvs name_sect
+    { Td_opaque($1,$2,$3) }
+  | x tnvs Eq texp
+    { Td($1,$2,Name_sect_none,fst $3,$4) }
+  | x tnvs name_sect Eq texp
+    { Td($1,$2,$3,fst $4,$5) }
+
+tds:
+  | td
+    { [($1,None)] }
+  | td And tds
+    { ($1,$2)::$3 }
+
+defs_help:
+  | def
+    { [($1,None,false)] }
+  | def SemiSemi
+    { [($1,$2,true)] }
+  | def defs_help
+    { ($1,None,false)::$2 }
+  | def SemiSemi defs_help
+    { ($1,$2,true)::$3 }
+
+defs:
+  | defs_help
+    { Defs($1) }
+
+file:
+  | defs Eof
+    { ($1,$2) }
+