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

5583 commits

Author SHA1 Message Date
Leonardo de Moura
48fbaefa2a chore(library/constants.txt): remove leftover 2019-04-05 14:29:51 -07:00
Leonardo de Moura
994ca779ef feat(library/compiler/csimp): improve try_inline_instance 2019-04-05 14:16:38 -07:00
Leonardo de Moura
3d393d9b1d fix(library/compiler/csimp): bug introduced earlier today 2019-04-02 17:21:25 -07:00
Leonardo de Moura
6ab935ebf6 feat(library/compiler/csimp): merge equal casesOn branches 2019-04-02 11:06:07 -07:00
Leonardo de Moura
95ca283854 chore(library/compiler/csimp): remove m_proj2var, we can use m_var2ctor instead 2019-04-02 10:05:20 -07:00
Leonardo de Moura
005d62185d feat(library/compiler/csimp): add "case merging" optimization 2019-04-02 09:41:53 -07:00
Leonardo de Moura
12595fb501 feat(library/compiler/specialize): cache whenever possible 
There were many opportunities for reusing previously specialized code at
stdlib
 2019-03-29 15:21:17 -07:00
Leonardo de Moura
9d325515d4 chore(library/compiler/util): reduce term size if possible 2019-03-28 17:35:12 -07:00
Leonardo de Moura
8c58314b84 fix(library/compiler/csimp): lc_unreachable simplifications 
The simplifications were introducing dangling free variables.
 2019-03-28 17:32:41 -07:00
Leonardo de Moura
1ebdb9f1b1 fix(library/compiler): do not inline definitions using unsafe inductives 
This commit also makes sure that `has_trivial_structure` returns false
for `unsafe` inductive datatypes.

See new test for further details.
 2019-03-28 16:07:57 -07:00
Leonardo de Moura
427d3b4d40 chore(library/compiler/specialize): reduce stack consumption 2019-03-28 15:05:48 -07:00
Leonardo de Moura
4dbae58646 fix(library/equations_compiler): make sure _unsafe_rec auxiliary definitions contain all local constants used in the safe one 
cc @kha
 2019-03-28 12:57:15 -07:00
Leonardo de Moura
1f197b5293 feat(library/equations_compiler/unbounded_rec): check whether f._unsafe_rec and f have the same type 
`f._unsafe_rec` is the auxiliary definition created by the equation
compiler to help the code generator to produce better code.
 2019-03-28 12:39:44 -07:00
Leonardo de Moura
b74a9b63de feat(library/equations_compiler/partial_rec): improve base case synthesis 2019-03-28 10:19:57 -07:00
Leonardo de Moura
0161ef8487 fix(library/compiler/name_mangling): bug 2019-03-28 08:23:38 -07:00
Leonardo de Moura
42fbe3c18c chore(library/init,runtime,library/compiler): add fix primitive back 
The new `partial def`s allow us to define `fix` in Lean, but the Lean
implementation is not as efficient as the native one. The native one
in C++ use weak pointers to prevent a closure allocation at every
recursive invocation.

This commit also fixes the `fixCore` helper functions that were broken
after we switched to camelCase.

We have updated the test `fix1.lean` to demonstrate the native
implementation is faster. Here are the numbers on my desktop.

```
./run.sh fix1.lean 24
721420279
Time for 'native fix': 816ms
721420279
Time for 'fix in lean': 1.34s
```
 2019-03-27 17:13:53 -07:00
Leonardo de Moura
9b47d134ae feat(library/equations_compiler/partial_rec): consider elements before : when constructing base case 2019-03-27 13:49:23 -07:00
Leonardo de Moura
a43a40b7f5 chore(library/init): remove fix.lean 
`partial def` is much more general
 2019-03-27 13:11:00 -07:00
Leonardo de Moura
62d7cc6b37 feat(library/init/wf): remove wf_term_hack 2019-03-27 12:41:16 -07:00
Leonardo de Moura
895bf2c91d feat(library/equations_compiler/partial_rec): try assumption if inhabitant could not be found 2019-03-27 12:24:24 -07:00
Leonardo de Moura
9a071c18e7 feat(library/equations_compiler): add support for partial definitions 2019-03-27 11:09:32 -07:00
Leonardo de Moura
ef5fac1481 chore(library/equations_compiler): add partial_rec skeleton 2019-03-27 08:37:59 -07:00
Leonardo de Moura
9ddc778ac3 feat(library/equations_compiler/equations): add m_is_partial to equation header 2019-03-26 16:18:43 -07:00
Leonardo de Moura
f1f2994781 chore(library/compiler/emit_cpp): update 2019-03-26 14:51:14 -07:00
Leonardo de Moura
681f3ec81b fix(library/compiler/llnf): constructor reuse 
We were not reusing constructor values for constructors that contained only
scalar values.
 2019-03-26 11:10:51 -07:00
Leonardo de Moura
3ad7d2ba81 fix(library/compiler/lcnf): disable transformation for Bool 
@kha Here is another motivation for re-implementing the equation compiler.
 2019-03-25 16:48:11 -07:00
Leonardo de Moura
7db4f60e50 feat(library/init/core): eagerly expanding Decidable.toBool seems to be a bad idea 
After we erase types and proofs, `Decidable.toBool` can be replaced with
the identity function since `Decidable A` and `Bool` have the same
runtime representation. By eagerly expanding `toBool`, we introduce
unnecessary `cases` expressions.
 2019-03-25 16:48:11 -07:00
Leonardo de Moura
87cab24a1d fix(library/compiler/csimp): at_most_once at elim_jp1_fn 
`elim_jp1_fn` was incorrectly expanding join points that were used more
than once. The issue is that the `foreach` combinator "may" skip nodes
that have already been visited.
 2019-03-25 14:19:11 -07:00
Leonardo de Moura
df9ce10623 feat(library/compiler): special support for initialization functions of the form def initFn : IO Unit 
We can now write
```
@[init] def initFn : IO Unit := ...
```
instead of
```
def initFn : IO Unit := ...
@[init initFn] constant execInitFn : Unit := ()
```
 2019-03-23 08:46:38 -07:00
Leonardo de Moura
3d52298c69 chore(util/sexpr): preparing to port options to Lean 2019-03-22 13:58:16 -07:00
Leonardo de Moura
50207e2c5a chore(library/constants.txt): remove dead variables 2019-03-22 13:26:48 -07:00
Leonardo de Moura
2b76d79791 chore(library/init/core): remove more nonsense 2019-03-22 13:14:20 -07:00
Leonardo de Moura
930653f292 chore(library/init): Unit.star => Unit.unit 
@kha Our stdlib is starting to match the names we used in our paper :)
 2019-03-22 13:06:45 -07:00
Sebastian Ullrich
09c65008f6 fix(library/compiler/emit_cpp): Lean namespace 2019-03-21 15:11:05 -07:00
Sebastian Ullrich
20451918a6 fix(library/constants): more Io -> IO 2019-03-21 15:11:05 -07:00
Leonardo de Moura
bcb78d9454 fix(library/compiler/emit_cpp): another assertion violation 2019-03-21 15:06:46 -07:00
Leonardo de Moura
fd7d676a1d fix(library/compiler/emit_cpp): tail call arguments may be neutral elements 2019-03-21 15:06:46 -07:00
Sebastian Ullrich
b9edaf888f chore(library/init/core): ne -> Ne, not -> Not 2019-03-21 15:06:45 -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
0b5862b6ce chore(*): and => And 2019-03-21 15:06:44 -07:00
Leonardo de Moura
4c50859129 chore(*): or => Or 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
f8113a01eb chore(library): unit => Unit 2019-03-21 15:06:44 -07:00
Leonardo de Moura
e0b0ca4830 chore(*): adapt C++ code to camelCase 2019-03-21 15:06:43 -07:00
Leonardo de Moura
bc75a24127 chore(library, frontends): use camelCase for attribute names 2019-03-21 15:06:43 -07:00
Leonardo de Moura
039e7fab48 refactor(library): add suffixes.h with commonly used suffixes such as brec_on 2019-03-21 15:06:43 -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
Leonardo de Moura
437f446844 chore(library/type_context): error instead of assertion violation 2019-03-19 11:25:55 -07:00