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

9482 commits

Author SHA1 Message Date
Leonardo de Moura
11e87545be chore(frontends/lean): remove dead variables 2018-02-21 15:04:19 -08:00
Leonardo de Moura
f8e0916c64 feat(library/tactic, frontends/lean): replace a few mk_tagged_fresh_name with mk_unused_name 2018-02-21 15:04:19 -08:00
Leonardo de Moura
73eda00ba3 refactor(library/compiler): mk_unused_name ==> mk_compiler_unused_name 2018-02-21 15:04:19 -08:00
Leonardo de Moura
058520d6e4 feat(frontends/lean/pp,library/local_context): use sanitize_name_generator_name 
Remark: we should remove `sanitize_if_fresh` as soon as we delete `::lean::mk_fresh_name`
 2018-02-21 15:04:19 -08:00
Leonardo de Moura
49e8867d29 feat(util/name_generator): mk_tagged_child ==> mk_child_with 
This commit also adds assertions to make sure only registered prefixes
are used to create name generators.
 2018-02-21 15:04:19 -08:00
Leonardo de Moura
b16f641179 feat(util/name_generator): name generator prefix bookkeeping 2018-02-21 15:04:19 -08:00
Leonardo de Moura
ce028d651d refactor(kernel): abstract_type_context::mk_fresh_name ==> abstract_type_context::next_name 2018-02-21 15:04:19 -08:00
Leonardo de Moura
28d6326228 refactor(frontends/lean/parser): add name_generator 2018-02-21 15:04:19 -08:00
Leonardo de Moura
fa2e67e8f3 refactor(library/compiler/vm_compiler): do not use mk_fresh_name 2018-02-21 15:04:19 -08:00
Leonardo de Moura
6ba4607c28 refactor(library/compiler): rename compiler mk_fresh_name to mk_unused_name 2018-02-21 15:04:19 -08:00
Leonardo de Moura
c0ded37f24 refactor(library/inductive_compiler): do not use fresh names in the inductive compiler 2018-02-21 15:04:19 -08:00
Leonardo de Moura
e06c3cbd8f chore(library/type_context): fix compilation warning 2018-02-21 15:04:19 -08:00
Leonardo de Moura
21e52408b2 refactor(library/constructions): make sure constructions do not use ::lean::mk_fresh_name 2018-02-21 15:04:19 -08:00
Leonardo de Moura
c176faed32 feat(kernel/inductive): make sure constructor types do not contain local constants nor metavariables 2018-02-21 15:04:19 -08:00
Leonardo de Moura
cc8eb83507 refactor(library/util,util): move is_internal_name to util/ 2018-02-21 15:04:19 -08:00
Leonardo de Moura
2e5b66a5f1 refactor(kernel): make sure kernel does not use global ::lean::mk_fresh_name 2018-02-21 15:04:19 -08:00
Leonardo de Moura
60d04987c8 chore(kernel/inductive/inductive): remove dead global variable 2018-02-21 15:04:19 -08:00
Leonardo de Moura
1547d47387 feat(util/fresh_name): add fresh_name_scope 2018-02-21 15:04:19 -08:00
Leonardo de Moura
8eb34a39cb feat(frontends/lean): save/restore fresh name_generator state in parser snapshots 2018-02-21 15:04:19 -08:00
Leonardo de Moura
799cc9b03d feat(util/fresh_name): implement mk_fresh_name using name_generator 2018-02-21 15:04:19 -08:00
Leonardo de Moura
05fc306550 feat(util): add name_generator back 2018-02-21 15:04:19 -08:00
Leonardo de Moura
78d8ff8031 feat(*): add reset_thread_local 2018-02-21 15:04:19 -08:00
Leonardo de Moura
505042b8c0 chore(library/tactic/smt/congruence_closure): simplify cache management 2018-02-21 15:04:18 -08:00
Leonardo de Moura
40a0465cca chore(library/tactic/simp_lemmas): fix typo 2018-02-21 15:04:18 -08:00
Leonardo de Moura
02231477f9 chore(library/tactic/ac_tactics): simplify cache management 2018-02-21 15:04:18 -08:00
Leonardo de Moura
bf4d47b560 chore(library/cache_helper): remove dead code 2018-02-21 15:04:18 -08:00
Leonardo de Moura
9e08cab381 chore(library/type_context): simplify cache management 2018-02-21 15:04:18 -08:00
Leonardo de Moura
3f04d041f6 chore(library/time_task): style 2018-02-19 10:30:49 -08:00
Sebastian Ullrich
f247363305 feat(library/time_task): print cumulative times on --profile 2018-02-19 09:13:24 -08:00
Sebastian Ullrich
b206b3bedf chore(util/timeit): make xtimeit non-copyable 2018-02-19 09:13:24 -08:00
Sebastian Ullrich
782af7e5d6 chore(library/vm/interaction_state): do not profile calls into Lean other than tactic execution 
Otherwise, we produce a message for e.g. every single interactive tactic parameter
 2018-02-19 09:13:24 -08:00
Sebastian Ullrich
9c5df7875a perf(frontends/lean/elaborator): visit_structure_instance_fn: delay building error message 2018-02-19 09:13:24 -08:00
Leonardo de Moura
56dba5b98a fix(frontends/lean/elaborator): fixes #1930 
@kha the following idiom is not safe
```
   while (is_pi(t)) {
      t = whnf(binding_body(t));
   }
```
`whnf(e)` assumes that `e` does not have dangling deBruijn variables.
We should use (the more expensive):
```
   while (is_pi(t)) {
      t = whnf(instantiate(binding_body(t), locals.push_local_from_binding(t)));
   }
```
BTW, this problem is not related to the assertion violation at #1930
I just stumbled on it when fixing the violation.
 2018-02-19 08:51:26 -08:00
Leonardo de Moura
dbfcc65c60 fix(library/compiler/erase_irrelevant): erase_type 2018-02-19 07:55:43 -08:00
Leonardo de Moura
aa24c15e61 feat(library/vm): basic performance counters 
@kha I have added a few performance counters.
I collect their values at each snapshot.
Right now, I am printing only the values in the last snapshot, but if we want
we can even display their progress over time.

Right now, I track the following information
- number of allocated closures
- number of allocated constructors/objects
- number of allocated big numbers
 2018-02-16 14:37:11 -08:00
Nuno Lopes
3bb1366b39 chore(api): remove unneeded #include 2018-02-16 12:19:20 -08:00
Leonardo de Moura
3666fac95a chore(util/parser_exception): avoid thread local storage 2018-02-16 12:12:56 -08:00
Leonardo de Moura
c35f2a2098 chore(library/io_state): avoid thread local storage 2018-02-16 12:12:50 -08:00
Leonardo de Moura
a076f0003d chore(util/exception): avoid thread local storage 
The overhead of creating the message eagerly should be really small.
These exceptions are seldom thrown.
 2018-02-16 12:12:44 -08:00
Leonardo de Moura
96fab5172f perf(library/compiler): apply lambda lifting after erase trivial structures 
cc @kha
 2018-02-15 16:55:27 -08:00
Leonardo de Moura
a115a1538b chore(library/vm/vm_io): style 2018-02-15 16:25:17 -08:00
Leonardo de Moura
1c9648a12d chore(library): remove dead constants 2018-02-15 16:17:43 -08:00
Leonardo de Moura
ac13f8b0f9 feat(library/system/io): add random number generator support in the io monad 
@aqjune @nunoplopes: See new tests at tests/lean/run/random.lean

We have two actions in `io`. By default, `io` uses the C++
random number generator, but we can force it to use a `std_gen` with
the action `set_rand_gen`.

def rand (lo : nat := std_range.1) (hi : nat := std_range.2) : io nat
def set_rand_gen : std_gen → io unit
 2018-02-15 16:12:08 -08:00
Nuno Lopes
1a9962011d chore(style): fix cast style 2018-02-13 10:42:08 -08:00
Nuno Lopes
7b45d28e77 chore(unicode): use utf8 chars directly in strings 2018-02-13 10:42:08 -08:00
Nuno Lopes
c43ebd8bf7 fix(msvc): remove another \uXX char that was causing an infinite loop 2018-02-13 10:42:08 -08:00
Nuno Lopes
977e11f9be fix(warnings): fix warnings on VS. its now /W2 clean 2018-02-13 10:42:08 -08:00
Leonardo de Moura
96e02613fc fix(library/compiler/simp_inductive): erase trivial structure bug 2018-02-11 11:43:05 -08:00
Leonardo de Moura
30cfcc0fa6 fix(library/compiler/inliner): missing reduction 2018-02-11 09:28:42 -08:00
Sebastian Ullrich
affe3463ab fix(frontends/lean/elaborator): fix assertion error: accidental mutation of a variable 2018-02-08 14:07:08 +01:00