Leonardo de Moura
ada4932507
feat(library/compiler): add new cache support to compiler
2018-02-21 15:04:20 -08:00
Leonardo de Moura
30cfcc0fa6
fix(library/compiler/inliner): missing reduction
2018-02-11 09:28:42 -08:00
Gabriel Ebner
e2717ec2c5
fix(library/compiler/inliner): inline auxiliary declarations
...
Fixes #1763 .
2017-08-06 10:24:26 +02:00
Leonardo de Moura
cabb4350d9
feat(library): instances are not reducible by default anymore
...
Motivation: see "Other goodies" section at
https://github.com/leanprover/lean/wiki/Refactoring-structures
We had to add a new transparency mode: Instances at type_context.
In this mode, instances and reducible definitions are considered
transparent.
The new mode is used in the defeq_canonizer, code generator,
and sizeof lemma generation at inductive_compiler.
We also use the new mode in the unfold tactics.
2017-04-26 14:10:11 -07:00
Leonardo de Moura
6916a8ceca
fix(library/compiler/inliner): inliner was unfolding constants aggressively when trying to reduce projections
...
@digama0 After this commit, your example will also produce a
non-destructive update.
```lean
structure test :=
(data1 : array nat 3)
(data2 : array nat 3)
(sz: nat)
def test.write (s : test) (i : fin 3) (v : nat) :=
{s with data1 := s^.data1^.write i v, data2 := s^.data2^.write i v}
set_option trace.array.update true
(fin.of_nat 1) 10 in
(a^.data1^.read (fin.of_nat 1), a^.data2^.read (fin.of_nat 2)) -- destructive write
```
2017-03-09 18:52:27 -08:00
Leonardo de Moura
22988bb95d
feat(library/compiler): avoid pack/unpack overhead produced by the inductive_compiler in the code generator
...
TODO: make sure the user is not manually using cases_on for the
auxiliary datatype generated by the inductive_compiler to
destruct nested inductives.
2017-03-04 13:54:44 -08:00
Leonardo de Moura
3178f41cce
fix(library/compiler/inliner): applications of definitions marked as [inline] are inlined even if they are not fully applied
...
see #1316
2017-01-17 16:33:19 -08:00
Leonardo de Moura
d6000416f8
feat(library/compiler,frontends/lean/elaborator): (try to) preserve position information
...
We will use this information in the debugger.
2016-11-09 16:51:48 -08:00
Leonardo de Moura
6ce00a9b45
fix(library/compiler): move inliner to the beginning
...
Reason: the inliner may introduce recursors, non eta-expanded terms,
etc. Before this commit, it was "undoing" previous compilation steps.
2016-11-08 16:14:01 -08:00
Sebastian Ullrich
441a219a66
feat(library/attribute_manager): make attributes with side-effect free callbacks removable
2016-08-23 21:52:52 -07:00
Sebastian Ullrich
ca8be3857c
feat(library/user_attribute): add user-defined attributes and make attribute_manager environment-aware
2016-08-18 12:56:44 -07:00
Sebastian Ullrich
34e00cd5a2
refactor(library/attribute_manger): simplify: make every attribute prioritizable
2016-08-16 13:49:02 -07:00
Leonardo de Moura
2736ac48f4
fix(library/compiler/inliner): disable problematic optimization
2016-08-08 13:59:12 -07:00
Sebastian Ullrich
82657b3b64
refactor(library/compiler/inliner, library): replace inline command with attribute
...
sed -Ei 's/inline (protected )?(meta_)?definition (\S+)/\1\2definition \3 [inline]/' library/**/*.lean
2016-08-08 12:45:22 -07:00
Leonardo de Moura
e89082a97e
feat(library/vm,library/init): add builtin timeit primitive for profiling
2016-05-26 12:44:49 -07:00
Leonardo de Moura
53811822d4
chore(*): style
2016-05-25 18:10:15 -07:00
Leonardo de Moura
de9df69ef6
refactor(src): move compiler folder to library
2016-05-09 13:28:00 -07:00
