max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
13084 commits 1 branch 0 tags 5.3 GiB
Commit graph

61 commits

Author SHA1 Message Date
Leonardo de Moura
403059acac doc(doc/changes): document change in the code generator 2017-11-01 14:41:36 -07:00
Leonardo de Moura
d2497d554f feat(frontends/lean): add support for unicode char literals and escape sequences 
TODO: we are not checking if the unicode escape values provide by the
user correspond to valud unicode scalar values. We should check how
other languanges handle this case.
 2017-10-23 13:46:57 -07:00
Leonardo de Moura
9399ce8346 feat(library/vm/vm_string): provide native implementation of type string in the VM 
closes #1175

The types `string_imp` and `string.iterator_imp` were supposed to be
marked private, but we cannot do it because we need to provide
`string_imp.mk`, `string_imp.cases_on`, `string.iterator_imp.mk` and
`string.iterator_imp.cases_on` in the VM since we use a different
internal representation. Note that marking them as private does not
work since users can still access `string_imp.cases_on` using
meta-programming.
So, we need better support for private declarations.

Missing feature, char literals do not support non ASCII values.
That is, in the current implementation, we cannot write 'α'.
This will be implemented in the future.

The VM native implementation does not behave correctly for huge
strings (i.e., strings with more than 4G characters).
The problem is that the current implementation relies on
```
size_t force_to_size_t(vm_obj const & o, size_t def)
```
We may also have overflow problems in the string.iterator implementation
code. This is not a big deal right now, since I doubt we will try
to process string with more than 2^32 characters.

@Kha the `core_lib` and tests seem to be working correctly, but
we need more tests.
 2017-10-23 10:55:26 -07:00
Sebastian Ullrich
5efa1b829c chore(src/emacs): move lean-mode to https://github.com/leanprover/lean-mode 
Closes #410
 2017-10-06 10:46:43 -07:00
Leonardo de Moura
f0bf1624fe feat(frontends/lean/brackets): closes #1820 2017-09-15 12:54:21 -07:00
Gabriel Ebner
3d711b37c3 chore(*): development version 3.3.1 2017-09-14 18:55:03 +02:00
Gabriel Ebner
fa9c868ed2 chore(*): version 3.3.0 2017-09-14 18:53:38 +02:00
Sebastian Ullrich
7ff06b2184 chore(init/meta/attribute): rename user_attribute.set_param to user_attribute.set 
Setting the parameter value really is a side effect of setting the whole attribute
 2017-09-14 18:48:18 +02:00
Gabriel Ebner
b59d2771ea fix(doc/changes): describe fallout from parameterized user attributes 
@kha This was an unexpected breakage resulting from #1809.
 2017-09-06 08:39:30 +02:00
Leonardo de Moura
51bac2918f chore(library/init/core): declare and using structure 
This change was requested by several users.
 2017-09-05 15:08:20 -07:00
Leonardo de Moura
8a10d4c72c fix(library/init/meta/injection_tactic): fixes #1805 2017-09-05 14:20:22 -07:00
Sebastian Ullrich
0dc9d1b4ac chore(doc/changes): update changelog 2017-09-05 23:14:34 +02:00
Leonardo de Moura
da46862b46 fix(library/init/meta/interactive): fixes #1813 2017-09-05 13:33:05 -07:00
Gabriel Ebner
f1ec117a24 doc(changes): option.{map,bind} renaming 2017-09-05 17:13:07 +02:00
Gabriel Ebner
40de4f14c1 feat(library/tactic/simp_lemmas): allow simplification with let-bindings in the local context 2017-09-05 10:24:02 +02:00
Gabriel Ebner
292527896a feat(leanpkg): store Lean version in leanpkg.toml 2017-09-05 08:34:40 +02:00
Sebastian Ullrich
9e53147e0a feat(frontends/lean/elaborator): allow field notation for recursive calls 2017-08-22 15:33:37 -07:00
Gabriel Ebner
22011dcde4 chore(init/algebra/order): typo 
Thanks to @fpvandoorn for proof-reading!
 2017-08-02 15:41:51 +01:00
Gabriel Ebner
f5a6429efc doc(doc/changes): describe order type class changes 2017-08-02 14:41:35 +01:00
Sebastian Ullrich
4f66673fc2 feat(init/meta/attribute,library/tactic/attribute): user_attribute apply handlers 2017-08-02 14:32:39 +01:00
Mario Carneiro
092fc89333 doc(changes): changelog 2017-07-28 22:40:25 +01:00
Leonardo de Moura
4faae27069 perf(frontends/lean): add notation #[...] 
The new notation should be use to input long sequences.
Closes #1755
 2017-07-21 04:20:48 -07:00
Sebastian Ullrich
20c2232bc6 feat(init/meta/interactive): auto-generalize induct parameter 
Like Isabelle
 2017-07-20 01:51:00 -07:00
Sebastian Ullrich
7d39b3e948 refactor(init/meta/interactive): merge generalize and generalize2 and introduce nicer syntax 2017-07-20 01:51:00 -07:00
Leonardo de Moura
ee612c8dd6 chore(changes): universe max u v + 1 2017-07-07 12:59:41 -07:00
Gabriel Ebner
9a8b84cee0 feat(doc/changes.md): add non-exhaustive pattern matches 2017-07-06 22:04:58 -07:00
Sebastian Ullrich
99515f48f8 doc(changes): great renaming 2017-07-06 23:15:45 +02:00
Leonardo de Moura
bb9e3ddae2 feat(library/init/meta/interactive): rw [-h] ==> rw [← h] 
@Armael: this change may affect your project.

The file `doc/changes.md` explains the motivation for the change.
 2017-07-05 11:42:55 -07:00
Leonardo de Moura
dd3616dd16 feat(library/init/meta/interactive): simp_all ==> simp * at * 
cc @Kha
 2017-07-04 11:57:16 -07:00
Leonardo de Moura
e24f3341d4 feat(library/init/meta/interactive): simp without foo ==> simp [-foo] 
This commit also adds "exception" validation.
A bad "exception" was being silently ignored.
We can also exclude hypotheses. Example: `simp [*, -h]`
 2017-07-03 17:10:46 -07:00
Leonardo de Moura
76799db032 feat(library/init/meta/interactive): simph ==> simp [*] 
This modification was suggested by @kha.

TODO:
- Use `simp [-f]` instead of `simp without f`
- Allow users to remove hypothesis from `*`. Example: `simp [*, -h]`
  for simplify using all hypotheses but `h`.
 2017-07-03 15:14:47 -07:00
Leonardo de Moura
69ed291aab refactor(library/init/meta/simp_tactic): tactic.simp_at => tactic.simp_hyp 2017-07-03 14:07:18 -07:00
Leonardo de Moura
34c212fa53 refactor(library/init/meta/simp_tactic): cleanup simp_intros mess 2017-07-03 13:46:16 -07:00
Leonardo de Moura
6b3e28d30b feat(library/init/meta/simp_tactic): add option for reducing [reducible] definitions at dsimp, and to_unfold : list name similar to the one in the simp tactic 
This complete addresses the two pending items at 16711fcdba
 2017-07-03 13:28:46 -07:00
Leonardo de Moura
16711fcdba feat(library/tactic/dsimplify): new configuration options for dsimp 
TODO for `dsimp`:
- Add an option for reducing [reducible] definitions
- Add (to_unfold : list name) similar to the one in the `simp` tactic
 2017-07-02 18:26:03 -07:00
Leonardo de Moura
df091f5c34 feat(library/init/meta/interactive): simp and unfold can unfold projection applications 
@Armael: we finally can write `simp [proj]` to unfold the `proj`
projection application.

Remark: we still need to add similar support for `dsimp`.
 2017-07-02 16:28:04 -07:00
Leonardo de Moura
70b27fb2d3 feat(library/init/meta/interactive): unfold is now based on the simp framework 
See issue #1694.

There is an orthogonal issue. `simp` (and consequently `unfold`) cannot be used to
reduce projections (e.g., `has_add.add`). This issue has been
previously raised by @Armael, but it was not addressed yet.
 2017-07-02 11:30:48 -07:00
Leonardo de Moura
86baab061d doc(changes): describe for tactic for conv interactive mode 2017-07-01 15:39:53 -07:00
Leonardo de Moura
4604d7fd5a feat(library/init/meta): allow users to specify tactic for discharging subgoals in the simp tactic family 
@dselsam @Armael: this feature may be useful for you.
The doc/changes.md describes many other new features.
 2017-07-01 15:35:33 -07:00
Leonardo de Moura
b1bdc4690f feat(library/init/meta/simp_tactic): cleanup dunfold 
Here are modifications:
- It fails if no definition is unfolded.
  See comment https://github.com/leanprover/lean/issues/1694#issuecomment-310956315
  at issue #1694

- Users can provide configuration parameters.

- `dunfold_occs` was deleted.
 2017-06-30 20:49:20 -07:00
Leonardo de Moura
52d4189805 feat(library/tactic): add dsimp_config configuration object for the dsimp tactic family 
Now, `dsimp` fails if the goal did not change.
We can use the config object to obtain the previous behavior:
```
dsimp {fail_if_unchaged := ff}
```
See comment https://github.com/leanprover/lean/issues/1694#issuecomment-310956315
at issue #1694
 2017-06-30 17:15:10 -07:00
Leonardo de Moura
6208934134 feat(library/init/meta/converter/interactive): add support for rw at conv tactical 2017-06-30 12:41:35 -07:00
Leonardo de Moura
f7fe2a775c feat(library/init/meta/rewrite_tactic): improve rewrite tactic 
`rewrite` tactic improvements
- Add support for `auto_param` and `opt_param`
- Order new goals using the same strategies available for `apply`
- Allow user to set configuration object in interactive mode.

@Armael This commit should address the issue you raised about the order
of new goals in the `rewrite` tactic.
See new test tests/lean/run/rw1.lean for examples.
 2017-06-30 12:03:27 -07:00
Leonardo de Moura
e1c76578c1 chore(tests/lean/run, doc/changes): more tests and document new feature 2017-06-29 17:12:04 -07:00
Leonardo de Moura
eb838c78bf doc(changes): simp improvement 2017-06-28 18:29:44 -07:00
Sebastian Ullrich
16fe494736 feat(frontends/lean/scanner): accept arbitrary escaped identifiers 2017-06-28 10:43:19 -07:00
Leonardo de Moura
98ba6666dc doc(changes): apply tactic 
closes #1342
 2017-06-27 18:44:54 -07:00
Sebastian Ullrich
46873d32ae chore(doc/changes): update changelog 2017-06-27 22:08:45 +02:00
Leonardo de Moura
d666742219 doc(changes): update 2017-06-22 08:07:25 -07:00
Leonardo de Moura
14d768ffa2 feat(library/init/meta/interactive): add simp_all tactic 
@Armael I added the simp_all tactic. See new test for an example.
 2017-06-21 20:43:56 -07:00