Leonardo de Moura
9d1f4a4f29
chore(library/init/control/state): indentation consistency
2019-03-23 19:03:26 -07:00
Leonardo de Moura
4d9150859b
chore(library/init/core): avoid {{x : A}} strict implicit arguments, and cleanup
2019-03-23 19:03:26 -07:00
Sebastian Ullrich
e3ea2e84d2
feat(frontends/lean/lean_elaborator): set position of #check output etc.
2019-03-23 23:13:09 +01:00
Sebastian Ullrich
07059fe2bf
fix(library/init/lean/frontend): naming style misrenamings
2019-03-23 23:09:55 +01:00
Sebastian Ullrich
e27bffabef
fix(lean4-mode/lean4-flycheck): allow changing lean4-extra-arguments without restart
2019-03-23 23:09:55 +01:00
Leonardo de Moura
8225146aa2
chore(library/init/core): HasLt => HasLess, HasLe => HasLessEq, ...
2019-03-23 10:07:46 -07:00
Leonardo de Moura
41f373cd0d
chore(library/init/lean/declaration): naming convention
2019-03-23 09:28:38 -07:00
Leonardo de Moura
d110a607fe
fix(runtime/io): bug at IO.Ref primitives in multi-threaded mode
2019-03-23 09:06:04 -07:00
Leonardo de Moura
df9ce10623
feat(library/compiler): special support for initialization functions of the form def initFn : IO Unit
...
We can now write
```
@[init] def initFn : IO Unit := ...
```
instead of
```
def initFn : IO Unit := ...
@[init initFn] constant execInitFn : Unit := ()
```
2019-03-23 08:46:38 -07:00
Leonardo de Moura
3b70e8785b
chore(tests/compiler/str): fix test
2019-03-22 17:26:43 -07:00
Leonardo de Moura
412d0ea578
feat(library/init/lean/options): add setOptionFromString
...
We can use this primitive to process command line arguments of the form
`-D <key> = <value>`
TODO: allow users to attach `[init]` to definitions of the form
```
@[init] def foo : IO Unit := ...
```
and avoid the awkward auxiliary constant.
2019-03-22 17:26:43 -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
d4aab31ada
feat(library/init/io): IO.userError
2019-03-22 17:26:43 -07:00
Leonardo de Moura
c10a99e96f
feat(library/init/lean/name): add String.toName
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
81f847a2d1
chore(stage0): update
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
1c671965c5
feat(library/init/lean/options): add registerOption
2019-03-22 17:26:43 -07:00
Leonardo de Moura
dc73d5443d
refactor(library/init/lean): add MData abbreviation
2019-03-22 17:26:43 -07:00
Sebastian Ullrich
91b244f679
chore(tests/playground/environment_ext): style and minor changes
2019-03-22 22:51:21 +01:00
Sebastian Ullrich
dc93bc37cc
chore(tests/playground/environment_ext): fix
2019-03-22 22:51:21 +01:00
Leonardo de Moura
3d52298c69
chore(util/sexpr): preparing to port options to Lean
2019-03-22 13:58:16 -07:00
Leonardo de Moura
50207e2c5a
chore(library/constants.txt): remove dead variables
2019-03-22 13:26:48 -07:00
Leonardo de Moura
45c4a78f59
chore(tests/playground/environment_ext): revert accidental commit
2019-03-22 13:26:17 -07:00
Leonardo de Moura
2b76d79791
chore(library/init/core): remove more nonsense
2019-03-22 13:14:20 -07:00
Leonardo de Moura
930653f292
chore(library/init): Unit.star => Unit.unit
...
@kha Our stdlib is starting to match the names we used in our paper :)
2019-03-22 13:06:45 -07:00
Leonardo de Moura
3fe5cf1528
chore(library/init/core): remove another weirdness: the bs at bnot, band and bor
2019-03-22 12:57:31 -07:00
Leonardo de Moura
e1ea2b3948
chore(library/init): fix names and add HasEmptyc instances
2019-03-22 12:38:22 -07:00
Leonardo de Moura
e24ad8c0b5
feat(library/init/core): add HasBeq default instances for types that implement DecidableEq
...
@kha I think code looks less weird if we don't mix Booleans and
propositions in the same expression.
2019-03-22 11:23:45 -07:00
Leonardo de Moura
3202840959
fix(runtime/io): make IO.Ref thread-safe again
...
See new comment at `io.cpp`
2019-03-22 09:59:32 -07:00
Leonardo de Moura
9c9a30d834
chore(stage0): update
2019-03-22 09:39:42 -07:00
Leonardo de Moura
87b066b87e
refactor(library/init): move function.lean definitions to core.lean
2019-03-22 09:33:10 -07:00
Leonardo de Moura
e31c3fde56
chore(library/init): remove dead code, lemma => theorem
2019-03-22 09:27:30 -07:00
Leonardo de Moura
46cb2436d8
chore(library/init/core): remove dead code, and naming convention
2019-03-22 09:19:28 -07:00
Leonardo de Moura
7552b2e1e4
chore(library/init/data/list/basic): mem => Mem
2019-03-22 09:10:21 -07:00
Sebastian Ullrich
5f7a63b34b
feat(shell/lean): accept stand-alone files as input
...
@leodemoura
2019-03-22 14:05:10 +01:00
Sebastian Ullrich
fa0381cecf
fix(library/Makefile): clean STAGE1_OUT too
...
vanished during merge
2019-03-22 10:18:33 +01:00
Leonardo de Moura
548e7c5436
chore(tests/playground): fix playground tests
2019-03-21 18:30:58 -07:00
Leonardo de Moura
452d5107ac
chore(library/init/data/array): naming convention
...
The array read and write operations are now called:
- "Comfortable" version (with runtime bound checks):
`Array.get` and `Array.set` like OCaml.
It is also consistent with `Ref.get` and `Ref.put`,
and `get` and `set` for `MonadState`.
- `Fin` version (without runtime bound checks):
`Array.index` and `Array.update` like in F*.
- `USize` version (without runtime bound checks and unboxing):
`Array.idx` and `Array.updt`.
cc @kha
2019-03-21 18:03:29 -07:00
Leonardo de Moura
4a08d6715a
chore(library/init/data/array): add HasEmptyc instance
2019-03-21 17:06:56 -07:00
Leonardo de Moura
91204a52d6
chore(library/init/data/dlist): Dlist => DList
2019-03-21 17:03:22 -07:00
Leonardo de Moura
3befc219c9
chore(library/init): Empty => empty when it is a function
2019-03-21 17:03:15 -07:00
Leonardo de Moura
4bf41f0036
chore(tests/lean/run/coroutine): fix test
2019-03-21 16:46:53 -07:00
Leonardo de Moura
a79b00d733
chore(runtime, stage0): update Ref primitive operation names
2019-03-21 16:43:54 -07:00
Leonardo de Moura
dfe15cf743
refactor(library/init): use get and set for State EState and Ref
...
TODO: use the same naming convention for array reads and writes.
2019-03-21 16:34:32 -07:00
Leonardo de Moura
0a326c666f
chore(library/init/data/list/basic): use Bool instead of Prop
2019-03-21 16:24:38 -07:00
Leonardo de Moura
1ff920f955
chore(library/init/core): remove dead code
2019-03-21 16:24:20 -07:00
Leonardo de Moura
c802c232a8
chore(shell/CMakeFiles): disable test
...
@kha I disabled this test for now. It seems to fail because we don't
have a `leanpkg.path` there. I thought about hacking the test and adding
a dummy `leanpkg.path` file there, but you might have a better idea.
It is not clear to me why we always need `leanpkg.path` now. It seems
this a new requirement that was introduced when you simplified the
module manager.
2019-03-21 15:11:05 -07:00
Leonardo de Moura
7bb015c6b3
chore(tests/lean): fix more tests
2019-03-21 15:11:05 -07:00
