Commit graph

27 commits

Author SHA1 Message Date
Leonardo de Moura
ff7e691d66 feat(library/vm): add support for system.platform.nbits in the VM 2018-05-03 15:54:54 -07:00
Leonardo de Moura
3771748b4c chore(library/native): remove dead code
The deleted code was not finished, and we are going to add a new IR
and compiler.
2018-02-07 17:29:25 -08: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
Jared Roesch
dc4086d0ed feat(library/vm/process): add basic process support 2017-03-28 18:08:06 -07:00
Leonardo de Moura
e9a98362d3 feat(library): functional arrays 2017-02-20 22:00:02 -08:00
Sebastian Ullrich
d15591a2d8 feat(library,frontends/lean): expose parser to Lean and use for parsing tactic parameters 2017-02-17 13:45:56 +01:00
Leonardo de Moura
6b416b4618 feat(library/vm): use native representation for int in the VM 2016-12-18 15:04:02 -08:00
Jared Roesch
e65d90ac79 feat(*): C++ code generator
in progress move of Lean.native to init
2016-12-05 16:11:41 -08:00
Gabriel Ebner
7ff2a77d67 feat(library/vm/vm_task): expose task_result objects to VM 2016-11-29 11:12:43 -08:00
Leonardo de Moura
19a6005f7e refactor(library): move user_attribute to tactic folder
It depends on tactic_state.
2016-08-26 09:28:42 -07:00
Sebastian Ullrich
ca8be3857c feat(library/user_attribute): add user-defined attributes and make attribute_manager environment-aware 2016-08-18 12:56:44 -07:00
Leonardo de Moura
7bb6ccc089 refactor(library/init/meta): qexpr ==> pexpr 2016-08-05 17:04:36 -07:00
Leonardo de Moura
ef28ae5073 feat(library/vm/vm_format,library/tactic): use thunks unit->format when producing error messages 2016-08-04 19:19:09 -07:00
Leonardo de Moura
586baa4118 feat(library,frontends/lean): support for quoted expressions in the VM, compiler and frontend
TODO: invoke elaborator at tactic.to_expr
2016-06-15 16:06:39 -07:00
Leonardo de Moura
2df6fb35e6 feat(library/vm): avoid list<A> eager conversion to vm_obj (for A in {name, level, expr}) 2016-06-09 14:16:32 -07:00
Leonardo de Moura
b28e724709 feat(library/vm): expose 'environment' C++ object 2016-06-07 17:01:17 -07:00
Leonardo de Moura
376bc8a090 feat(library/vm): expose 'declaration' C++ object 2016-06-07 15:38:48 -07:00
Leonardo de Moura
7ff06e1b2c feat(library/meta): exceptional monad 2016-06-07 15:19:43 -07:00
Leonardo de Moura
a55a936db2 feat(library/vm): expose C++ 'expr' object 2016-06-05 21:13:00 -07:00
Leonardo de Moura
1f8c58415e feat(library/vm): expose C++ 'level' object 2016-06-05 12:55:57 -07:00
Leonardo de Moura
9a14f7543c feat(library/vm): expose rb_map object 2016-06-03 13:45:06 -07:00
Leonardo de Moura
801a57dba1 feat(library/vm): expose C++ 'format' object 2016-06-02 17:37:27 -07:00
Leonardo de Moura
06cb26176c feat(library/vm): expose C++ options object 2016-06-02 11:46:17 -07:00
Leonardo de Moura
6f02d30185 feat(library/vm): add basic support for C++ name objects in the VM
We still need to add support for the recursor
2016-06-01 13:10:24 -07:00
Leonardo de Moura
e89082a97e feat(library/vm,library/init): add builtin timeit primitive for profiling 2016-05-26 12:44:49 -07:00
Leonardo de Moura
e40c54013a feat(library/vm): add basic support for IO monad 2016-05-24 17:52:22 -07:00
Leonardo de Moura
399b83122c refactor(library): move vm to a separate directory 2016-05-12 14:45:06 -07:00