Leonardo de Moura
67088b130e
refactor(kernel/constraint): simplify constraint interface, and add choice constraint
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-21 12:25:54 -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
5c17411a86
fix(kernel/converter): relax is_def_eq test, for example is_def_eq(f(?m1), a) should generate a constraint instead of returning an error
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-20 09:46:58 -07:00
Leonardo de Moura
2954d10df5
refactor(kernel/converter): remove unnecessary exception
...
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
0779db7ae9
fix(kernel): set module_idx on theorems, otherwise we are not able to import theorems that use opaque definitions
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-16 16:56:11 -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
21c54755a9
fix(kernel/converter): bug in is_def_eq
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-16 14:09:12 -07:00
Leonardo de Moura
2312f43443
fix(kernel/abstract): propagate tags when abstracting
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-16 13:00:13 -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
961b0bfacf
feat(kernel/type_checker): use argument position when reporting application type mismatch errors
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-15 10:06:53 -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
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
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
1a67cc7293
fix(kernel/for_each_fn): typo
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-11 15:06:11 -07:00
Leonardo de Moura
fe6ab51c12
feat(kernel/inductive): add APIs for retrieving information about declared inductive datatypes, intro rules, and elimination rules
...
The new API is important for implementing environment transformation procedures, and export Lean environment to different systems (e.g., Coq).
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-08 17:15:21 -07:00
Leonardo de Moura
1c49b4d85f
chore(*): replace unique_lock with lock_guard when we do not need to use conditional variables
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-07 20:55:25 -07:00
Leonardo de Moura
15f0899efb
refactor(*): replace LEAN_THREAD_LOCAL with MK_THREAD_LOCAL_GET, the new macro uses the Boost thread_local_ptr instead of 'thread_local' directive
...
Motivation: clang++ on OSX does not support 'thread_local'.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-07 10:18:36 -07:00
Leonardo de Moura
91df9a5550
feat(util/thread): add LEAN_THREAD_PTR macro, it uses boost::thread_specific_ptr instead of thread_local keyword when we compile with Boost
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-07 08:16:20 -07:00
Leonardo de Moura
89a7898054
fix(*): static variable initialization problems
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-06 18:44:12 -07:00
Leonardo de Moura
4a43016735
fix(kernel/expr): expr_cache initialization
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-06 18:00:26 -07:00
Leonardo de Moura
bab430af43
chore(kernel/expr): cleanup
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-04 14:51:36 -07:00
Leonardo de Moura
3354832c21
perf(kernel/expr_eq_fn): delay cache allocation
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-03 17:03:09 -07:00
Leonardo de Moura
4a25e7442a
feat(kernel/expr): add optional expression caching (aka "partial" hash-consing)
...
We do not enforce full hash-consing because we would need to synchronize
the access to the hashtable/cache.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-03 15:35:47 -07:00
Leonardo de Moura
02df63b85e
fix(kernel/level): add workaround for clang++ bug: memory leak at thread_local
...
The fix has an advantage. There is only one copy of level Zero in the system even when multiple threads are used.
Moreover, it does no require any form of synchronization, and modules can be initialized in any order.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-03 10:37:50 -07:00
Leonardo de Moura
ab5f570924
refactor(kernel/constraint): remove choice constraints from the kernel, the kernel does not use them, we will implement them in elaborator
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-03 00:46:28 -07:00
Leonardo de Moura
536b7539c6
chore(kernel/inductive): cleanup code
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-03 00:38:45 -07:00
Leonardo de Moura
f816487f4b
fix(kernel/level): add (trivial) case for is_geq predicate: l >= 0 for any l
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-02 18:13:50 -07:00
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
Leonardo de Moura
33ae79cd9e
refactor(kernel): move shallow copy function to library
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-17 11:20:24 -07:00
Leonardo de Moura
d625c9a26c
refactor(kernel): move max_sharing to library
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-17 11:15:08 -07:00
Leonardo de Moura
aafdd98acb
refactor(kernel): remove telescope type, and procedures
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-17 10:51:40 -07:00
Leonardo de Moura
36b070cb5b
refactor(kernel/inductive): simplify inductive datatype API
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-17 09:24:34 -07:00
Leonardo de Moura
5fc0f06a8d
feat(library/kernel_bindings): add Lua API for declaring datatypes
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-16 18:08:50 -07:00
Leonardo de Moura
ace5dee63d
feat(kernel/inductive): add getters for inductive decls
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-16 17:47:37 -07:00
Leonardo de Moura
6dedb480ec
fix(kernel/abstract): bug in abstract for telescopes
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-16 17:47:04 -07:00
Leonardo de Moura
e6c52d17a6
fix(kernel/expr): memory leak introduced today
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-16 16:21:31 -07:00
Leonardo de Moura
7d76278506
fix(kernel/abstract): compilation warnining
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-16 15:39:19 -07:00
Leonardo de Moura
a0abbf7662
feat(kernel/formatter): make simple_formatter display Type instead of Bool if impredicativity is disabled
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-16 15:31:19 -07:00
Leonardo de Moura
69e72c278d
feat(kernel): add proof irrelevance for classes
...
We can use this feature to implement proof irrelevance for Identity types.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-16 15:30:32 -07:00
Leonardo de Moura
193aa4a83f
feat(library/kernel_bindings): improve Pi and Fun Lua APIs, and allow users to provide binder information
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-16 14:09:00 -07:00
Leonardo de Moura
862c5e354d
feat(kernel/expr): attach auxiliary name (for pretty printing) into local constants
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-16 13:08:09 -07:00
Leonardo de Moura
91a1b62b9e
feat(kernel): add telescope abstract procedure
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-16 11:56:44 -07:00
Leonardo de Moura
9a689ab0c3
feat(kernel): add telescope instantiate procedure
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-16 11:56:20 -07:00
Leonardo de Moura
40b3129e7b
refactor(kernel): improve names
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-16 11:28:05 -07:00
Leonardo de Moura
d6d72ba80e
refactor(kernel): add binder structure
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-16 10:51:54 -07:00
Leonardo de Moura
eb0abf557d
feat(kernel/inductive): add inductive datatype kernel extension module interface
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-16 09:53:51 -07:00
Leonardo de Moura
660b9299ad
refactor(kernel): (de)serialization procedures don't need to be in the kernel
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-15 17:23:36 -07:00
Leonardo de Moura
16553e77fa
fix(kernel/type_checker): avoid assertion violation due to API misuse
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-15 14:17:34 -07:00
Leonardo de Moura
7c0cc3111a
fix(kernel/type_checker): we must use different caches for infer_type and check
...
The new test tc4.lua exposes the problem being fixed.
We need separate caches otherwise we may mistakenly assume that an expression was already checked by the type checker, while only its type was inferred.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-15 13:53:11 -07:00
Leonardo de Moura
687639a599
fix[kernel/justification.cpp]: style
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-15 13:53:11 -07:00
Leonardo de Moura
494874fbab
fix(kernel/type_checker): trust level test
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-15 13:53:10 -07:00
Leonardo de Moura
830537a58b
feat(kernel/justification): add function for creating simple justification objects
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-15 13:53:10 -07:00
Leonardo de Moura
d58b8a8102
refactor(kernel): move delayed_justification to justification.h
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-15 13:53:10 -07:00
Leonardo de Moura
84c1cf9600
feat(kernel/kernel_exception): add new auxiliary functions for throwing kernel exceptions
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-15 13:53:10 -07:00
Leonardo de Moura
3a19d9fee1
refactor(kernel): revise macro_definition API
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-15 13:53:10 -07:00
Leonardo de Moura
6d30141a31
fix(kernel/formatter): remove unnecessary parenthesis
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-15 13:53:10 -07:00
Leonardo de Moura
08ac9c1f05
feat(kernel): add is_def_eq predicate in the extension_context API
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-15 13:53:10 -07:00
Leonardo de Moura
a6dc6060e2
fix(kernel/formatter): typo
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-15 13:53:10 -07:00
Leonardo de Moura
606e6226c2
fix(kernel/type_checker): the type checker cache was not taking into account binder information
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-14 17:14:57 -07:00
Leonardo de Moura
d5184a1751
feat(kernel/formatter): print binder_info in simple formater
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-14 16:51:49 -07:00
Leonardo de Moura
5d61d23bf6
refactor(kernel): move mk_tele_pi to expr.h, and rename it mk_pi
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-14 16:24:55 -07:00
Leonardo de Moura
9c5dfc387b
refactor(kernel/replace_visitor): remove context from replace_visitor
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-14 15:53:09 -07:00
Leonardo de Moura
2e1a0bd50c
feat(kernel/expr): add is_contextual binder info
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-14 14:54:27 -07:00
Leonardo de Moura
893e4d4ae2
fix(kernel/expr): bug in m_free_var_range let-expr field
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-14 14:28:47 -07:00
Leonardo de Moura
cf55a1bcc2
fix(kernel/type_checker): typo
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-14 10:35:42 -07:00
Leonardo de Moura
277e0e6d49
feat(kernel/formatter): prefix metavars with '?' and local vars with '!' in the simple formatter
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-14 10:16:54 -07:00
Leonardo de Moura
9ed700a5a6
feat(kernel/environment): add forget method
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-13 08:40:46 -07:00
Leonardo de Moura
7b15e558a2
refactor(kernel/converter): implement eta in whnf instead of is_def_eq.
...
Without cumulativity, we do not have problems with Eta at whnf anymore.
When we had cumulativity, we could not not simply reduce
(fun x : A, f x) ==> f
This step is correct only if domain(f) was definitionally equal to f.
Here is a problematic example for systems with cumulativity
Given, f : Type.{2} -> Bool
(fun x : Type.{1}, f x)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-12 17:49:53 -07:00
Leonardo de Moura
3bc83fae56
refactor(kernel/type_checker): remove trace capability, we get it for free with tags
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-12 16:38:53 -07:00
Leonardo de Moura
2593f65ce1
feat(kernel): add tag to kernel expressions
...
Frontends can used tags to associate expressions with line number information.
The update_* procedures automatically propagate tags.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-12 16:33:25 -07:00
Leonardo de Moura
2e753e2cc0
fix(kernel/error_msgs): application type mismatch error message
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-12 14:49:42 -07:00
Leonardo de Moura
b18263a014
feat(kernel/formatter): adjust simple formatter to the new convention for displaying universe levels
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-12 14:42:01 -07:00
Leonardo de Moura
d4922daedf
fix(kernel/level): add missing LEAN_THREAD_LOCAL directive
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-12 14:39:37 -07:00
Leonardo de Moura
a8a6bb1b7f
fix(kernel/level): bug in get_undef_global
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-12 14:34:24 -07:00
Leonardo de Moura
89d6a1e691
fix(kernel/type_checker): check for undefined global/local levels
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-12 14:23:04 -07:00
Leonardo de Moura
b6d6df161f
fix(kernel/level): bug in get_undef_param
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-12 14:22:23 -07:00
Leonardo de Moura
1244a951f2
fix(kernel/type_checker): add missing test: number of universe level parameters
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-12 12:57:27 -07:00
Leonardo de Moura
ff9004dae2
refactor(kernel): add level normalizer, is_equivalent predicate, switch to is_equivalent in the type checker, fix bugs in is_lt predicate
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-11 18:05:02 -07:00
Leonardo de Moura
7176181b42
refactor(kernel/converter): cleanup and remove universe cumulativity support
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-09 20:43:11 -07:00
Leonardo de Moura
e942aecca6
refactor(kernel/type_checker): remove method is_conv
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-09 20:29:35 -07:00
Leonardo de Moura
9d96f24766
refactor(kernel): remove convertability constraints
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-09 20:25:27 -07:00
Leonardo de Moura
d4400d6135
refactor(library/kernel_bindings): remove level_cnstrs
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-09 20:16:51 -07:00
Leonardo de Moura
7b6d555433
refactor(kernel): remove level constraints from definitions
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-09 20:11:50 -07:00
Leonardo de Moura
23ed003389
refactor(kernel): remove diff_cnstrs module
...
We don't need them anymore. We will drop universe cumulativity from the kernel.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-09 19:58:25 -07:00
Leonardo de Moura
6493ff5388
fix(kernel/formatter): print level parameters
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-09 19:50:04 -07:00
Leonardo de Moura
fca65a9d69
fix(kernel/environment): is_descendant optimization
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-08 18:48:25 -07:00
Leonardo de Moura
c843243f64
feat(library/kernel_bindings): add add_decl and type_check functions to Lua API
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-08 18:08:32 -07:00
Leonardo de Moura
f3c7bc948a
feat(library/kernel_bindings): type_checker Lua API
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-07 19:04:15 -07:00
Leonardo de Moura
db39458c30
fix(kernel/level): predicate is_param_core
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-07 16:22:08 -07:00
Leonardo de Moura
9c760132e2
feat(kernel): add global levels to environment
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-07 16:07:31 -07:00
Leonardo de Moura
2424cf7ece
fix(kernel/expr): old comment
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-07 13:07:17 -07:00
Leonardo de Moura
503d8dfa9e
feat(kernel): add global universe level
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-06 16:13:29 -07:00
Leonardo de Moura
850ec69538
feat(kernel): add flag for disabling impredicativity of Prop/Bool in the kernel
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-05 14:09:17 -07:00
Leonardo de Moura
b83410f042
fix(library/kernel_bindings): g++ compilation error
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-02 14:34:56 -07:00
Leonardo de Moura
802edd77d1
feat(kernel/justification): add is_eqp predicate
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-02 12:15:29 -07:00
Leonardo de Moura
e4f69bd780
fix(kernel/justification): bug in depends_on
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-02 12:15:01 -07:00
Leonardo de Moura
50089dc64e
feat(kernel/error_msgs): expose pp_indent_expr
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-02 12:03:12 -07:00
Leonardo de Moura
65486b2dec
refactor(kernel/expr): add macro_definition smart pointer
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-01 18:05:46 -07:00
Leonardo de Moura
0bc101ac28
fix(kernel/metavar): typo
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-01 15:28:34 -07:00
Leonardo de Moura
ddd980aa63
fix(kernel/level): warning messages when compiling in release mode
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-01 13:06:00 -07:00
Leonardo de Moura
027614cebb
fix(kernel/metavar): wierd memory leak that only happens when compiling with clang++
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-01 12:55:55 -07:00
Leonardo de Moura
6fb7039746
refactor(kernel): use structural hashing in type_checker and converter
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-01 10:41:53 -07:00
Leonardo de Moura
a5ae4b6570
feat(kernel): add binder annotations (implicit, cast)
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-01 10:35:02 -07:00
Leonardo de Moura
b0e0e82350
refactor(kernel): separate type_checker and converter
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-30 18:42:01 -07:00
Leonardo de Moura
3e222e2f22
refactor(kernel/formatter): add environment as an extra argument to the formatter
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-30 10:28:07 -07:00
Leonardo de Moura
93a61748e9
fix(kernel/level): bug in optional<level>() constructor
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-29 17:00:57 -07:00
Leonardo de Moura
49e626a0e0
refactor(kernel/metavar): switch to functional substitution datastructure
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-29 10:22:36 -07:00
Leonardo de Moura
cdae3ee780
fix(kernel/type_checker): style
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-28 14:17:34 -07:00
Leonardo de Moura
b70bac0e8d
feat(kernel/type_checker): add backtracking trick to minimize the number of delta-reduction steps
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-28 14:03:46 -07:00
Leonardo de Moura
e62254fbb3
fix(kernel/expr): relax macro_definition interface
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-28 14:02:48 -07:00
Leonardo de Moura
1b9e2efb0c
fix(kernel/environment): relax normalizer_extesion interface
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-28 14:01:44 -07:00
Leonardo de Moura
f320277248
feat(kernel/definition): add mk_definition procedure that automatically computes the weight
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-28 12:48:21 -07:00
Leonardo de Moura
6c3a796119
fix(kernel/type_checker): bug in whnf method, and missing call to max_sharing in is_conv and is_def_eq methods
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-28 12:09:23 -07:00
Leonardo de Moura
4e893d3902
fix(kernel/constraint): printer
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-28 12:02:59 -07:00
Leonardo de Moura
54936c201a
fix(kernel/kernel_exception): typo
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-28 11:31:39 -07:00
Leonardo de Moura
6dfeff92f8
fix(kernel/constraint): add dealloc method
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-28 11:13:51 -07:00
Leonardo de Moura
e3b79730ba
fix(kernel/level): initialization error
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-28 11:03:23 -07:00
Leonardo de Moura
2ddadfc920
fix(kernel/environment): compilation errors
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-28 10:58:14 -07:00
Leonardo de Moura
9f57ec059a
fix(kernel/constraint): missing inline directive
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-28 10:53:53 -07:00
Leonardo de Moura
272463bd66
feat(kernel/type_checker): add check function
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-28 10:47:50 -07:00
Leonardo de Moura
e769c26800
refactor(kernel): move files that don't need to be in the kernel
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-25 18:30:40 -07:00
Leonardo de Moura
b2518f873d
feat(kernel/type_checker): handle ensure_pi when whnf is a meta application
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-25 18:17:32 -07:00
Leonardo de Moura
6b05146eca
fix(kernel/type_checker): preserve bound variable name when inferring type of a lambda expression
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-25 17:29:47 -07:00
Leonardo de Moura
63b6564b78
refactor(kernel): define extension_context API for normalizer_extesions and macro_definitions
...
A particular macro definition may use the extra information to retrieve information necessary to expand/type a given macro application. Example: it may need to invoke whnf.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-25 15:43:17 -07:00
Leonardo de Moura
4842ae4fc7
refactor(kernel): store macro arguments in the macro_expr
...
Before this commit, we "stored" macro arguments using applications.
This representation had some issues. Suppose we use [m a] to denote a macro
application. In the old representation, ([m a] b) and [m a b] would have
the same representation. Another problem is that some procedures (e.g., type inference)
would not have a clean implementation.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-25 15:02:56 -07:00
Leonardo de Moura
9d5ed2bae1
chore(kernel/type_checker): fix style
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-25 12:04:14 -07:00
Leonardo de Moura
a39a5b4195
refactor(kernel): remove normalizer
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-25 12:02:33 -07:00
Leonardo de Moura
a55c3c617d
feat(kernel/type_checker): add infer_type
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-25 11:58:29 -07:00
Leonardo de Moura
3e122ed355
feat(kernel/error_msgs): add error message for unsatisfied level constraints, remove messages for dependent pairs
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-25 10:47:05 -07:00
Leonardo de Moura
508bccb0c5
fix(kernel/max_sharing): add example exposing bug in max_sharing_fn, and fix it
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-24 15:55:48 -07:00
Leonardo de Moura
1c8e78e3ae
fix(kernel/justification): typo
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-24 15:08:10 -07:00
Leonardo de Moura
4be4f21de6
fix(kernel/type_checker): bug in quick_is_conv, it was not converting free variables to local constants.
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-24 12:46:31 -07:00
Leonardo de Moura
0d7902f9eb
feat(kernel/type_checker): finish is_convertible predicate
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-23 20:16:14 -07:00
Leonardo de Moura
e78de448aa
feat(kernel/type_checker): add is_convertible predicate (and support for proof irrelevance and eta-reduction)
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-23 19:21:26 -07:00
Leonardo de Moura
cdbef0bf15
fix(kernel/type_checker): is_opaque predicate
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-23 10:51:39 -07:00
Leonardo de Moura
a3554c85fe
fix(kernel/definition): clang compilation warning, and add module_idx typedef
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-23 10:50:55 -07:00
Leonardo de Moura
ed37bf650d
chore(kernel/environment): fix style
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-22 18:34:55 -07:00
Leonardo de Moura
04a61bdffe
feat(kernel/type_checker): remove dead code, add basic whnf procedure
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-22 18:32:50 -07:00
Leonardo de Moura
188da7e4c6
feat(kernel/max_sharing): add method already_processed
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-22 18:30:07 -07:00
Leonardo de Moura
9fda7e2529
fix(kernel): incorrect optimization in max_sharing_fn class
...
The resultant expression may failed to be fully shared.
Add an example that demonstrates the problem.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-22 15:38:22 -07:00
Leonardo de Moura
086dd6b1a1
chore(kernel/environment): fix style
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-22 15:36:52 -07:00
Leonardo de Moura
cc1cfba8ad
refactor(kernel/type_checker): new API for type checker
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-21 16:12:47 -07:00
Leonardo de Moura
6417c79569
feat(kernel/environment): add is_descendant method
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-21 14:28:50 -07:00
Leonardo de Moura
bfeb51ce58
feat(kernel/environment): add trust level field
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-21 13:39:47 -07:00
Leonardo de Moura
ee58a83e25
chore(kernel): remove unnecessary files
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-18 14:25:09 -07:00
Leonardo de Moura
d0dc16355b
chore(kernel): remove unnecessary file
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-18 14:23:32 -07:00
Leonardo de Moura
582352d647
refactor(kernel/environment): simplified (functional) environment object
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-18 14:21:49 -07:00