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

476 commits

Author SHA1 Message Date
Leonardo de Moura
b81d3309b9 fix(kernel): remove ios hack 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-02 13:03:25 -08:00
Leonardo de Moura
43909ca66b feat(frontends/lean/pp): pretty print SetOpaque command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-01 13:16:44 -08:00
Leonardo de Moura
74cae2a154 refactor(library/elaborator): remove hackish rule 
After the recent fixes, the hack in process_metavar is not needed anymore.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-01 10:55:39 -08:00
Leonardo de Moura
cbd1f98365 fix(library/elaborator): bug at method process_metavar_inst, add new test that exposed the bug 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-01 03:02:41 -08:00
Leonardo de Moura
0d815b8594 refactor(kernel/context): hide that the context is implemented using lists 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-31 19:43:50 -08:00
Leonardo de Moura
1cb7408c46 fix(kernel/normalizer): metavariable reification was incorrect, add tst11 at tests/kernel/normalizer.cpp to expose the bug 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-31 16:24:36 -08:00
Leonardo de Moura
cd3bbb1ebf fix(kernel/builtin): enforcing design decision: semantic attachments are NOT simplifiers, they should do only evaluation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-31 10:14:17 -08:00
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