add macro to parse literals (#12)

* add macro to parse literals

* update changelog

* bump version

Author: lucaferranti

Project.toml

@@ -1,7 +1,7 @@
 name = "DedekindCutArithmetic"
 uuid = "a9cf20ff-59c8-5762-8ce8-520b700dfeff"
 authors = ["Luca Ferranti"]
-version = "0.1.0"
+version = "0.1.1"
 
 [deps]
 ForwardDiff = "f6369f11-7733-5829-9624-2563aa707210"

docs/src/changelog.md

@@ -10,13 +10,15 @@ EditURL = "https://github.com/lucaferranti/DedekindCutArithmetic.jl/blob/main/CH
 
 The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/), and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
 
-## Unreleased
+## [v0.1.1](https://github.com/lucaferranti/DedekindCutArithmetic.jl/releases/tag/v0.1.1) -- 2025-04-13
 
 ### Added
 
 - Support `Base.one` and `Base.zero` for cuts ([#5](https://github.com/lucaferranti/DedekindCutArithmetic.jl/issues/5))
 - Support `^` operation with non-negative integer exponent ([#4](https://github.com/lucaferranti/DedekindCutArithmetic.jl/issues/4))
 - Support `inv` and division ([#9](https://github.com/lucaferranti/DedekindCutArithmetic.jl/issues/9))
+- Add `@exact_str` string macro to correctly parse float literals ([#12](https://github.com/lucaferranti/DedekindCutArithmetic.jl/issues/12))
+- Add non-unicode `@forall` and `@exists` aliases ([#12](https://github.com/lucaferranti/DedekindCutArithmetic.jl/issues/12))
 
 ## [v0.1.0](https://github.com/lucaferranti/DedekindCutArithmetic.jl/releases/tag/v0.1.0) -- 2024-10-25
 

docs/src/tutorial.md

@@ -192,3 +192,42 @@ we can now use that to compute the maximum of ``f(x) = x(1 - x)``, which should
 ```@repl tutorial1
 my_max(x -> x * (1 - x))
 ```
+
+## Working with float literals
+
+By default, real numbers on compuers are approximately represented via floating point numbers.
+Floats cannot represent all reals exactly and when typing decimals, e.g. `0.1` one does not get the
+exact value, but an approximation
+
+```@repl tutorial1
+a = 0.1
+
+a == 1//10
+
+big(a)
+```
+
+Unfortunately, the parsing of literals in Julia happens already before building the abstract syntax tree,
+hence when processing expressions with macros, the rounding sin has already happened.
+
+For example, the following would fail to terminate
+
+```julia
+@∀ x ∈ [0, 1]: x + 0.1000000000000000000001 > x + 0.1
+```
+
+because when parsing the literals both produce the same floating point number.
+
+```@repl tutorial1
+0.1000000000000000000001 == 0.1
+```
+
+When working with rational numbers in decimal form, use the [`@exact_str`](@ref) string macro, which ensures the literal is parsed to the correct rational number.
+
+```@repl tutorial1
+exact"0.1"
+```
+
+```@repl tutorial1
+@∀ x ∈ [0, 1]: x + exact"0.1000000000000000000001" > x + exact"0.1"
+```

src/DedekindCutArithmetic.jl

@@ -12,7 +12,8 @@ using ForwardDiff
 export DyadicReal, DyadicInterval, DedekindCut, RationalCauchyCut, BinaryCompositeCut, @cut,
        refine!, dual, overlaps,
        width, midpoint, radius, thirds, low, high, isforward, isbackward,
-       exists, forall, @∀, @∃
+       exists, forall, @∀, @∃, @forall, @exists,
+       @exact_str
 
 const _Real = Union{Integer, AbstractFloat, Rational}
 

src/macros.jl

@@ -13,16 +13,18 @@ end
 """
 Check whether ``∃ x ∈ dom : prop(x)``
 """
-macro ∃(ex)
+macro exists(ex)
     parse_quantifier_body(ex, :exists)
 end
+const var"@∃" = var"@exists"
 
 """
 Check whether ``∀ x ∈ dom : prop(x)``
 """
-macro ∀(ex)
+macro forall(ex)
     parse_quantifier_body(ex, :forall)
 end
+const var"@∀" = var"@forall"
 
 """
 Transformations on the expression before being processed by [`@cut`](@ref)
@@ -73,3 +75,41 @@ macro cut(ex)
         throw(ArgumentError("Invalid cut expression $ex"))
     end
 end
+
+function parse_decimal(s::AbstractString)
+    num_exp = split(s, ('e', 'E'))
+    1 <= length(num_exp) <= 2 || throw(Meta.ParseError("invalid literal $s"))
+    n = first(num_exp)
+    int_dec = split(n, '.')
+    1 <= length(int_dec) <= 2 || throw(Meta.ParseError("invalid literal $s"))
+    num, logden = if length(int_dec) == 2
+        int, dec = int_dec
+        parse(BigInt, int * dec), -length(dec)
+    else
+        parse(BigInt, first(int_dec)), 0
+    end
+    if length(num_exp) == 2
+        logden += parse(BigInt, last(num_exp))
+    end
+    if logden < 0
+        num // 10^(-logden)
+    else
+        num * 10^logden
+    end
+end
+
+"""
+Parse a decimal literal into a Rational{BigInt}
+
+```julia
+julia> exact"0.1"
+1//10
+```
+
+This is needed because literals are already parsed before constructing the AST, hence
+when writing :(x - 0.1) one would get the floating point approximation of 1//10 instead of the
+exact rational.
+"""
+macro exact_str(s::AbstractString)
+    parse_decimal(s)
+end

src/quantifiers.jl

@@ -2,12 +2,12 @@
 Check whether ``∃ x ∈ dom : f(x) < 0``
 """
 function exists(dom::DyadicInterval, f::Function)::Bool
-    high(f(midpoint(dom))) < 0 && return true
+    f(midpoint(dom)) < 0 && return true
 
     # try to avoid bisection by checking for monotonicity
     d = ForwardDiff.derivative(f, dom)
-    low(d) > 0 && low(f(low(dom))) >= 0 && return false
-    high(d) < 0 && low(f(high(dom))) >= 0 && return false
+    low(d) > 0 && f(low(dom)) >= 0 && return false
+    high(d) < 0 && f(high(dom)) >= 0 && return false
 
     high(f(dual(dom))) >= 0 && return false
 
@@ -19,12 +19,12 @@ end
 Check whether ``∀ x ∈ dom : f(x) < 0``
 """
 function forall(dom::DyadicInterval, f::Function)::Bool
-    low(f(midpoint(dom))) >= 0 && return false
+    f(midpoint(dom)) >= 0 && return false
 
     # try to avoid bisection by checking for monotonicity
     d = ForwardDiff.derivative(f, dom)
-    low(d) > 0 && high(f(high(dom))) < 0 && return true
-    high(d) < 0 && high(f(low(dom))) < 0 && return true
+    low(d) > 0 && f(high(dom)) < 0 && return true
+    high(d) < 0 && f(low(dom)) < 0 && return true
 
     high(f(dom)) < 0 && return true
 

test/test-quantifiers.jl

@@ -7,6 +7,8 @@ using Test
     @test @∀ x ∈ [0, 1]:x < 2
     @test @∀ x ∈ [0, 1]:x < 1.0001
 
+    @test @∀ x ∈ [0, 1]:x > exact"-0.1e-12"
+
     @test !(@∀ x ∈ [0, 1]:x > 0.0001)
     @test !(@∀ x ∈ [0, 1]:x < 0.9999)
 end