max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
11727 commits 1 branch 0 tags 5.3 GiB
Commit graph

2608 commits

Author SHA1 Message Date
Daniel Selsam
7dcc36277a feat(frontends/lean/inductive_cmds.cpp): better resultant universe inference 2017-03-07 12:55:01 -08:00
Leonardo de Moura
f2faea9b9f refactor(frontends/lean/equations_validator): move validation code to another file 2017-03-06 14:36:42 -08:00
Daniel Selsam
5f0ebf90de fix(frontends/lean/structure_cmd): call inductive compiler without params in type 2017-03-06 14:01:46 -08:00
Sebastian Ullrich
2394f1faa5 fix(frontends/lean/util): do not fall back to current position 2017-03-06 11:02:51 -08:00
Sebastian Ullrich
c4ebfab14c fix(frontends/lean/structure_cmd): inheriting defaulted field depending on field starting with implicit parameter 2017-03-06 11:02:51 -08:00
Sebastian Ullrich
87b98d5aa2 fix(frontends/lean/structure_cmd): fix assertion violation when field depends on defaulted field 2017-03-06 11:02:50 -08:00
Daniel Selsam
ce1ec69ea6 fix(frontends/lean/decl_utils.cpp): closes #1417 2017-03-06 10:54:22 -08:00
Leonardo de Moura
045fe4ad25 fix(frontends/lean/structure_cmd): allow default values for function fields 2017-03-06 07:41:42 -08:00
Leonardo de Moura
61c9a7d466 feat(frontends/lean/elaborator): address issue described at https://github.com/leanprover/lean/issues/1403#issuecomment-282846138 
see #1403
 2017-03-05 21:01:12 -08:00
Leonardo de Moura
fa99861788 feat(frontends/lean/elaborator): add new ^. notation 
see #1403
 2017-03-05 20:12:49 -08:00
Sebastian Ullrich
876a2bee46 feat(frontends/lean/elaborator): flag expr quotes containing universe params 2017-03-05 08:37:16 -08:00
Sebastian Ullrich
5d68938a9c feat(frontends/lean): expr literals ```(...) 2017-03-05 08:37:16 -08:00
Leonardo de Moura
17556758cb feat(library/constructions,library/inductive_compiler): automatically generate dependent eliminator for inductive predicates 
The dependent eliminator for an inductive predicate C is called C.drec

TODO: construct dcases_on and drec_on using C.drec

We need this recursor for implementing dependent elimination for
inductive predicates.

We don't need to define acc.drec and eq.drec in the standard library anymore.
 2017-02-28 20:58:04 -08:00
Leonardo de Moura
1fa1312c57 chore(CMakeLists,frontends/lean): add SAVE_SNAPSHOT=OFF SAVE_INFO=OFF compilation options 2017-02-28 12:09:19 -08:00
Gabriel Ebner
fcc0f30b84 fix(frontends/lean/definition_cmds): set scope_pos_info when checking examples 2017-02-25 12:56:46 -08:00
Leonardo de Moura
52221cdbd1 fix(frontends/lean/elaborator): {} elaboration issue 2017-02-24 21:20:39 -08:00
Leonardo de Moura
552a185e6a feat(frontends/lean): 'let' in 'do' blocks 2017-02-24 09:10:36 -08:00
Sebastian Ullrich
dfe1874365 refactor(frontends/lean/{parser,util}): extract quote functions 
Also fixes ``f when f is private
 2017-02-23 01:52:13 +01:00
Sebastian Ullrich
1c7ca3f20a feat(frontends/lean/parser): ignore implicit arguments in expr patterns 2017-02-23 01:52:13 +01:00
Sebastian Ullrich
908a7bd9f3 feat(frontends/lean/parser): expr patterns 2017-02-23 01:52:13 +01:00
Leonardo de Moura
ca31ad0107 perf(library/metavar_util): quadratic behavior when assembling the final proof 
The peformance problem was affecting theorems that contain many `intro`
tactic applications.

@gebner After this optimization, the GAPT benchmark elaboration time went from
1.6 secs to 0.6 secs.
 2017-02-21 21:02:43 -08:00
Leonardo de Moura
622e9a6035 feat(library/type_context): use m_unfold_pred to decide whether macros should be unfolded or not 
see #1394
 2017-02-21 18:07:39 -08:00
Sebastian Ullrich
a053175714 refactor(init/meta,library/vm): use structure for position information 2017-02-21 11:06:39 -08:00
Leonardo de Moura
61254847fb fix(frontends/lean/structure_cmd): when error recovery is enabled, we must not assume the expression in the fixed line is a binding expression (it may be a sorry expression) 2017-02-20 14:51:59 -08:00
Leonardo de Moura
ddee94b831 fix(frontends/lean/elaborator): incorrect invariant due to error recovery 
We cannot assume both source and target are binding expressions.
The source has already been elaborated, and it may be a `sorry` because
of error recovery code.
 2017-02-20 14:30:10 -08:00
Leonardo de Moura
0d22410e2e feat(library/tactic): add zeta option, refactor simplify config option, allow users to change simplify_config in interactive mode 2017-02-19 12:11:22 -08:00
Leonardo de Moura
c065faaf1f feat(frontends/lean/elaborator): improve ^. notation 2017-02-18 16:20:21 -08:00
Leonardo de Moura
74f7bc0473 feat(frontends/lean): improve notation for converting infix notation into functions 2017-02-17 23:11:22 -08:00
Leonardo de Moura
077176b82f feat(frontends/lean): add Haskell-like for converting infix notation into functions 
Examples:

 qsort (<) [20, 5, 10, 3, 2, 14, 1]

 foldl (+) 0 [1, 2, 3]
 2017-02-17 22:51:50 -08:00
Leonardo de Moura
10c881266b refactor(frontends/lean): add parse_lparen 2017-02-17 21:46:39 -08:00
Sebastian Ullrich
b9424975b3 refactor(init/meta): replace dynamically-checked quotes where possible 2017-02-17 19:59:57 -08:00
Gabriel Ebner
0c2878e509 fix(frontends/lean/definition_cmds): copy position for equation in meta definitions 
Fixes #1377.
 2017-02-17 19:57:49 -08:00
Sebastian Ullrich
d402b2a467 feat(frontends/lean/print_cmd): add to info_manager when not overloaded 2017-02-17 15:41:58 +01:00
Sebastian Ullrich
4d41b03168 chore(frontends/lean,library/tactic): remove old tactic_state functions 2017-02-17 15:41:58 +01:00
Sebastian Ullrich
9d8c84713c refactor(*): reduce exception context info from expr to pos_info 2017-02-17 13:45:57 +01:00
Sebastian Ullrich
d15591a2d8 feat(library,frontends/lean): expose parser to Lean and use for parsing tactic parameters 2017-02-17 13:45:56 +01:00
Sebastian Ullrich
5ed1ac924c feat(frontends/lean/elaborator): support partially applied eval_expr 2017-02-17 13:03:47 +01:00
Sebastian Ullrich
339713091f refactor(frontends/lean): simpler field notation info that also works with implicit parameters 2017-02-17 13:03:47 +01:00
Leonardo de Moura
71950bdf01 fix(frontends/lean/elaborator): expression may not be an application due to error recovery 
Issue described at https://groups.google.com/forum/#!topic/lean-user/uSSYhgVKKH0
 2017-02-16 21:13:21 -08:00
Leonardo de Moura
c1c1cd417a fix(frontends/lean/builtin_exprs): make sure we use internal names (i.e., names starting with _) when compiling do-blocks 
@johoelzl This commit fixes the problem you reported at slack.
 2017-02-15 22:45:59 -08:00
Leonardo de Moura
edd5e97045 feat(frontends/lean/elaborator): coercion from (decidable) Prop to bool 
This is a hard coded extra case. It is not an instance of has_coe.
Even if we change has_coe to accomodate this case, it will not be a
satisfactory solution because this coercion depends on the element and
not the type, and the element usually contains metavariables.

We should eventually write a tactic for synthesizing coercions.
 2017-02-14 18:41:32 -08:00
Leonardo de Moura
1ab2bb7714 feat(frontends/lean/elaborator): eta-expand function applications until we consume all optional and auto parameters 2017-02-14 17:38:08 -08:00
Leonardo de Moura
f650a1b873 refactor(library/init/meta): avoid '_core' idiom using default parameters 
I kept a few core methods (e.g., exact_core and apply_core). Reason:
if we use default parameters

    meta constant exact (e : expr) (md := semireducible) : tactic unit

then, we will not be able to write

    to_expr p >>= exact

The workaround is

    do t <- to_expr p, exact t

or
    to_expr p >>= (fun x, exact x)

One alternative is to change how we handle default parameters, and
eta-expand applications that involve default parameters.
We may also have an attribute [eta_expand]. Then

    attribute [eta_expand] foo

instructs the elaborator to automatically eta-expand foo-applications.
The attribute would give users more control, and avoid potential
performance problems. Without the attribute, then for every function
application the elaborator has to check the type and decide whether it
must be eta-expanded or not.

@gebner @kha What do you think?
 2017-02-14 09:46:55 -08:00
Leonardo de Moura
8a34680916 fix(frontends/lean/elaborator): name resolution at tactic execution times with overloaded notation and aliased symbols 
See https://groups.google.com/forum/#!topic/lean-user/Jja_lh28v3g
 2017-02-13 21:06:49 -08:00
Leonardo de Moura
9210e45da0 feat(frontends/lean): add notation for ';' and '<|>' in the tactic interactive mode 2017-02-10 22:53:30 -08:00
Leonardo de Moura
6334ff24eb fix(frontends/lean/tactic_notation): erase position information quoted terms occurring inside `[...] 
See new test for understanding the problem.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2017-02-09 19:06:56 -08:00
Leonardo de Moura
add5266df7 fix(frontends/lean, library/tactic): error position in auto quoted terms 
This commit also gets rid of the redundant "elaborator failed" error
message.
 2017-02-09 18:03:04 -08:00
Leonardo de Moura
898894ffaa feat(frontends/lean/parser): syntax sugar for auto_param gadget 2017-02-09 16:06:55 -08:00
Leonardo de Moura
c8bbb34e2a feat(frontends/lean): add auto_param gadget 2017-02-09 15:49:10 -08:00
Leonardo de Moura
f5e0fc4876 fix(frontends/lean/elaborator): '{}' inside quotations 2017-02-08 17:50:17 -08:00