From 78c95f6f3ed42633c4b2cbf62b816538d4208d7c Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 9 Dec 2004 15:18:30 +0000 Subject: [PATCH] - enriched Parse_error exception with error location - first implementation of inductive type definitions (not yet completed: mutual inductive definition are still missing) - test parser now displays error location using ASCII escape coloring --- .../cic_disambiguation/cicTextualParser2.ml | 48 +++++++++++-------- .../cic_disambiguation/cicTextualParser2.mli | 2 +- helm/ocaml/cic_disambiguation/test_parser.ml | 19 ++++---- 3 files changed, 41 insertions(+), 28 deletions(-) diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index fddf27e99..a1f431b60 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -38,7 +38,7 @@ let use_fresh_num_instances = false open Printf open DisambiguateTypes -exception Parse_error of string +exception Parse_error of Token.flocation * string let fresh_num_instance = let n = ref 0 in @@ -83,10 +83,7 @@ EXTEND [ num = NUM -> try int_of_string num - with Failure _ -> - let (x, y) = CicAst.loc_of_floc loc in - raise (Parse_error (sprintf - "integer literal expected at characters %d-%d" x y)) + with Failure _ -> raise (Parse_error (loc, "integer literal expected")) ] ]; meta_subst: [ @@ -134,6 +131,7 @@ EXTEND (head, vars) ] ]; + constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ]; term0: [ [ t = term; EOI -> return_term loc t ] ]; term: [ "letin" NONA @@ -377,6 +375,21 @@ EXTEND | flavour = theorem_flavour; name = OPT IDENT; SYMBOL ":"; typ = term; body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> return_command loc (TacticAst.Theorem (flavour, name, typ, body)) + | [ IDENT "inductive" | IDENT "Inductive" ]; fst_name = IDENT; + params = LIST0 [ + PAREN "("; names = LIST1 IDENT SEP SYMBOL ","; SYMBOL ":"; + typ = term; PAREN ")" -> (names, typ) ]; + SYMBOL ":"; fst_typ = term; SYMBOL <:unicode>; OPT SYMBOL "|"; + fst_constructors = LIST0 constructor SEP SYMBOL "|" -> + let params = + List.fold_right + (fun (names, typ) acc -> + (List.map (fun name -> (name, typ)) names) @ acc) + params [] + in + let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in + let ind_types = [fst_ind_type] in + return_command loc (TacticAst.Inductive (params, ind_types)) | [ IDENT "goal" | IDENT "Goal" ]; typ = term; body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> return_command loc (TacticAst.Theorem (`Goal, None, typ, body)) @@ -394,18 +407,19 @@ END let exc_located_wrapper f = try - Lazy.force f - 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))) + f () + with + | Stdpp.Exc_located (floc, Stream.Error msg) -> + raise (Parse_error (floc, msg)) + | Stdpp.Exc_located (floc, exn) -> + raise (Parse_error (floc, (Printexc.to_string exn))) let parse_term stream = - exc_located_wrapper (lazy (Grammar.Entry.parse term0 stream)) + exc_located_wrapper (fun () -> (Grammar.Entry.parse term0 stream)) let parse_tactic stream = - exc_located_wrapper (lazy (Grammar.Entry.parse tactic stream)) + exc_located_wrapper (fun () -> (Grammar.Entry.parse tactic stream)) let parse_tactical stream = - exc_located_wrapper (lazy (Grammar.Entry.parse tactical0 stream)) + exc_located_wrapper (fun () -> (Grammar.Entry.parse tactical0 stream)) (**/**) @@ -471,12 +485,8 @@ module EnvironmentP3 = if s = empty then Environment.empty else - try - Grammar.Entry.parse aliases (Stream.of_string s) - 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))) + exc_located_wrapper + (fun () -> Grammar.Entry.parse aliases (Stream.of_string s)) end (* vim:set encoding=utf8: *) diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.mli b/helm/ocaml/cic_disambiguation/cicTextualParser2.mli index 351d929e2..9ed3bdefc 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.mli +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.mli @@ -23,7 +23,7 @@ * http://helm.cs.unibo.it/ *) -exception Parse_error of string +exception Parse_error of Token.flocation * string (** {2 Parsing functions} *) diff --git a/helm/ocaml/cic_disambiguation/test_parser.ml b/helm/ocaml/cic_disambiguation/test_parser.ml index 4ee8ec6ef..51a0d911f 100644 --- a/helm/ocaml/cic_disambiguation/test_parser.ml +++ b/helm/ocaml/cic_disambiguation/test_parser.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +open Printf + let pp_tactical = TacticAst2Box.tacticalPp let mode = @@ -41,9 +43,9 @@ let _ = let ic = stdin in try while true do + let line = input_line ic in + let istream = Stream.of_string line in try - let line = input_line ic in - let istream = Stream.of_string line in (match mode with | `Term -> let term = CicTextualParser2.parse_term istream in @@ -59,12 +61,13 @@ let _ = print_endline (CicTextualParser2.EnvironmentP3.to_string env)); flush stdout with - | CicTextualParser2.Parse_error msg -> prerr_endline msg -(* - | Stdpp.Exc_located ((p_start, p_end), exn) -> - prerr_endline (Printf.sprintf "Exception at character %d-%d: %s" - p_start p_end (Printexc.to_string exn)) -*) + | CicTextualParser2.Parse_error (floc, msg) -> + let (x, y) = CicAst.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 + eprintf "%s%s%s\n" before error after; + prerr_endline (sprintf "at character %d-%d: %s" x y msg) done with End_of_file -> close_in ic -- 2.39.2