FStarLang/FStar

Floating point literals are badly handled by the F# extraction mechanism

Open

#793 opened on Dec 23, 2016

View on GitHub
 (8 comments) (0 reactions) (0 assignees)F* (258 forks)auto 404
area/fsharp-vs-ocamlcomponent/buildcomponent/extractiongood first issuekind/bug

Repository metrics

Stars
 (3,068 stars)
PR merge metrics
 (PR metrics pending)

Description

Using literal floating point in some meant-to-be-extracted file like the F* compiler can produce bad results when extracting with the F# version of the F* compiler (seems to be fine with the ocaml version). For example 1.0 is extracted to 1 and 0.99 to 0,99 which are no longer of the same type. A temporary solution is to use float_of_string "1.0" but I would be rather surprised if there is no better way to do that in F#.

Contributor guide

Research direction
Examine the F# code generation for floating point literals in the F* extraction mechanism. Ensure that the literal is emitted with a decimal point and correct F# syntax (e.g., '1.0' instead of '1').
Tech stack
None
Domain
compilers
Issue type
Bug
DifficultyEstimated implementation difficulty for a new contributor, from 1 for very small changes to 5 for expert-level work.
2
Estimated timeA rough time range for an experienced contributor to investigate, implement, test, and prepare a pull request.
1-3 hours
Activity statusHow available the issue appears right now: fresh, active, stale, blocked, or waiting on maintainer input.
Active
ClarityHow clearly the issue explains the expected change, acceptance criteria, and next step.
Clear
Prerequisites
F*
Newbie friendlinessA 1-100 score estimating how approachable this issue is for first-time contributors.
40