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

3418 commits

Author SHA1 Message Date
Leonardo de Moura
4bf97be30a chore(library/init/compiler/ir): cleanup 2018-04-24 13:00:39 -07:00
Leonardo de Moura
1fd399d06f feat(library/init/compiler/ir): use run_state and run_reader 2018-04-24 12:48:12 -07:00
Leonardo de Moura
9389176380 feat(library/init/category): add missing @[inline] to adapt functions 2018-04-23 10:38:54 -07:00
Leonardo de Moura
c0d782ce3c feat(library/init/compiler/ir): we don't need collector 2018-04-23 08:56:22 -07:00
Leonardo de Moura
563c9fce4e fix(library/init/compiler/ir): SSA validator 
TODO: check whether the assumptions made here match LLVM IR semantics
 2018-04-20 18:27:13 -07:00
Leonardo de Moura
3eeb337423 fix(library/init/compiler/ir): phi instructions must only occur in the beggining of the block 2018-04-20 18:27:13 -07:00
Leonardo de Moura
b35be8e6b7 feat(library/init/compiler/ir): simplify phi instruction 
The blockid is only needed by LLVM, and we can infer this information
when mapping to LLVM.
 2018-04-20 18:27:13 -07:00
Leonardo de Moura
29ee8493c0 feat(library/init/compiler/ir): blockid validator 2018-04-20 18:27:13 -07:00
Leonardo de Moura
ba9782bc5a feat(library/init/compiler/ir): collect used variables 2018-04-20 18:27:13 -07:00
Leonardo de Moura
7260ac91ed feat(library/init/compiler/ir): declare new IR in Lean 
Next steps:
- Implement more validators (e.g., blockid validator, type checker).
- Implement C++ code generator (in Lean). We can use it for testing the new
  lean_obj module implemented in C++.
- Implement interpreter (in C++) for sanity checking.
- Implement LLVM IR generator (in Lean). It just outputs a text file using LLVM
  syntax. After, we are confident we are generating valid LLVM IR, we
  can try to link LLVM with Lean.
 2018-04-20 18:27:13 -07:00
Leonardo de Moura
8b51a05657 feat(library/init/category/combinators): add list.mforall and list.mexists 
Remark: the non monadic versions are called list.all and list.any.
We did not use `list.mall` and `list.many` since `mall` and `many` are
existing words.
 2018-04-20 18:27:13 -07:00
Leonardo de Moura
50328d62e1 feat(library/init/data): add uint16 and make sure uint* - uses wraparound semantics like most programming languages 2018-04-20 18:27:13 -07:00
Sebastian Ullrich
a7688a10b8 feat(frontends/lean/definition_cmds): elaborate a def's type separately when explicit return type is given 2018-04-20 09:59:09 -07:00
Leonardo de Moura
1e11611388 chore(library): cleanup constants.txt 2018-04-12 16:43:11 -07:00
Sebastian Ullrich
726a5547de fix(init/core): typed_expr should accept Props 
Fixes #1954
 2018-04-12 16:14:47 +02:00
Leonardo de Moura
1ad1080f11 refactor(library): keep only basic nat theorems 
All theorems are proved without using the tactic framework.
Thus, we can define `fin/uint32/uint64` types and their operations
before we define the tactic framework.
 2018-04-11 16:47:54 -07:00
Leonardo de Moura
75f91df707 chore(library/init/data/fin/ops): remove unnecessary ops 2018-04-10 16:41:18 -07:00
Leonardo de Moura
ce0467638e chore(*): remove unification hints 2018-04-10 16:29:04 -07:00
Leonardo de Moura
10ddfdafbd chore(*): remove VM monitor 2018-04-10 16:08:47 -07:00
Leonardo de Moura
b74e05b262 chore(*): remove mk_*_instance tactics 2018-04-10 16:03:42 -07:00
Leonardo de Moura
1b1495aea4 chore(*): remove norm_num 2018-04-10 15:59:29 -07:00
Leonardo de Moura
0bcf5c8f5d chore(*): remove algebra 2018-04-10 15:53:14 -07:00
Leonardo de Moura
7aaac31e35 chore(library/init/data/nat): remove dependency 2018-04-10 15:48:13 -07:00
Leonardo de Moura
b0e49535fa chore(*): remove transfer and coinductive predicates 2018-04-10 13:38:18 -07:00
Leonardo de Moura
c03d351744 chore(library/init/data/int): keep only definitions 2018-04-10 13:29:06 -07:00
Leonardo de Moura
a023128738 chore(*): reduce corelib 2018-04-10 13:11:40 -07:00
Leonardo de Moura
47cd2ee61a chore(leanpkg): delete 2018-04-10 12:43:17 -07:00
Leonardo de Moura
41d1293b38 chore(*): reduce corelib 2018-04-10 12:33:09 -07:00
Leonardo de Moura
b14d69b1d7 chore(*): remove converter, ac_tactics, hole_commands, rbtree/rbmap proofs, bitvec 2018-04-10 12:25:51 -07:00
Leonardo de Moura
a2f0bf7c1b chore(*): disable SMT tactic framework and backward chaining 2018-04-10 12:05:51 -07:00
Leonardo de Moura
bcaa0b2ad3 refactor(library/typed_expr): do not use macros for implementing typed_expr 
Remark: in Lean4, we will not have macro_defs.
 2018-04-09 15:16:46 -07:00
Sebastian Ullrich
8f55ec4c50 fix(init/core): remove out_param from has_pow 
With the current elaboration scheme, out_params and coercions do not mix well,
as evidenced by the following example by @digama:

```
variables {α : Type*} [group α]
def gpow : α → ℤ → α := sorry
instance group.has_pow : has_pow α ℤ := ⟨gpow⟩

example (a : α) : a ^ 0 = 1 := sorry -- failed to synth ⊢ has_pow α ℕ
example (a : α) : a ^ (0:ℕ) = 1 := sorry -- ok, coerces
example (a : α) : a ^ (0:ℤ) = 1 := sorry -- ok
```

The issue is that
* we first try to solve `has_pow ?α ?β`, which is postponed
* then infer `?α = nat` from `a`
* then at some point call `elaborator::synthesize()` and default `β` to `nat`
* then try to solve `has_pow nat nat`, which fails at `int =?= nat`
 2018-04-04 13:05:59 +02:00
Leonardo de Moura
d387103aa2 fix(library/init/core): closes #1951 
- Add has_pow type class
- Make `^` notation right associative
 2018-03-29 16:25:47 -07:00
Sebastian Ullrich
3fefe94757 refactor(library/init/core,library/init/unit): make unit an abbreviation of punit.{0} 2018-03-27 10:33:04 -07:00
Sebastian Ullrich
a41d797900 fix(init/category/state): lift unintended universe restriction 2018-03-26 13:00:23 +02:00
Sebastian Ullrich
0f7a8907c7 fix(init/data/default): add missing files 2018-03-22 00:15:56 +01:00
Sebastian Ullrich
0c0646f03b chore(leanpkg/lean_version): recognize nightlies as releases separate from master 2018-03-20 15:14:45 -07:00
Sebastian Ullrich
28f4143be3 feat(init/category/except): add monad_except_adapter for change the error type of a monad stack 2018-03-20 14:58:37 -07:00
Sebastian Ullrich
4593d7fcda feat(init/category/reader): add transitive monad_except instance 2018-03-20 14:58:37 -07:00
Sebastian Ullrich
277f8b7929 perf(init/category/reader): add inline annotations 2018-03-20 14:58:37 -07:00
Sebastian Ullrich
7daf6a2133 refactor(init/category): change _functor classes into new _adapter classes, add docs 2018-03-20 14:58:37 -07:00
Sebastian Ullrich
6b88f84cd6 refactor(init/category/reader): replace monad_reader_lift with Haskell's MonadReader class 2018-03-20 14:58:37 -07:00
Sebastian Ullrich
70167def6f refactor(init/category/state): replace monad_state_lift with Haskell's MonadState 
* does not leak information about the inner monad via out_param
* can be derived from an inner `monad_state` instance
 2018-03-20 14:58:37 -07:00
Sebastian Ullrich
112bddd343 chore(init/category/lift): remove unused monad_run.unrun field 2018-03-20 14:58:37 -07:00
Sebastian Ullrich
8fce7a342d chore(init/category/monad_fail): remove monad superclass for consistency with other monad classes 
Also remove misleading TODO
 2018-03-20 14:58:37 -07:00
Sebastian Ullrich
dc3db17fcd chore(data/buffer/parser): remove universe parameter 
All operations are defined on Type only anyway
 2018-03-20 14:58:36 -07:00
Sebastian Ullrich
23884d2863 refactor(init/data/option_t): move to init/category and adapt style 2018-03-20 14:58:36 -07:00
Sebastian Ullrich
bcbe5ec9f4 refactor(init/category/functor): merge has_map into functor 2018-03-20 14:58:36 -07:00
Sebastian Ullrich
3adc5113cb feat(init/category/state): make zoom work linearly 2018-03-20 14:58:36 -07:00
Sebastian Ullrich
720e8c2640 doc(init/category/except): add reference to monad_except and move to end 2018-03-20 14:58:36 -07:00