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

757 commits

Author SHA1 Message Date
Leonardo de Moura
33bbcd9526 chore(kernel/declaration): rename declaration::get_params to declaration::get_univ_params 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-02 16:20:34 -07:00
Leonardo de Moura
82e1f87e08 feat(kernel): add function param_names_to_levels 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-02 16:17:04 -07:00
Leonardo de Moura
96f639811c chore(kernel/level): remove unnecessary code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-02 15:42:37 -07:00
Leonardo de Moura
e9664cb042 fix(kernel/type_checker): check if the declaration contains duplicate universe level parameters 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-02 13:57:43 -07:00
Leonardo de Moura
585f3adde1 feat(library/scope): add sections 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-01 17:55:11 -07:00
Leonardo de Moura
1b5366cfb7 feat(library): add module for implementing aliases and 'using' command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-30 21:42:40 -07:00
Leonardo de Moura
e206fcc1af perf(kernel/type_checker): reduce the overhead of creating delayed_justification objects, a huge number of them is created when type checking applications 
We reduce the cost by avoiding the allocation of std::functional objects, and the unnecessary increment/decrement of reference counters.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-27 23:16:52 -07:00
Leonardo de Moura
1b4c9f63ce perf(kernel/environment): improve is_descendant performance, optimize for the common case: the is_descendant tree is huge but has few deep branches 
This is an important optimization for module.cpp. The benchmark tests/lua/slow/mod2.lua is a good example where the cost of is_descendant was neutralizing the benefit of the replace method.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-27 22:29:03 -07:00
Leonardo de Moura
eca906b074 feat(library/module): add inductive decls to .olean files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-26 15:38:09 -07:00
Leonardo de Moura
f050308df7 feat(kernel/instantiate): relax apply_beta pre-conditions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-25 07:45:41 -07:00
Leonardo de Moura
2be9bcef78 feat(library/coercion): add coercion management implementation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-24 19:28:42 -07:00
Leonardo de Moura
49b2bb209d refactor(kernel/formatter): formatter_cell object should not perform destructive updates 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-24 13:51:39 -07:00
Leonardo de Moura
2344fb9476 feat(kernel/expr): use the expression depth in the hash code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-23 14:16:51 -07:00
Leonardo de Moura
b68b9ccc05 fix(kernel/environment): bug in extension id checking 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-23 11:24:00 -07:00
Leonardo de Moura
6246fae32c fix(kernel/inductive): inductive datatype declaration validation bug pointed out by Cody Roux 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-21 16:29:25 -07:00
Leonardo de Moura
a45dc0bb86 chore(kernel): remove dead code, we don't have level constraints anymore 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-21 15:46:17 -07:00
Leonardo de Moura
45d473d44e feat(kernel): add mk_hott_environment function for creating HoTT compatible environments 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-21 11:31:34 -07:00
Leonardo de Moura
9b9041fa2e feat(kernel/environment): add method for adding declarations that were not type checked (if trust_lvl() > LEAN_BELIEVER_TRUST_LEVEL) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-21 11:12:26 -07:00
Leonardo de Moura
8872d4a531 refactor(kernel): rename definition class to declaration 
The name was misleading since not every declaration is a definition.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-20 10:41:38 -07:00
Leonardo de Moura
34a9c8304a feat(kernel/environment): add for_each method for traversing environment declarations 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-20 10:15:28 -07:00
Leonardo de Moura
9de8249d8f feat(kernel): let Pi/Fun also take local constants 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-19 17:03:48 -07:00
Leonardo de Moura
df9c935f0a fix(kernel/inductive): remove unused argument, bug in is_rec_argument (free variable occurrence) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-19 17:02:20 -07:00
Leonardo de Moura
3e3d3c8380 feat(kernel/inductive): check in add_inductive whether the environment supports inductive datatypes or not 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-19 15:44:15 -07:00
Leonardo de Moura
a1086e440d feat(kernel/inductive): use non-dependent elimination for Bool/Prop only if it is proof irrelevant 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-19 13:33:29 -07:00
Leonardo de Moura
eb92f3722f fix(kernel/inductive): typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-19 13:27:05 -07:00
Leonardo de Moura
f3ed20a229 feat(kernel/inductive): add normalizer extension for inductive datatypes, add procedure for creating an standard (empty) Lean environment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-19 12:52:25 -07:00
Leonardo de Moura
edc8af7bb3 refactor(kernel): reduce code duplication 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-19 11:11:19 -07:00
Leonardo de Moura
0e582675d9 feat(kernel/inductive): store computational rules in an environment extension 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-19 10:45:52 -07:00
Leonardo de Moura
90d83fa2ad fix(kernel/environment): bug in get_extension 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-19 10:41:22 -07:00
Leonardo de Moura
1a9122f158 doc(kernel/inductive): improve module documentation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-19 10:04:28 -07:00
Leonardo de Moura
2aacb769dd feat(kernel/inductive): generate computational rules RHS for inductive datatypes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-19 09:08:19 -07:00
Leonardo de Moura
eb409a9ce3 feat(kernel/abstract): add more Fun functions for simplifying the creation lambda-expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-19 09:01:20 -07:00
Leonardo de Moura
2daad71d47 fix(kernel/type_checker): memory access violation, closures (for printing error messages) had a uninteded reference to the type_checker 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-19 08:59:32 -07:00
Leonardo de Moura
39e101d323 feat(kernel/formatter): improve simple printer support for Pi and lambda 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-19 08:16:32 -07:00
Leonardo de Moura
28b70b4e04 feat(kernel/inductive): use nondependent elimination when the datatype is in Bool/Prop 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-18 15:39:48 -07:00
Leonardo de Moura
45252e2229 feat(kernel/inductive): add eliminator/recursor for inductive datatype declarations 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-18 14:17:57 -07:00
Leonardo de Moura
f826e98196 feat(kernel/formatter): avoid hierarchical names when printing local constants 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-18 13:50:29 -07:00
Leonardo de Moura
7bf0011905 feat(kernel/expr): add additional template for mk_app 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-18 13:15:58 -07:00
Leonardo de Moura
08aa4afb3e feat(kernel/abstract): add more Pi functions for simplifying the creation Pi-expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-18 13:15:00 -07:00
Leonardo de Moura
950d69b977 test(lua): add tests for exercising datatype validation code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 20:10:45 -07:00
Leonardo de Moura
ff3a7bd734 fix(kernel/type_checker): style 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 19:21:09 -07:00
Leonardo de Moura
8fcb84c8f2 feat(kernel/inductive): finish inductive datatype declaration validation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 19:19:32 -07:00
Leonardo de Moura
5c7d3c79c4 feat(kernel/expr): improve get_app_args interface 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 19:19:10 -07:00
Leonardo de Moura
28e8299f6d feat(kernel/type_checker): add swap method 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 19:18:46 -07:00
Leonardo de Moura
f818c1a63e feat(kernel/inductive): add more inductive datatype validation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 14:47:06 -07:00
Leonardo de Moura
d03e35aaac feat(kernel/inductive): add datatype and introduction rules declarations to environment, and fix tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 13:59:06 -07:00
Leonardo de Moura
18a17cd48b feat(kernel/level): add is_geq predicate, we need it for implementing the inductive datatype validation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 13:39:54 -07:00
Leonardo de Moura
4348d5e63f refactor(kernel): remove unnecessary module 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 12:35:41 -07:00
Leonardo de Moura
a85a6b685b feat(kernel/formatter): add binding_body_fresh, let_body_fresh, and simplify formatter 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 12:30:03 -07:00
Leonardo de Moura
5ce134e24e chore(kernel): binder => binding where appropriate 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 11:37:27 -07:00