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

10568 commits

Author SHA1 Message Date
Sebastian Ullrich
84e9dd9b1a feat(library/init/lean/elaborator,frontends/lean/vm_elaborator): implement def/theorem/abbreviation 2019-01-12 15:10:00 +01:00
Sebastian Ullrich
49f580f190 feat(library/compiler/builtin,frontends/lean/vm_elaborator): add temporary expr.local primitive 
This makes it possible (or at least much easier) to interface with old
parser/elaborator code using local_consts for e.g. `def` parameters.
 2019-01-12 14:16:43 +01:00
Sebastian Ullrich
da865fc33a refactor(frontends/lean/{vm_,}elaborator): move name resolution over to parser locals 
In the end I wasn't quite sure whether this is necessary, but it's at least simpler.
 2019-01-12 14:14:22 +01:00
Leonardo de Moura
e0da13128e refactor(library/compiler/llnf): explicit_rc_fn 2019-01-09 16:57:38 -08:00
Leonardo de Moura
7b4b92702f feat(library/compiler/llnf): cancel _unbox over _box and _box over _unbox 2019-01-09 16:57:38 -08:00
Leonardo de Moura
78379e2224 fix(library/compiler/llnf): avoid unnecessary let-decl at cast_if_needed 2019-01-09 16:57:38 -08:00
Leonardo de Moura
c1fd3e6062 fix(library/compiler/llnf): unnecessary let-decl 2019-01-09 16:57:38 -08:00
Leonardo de Moura
8111aaad8a fix(library/compiler/llnf): missing case 2019-01-09 16:57:37 -08:00
Sebastian Ullrich
2b5f19677d feat(frontends/lean/vm_elaborator): elaborate #check 2019-01-07 22:19:47 +01:00
Sebastian Ullrich
b17568aeff feat(library/init/lean/elaborator): pass current namespace to C++ elaborator 
This seems to be the only information in `scope_mng_ext` we definitely need
 2019-01-06 18:10:49 +01:00
Sebastian Ullrich
d2de703e51 feat(frontends/lean/vm_elaborator): add primitive environment.contains 2019-01-06 15:47:06 +01:00
Sebastian Ullrich
9a6ae42be8 feat(frontends/lean/vm_elaborator): return new environment 2019-01-06 15:44:56 +01:00
Sebastian Ullrich
807b460e9c feat(*/elaborator): pass preresolved names to C++ as annotations and use them for global name resolution 
With actual preresolution still missing, the only preresolved names so far are
ones like `opt_param` from built-in macros that have been preresolved manually
(and which weren't successfully resolved before this commit because of the macro
scopes applied to them)
 2019-01-01 23:59:23 +01:00
Sebastian Ullrich
23c83d7e06 refactor(library/placeholder,library/init/lean/elaborator): encode pexpr placeholders as anonymous mvars 2018-12-21 15:53:12 +01:00
Sebastian Ullrich
5757792345 chore(library/placeholder): remove unused placeholder type and kinds 2018-12-21 15:52:56 +01:00
Sebastian Ullrich
8753491cb5 chore(library/placeholder): remove obsolete level one_placeholder 
Remnant of the previous Type/Sort approach
 2018-12-21 15:52:56 +01:00
Sebastian Ullrich
cbc297e5c5 feat(frontends/lean/vm_elaborator): resolve names in constants' types 
This is just a stop-gap solution. We need to move name resolution to Lean to
correctly handle names preresolved by the macro expander.
 2018-12-19 18:49:33 +01:00
Sebastian Ullrich
0a5af76f1a feat(frontends/lean/vm_elaborator): capture and pass all elab messages to Lean 2018-12-19 16:22:30 +01:00
Sebastian Ullrich
ead4e8998d feat(library/init/lean/elaborator): elaborate constants 2018-12-19 15:04:48 +01:00
Sebastian Ullrich
c5dfe7f86e refactor(frontends/lean/decl_cmds): factor out and expose elaboration of variables and constants 2018-12-19 15:04:48 +01:00
Sebastian Ullrich
4f7be93e87 feat(library/init/lean): remove support for section aliases 2018-12-18 17:04:04 +01:00
Sebastian Ullrich
db6b1d6e85 feat(frontends/lean/vm_elaborator,library/init/lean/elaborator): pass parser_state between languages, create parser object on C++ side to existing functions (that don't actually parse anything) 2018-12-18 15:30:38 +01:00
Sebastian Ullrich
d214df63f1 fix(library/equations_compiler/compiler): eta-expand recursive occurrences earlier 2018-12-18 15:30:38 +01:00
Sebastian Ullrich
861136d290 feat(frontends/lean/decl_cmds): universe(s) now behaves like universe variable(s) 2018-12-17 23:30:28 +01:00
Sebastian Ullrich
4e96f092f9 feat(library/init/lean/elaborator): delegate elaboration of attribute 2018-12-14 17:38:19 +01:00
Sebastian Ullrich
d9a22d43b2 feat(library/vm/vm_aux): add primitive for calling old elaborator 2018-12-14 17:36:56 +01:00
Sebastian Ullrich
ac1bb5dfb0 feat(library/equations_compiler/wf_rec): eta-expand unapplied recursive calls 2018-12-06 13:23:12 +01:00
Leonardo de Moura
607d22ae58 fix(library/compiler/csimp): bug at float_cases_on_core 
The bug occurs when floating `cases_on` application in code of the form
```
let x := C.cases_on ...
in t
```
and when the type of `t` depends on `x`.
The issue here is that the `x` declaration disappears after the float, but the resulting type still depends on it.
We fix the bug by replacing `x` with its value in the type.

cc @kha
 2018-11-30 11:40:41 -08:00
Leonardo de Moura
eae421c506 feat(library/compiler/llnf): explicit_rc skeleton 2018-11-28 15:44:55 -08:00
Leonardo de Moura
05d25d92c0 feat(library/compiler): only create _boxed version if needed 2018-11-28 09:46:48 -08:00
Sebastian Ullrich
c8eaee74b4 feat(frontends/lean,library/init/lean/parser/combinators): add node_longest_choice! macro 2018-11-19 18:02:28 +01:00
Sebastian Ullrich
7d7d15f8f7 chore(frontends/lean/elaborator): improve error positions 2018-11-19 15:28:23 +01:00
Sebastian Ullrich
774d776133 feat(frontends/lean/builtin_exprs): pattern let with type 2018-11-19 14:15:25 +01:00
Sebastian Ullrich
6d0b3afa7e fix(library/compiler/compiler): do not silently abort on user-given sorrys 2018-11-17 18:00:55 +01:00
Leonardo de Moura
3d24c6466b feat(library/compiler/llnf): generate _boxed version eagerly 2018-11-15 18:10:20 -08:00
Leonardo de Moura
ae037c2a23 fix(library/compiler/builtin): incorrect assertion 2018-11-15 18:09:02 -08:00
Leonardo de Moura
da92557076 chore(library/vm/vm_int): missing builtin in the old VM 2018-11-15 16:58:05 -08:00
Leonardo de Moura
b55b1deaf5 chore(library/compiler): remove ir.cpp 
There is only one missing transformation: insert explicit reference counting instructions.
We will implement this transformation at `llnf.cpp`. After that, we are
ready to emit C++ code.
 2018-11-15 16:53:44 -08:00
Leonardo de Moura
e5666b3464 feat(library/compiler): remove another reference to vm.h 2018-11-15 16:38:01 -08:00
Leonardo de Moura
db5d976278 feat(library/compiler): use new builtin module 2018-11-15 16:30:42 -08:00
Leonardo de Moura
3a7d407d6c feat(library/compiler/builtin): register io primitives 
TODO: implement `io` primitives in the new runtime
 2018-11-15 16:14:50 -08:00
Leonardo de Moura
4f2997d691 feat(library/compiler/builtin): use std::unordered_map 2018-11-15 13:48:11 -08:00
Leonardo de Moura
4b65e0bace refactor(library/compiler/builtin): do not store pointer to functions 
The interface between the (to be implemented) new interpreter and the
compiled code will be automatically generated.
 2018-11-15 13:39:04 -08:00
Leonardo de Moura
5acdd68ad5 feat(library/compiler/init_module): initialize builtin module 2018-11-15 13:33:02 -08:00
Leonardo de Moura
b501613f8c feat(library/compiler/builtin): register string primitive functions 2018-11-15 13:26:41 -08:00
Leonardo de Moura
70c4e33cf2 feat(runtime/object): missing string.iterator builtin functions 2018-11-15 13:05:29 -08:00
Leonardo de Moura
4a0a3f8d85 feat(library/compiler/builtin): register int primitives 2018-11-15 12:39:35 -08:00
Leonardo de Moura
d0e96ee600 feat(runtime/object): missing int builtins 2018-11-15 12:31:34 -08:00
Leonardo de Moura
a3db4e8e09 chore(*): style 2018-11-15 10:59:17 -08:00
Leonardo de Moura
efa703d2b5 feat(runtime): implement string.iterator primitives in the new runtime 
Some of the primitives do not have optimal implementation.

@Kha Could you please check if everything we use in the parser has a
reasonable implementation?
 2018-11-15 10:42:23 -08:00