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

123 commits

Author SHA1 Message Date
Soonho Kong
83edc38fa1 Change folddoc to fold_right, add static_asserts for template functions 2013-08-02 19:48:11 -07:00
Soonho Kong
5f10d47035 Change operators in format: 
f1 + f2 = f1 <> f2
f1 ^ f2 = f1 <> " " <> f2
 2013-08-02 19:17:29 -07:00
Soonho Kong
bddecd7d9c Roll back to flatten(line) == " " 2013-08-02 19:16:19 -07:00
Soonho Kong
4ebb96d7cd Add static_asserts to sexpr_funcs.h 2013-08-02 18:26:51 -07:00
Soonho Kong
cda969187a Add one small test to expr 2013-08-02 10:34:46 -07:00
Leonardo de Moura
ae697ddda7 Update CMakeLists.txt: bison++ and flex 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-02 07:56:18 -07:00
Leonardo de Moura
a8c77ff40e Disable eta-reduction for now. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-01 23:19:34 -07:00
Leonardo de Moura
c13b9a792a Add small example 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-01 22:07:28 -07:00
Leonardo de Moura
3ef9d21875 Fix bugs in type checker 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-01 21:40:39 -07:00
Leonardo de Moura
7b00561a94 Normalize level expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-01 21:40:39 -07:00
Leonardo de Moura
e220d7c525 Add type checker. Fix normalization with non-empty context 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-01 21:40:36 -07:00
Leonardo de Moura
bed5f09907 Rename normalize context to local_context. Create context. Fix bug in name.cpp 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-01 21:39:02 -07:00
Soonho Kong
322c2b472d Add more to expr pretty-print 2013-08-01 18:54:06 -07:00
Soonho Kong
229b4f8759 Update format.cpp, flatten(LINE) = "" instead of " " 2013-08-01 18:53:41 -07:00
Soonho Kong
e898bb996c Fix performance bug in format, add paren combinator 2013-08-01 18:03:51 -07:00
Soonho Kong
5a89bffe83 Add pp to expr 2013-08-01 15:42:06 -07:00
Soonho Kong
426c3a667a Update format 
1) operator+ is <> (previously, it was a + b = a <> ' ' <> b)
2) using sstream to compute length of text
 2013-08-01 15:41:45 -07:00
Soonho Kong
0f98ee03b5 Use 'nullptr' instead of '0' 2013-08-01 13:57:43 -07:00
Soonho Kong
a7910e1fe7 Update format.cpp & format.h + Update format tests 2013-08-01 13:43:49 -07:00
Soonho Kong
092b8889e4 Add more tests on sexpr_funcs 2013-08-01 13:43:27 -07:00
Soonho Kong
5be67bd42c Add forall, foldl, foldr to sexpr_funcs 2013-08-01 13:43:27 -07:00
Leonardo de Moura
10def5cabe Remove duplicate code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-29 21:34:16 -07:00
Leonardo de Moura
4efa9a92df Fix performance issue 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-29 21:33:43 -07:00
Leonardo de Moura
08b750c825 Remove Prop from kernel 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-29 19:49:34 -07:00
Leonardo de Moura
6452c69b96 Use level at kernel expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-29 19:44:26 -07:00
Leonardo de Moura
537e2c101c Add more tests. Fix bug in universe implication test. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-29 19:05:43 -07:00
Leonardo de Moura
299ec9c254 Fix space 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-28 23:14:27 -07:00
Leonardo de Moura
279e524c9e Fix bug in universe levels 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-28 23:11:35 -07:00
Leonardo de Moura
a4f456c99e Universe levels 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-28 22:34:39 -07:00
Leonardo de Moura
13bce7bb6f checkpoint 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-26 14:16:29 -07:00
Leonardo de Moura
a241d5f4b1 Add eta-reduction 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-26 12:37:13 -07:00
Leonardo de Moura
ed13132c12 Add has_free_var, lower_free_vars 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-26 12:27:55 -07:00
Leonardo de Moura
09708209a7 Improve documentation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-26 11:43:53 -07:00
Leonardo de Moura
bf0cca3805 Add multi-thread tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-25 22:33:13 -07:00
Leonardo de Moura
b6236130f9 Fix stack overflow at travis when using clang++ 3.3 in debug mode 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-25 22:05:09 -07:00
Leonardo de Moura
f7138b6ecf Fix normalize 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-25 19:13:45 -07:00
Leonardo de Moura
14c899e7ca Add normalize 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-24 19:36:54 -07:00
Leonardo de Moura
5889c6488f Add list template. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-24 16:32:50 -07:00
Leonardo de Moura
b45a5d231c Add buffer test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-24 15:01:19 -07:00
Leonardo de Moura
c2ebe42ca8 Move numerics and sexpr to util 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-24 14:57:51 -07:00
Leonardo de Moura
1f7011353b Add (temporary) buffer class 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-24 14:57:51 -07:00
Leonardo de Moura
0fb93ad6ef Expose max_sharing_fn object 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-24 14:56:32 -07:00
Leonardo de Moura
ed3df178ac Improve hash for hierarchical names. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-24 14:56:32 -07:00
Leonardo de Moura
59592ed36b Add deep copy for kernel expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-24 14:56:32 -07:00
Leonardo de Moura
ceb6537e3a Fix race condition when updating expression flags: max_shared and closed 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-24 14:56:32 -07:00
Leonardo de Moura
1398c927cd Fix compilation error with clang++ 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-24 14:56:32 -07:00
Leonardo de Moura
4b61639f4d Use consistent naming for functional objects 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-24 14:56:32 -07:00
Leonardo de Moura
4ae0c4c445 Remove dead code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-24 14:56:32 -07:00
Leonardo de Moura
9b3c47a521 Refactor instantiate/abstract code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-24 14:56:32 -07:00
Leonardo de Moura
c7b12a2815 Add abstract/instantiate for kernel expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-24 14:56:32 -07:00