Commit graph

22 commits

Author SHA1 Message Date
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
434c33f225 feat(metavar): automatically apply beta-reduction when instantiating metavariable applications (i.e., expressions of the form (?m a)), when the metavariable is a lambda
This feature is useful for problems that require higher-order matching and/or unification.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-23 16:35:50 -07:00
Leonardo de Moura
13531b7d3e refactor(kernel): rename trace to justification
Motivations:

- We have been writing several comments of the form "... trace/justification..." and "this trace object justify ...".
- Avoid confusion with util/trace.h

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-23 13:42:17 -07:00
Leonardo de Moura
274b11530f feat(metavar): improve apply_local_context
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-23 11:59:36 -07:00
Leonardo de Moura
183f5a1ccf feat(elaborator): solve unification constraints
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 08:15:36 -07:00
Leonardo de Moura
a1710aeeb9 feat(elaborator): add trace objects for elaborator
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 08:15:36 -07:00
Leonardo de Moura
7cf83800c0 refactor(metavar): implement metavar_env, and use unification_constraint and trace objects in the type_checker, light_checker
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 08:15:36 -07:00
Leonardo de Moura
59914a36f3 refactor(metavar): reorganize and simplify metavariables
- Use hierarchical names instead of unsigned integers to identify metavariables.
- Associate type with metavariable.
- Replace metavar_env with substitution.
- Rename meta_ctx --> local_ctx
- Rename meta_entry --> local_entry
- Disable old elaborator
- Rename unification_problems to unification_constraints
- Add metavar_generator
- Fix metavar unit tests
- Modify type checker to use metavar_generator
- Fix placeholder module

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 08:15:36 -07:00
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