fix notation precedence

lecopivo · Jan 3, 2024 · 67069e2 · 67069e2
1 parent 890d61c
commit 67069e2
Show file tree

Hide file tree

Showing 5 changed files with 22 additions and 11 deletions.
diff --git a/SciLean/Core/Notation/CDeriv.lean b/SciLean/Core/Notation/CDeriv.lean
@@ -10,11 +10,11 @@ syntax diffBinderType  := " : " term
 syntax diffBinderValue := ":=" term (";" term)?
 syntax diffBinder := ident (diffBinderType <|> diffBinderValue)?
 
-scoped syntax "∂ " term+ : term
+scoped syntax "∂ " term:66 : term
 scoped syntax "∂ " diffBinder ", " term:66 : term
 scoped syntax "∂ " "(" diffBinder ")" ", " term:66 : term
 
-scoped syntax "∂! " term+ : term
+scoped syntax "∂! " term:66 : term
 scoped syntax "∂! " diffBinder ", " term:66 : term
 scoped syntax "∂! " "(" diffBinder ")" ", " term:66 : term
 

diff --git a/SciLean/Core/Notation/FwdCDeriv.lean b/SciLean/Core/Notation/FwdCDeriv.lean
@@ -8,19 +8,19 @@ import SciLean.Core.FunctionTransformations.FwdCDeriv
 namespace SciLean.NotationOverField
 
 
-scoped syntax "∂> " term+ : term
+scoped syntax "∂> " term:66 : term
 scoped syntax "∂> " diffBinder ", " term:66 : term
 scoped syntax "∂> " "(" diffBinder ")" ", " term:66 : term
 
-scoped syntax "∂>! " term+ : term
+scoped syntax "∂>! " term:66 : term
 scoped syntax "∂>! " diffBinder ", " term:66 : term
 scoped syntax "∂>! " "(" diffBinder ")" ", " term:66 : term
 
 open Lean Elab Term Meta in
 elab_rules : term
-| `(∂> $f $xs*) => do
+| `(∂> $f $x $xs*) => do
   let K := mkIdent (← currentFieldName.get)
-  elabTerm (← `(fwdCDeriv $K $f $xs*)) none
+  elabTerm (← `(fwdCDeriv $K $f $x $xs*)) none
 
 | `(∂> $f) => do
   let K := mkIdent (← currentFieldName.get)

diff --git a/SciLean/Core/Notation/Gradient.lean b/SciLean/Core/Notation/Gradient.lean
@@ -5,11 +5,11 @@ import SciLean.Core.Notation.CDeriv
 
 namespace SciLean.NotationOverField
 
-scoped syntax (name:=gradNotation1) "∇ " term+ : term
+scoped syntax (name:=gradNotation1) "∇ " term:66 : term
 scoped syntax "∇ " diffBinder ", " term:66 : term
 scoped syntax "∇ " "(" diffBinder ")" ", " term:66 : term
 
-scoped syntax "∇! " term+ : term
+scoped syntax "∇! " term:66 : term
 scoped syntax "∇! " diffBinder ", " term:66 : term
 scoped syntax "∇! " "(" diffBinder ")" ", " term:66 : term
 

diff --git a/SciLean/Core/Notation/RevCDeriv.lean b/SciLean/Core/Notation/RevCDeriv.lean
@@ -8,11 +8,11 @@ import SciLean.Core.FunctionTransformations.RevCDeriv
 
 namespace SciLean.NotationOverField
 
-scoped syntax "<∂ " term+ : term
+scoped syntax "<∂ " term:66 : term
 scoped syntax "<∂ " diffBinder ", " term:66 : term
 scoped syntax "<∂ " "(" diffBinder ")" ", " term:66 : term
 
-scoped syntax "<∂! " term+ : term
+scoped syntax "<∂! " term:66 : term
 scoped syntax "<∂! " diffBinder ", " term:66 : term
 scoped syntax "<∂! " "(" diffBinder ")" ", " term:66 : term
 

diff --git a/test/deriv_notation.lean b/test/deriv_notation.lean
@@ -17,13 +17,22 @@ set_default_scalar K
 #check ∂ (x:=1), x*x
 #check ∂ (x:=0.1), x*x
 #check ∂ (x:=((1:K),(2:K))), (x + x)
+#check 
+  let df := ∂ (fun x : K×K => (x.1 + x.2*x.1)) (0,0)
+  df (0,0)
+
 
 #check ∂! (fun x : K => x^2)
 #check ∂! (fun x : K×K => x + x)
 #check ∂! (fun x => x*x) 1
 #check ∂! (x:=((1:K),(2:K))), (x + x)
 #check ∂! (x:=1), x*x
 
+
+#check ∂ (fun x : K => x*x)
+       =
+       (fun x => x + x)
+
 variable {X} [Vec K X] (f : X → X)
 
 #check ∂ (x:=0), f x
@@ -70,7 +79,9 @@ set_default_scalar K
 
 #check ∂>! x : K×K, (x.1 + x.2*x.1)
 #check ∂>! x:=(1:K);2, (x + x*x)
-
+#check 
+  let a := ∂> (fun x : K×K => (x.1 + x.2*x.1))
+  a (0,0)
 
 
 --------------------------------------------------------------------------------