Leonardo de Moura
|
1647e44510
|
Fix memory corruption bug
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-22 18:53:58 -07:00 |
|
Leonardo de Moura
|
16a6a54df1
|
Fix abuse of operator-> overload
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-22 16:41:51 -07:00 |
|
Soonho Kong
|
ab6ca82e6f
|
Update to suppress unused-parameter warnings
|
2013-09-19 22:40:34 -07:00 |
|
Leonardo de Moura
|
2f29ff70d7
|
Implement higher-order unification
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-18 20:46:00 -07:00 |
|
Leonardo de Moura
|
3df6149daa
|
Add support for metavariables in the type checker.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-17 11:09:59 -07:00 |
|
Leonardo de Moura
|
30b19c314a
|
Add basic support for metavariables at is_convertible. Swap is_convertible arguments to make it more intuitive.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-17 07:15:47 -07:00 |
|
Leonardo de Moura
|
a26c7d47f2
|
Add simplification to add_lift
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-17 03:14:02 -07:00 |
|
Leonardo de Moura
|
99e8d2feae
|
Add simplification rule to add_inst
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-17 02:57:28 -07:00 |
|
Leonardo de Moura
|
da09e7217a
|
Cleanup meta_entry code
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-16 19:32:28 -07:00 |
|
Leonardo de Moura
|
99a163f11d
|
Simplify metavariable context. Now, we have only 'lift' and 'inst' instead of 'subst', 'lift' and 'lower'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-16 19:32:28 -07:00 |
|
Leonardo de Moura
|
cad562a448
|
Add support for metavariables in the normalizer.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-16 19:32:28 -07:00 |
|
Leonardo de Moura
|
2800292947
|
Add timestamp to metavar_env
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-15 19:50:48 -07:00 |
|
Leonardo de Moura
|
5a4bc331d2
|
Make unification_problems a virtual class. Associate a 'standard' context with each metavariable in metavar_env
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-15 19:38:36 -07:00 |
|
Leonardo de Moura
|
63e102055e
|
Move metavariables to the kernel. This is the first step for implementing the new elaborator.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-15 12:09:01 -07:00 |
|