Leonardo de Moura
8bc90bc48d
chore: move to new frontend
2020-10-23 11:19:50 -07:00
Leonardo de Moura
21757b2be9
feat: add helper option for fixing bootstrapping issue at src/Init/Data/Int/Basic
2020-10-23 11:13:04 -07:00
Leonardo de Moura
de66ca3943
feat: add helper functions for writing macros
2020-10-23 10:59:59 -07:00
Leonardo de Moura
bebd5075fd
chore: cleanup
2020-10-23 10:00:23 -07:00
Leonardo de Moura
c7dc61adb9
chore: cleanup
2020-10-23 10:00:23 -07:00
Leonardo de Moura
e642c1047a
chore: move to new frontend
2020-10-23 10:00:23 -07:00
Sebastian Ullrich
2ea5d7e480
fix: build
2020-10-23 18:55:06 +02:00
Sebastian Ullrich
fc5f93331d
feat: profile new frontend
2020-10-23 18:34:47 +02:00
Sebastian Ullrich
0720334450
feat: make profileit actually usable
2020-10-23 18:34:47 +02:00
Sebastian Ullrich
890e84d351
feat: unsafeEIO
2020-10-23 18:34:47 +02:00
Leonardo de Moura
8c03075e58
feat: improve function expected error message
2020-10-23 06:52:51 -07:00
Leonardo de Moura
f339efa100
feat: improve invalid named argument error message
2020-10-23 06:47:07 -07:00
Leonardo de Moura
1e8a4d1da5
chore: avoid useless failed to synthesize CoeFun ... tail message
2020-10-23 06:15:29 -07:00
Leonardo de Moura
14e3b26e57
fix: missing instantiateMVars
2020-10-23 05:38:08 -07:00
Leonardo de Moura
0d99c92886
chore: use motive to name the motive of Eq.ndrec and friends
2020-10-23 05:34:26 -07:00
Leonardo de Moura
ec17fcbc1a
feat: use motive to name the kernel generated recursor
...
Motivation: users can use named arguments to provide them.
2020-10-23 05:31:28 -07:00
Leonardo de Moura
de4bede6ff
fix: use correct metavar context
2020-10-23 05:15:36 -07:00
Leonardo de Moura
630dcf4cc1
chore: code convention
2020-10-22 18:34:43 -07:00
Leonardo de Moura
a0b8f13094
chore: remove temporary def
2020-10-22 17:42:25 -07:00
Leonardo de Moura
d4a67baa8e
refactor: rename MonadFinally.finally' => MonadFinally.tryFinally'
2020-10-22 17:40:30 -07:00
Leonardo de Moura
f1dd85e8a3
chore: remove temporary defs
2020-10-22 17:31:07 -07:00
Leonardo de Moura
02521397ac
refactor: rename MonadExceptOf.catch => MonadExceptOf.tryCatch
2020-10-22 17:27:15 -07:00
Leonardo de Moura
053b767336
chore: move to new frontend
2020-10-22 17:16:28 -07:00
Leonardo de Moura
a37e2ae46f
refactor: simplify MonadFunctor
2020-10-22 17:05:34 -07:00
Leonardo de Moura
fa3c32d3b1
chore: remove adaptExcept
2020-10-22 16:56:23 -07:00
Leonardo de Moura
31fd054214
chore: remove adaptState and adaptReader
2020-10-22 16:32:58 -07:00
Leonardo de Moura
bc8b78f481
chore: cleanup
2020-10-22 16:30:06 -07:00
Leonardo de Moura
620647f2f1
refactor: simplify MonadCache and generalize instantiateExprMVars
2020-10-22 16:30:06 -07:00
Leonardo de Moura
c865abb340
refactor: remove MonadRun
2020-10-22 16:30:06 -07:00
Leonardo de Moura
a5a153d1fb
refactor: remove foldlFrom from PersistentArray and LocalContext
2020-10-22 16:30:05 -07:00
Leonardo de Moura
34cdc3a1f1
chore: avoid Array.foldlFrom
2020-10-22 16:30:05 -07:00
Leonardo de Moura
43fbfec1fd
chore: avoid Array.iterate and Array.iterateM
2020-10-22 16:30:04 -07:00
Leonardo de Moura
073bbeb676
chore: move to new frontend
2020-10-22 16:30:03 -07:00
Leonardo de Moura
19d7050847
chore: remove Lean.Name.Name.beq
2020-10-22 16:30:02 -07:00
Leonardo de Moura
311265d833
fix: Name.beq primitive name
...
@Kha I cannot change the name is one step. The problem is that stage0
contains only the function `l_Lean_Name_Name_beq___boxed`.
So, I have to add a function with the new name, update stage0, and
then delete the old one. Otherwise, the build breaks because
the interpreter will fail when we try to test whether two names are
equal or not. The summary is: we cannot change the Lean name for a
primitive in one step because it changes the name of the auxiliary
"boxed" definition used by the interpreter.
2020-10-22 16:30:02 -07:00
Leonardo de Moura
4f6538fa9f
fix: extern detection
2020-10-22 16:30:02 -07:00
Sebastian Ullrich
7964b727e5
chore: improve error message
2020-10-22 21:40:58 +02:00
Leonardo de Moura
85c955d77f
feat: improve ▸ notation
2020-10-22 10:35:45 -07:00
Leonardo de Moura
34945dfc1c
feat: elaborate ▸ notation
2020-10-22 10:20:23 -07:00
Leonardo de Moura
417336ad2f
feat: allow .. in non-pattern applications
2020-10-22 08:56:10 -07:00
Leonardo de Moura
a2de86f0e2
chore: cleanup
2020-10-22 08:35:51 -07:00
Leonardo de Moura
af968c60e6
chore: cleanup
2020-10-22 07:32:23 -07:00
Leonardo de Moura
4efad86fa5
chore: cleanup
2020-10-22 07:26:13 -07:00
Leonardo de Moura
2a393cd4ab
chore: remove workaround
2020-10-22 07:06:09 -07:00
Leonardo de Moura
2041277cae
fix: field default value with implicit type
2020-10-22 07:02:40 -07:00
Leonardo de Moura
427936fa63
chore: move to new frontend
2020-10-22 07:02:40 -07:00
Sebastian Ullrich
c32f843efc
fix: profiling from the new frontend; use trace out for the time being
2020-10-22 16:00:03 +02:00
Sebastian Ullrich
997365b622
chore: remove lone #check
2020-10-22 15:58:53 +02:00
Sebastian Ullrich
7f8d6b803f
feat: interpolatedStr pretty printer
2020-10-22 15:01:53 +02:00
Sebastian Ullrich
ecece59cc3
fix: tracing the compiler from the new frontend
2020-10-22 14:50:26 +02:00
