Leonardo de Moura
ed976027fe
chore: naming convention
2020-08-26 20:24:33 -07:00
Leonardo de Moura
09a375b540
feat: reject _ where function is expected
...
It should behave like Lean3.
2020-08-26 18:48:05 -07:00
Leonardo de Moura
4934a2d522
chore: remove workaround
2020-08-26 16:24:20 -07:00
Leonardo de Moura
7db6f420f5
refactor: move mkAuxDefinitionCore
2020-08-26 16:20:09 -07:00
Leonardo de Moura
00599cf62b
fix: types of the recursive functions being defined cannot reference other functions in the same mutual block
2020-08-26 15:29:06 -07:00
Leonardo de Moura
8543a20b8f
feat: add checkpoint using withSynthesize
2020-08-26 15:10:26 -07:00
Leonardo de Moura
89bd5d6da2
fix: bug introduced today
2020-08-26 14:49:20 -07:00
Leonardo de Moura
5d036d0ca3
feat: generalize mkClosure
2020-08-26 14:45:46 -07:00
Leonardo de Moura
5af763f243
feat: use checkNotAlreadyDeclared
2020-08-26 13:44:25 -07:00
Leonardo de Moura
de2df5955f
refactor: polymorphic checkNotAlreadyDeclared
2020-08-26 13:42:57 -07:00
Leonardo de Moura
497d8592cf
feat: elaborate letrec values
2020-08-26 13:35:51 -07:00
Leonardo de Moura
1f2204af96
feat: add LetIdDeclView
2020-08-26 13:28:41 -07:00
Leonardo de Moura
f4f0684636
chore: remove dead code
2020-08-26 13:19:13 -07:00
Leonardo de Moura
5dc5e8a92f
feat: add LetRecView and expand letEqnsDecl occurring in letrec's
2020-08-26 11:30:06 -07:00
Leonardo de Moura
546c108497
chore: revise letrec syntax
2020-08-26 10:50:32 -07:00
Leonardo de Moura
70e508d704
chore: add Lean/Elab/LetRec.lean
2020-08-26 10:07:59 -07:00
Leonardo de Moura
effaf64a07
feat: allow user to specify attributes letrec declarations
2020-08-26 09:57:46 -07:00
Leonardo de Moura
8a9b031a9d
refactor: add Lean/Elab/Attributes.lean
2020-08-26 09:54:48 -07:00
Leonardo de Moura
a413da856f
refactor: polymorphic elabAttrs and elabAttr
2020-08-26 09:50:03 -07:00
Leonardo de Moura
6a83577703
feat: letrec syntax
2020-08-26 09:33:52 -07:00
Leonardo de Moura
467e912380
fix: bug on JP handling
2020-08-26 08:34:35 -07:00
Leonardo de Moura
76f9b155a1
chore: document kind of crash
2020-08-26 08:34:35 -07:00
Leonardo de Moura
5efa628e43
chore: split Lift.lean into MonadLift.lean, MonadFunctor.lean, and MonadRun.lean
2020-08-26 08:34:35 -07:00
Leonardo de Moura
321719b300
feat: add MonadFinally
2020-08-25 17:58:35 -07:00
Leonardo de Moura
31716731ba
chore: cleanup
2020-08-25 15:06:12 -07:00
Leonardo de Moura
813a964767
refactor: move polymorphic Meta methods back to Meta namespace
2020-08-25 14:57:58 -07:00
Leonardo de Moura
cf0149a1a7
refactor: use MonadControlT
2020-08-25 13:54:42 -07:00
Leonardo de Moura
b095f0652a
fix: tryLiftAndCoe
2020-08-25 13:54:41 -07:00
Leonardo de Moura
1103806ff4
refactor: HasMonadLift ==> MonadLift
2020-08-25 13:54:41 -07:00
Leonardo de Moura
b03cd748cf
feat: add MonadControl
2020-08-25 13:54:41 -07:00
Leonardo de Moura
e5b7daf9c2
refactor: make AppBuilder methods polymorphic
2020-08-24 18:23:34 -07:00
Leonardo de Moura
49f5e4db20
refactor: cleanup
2020-08-24 17:47:27 -07:00
Leonardo de Moura
eaed6ba6a3
refactor: polymorphic MetaM combinators
2020-08-24 17:03:54 -07:00
Leonardo de Moura
e391cb5b64
refactor: use internal exceptions instead of OptionT
...
@Kha: the motivations are
- Code is more uniform, and make sure we are using only `ReaderT` and
`StateRefT` on top of our basic monads.
- It is easier to support variants of `monadMap`. We don't need to
explain the system how these variants behave with `OptionT`.
2020-08-24 16:48:15 -07:00
Leonardo de Moura
ac565de96c
refactor: add MonadMetaM class
2020-08-24 12:17:47 -07:00
Leonardo de Moura
57a6998426
chore: minor
2020-08-24 12:17:47 -07:00
Leonardo de Moura
5b23b5302f
refactor: move TransparencyMode to its own file
2020-08-24 12:17:47 -07:00
Leonardo de Moura
e000fcaeda
chore: cleanup
2020-08-24 12:17:47 -07:00
Leonardo de Moura
143760d443
refactor: polymorphic withIncRecDepth
2020-08-24 12:17:47 -07:00
Leonardo de Moura
4f14fe3b79
refactor: polymorphic withRef
2020-08-24 12:17:47 -07:00
Sebastian Ullrich
8630d78b3f
fix: Int.add spec
2020-08-24 13:55:14 +02:00
Sebastian Ullrich
015903f055
chore: speedcenter: benchmark actual, parallel stdlib build
2020-08-24 13:43:44 +02:00
Leonardo de Moura
b672f0820b
chore: remove workarounds
2020-08-23 19:56:01 -07:00
Leonardo de Moura
6fc935f6d1
refactor: add MonadNameGenerator
2020-08-23 19:56:01 -07:00
Leonardo de Moura
d85836a387
chore: mark TODO
2020-08-23 19:55:53 -07:00
Leonardo de Moura
50f779e858
refactor: polymorphic setTraceState, getTraceState, etc
2020-08-23 19:10:38 -07:00
Leonardo de Moura
6180ba6d7d
chore: rename ST.Ref primitives
2020-08-23 12:28:14 -07:00
Leonardo de Moura
77b9445544
feat: real ST monad
...
@Kha: the new `ST` (and `EST`) are escapable like the Haskell ST monad.
It makes `StateRefT` much more useful because we can now run it from pure
code.
2020-08-23 12:15:32 -07:00
Leonardo de Moura
5ffbada3df
feat: add Lean.MonadEnv, Lean.MonadError, and Lean.MonadOptions
...
This is the first set of polymorphic methods. I will add more later,
and keep reducing code duplication.
cc @Kha
2020-08-22 16:00:43 -07:00
Leonardo de Moura
37571edce5
fix: remove unnecessary dependencies
2020-08-22 15:15:10 -07:00
