handled difference associativity for the same level of the extensible grammar

[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 041010649b26a11b76871a71369a5fe695b57003..85b89451118d4cdf8cf923a4f9b2fbe7b242e916 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationParser.ml
+++ b/helm/ocaml/cic_notation/cicNotationParser.ml
@@ -38,7 +38,6 @@ let level2_meta_grammar = Grammar.gcreate CicNotationLexer.level2_meta_lexer
 
 let min_precedence = 0
 let max_precedence = 100
-let default_precedence = 50
 
 let level1_pattern =
   Grammar.Entry.create level1_pattern_grammar "level1_pattern"
@@ -211,30 +210,34 @@ let extract_term_production pattern =
   in
   aux pattern
 
-let level_of_int precedence =
+let level_of precedence associativity =
   if precedence < min_precedence || precedence > max_precedence then
     raise (Level_not_found precedence);
-  string_of_int precedence
+  let assoc_string =
+    match associativity with
+    | Gramext.NonA -> "N"
+    | Gramext.LeftA -> "L"
+    | Gramext.RightA -> "R"
+  in
+  string_of_int precedence ^ assoc_string
 
 type rule_id = Token.t Gramext.g_symbol list
 
   (* mapping: rule_id -> owned keywords. (rule_id, string list) Hashtbl.t *)
 let owned_keywords = Hashtbl.create 23
 
-let extend level1_pattern ?(precedence = default_precedence)
-  ?associativity action
-=
+let extend level1_pattern ~precedence ~associativity action =
   let p_bindings, p_atoms =
     List.split (extract_term_production level1_pattern)
   in
-  let level = level_of_int precedence in
+  let level = level_of precedence associativity in
   let p_names = flatten_opt p_bindings in
   let _ =
     Grammar.extend
       [ Grammar.Entry.obj (term: 'a Grammar.Entry.e),
         Some (Gramext.Level level),
         [ None,
-          associativity,
+          Some associativity,
           [ p_atoms, 
             (make_action
               (fun (env: CicNotationEnv.t) (loc: location) -> (action env loc))
@@ -276,7 +279,13 @@ let _ = (* create empty precedence level for "term" *)
   let mk_level_list first last =
     let rec aux acc = function
       | i when i < first -> acc
-      | i -> aux ((Some (string_of_int i), None, []) :: acc) (i - 1)
+      | i ->
+          aux
+            ((Some (string_of_int i ^ "N"), Some Gramext.NonA, [])
+             :: (Some (string_of_int i ^ "L"), Some Gramext.LeftA, [])
+             :: (Some (string_of_int i ^ "R"), Some Gramext.RightA, [])
+             :: acc)
+            (i - 1)
     in
     aux [] last
   in
@@ -356,7 +365,7 @@ EXTEND
   END
 (* }}} *)
 
-
+(* {{{ Grammar for ast magics, notation level 2 *)
 EXTEND
   GLOBAL: level2_meta;
   l2_variable: [
@@ -387,10 +396,11 @@ EXTEND
     ]
   ];
 END
+(* }}} *)
 
+(* {{{ Grammar for ast patterns, notation level 2 *)
 EXTEND
   GLOBAL: level2_ast term let_defs;
-(* {{{ Grammar for ast patterns, notation level 2 *)
   level2_ast: [ [ p = term -> p ] ];
   sort: [
     [ "Prop" -> `Prop
@@ -513,24 +523,23 @@ EXTEND
       RPAREN -> (vars, typ)
     ]
   ];
-  term: LEVEL "10"  (* let in *)
-    [ "10" NONA
-      [ "let"; var = possibly_typed_name; SYMBOL <:unicode<def>> (* ≝ *);
-        p1 = term; "in"; p2 = term ->
-          return_term loc (LetIn (var, p1, p2))
-      | "let"; k = induction_kind; defs = let_defs; "in";
-        body = term ->
-          return_term loc (LetRec (k, defs, body))
-      ]
-    ];
-  term: LEVEL "20"  (* binder *)
-    [ "20" RIGHTA
+  term: LEVEL "10N" [ (* let in *)
+    [ "let"; var = possibly_typed_name; SYMBOL <:unicode<def>> (* ≝ *);
+      p1 = term; "in"; p2 = term ->
+        return_term loc (LetIn (var, p1, p2))
+    | "let"; k = induction_kind; defs = let_defs; "in";
+      body = term ->
+        return_term loc (LetRec (k, defs, body))
+    ]
+  ];
+  term: LEVEL "20R"  (* binder *)
+    [
       [ b = binder; (vars, typ) = binder_vars; SYMBOL "."; body = term ->
           return_term loc (fold_cluster b vars typ body)
       ]
     ];
-  term: LEVEL "70"  (* apply *)
-    [ "70" LEFTA
+  term: LEVEL "70L"  (* apply *)
+    [
       [ p1 = term; p2 = term ->
           let rec aux = function
             | Appl (hd :: tl)
@@ -541,8 +550,8 @@ EXTEND
           return_term loc (Appl (aux p1 @ [p2]))
       ]
     ];
-  term: LEVEL "90"  (* simple *)
-    [ "90" NONA
+  term: LEVEL "90N"  (* simple *)
+    [
       [ id = IDENT -> return_term loc (Ident (id, None))
       | id = IDENT; s = explicit_subst -> return_term loc (Ident (id, Some s))
       | s = CSYMBOL -> return_term loc (Symbol (s, 0))
@@ -570,8 +579,8 @@ EXTEND
       | blob = UNPARSED_META -> !parse_level2_meta_ref (Stream.of_string blob)
       ]
     ];
-(* }}} *)
 END
+(* }}} *)
 
 (** {2 API implementation} *)