Skip to content

Commit

Permalink
[ bug:racket ] Repro the issue with epsilon.0
Browse files Browse the repository at this point in the history
For some reason, having `epsilon.0` from `(require math/flonum)`
anywhere in the Racket support library trips the totality checker,
regardless of whether the code is used or not. Operations from
`math/flonum` (e.g. `fl/`) do not reproduce this behaviour.

See idris-lang#3116 for the full context.
  • Loading branch information
CodingCellist committed Nov 3, 2023
1 parent db87cef commit 416e109
Show file tree
Hide file tree
Showing 3 changed files with 24 additions and 0 deletions.
9 changes: 9 additions & 0 deletions bootstrap/idris2_app/idris2.rkt

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

1 change: 1 addition & 0 deletions src/Compiler/Scheme/Racket.idr
Original file line number Diff line number Diff line change
Expand Up @@ -56,6 +56,7 @@ schHeader prof libs = fromString """
(require ffi/unsafe ffi/unsafe/define) ; for calling C
\{ ifThenElse prof "(require profile)" "" }
(require racket/flonum) ; for float-typed transcendental functions
(require math/flonum) ; for flonum constants
""" ++ libs ++ """
Expand Down
14 changes: 14 additions & 0 deletions support/racket/support.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,20 @@
(if (> b 0) (+ r b) (- r b))
r)))


; flonum constants

;; /!\ This code trips the totality checker, even when it is never referenced in
;; /!\ Idris2, but only on the file `libs/papers/Data/Description/Regular.idr`??

(define (blodwen-flonumEpsilon)
epsilon.0)

;; /!\ End of cursed code


; Bits

(define bu+ (lambda (x y bits) (blodwen-toUnsignedInt (+ x y) bits)))
(define bu- (lambda (x y bits) (blodwen-toUnsignedInt (- x y) bits)))
(define bu* (lambda (x y bits) (blodwen-toUnsignedInt (* x y) bits)))
Expand Down

0 comments on commit 416e109

Please sign in to comment.