- enriched Parse_error exception with error location

[helm.git] / helm / ocaml / cic_disambiguation / cicTextualParser2.ml

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: *)