Leonardo de Moura
faee08591f
fix(*): make sure elaborator and type_checker use the same "rules" for treating opaque definitions
...
This is a big change because we have to store in constraints whether we can use the "relaxed" rules or not.
The "relaxed" case says that when type checking the value of an opaque definition we can treat other opaque definitions in the same module as transparent.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-27 12:12:54 -07:00
Leonardo de Moura
b956ce68d2
feat(frontends/lean/elaborator): keep postponing delayed coercions until the type can be inferred
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-07 12:50:43 -07:00
Leonardo de Moura
d7cb1952ae
feat(kernel): simplify choice_fn, and make its interface closer to the unifier_plugin interface
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-04 12:47:33 -07:00
Leonardo de Moura
a0e4dccdac
refactor(kernel/constraint): rename choice constraint fields
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-23 13:52:03 -07:00
Leonardo de Moura
6d14de76f3
feat(kernel/constraint): add 'delayed' flag to choice constraints
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-23 12:56:06 -07:00
Leonardo de Moura
228f51dcfa
feat(library/unifier): add support for choice constraint
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-22 17:21:24 -07:00
Leonardo de Moura
c8a07dee53
feat(library/unifier): add unifier_plugin support, and unit test with plugin implemented using Lua
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-22 16:27:04 -07:00
Leonardo de Moura
644c387cfe
refactor(kernel/constraint): rename: level constraints are also equality constraints
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-22 10:50:47 -07:00
Leonardo de Moura
67088b130e
refactor(kernel/constraint): simplify constraint interface, and add choice constraint
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-21 12:25:54 -07:00
Leonardo de Moura
ab5f570924
refactor(kernel/constraint): remove choice constraints from the kernel, the kernel does not use them, we will implement them in elaborator
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-03 00:46:28 -07:00
Leonardo de Moura
9d96f24766
refactor(kernel): remove convertability constraints
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-09 20:25:27 -07:00
Leonardo de Moura
b83410f042
fix(library/kernel_bindings): g++ compilation error
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-02 14:34:56 -07:00
Leonardo de Moura
9f57ec059a
fix(kernel/constraint): missing inline directive
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-28 10:53:53 -07:00
Leonardo de Moura
25948ac534
refactor(kernel): cleanup interfaces
...
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
Leonardo de Moura
54801bbd05
refactor(kernel): constraints
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-03-18 10:27:57 -07:00
