Leonardo de Moura
2ddc797f65
feat(library/init/system/filepath): add dirName
2019-07-26 14:53:54 -07:00
Leonardo de Moura
ea6eee516b
chore(frontends/lean): use => instead of := in match-expressions
...
Motivation: use same separator used in lambda expressions as in
other programming languages.
2019-07-04 11:38:38 -07:00
Leonardo de Moura
a02443d23d
chore(frontends/lean): fun x, e ==> fun x => e
2019-07-02 13:22:11 -07:00
Leonardo de Moura
6841e47aa4
chore(frontends/lean/builtin_exprs): remove support for (<infix>) and (<infix> <expr>) notations
...
In Lean 4, we will support the more general
`a + ·` ==> `fun x, a + x`
`· + b` ==> `fun x, x + b`
`· + ·` ==> `fun x y, x + y`
`f · y` ==> `fun x, f a y`
`g · · b` ==> `fun x y, g x y b`
2019-07-02 08:06:06 -07:00
Leonardo de Moura
ab487ea4ac
feat(frontends/lean): allow ; instead of in in let-decls
2019-06-27 17:12:03 -07:00
Leonardo de Moura
1658be20f1
feat(library/init/data/string): add String.isPrefixOf
2019-06-06 14:20:50 -07:00
Leonardo de Moura
0d1a0c8b6e
chore(library): toBool ==> decide
...
We want to define a type class similar to Haskell's `ToBool`.
2019-05-06 14:02:15 -07:00
Leonardo de Moura
0a1b751efd
chore(library/init/data/string/basic): naming consistency
2019-04-09 08:18:29 -07:00
Leonardo de Moura
49551036ed
refactor(library/init): minor changes
...
Old `Nat.repeat` => `Nat.for`
Old `Nat.mrepeat` => `Nat.mfor`
New `Nat.repeat` has type
```
def repeat {α : Type u} (f : α → α) (n : Nat) (a : α) : α :=
``
`List.repeat` => `List.replicate` (like in Haskell)
Avoid weird `ℕ` in List library
2019-03-29 10:39:00 -07:00
Leonardo de Moura
90a6b36783
refactor(library/init/data/string/basic): avoid artificial "fuel" using partial
...
After we restore the tactic framework, we will be able to eliminate the
`partial` keywords in this module by using well-founded recursion.
2019-03-27 13:51:52 -07:00
Leonardo de Moura
b29fb57fcf
refactor(library/init/data/string/basic): String.Pos as Nat
...
@kha: I initially planned to use the UTF8 API only in very special
cases, but I found them to be super useful. They allow us to implement
an efficient String library mostly in Lean.
However, the there was a problem: `abbrev String.Pos := USize`.
This definition is fine for a low level API, but this is not the case
anymore. By having `String.Pos := USize`, we will not be able to
prove natural theorems for the `String` API. For example,
`String.map id s = s` did not hold. We would have to include the
artificial antecedent `s.length <= usizeMax` (or something like this).
I suspect it would be very painful.
So, this commit defines `String.Pos` as `Nat`. The performance
overhead seems to be very small.
2019-03-26 15:35:52 -07:00
Leonardo de Moura
b0da4360d0
chore(runtime, library/init/data/string/basic): prepare to change String.Pos
2019-03-26 12:25:12 -07:00
Leonardo de Moura
79b6a144d5
feat(library/init/data/string/basic): improve and cleanup String/Substring API
2019-03-25 14:19:10 -07:00
Leonardo de Moura
bbe93c036d
feat(library/init/data/string): add Substring
2019-03-25 09:29:06 -07:00
Leonardo de Moura
18f3ec41a9
chore(library/init/data/string/basic): reorg and cleanup
2019-03-25 09:29:06 -07:00
Leonardo de Moura
60f8d17942
refactor(library/init/data/string/basic): simplify String.Iterator
...
The `offset` field is problematic because it prevents us from having an
efficient way of moving back and forth between `String.Pos` and `String.Iterator`.
@kha I temporarily added `String.OldIterator` for making sure the
parser doesn't break. This is a temporary fix that will be eliminated
after we replace `parsec`.
2019-03-25 07:57:12 -07:00
Leonardo de Moura
8225146aa2
chore(library/init/core): HasLt => HasLess, HasLe => HasLessEq, ...
2019-03-23 10:07:46 -07:00
Leonardo de Moura
cc8ccae754
feat(library/init/data/string/basic): add String.foldl and String.foldr
2019-03-22 17:26:43 -07:00
Leonardo de Moura
4f80e30574
feat(library/init/data/string/basic): add String.split
2019-03-22 17:26:43 -07:00
Leonardo de Moura
98163e53ac
chore(library/init/data/string/basic): simplify UTF8 API names
...
@kha I am finding the UTF8 API super useful. So, I am giving nice names
to it. The API is safe for users and the runtime implementation should
match the reference one.
2019-03-22 17:26:43 -07:00
Leonardo de Moura
050985121d
chore(library/init/data/string/basic): utf8Pos => Pos
2019-03-22 17:26:43 -07:00
Leonardo de Moura
1fe3f14ad0
chore(*): Uint => UInt, Usize => USize
2019-03-21 15:06:44 -07:00
Leonardo de Moura
2be87ecd92
chore(library/init): Bool.tt => Bool.true and Bool.ff => Bool.false
2019-03-21 15:06:44 -07:00
Leonardo de Moura
2ea0baeb99
chore(library): use lowercase in imports
2019-03-21 15:06:44 -07:00
Leonardo de Moura
675003318e
chore(*): small fixes
2019-03-21 15:06:44 -07:00
Sebastian Ullrich
beda5f5f43
chore(library): capitalize types and namespaces
2019-03-21 15:06:43 -07:00
Sebastian Ullrich
f7aeeaf237
exclude export/extern, translate constants.txt
2019-03-21 15:06:43 -07:00
Sebastian Ullrich
b939162168
chore(library): switch from snake_case to camelCase
2019-03-21 15:06:43 -07:00
Leonardo de Moura
ecdb9d6df0
feat(library/init, frontends/lean): add abbreviation for abbreviation
2019-03-15 16:01:25 -07:00
Leonardo de Moura
68ebc2a5c5
feat(library/init/data/string/basic): implement iterators using uft8 low level API
2019-03-12 06:56:05 -07:00
Leonardo de Moura
cf3bbd7e25
feat(runtime): add utf8_prev and utf8_set
...
Next goal: implement string.iterator in Lean
2019-03-11 18:05:40 -07:00
Leonardo de Moura
c862ce4a75
feat(runtime, library/init/data/string/basic): add utf8_pos
...
`utf8_pos` is a low level alternative for `string.iterator`.
TODO: implement `string.iterator` using it.
2019-03-09 12:30:19 -08:00
Leonardo de Moura
6be47dfb97
feat(library/init/data/string/basic): use extern attribute
2019-02-11 17:54:24 -08:00
Leonardo de Moura
ed4eeddf0a
feat(runtime/object): add more string primitives
2018-11-14 16:51:10 -08:00
Leonardo de Moura
2fa938220b
chore(library/init/data/string): cleanup
2018-11-14 14:09:45 -08:00
Leonardo de Moura
dc937281b3
chore(library/init/string): remove string.iterator_imp
2018-10-02 13:46:01 -07:00
Leonardo de Moura
3a4acbee9e
chore(library/init/data/string): remove string_imp
...
We will use the (to be implemented) `opaque` keyword
2018-10-01 14:17:11 -07:00
Sebastian Ullrich
5123148aa6
feat(library/init/data/string/basic): trim whitespace around symbols
2018-09-28 13:08:24 -07:00
Leonardo de Moura
71dd8653bc
feat(library/init/core): decidable_eq is a proper class
...
We need this to take advantage of the new indexing structure we are
going to add to improve performance.
2018-09-07 16:38:11 -07:00
Sebastian Ullrich
80745ba776
chore(library/init/data/string/basic): rename string.iterator's next_to_string to remaining_to_string
...
The old name implied that `curr` was not part of its result
2018-07-05 10:42:37 +02:00
Sebastian Ullrich
9e51ff5580
feat(library/init/data/string/basic): add forward and is_prefix_of_remaining to iterator
2018-07-05 10:20:25 +02:00
Leonardo de Moura
d5fe509c36
chore(*): remove end after each match-expression
...
`end` is not optional anymore
2018-05-04 11:30:06 -07:00
Leonardo de Moura
f20f50254c
feat(library/init/data/string/basic): add string.line_column
2018-04-30 15:55:34 -07:00
Leonardo de Moura
62d425073e
feat(library/init/data/string/basic): add string.iterator.offset
2018-04-30 15:43:51 -07:00
Leonardo de Moura
6ef4806fca
feat(library/init/lean/format): add lean.format
2018-04-29 14:36:49 -07:00
Leonardo de Moura
0af913c99f
refactor(library/init/data/string): define decidable_eq string instance earlier
2018-04-27 08:16:14 -07:00
Leonardo de Moura
9e9a0d103f
feat(library/vm/vm_string): add fast string.iterator.remaining
2018-04-26 18:03:41 -07:00
Leonardo de Moura
1ad1080f11
refactor(library): keep only basic nat theorems
...
All theorems are proved without using the tactic framework.
Thus, we can define `fin/uint32/uint64` types and their operations
before we define the tactic framework.
2018-04-11 16:47:54 -07:00
Leonardo de Moura
7aaac31e35
chore(library/init/data/nat): remove dependency
2018-04-10 15:48:13 -07:00
Sebastian Ullrich
c64284a377
perf(init/data/string/ops): make string.split linear
2018-01-15 10:51:27 +01:00
