chore: move to new frontend
This commit is contained in:
Leonardo de Moura
parent
b0cfe1ce07
commit
e53874ce45
16 changed files with 185 additions and 163 deletions
|
|
@ -1,3 +1,4 @@
|
|||
#lang lean4
|
||||
/-
|
||||
Copyright (c) 2017 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
|
|
|||
|
|
@ -1,3 +1,4 @@
|
|||
#lang lean4
|
||||
/-
|
||||
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
|
|
|||
|
|
@ -1,3 +1,4 @@
|
|||
#lang lean4
|
||||
/-
|
||||
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
|
|
|||
|
|
@ -1,3 +1,4 @@
|
|||
#lang lean4
|
||||
/-
|
||||
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
|
|
|||
|
|
@ -1,3 +1,4 @@
|
|||
#lang lean4
|
||||
/-
|
||||
Copyright (c) 2017 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
|
|
|||
|
|
@ -1,3 +1,4 @@
|
|||
#lang lean4
|
||||
/-
|
||||
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
|
@ -8,12 +9,12 @@ import Init.Core
|
|||
import Init.Data.ToString.Basic
|
||||
|
||||
structure FloatSpec :=
|
||||
(float : Type)
|
||||
(val : float)
|
||||
(lt : float → float → Prop)
|
||||
(le : float → float → Prop)
|
||||
(decLt : DecidableRel lt)
|
||||
(decLe : DecidableRel le)
|
||||
(float : Type)
|
||||
(val : float)
|
||||
(lt : float → float → Prop)
|
||||
(le : float → float → Prop)
|
||||
(decLt : DecidableRel lt)
|
||||
(decLe : DecidableRel le)
|
||||
|
||||
-- Just show FloatSpec is inhabited.
|
||||
constant floatSpec : FloatSpec := {
|
||||
|
|
@ -26,21 +27,23 @@ constant floatSpec : FloatSpec := {
|
|||
}
|
||||
|
||||
structure Float :=
|
||||
(val : floatSpec.float)
|
||||
(val : floatSpec.float)
|
||||
|
||||
instance : Inhabited Float := ⟨{ val := floatSpec.val }⟩
|
||||
|
||||
@[extern "lean_float_of_nat"] constant Float.ofNat : (@& Nat) → Float := arbitrary _
|
||||
@[extern c inline "#1 + #2"] constant Float.add : Float → Float → Float := arbitrary _
|
||||
@[extern c inline "#1 - #2"] constant Float.sub : Float → Float → Float := arbitrary _
|
||||
@[extern c inline "#1 * #2"] constant Float.mul : Float → Float → Float := arbitrary _
|
||||
@[extern c inline "#1 / #2"] constant Float.div : Float → Float → Float := arbitrary _
|
||||
@[extern "lean_float_of_nat"] constant Float.ofNat : (@& Nat) → Float
|
||||
@[extern c inline "#1 + #2"] constant Float.add : Float → Float → Float
|
||||
@[extern c inline "#1 - #2"] constant Float.sub : Float → Float → Float
|
||||
@[extern c inline "#1 * #2"] constant Float.mul : Float → Float → Float
|
||||
@[extern c inline "#1 / #2"] constant Float.div : Float → Float → Float
|
||||
|
||||
def Float.lt : Float → Float → Prop :=
|
||||
fun a b => match a, b with
|
||||
| ⟨a⟩, ⟨b⟩ => floatSpec.lt a b
|
||||
set_option bootstrap.gen_matcher_code false
|
||||
def Float.lt : Float → Float → Prop := fun a b =>
|
||||
match a, b with
|
||||
| ⟨a⟩, ⟨b⟩ => floatSpec.lt a b
|
||||
|
||||
def Float.le : Float → Float → Prop := fun a b => floatSpec.le a.val b.val
|
||||
def Float.le : Float → Float → Prop := fun a b =>
|
||||
floatSpec.le a.val b.val
|
||||
|
||||
instance : HasZero Float := ⟨Float.ofNat 0⟩
|
||||
instance : HasOne Float := ⟨Float.ofNat 1⟩
|
||||
|
|
@ -52,48 +55,48 @@ instance : HasDiv Float := ⟨Float.div⟩
|
|||
instance : HasLess Float := ⟨Float.lt⟩
|
||||
instance : HasLessEq Float := ⟨Float.le⟩
|
||||
|
||||
@[extern c inline "#1 == #2"] constant Float.beq (a b : Float) : Bool := arbitrary _
|
||||
@[extern c inline "#1 == #2"] constant Float.beq (a b : Float) : Bool
|
||||
|
||||
instance : HasBeq Float := ⟨Float.beq⟩
|
||||
|
||||
@[extern c inline "#1 < #2"] constant Float.decLt (a b : Float) : Decidable (a < b) :=
|
||||
match a, b with
|
||||
| ⟨a⟩, ⟨b⟩ => floatSpec.decLt a b
|
||||
match a, b with
|
||||
| ⟨a⟩, ⟨b⟩ => floatSpec.decLt a b
|
||||
|
||||
@[extern c inline "#1 <= #2"] constant Float.decLe (a b : Float) : Decidable (a ≤ b) :=
|
||||
match a, b with
|
||||
| ⟨a⟩, ⟨b⟩ => floatSpec.decLe a b
|
||||
match a, b with
|
||||
| ⟨a⟩, ⟨b⟩ => floatSpec.decLe a b
|
||||
|
||||
instance floatDecLt (a b : Float) : Decidable (a < b) := Float.decLt a b
|
||||
instance floatDecLe (a b : Float) : Decidable (a ≤ b) := Float.decLe a b
|
||||
|
||||
@[extern "lean_float_to_string"] constant Float.toString : Float → String := arbitrary _
|
||||
@[extern "lean_float_to_string"] constant Float.toString : Float → String
|
||||
|
||||
instance : HasToString Float := ⟨Float.toString⟩
|
||||
|
||||
abbrev Nat.toFloat (n : Nat) : Float :=
|
||||
Float.ofNat n
|
||||
Float.ofNat n
|
||||
|
||||
@[extern "sin"] constant Float.sin : Float → Float := arbitrary _
|
||||
@[extern "cos"] constant Float.cos : Float → Float := arbitrary _
|
||||
@[extern "tan"] constant Float.tan : Float → Float := arbitrary _
|
||||
@[extern "asin"] constant Float.asin : Float → Float := arbitrary _
|
||||
@[extern "acos"] constant Float.acos : Float → Float := arbitrary _
|
||||
@[extern "atan"] constant Float.atan : Float → Float := arbitrary _
|
||||
@[extern "atan2"] constant Float.atan2 : Float → Float → Float := arbitrary _
|
||||
@[extern "sinh"] constant Float.sinh : Float → Float := arbitrary _
|
||||
@[extern "cosh"] constant Float.cosh : Float → Float := arbitrary _
|
||||
@[extern "tanh"] constant Float.tanh : Float → Float := arbitrary _
|
||||
@[extern "asinh"] constant Float.asinh : Float → Float := arbitrary _
|
||||
@[extern "acosh"] constant Float.acosh : Float → Float := arbitrary _
|
||||
@[extern "atanh"] constant Float.atanh : Float → Float := arbitrary _
|
||||
@[extern "exp"] constant Float.exp : Float → Float := arbitrary _
|
||||
@[extern "exp2"] constant Float.exp2 : Float → Float := arbitrary _
|
||||
@[extern "log"] constant Float.log : Float → Float := arbitrary _
|
||||
@[extern "log2"] constant Float.log2 : Float → Float := arbitrary _
|
||||
@[extern "log10"] constant Float.log10 : Float → Float := arbitrary _
|
||||
@[extern "pow"] constant Float.pow : Float → Float → Float := arbitrary _
|
||||
@[extern "sqrt"] constant Float.sqrt : Float → Float := arbitrary _
|
||||
@[extern "cbrt"] constant Float.cbrt : Float → Float := arbitrary _
|
||||
@[extern "sin"] constant Float.sin : Float → Float
|
||||
@[extern "cos"] constant Float.cos : Float → Float
|
||||
@[extern "tan"] constant Float.tan : Float → Float
|
||||
@[extern "asin"] constant Float.asin : Float → Float
|
||||
@[extern "acos"] constant Float.acos : Float → Float
|
||||
@[extern "atan"] constant Float.atan : Float → Float
|
||||
@[extern "atan2"] constant Float.atan2 : Float → Float → Float
|
||||
@[extern "sinh"] constant Float.sinh : Float → Float
|
||||
@[extern "cosh"] constant Float.cosh : Float → Float
|
||||
@[extern "tanh"] constant Float.tanh : Float → Float
|
||||
@[extern "asinh"] constant Float.asinh : Float → Float
|
||||
@[extern "acosh"] constant Float.acosh : Float → Float
|
||||
@[extern "atanh"] constant Float.atanh : Float → Float
|
||||
@[extern "exp"] constant Float.exp : Float → Float
|
||||
@[extern "exp2"] constant Float.exp2 : Float → Float
|
||||
@[extern "log"] constant Float.log : Float → Float
|
||||
@[extern "log2"] constant Float.log2 : Float → Float
|
||||
@[extern "log10"] constant Float.log10 : Float → Float
|
||||
@[extern "pow"] constant Float.pow : Float → Float → Float
|
||||
@[extern "sqrt"] constant Float.sqrt : Float → Float
|
||||
@[extern "cbrt"] constant Float.cbrt : Float → Float
|
||||
|
||||
instance : HasPow Float Float := ⟨Float.pow⟩
|
||||
|
|
|
|||
|
|
@ -1,3 +1,4 @@
|
|||
#lang lean4
|
||||
/-
|
||||
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
|
|
|||
|
|
@ -1,3 +1,4 @@
|
|||
#lang lean4
|
||||
/-
|
||||
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
|
@ -9,32 +10,36 @@ import Init.Data.String
|
|||
universes u
|
||||
|
||||
class Hashable (α : Type u) :=
|
||||
(hash : α → USize)
|
||||
(hash : α → USize)
|
||||
|
||||
export Hashable (hash)
|
||||
|
||||
@[extern "lean_usize_mix_hash"]
|
||||
constant mixHash (u₁ u₂ : USize) : USize := arbitrary _
|
||||
constant mixHash (u₁ u₂ : USize) : USize
|
||||
|
||||
@[extern "lean_string_hash"]
|
||||
protected constant String.hash (s : @& String) : USize := arbitrary _
|
||||
protected constant String.hash (s : @& String) : USize
|
||||
|
||||
instance : Hashable String := ⟨String.hash⟩
|
||||
|
||||
protected def Nat.hash (n : Nat) : USize :=
|
||||
USize.ofNat n
|
||||
instance : Hashable Nat := {
|
||||
hash := fun n => USize.ofNat n
|
||||
}
|
||||
|
||||
instance : Hashable Nat := ⟨Nat.hash⟩
|
||||
instance {α β} [Hashable α] [Hashable β] : Hashable (α × β) := {
|
||||
hash := fun (a, b) => mixHash (hash a) (hash b)
|
||||
}
|
||||
|
||||
instance {α β} [Hashable α] [Hashable β] : Hashable (α × β) :=
|
||||
⟨fun ⟨a, b⟩ => mixHash (hash a) (hash b)⟩
|
||||
protected def Option.hash {α} [Hashable α] : Option α → USize
|
||||
| none => 11
|
||||
| some a => mixHash (hash a) 13
|
||||
|
||||
def Option.hash {α} [Hashable α] : Option α → USize
|
||||
| none => 11
|
||||
| some a => mixHash (hash a) 13
|
||||
instance {α} [Hashable α] : Hashable (Option α) := {
|
||||
hash := fun
|
||||
| none => 11
|
||||
| some a => mixHash (hash a) 13
|
||||
}
|
||||
|
||||
instance {α} [Hashable α] : Hashable (Option α) := ⟨Option.hash⟩
|
||||
|
||||
def List.hash {α} [Hashable α] (as : List α) : USize :=
|
||||
as.foldl (fun r a => mixHash r (hash a)) 7
|
||||
|
||||
instance {α} [Hashable α] : Hashable (List α) := ⟨List.hash⟩
|
||||
instance {α} [Hashable α] : Hashable (List α) := {
|
||||
hash := fun as => as.foldl (fun r a => mixHash r (hash a)) 7
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,3 +1,4 @@
|
|||
#lang lean4
|
||||
/-
|
||||
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
|
|
|||
|
|
@ -1,3 +1,4 @@
|
|||
#lang lean4
|
||||
/-
|
||||
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
|
|
|||
|
|
@ -1,3 +1,4 @@
|
|||
#lang lean4
|
||||
/-
|
||||
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
|
|
|||
|
|
@ -1,3 +1,4 @@
|
|||
#lang lean4
|
||||
/-
|
||||
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
|
|
|||
|
|
@ -1,3 +1,4 @@
|
|||
#lang lean4
|
||||
/-
|
||||
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
|
@ -5,29 +6,28 @@ Authors: Leonardo de Moura
|
|||
-/
|
||||
prelude
|
||||
import Init.LeanInit
|
||||
new_frontend
|
||||
|
||||
namespace Std
|
||||
-- We put `Range` in `Init` because we want the notation `[i:j]` without importing `Std`
|
||||
-- We don't put `Range` in the top-level namespace to avoid collisions with user defined types
|
||||
structure Range :=
|
||||
(start : Nat := 0)
|
||||
(stop : Nat)
|
||||
(step : Nat := 1)
|
||||
(start : Nat := 0)
|
||||
(stop : Nat)
|
||||
(step : Nat := 1)
|
||||
|
||||
namespace Range
|
||||
universes u v
|
||||
|
||||
@[inline] def forIn {β : Type u} {m : Type u → Type v} [Monad m] (range : Range) (init : β) (f : Nat → β → m (ForInStep β)) : m β :=
|
||||
let rec @[specialize] loop (i : Nat) (j : Nat) (b : β) : m β := do
|
||||
if j ≥ range.stop then
|
||||
pure b
|
||||
else match i with
|
||||
| 0 => pure b
|
||||
| i+1 => match ← f j b with
|
||||
| ForInStep.done b => pure b
|
||||
| ForInStep.yield b => loop i (j + range.step) b
|
||||
loop range.stop range.start init
|
||||
let rec @[specialize] loop (i : Nat) (j : Nat) (b : β) : m β := do
|
||||
if j ≥ range.stop then
|
||||
pure b
|
||||
else match i with
|
||||
| 0 => pure b
|
||||
| i+1 => match ← f j b with
|
||||
| ForInStep.done b => pure b
|
||||
| ForInStep.yield b => loop i (j + range.step) b
|
||||
loop range.stop range.start init
|
||||
|
||||
syntax:max "[" ":" term "]" : term
|
||||
syntax:max "[" term ":" term "]" : term
|
||||
|
|
@ -35,10 +35,10 @@ syntax:max "[" ":" term ":" term "]" : term
|
|||
syntax:max "[" term ":" term ":" term "]" : term
|
||||
|
||||
macro_rules
|
||||
| `([ : $stop]) => `({ stop := $stop : Range })
|
||||
| `([ $start : $stop ]) => `({ start := $start, stop := $stop : Range })
|
||||
| `([ $start : $stop : $step ]) => `({ start := $start, stop := $stop, step := $step : Range })
|
||||
| `([ : $stop : $step ]) => `({ stop := $stop, step := $step : Range })
|
||||
| `([ : $stop]) => `({ stop := $stop : Range })
|
||||
| `([ $start : $stop ]) => `({ start := $start, stop := $stop : Range })
|
||||
| `([ $start : $stop : $step ]) => `({ start := $start, stop := $stop, step := $step : Range })
|
||||
| `([ : $stop : $step ]) => `({ stop := $stop, step := $step : Range })
|
||||
|
||||
end Range
|
||||
end Std
|
||||
|
|
|
|||
|
|
@ -1,3 +1,4 @@
|
|||
#lang lean4
|
||||
/-
|
||||
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
|
@ -13,167 +14,168 @@ open Sum Subtype Nat
|
|||
universes u v
|
||||
|
||||
class HasRepr (α : Type u) :=
|
||||
(repr : α → String)
|
||||
(repr : α → String)
|
||||
|
||||
export HasRepr (repr)
|
||||
|
||||
-- This instance is needed because `id` is not reducible
|
||||
instance {α : Type u} [HasRepr α] : HasRepr (id α) :=
|
||||
inferInstanceAs (HasRepr α)
|
||||
inferInstanceAs (HasRepr α)
|
||||
|
||||
instance : HasRepr Bool :=
|
||||
⟨fun b => cond b "true" "false"⟩
|
||||
⟨fun b => cond b "true" "false"⟩
|
||||
|
||||
instance {α} [HasRepr α] : HasRepr (Id α) :=
|
||||
inferInstanceAs (HasRepr α)
|
||||
inferInstanceAs (HasRepr α)
|
||||
|
||||
instance {p : Prop} : HasRepr (Decidable p) :=
|
||||
⟨fun h => match h with
|
||||
instance {p : Prop} : HasRepr (Decidable p) := {
|
||||
repr := fun h => match h with
|
||||
| Decidable.isTrue _ => "true"
|
||||
| Decidable.isFalse _ => "false"⟩
|
||||
| Decidable.isFalse _ => "false"
|
||||
}
|
||||
|
||||
protected def List.reprAux {α : Type u} [HasRepr α] : Bool → List α → String
|
||||
| b, [] => ""
|
||||
| true, x::xs => repr x ++ List.reprAux false xs
|
||||
| false, x::xs => ", " ++ repr x ++ List.reprAux false xs
|
||||
| b, [] => ""
|
||||
| true, x::xs => repr x ++ List.reprAux false xs
|
||||
| false, x::xs => ", " ++ repr x ++ List.reprAux false xs
|
||||
|
||||
protected def List.repr {α : Type u} [HasRepr α] : List α → String
|
||||
| [] => "[]"
|
||||
| x::xs => "[" ++ List.reprAux true (x::xs) ++ "]"
|
||||
| [] => "[]"
|
||||
| x::xs => "[" ++ List.reprAux true (x::xs) ++ "]"
|
||||
|
||||
instance {α : Type u} [HasRepr α] : HasRepr (List α) :=
|
||||
⟨List.repr⟩
|
||||
⟨List.repr⟩
|
||||
|
||||
instance : HasRepr PUnit.{u+1} :=
|
||||
⟨fun u => "PUnit.unit"⟩
|
||||
⟨fun u => "PUnit.unit"⟩
|
||||
|
||||
instance {α : Type u} [HasRepr α] : HasRepr (ULift.{v} α) :=
|
||||
⟨fun v => "ULift.up (" ++ repr v.1 ++ ")"⟩
|
||||
⟨fun v => "ULift.up (" ++ repr v.1 ++ ")"⟩
|
||||
|
||||
instance : HasRepr Unit :=
|
||||
⟨fun u => "()"⟩
|
||||
⟨fun u => "()"⟩
|
||||
|
||||
instance {α : Type u} [HasRepr α] : HasRepr (Option α) :=
|
||||
⟨fun o => match o with | none => "none" | (some a) => "(some " ++ repr a ++ ")"⟩
|
||||
⟨fun | none => "none" | (some a) => "(some " ++ repr a ++ ")"⟩
|
||||
|
||||
instance {α : Type u} {β : Type v} [HasRepr α] [HasRepr β] : HasRepr (Sum α β) :=
|
||||
⟨fun s => match s with | (inl a) => "(inl " ++ repr a ++ ")" | (inr b) => "(inr " ++ repr b ++ ")"⟩
|
||||
⟨fun | (inl a) => "(inl " ++ repr a ++ ")" | (inr b) => "(inr " ++ repr b ++ ")"⟩
|
||||
|
||||
instance {α : Type u} {β : Type v} [HasRepr α] [HasRepr β] : HasRepr (α × β) :=
|
||||
⟨fun ⟨a, b⟩ => "(" ++ repr a ++ ", " ++ repr b ++ ")"⟩
|
||||
⟨fun ⟨a, b⟩ => "(" ++ repr a ++ ", " ++ repr b ++ ")"⟩
|
||||
|
||||
instance {α : Type u} {β : α → Type v} [HasRepr α] [s : ∀ x, HasRepr (β x)] : HasRepr (Sigma β) :=
|
||||
⟨fun ⟨a, b⟩ => "⟨" ++ repr a ++ ", " ++ repr b ++ "⟩"⟩
|
||||
⟨fun ⟨a, b⟩ => "⟨" ++ repr a ++ ", " ++ repr b ++ "⟩"⟩
|
||||
|
||||
instance {α : Type u} {p : α → Prop} [HasRepr α] : HasRepr (Subtype p) :=
|
||||
⟨fun s => repr (val s)⟩
|
||||
⟨fun s => repr (val s)⟩
|
||||
|
||||
namespace Nat
|
||||
|
||||
def digitChar (n : Nat) : Char :=
|
||||
if n = 0 then '0' else
|
||||
if n = 1 then '1' else
|
||||
if n = 2 then '2' else
|
||||
if n = 3 then '3' else
|
||||
if n = 4 then '4' else
|
||||
if n = 5 then '5' else
|
||||
if n = 6 then '6' else
|
||||
if n = 7 then '7' else
|
||||
if n = 8 then '8' else
|
||||
if n = 9 then '9' else
|
||||
if n = 0xa then 'a' else
|
||||
if n = 0xb then 'b' else
|
||||
if n = 0xc then 'c' else
|
||||
if n = 0xd then 'd' else
|
||||
if n = 0xe then 'e' else
|
||||
if n = 0xf then 'f' else
|
||||
'*'
|
||||
if n = 0 then '0' else
|
||||
if n = 1 then '1' else
|
||||
if n = 2 then '2' else
|
||||
if n = 3 then '3' else
|
||||
if n = 4 then '4' else
|
||||
if n = 5 then '5' else
|
||||
if n = 6 then '6' else
|
||||
if n = 7 then '7' else
|
||||
if n = 8 then '8' else
|
||||
if n = 9 then '9' else
|
||||
if n = 0xa then 'a' else
|
||||
if n = 0xb then 'b' else
|
||||
if n = 0xc then 'c' else
|
||||
if n = 0xd then 'd' else
|
||||
if n = 0xe then 'e' else
|
||||
if n = 0xf then 'f' else
|
||||
'*'
|
||||
|
||||
def toDigitsCore (base : Nat) : Nat → Nat → List Char → List Char
|
||||
| 0, n, ds => ds
|
||||
| fuel+1, n, ds =>
|
||||
let d := digitChar $ n % base;
|
||||
let n' := n / base;
|
||||
if n' = 0 then d::ds
|
||||
else toDigitsCore fuel n' (d::ds)
|
||||
| 0, n, ds => ds
|
||||
| fuel+1, n, ds =>
|
||||
let d := digitChar $ n % base;
|
||||
let n' := n / base;
|
||||
if n' = 0 then d::ds
|
||||
else toDigitsCore base fuel n' (d::ds)
|
||||
|
||||
def toDigits (base : Nat) (n : Nat) : List Char :=
|
||||
toDigitsCore base (n+1) n []
|
||||
toDigitsCore base (n+1) n []
|
||||
|
||||
protected def repr (n : Nat) : String :=
|
||||
(toDigits 10 n).asString
|
||||
(toDigits 10 n).asString
|
||||
|
||||
def superDigitChar (n : Nat) : Char :=
|
||||
if n = 0 then '⁰' else
|
||||
if n = 1 then '¹' else
|
||||
if n = 2 then '²' else
|
||||
if n = 3 then '³' else
|
||||
if n = 4 then '⁴' else
|
||||
if n = 5 then '⁵' else
|
||||
if n = 6 then '⁶' else
|
||||
if n = 7 then '⁷' else
|
||||
if n = 8 then '⁸' else
|
||||
if n = 9 then '⁹' else
|
||||
'*'
|
||||
if n = 0 then '⁰' else
|
||||
if n = 1 then '¹' else
|
||||
if n = 2 then '²' else
|
||||
if n = 3 then '³' else
|
||||
if n = 4 then '⁴' else
|
||||
if n = 5 then '⁵' else
|
||||
if n = 6 then '⁶' else
|
||||
if n = 7 then '⁷' else
|
||||
if n = 8 then '⁸' else
|
||||
if n = 9 then '⁹' else
|
||||
'*'
|
||||
|
||||
partial def toSuperDigitsAux : Nat → List Char → List Char
|
||||
| n, ds =>
|
||||
let d := superDigitChar $ n % 10;
|
||||
let n' := n / 10;
|
||||
if n' = 0 then d::ds
|
||||
else toSuperDigitsAux n' (d::ds)
|
||||
| n, ds =>
|
||||
let d := superDigitChar $ n % 10;
|
||||
let n' := n / 10;
|
||||
if n' = 0 then d::ds
|
||||
else toSuperDigitsAux n' (d::ds)
|
||||
|
||||
def toSuperDigits (n : Nat) : List Char :=
|
||||
toSuperDigitsAux n []
|
||||
toSuperDigitsAux n []
|
||||
|
||||
def toSuperscriptString (n : Nat) : String :=
|
||||
(toSuperDigits n).asString
|
||||
(toSuperDigits n).asString
|
||||
|
||||
end Nat
|
||||
|
||||
instance : HasRepr Nat :=
|
||||
⟨Nat.repr⟩
|
||||
⟨Nat.repr⟩
|
||||
|
||||
def hexDigitRepr (n : Nat) : String :=
|
||||
String.singleton $ Nat.digitChar n
|
||||
String.singleton $ Nat.digitChar n
|
||||
|
||||
def charToHex (c : Char) : String :=
|
||||
let n := Char.toNat c;
|
||||
let d2 := n / 16;
|
||||
let d1 := n % 16;
|
||||
hexDigitRepr d2 ++ hexDigitRepr d1
|
||||
let n := Char.toNat c;
|
||||
let d2 := n / 16;
|
||||
let d1 := n % 16;
|
||||
hexDigitRepr d2 ++ hexDigitRepr d1
|
||||
|
||||
def Char.quoteCore (c : Char) : String :=
|
||||
if c = '\n' then "\\n"
|
||||
else if c = '\t' then "\\t"
|
||||
else if c = '\\' then "\\\\"
|
||||
else if c = '\"' then "\\\""
|
||||
else if c.toNat <= 31 ∨ c = '\x7f' then "\\x" ++ charToHex c
|
||||
else String.singleton c
|
||||
if c = '\n' then "\\n"
|
||||
else if c = '\t' then "\\t"
|
||||
else if c = '\\' then "\\\\"
|
||||
else if c = '\"' then "\\\""
|
||||
else if c.toNat <= 31 ∨ c = '\x7f' then "\\x" ++ charToHex c
|
||||
else String.singleton c
|
||||
|
||||
instance : HasRepr Char :=
|
||||
⟨fun c => "'" ++ Char.quoteCore c ++ "'"⟩
|
||||
⟨fun c => "'" ++ Char.quoteCore c ++ "'"⟩
|
||||
|
||||
def String.quote (s : String) : String :=
|
||||
if s.isEmpty = true then "\"\""
|
||||
else s.foldl (fun s c => s ++ c.quoteCore) "\"" ++ "\""
|
||||
if s.isEmpty = true then "\"\""
|
||||
else s.foldl (fun s c => s ++ c.quoteCore) "\"" ++ "\""
|
||||
|
||||
instance : HasRepr String :=
|
||||
⟨String.quote⟩
|
||||
⟨String.quote⟩
|
||||
|
||||
instance : HasRepr Substring :=
|
||||
⟨fun s => String.quote s.toString ++ ".toSubstring"⟩
|
||||
⟨fun s => String.quote s.toString ++ ".toSubstring"⟩
|
||||
|
||||
instance : HasRepr String.Iterator :=
|
||||
⟨fun ⟨s, pos⟩ => "(String.Iterator.mk " ++ repr s ++ " " ++ repr pos ++ ")"⟩
|
||||
⟨fun ⟨s, pos⟩ => "(String.Iterator.mk " ++ repr s ++ " " ++ repr pos ++ ")"⟩
|
||||
|
||||
instance (n : Nat) : HasRepr (Fin n) :=
|
||||
⟨fun f => repr (Fin.val f)⟩
|
||||
⟨fun f => repr (Fin.val f)⟩
|
||||
|
||||
instance : HasRepr UInt16 := ⟨fun n => repr n.toNat⟩
|
||||
instance : HasRepr UInt32 := ⟨fun n => repr n.toNat⟩
|
||||
instance : HasRepr UInt64 := ⟨fun n => repr n.toNat⟩
|
||||
instance : HasRepr USize := ⟨fun n => repr n.toNat⟩
|
||||
|
||||
def Char.repr (c : Char) : String :=
|
||||
repr c
|
||||
protected def Char.repr (c : Char) : String :=
|
||||
repr c
|
||||
|
|
|
|||
|
|
@ -1,3 +1,4 @@
|
|||
#lang lean4
|
||||
/-
|
||||
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
|
|
|||
|
|
@ -1,3 +1,4 @@
|
|||
#lang lean4
|
||||
/-
|
||||
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue