Leonardo de Moura
bbc265ded4
feat(frontends/lean): hook new elaborator in the default frontend
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-24 15:14:29 -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
f1e0d6ec29
refactor(beta_reduction): move beta reduction functions to the kernel, delete reduce.cpp file and tests
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-23 15:44:26 -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
8e1a75ce1c
feat(elaborator): only process upper bound constraints when the corresponding metavariable does not have lower bound and max constraints
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-23 13:09:13 -07:00
Leonardo de Moura
172567a2fb
feat(elaborator): add support for upper bounds, max constraints, and fix bugs
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-23 12:01:39 -07:00
Leonardo de Moura
019f64671b
fix(elaborator): add basic support for flex-flex pairs, add more tests, fix bug when enumerating different solutions
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 17:49:37 -07:00
Leonardo de Moura
7ad256131e
feat(elaborator): add support for constraints of the form ?m[inst, ...] == t, fix bugs, add more tests
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 16:39:22 -07:00
Leonardo de Moura
a5b4908f71
fix(elaborator): process_simple_ho_match and missing cases
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 13:45:04 -07:00
Leonardo de Moura
cb2c73cf37
feat(elaborator): add higher-order matching support to elaborator
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 11:22:00 -07:00
Leonardo de Moura
f4592da87f
feat(elaborator): solve more unification constraints, add more tests
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 08:15:37 -07:00
Leonardo de Moura
7f96c07a01
refactor(library): rename light_checker to type_inferer
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 08:15: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
dc0e7a4472
feat(pos_info_provider): add position information provider for expressions
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 08:15:36 -07:00
Leonardo de Moura
b1b49e86e7
test(elaborator): add simple test
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 08:15:36 -07:00
Leonardo de Moura
1548ffabb1
feat(elaborator): add new elaborator interface
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 08:15:36 -07:00
