Sebastian Ullrich
09a0397648
fix(library/init/lean/parser/reader/token): fix keyword parsing using longest_match
2018-07-13 15:51:48 +02:00
Sebastian Ullrich
8707773872
feat(library/init/lean/parser/parsec): introduce observing and longest_match primitive parser combinators
2018-07-13 15:51:00 +02:00
Sebastian Ullrich
9db0724bf1
refactor(library/init/lean/parser/parsec): monad_parsec: move from monad_lift/monad_map to direct primitives
...
This breaks the code for variable-length tokens that depended on lifting
`parsec` into `read_m`. Either `read_m` could be parameterized by its state,
or we just hard-code all variable-length tokens.
2018-07-12 17:53:43 +02:00
Sebastian Ullrich
d8122a7284
feat(src/frontends/lean/structure_cmd): allow default values in field parameters
2018-07-12 17:40:45 +02:00
Sebastian Ullrich
7cb90bedfe
fix(src/kernel/old_type_checker): literals in inductive defs
2018-07-12 10:55:28 +02:00
Sebastian Ullrich
5955e3fce8
chore(library/init/lean/parser/parsec): proper namespacing
2018-07-12 10:35:22 +02:00
Sebastian Ullrich
72b255d4e1
chore(library/init/lean/parser/parser_t): rename module and type to parsec to avoid nested use of parser
2018-07-12 10:35:20 +02:00
Sebastian Ullrich
e57117a9b3
chore(library/init/lean/parser/parser_t): revert introduction of parser_t
2018-07-11 18:44:04 +02:00
Sebastian Ullrich
6fa4e56fbe
feat(library/init/lean/parser/syntax): add and test reprinter
2018-07-11 14:34:50 +02:00
Sebastian Ullrich
b2f9b2c180
feat(library/init/lean/parser/{syntax,reader}): store whitespace around tokens
2018-07-11 14:34:50 +02:00
Sebastian Ullrich
67d93ff051
fix(library/init/lean/parser/reader/token): fix loops running out of fuel
2018-07-06 15:56:01 +02:00
Sebastian Ullrich
ab19966d65
feat(library/init/lean/parser/reader): automatically promote tokens through readers
2018-07-05 18:01:17 +02:00
Sebastian Ullrich
fbdb73665f
test(tests/lean/reader1): start testing the tokenizer on core.lean and fix a comment bug
2018-07-05 16:51:48 +02:00
Sebastian Ullrich
fea91abf88
chore(tests/lean): add leanpkg file to make sure the same cwd is used in test runs and the interactive server
2018-07-05 16:48:56 +02:00
Sebastian Ullrich
08474e04ff
fix(library/system/io): read_to_end: work around UTF-8 bug in io.read
2018-07-05 16:47:53 +02:00
Sebastian Ullrich
f254a906b3
fix(src/library/vm/vm_io): get_cwd
2018-07-05 10:53:07 +02:00
Sebastian Ullrich
6b6c16b6d6
chore(library/init/lean/parser/reader/module): remove theory command
...
We plan to allow `noncomputable`, as well as more modifiers, on `namespace/section`
2018-07-05 10:42:52 +02:00
Sebastian Ullrich
80745ba776
chore(library/init/data/string/basic): rename string.iterator's next_to_string to remaining_to_string
...
The old name implied that `curr` was not part of its result
2018-07-05 10:42:37 +02:00
Sebastian Ullrich
8ef87818ce
feat(library/init/lean/parser/reader): implement basic tokenizer
2018-07-05 10:42:37 +02:00
Sebastian Ullrich
d0e53be0dd
feat(library/init/lean/parser/parser_t): improve str's error message and allow error messages without 'unexpected' part
...
Showing the expected string at the initial position is much more helpful than
showing "unexpected <char>"
2018-07-05 10:20:25 +02:00
Sebastian Ullrich
9e51ff5580
feat(library/init/data/string/basic): add forward and is_prefix_of_remaining to iterator
2018-07-05 10:20:25 +02:00
Sebastian Ullrich
2ebbfa813c
doc(doc/coding_style,doc/commit_convention): fix git hook commands
2018-07-05 10:20:25 +02:00
Sebastian Ullrich
f31e5f407f
chore(tests/lean/run/handlers): fix test
2018-06-29 16:39:47 +02:00
Sebastian Ullrich
47f18661c5
refactor(library/init/lean/parser/parser_t): remove some uses of lift
2018-06-29 16:39:45 +02:00
Sebastian Ullrich
4e2234fd3a
feat(library/init/control/state): remove monad_state.lift to avoid allocating tuples
2018-06-28 09:56:26 +02:00
Leonardo de Moura
bda46cc9ac
feat(kernel): add inductive_decl type on top of runtime/object, and ajust kernel/inductive.cpp
2018-06-26 12:16:33 -07:00
Leonardo de Moura
bb0b43798c
feat(kernel/declaration): add wrappers for accessing inductive/constructor/recursor declarations
2018-06-25 15:01:02 -07:00
Leonardo de Moura
7684860aec
feat(kernel): add C++ wrappers for creating inductive declarations
2018-06-25 14:24:48 -07:00
Leonardo de Moura
f62256853c
refactor(library/init/lean/declaration): use lean.declaration to implement init.meta.declaration
2018-06-25 13:08:13 -07:00
Leonardo de Moura
ec1aa2553c
refactor(kernel/declaration): implement definition/constant/axiom/theorem using runtime/object
...
TODO: inductive, constructor, recursor
2018-06-25 10:05:45 -07:00
Leonardo de Moura
9c6238e1ac
refactor(kernel/declaration): reducibility hints as runtime/object
2018-06-25 08:04:44 -07:00
Leonardo de Moura
ef6ed1e660
feat(library/init/lean/declaration): add lean.declaration
2018-06-23 10:19:26 -07:00
Leonardo de Moura
fdbb1964e0
chore(library/init/lean/expr): document mvar new design
2018-06-22 15:06:36 -07:00
Leonardo de Moura
fd0f142bae
chore(kernel/expr): comment
2018-06-22 14:48:42 -07:00
Leonardo de Moura
a18c508f5c
chore(kernel/old_type_checker): fix test
2018-06-22 14:39:46 -07:00
Leonardo de Moura
f809758dd3
refactor(kernel/expr): remove extra field
2018-06-22 14:35:32 -07:00
Leonardo de Moura
e9f843ddf6
refactor(kernel/expr): remove mlocal_* functions
...
The constructors `mvar` and `fvar` have different memory layouts.
2018-06-22 14:25:31 -07:00
Leonardo de Moura
1371c636e5
refactor(kernel/expr): remove pp_name from metavariables
2018-06-22 13:12:42 -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
1063905d07
chore(kernel/expr): reorder constructors and fix typo
2018-06-22 12:39:16 -07:00
Leonardo de Moura
d0a54aceb6
refactor(kernel): remove unnecessary expr_kind printer
2018-06-22 12:35:38 -07:00
Leonardo de Moura
91d2ad5925
chore(library/init/meta): remove level and expr unused functions
2018-06-22 10:54:43 -07:00
Leonardo de Moura
318530cf07
refactor(library/init/meta/expr): use lean.expr
...
`expr` is finally non-meta
2018-06-22 10:29:56 -07:00
Leonardo de Moura
bc57c66ae3
refactor(kernel/level): naming consistency
2018-06-22 10:29:56 -07:00
Leonardo de Moura
c30f40e4ac
feat(library/init/meta/level): use lean.level
2018-06-22 10:29:49 -07:00
Leonardo de Moura
ede1a51d60
refactor(kernel/declaration): remove self_opt flag from reducibility hints
...
This flag was used by the kernel to decide whether the following
heuristic should be used to avoid unfolding `f` at `is_def_eq`.
f a =?= f b
-----------
a =?= b
This heuristic was introduced at Lean1 after a discussion with
Georges Gontier. Since this discussion, we added support for
caching failures of this heuristic. This proved to be much more
effective to attack the performance problems.
Moreover, we do not even use this flag in the `type_context::is_def_eq`
used during elaboration.
The current codebase contains only one place where this flag was set to
`false`: coercions generated at structure_cmd. This change was
made at commit
1c70514231
2018-06-22 09:02:50 -07:00
Leonardo de Moura
ee4e0d03d0
chore(frontends/lean/structure_cmd): fix bogus g++ 4.9 warning
2018-06-21 16:52:34 -07:00
Leonardo de Moura
b24ba6b93d
chore(library/compiler/simp_inductive): fix bogus g++ 4.9 warning
2018-06-21 16:52:27 -07:00
Leonardo de Moura
01ea596aea
refactor(kernel/expr): implement expr using runtime/object
2018-06-21 16:05:33 -07:00
Leonardo de Moura
9a46fb51cd
perf(runtime/object): use memcmp to implement string_lt
...
The encoding of unicode scalars into UTF8 byte stream is order
preserving. So, we can use `std::memcmp` to compare strings
2018-06-21 09:54:46 -07:00
