summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/_build/reporting_basic.ml172
-rw-r--r--src/_build/reporting_basic.mli103
-rw-r--r--src/ast.ml118
-rw-r--r--src/main.ml7
-rw-r--r--src/parser.mly84
-rw-r--r--src/process_file.ml13
6 files changed, 411 insertions, 86 deletions
diff --git a/src/_build/reporting_basic.ml b/src/_build/reporting_basic.ml
new file mode 100644
index 00000000..7f207651
--- /dev/null
+++ b/src/_build/reporting_basic.ml
@@ -0,0 +1,172 @@
+(**************************************************************************)
+(* 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 * char
+ | 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, c) -> ("Lexical error", false, Pos p, "unknown character "^(String.make 1 c))
+ | 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 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
new file mode 100644
index 00000000..3cfdf864
--- /dev/null
+++ b/src/_build/reporting_basic.mli
@@ -0,0 +1,103 @@
+(**************************************************************************)
+(* 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 * char
+ | 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
+
+(** 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 9a394767..adbc876b 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -97,17 +97,6 @@ and nexp =
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
kinded_id_aux = (* optionally kind-annotated identifier *)
KOpt_none of id (* identifier *)
| KOpt_kind of kind * id (* kind-annotated variable *)
@@ -122,8 +111,14 @@ type
type
-efct =
- Effect_aux of efct_aux * l
+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
@@ -137,6 +132,17 @@ type
type
+efct =
+ Effect_aux of efct_aux * l
+
+
+type
+'a 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 'a nexp_constraint (* A constraint for this type *)
+
+
+type
effects_aux = (* effect set, of kind $_$ *)
Effects_var of id
| Effects_set of (efct) list (* effect set *)
@@ -150,9 +156,8 @@ order_aux = (* vector order specifications, of kind $_$ *)
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 'a nexp_constraint (* A constraint for this type *)
+'a quant_item =
+ QI_aux of 'a quant_item_aux * 'a annot
type
@@ -167,7 +172,7 @@ order =
type
'a typquant_aux = (* type quantifiers and constraints *)
- TypQ_tq of (quant_item) list
+ TypQ_tq of ('a quant_item) list
| TypQ_no_forall (* sugar, omitting quantifier and constraints *)
@@ -314,15 +319,14 @@ and 'a pexp =
type
-'a effects_opt_aux = (* Optional effect annotation for functions *)
- Effects_opt_pure (* sugar for empty effect set *)
- | Effects_opt_effects of effects
+naming_scheme_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *)
+ Name_sect_none
+ | Name_sect_some of string
type
-'a tannot_opt_aux = (* Optional type annotation for functions *)
- Typ_annot_opt_none
- | Typ_annot_opt_some of 'a typquant * typ
+'a funcl_aux = (* Function clause *)
+ FCL_Funcl of id * 'a pat * 'a exp
type
@@ -332,29 +336,29 @@ rec_opt_aux = (* Optional recursive annotation for functions *)
type
-'a funcl_aux = (* Function clause *)
- FCL_Funcl of id * 'a pat * 'a exp
+'a tannot_opt_aux = (* Optional type annotation for functions *)
+ Typ_annot_opt_some of 'a typquant * typ
type
-naming_scheme_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *)
- Name_sect_none
- | Name_sect_some of string
+'a effects_opt_aux = (* Optional effect annotation for functions *)
+ Effects_opt_pure (* sugar for empty effect set *)
+ | Effects_opt_effects of effects
type
-'a effects_opt =
- Effects_opt_aux of 'a effects_opt_aux * 'a annot
-
+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 *)
-type
-'a tannot_opt =
- Typ_annot_opt_aux of 'a tannot_opt_aux * 'a annot
+and index_range =
+ BF_aux of index_range_aux * l
type
-rec_opt =
- Rec_aux of rec_opt_aux * l
+naming_scheme_opt =
+ Name_sect_aux of naming_scheme_opt_aux * l
type
@@ -363,18 +367,18 @@ type
type
-naming_scheme_opt =
- Name_sect_aux of naming_scheme_opt_aux * l
+rec_opt =
+ Rec_aux of rec_opt_aux * l
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 *)
+'a tannot_opt =
+ Typ_annot_opt_aux of 'a tannot_opt_aux * 'a annot
-and index_range =
- BF_aux of index_range_aux * l
+
+type
+'a effects_opt =
+ Effects_opt_aux of 'a effects_opt_aux * 'a annot
type
@@ -383,6 +387,15 @@ type
type
+'a type_def_aux = (* Type definition body *)
+ TD_abbrev of id * naming_scheme_opt * 'a typschm (* type abbreviation *)
+ | TD_record of id * naming_scheme_opt * 'a typquant * ((typ * id)) list * bool (* struct type definition *)
+ | TD_variant of id * naming_scheme_opt * 'a 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
'a fundef_aux = (* Function definition *)
FD_function of rec_opt * 'a tannot_opt * 'a effects_opt * ('a funcl) list
@@ -394,17 +407,13 @@ type
type
-'a type_def_aux = (* Type definition body *)
- TD_abbrev of id * naming_scheme_opt * 'a typschm (* type abbreviation *)
- | TD_record of id * naming_scheme_opt * 'a typquant * ((typ * id)) list * bool (* struct type definition *)
- | TD_variant of id * naming_scheme_opt * 'a 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 *)
+'a val_spec =
+ VS_aux of 'a val_spec_aux * 'a annot
type
-'a val_spec =
- VS_aux of 'a val_spec_aux * 'a annot
+'a type_def =
+ TD_aux of 'a type_def_aux * 'a annot
type
@@ -418,11 +427,6 @@ type
type
-'a type_def =
- TD_aux of 'a type_def_aux * 'a annot
-
-
-type
'a def_aux = (* Top-level definition *)
DEF_type of 'a type_def (* type definition *)
| DEF_fundef of 'a fundef (* function definition *)
diff --git a/src/main.ml b/src/main.ml
index f790627c..b5e7878b 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -404,4 +404,9 @@ let main() =
then Printf.printf "L2 pre alpha \n"
else ignore(List.map (fun f -> (parse_file f)) !opt_file_arguments)
-let _ = main()
+let _ = try
+ begin
+ try ignore(main ())
+ with Failure(s) -> raise (Reporting_basic.err_general Parse_ast.Unknown ("Failure "^s))
+ end
+ with Reporting_basic.Fatal_error e -> Reporting_basic.report_error e
diff --git a/src/parser.mly b/src/parser.mly
index d08ab7bf..257c6d7a 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -549,12 +549,8 @@ star_right_atomic_exp:
{ eloc (E_app_infix($1,Id_aux(Id("mod"), locn 2 2), $3)) }
| star_exp StarUnderS starstar_right_atomic_exp
{ eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
- | star_exp StarUnderSi starstar_right_atomic_exp
- { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
| star_exp StarUnderU starstar_right_atomic_exp
{ eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
- | star_exp StarUnderUi starstar_right_atomic_exp
- { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
plus_exp:
| star_exp
@@ -572,18 +568,34 @@ plus_right_atomic_exp:
| plus_exp Minus star_right_atomic_exp
{ eloc (E_app_infix($1,Id_aux(Id("-"), locn 2 2), $3)) }
-cons_exp:
+shift_exp:
| plus_exp
{ $1 }
- | plus_exp ColonColon cons_exp
+ | shift_exp GtGt plus_exp
+ { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
+ | shift_exp GtGtGt plus_exp
+ { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
+ | shift_exp LtLt plus_exp
+ { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
+
+shift_right_atomic_exp:
+ | plus_right_atomic_exp
+ { $1 }
+ | shift_exp GtGt plus_right_atomic_exp
+ { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
+
+cons_exp:
+ | shift_exp
+ { $1 }
+ | shift_exp ColonColon cons_exp
{ eloc (E_cons($1,$3)) }
- | plus_exp Colon cons_exp
+ | shift_exp Colon cons_exp
{ eloc (E_app_infix($1,Id_aux(Id(":"), locn 2 2), $3)) }
cons_right_atomic_exp:
- | plus_right_atomic_exp
+ | shift_right_atomic_exp
{ $1 }
- | plus_exp ColonColon cons_right_atomic_exp
+ | shift_exp ColonColon cons_right_atomic_exp
{ eloc (E_cons($1,$3)) }
at_exp:
@@ -595,6 +607,8 @@ at_exp:
{ eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
| cons_exp Carrot at_exp
{ eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
+ | cons_exp TildeCarrot at_exp
+ { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
at_right_atomic_exp:
| cons_right_atomic_exp
@@ -611,20 +625,32 @@ eq_exp:
{ $1 }
| eq_exp Eq at_exp
{ eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
+ | eq_exp EqEq at_exp
+ { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
+ | eq_exp ExclEq at_exp
+ { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
| eq_exp GtEq at_exp
{ eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) }
+ | eq_exp GtEqUnderS at_exp
+ { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
+ | eq_exp GtEqUnderU at_exp
+ { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
| eq_exp Gt at_exp
{ eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) }
+ | eq_exp GtUnderS at_exp
+ { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
| eq_exp LtEq at_exp
{ eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) }
+ | eq_exp LtEqUnderS at_exp
+ { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
| eq_exp Lt at_exp
{ eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) }
| eq_exp LtUnderS at_exp
{ eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) }
| eq_exp LtUnderSi at_exp
{ eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) }
- | eq_exp IN at_exp
- { eloc (E_app_infix($1,Id_aux(Id("In"), locn 2 2), $3)) }
+ | eq_exp LtUnderU at_exp
+ { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
| eq_exp ColonEq at_exp
{ eloc (E_assign($1,$3)) }
@@ -633,6 +659,32 @@ eq_right_atomic_exp:
{ $1 }
| eq_exp Eq at_right_atomic_exp
{ eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
+ | eq_exp EqEq at_right_atomic_exp
+ { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
+ | eq_exp ExclEq at_right_atomic_exp
+ { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
+ | eq_exp GtEq at_right_atomic_exp
+ { eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) }
+ | eq_exp GtEqUnderS at_right_atomic_exp
+ { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
+ | eq_exp GtEqUnderU at_right_atomic_exp
+ { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
+ | eq_exp Gt at_right_atomic_exp
+ { eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) }
+ | eq_exp GtUnderS at_right_atomic_exp
+ { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
+ | eq_exp LtEq at_right_atomic_exp
+ { eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) }
+ | eq_exp LtEqUnderS at_right_atomic_exp
+ { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
+ | eq_exp Lt at_right_atomic_exp
+ { eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) }
+ | eq_exp LtUnderS at_right_atomic_exp
+ { eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) }
+ | eq_exp LtUnderSi at_right_atomic_exp
+ { eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) }
+ | eq_exp LtUnderU at_right_atomic_exp
+ { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
| eq_exp ColonEq at_right_atomic_exp
{ eloc (E_assign($1,$3)) }
@@ -643,9 +695,6 @@ and_exp:
{ eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
| eq_exp AmpAmp and_exp
{ eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
- | eq_exp AND and_exp
- { eloc (E_app_infix($1,Id_aux(Id("And"), locn 2 2), $3)) }
-
and_right_atomic_exp:
| eq_right_atomic_exp
@@ -654,8 +703,6 @@ and_right_atomic_exp:
{ eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
| eq_exp AmpAmp and_right_atomic_exp
{ eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
- | eq_exp AND and_right_atomic_exp
- { eloc (E_app_infix($1,Id_aux(Id("And"), locn 2 2), $3)) }
or_exp:
| and_exp
@@ -664,9 +711,6 @@ or_exp:
{ eloc (E_app_infix($1,Id_aux(Id("|"), locn 2 2), $3)) }
| and_exp BarBar or_exp
{ eloc (E_app_infix($1,Id_aux(Id("||"), locn 2 2), $3)) }
- | and_exp OR or_exp
- { eloc (E_app_infix($1,Id_aux(Id("OR"), locn 2 2), $3)) }
-
or_right_atomic_exp:
| and_right_atomic_exp
@@ -675,8 +719,6 @@ or_right_atomic_exp:
{ eloc (E_app_infix($1,Id_aux(Id("|"), locn 2 2), $3)) }
| and_exp BarBar or_right_atomic_exp
{ eloc (E_app_infix($1,Id_aux(Id("||"), locn 2 2), $3)) }
- | and_exp OR or_right_atomic_exp
- { eloc (E_app_infix($1,Id_aux(Id("OR"), locn 2 2), $3)) }
exp:
| or_exp
diff --git a/src/process_file.ml b/src/process_file.ml
index a674c66f..f8bc9786 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -58,17 +58,16 @@ let get_lexbuf fn =
let parse_file (f : string) : Parse_ast.defs =
let lexbuf = get_lexbuf f in
- Parser.file Lexer.token lexbuf
-(* try
- Parser.file (Lexer.token []) lexbuf
+ try
+ Parser.file Lexer.token lexbuf
with
| Parsing.Parse_error ->
let pos = Lexing.lexeme_start_p lexbuf in
- raise "Parse error" (* (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos, "")))*)
- | Ast.Parse_error_locn(l,m) ->
- raise "Parse error 2" (*Reporting_basic.Fatal_error (Reporting_basic.Err_syntax_locn (l, m))*)
+ raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos, "")))
+ | Parse_ast.Parse_error_locn(l,m) ->
+ raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax_locn (l, m)))
| Lexer.LexError(c,p) ->
- raise "Lex error" (*Reporting_basic.Fatal_error (Reporting_basic.Err_lex (p, c))*)*)
+ raise (Reporting_basic.Fatal_error (Reporting_basic.Err_lex (p, c)))
(* type instances = Types.instance list Types.Pfmap.t
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 20:04:43 +0000