From a611291b68a2f9a0c627de0cdabf8f7448136bcf Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli 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 - | SYMBOL <:unicode> (* Π *) -> `Pi + binder_low: [ + [ SYMBOL <:unicode> (* Π *) -> `Pi | SYMBOL <:unicode> (* ∃ *) -> `Exists | SYMBOL <:unicode> (* ∀ *) -> `Forall ] ]; + binder_high: [ [ SYMBOL <:unicode> (* λ *) -> `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> (* → *); 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> (* → *); 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