Clean up build system

5 files changed, 3 insertions, 1475 deletions

diff --git a/src/_build/reporting_basic.ml b/src/_build/reporting_basic.ml
deleted file mode 100644
index b3880598..00000000
--- a/src/_build/reporting_basic.ml
+++ /dev/null
@@ -1,172 +0,0 @@
-(**************************************************************************)
-(*                        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 format_pos ff p = (
-  Format.fprintf ff "File \"%s\", line %d, character %d:\n"
-    p.Lexing.pos_fname p.Lexing.pos_lnum (p.Lexing.pos_cnum - p.Lexing.pos_bol);
-  Format.pp_print_flush ff ())
-
-
-let format_pos2 ff p1 p2 = (
-  Format.fprintf ff "File \"%s\", line %d, character %d to line %d, character %d"
-    p1.Lexing.pos_fname 
-    p1.Lexing.pos_lnum (p1.Lexing.pos_cnum - p1.Lexing.pos_bol + 1)
-    p2.Lexing.pos_lnum (p2.Lexing.pos_cnum - p2.Lexing.pos_bol);
-  Format.pp_print_flush ff ()
-)
-
-(* reads the part between p1 and p2 from the file *)
-
-let read_from_file_pos2 p1 p2 =
-  let (s, e, multi) = if p1.Lexing.pos_lnum = p2.Lexing.pos_lnum then
-                  (* everything in the same line, so really only read this small part*)
-                  (p1.Lexing.pos_cnum, p2.Lexing.pos_cnum, None) 
-               else (*multiline, so start reading at beginning of line *)
-                  (p1.Lexing.pos_bol, p2.Lexing.pos_cnum, Some (p1.Lexing.pos_cnum - p1.Lexing.pos_bol)) in
-
-  let ic = open_in p1.Lexing.pos_fname in
-  let _ = seek_in ic s in
-  let l = (e - s) in
-  let buf = String.create l in
-  let _ = input ic buf 0 l in
-  let _ = match multi with None -> () | Some sk -> String.fill buf 0 sk ' ' in
-  let _ = close_in ic in
-  (buf, not (multi = None))
-
-(* Destruct a location by splitting all the Trans strings except possibly the
-   last one into a string list and keeping only the last location *)
-let dest_loc (l : Parse_ast.l) : (Parse_ast.l * string list) = 
-  let rec aux acc l = match l with
-    | Parse_ast.Trans(s, Some l') -> aux (s::acc) l'
-    | _ -> (l, acc)
-  in
-  aux [] l
-
-let rec format_loc_aux ff l =
-  let (l_org, mod_s) = dest_loc l in
-  let _ = match l_org with
-    | Parse_ast.Unknown -> Format.fprintf ff "no location information available"
-    | Parse_ast.Range(p1,p2) -> format_pos2 ff p1 p2
-    | Parse_ast.Trans(s,_) -> Format.fprintf ff "code generated by: %s" s
-  in
-  ()
-
-let format_loc_source ff l = 
-  match dest_loc l with 
-  | (Parse_ast.Range (p1, p2), _) -> 
-    begin
-      let (s, multi_line) = read_from_file_pos2 p1 p2 in
-      if multi_line then 
-        Format.fprintf ff "  original input:\n%s\n" s
-      else
-        Format.fprintf ff "  original input: \"%s\"\n" s
-    end
-  | _ -> ()
-
-let format_loc ff l =
- (format_loc_aux ff l;
-  Format.pp_print_newline ff ();
-  Format.pp_print_flush ff ()
-);;
-
-let print_err_loc l = 
-   (format_loc Format.err_formatter l)
-
-let print_pos p = format_pos Format.std_formatter p
-let print_err_pos p = format_pos Format.err_formatter p
-
-let loc_to_string l =
-  let _ = Format.flush_str_formatter () in
-  let _ = format_loc_aux Format.str_formatter l in
-  let s = Format.flush_str_formatter () in
-  s
-
-type pos_or_loc = Loc of Parse_ast.l | Pos of Lexing.position
-
-let print_err_internal fatal verb_loc p_l m1 m2 =
-  let _ = (match p_l with Pos p -> print_err_pos p | Loc l -> print_err_loc l) in
-  let m12 = if String.length m2 = 0 then "" else ": " in
-  Format.eprintf "  %s%s%s\n" m1 m12 m2;
-  if verb_loc then (match p_l with Loc l -> format_loc_source Format.err_formatter l; Format.pp_print_newline Format.err_formatter (); | _ -> ());
-  Format.pp_print_flush Format.err_formatter ();
-  if fatal then (exit 1) else ()
-
-let print_err fatal verb_loc l m1 m2 =
-  print_err_internal fatal verb_loc (Loc l) m1 m2
-
-
-type error = 
-  | Err_general of Parse_ast.l * string
-  | Err_unreachable of Parse_ast.l * string
-  | Err_todo of Parse_ast.l * string
-  | Err_syntax of Lexing.position * string
-  | Err_syntax_locn of Parse_ast.l * string
-  | Err_lex of Lexing.position * string
-  | Err_type of Parse_ast.l * string
-
-let dest_err = function
-  | Err_general (l, m) -> ("Error", false, Loc l, m)
-  | Err_unreachable (l, m) -> ("Internal error: Unreachable code", false, Loc l, m)
-  | Err_todo (l, m) -> ("Todo" ^ m, false, Loc l, "")
-  | Err_syntax (p, m) -> ("Syntax error", false, Pos p, m)
-  | Err_syntax_locn (l, m) -> ("Syntax error", false, Loc l, m)
-  | Err_lex (p, s) -> ("Lexical error", false, Pos p, s)
-  | Err_type (l, m) -> ("Type error", false, Loc l, m)
-
-exception Fatal_error of error
-
-(* Abbreviations for the very common cases *)
-let err_todo l m = Fatal_error (Err_todo (l, m))
-let err_unreachable l m = Fatal_error (Err_unreachable (l, m))
-let err_general l m = Fatal_error (Err_general (l, m))
-let err_typ l m = Fatal_error (Err_type (l,m))
-
-let report_error e = 
-  let (m1, verb_pos, pos_l, m2) = dest_err e in
-  (print_err_internal verb_pos false pos_l m1 m2; exit 1)
-
-
-
diff --git a/src/_build/reporting_basic.mli b/src/_build/reporting_basic.mli
deleted file mode 100644
index 462d2394..00000000
--- a/src/_build/reporting_basic.mli
+++ /dev/null
@@ -1,106 +0,0 @@
-(**************************************************************************)
-(*                        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.                         *)
-(**************************************************************************)
-
-(** Basic error reporting
-
-  [Reporting_basic] contains functions to report errors and warnings. 
-  It contains functions to print locations ([Parse_ast.l] and [Ast.l]) and lexing positions.
-
-  The main functionality is reporting errors. This is done by raising a
-  [Fatal_error] exception. This is caught internally and reported via [report_error]. 
-  There are several predefined types of errors which all cause different error
-  messages. If none of these fit, [Err_general] can be used.       
-
-*)
-
-(** {2 Auxiliary Functions } *)
-
-val loc_to_string : Parse_ast.l -> string
-
-(** [print_err fatal print_loc_source l head mes] prints an error / warning message to
-    std-err. It starts with printing location information stored in [l]
-    It then prints "head: mes". If [fatal] is set, the program exists with error-code 1 afterwards.
-*)
-val print_err : bool -> bool -> Parse_ast.l -> string -> string -> unit
-
-(** {2 Errors } *)
-
-(** Errors stop execution and print a message; they typically have a location and message.
-*)
-type error = 
-  (** General errors, used for multi purpose. If you are unsure, use this one. *)
-  | Err_general of Parse_ast.l * string
-
-  (** Unreachable errors should never be thrown. It means that some
-      code was excuted that the programmer thought of as unreachable *)
-  | Err_unreachable of Parse_ast.l * string
-
-  (** [Err_todo] indicates that some feature is unimplemented; it should be built using [err_todo]. *)
-  | Err_todo of Parse_ast.l * string
-
-  | Err_syntax of Lexing.position * string
-  | Err_syntax_locn of Parse_ast.l * string
-  | Err_lex of Lexing.position * string
-  | Err_type of Parse_ast.l * string
-  
-exception Fatal_error of error
-
-(** [err_todo l m] is an abreviatiation for [Fatal_error (Err_todo (l, m))] *)
-val err_todo : Parse_ast.l -> string -> exn
-
-(** [err_general l m] is an abreviatiation for [Fatal_error (Err_general (b, l, m))] *)
-val err_general : Parse_ast.l -> string -> exn
-
-(** [err_unreachable l m] is an abreviatiation for [Fatal_error (Err_unreachable (b, l, m))] *)
-val err_unreachable : Parse_ast.l -> string -> exn
-
-(** [err_typ l m] is an abreviatiation for [Fatal_error (Err_type (l, m))] *)
-val err_typ : Parse_ast.l -> string -> exn
-
-(** Report error should only be used by main to print the error in the end. Everywhere else,
-    raising a [Fatal_error] exception is recommended. *)
-val report_error : error -> 'a
-
diff --git a/src/ast.ml b/src/ast.ml
index bf5ecf31..8bf3b60c 100644..120000
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -1,471 +1 @@
-(* generated by Ott 0.22 from: l2.ott *)
-
-
-type text = string
-
-type l = Parse_ast.l
-
-type 'a annot = l * 'a
-
-
-type x = text (* identifier *)
-type ix = text (* infix identifier *)
-
-type 
-base_kind_aux =  (* base kind *)
-   BK_type (* kind of types *)
- | BK_nat (* kind of natural number size expressions *)
- | BK_order (* kind of vector order specifications *)
- | BK_effects (* kind of effect sets *)
-
-
-type 
-id_aux =  (* Identifier *)
-   Id of x
- | DeIid of x (* remove infix status *)
-
-
-type 
-base_kind = 
-   BK_aux of base_kind_aux * l
-
-
-type 
-id = 
-   Id_aux of id_aux * l
-
-
-type 
-kind_aux =  (* kinds *)
-   K_kind of (base_kind) list
-
-
-type 
-nexp_aux =  (* expression of kind $_$, for vector sizes and origins *)
-   Nexp_id of id (* identifier *)
- | Nexp_constant of int (* constant *)
- | Nexp_times of nexp * nexp (* product *)
- | Nexp_sum of nexp * nexp (* sum *)
- | Nexp_exp of nexp (* exponential *)
-
-and nexp = 
-   Nexp_aux of nexp_aux * l
-
-
-type 
-kind = 
-   K_aux of kind_aux * l
-
-
-type 
-nexp_constraint_aux =  (* constraint over kind $_$ *)
-   NC_fixed of nexp * nexp
- | NC_bounded_ge of nexp * nexp
- | NC_bounded_le of nexp * nexp
- | NC_nat_set_bounded of id * (int) list
-
-
-type 
-kinded_id_aux =  (* optionally kind-annotated identifier *)
-   KOpt_none of id (* identifier *)
- | KOpt_kind of kind * id (* kind-annotated variable *)
-
-
-type 
-nexp_constraint = 
-   NC_aux of nexp_constraint_aux * l
-
-
-type 
-kinded_id = 
-   KOpt_aux of kinded_id_aux * l
-
-
-type 
-efct_aux =  (* effect *)
-   Effect_rreg (* read register *)
- | Effect_wreg (* write register *)
- | Effect_rmem (* read memory *)
- | Effect_wmem (* write memory *)
- | Effect_undef (* undefined-instruction exception *)
- | Effect_unspec (* unspecified values *)
- | Effect_nondet (* nondeterminism from intra-instruction parallelism *)
-
-
-type 
-quant_item_aux =  (* Either a kinded identifier or a nexp constraint for a typquant *)
-   QI_id of kinded_id (* An optionally kinded identifier *)
- | QI_const of nexp_constraint (* A constraint for this type *)
-
-
-type 
-efct = 
-   Effect_aux of efct_aux * l
-
-
-type 
-quant_item = 
-   QI_aux of quant_item_aux * l
-
-
-type 
-effects_aux =  (* effect set, of kind $_$ *)
-   Effects_var of id
- | Effects_set of (efct) list (* effect set *)
-
-
-type 
-order_aux =  (* vector order specifications, of kind $_$ *)
-   Ord_id of id (* identifier *)
- | Ord_inc (* increasing (little-endian) *)
- | Ord_dec (* decreasing (big-endian) *)
-
-
-type 
-typquant_aux =  (* type quantifiers and constraints *)
-   TypQ_tq of (quant_item) list
- | TypQ_no_forall (* sugar, omitting quantifier and constraints *)
-
-
-type 
-effects = 
-   Effects_aux of effects_aux * l
-
-
-type 
-order = 
-   Ord_aux of order_aux * l
-
-
-type 
-lit_aux =  (* Literal constant *)
-   L_unit (* $() : _$ *)
- | L_zero (* $_ : _$ *)
- | L_one (* $_ : _$ *)
- | L_true (* $_ : _$ *)
- | L_false (* $_ : _$ *)
- | L_num of int (* natural number constant *)
- | L_hex of string (* bit vector constant, C-style *)
- | L_bin of string (* bit vector constant, C-style *)
- | L_undef (* constant representing undefined values *)
- | L_string of string (* string constant *)
-
-
-type 
-typquant = 
-   TypQ_aux of typquant_aux * l
-
-
-type 
-typ_aux =  (* Type expressions, of kind $_$ *)
-   Typ_wild (* Unspecified type *)
- | Typ_var of id (* Type variable *)
- | Typ_fn of typ * typ * effects (* Function type (first-order only in user code) *)
- | Typ_tup of (typ) list (* Tuple type *)
- | Typ_app of id * (typ_arg) list (* type constructor application *)
-
-and typ = 
-   Typ_aux of typ_aux * l
-
-and typ_arg_aux =  (* 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 * l
-
-
-type 
-lit = 
-   L_aux of lit_aux * l
-
-
-type 
-typschm_aux =  (* type scheme *)
-   TypSchm_ts of typquant * typ
-
-
-type 
-'a pat_aux =  (* Pattern *)
-   P_lit of lit (* literal constant pattern *)
- | P_wild (* wildcard *)
- | P_as of 'a pat * id (* named pattern *)
- | P_typ of typ * 'a pat (* typed pattern *)
- | P_id of id (* identifier *)
- | P_app of id * ('a pat) list (* union constructor pattern *)
- | P_record of ('a fpat) list * bool (* struct pattern *)
- | P_vector of ('a pat) list (* vector pattern *)
- | P_vector_indexed of ((int * 'a pat)) list (* vector pattern (with explicit indices) *)
- | P_vector_concat of ('a pat) list (* concatenated vector pattern *)
- | P_tup of ('a pat) list (* tuple pattern *)
- | P_list of ('a pat) list (* list pattern *)
-
-and 'a pat = 
-   P_aux of 'a pat_aux * 'a annot
-
-and 'a fpat_aux =  (* Field pattern *)
-   FP_Fpat of id * 'a pat
-
-and 'a fpat = 
-   FP_aux of 'a fpat_aux * 'a annot
-
-
-type 
-typschm = 
-   TypSchm_aux of typschm_aux * l
-
-
-type 
-'a exp_aux =  (* Expression *)
-   E_block of ('a exp) list (* block (parsing conflict with structs?) *)
- | E_id of id (* identifier *)
- | E_lit of lit (* literal constant *)
- | E_cast of typ * 'a exp (* cast *)
- | E_app of 'a exp * ('a exp) list (* function application *)
- | E_app_infix of 'a exp * id * 'a exp (* infix function application *)
- | E_tuple of ('a exp) list (* tuple *)
- | E_if of 'a exp * 'a exp * 'a exp (* conditional *)
- | E_for of id * 'a exp * 'a exp * 'a exp * 'a exp (* loop *)
- | E_vector of ('a exp) list (* vector (indexed from 0) *)
- | E_vector_indexed of ((int * 'a exp)) list (* vector (indexed consecutively) *)
- | E_vector_access of 'a exp * 'a exp (* vector access *)
- | E_vector_subrange of 'a exp * 'a exp * 'a exp (* subvector extraction *)
- | E_vector_update of 'a exp * 'a exp * 'a exp (* vector functional update *)
- | E_vector_update_subrange of 'a exp * 'a exp * 'a exp * 'a exp (* vector subrange update (with vector) *)
- | E_list of ('a exp) list (* list *)
- | E_cons of 'a exp * 'a exp (* cons *)
- | E_record of 'a fexps (* struct *)
- | E_record_update of 'a exp * 'a fexps (* functional update of struct *)
- | E_field of 'a exp * id (* field projection from struct *)
- | E_case of 'a exp * ('a pexp) list (* pattern matching *)
- | E_let of 'a letbind * 'a exp (* let expression *)
- | E_assign of 'a lexp * 'a exp (* imperative assignment *)
-
-and 'a exp = 
-   E_aux of 'a exp_aux * 'a annot
-
-and 'a lexp_aux =  (* lvalue expression *)
-   LEXP_id of id (* identifier *)
- | LEXP_vector of 'a lexp * 'a exp (* vector element *)
- | LEXP_vector_range of 'a lexp * 'a exp * 'a exp (* subvector *)
- | LEXP_field of 'a lexp * id (* struct field *)
-
-and 'a lexp = 
-   LEXP_aux of 'a lexp_aux * 'a annot
-
-and 'a fexp_aux =  (* Field-expression *)
-   FE_Fexp of id * 'a exp
-
-and 'a fexp = 
-   FE_aux of 'a fexp_aux * 'a annot
-
-and 'a fexps_aux =  (* Field-expression list *)
-   FES_Fexps of ('a fexp) list * bool
-
-and 'a fexps = 
-   FES_aux of 'a fexps_aux * 'a annot
-
-and 'a pexp_aux =  (* Pattern match *)
-   Pat_exp of 'a pat * 'a exp
-
-and 'a pexp = 
-   Pat_aux of 'a pexp_aux * 'a annot
-
-and 'a letbind_aux =  (* Let binding *)
-   LB_val_explicit of typschm * 'a pat * 'a exp (* value binding, explicit type ('a pat must be total) *)
- | LB_val_implicit of 'a pat * 'a exp (* value binding, implicit type ('a pat must be total) *)
-
-and 'a letbind = 
-   LB_aux of 'a letbind_aux * 'a annot
-
-
-type 
-rec_opt_aux =  (* Optional recursive annotation for functions *)
-   Rec_nonrec (* non-recursive *)
- | Rec_rec (* recursive *)
-
-
-type 
-'a funcl_aux =  (* Function clause *)
-   FCL_Funcl of id * 'a pat * 'a exp
-
-
-type 
-'a tannot_opt_aux =  (* Optional type annotation for functions *)
-   Typ_annot_opt_some of typquant * typ
-
-
-type 
-'a effects_opt_aux =  (* Optional effect annotation for functions *)
-   Effects_opt_pure (* sugar for empty effect set *)
- | Effects_opt_effects of effects
-
-
-type 
-naming_scheme_opt_aux =  (* Optional variable-naming-scheme specification for variables of defined type *)
-   Name_sect_none
- | Name_sect_some of string
-
-
-type 
-rec_opt = 
-   Rec_aux of rec_opt_aux * l
-
-
-type 
-'a funcl = 
-   FCL_aux of 'a funcl_aux * 'a annot
-
-
-type 
-'a tannot_opt = 
-   Typ_annot_opt_aux of 'a tannot_opt_aux * 'a annot
-
-
-type 
-'a effects_opt = 
-   Effects_opt_aux of 'a effects_opt_aux * 'a annot
-
-
-type 
-index_range_aux =  (* index specification, for bitfields in register types *)
-   BF_single of int (* single index *)
- | BF_range of int * int (* index range *)
- | BF_concat of index_range * index_range (* concatenation of index ranges *)
-
-and index_range = 
-   BF_aux of index_range_aux * l
-
-
-type 
-naming_scheme_opt = 
-   Name_sect_aux of naming_scheme_opt_aux * l
-
-
-type 
-'a fundef_aux =  (* Function definition *)
-   FD_function of rec_opt * 'a tannot_opt * 'a effects_opt * ('a funcl) list
-
-
-type 
-'a val_spec_aux =  (* Value type specification *)
-   VS_val_spec of typschm * id
-
-
-type 
-'a default_typing_spec_aux =  (* Default kinding or typing assumption *)
-   DT_kind of base_kind * id
- | DT_typ of typschm * id
-
-
-type 
-'a type_def_aux =  (* Type definition body *)
-   TD_abbrev of id * naming_scheme_opt * typschm (* type abbreviation *)
- | TD_record of id * naming_scheme_opt * typquant * ((typ * id)) list * bool (* struct type definition *)
- | TD_variant of id * naming_scheme_opt * typquant * ((typ * id)) list * bool (* union type definition *)
- | TD_enum of id * naming_scheme_opt * (id) list * bool (* enumeration type definition *)
- | TD_register of id * nexp * nexp * ((index_range * id)) list (* register mutable bitfield type definition *)
-
-
-type 
-ne =  (* internal numeric expressions *)
-   Ne_var of id
- | Ne_const of int
- | Ne_mult of ne * ne
- | Ne_add of ne * ne
- | Ne_exp of ne
- | Ne_unary of ne
-
-
-type 
-'a fundef = 
-   FD_aux of 'a fundef_aux * 'a annot
-
-
-type 
-'a val_spec = 
-   VS_aux of 'a val_spec_aux * 'a annot
-
-
-type 
-'a default_typing_spec = 
-   DT_aux of 'a default_typing_spec_aux * 'a annot
-
-
-type 
-'a type_def = 
-   TD_aux of 'a type_def_aux * 'a annot
-
-
-type 
-k =  (* Internal kinds *)
-   Ki_typ
- | Ki_nat
- | Ki_ord
- | Ki_efct
- | Ki_val (* Representing values, for use in identifier checks *)
- | Ki_ctor of (k) list * k
- | Ki_infer (* Representing an unknown kind, inferred by context *)
-
-
-type 
-'a def_aux =  (* Top-level definition *)
-   DEF_type of 'a type_def (* type definition *)
- | 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 typ * id (* register declaration *)
- | DEF_scattered_function of rec_opt * 'a tannot_opt * 'a effects_opt * id (* scattered function definition header *)
- | DEF_scattered_funcl of 'a funcl (* scattered function definition clause *)
- | DEF_scattered_variant of id * naming_scheme_opt * typquant (* scattered union definition header *)
- | DEF_scattered_unioncl of id * typ * id (* scattered union definition member *)
- | DEF_scattered_end of id (* scattered definition end *)
-
-
-type 
-'a ctor_def_aux =  (* Datatype constructor definition clause *)
-   CT_ct of id * typschm
-
-
-type 
-'a typ_lib_aux =  (* library types and syntactic sugar for them *)
-   Typ_lib_unit (* unit type with value $()$ *)
- | Typ_lib_bool (* booleans $_$ and $_$ *)
- | Typ_lib_bit (* pure bit values (not mutable bits) *)
- | Typ_lib_nat (* natural numbers 0,1,2,... *)
- | Typ_lib_string of string (* UTF8 strings *)
- | Typ_lib_enum of nexp * nexp * order (* natural numbers nexp .. nexp+nexp-1, ordered by order *)
- | Typ_lib_enum1 of nexp (* sugar for \texttt{enum nexp 0 inc} *)
- | Typ_lib_enum2 of nexp * nexp (* sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} *)
- | Typ_lib_vector of nexp * nexp * order * typ (* vector of typ, indexed by natural range *)
- | Typ_lib_vector2 of typ * nexp (* sugar for vector indexed by [ nexp ] *)
- | Typ_lib_vector3 of typ * nexp * nexp (* sugar for vector indexed by [ nexp..nexp ] *)
- | Typ_lib_list of typ (* list of typ *)
- | Typ_lib_set of typ (* finite set of typ *)
- | Typ_lib_reg of typ (* mutable register components holding typ *)
-
-
-type 
-'a def = 
-   DEF_aux of 'a def_aux * 'a annot
-
-
-type 
-'a ctor_def = 
-   CT_aux of 'a ctor_def_aux * 'a annot
-
-
-type 
-'a typ_lib = 
-   Typ_lib_aux of 'a typ_lib_aux * l
-
-
-type 
-'a defs =  (* Definition sequence *)
-   Defs of ('a def) list
-
-
-
+../language/l2.ml
\ No newline at end of file
diff --git a/src/lem_interp/ast.lem b/src/lem_interp/ast.lem
index 51831898..37719b1b 100644..120000
--- a/src/lem_interp/ast.lem
+++ b/src/lem_interp/ast.lem
@@ -1,304 +1 @@
-(* generated by Ott 0.22 from: l2.ott *)
-
-open Pmap
-open Pervasives
-
-type l =
-  | Unknown
-  | Trans of string * option l
-  | Range of num * num
-
-val disjoint : forall 'a . set 'a -> set 'a -> bool
-let disjoint s1 s2 = 
-  let diff = s1 inter s2 in
-  diff = Pervasives.empty
-
-val disjoint_all : forall 'a. list (set 'a) -> bool
-let rec disjoint_all ls = match ls with
-  | [] -> true
-  | [a] -> true
-  | a::b::rs -> (disjoint a b) && (disjoint_all (b::rs))
-end
-
-val duplicates : forall 'a. list 'a -> list 'a
-
-val union_map : forall 'a 'b. map 'a 'b -> map 'a 'b -> map 'a 'b
-
-val set_from_list : forall 'a. list 'a -> set 'a
-
-val subst : forall 'a. list 'a -> list 'a -> bool
-
-
-type x = string (* identifier *)
-type ix = string (* infix identifier *)
-
-type base_kind =  (* base kind *)
- | BK_type (* kind of types *)
- | BK_nat (* kind of natural number size expressions *)
- | BK_order (* kind of vector order specifications *)
- | BK_effects (* kind of effect sets *)
-
-
-type id =  (* Identifier *)
- | Id of x
- | DeIid of x (* remove infix status *)
-
-
-type kind =  (* kinds *)
- | K_kind of list base_kind
-
-
-type nexp =  (* expression of kind $Nat$, for vector sizes and origins *)
- | Nexp_id of id (* identifier *)
- | Nexp_constant of num (* constant *)
- | Nexp_times of nexp * nexp (* product *)
- | Nexp_sum of nexp * nexp (* sum *)
- | Nexp_exp of nexp (* exponential *)
-
-
-type efct =  (* effect *)
- | Effect_rreg (* read register *)
- | Effect_wreg (* write register *)
- | Effect_rmem (* read memory *)
- | Effect_wmem (* write memory *)
- | Effect_undef (* undefined-instruction exception *)
- | Effect_unspec (* unspecified values *)
- | Effect_nondet (* nondeterminism from intra-instruction parallelism *)
-
-
-type kinded_id =  (* optionally kind-annotated identifier *)
- | KOpt_none of id (* identifier *)
- | KOpt_kind of kind * id (* kind-annotated variable *)
-
-
-type nexp_constraint =  (* constraint over kind $Nat$ *)
- | NC_fixed of nexp * nexp
- | NC_bounded_ge of nexp * nexp
- | NC_bounded_le of nexp * nexp
- | NC_nat_set_bounded of id * list num
-
-
-type order =  (* vector order specifications, of kind $Order$ *)
- | Ord_id of id (* identifier *)
- | Ord_inc (* increasing (little-endian) *)
- | Ord_dec (* decreasing (big-endian) *)
-
-
-type effects =  (* effect set, of kind $Effects$ *)
- | Effects_var of id
- | Effects_set of list efct (* effect set *)
-
-
-type quant_item =  (* Either a kinded identifier or a nexp constraint for a typquant *)
- | QI_id of kinded_id (* An optionally kinded identifier *)
- | QI_const of nexp_constraint (* A constraint for this type *)
-
-
-type typ =  (* Type expressions, of kind $Type$ *)
- | Typ_wild (* Unspecified type *)
- | Typ_var of id (* Type variable *)
- | Typ_fn of typ * typ * effects (* Function type (first-order only in user code) *)
- | Typ_tup of list typ (* Tuple type *)
- | Typ_app of id * list typ_arg (* type constructor application *)
-
-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
-
-
-type typquant =  (* type quantifiers and constraints *)
- | TypQ_tq of list quant_item
- | TypQ_no_forall (* sugar, omitting quantifier and constraints *)
-
-
-type lit =  (* Literal constant *)
- | L_unit (* $() : unit$ *)
- | L_zero (* $bitzero : bit$ *)
- | L_one (* $bitone : bit$ *)
- | L_true (* $true : bool$ *)
- | L_false (* $false : bool$ *)
- | L_num of num (* natural number constant *)
- | L_hex of string (* bit vector constant, C-style *)
- | L_bin of string (* bit vector constant, C-style *)
- | L_undef (* constant representing undefined values *)
- | L_string of string (* string constant *)
-
-
-type typschm =  (* type scheme *)
- | TypSchm_ts of typquant * typ
-
-
-type pat =  (* Pattern *)
- | P_lit of lit (* literal constant pattern *)
- | P_wild (* wildcard *)
- | P_as of pat * id (* named pattern *)
- | P_typ of typ * pat (* typed pattern *)
- | P_id of id (* identifier *)
- | P_app of id * list pat (* union constructor pattern *)
- | P_record of list fpat * bool (* struct pattern *)
- | P_vector of list pat (* vector pattern *)
- | P_vector_indexed of list (num * pat) (* vector pattern (with explicit indices) *)
- | P_vector_concat of list pat (* concatenated vector pattern *)
- | P_tup of list pat (* tuple pattern *)
- | P_list of list pat (* list pattern *)
-
-and fpat =  (* Field pattern *)
- | FP_Fpat of id * pat
-
-
-type ne =  (* internal numeric expressions *)
- | Ne_var of id
- | Ne_const of num
- | Ne_mult of ne * ne
- | Ne_add of ne * ne
- | Ne_exp of ne
- | Ne_unary of ne
-
-
-type letbind =  (* Let binding *)
- | LB_val_explicit of typschm * pat * exp (* value binding, explicit type (pat must be total) *)
- | LB_val_implicit of pat * exp (* value binding, implicit type (pat must be total) *)
-
-and exp =  (* Expression *)
- | E_block of list exp (* block (parsing conflict with structs?) *)
- | E_id of id (* identifier *)
- | E_lit of lit (* literal constant *)
- | E_cast of typ * exp (* cast *)
- | E_app of exp * list exp (* function application *)
- | E_app_infix of exp * id * exp (* infix function application *)
- | E_tuple of list exp (* tuple *)
- | E_if of exp * exp * exp (* conditional *)
- | E_for of id * exp * exp * exp * exp (* loop *)
- | E_vector of list exp (* vector (indexed from 0) *)
- | E_vector_indexed of list (num * exp) (* vector (indexed consecutively) *)
- | E_vector_access of exp * exp (* vector access *)
- | E_vector_subrange of exp * exp * exp (* subvector extraction *)
- | E_vector_update of exp * exp * exp (* vector functional update *)
- | E_vector_update_subrange of exp * exp * exp * exp (* vector subrange update (with vector) *)
- | E_list of list exp (* list *)
- | E_cons of exp * exp (* cons *)
- | E_record of fexps (* struct *)
- | E_record_update of exp * fexps (* functional update of struct *)
- | E_field of exp * id (* field projection from struct *)
- | E_case of exp * list pexp (* pattern matching *)
- | E_let of letbind * exp (* let expression *)
- | E_assign of lexp * exp (* imperative assignment *)
-
-and lexp =  (* lvalue expression *)
- | LEXP_id of id (* identifier *)
- | LEXP_vector of lexp * exp (* vector element *)
- | LEXP_vector_range of lexp * exp * exp (* subvector *)
- | LEXP_field of lexp * id (* struct field *)
-
-and fexp =  (* Field-expression *)
- | FE_Fexp of id * exp
-
-and fexps =  (* Field-expression list *)
- | FES_Fexps of list fexp * bool
-
-and pexp =  (* Pattern match *)
- | Pat_exp of pat * exp
-
-
-type k =  (* Internal kinds *)
- | Ki_typ
- | Ki_nat
- | Ki_ord
- | Ki_efct
- | Ki_val (* Representing values, for use in identifier checks *)
- | Ki_ctor of list k * k
- | Ki_infer (* Representing an unknown kind, inferred by context *)
-
-
-type index_range =  (* index specification, for bitfields in register types *)
- | BF_single of num (* single index *)
- | BF_range of num * num (* index range *)
- | BF_concat of index_range * index_range (* concatenation of index ranges *)
-
-
-type naming_scheme_opt =  (* Optional variable-naming-scheme specification for variables of defined type *)
- | Name_sect_none
- | Name_sect_some of string
-
-
-type rec_opt =  (* Optional recursive annotation for functions *)
- | Rec_nonrec (* non-recursive *)
- | Rec_rec (* recursive *)
-
-
-type effects_opt =  (* Optional effect annotation for functions *)
- | Effects_opt_pure (* sugar for empty effect set *)
- | Effects_opt_effects of effects
-
-
-type funcl =  (* Function clause *)
- | FCL_Funcl of id * pat * exp
-
-
-type tannot_opt =  (* Optional type annotation for functions *)
- | Typ_annot_opt_some of typquant * typ
-
-
-type default_typing_spec =  (* Default kinding or typing assumption *)
- | DT_kind of base_kind * id
- | DT_typ of typschm * id
-
-
-type val_spec =  (* Value type specification *)
- | VS_val_spec of typschm * id
-
-
-type type_def =  (* Type definition body *)
- | TD_abbrev of id * naming_scheme_opt * typschm (* type abbreviation *)
- | TD_record of id * naming_scheme_opt * typquant * list (typ * id) * bool (* struct type definition *)
- | TD_variant of id * naming_scheme_opt * typquant * list (typ * id) * bool (* union type definition *)
- | TD_enum of id * naming_scheme_opt * list id * bool (* enumeration type definition *)
- | TD_register of id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *)
-
-
-type fundef =  (* Function definition *)
- | FD_function of rec_opt * tannot_opt * effects_opt * list funcl
-
-
-type def =  (* 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 typ * id (* register declaration *)
- | DEF_scattered_function of rec_opt * tannot_opt * effects_opt * id (* scattered function definition header *)
- | DEF_scattered_funcl of funcl (* scattered function definition clause *)
- | DEF_scattered_variant of id * naming_scheme_opt * typquant (* scattered union definition header *)
- | DEF_scattered_unioncl of id * typ * id (* scattered union definition member *)
- | DEF_scattered_end of id (* scattered definition end *)
-
-
-type typ_lib =  (* library types and syntactic sugar for them *)
- | Typ_lib_unit (* unit type with value $()$ *)
- | Typ_lib_bool (* booleans $true$ and $false$ *)
- | Typ_lib_bit (* pure bit values (not mutable bits) *)
- | Typ_lib_nat (* natural numbers 0,1,2,... *)
- | Typ_lib_string of string (* UTF8 strings *)
- | Typ_lib_enum of nexp * nexp * order (* natural numbers nexp .. nexp+nexp-1, ordered by order *)
- | Typ_lib_enum1 of nexp (* sugar for \texttt{enum nexp 0 inc} *)
- | Typ_lib_enum2 of nexp * nexp (* sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} *)
- | Typ_lib_vector of nexp * nexp * order * typ (* vector of typ, indexed by natural range *)
- | Typ_lib_vector2 of typ * nexp (* sugar for vector indexed by [ nexp ] *)
- | Typ_lib_vector3 of typ * nexp * nexp (* sugar for vector indexed by [ nexp..nexp ] *)
- | Typ_lib_list of typ (* list of typ *)
- | Typ_lib_set of typ (* finite set of typ *)
- | Typ_lib_reg of typ (* mutable register components holding typ *)
-
-
-type ctor_def =  (* Datatype constructor definition clause *)
- | CT_ct of id * typschm
-
-
-type defs =  (* Definition sequence *)
- | Defs of list def
-
-
-
+../../language/l2.lem
\ No newline at end of file
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index b12651c0..c4f970ec 100644..120000
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -1,422 +1 @@
-(* generated by Ott 0.22 from: l2_parse.ott *)
-
-
-type text = string
-
-type l =
-  | Unknown
-  | Trans of string * l option
-  | Range of Lexing.position * Lexing.position
-
-type 'a annot = l * 'a
-
-exception Parse_error_locn of l * string
-
-
-type x = text (* identifier *)
-type ix = text (* infix identifier *)
-
-type 
-base_kind_aux =  (* base kind *)
-   BK_type (* kind of types *)
- | BK_nat (* kind of natural number size expressions *)
- | BK_order (* kind of vector order specifications *)
- | BK_effects (* kind of effect sets *)
-
-
-type 
-efct_aux =  (* effect *)
-   Effect_rreg (* read register *)
- | Effect_wreg (* write register *)
- | Effect_rmem (* read memory *)
- | Effect_wmem (* write memory *)
- | Effect_undef (* undefined-instruction exception *)
- | Effect_unspec (* unspecified values *)
- | Effect_nondet (* nondeterminism from intra-instruction parallelism *)
-
-
-type 
-id_aux =  (* Identifier *)
-   Id of x
- | DeIid of x (* remove infix status *)
-
-
-type 
-base_kind = 
-   BK_aux of base_kind_aux * l
-
-
-type 
-efct = 
-   Effect_aux of efct_aux * l
-
-
-type 
-id = 
-   Id_aux of id_aux * l
-
-
-type 
-kind_aux =  (* kinds *)
-   K_kind of (base_kind) list
-
-
-type 
-atyp_aux =  (* expressions of all kinds, to be translated to types, nats, orders, and effects after parsing *)
-   ATyp_id of id (* identifier *)
- | ATyp_constant of int (* constant *)
- | ATyp_times of atyp * atyp (* product *)
- | ATyp_sum of atyp * atyp (* sum *)
- | ATyp_exp of atyp (* exponential *)
- | ATyp_inc (* increasing (little-endian) *)
- | ATyp_dec (* decreasing (big-endian) *)
- | ATyp_efid of id
- | ATyp_set of (efct) list (* effect set *)
- | ATyp_wild (* Unspecified type *)
- | ATyp_fn of atyp * atyp * atyp (* Function type (first-order only in user code), last atyp is an effect *)
- | ATyp_tup of (atyp) list (* Tuple type *)
- | ATyp_app of id * (atyp) list (* type constructor application *)
-
-and atyp = 
-   ATyp_aux of atyp_aux * l
-
-
-type 
-kind = 
-   K_aux of kind_aux * l
-
-
-type 
-nexp_constraint_aux =  (* constraint over kind $_$ *)
-   NC_fixed of atyp * atyp
- | NC_bounded_ge of atyp * atyp
- | NC_bounded_le of atyp * atyp
- | NC_nat_set_bounded of id * (int) list
-
-
-type 
-kinded_id_aux =  (* optionally kind-annotated identifier *)
-   KOpt_none of id (* identifier *)
- | KOpt_kind of kind * id (* kind-annotated variable *)
-
-
-type 
-nexp_constraint = 
-   NC_aux of nexp_constraint_aux * l
-
-
-type 
-kinded_id = 
-   KOpt_aux of kinded_id_aux * l
-
-
-type 
-quant_item_aux =  (* Either a kinded identifier or a nexp constraint for a typquant *)
-   QI_id of kinded_id (* An optionally kinded identifier *)
- | QI_const of nexp_constraint (* A constraint for this type *)
-
-
-type 
-quant_item = 
-   QI_aux of quant_item_aux * l
-
-
-type 
-typquant_aux =  (* type quantifiers and constraints *)
-   TypQ_tq of (quant_item) list
- | TypQ_no_forall (* sugar, omitting quantifier and constraints *)
-
-
-type 
-lit_aux =  (* Literal constant *)
-   L_unit (* $() : _$ *)
- | L_zero (* $_ : _$ *)
- | L_one (* $_ : _$ *)
- | L_true (* $_ : _$ *)
- | L_false (* $_ : _$ *)
- | L_num of int (* natural number constant *)
- | L_hex of string (* bit vector constant, C-style *)
- | L_bin of string (* bit vector constant, C-style *)
- | L_undef (* undefined value *)
- | L_string of string (* string constant *)
-
-
-type 
-typquant = 
-   TypQ_aux of typquant_aux * l
-
-
-type 
-lit = 
-   L_aux of lit_aux * l
-
-
-type 
-typschm_aux =  (* type scheme *)
-   TypSchm_ts of typquant * atyp
-
-
-type 
-pat_aux =  (* Pattern *)
-   P_lit of lit (* literal constant pattern *)
- | P_wild (* wildcard *)
- | P_as of pat * id (* named pattern *)
- | P_typ of atyp * pat (* typed pattern *)
- | P_id of id (* identifier *)
- | P_app of id * (pat) list (* union constructor pattern *)
- | P_record of (fpat) list * bool (* struct pattern *)
- | P_vector of (pat) list (* vector pattern *)
- | P_vector_indexed of ((int * pat)) list (* vector pattern (with explicit indices) *)
- | P_vector_concat of (pat) list (* concatenated vector pattern *)
- | P_tup of (pat) list (* tuple pattern *)
- | P_list of (pat) list (* list pattern *)
-
-and pat = 
-   P_aux of pat_aux * l
-
-and fpat_aux =  (* Field pattern *)
-   FP_Fpat of id * pat
-
-and fpat = 
-   FP_aux of fpat_aux * l
-
-
-type 
-typschm = 
-   TypSchm_aux of typschm_aux * l
-
-
-type 
-exp_aux =  (* Expression *)
-   E_block of (exp) list (* block (parsing conflict with structs?) *)
- | E_id of id (* identifier *)
- | E_lit of lit (* literal constant *)
- | E_cast of atyp * exp (* cast *)
- | E_app of exp * (exp) list (* function application *)
- | E_app_infix of exp * id * exp (* infix function application *)
- | E_tuple of (exp) list (* tuple *)
- | E_if of exp * exp * exp (* conditional *)
- | E_for of id * exp * exp * exp * exp (* loop *)
- | E_vector of (exp) list (* vector (indexed from 0) *)
- | E_vector_indexed of ((int * exp)) list (* vector (indexed consecutively) *)
- | E_vector_access of exp * exp (* vector access *)
- | E_vector_subrange of exp * exp * exp (* subvector extraction *)
- | E_vector_update of exp * exp * exp (* vector functional update *)
- | E_vector_update_subrange of exp * exp * exp * exp (* vector subrange update (with vector) *)
- | E_list of (exp) list (* list *)
- | E_cons of exp * exp (* cons *)
- | E_record of fexps (* struct *)
- | E_record_update of exp * (exp) list (* functional update of struct *)
- | E_field of exp * id (* field projection from struct *)
- | E_case of exp * (pexp) list (* pattern matching *)
- | E_let of letbind * exp (* let expression *)
- | E_assign of exp * exp (* imperative assignment *)
-
-and exp = 
-   E_aux of exp_aux * l
-
-and fexp_aux =  (* Field-expression *)
-   FE_Fexp of id * exp
-
-and fexp = 
-   FE_aux of fexp_aux * l
-
-and fexps_aux =  (* Field-expression list *)
-   FES_Fexps of (fexp) list * bool
-
-and fexps = 
-   FES_aux of fexps_aux * l
-
-and pexp_aux =  (* Pattern match *)
-   Pat_exp of pat * exp
-
-and pexp = 
-   Pat_aux of pexp_aux * l
-
-and letbind_aux =  (* Let binding *)
-   LB_val_explicit of typschm * pat * exp (* value binding, explicit type (pat must be total) *)
- | LB_val_implicit of pat * exp (* value binding, implicit type (pat must be total) *)
-
-and letbind = 
-   LB_aux of letbind_aux * l
-
-
-type 
-naming_scheme_opt_aux =  (* Optional variable-naming-scheme specification for variables of defined type *)
-   Name_sect_none
- | Name_sect_some of string
-
-
-type 
-tannot_opt_aux =  (* Optional type annotation for functions *)
-   Typ_annot_opt_none
- | Typ_annot_opt_some of typquant * atyp
-
-
-type 
-effects_opt_aux =  (* Optional effect annotation for functions *)
-   Effects_opt_pure (* sugar for empty effect set *)
- | Effects_opt_effects of atyp
-
-
-type 
-rec_opt_aux =  (* Optional recursive annotation for functions *)
-   Rec_nonrec (* non-recursive *)
- | Rec_rec (* recursive *)
-
-
-type 
-funcl_aux =  (* Function clause *)
-   FCL_Funcl of id * pat * exp
-
-
-type 
-index_range_aux =  (* index specification, for bitfields in register types *)
-   BF_single of int (* single index *)
- | BF_range of int * int (* index range *)
- | BF_concat of index_range * index_range (* concatenation of index ranges *)
-
-and index_range = 
-   BF_aux of index_range_aux * l
-
-
-type 
-naming_scheme_opt = 
-   Name_sect_aux of naming_scheme_opt_aux * l
-
-
-type 
-tannot_opt = 
-   Typ_annot_opt_aux of tannot_opt_aux * l
-
-
-type 
-effects_opt = 
-   Effects_opt_aux of effects_opt_aux * l
-
-
-type 
-rec_opt = 
-   Rec_aux of rec_opt_aux * l
-
-
-type 
-funcl = 
-   FCL_aux of funcl_aux * l
-
-
-type 
-val_spec_aux =  (* Value type specification *)
-   VS_val_spec of typschm * id
-
-
-type 
-type_def_aux =  (* Type definition body *)
-   TD_abbrev of id * naming_scheme_opt * typschm (* type abbreviation *)
- | TD_record of id * naming_scheme_opt * typquant * ((atyp * id)) list * bool (* struct type definition *)
- | TD_variant of id * naming_scheme_opt * typquant * ((atyp * id)) list * bool (* union type definition *)
- | TD_enum of id * naming_scheme_opt * (id) list * bool (* enumeration type definition *)
- | TD_register of id * atyp * atyp * ((index_range * id)) list (* register mutable bitfield type definition *)
-
-
-type 
-default_typing_spec_aux =  (* Default kinding or typing assumption *)
-   DT_kind of base_kind * id
- | DT_typ of typschm * id
-
-
-type 
-fundef_aux =  (* Function definition *)
-   FD_function of rec_opt * tannot_opt * effects_opt * (funcl) list
-
-
-type 
-val_spec = 
-   VS_aux of val_spec_aux * l
-
-
-type 
-type_def = 
-   TD_aux of type_def_aux * l
-
-
-type 
-default_typing_spec = 
-   DT_aux of default_typing_spec_aux * l
-
-
-type 
-fundef = 
-   FD_aux of fundef_aux * l
-
-
-type 
-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 atyp * id (* register declaration *)
- | DEF_scattered_function of rec_opt * tannot_opt * effects_opt * id (* scattered function definition header *)
- | DEF_scattered_funcl of funcl (* scattered function definition clause *)
- | DEF_scattered_variant of id * naming_scheme_opt * typquant (* scattered union definition header *)
- | DEF_scattered_unioncl of id * atyp * id (* scattered union definition member *)
- | DEF_scattered_end of id (* scattered definition end *)
-
-
-type 
-def = 
-   DEF_aux of def_aux * l
-
-
-type 
-ctor_def_aux =  (* Datatype constructor definition clause *)
-   CT_ct of id * typschm
-
-
-type 
-typ_lib_aux =  (* library types and syntactic sugar for them *)
-   Typ_lib_unit (* unit type with value $()$ *)
- | Typ_lib_bool (* booleans $_$ and $_$ *)
- | Typ_lib_bit (* pure bit values (not mutable bits) *)
- | Typ_lib_nat (* natural numbers 0,1,2,... *)
- | Typ_lib_string of string (* UTF8 strings *)
- | Typ_lib_enum (* natural numbers _ .. _+_-1, ordered by order *)
- | Typ_lib_enum1 (* sugar for \texttt{enum nexp 0 inc} *)
- | Typ_lib_enum2 (* sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} *)
- | Typ_lib_vector of atyp (* vector of atyp, indexed by natural range *)
- | Typ_lib_vector2 of atyp (* sugar for vector indexed by [ atyp ] *)
- | Typ_lib_vector3 of atyp (* sugar for vector indexed by [ atyp.._ ] *)
- | Typ_lib_list of atyp (* list of atyp *)
- | Typ_lib_set of atyp (* finite set of atyp *)
- | Typ_lib_reg of atyp (* mutable register components holding atyp *)
-
-
-type 
-lexp_aux =  (* lvalue expression *)
-   LEXP_id of id (* identifier *)
- | LEXP_vector of lexp * exp (* vector element *)
- | LEXP_vector_range of lexp * exp * exp (* subvector *)
- | LEXP_field of lexp * id (* struct field *)
-
-and lexp = 
-   LEXP_aux of lexp_aux * l
-
-
-type 
-defs =  (* Definition sequence *)
-   Defs of (def) list
-
-
-type 
-ctor_def = 
-   CT_aux of ctor_def_aux * l
-
-
-type 
-typ_lib = 
-   Typ_lib_aux of typ_lib_aux * l
-
-
-
+../language/l2_parse.ml
\ No newline at end of file