From f71aafaaa510ad5e484560c5af47f4c4f6015219 Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Sat, 24 Jan 2004 12:32:04 +0000
Subject: [PATCH] split a term0 rule for dinamycally change top-level (i.e.
 non-recursive) term rul

---
 .../cic_disambiguation/cicTextualParser2.ml   | 32 +++++++++++--------
 .../cic_disambiguation/cicTextualParser2.mli  |  8 ++++-
 2 files changed, 25 insertions(+), 15 deletions(-)

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 0ac8ab380..030fa5938 100644
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -38,6 +38,7 @@ exception Parse_error of string
 let grammar = Grammar.gcreate CicTextualLexer2.lex
 
 let term = Grammar.Entry.create grammar "term"
+let term0 = Grammar.Entry.create grammar "term0"
 (* let tactic = Grammar.Entry.create grammar "tactic" *)
 (* let tactical = Grammar.Entry.create grammar "tactical" *)
 
@@ -48,7 +49,7 @@ let fail (x, y) msg =
   failwith (Printf.sprintf "Error at characters %d - %d: %s" x y msg)
 
 EXTEND
-  GLOBAL: term;
+  GLOBAL: term term0;
   meta_subst: [
     [ s = SYMBOL "_" -> None
     | t = term -> Some t ]
@@ -64,11 +65,11 @@ EXTEND
     [ s = [ IDENT | SYMBOL ];
       subst = OPT [
         SYMBOL "\subst";  (* to avoid catching frequent "a [1]" cases *)
-        LPAREN "[";
+        PAREN "[";
         substs = LIST1 [
           i = IDENT; SYMBOL <:unicode<Assign>> (* ≔ *); t = term -> (i, t)
         ] SEP SYMBOL ";";
-        RPAREN "]" ->
+        PAREN "]" ->
           substs
       ] ->
         (match subst with
@@ -81,8 +82,9 @@ EXTEND
   ];
   pattern: [
     [ n = name -> [n]
-    | LPAREN "("; names = LIST1 name; RPAREN ")" -> names ]
+    | PAREN "("; names = LIST1 name; PAREN ")" -> names ]
   ];
+  term0: [ [ t = term -> return_term loc t ] ];
   term:
     [ "arrow" RIGHTA
       [ t1 = term; SYMBOL <:unicode<to>>; t2 = term ->
@@ -118,12 +120,12 @@ EXTEND
         ] ->
           CicTextualParser2Ast.Sort sort_kind
       | n = substituted_name -> return_term loc n
-      | LPAREN "("; head = term; args = LIST1 term; RPAREN ")" ->
+      | PAREN "("; head = term; args = LIST1 term; PAREN ")" ->
           return_term loc (CicTextualParser2Ast.Appl (head :: args))
       | i = NUM -> return_term loc (CicTextualParser2Ast.Num (i, 0))
       | m = META;
         substs = [
-          LPAREN "["; substs = LIST0 meta_subst SEP SYMBOL ";" ; RPAREN "]" ->
+          PAREN "["; substs = LIST0 meta_subst SEP SYMBOL ";" ; PAREN "]" ->
             substs
         ] ->
             let index =
@@ -141,7 +143,7 @@ EXTEND
       | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
           defs = LIST1 [
           name = IDENT;
-          index = OPT [ LPAREN "("; index = INT; RPAREN ")" ->
+          index = OPT [ PAREN "("; index = INT; PAREN ")" ->
             int_of_string index
           ];
           typ = OPT [ SYMBOL ":"; typ = term -> typ ];
@@ -150,24 +152,26 @@ EXTEND
         ] SEP (IDENT "and");
         IDENT "in"; body = term ->
           return_term loc (CicTextualParser2Ast.LetRec (ind_kind, defs, body))
-      | outtyp = OPT [ LPAREN "["; typ = term; RPAREN "]" -> typ ];
+      | outtyp = OPT [ PAREN "["; typ = term; PAREN "]" -> typ ];
         "match"; t = term;
         SYMBOL ":"; indty = IDENT;
         "with";
-        LPAREN "[";
+        PAREN "[";
         patterns = LIST0 [
-          p = pattern; SYMBOL <:unicode<Rightarrow>> (* ⇒ *); t = term -> (p, t)
+          p = pattern; SYMBOL <:unicode<Rightarrow>> (* ⇒ *); t = term ->
+            (p, t)
         ] SEP SYMBOL "|";
-        RPAREN "]" ->
-          return_term loc (CicTextualParser2Ast.Case (t, indty, outtyp, patterns))
-      | LPAREN "("; t = term; RPAREN ")" -> return_term loc t
+        PAREN "]" ->
+          return_term loc
+            (CicTextualParser2Ast.Case (t, indty, outtyp, patterns))
+      | PAREN "("; t = term; PAREN ")" -> return_term loc t
       ]
     ];
 END
 
 let parse_term stream =
   try
-    Grammar.Entry.parse term stream
+    Grammar.Entry.parse term0 stream
   with Stdpp.Exc_located ((x, y), exn) ->
     raise (Parse_error (sprintf "parse error at characters %d-%d: %s" x y
         (Printexc.to_string exn)))
diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.mli b/helm/ocaml/cic_disambiguation/cicTextualParser2.mli
index 0d600cc20..a2b225143 100644
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.mli
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.mli
@@ -31,9 +31,15 @@ val parse_term: char Stream.t -> CicTextualParser2Ast.term
 
 (** {2 Grammar extensions} *)
 
+  (** recursive rule *)
 val term: CicTextualParser2Ast.term Grammar.Entry.e
 
-val return_term: CicTextualParser2Ast.location -> CicTextualParser2Ast.term -> CicTextualParser2Ast.term
+  (** top level rule *)
+val term0: CicTextualParser2Ast.term Grammar.Entry.e
+
+val return_term:
+  CicTextualParser2Ast.location -> CicTextualParser2Ast.term ->
+    CicTextualParser2Ast.term
 
   (** raise a parse error *)
 val fail: CicTextualParser2Ast.location -> string -> 'a
-- 
2.39.2