lean2

Author	SHA1	Message	Date
Leonardo de Moura	5b69f88664	feat(frontends/lean/notation_cmd): make the notation for setting precedence uniform Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-01 16:55:41 -07:00
Leonardo de Moura	ec3743dede	fix(frontends/lean/parser): avoid nontermination Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-01 16:46:58 -07:00
Leonardo de Moura	8cdf44b87b	feat(frontends/lean/notation_cmd): allow 'max' to use as a precedence level Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-01 16:46:32 -07:00
Leonardo de Moura	4cb5f97038	refactor(library/tactic): simplify tactic framework, no more proof builders Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-01 16:11:19 -07:00
Leonardo de Moura	c84218e24a	chore(frontends/lean/inductive_cmd): cleanup Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-30 17:16:10 -07:00
Leonardo de Moura	3e299a1d5a	refactor(frontends/lean/parser): move parser Lua bindings to a separate file Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-30 17:00:10 -07:00
Leonardo de Moura	bccc3df1aa	chore(frontends/lean): reduce code duplication Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-30 16:52:20 -07:00
Leonardo de Moura	cb000eda13	refactor(kernel): store binder_infor in local constants Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-30 11:37:46 -07:00
Leonardo de Moura	8d584e54da	feat(frontends/lean): add exact_apply Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-30 00:51:11 -07:00
Leonardo de Moura	ccdb96775f	feat(frontends/lean/parser): allow 'assume'/'take'/'fun' as notation for apply tactic Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-29 23:00:41 -07:00
Leonardo de Moura	33cb9382aa	feat(frontends/lean): add beta-reduction tactic command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-29 19:41:54 -07:00
Leonardo de Moura	360e9b9486	feat(library/tactic): add apply tactic Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-29 18:33:53 -07:00
Leonardo de Moura	6645fdeae0	feat(frontends/lean): add repeat tactic command, refactor tactic sequence notation Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-29 12:24:13 -07:00
Leonardo de Moura	2510d5722a	feat(frontends/lean): add unfold tactic command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-29 12:05:45 -07:00
Leonardo de Moura	6d09d82a7c	feat(frontends/lean): add notation for orelse tactic, add show and now tactics Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-29 11:39:18 -07:00
Leonardo de Moura	a1bbb09de4	feat(frontends/lean): add notation for then tactic Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-29 11:24:56 -07:00
Leonardo de Moura	6891f48c67	fix(library/module): do not store full path of imported modules Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-29 10:48:57 -07:00
Leonardo de Moura	1f0171cd57	fix(frontends/lean/dependencies): compilation warning Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-29 09:55:30 -07:00
Leonardo de Moura	ffa175009b	feat(frontends/lean): use tactics for solving unassigned metavariables Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-29 09:50:16 -07:00
Leonardo de Moura	1e39a21823	feat(frontends/lean): add basic tactics Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-29 09:03:51 -07:00
Leonardo de Moura	ec18bd93f9	feat(frontends/lean): send tactic hint table to elaborator Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-29 07:03:25 -07:00
Leonardo de Moura	65c63e146f	feat(frontends/lean): add display_deps function, and --deps command line option Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-28 18:35:18 -07:00
Leonardo de Moura	193ce35419	refactor(frontends/lean/inductive_cmd): redesign inductive datatype elaboration, use the new elaborator, and use simpler algorithm to infer the resulting universe Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-28 15:33:56 -07:00
Leonardo de Moura	0adacb5191	feat(kernel): add infer implicit, and use it to infer implicit arguments of inductive datatype eliminators, and tag whether parameters should be implicit or not in introduction rules in the module inductive_cmd Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-28 13:57:36 -07:00
Leonardo de Moura	0e015974ca	fix(library/unifier): bug in process_flex_rigid, also cleanup the code and break it into different cases Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-28 11:19:56 -07:00
Leonardo de Moura	47ff300d1a	fix(frontends/lean): '@' explicit mark Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-28 07:30:36 -07:00
Leonardo de Moura	cf9b486179	feat(frontends/lean): automatically import lua modules imported by imported lean files Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-27 23:23:51 -07:00
Leonardo de Moura	aaa7960b75	refactor(library/tactic/goal): use local names for hypotheses Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-27 11:11:12 -07:00
Leonardo de Moura	ccce9d90a4	feat(frontends/lean/elaborator): add 'delayed coercions', add example demonstrating why the new feature is useful Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-26 18:39:23 -07:00
Leonardo de Moura	e769121c2a	fix(frontends/lean/elaborator): memory leaks that only occur when compiling with clang++ Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-26 16:02:54 -07:00
Leonardo de Moura	16bdc51fc4	refactor(kernel/type_checker): simplify type checker API, and remove add_cnstr_fn Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-26 13:36:31 -07:00
Leonardo de Moura	930960c54d	fix(frontends/lean/builtin_cmds): abstract section parameters in the 'check' command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-26 10:06:50 -07:00
Leonardo de Moura	0480dab986	feat(frontends/lean/parse_table): avoid duplicates in the parse table Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-26 09:32:19 -07:00
Leonardo de Moura	2d2f23cda6	feat(library/lean/lean): improve overload error message Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-26 08:52:40 -07:00
Leonardo de Moura	656bcd55ed	fix(frontends/lean): save 'choice' position Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-26 08:50:44 -07:00
Leonardo de Moura	52ff29a6f7	feat(frontends/lean): add 'coercion' command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-26 08:08:39 -07:00
Leonardo de Moura	06f9e7bfdd	fix(build): add missing file Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-25 18:12:23 -07:00
Leonardo de Moura	acf8c13619	feat(kernel): add strict implicit arguments Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-25 17:50:49 -07:00
Leonardo de Moura	9f83ef8f6c	chore(frontends/lean/elaborator): cleanup Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-25 17:13:03 -07:00
Leonardo de Moura	543b1003a6	fix(frontends/lean/elaborator): typo Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-25 13:11:35 -07:00
Leonardo de Moura	f2b41312fb	feat(frontends/lean): add '@' explicit notation Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-25 12:50:47 -07:00
Leonardo de Moura	905209df1c	fix(frontends/lean/elaborator): to cache values, we must push/pop whenever we update the m_ctx Thus, we are disabling the cache for now. It is also unclear whether it is useful or not. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-25 11:05:14 -07:00
Leonardo de Moura	0791c83731	fix(frontends/lean/parser): add missing save_pos Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-25 10:32:43 -07:00
Leonardo de Moura	6db6048bf8	feat(library/error_handling): pretty print unifier exceptions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-25 09:41:25 -07:00
Leonardo de Moura	5b6589709c	fix(frontends/lean/decl_cmds): allow binders but no type in definitions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-25 09:00:57 -07:00
Leonardo de Moura	3e7dfa6212	fix(frontends/lean): infer type of definitions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-25 08:39:14 -07:00
Leonardo de Moura	d055c4880f	feat(frontends/lean): connect new elaborator to frontend Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-25 08:31:00 -07:00
Leonardo de Moura	fe0cee7536	feat(frontends/lean): add frontend elaborator Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-24 18:25:56 -07:00
Leonardo de Moura	603dafbaf7	refactor(kernel): remove 'let'-expressions We simulate it in the following way: 1- An opaque 'let'-expressions (let x : t := v in b) is encoded as ((fun (x : t), b) v) We also use a macro (let-macro) to mark this pattern. Thus, the pretty-printer knows how to display it correctly. 2- Transparent 'let'-expressions are eagerly expanded by the parser. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-24 16:27:27 -07:00
Leonardo de Moura	61595f516c	fix(frontends/lean/notation_cmd): initialization bug Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-23 16:20:28 -07:00
Leonardo de Moura	aa8b5655dd	feat(frontends/lean): add notation overwrite Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-23 16:10:36 -07:00
Leonardo de Moura	5bd86754af	feat(frontends/lean/builtin_cmds): change notation for marking implicit/cast parameter in sections Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-22 17:51:00 -07:00
Leonardo de Moura	c7c5e41653	fix(frontends/lean/parser): warning when compiling in release mode Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-22 09:58:05 -07:00
Leonardo de Moura	2589d60bfd	feat(frontends/lean): add nameless 'have' expression Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-20 17:18:18 -07:00
Leonardo de Moura	4b227409bf	feat(frontends/lean): add 'then have' expression Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-20 14:27:21 -07:00
Leonardo de Moura	4560413a92	feat(frontends/lean): add '[fact]' modifier for 'have' expression Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-20 11:58:05 -07:00
Leonardo de Moura	39177ec10a	feat(frontends/lean): flip definition modifiers position, now they must occur after the identifier Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-20 11:58:05 -07:00
Leonardo de Moura	16412daf39	feat(frontends/lean): add 'using' syntax sugar for adding expressions to the goal's context Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-20 11:58:05 -07:00
Leonardo de Moura	2cc8172d61	refactor(frontends/lean): remove m_pos field from parameter object Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-19 23:06:49 -07:00
Leonardo de Moura	05d1832425	refactor(kernel/type_checker): improve ensure_pi and ensure_sort APIs Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-19 22:33:58 -07:00
Leonardo de Moura	0cc8117fb4	fix(frontends/lean): add missing file Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-19 06:10:15 -07:00
Leonardo de Moura	bdab979e09	feat(frontends/lean): add inductive_cmd Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-18 16:00:59 -07:00
Leonardo de Moura	461689f758	refactor(frontends/lean/builtin_cmds): move declaration commands to new file Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-18 15:55:52 -07:00
Leonardo de Moura	08845be2fc	feat(frontends/lean/notation_cmd): improve 'notation' cmd Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-18 09:28:01 -07:00
Leonardo de Moura	3e3c4ee5ed	feat(frontends/lean/parser): add local_scope object to Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-18 08:38:23 -07:00
Leonardo de Moura	6259d20218	feat(frontends/lean/parser): expand Lua parser API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-18 08:03:17 -07:00
Leonardo de Moura	3ea24c0f32	fix(library/kernel_bindings): set_environment and set_io_state objects Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-17 22:36:47 -07:00
Leonardo de Moura	06002c5312	feat(frontends/lean/parser): use system_import when processing Lean import command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-17 22:09:42 -07:00
Leonardo de Moura	1378fa5cbb	refactor(util/script_state): remove support for threads and communication channels from the Lua API, the goal is to keep is simple, and use one Lua state object per thread Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-17 21:56:45 -07:00
Leonardo de Moura	f17e8a853a	feat(frontends/lean): allow parser actions to be implemented using Lua Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-17 21:56:16 -07:00
Leonardo de Moura	4cbc429192	feat(frontends/lean/calc): add parse_calc function Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-17 17:16:15 -07:00
Leonardo de Moura	037cfcf622	refactor(frontends/lean/notation_cmd): add register_notation_cmds procedure Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-17 13:39:44 -07:00
Leonardo de Moura	e178979061	feat(frontends/lean): add calc_subst, calc_refl, calc_trans commands for configuring calc-expressions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-17 13:35:31 -07:00
Leonardo de Moura	ddba6b222a	feat(frontends/lean): add calculational proof environment extension, it stores transitivity, reflexivity (and substitution) rules Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-17 13:13:13 -07:00
Leonardo de Moura	28c904abea	feat(frontends/lean/parser): add 'flag' for disabling 'unknown identifier' errors Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-17 10:30:03 -07:00
Leonardo de Moura	4be05e1d8c	refactor(frontends/lean): expose notation_entry and token_entry structures, and add functions for parsing notation without affecting the environment Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-17 10:12:04 -07:00
Leonardo de Moura	819c8276f2	feat(frontends/lean/builtin_cmds): add 'variables' command family Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-17 08:25:00 -07:00
Leonardo de Moura	ea49176043	feat(frontends/lean/builtin_cmds): add 'using' command, and 'hiding/renaming' directives Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-16 18:42:39 -07:00
Leonardo de Moura	639d58f4c7	feat(frontends/lean/builtin_cmds): add 'print options' command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-16 17:31:28 -07:00
Leonardo de Moura	3e377a9732	feat(frontends/lean/builtin_cmds): add 'set_option' command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-16 17:27:43 -07:00
Leonardo de Moura	82e79d9c78	fix(frontends/lean/parser): style Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-16 16:54:44 -07:00
Leonardo de Moura	a964ceb0e2	feat(frontends/lean): add 'import' command, add command line option for setting number of threads Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-16 16:37:46 -07:00
Leonardo de Moura	4f3da90443	feat(frontends/lean/builtin_exprs): add 'have' and 'show' expressions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-16 15:04:29 -07:00
Leonardo de Moura	07f2379dec	refactor(kernel): add mk_local function that has only two arguments Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-16 14:27:26 -07:00
Leonardo de Moura	f1e3449aae	fix(frontends/lean): propagate position information Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-16 13:20:10 -07:00
Leonardo de Moura	f70b1b028a	feat(frontends/lean): provide position to parse_fn external function, add 'by' expression Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-16 12:28:58 -07:00
Leonardo de Moura	34dfacc10e	refactor(frontends/lean): Bool does not need to be a reserved keyword Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-16 10:52:12 -07:00
Leonardo de Moura	6db265e7ab	feat(frontends/lean/builtin_exprs): parse '_' placeholder Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-16 10:41:08 -07:00
Leonardo de Moura	5ce0502a36	feat(frontends/lean/builtin_exprs): add parser for 'let' expressions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-16 09:50:34 -07:00
Leonardo de Moura	775e10186d	refactor(parser): use 'scope objects' for creating local scopes and setting m_type_use_placeholder flag Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-16 09:24:41 -07:00
Leonardo de Moura	27130c9499	feat(frontends/lean): local notation 'shadows' global one Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-15 11:50:41 -07:00
Leonardo de Moura	28047a33ae	feat(frontends/lean): add local notation support Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-15 11:30:52 -07:00
Leonardo de Moura	64cafd6875	feat(frontends/lean/notation_cmd): add 'notation' command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-15 10:49:05 -07:00
Leonardo de Moura	9b389a96d5	feat(frontends/lean/notation_cmd): modify infixl/infixr/postfix command syntax Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-15 08:28:49 -07:00
Leonardo de Moura	e7019ec840	feat(frontends/lean): add infixl/infixr/postfix/precedence commands, add support for storing notation in .olean files, add support for organizing notation into namespaces Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-14 22:13:25 -07:00
Leonardo de Moura	891a3fb48b	feat(frontends/lean): add command block reader with snapshot and resume Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-14 14:13:32 -07:00
Leonardo de Moura	6b99a29c2c	refactor(frontends/lean): add local_decls template that is cheap to copy Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-14 09:56:05 -07:00
Leonardo de Moura	5fee6fd140	feat(shell/lean): add '-o' command line option Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-14 08:10:43 -07:00
Leonardo de Moura	282a35bd1b	feat(frontends/lean): add '#setline' directive Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-14 07:28:56 -07:00
Leonardo de Moura	48c58af9b5	feat(frontends/lean/parser): allow explicit universe level to be provided to aliases and locals Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-13 18:00:52 -07:00
Leonardo de Moura	a65c43c0db	feat(frontends/lean/builtin_cmds): add definition command family Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-13 17:30:35 -07:00
Leonardo de Moura	01cecb76db	feat(frontends/lean/builtin_cmds): add 'variable' command family Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-13 15:13:50 -07:00
Leonardo de Moura	ce259e6265	feat(frontends/lean/parser): add namespace/section/end commands, add support for explicit universe levels, fix Type notation' Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-13 11:34:43 -07:00
Leonardo de Moura	5aca452439	feat(library/aliases): add 'exceptions' and support for universes to add_aliases procedure, add for_each_universe method to environment Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-13 08:26:05 -07:00
Leonardo de Moura	d50376249f	feat(library/aliases): add level aliases Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-12 12:35:02 -07:00
Leonardo de Moura	3bde699fbe	feat(frontends/lean/parser): add parse_level Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-12 12:34:55 -07:00
Leonardo de Moura	5a008717a4	feat(frontends/lean/parser): add parse_notation Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-11 21:00:34 -07:00
Leonardo de Moura	e7d7996fa9	feat(frontends/lean/parser): add parser_binder(s) and abstract methods Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-11 18:51:12 -07:00
Leonardo de Moura	959c3ffc68	feat(frontends/lean/parser): add parse_id method Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-11 15:09:16 -07:00
Leonardo de Moura	1972a09021	feat(frontends/lean/builtin_cmds): add simple 'print' command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-11 14:35:34 -07:00
Leonardo de Moura	7fd502993b	refactor(frontends/lean/cmd_table): remove register_builtin_cmd procedures, they would cause initialization problems Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-11 14:35:34 -07:00
Leonardo de Moura	2e8ebb6d9e	feat(frontends/lean/parser): add 'parse_commands' and 'parse_script' Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-11 14:32:07 -07:00
Leonardo de Moura	8fcc25d55a	fix(frontends/lean/token_table): static initialization problem Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-11 10:56:04 -07:00
Leonardo de Moura	3dc26666b9	feat(frontends/lean): add parser interface Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-10 18:20:59 -07:00
Leonardo de Moura	d3e3301208	refactor(frontends/lean/scanner): use the parser configuration in the environment Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-10 10:59:12 -07:00
Leonardo de Moura	e2adb101d5	feat(frontends/lean): add parser_config environment extension Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-10 10:39:22 -07:00
Leonardo de Moura	d81df2efe2	feat(frontends/lean/parse_table): add use_lambda_abstraction flag to scoped_expr_actions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-10 09:39:01 -07:00
Leonardo de Moura	546f9dc00b	chore(frontends/lean): use consistent name conventions, rename token_set to token_table Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-10 09:18:57 -07:00
Leonardo de Moura	00e0cc15ba	feat(frontends/lean/token_set): add token_set Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-09 16:49:22 -07:00
Leonardo de Moura	af0c93e0eb	feat(frontends/lean/parse_table): add typedef for notation::parse_table Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-09 15:54:56 -07:00
Leonardo de Moura	439b6c1e96	feat(frontends/lean/parse_table): add parse_table Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-09 15:33:39 -07:00
Leonardo de Moura	722ea7273e	feat(frontends/lean): add parse_table datastructure Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-09 13:20:33 -07:00
Leonardo de Moura	d10d70423a	feat(frontends/lean): add new scanner Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-05 18:57:26 -07:00
Leonardo de Moura	4cf1b05831	refactor(library/token_set): move to frontends/lean Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-05 13:10:50 -07:00
Leonardo de Moura	e79e0302d0	fix(frontends/lean): style Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-15 16:09:21 -07:00
Leonardo de Moura	c6af56260e	refactor(frontends/lean): remove dead code Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-15 15:51:41 -07:00
Leonardo de Moura	f7e705badb	refactor(library/kernel_bindings): reactive some of the kernel Lua bindings Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-29 11:52:09 -07:00
Leonardo de Moura	af927ecb7a	refactor(frontends/lua): reactivate some of the Lua extensions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-28 17:57:39 -07:00
Leonardo de Moura	aa8240985a	test(examples/lean): small version of algebraic hierarchy (proof of concept) Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-24 20:51:19 -08:00
Leonardo de Moura	d79e9af210	fix(frontends/lean): help msg Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-18 09:31:30 -08:00
Leonardo de Moura	0878b44fc7	feat(frontends/lean): allow user to import several theories using a single import Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-11 17:15:12 -08:00
Leonardo de Moura	a2d2e36f04	refactor(frontends/lean): remove notation for creating tuples Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-10 09:03:42 -08:00
Leonardo de Moura	633ed6bb69	fix(frontends/lean/parser): bug in add_rewrite Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-09 09:46:56 -08:00
Leonardo de Moura	b24c085cb0	feat(frontends/lean): avoid warning message Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-09 09:26:51 -08:00
Leonardo de Moura	24528ff685	fix(library/elaborator): fix glitches in the elaborator that were forcing us to provide parameters explicitly Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-07 18:02:08 -08:00
Leonardo de Moura	1ec01f5757	refactor(builtin): merge pair.lean with kernel.lean, and add basic theorems Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-07 16:04:44 -08:00
Leonardo de Moura	ad7b13104f	feat(*): add support for heterogeneous equality in the parser, elaborator and simplifier, adjusts unit test to reflect changes Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-07 15:03:16 -08:00
Leonardo de Moura	6d7ec9d7b6	refactor(kernel): add heterogeneous equality back to expr The main motivation is that we will be able to move equalities between universes. For example, suppose we have A : (Type i) B : (Type i) H : @eq (Type j) A B where j > i We didn't find any trick for deducing (@eq (Type i) A B) from H. Before this commit, heterogeneous equality as a constant with type heq : {A B : (Type U)} : A -> B -> Bool So, from H, we would only be able to deduce (@heq (Type j) (Type j) A B) Not being able to move the equality back to a smaller universe is problematic in several cases. I list some instances in the end of the commit message. With this commit, Heterogeneous equality is a special kind of expression. It is not a constant anymore. From H, we can deduce H1 : A == B That is, we are essentially "erasing" the universes when we move to heterogeneous equality. Now, since A and B have (Type i), we can deduce (@eq (Type i) A B) from H1. The proof term is (to_eq (Type i) A B (to_heq (Type j) A B H)) : (@eq (Type i) A B) So, it remains to explain why we need this feature. For example, suppose we want to state the Pi extensionality axiom. axiom hpiext {A A' : (Type U)} {B : A → (Type U)} {B' : A' → (Type U)} : A = A' → (∀ x x', x == x' → B x == B' x') → (∀ x, B x) == (∀ x, B' x) This axiom produces an "inflated" equality at (Type U) when we treat heterogeneous equality as a constant. The conclusion (∀ x, B x) == (∀ x, B' x) is syntax sugar for (@heq (Type U) (Type U) (∀ x : A, B x) (∀ x : A', B' x)) Even if A, A', B, B' live in a much smaller universe. As I described above, it doesn't seem to be a way to move this equality back to a smaller universe. So, if we wanted to keep the heterogeneous equality as a constant, it seems we would have to support axiom schemas. That is, hpiext would be parametrized by the universes where A, A', B and B'. Another possibility would be to have universe polymorphism like Agda. None of the solutions seem attractive. So, we decided to have heterogeneous equality as a special kind of expression. And use the trick above to move equalities back to the right universe. BTW, the parser is not creating the new heterogeneous equalities yet. Moreover, kernel.lean still contains a constant name heq2 that is the heterogeneous equality as a constant. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-07 10:28:10 -08:00
Leonardo de Moura	ff955f9830	chore(frontends/lean/parser): update comments Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-06 20:56:31 -08:00
Leonardo de Moura	593f1f2ebd	fix(frontends/lean): allow user set constants defined in other namespaces as opaque Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-06 20:56:31 -08:00
Leonardo de Moura	4b4b5e3345	fix(frontends/lean): import explicit versions when using the command 'using' Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-06 17:33:58 -08:00
Leonardo de Moura	ea06bb2885	feat(frontends/lean/pp): change how lift local entries are pretty printed Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-06 17:26:38 -08:00
Leonardo de Moura	a51139e63b	feat(frontends/lean): position information in error messages Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-06 17:26:38 -08:00
Leonardo de Moura	e85b1f1ac0	feat(library/elaborator): expose elaborator configuration options Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-06 17:26:38 -08:00
Leonardo de Moura	1d23d93e60	feat(frontends/lean): new 'have' expression Add 'have' notation suggested by Jeremy Avigad. Add his example to the test suite. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-06 08:03:59 -08:00
Leonardo de Moura	ba9a8f9d98	feat(frontends/lean): add 'show' expression syntax sugar Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-06 07:50:22 -08:00
Leonardo de Moura	493007b7bc	fix(frontends/lean/pp): bug in tuple/pair pretty printing Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-04 13:58:01 -08:00
Leonardo de Moura	c9b72df34b	fix(frontends/lean/parser): bug when applying tactics to synthesize remaining meta-variables Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-04 11:36:26 -08:00
Leonardo de Moura	9dc86e3cf5	fix(builtin/kernel): rename generalized proof_irrel axiom to hproof_irrel, and derive the restricted one Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-04 10:06:29 -08:00
Leonardo de Moura	61d0c792ff	fix(frontends/lean/parser): bug in tuple/proj1/proj2 Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-03 22:46:29 -08:00
Leonardo de Moura	4fcc292332	feat(frontends/lean): parse and pretty print pair/tuple projection operators proj1 and proj2, fix bug in the type checker Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-03 22:10:01 -08:00
Leonardo de Moura	cc96b50644	feat(frontends/lean): support for nary-tuples, improve notation for non-dependent tuples, add support in the elaborator for sigma types Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-03 20:53:11 -08:00
Leonardo de Moura	5c991f8fbf	feat(frontends/lean): parse and pretty print tuples/pairs This commit also fixes a bug in the type checker when processing dependent pairs. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-03 20:10:30 -08:00
Leonardo de Moura	5e5ab1429d	feat(frontends/lean): parse and pretty print sigma types This commit also fixes some bugs in the implementation of Sigma types. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-03 18:16:00 -08:00
Leonardo de Moura	c56df132b8	refactor(kernel): remove semantic attachments from the kernel Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-02 14:48:27 -08:00
Leonardo de Moura	759aa61f70	refactor(builtin/kernel): define if-then-else using Hilbert's operator Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-30 19:28:42 -08:00
Leonardo de Moura	b45ab9dc30	feat(library/elaborator): use equality constraints instead of convertability constraints on definitions Convertability constraints are harder to solve than equality constraints, and it seems they don't buy us anything definitions. They are just increasing the search space for the elaborator. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-30 14:13:21 -08:00
Leonardo de Moura	ea6bf224e5	feat(frontends/lean): make the parser accept (Type -> ...) Before this commit, the parser would accept only a universe level or a ')' after '(' 'Type' Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-29 15:23:20 -08:00
Leonardo de Moura	4dc3aa46c3	feat(frontends/lean): allow tactics to be used in axiom/variable declarations and in the type of definitions/theorems; add a new test showing the need for this feature Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-29 12:02:12 -08:00
Leonardo de Moura	f0a2d3627e	refactor(frontends/lean): use ascii prefix for auxiliary let-declarations Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-29 11:58:09 -08:00
Leonardo de Moura	7f53cb9601	feat(frontends/lean/parser): add_rewrite take the 'using' command into account Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-28 01:15:28 -08:00
Leonardo de Moura	4d25cb7f47	feat(library/tactic): add simplify_tactic based on the simplifier Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-26 18:53:18 -08:00
Leonardo de Moura	e8bba1ebf3	fix(frontends/lean/frontend): the definition of the explicit version @f must be definitionally equal to f Before this commit, the explicit version @f of a constant f with implicit arguments as not definitionally equal to f. For example, if we had variable f {A : Type} : A -> Bool Then, the definition of @f was definition @f (A : Type) (a : A) : Bool := f A a This definition is equivalent to fun A a, f A a which is not definitionally equal to f since definitionally equality in Lean ignores Eta conversion. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-25 20:34:28 -08:00
Leonardo de Moura	6bc1537e25	feat(frontends/lean/parser): allow the user to write (Type) without providing a level Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-25 20:17:36 -08:00
Leonardo de Moura	8f455f5965	fix(frontends/lean): bug in scope construct Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-24 17:23:29 -08:00
Leonardo de Moura	7f3e2b3ef4	fix(frontends/lean/parser): bug in 'using' construct Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-24 17:09:46 -08:00
Leonardo de Moura	1638a7bb02	fix(frontends/lean/pp): compute local shared nodes, and avoid unnecessary let's Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-22 21:44:24 -08:00
Leonardo de Moura	ad219d43d9	refactor(*): semantic attachment parsing and simplification Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-20 14:44:45 -08:00
Leonardo de Moura	90ffb9d5ec	fix(frontends/lean/pp): bug in pp_abstraction_core Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-19 19:47:40 -08:00
Leonardo de Moura	d322f63113	feat(frontends/lea): add commands for creating and managing rewrite rule sets Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-19 12:03:59 -08:00
Leonardo de Moura	a43020b31b	refactor(kernel): remove heterogeneous equality Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-16 17:39:12 -08:00
Leonardo de Moura	14c6218bdc	chore(kernel): file name convention Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-15 20:06:29 -08:00
Leonardo de Moura	3ab2d2a441	fix(frontends/lean/parser): memory leak due to g++ bug g++ implementation of std::initializer_list has bug. http://gcc.gnu.org/ml/gcc-bugs/2013-06/msg00095.html This commit memory leaks triggered by this bug. It also adds minimal tests to expose three different instances of the problem. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-15 10:15:04 -08:00
Leonardo de Moura	83efa644d1	fix(frontends/lean/parser): uninitialized var error reported by valgrind Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-15 08:43:43 -08:00
Leonardo de Moura	28eb980484	fix(build): C++ module dependency problem, and style Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-14 18:30:31 -08:00
Leonardo de Moura	c8e1ec87d2	feat(library/simplifier): add to_ceqs function that converts a theorem into a sequence of conditional equations Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-14 18:30:19 -08:00
Leonardo de Moura	ccb9faf065	refactor(*): error messages Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-13 16:54:21 -08:00
Leonardo de Moura	55aa4cbfa3	feat(frontends/lean): improve error message for expressions containing unsolved metavariables Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-13 13:21:44 -08:00
Leonardo de Moura	12451e4a35	feat(frontends/lean/pp): display implicit arguments when expression contains metavariables Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-13 12:42:05 -08:00
Leonardo de Moura	35bacf95fc	feat(shell): provide the default environment when parsing Lua files Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-12 18:21:14 -08:00
Leonardo de Moura	582569b793	feat(frontends/lean): allow the user to set the trust_imported flag when creating environments using Lua Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-12 16:46:53 -08:00
Leonardo de Moura	65bdb9c7e0	fix(frontends/lean): unprotected call to Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-09 19:56:20 -08:00
Leonardo de Moura	411f14415d	feat(builtin): automatically generate Lean/C++ interface for builtin theories Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-09 18:09:53 -08:00
Leonardo de Moura	a339a53f50	feat(util/options): 'verbose' as a system option, add -q (quiet) option Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-09 15:31:58 -08:00
Leonardo de Moura	2179e57db3	refactor(builtin): move if_then_else to its own module Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-09 14:08:39 -08:00
Leonardo de Moura	fdeb457a81	feat(kernel/pos_info_provider): add support for file names in pos_info_provider The idea is to include the file name when displaying justification objects. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-09 12:19:30 -08:00
Leonardo de Moura	84e211b81b	fix(frontends/lean): missing ':' in error messages Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-09 11:19:58 -08:00
Leonardo de Moura	f7c7dd4ed4	feat(frontends/lean): include filename in error messages, use GNU error message style Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-09 11:01:27 -08:00
Leonardo de Moura	57c0006916	chore(*): cleanup lean builtin symbols, replace :: with _ Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-09 08:33:52 -08:00
Leonardo de Moura	048151487e	feat(kernel): use Pi as forall/implication Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-08 00:38:39 -08:00
Leonardo de Moura	6f4ca7bd2a	feat(frontends/lean): expose is_explicit function in the Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-07 17:36:27 -08:00
Leonardo de Moura	a3af87f8d3	chore(frontends/lean/frontend): remove dead code Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-07 15:28:21 -08:00
Leonardo de Moura	0363faeec8	fix(frontends/lean/scanner): assertion violation, and add more tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-07 15:12:34 -08:00
Leonardo de Moura	fb73514913	fix(frontends/lean/parser): parser aborted if the scanner throws an exception in the first call to scan(); position information was being shown twice for scanner exceptions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-07 15:04:30 -08:00
Leonardo de Moura	c7338a8eab	chore(frontends/lean/scanner): remove dead code Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-07 14:37:28 -08:00
Leonardo de Moura	0f1737d62c	fix(frontends/lean): more precise position information for infix operators Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-07 13:19:26 -08:00
Leonardo de Moura	abb9b8af83	fix(frontends/lean): bug in pop::context command, and add new tests for the universe command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-06 17:14:07 -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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	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
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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	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
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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	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
Soonho Kong	044813615e	fix: add '#include <tuple>'	2013-11-03 13:00:42 -05: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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	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	ab6ca82e6f	Update to suppress unused-parameter warnings	2013-09-19 22:40:34 -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	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	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	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	bc60b47295	Apply coding style	2013-09-13 18:48:09 -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	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	3657320edb	Add basic list functions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-11 19:48:54 -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
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	2ca30571b4	Display the input term in the output of the Check command. It is useful to see the fully elaborated term. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-08 22:55:21 -07:00
Leonardo de Moura	59a589037e	Keep expanded form when pretty printings variable declarations with implicit marks (i.e., curly braces) Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-08 11:23:46 -07:00
Leonardo de Moura	df116f88e0	Improve pretty printer for Pi's Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-08 11:04:07 -07:00
Leonardo de Moura	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	c674bb3790	Add castlib as an independent library Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-06 23:40:47 -07:00

... 7 8 9 10 11 ...

927 commits