michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
4440 commits 3 branches 0 tags 28 MiB
Commit graph

86 commits

Author SHA1 Message Date
Leonardo de Moura
1ce3b83d79 fix(kernel/metavar): compilation error in some compilers 2014-10-17 17:22:25 -07:00
Leonardo de Moura
58aff5b4af perf(kernel/metavar): used thread local cache for instantiate_metavars 2014-10-17 17:08:35 -07:00
Leonardo de Moura
10b880ce3b perf(kernel/metavar): improve occurs_expr and occurs performance 2014-10-17 14:05:22 -07:00
Leonardo de Moura
14ebbda8cb perf(kernel/metavar): minor improvement 2014-10-16 21:43:54 -07:00
Leonardo de Moura
4cf3d32e0c chore(*): create alias for std::pair 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-20 16:46:19 -07:00
Leonardo de Moura
77c0456be4 fix(kernel/metavar): make sure instantiate_metavars_fn does not loop on 'fake' recursive dependencies, we say they are fake because they disappear after applying beta-reduction 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-24 12:04:33 -07:00
Leonardo de Moura
13fe28dd1c perf(library/unifier): delay the instantiation of metavariables occurring in the types of local constants 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-23 14:31:30 -07:00
Leonardo de Moura
adddf06e44 perf(kernel/metavar): avoid destructive update in occurs method 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-23 13:12:29 -07:00
Leonardo de Moura
301c395e59 perf(kernel/metavar): performance problem with occurs method 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-23 10:35:27 -07:00
Leonardo de Moura
61661478ad refactor(kernel/metavar): simplify substitution class, and remove dead code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-23 10:03:03 -07:00
Leonardo de Moura
caf3e5a449 fix(kernel/metavar): missing justification bug 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-23 08:41:09 -07:00
Leonardo de Moura
46005b4ffe perf(kernel/metavar): improve occurs_expr method 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-15 01:57:17 +01:00
Leonardo de Moura
a38dc76b37 feat(kernel/metavar): add option to instantiate only expr metavars 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-12 05:54:05 +01:00
Leonardo de Moura
9517f31a71 refactor(kernel/metavar): remove unnecessary functionality 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-12 04:45:50 +01:00
Leonardo de Moura
a009225435 feat(kernel/metavar): expose destructive assign 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-03 14:07:47 -07:00
Leonardo de Moura
b49902807c refactor(kernel/metavar): separate substitution from their justifications 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-03 14:01:22 -07:00
Leonardo de Moura
6a6ebd5c2d refactor(kernel/metavar): add method instantiate as alias for instantiate_metavars_wo_jst 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-02 15:39:25 -07:00
Leonardo de Moura
fedbf8595b feat(kernel/metavar): collect unassigned metavariables while instantiating 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-21 16:58:09 -07:00
Leonardo de Moura
40b3129e7b refactor(kernel): improve names 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-16 11:28:05 -07:00
Leonardo de Moura
9c5dfc387b refactor(kernel/replace_visitor): remove context from replace_visitor 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-14 15:53:09 -07:00
Leonardo de Moura
0bc101ac28 fix(kernel/metavar): typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-01 15:28:34 -07:00
Leonardo de Moura
027614cebb fix(kernel/metavar): wierd memory leak that only happens when compiling with clang++ 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-01 12:55:55 -07:00
Leonardo de Moura
49e626a0e0 refactor(kernel/metavar): switch to functional substitution datastructure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-29 10:22:36 -07:00
Leonardo de Moura
a55c3c617d feat(kernel/type_checker): add infer_type 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-25 11:58:29 -07:00
Leonardo de Moura
3939b93c2d refactor(kernel): substitution 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:57 -07:00
Leonardo de Moura
bf13441bd7 fix(kernel): bugs in justification module, add missing metavar methods, add basic metavar tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:56 -07:00
Leonardo de Moura
3c6002e969 refactor(kernel): add mk_rev_app, update_rev_app, implement instantiate_metavars functions, modify instantiate (free vars) API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:56 -07:00
Leonardo de Moura
968c0d799f refactor(kernel): implement substitution methods 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:56 -07:00
Leonardo de Moura
5f4b1cf47e feat(kernel): define metavar substitution based on red-black trees 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:56 -07:00
Leonardo de Moura
997f32378c refactor(kernel): remove unnecessary files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:56 -07:00
Leonardo de Moura
1739b5c153 fix(kernel/type_checker): caching bug 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-12 10:43:01 -08:00
Leonardo de Moura
160dc71cb5 refactor(kernel/type_checker): use read-only metavariable environment in methods that do not require write access to the metavariable environment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-27 17:38:06 -08:00
Leonardo de Moura
05b4d8411b refactor(kernel/normalizer): normalizer only needs read access to metavariable environment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-27 17:03:36 -08:00
Leonardo de Moura
3b152d1a9e refactor(kernel): use ro_metavar_env instead of metavar_env in places where we only need to read the metavariable environment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-27 16:44:43 -08:00
Leonardo de Moura
4d25cb7f47 feat(library/tactic): add simplify_tactic based on the simplifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-26 18:53:18 -08:00
Leonardo de Moura
9eb4dc4a81 feat(kernel, library/elaborator, frontends/lean): improve how elaborator_exceptions are displayed in the Lean frontend 
This commit affects different modules.
I used the following approach:
1- I store the metavariable environment at unification_failure_justifications. The idea is to capture the set of instantiated metavariables at the time of failure.
2- I added a remove_detail function. It removes propagation steps from the justification tree object. I also remove the backtracking search space associated with higher-order unificiation. I keep only the search related to case-splits due to coercions and overloads.

3- I use the metavariable environment captured at step 1 when pretty printing the justification of an elaborator_exception.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-03 17:18:23 -08:00
Leonardo de Moura
9620b00e24 feat(kernel/metavar): is instantiate_metavars, we are also instantiating assigned metavariables that occur in the local context of unassinged ones. 
This modification improves the effectiveness of the process_metavar_inst procedure in the Lean elaborator.

For example, suppose we have the constraint

   ctx |- ?M1[inst:0 ?M2] == a

If ?M1 and ?M2 are unassigned, then we have to consider the two possible solutions:

        ?M1 == a
    or
        ?M1 == #0 and ?M2 == a

On the other hand, if ?M2 is assigned to b, then we can ignore the second case.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-02 16:08:38 -08:00
Leonardo de Moura
cbd1f98365 fix(library/elaborator): bug at method process_metavar_inst, add new test that exposed the bug 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-01 03:02:41 -08:00
Leonardo de Moura
b83b17d3ab fix(kernel/metavar): bug at cached_metavar_env::update method 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-23 15:41:02 -08:00
Leonardo de Moura
7b0b363b32 fix(kernel/normalizer): metavariable reification 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-21 06:40:26 -08:00
Leonardo de Moura
84bfe2a222 fix(library/elaborator): bug in process_meta_app 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-17 10:56:20 -08:00
Leonardo de Moura
4357c9196e feat(kernel/metavar): make sure that a metavariable 'm' can only be assigned to a term that contains free variables available in the context associated with 'm' 
This commit also simplifies the method check_pi in the type_checker and type_inferer.
It also fixes process_meta_app in the elaborator.
The problem was in the method process_meta_app and process_meta_inst.
They were processing convertability constrains as equality constraints.
For example, process_meta_app would handle

    ctx |- Type << ?f b

as

    ctx |- Type =:= ?f b

This is not correct because a ?f that returns (Type U) for b satisfies the first but not the second.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-14 12:25:00 -08:00
Leonardo de Moura
51aee83b70 refactor(kernel/metavar_env): use the same approach used in the class environment in the class metavar_env 
This modification was motivated by a bug exposed by tst17 at tests/kernel/type_checker.
metavar_env is now a smart point to metavar_env_cell.
ro_metavar_env is a read-only smart pointer. It is useful to make sure we are using proof_state correctly.

example showing that the approach for caching metavar_env is broken in the type_checker

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-13 18:59:15 -08:00
Leonardo de Moura
ae52c8062e chore(kernel/metavar): remove unused function 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-12 17:39:14 -08:00
Leonardo de Moura
450d6a4b1e refactor(util/splay_tree): replace find with splay_find 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-12 17:27:30 -08:00
Leonardo de Moura
1852c86948 feat(kernel): improve instantiate and lift_free_vars (use metavar_env to minimize the number of lift and inst local_entries needed) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-12 16:48:33 -08:00
Leonardo de Moura
38a25a1bd2 feat(kernel/metavar): (re-)enable add_lift simplification 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-12 16:48:33 -08:00
Leonardo de Moura
4de5f06a97 fix(library/elaborator): bug in process_metavar_inst, and disable simplification that is negatively impacting the elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-10 19:26:58 -08:00
Leonardo de Moura
2f88d6710c feat(kernel/expr): add some_expr and none_expr for building values of type optional<expr> 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-08 10:34:38 -08:00
Leonardo de Moura
3e1fd06903 refactor(kernel/expr): remove 'null' expression, and operator bool for expression 
After this commit, a value of type 'expr' cannot be a reference to nullptr.
This commit also fixes several bugs due to the use of 'null' expressions.

TODO: do the same for kernel objects, sexprs, etc.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-07 23:21:10 -08:00