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

49 commits

Author SHA1 Message Date
Leonardo de Moura
3dad81daee feat(library/init/lean/elaborator): add resolvename.lean 2019-08-11 15:37:37 -07:00
Leonardo de Moura
d00019f57e chore(library/init): fix whitspaces before => 2019-08-09 09:13:49 -07:00
Leonardo de Moura
4d913370a7 chore(library/init): eliminate whitespaces using another patch script 2019-08-09 09:01:39 -07:00
Sebastian Ullrich
3ed67138d5 chore(*): update equation syntax in files and old parser 
for f in ../../**/*.lean; do echo $f; ./patch.lean.out $f > tmp && cat tmp > $f; done
 2019-08-09 11:11:34 +02:00
Leonardo de Moura
2387f3c2a2 feat(library/init/lean/elaborator): improve namespace, scope, and end commands 2019-07-22 08:14:35 -07:00
Leonardo de Moura
ea6eee516b chore(frontends/lean): use => instead of := in match-expressions 
Motivation: use same separator used in lambda expressions as in
other programming languages.
 2019-07-04 11:38:38 -07:00
Leonardo de Moura
07cff06b6e chore(library): Π ==> ∀ 2019-07-02 17:35:15 -07:00
Leonardo de Moura
a02443d23d chore(frontends/lean): fun x, e ==> fun x => e 2019-07-02 13:22:11 -07:00
Leonardo de Moura
ab487ea4ac feat(frontends/lean): allow ; instead of in in let-decls 2019-06-27 17:12:03 -07:00
Leonardo de Moura
3651dc7618 feat(library/init/lean): add evalConst 
The implementation is good enough for implementing extensible parsers,
elaborators and tactics, but there are a few TODOs

1- We should have a better story for standalone applications.
   Most of them don't need `evalConst`, and the global table is
   just initialization overhead.

2- The global table introduces a dependency on the `Lean.Name`
   implementation. So, all standalone applications will depend on it.

3- We are not storing arity 0 constants in the table.
   This one should be easy to fix in the future.
 2019-06-07 16:31:28 -07:00
Leonardo de Moura
9b457cc77c feat(library/init/lean/compiler/inline): implement tester functions and export them 2019-06-06 15:07:08 -07:00
Leonardo de Moura
dbe38b054d feat(library/init/lean/name): add Lean version of name::append_after 2019-06-06 14:28:59 -07:00
Leonardo de Moura
ff74b9f44a feat(library/init/lean/compiler/ir): add emitutil.lean and emitcpp.lean files 2019-05-20 09:25:16 -07:00
Leonardo de Moura
dc6c1e329f refactor(library/init/data/rbmap): use Bool instead of Prop 2019-04-03 02:54:34 -07:00
Leonardo de Moura
b66f5dcf5c chore(library/init): avoid wf_term_hack 2019-03-27 12:12:21 -07:00
Leonardo de Moura
5b08bf18c5 feat(library/init/lean): improving options 
@kha It will be awesome to automate the following idiom with a macro :)
```
def defIndent  := 4
def getIndent (o : Options) : Nat   := o.get `format.indent defIndent
@[init] def indentOption : IO Unit :=
registerOption `format.indent { defValue := defIndent, group := "format", descr := "indentation" }
```
 2019-03-24 09:30:20 -07:00
Leonardo de Moura
8225146aa2 chore(library/init/core): HasLt => HasLess, HasLe => HasLessEq, ... 2019-03-23 10:07:46 -07:00
Leonardo de Moura
c10a99e96f feat(library/init/lean/name): add String.toName 2019-03-22 17:26:43 -07:00
Leonardo de Moura
e1ea2b3948 chore(library/init): fix names and add HasEmptyc instances 2019-03-22 12:38:22 -07:00
Sebastian Ullrich
97e5aa2411 chore(library): s/Punit/PUnit/g etc 2019-03-21 15:06:45 -07:00
Leonardo de Moura
1fe3f14ad0 chore(*): Uint => UInt, Usize => USize 2019-03-21 15:06:44 -07:00
Leonardo de Moura
79a8d9aa65 chore(*): decidablePred/decidableRel => DecidablePred/DecidableRel 2019-03-21 15:06:44 -07:00
Leonardo de Moura
2be87ecd92 chore(library/init): Bool.tt => Bool.true and Bool.ff => Bool.false 2019-03-21 15:06:44 -07:00
Leonardo de Moura
04e20623e6 chore(*): use lowercase dir names 2019-03-21 15:06:44 -07:00
Leonardo de Moura
67fb78bb47 chore(*): renaming files 2019-03-21 15:06:44 -07:00
Sebastian Ullrich
beda5f5f43 chore(library): capitalize types and namespaces 2019-03-21 15:06:43 -07:00
Sebastian Ullrich
f7aeeaf237 exclude export/extern, translate constants.txt 2019-03-21 15:06:43 -07:00
Sebastian Ullrich
b939162168 chore(library): switch from snake_case to camelCase 2019-03-21 15:06:43 -07:00
Leonardo de Moura
ffc3436dd6 feat(library/init/lean): remove some TODOs using the new opaque constants 2019-03-15 17:49:10 -07:00
Leonardo de Moura
db6f08e66d feat(library/init/lean/compiler/ir): collect fnbody free variables 2019-03-07 15:37:45 -08:00
Leonardo de Moura
50476328ff feat(library/init/lean/name): add name_map 2019-03-06 12:32:08 -08:00
Leonardo de Moura
3f50df70bc perf(library/init/lean/name): use hash code to speedup name.quick_lt 
We use the same trick in the C++ version of this function.

I measured the impact using `lean --new-frontend core.lean` and checking
the number of instructions executed reported by Valgrind.
Before:  4,891,642,264
After:   4,847,313,330
 2019-03-04 12:48:06 -08:00
Leonardo de Moura
4627929a83 refactor(boot,runtime,util): move name runtime implementation to util/name, and use "extern C" ABI 2019-02-13 08:27:23 -08:00
Leonardo de Moura
5a5e949578 feat(library/init/lean/name): use extern attribute 2019-02-11 16:12:25 -08:00
Leonardo de Moura
2058d33d07 feat(runtime,library/compiler): add name.dec_eq builtin 2019-02-05 14:36:02 -08:00
Sebastian Ullrich
595590e7f5 feat(library/init/lean/elaborator): elaborate open and export 2019-01-01 13:50:21 +01:00
Leonardo de Moura
12d8b0e7ef feat(library/init/data): annotate rbtree and rbmap functions 2018-10-19 14:57:31 -07:00
Sebastian Ullrich
5a21d45836 refactor(library/init/lean/expander): introduce some coercions 2018-09-25 09:16:02 -07:00
Leonardo de Moura
71dd8653bc feat(library/init/core): decidable_eq is a proper class 
We need this to take advantage of the new indexing structure we are
going to add to improve performance.
 2018-09-07 16:38:11 -07:00
Leonardo de Moura
e9b4b811de chore(library/equations_compiler/util): disable generation of equational lemmas 
@kha, `eqn_compiler.lemmas` is false by default.
I will keep them disabled until I remove the inductive compiler.
I'm building the new inductive datatype module (to replace the inductive
compiler), and the lemmas will fail to be proved in the next commits
until the transition is complete.
 2018-06-12 13:03:25 -07:00
Leonardo de Moura
441b9077b2 feat(library/comp_val): add mk_name_val_ne_proof 
We need this procedure otherwise it takes forever to prove equation lemmas
for definitions such as:

```
def macros : name → option macro
| `lambda := some lambda_macro
| `intro_x := some intro_x_macro
| _ := none
```

We never experienced this problem in Lean3 because we used `name`
literals only occurred in patterns of *meta* definitions. So, no
equation lemma was generated.

@kha `def macros` was taking more than 1 second to elaborate on my
machine. It is now instantaneous.
 2018-06-06 09:18:59 -07:00
Sebastian Ullrich
732c823646 feat(library/init/lean/parser): remove syntax_id, use De Bruijn indices instead 2018-06-06 15:36:28 +02:00
Leonardo de Moura
89b4bb7210 feat(library/init/data/hashable): add hashable nat instance 2018-05-06 07:53:29 -07:00
Leonardo de Moura
3079d2d007 feat(library/init/lean/name): add hashable instance 2018-05-06 07:49:17 -07:00
Leonardo de Moura
d5fe509c36 chore(*): remove end after each match-expression 
`end` is not optional anymore
 2018-05-04 11:30:06 -07:00
Leonardo de Moura
92fa43e7d8 feat(library/init/lean/ir/ir): use name 2018-05-01 12:40:49 -07:00
Leonardo de Moura
09d3809a42 feat(library/init/lean/name): add has_to_string and has_to_format instances 2018-04-30 12:01:56 -07:00
Leonardo de Moura
c5abd6868d feat(library/init/lean/name): add quick_lt 2018-04-30 11:29:26 -07:00
Leonardo de Moura
b39daa40ef feat(library/init/lean/name): add lean.name 2018-04-29 08:44:58 -07:00