Commit graph

1003 commits

Author SHA1 Message Date
Leonardo de Moura
032f5cd7b3 feat(frontends/lean): make the 'expression template' argument in Subst implicit because higher-order matching can infer it.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-30 10:45:43 -07:00
Leonardo de Moura
bc92671ae4 fix(frontends/lean/notation): adjust the implicit arguments of TransExt, and add new test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 17:12:50 -07:00
Leonardo de Moura
7fc87faa8f feat(kernel): heterogeneous transitivity axiom, we need this axiom to be able to generate modular proofs in the rewriting engine module
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 17:07:30 -07:00
Leonardo de Moura
a57ca284ec fix(tests/library/elaborator): replace eq with my_eq because eq is now a builtin symbol
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 17:06:32 -07:00
Leonardo de Moura
e3228b1f5c test(frontends/lean): add 'l = nil' test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 16:30:03 -07:00
Leonardo de Moura
4dd6cead83 refactor(equality): make homogeneous equality the default equality
It was not a good idea to use heterogeneous equality as the default equality in Lean.
It creates the following problems.

- Heterogeneous equality does not propagate constraints in the elaborator.
For example, suppose that l has type (List Int), then the expression
     l = nil
will not propagate the type (List Int) to nil.

- It is easy to write false. For example, suppose x has type Real, and the user
writes x = 0. This is equivalent to false, since 0 has type Nat. The elaborator cannot introduce
the coercion since x = 0 is a type correct expression.

Homogeneous equality does not suffer from the problems above.
We keep heterogeneous equality because it is useful for generating proof terms.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 16:20:06 -07:00
Leonardo de Moura
d0009d0242 feat(frontends/lean): make the first argument of if-expression implicit, add support for marking implicit arguments on builtin symbols (aka semantic attachments)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 15:53:50 -07:00
Leonardo de Moura
2d88922543 feat(frontends/lean/elaborator): solve easy overloads at preprocessing time
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 10:07:15 -07:00
Leonardo de Moura
577ca128a1 fix(library/elaborator): add missing conflict justification
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 03:01:17 -07:00
Leonardo de Moura
521fa1ddb8 style(kernel/metavar): add missing includes
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 03:00:43 -07:00
Leonardo de Moura
7c8daf8974 fix(kernel/metavar): make sure the justification and substitution are always matching each other
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 02:39:52 -07:00
Leonardo de Moura
2c6d4d2225 fix(kernel/normalizer): do not apply substitutions in the normalizer
It is incorrect to apply substitutions during normalization.
The problem is that we do not have support for tracking justifications in the normalizer. So, substitutions were being silently applied during normalization. Thus, the correctness of the conflict resolution in the elaboration was being affected.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 02:14:48 -07:00
Soonho Kong
7944db2f18 doc(coding_style): add how to organize template source code
[skip ci]
2013-10-28 11:31:46 -04:00
Leonardo de Moura
5f11392fcc test(numerics/numeric_traits): add missing test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-28 07:50:33 -07:00
Leonardo de Moura
1d18f60dd5 fix(numerics): add missing numeric_traits<float>::zero()
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-28 07:47:23 -07:00
Leonardo de Moura
b16a64f44b fix(library/elaborator): missing normalization step for semantic attachments
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-28 07:42:14 -07:00
Leonardo de Moura
4564bfa1d3 feat(library/elaborator): improve simple_ho_match
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 11:17:03 -07:00
Leonardo de Moura
dbefc91151 fix(kernel/metavar): add normalize assignment justification
We need that when we normalize the assignment in a metavariable environment.
That is, we replace metavariable in a substitution with other assignments.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 11:02:34 -07:00
Leonardo de Moura
92f5a31976 feat(kernel/expr): add new mk_app template for creating applications using a collection
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 08:53:58 -07:00
Leonardo de Moura
eaccdcb558 refactor(assumption_justification): move to the kernel
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-26 14:21:29 -07:00
Leonardo de Moura
4bed9f85b0 feat(kernel/for_each): add option for disabling cache of atomic expressions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 15:25:17 -07:00
Leonardo de Moura
ce10bfeaf6 perf(kernel/metavar): improve performance of has_assigned_metavar by avoiding for_each+exception
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 15:19:59 -07:00
Leonardo de Moura
57d9d23bd4 feat(kernel/for_each): allow function F to interrupt for_each search
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 14:58:02 -07:00
Leonardo de Moura
2dd44bdf1a perf(kernel/for_each): delay initialization of visited set
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 14:52:08 -07:00
Leonardo de Moura
e765105ea5 fix(frontends/lean/pp): let expressions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 12:30:39 -07:00
Leonardo de Moura
c3c66b6c90 feat(make): add THREAD_SAFE build option
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 11:50:35 -07:00
Leonardo de Moura
c53d559f7f perf(library/elaborator): improve process_metavar
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 11:19:17 -07:00
Leonardo de Moura
471bbd4040 refactor(kernel/metavar): combine several splay_trees (at metavar_env) into a single one
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 11:02:19 -07:00
Leonardo de Moura
5e34f410b3 refactor(splay_map): modify splay_find signature
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 10:47:15 -07:00
Leonardo de Moura
5812dfcf44 perf(kernel/justification): remove cache from depends_on
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 10:26:05 -07:00
Leonardo de Moura
2b5c951de3 perf(name): add quick_cmp for hierarchical names
It first compare names using hash codes.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 09:58:06 -07:00
Leonardo de Moura
66f4834dbc perf(kernel/metavar): add quick test that catches many cases
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 09:24:01 -07:00
Leonardo de Moura
833c513840 doc(commit_convention): add new category
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 09:23:14 -07:00
Leonardo de Moura
f38178311c perf(kernel/expr_eq): delay hashtable initialization
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 09:21:47 -07:00
Leonardo de Moura
e0ca27bfb3 fix(tests/library/rewriter): warning
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 08:33:53 -07:00
Leonardo de Moura
412bc792c9 fix(style): missing include
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 08:10:28 -07:00
Leonardo de Moura
0c21f45292 fix(kernel/unification_constraint): memory leak
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 08:06:21 -07:00
Leonardo de Moura
7d602c1068 doc(todo): update todo
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-24 20:21:17 -07:00
Leonardo de Moura
cb06d0a959 test(frontends/lean): add example showing higher order matching is working, and is useful
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-24 20:18:48 -07:00
Leonardo de Moura
02c22e509d fix(tests/lean): remove obsolete comments
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-24 20:16:02 -07:00
Leonardo de Moura
250cf70410 test(frontends/lean): all 'bad' examples can be solved
Move them to the main test directory

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-24 20:12:58 -07:00
Leonardo de Moura
c1c1af4b98 fix(tests/lean): add parenthesis
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-24 20:04:50 -07:00
Leonardo de Moura
f0e149d77b fix(frontends/lean/pp): fix how Type expressions are pretty printed
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-24 20:02:34 -07:00
Leonardo de Moura
a5c3829d1b feat(kernel): add unexpected_metavar_occurrence exception
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-24 19:56:44 -07:00
Leonardo de Moura
83907d7c73 fix(elaborator): max constraints
elaborator was not handling max constraints where one of the arguments was a Bool. Example:
      ctx |- max(Bool, Type) == ?M

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-24 19:27:57 -07:00
Leonardo de Moura
46b9b2114a fix(tests/lean): adjust error messages in the expected output
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-24 19:27:26 -07:00
Leonardo de Moura
65a514ad8a fix(frontends/lean/parser): option propagation
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-24 19:04:06 -07:00
Leonardo de Moura
576b4e2169 fix(frontends/lean/pp): missing comma when printing contexts
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-24 19:00:24 -07:00
Leonardo de Moura
df07a84d11 feat(frontends/lean/parser): display elaborator error messages
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-24 18:48:53 -07:00
Leonardo de Moura
ca6a6d71e5 fix(kernel/printer): bug when printing let expression
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-24 18:05:23 -07:00