From: Stefano Zacchiroli Date: Thu, 5 Aug 2004 15:03:48 +0000 (+0000) Subject: ported location handling to camlp4 3.08 X-Git-Tag: V_0_6_3_2~2 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e3ce9e2940a9e9c736209517e20e4c4292fdd0c3;p=helm.git ported location handling to camlp4 3.08 --- diff --git a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml index 22c911eaf..ba70d2745 100644 --- 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 1b2ef3657..c64fcd42c 100644 --- 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> (* ≔ *); 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 93795f96e..02a51678b 100644 --- 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 4ba3541e5..dc15b8c8b 100644 --- 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 12d5ca1e8..470019835 100644 --- 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 f7392fa3a..fcc803697 100644 --- 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 ]