From e52a9fa8835eddf70d0c8e454470fb12eebef7cd Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 30 Oct 2003 14:29:39 +0000 Subject: Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre associative a gauche; gestion du signe dans le parseur pas dans l'interpreteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4745 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/ring/Ring_theory.v | 10 ++++------ contrib/ring/Setoid_ring_theory.v | 8 +++----- interp/constrintern.ml | 3 --- parsing/g_constrnew.ml4 | 5 +++-- parsing/pcoq.ml4 | 2 +- theories/Init/Notations.v | 5 +++-- theories/Reals/Rsyntax.v | 36 +++++++++++++++--------------------- 7 files changed, 29 insertions(+), 40 deletions(-) diff --git a/contrib/ring/Ring_theory.v b/contrib/ring/Ring_theory.v index 55ad8023f3..b938f7db04 100644 --- a/contrib/ring/Ring_theory.v +++ b/contrib/ring/Ring_theory.v @@ -150,12 +150,10 @@ Infix 4 "+" Aplus V8only 50 (left associativity). Infix 4 "*" Amult V8only 40 (left associativity). Notation "0" := Azero. Notation "1" := Aone. -Notation "- 0" := (Aopp Azero) (at level 0) - V8only (at level 50, left associativity). -Notation "- 1" := (Aopp Aone) (at level 0) - V8only (at level 50, left associativity). -Notation "- x" := (Aopp x) (at level 0) - V8only (at level 50, left associativity). +Notation "- 0" := (Aopp Azero) (at level 0) V8only (at level 10). +Notation "- 1" := (Aopp Aone) (at level 0) V8only (at level 10). +Notation "- x" := (Aopp x) (at level 0) + V8only (at level 10, right associativity). Record Ring_Theory : Prop := { Th_plus_sym : (n,m:A) n + m == m + n; diff --git a/contrib/ring/Setoid_ring_theory.v b/contrib/ring/Setoid_ring_theory.v index c97536846b..eedc92197a 100644 --- a/contrib/ring/Setoid_ring_theory.v +++ b/contrib/ring/Setoid_ring_theory.v @@ -35,12 +35,10 @@ Infix 4 "+" Aplus V8only 50 (left associativity). Infix 4 "*" Amult V8only 40 (left associativity). Notation "0" := Azero. Notation "1" := Aone. -Notation "- 0" := (Aopp Azero) (at level 0) - V8only (at level 50, left associativity). -Notation "- 1" := (Aopp Aone) (at level 0) - V8only (at level 50, left associativity). +Notation "- 0" := (Aopp Azero) (at level 0) V8only (at level 10). +Notation "- 1" := (Aopp Aone) (at level 0) V8only (at level 10). Notation "- x" := (Aopp x) (at level 0) - V8only (at level 50, left associativity). + V8only (at level 10, right associativity). Variable plus_morph : (a,a0,a1,a2:A) a == a0 -> a1 == a2 -> a+a1 == a0+a2. Variable mult_morph : (a,a0,a1,a2:A) a == a0 -> a1 == a2 -> a*a1 == a0*a2. diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 66851e70e8..97790d3633 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -586,9 +586,6 @@ let internalise sigma env allow_soapp lvar c = | CLetIn (loc,(_,na),c1,c2) -> RLetIn (loc, na, intern (reset_tmp_scope env) c1, intern (push_name_env lvar env na) c2) - | CNotation (loc,"- _",[CNumeral(_,Bignat.POS p)]) -> - let scopes = option_cons tmp_scope scopes in - Symbols.interp_numeral loc (Bignat.NEG p) scopes | CNotation (loc,ntn,args) -> let scopes = option_cons tmp_scope scopes in let (ids,c) = Symbols.interp_notation ntn scopes in diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4 index d5d1db939e..ea736cc91f 100644 --- a/parsing/g_constrnew.ml4 +++ b/parsing/g_constrnew.ml4 @@ -178,9 +178,10 @@ GEXTEND Gram | "90" RIGHTA [ c1 = operconstr; "->"; c2 = binder_constr -> CArrow(loc,c1,c2) | c1 = operconstr; "->"; c2 = operconstr -> CArrow(loc,c1,c2) ] - | "10" LEFTA + | "10" [ f=operconstr; args=LIST1 appl_arg -> CApp(loc,(None,f),args) - | "@"; f=global; args=LIST0 NEXT -> CAppExpl(loc,(None,f),args) ] + | "@"; f=global; args=LIST0 NEXT -> CAppExpl(loc,(None,f),args) + | "-"; n=INT -> CNumeral (loc,Bignat.NEG (Bignat.of_string n)) ] | "9" [ ] | "1" LEFTA [ c=operconstr; ".("; f=global; args=LIST0 appl_arg; ")" -> diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 152141bfae..5380115e1e 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -547,7 +547,7 @@ let default_levels_v8 = 100,Gramext.RightA; 99,Gramext.RightA; 90,Gramext.RightA; - 10,Gramext.LeftA; + 10,Gramext.RightA; 9,Gramext.RightA; 1,Gramext.LeftA; 0,Gramext.RightA] diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v index 00c35de84e..7fb43a703e 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.v @@ -54,9 +54,10 @@ Uninterpreted Notation "x * y" (at level 3, right associativity) Uninterpreted V8Notation "x / y" (at level 40, left associativity). Uninterpreted Notation "x + y" (at level 4, left associativity). Uninterpreted Notation "x - y" (at level 4, left associativity). -Uninterpreted Notation "- x" (at level 0) V8only (at level 50). +Uninterpreted Notation "- x" (at level 0) + V8only (at level 10, right associativity). Uninterpreted Notation "/ x" (at level 0) - V8only (at level 40, left associativity). + V8only (at level 10, right associativity). Uninterpreted V8Notation "x ^ y" (at level 30, left associativity). diff --git a/theories/Reals/Rsyntax.v b/theories/Reals/Rsyntax.v index 3929acdf9f..53f8aec077 100644 --- a/theories/Reals/Rsyntax.v +++ b/theories/Reals/Rsyntax.v @@ -205,37 +205,31 @@ Syntax constr (* For parsing/printing based on scopes *) Module R_scope. -Infix "<=" Rle (at level 5, no associativity) : R_scope. -Infix "<" Rlt (at level 5, no associativity) : R_scope. -Infix ">=" Rge (at level 5, no associativity) : R_scope. -Infix ">" Rgt (at level 5, no associativity) : R_scope. -Infix "+" Rplus (at level 4) : R_scope - V8only (at level 50, left associativity). -Infix "-" Rminus (at level 4) : R_scope - V8only (at level 50, left associativity). -Infix "*" Rmult (at level 3) : R_scope - V8only (at level 40, left associativity). -Infix "/" Rdiv (at level 3) : R_scope - V8only (at level 40, left associativity). -Notation "- x" := (Ropp x) (at level 0) : R_scope - V8only (at level 50, left associativity). +Infix "<=" Rle (at level 5, no associativity) : R_scope V8only. +Infix "<" Rlt (at level 5, no associativity) : R_scope V8only. +Infix ">=" Rge (at level 5, no associativity) : R_scope V8only. +Infix ">" Rgt (at level 5, no associativity) : R_scope V8only. +Infix "+" Rplus (at level 4) : R_scope V8only. +Infix "-" Rminus (at level 4) : R_scope V8only. +Infix "*" Rmult (at level 3) : R_scope V8only. +Infix "/" Rdiv (at level 3) : R_scope V8only. +Notation "- x" := (Ropp x) (at level 0) : R_scope V8only. Notation "x == y == z" := (eqT R x y)/\(eqT R y z) - (at level 5, y at level 4, no associtivity): R_scope - V8only "x = y = z" (at level 70, y at next level, no associativity). + (at level 5, y at level 4, no associtivity): R_scope. Notation "x <= y <= z" := (Rle x y)/\(Rle y z) (at level 5, y at level 4) : R_scope - V8only (at level 70, y at next level, no associativity). + V8only. Notation "x <= y < z" := (Rle x y)/\(Rlt y z) (at level 5, y at level 4) : R_scope - V8only (at level 70, y at next level, no associativity). + V8only. Notation "x < y < z" := (Rlt x y)/\(Rlt y z) (at level 5, y at level 4) : R_scope - V8only (at level 70, y at next level, no associativity). + V8only. Notation "x < y <= z" := (Rlt x y)/\(Rle y z) (at level 5, y at level 4) : R_scope - V8only (at level 70, y at next level, no associativity). + V8only. Notation "/ x" := (Rinv x) (at level 0): R_scope - V8only (at level 40, left associativity). + V8only. Open Local Scope R_scope. End R_scope. -- cgit v1.2.3