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

1146 commits

Author SHA1 Message Date
Leonardo de Moura
5fc90adf6b feat(kernel): add whnf_cond to kernel type_checker 2016-04-28 16:08:03 -07:00
Leonardo de Moura
0b812bc91d fix(kernel/declaration): typo and restoring trusted flag for constants 2016-04-28 15:59:09 -07:00
Leonardo de Moura
7932872487 feat(kernel/declaration): untrusted constant declarations 
This feature is useful for implementing the new tactic framework
 2016-04-28 15:16:24 -07:00
Leonardo de Moura
a29eaf0067 feat(kernel): add 'trusted' flag for definitions 2016-04-11 15:49:29 -07:00
Leonardo de Moura
4728b03f20 refactor(kernel/type_checker): do not use definitional depth in the kernel type checker 2016-04-11 14:53:02 -07:00
Leonardo de Moura
29ad781ec2 refactor(kernel): remove converter class 
This abstraction is not useful after refactoring.
 2016-03-19 15:58:15 -07:00
Leonardo de Moura
856889a08d refactor(kernel): remove dead code from type_checker 2016-03-19 15:28:19 -07:00
Leonardo de Moura
6406d7cf8b refactor(kernel): merge include files that are used only once 2016-03-19 15:20:12 -07:00
Leonardo de Moura
487a1e7f89 refactor(kernel): remove extension_context 
We replaced it with abstract_type_context
 2016-03-19 15:15:39 -07:00
Leonardo de Moura
63d8a0ed45 refactor(kernel): move justification/constraint/metavar to library 
These files will be eventually deleted
 2016-03-19 14:39:15 -07:00
Leonardo de Moura
e7f1f409c4 refactor(kernel): simplify kernel type_checker 
TODO: cleanup, move justification/metavar/constraints to library
 2016-03-18 16:28:42 -07:00
Leonardo de Moura
d8079aa16a refactor(library): create copy of the kernel type_checker in library 
Motivation: it will allow us to simplify the kernel type_checker and
make sure it implements the same API provided by type_context
 2016-03-18 14:34:10 -07:00
Leonardo de Moura
c679c3a8d4 dev(kernel/abstract_type_context): extend abstract_type_context API 2016-03-08 11:40:36 -08:00
Leonardo de Moura
3c878ecd01 feat(kernel): add let-expressions to the kernel 
The frontend is still using the old "let-expression macros".
We will use the new let-expressions to implement the new tactic framework.
 2016-02-29 16:40:17 -08:00
Leonardo de Moura
2b1d734544 feat(kernel/expr): remove 'contextual' flag from binder_info 2016-02-29 12:41:43 -08:00
Leonardo de Moura
2fd5347901 refactor(library/blast): ppb is not necessary anymore 2016-02-26 15:51:46 -08:00
Leonardo de Moura
eee74ef1b4 refactor(frontends/lean/pp): use abstract_type_context instead of type_checker 2016-02-26 15:35:29 -08:00
Leonardo de Moura
7d61f640f6 refactor(*): add abstract_type_context class 2016-02-26 14:17:34 -08:00
Leonardo de Moura
c9e9fee76a refactor(*): remove name_generator and use simpler mk_fresh_name 2016-02-11 18:05:57 -08:00
Leonardo de Moura
f67181baf3 chore(*): remove support for Lua 2016-02-11 17:17:55 -08:00
Leonardo de Moura
4324726a8e perf(kernel/expr_eq_fn): minimize number of calls to check_system 2016-02-02 18:16:14 -08:00
Leonardo de Moura
d9294fc164 chore(kernel/expr): remove dead var 2016-01-13 17:36:33 -08:00
Leonardo de Moura
723a9e227a chore(kernel/default_converter): remove dead code 2016-01-13 13:33:13 -08:00
Leonardo de Moura
930fcddace feat(kernel/expr): add get_app_args_at_most 2016-01-06 17:29:28 -08:00
Leonardo de Moura
ba392f504f feat(kernel/expr,library/blast/blast,frontends/lean/decl_cmds): add workaround for allowing users to use blast inside of recursive equations 2016-01-03 21:53:31 -08:00
Leonardo de Moura
999f23cbc0 feat(kernel/expr_eq_fn): take names into account when CompareBinderInfo is true 
This is the correct fix for the id declaration pretty printing
discrepancy reported by Daniel.

TODO: decide whether we need another eq-mode where names are ignored.
For example, in blast, it makes sense to increase sharing by ignoring
binder names.
 2015-12-13 14:47:11 -08:00
Leonardo de Moura
1abaa9eb71 fix(frontends/lean/parser): fixes #858 2015-12-10 10:31:14 -08:00
Leonardo de Moura
93b17e2ec1 refactor(kernel/ext_exception): add ext_exception 
Now, any exception that requires pretty printing support should be a
subclass of ext_exception
 2015-12-04 13:22:42 -08:00
Leonardo de Moura
769da9c95a fix(library/unifier): missing occurs check 2015-12-04 09:14:55 -08:00
Daniel Selsam
413989afd6 feat(library/blast/backward): backward chaining strategy 2015-11-18 17:48:39 -08:00
Leonardo de Moura
d5d8ac8b44 fix(kernel/expr): warning when compiling using clang on OSX 2015-11-16 18:50:34 -08:00
Leonardo de Moura
92a7c38260 feat(kernel/expr): add mk_app that takes a list of arguments 2015-11-13 14:01:15 -08:00
Leonardo de Moura
76032eea90 feat(kernel/expr): change dummy expression used in default constructor 2015-11-08 14:05:02 -08:00
Leonardo de Moura
a446c54b87 fix(tests/kernel/max_sharing): max_sharing on OSX 2015-10-03 12:12:21 -07:00
Leonardo de Moura
d324d54d21 fix(kernel/expr): add global expressions storing Prop and Type.{1} to 
hash-consing cache when max-sharing is enabled
 2015-10-02 15:04:10 -07:00
Leonardo de Moura
3cf11dac87 feat(kernel/instantiate): make sure instantiate_type_univ_params and instantiate_value_univ_params caches are reset when we enable max-sharing 2015-10-01 15:42:33 -07:00
Leonardo de Moura
45594e86c7 feat(kernel/abstract): make sure Pi/Fun cache is reset when we enable max-sharing 2015-10-01 15:28:55 -07:00
Leonardo de Moura
cb2f93ee6a fix(kernel/expr,kernel/level): performance problem 
The method unordered_set::clear takes time O(n) where n is the number of
buckets in the hashtable used to implement the set.
Moreover, it does not reduce the number of buckets to 0.
That is, it keeps `n` empty buckets.

This creates performance problems if the number of buckets gets really
huge at one point.
The tst6 at tests/kernel/expr.cpp demonstrates the problem
 2015-09-30 17:25:13 -07:00
Leonardo de Moura
d07bbe7e8c fix(kernel/expr): must take binder annotations into account in the hash-consing tables 2015-09-30 17:24:41 -07:00
Leonardo de Moura
57035d3162 feat(kernel/level,library/blast/expr): add universe level hash consing support in the kernel, simplify blast/expr even more 2015-09-30 13:31:42 -07:00
Leonardo de Moura
c5603e456a feat(kernel/expr): replace "opportunistic" caching with precise caching 
We also removed compilation option LEAN_CACHE_EXPRS
 2015-09-30 12:29:43 -07:00
Leonardo de Moura
4cfebe7f1c refactor(kernel): move instantiate_univ_cache to separate .h file 2015-09-21 16:08:34 -07:00
Leonardo de Moura
9c09b0750b chore(kernel/expr): remove dead code 2015-09-21 15:43:51 -07:00
Leonardo de Moura
a7c2d798de refactor(kernel): move replace_cache to separate .h file 2015-09-21 15:24:45 -07:00
Leonardo de Moura
df3100d2cd fix(library/local_context): bug in abstract_locals procedure 2015-09-12 17:17:13 -07:00
Leonardo de Moura
45163acf25 refactor(kernel/inductive): use local constants to represent introduction rules 2015-08-25 03:46:28 -07:00
Leonardo de Moura
edb4c09bc1 fix(frontends/lean,kernel/inductive): compilation errors in Debug mode 2015-08-16 19:02:48 -07:00
Leonardo de Moura
5f5642c4ce fix(kernel/inductive): compilation error with clang++ 2015-08-15 15:06:57 -07:00
Leonardo de Moura
7bc8673786 feat(library/module): efficient inductive_reader 
Do not check imported inductive declarations when trust level is greater than 0.
 2015-08-15 14:48:49 -07:00
Leonardo de Moura
e80d9685e5 refactor(kernel/inductive): add certified_inductive_decl object 
We will use this object to implement a more efficient import procedure
 2015-08-15 13:26:38 -07:00