lean2

Author	SHA1	Message	Date
Leonardo de Moura	111949b9be	feat(frontends/lean): calculational proofs Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-02 10:53:14 -08:00
Leonardo de Moura	0cb741285c	chore(*): do not type check imported modules when running .cpp tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-02 07:11:55 -08:00
Leonardo de Moura	d7493ea86c	refactor(frontends/lean/parser): use std::function Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-02 06:53:34 -08:00
Leonardo de Moura	5540fc861a	refactor(frontends/lean/parser): break parser in smaller chunks Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-02 06:48:40 -08:00
Leonardo de Moura	7d18e9b32e	refactor(frontends/lean/parser): cleanup Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-02 04:37:21 -08:00
Leonardo de Moura	49425f1a5b	feat(builtin/Nat): multiplication axioms and theorems Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-01 21:32:07 -08:00
Leonardo de Moura	d72b165db4	feat(builtin/Nat): cleanup and add PlusAssoc Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-01 17:19:12 -08:00
Leonardo de Moura	aa009b6b05	feat(builtin/Nat): add basic axioms and theorems Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-01 15:53:53 -08:00
Leonardo de Moura	b2a8f4118d	feat(library/elaborator): process ho-match before normalizing Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-01 14:46:19 -08:00
Leonardo de Moura	7726ccad28	chore(builtin): rename nat, int and real modules to Nat, Int and Real. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-01 13:52:25 -08:00
Leonardo de Moura	43909ca66b	feat(frontends/lean/pp): pretty print SetOpaque command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-01 13:16:44 -08:00
Leonardo de Moura	770145a361	feat(builtin): use namespaces when defining nat, int and real. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-01 12:55:09 -08:00
Leonardo de Moura	d633622d90	feat(frontends/lean/parser): namespaces Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-01 12:28:18 -08:00
Leonardo de Moura	c423198a69	feat(builtin/kernel): add Not.*Elim theorems Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-01 11:35:21 -08:00
Leonardo de Moura	a8bc9fb4e0	refactor(builtin/kernel): mark exists as opaque after proving key theorems Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-01 11:00:32 -08:00
Leonardo de Moura	74cae2a154	refactor(library/elaborator): remove hackish rule After the recent fixes, the hack in process_metavar is not needed anymore. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-01 10:55:39 -08:00
Leonardo de Moura	5f29146e0b	feat(library/elaborator): use is_convertible for constraints without metavariables in the elaborator Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-01 03:14:01 -08:00
Leonardo de Moura	cbd1f98365	fix(library/elaborator): bug at method process_metavar_inst, add new test that exposed the bug Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-01 03:02:41 -08:00
Leonardo de Moura	0d815b8594	refactor(kernel/context): hide that the context is implemented using lists Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-31 19:43:50 -08:00
Leonardo de Moura	1cb7408c46	fix(kernel/normalizer): metavariable reification was incorrect, add tst11 at tests/kernel/normalizer.cpp to expose the bug Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-31 16:24:36 -08:00
Leonardo de Moura	cd3bbb1ebf	fix(kernel/builtin): enforcing design decision: semantic attachments are NOT simplifiers, they should do only evaluation Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-31 10:14:17 -08:00
Leonardo de Moura	c485b4bc4c	fix(kernel/environment): binary file reader, force the file to be read in binary mode We need this flag to be able to read the file on Windows. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-30 18:20:40 -08:00
Leonardo de Moura	1f6e959139	feat(deserializer): protect against corrupted binary files Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-30 18:05:38 -08:00
Leonardo de Moura	c473a484bb	feat(util/object_serializer): protect against corrupted files Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-30 17:58:20 -08:00
Leonardo de Moura	390a78a8d2	chore(frontends/lean/parser): remove 'Skipped' message Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-30 15:35:12 -08:00
Leonardo de Moura	909b10f515	fix(builtin): dependency Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-30 15:31:19 -08:00
Leonardo de Moura	931e196e83	fix(build): problem with reading LEAN_PATH on cygwin Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-30 15:12:31 -08:00
Leonardo de Moura	cc07c440e1	refactor(builtin): move pre-compiled object files to subdirectory Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-30 13:46:39 -08:00
Leonardo de Moura	49698bd053	chore(library/all): remove unnecessary files Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-30 13:37:25 -08:00
Leonardo de Moura	08718e33dc	refactor(builtin): only load the kernel and natural numbers by default Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-30 13:35:37 -08:00
Leonardo de Moura	a017801983	chore(builtin): cleanup dependencies Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-30 12:40:42 -08:00
Leonardo de Moura	a80fccea93	chore(*): cleanup builtin registration Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-30 12:19:00 -08:00
Leonardo de Moura	2a2f0b0d89	refactor(kernel/builtin): move helper decl macros to a separate file Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-30 11:51:30 -08:00
Leonardo de Moura	ecd62a1783	refactor(builtin/basic): rename basic.lean to kernel.lean Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-30 11:46:03 -08:00
Leonardo de Moura	4401b390fe	refactor(library/arith): do not load specialfn by default Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-30 11:25:43 -08:00
Leonardo de Moura	72761f14e4	refactor(library/io_state): move to the kernel Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-30 11:20:23 -08:00
Leonardo de Moura	46a8300a2d	refactor(library/arith): move real and special function declarations to .lean files Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-30 11:02:22 -08:00
Leonardo de Moura	c3bc6afb12	refactor(library/arith): move int and nat declarations to .lean files. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-30 10:32:14 -08:00
Leonardo de Moura	097b10e424	refactor(kernel/builtin): move builtin declarations to basic There is a lot to be done. We should do the same for Nat, Int and Real. We also should cleanup the file builtin.cpp and builtin.h. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 22:00:03 -08:00
Leonardo de Moura	37e8738a5f	refactor(kernel/expr): value deserializer Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 20:47:14 -08:00
Leonardo de Moura	9b7d596e6b	chore(builtin/basic): simplify UnfoldExists2 proof Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 20:33:31 -08:00
Leonardo de Moura	a7654cfdbe	chore(builtin/basic): remove unnecessary parentheses Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 20:16:01 -08:00
Leonardo de Moura	de77851a00	refactor(util/object_serializer): add methods write_core and read_core that allows to pack information in the byte used to indicate whether an object is already in the cache or not Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 19:59:53 -08:00
Leonardo de Moura	dbd122301a	feat(kernel/object): compact object serialization kind ids Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 19:19:24 -08:00
Leonardo de Moura	d0fdc3619b	feat(kernel/expr): compress application serialization Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 19:11:57 -08:00
Leonardo de Moura	63a4a2f288	feat(builtin/basic): add UnfoldExists and neq Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 18:30:41 -08:00
Leonardo de Moura	15621610e9	refactor(library/arith): replace Nat, Int, Real with simple variable decls instead of semantic attachments This commit also fixes bugs in the Alias command. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 17:04:36 -08:00
Leonardo de Moura	a1a5fb101d	feat(frontends/lean): add Alias command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 16:25:45 -08:00
Leonardo de Moura	14c3e11289	refactor(kernel/builtin): emove mk_bin_rop and mk_bin_lop to library Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 15:23:18 -08:00
Leonardo de Moura	92404c511c	refactor(kernel/builtin): Bool type does not need to be a semantic attachment Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 15:12:08 -08:00
Leonardo de Moura	8ff919ef2a	chore(build): remove dead dependency Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 14:49:22 -08:00
Leonardo de Moura	6633dff46f	fix(build): githash generation Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 14:41:28 -08:00
Leonardo de Moura	dfe46b9d25	refactor(kernel/builtin): move definition and axioms to basic.lean Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 14:01:30 -08:00
Leonardo de Moura	b1efdac07b	feat(frontends/lean/parser): universe declarations Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 13:15:09 -08:00
Leonardo de Moura	f8b82d854e	feat(builtin/basic): add TypeM alias Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 13:03:32 -08:00
Leonardo de Moura	1b300d3598	chore(kernel/builtin): remove unnecessary functions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 12:55:51 -08:00
Leonardo de Moura	f7889511f9	fix(build): cycle triggered by githash.h dependencies Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 12:47:25 -08:00
Leonardo de Moura	df3686634d	refactor(kernel/builtin): remove unnecessary predicates Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 12:20:29 -08:00
Leonardo de Moura	ac9801c7d7	feat(builtin): add support for cross-compilation Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 11:58:55 -08:00
Leonardo de Moura	5b7d254e52	feat(builtin): add pre-compiled .lean builtin files to repository Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 11:49:17 -08:00
Leonardo de Moura	ba592c845c	fix(builtin): dependencies Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 11:19:17 -08:00
Leonardo de Moura	9fdf2a3f55	feat(kernel): add trust_imported flag, it skips type checking of 'pre-compiled' Lean modules "Pre-compiled" .olean files were already type checked. The flag -t instructs to Lean to skip type checking when importing these files. TODO: add a check-sum. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 03:43:53 -08:00
Leonardo de Moura	411ebbc3c1	refactor(library/basic_thms): move the proof of all basic theorems to a .Lean file This commit also adds several new theorems that are useful for implementing the simplifier. TODO: perhaps we should remove the declarations at basic_thms.h? Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 03:04:49 -08:00
Leonardo de Moura	a05c815d31	chore(builtin): cleanup cmake file Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-28 22:27:36 -08:00
Leonardo de Moura	66178ae65a	refactor(extra): move extra to builtin Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-28 22:06:11 -08:00
Leonardo de Moura	5e0b344871	fix(kernel/object): uninitialized variable Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-28 21:57:56 -08:00
Leonardo de Moura	41c1010043	feat(frontends/lean/parser): make Import command use binary Lean files Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-28 19:20:04 -08:00
Leonardo de Moura	aee1c6d3f3	feat(kernel): export/import (.olean) binary files Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-28 17:31:35 -08:00
Leonardo de Moura	22bebbf242	feat(kernel/object): serializer for kernel objects Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-28 14:39:10 -08:00
Leonardo de Moura	1fd81dd3a1	feat(frontends/lean/parser): disable verbose messages when importing files Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-28 12:24:13 -08:00
Leonardo de Moura	44a31dd8fb	feat(frontends/lean/parser): improve Import command - The extension does not have to be provided. - It can also import Lua files. - Hierachical names can be used instead of strings. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-28 12:05:01 -08:00
Leonardo de Moura	755e8b735f	feat(kernel/expr): serializer for kernel expressions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-28 01:23:21 -08:00
Leonardo de Moura	0ef8ba2939	feat(kernel/level): serializer for level objects Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-27 23:30:13 -08:00
Leonardo de Moura	b94503ab20	chore(util/sexpr): remove unnecessary decls Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-27 23:24:31 -08:00
Leonardo de Moura	3715b10ce7	feat(util/sexpr/options): serialization for options Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-27 20:40:00 -08:00
Leonardo de Moura	dbebb4a4a1	feat(util/sexpr): serialization for sexpr Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-27 20:19:56 -08:00
Leonardo de Moura	9c6dc5d230	feat(util/serializer): add hackish write_double/read_double Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-27 19:46:45 -08:00
Leonardo de Moura	abc370a011	feat(util/numerics): serialization for mpz and mpq Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-27 18:32:01 -08:00
Leonardo de Moura	49df0c435d	feat(util/serializer): make sure the read/write is portable Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-27 18:07:19 -08:00
Leonardo de Moura	d05695c331	feat(util/name): serialization for hierarchical names Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-27 17:47:20 -08:00
Leonardo de Moura	cbe0b8532a	feat(util/serializer): add write_char and read_char Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-27 17:22:15 -08:00
Leonardo de Moura	b72937c02c	feat(util/serializer): simple serialization infrastructure Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-27 16:50:06 -08:00
Leonardo de Moura	8b6421e4de	feat(util/extensible_object): add template for creating 'extensible' objects Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-27 15:40:21 -08:00
Leonardo de Moura	8cf65f354b	fix(frontends/lean/pp): forall and exists pretty printing when used as constants Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-27 12:50:41 -08:00
Leonardo de Moura	a02c6e70fa	fix(frontends/lean/pp): missing parenthesis around nested forall/exists Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-27 12:13:36 -08:00
Leonardo de Moura	3f0279b88c	refactor(frontends/lua): replace lean.lua.h with util.lua Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-26 19:49:26 -08:00
Leonardo de Moura	40eca048e0	feat(extra): replace parse_lean_tpl with improved parse_template, that is based on macros Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-26 19:28:02 -08:00
Leonardo de Moura	a9ee92aa3f	fix(frontends/lean/parser): macro precedence Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-26 19:17:43 -08:00
Leonardo de Moura	3abfad7a88	feat(frontends/lean/parser): add support for integer arguments in macros Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-26 18:51:37 -08:00
Leonardo de Moura	f1b97b18b4	refactor(frontends/lean/parser): tactic macros, and tactic Lua bindings Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-26 15:54:53 -08:00
Leonardo de Moura	ef18cc4a92	fix(frontends/lean/parser): add existing command macros when creating parser object Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-26 13:38:14 -08:00
Leonardo de Moura	8e4560a866	feat(frontends/lean/parser): protect imported modules from Lua definitions and macros in the file importing the module Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-26 13:21:36 -08:00
Leonardo de Moura	ba02132a90	feat(frontends/lean/parser): add command macros The idea is to allow users to define their own commands using Lua. The builtin command Find is now written in Lua. This commit also fixes a bug in the get_formatter() Lua API. It also adds String arguments to macros. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-26 13:00:28 -08:00
Leonardo de Moura	480781d13e	feat(frontends/lean/parser): provide environment as an argument to macros, allow macros to parse tactics Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-26 11:15:45 -08:00
Leonardo de Moura	71a0f83143	feat(util/sexpr/format): turn off colors on Windows Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-26 09:54:29 -08:00
Leonardo de Moura	3673f2ac1d	feat(frontends/lean/parser): add Find command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-25 18:31:52 -08:00
Leonardo de Moura	d44925f943	fix(build): missing file Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-25 16:20:25 -08:00
Leonardo de Moura	99f9478d93	feat(build): cpack support Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-25 16:18:51 -08:00
Leonardo de Moura	a9712b91a8	feat(util/lean_path): include ../library in the default LEAN_PATH Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-25 16:18:27 -08:00
Leonardo de Moura	768f86aa12	chore(memcheck.supp): another suppression for awk Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-25 13:56:50 -08:00
Leonardo de Moura	a3dde29f3c	feat(frontends/lua/parser): allow users to specify the precedence of macros Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-25 12:27:56 -08:00
Leonardo de Moura	f418491c70	fix(frontends/lua/parser): typo Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-25 12:03:04 -08:00
Leonardo de Moura	88235d2922	feat(library/tactic/apply_tactic): try other solutions produced by the elaborator Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-25 11:51:27 -08:00
Leonardo de Moura	8e45064f25	feat(library/tactic/apply_tactic): improved parametric apply_tactic Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-24 22:40:34 -08:00
Leonardo de Moura	60ac0b508d	fix(tests/kernel/environment): adjust the test to reflect (recent) change in the normalizer Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-24 21:14:22 -08:00
Leonardo de Moura	2aa691ccb3	fix(kernel/replace_fn): ignore the cached type in constants Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-24 21:11:25 -08:00
Leonardo de Moura	afd10d62ca	feat(util/list): improve to_list function, it takes an optional tail Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-24 20:56:34 -08:00
Leonardo de Moura	1a0f0c1609	feat(kernel/normalizer): let normalizer ignore 'undefined' constants Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-24 20:54:15 -08:00
Leonardo de Moura	75cf751959	feat(library/tactic/apply_tactic): allow apply_tac Lua binding to take expressions as argument Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-24 16:03:16 -08:00
Leonardo de Moura	6cc57cc4b5	fix(library/tactic/apply_tactic): bug in apply_tac Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-24 15:54:56 -08:00
Leonardo de Moura	cb95b14332	feat(library/tactic/apply_tactic): improve apply_tactic Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-24 14:23:06 -08:00
Leonardo de Moura	879ab6924a	tests(test/lean): remove 'Importing...' message, the tests using the Import command fail when running on a different machine Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-24 12:26:53 -08:00
Soonho Kong	de018220e1	feat(*): use std::make_shared to create shared_ptr	2013-12-24 14:32:50 -05:00
Leonardo de Moura	00e89190c2	refactor(library/cast): use .lean file instead of .cpp file to define casting library Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-23 22:04:19 -08:00
Leonardo de Moura	d5dc5cb576	feat(frontends/lean/parser): use LEAN_PATH in the Import command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-23 22:00:44 -08:00
Leonardo de Moura	8c8cefcb0c	feat(frontends/lean/parser): compact definitions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-23 21:24:50 -08:00
Leonardo de Moura	5fd3fa1c0e	chore(memcheck.supp): add suppression for readline problem Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-23 17:27:04 -08:00
Leonardo de Moura	b83b17d3ab	fix(kernel/metavar): bug at cached_metavar_env::update method Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-23 15:41:02 -08:00
Leonardo de Moura	5043cc75f6	fix(frontends/lean/parser): allow parenthesis in level expressions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-23 13:31:55 -08:00
Leonardo de Moura	5244ccafe8	fix(frontends/lean/parser): readline compilation problem on Fedora19 Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-23 13:12:39 -08:00
Leonardo de Moura	702f0c2190	fix(tests/kernel/free_vars): reduce example stack size consumption Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-23 12:57:25 -08:00
Leonardo de Moura	7c05eb4695	fix(frontends/lean/parser): make sure Lean passes all tests when being compiled with the readline library Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-23 12:57:25 -08:00
Leonardo de Moura	bcb41cd938	fix(util/lean_path): warnings produced by Valgrind Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-23 10:02:48 -08:00
Leonardo de Moura	f0833b6f46	chore(frontends/lua/lean.lua.h): fix style warnings Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-22 21:34:20 -08:00
Leonardo de Moura	b5d23619cb	feat(util/script_state): add 'import' command to Lua, it import files from the LEAN_PATH Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-22 21:27:12 -08:00
Leonardo de Moura	84c984a435	feat(build): copy extra files to bin directory Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-22 21:00:32 -08:00
Leonardo de Moura	e91fdaed00	refactor(frontends/lean): rename lean.lua to lean.lua.h Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-22 20:16:31 -08:00
Leonardo de Moura	e5f53595b6	fix(util/lean_path): bug at init_lean_path (it was missing last path), and add normalization function Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-22 19:38:32 -08:00
Leonardo de Moura	50de85ee29	fix(util/lean_path): get_exe_location for Windows Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-22 19:13:41 -08:00
Leonardo de Moura	cc9e16c3fc	feat(util/lean_path): add function for searching for a file in the LEAN_PATH Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-22 18:47:49 -08:00
Leonardo de Moura	baf99779dc	feat(frontends/lean/frontend_elaborator): use is_convertible to minimize number of coercions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-22 17:57:51 -08:00
Leonardo de Moura	777582380f	feat(util/lean_path): add support for LEAN_PATH Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-22 17:56:53 -08:00
Leonardo de Moura	df1b21a03d	feat(util/exe_location): add function for finding the location of the executable Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-22 17:12:31 -08:00
Leonardo de Moura	3e32d9bef2	feat(library/tactic): add support for Pi's at to_proof_state Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-22 16:40:55 -08:00
Leonardo de Moura	104bd990e1	feat(library/tactic): add normalize_tac, eval_tac and trivial_tac Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-22 14:10:42 -08:00
Leonardo de Moura	21d244d880	feat(frontends/lean/parser): allow tactic to be used to fill holes in definitions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-22 12:08:25 -08:00
Leonardo de Moura	4229e498d2	refactor(kernel/type_checker): combine type_checker and type_inferer into a single class, and avoid code duplication Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-22 11:51:38 -08:00
Leonardo de Moura	9bac91f5ef	fix(frontends/lean): libreadline support Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-21 18:57:15 -08:00
Leonardo de Moura	9128a437b8	refactor(library/cast): replace cast semantic attachment with axioms, add heterogeneous symmetry axiom Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-21 18:23:37 -08:00
Leonardo de Moura	df58eb132e	feat(frontends/lean): simplify explicit version names Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-21 17:05:25 -08:00
Leonardo de Moura	36b2ec9abb	fix(library/cast): bugs in Cast semantic attachment TODO: revise cast semantic attachment. It should be axioms instead of semantic attachments. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-21 16:16:54 -08:00
Leonardo de Moura	aebff0b4d3	fix(library/type_inferer): bug in get_range method Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-21 14:55:07 -08:00
Leonardo de Moura	90dbdaec40	feat(kernel/expr): cache is_arrow result Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-21 13:59:45 -08:00
Leonardo de Moura	1faf42e2e1	chore(kernel/expr): remove unnecessary #if-#then-#else Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-21 13:36:41 -08:00
Leonardo de Moura	97145c0f88	fix(library/elaborator): bug in free variable normalization (lift was missing) Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-21 06:41:09 -08:00
Leonardo de Moura	7b0b363b32	fix(kernel/normalizer): metavariable reification Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-21 06:40:26 -08:00
Leonardo de Moura	fddcdb8f40	fix(library/elaborator): bug in process_lower Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-21 04:13:14 -08:00
Leonardo de Moura	ce84fe5d33	feat(frontends/lean): improve error messages when elaborator cannot instantiate all metavariables Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-20 22:00:50 -08:00
Leonardo de Moura	bb81311e0a	feat(frontends/lean/parser): include proof state in exception for tactic failure Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-20 17:15:12 -08:00
Leonardo de Moura	84df182beb	refactor(kernel/instantiate): remove hackish (dead) function Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-20 14:37:05 -08:00
Leonardo de Moura	4d05a8b65b	fix(library/tactic/apply_tactic): provide the metavar_env to instantiate, the goal is to avoid add_lift and add_inst local entries Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-20 14:17:04 -08:00
Leonardo de Moura	1ed4aa391c	fix(library/fo_unify): bug at function that extracts the lhs and rhs of homogeneous/heterogeneous equality For homogeneous equality, arg #1 is the Type of the lhs/rhs. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-20 14:14:20 -08:00
Leonardo de Moura	7772c16033	refactor(kernel): add unfold_opaque flag to normalizer, modify how type checker uses the opaque flag, remove hidden_defs, and mark most builtin definitions as opaque After this commit, in the type checker, when checking convertability, we first compute a normal form without expanding opaque terms. If the terms are convertible, then we are done, and saved a lot of time by not expanding unnecessary definitions. If they are not, instead of throwing an error, we try again expanding the opaque terms. This seems to be the best of both worlds. The opaque flag is a hint for the type checker, but it would never prevent us from type checking a valid term. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-20 12:47:47 -08:00
Leonardo de Moura	026f666526	feat(kernel/type_checker): use expression before normalization in the unification constraints generated by the typechecker Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-20 11:22:13 -08:00
Leonardo de Moura	daef2b7b24	feat(util/sexpr/options): add is_eqp predicate for options Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-20 10:53:53 -08:00
Leonardo de Moura	4838c055b8	feat(kernel/environment): add set_opaque method Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-20 10:45:44 -08:00
Leonardo de Moura	812c1a2960	feat(library/elaborator): only expand definitions that are not marked as hidden The elaborator produces better proof terms. This is particularly important when we have to prove the remaining holes using tactics. For example, in one of the tests, the elaborator was producing the sub-expression (λ x : N, if ((λ x::1 : N, if (P a x x::1) ⊥ ⊤) == (λ x : N, ⊤)) ⊥ ⊤) After, this commit it produces (λ x : N, ¬ ∀ x::1 : N, ¬ P a x x::1) The expressions above are definitionally equal, but the second is easier to work with. Question: do we really need hidden definitions? Perhaps, we can use only the opaque flag. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-20 02:16:49 -08:00
Leonardo de Moura	cb48fbf3c4	fix(library/elaborator): missing case The elaborator was failing in the following scenario: - Failing constraint of the form ctx \|- ?m1 =:= ?m2 where ?m2 is assigned to ?m1, and ?m1 is unassigned. has_metavar(?m2, ?m1) returns true, and a cycle is incorrectly reported. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-20 01:39:43 -08:00
Leonardo de Moura	96ea8b81c8	feat(frontends/lean/parser): change show-expression binder name Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-20 01:30:18 -08:00
Leonardo de Moura	c730dd7872	feat(frontends/lean/parser): propagate position information to expressions created by macro implemented in Lua Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-20 01:07:37 -08:00
Leonardo de Moura	3eb4de6760	fix(frontends/lean/parser): fix deadlock in macro parser Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-19 21:40:00 -08:00
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
Leonardo de Moura	4357c9196e	feat(kernel/metavar): make sure that a metavariable 'm' can only be assigned to a term that contains free variables available in the context associated with 'm' This commit also simplifies the method check_pi in the type_checker and type_inferer. It also fixes process_meta_app in the elaborator. The problem was in the method process_meta_app and process_meta_inst. They were processing convertability constrains as equality constraints. For example, process_meta_app would handle ctx \|- Type << ?f b as ctx \|- Type =:= ?f b This is not correct because a ?f that returns (Type U) for b satisfies the first but not the second. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-14 12:25:00 -08:00
Leonardo de Moura	51aee83b70	refactor(kernel/metavar_env): use the same approach used in the class environment in the class metavar_env This modification was motivated by a bug exposed by tst17 at tests/kernel/type_checker. metavar_env is now a smart point to metavar_env_cell. ro_metavar_env is a read-only smart pointer. It is useful to make sure we are using proof_state correctly. example showing that the approach for caching metavar_env is broken in the type_checker Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-13 18:59:15 -08:00
Soonho Kong	26afc6cf12	fix(cmake): fix problem of using LuaJit on OSX(64-bit) http://luajit.org/install.html If you're building a 64 bit application on OSX which links directly or indirectly against LuaJIT, you need to link your main executable with these flags: -pagezero_size 10000 -image_base 100000000	2013-12-13 19:52:40 -05:00
Leonardo de Moura	2e5e5e187f	chore(util/rc): remove unnecessary argument from LEAN_COPY_REF and LEAN_MOVE_REF macros Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-13 15:01:24 -08:00
Leonardo de Moura	3416df85f8	fix(util/thread): warning 'thread.cpp.o has no symbols' Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-13 14:00:40 -08:00
Leonardo de Moura	fa8b984e27	fix(kernel/environment): compilation warnings Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-13 13:54:45 -08:00
Soonho Kong	46e7802d9a	test(library/rewriter): add lambda_{body/type}_rewriter tests	2013-12-13 15:08:23 -05:00
Soonho Kong	5b95cf1e03	fix(shell/lua_repl.h): use loadstring for Lua-5.1 instead of load	2013-12-13 00:13:48 -05:00
Soonho Kong	f90a9e96d0	fix(shell/lean.cpp): fix not to overwrite optind by getopt_long	2013-12-12 23:20:47 -05:00
Leonardo de Moura	ae52c8062e	chore(kernel/metavar): remove unused function Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-12 17:39:14 -08:00
Leonardo de Moura	450d6a4b1e	refactor(util/splay_tree): replace find with splay_find Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-12 17:27:30 -08:00
Leonardo de Moura	f97c260b0b	refactor(kernel/environment): add ro_environment The environment object is a "smart-pointer". Before this commit, the use of "const &" for environment objects was broken. For example, suppose we have a function f that should not modify the input environment. Before this commit, its signature would be void f(environment const & env) This is broken, f's implementation can easilty convert it to a read-write pointer by using the copy constructor. environment rw_env(env); Now, f can use rw_env to update env. To fix this issue, we now have ro_environment. It is a shared const pointer. We can convert an environment into a ro_environment, but not the other way around. ro_environment can also be seen as a form of documentation. For example, now it is clear that type_inferer is not updating the environment, since its constructor takes a ro_environment. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-12 16:48:34 -08:00
Leonardo de Moura	7b2cbd6926	chore(kernel/environment): remove implementation hack Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-12 16:48:34 -08:00
Leonardo de Moura	7d184c3c4b	fix(util/shared_mutex) missing pragma Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-12 16:48:34 -08:00
Leonardo de Moura	3457fe5935	chore(kernel): rename read_only_environment and read_write_environment Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-12 16:48:33 -08:00
Leonardo de Moura	1852c86948	feat(kernel): improve instantiate and lift_free_vars (use metavar_env to minimize the number of lift and inst local_entries needed) Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-12 16:48:33 -08:00
Leonardo de Moura	058bdb88ac	feat(kernel/context): add operator== for contexts, and new constructor Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-12 16:48:33 -08:00
Leonardo de Moura	38a25a1bd2	feat(kernel/metavar): (re-)enable add_lift simplification Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-12 16:48:33 -08:00
Leonardo de Moura	6ed62247b0	chore(memcheck.supp): generalize Memcheck:Addr4 suppression for LuaJIT, there many warnings of this kind Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-12 09:24:15 -08:00
Leonardo de Moura	98f5ce0512	fix(kernel/context): unused var warning in release mode Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-11 21:24:05 -08:00
Leonardo de Moura	3e77dd0c42	fix(kernel/context): make context remove more robust Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-11 19:51:57 -08:00
Leonardo de Moura	f728f80960	fix(library/elaborator): remove is_neutral_abstraction hack, and bug at process_metavar_lift_abstraction Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-11 19:41:24 -08:00
Leonardo de Moura	8f67348c05	fix(library/elaborator): remove nasty hack, this hack was throwing away the local context at process_meta_app_core Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-11 19:27:21 -08:00
Leonardo de Moura	c29b155fdd	feat(library/elaborator): use improved has_free_vars in the elaborator Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-11 16:15:20 -08:00
Leonardo de Moura	0e2b7973cf	feat(kernel/free_vars): improve has_free_vars function, it produces better results for expressions containing metavariables Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-11 16:09:33 -08:00
Leonardo de Moura	af1b0d2e81	feat(library): add function free_var_range for computing the range [0, R) of free variables occurring in an expression Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-11 15:32:50 -08:00
Leonardo de Moura	1d33d3b5db	fix(library/elaborator): the context of auxiliary metavariables created in the imitation step was incorrect Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-11 12:35:32 -08:00
Leonardo de Moura	55389cf6e5	feat(kernel/context): add find, a version of lookup that does not throw an exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-11 09:54:54 -08:00
Leonardo de Moura	cdec9762ce	chore(util/pvector): remove unused template Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-10 20:32:10 -08:00
Leonardo de Moura	f8e87436a7	perf(library/elaborator): avoid exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-10 19:40:59 -08:00
Leonardo de Moura	4de5f06a97	fix(library/elaborator): bug in process_metavar_inst, and disable simplification that is negatively impacting the elaborator Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-10 19:26:58 -08:00
Leonardo de Moura	5ae71e75bd	perf(library/elaborator): avoid exception Lean was spending 17% on the runtime "throwing exceptions" in the test tests/lean/implicit7.lean Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-10 16:31:36 -08:00
Leonardo de Moura	1fb526a3d4	perf(library/type_inferer): improve is_proposition performance Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-10 16:18:45 -08:00
Leonardo de Moura	b270fb0030	refactor(library/elaborator): remove synthesizer Synthesizer is not part of the elaborator anymore. The elaborator fills the "easy" holes. The remaining holes are filled using different techniques (e.g., tactic framework) that are independent of the elaborator. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-10 15:55:54 -08:00
Leonardo de Moura	bbaa83e16a	feat(frontends/lean): implement relaxed operator compatibility in the parser Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-10 15:42:43 -08:00
Leonardo de Moura	c0b9c7ffc4	refactor(library/io_state): simplify regular/diagnostic Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-10 13:09:35 -08:00
Leonardo de Moura	e0eeb7c8d5	feat(frontends/lean/operator_info): add << for diagnostic and regular streams Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-10 12:52:31 -08:00
Leonardo de Moura	90f88acf42	feat(frontends/lean): relax compatible_denotation predicate Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-10 12:42:29 -08:00
Leonardo de Moura	abe2cf2fb5	feat(frontends/lean): simplify how implicit parameters are marked Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-10 12:11:04 -08:00
Leonardo de Moura	88f80c9693	fix(shell): add 'file not found' error message Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-10 10:55:13 -08:00
Leonardo de Moura	78ec4b152b	feat(frontends/lean): relax restricitions on parsing applications of functions containing implicit arguments Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-10 09:48:24 -08:00
Leonardo de Moura	7ab321f568	chore(util): remove dead file Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-09 22:32:11 -08:00
Leonardo de Moura	0cd8e3e76b	feat(split-stack): add support for split-stacks (no more stackoverflows) Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-09 22:30:54 -08:00
Leonardo de Moura	fd2a04e9ac	fix(util/stackinfo): bug on Fedora Signed-off-by: Leonardo de Moura <leonardo@nod1-2008.corp.crtest.com>	2013-12-09 18:44:14 -08:00
Leonardo de Moura	e3403492a5	feat(build): -D STATIC=ON option for building a static Lean executable On Linux, -D STATIC=ON does not work if MULTI_THREAD support is enabled. If we search for "pthread static crash" we find other projects with the same problem. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-09 18:02:10 -08:00
Leonardo de Moura	0b1789edf2	feat(shell): add command line option to set thread stack size (only available if using Boost) Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-09 17:33:47 -08:00
Leonardo de Moura	e7ae749221	feat(boost): implement multi-threading support using Boost To use Boost instead of the standard library, we must use the cmake option -D BOOST=ON Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-09 17:24:32 -08:00
Leonardo de Moura	533ed51f51	feat(util/shared_mutex): skip shared_mutex implementation if LEAN_MULTI_THREAD is not defined Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-09 15:42:08 -08:00
Leonardo de Moura	8f2fe273ea	refactor(*): isolate std::thread dependency This commit allows us to build Lean without the pthread dependency. It is also useful if we want to implement multi-threading on top of Boost. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-09 15:20:26 -08:00
Leonardo de Moura	0eaa98221b	fix(shell/lean): Lua repl missing, incorrect exit code in interactive mode, missing tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-09 12:25:19 -08:00
Leonardo de Moura	0d10cba4a0	refactor(util/sexpr/format): minimize the use of recursion, combine be and layout into a single procedure (without creating a temporary potentially big sexpr) Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-08 21:06:24 -08:00
Leonardo de Moura	25a2f5f7e0	fix(kernel/formatter): clang++ errors and warnings Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-08 18:54:04 -08:00
Leonardo de Moura	445d4f6793	refactor(kernel/unification_constraint): remove 'null' unification_constraint and its operator bool Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-08 18:11:35 -08:00
Leonardo de Moura	3ea09daf44	fix(frontends/lean/frontend): is_coercion for environment objects that have parents Bug was exposed by tests/lua/coercion_bug1.lua Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-08 17:47:00 -08:00
Leonardo de Moura	2a80807fef	refactor(frontends/lean/pp): replace weak_ref with a strong reference, add new function (lean_formatter) for creating a Lean object formatter in the Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-08 17:33:18 -08:00
Leonardo de Moura	340d643d89	fix(library/kernel_bindings): make sure that when a formatter is invoked and it has a reference to an environment object, we get a read-only lock to the environment object Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-08 16:55:55 -08:00
Leonardo de Moura	da613f67a8	refactor(frontends/lean/pp): replace dangerous frontend reference with a weak_ref to the environment Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-08 16:42:12 -08:00
Leonardo de Moura	759fcb7b4f	refactor(kernel/formatter): hide 'unsafe' constructor Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-08 15:39:26 -08:00
Leonardo de Moura	68c2e5cc7d	fix(frontends/lean/parser): reachable code The new test nbug1.lean exposes the problem. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-08 15:22:21 -08:00
Leonardo de Moura	8add5571f1	refactor(library/tactic): remove 'null' tactic, and operator bool tactics Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-08 15:00:16 -08:00
Leonardo de Moura	a4afdfeace	refactor(kernel/expr): remove the dangerous expr::release method Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-08 14:45:18 -08:00
Leonardo de Moura	04b67f8b14	refactor(kernel/object): remove 'null' object, and operator bool for kernel objects Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-08 14:37:38 -08:00
Leonardo de Moura	2f88d6710c	feat(kernel/expr): add some_expr and none_expr for building values of type optional<expr> Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-08 10:34:38 -08:00
Leonardo de Moura	25b812f1c9	feat(kernel/expr): no overhead optional<expr> template specialization Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-08 10:17:29 -08:00
Leonardo de Moura	3e1fd06903	refactor(kernel/expr): remove 'null' expression, and operator bool for expression After this commit, a value of type 'expr' cannot be a reference to nullptr. This commit also fixes several bugs due to the use of 'null' expressions. TODO: do the same for kernel objects, sexprs, etc. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-07 23:21:10 -08:00
Leonardo de Moura	e4dff52d7a	refactor(frontends/lean/parser): cleanup method apply_tactics Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-07 15:44:47 -08:00
Leonardo de Moura	1ff6013594	fix(frontends/lean/frontend_elaborator): must elaborate type attached to placeholder, it may also contain holes The test tactic14.lean exposes the problem. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-07 15:37:59 -08:00
Leonardo de Moura	b6b520302d	feat(kernel/replace_visitor): relax replace_visitor contract, the input expression can be null Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-07 15:35:26 -08:00
Leonardo de Moura	e2999d3ff6	feat(*): add component name to check_stack and check_system I also reduced the stack size to 8 Mb in the tests at tests/lean and tests/lean/slow. The idea is to simulate stackoverflow conditions. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-07 15:11:55 -08:00
Leonardo de Moura	33b72f1dd0	feat(frontends/lean/parser): apply type inference elaborator to fill remaining metavariables/holes (these are holes produced by tactics such as apply_tac) Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-07 13:09:39 -08:00
Leonardo de Moura	bc3a6a3185	refactor(frontends/lean/parser): cleanup tactic support in the default lean parser Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-07 12:15:03 -08:00
Leonardo de Moura	195ea24d71	refactor(kernel/type_checker): pass buffer<unification_constraint> as a pointer The idea is to make it an optional parameter independent of metavar_env. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-07 10:27:11 -08:00
Leonardo de Moura	5f3b9dbbbd	fix(library/fo_unify): unify (?f ?x) with (g a b) We flat applications. So, (g a b) is actually ((g a) b). So, we must be able to unify (?f ?x) with (g a b). Solution: ?g <- (g a) ?x <- b Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-07 10:25:11 -08:00
Leonardo de Moura	015bff8283	fix(library/tactic/goal): to_goal way of handling context_entries of the form (name, domain, body) where domain is null, and body is a proof term This commit fixes a problem exposed by t13.lean. It has a theorem of the form: Theorem T1 (A B : Bool) : A /\ B -> B /\ A := fun assumption : A /\ B, let lemma1 := (show A by auto), lemma2 := (show B by auto) in (show B /\ A by auto) When to_goal creates a goal for the metavariable associated with (show B /\ A by auto) it receives a context and proposition of the form [ A : Bool, B : Bool, assumption : A /\ B, lemma1 := Conjunct1 assumption, lemma2 := Conjunct2 assumption ] \|- B /\ A The context_entries "lemma1 := Conjunct1 assumption" and "lemma2 := Conjunct2 assumption" do not have a domain (aka type). Before this commit, to_goal would simply replace and references to "lemma1" and "lemma2" in "B /\ A" with their definitions. Note that, "B /\ A" does not contain references to "lemma1" and "lemma2". Then, the following goal is created A : Bool, B : Bool, assumption : A /\ B \|- B /\ A That is, the lemmas are not available when solving B /\ A. Thus, the tactic auto produced the following (weird) proof for T1, where the lemmas are computed but not used. Theorem T1 (A B : Bool) (assumption : A ∧ B) : B ∧ A := let lemma1 := Conjunct1 assumption, lemma2 := Conjunct2 assumption in Conj (Conjunct2 assumption) (Conjunct1 assumption) This commit fixed that. It computes the types of "Conjunct1 assumption" and "Conjunct2 assumption", and creates the goal A : Bool, B : Bool, assumption : A /\ B, lemma1 : A, lemma2 : B \|- B /\ A After this commit, the proof for theorem T1 is Theorem T1 (A B : Bool) (assumption : A ∧ B) : B ∧ A := let lemma1 := Conjunct1 assumption, lemma2 := Conjunct2 assumption in Conj lemma2 lemma1 as expected. Finally, this example suggests that the encoding Theorem T1 (A B : Bool) : A /\ B -> B /\ A := fun assumption : A /\ B, let lemma1 : A := (by auto), lemma2 : B := (by auto) in (show B /\ A by auto) is more efficient than Theorem T1 (A B : Bool) : A /\ B -> B /\ A := fun assumption : A /\ B, let lemma1 := (show A by auto), lemma2 := (show B by auto) in (show B /\ A by auto) Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-06 16:14:25 -08:00
Leonardo de Moura	bd9df3b08f	fix(library/tactic/goal): null hypothesis being added by to_goal Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-06 16:03:06 -08:00
Leonardo de Moura	872434e632	fix(kernel/has_free_vars): return false for null expression Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-06 16:01:57 -08:00
Leonardo de Moura	147626c906	fix(kernel/printer): memory access violation when printing contexts Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-06 15:50:29 -08:00
Leonardo de Moura	0390f3c39b	feat(library/tactic/boolean_tactics): avoid unnecessary Let expression in proof terms Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-06 15:01:54 -08:00
Leonardo de Moura	1df9d18891	feat(frontends/lean): allow 'tactic hints' to be associated with 'holes' Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-06 14:49:39 -08:00
Leonardo de Moura	2ddcc32c1d	fix(frontends/lean/notation): change the precedence of '->' It should match the precedence of the implication '=>'. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-06 13:23:24 -08:00
Leonardo de Moura	d79a626523	fix(kernel/type_checker): Pi with metavariables case The type checker (and type inferer) were not handling correctly Pi expressions where the type universe cannot be established due to the occurrence of metavariables. In this case, a max-constraint is created. The problem is that the domain and body of the Pi are in different contexts. The constrain generated before this commit was incorrect, it could contain a free variable. This commit fix the issue by using the context of the body, and lifting the free variables in the domain by 1. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-06 13:07:59 -08:00
Leonardo de Moura	fa03ae2a26	fix(library/elaborator): strength elaborator procedure for handling equality and convertability constraints This commit improves the condition for showing that an equality(and convertability) constraint cannot be solved. A nice consequence is that Lean produces nicer error messages. For example, the error message for unit test elab1.lean is more informative. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-06 13:04:34 -08:00
Leonardo de Moura	d46cf5fdd5	fix(frontends/lean/parser): display failed state in noninteractive mode, stop processing tactic commands when a Lean command is found Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-06 05:13:29 -08:00
Leonardo de Moura	c841763a05	feat(library/elaborator): add special treatment for constraints of the form ?m[inst:i v] << t, where t is a proposition Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-06 04:51:07 -08:00
Leonardo de Moura	4e4fea1eca	fix(examples/lean): add all examples to test suite Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-05 21:54:55 -08:00
Leonardo de Moura	13f9454fe1	feat(library/tactic/proof_state): add option tactic::proof_state::goal_names Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-05 21:18:22 -08:00
Leonardo de Moura	e6fb6f7d1e	feat(frontends/lean/parser): add assumption command, and allow Lean expressions (proof terms) to be used with apply tactic command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-05 20:08:51 -08:00
Leonardo de Moura	0c059a9917	feat(library/tactic): use _tac suffix instead of _tactic like Isabelle Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-05 20:06:32 -08:00
Leonardo de Moura	1b176204b4	feat(frontends/lean/parser): allow the user to use a theorem/axiom name as an argument for the apply tactic command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-05 19:03:12 -08:00
Leonardo de Moura	c1afefb873	feat(library/fo_unify): unify heterogeneous - homogeneous equality Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-05 19:00:31 -08:00
Leonardo de Moura	e1d44eec6b	fix(frontends/lean/parser): bug in parse_tactic Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-05 17:40:55 -08:00
Leonardo de Moura	a564795fe6	fix(frontends/lean/parser): remove unnecessary '#' after error Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-05 17:27:08 -08:00
Leonardo de Moura	e069ce640b	feat(frontends/lean/parser): add tactic abort command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-05 17:15:19 -08:00
Leonardo de Moura	34654ad06b	feat(tests/lean/interactive): add interactive mode test script Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-05 16:56:20 -08:00
Leonardo de Moura	e3848d43a2	feat(frontends/lean): improve tactic command parsing in interactive mode Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-05 16:28:08 -08:00
Leonardo de Moura	a1b5a8e50f	fix(frontends/lean): check wheter the synthesized proof term has metavars or not Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-05 14:22:19 -08:00
Leonardo de Moura	873a07d34c	feat(kernel/replace_visitor): check interrupted flag and stackoverflow Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-05 05:42:12 -08:00
Leonardo de Moura	43ef8b9a4b	refactor(library/tactic): rename boolean.* to boolean_tactics.* Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-05 05:03:18 -08:00
Leonardo de Moura	fa98c1358f	feat(library/tactic): add disj_tactic Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-05 04:49:06 -08:00
Leonardo de Moura	056759880c	feat(frontends/lean): add back (backtracking) command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-05 04:39:08 -08:00
Leonardo de Moura	029ef57abd	feat(library/tactic): add apply_tactic Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-05 03:22:12 -08:00
Leonardo de Moura	7b4ea75dee	fix(frontends/lean): do not display Ctrl-D message on Windows Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-04 11:39:30 -08:00
Leonardo de Moura	d949dfd46d	fix(util/stackinfo): compilation warning on cygwin/mingw Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-04 11:32:39 -08:00
Leonardo de Moura	1e5518002b	feat(shell/lean): add git hash to executable Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-04 11:23:15 -08:00
Leonardo de Moura	e60e20a11d	feat(frontends/lean): add Exit command Remark: on Windows, Ctrl-D does not seem to work. So, this commit also changes the Lean startup message. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-04 10:40:22 -08:00
Leonardo de Moura	fa35fd6989	chore(*): make sure LEAN_THREAD_UNSAFE build flag is handled correctly When LEAN_THREAD_UNSAFE=ON, we: - Do not run tests at tests/lua/threads - Disable thread object at Lua API - par tactical becomes an alias for interleave - Disable some unit tests that use threads Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-04 10:27:22 -08:00
Leonardo de Moura	1a02abf7b2	feat(util/script_state): add a lua hook function that checks for the interrupt flag This is a very convenient feature for interrupting non-terminating user scripts. Before this commit, the user had to manually invoke check_interrupt() in potentially expensive loops. Now, this is not needed anymore. Remark: we still have to check whether this trick works with LuaJIT or not. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-04 09:57:36 -08:00
Leonardo de Moura	ef6a27fe84	feat(util/script_state): add join method to Lua threads Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-04 09:15:09 -08:00
Leonardo de Moura	def186a9cd	fix(util/stackinfo): try to fix incorrect main thread stack size on OSX This fix tries to fix two failures on our unit tests. tests/kernel/normalizer tests/kernel/type_checker Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-04 08:56:46 -08:00
Leonardo de Moura	d481cb251d	chore(memcheck): add another suppression for LuaJIT Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-04 08:32:44 -08:00
Leonardo de Moura	fd9781d58d	fix(util/stackinfo): compilation warning on mingw and cygwin Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-04 08:26:50 -08:00
Leonardo de Moura	ef069e39b0	chore(*): replace to_expr with to_nonnull_expr (when appropriate) The goal is to make the Lua API more robust. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-03 12:53:53 -08:00
Leonardo de Moura	bcc8b67592	chore(*): consistent file name convention Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-03 12:40:52 -08:00
Leonardo de Moura	8e53643b61	feat(library/fo_unify): first order unification Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-03 12:21:21 -08:00
Leonardo de Moura	f80106a895	chore(*): use 'explicit operator bool' everywhere. operator bool() may produce unwanted conversions. For example, we had the following bug in the code base. ... object const & obj = find_object(const_name(n)); if (obj && obj.is_builtin() && obj.get_name() == n) ... obj.get_name() has type lean::name n has type lean::expr Both have 'operator bool()', then the compiler uses the operator to convert them to Boolean, and then compare the result. Of course, this is not our intention. After this commit, the compiler correctly signs the error. The correct code is ... object const & obj = find_object(const_name(n)); if (obj && obj.is_builtin() && obj.get_name() == const_name(n)) ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-02 23:02:45 -08:00
Leonardo de Moura	d79b2babd3	fix(*): typo Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-02 08:46:47 -08:00
Leonardo de Moura	dd62af1641	feat(frontends/parser): simplified theorem definition using tactical proof When using tactics for proving theorems, a common pattern is Theorem T : <proposition> := _. apply <tactic>. ... done. This commit allows the user to write the simplified form: Theorem T : <proposition>. apply <tactic>. ... done. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-02 08:20:18 -08:00
Leonardo de Moura	25978118df	feat(library/tactic): add beta-reduction tactic Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-02 08:10:51 -08:00
Leonardo de Moura	39b99683a8	fix(util/stackinfo): handle error codes in the Linux version Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-02 07:56:53 -08:00
Soonho Kong	31b26f53ad	fix(util/stackinfo): fix typo	2013-12-02 00:03:57 -05:00
Soonho Kong	7776f4b24b	fix(util/stackinfo): fix preprocessor directive	2013-12-01 23:44:58 -05:00
Soonho Kong	4de3b772fd	feat(util/stackinfo): implement get_stack_size (Mac OSX version)	2013-12-01 22:24:12 -05:00
Soonho Kong	a2d6918348	fix(library/rewriter): use Abst axiom in lambda_body RW	2013-12-01 22:24:12 -05:00
Soonho Kong	0553d29078	test(library/rewriter): add lambda_rewrite tests	2013-12-01 22:24:12 -05:00
Leonardo de Moura	75f8d56eb1	fix(util/stackinfo): memory leak at get_stack_size Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-01 19:17:28 -08:00
Leonardo de Moura	74dfdd02de	feat(util): add primitives for checking the amount of available stack space Recursive functions that may go very deep should invoke the function check_stack. It throws an exception if the amount of stack space is limited. The function check_system() is syntax sugar for check_interrupted(); check_stack(); Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-01 17:19:27 -08:00
Leonardo de Moura	1ec8f9d536	feat(kernel): add abstraction (aka function extensionality) axiom Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-01 13:57:14 -08:00
Leonardo de Moura	09f98ecddc	feat(library/tactic): add unfold_tactic() that unfolds every non-hidden definition Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-01 10:41:05 -08:00
Leonardo de Moura	70e06f8e86	feat(library/hidden_defs): hidden definitions are just hints for tactics and solvers Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-01 10:27:27 -08:00
Leonardo de Moura	ca53a5a1cc	feat(library/tactic): add unfold tactic Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-01 08:51:56 -08:00
Leonardo de Moura	737e634556	fix(util/list): bug in map template Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-01 08:51:24 -08:00
Leonardo de Moura	568931ccb1	refactor(library/tactic): remove duplicate code, add add_proofs Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-01 07:55:01 -08:00
Leonardo de Moura	f91c4901e8	feat(library/tactic): add absurd_tactic Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-01 07:55:00 -08:00
Leonardo de Moura	bf2adb20e7	feat(library/tactic): add disj_hyp_tactic Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-01 07:55:00 -08:00
Soonho Kong	6a6b69ddf4	test(library/rewriter): add test for depth RW	2013-12-01 01:59:21 -05:00
Soonho Kong	064e3fe20d	refactor(library/rewriter): rename lc => ti	2013-12-01 01:59:20 -05:00
Soonho Kong	506cca0ac1	feat(library/rewriter): implement depth RW	2013-12-01 01:59:20 -05:00
Soonho Kong	ae0508128f	refactor(library/rewriter): move apply_rewriter_fn into rewriter.h	2013-12-01 00:57:09 -05:00
Soonho Kong	d7ba5e3893	doc(library/rewriter): add doxygen annotations for rewrite_* funcs	2013-12-01 00:47:53 -05:00
Leonardo de Moura	1a221d8bbe	feat(library/tactic): add focus tactical Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-30 11:28:38 -08:00
Leonardo de Moura	7ff791eb9f	feat(util/name_set): add mk_unique (with respect to a name_set) Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-30 11:28:38 -08:00
Leonardo de Moura	6da13cc245	feat(util/list): map_append template Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-30 11:28:38 -08:00
Leonardo de Moura	fe79bbf2b7	feat(util/list): filter template Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-30 11:28:38 -08:00
Soonho Kong	f205dd0763	fix(library/rewriter): unused variable warnings	2013-11-30 07:05:18 -05:00
Leonardo de Moura	83aaf64318	fix(library/tactic): memory leaks Proof/Cex builders and tactics implemented in Lua had a "strong reference" to script_state. If they are stored in the Lua state, then we get a cyclic reference. That is, script_state points to these objects, and they point back to script_state. To avoid this memory leak, this commit defines a weak reference for script_state objects. The Proof/Cex builders and tactics now store a weak reference to the Lua state. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-30 00:44:39 -08:00
Leonardo de Moura	2372567a6e	fix(util/luaref): warnings produced by valgrind Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-30 00:34:38 -08:00
Leonardo de Moura	a7027a1d00	feat(library/tactic): polish tactic API, and add new example showing how to implement tactics using Lua Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-30 00:16:39 -08:00
Soonho Kong	aed8b1fc73	fix(tests/library/rewriter): app_rewriter1_tst There was a bug in the app_rewriter1_tst. If we apply the ADD_COMM RW to f(0), then the result should be f(0) since there is nothing to do for ADD_COMM. f(0) = f(0) The proof for this equality should be Refl(Nat, f(0)). But it was Refl(Nat -> Nat, f) which is wrong. Somehow, the previous kernel didn't detect this type mismatch and recent changes of the kernel found the problem. I fixed the bug and re-enable the test as it was.	2013-11-30 02:25:30 -05:00
Soonho Kong	f5f7380fbe	feat(library/rewriter): add apply_rewriter_fn which will be used in depth RW	2013-11-30 02:25:30 -05:00
Soonho Kong	1d76a6f71d	feat(library/rewriter): add rewrite_* functions rewrite_* functions take the rewriting results of the sub-components and construct the rewriting result for the main component. For instance, rewrite_app function takes env, ctx, and the value v s.t. v = (e_0 e_1 ... e_n) and the rewriting results for e_i's as a vector(buffer) (e'_0, pf_0 -- proof of e_0 = e'_0) (e'_1, pf_1 -- proof of e_1 = e'_1) ... (e'_n, pf_n -- proof of e_n = e'_n). Then rewrite_app function construct the new v' v' = (e'_0 e'_1 ... e'_n) and the proof of v = v' which is constructed with pf_i's. These functions are used in the component rewriters such as app_RW and let_type_RW, as well as more complicated rewriters such as depth rewriter.	2013-11-30 02:25:29 -05:00
Leonardo de Moura	a9eb2a9307	feat(kernel/builtin): add is_* functions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-29 11:35:58 -08:00
Leonardo de Moura	18eb9e427f	fix(library/tactic): compilation warning Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-29 10:35:14 -08:00
Leonardo de Moura	98897b467d	feat(frontends/lean/parser): add support for Lua expression code blocks In expression code blocks, we do not have to write a "return". After this commit, the argument of an apply command is a Lua expression instead of a Lua block of code. That is, we can now write apply ( REPEAT(ORELSE(imp_tactic, conj_tactic, conj_hyp_tactic, assumption_tactic)) ) instead of apply ( return REPEAT(ORELSE(imp_tactic, conj_tactic, conj_hyp_tactic, assumption_tactic)) ) Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-29 10:21:24 -08:00
Leonardo de Moura	f9874cd675	feat(library/tactic): add to_tactic_ext, it allows functions that return tactics to be used where a tactic is expected For example, after this commit, we can write simple_tac = REPEAT(ORELSE(imp_tactic, conj_tactic)) .. assumption_tactic instead of simple_tac = REPEAT(ORELSE(imp_tactic(), conj_tactic())) .. assumption_tactic() Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-29 09:40:21 -08:00
Leonardo de Moura	20a36e98ec	feat(library/elaborator): modify how elaborator handles constraints of the form ?M << P and P << ?M, where P is a proposition. Before this commit, the elaborator would only assign ?M <- P, if P was normalized. This is bad since normalization may "destroy" the structure of P. For example, consider the constraint [a : Bool; b : Bool; c : Bool] ⊢ ?M::1 ≺ implies a (implies b (and a b)) Before this, ?M::1 will not be assigned to the "implies-term" because the "implies-term" is not normalized yet. So, the elaborator would continue to process the constraint, and convert it into: [a : Bool; b : Bool; c : Bool] ⊢ ?M::1 ≺ if Bool a (if Bool b (if Bool (if Bool a (if Bool b false true) true) false true) true) true Now, ?M::1 is assigned to the term if Bool a (if Bool b (if Bool (if Bool a (if Bool b false true) true) false true) true) true This is bad, since the original structure was lost. This commit also contains an example that only works after the commit is applied. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-29 09:15:01 -08:00
Leonardo de Moura	066dacea31	feat(library/tactic): add show_tactic, and optional '.' in the end of tactic command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-29 01:33:26 -08:00
Leonardo de Moura	b3f87e2e4f	feat(library/tactic): make THEN, ORELSE, APPEND, PAR and INTERLEAVE nary combinators Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-28 22:11:07 -08:00
Leonardo de Moura	6832b265e9	style(frontends/lean/parse): missing include Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-28 21:50:55 -08:00
Leonardo de Moura	5dfb3b8b56	feat(frontends/lean/parse): allow script-code blocks to be used in the apply command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-28 21:48:30 -08:00
Leonardo de Moura	67def8da21	fix(library/type_inferer): typo Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-28 21:47:29 -08:00
Leonardo de Moura	dae86c2ffa	feat(frontends/lean/parser): add basic tactic support in the frontend Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-28 21:08:12 -08:00
Leonardo de Moura	73bbf67702	refactor(library/elaborator): simplify synthesizer interface Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-28 19:00:48 -08:00
Leonardo de Moura	c6b05bcfcb	feat(library/tactic): modify assumption_tactic, it should fail if not applicable, and TRY tactical Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-28 18:23:38 -08:00
Leonardo de Moura	e3f3ec5553	feat(library/tactic): expose conj_tactic, imp_tactic, conj_hyp_tactic in the Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-28 18:17:15 -08:00
Leonardo de Moura	d36a91e145	feat(library/tactic): expose COND and WHEN tacticals in Lua, add HOL-like tactical names Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-28 17:57:24 -08:00
Leonardo de Moura	ff052d41ee	chore(*): fix cygwin compilation errors Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-28 13:49:18 -08:00
Leonardo de Moura	ce674d2d43	feat(library/tactic): execute Lua tactics using coroutines This is very important when several Lua tactics are implemented in the same Lua State object. In this case, even if we use the par combinator, a Lua tactic will block the other Lua tactics running in the same Lua State object. With this commit, a Lua tactic can use yield to allow other tactics in the same State object to execute. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-28 13:09:33 -08:00
Leonardo de Moura	6cb8300076	doc(lua): add S-expression documentation Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-28 10:33:32 -08:00
Leonardo de Moura	09bc7ddf91	feat(library/tactic): add support for migratic tactic framework object between Lua states Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-28 08:03:05 -08:00
Leonardo de Moura	3dc7a856f0	refactor(library/tactic): use unprotect/protect idiom for callbacks in the tactic API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-27 18:11:46 -08:00
Leonardo de Moura	b4a8418d38	feat(library/tactic): expose tactics in the Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-27 17:47:29 -08:00
Leonardo de Moura	55f86f79a8	fix(util/optional): typo Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-27 16:57:29 -08:00
Leonardo de Moura	a2aa90ae66	refactor(util/script_state): replace std::recursive_mutex with std::mutex, and use unlock_guard The unlock_guard and exec_unprotected will be useful also for implementing the Lua tactic API. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-27 15:40:41 -08:00
Leonardo de Moura	b038636ff5	refactor(util/script_state): remove unsafe unguarded_apply Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-27 15:14:26 -08:00
Leonardo de Moura	75b4a96d0e	chore(tests/lua/threads): break lua thread tests into individual tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-27 15:06:07 -08:00
Leonardo de Moura	f7e8545e97	refactor(frontends/lua): rename leanlua_state to script_state, and move it to util This commit also minimizes the dependencies of script_state. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-27 14:57:36 -08:00
Leonardo de Moura	0934d7b2f4	fix(frontends/lua): make sure Lua 'sleep' function support interruption Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-27 13:25:06 -08:00
Leonardo de Moura	3a93212d5e	chore(kernel/expr): fix cpplint warning Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-27 12:59:16 -08:00
Leonardo de Moura	e737f501e4	fix(frontends/lua): remove unnecessary function reference Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-27 12:58:35 -08:00
Leonardo de Moura	262670abd6	fix(frontends/lua/leanlua_thread): propagate C++ thread over Lua thread boundaries Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-27 12:49:12 -08:00
Leonardo de Moura	d87ad9eb7e	refactor(util/lua): propagate C++ Lean exceptions in Lua The following call sequence is possible: C++ -> Lua -> C++ -> Lua -> C++ The first block of C++ is the Lean main function. The main function invokes the Lua interpreter. The Lua interpreter invokes a C++ Lean API. Then the Lean API invokes a callback implemented in Lua. The Lua callback invokes another Lean API. Now, suppose the Lean API throws an exception. We want the C++ exception to propagate over the mixed C++/Lua call stack. We use the clone/rethrow exception idiom to achieve this goal. Before this commit, the C++ exceptions were converted into strings using the method what(), and then they were propagated over the Lua stack using lua_error. A lua_error was then converted into a lua_exception when going back to C++. This solution was very unsatisfactory, since all C++ exceptions were being converted into a lua_exception, and consequently the structure of the exception was being lost. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-27 12:25:29 -08:00
Leonardo de Moura	a6f6f49b5f	refactor(frontends/lua): add lua_migrate_fn, and make copy_values modular copy_values is not a big if-then-else anymore. Before this change, whenever we added a new kind of userdata, we would have to update copy_values. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-27 10:32:19 -08:00
Leonardo de Moura	4c323093ac	refactor(frontends/lua/leanlua_state): minimize the use of 'friend' directive Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-27 09:25:56 -08:00
Leonardo de Moura	4c5ec53a44	chore(util/lua): remove dead code I removed lua_module helper class because it does not work. The problem is that the linker may eliminate ignore a object file that contains a lua_module global object used for initialization. When this happens, the associated Lua bindings will not be exposed in the Lua API. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-26 19:36:32 -08:00
Leonardo de Moura	feca9dbdf8	refactor(bindings/lua): move to frontends/lua Lua API is an integral part of Lean. It does not have the same status of external APIs (e.g., Python) we will add in the future. We will reserve the directory bindings for external APIs for using Lean as a library. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-26 19:30:07 -08:00
Leonardo de Moura	fb06a2b1df	refactor(bindings/lua/leanlua_state): cleanup Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-26 19:24:18 -08:00
Leonardo de Moura	956f203a55	refactor(bindings/lua): move Lua bindings to the file associated with them The directory bindings/lua was getting too big and had too many dependencies. Moreover, it was getting too painful to edit/maintain two different places. Now, the bindings for module X are in the directory that defines X. For example, the bindings for util/name.cpp are located at util/name.cpp. The only exception is the kernel. We do not want to inflate the kernel with Lua bindings. The bindings for the kernel classes are located at bindings/kernel_bindings. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-26 19:15:56 -08:00
Leonardo de Moura	99a811a586	feat(bindings/lua): expose io_state object in the Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-26 12:54:47 -08:00
Leonardo de Moura	861be072d8	feat(bindings/lua): add proof_state to Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-26 11:34:58 -08:00
Leonardo de Moura	4e66a2e14a	fix(library/tactic/goal): typo Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-26 11:34:58 -08:00
Leonardo de Moura	b41789d085	feat(kernel): add is_bool predicate Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-26 11:34:50 -08:00
Leonardo de Moura	fd3b9e39f6	feat(bindings/lua): add cex_builder to Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-26 09:17:57 -08:00
Leonardo de Moura	4d9075bdfd	feat(bindings/lua): add proof_map, assignment and proof_builder to Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-26 08:37:37 -08:00
Leonardo de Moura	3ebc099ec5	feat(bindings/lua/options): improve options Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-25 21:05:05 -08:00
Leonardo de Moura	feeb6d9105	feat(bindings/lua): add goal object to Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-25 20:51:47 -08:00
Leonardo de Moura	e29a2f4d11	chore(util/interrupt): improve comment Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-25 17:23:36 -08:00
Leonardo de Moura	4eb62fef91	fix(util/interrupt): fix nasty bug on interruptible_thread, it seems to occur only on cygwin Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-25 17:14:22 -08:00
Leonardo de Moura	c22f863114	refactor(library/tactic): improve solve method Now, it produces the following outcomes: 1- A proof 2- A counterexample 3- A list of (unsolved) final states Remark: the solve method does not check whether the proof or counterexample is correct. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-25 13:04:12 -08:00
Leonardo de Moura	9a8ea0c735	feat(library/tactic): add precision and counterexample builder to proof state Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-25 11:43:16 -08:00
Leonardo de Moura	ccaa272f9a	refactor(library/tactic): simplify proof_builder API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-25 10:50:33 -08:00
Leonardo de Moura	500ed7a05b	refactor(library/tactic): remove dead code, make proof_state a smart pointer, cleanup Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-25 10:39:40 -08:00
Leonardo de Moura	5af648030d	chore(memcheck.supp): hide another false positive at luajit Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-25 10:07:40 -08:00
Leonardo de Moura	2c65fdb346	refactor(library/tactic): cleanup Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-25 01:06:34 -08:00
Soonho Kong	03791b099c	chore(ctest): fix typo in CTEST_DROP_LOCATION	2013-11-25 03:14:35 -05:00
Soonho Kong	ac5a061f2a	chore(ctest): use CDash server located at borel.modck.cs.cmu.edu	2013-11-25 02:48:04 -05:00
Leonardo de Moura	9dcfa03dd2	feat(library/tactic): add conj_hyp_tactic Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-24 21:00:38 -08:00
Leonardo de Moura	d75bd2ae98	feat(library/tactic/proof_state): remove goal name when pretty printing the proof state Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-24 20:22:47 -08:00
Leonardo de Moura	48d7afb0e8	feat(library/tactic): add trace_state_tactic Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-24 16:44:02 -08:00
Leonardo de Moura	6f05276acd	refactor(library/tactic): remove unnecessary tactic_exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-24 16:31:49 -08:00
Leonardo de Moura	9c42a05b08	feat(library/tactic): add conj_tactic and imp_tactic Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-24 16:29:04 -08:00
Leonardo de Moura	1c607f3350	feat(library/tactic): add cond and when tacticals. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-24 12:04:32 -08:00
Leonardo de Moura	40d612eca0	feat(library/tactic): add repeat1 and determ tacticals Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-24 11:38:51 -08:00
Leonardo de Moura	cb7a5288c5	refactor(library/tactic): minimize the amount of copying in the tactic API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-24 11:27:06 -08:00
Leonardo de Moura	22c49146ae	feat(library/tactic): refine repeat and repeat_at_most tacticals Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-24 11:18:32 -08:00
Leonardo de Moura	8e87ef5da8	feat(util/lazy_list): add repeat and repeat_at_most templates for lazy_lists Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-24 11:16:37 -08:00
Leonardo de Moura	e839787b74	refactor(library/tactic): cleanup Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-24 00:38:52 -08:00
Leonardo de Moura	b74aeb1216	fix(util/lazy_list): par template missing case Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-24 00:38:31 -08:00
Leonardo de Moura	4e24dfd5a6	fix(util/optional): move constructor Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-24 00:22:02 -08:00
Leonardo de Moura	40a2f0a588	refactor(util/lazy_list): polish lazy_list API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-23 17:45:01 -08:00
Leonardo de Moura	9da95dc6e6	style(library/tactic): missing include Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-23 17:06:00 -08:00
Leonardo de Moura	bcd88cac08	style(util): missing includes Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-23 17:05:46 -08:00
Leonardo de Moura	16cf60a04b	refactor(library/tactic): modify par and try_for tactics Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-23 17:03:59 -08:00
Leonardo de Moura	924187b055	feat(util/lazy_list): add par template for lazy lists) Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-23 16:51:17 -08:00
Leonardo de Moura	157a2b36db	feat(lazy_list): add timeout template for lazy_lists Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-23 16:27:36 -08:00
Leonardo de Moura	cb3c685fb1	feat(util/lazy_list): check for interruption between pulls Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-23 15:54:32 -08:00
Leonardo de Moura	d1adfd52e6	feat(library/tactic): add mk_simple_tactic template Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-23 15:53:45 -08:00
Leonardo de Moura	f19944cf09	refactor(util/lazy_list): 'lazier' lazy_lists In the new implementation, even the head of the lazy list is computed on demand. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-23 15:33:30 -08:00
Leonardo de Moura	9eb6da2a31	feat(util): add optional template Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-23 13:27:22 -08:00
Leonardo de Moura	18d114416f	feat(library/tactic): add take and force tacticals Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-22 17:05:18 -08:00
Leonardo de Moura	d258a4b7b8	feat(library/tactic): add repeat and repeat_at_most tacticals Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-22 16:39:25 -08:00
Leonardo de Moura	8bece1b53d	feat(library/tactic): add append, interleave and par tacticals Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-22 16:15:03 -08:00
Leonardo de Moura	df96068caa	fix(library/tactic): clean up try_for Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-22 15:51:17 -08:00
Leonardo de Moura	9fd594533d	refactor(library/tactic): simplify tactic framework, add orelse and try_for combinators/tacticals Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-22 15:46:43 -08:00
Leonardo de Moura	a776c8b158	feat(util/interrupt): add sleep_for, and simplify request_interrupt The Lean sleep_for checks the interrupt flag from time to time. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-22 11:32:12 -08:00
Leonardo de Moura	935349ec91	fix(tests/util/thread): typo Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-22 10:23:20 -08:00
Leonardo de Moura	1f225d2752	feat(util/lazy_list): add useful lazy_list function templates Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-22 09:40:56 -08:00
Leonardo de Moura	796fb3c3bf	refactor(library/tactic): remove justification_builder Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-21 17:29:06 -08:00
Leonardo de Moura	41062fdf9f	feat(library/tactic): add pretty printer for goal and proof_state objects, add solve method for tactics, add trivial example Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-21 17:29:06 -08:00
Leonardo de Moura	28a56e3acf	fix(kernel/expr_eq): the cached type should ignored when comparing expressions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-21 17:29:06 -08:00
Leonardo de Moura	5346b67651	refactor(library/state): rename Lean state object to io_state The idea is to make it clear that io_state is distinguish it from proof_state, and from leanlua_state. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-21 17:29:06 -08:00
Leonardo de Moura	680ec8abba	refactor(library/tactic): reorganize tactic API, add assumption_tactic Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-21 17:29:06 -08:00
Leonardo de Moura	ca74d069b9	feat(util/interrupt): reset interrupt flag before throwing exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-21 17:29:06 -08:00
Leonardo de Moura	8515821d56	feat(util/list): add map_filter template Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-21 17:29:06 -08:00
Leonardo de Moura	f6bfd11aed	chore(util/list_fn): fix typo Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-21 17:29:06 -08:00
Leonardo de Moura	df04dbe096	chore(util): use && when appropriate Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-21 17:29:06 -08:00
Leonardo de Moura	63bbf07f64	feat(library/tactic): add 'idtac' tactic and 'then' tactical Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-21 17:29:06 -08:00
Leonardo de Moura	a03841c18b	feat(tactic): refine tactic API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-21 17:29:06 -08:00
Leonardo de Moura	367108edfa	fix(library/tactic): compilation problem reported by clang++ Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-21 08:53:37 -08:00
Leonardo de Moura	f6d1f4db60	chore(library/tactic): remove trash Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-20 17:25:00 -08:00
Leonardo de Moura	3a6aa2dc75	feat(library/tactic): add tactic framework APIs Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-20 17:19:05 -08:00
Leonardo de Moura	be8fe1b902	fix(kernel/replace): make it more robust, and add clear method Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-20 13:19:21 -08:00
Leonardo de Moura	87eb254a1a	fix(tests/util/thread): incorrect unit test Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-20 11:28:19 -08:00
Leonardo de Moura	b0a4d60174	fix(util/interval): add missing explicit template instantiation Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-20 09:56:19 -08:00
Leonardo de Moura	a3a90f8e69	feat(shell): add command line options Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-19 19:30:39 -08:00
Leonardo de Moura	eba31a0516	test(util/interval): add more tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-19 19:07:09 -08:00
Leonardo de Moura	7b8bd97699	feat(lua/expr): add method for extracting semantic attachment data Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-19 19:06:47 -08:00
Leonardo de Moura	f78cf6a415	feat(shell): add getopt Let travis find out which platforms support it Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-19 17:04:55 -08:00
Leonardo de Moura	a98fdd9be6	refactor(shell): combine lean and leanlua executables in a single executable The main motivation is to allow users to configure/extend Lean using .lua files before loading the actual .lean files. Example: ./lean extension1.lua extension2.lua file.lean Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-19 16:48:21 -08:00
Leonardo de Moura	2265ef78c4	feat(util/list): add emplace_front Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-19 16:27:31 -08:00
Leonardo de Moura	20c6789d1c	feat(extra): add extension that demonstrates how to parse 'templates' Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-19 15:56:44 -08:00
Leonardo de Moura	6989f1f9ba	refactor(kernel/metavar): remove unnecessary variable Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-19 14:41:54 -08:00
Leonardo de Moura	0126fa0499	refactor(kernel): add find_fn, replace for_each_fn with find_fn when appropriate, remove unnecessary function has_cached_type Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-19 13:03:46 -08:00
Leonardo de Moura	5cfcb7e144	chore(kernel/for_each): use consistent naming convetions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-19 11:24:02 -08:00
Leonardo de Moura	7f088b7635	feat(kernel): add (optional) field m_type to expr_const, this field is useful for implementing the tactic framework This field should not be visible in the external API. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-19 11:21:52 -08:00
Leonardo de Moura	9bafa5a9e8	chore(memcheck): suppress memory leak at awk Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-18 23:50:41 -08:00
Leonardo de Moura	57bf4f3e67	feat(kernel/expr): avoid recursion when deleting expressions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-18 18:41:08 -08:00
Leonardo de Moura	2951c92ad1	feat(kernel/for_each): avoid recursion at for_each template It saves a lot of stack space. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-18 18:08:31 -08:00
Leonardo de Moura	e10d17a0f4	feat(util/sexpr): avoid recursion when destructing sexpr's Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-18 17:46:53 -08:00
Leonardo de Moura	64379a5a10	perf(util/list): use buffer of cells instead of buffer of T T may be a big object. We minimize the ammount of copying using buffer of (pointers to) cells. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-18 17:12:02 -08:00
Leonardo de Moura	76252816ac	perf(util/list): avoid recursion in map and destructor Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-18 16:47:52 -08:00
Leonardo de Moura	d67bf995ed	feat(util/list): avoid recursion at for_each template Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-18 15:52:31 -08:00
Leonardo de Moura	06c004aa75	fix(build): typo Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-18 15:36:07 -08:00
Leonardo de Moura	adf4856f88	feat(util/list): add map_reuse template Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-18 15:32:02 -08:00
Soonho Kong	20756c382c	test(*): split leantests, leanslowtests, leanluatests, leanluadocs into singletons	2013-11-18 18:27:11 -05:00
Leonardo de Moura	53dc8c8c57	test(util/shared_mutex): add missing tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-18 14:03:18 -08:00
Leonardo de Moura	88b2feff6f	test(doc/lua): add script for validating examples in the Lua API documentation Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-18 12:49:57 -08:00
Leonardo de Moura	4d1d3d7cc7	fix(build): cygwin also needs the LEAN_WINDOWS flag Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-18 12:40:02 -08:00
Leonardo de Moura	bfc4023a9e	fix(tests/kernel/expr): remove unused function Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-18 10:09:47 -08:00
Leonardo de Moura	80fccc5533	fix(util/realpath): style Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-18 09:55:16 -08:00
Leonardo de Moura	e0c23e5984	fix(kernel/environment): compilation problem on Windows Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-18 09:52:47 -08:00
Leonardo de Moura	b2d1acd0b7	test(lua/environment): add missing tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-18 09:27:46 -08:00
Leonardo de Moura	1315378ebb	test(*): add missing tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-18 09:13:34 -08:00
Leonardo de Moura	93b02a6fad	fix(lua): fix C++ stack unwinding bug, we should never invoke lua_error from a catch block lua_error and luaL_error are based on the longjmp C function. They will not correctly unwind the C++ stack. We should only invoke them after we finished handling the C++ exceptions and unwinding the C++ stack, and invoking the destructors for each object living on the stack. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-18 06:49:54 -08:00
Leonardo de Moura	2ccd5cc559	fix(lua): workaround memory leak problem with __cxa_thread_atexit code generated by g++ Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-18 06:40:32 -08:00
Leonardo de Moura	7976937e4c	test(lua/metavar_env): add missing tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-17 19:18:47 -08:00
Leonardo de Moura	69be5f6c94	feat(kernel/environment): track which modules were already imported Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-17 18:15:44 -08:00
Leonardo de Moura	5254dba195	test(library/update_expr): add missing tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-17 13:36:15 -08:00
Leonardo de Moura	df94e44806	test(lua/expr): add missing tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-17 11:46:24 -08:00
Leonardo de Moura	f586e58ac3	test(lua/justification): add more tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-17 11:13:10 -08:00
Leonardo de Moura	d0bac61e74	fix(lua/numerics): bug in bindings, add more tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-17 11:02:44 -08:00
Leonardo de Moura	0e6df0a55b	fix(lua): warning message Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-16 19:58:34 -08:00
Leonardo de Moura	926ed0a02d	feat(lua): add type_inferer object to Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-16 19:18:15 -08:00
Leonardo de Moura	4ebb3c572a	feat(kernel/environment): make the environment throw an exception when weak-ref has expired Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-16 18:35:17 -08:00
Leonardo de Moura	590b14570f	feat(lua): improve error handling in Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-16 18:21:42 -08:00
Leonardo de Moura	516c5c8fea	feat(lua): add metavar_env objects to Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-16 14:44:33 -08:00
Leonardo de Moura	c8fff45319	feat(lua): add justification objects to Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-16 11:12:58 -08:00
Leonardo de Moura	9398ea5a59	feat(util/shared_mutex): add support for recursive lock at shared_mutex We need support for recursive locks. The main user of this class is the environment object. This commit adds a test that demonstrates that the shared_lock of the environment object may be recursively requested. Before this fix, the Lean was deadlocking in this example. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-15 22:01:11 -08:00
Leonardo de Moura	209a2d10f7	fix(lua): replace std::mutex with std::recursive_mutex, add test that demonstrates the problem that is being fixed Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-15 21:26:16 -08:00
Leonardo de Moura	8525e8534b	feat(lua): expose parse_expr and parse_commands from frontends/lean in the Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-15 16:11:26 -08:00
Leonardo de Moura	d9d9c05e4f	refactor(lua/options): remove unnecessary function Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-15 12:53:27 -08:00
Leonardo de Moura	19533c811b	feat(library/script_evaluator): add abstract class that exposes only the API needed by frontend objects The main motivation is to break the remove the dependency frontends/lean <-- bindings/lua. This dependency is undesirable because we want to expose the frontends/lean parser and pretty printer objects at bindings/lua. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-15 12:13:09 -08:00
Leonardo de Moura	1cb0262ec5	chore(memcheck): make the suppression entries for LuaJIT more general Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-15 11:34:50 -08:00
Leonardo de Moura	e7552d35e0	chore(memcheck): hide another tcmalloc bug Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-15 11:33:34 -08:00
Leonardo de Moura	a74412963a	chore(build): only execute lua multi-threading tests when on cygwin or linux, and using g++ Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-15 09:27:58 -08:00
Leonardo de Moura	782335581b	fix(lua/thread): uninitialized memory Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-15 09:07:18 -08:00
Leonardo de Moura	b5dcb93550	feat(lua): communication channels for threads Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-14 21:10:46 -08:00
Leonardo de Moura	bd1e9c7548	feat(lua): throw an exception if the user tries to create a thread and Lean was compiled without multi-threading support Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-14 19:06:36 -08:00
Leonardo de Moura	3a924a5fb1	perf(lua/name): improve to_name_ext performance Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-14 18:06:09 -08:00
Leonardo de Moura	cd6bd79d63	refactor(lua): cleanup Lua API, improve performance Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-14 17:33:46 -08:00
Leonardo de Moura	6575566f9f	fix(lua): rename lua_ref to lref, lua_ref is a macro in LuaJIT Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-14 15:50:56 -08:00
Leonardo de Moura	09bed4786c	feat(lua): add semantic attachments for builtin arithmetical values to Lua API, improve mk_constant Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-14 15:15:04 -08:00
Leonardo de Moura	05f254f605	refactor(lua): move lua_ref to separate file Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-14 14:41:54 -08:00
Leonardo de Moura	bdea42b2a9	style(lua): ignore bogus warning Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-14 14:13:06 -08:00
Leonardo de Moura	abe93dfec0	fix(lua/splay_tree): for_each method was crashing if the map was updated during for_each Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-14 13:48:23 -08:00
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	8e56726116	fix(library/expr_lt): fix bug when using hash codes Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-14 13:18:33 -08:00
Leonardo de Moura	b0322787ff	feat(lua): add has_metavar method Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-14 10:28:50 -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	6e0fc0ca9b	chore(build): include dl.so when compiling on Linux Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-13 18:44:28 -08:00
Leonardo de Moura	6964e374c0	fix(lua): luajit incompatibility Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-13 18:08:00 -08:00
Leonardo de Moura	cbc4254ff5	feat(lua): add occurs method to expr Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-13 17:10:09 -08:00
Leonardo de Moura	ad1180c5b4	fix(kernel/occurs): typos Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-13 17:04:56 -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	eacd60de9c	feat(frontends/lean): return the operator associated with constant expressions that are names of builtin values Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-13 16:08:21 -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	ba0889265e	refactor(lua): cleanup Lua bindings Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-13 13:55:05 -08:00
Leonardo de Moura	b5f0185729	fix(lua): replace lua_pushfstring with lua_pushstring Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-13 12:14:55 -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	e2efce6b62	style(util/sexpr): name convetion for enumeration types Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-13 11:50:12 -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	c4c548dc5d	feat(*): simplify interrupt propagation Instead of having m_interrupted flags in several components. We use a thread_local global variable. The new approach is much simpler to get right since there is no risk of "forgetting" to propagate the set_interrupt method to sub-components. The plan is to support set_interrupt methods and m_interrupted flags only in tactic objects. We need to support them in tactics and tacticals because we want to implement combinators/tacticals such as (try_for T M) that fails if tactic T does not finish in M ms. For example, consider the tactic: try-for (T1 ORELSE T2) 5 It tries the tactic (T1 ORELSE T2) for 5ms. Thus, if T1 does not finish after 5ms an interrupt request is sent, and T1 is interrupted. Now, if you do not have a m_interrupted flag marking each tactic, the ORELSE combinator will try T2. The set_interrupt method for ORELSE tactical should turn on the m_interrupted flag. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-12 21:45:48 -08:00
Leonardo de Moura	b31233e8c2	feat(util/interrupt): restore interrupt module Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-12 21:16:10 -08:00
Leonardo de Moura	126c45626c	chore(memcheck.supp): add suppressions for LuaJIT bugs Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-12 18:52:03 -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	0a6f622aec	chore(build): remove CheckLuaObjlen, it is easier to check the Lua version Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-12 12:58:22 -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	c46edcf370	feat(lua): expose formatter in the Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-12 11:19:15 -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	7cb15cdac5	feat(lua): allow environment object references to be moved between Lua states Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-11 20:32:36 -08:00
Leonardo de Moura	ac6c18321a	fix(lua): make sure environment objects can be safely accessed/updated from current threads Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-11 20:29:53 -08:00
Leonardo de Moura	596e4aeb57	feat(util/shared_mutex): add shared_mutex object, this is a temporary replacement for std::shared_mutex that will be available in C++11 Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-11 20:00:21 -08:00
Leonardo de Moura	cc7b5b7e50	fix(lua): disable custom allocation for Lua, it is crashing Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-11 18:20:52 -08:00
Leonardo de Moura	7d49df3985	style(lua): fix cpplint.py warnings Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-11 17:46:39 -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	f158b0b311	fix(util/memory): make sure realloc behaves like free when sz == 0 Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-11 13:42:22 -08:00
Leonardo de Moura	7cc6c35eee	feat(lua/name): add hash method to name objects Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-11 13:32:56 -08:00
Leonardo de Moura	8dd85ebc15	fix(lua): typos and a bug in the expr Lua bindings Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-11 13:11:06 -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	31abc00db8	chore(*): add LCOV_EXCL_LINE to lean_unreachable statements Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-11 09:19:38 -08:00
Leonardo de Moura	dbdb9a41af	style(lua): use C++-style cast Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-10 11:14:04 -08:00
Leonardo de Moura	7683188ab0	chore(emplace_back): use emplace_back when appropriate Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-10 11:14:04 -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	119e0ba5e6	feat(lua): add to_nonnull_expr 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
Soonho Kong	1cf037f11e	chore(cmake): do not delete coverage.info.cleaned which will be used for coveralls.io	2013-11-09 22:19:08 -05:00
Leonardo de Moura	6b71fb346c	fix(lua): add missing files for local_context Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-09 12:47:52 -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	183080294b	fix(cmake/Modules/CheckLuaNewstate.cc): compilation problem on cygwin Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-09 12:18:20 -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
Soonho Kong	d4dbc18404	chore(cmake/Modules/FindLua): disable TRY_RUN in cross-compilation.	2013-11-08 18:04:55 -05:00
Leonardo de Moura	bbab454b6c	fix(lua): cpplint.py does not like multiline strings Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-08 13:27:20 -08:00
Leonardo de Moura	ec56ba72ea	fix(lua): cygwing compilation problem Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-08 13:27:20 -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	b7d8391306	refactor(lua): remove duplicate code, separate lua_exception, add missing #pragma once Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-08 11:59:47 -08:00
Leonardo de Moura	c8b0c10c88	refactor(lua): make Lua a required (non-optional) package Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-08 10:56:29 -08:00
Leonardo de Moura	c5207489fd	fix(memory): realloc must behave like malloc when ptr is nullptr Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-08 10:31:57 -08:00
Leonardo de Moura	a10aa0880f	fix(build): add CheckLuaObjlen.cc test, not every Lua version has the function lua_objlen Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-08 08:26:04 -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	fb09fc9fe6	feat(lua): add set_global_function template, and to_name_ext function Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-07 21:54:57 -08:00
Leonardo de Moura	db8b16641c	chore(build): check if the Lua installed in the system supports lua_newstate 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	6f432b4094	feat(lua): make Lua use our malloc/realloc, catch error when initializing Lua Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-07 15:52:39 -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	ff16ffaea3	fix(kernel/environment): warning produced by clang Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-07 11:36:08 -08:00
Leonardo de Moura	8012c4f644	fix(kernel/environment): add weak reference to environment objects We need weak references to environment objects because the environment has a reference to the type_checker and the type_checker has a reference back to the environment. Before, we were breaking the cycle using an "environment const &". This was a dangerous hack because the environment smart pointer passed to the type_checker could be on the stack. The weak_ref is much safer. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-07 11:29:08 -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	2141ee12f4	refactor(frontends/lean): use extension objects to store lean default frontend data in the environment Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-07 10:00:12 -08:00
Leonardo de Moura	80e23f98c7	feat(kernel/environment): add environment extension objects, the environment can be extended with frontend specific objects Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-06 19:22:30 -08:00
Soonho Kong	c5fd828a71	chore(cmake): switch the ordering between gmp and mpfr	2013-11-05 19:31:10 -05:00
Leonardo de Moura	e7d508043b	fix(lua/numerics): errors when cross-compiling for Windows Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-05 13:35:34 -08:00
Leonardo de Moura	40fde1a69c	test(lua): invoke Lua binding tests from ctest Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-05 13:17:10 -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	055cc7f957	fix(lua): make testudata compatible with Lua 5.1 Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-05 11:35:09 -08:00
Leonardo de Moura	5a01f167df	fix(lua): expose missing functions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-04 21:33:33 -08:00
Leonardo de Moura	0ac8f2d8d9	feat(lua/sexpr): improve sexpr Lua bindings Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-04 21:28:17 -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	1e12ddc7a9	refactor(lua): add goodies for accessing Lean values on the Lua stack Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-04 19:45:15 -08:00
Leonardo de Moura	47c289a24b	refactor(lua/name): improve name bindings for Lua Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-04 18:48:21 -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	f488e6bbfc	fix(lua): safe_function_wrapper Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-04 18:12:53 -08:00
Leonardo de Moura	92b2591a6f	style(lua): add missing include Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-04 16:29:47 -08:00
Leonardo de Moura	32d3990fc7	fix(lua): problem when compiling with clang++ Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-04 15:05:04 -08:00
Leonardo de Moura	0579970fc5	feat(lua): expose options object in the Lua bindings Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-04 14:38:49 -08:00
Leonardo de Moura	543aea65c9	chore(lua): rename init_* functions to open_* Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-04 13:54:51 -08:00
Leonardo de Moura	fd7e85f0bb	feat(lua): add safe_function template that catches Lean and C++ exceptions and convert them into Lua errors I'm using the approach described at: http://stackoverflow.com/questions/4615890/how-to-handle-c-exceptions-when-calling-functions-from-lua BTW, in some Lua versions, the C++ exceptions are correctly propagated. I think we should not rely on features of particular implementations. For example, LuaJIT does not propagate C++ exceptions. Whenever an exception is thrown from C++ code invoked from LuaJit, LuaJit interrupts the execution and converts it to an error "C++ exception". On the other hand, Lua 5.2 PUC-Rio interpreter (for Ubuntu) seem to propagate the C++ exceptions. The template safe_function solves the issue. It will also produce a Lua error whenever the function being wrapped throws an exception. The error message is based on the "what()" method. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-03 14:42:57 -08:00
Leonardo de Moura	1a734979b4	fix(shell/lua): catch lean exceptions in the leanlua frontend Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-03 13:46:15 -08:00
Leonardo de Moura	6f2183fafe	feat(FindLua.cmake): search also for LuaJit Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-03 13:45:23 -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	df7dbe17b5	feat(lua/util): remove dependency on luaL_setfuncs Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-03 12:16:23 -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
Soonho Kong	88ebdbcfb6	fix(shell/lua): move "#include<iostream>"	2013-11-03 13:25:33 -05:00
Soonho Kong	a9d55bf036	fix(lua): use updated FindLua and check version 5.2	2013-11-03 13:24:46 -05:00
Soonho Kong	044813615e	fix: add '#include <tuple>'	2013-11-03 13:00:42 -05:00
Soonho Kong	0d0d0cd533	chore(cmake): add gmp/mpfr include paths to cmakelists.txt	2013-11-03 13:00:42 -05:00
Leonardo de Moura	ccd95a9b66	fix(lua/name): fix memory leak Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-02 20:57:41 -07: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	1b9cf816c4	fix(lua): mark package as optional Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-02 11:43:23 -07:00
Leonardo de Moura	ac08e244a6	feat(lua): add Lua support to build Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-02 11:16:30 -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	fdea8aba10	feat(frontends/lean/scanner): allow '#' to be used in class B identifiers Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-01 08:42:25 -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	7fc87faa8f	feat(kernel): heterogeneous transitivity axiom, we need this axiom to be able to generate modular proofs in the rewriting engine module Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-29 17:07:30 -07:00
Leonardo de Moura	a57ca284ec	fix(tests/library/elaborator): replace eq with my_eq because eq is now a builtin symbol Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-29 17:06:32 -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	577ca128a1	fix(library/elaborator): add missing conflict justification Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-29 03:01:17 -07:00
Leonardo de Moura	521fa1ddb8	style(kernel/metavar): add missing includes Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-29 03:00:43 -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	5f11392fcc	test(numerics/numeric_traits): add missing test Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-28 07:50:33 -07:00
Leonardo de Moura	1d18f60dd5	fix(numerics): add missing numeric_traits<float>::zero() Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-28 07:47:23 -07:00
Leonardo de Moura	b16a64f44b	fix(library/elaborator): missing normalization step for semantic attachments Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-28 07:42:14 -07:00
Leonardo de Moura	4564bfa1d3	feat(library/elaborator): improve simple_ho_match Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-27 11:17:03 -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	92f5a31976	feat(kernel/expr): add new mk_app template for creating applications using a collection Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-27 08:53:58 -07:00
Leonardo de Moura	eaccdcb558	refactor(assumption_justification): move to the kernel Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-26 14:21:29 -07:00
Leonardo de Moura	4bed9f85b0	feat(kernel/for_each): add option for disabling cache of atomic expressions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-25 15:25:17 -07:00
Leonardo de Moura	ce10bfeaf6	perf(kernel/metavar): improve performance of has_assigned_metavar by avoiding for_each+exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-25 15:19:59 -07:00
Leonardo de Moura	57d9d23bd4	feat(kernel/for_each): allow function F to interrupt for_each search Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-25 14:58:02 -07:00
Leonardo de Moura	2dd44bdf1a	perf(kernel/for_each): delay initialization of visited set Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-25 14:52:08 -07:00
Leonardo de Moura	e765105ea5	fix(frontends/lean/pp): let expressions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-25 12:30:39 -07:00
Leonardo de Moura	c3c66b6c90	feat(make): add THREAD_SAFE build option Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-25 11:50:35 -07:00
Leonardo de Moura	c53d559f7f	perf(library/elaborator): improve process_metavar Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-25 11:19:17 -07:00
Leonardo de Moura	471bbd4040	refactor(kernel/metavar): combine several splay_trees (at metavar_env) into a single one Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-25 11:02:19 -07:00
Leonardo de Moura	5e34f410b3	refactor(splay_map): modify splay_find signature Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-25 10:47:15 -07:00
Leonardo de Moura	5812dfcf44	perf(kernel/justification): remove cache from depends_on Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-25 10:26:05 -07:00
Leonardo de Moura	2b5c951de3	perf(name): add quick_cmp for hierarchical names It first compare names using hash codes. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-25 09:58:06 -07:00
Leonardo de Moura	66f4834dbc	perf(kernel/metavar): add quick test that catches many cases Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-25 09:24:01 -07:00
Leonardo de Moura	f38178311c	perf(kernel/expr_eq): delay hashtable initialization Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-25 09:21:47 -07:00
Leonardo de Moura	e0ca27bfb3	fix(tests/library/rewriter): warning Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-25 08:33:53 -07:00
Leonardo de Moura	412bc792c9	fix(style): missing include Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-25 08:10:28 -07:00
Leonardo de Moura	0c21f45292	fix(kernel/unification_constraint): memory leak Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-25 08:06:21 -07:00
Leonardo de Moura	f0e149d77b	fix(frontends/lean/pp): fix how Type expressions are pretty printed Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-24 20:02:34 -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	83907d7c73	fix(elaborator): max constraints elaborator was not handling max constraints where one of the arguments was a Bool. Example: ctx \|- max(Bool, Type) == ?M Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-24 19:27:57 -07:00
Leonardo de Moura	65a514ad8a	fix(frontends/lean/parser): option propagation Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-24 19:04:06 -07:00
Leonardo de Moura	576b4e2169	fix(frontends/lean/pp): missing comma when printing contexts Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-24 19:00:24 -07:00
Leonardo de Moura	df07a84d11	feat(frontends/lean/parser): display elaborator error messages Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-24 18:48:53 -07:00
Leonardo de Moura	ca6a6d71e5	fix(kernel/printer): bug when printing let expression Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-24 18:05:23 -07:00
Leonardo de Moura	e3efe39eeb	fix(elaborator): fix bug in higher-order matching/unification Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-24 17:53:37 -07:00
Leonardo de Moura	d1a2a4ea7e	feat(frontends/lean/elaborator): add support for coercions in let declarations Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-24 17:01:06 -07:00
Leonardo de Moura	872b698bc3	feat(elaborator): add option m_assume_injectivity for getting more concise solutions We may miss solutions, but the solutions found are much more readable. For example, without this option, for elaboration problem Theorem Example4 (a b c d e : N) (H: (a = b ∧ b = e ∧ b = c) ∨ (a = d ∧ d = c)) : (h a c) = (h c a) := DisjCases H (fun H1 : _, let AeqC := Trans (Conjunct1 H1) (Conjunct2 (Conjunct2 H1)) in CongrH AeqC (Symm AeqC)) (fun H1 : _, let AeqC := Trans (Conjunct1 H1) (Conjunct2 H1) in CongrH AeqC (Symm AeqC)) the elaborator generates Theorem Example4 (a b c d e : N) (H : a = b ∧ b = e ∧ b = c ∨ a = d ∧ d = c) : (h a c) = (h c a) := DisjCases H (λ H1 : if Bool (if Bool (a = b) (if Bool (if Bool (if Bool (b = e) (if Bool (b = c) ⊥ ⊤) ⊤) ⊥ ⊤) ⊥ ⊤) ⊤) ⊥ ⊤, let AeqC := Trans (Conjunct1 H1) (Conjunct2 (Conjunct2 H1)) in CongrH AeqC (Symm AeqC)) (λ H1 : if Bool (if Bool (a = d) (if Bool (d = c) ⊥ ⊤) ⊤) ⊥ ⊤, let AeqC := Trans (Conjunct1 H1) (Conjunct2 H1) in CongrH AeqC (Symm AeqC)) The solution is correct, but it is not very readable. The problem is that the elaborator expands the definitions of \/ and /\. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-24 16:47:50 -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	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	c9f7b8bce2	feat(frontends/lean): add get_coercions method Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-24 14:38:09 -07:00
Leonardo de Moura	71ccec5b9e	refactor(frontends/lean/elaborator): delete old_elaborator, and create frontend_elaborator class that will be based on library/elaborator/elaborator Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-24 10:45:59 -07:00
Leonardo de Moura	449454efdb	fix(debug): remove typeid information from assertion, the names are mangled and are not very useful Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-23 16:41:51 -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	873e56844a	refactor(beta_reduction): add function apply_beta Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-23 16:03:52 -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	c1e451151a	feat(replace_visitor): add an abstract class for applying transformations on expressions I also removed replace_using_ctx since it is subsumed by the new class. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-23 15:01:37 -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	17b48010b7	fix(unification_constraint): fix printer for max constraints Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-23 12:00:29 -07:00
Leonardo de Moura	274b11530f	feat(metavar): improve apply_local_context Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-23 11:59:36 -07:00
Leonardo de Moura	b57f492e2d	fix(kernel/printer): improve printer for Type expressions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-23 11:58:49 -07:00
Leonardo de Moura	c635c16637	refactor(ho_unifier): remove ho_unifier, it has been subsumed by the elaborator class Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-22 17:51:54 -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	80a507cf45	refactor(tests/frontends/lean/implicit_args): remove implicit_args unit tests from frontends/lean, all tests were moved to tests/library/elaborator Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-22 16:42:07 -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	891d22b3de	feat(kernel/context): add method for remove context entries at positions [s, s+n). Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-22 15:52:24 -07:00
Leonardo de Moura	3fa4eac4ef	fix(replace_using_ctx_fn): typo Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-22 15:46:11 -07:00
Leonardo de Moura	8142726923	fix(type_inferer): bug when inferring the type of free variables Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-22 15:41:22 -07:00
Leonardo de Moura	874f67c605	feat(normalizer): remove normalization rule t == t ==> true This normalization rule is not really a computational rule. It is essentially encoding the reflexivity axiom as computation. It can also be abaused. For example, with this rule, the following definition is valid: Theorem Th : a = a := Refl b Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-22 14:02:48 -07:00
Leonardo de Moura	5e61496381	test(elaborator): add more tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-22 13:45:20 -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	c3e87f106f	fix(kernel/trace): fix typo in depends_on Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-22 08:15:37 -07:00
Leonardo de Moura	dc51d35dc0	feat(library/type_inferer): add support for metavariables at type_inferer 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	8663ac550f	feat(kernel/trace): add function depends_on for trace objects Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-22 08:15:36 -07:00
Leonardo de Moura	42edc4a72d	test(set): add set of pointers test 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
Leonardo de Moura	827c65b5e9	feat(kernel): add static_assert for update_metavar Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-22 08:15:36 -07:00
Leonardo de Moura	61ccaf741c	fix(frontend/lean): minor modification to be able to execute lean frontend while refactoring elaborator Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-22 08:15:36 -07:00
Leonardo de Moura	7cf83800c0	refactor(metavar): implement metavar_env, and use unification_constraint and trace objects in the type_checker, light_checker Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-22 08:15:36 -07:00
Leonardo de Moura	1f0eab7a14	test(type_checker): add new tests for type_checker trace objects Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-22 08:15:36 -07:00
Leonardo de Moura	fc288929a2	feat(type_checker): add trace objects to justify constraints created by the type checker Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-22 08:15:36 -07:00
Leonardo de Moura	5b1b03bafd	refactor(is_convertible): move from normalizer to type_checker class Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-22 08:15:36 -07:00
Leonardo de Moura	85bfa45e6a	refactor(kernel_exception): delete kernel_exception_formatter, and implement kernel_exception pretty printer as a virtual method Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-22 08:15:36 -07:00
Leonardo de Moura	d843d432d3	refactor(kernel): move printer and formatter objects to the kernel The printer and formatter objects are not trusted code. We moved them to the kernel to be able to provide them as an argument to the trace objects. Another motivation is to eliminate the kernel_exception_formatter hack. With the formatter in the kernel, we can implement the pretty printer for kernel exceptions as a virtual method. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-22 08:15:36 -07:00
Leonardo de Moura	ddb90d3038	feat(kernel): add unification_constraint and trace objects to the kernel Trace objects will be used to justify steps performed by engines such as the elaborator. We use them to implement non-chronological backtracking in the elaborator. They are also use to justify to the user why something did not work. The unification constraints are in the kernel because the type checker may create them when type checking a term containing metavariables. Remark: a minimalistic kernel does not need to include metavariables, unification constraints, nor trace objects. We include these objects in our kernel to minimize code duplication. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-22 08:15:36 -07:00
Leonardo de Moura	e741cc29ef	test(metavar): encode two of the bad examples as unit tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-22 08:15:36 -07:00
Leonardo de Moura	59914a36f3	refactor(metavar): reorganize and simplify metavariables - Use hierarchical names instead of unsigned integers to identify metavariables. - Associate type with metavariable. - Replace metavar_env with substitution. - Rename meta_ctx --> local_ctx - Rename meta_entry --> local_entry - Disable old elaborator - Rename unification_problems to unification_constraints - Add metavar_generator - Fix metavar unit tests - Modify type checker to use metavar_generator - Fix placeholder module Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-22 08:15:36 -07:00
Leonardo de Moura	3387c300a0	feat(polynomial): add multivariate polynomials Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-21 18:22:14 -07:00
Leonardo de Moura	93d4466d06	refactor(interval): move interval unit tests to tests/util/interval Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-21 18:17:34 -07:00
Leonardo de Moura	f18d35555e	refactor(interval): organize template source code using the approach described at http://www.codeproject.com/Articles/3515/How-To-Organize-Template-Source-Code Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-21 18:15:27 -07:00
Leonardo de Moura	e208309abd	refactor(numerics): rename power operator to pow, the idea is to follow the C/C++ name convention for the power operator Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-21 17:23:56 -07:00
Leonardo de Moura	f1d9312521	feat(numerics/zpz): add numeric_traits for zpz numerals Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-18 14:41:18 -07:00
Leonardo de Moura	1429cc9df2	feat(numerics): add finite field Z/pZ Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-18 13:27:28 -07:00
Leonardo de Moura	bdade0e638	fix(numerics): problem with gcd tests on OSX Now, we only test gcd(a, b) for a != b && a != 0 && b != 0. When one of these conditions do not hold, the result is implementation dependent. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-17 10:38:02 -07:00
Leonardo de Moura	cf2c0f8ebb	feat(numerics): add gcd and extended gcd templates (for primitive types) Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-16 18:18:20 -07:00
Leonardo de Moura	39f68ed0d6	feat(numerics): add is_prime function Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-16 17:25:08 -07:00
Leonardo de Moura	1097bbfb22	fix(style): fix warnings produced by cpplint.py, disable sizeof(type) warning Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-16 17:04:39 -07:00
Leonardo de Moura	105f55c68b	feat(numerics): add zero() method to all numeric_traits Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-16 16:55:17 -07:00
Leonardo de Moura	ff04c5a2e2	test(numerics): add test to make sure that zeros of different precision mpfp numbers are the equal. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-16 16:54:43 -07:00
Leonardo de Moura	467eff4662	add(numerics): add prime number generator/iterator Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-16 16:05:45 -07:00
Leonardo de Moura	0783805671	feat(kernel): add weight to kernel definitions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-15 14:50:08 -07:00
Leonardo de Moura	5bd6ba37d0	fix(light_checker): fix inconsistent cache bug in light_checker, add tests that expose the problem Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-01 19:25:58 -07:00
Leonardo de Moura	aa5be3262f	fix(type_checker): fix inconsistent cache bug in type_checker, add tests that expose the problem Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-01 19:23:55 -07:00
Leonardo de Moura	2089d12bd0	fix(replace_using_ctx): fix inconsistent cache bug in replace_using_ctx, and add tests that expose the problem Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-01 18:52:18 -07:00
Soonho Kong	760f2e15ce	feat(library/replace_using_ctx): add static_assert	2013-10-01 16:47:49 -07:00
Soonho Kong	e3b762e909	feat(kernel): add static_assert to expr,expr_eq,replace	2013-10-01 16:47:36 -07:00
Soonho Kong	b823c7d779	feat(util): add static_assert to {scoped,splay}_{map,set}	2013-10-01 16:47:28 -07:00
Soonho Kong	a726f5fbb7	feat(util/list): add static_asserts for map/for_each/compare	2013-10-01 09:05:53 -07:00
Soonho Kong	3381df0150	fix(util/list_fn): rename iter to for_each	2013-10-01 09:03:07 -07:00
Soonho Kong	c50bc13be0	test(library/rewriter): add more tests	2013-10-01 00:30:38 -07:00
Soonho Kong	7c0b56ad0d	feat(library/rewriter): implement repeat/app/lambda/pi/try rewriter - refactor to use rewriter_cell - implement display and operator<< for debugging	2013-10-01 00:30:31 -07:00
Soonho Kong	e6c76fbe76	refactor(library/rewriter/fo_match): add more lean_trace for debugging	2013-10-01 00:20:12 -07:00
Soonho Kong	a832173f5f	feat(kernel/expr): add expr::operator() which takes 8 args	2013-10-01 00:19:30 -07:00
Soonho Kong	1a3ea26032	feat(util/list_fn): add iter function	2013-10-01 00:18:55 -07:00
Leonardo de Moura	15979ab991	fix(lean): fix warnings produced by cppcheck Fix (relevant) warnings produced by http://cppcheck.sourceforge.net. Most warnings produced were incorrect. The tool does not seem to support some of the C++11 new features. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-30 21:38:55 -07:00
Leonardo de Moura	30089aa4f8	test(type_checker): add example showing how to use the kernel exception formatter Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-30 16:39:29 -07:00
Soonho Kong	54f4c4d9bc	test(library/rewriter/fo_match): clean up enable_trace	2013-09-29 18:36:01 -07:00
Leonardo de Moura	8d3ae665e7	fix(splay_map): fix typo Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-29 17:30:08 -07:00
Leonardo de Moura	21f9699661	test(splay_tree): add missing test Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-29 17:28:10 -07:00
Leonardo de Moura	790c2a72d5	test(safe_arith): add unit tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-29 17:20:32 -07:00
Leonardo de Moura	1179b6b52b	test(hash): add missing tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-29 17:20:32 -07:00
Leonardo de Moura	57b6148bbb	test(buffer): add missing tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-29 17:20:32 -07:00
Leonardo de Moura	02f621aa45	test(lazy_list): add more tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-29 14:38:35 -07:00
Leonardo de Moura	3c8dff9085	feat(lazy_list): implement ML-like lazy lists We will use lazy lists to represent the set of solutions produced by the elaborator. The elaborator plugins will also use lazy lists. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-29 12:35:26 -07:00
Soonho Kong	841a1fb20c	fix(debug): print type in lean_assert, print bool correctly - use typeinfo to print out a type of value when an assertion fails. need to use "c++filt --types" to demangle names for non-basic types. - use std::boolalpha and std::noboolalpha to control the printed values for "true" and "false"	2013-09-28 23:38:21 -07:00
Soonho Kong	4602dfd209	test(util/numerics): more tests to improve coverage	2013-09-28 23:38:17 -07:00
Soonho Kong	fb3635a9ef	test(util/numerics/mpbp): add more tests for improving coverage	2013-09-28 01:01:52 -07:00
Soonho Kong	6519d4bb0f	chore(memcheck.supp): generalize TCmalloc_Bug2 pattern to suppress a warning from MSR 32bit build [skip-ci]	2013-09-27 19:16:02 -07:00
Soonho Kong	0065d69e0a	chore(build): put --coverage CXX_FLAGS for TESTCOV build	2013-09-27 10:24:31 -07:00
Leonardo de Moura	d2667d56c0	test(lean/parser): add more tests for improving coverage Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-27 09:59:50 -07:00
Leonardo de Moura	0ff69d28f3	test(lean/scanner): add more tests for improving coverage Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-27 09:59:50 -07:00
Leonardo de Moura	6fc177056e	refactor(tests/frontends/lean): use consistent name convention for file names Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-27 09:59:50 -07:00
Soonho Kong	6a0d211d54	test(fo_match): add more unittests [skip ci]	2013-09-27 01:53:42 -07:00
Soonho Kong	285495313b	refactor(rewrite): use scoped_map as a type of substitution	2013-09-27 01:45:22 -07:00
Soonho Kong	1d4a1b68f5	refactor(fo_match): use scoped_map	2013-09-27 01:44:05 -07:00
Soonho Kong	6307beedc9	feat(scoped_map): add operator<< to scoped_map for debugging	2013-09-27 01:42:11 -07:00
Soonho Kong	a05b6b476e	fix(testcov): install lcov and include testcov only when it's on	2013-09-26 22:24:24 -07:00
Soonho Kong	6abb7bf2ff	chore(testcov): add missing CodeCoverage.cmake	2013-09-26 21:26:52 -07:00
Soonho Kong	3a5a565594	feat(splay_map): add operator<< to splay_map for debugging	2013-09-26 20:44:20 -07:00
Soonho Kong	5e5087b0a3	chore(testcov): add compile target "cov" to run code-coverage locally - need to run cmake with "-DTESTCOV=ON" and "-DCMAKE_BUILD_TYPE=Debug" - type "make/ninja cov" - open "coverage/index.html" to check the code coverage	2013-09-26 20:28:52 -07:00
Leonardo de Moura	9d8ff0eadb	test(mpz): add unit tests for mpz Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-26 20:01:39 -07:00
Leonardo de Moura	5cce74d116	test(library): add tests for improving coverage Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-26 19:43:10 -07:00
Soonho Kong	60157aa92a	fix(splay_map): add 'const' to coersion operator of ref class [skip ci]	2013-09-26 19:09:37 -07:00
Leonardo de Moura	54e63fd4de	feat(splay_tree): add fold and for_each templates for splay_tree and splay_map Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-26 18:18:20 -07:00
Leonardo de Moura	1aca1d2d77	refactor(list): improve append function Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-26 18:18:20 -07:00
Leonardo de Moura	24c173a519	feat(debug): add assert_ne (not equal) macro Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-26 18:18:20 -07:00
Leonardo de Moura	d7ed1560a9	feat(name_generator): add name_generator for unique names modulo a prefix Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-26 18:18:06 -07:00
Leonardo de Moura	e5d312dc18	fix(kernel): the hash code of expressions was not being used to compare them Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-26 08:41:20 -07:00
Leonardo de Moura	19f4554145	test(exception): add tests for improving coverage Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-26 08:35:13 -07:00
Leonardo de Moura	a24dbc3527	test(buffer): add tests for improving coverage Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-26 08:35:13 -07:00
Soonho Kong	bc31322a78	chore(memcheck): add another memcheck.supp entry for tcmalloc bug suppress a valgrind warning we had on "normalizer" testcase (only with g++-4.8.1)	2013-09-26 00:49:43 -07:00
Soonho Kong	a2a5a77a44	fix(memory): increase memory counters by the actual size of reallocated memory On OSX, we had a test failure on memory module. The problem was in the realloc function (line 38): void * realloc(void * ptr, size_t sz) { size_t old_sz = malloc_size(ptr); g_global_memory.dec(old_sz); g_global_memory.inc(sz); g_thread_memory.dec(old_sz); g_thread_memory.inc(sz); void * r = realloc_core(ptr, sz); if (r \|\| sz == 0) return r; else ... The size of r could be bigger than sz. For instance, \|ptr\| = 40 but \|r\| = 48 In the current code, here we only increase counters by 40. But later when we free it, we decrease them by 48, and this caused the problem, underflow of an unsigned counter in g_global_memory.	2013-09-26 00:33:56 -07:00
Leonardo de Moura	4bae715350	fix(memory): disable problematic test when tcmalloc is used Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-25 22:39:49 -07:00
Leonardo de Moura	c00534209a	test(splay_map): add tests for improving code coverage Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-25 22:12:49 -07:00
Leonardo de Moura	98b4e09063	refactor(kernel): simplify expr_eq Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-25 22:09:08 -07:00
Leonardo de Moura	23e2f72f42	test(list): add tests for improving code coverage Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-25 22:04:24 -07:00
Leonardo de Moura	db4e5ab0ad	feat(expr_lt): improve expr_lt performance by using hash codes, and add more tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-25 21:59:58 -07:00
Leonardo de Moura	6477708d78	refactor(debug): improve lean_unreachable(), now we can avoid 'fake' return statements Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-25 21:27:20 -07:00
Leonardo de Moura	a7707dd669	test(bit_tricks): add tests for log2	2013-09-25 20:58:01 -07:00
Leonardo de Moura	44a16cab6a	test(exception): add new tests exception and parser_exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-25 20:57:53 -07:00
Leonardo de Moura	87e749cd12	test(trace): add unit test for trace module Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-25 20:30:05 -07:00
Leonardo de Moura	e16f45854b	refactor(deep_copy): simplify deep_copy implementation, and move unit test to separate file Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-25 20:25:24 -07:00
Leonardo de Moura	037ebfd1d4	refactor(util): make 'util/test.h' the first include Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-25 20:13:05 -07:00
Soonho Kong	ad62f9762b	fix(tests/util): use lean_assert_eq	2013-09-25 19:22:36 -07:00
Soonho Kong	475338080f	fix(tests/interval): use new lean_assert and lean_assert_eq	2013-09-25 18:40:45 -07:00
Leonardo de Moura	9f0dab1add	fix(kernel): add declarations for operator<<(std::ostream&, expr const&) and operator<<(std::ostream&, context const&) in the kernel The actual implementation of these two operators is outside of the kernel. They are implemented in the file 'library/printer.cpp'. We declare them in the kernel to prevent the following problem. Suppose there is a file 'foo.cpp' that does not include 'library/printer.h', but contains expr a; ... std::cout << a << "\n"; ... The compiler does not generate an error message. It silently uses the operator bool() to coerce the expression into a Boolean. This produces counter-intuitive behavior, and may confuse developers.	2013-09-25 17:45:54 -07:00
Leonardo de Moura	1452e9319e	feat(debug): improve lean_assert macro Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-25 17:29:00 -07:00
Soonho Kong	1d8b7dc193	Update 'orelse' and 'then' rewriter to take a list of rewriters	2013-09-25 16:46:39 -07:00
Soonho Kong	a50f5f92b8	Rename 'rewrite' to 'Rewriter', change type of rewriter::operator()	2013-09-25 15:38:16 -07:00
Soonho Kong	573ca92a08	Fix typo in CTestConfig.cmake	2013-09-24 21:46:51 -07:00
Soonho Kong	6d10e978dc	Add "--gen-suppressions=all" to valgrind option	2013-09-24 21:36:03 -07:00
Soonho Kong	0ef633a3c5	Fix to be compiled by clang++-3.4 Clang++-3.4 is starting to enforce the following item of C++11 standard, thus it's making lean not compiling: It's illegal in C++11: §8.3.6.4 [dcl.fct.default] "If a friend declaration specifies a default argument expression, that declaration shall be a definition and shall be the only declaration of the function or function template in the translation unit."	2013-09-24 21:30:56 -07:00
Soonho Kong	8e9bd9ee67	Add Repeat/Success/Fail to rewrite (skeleton)	2013-09-24 20:04:08 -07:00
Soonho Kong	ac0eafa1b6	Fix style-warning	2013-09-24 19:34:58 -07:00
Soonho Kong	57e9e2c658	Re-implement rewrite module using rewrite_cell	2013-09-24 19:11:09 -07:00
Leonardo de Moura	ba0528c298	Implement total order on expressions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-24 12:16:32 -07:00
Leonardo de Moura	e23813f15d	Add support for creating unique internal names. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-24 11:01:30 -07:00
Leonardo de Moura	1779b29355	Implement map using splay_trees Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-24 01:44:46 -07:00
Soonho Kong	71fb150333	Fix type of rewrite() to take an env. Add skeletons for other rewriters	2013-09-24 01:20:45 -07:00
Soonho Kong	81c9de229b	Add then and orelse rewrite combinators and tests	2013-09-24 01:19:03 -07:00
Soonho Kong	9ba6068858	Update fo_match	2013-09-24 01:19:03 -07:00
Soonho Kong	f89ededddc	Add rewrite and first-order pattern matching skeletal	2013-09-24 01:19:03 -07:00
Leonardo de Moura	b78b2e0585	Add remaining splay tree methods Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-24 01:04:02 -07:00
Soonho Kong	01f5fa59b1	Update src/memcheck.supp to suppress warnings caused by tcmalloc	2013-09-24 03:58:13 -04:00
Leonardo de Moura	d31f3facac	Implement splay trees Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-23 22:31:18 -07:00
Soonho Kong	c1b12eae99	Update memcheck.supp to suppress a valgrind warning caused by a bug in tcmalloc-2.0	2013-09-23 19:57:16 -07:00
Leonardo de Moura	46d6c41835	Fix bug in the type checker (when type checking terms with meta-variables). Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-22 19:12:19 -07:00
Leonardo de Moura	1647e44510	Fix memory corruption bug Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-22 18:53:58 -07:00
Leonardo de Moura	16a6a54df1	Fix abuse of operator-> overload Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-22 16:41:51 -07:00
Leonardo de Moura	c847d27763	Improve higher order unification Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-21 00:41:49 -07:00
Soonho Kong	80581a76bb	Update Find{MSize,MallocSize,MallocUsableSize}.cmake to handle the case where find_path fails	2013-09-21 00:10:25 -07:00
Soonho Kong	48318511f2	Undo the previous change which caused compile-errors	2013-09-21 00:04:23 -07:00
Soonho Kong	66ba1a20d7	Suppress cmake warning for OSX build	2013-09-20 23:49:09 -07:00
Leonardo de Moura	d29ec9ab6f	Add tests for memory.cpp Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-20 22:37:13 -07:00
Leonardo de Moura	7ac94ee976	Add max_sharing tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-20 22:01:40 -07:00
Leonardo de Moura	d34cfe3f8a	Add simple formatter tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-20 21:46:32 -07:00
Soonho Kong	bef44899c8	Suppress style warning on util/memory.cpp	2013-09-20 18:07:12 -07:00
Soonho Kong	9226c46358	Add support OSX's malloc_size	2013-09-20 17:48:55 -07:00
Soonho Kong	8dc31dae4d	Fix Check{MSize,MallocUsableSize}.cc and FindMSize.cmake to consider cross-compilation	2013-09-20 16:10:00 -07:00
Leonardo de Moura	3971265bcb	Add support for _msize Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-20 14:14:57 -07:00
Leonardo de Moura	dae654e4c6	Track memory usage. Add new CMake option TRACK_MEMORY_USAGE (It is ON by default). Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-20 12:32:12 -07:00
Leonardo de Moura	9d1266c972	Fix bugs in Tcmalloc detection. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-19 23:52:50 -07:00
Leonardo de Moura	a7a5426ff5	Fix wrong message in tcmalloc detection code Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-19 23:36:57 -07:00
Leonardo de Moura	16dc056abc	Remove invalid use of register Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-19 22:59:39 -07:00
Soonho Kong	49e87ccbb1	Enable "-Wextra" compiler option and fix code to remove warnings "-Wextra" option turns on the following warnings: -Wclobbered -Wempty-body -Wignored-qualifiers -Wmissing-field-initializers -Wmissing-parameter-type (C only) -Wold-style-declaration (C only) -Woverride-init -Wsign-compare -Wtype-limits -Wuninitialized -Wunused-parameter (only with -Wunused or -Wall) -Wunused-but-set-parameter (only with -Wunused or -Wall)	2013-09-19 22:52:52 -07:00
Leonardo de Moura	651c5d6751	Fix warnings and bugs related to unused variables. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-19 22:41:07 -07:00
Soonho Kong	2b72c5f681	Update cpplint.py, disable "All parameters should be named in a function"	2013-09-19 22:41:07 -07:00
Soonho Kong	ab6ca82e6f	Update to suppress unused-parameter warnings	2013-09-19 22:40:34 -07:00
Leonardo de Moura	80a1b96925	Remove duplicate solutions in the higher order matching module. Simplify solutions when higher-order matching is used, and we don't have a residue. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-19 18:59:28 -07:00
Leonardo de Moura	ffef055e34	Add options to ho_unifier Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-19 18:19:25 -07:00
Leonardo de Moura	8c5c17ee12	Fix typo Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-19 16:30:37 -07:00
Leonardo de Moura	42482622f6	Add imitation for lambdas and Pis Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-19 16:28:23 -07:00
Leonardo de Moura	4afeb1a400	Add imitation step for equalities. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-19 16:28:23 -07:00
Leonardo de Moura	b3aa8b37f3	Remove cleanup_subst. The residue may still reference auxiliary variable. So, it is not safe to remove then from the resultant partial substitution. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-19 16:28:23 -07:00
Leonardo de Moura	d7cc5d2404	Fix bug in ho_unifier Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-19 16:28:23 -07:00
Soonho Kong	0005d22bd1	Update memcheck.supp, add a new suppression rule for 32bit ubuntu [skip ci]	2013-09-19 11:46:47 -07:00
Leonardo de Moura	2f29ff70d7	Implement higher-order unification Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-18 20:46:00 -07:00
Leonardo de Moura	ad901ce087	Use consistent naming conventions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-17 14:43:07 -07:00
Leonardo de Moura	22949051f1	Higher-order unifier skeleton Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-17 14:43:07 -07:00
Soonho Kong	27d5ae13d7	Move src/interval to src/util/interval	2013-09-17 14:10:53 -07:00
Leonardo de Moura	df054477eb	Remove unnecessary TODOs. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-17 13:33:52 -07:00
Leonardo de Moura	3df6149daa	Add support for metavariables in the type checker. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-17 11:09:59 -07:00
Leonardo de Moura	9f9dcf9a29	Fix bug in the creation of children environments. Remove unnecessary function. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-17 07:37:33 -07:00
Leonardo de Moura	30b19c314a	Add basic support for metavariables at is_convertible. Swap is_convertible arguments to make it more intuitive. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-17 07:15:47 -07:00
Leonardo de Moura	a26c7d47f2	Add simplification to add_lift Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-17 03:14:02 -07:00
Leonardo de Moura	99e8d2feae	Add simplification rule to add_inst Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-17 02:57:28 -07:00
Leonardo de Moura	21c7a45f67	Relax definition of identity_stack. Fix printer for metavariable contexts. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-17 02:09:45 -07:00
Leonardo de Moura	d3bce584f4	Add support for new metavariable representation in the normalizer. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-17 01:57:21 -07:00
Leonardo de Moura	da09e7217a	Cleanup meta_entry code Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-16 19:32:28 -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	cad562a448	Add support for metavariables in the normalizer. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-16 19:32:28 -07:00
Leonardo de Moura	1be2a30c8c	Fix bug in normalizer. We must create a scope whenever we extend the value stack. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-16 19:32:28 -07:00
Soonho Kong	01339a93a3	Fix cpplint warning in util/safe_arith.cpp	2013-09-16 19:12:12 -07:00
Soonho Kong	13401d534c	Add static assertion to util/safe_arith.cpp	2013-09-16 18:17:05 -07:00
Soonho Kong	6ee14bf17f	Use unsigned short for the type of interval::bound_deps	2013-09-16 18:15:32 -07:00
Soonho Kong	ef18759e77	Update src/CmakeLists.txt - only check style over files starting with [A-z]	2013-09-16 16:23:20 -07:00
Leonardo de Moura	f79f046294	Add partial support for metavariables in the normalizer Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-15 21:23:50 -07:00
Soonho Kong	58c8c1a5ec	Add EXCLUDE_PATTERNS to src/Doxyfile - /src/cmake/ - GTAGS GPATH GRTAGS - memcheck.supp - .cmake .cmake.in - *.txt	2013-09-15 20:31:15 -07:00
Leonardo de Moura	2800292947	Add timestamp to metavar_env Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-15 19:50:48 -07:00
Leonardo de Moura	5a4bc331d2	Make unification_problems a virtual class. Associate a 'standard' context with each metavariable in metavar_env Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-15 19:38:36 -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
Soonho Kong	e4b327bbaa	Use C++11's <random> in pdeque/pvector tests (cygwin doesn't support rand_r)	2013-09-15 01:38:57 -07:00
Soonho Kong	dcc917a6b4	Use "sprintf" instead of "snprintf" because cygwin doesn't support "snprintf"	2013-09-15 01:38:21 -07:00
Soonho Kong	b553521578	Attempt to suppress valgrind warnings on Travis - don't understand why cmake on travis doesn't pick up the memcheck.supp file. It works on my local machine.	2013-09-15 01:17:05 -07:00
Soonho Kong	30f4b2de5f	Update memcheck.supp [skip ci]	2013-09-14 19:33:47 -07:00
Soonho Kong	ce05345129	Update CTestConfig.cmake to fix memcheck.supp	2013-09-14 20:22:05 -04:00
Soonho Kong	60903d3cea	Fix cygwin build which was failed due to snprintf	2013-09-14 17:11:37 -07:00
Soonho Kong	c96a6982a0	Add <ctime> header for time() in pdeque/pvector tests	2013-09-13 20:42:49 -07:00
Soonho Kong	5266e22f05	Remove debug code from cpplint.py	2013-09-13 20:37:31 -07:00
Soonho Kong	eda25e77a4	Use time(0) as an initial seed for rand_r() in pvector/pdeque tests	2013-09-13 20:28:15 -07:00
Soonho Kong	f8c0c02cb0	Exclude 'style_check' from MemCheck list	2013-09-13 20:27:35 -07:00
Soonho Kong	0905529720	Add "style_check" test	2013-09-13 20:00:55 -07:00
Soonho Kong	0c450b5c23	Add StyleCheck.cmake	2013-09-13 19:21:02 -07:00
Soonho Kong	f620f54b32	Add target "style" to run cpplint.py - try "ninja style"	2013-09-13 19:15:38 -07:00
Soonho Kong	bc60b47295	Apply coding style	2013-09-13 18:48:09 -07:00
Leonardo de Moura	99eaff0b4f	Extract private and static, and add treeview to documentation Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-13 17:55:37 -07:00
Leonardo de Moura	bcc3827a99	Modify Doxygen file to extract all elements even the undocumented ones. Disable warnings for undocumented entities. Add extra comments. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-13 13:46:22 -07:00
Leonardo de Moura	d54834279e	Use consistent coding style for if-then-else Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-13 12:57:40 -07:00
Leonardo de Moura	8c735f1daa	Use consistent coding style for spaces after ',' Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-13 12:49:03 -07:00
Leonardo de Moura	2c68117adf	Tag TODOs Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-13 12:25:21 -07:00
Leonardo de Moura	18f9378f97	Rename numtype.h to num_type.h Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-13 09:07:44 -07:00
Leonardo de Moura	573ec5ccc2	Rename import_all. The idea is to use consistent name for library files. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-13 09:06:46 -07:00
Leonardo de Moura	0c09e4524a	Use consistent names for import functions, and library files. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-13 08:58:34 -07:00
Leonardo de Moura	070c87bef0	Rename arith library files Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-13 08:55:09 -07:00
Soonho Kong	5c3866cd71	Use fullpath in #include directives, add missing STL headers	2013-09-13 03:35:29 -07:00
Leonardo de Moura	4c19cc6957	Rename lean frontend files. The prefix lean_ is not necessary anymore. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-12 20:09:35 -07:00
Leonardo de Moura	26097475fd	Use fullpath in #include directives. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-12 20:04:10 -07:00
Leonardo de Moura	c655e9fe7b	Move sexpr_funcs to sexpr_fn. Using consistent file name conventions. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-12 18:27:46 -07:00
Leonardo de Moura	2e990ef7d3	Fix warnings Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-12 14:02:40 -07:00
Leonardo de Moura	bc69e7803f	Add support for writing a[i] = v instead of a.set(i, v) in the pdeque class. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-12 11:18:26 -07:00
Leonardo de Moura	74b8a4f0ac	Add support for writing a[i] = v instead of a.set(i, v) in the pvector class. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-12 11:12:02 -07:00
Leonardo de Moura	f972cc9aae	Fix bugs in pvector. Improve test driver Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-12 11:01:40 -07:00
Leonardo de Moura	55ff49d2d5	Replace queue.h with pdeque.h Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-12 10:09:54 -07:00
Leonardo de Moura	cd5e45bae2	Reduce pvector delta_cell quota on reads. Add example that demonstrates why this is needed. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-12 08:28:24 -07:00
Soonho Kong	5858c9d5e0	Update tests/util/list.cpp to suppress a g++ warning	2013-09-12 01:39:04 -07:00
Leonardo de Moura	f7196e05ff	Add 'persistent' vectors. We should use the same approach for queues. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-11 19:48:55 -07:00
Leonardo de Moura	ef0e0ad382	Add (optional) performance tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-11 19:48:55 -07:00
Leonardo de Moura	572c7ced2a	Add #include<atomic> to expr.h. We need it when #define LEAN_THREAD_UNSAFE_REF_COUNT is used Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-11 19:48:55 -07:00
Leonardo de Moura	ed15a2df9b	Use split_reverse_second instead of split and then reverse in queue Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-11 19:48:55 -07:00
Leonardo de Moura	37498f9fb8	Add persistent queues Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-11 19:48:54 -07:00
Leonardo de Moura	3657320edb	Add basic list functions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-11 19:48:54 -07:00
Soonho Kong	7a6032dd86	Update memcheck.supp to ignore bash memroy leak on Fedora19	2013-09-10 22:44:24 -04:00
Soonho Kong	9e3583a04a	Update memcheck.supp to match the thread bug patterns we get by using clang++-3.3	2013-09-10 17:37:22 -07:00
Soonho Kong	a993424165	Use "--gen-suppressions=all" in valgrind	2013-09-10 17:09:39 -07:00
Soonho Kong	6569406fb9	Update memcheck.supp add reference for the suppression stuff [skip ci]	2013-09-10 15:47:47 -07:00
Soonho Kong	3505ed8adb	Use suppressions file to ignore certain valgrind warnings	2013-09-10 15:37:09 -07:00
Soonho Kong	9113f824bd	Use '--track-origins=yes' option in valgrind	2013-09-10 14:31:30 -07:00
Leonardo de Moura	6fe86ffefd	Fix initialized memory error reported by Valgrind. Disable 2 tests that produce memory leaks due to a bug in g++. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-10 13:51:02 -07:00
Soonho Kong	fae6c29237	Fix memory leaks in mpfp.h	2013-09-10 13:26:14 -07:00
Soonho Kong	8ce18a1508	Use "--leak-check=full" option in valgrind	2013-09-10 13:12:22 -07:00
Soonho Kong	f4edbba325	Turn off '--show-reachable=yes' valgrind option	2013-09-10 12:34:33 -07:00
Soonho Kong	b04bdae763	Use "--trace-children=yes" option for MemCheck(valgrind) to handle leantests shell script	2013-09-10 10:47:04 -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	adfbba6447	Fix problem reported by Soonho Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-08 23:10:33 -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	a8ba50531b	Fix typo Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-08 20:38:11 -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	1cee392483	Add light_checker: module for extracting the type of (fully elaborated) expressions. It is much faster than type_checker, which infers the type but also check whether the input is type correct or not. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-07 22:33:18 -07:00
Leonardo de Moura	33c4b44b2b	Encapsulate context implementation. The current implementantion based on lists may be a performance problem in the future, and we should be able to change it without affecting the whole code base. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-07 11:15:11 -07:00
Leonardo de Moura	bab11b57ad	Move Symm and Trans back to basic_thms.cpp Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-06 23:49:35 -07:00
Leonardo de Moura	c674bb3790	Add castlib as an independent library Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-06 23:40:47 -07:00
Leonardo de Moura	7a9d53d0d7	Refactor arith libraries Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-06 23:19:47 -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	7eab229114	Improve check_pi in lean elaborator Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-06 18:58:33 -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	b3a095b068	Fix pretty printer for evaluator Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-05 18:57:29 -07:00
Leonardo de Moura	c22bd8b6ed	Clean elaborator_exception pretty printing Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-05 10:15:52 -07:00
Leonardo de Moura	eb96e6441f	Moved kernel exception formatting to kernel_exception_formatter.cpp. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-05 10:15:43 -07:00
Soonho Kong	974b99b424	Update CTestCustom.cmake.in Exclude "threads" test from valgrind targets [skip ci]	2013-09-04 16:41:04 -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	408005b730	Fix typo Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-04 16:36:57 -07:00
Soonho Kong	30e5ac7004	Fix OSX linker warning issue	2013-09-04 15:35:07 -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	d41160f8a5	Modify environment. Now, when a builtin value is declared, if it has a unicode alternative representation, then we add it as a definition. Now, everything that occurs in the environment has been 'declared'. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-04 08:53:00 -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	9f34f96b08	Add another example Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-04 05:40:28 -07:00
Soonho Kong	a8c16bc127	Fix test coverage problem by forcing to use gcov-4.8	2013-09-04 08:07:24 -04:00
Soonho Kong	5e603dbf9f	Use cdash on cmacslab2 machine due to 10-build per day restriction	2013-09-04 04:46:37 -07:00
Leonardo de Moura	9f64e2b14b	Fix another cdash warning Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-04 04:43:55 -07:00
Leonardo de Moura	00bee9c96e	Fix warning produced by clang++ Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-04 04:40:43 -07:00
Leonardo de Moura	57c0c69872	Fix bug reported by Valgrind. Reason: m_metavars is a vector of metavar_info; each metavar_info has a context; when we invoke mk_metavar the vector can grow in size, and the context is moved to a new location. The previous location is invalidated. To avoid the problem we have to save ctx in a local variable. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-04 04:29:03 -07:00
Soonho Kong	bbbd584b45	Use my.cdash.org to store results of unittests, coverage, and valgrind	2013-09-04 00:51:20 -07:00
Leonardo de Moura	887f696f66	Factor duplicate code. Add more comments Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-03 23:27:58 -07:00
Leonardo de Moura	0c071d43af	Move examples to lean examples subdir. We should have an example subdirectory for each frontend Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-03 20:42:20 -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
Leonardo de Moura	3992c4b8f9	Define divides, and add examples Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-03 20:18:20 -07:00
Leonardo de Moura	8e7c657cf7	Use expected type of a definition in the elaborator. Improve elaborator solver. Add new example Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-03 18:04:42 -07:00
Leonardo de Moura	4a75e2d965	Fix bug when pretty printing function applications where the head is a meta-variable. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-03 17:51:56 -07:00
Leonardo de Moura	51422fe654	Modify the parser for accepting expressions such as: 'fun a b, f a b', 'forall a, f a > 0', etc. This is just syntax sugar for 'fun (a : _) (b : _), f a b' and 'forall a : _, f a > 0' Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-03 17:24:05 -07:00
Leonardo de Moura	6f3fa63ccb	Add missing test Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-03 14:51:34 -07:00
Leonardo de Moura	a154f4e439	Modify Set command in the default lean frontend. Now, the lean prefix (for lean default frontend specific options) is optional when we are in the lean front-end. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-03 11:07:28 -07:00
Leonardo de Moura	a341643335	Fix unit tests for Windows Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-03 10:44:51 -07:00
Leonardo de Moura	2d97bc3861	Make pp::unicode false by default in Windows Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-03 10:26:12 -07:00
Leonardo de Moura	544229e5d3	Create pp::unicode option. The idea is to be able to disable unicode characters, but still be able to use mixfix notation. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-03 10:11:45 -07:00
Leonardo de Moura	e031d7bc10	Improve error messages when overloads+coercions do not work Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-02 20:05:47 -07:00
Leonardo de Moura	fd44ec8d79	Improve application type mismatch error messages Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-02 18:28:12 -07:00
Leonardo de Moura	72188691de	Add hyperbolic functions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-02 17:28:43 -07:00
Leonardo de Moura	4eaba93591	Add trigonometric functions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-02 17:03:02 -07:00
Leonardo de Moura	395513258e	Define mod and unary minus Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-02 16:31:44 -07:00
Leonardo de Moura	b483d0dc45	Replace Int::sub and Real::sub with definitions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-02 16:31:30 -07:00
Leonardo de Moura	abc939382b	Add Real arithmetic. Fix elaborator for coercions. Now, two overloads are considered ambiguous if they need the same number of coercions. Improve pretty printer for nest infix operators with same precedence and associativity. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-02 13:20:00 -07:00
Leonardo de Moura	e218b92a9d	Modify verbose message for Set command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-02 12:29:21 -07:00
Leonardo de Moura	0a67679afb	Add natural numbers. Fix how coercions and overloads interact (switch to approach used in C++). Add notation for natural and integer arithmetic. Rename m and u universe variables to M and U. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-02 12:24:29 -07:00
Leonardo de Moura	7acf438bf4	Metavariables will not be part of the kernel Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-02 09:36:04 -07:00
Leonardo de Moura	990f428a81	Remove virtual method kind from value class and subclasses. We can use dynamic_cast to achieve the same goal Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-02 09:35:10 -07:00
Leonardo de Moura	81d0203ee0	Replace macros TypeM, TypeU, Int, Bool, True and False with constant global expressions. The macros were producing counterintuitive behavior. For example, we had an enumeration type with an element called Int. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-02 09:11:53 -07:00
Leonardo de Moura	db88920f81	Rename normalize and type_check to normalizer and type_checker (using a consistent naming convention) Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-02 08:43:38 -07:00
Leonardo de Moura	c97e669f0c	Add coercion support in the elaborator and pretty printer Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-01 19:09:07 -07:00
Leonardo de Moura	e8c09015ad	Move elaborator to lean default frontend. It is getting too specific Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-01 18:22:24 -07:00
Leonardo de Moura	42be7a4989	Add coercion declarations Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-01 18:11:28 -07:00
Leonardo de Moura	75f4ec5092	Add functions for 'updating expressions'. The new functions are used to simplify the elaborator. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-01 15:37:30 -07:00
Leonardo de Moura	61a8fd16db	Remove unnecessary files Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-01 14:57:08 -07:00
Leonardo de Moura	d27680d7fc	Add support for overloads in the elaborator Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-01 14:54:02 -07:00
Leonardo de Moura	598daa40bc	Refactor elaborator for supporting overloads Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-01 10:24:10 -07:00
Leonardo de Moura	b2924bba99	Fix typos Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-01 10:03:15 -07:00
Leonardo de Moura	e54338f4a8	Add a real example. Fix bug in the parser Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-31 19:32:08 -07:00
Leonardo de Moura	51640ecff8	Move files in examples directory to tests directory. They are not real examples Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-31 19:16:30 -07:00
Leonardo de Moura	389f23f356	Add test script Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-31 18:31:39 -07:00
Leonardo de Moura	9d9f9797e4	Improve elaborator interface. Now, the metavariables are created inside the elaborator. The elaborator-user only needs to create placeholders. Motivaton: the placeholders are meaningful independently of the elaborator. On the other hand, the metavariables depend on the elaborator state. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-31 17:11:06 -07:00
Leonardo de Moura	71b8b6408e	Handle (and pretty print) elaborator error messages in the lean default frontend Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-31 16:46:41 -07:00
Leonardo de Moura	03a5b5dbd0	Add more tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-31 14:25:27 -07:00
Leonardo de Moura	64788320f2	Fix elaborator for let-expressions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-31 14:24:07 -07:00
Leonardo de Moura	4a28a64685	Fix type checker for let expressions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-31 14:19:24 -07:00
Leonardo de Moura	793468072b	Fix nontermination problem Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-31 12:32:16 -07:00
Leonardo de Moura	4c27530930	Fix missing case in the elaborator Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-30 17:07:45 -07:00
Leonardo de Moura	4b7d4cf0d1	Add latest example to regression suite Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-30 16:39:31 -07:00
Leonardo de Moura	dadbf15e70	Change how the (auxiliary) explicit definitions are encoded in the system. The previous encoding was confusing the pretty printer, and the definition looked recursive. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-30 16:37:21 -07:00
Leonardo de Moura	1b6d51b0aa	Mark implicit arguments of builtin symbols Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-30 15:56:04 -07:00
Leonardo de Moura	4ef4655183	Add homogeneous equality Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-30 14:26:12 -07:00
Leonardo de Moura	1e370023b1	Attach elaborator the lean default parser Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-30 13:25:30 -07:00
Leonardo de Moura	45d89ace65	Fix name clash problem when pretty printing Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-30 13:25:12 -07:00
Leonardo de Moura	6efb6c6e83	Fix clang++ compilation problem. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-30 09:04:11 -07:00
Leonardo de Moura	2aac94f2e6	Refactor elaborator using new metavar library. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-30 01:25:06 -07:00
Leonardo de Moura	682df7699d	Fix is_convertible propositions => type Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-30 01:24:06 -07:00
Leonardo de Moura	1f6943e3a4	Add head_reduce_mmv (reduction function modulo metavariables) Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-29 14:15:17 -07:00
Leonardo de Moura	2cf9ca9345	Add metavariable utilities. They will be used to refactor the elaborator. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-29 13:49:22 -07:00
Leonardo de Moura	01e4b4b7fe	Add postprocessor functional object to the replace_fn template. Add unit-test that demonstrates how to build a replacer that builds a trace. The trace associates new expressions with the old ones that were used to create it. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-28 10:47:19 -07:00
Leonardo de Moura	cdab19b88c	Simplify the elaborator Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-27 20:39:38 -07:00
Leonardo de Moura	8dacd97801	Remove obsolete commands.	2013-08-27 16:03:45 -07:00
Leonardo de Moura	a9c6088d11	Uniform notation declarations.	2013-08-27 15:59:13 -07:00
Leonardo de Moura	5aae838e1c	Add missing mixfix notation Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-27 10:09:46 -07:00
Leonardo de Moura	85daaea8ce	Rename get_exs in oper to get_deno Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-27 09:49:48 -07:00
Leonardo de Moura	206c7fa203	Implement support for notation + implicit arguments. Cleanup pretty printer code for handling implicit arguments. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-27 09:45:00 -07:00
Leonardo de Moura	76c968a5b8	Add basic support for hiding implicit arguments when pretty printing. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-26 20:35:10 -07:00
Leonardo de Moura	fc6cc17925	Improve lean pretty printer support for implicit argument annotations Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-26 19:19:56 -07:00
Leonardo de Moura	7bca3705ca	Add implicit argument declarations to lean parser. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-26 10:16:29 -07:00
Leonardo de Moura	7003f85213	Add implicit argument management to lean frontend. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-26 10:16:29 -07:00
Leonardo de Moura	0a34959716	Fix a bug. Add another test. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-25 20:43:50 -07:00
Leonardo de Moura	3721577700	Fix bugs in elaborator. Cleanup tests. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-25 18:46:33 -07:00
Leonardo de Moura	8f4a844598	Fix unit tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-25 11:42:36 -07:00
Leonardo de Moura	7e130ac47f	Propagate interrupt to normalizer in the lean frontend Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-25 11:34:46 -07:00
Leonardo de Moura	b42e04297d	Add support for creating meta-variables in the parser. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-25 11:18:19 -07:00
Leonardo de Moura	25e47a8a2f	Add check_interrupted 'macro' Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-25 11:03:09 -07:00
Leonardo de Moura	ece6e6ca6a	Add interrupt to parser. Add elaborator to parser. Add placeholder support in the scanner. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-25 11:02:34 -07:00
Leonardo de Moura	02b72acc2f	Add implicit arguments unit tests	2013-08-24 18:23:39 -07:00
Leonardo de Moura	ac1267bef3	Add expression elaborator to library Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-24 18:14:09 -07:00
Leonardo de Moura	68e1a1a24a	Add metavar_env to library Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-24 17:51:53 -07:00
Leonardo de Moura	dc91a7adb8	Add Ctrl-C support for interrupting Lean shell. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-24 16:11:35 -07:00
Leonardo de Moura	f0edf2b4a3	Pretty print kernel exceptions. Improve default lean frontend error messages. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-24 13:16:43 -07:00
Leonardo de Moura	0b112b6637	Add sstream to simplify the generation of exception messages. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-24 11:55:17 -07:00
Leonardo de Moura	48ba655bd5	Store position at parser_error. It produces better error messages. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-24 11:30:54 -07:00
Leonardo de Moura	55eaef1a44	Save position information when parsing expression in the lean default fronted. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-24 09:56:07 -07:00
Leonardo de Moura	bf608a38aa	Add head_reduce Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-23 19:35:33 -07:00
Leonardo de Moura	be1ea2ddc7	Add name_set typedef Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-23 19:34:10 -07:00
Leonardo de Moura	e95a0c2559	Modify basic printer for contexts Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-23 12:11:16 -07:00
Leonardo de Moura	18a195029b	Refactor expression equality Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-23 09:42:49 -07:00
Leonardo de Moura	f08c06d582	Add head_beta tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-23 09:42:49 -07:00
Leonardo de Moura	e7487a1fec	Add head_beta function Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-23 09:42:49 -07:00
Leonardo de Moura	670dc5ad55	Add option to control maximum recursion depth in the expression normalizer Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> Conflicts: src/tests/kernel/normalize.cpp	2013-08-23 09:42:49 -07:00
Leonardo de Moura	198fd46fc2	Track recursion depth at normalizer. Add fluid let template. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-23 09:42:49 -07:00
Leonardo de Moura	d30c6b2c9d	Fix spaces Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-23 09:42:49 -07:00
Leonardo de Moura	42a7094ca2	Fix bug in display_decimal. Add more mpq tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-23 09:42:49 -07:00
Leonardo de Moura	218b6ac8b7	Fix typo Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-23 09:42:49 -07:00
Soonho Kong	ca779265e5	Update src/CMakeLists.txt to increase stack size for windows build [skip ci]	2013-08-22 21:16:57 -07:00
Leonardo de Moura	f1462dc51e	Change lean frontend specific options. Now, frontend specific options must begin with the frontend name. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-22 10:55:55 -07:00
Leonardo de Moura	0f6a7e4a95	Rename exprlib to library. Name was misleading, it is more than a library for manipulating expressions. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-22 10:26:52 -07:00
Leonardo de Moura	60fdcf0011	Add option_declaration tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-22 08:59:39 -07:00
Leonardo de Moura	5d813c30d0	Add missing option test Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-22 08:51:33 -07:00
Leonardo de Moura	fbd25cac9f	Add hierarchical names tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-22 08:48:52 -07:00
Leonardo de Moura	1b5fcb80ee	Add sexpr tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-22 08:30:52 -07:00
Leonardo de Moura	6272408f12	Add format tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-22 08:20:42 -07:00
Leonardo de Moura	3c5f993191	Fix bugs in options module. Add more tests. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-22 08:08:55 -07:00
Leonardo de Moura	eb4315baab	Add small trick to improve pretty printer performance. Now, deep.lean takes 0.140secs to be processed. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-21 22:54:58 -07:00
Leonardo de Moura	56d2d2a112	Improve pretty printer performance for deep formulas and formats with long lines. Add example that demonstrates performance problem (before: 13 secs, after: 1 sec). Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-21 22:45:48 -07:00
Leonardo de Moura	aceae7a1b2	Change policy for adding input to readline history. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-21 19:43:47 -07:00
Leonardo de Moura	bd3b422158	Add support for READLINE. Remark: it is not enabled by default. Rename tcmalloc option to TCMALLOC (using consistent name convention for cmake parameters). Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-21 19:08:44 -07:00
Leonardo de Moura	59e63c0421	Add prompt when in interactive mode. Fix Show Environment [num] Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-21 18:24:26 -07:00
Leonardo de Moura	0ffa76aa5e	Fix unused variable warnings Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-21 17:02:09 -07:00
Leonardo de Moura	31460aa5b8	Add option declarations. Add Help. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-21 17:02:09 -07:00
Leonardo de Moura	65898f6d5b	Add Import command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-21 17:02:09 -07:00
Leonardo de Moura	90678566b4	Improve lambda/pi formatting Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-21 17:02:09 -07:00
Soonho Kong	5f1c12feb8	Fix interval<T>::mul to suppress clang warnings	2013-08-21 14:35:46 -07:00
Soonho Kong	c9b6be829e	Doxygen: exclude src/tests directory	2013-08-21 14:35:46 -07:00
Soonho Kong	3f40953efc	Add comments for unicode symbols, fix a typo	2013-08-21 14:35:45 -07:00
Leonardo de Moura	ce470f57db	Add set options to lean_parser. Add support for disabling unicode output. Use channels in lean_parser. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-21 12:42:55 -07:00
Leonardo de Moura	6534142fb9	Fix annoying problem when an integer occurs in the end of a command. Example 'Show 1.' was being parsed as 'Show 1.0'. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-21 11:57:22 -07:00
Leonardo de Moura	d750469667	Move frontend to frontends/lean Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-21 09:04:49 -07:00
Leonardo de Moura	6f36611010	Fix clang++ error Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-20 20:16:02 -07:00
Leonardo de Moura	7778ae0ade	Fix cyclic reference: frontend -> state -> pp_formatter -> frontend. Now pp_formatter is only valid while frontend is still alive. This should not be problem in practice. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-20 20:16:02 -07:00
Leonardo de Moura	3f5a2a83cc	Add methods for setting options. Add string output channel. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-20 20:16:02 -07:00
Leonardo de Moura	4fa2468a85	Add output_channel and state abstractions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-20 20:16:02 -07:00
Leonardo de Moura	73262e9786	Add Echo command. Allow '\' 'n' escape sequence in strings. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-20 20:16:02 -07:00
Leonardo de Moura	57b9a4f2b3	Allow square brackets to be used in operator names Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-20 20:16:02 -07:00
Leonardo de Moura	fbb021386c	Add minor improvement to pretty printer Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-20 20:16:02 -07:00
Leonardo de Moura	d82c60a314	Add test normalizer interrupt Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-20 20:16:02 -07:00
Soonho Kong	fce26a824e	Implement dependencies on interval arithmetic functions (+,-,*,/,inv,power), fix problems on trigonometric functions	2013-08-20 19:49:50 -07:00
Soonho Kong	176b1fccf7	Implement dependencies on interval functions (exp, log, and trigonometric functions)	2013-08-20 02:03:24 -07:00
Leonardo de Moura	b2ba0618c9	Use normalizer object in type checker. The idea is to make sure the interruption is propagated to normalizer. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-19 20:05:56 -07:00
Leonardo de Moura	88cc3dc20d	Add interrupt to normalizer. Fix tests (they were not using the basic printer). Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-19 20:05:56 -07:00
Leonardo de Moura	f6ea9fca7d	Remove interrupt.cpp. We changed the way we will handle interruptions in Lean. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-19 20:05:56 -07:00
Leonardo de Moura	b964edfb3e	Add interrupt method to type checker. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-19 20:05:56 -07:00
Leonardo de Moura	eba4172a0c	Remove verbosity.cpp, verbosity message channel should not be a global. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-19 20:05:56 -07:00
Leonardo de Moura	f5e0150db3	Allow notation to be associated with arbitrary expression (instead of only constants). Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-19 20:05:56 -07:00
Leonardo de Moura	f0b5ec8dfa	Fix bug in parse_arrow Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-19 20:05:56 -07:00
Soonho Kong	db8322e6e8	Fix interval::sin to suppress a warning	2013-08-19 16:46:36 -07:00
Leonardo de Moura	754227fc89	Pretty print forall/exists expressions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-19 15:48:31 -07:00
Leonardo de Moura	986d9635e1	Add syntax sugar for forall/exists expressions. Fix problem when pretty printing nested equalities. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-19 15:48:07 -07:00
Leonardo de Moura	de80db3985	Add support for pretty printing Dags. Find unused prefix for naming shared expressions. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-19 12:04:40 -07:00
Leonardo de Moura	90ad0ba3b3	Add is_prefix_of for hierarchical names Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-19 11:43:46 -07:00
Leonardo de Moura	b2c877b0c3	Add comments to parser.cpp Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-19 09:39:46 -07:00
Leonardo de Moura	ce43c1cbae	Fix cup symbol. In Emacs, the unicode characters cup and cap are assigned incorrectly. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-18 18:43:31 -07:00
Leonardo de Moura	a46bf357b0	Fix bug in level.cpp. Add new example Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-18 18:37:47 -07:00
Leonardo de Moura	95cfac426d	Add parse_level. Fix bug at environment::is_ge Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-18 18:25:34 -07:00
Leonardo de Moura	5d609928af	Add support for reading input files from the command line. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-18 16:23:29 -07:00
Leonardo de Moura	aa49eb4b0f	Run examples during testing Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-18 15:51:27 -07:00
Leonardo de Moura	676ebcca3d	Add parse_arrow Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-18 15:44:39 -07:00
Leonardo de Moura	4d5b65fe87	Fix bug in parser. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-18 15:25:20 -07:00
Leonardo de Moura	afd62ced87	Add parse_let Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-18 15:25:20 -07:00
Leonardo de Moura	7a9319b72e	Pretty print let expressions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-18 15:25:20 -07:00
Leonardo de Moura	ae523e33b4	Add parse_theorem and parse_definition Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-18 12:48:42 -07:00
Leonardo de Moura	5d2027d889	Add parse_lambda and parse_pi Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-18 12:34:00 -07:00
Leonardo de Moura	843253355b	Improve parser Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-18 11:02:29 -07:00
Leonardo de Moura	cdccca9316	Rename builtin operator if-then-else Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-18 11:02:29 -07:00
Leonardo de Moura	51280864cf	Move '\' character to class b Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-18 11:02:29 -07:00
Leonardo de Moura	7ec7b4dce8	Fix bug in pretty printer Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-18 11:02:29 -07:00
Leonardo de Moura	18f319d00f	Add more notation Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-18 11:02:29 -07:00
Leonardo de Moura	823fe6df07	Move test from lean.cpp Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-18 11:02:29 -07:00
Leonardo de Moura	c82a704302	Add Lean default application. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-18 11:02:29 -07:00
Soonho Kong	ec83fd8093	Fix interval::acosh and add more tests on interval to improve code coverage	2013-08-18 01:20:16 -07:00
Leonardo de Moura	65b4845fbc	Add more tests to improve coverage. Fix bug in mpz. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-18 00:28:50 -07:00
Soonho Kong	3b0a7a2d96	Update src/CMakeLists.txt to include 'TESTCOV' build	2013-08-17 20:58:05 -07:00
Leonardo de Moura	06f1b2a7db	Add parse_expr. Add more tests. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-17 18:35:50 -07:00
Leonardo de Moura	685aeae43a	Add parser skeleton Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-17 18:13:55 -07:00
Leonardo de Moura	f1961ab33f	Add another pp example Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-17 12:38:32 -07:00
Leonardo de Moura	80ec48c93d	Make sure formatter can be used even when associated frontend is not in scope. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-17 12:33:19 -07:00
Leonardo de Moura	6edae938b7	Improve list iterator Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-17 11:31:36 -07:00
Leonardo de Moura	a6f36ba546	Improve formatter usage. Fix bug in object printer. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-17 11:29:43 -07:00
Leonardo de Moura	0f3af23778	Fix crash when trying to format an object created by a different frontend. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-17 11:04:22 -07:00
Leonardo de Moura	b633c866e6	Expose environment API in the frontend object. Add support for formatting objects. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-17 10:55:42 -07:00
Leonardo de Moura	c6226c6951	Fix typo Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-16 20:51:11 -07:00
Leonardo de Moura	15c1c97873	Refactor frontend pretty printer Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-16 20:40:39 -07:00

... 21 22 23 24 25 ...

2561 commits