* New implementation of localized exceptions

* Localized exceptions moved into the extlib

diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml
index 32b6b0a9068312564dcc8c65648b12892a6f4bc3..71cc2bffd6c4d1f919c77898436583ccfa3585ac 100644 (file)
--- 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 d614c68bca4b1dedd997677480fefe15ccf748bd..e25968bbbc4aa03cec62cda83aed3558086430e4 100644 (file)
--- 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 ac6a0edbd1a37a9e1684a4089b9fd8849a3e3342..d0310d0e57e6683e689f68cad961cf6aac08f230 100644 (file)
--- 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 cf2f7b1fce827425e78c96322a55c057a22d878e..e7c54213d8f64f1ebc29d7548e7ec75b7ed5e268 100644 (file)
--- 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 b3685232e8e96e3a898e6a361bc9dd940cb63601..0dc914156056bf7088234d5cf2d8a5c5c665fc2a 100644 (file)
--- 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 d05af7c02548f22cefbd6ba1b43d8dd4b067bbc4..c8df533ed43eaa80f4b9648e68ab206959042446 100644 (file)
--- 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 a76a5c76e8252dcb7eb734a7ca4a55122a2971d8..6afae34a79fd240f3be640bb209240330579a29c 100644 (file)
--- 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 40a1aca15d9daa00c435b5d1f6ec4554b4db4f57..a598ddb1a8cf34b258875d6f2ee3ab2497dbeb20 100644 (file)
--- 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