FStarLang/FStar

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

Open

#793 aperta il 23 dic 2016

Vedi su GitHub
 (8 commenti) (0 reazioni) (0 assegnatari)F* (258 fork)auto 404
area/fsharp-vs-ocamlcomponent/buildcomponent/extractiongood first issuekind/bug

Metriche repository

Star
 (3068 star)
Metriche merge PR
 (Metriche PR in attesa)

Descrizione

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#.

Guida contributor

Direzione di ricerca
Esamina la generazione del codice F# per i letterali a virgola mobile nel meccanismo di estrazione di F*. Assicurati che il letterale venga emesso con il punto decimale e la sintassi F# corretta (ad es. '1.0' invece di '1').
Tech stack
Nessuno
Dominio
compilers
Tipo issue
Bug
DifficoltàQuanto dovrebbe essere impegnativa per un nuovo contributor.
2
Tempo stimatoTempo stimato per completare e verificare uno scope piccolo.
1-3 ore
Stato attivitàQuanto è probabile che la issue sia ancora attiva e reviewable.
Attiva
ChiarezzaQuanto chiaramente la issue descrive problema, scope e risultato atteso.
Chiara
Prerequisiti
F*
Adatta ai principiantiQuanto la issue è adatta a contributor alla prima esperienza.
40