(hopefully) final decision on precedence levels:

  binder > apply > infix operators

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 44587104554a7955fcd0bab31da800b232cf8036..b9cb4755b948a81dd24256f4003badf9efe96cab 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -225,6 +225,17 @@ EXTEND
         defs = let_defs; "in"; body = term ->
             return_term loc (CicAst.LetRec (ind_kind, defs, body))
       ]
+    | "logic_add" LEFTA   [ (* nothing here by default *) ]
+    | "logic_mult" LEFTA  [ (* nothing here by default *) ]
+    | "logic_inv" NONA    [ (* nothing here by default *) ]
+    | "relop" LEFTA
+      [ t1 = term; SYMBOL "="; t2 = term ->
+        return_term loc (CicAst.Appl [CicAst.Symbol ("eq", 0); t1; t2])
+      ]
+    | "add" LEFTA     [ (* nothing here by default *) ]
+    | "mult" LEFTA    [ (* nothing here by default *) ]
+    | "power" LEFTA   [ (* nothing here by default *) ]
+    | "inv" NONA      [ (* nothing here by default *) ]
     | "apply" LEFTA
       [ t1 = term; t2 = term ->
         let rec aux = function
@@ -255,17 +266,6 @@ EXTEND
             return_term loc
               (CicAst.Binder (`Pi, (Cic.Anonymous, Some t1), t2))
       ]
-    | "logic_add" LEFTA   [ (* nothing here by default *) ]
-    | "logic_mult" LEFTA  [ (* nothing here by default *) ]
-    | "logic_inv" NONA    [ (* nothing here by default *) ]
-    | "relop" LEFTA
-      [ t1 = term; SYMBOL "="; t2 = term ->
-        return_term loc (CicAst.Appl [CicAst.Symbol ("eq", 0); t1; t2])
-      ]
-    | "add" LEFTA     [ (* nothing here by default *) ]
-    | "mult" LEFTA    [ (* nothing here by default *) ]
-    | "power" LEFTA   [ (* nothing here by default *) ]
-    | "inv" NONA      [ (* nothing here by default *) ]
     | "simple" NONA
       [ sort = sort -> CicAst.Sort sort
       | n = substituted_name -> return_term loc n

diff --git a/helm/ocaml/cic_disambiguation/doc/precedence.txt b/helm/ocaml/cic_disambiguation/doc/precedence.txt
new file mode 100644 (file)
index 0000000..82e8d4a
--- /dev/null
+++ b/helm/ocaml/cic_disambiguation/doc/precedence.txt
@@ -0,0 +1,12 @@
+
+Input                  Should be parsed as             Derived constraint
+                                                       on precedence
+--------------------------------------------------------------------------------
+\lambda x.x y          ((\lambda x.x) y)               binder > apply
+S x = y                  (= (S x) y)                   apply  > infix operators
+--------------------------------------------------------------------------------
+
+Precedence total order:
+
+  binder > apply > infix operators
+