Commit graph

3678 commits

Author SHA1 Message Date
Leonardo de Moura
1d62a614e7 fix(frontends/lean): remove keywords 'class' and '[class]'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-30 15:05:44 -07:00
Leonardo de Moura
9637ceb86e feat(frontends/lean): allow user to provide a terminator for 'foldr' and 'foldl'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-30 15:04:44 -07:00
Leonardo de Moura
5238da9ac7 refactor(frontends/lean): rename action::is_compatible to action::is_equal
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-30 12:37:35 -07:00
Leonardo de Moura
450131692a fix(library/converter): missing constraint on eta expansion
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-30 10:43:47 -07:00
Leonardo de Moura
b4700e4eed chore(build): eliminate artificial dependencies
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-29 18:25:57 -07:00
Leonardo de Moura
936bb2744b fix(library/unifier): add a flag to sign that a choice constraint owns a metavariable ?m, that is, it has the right to assign ?m, and the unifier should postpone any other constraint that tries to assign ?m
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-29 17:32:55 -07:00
Leonardo de Moura
6e135832d8 feat(frontends/lean/pp): pretty print '@' explict operator
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-29 14:26:27 -07:00
Leonardo de Moura
320bc55e85 fix(frontends/lean/elaborator): use preprocessed expression when displaying errors
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-29 14:25:50 -07:00
Leonardo de Moura
634363c5ec fix(frontends/lean/dependencies): dependency generation
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-29 14:13:31 -07:00
Leonardo de Moura
b15f1bb8c7 fix(frontends/lean/elaborator): apply coercions in definitions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-29 13:55:39 -07:00
Leonardo de Moura
501cae37e5 fix(frontends/lean/parser): bug in check_constant_next (when invoked inside of a section)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-29 13:04:58 -07:00
Leonardo de Moura
c0039735f4 feat(emacs): add shortcut for using --hott option
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-29 10:57:52 -07:00
Leonardo de Moura
793b2817ec fix(util/lean_path): clear g_lean_path_vector before (re-)initializing it
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-29 10:57:20 -07:00
Leonardo de Moura
8278700b47 feat(build): copy lean executable to bin directory
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-29 10:25:55 -07:00
Leonardo de Moura
f8eba36b0a fix(build): set LEAN_PATH before make standard and hott libraries
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-29 10:06:39 -07:00
Leonardo de Moura
7df78ea503 feat(kernel): add combinator for combining normalizer_extensions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-29 10:00:40 -07:00
Leonardo de Moura
33c77afc29 feat(frontends/lean/structure): add 'structure' command skeleton
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-28 19:59:38 -07:00
Leonardo de Moura
105c29b51e refactor(library/standard): use new coding style, rename bool.b0 and bool.b1 to bool.ff and bool.tt
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-28 19:59:38 -07:00
Leonardo de Moura
df8b88dca2 chore(doc/todo): update todo list
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-28 12:08:54 -07:00
Leonardo de Moura
2b4bd66081 feat(build): generate tests for all code blocks in org-files, and examples at ./examples/standard
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-28 12:06:11 -07:00
Leonardo de Moura
8ad6d7a98b doc(doc/lean): update Lean tutorial to Lean 0.2, and use org-mode
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-28 10:52:09 -07:00
Leonardo de Moura
5f360cd8ec feat(kernel/error_msgs): improve application type mismatch error messages
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-28 07:08:12 -07:00
Leonardo de Moura
555425539d refactor(kernel/error_msgs): remove dead code
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-28 06:52:59 -07:00
Leonardo de Moura
acf8a4261b doc(examples/standard/constable): add section delimiters
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-28 01:17:31 -07:00
Leonardo de Moura
fb56767e07 doc(examples/standard): add theorems and exercises from Bob Constable
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-28 01:13:21 -07:00
Leonardo de Moura
864fdd37da refactor(library/aliases): aliases are from name to names
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-27 21:01:59 -07:00
Leonardo de Moura
5555d620cf feat(library/standard): add or_inl and or_inr as short-hands for the commonly used 'or_intro_left _' and 'or_intro_right _'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-27 17:25:57 -07:00
Leonardo de Moura
d1fe1286c0 fix(library/unifier): bug introduced today in consume_tc_cnstrs
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-27 17:16:30 -07:00
Leonardo de Moura
bc0a8b8da4 feat(emacs): make lean-mode org-mode friendly
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-27 17:03:06 -07:00
Leonardo de Moura
99a1966fd6 refactor(library/standard/set): use the same style for mem_inter and mem_union
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-27 13:32:59 -07:00
Leonardo de Moura
88130f339e feat(library/standard): add basic set theory that does not rely on classical axioms
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-27 13:18:33 -07:00
Leonardo de Moura
3a77226b92 feat(library/standard/bool): add bor_to_or theorem
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-27 13:17:55 -07:00
Leonardo de Moura
25f7929ea3 feat(library/standard/bool): add band_assoc and bor_assoc theorems
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-27 12:50:57 -07:00
Leonardo de Moura
4b2e403023 test(tests/lean/run): add more tests sent by Cody
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-27 12:17:38 -07:00
Leonardo de Moura
faee08591f fix(*): make sure elaborator and type_checker use the same "rules" for treating opaque definitions
This is a big change because we have to store in constraints whether we can use the "relaxed" rules or not.
The "relaxed" case says that when type checking the value of an opaque definition we can treat other opaque definitions in the same module as transparent.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-27 12:12:54 -07:00
Leonardo de Moura
83d38674c9 feat(kernel/error_msgs): improve cryptic type mismatch error messages where the types may seem identical because key information is being suppressed
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-27 09:41:25 -07:00
Leonardo de Moura
6ca120bf77 test(tests/lean/run): add Cody's file to test suite
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-27 08:17:46 -07:00
Leonardo de Moura
0cdd4a267c feat(frontends/lean/pp): pretty print 'show' expressions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-26 21:56:35 -07:00
Leonardo de Moura
60cc9ac8e2 feat(frontends/lean/pp): pretty print 'have' expressions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-26 21:35:26 -07:00
Leonardo de Moura
cf35c07786 fix(frontends/lean): fix 'let' annotation placement and pretty printer
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-26 21:00:22 -07:00
Leonardo de Moura
206206060f test(tests/lean/hott): add some of Vladimir's definitions as tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-26 20:50:37 -07:00
Leonardo de Moura
8e402ae862 fix(kernel/type_checker): error message position information
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-26 20:33:44 -07:00
Leonardo de Moura
cb232f2a9b fix(kernel/inductive): use has_expr_metavar_strict instead of has_expr_metavar
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-26 19:57:54 -07:00
Leonardo de Moura
5c5dea7c8e feat(kernel/expr): add has_expr_metavar_strict
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-26 19:54:04 -07:00
Leonardo de Moura
d9ee994281 feat(library/hott): copy basic files to hott library
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-26 19:13:04 -07:00
Leonardo de Moura
5bf3197306 refactor(frontends/lean): create theorem_queue class
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-26 15:00:51 -07:00
Leonardo de Moura
78a1670905 refactor(frontends/lean): cleanup add_delayed_theorem method
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-26 14:01:20 -07:00
Leonardo de Moura
70ef92cd5e feat(build): add tests/lean/slow test directory, and add nat_wo_hints.lean file that elaborates nat.lean without using any hint
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-26 10:53:44 -07:00
Leonardo de Moura
23af5ab217 fix(library/unifier): eager whnf application
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-26 10:37:02 -07:00
Leonardo de Moura
556861c8d6 fix(library/unifier): remove incorrect assertion
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-26 07:52:10 -07:00