From b95c4788c1f7372ade538ddf663fe1938caac6da Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 3 Dec 2020 08:06:45 -0800 Subject: [PATCH] refactor: `OfDecimal` ==> `OfScientific` `decimalLit` ==> `scientificLit` --- src/Init/Data.lean | 2 +- src/Init/Data/Float.lean | 2 +- src/Init/Data/OfDecimal.lean | 20 ------------------- src/Init/Data/OfScientific.lean | 20 +++++++++++++++++++ src/Init/Meta.lean | 12 +++++------ src/Init/Prelude.lean | 2 +- src/Lean/Elab/Match.lean | 2 +- src/Lean/Elab/Term.lean | 9 +++++---- src/Lean/Parser.lean | 4 ++-- src/Lean/Parser/Basic.lean | 18 ++++++++--------- src/Lean/Parser/Extension.lean | 2 +- src/Lean/Parser/Extra.lean | 2 +- src/Lean/Parser/Term.lean | 2 +- .../PrettyPrinter/Delaborator/Builtins.lean | 10 +++++----- src/Lean/PrettyPrinter/Formatter.lean | 4 ++-- src/Lean/PrettyPrinter/Parenthesizer.lean | 4 ++-- src/runtime/object.cpp | 8 ++++---- 17 files changed, 62 insertions(+), 61 deletions(-) delete mode 100644 src/Init/Data/OfDecimal.lean create mode 100644 src/Init/Data/OfScientific.lean diff --git a/src/Init/Data.lean b/src/Init/Data.lean index 629f75eea7..cbde3a49c9 100644 --- a/src/Init/Data.lean +++ b/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 diff --git a/src/Init/Data/Float.lean b/src/Init/Data/Float.lean index a39bd19c4e..6595667409 100644 --- a/src/Init/Data/Float.lean +++ b/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 diff --git a/src/Init/Data/OfDecimal.lean b/src/Init/Data/OfDecimal.lean deleted file mode 100644 index a4d097a140..0000000000 --- a/src/Init/Data/OfDecimal.lean +++ /dev/null @@ -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 diff --git a/src/Init/Data/OfScientific.lean b/src/Init/Data/OfScientific.lean new file mode 100644 index 0000000000..bc8cb38af7 --- /dev/null +++ b/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 diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean index 93f52815bb..369a4da488 100644 --- a/src/Init/Meta.lean +++ b/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 diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index ec4c86ea1c..1df0eef242 100644 --- a/src/Init/Prelude.lean +++ b/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 diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean index 890aa8091b..1483061cc9 100644 --- a/src/Lean/Elab/Match.lean +++ b/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 diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index f738714a39..dcce840daf 100644 --- a/src/Lean/Elab/Term.lean +++ b/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 diff --git a/src/Lean/Parser.lean b/src/Lean/Parser.lean index 5f30dfd520..1b57e2a7d8 100644 --- a/src/Lean/Parser.lean +++ b/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 diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean index 3b88a6d5ed..ce19859be4 100644 --- a/src/Lean/Parser/Basic.lean +++ b/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 diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean index 2cb0e6e232..fe055579e4 100644 --- a/src/Lean/Parser/Extension.lean +++ b/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 diff --git a/src/Lean/Parser/Extra.lean b/src/Lean/Parser/Extra.lean index 72074297e9..38d99c19a6 100644 --- a/src/Lean/Parser/Extra.lean +++ b/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 diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index e221ac93e9..0a0df6c35a 100644 --- a/src/Lean/Parser/Term.lean +++ b/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) diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean index de39e99760..8437b60ae8 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/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 diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean index cd37af46bf..3fbd84c86b 100644 --- a/src/Lean/PrettyPrinter/Formatter.lean +++ b/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) diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean index e22aab6c59..7b4e40e697 100644 --- a/src/Lean/PrettyPrinter/Parenthesizer.lean +++ b/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) diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp index fd5cc71ff5..a2b81ecb44 100644 --- a/src/runtime/object.cpp +++ b/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)); } }