refactor: OfDecimal ==> OfScientific

`decimalLit` ==> `scientificLit`

src/Init/Data.lean

@@ -21,4 +21,4 @@ import Init.Data.Random
 import Init.Data.ToString
 import Init.Data.Range
 import Init.Data.Hashable
-import Init.Data.OfDecimal
+import Init.Data.OfScientific

src/Init/Data/Float.lean

@@ -98,4 +98,4 @@ abbrev Nat.toFloat (n : Nat) : Float :=
 
 instance : Pow Float := ⟨Float.pow⟩
 
-@[extern "lean_float_of_decimal"] constant Float.ofDecimal (m : Nat) (s : Bool) (e : Nat) : Float
+@[extern "lean_float_of_scientific"] constant Float.ofScientific (m : Nat) (s : Bool) (e : Nat) : Float

src/Init/Data/OfDecimal.lean

@@ -1,20 +0,0 @@
-/-
-Copyright (c) 2020 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Init.Data.Float
-import Init.Data.Nat
-
-/- For decimal numbers (e.g., `1.23`).
-   Examples:
-   - `OfDecimal.ofDecimal 123 true 2`    represents `1.23`
-   - `Ofdecimal.ofdecimal 121 false 100` represents `121e100`
--/
-class OfDecimal (α : Type u) where
-  ofDecimal : Nat → Bool → Nat → α
-
-@[defaultInstance]
-instance : OfDecimal Float where
-  ofDecimal m s e := Float.ofDecimal m s e

src/Init/Data/OfScientific.lean

@@ -0,0 +1,20 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Data.Float
+import Init.Data.Nat
+
+/- For decimal and scientific numbers (e.g., `1.23`, `3.12e10`).
+   Examples:
+   - `OfScientific.ofScientific 123 true 2`    represents `1.23`
+   - `OfScientific.ofScientific 121 false 100` represents `121e100`
+-/
+class OfScientific (α : Type u) where
+  ofScientific : Nat → Bool → Nat → α
+
+@[defaultInstance]
+instance : OfScientific Float where
+  ofScientific m s e := Float.ofScientific m s e

src/Init/Meta.lean

@@ -285,8 +285,8 @@ def mkStrLit (val : String) (info : SourceInfo := {}) : Syntax :=
 def mkNumLit (val : String) (info : SourceInfo := {}) : Syntax :=
   mkLit numLitKind val info
 
-def mkDecimalLit (val : String) (info : SourceInfo := {}) : Syntax :=
-  mkLit decimalLitKind val info
+def mkScientificLit (val : String) (info : SourceInfo := {}) : Syntax :=
+  mkLit scientificLitKind val info
 
 /- Recall that we don't have special Syntax constructors for storing numeric and string atoms.
    The idea is to have an extensible approach where embedded DSLs may have new kind of atoms and/or
@@ -370,7 +370,7 @@ def isNatLit? (s : Syntax) : Option Nat :=
 def isFieldIdx? (s : Syntax) : Option Nat :=
   isNatLitAux fieldIdxKind s
 
-partial def decodeDecimalLitVal? (s : String) : Option (Nat × Bool × Nat) :=
+partial def decodeScientificLitVal? (s : String) : Option (Nat × Bool × Nat) :=
   let len := s.length
   if len == 0 then none
   else
@@ -427,9 +427,9 @@ where
       else
         none
 
-def isDecimalLit? (stx : Syntax) : Option (Nat × Bool × Nat) :=
-  match isLit? decimalLitKind stx with
-  | some val => decodeDecimalLitVal? val
+def isScientificLit? (stx : Syntax) : Option (Nat × Bool × Nat) :=
+  match isLit? scientificLitKind stx with
+  | some val => decodeScientificLitVal? val
   | _        => none
 
 def isIdOrAtom? : Syntax → Option String

src/Init/Prelude.lean

@@ -1595,7 +1595,7 @@ def identKind : SyntaxNodeKind := `ident
 def strLitKind : SyntaxNodeKind := `strLit
 def charLitKind : SyntaxNodeKind := `charLit
 def numLitKind : SyntaxNodeKind := `numLit
-def decimalLitKind : SyntaxNodeKind := `decimalLit
+def scientificLitKind : SyntaxNodeKind := `scientificLit
 def nameLitKind : SyntaxNodeKind := `nameLit
 def fieldIdxKind : SyntaxNodeKind := `fieldIdx
 def interpolatedStrLitKind : SyntaxNodeKind := `interpolatedStrLitKind

src/Lean/Elab/Match.lean

@@ -481,7 +481,7 @@ partial def collect : Syntax → M Syntax
       pure stx
     else if k == numLitKind then
       pure stx
-    else if k == decimalLitKind then
+    else if k == scientificLitKind then
       pure stx
     else if k == charLitKind then
       pure stx

src/Lean/Elab/Term.lean

@@ -1274,14 +1274,15 @@ private def mkFreshTypeMVarFor (expectedType? : Option Expr) : TermElabM Expr :=
   | some val => return mkNatLit val
   | none     => throwIllFormedSyntax
 
-@[builtinTermElab decimalLit] def elabDecimalLit : TermElab := fun stx expectedType? => do
-  match stx.isDecimalLit? with
+@[builtinTermElab scientificLit]
+def elabScientificLit : TermElab := fun stx expectedType? => do
+  match stx.isScientificLit? with
   | none        => throwIllFormedSyntax
   | some (m, sign, e) =>
     let typeMVar ← mkFreshTypeMVarFor expectedType?
     let u ← getDecLevel typeMVar
-    let mvar ← mkInstMVar (mkApp (Lean.mkConst `OfDecimal [u]) typeMVar)
-    return mkApp5 (Lean.mkConst `OfDecimal.ofDecimal [u]) typeMVar mvar (mkNatLit m) (toExpr sign) (mkNatLit e)
+    let mvar ← mkInstMVar (mkApp (Lean.mkConst `OfScientific [u]) typeMVar)
+    return mkApp5 (Lean.mkConst `OfScientific.ofScientific [u]) typeMVar mvar (mkNatLit m) (toExpr sign) (mkNatLit e)
 
 @[builtinTermElab charLit] def elabCharLit : TermElab := fun stx _ => do
   match stx.isCharLit? with

src/Lean/Parser.lean

@@ -25,7 +25,7 @@ def mkAntiquot.parenthesizer (name : String) (kind : Option SyntaxNodeKind) (ano
 -- (e.g. `ident`) is not equal to the parser name `Lean.Parser.Term.ident`.
 @[builtinParenthesizer ident] def ident.parenthesizer : Parenthesizer := Parser.Term.ident.parenthesizer
 @[builtinParenthesizer numLit] def numLit.parenthesizer : Parenthesizer := Parser.Term.num.parenthesizer
-@[builtinParenthesizer decimalLit] def decimalLit.parenthesizer : Parenthesizer := Parser.Term.decimal.parenthesizer
+@[builtinParenthesizer scientificLit] def scientificLit.parenthesizer : Parenthesizer := Parser.Term.scientific.parenthesizer
 @[builtinParenthesizer charLit] def charLit.parenthesizer : Parenthesizer := Parser.Term.char.parenthesizer
 @[builtinParenthesizer strLit] def strLit.parenthesizer : Parenthesizer := Parser.Term.str.parenthesizer
 
@@ -39,7 +39,7 @@ def mkAntiquot.formatter (name : String) (kind : Option SyntaxNodeKind) (anonymo
 
 @[builtinFormatter ident] def ident.formatter : Formatter := Parser.Term.ident.formatter
 @[builtinFormatter numLit] def numLit.formatter : Formatter := Parser.Term.num.formatter
-@[builtinFormatter decimalLit] def decimalLit.formatter : Formatter := Parser.Term.decimal.formatter
+@[builtinFormatter scientificLit] def scientificLit.formatter : Formatter := Parser.Term.scientific.formatter
 @[builtinFormatter charLit] def charLit.formatter : Formatter := Parser.Term.char.formatter
 @[builtinFormatter strLit] def strLit.formatter : Formatter := Parser.Term.str.formatter
 

src/Lean/Parser/Basic.lean

@@ -68,7 +68,7 @@ namespace Lean
 namespace Parser
 
 def isLitKind (k : SyntaxNodeKind) : Bool :=
-  k == strLitKind || k == numLitKind || k == charLitKind || k == nameLitKind || k == decimalLitKind
+  k == strLitKind || k == numLitKind || k == charLitKind || k == nameLitKind || k == scientificLitKind
 
 abbrev mkAtom (info : SourceInfo) (val : String) : Syntax :=
   Syntax.atom info val
@@ -815,7 +815,7 @@ def decimalNumberFn (startPos : Nat) (c : ParserContext) : ParserState → Parse
   if curr == '.' || curr == 'e' || curr == 'E' then
     let s := parseOptDot s
     let s := parseOptExp s
-    mkNodeToken decimalLitKind startPos c s
+    mkNodeToken scientificLitKind startPos c s
   else
     mkNodeToken numLitKind startPos c s
 where
@@ -1186,15 +1186,15 @@ def numLitFn : ParserFn :=
   info := mkAtomicInfo "numLit"
 }
 
-def decimalLitFn : ParserFn :=
+def scientificLitFn : ParserFn :=
   fun c s =>
     let iniPos := s.pos
     let s      := tokenFn c s
-    if s.hasError || !(s.stxStack.back.isOfKind decimalLitKind) then s.mkErrorAt "decimal number" iniPos else s
+    if s.hasError || !(s.stxStack.back.isOfKind scientificLitKind) then s.mkErrorAt "scientific number" iniPos else s
 
-@[inline] def decimalLitNoAntiquot : Parser := {
-  fn   := decimalLitFn,
-  info := mkAtomicInfo "decimalLit"
+@[inline] def scientificLitNoAntiquot : Parser := {
+  fn   := scientificLitFn,
+  info := mkAtomicInfo "scientificLit"
 }
 
 def strLitFn : ParserFn := fun c s =>
@@ -1630,8 +1630,8 @@ def rawIdent : Parser :=
 def numLit : Parser :=
   withAntiquot (mkAntiquot "numLit" numLitKind) numLitNoAntiquot
 
-def decimalLit : Parser :=
-  withAntiquot (mkAntiquot "decimalLit" decimalLitKind) decimalLitNoAntiquot
+def scientificLit : Parser :=
+  withAntiquot (mkAntiquot "scientificLit" scientificLitKind) scientificLitNoAntiquot
 
 def strLit : Parser :=
   withAntiquot (mkAntiquot "strLit" strLitKind) strLitNoAntiquot

src/Lean/Parser/Extension.lean

@@ -26,7 +26,7 @@ builtin_initialize
   registerBuiltinNodeKind identKind
   registerBuiltinNodeKind strLitKind
   registerBuiltinNodeKind numLitKind
-  registerBuiltinNodeKind decimalLitKind
+  registerBuiltinNodeKind scientificLitKind
   registerBuiltinNodeKind charLitKind
   registerBuiltinNodeKind nameLitKind
 

src/Lean/Parser/Extra.lean

@@ -15,7 +15,7 @@ namespace Parser
 -- (because `Parser.Extension` depends on them)
 attribute [runBuiltinParserAttributeHooks]
   leadingNode termParser commandParser antiquotNestedExpr antiquotExpr mkAntiquot nodeWithAntiquot
-  ident numLit decimalLit charLit strLit nameLit
+  ident numLit scientificLit charLit strLit nameLit
 
 @[runBuiltinParserAttributeHooks, inline] def group (p : Parser) : Parser :=
   node nullKind p

src/Lean/Parser/Term.lean

@@ -44,7 +44,7 @@ def optSemicolon (p : Parser) : Parser := ppDedent $ optional ";" >> ppLine >> p
 -- `checkPrec` necessary for the pretty printer
 @[builtinTermParser] def ident := checkPrec maxPrec >> Parser.ident
 @[builtinTermParser] def num : Parser := checkPrec maxPrec >> numLit
-@[builtinTermParser] def decimal : Parser := checkPrec maxPrec >> decimalLit
+@[builtinTermParser] def scientific : Parser := checkPrec maxPrec >> scientificLit
 @[builtinTermParser] def str : Parser := checkPrec maxPrec >> strLit
 @[builtinTermParser] def char : Parser := checkPrec maxPrec >> charLit
 @[builtinTermParser] def type := parser! "Type" >> optional (checkWsBefore "" >> checkPrec leadPrec >> checkColGt >> levelParser maxPrec)

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -369,8 +369,8 @@ def delabOfNat : Delab := whenPPOption getPPCoercions do
   return quote n
 
 -- `@OfDecimal.ofDecimal _ _ m s e` ~> `m*10^(sign * e)` where `sign == 1` if `s = false` and `sign = -1` if `s = true`
-@[builtinDelab app.OfDecimal.ofDecimal]
-def delabOfDecimal : Delab := whenPPOption getPPCoercions do
+@[builtinDelab app.OfScientific.ofScientific]
+def delabOfScientific : Delab := whenPPOption getPPCoercions do
   let expr ← getExpr
   guard <| expr.getAppNumArgs == 5
   let Expr.lit (Literal.natVal m) _ ← pure (expr.getArg! 2) | failure
@@ -381,13 +381,13 @@ def delabOfDecimal : Delab := whenPPOption getPPCoercions do
     | _ => failure
   let str  := toString m
   if s && e == str.length then
-    return Syntax.mkDecimalLit ("0." ++ str)
+    return Syntax.mkScientificLit ("0." ++ str)
   else if s && e < str.length then
     let mStr := str.extract 0 (str.length - e)
     let eStr := str.extract (str.length - e) str.length
-    return Syntax.mkDecimalLit (mStr ++ "." ++ eStr)
+    return Syntax.mkScientificLit (mStr ++ "." ++ eStr)
   else
-    return Syntax.mkDecimalLit (str ++ "e" ++ (if s then "-" else "") ++ toString e)
+    return Syntax.mkScientificLit (str ++ "e" ++ (if s then "-" else "") ++ toString e)
 
 /--
 Delaborate a projection primitive. These do not usually occur in

src/Lean/PrettyPrinter/Formatter.lean

@@ -353,7 +353,7 @@ def visitAtom (k : SyntaxNodeKind) : Formatter := do
 @[combinatorFormatter Lean.Parser.strLitNoAntiquot] def strLitNoAntiquot.formatter := visitAtom strLitKind
 @[combinatorFormatter Lean.Parser.nameLitNoAntiquot] def nameLitNoAntiquot.formatter := visitAtom nameLitKind
 @[combinatorFormatter Lean.Parser.numLitNoAntiquot] def numLitNoAntiquot.formatter := visitAtom numLitKind
-@[combinatorFormatter Lean.Parser.decimalLitNoAntiquot] def decimalLitNoAntiquot.formatter := visitAtom decimalLitKind
+@[combinatorFormatter Lean.Parser.scientificLitNoAntiquot] def scientificLitNoAntiquot.formatter := visitAtom scientificLitKind
 @[combinatorFormatter Lean.Parser.fieldIdx] def fieldIdx.formatter := visitAtom fieldIdxKind
 
 @[combinatorFormatter Lean.Parser.many]
@@ -440,7 +440,7 @@ builtin_initialize
   registerAlias "ws" checkWsBefore.formatter
   registerAlias "noWs" checkNoWsBefore.formatter
   registerAlias "num" (withAntiquot.formatter (mkAntiquot.formatter' "numLit" `numLit) numLitNoAntiquot.formatter)
-  registerAlias "decimal" (withAntiquot.formatter (mkAntiquot.formatter' "decimalLit" `decimalLit) decimalLitNoAntiquot.formatter)
+  registerAlias "scientific" (withAntiquot.formatter (mkAntiquot.formatter' "scientificLit" `scientificLit) scientificLitNoAntiquot.formatter)
   registerAlias "str" (withAntiquot.formatter (mkAntiquot.formatter' "strLit" `strLit) strLitNoAntiquot.formatter)
   registerAlias "char" (withAntiquot.formatter (mkAntiquot.formatter' "charLit" `charLit) charLitNoAntiquot.formatter)
   registerAlias "name" (withAntiquot.formatter (mkAntiquot.formatter' "nameLit" `nameLit) nameLitNoAntiquot.formatter)

src/Lean/PrettyPrinter/Parenthesizer.lean

@@ -407,7 +407,7 @@ def trailingNode.parenthesizer (k : SyntaxNodeKind) (prec : Nat) (p : Parenthesi
 @[combinatorParenthesizer Lean.Parser.strLitNoAntiquot] def strLitNoAntiquot.parenthesizer := visitToken
 @[combinatorParenthesizer Lean.Parser.nameLitNoAntiquot] def nameLitNoAntiquot.parenthesizer := visitToken
 @[combinatorParenthesizer Lean.Parser.numLitNoAntiquot] def numLitNoAntiquot.parenthesizer := visitToken
-@[combinatorParenthesizer Lean.Parser.decimalLitNoAntiquot] def decimalLitNoAntiquot.parenthesizer := visitToken
+@[combinatorParenthesizer Lean.Parser.scientificLitNoAntiquot] def scientificLitNoAntiquot.parenthesizer := visitToken
 @[combinatorParenthesizer Lean.Parser.fieldIdx] def fieldIdx.parenthesizer := visitToken
 
 @[combinatorParenthesizer Lean.Parser.many]
@@ -495,7 +495,7 @@ builtin_initialize
   registerAlias "ws" checkWsBefore.parenthesizer
   registerAlias "noWs" checkNoWsBefore.parenthesizer
   registerAlias "num" (withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "numLit" `numLit) numLitNoAntiquot.parenthesizer)
-  registerAlias "decimal" (withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "decimalLit" `decimalLit) decimalLitNoAntiquot.parenthesizer)
+  registerAlias "scientific" (withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "scientificLit" `scientificLit) scientificLitNoAntiquot.parenthesizer)
   registerAlias "str" (withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "strLit" `strLit) strLitNoAntiquot.parenthesizer)
   registerAlias "char" (withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "charLit" `charLit) charLitNoAntiquot.parenthesizer)
   registerAlias "name" (withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "nameLit" `nameLit) nameLitNoAntiquot.parenthesizer)

src/runtime/object.cpp

@@ -1464,14 +1464,14 @@ extern "C" lean_obj_res lean_float_to_string(double a) {
     return mk_string(std::to_string(a));
 }
 
-static double of_decimal(mpz const & m, bool sign, size_t e) {
+static double of_scientific(mpz const & m, bool sign, size_t e) {
     if (sign)
         return (mpq(m)/mpz(10).pow(e)).get_double();
     else
         return (mpq(m)*mpz(10).pow(e)).get_double();
 }
 
-extern "C" double lean_float_of_decimal(b_lean_obj_arg m, uint8 esign, b_lean_obj_arg e) {
+extern "C" double lean_float_of_scientific(b_lean_obj_arg m, uint8 esign, b_lean_obj_arg e) {
     if (!lean_is_scalar(e)) {
         if (esign) {
             return 0.0;
@@ -1480,9 +1480,9 @@ extern "C" double lean_float_of_decimal(b_lean_obj_arg m, uint8 esign, b_lean_ob
         }
     }
     if (lean_is_scalar(m)) {
-        return of_decimal(mpz::of_size_t(lean_unbox(m)), esign, lean_unbox(e));
+        return of_scientific(mpz::of_size_t(lean_unbox(m)), esign, lean_unbox(e));
     } else {
-        return of_decimal(mpz_value(m), esign, lean_unbox(e));
+        return of_scientific(mpz_value(m), esign, lean_unbox(e));
     }
 }