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

87 commits

Author SHA1 Message Date
Leonardo de Moura
e16e9880f7 chore(library/system): enforce Lean naming conventions IO ==> io 2016-11-17 11:27:37 -08:00
Leonardo de Moura
fffe69fdf9 feat(library/vm,library/tactic/vm_monitor): use optionT to define vm monad 2016-11-14 16:13:56 -08:00
Leonardo de Moura
7232e3a076 feat(library/vm/vm): invoke debugger (aka vm_monitor) 2016-11-14 14:45:49 -08:00
Leonardo de Moura
e673fa65ba feat(library/vm/vm): Store position information at vm_decl's 2016-11-11 15:39:32 -08:00
Leonardo de Moura
7d3c0c24f8 fix(library/compiler): missing file 2016-11-10 09:34:32 -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
b79b76db83 feat(library/compiler/vm_compiler): improve local_info collection 2016-11-09 12:18:44 -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
Leonardo de Moura
6b3da2daf4 feat(library/compiler/vm_compiler): save local_info for let-expressions 2016-11-08 15:50:38 -08:00
Leonardo de Moura
d66584f390 feat(library/vm,library/compiler): save argument names 2016-11-08 15:10:04 -08:00
Leonardo de Moura
1cee5fbfea chore(library/compiler/vm_compiler): hide API 2016-11-05 14:11:21 -07:00
Gabriel Ebner
41643d6400 fix(library/compiler/vm_compiler): prevent segfault 2016-11-04 09:47:17 -07:00
Leonardo de Moura
9d3aa5b627 fix(library/compiler/elim_recursors): bug in elim_recursors 
We may fail to type check auxiliary definitions that use rec_fn_macro.
The problem is that this macro cannot be unfolded.
So, we fix the problem by not type checking them. We add them as
constants, and store the definition in an auxiliary vector.
 2016-11-02 14:19:28 -07:00
Leonardo de Moura
e62810c9b8 fix(library/compiler/lambda_lifting): make sure constructors are eta-expanded 
closes #1133
 2016-11-02 13:26:15 -07:00
Leonardo de Moura
30ae8a29b6 fix(library/compiler/elim_recursors): some recursor applications were not being eliminated 2016-11-02 13:05:52 -07:00
Leonardo de Moura
a77e4b5abf fix(library/compiler/erase_irrelevant): bug at is_comp_irrelevant 2016-10-27 11:51:37 +08:00
Leonardo de Moura
7465529445 feat(library/tactic): 'eval_expr' tactic skeleton 2016-10-03 16:26:28 -07:00
Leonardo de Moura
5e5285ee67 refactor(library): rename pr1/pr2 ==> fst/snd 2016-09-21 09:48:39 -07:00
Leonardo de Moura
b524e3d5f1 fix(frontends/lean/elaborator): postprocess rec_fn_macros used in meta_definitions 2016-09-18 13:01:50 -07:00
Leonardo de Moura
2ac2badd58 fix(library/compiler/preprocess): do not unfold proofs 2016-09-13 08:47:39 -07:00
Leonardo de Moura
932d14241b chore(kernel): remove support for mutually inductive datatypes from the kernel 2016-09-10 17:39:17 -07:00
Leonardo de Moura
0b2c3659cf perf(library/compiler/nat_value): replace all numerals with nat_value_macro 
Reason: Later we try to type check the compiler intermediate results.
If only some of the numerals are converted, we may spend a lot of time
making sure the two different representations are equivalent.
 2016-09-04 16:42:40 -07:00
Leonardo de Moura
567d6824f4 chore(library/compiler/preprocess): mark assertions as conditional 
is_def_eq may take a very long time after the transformations are applied.
 2016-09-03 16:15:22 -07:00
Leonardo de Moura
0ec22bb2cf refactor(library/type_context): new type class instance cache 2016-09-01 17:37:30 -07:00
Sebastian Ullrich
441a219a66 feat(library/attribute_manager): make attributes with side-effect free callbacks removable 2016-08-23 21:52:52 -07:00
Leonardo de Moura
a93eada058 feat(library/type_context): improved (and simplified) cache management for type_context 2016-08-23 17:56:58 -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
f5c35f8d76 chore(*): fix compilation warnings 2016-08-10 18:03:13 -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
7bb6ccc089 refactor(library/init/meta): qexpr ==> pexpr 2016-08-05 17:04:36 -07:00
Leonardo de Moura
60c4384d09 fix(library/compiler/elim_recursors): buggy way to detect recursive arguments 2016-07-06 23:27:04 -07:00
Leonardo de Moura
2b43f591c9 fix(library/type_context): remove m_cache_owner field 
This idiom creates problem if we use (even accidentally) the copy constructor.
 2016-06-23 14:03:46 -07:00
Leonardo de Moura
586baa4118 feat(library,frontends/lean): support for quoted expressions in the VM, compiler and frontend 
TODO: invoke elaborator at tactic.to_expr
 2016-06-15 16:06:39 -07:00
Leonardo de Moura
165d45ac32 fix(library/compiler/erase_irrelevant): monad.return was renamed to monad.ret 2016-06-08 16:17:33 -07:00
Leonardo de Moura
2eafe66240 fix(library/compiler/lambda_lifting): relax assertion 2016-06-06 14:11:05 -07:00
Leonardo de Moura
81947e145e feat(library/vm,library/compiler): add support for builtin cases_on 2016-06-01 19:06:52 -07:00
Leonardo de Moura
6f02d30185 feat(library/vm): add basic support for C++ name objects in the VM 
We still need to add support for the recursor
 2016-06-01 13:10:24 -07:00
Leonardo de Moura
faf70ed58c feat(library/vm/vm): add support for declaring builtin cfunctions 2016-05-31 16:48:11 -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
713c97a3be fix(library/compiler/preprocess): make sure no_confusion is not expanded by expand_aux 2016-05-25 17:57:17 -07:00
Leonardo de Moura
f9624b4c49 fix(library/compiler/vm_compiler): ignore applications of the form (neutral ...) during code generation 2016-05-25 17:52:42 -07:00
Leonardo de Moura
856f6bcbdf fix(library/compiler/erase_irrelevant): missing case 2016-05-25 17:49:02 -07:00
Leonardo de Moura
bf9300686c feat(library/compiler/vm_compiler): ignore macro annotations 2016-05-25 17:26:15 -07:00
Leonardo de Moura
abd2bbab78 feat(library/compiler/preprocess): expand auxiliary declarations automatically created by Lean (e.g., transitivite instances) 
These declarations do not have VM bytecode associated with them.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2016-05-25 17:09:16 -07:00
Leonardo de Moura
c5616969e0 fix(library/compiler/simp_inductive): distribute extra cases_on arguments over minor premises in the simp_inductive step 2016-05-25 15:46:01 -07:00
Leonardo de Moura
1b8d9deb37 chore(library/compiler/erase_irrelevant): style 2016-05-25 15:45:43 -07:00
Leonardo de Moura
be7a736a42 feat(library/compiler/vm_compiler): trace bytecode after/before optimization 2016-05-25 15:45:16 -07:00