Leonardo de Moura
80b6bb47f8
feat(frontends/lean): parse mutual_definition
2016-08-11 13:47:52 -07:00
Leonardo de Moura
fc4e304b27
refactor(library): move equations to equations_compiler
2016-08-11 10:08:30 -07:00
Leonardo de Moura
f056f0f2cb
refactor(library): definitional ==> constructions
2016-08-11 10:08:22 -07:00
Leonardo de Moura
f5c35f8d76
chore(*): fix compilation warnings
2016-08-10 18:03:13 -07:00
Leonardo de Moura
a0a72b5b82
refactor(frontends/lean): move local_context_adapter to separate folder
2016-08-10 07:52:38 -07:00
Sebastian Ullrich
82657b3b64
refactor(library/compiler/inliner, library): replace inline command with attribute
...
sed -Ei 's/inline (protected )?(meta_)?definition (\S+)/\1\2definition \3 [inline]/' library/**/*.lean
2016-08-08 12:45:22 -07:00
Sebastian Ullrich
c3ea0c1852
refactor(frontends/decl_cmds): simplify definition parsing logic
...
Also restrict syntax to `inline? (private|protected)? noncomputable?`
2016-08-08 12:44:37 -07:00
Leonardo de Moura
1602a53336
feat(frontends/lean): nary match
2016-08-08 10:04:58 -07:00
Leonardo de Moura
b9c62af37d
feat(frontends/lean/parser): remove unnecessary restriction
2016-08-07 11:40:39 -07:00
Leonardo de Moura
1e6b3614ab
feat(frontends/lean): new pattern matching validation
...
@Kha, we now support variable/constant shadowing in patterns.
A constant may occur in a pattern if it is a constructor or tagged with
the new [pattern] attribute. In the standard library, I have tagged
'add', 'zero', 'one', 'bit0', 'bit1' and 'rfl' with this new attribute.
BTW, arbitrary constants and variables may occur nested in type ascriptions and
inaccessible terms.
Here is an example:
meta_definition tactic_result_to_string {A : Type} : tactic_result A → string
| (success a s) := to_string a
| (exception ⌞A⌟ e s) := "Exception: " ++ to_string (e ())
I had to use the inaccessible ⌞A⌟ in the example above, otherwise, we would be shadowing the parameter
{A : Type}, and we would get a type error.
The new validation is performed at to_pattern_fn (parser.cpp).
2016-08-07 11:31:11 -07:00
Leonardo de Moura
d36280f74f
refactor(frontends/lean): id_behavior
2016-08-07 08:07:24 -07:00
Leonardo de Moura
b6420904f5
feat(frontends/lean): resolved quoted names
2016-08-05 17:04:36 -07:00
Leonardo de Moura
aeafe0293b
feat(frontends/lean/structure_cmd): use new elaborator to process the structure command
2016-08-03 16:56:41 -07:00
Leonardo de Moura
e87b54988b
feat(frontends/lean/elaborator): minor cleanup
2016-08-03 13:25:49 -07:00
Leonardo de Moura
2c8e484aa3
feat(frontends/lean/elaborator): universe parameter name sanitizer
2016-08-03 13:13:44 -07:00
Leonardo de Moura
4e80094927
feat(frontends/lean/inductive_cmd): use new elaborator in the inductive command
2016-08-03 13:13:12 -07:00
Leonardo de Moura
dcba76ba7e
feat(frontends/lean/parser): at parser::elaborate convert metavar_decl_ref's into regular metavars
2016-08-02 14:45:04 -07:00
Leonardo de Moura
8127ba9a5f
feat(frontends/lean/parser): adapter for converting local_expr_decls ==> local_context
2016-08-01 14:52:01 -07:00
Leonardo de Moura
09c000fcb8
chore(frontends/lean/elaborator): remove unnecessary field
2016-07-31 19:54:04 -07:00
Leonardo de Moura
e5298c9d8f
feat(frontends/lean/elaborator): modify the pre-term for overloaded notation
...
The new encoding is better for the new elaborator.
2016-07-31 17:14:01 -07:00
Leonardo de Moura
1aeda0e74b
feat(frontends/lean/elaborator): invoke tactics
2016-07-31 11:56:52 -07:00
Sebastian Ullrich
e69b508492
refactor(library/export_decl): Re-implement for new scoped_ext
...
Use environment_extension to persist mapping from namespaces to export
decls, use new scoped_ext to keep track of currently active export decls.
2016-07-29 23:44:22 -04:00
Leonardo de Moura
931251d403
feat(frontends/lean): remove local_context from parser
2016-07-28 16:19:31 -07:00
Leonardo de Moura
dcf0244ecd
chore(frontends/lean/parser): remove dead code
2016-07-28 09:56:03 -07:00
Leonardo de Moura
e6627cdfc1
feat(frontends/lean/parser): add new_elaborator option
2016-07-28 09:48:12 -07:00
Leonardo de Moura
3a5f6f2e64
feat(frontends/lean/builtin_cmds): improve output produced by #elab command, use kernel type checker to check elaboration result
2016-07-27 15:29:25 -07:00
Leonardo de Moura
3218f91e35
feat(frontends/lean): add support for character literals
2016-07-18 14:07:10 -04:00
Leonardo de Moura
f34e84dacb
feat(frontends/lean/parser): cute binders
2016-07-08 07:50:58 -07:00
Leonardo de Moura
58569b82d3
refactor(frontends/lean,library,library/tactic): move type_context_cache_helper to type_context module
2016-06-30 12:03:40 +01:00
Leonardo de Moura
1a5756661f
refactor(frontends/lean,library): move scope_pos_info_provider to library
2016-06-30 10:19:35 +01:00
Leonardo de Moura
bb70fbbd48
refactor(frontends/lean): simplify elaborator_context
2016-06-29 16:56:19 +01:00
Leonardo de Moura
ccc65c6171
refactor(frontends/lean): add thread local parser_pos_provider
2016-06-29 16:09:06 +01:00
Leonardo de Moura
f3803c6ee4
refactor(frontends/lean/elaborator_context): remove io_state from elaborator_context
2016-06-27 06:29:54 +01:00
Leonardo de Moura
2ea8b26c4f
refactor(library/io_state): move get_global_ios to io_state module
2016-06-25 20:59:52 -07:00
Leonardo de Moura
77286e6abb
fix(frontends/lean): replay exported decls in imported files
2016-06-25 12:13:36 -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
3996f9db4d
feat(frontends/lean): add ( token and remove token
2016-06-15 13:22:31 -07:00
Leonardo de Moura
5459e9ad8a
chore(frontends/lean): remove dead code
2016-06-13 10:42:38 -07:00
Leonardo de Moura
b54203f6b3
feat(frontends/lean): parse by-expression
2016-06-13 10:25:26 -07:00
Leonardo de Moura
d302514933
chore(frontends/lean): remove tactic notation
2016-06-10 18:29:41 -07:00
Leonardo de Moura
e7b47a504e
feat(frontends/lean): add meta_definition and meta_constant commands
2016-06-01 09:12:41 -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
fdea718d9d
chore(frontends/lean): remove all #include "library/tactic.*" from frontends/lean
2016-04-25 15:41:12 -07:00
Leonardo de Moura
d88098f38d
chore(frontends/lean): remove some of the tactic support
2016-04-25 15:26:56 -07:00
Leonardo de Moura
d66406a1f4
feat(frontends/lean): add #elab command for testing new elaborator
2016-04-05 17:03:23 -07:00
Leonardo de Moura
03809e7973
refactor(frontends/lean): elaborator_context
2016-04-05 16:19:06 -07:00
Leonardo de Moura
a1bc662eca
dev(frontends/lean/parser): add local_context
2016-03-30 16:33:17 -07:00
Leonardo de Moura
06ef0ad7be
refactor(frontends/lean): add local_level_decls
...
Remark: the template local_decls will be deleted in the future.
The instances local_expr_decls will be replace by local_context.
2016-03-30 15:47:32 -07:00
Leonardo de Moura
c4f25cf15b
refactor(frontends/lean): rename elaborate methods
2016-03-30 15:05:24 -07:00
Leonardo de Moura
75549bafd7
refactor(frontends/lean/elaborator): rename elaborator to old_elaborator
2016-03-30 14:59:18 -07:00
