lean2

Author	SHA1	Message	Date
Leonardo de Moura	4424a314e0	feat(kernel): add get_universe_distance method Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-06 17:13:13 -08:00
Leonardo de Moura	5fe8c32da9	feat(kernel): use new universe contraints in the environment, allow new constraints to be added Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-06 16:46:11 -08:00
Leonardo de Moura	b5a30855f8	feat(kernel/universe_constraints): add new class for managing universe constraints Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-06 15:01:28 -08:00
Leonardo de Moura	68832dc6f2	fix(builtin/macros): comments Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-06 12:07:13 -08:00
Leonardo de Moura	929a536e2f	fix(builtin/README): update documentation Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-06 12:03:11 -08:00
Leonardo de Moura	62bb2ab2f9	fix(builtin/Nat): name convention Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-06 11:41:14 -08:00
Leonardo de Moura	645e748302	feat(frontends/lean): add 'using' command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-06 11:41:14 -08:00
Leonardo de Moura	8c956280d9	chore(frontends/lean): rename setoption and setopaque commands to set::option and set::opaque Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-06 11:41:03 -08:00
Leonardo de Moura	7222a2d1a9	feat(builtin/kernel): use the same notation for mp, eq::mp and forall::elim Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-05 21:39:31 -08:00
Leonardo de Moura	935c2a03a3	feat(*): change name conventions for Lean builtin libraries Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-05 19:21:44 -08:00
Leonardo de Moura	771b099c0c	fix(frontends/lean): must invoke lua GC before closing a scope, reason: we may still have references to the current environment inside of the Lua state object Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-05 16:38:29 -08:00
Leonardo de Moura	9d6bd7501c	feat(doc/lean): include lean documentation scripts in the test set Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-05 13:16:47 -08:00
Leonardo de Moura	4ba097a141	feat(frontends/lean): use lowercase commands, replace 'endscope' and 'endnamespace' with 'end' Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-05 13:06:36 -08:00
Leonardo de Moura	6569b07b7c	feat(frontends/lean/parser): rename 'show' expression to 'have' Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-05 11:25:58 -08:00
Leonardo de Moura	0b4bdceb10	feat(builtin/macros): rename 'For' macro to 'take' Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-05 11:08:55 -08:00
Leonardo de Moura	9f08156a73	feat(frontends/lean/parser): combine Echo and Show commands into the 'print' command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-05 11:03:35 -08:00
Leonardo de Moura	ce1213a020	feat(frontends/lean): use '(* ... )' instead of '(* ... **)' for script code blocks Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-05 10:32:47 -08:00
Leonardo de Moura	028a9bd9bd	feat(frontends/lean/scanner): use Lua style comments in Lean Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-05 08:53:27 -08:00
Leonardo de Moura	f5cc2458a9	fix(frontends/lean/parser_calc): missing save calls Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-03 18:26:30 -08:00
Leonardo de Moura	fbe0bccf51	chore(*): name convention, proof construnction functions/macros start with upper-case Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-03 18:11:01 -08:00
Leonardo de Moura	9eb4dc4a81	feat(kernel, library/elaborator, frontends/lean): improve how elaborator_exceptions are displayed in the Lean frontend This commit affects different modules. I used the following approach: 1- I store the metavariable environment at unification_failure_justifications. The idea is to capture the set of instantiated metavariables at the time of failure. 2- I added a remove_detail function. It removes propagation steps from the justification tree object. I also remove the backtracking search space associated with higher-order unificiation. I keep only the search related to case-splits due to coercions and overloads. 3- I use the metavariable environment captured at step 1 when pretty printing the justification of an elaborator_exception. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-03 17:18:23 -08:00
Leonardo de Moura	66ec538c63	doc(doc/lean/calc.md): calculational proof documentation Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-03 11:52:21 -08:00
Leonardo de Moura	5b5cebe750	refactor(builtin/Nat): use obtain-from instead of ExistsElim, and use more user-friendly argument order for Induction Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-03 10:33:57 -08:00
Leonardo de Moura	9f3706e365	feat(builtin/macros): add obtain-from macro for ExistsElim Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-03 10:32:49 -08:00
Leonardo de Moura	d7efdff83d	feat(builtin/Nat): add more leq theorems Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-02 22:48:10 -08:00
Leonardo de Moura	cf35e7bed7	feat(frontends/lean): add support for disequalities in calculational proofs Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-02 22:47:45 -08:00
Leonardo de Moura	6329d1828d	feat(frontends/lean): reuse name expression Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-02 20:08:21 -08:00
Leonardo de Moura	92c7145d7f	feat(kernel/expr): maximize sharing before serializing Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-02 20:03:42 -08:00
Leonardo de Moura	2d5800ace4	feat(builtin/Nat): leq axiom, and some theorems Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-02 18:24:32 -08:00
Leonardo de Moura	9620b00e24	feat(kernel/metavar): is instantiate_metavars, we are also instantiating assigned metavariables that occur in the local context of unassinged ones. This modification improves the effectiveness of the process_metavar_inst procedure in the Lean elaborator. For example, suppose we have the constraint ctx \|- ?M1[inst:0 ?M2] == a If ?M1 and ?M2 are unassigned, then we have to consider the two possible solutions: ?M1 == a or ?M1 == #0 and ?M2 == a On the other hand, if ?M2 is assigned to b, then we can ignore the second case. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-02 16:08:38 -08:00
Leonardo de Moura	ecc5d1bc3a	refactor(kernel): move printer to library, cleanup io_state interface Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-02 13:37:50 -08:00
Leonardo de Moura	0592261847	refactor(kernel/io_state): move io_state_stream to library Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-02 13:14:21 -08:00
Leonardo de Moura	b81d3309b9	fix(kernel): remove ios hack Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-02 13:03:25 -08:00
Leonardo de Moura	9c5fa72f56	fix(library/elaborator): avoid unused variable warning in release build Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-02 12:40:41 -08:00
Leonardo de Moura	430b75f38f	test(tests/lean): add version of the Nat library full of holes Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-02 12:31:13 -08:00
Leonardo de Moura	307099b1cb	refactor(builtin/Nat): cleanup all proofs using calculational proof style Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-02 12:13:26 -08:00
Leonardo de Moura	e714bd7982	feat(frontends/lean): add syntax sugar for applying Subst in calculational proofs Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-02 11:23:55 -08:00
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

... 6 7 8 9 10 ...

1848 commits