Sebastian Ullrich
c104d5d34b
doc(init/category/state): add docs and tests
2018-03-20 14:58:36 -07:00
Sebastian Ullrich
97496509d7
feat(init/data/option_t): add has_monad_lift instance
2018-03-20 14:58:36 -07:00
Sebastian Ullrich
4c877cff07
doc(init/category/lift): expand docs and note similarities to layers package
2018-03-20 14:58:36 -07:00
Sebastian Ullrich
36f623af42
feat(init/category/reader): lift alternative through reader_t
2018-03-20 14:58:36 -07:00
Sebastian Ullrich
1bd73f191f
style(init/category): consistently use Greek letters for type parameters (well, except for m)
2018-03-20 14:58:36 -07:00
Sebastian Ullrich
c56606d06a
refactor(init/category/state): remove flipped state_t.run
2018-03-20 14:58:36 -07:00
Sebastian Ullrich
10982cd94d
chore(init/category/lift): document monad_run
2018-03-20 14:58:36 -07:00
Sebastian Ullrich
afe3078b4b
chore(init/category): final touches
2018-03-20 14:58:36 -07:00
Sebastian Ullrich
f4c2499063
chore(init/category/transformers): remove now-unused monad_transformer class, rename to lift.lean
2018-03-20 14:58:36 -07:00
Sebastian Ullrich
b5c9569d86
feat(init/category): add cont_t monad transformer
2018-03-20 14:58:36 -07:00
Sebastian Ullrich
c653292422
feat(init/category/monad_fail): make m in fail implicit
2018-03-20 14:58:36 -07:00
Sebastian Ullrich
ace8ef286a
feat(init/category): even more refactorings, simp lemmas
2018-03-20 14:58:36 -07:00
Sebastian Ullrich
5599c9ca67
feat(init/category): misc enhancements from the tactic refactoring
2018-03-20 14:58:36 -07:00
Sebastian Ullrich
4742d44a74
feat(init/category/state): add monad_except instance for state_t
2018-03-20 14:58:36 -07:00
Sebastian Ullrich
b372dd94d3
feat(init/category/transformers): add monad_run class
2018-03-20 14:58:36 -07:00
Sebastian Ullrich
69cfdbd290
refactor(init/category): make all monad transformers structures, replace monad classes with has_monad_lift_t wrappers
2018-03-20 14:58:36 -07:00
Sebastian Ullrich
8c157eba64
refactor(init/category/state): replace monad_state with monad_state_lift
2018-03-20 14:58:36 -07:00
Sebastian Ullrich
248e035402
fix(init/category/transformers): make has_monad_lift more universe polymorphic
2018-03-20 14:58:36 -07:00
Sebastian Ullrich
1a0363c7c2
feat(init/category/state): add run method, rename with_state
2018-03-20 14:58:36 -07:00
Sebastian Ullrich
c36393066e
feat(init/category): introduce monad_functor and implement it for reader, state, and except
2018-03-20 14:58:36 -07:00
Sebastian Ullrich
7565ce380f
feat(init/category): some helper functions
2018-03-20 14:58:35 -07:00
Sebastian Ullrich
e24b364d0e
refactor(init/category/state): change monad_state.state to monad_state.embed taking state
2018-03-20 14:58:35 -07:00
Sebastian Ullrich
788e8695eb
refactor(init/category/state): replace modify/put (returning unit) with modify'/put' (returning punit)
2018-03-20 14:58:35 -07:00
Sebastian Ullrich
7f0b3b7628
feat(init/category): add monad_reader, reader, reader_t
2018-03-20 14:58:35 -07:00
Sebastian Ullrich
d7c6bb4b99
feat(init/category/except): monad_except class
2018-03-20 14:58:35 -07:00
Sebastian Ullrich
0ab672e304
feat(init/category): except_t monad transformer
2018-03-20 14:58:35 -07:00
Sebastian Ullrich
b28a0392f7
feat(frontends/lean/structure_cmd): allow implicitness infer annotation and parameters in field declaration
2018-03-20 14:58:35 -07:00
Sebastian Ullrich
940aca1ec3
refactor(init/category/lawful): unbundle lawful classes
2018-03-20 14:58:35 -07:00
Sebastian Ullrich
e9b2d1fdc8
refactor(init/category/state): remove dependency on tactic framework
2018-03-20 14:58:35 -07:00
Sebastian Ullrich
159b45c74f
refactor(init/category/state): introduce monad_state
...
* rename `read/write` to `get/put`, as in Haskell
* define `state` as `state_t id`
2018-03-20 14:58:35 -07:00
Sebastian Ullrich
c799a52411
feat(init/category/id): id is a monad
2018-03-20 14:58:35 -07:00
Sebastian Ullrich
8e2e101e0b
refactor(init/category/lawful): prove seq_assoc by normalization to bind
2018-03-20 14:58:35 -07:00
Sebastian Ullrich
1c6861528b
refactor(init/category): move monad laws into separate type classes defined after the tactic framework
2018-03-20 14:58:35 -07:00
Sebastian Ullrich
63382cf7e3
chore(init/category/transformers): move monad_transformer, monad_lift out of monad namespace, make universe polymorphic
2018-03-20 14:58:35 -07:00
Leonardo de Moura
169cd87dbe
feat(library/system/io): add io.run_tactic
...
@nunoplopes @aqjune
I had to add a new primitive to allow you to execute a tactic from the
`main` function. The `main` function is in the `io` monad. The new
primitive has type:
```
meta constant io.run_tactic {α : Type} (a : tactic α) : io α
```
I also added a new test that shows how to use it.
The test displays all declarations that have the `nat` prefix.
cc @kha
2018-03-07 12:15:26 -08:00
Leonardo de Moura
2889482fe9
fix(library/init/meta/interactive): fixes #1943
2018-03-06 17:36:18 -08:00
Leonardo de Moura
0492f254b7
chore(library/data/dlist): remove rsimp dependency
...
Reason: `rsimp` is based on the smt framework. The smt framework
has to be reimplemented. Moreover, the smt framework is currently
not using the new cache infrastructure and we pay a substantial
performance penalty.
2018-03-05 17:09:08 -08:00
Sebastian Ullrich
f487989470
feat(init/core): add infer_instance
2018-03-01 16:09:10 +01:00
Sebastian Ullrich
3d63169b44
feat(init): some simp lemmas
2018-03-01 16:07:52 +01:00
Sebastian Ullrich
61b6e26671
fix(init/meta/tactic): make tactic.funext work on non-abstractions
2018-02-28 12:49:22 +01:00
Sebastian Ullrich
1abf8738fc
feat(frontends/lean/structure_cmd): allow implicitness infer annotation and parameters in field declaration
2018-02-28 12:49:22 +01:00
Sebastian Ullrich
cf8dd9e75e
feat(fronteds/lean/builtin_exprs): do notation: use overloadable bind instead of has_bind.bind
2018-02-28 12:49:22 +01:00
Leonardo de Moura
b72d465835
refactor(library/init/meta): remove tactic_state.mk_empty
...
The tactic_state object will contain a name_generator for creating fresh
names. `tactic_state.mk_empty` is bad because it does not have sufficient
information to create this name_generator.
Moreover `tactic_state.mk_empty` was only being used to convert
`tactic A` into a `parser A`.
We implement this primitive now in C++. In C++, we will be able
to use the parser name generator to initialize a fresh `tactic_state`.
2018-02-27 14:45:47 -08:00
Nuno Lopes
f6a5c26a1f
fix(io.cmd): close stdout pipe
2018-02-27 10:43:09 -08:00
Leonardo de Moura
c0267727a8
fix(library/init/meta): mk_fresh_name should not be used to create user facing names
...
The tactic `mk_fresh_name` is used to create internal unique ids.
We should not use them to create (temporary) user facing
names. Reasons:
1- They are "cryptic".
2- They are not very stable. Minor changes in Lean may change the
value returned and may break proofs that rely on these fresh names.
2018-02-26 10:49:53 -08:00
Leonardo de Moura
21812768b0
fix(library/init/meta/interactive): fixes #1889
2018-02-23 12:39:11 -08:00
Leonardo de Moura
24e7a5a339
feat(library/tactic): add frozen_local_instances tactic for retrieving list of frozen local instances
2018-02-23 11:39:38 -08:00
Leonardo de Moura
db4fcac40c
feat(library): add tactic unfreeze_local_instances
2018-02-23 11:12:05 -08:00
Leonardo de Moura
7762dc381a
feat(library/type_context): use context_cache interface
2018-02-21 15:04:20 -08:00
Leonardo de Moura
46ed0ad677
refactor(library/congr_lemma): remove mk_rel_iff_congr_lemma and mk_rel_eq_congr_lemma
2018-02-21 15:04:20 -08:00
