Commit graph

569 commits

Author SHA1 Message Date
Leonardo de Moura
c485b4bc4c fix(kernel/environment): binary file reader, force the file to be read in binary mode
We need this flag to be able to read the file on Windows.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-30 18:20:40 -08:00
Leonardo de Moura
1f6e959139 feat(deserializer): protect against corrupted binary files
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-30 18:05:38 -08:00
Leonardo de Moura
a80fccea93 chore(*): cleanup builtin registration
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-30 12:19:00 -08:00
Leonardo de Moura
2a2f0b0d89 refactor(kernel/builtin): move helper decl macros to a separate file
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-30 11:51:30 -08:00
Leonardo de Moura
ecd62a1783 refactor(builtin/basic): rename basic.lean to kernel.lean
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-30 11:46:03 -08:00
Leonardo de Moura
72761f14e4 refactor(library/io_state): move to the kernel
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-30 11:20:23 -08:00
Leonardo de Moura
097b10e424 refactor(kernel/builtin): move builtin declarations to basic
There is a lot to be done. We should do the same for Nat, Int and Real.
We also should cleanup the file builtin.cpp and builtin.h.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-29 22:00:03 -08:00
Leonardo de Moura
37e8738a5f refactor(kernel/expr): value deserializer
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-29 20:47:14 -08:00
Leonardo de Moura
de77851a00 refactor(util/object_serializer): add methods write_core and read_core that allows to pack information in the byte used to indicate whether an object is already in the cache or not
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-29 19:59:53 -08:00
Leonardo de Moura
dbd122301a feat(kernel/object): compact object serialization kind ids
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-29 19:19:24 -08:00
Leonardo de Moura
d0fdc3619b feat(kernel/expr): compress application serialization
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-29 19:11:57 -08:00
Leonardo de Moura
14c3e11289 refactor(kernel/builtin): emove mk_bin_rop and mk_bin_lop to library
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-29 15:23:18 -08:00
Leonardo de Moura
92404c511c refactor(kernel/builtin): Bool type does not need to be a semantic attachment
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-29 15:12:08 -08:00
Leonardo de Moura
dfe46b9d25 refactor(kernel/builtin): move definition and axioms to basic.lean
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-29 14:01:30 -08:00
Leonardo de Moura
1b300d3598 chore(kernel/builtin): remove unnecessary functions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-29 12:55:51 -08:00
Leonardo de Moura
df3686634d refactor(kernel/builtin): remove unnecessary predicates
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-29 12:20:29 -08:00
Leonardo de Moura
9fdf2a3f55 feat(kernel): add trust_imported flag, it skips type checking of 'pre-compiled' Lean modules
"Pre-compiled" .olean files were already type checked. The flag -t instructs to Lean to skip
type checking when importing these files.
TODO: add a check-sum.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-29 03:43:53 -08:00
Leonardo de Moura
411ebbc3c1 refactor(library/basic_thms): move the proof of all basic theorems to a .Lean file
This commit also adds several new theorems that are useful for implementing the simplifier.
TODO: perhaps we should remove the declarations at basic_thms.h?

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-29 03:04:49 -08:00
Leonardo de Moura
5e0b344871 fix(kernel/object): uninitialized variable
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-28 21:57:56 -08:00
Leonardo de Moura
41c1010043 feat(frontends/lean/parser): make Import command use binary Lean files
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-28 19:20:04 -08:00
Leonardo de Moura
aee1c6d3f3 feat(kernel): export/import (.olean) binary files
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-28 17:31:35 -08:00
Leonardo de Moura
22bebbf242 feat(kernel/object): serializer for kernel objects
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-28 14:39:10 -08:00
Leonardo de Moura
755e8b735f feat(kernel/expr): serializer for kernel expressions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-28 01:23:21 -08:00
Leonardo de Moura
0ef8ba2939 feat(kernel/level): serializer for level objects
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-27 23:30:13 -08:00
Leonardo de Moura
8cf65f354b fix(frontends/lean/pp): forall and exists pretty printing when used as constants
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-27 12:50:41 -08:00
Leonardo de Moura
2aa691ccb3 fix(kernel/replace_fn): ignore the cached type in constants
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-24 21:11:25 -08:00
Leonardo de Moura
1a0f0c1609 feat(kernel/normalizer): let normalizer ignore 'undefined' constants
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-24 20:54:15 -08:00
Leonardo de Moura
6cc57cc4b5 fix(library/tactic/apply_tactic): bug in apply_tac
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-24 15:54:56 -08:00
Leonardo de Moura
cb95b14332 feat(library/tactic/apply_tactic): improve apply_tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-24 14:23:06 -08:00
Soonho Kong
de018220e1 feat(*): use std::make_shared to create shared_ptr 2013-12-24 14:32:50 -05:00
Leonardo de Moura
b83b17d3ab fix(kernel/metavar): bug at cached_metavar_env::update method
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-23 15:41:02 -08:00
Leonardo de Moura
3e32d9bef2 feat(library/tactic): add support for Pi's at to_proof_state
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-22 16:40:55 -08:00
Leonardo de Moura
4229e498d2 refactor(kernel/type_checker): combine type_checker and type_inferer into a single class, and avoid code duplication
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-22 11:51:38 -08:00
Leonardo de Moura
9128a437b8 refactor(library/cast): replace cast semantic attachment with axioms, add heterogeneous symmetry axiom
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-21 18:23:37 -08:00
Leonardo de Moura
90dbdaec40 feat(kernel/expr): cache is_arrow result
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-21 13:59:45 -08:00
Leonardo de Moura
1faf42e2e1 chore(kernel/expr): remove unnecessary #if-#then-#else
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-21 13:36:41 -08:00
Leonardo de Moura
7b0b363b32 fix(kernel/normalizer): metavariable reification
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-21 06:40:26 -08:00
Leonardo de Moura
84df182beb refactor(kernel/instantiate): remove hackish (dead) function
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-20 14:37:05 -08:00
Leonardo de Moura
7772c16033 refactor(kernel): add unfold_opaque flag to normalizer, modify how type checker uses the opaque flag, remove hidden_defs, and mark most builtin definitions as opaque
After this commit, in the type checker, when checking convertability, we first compute a normal form without expanding opaque terms.
If the terms are convertible, then we are done, and saved a lot of time by not expanding unnecessary definitions.
If they are not, instead of throwing an error, we try again expanding the opaque terms.
This seems to be the best of both worlds.
The opaque flag is a hint for the type checker, but it would never prevent us from type checking  a valid term.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-20 12:47:47 -08:00
Leonardo de Moura
026f666526 feat(kernel/type_checker): use expression before normalization in the unification constraints generated by the typechecker
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-20 11:22:13 -08:00
Leonardo de Moura
4838c055b8 feat(kernel/environment): add set_opaque method
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-20 10:45:44 -08:00
Leonardo de Moura
46627289b8 fix(kernel/expr): avoid '_' as a binder name, we use '_' as a placeholder in the Lean frontend
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-19 14:47:53 -08:00
Leonardo de Moura
6cc83dbe2a fix(kernel/kernel_exception): incorrect pp method
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-19 14:46:22 -08:00
Leonardo de Moura
47c7bb1bde refactor(*): uses aliases for unordered_map and unordered_set
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-18 12:30:45 -08:00
Leonardo de Moura
1e4fa76a47 feat(util/name_map): add template alias
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-18 11:34:40 -08:00
Leonardo de Moura
7b2fea3fab fix(kernel/normalizer): compilation problem with clang++
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-18 08:46:36 -08:00
Leonardo de Moura
418623b874 feat(kernel/replace_fn): add template replace that captures commonly used pattern
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-17 18:31:59 -08:00
Leonardo de Moura
23e518001a feat(kernel/normalizer): avoid unnecessary creation of closures for n-ary functions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-17 18:10:13 -08:00
Leonardo de Moura
10f28c7bec feat(kernel/replace_fn): non-recursive replace_fn
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-17 16:35:39 -08:00
Leonardo de Moura
af4a6c9364 fix(kernel/normalizer): cache problems
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-17 14:52:14 -08:00
Leonardo de Moura
33789fad4c fix(kernel/builtin): make sure the if-then-else semantic attachment is not a simplifier
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-17 14:34:40 -08:00
Leonardo de Moura
c53233ea26 fix(kernel/normalizer): avoid svalue hack, use 'semantic attachments' for implementing closures, include context in the closure
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-17 14:33:42 -08:00
Leonardo de Moura
836357c65c fix(kernel/normalizer): bug in Let normalization
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-17 12:35:25 -08:00
Leonardo de Moura
84bfe2a222 fix(library/elaborator): bug in process_meta_app
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-17 10:56:20 -08:00
Leonardo de Moura
f09fd0fc04 feat(kernel/printer): include de Bruijn index in the debug printer
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-16 16:56:46 -08:00
Leonardo de Moura
af42078205 fix(kernel): incorrect use of scoped_map
This commit also adds a new test that exposes the problem.
The scoped_map should not be used for caching values in the normalizer and type_checker. When we extend the context, the meaning of all variables is modified (we are essentially performing a lift). So, the values stored in the cache are not correct in the new context.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-16 15:11:39 -08:00
Leonardo de Moura
02ee31b786 feat(kernel/normalizer): provide the metavar_env to instantiate and add_inst in the normalizer, it will minimize the number of local_entries needed
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-14 15:41:50 -08:00
Leonardo de Moura
3d30664611 feat(kernel/type_checker): provide the metavar_env to instantiate, it will minimize the number of local_entries needed
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-14 15:13:56 -08:00
Leonardo de Moura
4357c9196e feat(kernel/metavar): make sure that a metavariable 'm' can only be assigned to a term that contains free variables available in the context associated with 'm'
This commit also simplifies the method check_pi in the type_checker and type_inferer.
It also fixes process_meta_app in the elaborator.
The problem was in the method process_meta_app and process_meta_inst.
They were processing convertability constrains as equality constraints.
For example, process_meta_app would handle

    ctx |- Type << ?f b

as

    ctx |- Type =:= ?f b

This is not correct because a ?f that returns (Type U) for b satisfies the first but not the second.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-14 12:25:00 -08:00
Leonardo de Moura
51aee83b70 refactor(kernel/metavar_env): use the same approach used in the class environment in the class metavar_env
This modification was motivated by a bug exposed by tst17 at tests/kernel/type_checker.
metavar_env is now a smart point to metavar_env_cell.
ro_metavar_env is a read-only smart pointer. It is useful to make sure we are using proof_state correctly.

example showing that the approach for caching metavar_env is broken in the type_checker

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-13 18:59:15 -08:00
Leonardo de Moura
2e5e5e187f chore(util/rc): remove unnecessary argument from LEAN_COPY_REF and LEAN_MOVE_REF macros
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-13 15:01:24 -08:00
Leonardo de Moura
fa8b984e27 fix(kernel/environment): compilation warnings
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-13 13:54:45 -08:00
Leonardo de Moura
ae52c8062e chore(kernel/metavar): remove unused function
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-12 17:39:14 -08:00
Leonardo de Moura
450d6a4b1e refactor(util/splay_tree): replace find with splay_find
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-12 17:27:30 -08:00
Leonardo de Moura
f97c260b0b refactor(kernel/environment): add ro_environment
The environment object is a "smart-pointer".
Before this commit, the use of "const &" for environment objects was broken.
For example, suppose we have a function f that should not modify the input environment.
Before this commit, its signature would be
       void f(environment const & env)
This is broken, f's implementation can easilty convert it to a read-write pointer by using
the copy constructor.
       environment rw_env(env);
Now, f can use rw_env to update env.

To fix this issue, we now have ro_environment. It is a shared *const* pointer.
We can convert an environment into a ro_environment, but not the other way around.

ro_environment can also be seen as a form of documentation.
For example, now it is clear that type_inferer is not updating the environment, since its constructor takes a ro_environment.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-12 16:48:34 -08:00
Leonardo de Moura
7b2cbd6926 chore(kernel/environment): remove implementation hack
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-12 16:48:34 -08:00
Leonardo de Moura
3457fe5935 chore(kernel): rename read_only_environment and read_write_environment
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-12 16:48:33 -08:00
Leonardo de Moura
1852c86948 feat(kernel): improve instantiate and lift_free_vars (use metavar_env to minimize the number of lift and inst local_entries needed)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-12 16:48:33 -08:00
Leonardo de Moura
058bdb88ac feat(kernel/context): add operator== for contexts, and new constructor
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-12 16:48:33 -08:00
Leonardo de Moura
38a25a1bd2 feat(kernel/metavar): (re-)enable add_lift simplification
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-12 16:48:33 -08:00
Leonardo de Moura
98f5ce0512 fix(kernel/context): unused var warning in release mode
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-11 21:24:05 -08:00
Leonardo de Moura
3e77dd0c42 fix(kernel/context): make context remove more robust
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-11 19:51:57 -08:00
Leonardo de Moura
c29b155fdd feat(library/elaborator): use improved has_free_vars in the elaborator
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-11 16:15:20 -08:00
Leonardo de Moura
0e2b7973cf feat(kernel/free_vars): improve has_free_vars function, it produces better results for expressions containing metavariables
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-11 16:09:33 -08:00
Leonardo de Moura
af1b0d2e81 feat(library): add function free_var_range for computing the range [0, R) of free variables occurring in an expression
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-11 15:32:50 -08:00
Leonardo de Moura
55389cf6e5 feat(kernel/context): add find, a version of lookup that does not throw an exception
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-11 09:54:54 -08:00
Leonardo de Moura
4de5f06a97 fix(library/elaborator): bug in process_metavar_inst, and disable simplification that is negatively impacting the elaborator
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-10 19:26:58 -08:00
Leonardo de Moura
8f2fe273ea refactor(*): isolate std::thread dependency
This commit allows us to build Lean without the pthread dependency.
It is also useful if we want to implement multi-threading on top of Boost.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-09 15:20:26 -08:00
Leonardo de Moura
25a2f5f7e0 fix(kernel/formatter): clang++ errors and warnings
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-08 18:54:04 -08:00
Leonardo de Moura
445d4f6793 refactor(kernel/unification_constraint): remove 'null' unification_constraint and its operator bool
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-08 18:11:35 -08:00
Leonardo de Moura
340d643d89 fix(library/kernel_bindings): make sure that when a formatter is invoked and it has a reference to an environment object, we get a read-only lock to the environment object
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-08 16:55:55 -08:00
Leonardo de Moura
759fcb7b4f refactor(kernel/formatter): hide 'unsafe' constructor
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-08 15:39:26 -08:00
Leonardo de Moura
a4afdfeace refactor(kernel/expr): remove the dangerous expr::release method
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-08 14:45:18 -08:00
Leonardo de Moura
04b67f8b14 refactor(kernel/object): remove 'null' object, and operator bool for kernel objects
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-08 14:37:38 -08:00
Leonardo de Moura
2f88d6710c feat(kernel/expr): add some_expr and none_expr for building values of type optional<expr>
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-08 10:34:38 -08:00
Leonardo de Moura
25b812f1c9 feat(kernel/expr): no overhead optional<expr> template specialization
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-08 10:17:29 -08:00
Leonardo de Moura
3e1fd06903 refactor(kernel/expr): remove 'null' expression, and operator bool for expression
After this commit, a value of type 'expr' cannot be a reference to nullptr.
This commit also fixes several bugs due to the use of 'null' expressions.

TODO: do the same for kernel objects, sexprs, etc.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-07 23:21:10 -08:00
Leonardo de Moura
b6b520302d feat(kernel/replace_visitor): relax replace_visitor contract, the input expression can be null
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-07 15:35:26 -08:00
Leonardo de Moura
e2999d3ff6 feat(*): add component name to check_stack and check_system
I also reduced the stack size to 8 Mb in the tests at tests/lean and tests/lean/slow. The idea is to simulate stackoverflow conditions.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-07 15:11:55 -08:00
Leonardo de Moura
33b72f1dd0 feat(frontends/lean/parser): apply type inference elaborator to fill remaining metavariables/holes (these are holes produced by tactics such as apply_tac)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-07 13:09:39 -08:00
Leonardo de Moura
195ea24d71 refactor(kernel/type_checker): pass buffer<unification_constraint> as a pointer
The idea is to make it an optional parameter independent of metavar_env.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-07 10:27:11 -08:00
Leonardo de Moura
872434e632 fix(kernel/has_free_vars): return false for null expression
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-06 16:01:57 -08:00
Leonardo de Moura
147626c906 fix(kernel/printer): memory access violation when printing contexts
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-06 15:50:29 -08:00
Leonardo de Moura
0390f3c39b feat(library/tactic/boolean_tactics): avoid unnecessary Let expression in proof terms
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-06 15:01:54 -08:00
Leonardo de Moura
d79a626523 fix(kernel/type_checker): Pi with metavariables case
The type checker (and type inferer) were not handling correctly Pi expressions where the type universe cannot be established due to the occurrence of metavariables. In this case, a max-constraint is created. The problem is that the domain and body of the Pi are in different contexts. The constrain generated before this commit was incorrect, it could contain a free variable. This commit fix the issue by using the context of the body, and lifting the free variables in the domain by 1.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-06 13:07:59 -08:00
Leonardo de Moura
c841763a05 feat(library/elaborator): add special treatment for constraints of the form ?m[inst:i v] << t, where t is a proposition
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-06 04:51:07 -08:00
Leonardo de Moura
c1afefb873 feat(library/fo_unify): unify heterogeneous - homogeneous equality
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-05 19:00:31 -08:00
Leonardo de Moura
873a07d34c feat(kernel/replace_visitor): check interrupted flag and stackoverflow
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-05 05:42:12 -08:00
Leonardo de Moura
029ef57abd feat(library/tactic): add apply_tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-05 03:22:12 -08:00
Leonardo de Moura
bcc8b67592 chore(*): consistent file name convention
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-03 12:40:52 -08:00
Leonardo de Moura
f80106a895 chore(*): use 'explicit operator bool' everywhere.
operator bool() may produce unwanted conversions.
For example, we had the following bug in the code base.

...
   object const & obj = find_object(const_name(n));
   if (obj && obj.is_builtin() && obj.get_name() == n)
...

obj.get_name() has type lean::name
n              has type lean::expr

Both have 'operator bool()', then the compiler uses the operator to
convert them to Boolean, and then compare the result.
Of course, this is not our intention.

After this commit, the compiler correctly signs the error.
The correct code is

...
   object const & obj = find_object(const_name(n));
   if (obj && obj.is_builtin() && obj.get_name() == const_name(n))
...

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-02 23:02:45 -08:00
Leonardo de Moura
74dfdd02de feat(util): add primitives for checking the amount of available stack space
Recursive functions that may go very deep should invoke the function check_stack. It throws an exception if the amount of stack space is limited.

The function check_system() is syntax sugar for
    check_interrupted();
    check_stack();

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-01 17:19:27 -08:00
Leonardo de Moura
1ec8f9d536 feat(kernel): add abstraction (aka function extensionality) axiom
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-01 13:57:14 -08:00
Leonardo de Moura
a9eb2a9307 feat(kernel/builtin): add is_* functions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-29 11:35:58 -08:00
Leonardo de Moura
dae86c2ffa feat(frontends/lean/parser): add basic tactic support in the frontend
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-28 21:08:12 -08:00
Leonardo de Moura
3a93212d5e chore(kernel/expr): fix cpplint warning
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-27 12:59:16 -08:00
Leonardo de Moura
d87ad9eb7e refactor(util/lua): propagate C++ Lean exceptions in Lua
The following call sequence is possible:
C++ -> Lua -> C++ -> Lua -> C++

The first block of C++ is the Lean main function.
The main function invokes the Lua interpreter.
The Lua interpreter invokes a C++ Lean API.
Then the Lean API invokes a callback implemented in Lua.
The Lua callback invokes another Lean API.
Now, suppose the Lean API throws an exception.
We want the C++ exception to propagate over the mixed C++/Lua call stack.
We use the clone/rethrow exception idiom to achieve this goal.

Before this commit, the C++ exceptions were converted into strings
using the method what(), and then they were propagated over the Lua
stack using lua_error. A lua_error was then converted into a lua_exception when going back to C++.
This solution was very unsatisfactory, since all C++ exceptions were being converted into a lua_exception, and consequently the structure of the exception was being lost.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-27 12:25:29 -08:00
Leonardo de Moura
956f203a55 refactor(bindings/lua): move Lua bindings to the file associated with them
The directory bindings/lua was getting too big and had too many dependencies.
Moreover, it was getting too painful to edit/maintain two different places.
Now, the bindings for module X are in the directory that defines X.
For example, the bindings for util/name.cpp are located at util/name.cpp.

The only exception is the kernel. We do not want to inflate the kernel
with Lua bindings. The bindings for the kernel classes are located
at bindings/kernel_bindings.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-26 19:15:56 -08:00
Leonardo de Moura
b41789d085 feat(kernel): add is_bool predicate
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-26 11:34:50 -08:00
Leonardo de Moura
28a56e3acf fix(kernel/expr_eq): the cached type should ignored when comparing expressions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-21 17:29:06 -08:00
Leonardo de Moura
63bbf07f64 feat(library/tactic): add 'idtac' tactic and 'then' tactical
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-21 17:29:06 -08:00
Leonardo de Moura
be8fe1b902 fix(kernel/replace): make it more robust, and add clear method
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-20 13:19:21 -08:00
Leonardo de Moura
6989f1f9ba refactor(kernel/metavar): remove unnecessary variable
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-19 14:41:54 -08:00
Leonardo de Moura
0126fa0499 refactor(kernel): add find_fn, replace for_each_fn with find_fn when appropriate, remove unnecessary function has_cached_type
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-19 13:03:46 -08:00
Leonardo de Moura
5cfcb7e144 chore(kernel/for_each): use consistent naming convetions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-19 11:24:02 -08:00
Leonardo de Moura
7f088b7635 feat(kernel): add (optional) field m_type to expr_const, this field is useful for implementing the tactic framework
This field should not be visible in the external API.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-19 11:21:52 -08:00
Leonardo de Moura
57bf4f3e67 feat(kernel/expr): avoid recursion when deleting expressions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-18 18:41:08 -08:00
Leonardo de Moura
2951c92ad1 feat(kernel/for_each): avoid recursion at for_each template
It saves a lot of stack space.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-18 18:08:31 -08:00
Leonardo de Moura
e0c23e5984 fix(kernel/environment): compilation problem on Windows
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-18 09:52:47 -08:00
Leonardo de Moura
1315378ebb test(*): add missing tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-18 09:13:34 -08:00
Leonardo de Moura
69be5f6c94 feat(kernel/environment): track which modules were already imported
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-17 18:15:44 -08:00
Leonardo de Moura
926ed0a02d feat(lua): add type_inferer object to Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-16 19:18:15 -08:00
Leonardo de Moura
4ebb3c572a feat(kernel/environment): make the environment throw an exception when weak-ref has expired
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-16 18:35:17 -08:00
Leonardo de Moura
516c5c8fea feat(lua): add metavar_env objects to Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-16 14:44:33 -08:00
Leonardo de Moura
8525e8534b feat(lua): expose parse_expr and parse_commands from frontends/lean in the Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-15 16:11:26 -08:00
Leonardo de Moura
691893258d feat(kernel/expr): add hash code based on allocation time
The new hash code has the property that given expr_cell * c1 and expr_cell * c2,
if c1 != c2 then there is a high propbability that c1->hash_alloc() != c2->hash_alloc().

The structural hash code hash() does not have this property because we may have
c1 != c2, but c1 and c2 are structurally equal.

The new hash code is only compatible with pointer equality.
By compatible we mean, if c1 == c2, then c1->hash_alloc() == c2->hash_alloc().
This property is obvious because hash_alloc() does not have side-effects.

The test tests/lua/big.lua exposes the problem fixed by this commit.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-14 02:43:11 -08:00
Leonardo de Moura
ad1180c5b4 fix(kernel/occurs): typos
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-13 17:04:56 -08:00
Leonardo de Moura
9a22702383 feat(lua): make objects() and localobjects() methods return iterators in the environment LUA API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-13 14:26:01 -08:00
Leonardo de Moura
ba0889265e refactor(lua): cleanup Lua bindings
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-13 13:55:05 -08:00
Leonardo de Moura
c4c548dc5d feat(*): simplify interrupt propagation
Instead of having m_interrupted flags in several components. We use a thread_local global variable.
The new approach is much simpler to get right since there is no risk of "forgetting" to propagate
the set_interrupt method to sub-components.

The plan is to support set_interrupt methods and m_interrupted flags only in tactic objects.
We need to support them in tactics and tacticals because we want to implement combinators/tacticals such as (try_for T M) that fails if tactic T does not finish in M ms.
For example, consider the tactic:

    try-for (T1 ORELSE T2) 5

It tries the tactic (T1 ORELSE T2) for 5ms.
Thus, if T1 does not finish after 5ms an interrupt request is sent, and T1 is interrupted.
Now, if you do not have a m_interrupted flag marking each tactic, the ORELSE combinator will try T2.
The set_interrupt method for ORELSE tactical should turn on the m_interrupted flag.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-12 21:45:48 -08:00
Leonardo de Moura
ac6c18321a fix(lua): make sure environment objects can be safely accessed/updated from current threads
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-11 20:29:53 -08:00
Leonardo de Moura
31abc00db8 chore(*): add LCOV_EXCL_LINE to lean_unreachable statements
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-11 09:19:38 -08:00
Leonardo de Moura
7683188ab0 chore(emplace_back): use emplace_back when appropriate
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-10 11:14:04 -08:00
Leonardo de Moura
3078923ea4 fix(kernel/type_checker): add missing test, and kernel_exception has_no_type_exception
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-10 11:14:04 -08:00
Leonardo de Moura
ff16ffaea3 fix(kernel/environment): warning produced by clang
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-07 11:36:08 -08:00
Leonardo de Moura
8012c4f644 fix(kernel/environment): add weak reference to environment objects
We need weak references to environment objects because the environment has a reference to the type_checker and the type_checker has a reference back to the environment. Before, we were breaking the cycle using an "environment const &". This was a dangerous hack because the environment smart pointer passed to the type_checker could be on the stack. The weak_ref is much safer.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-07 11:29:08 -08:00
Leonardo de Moura
9c60eed93c refactor(kernel/metavar): avoid using unique names for default metavariable prefix
The problem is that unique names depend on the order compilation units are initialized. The order of initialization is not specified by the C++ standard. Then, different compilers (or even the same compiler) may produce different initialization orders, and consequently the metavariable prefix is going to be different for different builds. This is not a bug, but it makes unit tests to fail since the output produced by different builds is different for the same input file.
Avoiding unique name feature in the default metavariable prefix avoids this problem.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-07 10:16:25 -08:00
Leonardo de Moura
80e23f98c7 feat(kernel/environment): add environment extension objects, the environment can be extended with frontend specific objects
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-06 19:22:30 -08:00
Soonho Kong
044813615e fix: add '#include <tuple>' 2013-11-03 13:00:42 -05:00
Leonardo de Moura
aa99ac6618 feat(kernel/value): allow semantic attachments to use coercions when being pretty printed
For example, this feature is useful when displaying the integer value 10 with coercions enabled. In this case, we want to display "nat_to_int 10" instead of "10".

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-30 11:42:26 -07:00
Leonardo de Moura
7fc87faa8f feat(kernel): heterogeneous transitivity axiom, we need this axiom to be able to generate modular proofs in the rewriting engine module
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 17:07:30 -07:00
Leonardo de Moura
4dd6cead83 refactor(equality): make homogeneous equality the default equality
It was not a good idea to use heterogeneous equality as the default equality in Lean.
It creates the following problems.

- Heterogeneous equality does not propagate constraints in the elaborator.
For example, suppose that l has type (List Int), then the expression
     l = nil
will not propagate the type (List Int) to nil.

- It is easy to write false. For example, suppose x has type Real, and the user
writes x = 0. This is equivalent to false, since 0 has type Nat. The elaborator cannot introduce
the coercion since x = 0 is a type correct expression.

Homogeneous equality does not suffer from the problems above.
We keep heterogeneous equality because it is useful for generating proof terms.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 16:20:06 -07:00
Leonardo de Moura
521fa1ddb8 style(kernel/metavar): add missing includes
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 03:00:43 -07:00
Leonardo de Moura
7c8daf8974 fix(kernel/metavar): make sure the justification and substitution are always matching each other
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 02:39:52 -07:00
Leonardo de Moura
2c6d4d2225 fix(kernel/normalizer): do not apply substitutions in the normalizer
It is incorrect to apply substitutions during normalization.
The problem is that we do not have support for tracking justifications in the normalizer. So, substitutions were being silently applied during normalization. Thus, the correctness of the conflict resolution in the elaboration was being affected.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 02:14:48 -07:00
Leonardo de Moura
dbefc91151 fix(kernel/metavar): add normalize assignment justification
We need that when we normalize the assignment in a metavariable environment.
That is, we replace metavariable in a substitution with other assignments.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 11:02:34 -07:00
Leonardo de Moura
92f5a31976 feat(kernel/expr): add new mk_app template for creating applications using a collection
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 08:53:58 -07:00
Leonardo de Moura
eaccdcb558 refactor(assumption_justification): move to the kernel
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-26 14:21:29 -07:00
Leonardo de Moura
4bed9f85b0 feat(kernel/for_each): add option for disabling cache of atomic expressions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 15:25:17 -07:00
Leonardo de Moura
ce10bfeaf6 perf(kernel/metavar): improve performance of has_assigned_metavar by avoiding for_each+exception
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 15:19:59 -07:00
Leonardo de Moura
57d9d23bd4 feat(kernel/for_each): allow function F to interrupt for_each search
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 14:58:02 -07:00
Leonardo de Moura
2dd44bdf1a perf(kernel/for_each): delay initialization of visited set
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 14:52:08 -07:00
Leonardo de Moura
c3c66b6c90 feat(make): add THREAD_SAFE build option
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 11:50:35 -07:00
Leonardo de Moura
471bbd4040 refactor(kernel/metavar): combine several splay_trees (at metavar_env) into a single one
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 11:02:19 -07:00
Leonardo de Moura
5e34f410b3 refactor(splay_map): modify splay_find signature
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 10:47:15 -07:00
Leonardo de Moura
5812dfcf44 perf(kernel/justification): remove cache from depends_on
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 10:26:05 -07:00
Leonardo de Moura
2b5c951de3 perf(name): add quick_cmp for hierarchical names
It first compare names using hash codes.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 09:58:06 -07:00
Leonardo de Moura
66f4834dbc perf(kernel/metavar): add quick test that catches many cases
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 09:24:01 -07:00
Leonardo de Moura
f38178311c perf(kernel/expr_eq): delay hashtable initialization
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 09:21:47 -07:00
Leonardo de Moura
412bc792c9 fix(style): missing include
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 08:10:28 -07:00
Leonardo de Moura
0c21f45292 fix(kernel/unification_constraint): memory leak
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 08:06:21 -07:00
Leonardo de Moura
a5c3829d1b feat(kernel): add unexpected_metavar_occurrence exception
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-24 19:56:44 -07:00
Leonardo de Moura
ca6a6d71e5 fix(kernel/printer): bug when printing let expression
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-24 18:05:23 -07:00
Leonardo de Moura
872b698bc3 feat(elaborator): add option m_assume_injectivity for getting more concise solutions
We may miss solutions, but the solutions found are much more readable.
For example, without this option, for elaboration problem

Theorem Example4 (a b c d e : N) (H: (a = b ∧ b = e ∧ b = c) ∨ (a = d ∧ d = c)) : (h a c) = (h c a) :=
    DisjCases H
              (fun H1 : _,
                   let AeqC := Trans (Conjunct1 H1) (Conjunct2 (Conjunct2 H1))
                   in CongrH AeqC (Symm AeqC))
              (fun H1 : _,
                   let AeqC := Trans (Conjunct1 H1) (Conjunct2 H1)
                   in CongrH AeqC (Symm AeqC))

the elaborator generates

Theorem Example4 (a b c d e : N) (H : a = b ∧ b = e ∧ b = c ∨ a = d ∧ d = c) : (h a c) = (h c a) :=
    DisjCases
        H
        (λ H1 : if
               Bool
               (if Bool (a = b) (if Bool (if Bool (if Bool (b = e) (if Bool (b = c) ⊥ ⊤) ⊤) ⊥ ⊤) ⊥ ⊤) ⊤)
               ⊥
               ⊤,
           let AeqC := Trans (Conjunct1 H1) (Conjunct2 (Conjunct2 H1)) in CongrH AeqC (Symm AeqC))
        (λ H1 : if Bool (if Bool (a = d) (if Bool (d = c) ⊥ ⊤) ⊤) ⊥ ⊤,
           let AeqC := Trans (Conjunct1 H1) (Conjunct2 H1) in CongrH AeqC (Symm AeqC))

The solution is correct, but it is not very readable. The problem is that the elaborator expands the definitions of \/ and /\.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-24 16:47:50 -07:00
Leonardo de Moura
bbc265ded4 feat(frontends/lean): hook new elaborator in the default frontend
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-24 15:14:29 -07:00
Leonardo de Moura
434c33f225 feat(metavar): automatically apply beta-reduction when instantiating metavariable applications (i.e., expressions of the form (?m a)), when the metavariable is a lambda
This feature is useful for problems that require higher-order matching and/or unification.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-23 16:35:50 -07:00
Leonardo de Moura
873e56844a refactor(beta_reduction): add function apply_beta
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-23 16:03:52 -07:00
Leonardo de Moura
f1e0d6ec29 refactor(beta_reduction): move beta reduction functions to the kernel, delete reduce.cpp file and tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-23 15:44:26 -07:00
Leonardo de Moura
c1e451151a feat(replace_visitor): add an abstract class for applying transformations on expressions
I also removed replace_using_ctx since it is subsumed by the new class.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-23 15:01:37 -07:00
Leonardo de Moura
13531b7d3e refactor(kernel): rename trace to justification
Motivations:

- We have been writing several comments of the form "... trace/justification..." and "this trace object justify ...".
- Avoid confusion with util/trace.h

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-23 13:42:17 -07:00
Leonardo de Moura
17b48010b7 fix(unification_constraint): fix printer for max constraints
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-23 12:00:29 -07:00
Leonardo de Moura
274b11530f feat(metavar): improve apply_local_context
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-23 11:59:36 -07:00
Leonardo de Moura
b57f492e2d fix(kernel/printer): improve printer for Type expressions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-23 11:58:49 -07:00
Leonardo de Moura
891d22b3de feat(kernel/context): add method for remove context entries at positions [s, s+n).
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 15:52:24 -07:00
Leonardo de Moura
874f67c605 feat(normalizer): remove normalization rule t == t ==> true
This normalization rule is not really a computational rule.
It is essentially encoding the reflexivity axiom as computation.
It can also be abaused. For example, with this rule,
the following definition is valid:

Theorem Th : a = a := Refl b

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 14:02:48 -07:00
Leonardo de Moura
c3e87f106f fix(kernel/trace): fix typo in depends_on
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 08:15:37 -07:00
Leonardo de Moura
183f5a1ccf feat(elaborator): solve unification constraints
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 08:15:36 -07:00
Leonardo de Moura
a1710aeeb9 feat(elaborator): add trace objects for elaborator
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 08:15:36 -07:00
Leonardo de Moura
dc0e7a4472 feat(pos_info_provider): add position information provider for expressions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 08:15:36 -07:00
Leonardo de Moura
8663ac550f feat(kernel/trace): add function depends_on for trace objects
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 08:15:36 -07:00
Leonardo de Moura
b1b49e86e7 test(elaborator): add simple test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 08:15:36 -07:00
Leonardo de Moura
1548ffabb1 feat(elaborator): add new elaborator interface
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 08:15:36 -07:00
Leonardo de Moura
827c65b5e9 feat(kernel): add static_assert for update_metavar
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 08:15:36 -07:00
Leonardo de Moura
61ccaf741c fix(frontend/lean): minor modification to be able to execute lean frontend while refactoring elaborator
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 08:15:36 -07:00
Leonardo de Moura
7cf83800c0 refactor(metavar): implement metavar_env, and use unification_constraint and trace objects in the type_checker, light_checker
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 08:15:36 -07:00
Leonardo de Moura
1f0eab7a14 test(type_checker): add new tests for type_checker trace objects
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 08:15:36 -07:00
Leonardo de Moura
fc288929a2 feat(type_checker): add trace objects to justify constraints created by the type checker
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 08:15:36 -07:00
Leonardo de Moura
5b1b03bafd refactor(is_convertible): move from normalizer to type_checker class
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 08:15:36 -07:00
Leonardo de Moura
85bfa45e6a refactor(kernel_exception): delete kernel_exception_formatter, and implement kernel_exception pretty printer as a virtual method
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 08:15:36 -07:00
Leonardo de Moura
d843d432d3 refactor(kernel): move printer and formatter objects to the kernel
The printer and formatter objects are not trusted code.
We moved them to the kernel to be able to provide them as an argument to the trace objects.
Another motivation is to eliminate the kernel_exception_formatter hack.
With the formatter in the kernel, we can implement the pretty printer for kernel exceptions as a virtual method.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 08:15:36 -07:00
Leonardo de Moura
ddb90d3038 feat(kernel): add unification_constraint and trace objects to the kernel
Trace objects will be used to justify steps performed by engines such as the elaborator. We use them to implement non-chronological backtracking in the elaborator. They are also use to justify to the user why something did not work.

The unification constraints are in the kernel because the type checker may create them when type checking a term containing metavariables.

Remark: a minimalistic kernel does not need to include metavariables, unification constraints, nor trace objects. We include these objects in our kernel to minimize code duplication.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 08:15:36 -07:00
Leonardo de Moura
59914a36f3 refactor(metavar): reorganize and simplify metavariables
- Use hierarchical names instead of unsigned integers to identify metavariables.
- Associate type with metavariable.
- Replace metavar_env with substitution.
- Rename meta_ctx --> local_ctx
- Rename meta_entry --> local_entry
- Disable old elaborator
- Rename unification_problems to unification_constraints
- Add metavar_generator
- Fix metavar unit tests
- Modify type checker to use metavar_generator
- Fix placeholder module

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 08:15:36 -07:00
Leonardo de Moura
0783805671 feat(kernel): add weight to kernel definitions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-15 14:50:08 -07:00
Leonardo de Moura
aa5be3262f fix(type_checker): fix inconsistent cache bug in type_checker, add tests that expose the problem
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-01 19:23:55 -07:00
Soonho Kong
e3b762e909 feat(kernel): add static_assert to expr,expr_eq,replace 2013-10-01 16:47:36 -07:00
Soonho Kong
a832173f5f feat(kernel/expr): add expr::operator() which takes 8 args 2013-10-01 00:19:30 -07:00
Leonardo de Moura
e5d312dc18 fix(kernel): the hash code of expressions was not being used to compare them
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-26 08:41:20 -07:00
Leonardo de Moura
98b4e09063 refactor(kernel): simplify expr_eq
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-25 22:09:08 -07:00
Leonardo de Moura
6477708d78 refactor(debug): improve lean_unreachable(), now we can avoid 'fake' return statements
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-25 21:27:20 -07:00
Leonardo de Moura
9f0dab1add fix(kernel): add declarations for operator<<(std::ostream&, expr const&) and operator<<(std::ostream&, context const&) in the kernel
The actual implementation of these two operators is outside of the
kernel. They are implemented in the file 'library/printer.cpp'.
We declare them in the kernel to prevent the following problem.
Suppose there is a file 'foo.cpp' that does not include
'library/printer.h', but contains

    expr a;
    ...
    std::cout << a << "\n";
    ...

The compiler does not generate an error message. It silently uses the
operator bool() to coerce the expression into a Boolean. This produces
counter-intuitive behavior, and may confuse developers.
2013-09-25 17:45:54 -07:00