From 5b3048fb48d58e2bd6f726254a06d95a48b2656f Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 21 Apr 2005 12:04:32 +0000 Subject: [PATCH] (hopefully) final decision on precedence levels: binder > apply > infix operators --- .../cic_disambiguation/cicTextualParser2.ml | 22 +++++++++---------- .../cic_disambiguation/doc/precedence.txt | 12 ++++++++++ 2 files changed, 23 insertions(+), 11 deletions(-) create mode 100644 helm/ocaml/cic_disambiguation/doc/precedence.txt diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index 445871045..b9cb4755b 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -225,6 +225,17 @@ EXTEND defs = let_defs; "in"; body = term -> return_term loc (CicAst.LetRec (ind_kind, defs, body)) ] + | "logic_add" LEFTA [ (* nothing here by default *) ] + | "logic_mult" LEFTA [ (* nothing here by default *) ] + | "logic_inv" NONA [ (* nothing here by default *) ] + | "relop" LEFTA + [ t1 = term; SYMBOL "="; t2 = term -> + return_term loc (CicAst.Appl [CicAst.Symbol ("eq", 0); t1; t2]) + ] + | "add" LEFTA [ (* nothing here by default *) ] + | "mult" LEFTA [ (* nothing here by default *) ] + | "power" LEFTA [ (* nothing here by default *) ] + | "inv" NONA [ (* nothing here by default *) ] | "apply" LEFTA [ t1 = term; t2 = term -> let rec aux = function @@ -255,17 +266,6 @@ EXTEND 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 *) ] - | "relop" LEFTA - [ t1 = term; SYMBOL "="; t2 = term -> - return_term loc (CicAst.Appl [CicAst.Symbol ("eq", 0); t1; t2]) - ] - | "add" LEFTA [ (* nothing here by default *) ] - | "mult" LEFTA [ (* nothing here by default *) ] - | "power" LEFTA [ (* nothing here by default *) ] - | "inv" NONA [ (* nothing here by default *) ] | "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 new file mode 100644 index 000000000..82e8d4ade --- /dev/null +++ b/helm/ocaml/cic_disambiguation/doc/precedence.txt @@ -0,0 +1,12 @@ + +Input Should be parsed as Derived constraint + on precedence +-------------------------------------------------------------------------------- +\lambda x.x y ((\lambda x.x) y) binder > apply +S x = y (= (S x) y) apply > infix operators +-------------------------------------------------------------------------------- + +Precedence total order: + + binder > apply > infix operators + -- 2.39.2