Leonardo de Moura
64cce595a5
feat(lua): add splay_maps to the Lua API
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-14 13:35:36 -08:00
Leonardo de Moura
9e445d1917
feat(lua): interrupt and sleep Lua APIs
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-14 10:04:32 -08:00
Leonardo de Moura
691893258d
feat(kernel/expr): add hash code based on allocation time
...
The new hash code has the property that given expr_cell * c1 and expr_cell * c2,
if c1 != c2 then there is a high propbability that c1->hash_alloc() != c2->hash_alloc().
The structural hash code hash() does not have this property because we may have
c1 != c2, but c1 and c2 are structurally equal.
The new hash code is only compatible with pointer equality.
By compatible we mean, if c1 == c2, then c1->hash_alloc() == c2->hash_alloc().
This property is obvious because hash_alloc() does not have side-effects.
The test tests/lua/big.lua exposes the problem fixed by this commit.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-14 02:43:11 -08:00
Leonardo de Moura
ae7ea99b56
fix(lua): copy_values and add tests
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-13 21:31:27 -08:00
Leonardo de Moura
c759fc93f7
test(lua): object Lua API
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-13 20:59:28 -08:00
Leonardo de Moura
351ef867d2
feat(lua): add abstract, instantiate, has_free_vars, lift/lower free_vars to Lua API
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-13 17:02:49 -08:00
Leonardo de Moura
ed3cf8152b
feat(lua): add for_each to expr Lua API
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-13 16:30:59 -08:00
Leonardo de Moura
3dea7ae0d6
test(frontends/lean): example mixing Lean and Lua
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-13 16:07:15 -08:00
Leonardo de Moura
1bf6051866
test(lua): expr LUA API test
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-13 15:29:31 -08:00
Leonardo de Moura
9a22702383
feat(lua): make objects() and localobjects() methods return iterators in the environment LUA API
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-13 14:26:01 -08:00
Leonardo de Moura
8c52d47692
chore(lua): rename env() to get_env()
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-13 13:58:51 -08:00
Leonardo de Moura
a80adae1c3
feat(lua): add fields method to sexpr Lua API
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-13 12:10:24 -08:00
Leonardo de Moura
450128e28b
refactor(lua): cleanup Lua bindings, and add accessor/tester to expr Lua API
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-13 11:46:09 -08:00
Leonardo de Moura
be093ecf90
feat(lua): use formatter available in the state object to convert Lean objects into strings in the Lua API
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-12 16:56:30 -08:00
Leonardo de Moura
9a5f86fce6
feat(lua): use (** ... **) instead of {{ ... }} for nested Lua scripts
...
The token }} is a bad delimiter for blocks of Lua script code nested in Lean files.
The problem is that the sequence }} occurs very often in Lua code because Lua uses { and } to build tables/lists/arrays.
Here is an example of Lua code that contains the sequence }}
t = {{1, 2}, {2, 3}, {3, 4}}
In Lean, (* ... *) is used to create comments. Thus, (** ... **) code blocks will not affect
valid Lean files. It also looks reasonably good.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-12 16:05:49 -08:00
Leonardo de Moura
8190d4fed5
feat(lua): allow Lua scripts to update 'global' options
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-12 15:38:00 -08:00
Leonardo de Moura
b986af09ed
feat(lua): add support for copying closures between Lua states
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-12 12:54:34 -08:00
Leonardo de Moura
2af2a69fc6
feat(lua): expose kernel objects in the Lua API
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-12 09:40:29 -08:00
Leonardo de Moura
d257156b88
fix(lua): memory leaks, we should not use luaL_error because it does not unwind C++ stack
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-11 21:45:13 -08:00
Leonardo de Moura
a30e02d862
fix(lua): redefine Lua 'print' function, and make sure it is thread safe
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-11 21:15:21 -08:00
Leonardo de Moura
eb9d0f0552
test(lua): add example showing how to access/update an environment object using multiple threads
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-11 20:53:23 -08:00
Leonardo de Moura
0af8f17834
feat(lua): allow Booleans to be copied between Lua states
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-11 20:39:46 -08:00
Leonardo de Moura
2ac594a159
test(lua): add a new example showing how to create nested State objects and threads
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-11 18:27:09 -08:00
Leonardo de Moura
69b41eae70
feat(lua): add support for multiple execution threads in the Lua API
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-11 16:25:17 -08:00
Leonardo de Moura
95785c7aaa
feat(lua): add State objects, it allows us to create several Lua State objects in a lua script
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-11 15:05:50 -08:00
Leonardo de Moura
bdc23fba32
test(lua): add tests for expr object
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-11 13:11:31 -08:00
Leonardo de Moura
b227775a07
test(lua): add tests for format object
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-11 12:58:47 -08:00
Leonardo de Moura
c2db18a003
test(lua): add tests for sexpr object
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-11 09:51:07 -08:00
Leonardo de Moura
6c7be28807
test(lua): add tests for options object
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-11 09:42:50 -08:00
Leonardo de Moura
8c140ff86f
feat(lua): allow lua scripts (embedded in Lean files) to access the environment
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-10 11:14:04 -08:00
Leonardo de Moura
3078923ea4
fix(kernel/type_checker): add missing test, and kernel_exception has_no_type_exception
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-10 11:14:04 -08:00
Leonardo de Moura
9d61fcf85b
feat(lua): expose environment objects in the Lua bindings
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-10 11:14:04 -08:00
Leonardo de Moura
8dd62e76be
feat(lua): add mk_metavar to Lua API
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-10 11:14:04 -08:00
Leonardo de Moura
554defe89d
feat(lua): expose local_context objects in the Lua bindings
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-09 12:18:46 -08:00
Leonardo de Moura
ad2de3b53c
feat(lua): expose level objects in the Lua bindings
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-08 17:08:24 -08:00
Leonardo de Moura
5a97f730af
feat(lua): add Type function
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-08 15:52:58 -08:00
Leonardo de Moura
32605d8266
feat(lua): expose level objects in the Lua bindings
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-08 15:38:00 -08:00
Leonardo de Moura
cc17be1ef1
feat(lua): add is_* predicates
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-08 12:40:28 -08:00
Leonardo de Moura
5c35a9ad0a
feat(lua): add Consts function
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-08 12:09:46 -08:00
Leonardo de Moura
b57ad80d5e
feat(lua): expose basic API for Lean expressions in the Lua bindings
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-07 21:54:57 -08:00
Leonardo de Moura
9000c7c2fa
feat(lua): expose format objects in the Lua bindings
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-07 21:54:42 -08:00
Leonardo de Moura
57b9657bf0
feat(lua): add lua_exception for wrapping lua errors, and improve Lua error messages in the Lean frontend
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-07 15:19:26 -08:00
Leonardo de Moura
a9b2be0b9c
feat(frontends/lean): add support for embedded Lua scripts in Lean files
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-07 13:56:04 -08:00
Leonardo de Moura
9c60eed93c
refactor(kernel/metavar): avoid using unique names for default metavariable prefix
...
The problem is that unique names depend on the order compilation units are initialized. The order of initialization is not specified by the C++ standard. Then, different compilers (or even the same compiler) may produce different initialization orders, and consequently the metavariable prefix is going to be different for different builds. This is not a bug, but it makes unit tests to fail since the output produced by different builds is different for the same input file.
Avoiding unique name feature in the default metavariable prefix avoids this problem.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-07 10:16:25 -08:00
Leonardo de Moura
76150620c3
test(lua): use assertions
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-05 13:21:01 -08:00
Leonardo de Moura
ba3faea586
test(lua): add test driver for Lua binding tests
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-05 13:11:34 -08:00
Leonardo de Moura
0cc475e581
fix(lua/sexpr): make sexpr bindings robust
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-05 13:03:32 -08:00
Leonardo de Moura
56344c0541
test(lua): add more s-exprs Lua tests
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-04 21:31:29 -08:00
Leonardo de Moura
f13a97397f
feat(lua): expose s-expressions in the Lua bindings
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-04 19:58:32 -08:00
Leonardo de Moura
3c475e890d
refactor(lua/options): improve options bindings for Lua
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-04 18:46:58 -08:00
Leonardo de Moura
7b77863507
refactor(lua/name): improve name bindings for Lua
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-04 18:44:20 -08:00
Leonardo de Moura
9884c056ce
feat(lua): allow Lean to be compiled with Lua 5.1 and LuaJit
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-03 12:40:44 -08:00
Leonardo de Moura
e2da8c1f4d
feat(lua/numerics): expose mpz and mpq numbers in the Lua bindings
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-03 12:05:54 -08:00
Leonardo de Moura
dbf2d56c77
feat(lua/name): expose hierarchical names in the Lua bindings
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-02 20:49:42 -07:00
Leonardo de Moura
bf998d8661
feat(frontends/lean/parser): allow 'typeless' definitions, the type is inferred by the system
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-01 08:51:49 -07:00
Leonardo de Moura
96dcd003c6
fix(frontends/lean/parser): associated position with 'type' placeholder
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-31 16:27:36 -07:00
Leonardo de Moura
aa99ac6618
feat(kernel/value): allow semantic attachments to use coercions when being pretty printed
...
For example, this feature is useful when displaying the integer value 10 with coercions enabled. In this case, we want to display "nat_to_int 10" instead of "10".
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-30 11:42:26 -07:00
Leonardo de Moura
032f5cd7b3
feat(frontends/lean): make the 'expression template' argument in Subst implicit because higher-order matching can infer it.
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-30 10:45:43 -07:00
Leonardo de Moura
bc92671ae4
fix(frontends/lean/notation): adjust the implicit arguments of TransExt, and add new test
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 17:12:50 -07:00
Leonardo de Moura
e3228b1f5c
test(frontends/lean): add 'l = nil' test
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 16:30:03 -07:00
Leonardo de Moura
4dd6cead83
refactor(equality): make homogeneous equality the default equality
...
It was not a good idea to use heterogeneous equality as the default equality in Lean.
It creates the following problems.
- Heterogeneous equality does not propagate constraints in the elaborator.
For example, suppose that l has type (List Int), then the expression
l = nil
will not propagate the type (List Int) to nil.
- It is easy to write false. For example, suppose x has type Real, and the user
writes x = 0. This is equivalent to false, since 0 has type Nat. The elaborator cannot introduce
the coercion since x = 0 is a type correct expression.
Homogeneous equality does not suffer from the problems above.
We keep heterogeneous equality because it is useful for generating proof terms.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 16:20:06 -07:00
Leonardo de Moura
d0009d0242
feat(frontends/lean): make the first argument of if-expression implicit, add support for marking implicit arguments on builtin symbols (aka semantic attachments)
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 15:53:50 -07:00
Leonardo de Moura
2d88922543
feat(frontends/lean/elaborator): solve easy overloads at preprocessing time
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 10:07:15 -07:00
Leonardo de Moura
7c8daf8974
fix(kernel/metavar): make sure the justification and substitution are always matching each other
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 02:39:52 -07:00
Leonardo de Moura
2c6d4d2225
fix(kernel/normalizer): do not apply substitutions in the normalizer
...
It is incorrect to apply substitutions during normalization.
The problem is that we do not have support for tracking justifications in the normalizer. So, substitutions were being silently applied during normalization. Thus, the correctness of the conflict resolution in the elaboration was being affected.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 02:14:48 -07:00
Leonardo de Moura
dbefc91151
fix(kernel/metavar): add normalize assignment justification
...
We need that when we normalize the assignment in a metavariable environment.
That is, we replace metavariable in a substitution with other assignments.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 11:02:34 -07:00
Leonardo de Moura
cb06d0a959
test(frontends/lean): add example showing higher order matching is working, and is useful
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-24 20:18:48 -07:00
Leonardo de Moura
02c22e509d
fix(tests/lean): remove obsolete comments
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-24 20:16:02 -07:00
Leonardo de Moura
250cf70410
test(frontends/lean): all 'bad' examples can be solved
...
Move them to the main test directory
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-24 20:12:58 -07:00
Leonardo de Moura
c1c1af4b98
fix(tests/lean): add parenthesis
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-24 20:04:50 -07:00
Leonardo de Moura
a5c3829d1b
feat(kernel): add unexpected_metavar_occurrence exception
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-24 19:56:44 -07:00
Leonardo de Moura
46b9b2114a
fix(tests/lean): adjust error messages in the expected output
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-24 19:27:26 -07:00
Leonardo de Moura
e55fb4f165
fix(tests/lean): adjust expected results, the new result is also acceptable
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-24 17:54:09 -07:00
Leonardo de Moura
d2f9c24d3c
fix(tests/lean): adjust tests
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-24 15:42:17 -07:00
Leonardo de Moura
a7f94b55db
fix(frontends/lean/elaborator): fix bugs and adjust tests
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-24 15:29:56 -07:00
Leonardo de Moura
29ad71f9fc
test(conversion): add more conversion tests
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-15 15:35:08 -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
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
Leonardo de Moura
4c67721d32
Fix test error on Cygwin
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-09 18:35:11 -07:00
Leonardo de Moura
d912c9cd09
Add more 'bad' examples
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-09 09:19:49 -07:00
Leonardo de Moura
0a08494f4d
Add another bad example for current elaborator
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-08 23:21:43 -07:00
Leonardo de Moura
2ca30571b4
Display the input term in the output of the Check command. It is useful to see the fully elaborated term.
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-08 22:55:21 -07:00
Leonardo de Moura
59a589037e
Keep expanded form when pretty printings variable declarations with implicit marks (i.e., curly braces)
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-08 11:23:46 -07:00
Leonardo de Moura
df116f88e0
Improve pretty printer for Pi's
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-08 11:04:07 -07:00
Leonardo de Moura
6bb9fc859e
Add examples that demonstrate limitations of the current elaborator. The new design, we are working on, will be able to solve them.
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-07 19:40:40 -07:00
Leonardo de Moura
b92bbeb83b
Add casting propagation and normalization
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-06 20:45:26 -07:00
Leonardo de Moura
c0c2f52087
Add Cast, DomInj and RanInj. Improve operator << for lean_frontend objects.
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-06 18:32:15 -07:00
Leonardo de Moura
b62816cc25
Fix problem with pretty printer. Add another test for elaborator
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-06 18:01:11 -07:00
Leonardo de Moura
edafd519e1
Add missing case to elaborator
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-06 17:43:08 -07:00
Leonardo de Moura
26bf7bcaac
Fix bug in the elaborator. Move character ' to class A
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-06 17:12:35 -07:00
Leonardo de Moura
8840b37258
Fix type checker and elaborator for let expressions. Fix get_coercions (we need to pass the context). Fix pretty printer for def_type_mismatch_exception.
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-06 11:02:00 -07:00
Leonardo de Moura
2459c4ae7c
Add (optional) type to let declarations
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-06 10:06:26 -07:00
Leonardo de Moura
6da194334e
Move 'slow' test files to different subdir. Modify CTestCustom.cmake.in to run leantests.
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-06 08:48:12 -07:00
Leonardo de Moura
6f3b0c30fb
Add 'Variables' command.
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-06 08:48:12 -07:00
Leonardo de Moura
3dc55c452c
Parse decimal values
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-06 08:48:12 -07:00
Leonardo de Moura
87d3961158
Improve elaborator error messages
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-04 16:36:58 -07:00
Leonardo de Moura
613d83cdf4
Improve application type mismatch errors. We also show the implicit arguments (not just their types)
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-04 16:36:58 -07:00
Leonardo de Moura
be7fa0932a
Add unicode name for the types: Nat, Int and Real
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-04 09:03:41 -07:00
Leonardo de Moura
e955c054ca
Modify type checker. Now, it only accepts builtin values that have been declared in the environment. The idea is to be able to track which classes of builtin values have been used in a given environment. We want to be able to quantify the size of the trusted code base for a particular development.
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-04 08:30:04 -07:00
Leonardo de Moura
fc9e395818
Define absolute value function and notation for it. Add new example.
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-03 20:39:54 -07:00