michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
6241 commits 3 branches 0 tags 28 MiB
Commit graph

1064 commits

Author SHA1 Message Date
Leonardo de Moura
c51e2ac428 feat(kernel/type_checker): expose get_arity function 2015-01-20 14:25:07 -08:00
Leonardo de Moura
c43b2c8640 feat(kernel/extension_context): add auxiliary methods 2015-01-20 14:23:10 -08:00
Leonardo de Moura
752b54085b refactor(kernel/type_checker): type checker should not unfold macros, but sign an error if a untrusted macro is used 
Now, we unfold untrusted macros outside of the Lean kernel.
 2015-01-20 12:36:56 -08:00
Leonardo de Moura
c6290f01d0 perf(kernel/free_vars): improve has_free_var 2015-01-15 18:42:56 -08:00
Leonardo de Moura
f397da111a perf(kernel/error_msgs): avoid unnecessary work 2015-01-15 18:32:52 -08:00
Leonardo de Moura
ce0b1d17a2 perf(kernel/free_vars): improve has_free_var 2015-01-15 18:31:43 -08:00
Leonardo de Moura
907f90096e feat(kernel): add memory consumption checks at replace_fn and for_each_fn 2015-01-15 16:54:55 -08:00
Leonardo de Moura
8ab775bd6f feat(*): distinguish between logical and runtime exceptions. 
Now, we use throwable as the new base class for all Lean exceptions, and
exception is the subclass for "logical" exceptions.
 2015-01-15 16:54:55 -08:00
Leonardo de Moura
7a75325416 feat(kernel/abstract): add new abstract_local procedure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-12-20 11:31:48 -08:00
Leonardo de Moura
8b3e97d285 feat(kernel/type_checker): add ensure_type variant 2014-12-11 17:32:17 -08:00
Leonardo de Moura
bc7ee2958f fix(library/tactic/inversion_tactic): bug in mutually recursive case 2014-12-01 18:32:38 -08:00
Leonardo de Moura
4e572fac4e feat(kernel/inductive): store whether an inductive datatype supports dependent elimination or not 2014-11-27 10:36:15 -08:00
Leonardo de Moura
5fff3113a9 refactor(library/tactic/inversion_tactic): add 'cases_on' step to inversion_tactic 2014-11-27 00:06:26 -08:00
Leonardo de Moura
ffdeb0edc4 fix(frontends/lean/elaborator): unsolved metavariables, fix #329 2014-11-26 11:56:39 -08:00
Leonardo de Moura
ef75cac1c0 feat(kernel/expr): change the rules for inferring implicit arguments, closes #344 2014-11-25 12:54:07 -08:00
Leonardo de Moura
e81d9c9184 perf(kernel/level): apply two simple normalization rules at mk_max 
They are variations of:
max l1 (max l1 l2) == (max l1 l2)
 2014-11-16 18:16:57 -08:00
Leonardo de Moura
67de3b06f3 feat(kernel/level): improve universe level pretty printer 
Example: produce `l+2` instead of `succ (succ l)`.
 2014-11-14 14:51:03 -08:00
Leonardo de Moura
ffffabad95 feat(kernel/level): improve is_geq procedure for universe levels 
Now, it also returns true for

          (succ^k1 a)  =?=  k2

where k1 >= k2
 2014-11-14 14:20:35 -08:00
Leonardo de Moura
51719145f9 feat(library/unifier): solved universe constraints of the form succ^k1 a = max k2 ?m (when k1 >= k2) 2014-11-12 17:28:33 -08:00
Leonardo de Moura
50973bb4f3 feat(frontends/lean): default 'eval' command ignores opaque/irreducible annotations 
To retrieve the previous behavior, we should use [strict] modifier
 2014-11-10 12:46:04 -08:00
Leonardo de Moura
8d05238533 fix(kernel/error_msgs): ignore binder information when comparing type mismatches, fixes #304 2014-11-06 21:03:51 -08:00
Leonardo de Moura
af88e34588 fix(kernel/inductive): bug in eliminator for recursive datatypes in Prop 2014-11-06 14:03:28 -08:00
Leonardo de Moura
e499f8e20a feat(kernel/inductive): relax conditions for an inductive datatype in Prop to be able to eliminate into Type 
The new relaxed version allows us to define the "accessability"
proposition and have an eliminator into Type.

See justification in the new comments at inductive.cpp
 2014-11-06 09:36:54 -08:00
Leonardo de Moura
84b516994c fix(library/tactic): type check generalization result, fixes #273 2014-10-29 20:34:01 -07:00
Leonardo de Moura
777aa63660 fix(kernel/inductive): relax eliminator generation rules for empty types 
This commit also removes the workaround false.rec_type. It is not needed anymore
 2014-10-28 10:31:00 -07:00
Leonardo de Moura
7516fcad97 feat(kernel/type_checker): add is_stuck method, and improve ensure_pi method, closes #261 2014-10-27 13:16:50 -07:00
Leonardo de Moura
7240a1a640 feat(kernel/inductive): add get_num_minor_premises and get_num_type_formers APIs 2014-10-25 11:17:29 -07:00
Leonardo de Moura
2bc034da2c feat(kernel/inductive): expose 'get_elim_name' API 2014-10-25 10:47:12 -07:00
Leonardo de Moura
9e69a95b26 feat(kernel/inductive): add API for retrieving the number of indices in an inductive datatype 2014-10-25 10:42:05 -07:00
Leonardo de Moura
c30c0fa3b8 fix(kernel/metavar): avoid crash due to stack overflow, closes #253 2014-10-25 00:20:59 -07:00
Leonardo de Moura
40235c6af0 fix(kernel/type_checker): propagate 'memoize' flag to default_converter 2014-10-23 13:15:53 -07:00
Leonardo de Moura
33f18b9454 fix(kernel/converter): remove buggy eta-reduction and rely only on eta-expansion 
The bug is exposed by new unit test
 2014-10-21 16:54:25 -07:00
Leonardo de Moura
6a31a79265 refactor(frontends/lean/inductive_cmd): move auxiliary method to expr.h 2014-10-18 15:11:26 -07:00
Leonardo de Moura
2369388629 refactor(kernel/instantiate): cleanup beta-reduce 2014-10-17 20:19:51 -07:00
Leonardo de Moura
1ce3b83d79 fix(kernel/metavar): compilation error in some compilers 2014-10-17 17:22:25 -07:00
Leonardo de Moura
58aff5b4af perf(kernel/metavar): used thread local cache for instantiate_metavars 2014-10-17 17:08:35 -07:00
Leonardo de Moura
6d64da2981 perf(kernel/expr_eq_fn): use thread local cache, and avoid memory allocation/deallocation 2014-10-17 16:44:20 -07:00
Leonardo de Moura
7cc3dd0b4d chore(kernel/replace_fn): "name" constant 2014-10-17 14:20:35 -07:00
Leonardo de Moura
b6afbcb7f5 perf(kernel/replace_fn): use 'recursive' replace_fn for "small" terms 2014-10-17 14:15:09 -07:00
Leonardo de Moura
10b880ce3b perf(kernel/metavar): improve occurs_expr and occurs performance 2014-10-17 14:05:22 -07:00
Leonardo de Moura
d2cbd25985 refactor(kernel): replace_visitor doesn't need to be in the kernel anymore 2014-10-17 10:23:35 -07:00
Leonardo de Moura
14ebbda8cb perf(kernel/metavar): minor improvement 2014-10-16 21:43:54 -07:00
Leonardo de Moura
fe484b26f3 refactor(kernel/expr): remove dead code 2014-10-16 13:45:36 -07:00
Leonardo de Moura
3b6b23c921 refactor(kernel/expr): remove silly overloads 2014-10-16 13:37:55 -07:00
Leonardo de Moura
c4f02bd16a refactor(kernel/expr): remove dead code 2014-10-16 13:09:26 -07:00
Leonardo de Moura
97a7dae12a refactor(kernel/expr): remove code duplication 2014-10-16 12:48:49 -07:00
Leonardo de Moura
814778abb1 refactor(kernel/expr): tag expressions at "creation" time 2014-10-15 13:12:09 -07:00
Leonardo de Moura
de7c850782 feat(kernel/converter): relax is_def_eq test for local constants and meta-variables 2014-10-14 15:31:57 -07:00
Leonardo de Moura
940092a975 fix(kernel/constraint): bug in operator<< 2014-10-14 15:22:03 -07:00
Leonardo de Moura
a26618e0f2 feat(frontends/lean): add '[]' notation for marking arguments where class-instance resolution should be applied 2014-10-12 13:06:00 -07:00
Leonardo de Moura
235b8975d2 feat(kernel/inductive): K-like reduction in the kernel 
Given (H_1 : a = a), we have that
      eq.rec H_2 H_1
reduces to H_2

This is not exclusive to equality.
It applies to any inductive datatype in Prop, containing only one
constructor with zero "arguments" (we say they are nullary).

BTW, the restriction to only one constructor is not needed, but it is
does not buy much to support multiple nullary constructors since Prop is
proof irrelevant.
 2014-10-10 14:37:45 -07:00
Leonardo de Moura
5a71542aeb feat(kernel/inductive): track when K-like reduction can be used 2014-10-10 08:50:24 -07:00
Leonardo de Moura
93e0599a0f feat(kernel/level): add missing normalization rule 2014-10-08 22:23:19 -07:00
Leonardo de Moura
92c424936a refactor(kernel/macro_definition_cell): improve macro get_type API 2014-10-07 16:38:31 -07:00
Leonardo de Moura
bf081ed431 refactor(kernel): rename var_decl to constant_assumption 
Motivation: it matches the notation used to declare it.
 2014-10-02 17:55:34 -07:00
Leonardo de Moura
98e66586e9 feat(frontends/lean/elaborator): elaborator rejects 'Type' if the universe is explicit 2014-10-02 14:29:51 -07:00
Leonardo de Moura
c46ec6a548 fix(frontends/lean): missing type information for INFO, fixes #218 2014-10-01 14:29:07 -07:00
Leonardo de Moura
966366e18e feat(kernel/inductive): relaxed rules for defining datatypes with explicit universes, closes #217 2014-10-01 10:56:05 -07:00
Leonardo de Moura
a0c37b231f feat(kernel/expr): add hash_bi function that takes binder information into account 2014-09-29 16:44:55 -07:00
Leonardo de Moura
9f6a8827e0 refactor(*): use name_map 2014-09-28 10:23:11 -07:00
Leonardo de Moura
22e47430b5 feat(library/unifier): add 'on-demand' choice constraints, they are processed as soon as their type does not contain meta-variables anymore 2014-09-27 21:50:39 -07:00
Leonardo de Moura
8e7aac1eb4 fix(frontends/lean): add 'eval' command 2014-09-26 20:16:03 -07:00
Leonardo de Moura
03f71c73dc perf(kernel/instantiate): cache result of instantiate_type_univ_params 
and instantiate_value_univ_params
 2014-09-25 13:24:43 -07:00
Leonardo de Moura
28796593e3 fix(kernel/type_checker): bug in new is_opaque method 2014-09-25 12:24:14 -07:00
Leonardo de Moura
1d92097781 refactor(kernel/declaration): return reference to type/value/name 2014-09-25 12:17:04 -07:00
Leonardo de Moura
d4236e40b4 feat(kernel/type_checker): expose is_opaque 2014-09-25 11:19:54 -07:00
Leonardo de Moura
516c0c73b9 refactor(*): remove dependency to thread_local C++11 keyword, the 
current compilers have several bugs associated with it

We use the simpler __thread (gcc and clang) and
__declspec(thread) (visual studio).
 2014-09-24 12:51:04 -07:00
Leonardo de Moura
ca1b8ca80f refactor(util/memory_pool): simplify memory_pool, it is not a template anymore 2014-09-24 10:48:32 -07:00
Leonardo de Moura
9b61b18eaa perf(kernel/replace_visitor): use more expensive/precise cache 
It does not use pointer equality, but structural equality
 2014-09-24 10:12:29 -07:00
Leonardo de Moura
358074ae3d refactor(kernel/record): remove kernel extension for records, we will 
implement it outside of the kernel on top of the inductive datatypes
 2014-09-24 10:12:28 -07:00
Leonardo de Moura
da481c3274 refactor(kernel): explicit initialization/finalization 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-24 10:12:28 -07:00
Leonardo de Moura
531046626a refactor(*): explicit initialization/finalization for environment extensions 2014-09-22 17:30:29 -07:00
Leonardo de Moura
b6781711b1 refactor(*): explicit initialization/finalization for serialization 
modules, expression annotations, and tactics
 2014-09-22 15:26:41 -07:00
Leonardo de Moura
49d5af473d refactor(kernel): remove support for proof irrelevant classes 
Motivation: we can use Prop
 2014-09-19 07:32:07 -07:00
Leonardo de Moura
243f80231a chore(kernel): fix style and lua bindings 2014-09-17 18:30:28 -07:00
Leonardo de Moura
ea1bae0143 refactor(kernel/converter): replace extra_opaque_set with predicate 
It gives us more flexibility.
 2014-09-17 17:05:13 -07:00
Leonardo de Moura
80fd14b39e refactor(frontends/lean): replace collect_metavars with metavar_closure helper class 2014-09-11 14:49:35 -07:00
Leonardo de Moura
4a4de27a6c refactor(frontends/lean/elaborator): move local_context to separate file 2014-09-10 11:20:16 -07:00
Leonardo de Moura
38058450d4 fix(frontends/lean/elaborator): whnf may produce assertion violation if term contains free variables 2014-09-09 16:09:05 -07:00
Leonardo de Moura
3310eb3dfc feat(frontends/lean): remove restriction on implict arguments, add new test that demonstrates the new feature 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-07 12:29:32 -07:00
Leonardo de Moura
8743394627 refactor(kernel/inductive): replace recursor name, use '.rec' instead of '_rec' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-04 15:04:57 -07:00
Leonardo de Moura
79acd3e1b7 fix(kernel/converter): missing case 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-28 15:21:57 -07:00
Leonardo de Moura
44c597724b fix(frontends/lean): fail if theorem type has metavariables after type elaboration (and before proof elaboration) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-26 09:01:17 -07:00
Leonardo de Moura
04d9eb17d1 feat(kernel/conveter): improve support for proof irrelevant in the converter 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-25 11:19:18 -07:00
Leonardo de Moura
fbf13994d8 refactor(*): use + for concatenating format objects 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-24 09:35:25 -07:00
Leonardo de Moura
d4ac482d76 refactor(kernel): move annotation to library 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-22 10:38:10 -07:00
Leonardo de Moura
7d987df429 refactor(kernel/formatter): move simple_formatter to library 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-22 10:26:45 -07:00
Leonardo de Moura
937c465685 fix(library/unifier): too much reduction 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-21 21:37:51 -07:00
Leonardo de Moura
359c72b02f fix(frontends/lean/pp): bug when pretty printing binder information, fixes #73 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-21 09:28:07 -07:00
Leonardo de Moura
9588336c15 refactor(kernel/type_checker): remove "global" constraint buffer from type_checker, and use constraint_seq instead 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-20 16:46:19 -07:00
Leonardo de Moura
4cf3d32e0c chore(*): create alias for std::pair 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-20 16:46:19 -07:00
Leonardo de Moura
dc1613f535 feat(frontends/lean): annotate 'notation' subterms with 'noinfo' annotation (goal: improve typeinfo generation); fix initialization problem (with annotations) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-15 15:07:14 -07:00
Leonardo de Moura
562926e7ad refactor(kernel/instantiate): add functions instantiate_value_univ_params and instantiate_type_univ_params 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-12 17:40:30 -07:00
Leonardo de Moura
8ad0949269 fix(kernel/environment): initialization problem on OSX 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-09 16:14:35 -07:00
Leonardo de Moura
4bcde576b8 perf(kernel/abstract): improve mk_binding performance 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-09 14:14:14 -07:00
Leonardo de Moura
4986226e41 fix(kernel/converter): missing delay_check case 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-09 08:07:41 -07:00
Leonardo de Moura
24e8dca014 feat(library/explicit): allow 'as-is', 'explicit' and 'implicit' annotations to be saved in .olean files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-07 19:13:48 -07:00
Leonardo de Moura
2486c483cf chore(kernel/error_msgs): change type mismatch error messages, closes #33 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-07 16:18:40 -07:00
Leonardo de Moura
9e6c5695be fix(library/unifier): make sure the imitation step is type correct, fix ensure_sufficient_args 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-07 16:09:45 -07:00
Leonardo de Moura
e6ffda0c51 feat(library/match): add basic match_plugin that just invokes whnf before failing 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-05 08:37:03 -07:00