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

2644 commits

Author SHA1 Message Date
Sebastian Ullrich
16558bf082 refactor(library,library): rename pre_monad to has_bind 2017-03-09 20:32:25 -08:00
Leonardo de Moura
9d3c0497cb chore(frontends/lean): rename transient commands 
See issue #1432
 2017-03-09 18:41:19 -08:00
Leonardo de Moura
a00f2e49a7 chore(frontends/lean): remove several command aliases 
We still have many more to remove and rename.
See issue #1432
 2017-03-09 16:49:03 -08:00
Leonardo de Moura
b6f6126075 feat(frontends/lean/pp): add attribute [pp_using_anonymous_constructor] for marking structures we should use the anonymous constructor notation when pretty printing instances 2017-03-09 15:17:18 -08:00
Leonardo de Moura
c58f61e925 feat(frontends/lean/elaborator): new encoding for structure updates {s with ...} 
See discussion at #1438
https://github.com/leanprover/lean/pull/1438#discussion_r105007325

@digama0 With this commit, the original `array_list.write` will also
perform a destructive update when the reference counter for `l` is 1.

```lean def write {α} (l : array_list α) : fin l^.length → α → array_list α :=
λ ⟨n, h⟩ v, { l with data := l^.data^.write ⟨n, l^.lt_capacity h⟩ h v }
```
 2017-03-09 00:11:51 -08:00
Leonardo de Moura
d775ee98b4 feat(frontends/lean): auto_param support at structure_instance, and better error messages 
Summary:

- A field value was being elaborated more than once when there is
  another field whose default value depends on it.
  The new test `structure_default_value_issue.lean` exposes the problem.

- Better error message and localization at field type mismatches.
  When there is field type mismatch, the error message contains the
  field name, and the error is reported at the field position instead of
  `{`.

- We add support for auto_param at structure instances `{...}`
  See #1422
 2017-03-08 18:04:36 -08:00
Leonardo de Moura
23935ee390 feat(frontends/lean): allow auto_param notation in structure declarations 
See #1422

TODO: take the auto_param into account in the `{ ... }` notation.
 2017-03-08 15:41:30 -08:00
Sebastian Ullrich
970e11bf5e feat(frontends/lean/{elaborator,structure_cmd}): allow overriding field defaults 2017-03-08 10:41:20 -08:00
Leonardo de Moura
8d3c7e7180 fix(frontends/lean/builtin_exprs): fixes #1433 2017-03-07 16:21:12 -08:00
Leonardo de Moura
51958df84b chore(frontends/lean/token_table): remove dead keywords 2017-03-07 14:00:49 -08:00
Leonardo de Moura
c427350dc0 chore(frontends/lean/token_table): remove dead commands 2017-03-07 13:50:14 -08:00
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
d1d5428808 feat(library): add check_constants.lean validation, cleanup unused names, minor stdlib fixes 2017-02-21 10:45:31 -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