From 2007173e83a5001053c2946b59d6827cc080f1c4 Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 18 May 2005 13:11:50 +0000
Subject: [PATCH] snapshot (implemented level 3 grammar)

---
 helm/ocaml/cic_notation/cicNotationParser.ml  | 39 +++++++++++++++++++
 helm/ocaml/cic_notation/cicNotationParser.mli |  3 ++
 helm/ocaml/cic_notation/test_parser.ml        |  1 +
 3 files changed, 43 insertions(+)

diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml
index bc33a815d..5e94d20a0 100644
--- a/helm/ocaml/cic_notation/cicNotationParser.ml
+++ b/helm/ocaml/cic_notation/cicNotationParser.ml
@@ -41,8 +41,16 @@ struct
 end
 module Level2Parser = Grammar.GMake (Level2Lexer)
 
+module Level3Lexer =
+struct
+  type te = string * string
+  let lexer = CicNotationLexer.ast_pattern_lexer
+end
+module Level3Parser = Grammar.GMake (Level3Lexer)
+
 let level1_pattern = Level1Parser.Entry.create "level1_pattern"
 let level2_pattern = Level2Parser.Entry.create "level2_pattern"
+let level3_interpretation = Level3Parser.Entry.create "level3_interpretation"
 
 let return_term loc term = ()
 
@@ -235,6 +243,31 @@ GEXTEND Level2Parser
 END
 (* }}} *)
 
+(* {{{ Grammar for interpretation, notation level 3 *)
+GEXTEND Level3Parser
+  GLOBAL: level3_interpretation;
+  level3_interpretation: [ [ i = interpretation -> () ] ];
+  argument: [
+    [ i = IDENT -> ()
+    | SYMBOL <:unicode<eta>> (* η *); SYMBOL "."; a = SELF -> ()
+    | SYMBOL <:unicode<eta>> (* η *); i = IDENT; SYMBOL "."; a = SELF -> ()
+    ]
+  ];
+  term: [
+    [ u = URI -> ()
+    | a = argument -> ()
+    | SYMBOL "("; terms = LIST1 SELF; SYMBOL ")" -> ()
+    ]
+  ];
+  interpretation: [
+    [ IDENT "interpretation"; s = SYMBOL; args = LIST1 argument; IDENT "as";
+      t = term ->
+        ()
+    ]
+  ];
+END
+(* }}} *)
+
 let exc_located_wrapper f =
   try
     f ()
@@ -254,4 +287,10 @@ let parse_ast_pattern stream =
     (fun () ->
       (Level2Parser.Entry.parse level2_pattern (Level2Parser.parsable stream)))
 
+let parse_interpretation stream =
+  exc_located_wrapper
+    (fun () ->
+      (Level3Parser.Entry.parse level3_interpretation
+        (Level3Parser.parsable stream)))
+
 (* vim:set encoding=utf8 foldmethod=marker: *)
diff --git a/helm/ocaml/cic_notation/cicNotationParser.mli b/helm/ocaml/cic_notation/cicNotationParser.mli
index fab4d4102..669c8336c 100644
--- a/helm/ocaml/cic_notation/cicNotationParser.mli
+++ b/helm/ocaml/cic_notation/cicNotationParser.mli
@@ -33,3 +33,6 @@ val parse_syntax_pattern: char Stream.t -> unit
   (** AST pattern: notation level 2 *)
 val parse_ast_pattern: char Stream.t -> unit
 
+  (** interpretation: notation level 3 *)
+val parse_interpretation: char Stream.t -> unit
+
diff --git a/helm/ocaml/cic_notation/test_parser.ml b/helm/ocaml/cic_notation/test_parser.ml
index 61fd56d73..53ee4f8eb 100644
--- a/helm/ocaml/cic_notation/test_parser.ml
+++ b/helm/ocaml/cic_notation/test_parser.ml
@@ -39,6 +39,7 @@ let _ =
     match !level with
     | 1 -> CicNotationParser.parse_syntax_pattern
     | 2 -> CicNotationParser.parse_ast_pattern
+    | 3 -> CicNotationParser.parse_interpretation
     | _ -> Arg.usage arg_spec usage; exit 1
   in
   let ic = stdin in
-- 
2.39.2