michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
5214 commits 3 branches 0 tags 28 MiB
Commit graph

4048 commits

Author SHA1 Message Date
Leonardo de Moura
2a00647089 refactor(library/tactic): cleanup 'revert' and 'clear' tactics 2014-11-26 17:08:14 -08:00
Leonardo de Moura
4bee7554a3 chore(lean-mode): remove 'annoying' abbreviations 2014-11-26 14:50:26 -08:00
Leonardo de Moura
e55397d422 feat(library/tactic): add 'clears' and 'reverts' variants 2014-11-26 14:49:48 -08:00
Leonardo de Moura
63eafaae9a feat(emacs): add syntax-highlight for clear and revert tactics 2014-11-26 14:33:28 -08:00
Leonardo de Moura
2bd8f969d5 feat(library/tactic): add 'revert' tactic, closes #346 2014-11-26 14:23:42 -08:00
Leonardo de Moura
c28e9b9234 feat(library/tactic): add 'clear' tactic, closes #341 2014-11-26 13:11:36 -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
ea63136434 fix(src/emacs/lean-flycheck): do not report 'sorry' warnings to flycheck, this is a temporary workaround since there is an overlap between flycheck and lean-mode type info 2014-11-26 09:35:22 -08:00
Leonardo de Moura
df51ba8b7c feat(library/definitional/projection): use strict implicit inference, closes #344 2014-11-25 18:04:06 -08:00
Leonardo de Moura
ef75cac1c0 feat(kernel/expr): change the rules for inferring implicit arguments, closes #344 2014-11-25 12:54:07 -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
Soonho Kong
fe638f0ee7 fix(emacs/lean-flycheck): fix bug in advice for lean-flycheck-try-parse-error-with-pattern 
I provided an "advice" for 'flycheck-try-parse-error-with-pattern'
function to change its behavior, namely to increase error-columns by
one.

Bug
===

The problem is that it doesn't consider the case where the pattern is
not matched and ends up with "err = nil". For this case,
"(flycheck-error-column err)" generates an exception if executed. The
whole error parsing process stops immediately.

This causes a problem when we have more than one error-patterns, which
is the case when we enable 'error' and 'warning' patterns.

Fix
===

Fix is simple: check err before executing (flycheck-error-column err)

-            (col (flycheck-error-column err)))
+            (col (and err (flycheck-error-column err))))
 2014-11-24 05:06:51 -05: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
13fba433b0 feat(library/tactic/generalize): add 'generalizes' syntax sugar, closes #327 2014-11-23 17:30:22 -08:00
Leonardo de Moura
47b6cfb28d feat(library/logic/if): add dependent if-then-else: dite 2014-11-22 09:56:32 -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
e81d9c9184 perf(kernel/level): apply two simple normalization rules at mk_max 
They are variations of:
max l1 (max l1 l2) == (max l1 l2)
 2014-11-16 18:16:57 -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
8b659ae679 fix(util/lean_path): change the default LEAN_PATH, a file in the current directory cannot shadow a library file, fixes #321 2014-11-14 17:23: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
67de3b06f3 feat(kernel/level): improve universe level pretty printer 
Example: produce `l+2` instead of `succ (succ l)`.
 2014-11-14 14:51:03 -08:00
Leonardo de Moura
00df34a1c4 feat(library/unifier): generalize method process_succ_eq_max_core 2014-11-14 14:25:41 -08:00
Leonardo de Moura
ffffabad95 feat(kernel/level): improve is_geq procedure for universe levels 
Now, it also returns true for

          (succ^k1 a)  =?=  k2

where k1 >= k2
 2014-11-14 14:20:35 -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
51719145f9 feat(library/unifier): solved universe constraints of the form succ^k1 a = max k2 ?m (when k1 >= k2) 2014-11-12 17:28:33 -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
b07b82cf43 fix(library/definitional): marking cases_on and rec_on as reducible 
The idea is to avoid counter-intuitive behavior
 2014-11-12 15:03:30 -08:00
Leonardo de Moura
858538a329 refactor(library/definitional): add new to_telescope procedure, and remove code duplication in no_confusion.cpp 2014-11-12 13:31:31 -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
b4c37d180b refactor(library/definitional): add some helper functions 2014-11-12 12:24:22 -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
5fbf9ee964 refactor(library/definitional/util): remove code duplication 2014-11-11 13:53:41 -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
b4be96c980 feat(library/definitional/util): add is_inductive_predicate auxiliary predicate 2014-11-11 13:32:56 -08:00
Leonardo de Moura
4fd1ee7619 feat(library/definitional/util): add is_recursive_datatype auxiliary function 2014-11-11 12:26:26 -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
bd5f3ec572 feat(emacs/lean-syntax): highlight [decls] modifier 2014-11-10 10:35:42 -08:00
Leonardo de Moura
363d4a7577 fix(library/definitional/no_confusion): assertion violation 2014-11-10 10:32:03 -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
Soonho Kong
d25e74b921 fix(emacs/lean-mode): remove whitespace-cleanup-mode dependency 
- When customization variable 'lean-delete-trailing-whitespace' is
   non-nil, trailing-whitespaces are removed before save.

 - It doesn't change TABs.

Close #226
 2014-11-09 00:21:43 -05:00
Soonho Kong
36476b9115 fix(lean-util): handle case where incomplete hierarchical name ends with "." 
Close #311
 2014-11-08 23:46:59 -05:00
Leonardo de Moura
e8bc0f8249 feat(library/defitional): add no_confusion construction for inductive datatypes that are not propositions 2014-11-08 18:56:52 -08:00
Leonardo de Moura
b5da143fc0 feat(library/defitional): add no_confusion_type construction for inductive datatypes that are not propositions 2014-11-08 15:20:19 -08:00
Leonardo de Moura
c7992f2cac feat(frontends/lean): add [whnf] modifier to eval command 2014-11-08 10:19:29 -08:00
Soonho Kong
d861c78072 fix(emacs/lean-syntax): change comment symbols to be considered as punctuations 
Please read the documentation of "modify-syntax-entry":

"The first character of NEWENTRY should be one of the following:
  _           symbol constituent
  .           punctuation
"

Close: #306
 2014-11-07 17:48:21 -05:00
Soonho Kong
18a41eb962 feat(emacs/lean-mode): bind "C-c C-k" to quail-show-key 
- Use this to see how to type a unicode character
 2014-11-07 17:28:21 -05:00
Leonardo de Moura
b5e0ded163 feat(frontends/lean): max precedence used by Lean is not max_uint anymore 
The motivation is to allow users to define notation with higher
precedence than function application.
 2014-11-07 07:57:11 -08:00
Leonardo de Moura
85d0521d48 feat(frontends/lean): add '[parsing-only]' modifier to notation declarations, closes #305 2014-11-06 21:34:05 -08:00
Leonardo de Moura
8d05238533 fix(kernel/error_msgs): ignore binder information when comparing type mismatches, fixes #304 2014-11-06 21:03:51 -08:00
Leonardo de Moura
ed83b7ff2a fix(emacs/lean-syntax): syntax highlight, issue #306 
1- FIXED     structure foo := (bar : Type) -- the name of structures is not highlighted
2- NOT FIXED check foo-- this comment is not highlighted
3- FIXED     check Type.{5} -- Type is not highlighted
4- FIXED     definition bar{thisishighlighted : Type} := foo
5- FIXED     definition bar2 {thetypeofthisvariableisnothighlighted :Type} := foo

Have no idea what is going on with 2. I'm not sure if this is our bug,
or Emacs code we depend on.
 2014-11-06 20:59:31 -08:00
Leonardo de Moura
af88e34588 fix(kernel/inductive): bug in eliminator for recursive datatypes in Prop 2014-11-06 14:03:28 -08:00
Leonardo de Moura
be52d950f0 fix(frontends/lean): improve error message, addresses issue #299 2014-11-06 12:19:40 -08:00
Leonardo de Moura
e499f8e20a feat(kernel/inductive): relax conditions for an inductive datatype in Prop to be able to eliminate into Type 
The new relaxed version allows us to define the "accessability"
proposition and have an eliminator into Type.

See justification in the new comments at inductive.cpp
 2014-11-06 09:36:54 -08:00
Leonardo de Moura
8723f5b613 fix(frontends/lean/inductive_cmd): inductive datatype elaborator was 'fixing' parameter mismatches. 
Given a datatype C with parameters As, if the declaration contained
(C Bs), the elaborator would silently replace it with (C As).

This bug would confuse users and make them believe they define something
different.
 2014-11-05 23:12:00 -08:00
Leonardo de Moura
b3ad8c704a feat(frontends/lean/structure_cmd): allow inheritance from two identical structures, closes #296 2014-11-05 15:01:05 -08:00
Leonardo de Moura
4650791108 feat(frontends/lean): add 'print fields' command 2014-11-05 14:06:54 -08:00
Leonardo de Moura
677e0aeef6 fix(frontends/lean/structure_cmd): accept ': Type' when universe levels are not specified 2014-11-05 12:02:52 -08:00
Leonardo de Moura
d6dc624ca8 fix(frontends/lean/structure_cmd): error parsing structure without parameters followed by ': Type' 2014-11-05 12:02:52 -08:00
Leonardo de Moura
defc2478b5 feat(frontends/lean): add 'record' as an alias for 'structure' command 2014-11-05 12:02:52 -08:00
Soonho Kong
e71db7109d fix(emacs/lean-mode.el): remove quotation marks in lean-execute 
Close #294
 2014-11-05 09:20:14 -05:00
Leonardo de Moura
5b87d060cf fix(frontends/lean/structure_cmd): universe level validation 2014-11-04 22:19:23 -08:00
Leonardo de Moura
6944c7d902 fix(frontends/lean/placeholder_elaborator): local context must be adjusted when performing class-instance resolution modulo Pi-abstraction, fixes #293 2014-11-04 18:41:27 -08:00
Leonardo de Moura
b5ad0fb504 refactor(frontends/lean/local_context): add 'const' modifier 2014-11-04 18:37:31 -08:00
Leonardo de Moura
3bfe5b0b7e fix(frontends/lean): type information for "atomic" notation declaration, fixes #292 2014-11-04 18:01:20 -08:00
Leonardo de Moura
fa405d7884 refactor(frontends/lean): combine info annotations in a single module 2014-11-04 18:01:20 -08:00
Leonardo de Moura
c6c090eda6 feat(src/emacs/lean-mode): add shortcut for restarting lean server 2014-11-04 18:01:20 -08:00
Soonho Kong
2273f75e9b fix(emacs/lean-mode): handle when there is spaces in filenames 2014-11-04 19:22:35 -05:00
Soonho Kong
53e18d0e39 chore(src/CMakeLists.txt): copy linja and ltag to bin when install 2014-11-04 18:16:04 -05:00
Leonardo de Moura
60eac0195d feat(frontends/lean/structure_cmd): generate projection over constructor theorems for structures 2014-11-04 09:10:25 -08:00
Leonardo de Moura
d58c3e498d feat(frontends/lean/builtin_cmds): add 'print prefix' command 2014-11-04 08:40:32 -08:00
Leonardo de Moura
3454e70017 fix(frontends/lean/inductive_cmd): bug in expression position propagation, fixes #289 
Fix incorrect line/column number information in error messages produced
during inductive datatype elaboration.
 2014-11-04 07:44:47 -08:00
Leonardo de Moura
b6722a5d33 feat(frontends/lean/structure_cmd): add 'private' modifier for parent structures 
When it is used coercions/instances to parent structure are to registered
 2014-11-03 23:16:49 -08:00
Leonardo de Moura
b24165dc7b feat(frontends/lean/structure_cmd): remove 'cases_on' for structures since it may confuse users, add 'destruct' as alternative name for 'rec_on' 2014-11-03 23:06:33 -08:00
Leonardo de Moura
7897e21a14 feat(frontends/lean/structure_cmd): allow fields to be suppresed, but constructor to be provided 2014-11-03 22:55:51 -08:00
Leonardo de Moura
08b4ce2db9 feat(frontends/lean/structure_cmd): use 'mk' as constructor name when it is not provided 2014-11-03 22:40:08 -08:00
Leonardo de Moura
8f3139231b feat(frontends/lean/structure_cmd): allow structure declarations that contains only a header 2014-11-03 22:17:43 -08:00
Leonardo de Moura
91749d2364 fix(frontends/lean/structure_cmd): modify coercion generation 
The previous coercion was more efficient, but the computation was
getting stuck when processing algebraic structures
 2014-11-03 19:37:11 -08:00
Leonardo de Moura
edd94c00df fix(library/definitional): add missing files 2014-11-03 18:36:25 -08:00
Leonardo de Moura
c306bfa83c feat(frontends/lean/structure_cmd): add 'eta' theorem for structures 2014-11-03 18:33:44 -08:00
Leonardo de Moura
101e9966fd fix(emacs/lean-syntax): bug in syntax highlight, examples do not have names 2014-11-03 18:32:18 -08:00
Leonardo de Moura
186d910d0b feat(frontends/lean/structure_cmd): mark coercion to parents as coercions and instances (when both structures as classes) 2014-11-03 17:55:59 -08:00
Leonardo de Moura
9531203d9d feat(frontends/lean/structure_cmd): mark structure as 'class' when [class] modifier is used 2014-11-03 17:47:08 -08:00
Leonardo de Moura
b112f3c582 feat(frontends/lean/structure_cmd): add coercions to parent structures 2014-11-03 17:39:52 -08:00
Leonardo de Moura
922e66c42f fix(frontends/lean/decl_cmds): do not save 'examples' in .ilean file 2014-11-03 16:13:46 -08:00
Leonardo de Moura
7afa69577e feat(frontends/lean/structure_cmd): add aliases for structure decls 2014-11-03 15:50:41 -08:00
Leonardo de Moura
efe1105eb9 fix(frontends/lean): alias generation for composite names was not working 
This is an issue for declarations that generate composite names such as
the inductive datatype packacke.

The commit also fix a bug in the generate of aliases for recursors
 2014-11-03 15:43:58 -08:00
Leonardo de Moura
594e3ea8fc fix(frontends/lean/structure_cmd): 'rec' must be marked as protected 2014-11-03 14:50:12 -08:00
Leonardo de Moura
5872c93eaf feat(frontends/lean/structure_cmd): add structure_cmd core 2014-11-03 14:14:40 -08:00
Leonardo de Moura
a2e75159c8 fix(frontends/lean): process choice-exprs at check_constant_next 2014-11-02 19:42:30 -08:00
Leonardo de Moura
c7406d6ce8 fix(library/scoped_ext): bug when declaring nested namespaces 2014-11-02 15:35:49 -08:00
Leonardo de Moura
df008dc3c3 feat(frontends/lean/inductive_cmd): create a namespace for each declared datatype 2014-11-01 19:15:46 -07:00
Leonardo de Moura
ea55ec4090 feat(frontends/lean/decl_cmds): remove useless name from 'example' commad 2014-11-01 16:12:23 -07:00
Leonardo de Moura
1e6f7cdbb4 chore(frontends/lean/decl_cmds): add 'example' command 
It is like a theorem, but it is discarded after checking
 2014-11-01 11:37:39 -07:00
Leonardo de Moura
b1c2efecbb chore(frontends/lean/decl_cmds): add missing static 2014-11-01 11:18:10 -07:00
Leonardo de Moura
94cf10284a fix(frontends/lean/calc_proof_elaborator): bug when inserting symmetry proofs for heq, fixes #286 
The problem was that heq type is
    Pi {A : Type} (a : A) {B : Type} (b : B), Prop

The calc_proof_elaborator was assuming that (a : A) (b : B) were the
last two arguments in any relation supported by calc.

The fix is to remove this assumption.
 2014-11-01 07:30:04 -07:00
Leonardo de Moura
2688ca38bf feat(frontends/lean/inductive_cmd): notation for enumeration types 2014-10-31 19:01:32 -07:00
Leonardo de Moura
aaad9a3c43 feat(library/definitional/projection): add option for marking main premise as instance implicit (i.e., [] binder decorator) 2014-10-31 19:01:32 -07:00
Soonho Kong
cae543e665 chore(emacs): remove unnecessary requires 2014-10-31 16:01:10 -07:00
Soonho Kong
96f620adf6 doc(README.md): add Aquamacs case, ask to update lean-rootdir 
[skip ci]
 2014-10-31 09:58:15 -07:00
Leonardo de Moura
57b19b787b feat(frontends/lean/calc_proof_elaborator): when 'elaborator.calc_assistant' is on, generate same info that is generated if ! was used 2014-10-31 09:49:45 -07:00
Leonardo de Moura
dc7ab17d2a feat(frontends/lean/calc_proof_elaborator): add 'elaborator.calc_assistant' option 2014-10-31 09:49:45 -07:00
Leonardo de Moura
d7beabe91c fix(frontends/lean/calc_proof_elaborator): improve calc proof assistant 2014-10-31 09:49:45 -07:00
Leonardo de Moura
8a4d4409cd feat(frontends/lean/calc_proof_elaborator): add '{...⁻¹}' if needed in calc proofs, closes #268 
This commit also simplifies library/data/nat/basic.lean
 2014-10-31 01:02:49 -07:00
Leonardo de Moura
17df85f592 feat(frontends/lean/calc_proof_elaborator): add '{...}' if needed in calc proof steps 
This is part of #268
 2014-10-31 00:55:19 -07:00
Leonardo de Moura
42dba5cc98 feat(frontends/lean/calc): expose get_calc_subst_info and get_calc_refl_info APIs 2014-10-30 23:56:38 -07:00
Leonardo de Moura
591e566472 feat(frontends/lean): try to inject symmetry (if needed) in calc proofs, add calc_symm command for configuring the symmetry theorem for a given operator 
This is part of #268
 2014-10-30 23:24:09 -07:00
Leonardo de Moura
c5a62f8abb feat(frontends/lean): insert ! in calculational proofs when needed 
This is part of #268
 2014-10-30 22:22:04 -07:00
Leonardo de Moura
407e35692b feat(frontends/lean/calc): wrap calc proofs with 'proof-qed' annotation to identify places where proof influences what is being proved 
Later, we will add a custom annotation and elaborator for calc proofs.
This is the first step for issue #268.

Remark: we don't wrap the proof if it is of the form

   - `by tactic`
   - `begin tactic-seq end`
   - `{ expr }`
 2014-10-30 18:33:47 -07:00
Leonardo de Moura
e79c7d9852 feat(frontends/lean): make set_option affect fingerprints 2014-10-30 14:45:35 -07:00
Leonardo de Moura
498b2f681e feat(frontends/lean/placeholder_elaborator): better error message for ambiguous class-instance resolution 2014-10-30 14:44:58 -07:00
Leonardo de Moura
79f73c44dc feat(frontends/lean/placeholder_elaborator): add 'elaborator.unique_class_instances' flag, closes #265 
By default, it is false.
When it is true, class instance resolution generates an error if there
is more than one solution.
 2014-10-30 14:21:24 -07:00
Leonardo de Moura
64c3ba7b74 feat(frontends/lean): display metavariable application arguments in check command 
The idea is to "fix" counter-intuitive output like the ones were
produced in the tests check.lean and check2.lean
 2014-10-30 13:28:25 -07:00
Leonardo de Moura
dcd7e53fa7 feat(frontends/lean/builtin_cmds): remove workaround for getting nice metavariable names in the check command 
We don't need it anymore after previous commit 2a16050
 2014-10-30 13:12:45 -07:00
Leonardo de Moura
2a160508c3 feat(frontends/lean): lean --server should display meta-variables using the approach used in check command, closes #280 2014-10-30 12:45:41 -07:00
Leonardo de Moura
a1ea087f8e fix(frontends/lean/info_manager): std::set insert is a noop if set already contains an equivalent element 2014-10-30 10:35:45 -07:00
Soonho Kong
b7d805a145 feat(emacs/lean-settings): add 'lean-follow-changes' option 2014-10-29 23:58:50 -07:00
Leonardo de Moura
84b516994c fix(library/tactic): type check generalization result, fixes #273 2014-10-29 20:34:01 -07:00
Leonardo de Moura
61f333d2c2 chore(library/tactic/expr_to_tactic): fix compilation warning 2014-10-29 19:47:47 -07:00
Leonardo de Moura
6107da05db fix(frontends/lean): universe variable is treated as parameter inside section, fixes #283 2014-10-29 19:47:14 -07:00
Leonardo de Moura
9547e2d077 feat(library/tactic): add rotate_left/rotate_right tactics, closes #278 2014-10-29 19:13:55 -07:00
Leonardo de Moura
8e9f97e95e fix(frontends/lean): do not save identifier info 2014-10-29 17:38:59 -07:00
Leonardo de Moura
c1653a9fb4 feat(frontends/lean): only valid proof states should be displayed, closes #275 2014-10-29 17:29:40 -07:00
Soonho Kong
5ad312f6ce test(emacs/lean-info-test): add test cases for goal visualization 
[skip ci]
 2014-10-29 17:09:08 -07:00
Soonho Kong
6973d3e7aa feat(emacs/lean-info): add goal visualization options 'lean-proofstate-display-style' 
lean-proofstate-display-style:

 - 'show-all: Show all goals
        a : Prop,
        b : Prop,
        c : Prop,
        H_1 : a,
        H_2 : b,
        H_3 : c
        ⊢ id a

        a : Prop,
        b : Prop,
        c : Prop,
        H_1 : a,
        H_2 : b,
        H_3 : c
        ⊢ b ∧ c

 - 'show-first: Show only the first
        a : Prop,
        b : Prop,
        c : Prop,
        H_1 : a,
        H_2 : b,
        H_3 : c
        ⊢ id a

 - 'show-first-and-other-conclusions: Show the first goal, and the
   conclusions of all other goals (DEFAULT OPTION)
        a : Prop,
        b : Prop,
        c : Prop,
        H_1 : a,
        H_2 : b,
        H_3 : c
        ⊢ id a

        ⊢ b ∧ c

Close #279
 2014-10-29 17:08:55 -07:00
Leonardo de Moura
a98b12f067 fix(frontends/lean/elaborator): incorrect error position in begin-end block, fixes #276 2014-10-29 16:51:06 -07:00
Leonardo de Moura
95e843e8ed feat(library/tactic/proof_state): add empty line between goals, closes #281 2014-10-29 16:51:06 -07:00
Leonardo de Moura
b0a7888346 fix(emacs/lean-flycheck): should accept error messages with empty lines 2014-10-29 16:51:06 -07:00
Leonardo de Moura
1c9992800f fix(frontends/lean/info_manager): suppress useless tactic type information, closes #277 2014-10-29 16:51:06 -07:00
Leonardo de Moura
88d55bfef0 fix(library/definitional/projection): remove redundant 'error in' 2014-10-29 16:51:06 -07:00
Soonho Kong
854e7ba1be fix(emacs/lean-type): improve displaying proof state messages 
- Do not repeat the same message
 - Do not display the empty message
 - Do not display "[stale]" for proof states
 2014-10-29 16:02:48 -07:00
Soonho Kong
99f85c8dbc fix(emacs/lean-info): proofstate display problem 2014-10-29 14:33:05 -07:00
Soonho Kong
fe710ac6d0 test(emacs/lean-info-test): add test for proofstate info 2014-10-29 14:33:05 -07:00
Soonho Kong
17455d191b feat(emacs/lean-mode): add lean-info-mode for "*lean-info*" buffer 2014-10-29 14:33:05 -07:00
Soonho Kong
12824c3e27 fix(emacs/lean-syntax): fix Type1, Type2 highlight 2014-10-29 14:33:05 -07:00
Soonho Kong
b0e249ce63 feat(emacs/lean-type): output INFO to *lean-info* buffer in addition to minibuffer 
Close #260
 2014-10-29 14:33:05 -07:00
Soonho Kong
0d8658d762 feat(emacs/lean-settings): add lean-show-proofstate-in-minibuffer option 2014-10-29 14:33:05 -07:00
Soonho Kong
53f79ec9c2 feat(emacs): extract proof state information attached to "," 2014-10-29 14:33:05 -07:00
Soonho Kong
fdf5f3ff8a feat(emacs/lean-info): add PROOF_STATE info 
Close #259
 2014-10-29 14:33:05 -07:00
Soonho Kong
cb83eca2f3 feat(emacs/lean-input): add lean-input-export-translations 2014-10-29 14:33:05 -07:00
Leonardo de Moura
30571ce418 fix(library/definitional/projection): error messages for projection generation 2014-10-29 13:39:17 -07:00
Leonardo de Moura
fe4ea48381 feat(library/definitional/projection): add projection generator, closes #257 2014-10-29 13:13:05 -07:00
Leonardo de Moura
0c185fc4ab fix(library/tactic): add relax_main_opaque flag to proof_state objects, closes #274 2014-10-29 08:57:34 -07:00
Leonardo de Moura
a2ef835809 fix(frontends/lean): squiggle position for unary begin-end block 2014-10-28 23:26:24 -07:00
Leonardo de Moura
e22eb3543c feat(library/tactic): add whnf tactic, closes #270 2014-10-28 23:18:49 -07:00
Leonardo de Moura
83e4c0fcec feat(frontends/lean): hide tactic "types" 
it is not very useful to display the type of tactics (e.g., apply,
intros, ...)
 2014-10-28 22:38:10 -07:00
Leonardo de Moura
eeb6c72508 feat(frontends/lean): modify begin-end semantics, closes #258 2014-10-28 22:15:38 -07:00
Leonardo de Moura
1c2bbcfebc feat(frontends/lean/info_manager): add separator -- when displaying PROOF_STATE info 
This feature was implemented to address issue #259
 2014-10-28 16:39:21 -07:00
Leonardo de Moura
186e598bf8 feat(library/tactic/goal): add option pp.compact_goals 2014-10-28 16:30:37 -07:00
Leonardo de Moura
a3801e84d4 fix(library/tactic/goal): avoid unnecessary line break when possible 2014-10-28 16:17:33 -07:00
Leonardo de Moura
ea739100b3 fix(library/unifier): broken optimization in the unifier 
See new comments and tests for details.
 2014-10-28 16:09:41 -07:00
Leonardo de Moura
777aa63660 fix(kernel/inductive): relax eliminator generation rules for empty types 
This commit also removes the workaround false.rec_type. It is not needed anymore
 2014-10-28 10:31:00 -07:00
Leonardo de Moura
60f32fa709 fix(frontends/lean): begin-end automatic tactic notation bug, fixes #262 2014-10-27 17:12:25 -07:00
Leonardo de Moura
78bc3ef7e4 feat(library/unifier): improve FailLocal/FailCircular failures in the unifier by using normalization 
This improvements was marked as TODO, and was preventing us from
elaborating the example in the new test vector3.lean
 2014-10-27 16:49:29 -07:00
Leonardo de Moura
bca2be56ec feat(library/normalize): add new flavors of normalize procedure 2014-10-27 16:25:30 -07:00
Leonardo de Moura
7516fcad97 feat(kernel/type_checker): add is_stuck method, and improve ensure_pi method, closes #261 2014-10-27 13:16:50 -07:00
Leonardo de Moura
2e5ad274a5 fix(frontends/lean/elaborator): remove invalid assertions 
These assertions became invalid when we changed the behavior of undef
indentifiers at

8e6de93394
 2014-10-27 10:31:09 -07:00
Leonardo de Moura
ee5a982c01 feat(shell/lean): add '--server-trace' flag, closes #264 2014-10-27 10:26:29 -07:00
Leonardo de Moura
d66e5a6c41 fix(frontends/lean/builtin_cmds): bug (name clashing) in 'check' command new meta-variable naming 2014-10-26 19:19:45 -07:00
Leonardo de Moura
81dc201bab fix(frontends/lean/elaborator): nested begin-end bug 2014-10-26 18:23:30 -07:00
Leonardo de Moura
a544d32fcf fix(frontends/lean/elaborator): missing information when displaying unsolved placeholders 2014-10-26 16:11:58 -07:00
Leonardo de Moura
cc6a96e8ba fix(frontends/lean): improve begin-end construct 2014-10-26 15:47:29 -07:00
Leonardo de Moura
08e8161243 feat(emacs/lean-syntax): add 'eassumption' highlight 2014-10-26 15:45:26 -07:00
Leonardo de Moura
fd60cf6a79 feat(library/tactic/exact_tactic): modify 'exact' tactic semantics, use higher-order unification 
See new node.inj4 theorem, we need the extra power to be able to avoid type information at
    exact (assume e₁ e₂, e₁)
 2014-10-26 10:27:33 -07:00
Leonardo de Moura
aed9a88b38 fix(frontends/lean/parser): save identifier info for undef local 2014-10-26 10:19:44 -07:00
Leonardo de Moura
8e6de93394 fix(frontends/lean/parser): add two kinds of no_undef_id behavior: to (global) constant; to local constant 2014-10-26 09:47:11 -07:00
Leonardo de Moura
50948be66b fix(emacs/lean-syntax): syntax highlight for composite names in declarations 2014-10-26 09:27:17 -07:00
Leonardo de Moura
707584376a fix(frontends/lean/inductive_cmd): include 'induction_on', 'cases_on', and 'rec_on' into .ilean index file 2014-10-25 17:56:22 -07:00
Leonardo de Moura
c7f6a6b94e feat(library/definitional/cases_on): automatically add 'cases_on' 2014-10-25 17:22:02 -07:00
Leonardo de Moura
c751bdd9e6 chore(library/definitional): remove dead code 2014-10-25 15:11:48 -07:00
Leonardo de Moura
fa1bf40d0f fix(library/definitional): make sure argument is an inductive datatype 2014-10-25 15:09:24 -07:00
Leonardo de Moura
cdcde661ef feat(library/definitional/induction_on): automatically add 'induction_on' 2014-10-25 13:37:04 -07:00
Leonardo de Moura
a7a06ab0f8 feat(library/definitional/rec_on): automatically generate rec_on function for inductive datatypes 2014-10-25 13:08:59 -07:00
Leonardo de Moura
7240a1a640 feat(kernel/inductive): add get_num_minor_premises and get_num_type_formers APIs 2014-10-25 11:17:29 -07:00
Leonardo de Moura
2bc034da2c feat(kernel/inductive): expose 'get_elim_name' API 2014-10-25 10:47:12 -07:00
Leonardo de Moura
9e69a95b26 feat(kernel/inductive): add API for retrieving the number of indices in an inductive datatype 2014-10-25 10:42:05 -07:00
Leonardo de Moura
c30c0fa3b8 fix(kernel/metavar): avoid crash due to stack overflow, closes #253 2014-10-25 00:20:59 -07:00
Leonardo de Moura
096c67b2e5 fix(library/unifier): occurs-check bug 2014-10-25 00:16:02 -07:00
Leonardo de Moura
5830da9e2d fix(frontends/lean/tokens): typo 2014-10-24 14:44:59 -07:00
Leonardo de Moura
aaad9633fb fix(library/tactic/expr_to_tactic): memory leak 2014-10-24 14:40:36 -07:00
Leonardo de Moura
7a033ac07e feat(frontends/lean): add 'print axioms' command, close #251 2014-10-24 14:35:03 -07:00
Leonardo de Moura
db25f933b0 feat(frontends/lean): use nice names for meta-variables when executing check c and c is a constant 2014-10-24 08:23:26 -07:00
Leonardo de Moura
79d0347721 feat(library/tactic): add generalize tactic, closes #34 
Remark: the intros tactic has been added in a different commit: 7d0100a340
 2014-10-23 22:40:15 -07:00
Leonardo de Moura
b83b065d00 feat(library/tactic/apply_tactic): modify heuristic for adding arguments to apply tactic. 2014-10-23 22:36:32 -07:00
Leonardo de Moura
f9aa1a1b84 refactor(library/tactic/goal): remove unnecessary parameter 2014-10-23 21:22:52 -07:00
Leonardo de Moura
ab4c292872 fix(build): do not disable unicode chars on Windows 2014-10-23 20:58:23 -07:00
Leonardo de Moura
f027acb5cb fix(frontends/lean): missing type info in expressions nested in tactics 2014-10-23 18:31:05 -07:00
Leonardo de Moura
a6571c3273 feat(frontends/lean): add 'print definition' command 2014-10-23 14:54:15 -07:00
Soonho Kong
04b4e36701 doc(emacs/README.md): fix typo 
[skip ci]
 2014-10-23 14:32:36 -07:00
Leonardo de Moura
22ae42d3af fix(frontends/lean/info_manager): use fresh formatter displaying each info object 
The formatter may cache results.
 2014-10-23 14:29:17 -07:00
Leonardo de Moura
20ab59c740 fix(frontends/lean/pp): avoid unnecessary parentheses when pretty printing delimited notation 2014-10-23 14:14:08 -07:00
Leonardo de Moura
43cfd5c26a fix(library/tactic): add missing file 2014-10-23 14:04:12 -07:00
Leonardo de Moura
212ae0b61c feat(frontends/lean): automatically add 'info' tactic in begin-end blocks 
Actually, the tactic is only added when Lean is in collect-info mode.
 2014-10-23 13:30:04 -07:00
Leonardo de Moura
e750c9b67a feat(frontends/lean): add 'info' tactic for producing PROOF_STATE info for emacs mode 2014-10-23 13:18:30 -07:00
Leonardo de Moura
40235c6af0 fix(kernel/type_checker): propagate 'memoize' flag to default_converter 2014-10-23 13:15:53 -07:00
Leonardo de Moura
8e3ac023bb feat(library/reducible): expose 'memoize' flag 2014-10-23 13:09:59 -07:00
Leonardo de Moura
cadc9b3ff3 feat(frontends/lean/info_manager): add proof_state info 2014-10-23 10:40:07 -07:00
Leonardo de Moura
38a9aa2a98 feat(frontends/lean): automatically open 'tactic' namespace (if it is not already open) in 'by' and 'begin-end' expressions 2014-10-23 10:26:19 -07:00
Leonardo de Moura
00f9a10e82 refactor(library/tactic/unfold_tactic): use new 'tactic.expr' to implement 'unfold' tactic 
This change also enabled us to remove hacks used in the tests modified
by this commit.
 2014-10-23 10:26:19 -07:00
Leonardo de Moura
2c330e704e fix(frontends/lean/elaborator): error localization for 'expr_to_tactic' failures 2014-10-23 10:26:19 -07:00
Leonardo de Moura
6fcba192b2 refactor(library/tactic): move 'unfold' tactic to separate module 2014-10-23 10:26:19 -07:00
Leonardo de Moura
96d7d9c8d9 feat(library/tactic/elaborate): do not invoke unifier if no constraints were generated during elaboration 2014-10-23 10:26:19 -07:00
Leonardo de Moura
f3fdc70400 refactor(library/tactic): add auxiliary module 'library/tactic/elaborate' 2014-10-23 10:26:11 -07:00
Leonardo de Moura
3aec70b92c feat(library/tactic): elaborate 'exact' tactic argument at tactic execution time 2014-10-22 22:13:37 -07:00
Leonardo de Moura
c50227ea6e feat(library/tactic): change apply tactic semantics: goals are not reversed; and dependent arguments are not included 
This commit also adds the tactic rapply that corresponds to the previous
semantics we have been using.
 2014-10-22 18:11:09 -07:00
Leonardo de Moura
60132912a4 refactor(library/tactic): remove unnecessary hack 
It is not needed anymore.
We had to use this hack when we had tactic_macro_definition_cell.
 2014-10-22 17:41:19 -07:00
Leonardo de Moura
7c62446023 refactor(frontends/lean): remove dead code 2014-10-22 17:39:06 -07:00
Leonardo de Moura
eb2b59ce4f refactor(frontends/lean): remove unnecessary files 2014-10-22 17:33:16 -07:00
Leonardo de Moura
e95c7c5f70 refactor(library/tactic/rename_tactic): use new 'tactic.expr' to implement 'intro/intros' tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-10-22 17:29:50 -07:00
Leonardo de Moura
9a316092d1 refactor(library/tactic/rename_tactic): use new 'tactic.expr' to implement rename tactic 2014-10-22 17:29:50 -07:00
Leonardo de Moura
5e15ac0c92 feat(library/tactic): add new approach for embedding non-elaborated expressions into tactics 2014-10-22 17:29:50 -07:00
Leonardo de Moura
7c617955d0 refactor(library/tactic): move 'exact' tactic to separate module 2014-10-22 17:29:44 -07:00
Leonardo de Moura
323715e951 refactor(library/tactic): move 'tracing' tactics to separate module 2014-10-22 14:12:45 -07:00
Soonho Kong
ef60e6abd2 fix(shell/lean.cpp): use temp ios 2014-10-21 17:23:02 -07:00
Leonardo de Moura
33f18b9454 fix(kernel/converter): remove buggy eta-reduction and rely only on eta-expansion 
The bug is exposed by new unit test
 2014-10-21 16:54:25 -07:00
Leonardo de Moura
6b89080b1a feat(frontends/lean): do not allow user to define notation using tokens ! and @, closes #248 2014-10-21 16:28:36 -07:00
Leonardo de Moura
e24225fabf feat(frontends/lean): validate infixl/infixr/postfix/prefix declarations against reserved notations 2014-10-21 15:39:47 -07:00
Leonardo de Moura
1896e6e273 feat(frontends/lean): allow 'reserve' inside namespaces 2014-10-21 15:39:47 -07:00
Leonardo de Moura
bb953b80aa feat(frontends/lean): reserve notation, closes #95 2014-10-21 15:39:47 -07:00
Soonho Kong
ba9d0a2b7f fix(shell/CMakeLists.txt): merge into a single lean.js file 2014-10-21 16:18:12 -04:00
Soonho Kong
ec43ad51ca feat(shell/lean.cpp): use trust_lvl=10000, flycheck for EMSCRIPTEN 2014-10-21 00:43:26 -07:00
Leonardo de Moura
2f62a5e887 fix(frontends/lean/info_manager): disable notation pretty printer when displaying OVERLOAD information 
We need that otherwise the Lean emacs mode will display useless overload
information such as:

            [+] int.add : ℤ → ℤ → ℤ
            overloaded with #1 + #0, #1 + #0

Note that this only became an issue after we implemented the new pretty printer
 2014-10-20 22:06:33 -07:00
Leonardo de Moura
92acd9affc chore(emacs): do not highlight arbitrary types 2014-10-20 19:17:02 -07:00
Leonardo de Moura
815dc9b63d chore(library/tactic/expr_to_tactic): remove dead code 2014-10-20 18:59:57 -07:00
Leonardo de Moura
8a44dfc1df fix(frontends/lean/pp): bug in pretty printer notation match procedure 2014-10-20 18:58:27 -07:00
Leonardo de Moura
40fb66bf07 feat(frontends/lean): change default precedence to 1 2014-10-20 18:40:55 -07:00
Leonardo de Moura
e2fa981e89 fix(frontends/lean/pp): avoid parentheses around atomic notation 2014-10-20 18:08:13 -07:00
Leonardo de Moura
53a64ac767 refactor(library/tactic): move intros_tactic initialization to intros_tactic module 2014-10-20 17:47:52 -07:00
Leonardo de Moura
3c4419ff23 refactor(library/tactic): move rename_tactic to separate module 2014-10-20 17:41:40 -07:00
Leonardo de Moura
ac9397816f refactor(library/tactic): move apply_tactic initialization to apply_tactic module 2014-10-20 17:32:32 -07:00