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

36 commits

Author SHA1 Message Date
Soonho Kong
bc60b47295 Apply coding style 2013-09-13 18:48:09 -07:00
Leonardo de Moura
4c19cc6957 Rename lean frontend files. The prefix lean_ is not necessary anymore. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-12 20:09:35 -07:00
Leonardo de Moura
26097475fd Use fullpath in #include directives. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-12 20:04:10 -07:00
Leonardo de Moura
6da194334e Move 'slow' test files to different subdir. Modify CTestCustom.cmake.in to run leantests. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-06 08:48:12 -07:00
Leonardo de Moura
9f34f96b08 Add another example 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-04 05:40:28 -07:00
Leonardo de Moura
0c071d43af Move examples to lean examples subdir. We should have an example subdirectory for each frontend 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-03 20:42:20 -07:00
Leonardo de Moura
8e7c657cf7 Use expected type of a definition in the elaborator. Improve elaborator solver. Add new example 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-03 18:04:42 -07:00
Leonardo de Moura
e54338f4a8 Add a real example. Fix bug in the parser 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-31 19:32:08 -07:00
Leonardo de Moura
51640ecff8 Move files in examples directory to tests directory. They are not real examples 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-31 19:16:30 -07:00
Leonardo de Moura
389f23f356 Add test script 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-31 18:31:39 -07:00
Leonardo de Moura
03a5b5dbd0 Add more tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-31 14:25:27 -07:00
Leonardo de Moura
4b7d4cf0d1 Add latest example to regression suite 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-30 16:39:31 -07:00
Leonardo de Moura
4ef4655183 Add homogeneous equality 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-30 14:26:12 -07:00
Leonardo de Moura
8dacd97801 Remove obsolete commands. 2013-08-27 16:03:45 -07:00
Leonardo de Moura
76c968a5b8 Add basic support for hiding implicit arguments when pretty printing. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-26 20:35:10 -07:00
Leonardo de Moura
ece6e6ca6a Add interrupt to parser. Add elaborator to parser. Add placeholder support in the scanner. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-25 11:02:34 -07:00
Leonardo de Moura
dc91a7adb8 Add Ctrl-C support for interrupting Lean shell. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-24 16:11:35 -07:00
Leonardo de Moura
bd3b422158 Add support for READLINE. Remark: it is not enabled by default. Rename tcmalloc option to TCMALLOC (using consistent name convention for cmake parameters). 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-21 19:08:44 -07:00
Leonardo de Moura
59e63c0421 Add prompt when in interactive mode. Fix Show Environment [num] 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-21 18:24:26 -07:00
Leonardo de Moura
31460aa5b8 Add option declarations. Add Help. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-21 17:02:09 -07:00
Leonardo de Moura
ce470f57db Add set options to lean_parser. Add support for disabling unicode output. Use channels in lean_parser. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-21 12:42:55 -07:00
Leonardo de Moura
d750469667 Move frontend to frontends/lean 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-21 09:04:49 -07:00
Leonardo de Moura
754227fc89 Pretty print forall/exists expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-19 15:48:31 -07:00
Leonardo de Moura
a46bf357b0 Fix bug in level.cpp. Add new example 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-18 18:37:47 -07:00
Leonardo de Moura
95cfac426d Add parse_level. Fix bug at environment::is_ge 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-18 18:25:34 -07:00
Leonardo de Moura
5d609928af Add support for reading input files from the command line. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-18 16:23:29 -07:00
Leonardo de Moura
aa49eb4b0f Run examples during testing 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-18 15:51:27 -07:00
Leonardo de Moura
c82a704302 Add Lean default application. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-18 11:02:29 -07:00
Leonardo de Moura
c581990f67 Clean white-spaces 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-19 10:29:33 -07:00
Leonardo de Moura
e559bf73a9 Add basic testing infrastructure using CTest 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-18 09:12:07 -07:00
Leonardo de Moura
4ccf770b64 Move mpz, mpq and mpbq to numerics directory 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-17 14:33:00 -07:00
Leonardo de Moura
d028041135 Add methods to mpz, mpq, mpbq 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-17 14:24:35 -07:00
Leonardo de Moura
88b49ec21f Add thread_local test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-17 12:43:28 -07:00
Leonardo de Moura
c0f9f06d70 Set clang++ as default compiler. Add -pthread as a linker flag 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-17 12:41:28 -07:00
Leonardo de Moura
501f63e27d Add build instructions. Improve build. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-16 22:32:21 -07:00
Leonardo de Moura
139f4f2a7f Add simple build system based on cmake 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-16 22:10:51 -07:00