- 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

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index fddf27e9995a100f72df291fcc478def9cf601fd..a1f431b60ef1e6f137e1b040b5eb080e637b7613 100644 (file)
--- 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<def>> (* ≝ *); 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<def>>; 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<def>> (* ≝ *); 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 351d929e27e75fafb8404c9e0f62842fcb09a42b..9ed3bdefcabef9024a7b556a2ba49ce7c13c48be 100644 (file)
--- 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 4ee8ec6ef1340c757cc2639bd44a9dac10ce9c2c..51a0d911f23ada0464480b5af8749ca441697102 100644 (file)
--- 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\e[01;31m%s\e[00m%s\n" before error after;
+          prerr_endline (sprintf "at character %d-%d: %s" x y msg)
     done
   with End_of_file ->
     close_in ic