snapshot (implemented level 3 grammar)

diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml
index bc33a815d89abfd5e57dcfb8ff710bd02fe241e5..5e94d20a08f0510ba0645c3d4141cf76d5aa10cb 100644 (file)
--- 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 fab4d4102b9e7b1416e3a52f8368e20ec4b5b30f..669c8336ca1dc48180e5a162c635223ab61aab2c 100644 (file)
--- 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 61fd56d73196b90071aa427c59931d5fc8888ca2..53ee4f8eb268a7c8f7829a637ab6e7a7e4dabb51 100644 (file)
--- 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