From f7aeeaf237db7a2500620f485dec88405bfc06a4 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 20 Mar 2019 17:28:38 +0100 Subject: [PATCH] exclude export/extern, translate constants.txt --- library/init/core.lean | 22 +- library/init/data/array/basic.lean | 28 +-- library/init/data/char/basic.lean | 2 +- library/init/data/int/basic.lean | 24 +-- library/init/data/nat/basic.lean | 16 +- library/init/data/nat/div.lean | 4 +- library/init/data/string/basic.lean | 28 +-- library/init/data/uint.lean | 30 +-- library/init/io.lean | 30 +-- library/init/lean/elaborator.lean | 6 +- library/init/lean/expr.lean | 28 +-- library/init/lean/extern.lean | 8 +- library/init/lean/frontend.lean | 2 +- library/init/lean/level.lean | 12 +- library/init/lean/name.lean | 8 +- library/init/lean/util.lean | 2 +- library/init/util.lean | 4 +- script/camel.py | 4 +- script/camel.sh | 1 + src/library/constants.txt | 318 ++++++++++++++-------------- 20 files changed, 289 insertions(+), 288 deletions(-) diff --git a/library/init/core.lean b/library/init/core.lean index f0e99bc1f8..765f502677 100644 --- a/library/init/core.lean +++ b/library/init/core.lean @@ -141,18 +141,18 @@ abbrev unit : Type := punit structure thunk (α : Type u) : Type u := (fn : unit → α) -attribute [extern cpp inline "lean::mkThunk(#2)"] thunk.mk +attribute [extern cpp inline "lean::mk_thunk(#2)"] thunk.mk -@[noinline, extern cpp inline "lean::thunkPure(#2)"] +@[noinline, extern cpp inline "lean::thunk_pure(#2)"] protected def thunk.pure {α : Type u} (a : α) : thunk α := ⟨λ _, a⟩ -@[noinline, extern cpp inline "lean::thunkGet(#2)"] +@[noinline, extern cpp inline "lean::thunk_get(#2)"] protected def thunk.get {α : Type u} (x : @& thunk α) : α := x.fn () -@[noinline, extern cpp inline "lean::thunkMap(#3, #4)"] +@[noinline, extern cpp inline "lean::thunk_map(#3, #4)"] protected def thunk.map {α : Type u} {β : Type v} (f : α → β) (x : thunk α) : thunk β := ⟨λ _, f x.get⟩ -@[noinline, extern cpp inline "lean::thunkBind(#3, #4)"] +@[noinline, extern cpp inline "lean::thunk_bind(#3, #4)"] protected def thunk.bind {α : Type u} {β : Type v} (x : thunk α) (f : α → thunk β) : thunk β := ⟨λ _, (f x.get).get⟩ @@ -160,18 +160,18 @@ protected def thunk.bind {α : Type u} {β : Type v} (x : thunk α) (f : α → structure task (α : Type u) : Type u := (fn : unit → α) -attribute [extern cpp inline "lean::mkTask(#2)"] task.mk +attribute [extern cpp inline "lean::mk_task(#2)"] task.mk -@[noinline, extern cpp inline "lean::taskPure(#2)"] +@[noinline, extern cpp inline "lean::task_pure(#2)"] protected def task.pure {α : Type u} (a : α) : task α := ⟨λ _, a⟩ -@[noinline, extern cpp inline "lean::taskGet(#2)"] +@[noinline, extern cpp inline "lean::task_get(#2)"] protected def task.get {α : Type u} (x : @& task α) : α := x.fn () -@[noinline, extern cpp inline "lean::taskMap(#3, #4)"] +@[noinline, extern cpp inline "lean::task_map(#3, #4)"] protected def task.map {α : Type u} {β : Type v} (f : α → β) (x : task α) : task β := ⟨λ _, f x.get⟩ -@[noinline, extern cpp inline "lean::taskBind(#3, #4)"] +@[noinline, extern cpp inline "lean::task_bind(#3, #4)"] protected def task.bind {α : Type u} {β : Type v} (x : task α) (f : α → task β) : task β := ⟨λ _, (f x.get).get⟩ @@ -439,7 +439,7 @@ export hasInsert (insert) hasInsert.insert a ∅ /- nat basic instances -/ -@[extern cpp "lean::natAdd"] +@[extern cpp "lean::nat_add"] protected def nat.add : (@& nat) → (@& nat) → nat | a nat.zero := a | a (nat.succ b) := nat.succ (nat.add a b) diff --git a/library/init/data/array/basic.lean b/library/init/data/array/basic.lean index 43294c238a..be8268966e 100644 --- a/library/init/data/array/basic.lean +++ b/library/init/data/array/basic.lean @@ -18,13 +18,13 @@ structure array (α : Type u) := (sz : nat) (data : fin sz → α) -attribute [extern cpp inline "lean::arraySz(#2)"] array.sz +attribute [extern cpp inline "lean::array_sz(#2)"] array.sz -@[extern cpp inline "lean::arrayGetSize(#2)"] +@[extern cpp inline "lean::array_get_size(#2)"] def array.size {α : Type u} (a : @& array α) : nat := a.sz -@[extern cpp inline "lean::mkArray(#2, #3)"] +@[extern cpp inline "lean::mk_array(#2, #3)"] def mkArray {α : Type u} (n : nat) (v : α) : array α := { sz := n, data := λ _, v} @@ -35,7 +35,7 @@ rfl namespace array variables {α : Type u} {β : Type v} -@[extern cpp inline "lean::mkNilArray()"] +@[extern cpp inline "lean::mk_nil_array()"] def mkNil (_ : unit) : array α := { sz := 0, data := λ ⟨x, h⟩, absurd h (nat.notLtZero x) } @@ -46,11 +46,11 @@ mkNil () def empty (a : array α) : bool := a.size = 0 -@[extern cpp inline "lean::arrayRead(#2, #3)"] +@[extern cpp inline "lean::array_read(#2, #3)"] def read (a : @& array α) (i : @& fin a.sz) : α := a.data i -@[extern cpp inline "lean::arrayWrite(#2, #3, #4)"] +@[extern cpp inline "lean::array_write(#2, #3, #4)"] def write (a : array α) (i : @& fin a.sz) (v : α) : array α := { sz := a.sz, data := λ j, if h : i = j then v else a.data j } @@ -58,38 +58,38 @@ def write (a : array α) (i : @& fin a.sz) (v : α) : array α := theorem szWriteEq (a : array α) (i : fin a.sz) (v : α) : (write a i v).sz = a.sz := rfl -@[extern cpp inline "lean::arraySafeRead(#2, #3, #4)"] +@[extern cpp inline "lean::array_safe_read(#2, #3, #4)"] def read' [inhabited α] (a : @& array α) (i : @& nat) : α := if h : i < a.sz then a.read ⟨i, h⟩ else default α -@[extern cpp inline "lean::arraySafeWrite(#2, #3, #4)"] +@[extern cpp inline "lean::array_safe_write(#2, #3, #4)"] def write' (a : array α) (i : @& nat) (v : α) : array α := if h : i < a.sz then a.write ⟨i, h⟩ v else a -@[extern cpp inline "lean::arrayUread(#2, #3)"] +@[extern cpp inline "lean::array_uread(#2, #3)"] def uread (a : @& array α) (i : usize) (h : i.toNat < a.sz) : α := a.read ⟨i.toNat, h⟩ -@[extern cpp inline "lean::arrayUwrite(#2, #3, #4)"] +@[extern cpp inline "lean::array_uwrite(#2, #3, #4)"] def uwrite (a : @& array α) (i : usize) (v : @& α) (h : i.toNat < a.sz) : array α := a.write ⟨i.toNat, h⟩ v -@[extern cpp inline "lean::arraySafeUread(#2, #3, #4)"] +@[extern cpp inline "lean::array_safe_uread(#2, #3, #4)"] def uread' [inhabited α] (a : array α) (i : usize) : α := if h : i.toNat < a.sz then a.read ⟨i.toNat, h⟩ else default α -@[extern cpp inline "lean::arraySafeUwrite(#2, #3, #4)"] +@[extern cpp inline "lean::array_safe_uwrite(#2, #3, #4)"] def uwrite' (a : array α) (i : usize) (v : α) : array α := if h : i.toNat < a.sz then a.write ⟨i.toNat, h⟩ v else a -@[extern cpp inline "lean::arrayPush(#2, #3)"] +@[extern cpp inline "lean::array_push(#2, #3)"] def push (a : array α) (v : α) : array α := { sz := nat.succ a.sz, data := λ ⟨j, h₁⟩, if h₂ : j = a.sz then v else a.data ⟨j, nat.ltOfLeOfNe (nat.leOfLtSucc h₁) h₂⟩ } -@[extern cpp inline "lean::arrayPop(#2)"] +@[extern cpp inline "lean::array_pop(#2)"] def pop (a : array α) : array α := { sz := nat.pred a.sz, data := λ ⟨j, h⟩, a.read ⟨j, nat.ltOfLtOfLe h (nat.predLe _)⟩ } diff --git a/library/init/data/char/basic.lean b/library/init/data/char/basic.lean index 8896c7a506..238ce8b50d 100644 --- a/library/init/data/char/basic.lean +++ b/library/init/data/char/basic.lean @@ -9,7 +9,7 @@ import init.data.uint n < 0xd800 ∨ (0xdfff < n ∧ n < 0x110000) /-- The `char` type represents an unicode scalar value. - See http://www.unicode.org/glossary/#unicodeScalarValue). -/ + See http://www.unicode.org/glossary/#unicode_scalar_value). -/ structure char := (val : uint32) (valid : isValidChar val) diff --git a/library/init/data/int/basic.lean b/library/init/data/int/basic.lean index 6b2f80c202..b3ddbb065d 100644 --- a/library/init/data/int/basic.lean +++ b/library/init/data/int/basic.lean @@ -16,7 +16,7 @@ inductive int : Type | negSuccOfNat : nat → int attribute [extern cpp "lean::nat2int"] int.ofNat -attribute [extern cpp "lean::intNegSuccOfNat"] int.negSuccOfNat +attribute [extern cpp "lean::int_neg_succ_of_nat"] int.negSuccOfNat notation `ℤ` := int @@ -39,7 +39,7 @@ def negOfNat : nat → int | 0 := 0 | (succ m) := -[1+ m] -@[extern cpp "lean::intNeg"] +@[extern cpp "lean::int_neg"] protected def neg (n : @& int) : int := match n with | (ofNat n) := negOfNat n @@ -50,7 +50,7 @@ match (n - m : nat) with | 0 := ofNat (m - n) -- m ≥ n | (succ k) := -[1+ k] -- m < n, and n - m = succ k -@[extern cpp "lean::intAdd"] +@[extern cpp "lean::int_add"] protected def add (m n : @& int) : int := match m, n with | (ofNat m), (ofNat n) := ofNat (m + n) @@ -58,7 +58,7 @@ match m, n with | -[1+ m], (ofNat n) := subNatNat n (succ m) | -[1+ m], -[1+ n] := -[1+ succ (m + n)] -@[extern cpp "lean::intMul"] +@[extern cpp "lean::int_mul"] protected def mul (m n : @& int) : int := match m, n with | (ofNat m), (ofNat n) := ofNat (m * n) @@ -70,7 +70,7 @@ instance : hasNeg int := ⟨int.neg⟩ instance : hasAdd int := ⟨int.add⟩ instance : hasMul int := ⟨int.mul⟩ -@[extern cpp "lean::intSub"] +@[extern cpp "lean::int_sub"] protected def sub (m n : @& int) : int := m + -n @@ -84,7 +84,7 @@ protected def lt (a b : int) : Prop := (a + 1) ≤ b instance : hasLt int := ⟨int.lt⟩ -@[extern cpp "lean::intDecEq"] +@[extern cpp "lean::int_dec_eq"] protected def decEq (a b : @& int) : decidable (a = b) := match a, b with | (ofNat a), (ofNat b) := @@ -99,21 +99,21 @@ match a, b with instance int.decidableEq : decidableEq int := {decEq := int.decEq} -@[extern cpp "lean::intDecNonneg"] +@[extern cpp "lean::int_dec_nonneg"] private def decNonneg (m : @& int) : decidable (nonneg m) := match m with | (ofNat m) := show decidable true, from inferInstance | -[1+ m] := show decidable false, from inferInstance -@[extern cpp "lean::intDecLe"] +@[extern cpp "lean::int_dec_le"] instance decLe (a b : @& int) : decidable (a ≤ b) := decNonneg _ -@[extern cpp "lean::intDecLt"] +@[extern cpp "lean::int_dec_lt"] instance decLt (a b : @& int) : decidable (a < b) := decNonneg _ -@[extern cpp "lean::natAbs"] +@[extern cpp "lean::nat_abs"] def natAbs (m : @& int) : nat := match m with | (ofNat m) := m @@ -134,14 +134,14 @@ def sign : int → int | 0 := 0 | -[1+ n] := -1 -@[extern cpp "lean::intDiv"] +@[extern cpp "lean::int_div"] def div : (@& int) → (@& int) → int | (ofNat m) (ofNat n) := ofNat (m / n) | (ofNat m) -[1+ n] := -ofNat (m / succ n) | -[1+ m] (ofNat n) := -ofNat (succ m / n) | -[1+ m] -[1+ n] := ofNat (succ m / succ n) -@[extern cpp "lean::intMod"] +@[extern cpp "lean::int_mod"] def mod : (@& int) → (@& int) → int | (ofNat m) (ofNat n) := ofNat (m % n) | (ofNat m) -[1+ n] := ofNat (m % succ n) diff --git a/library/init/data/nat/basic.lean b/library/init/data/nat/basic.lean index 11a1a4fc98..eea707fb30 100644 --- a/library/init/data/nat/basic.lean +++ b/library/init/data/nat/basic.lean @@ -11,7 +11,7 @@ notation `ℕ` := nat namespace nat -@[extern cpp "lean::natDecEq"] +@[extern cpp "lean::nat_dec_eq"] def beq : nat → nat → bool | zero zero := tt | zero (succ m) := ff @@ -36,7 +36,7 @@ theorem neOfBeqEqFf : ∀ {n m : nat}, beq n m = ff → n ≠ m have n ≠ m, from neOfBeqEqFf this, nat.noConfusion h₂ (λ h₂, absurd h₂ this) -@[extern cpp "lean::natDecEq"] +@[extern cpp "lean::nat_dec_eq"] protected def decEq (n m : @& nat) : decidable (n = m) := if h : beq n m = tt then isTrue (eqOfBeqEqTt h) else isFalse (neOfBeqEqFf (eqFfOfNeTt h)) @@ -44,7 +44,7 @@ else isFalse (neOfBeqEqFf (eqFfOfNeTt h)) @[inline] instance : decidableEq nat := {decEq := nat.decEq} -@[extern cpp "lean::natDecLe"] +@[extern cpp "lean::nat_dec_le"] def ble : nat → nat → bool | zero zero := tt | zero (succ m) := tt @@ -63,17 +63,17 @@ nat.le (succ n) m instance : hasLt nat := ⟨nat.lt⟩ -@[extern cpp inline "lean::natSub(#1, lean::box(1))"] +@[extern cpp inline "lean::nat_sub(#1, lean::box(1))"] def pred : nat → nat | 0 := 0 | (a+1) := a -@[extern cpp "lean::natSub"] +@[extern cpp "lean::nat_sub"] protected def sub : (@& nat) → (@& nat) → nat | a 0 := a | a (b+1) := pred (sub a b) -@[extern cpp "lean::natMul"] +@[extern cpp "lean::nat_mul"] protected def mul : (@& nat) → (@& nat) → nat | a 0 := 0 | a (b+1) := (mul a b) + a @@ -259,11 +259,11 @@ theorem predLePred : ∀ {n m : nat}, n ≤ m → pred n ≤ pred m theorem leOfSuccLeSucc {n m : nat} : succ n ≤ succ m → n ≤ m := predLePred -@[extern cpp "lean::natDecLe"] +@[extern cpp "lean::nat_dec_le"] instance decLe (n m : @& nat) : decidable (n ≤ m) := decEq (ble n m) tt -@[extern cpp "lean::natDecLt"] +@[extern cpp "lean::nat_dec_lt"] instance decLt (n m : @& nat) : decidable (n < m) := nat.decLe (succ n) m diff --git a/library/init/data/nat/div.lean b/library/init/data/nat/div.lean index 9e2a5f8698..40b8aba89b 100644 --- a/library/init/data/nat/div.lean +++ b/library/init/data/nat/div.lean @@ -13,7 +13,7 @@ private def divRecLemma {x y : nat} : 0 < y ∧ y ≤ x → x - y < x := private def div.F (x : nat) (f : Π x₁, x₁ < x → nat → nat) (y : nat) : nat := if h : 0 < y ∧ y ≤ x then f (x - y) (divRecLemma h) y + 1 else zero -@[extern cpp "lean::natDiv"] +@[extern cpp "lean::nat_div"] protected def div (a b : @& nat) : nat := wellFounded.fix ltWf div.F a b @@ -45,7 +45,7 @@ wellFounded.fix nat.ltWf (div.induction.F C h₁ h₂) x y private def mod.F (x : nat) (f : Π x₁, x₁ < x → nat → nat) (y : nat) : nat := if h : 0 < y ∧ y ≤ x then f (x - y) (divRecLemma h) y else x -@[extern cpp "lean::natMod"] +@[extern cpp "lean::nat_mod"] protected def mod (a b : @& nat) : nat := wellFounded.fix ltWf mod.F a b diff --git a/library/init/data/string/basic.lean b/library/init/data/string/basic.lean index e843fdc244..30121bef3c 100644 --- a/library/init/data/string/basic.lean +++ b/library/init/data/string/basic.lean @@ -13,10 +13,10 @@ import init.data.option.basic structure string := (data : list char) -attribute [extern cpp "lean::stringMk"] string.mk -attribute [extern cpp "lean::stringData"] string.data +attribute [extern cpp "lean::string_mk"] string.mk +attribute [extern cpp "lean::string_data"] string.data -@[extern cpp "lean::stringDecEq"] +@[extern cpp "lean::string_dec_eq"] def string.decEq (s₁ s₂ : @& string) : decidable (s₁ = s₂) := match s₁, s₂ with | ⟨s₁⟩, ⟨s₂⟩ := @@ -34,23 +34,23 @@ instance : hasLt string := ⟨λ s₁ s₂, s₁.data < s₂.data⟩ /- Remark: this function has a VM builtin efficient implementation. -/ -@[extern cpp "lean::stringDecLt"] +@[extern cpp "lean::string_dec_lt"] instance decLt (s₁ s₂ : @& string) : decidable (s₁ < s₂) := list.hasDecidableLt s₁.data s₂.data -@[extern cpp "lean::stringLength"] +@[extern cpp "lean::string_length"] def length : (@& string) → nat | ⟨s⟩ := s.length /- The internal implementation uses dynamic arrays and will perform destructive updates if the string is not shared. -/ -@[extern cpp "lean::stringPush"] +@[extern cpp "lean::string_push"] def push : string → char → string | ⟨s⟩ c := ⟨s ++ [c]⟩ /- The internal implementation uses dynamic arrays and will perform destructive updates if the string is not shared. -/ -@[extern cpp "lean::stringAppend"] +@[extern cpp "lean::string_append"] def append : string → (@& string) → string | ⟨a⟩ ⟨b⟩ := ⟨a ++ b⟩ @@ -65,7 +65,7 @@ private def utf8ByteSizeAux : list char → usize → usize | [] r := r | (c::cs) r := utf8ByteSizeAux cs (r + csize c) -@[extern cpp "lean::stringUtf8ByteSize"] +@[extern cpp "lean::string_utf8_byte_size"] def utf8ByteSize : (@& string) → usize | ⟨s⟩ := utf8ByteSizeAux s 0 @@ -80,7 +80,7 @@ private def utf8GetAux : list char → usize → usize → char | [] i p := default char | (c::cs) i p := if i = p then c else utf8GetAux cs (i + csize c) p -@[extern cpp "lean::stringUtf8Get"] +@[extern cpp "lean::string_utf8_get"] def utf8Get : (@& string) → utf8Pos → char | ⟨s⟩ p := utf8GetAux s 0 p @@ -89,11 +89,11 @@ private def utf8SetAux (c' : char) : list char → usize → usize → list char | (c::cs) i p := if i = p then (c'::cs) else c::(utf8SetAux cs (i + csize c) p) -@[extern cpp "lean::stringUtf8Set"] +@[extern cpp "lean::string_utf8_set"] def utf8Set : string → utf8Pos → char → string | ⟨s⟩ i c := ⟨utf8SetAux c s 0 i⟩ -@[extern cpp "lean::stringUtf8Next"] +@[extern cpp "lean::string_utf8_next"] def utf8Next (s : @& string) (p : utf8Pos) : utf8Pos := let c := utf8Get s p in p + csize c @@ -105,7 +105,7 @@ private def utf8PrevAux : list char → usize → usize → usize let i' := i + cz in if i' = p then i else utf8PrevAux cs i' p -@[extern cpp "lean::stringUtf8Prev"] +@[extern cpp "lean::string_utf8_prev"] def utf8Prev : (@& string) → utf8Pos → utf8Pos | ⟨s⟩ p := if p = 0 then 0 else utf8PrevAux s 0 p @@ -115,7 +115,7 @@ utf8Get s 0 def back (s : string) : char := utf8Get s (utf8Prev s (bsize s)) -@[extern cpp "lean::stringUtf8AtEnd"] +@[extern cpp "lean::string_utf8_at_end"] def utf8AtEnd : (@& string) → utf8Pos → bool | s p := p ≥ utf8ByteSize s @@ -127,7 +127,7 @@ private def utf8ExtractAux₁ : list char → usize → usize → usize → list | [] _ _ _ := [] | s@(c::cs) i b e := if i = b then utf8ExtractAux₂ s i e else utf8ExtractAux₁ cs (i + csize c) b e -@[extern cpp "lean::stringUtf8Extract"] +@[extern cpp "lean::string_utf8_extract"] def extract : (@& string) → utf8Pos → utf8Pos → string | ⟨s⟩ b e := if b ≥ e then ⟨[]⟩ else ⟨utf8ExtractAux₁ s 0 b e⟩ diff --git a/library/init/data/uint.lean b/library/init/data/uint.lean index 172636ef66..602ef8e60e 100644 --- a/library/init/data/uint.lean +++ b/library/init/data/uint.lean @@ -12,9 +12,9 @@ def uint8Sz : nat := 256 structure uint8 := (val : fin uint8Sz) -@[extern cpp "lean::uint8OfNat"] +@[extern cpp "lean::uint8_of_nat"] def uint8.ofNat (n : @& nat) : uint8 := ⟨fin.ofNat n⟩ -@[extern cpp "lean::uint8ToNat"] +@[extern cpp "lean::uint8_to_nat"] def uint8.toNat (n : uint8) : nat := n.val.val @[extern cpp inline "#1 + #2"] def uint8.add (a b : uint8) : uint8 := ⟨a.val + b.val⟩ @@ -26,7 +26,7 @@ def uint8.mul (a b : uint8) : uint8 := ⟨a.val * b.val⟩ def uint8.div (a b : uint8) : uint8 := ⟨a.val / b.val⟩ @[extern cpp inline "#2 == 0 ? 0 : #1 % #2"] def uint8.mod (a b : uint8) : uint8 := ⟨a.val % b.val⟩ -@[extern cpp "lean::uint8Modn"] +@[extern cpp "lean::uint8_modn"] def uint8.modn (a : uint8) (n : @& nat) : uint8 := ⟨a.val %ₙ n⟩ @[extern cpp inline "#1 & #2"] def uint8.land (a b : uint8) : uint8 := ⟨fin.land a.val b.val⟩ @@ -70,9 +70,9 @@ def uint16Sz : nat := 65536 structure uint16 := (val : fin uint16Sz) -@[extern cpp "lean::uint16OfNat"] +@[extern cpp "lean::uint16_of_nat"] def uint16.ofNat (n : @& nat) : uint16 := ⟨fin.ofNat n⟩ -@[extern cpp "lean::uint16ToNat"] +@[extern cpp "lean::uint16_to_nat"] def uint16.toNat (n : uint16) : nat := n.val.val @[extern cpp inline "#1 + #2"] def uint16.add (a b : uint16) : uint16 := ⟨a.val + b.val⟩ @@ -84,7 +84,7 @@ def uint16.mul (a b : uint16) : uint16 := ⟨a.val * b.val⟩ def uint16.div (a b : uint16) : uint16 := ⟨a.val / b.val⟩ @[extern cpp inline "#2 == 0 ? 0 : #1 % #2"] def uint16.mod (a b : uint16) : uint16 := ⟨a.val % b.val⟩ -@[extern cpp "lean::uint16Modn"] +@[extern cpp "lean::uint16_modn"] def uint16.modn (a : uint16) (n : @& nat) : uint16 := ⟨a.val %ₙ n⟩ @[extern cpp inline "#1 & #2"] def uint16.land (a b : uint16) : uint16 := ⟨fin.land a.val b.val⟩ @@ -128,9 +128,9 @@ def uint32Sz : nat := 4294967296 structure uint32 := (val : fin uint32Sz) -@[extern cpp "lean::uint32OfNat"] +@[extern cpp "lean::uint32_of_nat"] def uint32.ofNat (n : @& nat) : uint32 := ⟨fin.ofNat n⟩ -@[extern cpp "lean::uint32ToNat"] +@[extern cpp "lean::uint32_to_nat"] def uint32.toNat (n : uint32) : nat := n.val.val @[extern cpp inline "#1 + #2"] def uint32.add (a b : uint32) : uint32 := ⟨a.val + b.val⟩ @@ -142,7 +142,7 @@ def uint32.mul (a b : uint32) : uint32 := ⟨a.val * b.val⟩ def uint32.div (a b : uint32) : uint32 := ⟨a.val / b.val⟩ @[extern cpp inline "#2 == 0 ? 0 : #1 % #2"] def uint32.mod (a b : uint32) : uint32 := ⟨a.val % b.val⟩ -@[extern cpp "lean::uint32Modn"] +@[extern cpp "lean::uint32_modn"] def uint32.modn (a : uint32) (n : @& nat) : uint32 := ⟨a.val %ₙ n⟩ @[extern cpp inline "#1 & #2"] def uint32.land (a b : uint32) : uint32 := ⟨fin.land a.val b.val⟩ @@ -186,9 +186,9 @@ def uint64Sz : nat := 18446744073709551616 structure uint64 := (val : fin uint64Sz) -@[extern cpp "lean::uint64OfNat"] +@[extern cpp "lean::uint64_of_nat"] def uint64.ofNat (n : @& nat) : uint64 := ⟨fin.ofNat n⟩ -@[extern cpp "lean::uint64ToNat"] +@[extern cpp "lean::uint64_to_nat"] def uint64.toNat (n : uint64) : nat := n.val.val @[extern cpp inline "#1 + #2"] def uint64.add (a b : uint64) : uint64 := ⟨a.val + b.val⟩ @@ -200,7 +200,7 @@ def uint64.mul (a b : uint64) : uint64 := ⟨a.val * b.val⟩ def uint64.div (a b : uint64) : uint64 := ⟨a.val / b.val⟩ @[extern cpp inline "#2 == 0 ? 0 : #1 % #2"] def uint64.mod (a b : uint64) : uint64 := ⟨a.val % b.val⟩ -@[extern cpp "lean::uint64Modn"] +@[extern cpp "lean::uint64_modn"] def uint64.modn (a : uint64) (n : @& nat) : uint64 := ⟨a.val %ₙ n⟩ @[extern cpp inline "#1 & #2"] def uint64.land (a b : uint64) : uint64 := ⟨fin.land a.val b.val⟩ @@ -244,9 +244,9 @@ def usizeSz : nat := (2:nat) ^ system.platform.nbits structure usize := (val : fin usizeSz) -@[extern cpp "lean::usizeOfNat"] +@[extern cpp "lean::usize_of_nat"] def usize.ofNat (n : @& nat) : usize := ⟨fin.ofNat n⟩ -@[extern cpp "lean::usizeToNat"] +@[extern cpp "lean::usize_to_nat"] def usize.toNat (n : usize) : nat := n.val.val @[extern cpp inline "#1 + #2"] def usize.add (a b : usize) : usize := ⟨a.val + b.val⟩ @@ -258,7 +258,7 @@ def usize.mul (a b : usize) : usize := ⟨a.val * b.val⟩ def usize.div (a b : usize) : usize := ⟨a.val / b.val⟩ @[extern cpp inline "#2 == 0 ? 0 : #1 % #2"] def usize.mod (a b : usize) : usize := ⟨a.val % b.val⟩ -@[extern cpp "lean::usizeModn"] +@[extern cpp "lean::usize_modn"] def usize.modn (a : usize) (n : @& nat) : usize := ⟨a.val %ₙ n⟩ @[extern cpp inline "#1 & #2"] def usize.land (a b : usize) : usize := ⟨fin.land a.val b.val⟩ diff --git a/library/init/io.lean b/library/init/io.lean index 926eda6017..dc698bec53 100644 --- a/library/init/io.lean +++ b/library/init/io.lean @@ -32,13 +32,13 @@ def io.error := string abbrev io : Type → Type := eio io.error -@[extern "leanIoUnsafe"] +@[extern "lean_io_unsafe"] constant unsafeIo {α : Type} (fn : io α) : option α := default _ -@[extern 4 "leanIoTimeit"] +@[extern 4 "lean_io_timeit"] constant timeit {α : Type} (msg : @& string) (fn : io α) : io α := default _ -@[extern 4 "leanIoAllocprof"] +@[extern 4 "lean_io_allocprof"] constant allocprof {α : Type} (msg : @& string) (fn : io α) : io α := default _ abbrev monadIo (m : Type → Type) := hasMonadLiftT io m @@ -71,22 +71,22 @@ def iterateAux {α β : Type} (f : α → io (sum α β)) : (α → io β) → ( @[specialize] def iterate {α β : Type} (a : α) (f : α → io (sum α β)) : io β := fixCore (λ _, throw "deep recursion") (iterateAux f) a -@[extern 2 "leanIoPrimPutStr"] +@[extern 2 "lean_io_prim_put_str"] constant putStr (s: @& string) : io unit := default _ -@[extern 1 "leanIoPrimGetLine"] +@[extern 1 "lean_io_prim_get_line"] constant getLine : io string := default _ -@[extern 4 "leanIoPrimHandleMk"] +@[extern 4 "lean_io_prim_handle_mk"] constant handle.mk (s : @& string) (m : mode) (bin : bool := ff) : io handle := default _ -@[extern 2 "leanIoPrimHandleIsEof"] +@[extern 2 "lean_io_prim_handle_is_eof"] constant handle.isEof (h : @& handle) : io bool := default _ -@[extern 2 "leanIoPrimHandleFlush"] +@[extern 2 "lean_io_prim_handle_flush"] constant handle.flush (h : @& handle) : io unit := default _ -@[extern 2 "leanIoPrimHandleClose"] +@[extern 2 "lean_io_prim_handle_close"] constant handle.close (h : @& handle) : io unit := default _ -- TODO: replace `string` with byte buffer -- constant handle.read : handle → nat → eio string -- constant handle.write : handle → string → eio unit -@[extern 2 "leanIoPrimHandleGetLine"] +@[extern 2 "lean_io_prim_handle_get_line"] constant handle.getLine (h : @& handle) : io string := default _ @[inline] def liftIo {m : Type → Type} {α : Type} [monadIo m] (x : io α) : m α := @@ -191,15 +191,15 @@ instance (α : Type) : inhabited (ref α) := ⟨refPointed.val⟩ namespace prim -@[extern 3 cpp inline "lean::ioMkRef(#2, #3)"] +@[extern 3 cpp inline "lean::io_mk_ref(#2, #3)"] constant mkRef {α : Type} (a : α) : io (ref α) := default _ -@[extern 3 cpp inline "lean::ioRefRead(#2, #3)"] +@[extern 3 cpp inline "lean::io_ref_read(#2, #3)"] constant ref.read {α : Type} (r : @& ref α) : io α := default _ -@[extern 4 cpp inline "lean::ioRefWrite(#2, #3, #4)"] +@[extern 4 cpp inline "lean::io_ref_write(#2, #3, #4)"] constant ref.write {α : Type} (r : @& ref α) (a : α) : io unit := default _ -@[extern 4 cpp inline "lean::ioRefSwap(#2, #3, #4)"] +@[extern 4 cpp inline "lean::io_ref_swap(#2, #3, #4)"] constant ref.swap {α : Type} (r : @& ref α) (a : α) : io α := default _ -@[extern 3 cpp inline "lean::ioRefReset(#2, #3)"] +@[extern 3 cpp inline "lean::io_ref_reset(#2, #3)"] constant ref.reset {α : Type} (r : @& ref α) : io unit := default _ end prim diff --git a/library/init/lean/elaborator.lean b/library/init/lean/elaborator.lean index 7343298865..5821b330be 100644 --- a/library/init/lean/elaborator.lean +++ b/library/init/lean/elaborator.lean @@ -15,10 +15,10 @@ namespace lean -- TODO(Sebastian): should probably be meta together with the whole elaborator constant environment : Type := unit -@[extern "leanEnvironmentContains"] +@[extern "lean_environment_contains"] constant environment.contains (env : @& environment) (n : @& name) : bool := ff -- deprecated constructor -@[extern "leanExprLocal"] +@[extern "lean_expr_local"] constant expr.local (n : name) (pp : name) (ty : expr) (bi : binderInfo) : expr := default expr namespace elaborator @@ -44,7 +44,7 @@ structure oldElaboratorState := (nextInstIdx : nat) (ns : name) -@[extern "leanElaboratorElaborateCommand"] +@[extern "lean_elaborator_elaborate_command"] constant elaborateCommand (filename : @& string) (e : expr) (s : @& oldElaboratorState) : option oldElaboratorState × messageLog := (none, ⟨[]⟩) open parser diff --git a/library/init/lean/expr.lean b/library/init/lean/expr.lean index fc7da2c68f..2a98e30561 100644 --- a/library/init/lean/expr.lean +++ b/library/init/lean/expr.lean @@ -49,18 +49,18 @@ inductive expr instance exprIsInhabited : inhabited expr := ⟨expr.sort level.zero⟩ -attribute [extern "leanExprMkBvar"] expr.bvar -attribute [extern "leanExprMkFvar"] expr.fvar -attribute [extern "leanExprMkMvar"] expr.mvar -attribute [extern "leanExprMkSort"] expr.sort -attribute [extern "leanExprMkConst"] expr.const -attribute [extern "leanExprMkApp"] expr.app -attribute [extern "leanExprMkLambda"] expr.lam -attribute [extern "leanExprMkPi"] expr.pi -attribute [extern "leanExprMkLet"] expr.elet -attribute [extern "leanExprMkLit"] expr.lit -attribute [extern "leanExprMkMdata"] expr.mdata -attribute [extern "leanExprMkProj"] expr.proj +attribute [extern "lean_expr_mk_bvar"] expr.bvar +attribute [extern "lean_expr_mk_fvar"] expr.fvar +attribute [extern "lean_expr_mk_mvar"] expr.mvar +attribute [extern "lean_expr_mk_sort"] expr.sort +attribute [extern "lean_expr_mk_const"] expr.const +attribute [extern "lean_expr_mk_app"] expr.app +attribute [extern "lean_expr_mk_lambda"] expr.lam +attribute [extern "lean_expr_mk_pi"] expr.pi +attribute [extern "lean_expr_mk_let"] expr.elet +attribute [extern "lean_expr_mk_lit"] expr.lit +attribute [extern "lean_expr_mk_mdata"] expr.mdata +attribute [extern "lean_expr_mk_proj"] expr.proj namespace expr def mkApp (fn : expr) (args : list expr) : expr := @@ -69,10 +69,10 @@ args.foldl expr.app fn def mkCapp (fn : name) (args : list expr) : expr := mkApp (expr.const fn []) args -@[extern "leanExprHash"] +@[extern "lean_expr_hash"] constant hash (n : @& expr) : usize := default usize -@[extern "leanExprDbgToString"] +@[extern "lean_expr_dbg_to_string"] constant dbgToString (e : @& expr) : string := default string end expr diff --git a/library/init/lean/extern.lean b/library/init/lean/extern.lean index 49eb801ca8..b1a1ed557c 100644 --- a/library/init/lean/extern.lean +++ b/library/init/lean/extern.lean @@ -22,15 +22,15 @@ inductive externEntry /- - `@[extern]` encoding: ```.entries = [adhoc `all]``` -- `@[extern "levelHash"]` +- `@[extern "level_hash"]` encoding: ```.entries = [standard `all "levelHash"]``` -- `@[extern cpp "lean::stringSize" llvm "leanStrSize"]` - encoding: ```.entries = [standard `cpp "lean::stringSize", standard `llvm "leanStrSize"]``` +- `@[extern cpp "lean::string_size" llvm "lean_str_size"]` + encoding: ```.entries = [standard `cpp "lean::string_size", standard `llvm "leanStrSize"]``` - `@[extern cpp inline "#1 + #2"]` encoding: ```.entries = [inline `cpp "#1 + #2"]``` - `@[extern cpp "foo" llvm adhoc]` encoding: ```.entries = [standard `cpp "foo", adhoc `llvm]``` -- `@[extern 2 cpp "ioPrimPrintln"]` +- `@[extern 2 cpp "io_prim_println"]` encoding: ```.arity = 2, .entries = [standard `cpp "ioPrimPrintln"]``` -/ structure externAttrData := diff --git a/library/init/lean/frontend.lean b/library/init/lean/frontend.lean index ed7f1d0521..7d43c8a656 100644 --- a/library/init/lean/frontend.lean +++ b/library/init/lean/frontend.lean @@ -69,7 +69,7 @@ def runFrontend (filename input : string) (printMsg : message → io unit) (coll } } -@[export leanProcessFile] +@[export lean_process_file] def processFile (f s : string) (json : bool) : stateT environment io unit := do let printMsg : message → io unit := λ msg, if json then diff --git a/library/init/lean/level.lean b/library/init/lean/level.lean index 60bc0c56fe..14d91ff08d 100644 --- a/library/init/lean/level.lean +++ b/library/init/lean/level.lean @@ -16,11 +16,11 @@ inductive level | param : name → level | mvar : name → level -attribute [extern "levelMkSucc"] level.succ -attribute [extern "levelMkMax"] level.max -attribute [extern "levelMkImax"] level.imax -attribute [extern "levelMkParam"] level.param -attribute [extern "levelMkMvar"] level.mvar +attribute [extern "level_mk_succ"] level.succ +attribute [extern "level_mk_max"] level.max +attribute [extern "level_mk_imax"] level.imax +attribute [extern "level_mk_param"] level.param +attribute [extern "level_mk_mvar"] level.mvar instance levelIsInhabited : inhabited level := ⟨level.zero⟩ @@ -71,7 +71,7 @@ def level.instantiate (s : name → option level) : level → level | none := l) | l := l -@[extern "leanLevelHash"] +@[extern "lean_level_hash"] constant level.hash (n : @& level) : usize := default usize /- level to format -/ diff --git a/library/init/lean/name.lean b/library/init/lean/name.lean index e1375313c3..a1ae33ab86 100644 --- a/library/init/lean/name.lean +++ b/library/init/lean/name.lean @@ -13,8 +13,8 @@ inductive name | mkString : name → string → name | mkNumeral : name → nat → name -attribute [extern "leanNameMkString"] name.mkString -attribute [extern "leanNameMkNumeral"] name.mkNumeral +attribute [extern "lean_name_mk_string"] name.mkString +attribute [extern "lean_name_mk_numeral"] name.mkNumeral instance : inhabited name := ⟨name.anonymous⟩ @@ -32,7 +32,7 @@ instance stringToName : hasCoe string name := ⟨mkSimpleName⟩ namespace name -@[extern "leanNameHashUsize"] +@[extern "lean_name_hash_usize"] constant hash (n : @& name) : usize := default usize instance : hashable name := @@ -56,7 +56,7 @@ def components' : name → list name def components (n : name) : list name := n.components'.reverse -@[extern "leanNameDecEq"] +@[extern "lean_name_dec_eq"] protected def decEq : Π (a b : @& name), decidable (a = b) | anonymous anonymous := isTrue rfl | (mkString p₁ s₁) (mkString p₂ s₂) := diff --git a/library/init/lean/util.lean b/library/init/lean/util.lean index 3f9c6a66a3..239c03c9eb 100644 --- a/library/init/lean/util.lean +++ b/library/init/lean/util.lean @@ -9,7 +9,7 @@ import init.lean.position init.io namespace lean /-- Print and accumulate run time of `act` when option `profiler` is set to `true`. -/ -@[extern 5 "leanLeanProfileit"] +@[extern 5 "lean_lean_profileit"] constant profileit {α : Type} (category : @& string) (pos : @& position) (act : io α) : io α := act def profileitPure {α : Type} (category : string) (pos : position) (fn : unit → α) : io α := profileit category pos $ io.lazyPure fn diff --git a/library/init/util.lean b/library/init/util.lean index bf582d2e62..1c7f03ff45 100644 --- a/library/init/util.lean +++ b/library/init/util.lean @@ -8,10 +8,10 @@ import init.data.string.basic universes u /- debugging helper functions -/ -@[extern cpp inline "lean::dbgTrace(#2, #3)"] +@[extern cpp inline "lean::dbg_trace(#2, #3)"] def dbgTrace {α : Type u} (s : string) (f : unit → α) : α := f () -@[extern cpp inline "lean::dbgSleep(#2, #3)"] +@[extern cpp inline "lean::dbg_sleep(#2, #3)"] def dbgSleep {α : Type u} (ms : uint32) (f : unit → α) : α := f () diff --git a/script/camel.py b/script/camel.py index d45456f98e..941a0265f4 100755 --- a/script/camel.py +++ b/script/camel.py @@ -1,5 +1,5 @@ #!/usr/bin/env python3 -import re +import regex as re import os import sys @@ -10,7 +10,7 @@ def to_camel_case(snake_str): # with the 'title' method and join them together. return components[0] + ''.join(x.title() for x in components[1:]) -snake = re.compile("[^\W_]+_\w+", re.MULTILINE) +snake = re.compile(r"(?