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

2550 commits

Author SHA1 Message Date
Gabriel Ebner
d4541ce2cc chore(frontends/lean/elaborator): fix clang-3.4 build error 2017-02-06 20:44:28 +01:00
Gabriel Ebner
7946b15511 feat(frontends/lean/elaborator): recover from most errors using sorry 2017-02-06 15:15:44 +01:00
Leonardo de Moura
55aa2023f4 feat(frontends/lean): add support for monad_fail type class in 'do' blocks 2017-02-05 20:09:08 -08:00
Leonardo de Moura
3ef463ccc9 chore(frontends/lean/builtin_exprs): update error messages for do-blocks 2017-02-05 19:07:23 -08:00
Leonardo de Moura
4283fe9bb7 fix(frontends/lean/builtin_exprs): missing pattern when lhs is a constant constructor 2017-02-05 19:03:00 -08:00
Leonardo de Moura
797b26f402 fix(frontends/lean/tactic_notation): trace messages in nested blocks were not being displayed in the correct place 2017-02-05 18:20:10 -08:00
Leonardo de Moura
1fc9cc37f7 chore(frontends/lean): remove dead field 2017-02-05 14:25:49 -08:00
diakopter
91b526fdd1 chore(frontends/lean): clang warnings 2017-02-05 14:03:15 -08:00
Leonardo de Moura
323db5a530 feat(frontends/lean/pp): pretty print structure instances and field projections 2017-02-05 14:01:53 -08:00
Gabriel Ebner
cbc0bb1f7c feat(library/module): store whether we used sorry in olean 2017-02-05 16:35:32 +01:00
Gabriel Ebner
6910f3f2b9 feat(frontends/lean/print_cmd): show sorry macro as axiom 2017-02-05 14:01:08 +01:00
Gabriel Ebner
95068e4e79 feat(library/sorry): make sorry a macro 2017-02-05 14:01:03 +01:00
Gabriel Ebner
98c2998a7b feat(frontends/lean/definition_cmds): make noncomputability check non-fatal 2017-02-05 13:42:52 +01:00
Leonardo de Moura
84188c5aa1 feat(frontends/lean/elaborator): add pattern validator in the elaborator 
@johoelzl We now produce a better message for your example:

   inductive R : ℕ → Prop
   | pos : ∀p n, R (p + n)

   lemma R_id : ∀n, R n → R n
   | (.p + .n) (R.pos p n) := R.pos p n

The new error is:

file.lean:5:2: error: invalid function application in pattern, it cannot be reduced to a constructor (possible solution, mark term as inaccessible using '.( )')
  .p + .n
 2017-02-04 19:00:20 -08:00
Leonardo de Moura
dbf65e4c6b chore(frontends/lean/parser_state): style 2017-02-04 13:48:24 -08:00
Leonardo de Moura
b28ed2453e feat(frontends/lean/definition_cmds): allow meta recursive definitions without recursive equations 2017-02-04 13:44:05 -08:00
Leonardo de Moura
160011b80e feat(frontends/lean/parser_state): parser_state API 2017-02-04 13:38:53 -08:00
Leonardo de Moura
36dc796f6c refactor(frontends/lean): add more parser_state methods 2017-02-04 11:37:26 -08:00
Leonardo de Moura
d7ab2bb196 feat(frontends/lean): add basic parser_state methods 2017-02-04 10:57:51 -08:00
Leonardo de Moura
abe0f1f386 feat(frontends/lean): new parser_state skeleton 2017-02-03 21:01:49 -08:00
Leonardo de Moura
91b68b6b90 chore(frontends/lean/parser): remove dead variable 2017-02-03 19:55:19 -08:00
Leonardo de Moura
01414cf21c feat(frontends/lean): add token class, and procedure for consuming the tokens 2017-02-03 18:11:06 -08:00
Leonardo de Moura
b2968f450c fix(frontends/lean/elaborator): use expected type when elaborating application for the form (c^.fn a) 
For example, the following definition did not work before this commit:

  protected meta def map {α β} (f : α → β) : lazy_tactic α → lazy_tactic β
  | t s := (t s)^.for (λ ⟨a, new_s⟩, (f a, new_s))
 2017-02-02 19:56:50 -08:00
Leonardo de Moura
9bee8ce36d fix(frontends/lean/elaborator): thunk gadget should not be considered in patterns 
The new test demonstrates the problem.
 2017-02-02 17:28:03 -08:00
Leonardo de Moura
bb9a0c79f4 feat(frontends/lean/builtin_exprs): better syntax for quoted terms with type ascription 2017-02-01 12:49:38 -08:00
Leonardo de Moura
6e7929252f feat(frontends/lean, library/init): add 'thunk' gadget 
We can now write
   trace "hello" t
instead of
   trace "hello" (fun _, t)
 2017-01-31 18:41:59 -08:00
Leonardo de Moura
be6ca7c244 feat(frontends/lean): allow default parameter values in constant decls 2017-01-31 15:19:47 -08:00
Leonardo de Moura
3a4ef00f66 feat(frontends/lean): allow constructor parameters to be declared before ':' 2017-01-31 15:11:39 -08:00
Gabriel Ebner
0f96809f7a fix(frontends/lean/parser): save noncomputable theory flag in snapshots 2017-01-31 11:05:11 -08:00
Leonardo de Moura
941ba6d96c chore(*): style 2017-01-31 11:04:21 -08:00
Gabriel Ebner
f404e8a2be feat(library/export,checker): add basic support for mixfix notation 2017-01-31 10:20:56 +01:00
Gabriel Ebner
61804eb8e9 chore(util/sexpr): remove mpz and mpq cases 2017-01-31 09:39:31 +01:00
Leonardo de Moura
5da8b205b9 feat(library/type_context, frontends/lean/elaborator): type classes with output parameters 2017-01-30 18:32:54 -08:00
Leonardo de Moura
4d3ff955d3 feat(frontends/lean): nicer syntax for default parameter values 
See #1340
 2017-01-30 15:54:26 -08:00
Leonardo de Moura
c09f60de6e fix(frontends/lean/structure_cmd): fixes #1347 2017-01-30 14:49:14 -08:00
Leonardo de Moura
d34386fef7 perf(frontends/lean/tactic_notation): closes #1345 
We can now elaborate
https://gist.github.com/gebner/439273deee592603190d4f8b4447295b
in 1.6 secs and using less than 500Kb of stack space.
It was takins 44 secs and 5Mb before this commit.

Two modifications:
1) Use pre_monad.seq instead of pre_monad.and_then.
They have the same implementation, but seq is not marked as [inline].

2) Modify how we concatenate the tactics in a begin...end block.
Before: (((a_1 ++ a_2) ++ a_3) ++ a_4)
After:  ((a_1 ++ a_2) ++ (a_3 ++ a_4))
 2017-01-30 14:13:53 -08:00
Leonardo de Moura
4fe73d3f87 fix(frontends/lean/elaborator, kernel/error_msgs): (re-)activate distinguishing_pp_options 2017-01-30 11:54:00 -08:00
Leonardo de Moura
36f37a3472 fix(frontends/lean/builtin_cmds): make vm_eval_cmd robust with respect to changes universe level changes at has_to_string 
see #1341
 2017-01-30 11:54:00 -08:00
Leonardo de Moura
3b38f71f11 fix(library,tests/lean): fix run/interactive tests, and problems in the standard library due to the new interpretation for Type 
We had to change subtype to use Sort since the axiom
strong_indefinite_description uses it.

see #1341
 2017-01-30 11:54:00 -08:00
Leonardo de Moura
77a9feaf70 refactor(frontends/lean): PType ==> Sort 
see #1341
 2017-01-30 11:54:00 -08:00
Leonardo de Moura
bf9f7560f7 feat(frontends/lean): (Type u) can't be a proposition 
(Type u)  is the old (Type (u+1))
(PType u) is the old (Type u)
Type*     is the old (Type (_+1))
PType*    is the old Type*

The stdlib can be compiled, but we still have > 70 broken tests

See discussion at #1341
 2017-01-30 11:54:00 -08:00
Gabriel Ebner
5fdc737dfc feat(library/tactic): store name of current declaration in tactic_state 2017-01-28 08:27:19 +01:00
Leonardo de Moura
9107439bce feat(frontends/lean/elaborator): default parameter prototype 
See #1340
 2017-01-27 16:32:22 -08:00
Leonardo de Moura
6f502b9afd fix(library/vm): make sure vm_rb_map objects can be stored in ts_vm_obj 
See discussion at #1337
 2017-01-26 15:58:11 -08:00
Sebastian Ullrich
2c3f6d0e1c fix(frontends/lean/structure_cmd): default field values of Pi type 
There were two separate issues:
* An explicit Pi as the type of a field with a default value would be considered a field reference
* An implicit Pi would be instantiated by the elaborator during `visit_structure_instance`
 2017-01-26 18:53:55 +01:00
Sebastian Ullrich
5c5c998813 fix(frontends/lean/structure_cmd): fix default field values referencing universe variables 2017-01-26 18:52:20 +01:00
Sebastian Ullrich
92ebaaa0f8 fix(frontends/lean/builtin_exprs): ite/dite prec should be lowest 2017-01-26 18:52:20 +01:00
Leonardo de Moura
750d02c3ac feat(frontends/lean/definition_cmds): remove equations_result macro from elaborated theorems 2017-01-24 16:51:33 -08:00
Leonardo de Moura
0048d0490b fix(frontends/lean/parser): structure followed by doc string 2017-01-23 10:35:07 -08:00
Leonardo de Moura
71a7a7f466 feat(frontends/lean): add default field values 2017-01-22 21:25:49 -08:00