From 01b7b3b642833e1421da21741729e643e08e6f76 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 16 Feb 2004 09:44:14 +0000 Subject: [PATCH] solved a precedence issue between binders and arrows --- .../cic_disambiguation/cicTextualParser2.ml | 29 +++++++++---------- .../cic_disambiguation/cicTextualParser2.mli | 4 +-- 2 files changed, 16 insertions(+), 17 deletions(-) diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index 0ac43a11e..793d95e02 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -64,10 +64,15 @@ EXTEND ]; binder: [ [ SYMBOL <:unicode> (* λ *) -> `Lambda - | SYMBOL <:unicode> (* π *) -> `Pi + | SYMBOL <:unicode> (* Π *) -> `Pi | SYMBOL <:unicode> (* ∃ *) -> `Exists - | SYMBOL <:unicode> (* ∀ *) -> `Forall - ] + | SYMBOL <:unicode> (* ∀ *) -> `Forall ] + ]; + sort: [ + [ "Prop" -> `Prop + | "Set" -> `Set + | "Type" -> `Type + | "CProp" -> `CProp ] ]; typed_name: [ [ PAREN "("; i = IDENT; SYMBOL ":"; typ = term; PAREN ")" -> @@ -100,14 +105,9 @@ EXTEND (head, vars) ] ]; - term0: [ [ t = term -> return_term loc t ] ]; + term0: [ [ t = term; EOI -> return_term loc t ] ]; term: - [ "arrow" RIGHTA - [ t1 = term; SYMBOL <:unicode>; t2 = term -> - return_term loc - (CicAst.Binder (`Pi, (Cic.Anonymous, Some t1), t2)) - ] - | "binder" RIGHTA + [ "binder" RIGHTA [ b = binder; (vars, typ) = @@ -125,6 +125,9 @@ EXTEND vars body in return_term loc binder + | t1 = term; SYMBOL <:unicode> (* → *); t2 = term -> + return_term loc + (CicAst.Binder (`Pi, (Cic.Anonymous, Some t1), t2)) ] | "eq" LEFTA [ t1 = term; SYMBOL "="; t2 = term -> @@ -134,11 +137,7 @@ EXTEND | "mult" LEFTA [ (* nothing here by default *) ] | "inv" NONA [ (* nothing here by default *) ] | "simple" NONA - [ - sort_kind = [ - "Prop" -> `Prop | "Set" -> `Set | "Type" -> `Type | "CProp" -> `CProp - ] -> - CicAst.Sort sort_kind + [ sort = sort -> CicAst.Sort sort | n = substituted_name -> return_term loc n | PAREN "("; head = term; args = LIST1 term; PAREN ")" -> return_term loc (CicAst.Appl (head :: args)) diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.mli b/helm/ocaml/cic_disambiguation/cicTextualParser2.mli index aec7c8f1d..7e0625cc3 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.mli +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.mli @@ -31,8 +31,8 @@ val parse_term: char Stream.t -> CicAst.term (** {2 Grammar extensions} *) -val term: CicAst.term Grammar.Entry.e (** recursive rule *) -val term0: CicAst.term Grammar.Entry.e (** top level rule *) +val term: CicAst.term Grammar.Entry.e (** recursive rule *) +val term0: CicAst.term Grammar.Entry.e (** top level rule *) val return_term: CicAst.location -> CicAst.term -> CicAst.term -- 2.39.2