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

39 commits

Author SHA1 Message Date
Leonardo de Moura
7c76a19885 chore: fix includes 2020-05-22 14:17:25 -07:00
Leonardo de Moura
8bdca35282 chore: use #include <lean/runtime/...> for runtime .h files 2020-05-18 11:30:07 -07:00
Leonardo de Moura
61274c7d35 feat(library/init/data/char): use uint32 instead of nat for defining char 2019-02-15 18:07:55 -08:00
Leonardo de Moura
58e91559d0 feat(*): use new inductive datatype module 2018-09-06 18:09:22 -07:00
Leonardo de Moura
3729c7ffb2 chore(kernel/expr): remove some old/legacy functions 2018-06-22 12:52:14 -07:00
Leonardo de Moura
13c532d0d4 fix(*): truncation bugs 
- Lean strings (like std::string) may contain null characters. The
  codebase was ignoring this issue.

- We now have a wrapper `string_ref` for wrapping Lean string objects in
  C++. This wrapper also implements correctly the coercions std::string <-> string_ref.
  Remark: I also found a few places where the code relies on the
  following property which is not true
  Forall s : std::string, std::string(s.c_str()) == s

- `name` object wrapper was assuming that all numerals were small
  `nat` values. This is true in most cases, but the system would
  crash when processing if it is a big number.

- The commit tries to make sure runtime/util/kernel are correct.
  Modules that will be deleted contain many `TODO` comments
  indicating they may crash and/or produce incorrect results
  when strings contain null characters and numerals are big.

cc @kha

@kha: I thought about using `string` instead of `string_ref`.
We consistently use `std::string`. So, it should be fine, but I
was concerned about code readability.

After we bootstrap Lean4, we will be able to delete `lean::list`
template, and rename `lean::list_ref` to `lean::list`.

I am going to add `pair_ref` for wrapping Lean pair objects.
If we use `lean::string` instead of `lean::string_ref`, then
we should also use `lean::pair` instead of `lean::pair_ref`.
But, there is a problem in this case since we have
https://github.com/leanprover/lean4/blob/master/src/util/pair.h#L13
:(
 2018-06-15 16:05:11 -07:00
Leonardo de Moura
8101b9df6e refactor(library/string): remove string_macro 
We now use expr_lit.
 2018-06-14 16:26:39 -07:00
Leonardo de Moura
c0e1d05199 chore(kernel): type_checker ==> old_type_checker 2018-06-06 16:10:40 -07:00
Leonardo de Moura
8ee2f4fea1 feat(*): basic runtime string support 2018-05-14 16:52:55 -07:00
Sebastian Ullrich
734ee66514 fix(library/string): unicode char literals 2017-10-27 09:48:09 -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
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
Gabriel Ebner
16fb5ade58 fix(library/string): correctly escape non-printable characters 
This also fixes a compiler warning on ARM, where `0 <= c` is always
true.
 2017-06-23 20:39:41 +02:00
Leonardo de Moura
4eefc41b6e refactor(*): wrap string in a structure 
We want to make sure string users do not depend on the string
implementation. This is the first step.

We need this refactoring *now* to make sure it will not be
super painful to address issue #1175
 2017-06-07 17:30:49 -07:00
Sebastian Ullrich
491802409a chore(*): remove unused macro_definition_cell::pp method 2017-05-24 09:51:23 +02:00
Leonardo de Moura
73b4e42485 chore(frontends/lean,library): fix character pretty printer 2017-05-02 13:17:22 -07:00
Leonardo de Moura
df91ae3738 fix(library/string,library/init/data/to_string): handle ASCII control characters 2017-01-11 23:44:33 -08:00
Leonardo de Moura
acef1efb86 fix(frontends/lean/pp,library/equations_compiler,library/tactic/smt/congruence_closure): bug at to_char function 2017-01-11 23:44:25 -08:00
Leonardo de Moura
a30081a715 feat(library/tactic/congruence/congruence_closure): interpreted values in the same equivalence class 2016-12-25 11:09:55 -08:00
Leonardo de Moura
17cc40b35e feat(library/tactic/congruence/congruence_closure): do not recurse on values and instances when internalizing terms 2016-12-23 13:24:43 -08:00
Leonardo de Moura
98fbe76f30 feat(library/comp_val): add mk_string_val_ne_proof 2016-11-23 13:19:24 -08:00
Leonardo de Moura
dfd2a23cd4 feat(frontends/lean): use #"c" instead of 'c' for character literals 
The new notation is the same one used in Standard ML.
It will also allow us to use ' in the beginning of identifiers like Standard ML.
 2016-11-17 11:35:54 -08:00
Leonardo de Moura
20276f9b93 feat(frontends/lean/pp): pretty print character literals 2016-08-18 17:14:50 -07:00
Leonardo de Moura
4e5b8e8d0e fix(library/string): conversion from std::string to lean expr 2016-05-31 16:19:01 -07:00
Leonardo de Moura
6a9e5079c9 feat(library,frontends/lean/pp): add support for new string encoding 2016-05-24 16:20:43 -07:00
Leonardo de Moura
487a1e7f89 refactor(kernel): remove extension_context 
We replaced it with abstract_type_context
 2016-03-19 15:15:39 -07:00
Leonardo de Moura
e7f1f409c4 refactor(kernel): simplify kernel type_checker 
TODO: cleanup, move justification/metavar/constraints to library
 2016-03-18 16:28:42 -07:00
Leonardo de Moura
061e26157e fix(kernel,library): make sure macros check relevant arguments when kernel is performing full type checking 2015-05-08 12:41:23 -07:00
Leonardo de Moura
27f6bfd3f0 refactor(*): add file constants.txt with all constants used by the Lean binary 2015-01-23 16:50:32 -08:00
Leonardo de Moura
92c424936a refactor(kernel/macro_definition_cell): improve macro get_type API 2014-10-07 16:38:31 -07:00
Leonardo de Moura
b6781711b1 refactor(*): explicit initialization/finalization for serialization 
modules, expression annotations, and tactics
 2014-09-22 15:26:41 -07:00
Leonardo de Moura
364bba2129 feat(frontends/lean/inductive_cmd): prefix introduction rules with the name of the inductive datatype 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-04 17:26:36 -07:00
Jeremy Avigad
6264fb52d6 fix(lean/library/standard): fix tests, more cleanup 2014-08-20 18:04:31 -07:00
Leonardo de Moura
9588336c15 refactor(kernel/type_checker): remove "global" constraint buffer from type_checker, and use constraint_seq instead 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-20 16:46:19 -07:00
Leonardo de Moura
0d97fff280 feat(library/module): include name of corrupted .olean file 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-14 11:28:44 -07:00
Leonardo de Moura
105c29b51e refactor(library/standard): use new coding style, rename bool.b0 and bool.b1 to bool.ff and bool.tt 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-28 19:59:38 -07:00
Leonardo de Moura
b522ea6f2d refactor(library/standard): rename bit to bool 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-22 09:49:54 -07:00
Leonardo de Moura
405e57eb2d refactor(kernel/formatter): add formatter_factory, and simplify formatter interface 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-10 18:32:00 +01:00
Leonardo de Moura
a66a08c89e feat(frontends/lean): parse strings as expressions of type 'string.string' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-02 10:00:55 -07:00