snapshot, notably:

[helm.git] / helm / ocaml / cic_notation / cicNotationParser.ml

diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml
index 2b5598c42a0873b5c2fa2c420a6cb2529465144f..ce90490052d0bb88e71cde8ec744a7089a77540f 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationParser.ml
+++ b/helm/ocaml/cic_notation/cicNotationParser.ml
@@ -27,9 +27,22 @@ open Printf
 
 exception Parse_error of Token.flocation * string
 
-let grammar = Grammar.gcreate CicNotationLexer.level1_lexer
-
-let level1 = Grammar.Entry.create grammar "level1"
+module Level1Lexer =
+struct
+  type te = string * string
+  let lexer = CicNotationLexer.syntax_pattern_lexer
+end
+module Level1Parser = Grammar.GMake (Level1Lexer)
+
+module Level2Lexer =
+struct
+  type te = string * string
+  let lexer = CicNotationLexer.ast_pattern_lexer
+end
+module Level2Parser = Grammar.GMake (Level2Lexer)
+
+let level1_pattern = Level1Parser.Entry.create "level1_pattern"
+let level2_pattern = Level2Parser.Entry.create "level2_pattern"
 
 let return_term loc term = ()
 
@@ -43,10 +56,10 @@ let int_of_string s =
   with Failure _ ->
     failwith (sprintf "Lexer failure: string_of_int \"%s\" failed" s)
 
-EXTEND
-  GLOBAL: level1;
-
-  level1: [ [ p = pattern -> () ] ];
+(* {{{ Grammar for concrete syntax patterns, notation level 1 *)
+GEXTEND Level1Parser
+  GLOBAL: level1_pattern;
+  level1_pattern: [ [ p = pattern -> () ] ];
 
   pattern: [ [ p = LIST1 simple_pattern -> () ] ];
 
@@ -67,38 +80,46 @@ EXTEND
     ]
   ];
 
-  layout_schemata: [
-    [ SYMBOL "\\ARRAY"; p = simple_pattern; fsep = OPT field_sep;
-      rsep = OPT row_sep ->
-        ()
-    | SYMBOL "\\FRAC"; p1 = simple_pattern; p2 = simple_pattern -> ()
-    | SYMBOL "\\SQRT"; p = simple_pattern -> ()
-    | SYMBOL "\\ROOT"; p1 = simple_pattern; SYMBOL "\\OF";
-      p2 = simple_pattern ->
-        ()
-     (* TODO XXX many issues here:
-      * - "^^" is lexed as two "^" symbols
-      * - "a_b" is lexed as IDENT "a_b" *)
-    | p1 = simple_pattern; SYMBOL "^"; p2 = simple_pattern -> ()
-    | p1 = simple_pattern; SYMBOL "^"; SYMBOL "^"; p2 = simple_pattern -> ()
-    | p1 = simple_pattern; SYMBOL "_"; p2 = simple_pattern -> ()
-    | p1 = simple_pattern; SYMBOL "_"; SYMBOL "_"; p2 = simple_pattern -> ()
-    ]
-  ];
+  simple_pattern:
+    [ "infix" LEFTA
+       (* TODO XXX many issues here:
+        * - "^^" is lexed as two "^" symbols
+        * - "a_b" is lexed as IDENT "a_b" *)
+      [ p1 = SELF; SYMBOL "^"; p2 = SELF -> ()
+      | p1 = SELF; SYMBOL "^"; SYMBOL "^"; p2 = SELF -> ()
+      | p1 = SELF; SYMBOL "_"; p2 = SELF -> ()
+      | p1 = SELF; SYMBOL "_"; SYMBOL "_"; p2 = SELF -> ()
+      ]
+    | "simple" NONA
+      [ SYMBOL "\\LIST0"; p = SELF; sep = OPT sep -> ()
+      | SYMBOL "\\LIST1"; p = SELF; sep = OPT sep -> ()
+      | b = box_token -> ()
+      | id = IDENT -> ()
+      | SYMBOL "\\NUM"; id = IDENT -> ()
+      | SYMBOL "\\IDENT"; id = IDENT -> ()
+      | SYMBOL "\\OPT"; p = SELF -> ()
+      | SYMBOL "\\ARRAY"; p = SELF; fsep = OPT field_sep; rsep = OPT row_sep ->
+          ()
+      | SYMBOL "\\FRAC"; p1 = SELF; p2 = SELF -> ()
+      | SYMBOL "\\SQRT"; p = SELF -> ()
+      | SYMBOL "\\ROOT"; p1 = SELF; SYMBOL "\\OF"; p2 = SELF ->
+          ()
+      | SYMBOL "["; p = pattern; SYMBOL "]" -> ()
+      ]
+    ];
+END
+(* }}} *)
 
-  simple_pattern: [
-    [ SYMBOL "\\LIST0"; p = simple_pattern; sep = OPT sep -> ()
-    | SYMBOL "\\LIST1"; p = simple_pattern; sep = OPT sep -> ()
-    | b = box_token -> ()
-    | id = IDENT -> ()
-    | SYMBOL "\\NUM"; id = IDENT -> ()
-    | SYMBOL "\\IDENT"; id = IDENT -> ()
-    | SYMBOL "\\OPT"; p = simple_pattern -> ()
-    | l = layout_schemata -> ()
-    | SYMBOL "["; p = pattern; SYMBOL "]" -> ()
-    ]
-  ];
+(* {{{ Grammar for ast patterns, notation level 2 *)
+GEXTEND Level2Parser
+  GLOBAL: level2_pattern;
+  level2_pattern: [ [ p = pattern -> () ] ];
+
+  pattern: [ [ a = ast -> () ] ];
+
+  ast: [ [ SYMBOL "\\FOO" -> () ] ];
 END
+(* }}} *)
 
 let exc_located_wrapper f =
   try
@@ -109,7 +130,14 @@ let exc_located_wrapper f =
   | Stdpp.Exc_located (floc, exn) ->
       raise (Parse_error (floc, (Printexc.to_string exn)))
 
-let parse_level1_pattern stream =
-  exc_located_wrapper (fun () -> (Grammar.Entry.parse level1 stream))
+let parse_syntax_pattern stream =
+  exc_located_wrapper
+    (fun () ->
+      (Level1Parser.Entry.parse level1_pattern (Level1Parser.parsable stream)))
+
+let parse_ast_pattern stream =
+  exc_located_wrapper
+    (fun () ->
+      (Level2Parser.Entry.parse level2_pattern (Level2Parser.parsable stream)))
 
-(* vim:set encoding=utf8: *)
+(* vim:set encoding=utf8 foldmethod=marker: *)