Leonardo de Moura
c77464703f
feat(frontends/lean): macro definition using Lua
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-19 19:08:10 -08:00
Leonardo de Moura
b08c606696
fix(library/io_state): bug in the io_state Lua bindings
...
This commit also includes a new test that exposes the problem.
The options in the io_state object were being lost.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-19 16:39:42 -08:00
Leonardo de Moura
2648f41eaa
test(tests/lean): add new test script that checks if Lean can parse the output produced by its pretty printer
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-19 16:16:56 -08:00
Leonardo de Moura
d9e692f506
feat(frontends/lean): improve coercion manangement
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-19 15:45:46 -08:00
Leonardo de Moura
f43db96e1f
fix(frontends/lean/pp): pretty printer for Type
...
Add parenthesis around Type when it has a universe.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-19 15:24:45 -08:00
Leonardo de Moura
ae01d3818d
fix(frontends/lean/parser): parse_type method
...
The parser had a nasty ambiguity. For example,
f Type 1
had two possible interpretations
(f (Type) (1))
or
(f (Type 1))
To fix this issue, whenever we want to specify a particular universe, we have to precede 'Type' with a parenthesis.
Examples:
(Type 1)
(Type U)
(Type M + 1)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-19 15:24:34 -08:00
Leonardo de Moura
46627289b8
fix(kernel/expr): avoid '_' as a binder name, we use '_' as a placeholder in the Lean frontend
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-19 14:47:53 -08:00
Leonardo de Moura
6cc83dbe2a
fix(kernel/kernel_exception): incorrect pp method
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-19 14:46:22 -08:00
Leonardo de Moura
d3d24696f4
feat(frontends/lean): hide builtin object in the 'Show Environment' command
...
The user can still display builtin objects by using
Show Environment all
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-19 14:00:58 -08:00
Leonardo de Moura
ad3f771b1d
feat(frontends/lean): hide 'explicit' version of objects with implicit arguments
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-19 13:12:39 -08:00
Leonardo de Moura
bff5a6bfb2
fix(frontends/lean/pp): make sure pp and parser are using the same precedences
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-19 12:46:14 -08:00
Leonardo de Moura
02bd166793
chore(library/basic_thms): fix typo in comment
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-19 12:22:05 -08:00
Leonardo de Moura
dd72269b13
feat(frontends/lean): rename command Set to SetOption
...
It is not nice to have Set as a reserved keyword. See example examples/lean/set.lean
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-18 21:18:48 -08:00
Leonardo de Moura
d7886c4f5f
doc(examples/lean): new example
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-18 21:03:16 -08:00
Leonardo de Moura
8cfe5cf9ed
fix(frontends/lean/pp): pretty printer was ignoring notation decls in the local scope
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-18 18:00:37 -08:00
Leonardo de Moura
79fa6e4940
feat(frontends/lean): Scopes in the default Lean frontend
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-18 17:40:21 -08:00
Leonardo de Moura
97b872a05c
refactor(frontends/lean): remove frontend class, it is not needed anymore
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-18 14:37:55 -08:00
Leonardo de Moura
2aaa9a5273
feat(frontends/lean/parser): change function application precedence
...
Now, we can write
Pi (x y : A), R x y -> R y x
instead of
Pi (x y : A), (R x y) -> (R y x)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-18 12:44:15 -08:00
Leonardo de Moura
47c7bb1bde
refactor(*): uses aliases for unordered_map and unordered_set
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-18 12:30:45 -08:00
Leonardo de Moura
1e4fa76a47
feat(util/name_map): add template alias
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-18 11:34:40 -08:00
Leonardo de Moura
7b2fea3fab
fix(kernel/normalizer): compilation problem with clang++
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-18 08:46:36 -08:00
Leonardo de Moura
418623b874
feat(kernel/replace_fn): add template replace that captures commonly used pattern
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-17 18:31:59 -08:00
Leonardo de Moura
23e518001a
feat(kernel/normalizer): avoid unnecessary creation of closures for n-ary functions
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-17 18:10:13 -08:00
Leonardo de Moura
10f28c7bec
feat(kernel/replace_fn): non-recursive replace_fn
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-17 16:35:39 -08:00
Leonardo de Moura
af4a6c9364
fix(kernel/normalizer): cache problems
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-17 14:52:14 -08:00
Leonardo de Moura
33789fad4c
fix(kernel/builtin): make sure the if-then-else semantic attachment is not a simplifier
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-17 14:34:40 -08:00
Leonardo de Moura
c53233ea26
fix(kernel/normalizer): avoid svalue hack, use 'semantic attachments' for implementing closures, include context in the closure
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-17 14:33:42 -08:00
Leonardo de Moura
836357c65c
fix(kernel/normalizer): bug in Let normalization
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-17 12:35:25 -08:00
Leonardo de Moura
84bfe2a222
fix(library/elaborator): bug in process_meta_app
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-17 10:56:20 -08:00
Leonardo de Moura
09b51a0fb7
fix(library/elaborator): missing condition
...
The elaborator was missing solutions because of the missing condition at is_simple_ho_match.
This commit also adds a new test that exposes the problem.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-16 17:13:36 -08:00
Leonardo de Moura
f09fd0fc04
feat(kernel/printer): include de Bruijn index in the debug printer
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-16 16:56:46 -08:00
Leonardo de Moura
91f4ced83b
feat(library/elaborator): do not create trivial constraints of the form 'ctx |- t =:= t'
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-16 16:41:20 -08:00
Leonardo de Moura
7792561b20
fix(library/type_inferer): another incorrect use of scoped_map
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-16 15:17:19 -08:00
Leonardo de Moura
af42078205
fix(kernel): incorrect use of scoped_map
...
This commit also adds a new test that exposes the problem.
The scoped_map should not be used for caching values in the normalizer and type_checker. When we extend the context, the meaning of all variables is modified (we are essentially performing a lift). So, the values stored in the cache are not correct in the new context.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-16 15:11:39 -08:00
Leonardo de Moura
2fee2def72
feat(library/basic_thms): simplify DoubleNegElim
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-16 13:19:19 -08:00
Leonardo de Moura
de53e92de8
feat(library/basic_thms): add ExistsElim theorem
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-16 12:43:34 -08:00
Leonardo de Moura
8f5c2b7d9f
feat(library/basic_thms): add Refute theorem
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-16 12:03:31 -08:00
Leonardo de Moura
8f9405c8b3
fix(library/elaborator): tag meta_app constraints of the form 'ctx |- m?[inst:i v] t1 =:= t2' as expensive
...
This commits also adds a new unit test that demonstrates non-termination due to this kind of constraint.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-16 09:39:02 -08:00
Leonardo de Moura
61bd27ff06
fix(library/elaborator): bug in simple_ho_match
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-15 21:48:55 -08:00
Leonardo de Moura
19ad39159e
feat(library/basic_thms): add ForallIntro theorem
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-15 17:35:31 -08:00
Leonardo de Moura
82dfb553d5
feat(library/basic_thms): add ExistsIntro theorem
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-15 16:26:23 -08:00
Leonardo de Moura
2253d8079b
chore(util/pdeque): remove unused template
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-14 23:31:44 -08:00
Leonardo de Moura
993bea8206
refactor(library/elaborator): improve elaborator state data-structure
...
The "quota" hack used before this commit was inefficient, and too hackish.
This commit uses two lists of constraints: active and delayed.
The delayed constraints are only processed when there are no active constraints.
We use a simple index to quickly find which delayed constraints have assigned metavariables.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
checkpoint
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-14 23:27:08 -08:00
Leonardo de Moura
5aa9264091
feat(util/list): add remove_last template
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-14 23:08:10 -08:00
Leonardo de Moura
1b1032eb99
feat(util/list): improved filter that reuses list cells
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-14 20:15:37 -08:00
Leonardo de Moura
bdbf85405a
feat(library/elaborator): add extra occurs-check test
...
The idea is to catch the inconsistency in constraints such as:
ctx |- ?m[inst:0 v] == fun x, ?m a x
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-14 19:47:33 -08:00
Leonardo de Moura
160a8379ef
feat(library/elaborator): provide the metavar_env to instantiate and lift_free_vars in the elaborator, it will minimize the number of local_entries needed
...
The modifications started at commit 1852c86948
made a big difference. For example, before these changes test tests/lean/implicit7.lean generated complicated constraints such as:
[x : Type; a : ?M::29[inst:1 ?M::0[lift:0:1]] x] ⊢ Pi B : Type, (Pi _ : x, (Pi _ : (?M::35[inst:0 #0 , inst:1 #2 , inst:2 #4 , inst:3 #6 , inst:5 #5 , inst:6 #7 , inst:7 #9 , inst:9 #9 , inst:10 #11 , inst:13 ?M::0[lift:0:13]] x a B _), (?M::36[inst:1 #1 , inst:2 #3 , inst:3 #5 , inst:4 #7 , inst:6 #6 , inst:7 #8 , inst:8 #10 , inst:10 #10 , inst:11 #12 , inst:14 ?M::0[lift:0:14]] x a B _ _))) ≈
?M::22 x a
After the changes, only very simple constraints are generated. The most complicated one is:
[] ⊢ Pi a : ?M::0, (Pi B : Type, (Pi _ : ?M::0, (Pi _ : B, ?M::0))) ≈ Pi x : ?M::17, ?M::18
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-14 15:59:35 -08:00
Leonardo de Moura
70b7e519f8
feat(library/type_inferer): provide the metavar_env to instantiate and lift_free_vars in the type_inferer, it will minimize the number of local_entries needed
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-14 15:54:49 -08:00
Leonardo de Moura
02ee31b786
feat(kernel/normalizer): provide the metavar_env to instantiate and add_inst in the normalizer, it will minimize the number of local_entries needed
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-14 15:41:50 -08:00
Leonardo de Moura
3d30664611
feat(kernel/type_checker): provide the metavar_env to instantiate, it will minimize the number of local_entries needed
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-14 15:13:56 -08:00