- 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 53559bcd298e8cb80a7be1fc7a9cd62d5381fafc..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
@@ -240,9 +238,9 @@ EXTEND
     [ PAREN "["; idents = LIST1 IDENT SEP SYMBOL ";"; PAREN "]" -> idents ]
   ];
   reduction_kind: [
-    [ "reduce" -> `Reduce
-    | "simpl" -> `Simpl
-    | "whd" -> `Whd ]
+    [ [ IDENT "reduce" | IDENT "Reduce" ] -> `Reduce
+    | [ IDENT "simplify" | IDENT "Simplify" ] -> `Simpl
+    | [ IDENT "whd" | IDENT "Whd" ] -> `Whd ]
   ];
   tactic: [
     [ [ IDENT "absurd" | IDENT "Absurd" ]; t = tactic_term ->
@@ -296,7 +294,20 @@ EXTEND
     | [ "let" | "Let" ];
       t = tactic_term; "in"; where = IDENT ->
         return_tactic loc (TacticAst.LetIn (t, where))
-    (* TODO Reduce *)
+    | kind = reduction_kind;
+      pat = OPT [
+        "in"; pat = [ IDENT "goal" -> `Goal | IDENT "hyp" -> `Everywhere ] ->
+          pat
+      ];
+      terms = LIST0 term SEP SYMBOL "," ->
+        let tac =
+          (match (pat, terms) with
+          | None, [] -> TacticAst.Reduce (kind, None)
+          | None, terms -> TacticAst.Reduce (kind, Some (terms, `Goal))
+          | Some pat, [] -> TacticAst.Reduce (kind, Some ([], pat))
+          | Some pat, terms -> TacticAst.Reduce (kind, Some (terms, pat)))
+        in
+        return_tactic loc tac
     | [ IDENT "reflexivity" | IDENT "Reflexivity" ] ->
         return_tactic loc TacticAst.Reflexivity
     | [ IDENT "replace" | IDENT "Replace" ];
@@ -314,7 +325,7 @@ EXTEND
         return_tactic loc (TacticAst.Transitivity t)
     ]
   ];
-  tactical0: [ [ t = tactical; SYMBOL ";;" -> t ] ];
+  tactical0: [ [ t = tactical; SYMBOL ";;" -> return_tactical loc t ] ];
   tactical:
     [ "command" NONA
       [ cmd = command -> return_tactical loc (TacticAst.Command cmd) ]
@@ -364,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))
@@ -371,6 +397,8 @@ EXTEND
         return_command loc (TacticAst.Undo (int_opt steps))
     | [ IDENT "redo"   | IDENT "Redo" ]; steps = OPT NUM ->
         return_command loc (TacticAst.Redo (int_opt steps))
+    | [ IDENT "baseuri"   | IDENT "Baseuri" ]; uri = OPT QSTRING ->
+        return_command loc (TacticAst.Baseuri uri)
     | [ IDENT "check"   | IDENT "Check" ]; t = term ->
         return_command loc (TacticAst.Check t)
     ]
@@ -379,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))
 
 (**/**)
 
@@ -456,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: *)