From bc504bdaca501cd4d33f3240e01855988bc15b79 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 23 Nov 2005 22:28:21 +0000 Subject: [PATCH] * New implementation of localized exceptions * Localized exceptions moved into the extlib --- helm/ocaml/cic_notation/cicNotationParser.ml | 6 ++--- helm/ocaml/cic_notation/cicNotationParser.mli | 2 +- helm/ocaml/cic_notation/cicNotationPt.ml | 8 ++---- helm/ocaml/cic_notation/grafiteParser.ml | 25 +++++++++++-------- helm/ocaml/cic_notation/test_parser.ml | 6 ++--- helm/ocaml/extlib/Makefile | 2 +- helm/ocaml/extlib/hExtlib.ml | 17 +++++++++++++ helm/ocaml/extlib/hExtlib.mli | 7 ++++++ 8 files changed, 48 insertions(+), 25 deletions(-) diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml index 32b6b0a90..71cc2bffd 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.ml +++ b/helm/ocaml/cic_notation/cicNotationParser.ml @@ -28,7 +28,7 @@ open Printf module Ast = CicNotationPt module Env = CicNotationEnv -exception Parse_error of Token.flocation * string +exception Parse_error of string exception Level_not_found of int let level1_pattern_grammar = @@ -614,9 +614,9 @@ let exc_located_wrapper f = f () with | Stdpp.Exc_located (floc, Stream.Error msg) -> - raise (Parse_error (floc, msg)) + raise (HExtlib.Localized (floc, Parse_error msg)) | Stdpp.Exc_located (floc, exn) -> - raise (Parse_error (floc, (Printexc.to_string exn))) + raise (HExtlib.Localized (floc, (Parse_error (Printexc.to_string exn)))) let parse_level1_pattern lexbuf = exc_located_wrapper diff --git a/helm/ocaml/cic_notation/cicNotationParser.mli b/helm/ocaml/cic_notation/cicNotationParser.mli index d614c68bc..e25968bbb 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.mli +++ b/helm/ocaml/cic_notation/cicNotationParser.mli @@ -23,7 +23,7 @@ * http://helm.cs.unibo.it/ *) -exception Parse_error of Token.flocation * string +exception Parse_error of string exception Level_not_found of int (** {2 Parsing functions} *) diff --git a/helm/ocaml/cic_notation/cicNotationPt.ml b/helm/ocaml/cic_notation/cicNotationPt.ml index ac6a0edbd..d0310d0e5 100644 --- a/helm/ocaml/cic_notation/cicNotationPt.ml +++ b/helm/ocaml/cic_notation/cicNotationPt.ml @@ -30,13 +30,9 @@ type induction_kind = [ `Inductive | `CoInductive ] type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp ] type fold_kind = [ `Left | `Right ] -type location = Lexing.position * Lexing.position -(* cut and past from CicAst.loc_of_floc *) -let loc_of_floc = function - | { Lexing.pos_cnum = loc_begin }, { Lexing.pos_cnum = loc_end } -> - (loc_begin, loc_end) +type location = Token.flocation let fail floc msg = - let (x, y) = loc_of_floc floc in + let (x, y) = HExtlib.loc_of_floc floc in failwith (Printf.sprintf "Error at characters %d - %d: %s" x y msg) type href = UriManager.uri diff --git a/helm/ocaml/cic_notation/grafiteParser.ml b/helm/ocaml/cic_notation/grafiteParser.ml index cf2f7b1fc..e7c54213d 100644 --- a/helm/ocaml/cic_notation/grafiteParser.ml +++ b/helm/ocaml/cic_notation/grafiteParser.ml @@ -161,9 +161,9 @@ EXTEND | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec -> let (pt,_,_) = p in if pt <> None then - raise (CicNotationParser.Parse_error - (loc, "the pattern cannot specify the term to replace, only its" - ^ " paths in the hypotheses and in the conclusion")) + raise (HExtlib.Localized (loc, CicNotationParser.Parse_error + ("the pattern cannot specify the term to replace, only its" + ^ " paths in the hypotheses and in the conclusion"))) else GrafiteAst.Fold (loc, kind, t, p) | IDENT "fourier" -> @@ -203,8 +203,9 @@ EXTEND let (pt,_,_) = p in if pt <> None then raise - (CicNotationParser.Parse_error - (loc,"the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")) + (HExtlib.Localized (loc, + (CicNotationParser.Parse_error + "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion"))) else GrafiteAst.Rewrite (loc, d, t, p) | IDENT "right" -> @@ -350,10 +351,11 @@ EXTEND then GrafiteAst.Ident_alias (id, uri) else - raise (CicNotationParser.Parse_error (loc,sprintf "Not a valid uri: %s" uri)) + raise + (HExtlib.Localized (loc, CicNotationParser.Parse_error (sprintf "Not a valid uri: %s" uri))) else - raise (CicNotationParser.Parse_error (loc, - sprintf "Not a valid identifier: %s" id)) + raise (HExtlib.Localized (loc, CicNotationParser.Parse_error ( + sprintf "Not a valid identifier: %s" id))) | IDENT "symbol"; symbol = QSTRING; instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ]; SYMBOL "="; dsc = QSTRING -> @@ -493,7 +495,7 @@ EXTEND | IDENT "metadata"; [ IDENT "dependency" | IDENT "baseuri" ] ; URI -> (** metadata commands lives only in .moo, where they are in marshalled * form *) - raise (CicNotationParser.Parse_error (loc, "metadata not allowed here")) + raise (HExtlib.Localized (loc,CicNotationParser.Parse_error "metadata not allowed here")) | IDENT "dump" -> GrafiteAst.Dump loc | IDENT "render"; u = URI -> @@ -528,9 +530,10 @@ let exc_located_wrapper f = with | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file | Stdpp.Exc_located (floc, Stream.Error msg) -> - raise (CicNotationParser.Parse_error (floc, msg)) + raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg)) | Stdpp.Exc_located (floc, exn) -> - raise (CicNotationParser.Parse_error (floc, (Printexc.to_string exn))) + raise + (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn))) let parse_statement lexbuf = exc_located_wrapper diff --git a/helm/ocaml/cic_notation/test_parser.ml b/helm/ocaml/cic_notation/test_parser.ml index b3685232e..0dc914156 100644 --- a/helm/ocaml/cic_notation/test_parser.ml +++ b/helm/ocaml/cic_notation/test_parser.ml @@ -67,7 +67,7 @@ let process_stream istream = try let statement = GrafiteParser.parse_statement istream in let floc = extract_loc statement in - let (_, y) = P.loc_of_floc floc in + let (_, y) = HExtlib.loc_of_floc floc in char_count := y + !char_count; match statement with (* | G.Executable (_, G.Macro (_, G.Check (_, @@ -134,8 +134,8 @@ let process_stream istream = | _ -> prerr_endline "Unsupported statement" with | End_of_file -> raise End_of_file - | CicNotationParser.Parse_error (floc, msg) -> - let (x, y) = P.loc_of_floc floc in + | HExtlib.Localized (floc,CicNotationParser.Parse_error msg) -> + let (x, y) = HExtlib.loc_of_floc floc in (* let before = String.sub line 0 x in let error = String.sub line x (y - x) in let after = String.sub line y (String.length line - y) in diff --git a/helm/ocaml/extlib/Makefile b/helm/ocaml/extlib/Makefile index d05af7c02..c8df533ed 100644 --- a/helm/ocaml/extlib/Makefile +++ b/helm/ocaml/extlib/Makefile @@ -1,5 +1,5 @@ PACKAGE = extlib -REQUIRES = unix +REQUIRES = unix camlp4.gramlib PREDICATES = INTERFACE_FILES = \ diff --git a/helm/ocaml/extlib/hExtlib.ml b/helm/ocaml/extlib/hExtlib.ml index a76a5c76e..6afae34a7 100644 --- a/helm/ocaml/extlib/hExtlib.ml +++ b/helm/ocaml/extlib/hExtlib.ml @@ -282,3 +282,20 @@ let finally at_end f arg = at_end (); res +(** {2 Localized exceptions } *) + +exception Localized of Token.flocation * exn + +let loc_of_floc = function + | { Lexing.pos_cnum = loc_begin }, { Lexing.pos_cnum = loc_end } -> + (loc_begin, loc_end) + +let raise_localized_exception ~offset floc exn = + let (x, y) = loc_of_floc floc in + let x = offset + x in + let y = offset + y in + let flocb,floce = floc in + let floc = + { flocb with Lexing.pos_cnum = x }, { floce with Lexing.pos_cnum = y } + in + raise (Localized (floc, exn)) diff --git a/helm/ocaml/extlib/hExtlib.mli b/helm/ocaml/extlib/hExtlib.mli index 40a1aca15..a598ddb1a 100644 --- a/helm/ocaml/extlib/hExtlib.mli +++ b/helm/ocaml/extlib/hExtlib.mli @@ -77,3 +77,10 @@ type profiler = { profile : 'a 'b. ('a -> 'b) -> 'a -> 'b } val profile : ?enable:bool -> string -> profiler val set_profiling_printings : (unit -> bool) -> unit +(** {2 Localized exceptions } *) + +exception Localized of Token.flocation * exn + +val loc_of_floc: Token.flocation -> int * int + +val raise_localized_exception: offset:int -> Token.flocation -> exn -> 'a -- 2.39.2