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

159 commits

Author SHA1 Message Date
Leonardo de Moura
405e57eb2d refactor(kernel/formatter): add formatter_factory, and simplify formatter interface 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-10 18:32:00 +01:00
Leonardo de Moura
fc4df6a430 feat(kernel/expr): add O(1) predicates has_expr_metavar and has_univ_metavar 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-05 13:11:30 -07:00
Leonardo de Moura
a66a08c89e feat(frontends/lean): parse strings as expressions of type 'string.string' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-02 10:00:55 -07:00
Leonardo de Moura
4cb5f97038 refactor(library/tactic): simplify tactic framework, no more proof builders 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-01 16:11:19 -07:00
Leonardo de Moura
cb000eda13 refactor(kernel): store binder_infor in local constants 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-30 11:37:46 -07:00
Leonardo de Moura
0adacb5191 feat(kernel): add infer implicit, and use it to infer implicit arguments of inductive datatype eliminators, and tag whether parameters should be implicit or not in introduction rules in the module inductive_cmd 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-28 13:57:36 -07:00
Leonardo de Moura
acf8c13619 feat(kernel): add strict implicit arguments 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-25 17:50:49 -07:00
Leonardo de Moura
c9133f33dd feat(kernel/expr): add flat_app auxiliary function 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-25 12:51:22 -07:00
Leonardo de Moura
603dafbaf7 refactor(kernel): remove 'let'-expressions 
We simulate it in the following way:
1- An opaque 'let'-expressions (let x : t := v in b) is encoded as
      ((fun (x : t), b) v)
   We also use a macro (let-macro) to mark this pattern.
   Thus, the pretty-printer knows how to display it correctly.

2- Transparent 'let'-expressions are eagerly expanded by the parser.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-24 16:27:27 -07:00
Leonardo de Moura
4f3da90443 feat(frontends/lean/builtin_exprs): add 'have' and 'show' expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-16 15:04:29 -07:00
Leonardo de Moura
07f2379dec refactor(kernel): add mk_local function that has only two arguments 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-16 14:27:26 -07:00
Leonardo de Moura
2312f43443 fix(kernel/abstract): propagate tags when abstracting 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-16 13:00:13 -07:00
Leonardo de Moura
e7d7996fa9 feat(frontends/lean/parser): add parser_binder(s) and abstract methods 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-11 18:51:12 -07:00
Leonardo de Moura
4a25e7442a feat(kernel/expr): add optional expression caching (aka "partial" hash-consing) 
We do not enforce full hash-consing because we would need to synchronize
the access to the hashtable/cache.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-03 15:35:47 -07:00
Leonardo de Moura
2be9bcef78 feat(library/coercion): add coercion management implementation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-24 19:28:42 -07:00
Leonardo de Moura
2344fb9476 feat(kernel/expr): use the expression depth in the hash code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-23 14:16:51 -07:00
Leonardo de Moura
9de8249d8f feat(kernel): let Pi/Fun also take local constants 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-19 17:03:48 -07:00
Leonardo de Moura
edc8af7bb3 refactor(kernel): reduce code duplication 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-19 11:11:19 -07:00
Leonardo de Moura
7bf0011905 feat(kernel/expr): add additional template for mk_app 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-18 13:15:58 -07:00
Leonardo de Moura
5c7d3c79c4 feat(kernel/expr): improve get_app_args interface 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 19:19:10 -07:00
Leonardo de Moura
5ce134e24e chore(kernel): binder => binding where appropriate 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 11:37:27 -07:00
Leonardo de Moura
33ae79cd9e refactor(kernel): move shallow copy function to library 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 11:20:24 -07:00
Leonardo de Moura
aafdd98acb refactor(kernel): remove telescope type, and procedures 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 10:51:40 -07:00
Leonardo de Moura
e6c52d17a6 fix(kernel/expr): memory leak introduced today 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-16 16:21:31 -07:00
Leonardo de Moura
862c5e354d feat(kernel/expr): attach auxiliary name (for pretty printing) into local constants 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-16 13:08:09 -07:00
Leonardo de Moura
9a689ab0c3 feat(kernel): add telescope instantiate procedure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-16 11:56:20 -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
d6d72ba80e refactor(kernel): add binder structure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-16 10:51:54 -07:00
Leonardo de Moura
660b9299ad refactor(kernel): (de)serialization procedures don't need to be in the kernel 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-15 17:23:36 -07:00
Leonardo de Moura
3a19d9fee1 refactor(kernel): revise macro_definition API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-15 13:53:10 -07:00
Leonardo de Moura
606e6226c2 fix(kernel/type_checker): the type checker cache was not taking into account binder information 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-14 17:14:57 -07:00
Leonardo de Moura
5d61d23bf6 refactor(kernel): move mk_tele_pi to expr.h, and rename it mk_pi 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-14 16:24:55 -07:00
Leonardo de Moura
2e1a0bd50c feat(kernel/expr): add is_contextual binder info 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-14 14:54:27 -07:00
Leonardo de Moura
2593f65ce1 feat(kernel): add tag to kernel expressions 
Frontends can used tags to associate expressions with line number information.
The update_* procedures automatically propagate tags.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-12 16:33:25 -07:00
Leonardo de Moura
2424cf7ece fix(kernel/expr): old comment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-07 13:07:17 -07:00
Leonardo de Moura
65486b2dec refactor(kernel/expr): add macro_definition smart pointer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-01 18:05:46 -07:00
Leonardo de Moura
a5ae4b6570 feat(kernel): add binder annotations (implicit, cast) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-01 10:35:02 -07:00
Leonardo de Moura
e62254fbb3 fix(kernel/expr): relax macro_definition interface 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-28 14:02:48 -07:00
Leonardo de Moura
b2518f873d feat(kernel/type_checker): handle ensure_pi when whnf is a meta application 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-25 18:17:32 -07:00
Leonardo de Moura
63b6564b78 refactor(kernel): define extension_context API for normalizer_extesions and macro_definitions 
A particular macro definition may use the extra information to retrieve information necessary to expand/type a given macro application. Example: it may need to invoke whnf.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-25 15:43:17 -07:00
Leonardo de Moura
4842ae4fc7 refactor(kernel): store macro arguments in the macro_expr 
Before this commit, we "stored" macro arguments using applications.
This representation had some issues. Suppose we use [m a] to denote a macro
application. In the old representation, ([m a] b) and [m a b] would have
the same representation. Another problem is that some procedures (e.g., type inference)
would not have a clean implementation.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-25 15:02:56 -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
0d7902f9eb feat(kernel/type_checker): finish is_convertible predicate 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-23 20:16:14 -07:00
Leonardo de Moura
04a61bdffe feat(kernel/type_checker): remove dead code, add basic whnf procedure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-22 18:32:50 -07:00
Leonardo de Moura
9fda7e2529 fix(kernel): incorrect optimization in max_sharing_fn class 
The resultant expression may failed to be fully shared.
Add an example that demonstrates the problem.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-22 15:38:22 -07:00
Leonardo de Moura
dc864bf7b9 feat(kernel): store free variable range in composite expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-17 11:31:48 -07:00
Leonardo de Moura
bc8379256a refactor(kernel): remove pairs from kernel 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-17 10:52:07 -07:00
Leonardo de Moura
9b161b825f refactor(kernel): instantiate_params 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:57 -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
916301bdfb refactor(kernel): parametric kernel objects 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:57 -07:00