From a4c955f9b69cae88879d366b01ac86fa1ea2b829 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 25 May 2005 13:44:34 +0000 Subject: [PATCH] \lambda x.x y ----> \lambda x.(x y) --- helm/ocaml/cic_disambiguation/cicTextualParser2.ml | 13 +++++-------- helm/ocaml/cic_disambiguation/doc/precedence.txt | 6 +++--- 2 files changed, 8 insertions(+), 11 deletions(-) diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index 431b15ae8..add74d03e 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -250,6 +250,11 @@ EXTEND b = binder_low; (vars, typ) = binder_vars; SYMBOL "."; body = term -> let binder = mk_binder_ast b typ vars body in return_term loc binder + | 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> (* → *); 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 *) ] @@ -270,14 +275,6 @@ EXTEND in CicAst.Appl (aux t1 @ [t2]) ] - | "binder" RIGHTA - [ - 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> (* → *); t2 = term -> - return_term loc (CicAst.Binder (`Pi, (Cic.Anonymous, Some t1), t2)) - ] | "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 index cd7186fcf..09efea853 100644 --- a/helm/ocaml/cic_disambiguation/doc/precedence.txt +++ b/helm/ocaml/cic_disambiguation/doc/precedence.txt @@ -2,7 +2,7 @@ Input Should be parsed as Derived constraint on precedence -------------------------------------------------------------------------------- -\lambda x.x y ((\lambda x.x) y) lambda > 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 \lambda x.x \to x \lambda. (x \to x) \to > \lambda @@ -10,7 +10,7 @@ S x = y (= (S x) y) apply > infix operators Precedence total order: - \to > lambda > apply > infix operators > binders + apply > infix operators > to > binders where binders are all binders except lambda (i.e. \forall, \pi, \exists) @@ -25,7 +25,7 @@ EOT should respond with: - (\lambda x.x y) + \lambda x.(x y) (eq (S x) y) \forall x.(eq x x) \lambda x.(x \to x) -- 2.39.2