Leonardo de Moura
f8ce142da7
fix(library/vm/vm_string): bug at string.iterator.insert VM builtin implementation
2017-10-23 10:55:26 -07:00
Leonardo de Moura
e30f2f6604
fix(library/vm/vm): bug at update_vm_constructor
2017-10-23 10:55:26 -07:00
Leonardo de Moura
47a8c2baef
fix(library/vm/vm_string): missing VM builtin for string_imp projections
2017-10-23 10:55:26 -07:00
Leonardo de Moura
ffb2464f1f
fix(library/vm/vm_string): missing VM builtin for string.iterator_imp projections
2017-10-23 10:55:26 -07:00
Leonardo de Moura
7cba1c6753
fix(library/vm/vm_string): bug at string.fold VM builtin implementation
2017-10-23 10:55:26 -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
Leonardo de Moura
28501a0e0e
feat(library/init/data/string): string as a list of unicode scalar values, and iterator abstraction
...
TODO:
- Implement string primitives in the VM.
- Support for unicode char literals.
2017-10-23 10:55:26 -07:00
Leonardo de Moura
bdc8e1ced8
feat(library/init/data/char): char as an unicode scalar value
...
TODO: this is the first step to have better unicode support.
2017-10-23 10:55:26 -07:00
Sebastian Ullrich
87e1a88d01
feat(init/meta/pexpr): allow creating structure instance pre-terms
2017-10-11 16:13:34 +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
Leonardo de Moura
6781681ae5
feat(frontends/lean/definition_cmds): when the kernel fails to type check a declaration include the fully elaborated term in the error message
2017-09-13 16:43:54 -07:00
Gabriel Ebner
9118079f7f
fix(library/module_mgr): error handling in cyclic imports
...
Fixes #1807
2017-09-12 17:22:47 +02:00
Leonardo de Moura
d428eca8a7
fix(library/equations_compiler,frontends/lean): private name support and alias generation for auxialiary declarations
...
fixes #1804
Remark: now, all auxiliary definitions in a private declaration share
the same "private" prefix.
2017-09-11 16:46:56 -07:00
Sebastian Ullrich
1544c3d390
feat(library/tactic/user_attribute,init/meta/attribute): user_attribute.set_param
2017-09-05 23:14:34 +02:00
Sebastian Ullrich
ea6a4159a9
feat(library/tactic/user_attribute,init/meta/attribute): implement parameterized user attributes
2017-09-05 23:14:34 +02:00
Sebastian Ullrich
3188c4cbcf
refactor(library/tactic/user_attribute,init/meta/attribute): merge caching_user_attribute into user_attribute
...
The inheritance-based approach doesn't scale to a second subclass for parameterized attributes
2017-09-05 23:14:34 +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
488850e03a
fix(library/util): get_num_inductive_hypotheses_for: use whnf to detect recursive arguments
...
Fixes #1812 .
2017-09-05 08:28:32 +02:00
Gabriel Ebner
de0fc09ab9
fix(library/congr_lemma): always return heq in mk_hcongr_lemma
2017-08-29 16:36:37 +02:00
Gabriel Ebner
9920062b69
fix(kernel/expr,library/constructions/projection): preserve instance-implicitness in structure parameters
2017-08-27 16:47:04 +02:00
Sebastian Ullrich
07d8b18caf
feat(init/meta/pexpr): expose pexpr.is_placeholder
2017-08-26 23:22:06 +02:00
Sebastian Ullrich
3062c6feb7
feat(init/meta): expose pexpr.get_structure_instance_info
2017-08-24 10:36:43 +02:00
Leonardo de Moura
e99ce26b16
fix(library/type_context): fixes #1801
...
This commit also fixes the decay in error message quality reported at
c6a10b127f
2017-08-22 14:03:58 -07:00
Leonardo de Moura
fb2186334a
fix(library/init/meta/relation_tactics,library/tactic/subst_tactic): fixes #1772
2017-08-21 14:51:30 -07:00
Gabriel Ebner
7453148ad2
fix(library/tactic/simp_lemmas): only check has_idx_metavar in simp_lemmas.rewrite
...
This copies the change made in 2ca2920284
2017-08-20 09:30:16 +02:00
Leonardo de Moura
94e7b46214
fix(library/string): is_char_value bug
...
Type may be a metavariable, and the is_def_eq test may succeed by
unifying the metavariable with `char`
2017-08-18 15:29:51 -07:00
Leonardo de Moura
d4f2bb77b8
feat(frontends/lean): recursive equation preprocessor
...
To make the equation compiler more convenient to use, we will add a
couple of preprocessing steps.
This commit adds the first one of them. In this step, we use
type inference to refine pattern variables, and we relax the
restrictions on inaccessible annotations.
We will also add a preprocessing step that implements the "complete
transition" step before we execute the elim_match step.
2017-08-18 15:06:11 -07:00
Gabriel Ebner
bbfbf1d8f5
doc(library/tactic/simp_lemmas): document and test change in ext_add_core
2017-08-18 19:34:08 +02:00
Gabriel Ebner
6b9bf5e2b7
fix(library/tactic/simp_lemmas): report invalid simplification lemmas also in add()
2017-08-18 19:32:51 +02:00
Gabriel Ebner
0d8e62ed40
feat(library/tactic/simp_lemmas): add both equational lemmas and the definition itself
2017-08-18 08:54:04 +02:00
Gabriel Ebner
256ca9789f
fix(library/tactic/simp_lemmas): fix typo in pp
2017-08-18 08:54:03 +02:00
Gabriel Ebner
6bd3fe2449
feat(library/tactic/simp_lemmas): support congruence lemmas that are metavariable applications
2017-08-18 08:54:03 +02:00
Leonardo de Moura
0660e18943
feat(library/metavar_context): add method for setting metavar user facing name
2017-08-17 16:03:32 -07:00
Sebastian Ullrich
579d4a459e
chore(init/meta/interactive): check simp lemmas for ambiguous overloads
...
Fixes #1786
2017-08-15 12:43:02 +02:00
Gabriel Ebner
32ddac5f40
feat(library/tactic/kabstract): expose kabstract to VM
2017-08-14 11:41:54 +02:00
Gabriel Ebner
867bc46d99
feat(library/vm/vm_parser): expose parse_command_like to the vm
2017-08-14 11:41:48 +02:00
Gabriel Ebner
e2717ec2c5
fix(library/compiler/inliner): inline auxiliary declarations
...
Fixes #1763 .
2017-08-06 10:24:26 +02:00
Gabriel Ebner
0c15724e8e
fix(library/tactic/simplify): handle universe polymorphic simplification rules
...
The issue was that instantiate_mvars(infer(m)) had a metavariable, while
infer(instantiate_mvars(m)) did not. Changing the call from assign to
is_def_eq also unifies the type, assigning the metavariable inside the
type.
2017-08-03 17:42:07 +01:00
Leonardo de Moura
f39e42bf2d
fix(library/tactic/destruct_tactic): fixes #1766
2017-08-02 15:35:33 +01:00
Leonardo de Moura
fdaa26f2fd
feat(library/equations_compiler/wf_rec): fixes #1782
2017-08-02 15:12:04 +01:00
Gabriel Ebner
ce509e621a
refactor(library/init/algebra): remove order_pair classes
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
Gabriel Ebner
89e1b196db
fix(library/compiler/preprocess): do not unfold noncomputable definitions
...
This happened in Johannes' real number formalization. We tried to
unfold a noncomputable definition even though it would have been erased
afterwards, and failed.
The check_computable check was introduced in order to fix the error
message in #1401 , the error message is still intelligible in that
example.
2017-08-01 08:37:18 +01:00
Gabriel Ebner
25aa847aba
fix(library/constructions/brec_on): make motive explicit in *.below
...
Otherwise you can't figure out the type from the pretty-printed output
`nat.below n`.
2017-07-23 09:38:44 +01:00
Gabriel Ebner
537b11f358
fix(library/tactic/cases_tactic): do not let internal exception escape
...
This was doubly ungood since the contained vm_obj was shared across
threads. @digama0 wseq.exists_of_lift_rel_left should work now.
2017-07-22 15:25:56 +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
Leonardo de Moura
3bcbfbf348
perf(library/compiler/elim_recursors): beta_reduce ==> head_beta_reduce
...
This commit fixes the byte code generation performace problem
exposed by #1755
2017-07-21 03:32:23 -07:00
Leonardo de Moura
af80c2890d
chore(library/init/meta/tactic): define focus_aux using is_assigned
2017-07-21 02:39:55 -07:00
Sebastian Ullrich
46c1a1a844
refactor(frontends/lean/elaborator,kernel/error_msgs): remove duplicate code
2017-07-21 01:46:31 -07:00
Sebastian Ullrich
f8cfc4ea1b
feat(kernel/error_msgs,frontends/lean/elaborator): add more context to 'type/function expected' errors
2017-07-21 01:46:31 -07:00
