Gabriel Ebner
37b998ff1e
feat(frontends/lean,library/flycheck): redirect all diagnostic output from commands to flycheck
2016-10-08 22:23:53 -07:00
Leonardo de Moura
6d9a9b46f3
chore(frontends/lean): cleanup
2016-09-23 16:26:21 -07:00
Leonardo de Moura
c8e13cd391
feat(frontends/lean): minimize errors being reported
2016-09-23 09:20:31 -07:00
Leonardo de Moura
8657230435
chore(frontends/lean): new token for projections, and cleanup
2016-09-21 10:18:49 -07:00
Leonardo de Moura
318ef761d3
feat(frontends/lean): lambda+anonymous_constructor+match notation
2016-09-21 08:49:05 -07:00
Leonardo de Moura
b2e1e920a9
chore(frontends/lean,library,linja): remove .ilean files
2016-09-20 08:43:45 -07:00
Leonardo de Moura
9df712581b
chore(frontends/lean): remove 'new_elaborator' option
2016-09-20 08:32:37 -07:00
Leonardo de Moura
a1d36b6c4d
chore(library): remove legacy_type_context
2016-09-19 21:31:21 -07:00
Leonardo de Moura
335242e9f1
chore(frontends/lean): remove info_annotation module
2016-09-19 21:19:31 -07:00
Leonardo de Moura
2a069a4d2a
chore(frontends/lean): remove server and info_manager
2016-09-19 18:44:03 -07:00
Leonardo de Moura
9f1a576e98
chore(frontends/lean): remove dead code from parser
2016-09-19 17:04:59 -07:00
Leonardo de Moura
24f1cb2726
chore(frontends/lean): new_elaborator is now the default
2016-09-19 16:34:06 -07:00
Leonardo de Moura
2153661642
fix(frontends/lean/parser): missing position information
2016-09-19 13:37:22 -07:00
Leonardo de Moura
51845d1622
fix(frontends/lean/parser): support as_atomic exprs at to_pattern_fn
2016-09-18 16:55:59 -07:00
Leonardo de Moura
90bfd84a07
feat(frontends/lean): Type is now (Type 1)
...
In the standard library, we should use explicit universe variables for
universe polymorphic definitions.
Users that want to declare universe polymorphic definitions but do not
want to provide universe level parameters should use
Type _
or
Type*
2016-09-17 14:30:54 -07:00
Leonardo de Moura
5e8f2add84
refactor(library/init): use universe variables
2016-09-17 12:25:02 -07:00
Daniel Selsam
52f87760d8
feat(src/library/inductive_compiler): support for nested inductive types
2016-09-16 12:50:59 -07:00
Leonardo de Moura
20cce8a0f6
feat(frontends/lean/parser): nicer notation for providing universes
2016-09-13 20:41:00 -07:00
Leonardo de Moura
b957d3ee94
fix(frontends/lean/parser): make sure anonymous constructors can be used in patterns
2016-09-11 22:13:50 -07:00
Leonardo de Moura
1afd81384f
chore(library/let): delete let-macro hack
2016-09-10 13:06:07 -07:00
Leonardo de Moura
d8caecff49
refactor(library/exception): avoid throw_generic_exception functions
2016-09-06 12:37:56 -07:00
Leonardo de Moura
a0b8766ffb
refactor(library): merge exception modules
2016-09-06 09:12:26 -07:00
Leonardo de Moura
e18500dcd4
feat(frontends/lean/parser): _ is an anonymous variable again in patterns.
2016-08-23 14:06:24 -07:00
Leonardo de Moura
e99eb6d47e
feat(frontends/lean): revising inaccessible terms syntax again :(
2016-08-19 13:57:12 -07:00
Leonardo de Moura
50c147cd0e
feat(frontends/lean/parser): allow string literals in patterns
2016-08-18 21:00:27 -07:00
Leonardo de Moura
93d48ae620
feat(frontends/lean/parser): revised pattern validation
2016-08-17 15:42:13 -07:00
Leonardo de Moura
323701bef1
feat(frontends/lean/parser): simplify pattern semantics '_' in a pattern is always a anonymous variable
2016-08-13 22:14:40 -07:00
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
