X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationParser.ml;h=bc33a815d89abfd5e57dcfb8ff710bd02fe241e5;hb=5a40de00f69847c247100b0bde4569cb4003e316;hp=ce90490052d0bb88e71cde8ec744a7089a77540f;hpb=31d7f139796d6597915cd430baf37552dc26511c;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml
index ce9049005..bc33a815d 100644
--- a/helm/ocaml/cic_notation/cicNotationParser.ml
+++ b/helm/ocaml/cic_notation/cicNotationParser.ml
@@ -60,50 +60,54 @@ let int_of_string s =
 GEXTEND Level1Parser
   GLOBAL: level1_pattern;
   level1_pattern: [ [ p = pattern -> () ] ];
-
   pattern: [ [ p = LIST1 simple_pattern -> () ] ];
-
   literal: [
     [ s = SYMBOL -> ()
     | k = KEYWORD -> ()
     ]
   ];
-
   sep:       [ [ SYMBOL "\\SEP";      sep = literal -> () ] ];
   row_sep:   [ [ SYMBOL "\\ROWSEP";   sep = literal -> () ] ];
   field_sep: [ [ SYMBOL "\\FIELDSEP"; sep = literal -> () ] ];
-
-  box_token: [
+  box_pattern: [
     [ SYMBOL "\\HBOX"; p = simple_pattern -> ()
     | SYMBOL "\\VBOX"; p = simple_pattern -> ()
     | SYMBOL "\\BREAK" -> ()
     ]
   ];
-
+  magic_pattern: [
+    [ SYMBOL "\\LIST0"; p = simple_pattern; sep = OPT sep -> ()
+    | SYMBOL "\\LIST1"; p = simple_pattern; sep = OPT sep -> ()
+    | SYMBOL "\\OPT"; p = simple_pattern -> ()
+    ]
+  ];
+  pattern_variable: [
+    [ id = IDENT -> ()
+    | SYMBOL "\\NUM"; id = IDENT -> ()
+    | SYMBOL "\\IDENT"; id = IDENT -> ()
+    ]
+  ];
   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 -> ()
+    [ "layout" LEFTA
+      [ p1 = SELF; SYMBOL "\\SUB"; p2 = SELF -> ()
+      | p1 = SELF; SYMBOL "\\SUP"; p2 = SELF -> ()
+      | p1 = SELF; SYMBOL "\\BELOW"; p2 = SELF -> ()
+      | p1 = SELF; SYMBOL "\\ABOVE"; p2 = SELF -> ()
+      | SYMBOL "["; p1 = pattern; SYMBOL "\\OVER"; p2 = pattern; SYMBOL "]" ->
+          ()
+      | SYMBOL "["; p1 = pattern; SYMBOL "\\ATOP"; p2 = pattern; SYMBOL "]" ->
+          ()
       | 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 "\\ROOT"; arg = pattern; SYMBOL "\\OF"; index = SELF -> ()
+      ]
+    | "simple" NONA
+      [ m = magic_pattern -> ()
+      | v = pattern_variable -> ()
+      | b = box_pattern -> ()
+      | n = NUMBER -> ()
       | SYMBOL "["; p = pattern; SYMBOL "]" -> ()
       ]
     ];
@@ -114,10 +118,120 @@ END
 GEXTEND Level2Parser
   GLOBAL: level2_pattern;
   level2_pattern: [ [ p = pattern -> () ] ];
-
-  pattern: [ [ a = ast -> () ] ];
-
-  ast: [ [ SYMBOL "\\FOO" -> () ] ];
+  sort: [
+    [ SYMBOL "\\PROP" -> ()
+    | SYMBOL "\\SET" -> ()
+    | SYMBOL "\\TYPE" -> ()
+    ]
+  ];
+  explicit_subst: [
+    [ (* TODO explicit substitution *)
+    ]
+  ];
+  meta_subst: [
+    [ (* TODO meta substitution *)
+    ]
+  ];
+  possibly_typed_name: [
+    [ SYMBOL "("; i = IDENT; SYMBOL ":"; typ = pattern; SYMBOL ")" -> ()
+    | i = IDENT -> ()
+    ]
+  ];
+  match_pattern: [
+    [ n = IDENT -> ()
+    | SYMBOL "("; head = IDENT; vars = LIST1 possibly_typed_name; SYMBOL ")" ->
+        ()
+    ]
+  ];
+  binder: [
+    [ SYMBOL <:unicode<Pi>>     (* Π *) -> ()
+    | SYMBOL <:unicode<exists>> (* ∃ *) -> ()
+    | SYMBOL <:unicode<forall>> (* ∀ *) -> ()
+    | SYMBOL <:unicode<lambda>> (* λ *) -> ()
+    ]
+  ];
+  bound_names: [
+    [ vars = LIST1 IDENT SEP SYMBOL ",";
+      typ = OPT [ SYMBOL ":"; p = pattern -> () ] -> ()
+    | LIST1 [
+        SYMBOL "("; vars = LIST1 IDENT SEP SYMBOL ",";
+        typ = OPT [ SYMBOL ":"; p = pattern -> () ]; SYMBOL ")" -> ()
+      ] ->
+        ()
+    ]
+  ];
+  induction_kind: [
+    [ IDENT "rec" -> ()
+    | IDENT "corec" -> ()
+    ]
+  ];
+  let_defs: [
+    [ defs = LIST1 [
+        name = IDENT; args = bound_names;
+        index_name = OPT [ IDENT "on"; idx = IDENT -> () ];
+        ty = OPT [ SYMBOL ":" ; p = pattern -> () ];
+        SYMBOL <:unicode<def>> (* ≝ *); body = pattern ->
+          ()
+      ] SEP IDENT "and" ->
+        ()
+    ]
+  ];
+  pattern_variable: [
+    [ SYMBOL "\\NUM"; id = IDENT -> ()
+    | SYMBOL "\\IDENT"; id = IDENT -> ()
+    | SYMBOL "\\FRESH"; id = IDENT -> ()
+    ]
+  ];
+  magic_pattern: [
+    [ SYMBOL "\\FOLD"; n = OPT NUMBER; [ IDENT "left" | IDENT "right" ];
+      LIST1 IDENT; SYMBOL "."; p1 = pattern;
+      OPT [ SYMBOL "\\LAMBDA"; LIST1 IDENT ]; p2 = pattern ->
+        ()
+    | SYMBOL "\\DEFAULT"; id = IDENT; p1 = pattern; p2 = pattern -> ()
+    ]
+  ];
+  pattern:
+    [ "letin" NONA
+      [ IDENT "let"; var = possibly_typed_name; SYMBOL <:unicode<def>> (* ≝ *);
+        p1 = pattern; "in"; p2 = pattern ->
+          ()
+      | IDENT "let"; k = induction_kind; defs = let_defs; IDENT "in";
+        body = pattern ->
+          ()
+      ]
+    | "binder" RIGHTA
+      [ b = binder; bound_names; SYMBOL "."; body = pattern -> () ]
+    | "extension"
+      [ ]
+    | "apply" LEFTA
+      [ p1 = pattern; p2 = pattern -> () ]
+    | "simple" NONA
+      [ i = IDENT -> ()
+      | i = IDENT; s = explicit_subst -> ()
+      | n = NUMBER -> ()
+      | IMPLICIT -> ()
+      | m = META -> ()
+      | m = META; s = meta_subst -> ()
+      | s = sort -> ()
+      | s = SYMBOL -> ()
+      | u = URI -> ()
+      | outtyp = OPT [ SYMBOL "["; typ = pattern; SYMBOL "]" ];
+        IDENT "match"; t = pattern;
+        indty_ident = OPT [ SYMBOL ":"; id = IDENT ];
+        IDENT "with"; SYMBOL "[";
+        patterns = LIST0 [
+          lhs = match_pattern; SYMBOL <:unicode<Rightarrow>> (* ⇒ *);
+          rhs = pattern ->
+            ()
+        ] SEP SYMBOL "|";
+        SYMBOL "]" ->
+          ()
+      | SYMBOL "("; p1 = pattern; SYMBOL ":"; p2 = pattern; SYMBOL ")" -> ()
+      | SYMBOL "("; p = pattern; SYMBOL ")" -> ()
+      | v = pattern_variable -> ()
+      | m = magic_pattern -> ()
+      ]
+    ];
 END
 (* }}} *)