From a611291b68a2f9a0c627de0cdabf8f7448136bcf Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 21 Apr 2005 12:54:31 +0000
Subject: [PATCH] split precedence level of binders: \lambda has higher
 precedence than others this is the resulting precedences scheme:   lambda >
 apply > infix operators > binders

---
 .../cic_disambiguation/cicTextualParser2.ml   | 48 +++++++++++--------
 .../cic_disambiguation/doc/precedence.txt     |  7 ++-
 2 files changed, 32 insertions(+), 23 deletions(-)

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index b9cb4755b..d32302a13 100644
--- 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 82e8d4ade..f8de4d7a5 100644
--- 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)
 
-- 
2.39.2