split precedence level of binders: \lambda has higher precedence than others

this is the resulting precedences scheme:
  lambda > apply > infix operators > binders

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index b9cb4755b948a81dd24256f4003badf9efe96cab..d32302a131e11c2d67ce292c4744ec6e18d995c1 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -102,6 +102,13 @@ let ind_expansion uri =
   else
     uri
 
+let mk_binder_ast binder typ vars body =
+  List.fold_right
+    (fun var body ->
+       let name = name_of_string var in
+       CicAst.Binder (binder, (name, typ), body))
+    vars body
+
 EXTEND
   GLOBAL: term term0 tactic tactical tactical0 command script;
   int: [
@@ -115,12 +122,12 @@ EXTEND
     [ s = SYMBOL "_" -> None
     | t = term -> Some t ]
   ];
-  binder: [
-    [ SYMBOL <:unicode<lambda>> (* λ *) -> `Lambda
-    | SYMBOL <:unicode<Pi>>     (* Π *) -> `Pi
+  binder_low: [
+    [ SYMBOL <:unicode<Pi>>     (* Π *) -> `Pi
     | SYMBOL <:unicode<exists>> (* ∃ *) -> `Exists
     | SYMBOL <:unicode<forall>> (* ∀ *) -> `Forall ]
   ];
+  binder_high: [ [ SYMBOL <:unicode<lambda>> (* λ *) -> `Lambda ] ];
   sort: [
     [ "Prop" -> `Prop
     | "Set" -> `Set
@@ -214,6 +221,13 @@ EXTEND
       ] SEP "and" -> defs
     ]];
   constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
+  binder_vars: [
+      [ vars = LIST1 IDENT SEP SYMBOL ",";
+        typ = OPT [ SYMBOL ":"; t = term -> t ] -> (vars, typ)
+      | PAREN "("; vars = LIST1 IDENT SEP SYMBOL ",";
+        typ = OPT [ SYMBOL ":"; t = term -> t ]; PAREN ")" -> (vars, typ)
+      ]
+  ];
   term0: [ [ t = term; EOI -> return_term loc t ] ];
   term:
     [ "letin" NONA
@@ -225,6 +239,14 @@ EXTEND
         defs = let_defs; "in"; body = term ->
             return_term loc (CicAst.LetRec (ind_kind, defs, body))
       ]
+    | "binder" RIGHTA
+      [
+        b = binder_low; (vars, typ) = binder_vars; SYMBOL "."; body = term ->
+          let binder = mk_binder_ast b typ vars body in
+          return_term loc binder
+      | t1 = term; SYMBOL <:unicode<to>> (* → *); t2 = term ->
+          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 *) ]
@@ -246,25 +268,9 @@ EXTEND
       ]
     | "binder" RIGHTA
       [
-        b = binder;
-        (vars, typ) =
-          [ vars = LIST1 IDENT SEP SYMBOL ",";
-            typ = OPT [ SYMBOL ":"; t = term -> t ] -> (vars, typ)
-          | PAREN "("; vars = LIST1 IDENT SEP SYMBOL ",";
-            typ = OPT [ SYMBOL ":"; t = term -> t ]; PAREN ")" -> (vars, typ)
-          ];
-        SYMBOL "."; body = term ->
-          let binder =
-            List.fold_right
-              (fun var body ->
-                let name = name_of_string var in
-                CicAst.Binder (b, (name, typ), body))
-              vars body
-          in
+        b = binder_high; (vars, typ) = binder_vars; SYMBOL "."; body = term ->
+          let binder = mk_binder_ast b typ vars body in
           return_term loc binder
-      | t1 = term; SYMBOL <:unicode<to>> (* → *); t2 = term ->
-            return_term loc
-              (CicAst.Binder (`Pi, (Cic.Anonymous, Some t1), t2))
       ]
     | "simple" NONA
       [ sort = sort -> CicAst.Sort sort

diff --git a/helm/ocaml/cic_disambiguation/doc/precedence.txt b/helm/ocaml/cic_disambiguation/doc/precedence.txt
index 82e8d4ade3c431eada834f3b5ac9e8d4e1f6707a..f8de4d7a56b61a5a50ea37dff1aaba41dedac931 100644 (file)
--- a/helm/ocaml/cic_disambiguation/doc/precedence.txt
+++ b/helm/ocaml/cic_disambiguation/doc/precedence.txt
@@ -2,11 +2,14 @@
 Input                  Should be parsed as             Derived constraint
                                                        on precedence
 --------------------------------------------------------------------------------
-\lambda x.x y          ((\lambda x.x) y)               binder > apply
+\lambda x.x y          ((\lambda x.x) y)               lambda > apply
 S x = y                  (= (S x) y)                   apply  > infix operators
+\forall x.x=x         (\forall x.(= x x))             infix operators > binders
 --------------------------------------------------------------------------------
 
 Precedence total order:
 
-  binder > apply > infix operators
+  lambda > apply > infix operators > binders
+
+where binders are all binders except lambda (i.e. \forall, \pi, \exists)