ported location handling to camlp4 3.08

diff --git a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml
index 22c911eaf5b543e16bb7b1a35d21b3a758eee43c..ba70d2745c8f73126733eff03c32664e15a1fc75 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml
@@ -58,7 +58,15 @@ let error lexbuf msg =
 let error_at_end lexbuf msg =
   raise (Error (Ulexing.lexeme_end lexbuf, Ulexing.lexeme_end lexbuf, msg))
 
-let return lexbuf token = (token, Ulexing.loc lexbuf)
+let return lexbuf token =
+  let flocation_begin =
+    { Lexing.pos_fname = ""; Lexing.pos_lnum = -1; Lexing.pos_bol = -1;
+      Lexing.pos_cnum = Ulexing.lexeme_start lexbuf }
+  in
+  let flocation_end =
+    { flocation_begin with Lexing.pos_cnum = Ulexing.lexeme_end lexbuf }
+  in
+  (token, (flocation_begin, flocation_end))
 
 (*
 let parse_ext_ident ident =
@@ -119,7 +127,7 @@ let rec token = lexer
 
 let tok_func stream =
   let lexbuf = Ulexing.from_utf8_stream stream in
-  Token.make_stream_and_location
+  Token.make_stream_and_flocation
     (fun () ->
       try
        token lexbuf

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 1b2ef365730c6310ac89997b711eb98f92f81af9..c64fcd42cb96faad16d4efb759b3fcb52324ffe1 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -65,7 +65,8 @@ let return_tactic loc tactic = TacticAst.LocatedTactic (loc, tactic)
 let return_tactical loc tactical = TacticAst.LocatedTactical (loc, tactical)
 let return_command loc cmd = cmd
 
-let fail (x, y) msg =
+let fail floc msg =
+  let (x, y) = CicAst.loc_of_floc floc in
   failwith (Printf.sprintf "Error at characters %d - %d: %s" x y msg)
 
 let name_of_string = function
@@ -79,7 +80,7 @@ EXTEND
         try
           int_of_string num
         with Failure _ ->
-          let (x, y) = loc in
+          let (x, y) = CicAst.loc_of_floc loc in
           raise (Parse_error (sprintf
             "integer literal expected at characters %d-%d" x y))
     ]
@@ -109,7 +110,7 @@ EXTEND
   substituted_name: [ (* a subs.name is an explicit substitution subject *)
     [ s = [ IDENT | SYMBOL ];
       subst = OPT [
-        SYMBOL "\subst";  (* to avoid catching frequent "a [1]" cases *)
+        SYMBOL "\\subst";  (* to avoid catching frequent "a [1]" cases *)
         PAREN "[";
         substs = LIST1 [
           i = IDENT; SYMBOL <:unicode<Assign>> (* ≔ *); t = term -> (i, t)
@@ -362,7 +363,8 @@ END
 let exc_located_wrapper f =
   try
     Lazy.force f
-  with Stdpp.Exc_located ((x, y), exn) ->
+  with Stdpp.Exc_located (floc, exn) ->
+    let (x, y) = CicAst.loc_of_floc floc in
     raise (Parse_error (sprintf "parse error at characters %d-%d: %s" x y
         (Printexc.to_string exn)))
 
@@ -439,7 +441,8 @@ module EnvironmentP3 =
       else
         try
           Grammar.Entry.parse aliases (Stream.of_string s)
-        with Stdpp.Exc_located ((x, y), exn) ->
+        with Stdpp.Exc_located (floc, exn) ->
+          let (x, y) = CicAst.loc_of_floc floc in
           raise (Parse_error (sprintf "parse error at characters %d-%d: %s" x y
           (Printexc.to_string exn)))
   end

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 93795f96ebb780eba031192d03ac15a16561a774..02a51678b070429c89b9d6abbf4e15a7c3b4885f 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -286,7 +286,7 @@ let interpretate ~context ~env ast =
   in
   match ast with
   | CicAst.AttributedTerm (`Loc loc, term) -> aux loc context term
-  | term -> aux (-1, -1) context term
+  | term -> aux CicAst.dummy_floc context term
 
 let domain_of_term ~context ast =
     (* "aux" keeps domain in reverse order and doesn't care about duplicates.
@@ -400,8 +400,7 @@ let domain_of_term ~context ast =
   rev_uniq
     (match ast with
     | CicAst.AttributedTerm (`Loc loc, term) -> aux loc context term
-    | term -> aux (-1, -1) context term)
-
+    | term -> aux CicAst.dummy_floc context term)
 
   (* dom1 \ dom2 *)
 let domain_diff dom1 dom2 =

diff --git a/helm/ocaml/cic_disambiguation/pa_unicode_macro.ml b/helm/ocaml/cic_disambiguation/pa_unicode_macro.ml
index 4ba3541e5653cea8f25f0f95ec80dc633a080f3a..dc15b8c8b2a264b7bd37783df30a0580528e9a8b 100644 (file)
--- a/helm/ocaml/cic_disambiguation/pa_unicode_macro.ml
+++ b/helm/ocaml/cic_disambiguation/pa_unicode_macro.ml
@@ -26,7 +26,12 @@
 let debug = false
 let debug_print s = if debug then prerr_endline s
 
-let loc = (0, 0)
+let loc =
+  let dummy_pos =
+    { Lexing.pos_fname = ""; Lexing.pos_lnum = -1; Lexing.pos_bol = -1;
+      Lexing.pos_cnum = -1 }
+  in
+  (dummy_pos, dummy_pos)
 
 let expand_unicode_macro macro =
   debug_print (Printf.sprintf "Expanding macro '%s' ..." macro);

diff --git a/helm/ocaml/cic_transformations/ast2pres.ml b/helm/ocaml/cic_transformations/ast2pres.ml
index 12d5ca1e8e0954ee9964eefeb0921dd74c00960f..470019835472be0a7880294d36f4c4a0e5163b59 100644 (file)
--- a/helm/ocaml/cic_transformations/ast2pres.ml
+++ b/helm/ocaml/cic_transformations/ast2pres.ml
@@ -100,7 +100,8 @@ let is_big t =
 
 let map_attribute =
   function
-      `Loc (n,m) -> 
+      `Loc floc -> 
+        let (n, m) = CicAst.loc_of_floc floc in
         (Some "helm","loc",(string_of_int n)^" "^(string_of_int m))
     | `IdRef s -> 
         (Some "helm","xref",s)

diff --git a/helm/ocaml/cic_transformations/cicAst.ml b/helm/ocaml/cic_transformations/cicAst.ml
index f7392fa3ac34bdfe8c4423902cd54a4c4c15fb06..fcc80369794c375c8bbe0b8d825d8cece1f2b701 100644 (file)
--- a/helm/ocaml/cic_transformations/cicAst.ml
+++ b/helm/ocaml/cic_transformations/cicAst.ml
@@ -23,7 +23,28 @@
  * http://helm.cs.unibo.it/
  *)
 
-type location = int * int
+(** {2 Parsing related types} *)
+
+type location = Lexing.position * Lexing.position
+
+  (* maps old style (i.e. <= 3.07) lexer location to new style location, padding
+  * with dummy values where needed *)
+let floc_of_loc (loc_begin, loc_end) =
+  let floc_begin =
+    { Lexing.pos_fname = ""; Lexing.pos_lnum = -1; Lexing.pos_bol = -1;
+      Lexing.pos_cnum = loc_begin }
+  in
+  let floc_end = { floc_begin with Lexing.pos_cnum = loc_end } in
+  (floc_begin, floc_end)
+
+  (* the other way round *)
+let loc_of_floc = function
+  | { Lexing.pos_cnum = loc_begin }, { Lexing.pos_cnum = loc_end } ->
+      (loc_begin, loc_end)
+
+let dummy_floc = floc_of_loc (-1, -1)
+
+(** {2 Cic Ast} *)
 
 type binder_kind = [ `Lambda | `Pi | `Exists | `Forall ]
 type induction_kind = [ `Inductive | `CoInductive ]