Leonardo de Moura
edcc92d9c7
feat(frontends/lean): remove 'using' from structure instance command
2015-01-17 09:38:10 -08:00
Leonardo de Moura
f9d7480f5c
feat(frontends/lean): notation for creating structure instances
2015-01-16 17:14:30 -08:00
Leonardo de Moura
bfd679d52d
feat(frontends/lean/structure_cmd): allow user to reference parent structures when defining new fields
...
See new test for an example.
closes #371
2015-01-16 13:04:48 -08:00
Leonardo de Moura
13660cfecd
feat(frontends/lean/parser): add parse_qualified_expr
2015-01-16 12:42:42 -08:00
Leonardo de Moura
8ab775bd6f
feat(*): distinguish between logical and runtime exceptions.
...
Now, we use throwable as the new base class for all Lean exceptions, and
exception is the subclass for "logical" exceptions.
2015-01-15 16:54:55 -08:00
Leonardo de Moura
e48df78938
feat(frontends/lean/elaborator): do not apply delayed_coercions on equation lhs
...
The variables in the equation lhs do not have type at preprocessing
time (i.e., their type is a metavariable). So, they may seem candidates
for delayed_coercions. If the coercions are injected, we will not be
able to pattern match. Thus, we disable coercions in this case.
2015-01-13 18:05:22 -08:00
Leonardo de Moura
37e852ba61
feat(frontends/lean/elaborator): improve error message for metavariable in inaccessible position on equation lhs
2015-01-13 14:38:25 -08:00
Leonardo de Moura
41935906a8
chore(frontends/lean): use update_if_undef
2015-01-13 13:02:14 -08:00
Leonardo de Moura
4f519be55e
fix(frontends/lean/elaborator): compilation problem
2015-01-11 20:58:41 -08:00
Leonardo de Moura
75d7e4ab9e
feat(frontends/lean): add 'end' token to match expressions
2015-01-10 12:35:29 -08:00
Leonardo de Moura
5796640392
fix(frontends/lean): do report unassigned metavariables in equation lhs
2015-01-10 10:39:47 -08:00
Leonardo de Moura
b172229a72
feat(frontends/lean): add 'match' expressions
...
We reuse the equations infrastructure to compile them.
2015-01-10 10:11:13 -08:00
Leonardo de Moura
6df9ffe5f6
fix(frontends/lean/elaborator): solve placeholders before invoking equantions compiler
2015-01-10 09:18:27 -08:00
Leonardo de Moura
87d41e90fc
fix(frontends/lean/decl_cmds): store equations positions
2015-01-07 18:50:56 -08:00
Leonardo de Moura
a9b6e20a22
fix(frontends/lean): save equations position
2015-01-06 15:55:04 -08:00
Leonardo de Moura
a3a6697f44
feat(library/definitional/equations): mutually recursive functions for mutually recursive datatypes
2015-01-06 14:07:17 -08:00
Leonardo de Moura
828ce3f8dc
feat(frontends/lean/decl_cmds): minor modifications for supporting mutually recursive functions
2015-01-05 19:23:50 -08:00
Leonardo de Moura
0aa7e4a9f9
fix(frontends/lean/pp): option 'pp.private_names' should also affect private declarations defined in the current file
2014-12-28 14:22:36 -08:00
Leonardo de Moura
d2958044fd
feat(frontends/lean): add multiple_instances command
...
After this commit, Lean "cuts" the search after the first instance is
computed. To obtain the previous behavior, we must use the new command
multiple_instances <class-name>
closes #370
2014-12-21 17:28:44 -08:00
Leonardo de Moura
4421069e34
refactor(library/tactic): rename placeholder_elaborator to class_instance_synth
2014-12-19 19:57:38 -08:00
Leonardo de Moura
ded869b7e0
refactor(frontends/lean): move placeholder_elaborator to library/tactic
2014-12-19 15:23:22 -08:00
Leonardo de Moura
a22dc773b7
refactor(frontends/lean): move some auxiliary procedures to library/tactic
2014-12-19 15:19:45 -08:00
Leonardo de Moura
07d7ea2f4e
refactor(frontends/lean/placeholder_elaborator): reduce coupling between placeholder_elaborator and frontends/lean
2014-12-19 15:08:21 -08:00
Leonardo de Moura
69750c50c6
refactor(frontends/lean): move pp_options to library
2014-12-19 15:00:05 -08:00
Leonardo de Moura
caf0a4bf15
refactor(frontends/lean): move type_checker_ptr typedef to library
2014-12-19 14:40:15 -08:00
Leonardo de Moura
02de288a51
refactor(frontends/lean): move choice_iterator to library
2014-12-19 14:29:32 -08:00
Leonardo de Moura
6f78315aa4
refactor(*): add uniform names for "meta-objects"
2014-12-17 11:42:14 -08:00
Leonardo de Moura
8939351903
refactor(library): add compile_equations function, generic_exception, and cleanup elaborator_exception
2014-12-15 19:22:17 -08:00
Leonardo de Moura
5cf8064269
refactor(library): rename exists_elim and exists_intro to exists.elim
...
and exists.intro
2014-12-15 19:07:38 -08:00
Leonardo de Moura
c291063f3a
fix(frontends/lean/structure_cmd): simplify structure names
2014-12-13 14:18:02 -08:00
Leonardo de Moura
ab873cfff9
feat(frontends/lean/elaborator): replace metavariables in the equation lhs with fresh local constants before invoking compiler
2014-12-11 19:51:49 -08:00
Leonardo de Moura
91ce99d921
feat(frontends/lean): type check 'decreasing' proofs in definition using well-founded recursion
2014-12-11 18:13:35 -08:00
Leonardo de Moura
3d199d275d
fix(frontends/lean/token_table): increase binding power of decreasing operator
2014-12-11 17:31:12 -08:00
Leonardo de Moura
287a444481
feat(frontends/lean/pp): add option 'pp.numerals'
2014-12-11 17:28:58 -08:00
Leonardo de Moura
b8f665e561
feat(frontends/lean): elaborate recursive equations
...
Remark: we are not compiling them yet.
2014-12-10 22:25:40 -08:00
Leonardo de Moura
756fae7c2a
refactor(frontends/lean): move local_context to library
2014-12-10 12:43:32 -08:00
Leonardo de Moura
bf875d5778
feat(library/definitional/equations): add support for inaccessible patterns
2014-12-10 12:35:08 -08:00
Leonardo de Moura
d98aabe9ab
refactor(library): move library/definitional/util module to library
2014-12-10 11:23:23 -08:00
Leonardo de Moura
ac664505e6
refactor(library): move class management to library module
2014-12-09 21:38:55 -08:00
Leonardo de Moura
05f27b8f0e
feat(frontends/lean/structure): add option for controlling whether we automatically generate eta and projection-over-intro theorems for structures
...
It seems most of the time these theorems are not used at all.
They are just polluting the namespace.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-12-09 12:40:09 -08:00
Leonardo de Moura
d67583df44
fix(frontends/lean/parser): do not generate error when 'exit' command is used
2014-12-09 10:14:14 -08:00
Leonardo de Moura
58432d0968
feat(library/definitional): add no_confusion construction that is compatible with the HoTT library
2014-12-08 22:11:48 -08:00
Leonardo de Moura
2bb51554d5
feat(library/definitional/util): add telescope equality for HoTT library
...
This is needed for implementing no_confusion for HoTT.
We can't use heterogeneous equality in HoTT.
2014-12-07 18:35:55 -08:00
Leonardo de Moura
ec7f90cb16
feat(hott/init): make sure eq is universe polymorphic
...
Jakob and Floris needed path equality to be universe polymorphic when
proving univalence.
2014-12-06 09:43:42 -08:00
Leonardo de Moura
53d6d76162
fix(frontends/lean/parser): generate error when 'exit' command is used
...
m_theorem_queue.join() method assumes there are no open namespaces/scopes
2014-12-05 16:12:23 -08:00
Leonardo de Moura
eb87c18693
feat(*): add support for separate HoTT library
2014-12-05 14:34:02 -08:00
Leonardo de Moura
e868ecce36
feat(frontends/lean): parse recursive equations
2014-12-04 17:03:21 -08:00
Leonardo de Moura
7a6d674b8e
refactor(frontends/lean/decl_cmds): cleanup definition_cmd
2014-12-04 16:03:29 -08:00
Leonardo de Moura
52334dca29
feat(frontends/lean): parse "decreasing" expressions
2014-12-04 15:11:23 -08:00
Leonardo de Moura
e72c4977f0
feat(frontends/lean): nicer notation for dependent if-then-else
2014-12-04 11:13:09 -08:00
Leonardo de Moura
0443c1e70c
fix(frontends/lean): intro tactic + universe variables, fixes #362
2014-12-03 12:56:30 -08:00
Leonardo de Moura
fca97d5bb2
feat(library/definitional): add brec_on construction, closes #272
2014-12-03 10:39:32 -08:00
Leonardo de Moura
5b2d17e4ab
feat(frontends/lean): add 'print notation' command
2014-12-02 12:04:18 -08:00
Leonardo de Moura
8c50048d1b
chore(frontends/lean/pp): fix style
2014-12-01 17:15:30 -08:00
Leonardo de Moura
320971832d
feat(frontends/lean/pp): add hard-coded pretty printer for nat numerals
2014-12-01 16:07:55 -08:00
Leonardo de Moura
8dfd22e66c
feat(frontends/lean): add 'prelude' command, and init directory
2014-11-30 17:03:08 -08:00
Leonardo de Moura
2281fb30c8
refactor(library): use "symbolic" precedences in the standard library
2014-11-29 19:08:37 -08:00
Leonardo de Moura
2c0472252e
feat(frontends/lean): allow expressions to be used to define precedence, closes #335
2014-11-29 18:29:48 -08:00
Leonardo de Moura
2487e3b83d
fix(frontends/lean/parser): user provided numeral notation should have precedence over the default based on 'num'
2014-11-29 17:29:03 -08:00
Leonardo de Moura
bc65aeb5e1
fix(frontends/lean/calc): add expected type for single-step calc expressions, fixes #357
...
This is not an issue for calc expressions containing multiple steps,
since the transitivity step will "force" the expected type for the proofs.
2014-11-29 15:35:09 -08:00
Leonardo de Moura
a97d7ffed7
feat(frontends/lean/builtin_cmds): display 'print' command output as flycheck information
2014-11-29 13:31:42 -08:00
Leonardo de Moura
366bf70ccd
fix(frontends/lean/elaborator): do not display flycheck related messages when --flycheck is not on
2014-11-28 21:20:25 -08:00
Leonardo de Moura
8b804f1d22
feat(frontends/lean): add option 'elaborator.flycheck_goals'
2014-11-28 16:34:02 -08:00
Leonardo de Moura
9516cd9ee3
feat(library/tactic): 'exact' tactic report unsolved placeholders in nested expression
...
Actually, the elaborator is the one reporting the unassigned
placeholders. The 'exact' tactic just makes the request.
To implement this feature we had to extend the elaboration interface
expected by the tactic framework.
2014-11-28 14:59:35 -08:00
Leonardo de Moura
4ec2101b06
feat(frontends/lean): add option 'pp.purify_locals'
2014-11-28 14:49:00 -08:00
Leonardo de Moura
db9fd53b80
fix(library/tactic): pretty printer for proof states
2014-11-27 09:43:58 -08:00
Leonardo de Moura
ffdeb0edc4
fix(frontends/lean/elaborator): unsolved metavariables, fix #329
2014-11-26 11:56:39 -08:00
Leonardo de Moura
24a15b6c46
fix(frontends/lean): disable class-instance resolution when executing find_decl, fixes #343
2014-11-24 21:33:52 -08:00
Leonardo de Moura
a005c8f4d0
feat(frontends/lean): display eval/check/find_decl results using flycheck
2014-11-24 08:35:49 -08:00
Leonardo de Moura
d81a6259e8
feat(frontends/lean/find_cmd): add options for controlling find_decl
2014-11-24 00:16:10 -08:00
Leonardo de Moura
f1e915a188
feat(frontends/lean): add 'find_decl' command
2014-11-23 23:00:59 -08:00
Leonardo de Moura
8c8bf41e39
feat(frontends/lean/server): do not unfold definitions in FINDG
2014-11-23 19:03:39 -08:00
Leonardo de Moura
44a2ef8f6f
fix(frontends/lean/parser_config): binder(s) rbp was not being saved in .olean file
2014-11-23 17:49:14 -08:00
Leonardo de Moura
64686c1278
feat(frontends/lean): allow user to associate precedence to binders, closes #323
2014-11-23 17:30:46 -08:00
Leonardo de Moura
cf3b0e1087
feat(frontends/lean/placeholder_elaborator): apply substitution before collecting local instances, closes #333
2014-11-23 17:30:46 -08:00
Leonardo de Moura
5d5fd2da50
fix(frontends/lean): tactic + section variables, fixes #332
2014-11-21 10:07:16 -08:00
Leonardo de Moura
28c63e685b
feat(frontends/lean): add '[local]' notation, closes #322
2014-11-16 21:15:04 -08:00
Leonardo de Moura
ea640257bf
feat(frontends/lean/structure_cmd): generate no_confusion for structures too
2014-11-15 16:00:09 -08:00
Leonardo de Moura
7685516d1e
feat(frontends/lean): better default for atomic notation
2014-11-14 16:25:13 -08:00
Leonardo de Moura
488f989c46
fix(frontends/lean/inductive_cmd): generate error for inductive datatype declarations that will produce an eliminator that can only eliminate to Prop
2014-11-14 13:57:42 -08:00
Leonardo de Moura
58525905d0
fix(frontends/lean/notation_cmd): bugs in 'reserve notation' command
2014-11-13 22:05:55 -08:00
Leonardo de Moura
6bc89f0916
feat(library/definitional): define ibelow and below
...
These are helper definitions for brec_on and binduction_on
2014-11-12 16:38:46 -08:00
Leonardo de Moura
a3066e3eaa
fix(frontends/lean/inductive_cmd): bug in inductive datatype elaborator
2014-11-12 13:10:19 -08:00
Leonardo de Moura
5312afa7ec
feat(frontends/lean/inductive_cmd): improve resulting universe level inference for inductive datatypes
...
The new test contains examples that required explicit levels.
2014-11-12 10:52:32 -08:00
Leonardo de Moura
e2bfe6ee36
refactor(library/definitional/no_confusion): cleanup API
2014-11-11 16:12:44 -08:00
Leonardo de Moura
f6889951c6
fix(library/definitional/cases_on): bug in inductive datatypes with higher-order recursion
2014-11-11 15:14:08 -08:00
Leonardo de Moura
902a551048
feat(definitional/brec_on): add 'mk_below' skeleton
2014-11-11 14:55:21 -08:00
Leonardo de Moura
1079d6b320
refactor(library/definitional): combine auxiliary functions used by definitional package in a single module
2014-11-11 13:46:36 -08:00
Leonardo de Moura
50973bb4f3
feat(frontends/lean): default 'eval' command ignores opaque/irreducible annotations
...
To retrieve the previous behavior, we should use [strict] modifier
2014-11-10 12:46:04 -08:00
Leonardo de Moura
95554a527c
feat(frontends/lean/placeholder_elaborator): display instance trace header once per class-instance resolution problem
2014-11-09 15:00:13 -08:00
Leonardo de Moura
fa26c2301c
fix(frontends/lean): fix pretty-printing spacing problem
2014-11-09 14:49:43 -08:00
Leonardo de Moura
3aac26d658
fix(frontends/lean): tactic + variables bug, fixes #315
2014-11-09 14:43:22 -08:00
Leonardo de Moura
eff3c6b774
feat(frontends/lean): add variation of the foldl/foldr notation where initial element is suppressed, closes #314
...
See tests/lean/fold.lean for examples
2014-11-09 14:08:33 -08:00
Leonardo de Moura
ce889ddf60
feat(frontends/lean/scanner): disallow hierarchical names such as 'x.1'
2014-11-09 12:55:13 -08:00
Leonardo de Moura
df5a17cdce
feat(frontends/lean/placeholder_elaborator): include type in class-instance resolution trace
2014-11-09 12:06:16 -08:00
Leonardo de Moura
1d9a0a6265
feat(frontends/lean/placeholder_elaborator): add option 'elaborator.instance_max_depth'
2014-11-09 11:59:44 -08:00
Leonardo de Moura
9b9ae128d5
feat(frontends/lean): include file-name and line/col numbers when displaying class-instance resolution trace
2014-11-09 11:47:01 -08:00
Leonardo de Moura
6362610411
fix(frontends/lean): include position information
2014-11-09 11:43:44 -08:00
Leonardo de Moura
76fb6893e1
feat(frontends/lean): add elaborator.trace_instances option
...
When on this option allows us to visualize "class-instance resolution"
2014-11-09 11:24:19 -08:00
Leonardo de Moura
0b8c44a94a
feat(frontends/lean): add option pp.purify_metavars
...
It is true by default. If the user sets it to false, then
the internal metavariable names are used in the pretty printer
2014-11-09 11:04:22 -08:00