Sebastian Ullrich
aadf2eb5c1
fix(library/init/lean/elaborator): resolve_global: add missing name part, append root and open resolutions
2019-01-06 18:19:12 +01:00
Sebastian Ullrich
93b0c372e0
fix(library/init/lean/elaborator): reset namespace stack at end of namespace
2019-01-06 18:17:28 +01:00
Sebastian Ullrich
b17568aeff
feat(library/init/lean/elaborator): pass current namespace to C++ elaborator
...
This seems to be the only information in `scope_mng_ext` we definitely need
2019-01-06 18:10:49 +01:00
Sebastian Ullrich
22d5d32387
feat(library/init/lean/elaborator): do name preresolution just before elaboration
2019-01-06 15:47:54 +01:00
Sebastian Ullrich
d2de703e51
feat(frontends/lean/vm_elaborator): add primitive environment.contains
2019-01-06 15:47:06 +01:00
Sebastian Ullrich
a1ecf14ebe
feat(library/init/lean/parser/syntax): syntax.to_format: show ident metadata
2019-01-06 15:45:23 +01:00
Sebastian Ullrich
9a6ae42be8
feat(frontends/lean/vm_elaborator): return new environment
2019-01-06 15:44:56 +01:00
Sebastian Ullrich
807b460e9c
feat(*/elaborator): pass preresolved names to C++ as annotations and use them for global name resolution
...
With actual preresolution still missing, the only preresolved names so far are
ones like `opt_param` from built-in macros that have been preresolved manually
(and which weren't successfully resolved before this commit because of the macro
scopes applied to them)
2019-01-01 23:59:23 +01:00
Sebastian Ullrich
38df819817
fix(library/init/lean/expander): all identifiers in terms should be ident_univs
2019-01-01 23:59:23 +01:00
Sebastian Ullrich
595590e7f5
feat(library/init/lean/elaborator): elaborate open and export
2019-01-01 13:50:21 +01:00
Sebastian Ullrich
23c83d7e06
refactor(library/placeholder,library/init/lean/elaborator): encode pexpr placeholders as anonymous mvars
2018-12-21 15:53:12 +01:00
Sebastian Ullrich
5757792345
chore(library/placeholder): remove unused placeholder type and kinds
2018-12-21 15:52:56 +01:00
Sebastian Ullrich
8753491cb5
chore(library/placeholder): remove obsolete level one_placeholder
...
Remnant of the previous Type/Sort approach
2018-12-21 15:52:56 +01:00
Sebastian Ullrich
fce5c5bd36
perf(library/init/lean/position): add file_map cache for position conversion
2018-12-20 15:32:46 +01:00
Sebastian Ullrich
dd65fbb736
refactor(library/init/lean): remove duplicate position type, rename pos to position
...
Makes it easier to work with local `pos` variables
2018-12-20 15:32:46 +01:00
Sebastian Ullrich
f7a395d035
feat(library/init/data/rbmap/basic): implement rbmap.lower_bound
2018-12-20 15:32:46 +01:00
Sebastian Ullrich
72274870ef
feat(lean4-mode/lean4-flycheck): add lean4-bootstrapped-checker
2018-12-20 14:28:18 +01:00
Sebastian Ullrich
32a3c0e62e
feat(library/init/lean/frontend,bin/lean-bootstrapped): expose new frontend as executable
2018-12-20 14:28:18 +01:00
Sebastian Ullrich
0e5cfa5e8f
feat(library/init/lean/elaborator): position on "unknown command" error
2018-12-20 14:28:18 +01:00
Sebastian Ullrich
0911d16bc3
feat(library/init/lean): compute and show error positions
2018-12-20 14:28:18 +01:00
Sebastian Ullrich
cbc297e5c5
feat(frontends/lean/vm_elaborator): resolve names in constants' types
...
This is just a stop-gap solution. We need to move name resolution to Lean to
correctly handle names preresolved by the macro expander.
2018-12-19 18:49:33 +01:00
Sebastian Ullrich
0a5af76f1a
feat(frontends/lean/vm_elaborator): capture and pass all elab messages to Lean
2018-12-19 16:22:30 +01:00
Sebastian Ullrich
ead4e8998d
feat(library/init/lean/elaborator): elaborate constants
2018-12-19 15:04:48 +01:00
Sebastian Ullrich
c5dfe7f86e
refactor(frontends/lean/decl_cmds): factor out and expose elaboration of variables and constants
2018-12-19 15:04:48 +01:00
Sebastian Ullrich
90458de7d0
feat(library/init/lean/expander): normalize type signatures of constants
2018-12-19 15:04:48 +01:00
Sebastian Ullrich
e5aaf391ff
fix(library/init/lean/parser/syntax): macro_scopes.flip
2018-12-19 15:04:48 +01:00
Sebastian Ullrich
5b44a6f93d
feat(library/init/lean/parser/parsec): structured doc_comment syntax nodes
2018-12-19 14:42:33 +01:00
Sebastian Ullrich
0cf88598d2
feat(library/init/lean/parser/declaration): stricter grammar for universe parameters and non-optional declaration types
2018-12-19 14:41:17 +01:00
Sebastian Ullrich
4f7be93e87
feat(library/init/lean): remove support for section aliases
2018-12-18 17:04:04 +01:00
Sebastian Ullrich
db6b1d6e85
feat(frontends/lean/vm_elaborator,library/init/lean/elaborator): pass parser_state between languages, create parser object on C++ side to existing functions (that don't actually parse anything)
2018-12-18 15:30:38 +01:00
Sebastian Ullrich
d214df63f1
fix(library/equations_compiler/compiler): eta-expand recursive occurrences earlier
2018-12-18 15:30:38 +01:00
Sebastian Ullrich
861136d290
feat(frontends/lean/decl_cmds): universe(s) now behaves like universe variable(s)
2018-12-17 23:30:28 +01:00
Sebastian Ullrich
4e96f092f9
feat(library/init/lean/elaborator): delegate elaboration of attribute
2018-12-14 17:38:19 +01:00
Sebastian Ullrich
0a63d39247
refactor(library/init/lean): syntax.mk_app'/mk_app ~> syntax.mk_app/mk_capp
2018-12-14 17:37:37 +01:00
Sebastian Ullrich
d9a22d43b2
feat(library/vm/vm_aux): add primitive for calling old elaborator
2018-12-14 17:36:56 +01:00
Sebastian Ullrich
1d524476b7
chore(tests/lean/parser1): restore #exit...
2018-12-12 11:06:52 +01:00
Sebastian Ullrich
ad11a8807f
refactor(library/init/lean/elaborator): also use locally in elab_scope
2018-12-12 10:58:27 +01:00
Sebastian Ullrich
83e73cd04f
feat(library/init/lean/elaborator): register declaration universe params
2018-12-12 10:42:18 +01:00
Sebastian Ullrich
009e499e95
feat(library/init/lean/elaborator): name lookup for universes
2018-12-11 19:01:56 +01:00
Sebastian Ullrich
94dec2cb9f
feat(library/init/lean/elaborator): elaborate universe
2018-12-11 19:01:41 +01:00
Sebastian Ullrich
86b4261b1d
refactor(library/init/lean/elaborator): store locally scoped data in the elab state instead of config, manually reset at scope end
2018-12-11 18:48:35 +01:00
Sebastian Ullrich
e5fec1ab00
feat(library/init/lean/elaborator): elaborate trivial headers
2018-12-07 10:32:09 +01:00
Sebastian Ullrich
306da89551
feat(library/init/lean/expander): expand universe( variable)s to multiple universe( variable) commands
2018-12-07 10:31:14 +01:00
Sebastian Ullrich
d372139d27
feat(library/init/lean/elaborator): recursively elaborate lists of commands
...
This allows the expander to expand a single command to multiple commands
2018-12-07 10:29:58 +01:00
Sebastian Ullrich
599d5c6c76
feat(library/init/lean/elaborator): log error on unknown command
2018-12-06 17:04:06 +01:00
Sebastian Ullrich
e7a6746b6a
refactor(library/init/lean): share error function between expander and elaborator
2018-12-06 17:03:01 +01:00
Sebastian Ullrich
11e5d1a8a2
chore(tests/lean/parser1): reintroduce #exit in front of core.lean test
2018-12-06 13:23:25 +01:00
Sebastian Ullrich
9c9e642210
feat(library/init/lean/elaborator): universe operators, subtype
2018-12-06 13:23:12 +01:00
Sebastian Ullrich
4b3995fac3
refactor(library/init/lean/parser/term): factor out opt_type parser
2018-12-06 13:23:12 +01:00
Sebastian Ullrich
8d3c0d4889
feat(library/init/lean/elaborator): also check to_pexpr on decl types
2018-12-06 13:23:12 +01:00
