Leonardo de Moura
7bf3e2ffbb
fix(compiler/simp_pr1_rec): typo
2016-05-01 16:47:53 -07:00
Leonardo de Moura
d86772e986
fix(library/type_context): compilation errors in debug mode
2016-05-01 12:05:42 -07:00
Leonardo de Moura
d64a8d24f9
fix(library/replace_visitor): remove replace_visitor_closed, it does not handle nested let-expr correctly
2016-05-01 12:04:28 -07:00
Leonardo de Moura
f2c10b0cee
feat(compiler): add compiler_step_visitor helper class
2016-05-01 12:02:42 -07:00
Leonardo de Moura
847e1c60e7
refactor(compiler/util): use new kernel type_checker
2016-05-01 10:49:36 -07:00
Leonardo de Moura
e2c1c7f3a4
feat(compiler): add mk_fresh_constant
2016-05-01 10:21:59 -07:00
Leonardo de Moura
92325f9295
fix(compiler/preprocess_rec): fix expand_aux_recursors_fn
2016-04-28 17:41:08 -07:00
Leonardo de Moura
21daa18950
chore(compiler/simp_pr1_rec): cleanup
2016-04-28 17:40:34 -07:00
Leonardo de Moura
0b3e23892b
refactor(library/replace_visitor): add replace_visitor_closed
2016-04-28 17:09:02 -07:00
Leonardo de Moura
836b3bfe95
refactor(compiler/preprocess_rec): make sure expand_aux_recursors does not depend on old code
2016-04-28 16:40:24 -07:00
Leonardo de Moura
f05e52e59f
fix(library/init/nat): recursor attribute should be in the top-level since nat was defined in the top-level
2016-04-28 16:34:37 -07:00
Leonardo de Moura
5fc90adf6b
feat(kernel): add whnf_cond to kernel type_checker
2016-04-28 16:08:03 -07:00
Leonardo de Moura
bf5e443418
feat(frontends/lean): add #compile command back
2016-04-28 15:59:38 -07:00
Leonardo de Moura
0b812bc91d
fix(kernel/declaration): typo and restoring trusted flag for constants
2016-04-28 15:59:09 -07:00
Leonardo de Moura
c14bee0bbd
feat(library/type_context): add whnf_pred helper method
2016-04-28 15:33:20 -07:00
Leonardo de Moura
7932872487
feat(kernel/declaration): untrusted constant declarations
...
This feature is useful for implementing the new tactic framework
2016-04-28 15:16:24 -07:00
Leonardo de Moura
54f68226f4
chore(frontends/lean): disable old tactic framework and blast
2016-04-25 16:22:15 -07:00
Leonardo de Moura
fdea718d9d
chore(frontends/lean): remove all #include "library/tactic.*" from frontends/lean
2016-04-25 15:41:12 -07:00
Leonardo de Moura
d88098f38d
chore(frontends/lean): remove some of the tactic support
2016-04-25 15:26:56 -07:00
Leonardo de Moura
de64750621
chore(frontends/lean): disable expressions that use tactic framework
2016-04-25 15:07:26 -07:00
Leonardo de Moura
a29eaf0067
feat(kernel): add 'trusted' flag for definitions
2016-04-11 15:49:29 -07:00
Leonardo de Moura
4728b03f20
refactor(kernel/type_checker): do not use definitional depth in the kernel type checker
2016-04-11 14:53:02 -07:00
Leonardo de Moura
d66406a1f4
feat(frontends/lean): add #elab command for testing new elaborator
2016-04-05 17:03:23 -07:00
Leonardo de Moura
03809e7973
refactor(frontends/lean): elaborator_context
2016-04-05 16:19:06 -07:00
Leonardo de Moura
2577be6344
chore(frontends/lean): remove useless elaborator options
2016-04-05 16:03:10 -07:00
Leonardo de Moura
a1bc662eca
dev(frontends/lean/parser): add local_context
2016-03-30 16:33:17 -07:00
Leonardo de Moura
e806700648
fix(frontends/lean/builtin_cmds): redeclare_aliases
2016-03-30 16:30:18 -07:00
Leonardo de Moura
06ef0ad7be
refactor(frontends/lean): add local_level_decls
...
Remark: the template local_decls will be deleted in the future.
The instances local_expr_decls will be replace by local_context.
2016-03-30 15:47:32 -07:00
Leonardo de Moura
c4f25cf15b
refactor(frontends/lean): rename elaborate methods
2016-03-30 15:05:24 -07:00
Leonardo de Moura
75549bafd7
refactor(frontends/lean/elaborator): rename elaborator to old_elaborator
2016-03-30 14:59:18 -07:00
Leonardo de Moura
59278b3911
chore(library/type_context): add trace
2016-03-27 15:37:24 -07:00
Leonardo de Moura
7ddf1ef7a7
feat(library/type_context): add on_is_def_eq_failure
2016-03-27 15:20:38 -07:00
Leonardo de Moura
c538269b47
feat(library/type_context): type class resolution
2016-03-27 14:41:18 -07:00
Leonardo de Moura
ee27480210
feat(library/type_context): initialize type class resolution
2016-03-27 13:41:07 -07:00
Leonardo de Moura
c5122223e1
feat(library/type_context): add is_class predicate
2016-03-27 10:20:32 -07:00
Leonardo de Moura
f6e3521b8e
chore(library/type_context): add trace
2016-03-27 09:58:06 -07:00
Leonardo de Moura
ca24518ab5
test(tests/lean/run/unify1.lean): new type_context is_def_eq
2016-03-25 17:14:59 -07:00
Leonardo de Moura
067f608732
feat(library/type_context): unification hints
2016-03-25 16:51:51 -07:00
Leonardo de Moura
f573ebd0a4
refactor(library): make sure prod.pr1 is a projection
2016-03-25 16:28:29 -07:00
Leonardo de Moura
3d238ee943
feat(frontends/lean/builtin_cmds): implement #unify using new type_context
2016-03-25 15:38:13 -07:00
Leonardo de Moura
7cca77c97c
dev(library/type_context): improve is_productive, add better tracing
2016-03-25 15:38:04 -07:00
Leonardo de Moura
a6b112d3b2
fix(tests/library/occurs): compilation error
2016-03-25 14:10:07 -07:00
Leonardo de Moura
02d2da38a7
dev(library/type_context): is_def_eq
2016-03-25 14:08:53 -07:00
Leonardo de Moura
bd3efca5e9
chore(library/CMakeFiles): make clear which files should be deleted after refactoring
2016-03-22 09:57:31 -07:00
Leonardo de Moura
2a38ddb124
refactor(library): merge util and occurs
2016-03-22 09:51:06 -07:00
Leonardo de Moura
f72d06c31e
refactor(library): remove resolve_macro
2016-03-21 18:04:43 -07:00
Leonardo de Moura
384e8bf7bf
refactor(library): remove unifier_plugin
2016-03-21 17:57:53 -07:00
Leonardo de Moura
c98f1bfd24
refactor(library): remove type_util module and implement get_num_args using abstract_type_context
2016-03-21 16:30:08 -07:00
Leonardo de Moura
9564758965
refactor(library/definitional/no_confusion): use new type_checker to derive no_confusion
2016-03-21 15:40:58 -07:00
Leonardo de Moura
7365c575cd
refactor(library/util): use type_checker at to_telescope
...
The to_telescope abstraction is not very useful for
abstract_type_context.
Reason: Fun/Pi (kernel) procedures are not compatible with abstract_type_context.
2016-03-21 15:34:02 -07:00
