Commit graph

2993 commits

Author SHA1 Message Date
Leonardo de Moura
2fa5b17592 feat(library/unifier): add unifier.max_steps unifier.use_exceptions options
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-23 12:38:57 -07:00
Leonardo de Moura
7b188ea37e feat(library/unifier): implement flex-rigid case
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-23 11:00:35 -07:00
Leonardo de Moura
68d55ef398 doc(library/unifier): document some of the unifier_fn methods
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-23 08:22:38 -07:00
Leonardo de Moura
9f7b92a410 refactor(library/unifier): combine active and delayed constraint sets
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-22 21:10:59 -07:00
Leonardo de Moura
4da9c2a2cb fix(emacs): modify emacs mode to reflect recent changes
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-22 17:56:53 -07:00
Leonardo de Moura
5bd86754af feat(frontends/lean/builtin_cmds): change notation for marking implicit/cast parameter in sections
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-22 17:51:00 -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
611f29a954 chore(library/elaborator): remove dead code
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-22 16:35:00 -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
b936c4d860 test(lua): add type checker test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-22 14:13:30 -07:00
Leonardo de Moura
238a0dbfba fix(library/unifier): memory violation, and missing set_conflict
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-22 14:09:06 -07:00
Leonardo de Moura
25cb1bf6a1 fix(kernel/converter): use type_checker::scope to make sure we restore the cache, and remove constraints when is_def_eq fails in the converter
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-22 14:08:54 -07:00
Leonardo de Moura
a1d94d71ec refactor(kernel/converter): eliminate converter::context, use type_checker directly
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-22 13:52:47 -07:00
Leonardo de Moura
edb2e85898 refactor(kernel/type_checker): remove type_checker::imp
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-22 13:39:58 -07:00
Leonardo de Moura
29a00c46d0 feat(library/unifier): add main loop and resolve_conflict
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-22 11:57:10 -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
1c47bd4847 fix(kernel/converter): remove temporary workaround, and temporarily disable unit test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-22 10:39:22 -07:00
Leonardo de Moura
73666af4a4 fix(library/register_module): missing open_unifier
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-22 10:01:51 -07:00
Leonardo de Moura
c7c5e41653 fix(frontends/lean/parser): warning when compiling in release mode
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-22 09:58:05 -07:00
Leonardo de Moura
3953d4d122 feat(kernel/type_checker): add push/pop methods to type_checker, they control the cache, and allow the type checker to reuse results even when it is used inside of a backtracking search
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-22 09:58:05 -07:00
Leonardo de Moura
eca22edda3 fix(kernel/type_checker): restore type checker cache when a failure occurs, do not send constraints to add_cnstr_fn when a type checker failure occurrs
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-22 09:00:32 -07:00
Leonardo de Moura
9c745057b4 feat(library/unifier): add unify_fn skeleton
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-21 20:08:39 -07:00
Leonardo de Moura
aac3830e31 fix(kernel/converter): add temporary fix, we need to be able to backtrack constraints
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-21 20:08:39 -07:00
Leonardo de Moura
f9a21166f0 feat(kernel/type_checker): add type_checker::is_def_eq method that takes a justification as argument
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-21 20:08:39 -07:00
Leonardo de Moura
fedbf8595b feat(kernel/metavar): collect unassigned metavariables while instantiating
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-21 16:58:09 -07:00
Leonardo de Moura
bf8f3318d8 feat(library): add unifier module skeleton
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-21 13:38:17 -07:00
Leonardo de Moura
37bee8c852 refactor(kernel/type_checker): simplify replace constraint_handler with closure
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-21 12:25:54 -07:00
Leonardo de Moura
86a56fbd2d feat(library/kernel_bindings): expose methods substitution::for_each_expr and substitution::for_each_level in the Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-21 12:25:54 -07:00
Leonardo de Moura
2c3e3cb544 refactor(kernel/abstract): add abstract_locals, and remove abstract_p
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-21 12:25:54 -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
9e50d5a1b8 test(util/lazy_list): add simple lazy_list example
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-21 12:25:54 -07:00
Leonardo de Moura
2589d60bfd feat(frontends/lean): add nameless 'have' expression
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-20 17:18:18 -07:00
Leonardo de Moura
4b227409bf feat(frontends/lean): add 'then have' expression
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-20 14:27:21 -07:00
Leonardo de Moura
4560413a92 feat(frontends/lean): add '[fact]' modifier for 'have' expression
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-20 11:58:05 -07:00
Leonardo de Moura
39177ec10a feat(frontends/lean): flip definition modifiers position, now they must occur after the identifier
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-20 11:58:05 -07:00
Leonardo de Moura
16412daf39 feat(frontends/lean): add 'using' syntax sugar for adding expressions to the goal's context
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-20 11:58:05 -07:00
Leonardo de Moura
5c17411a86 fix(kernel/converter): relax is_def_eq test, for example is_def_eq(f(?m1), a) should generate a constraint instead of returning an error
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-20 09:46:58 -07:00
Leonardo de Moura
2cc8172d61 refactor(frontends/lean): remove m_pos field from parameter object
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-19 23:06:49 -07:00
Leonardo de Moura
2954d10df5 refactor(kernel/converter): remove unnecessary exception
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-19 23:06:49 -07:00
Leonardo de Moura
05d1832425 refactor(kernel/type_checker): improve ensure_pi and ensure_sort APIs
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-19 22:33:58 -07:00
Leonardo de Moura
0cc8117fb4 fix(frontends/lean): add missing file
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-19 06:10:15 -07:00
Leonardo de Moura
bdab979e09 feat(frontends/lean): add inductive_cmd
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-18 16:00:59 -07:00
Leonardo de Moura
461689f758 refactor(frontends/lean/builtin_cmds): move declaration commands to new file
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-18 15:55:52 -07:00
Leonardo de Moura
3bb53810c5 test(lean/run): add notation test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-18 09:48:47 -07:00
Leonardo de Moura
08845be2fc feat(frontends/lean/notation_cmd): improve 'notation' cmd
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-18 09:28:01 -07:00
Leonardo de Moura
3e3c4ee5ed feat(frontends/lean/parser): add local_scope object to Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-18 08:38:23 -07:00
Leonardo de Moura
6259d20218 feat(frontends/lean/parser): expand Lua parser API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-18 08:03:17 -07:00
Leonardo de Moura
77c5319c4a chore(*): remove Lua 'migrate'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-18 07:01:34 -07:00
Leonardo de Moura
813e033f54 test(lean): add simple example of notation implemented using Lua
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-17 22:37:22 -07:00
Leonardo de Moura
3ea24c0f32 fix(library/kernel_bindings): set_environment and set_io_state objects
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-17 22:36:47 -07:00