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

90 commits

Author SHA1 Message Date
Leonardo de Moura
0c09e4524a Use consistent names for import functions, and library files. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-13 08:58:34 -07:00
Leonardo de Moura
070c87bef0 Rename arith library files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-13 08:55:09 -07:00
Soonho Kong
5c3866cd71 Use fullpath in #include directives, add missing STL headers 2013-09-13 03:35:29 -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
3657320edb Add basic list functions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-11 19:48:54 -07:00
Leonardo de Moura
6fe86ffefd Fix initialized memory error reported by Valgrind. Disable 2 tests that produce memory leaks due to a bug in g++. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-10 13:51:02 -07:00
Leonardo de Moura
4c67721d32 Fix test error on Cygwin 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-09 18:35:11 -07:00
Leonardo de Moura
2ca30571b4 Display the input term in the output of the Check command. It is useful to see the fully elaborated term. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-08 22:55:21 -07:00
Leonardo de Moura
59a589037e Keep expanded form when pretty printings variable declarations with implicit marks (i.e., curly braces) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-08 11:23:46 -07:00
Leonardo de Moura
df116f88e0 Improve pretty printer for Pi's 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-08 11:04:07 -07:00
Leonardo de Moura
33c4b44b2b Encapsulate context implementation. The current implementantion based on lists may be a performance problem in the future, and we should be able to change it without affecting the whole code base. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-07 11:15:11 -07:00
Leonardo de Moura
c674bb3790 Add castlib as an independent library 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-06 23:40:47 -07:00
Leonardo de Moura
7a9d53d0d7 Refactor arith libraries 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-06 23:19:47 -07:00
Leonardo de Moura
7eab229114 Improve check_pi in lean elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-06 18:58:33 -07:00
Leonardo de Moura
c0c2f52087 Add Cast, DomInj and RanInj. Improve operator << for lean_frontend objects. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-06 18:32:15 -07:00
Leonardo de Moura
b62816cc25 Fix problem with pretty printer. Add another test for elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-06 18:01:11 -07:00
Leonardo de Moura
edafd519e1 Add missing case to elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-06 17:43:08 -07:00
Leonardo de Moura
26bf7bcaac Fix bug in the elaborator. Move character ' to class A 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-06 17:12:35 -07:00
Leonardo de Moura
8840b37258 Fix type checker and elaborator for let expressions. Fix get_coercions (we need to pass the context). Fix pretty printer for def_type_mismatch_exception. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-06 11:02:00 -07:00
Leonardo de Moura
2459c4ae7c Add (optional) type to let declarations 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-06 10:06:26 -07:00
Leonardo de Moura
6f3b0c30fb Add 'Variables' command. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-06 08:48:12 -07:00
Leonardo de Moura
3dc55c452c Parse decimal values 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-06 08:48:12 -07:00
Leonardo de Moura
b3a095b068 Fix pretty printer for evaluator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-05 18:57:29 -07:00
Leonardo de Moura
c22bd8b6ed Clean elaborator_exception pretty printing 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-05 10:15:52 -07:00
Leonardo de Moura
eb96e6441f Moved kernel exception formatting to kernel_exception_formatter.cpp. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-05 10:15:43 -07:00
Leonardo de Moura
87d3961158 Improve elaborator error messages 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-04 16:36:58 -07:00
Leonardo de Moura
408005b730 Fix typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-04 16:36:57 -07:00
Leonardo de Moura
d41160f8a5 Modify environment. Now, when a builtin value is declared, if it has a unicode alternative representation, then we add it as a definition. Now, everything that occurs in the environment has been 'declared'. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-04 08:53:00 -07:00
Leonardo de Moura
e955c054ca Modify type checker. Now, it only accepts builtin values that have been declared in the environment. The idea is to be able to track which classes of builtin values have been used in a given environment. We want to be able to quantify the size of the trusted code base for a particular development. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-04 08:30:04 -07:00
Leonardo de Moura
00bee9c96e Fix warning produced by clang++ 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-04 04:40:43 -07:00
Leonardo de Moura
57c0c69872 Fix bug reported by Valgrind. Reason: m_metavars is a vector of metavar_info; each metavar_info has a context; when we invoke mk_metavar the vector can grow in size, and the context is moved to a new location. The previous location is invalidated. To avoid the problem we have to save ctx in a local variable. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-04 04:29:03 -07:00
Leonardo de Moura
fc9e395818 Define absolute value function and notation for it. Add new example. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-03 20:39:54 -07:00
Leonardo de Moura
3992c4b8f9 Define divides, and add examples 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-03 20:18: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
4a75e2d965 Fix bug when pretty printing function applications where the head is a meta-variable. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-03 17:51:56 -07:00
Leonardo de Moura
51422fe654 Modify the parser for accepting expressions such as: 'fun a b, f a b', 'forall a, f a > 0', etc. This is just syntax sugar for 'fun (a : _) (b : _), f a b' and 'forall a : _, f a > 0' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-03 17:24:05 -07:00
Leonardo de Moura
a154f4e439 Modify Set command in the default lean frontend. Now, the lean prefix (for lean default frontend specific options) is optional when we are in the lean front-end. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-03 11:07:28 -07:00
Leonardo de Moura
544229e5d3 Create pp::unicode option. The idea is to be able to disable unicode characters, but still be able to use mixfix notation. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-03 10:11:45 -07:00
Leonardo de Moura
e031d7bc10 Improve error messages when overloads+coercions do not work 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-02 20:05:47 -07:00
Leonardo de Moura
fd44ec8d79 Improve application type mismatch error messages 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-02 18:28:12 -07:00
Leonardo de Moura
395513258e Define mod and unary minus 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-02 16:31:44 -07:00
Leonardo de Moura
abc939382b Add Real arithmetic. Fix elaborator for coercions. Now, two overloads are considered ambiguous if they need the same number of coercions. Improve pretty printer for nest infix operators with same precedence and associativity. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-02 13:20:00 -07:00
Leonardo de Moura
e218b92a9d Modify verbose message for Set command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-02 12:29:21 -07:00
Leonardo de Moura
0a67679afb Add natural numbers. Fix how coercions and overloads interact (switch to approach used in C++). Add notation for natural and integer arithmetic. Rename m and u universe variables to M and U. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-02 12:24:29 -07:00
Leonardo de Moura
db88920f81 Rename normalize and type_check to normalizer and type_checker (using a consistent naming convention) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-02 08:43:38 -07:00
Leonardo de Moura
c97e669f0c Add coercion support in the elaborator and pretty printer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-01 19:09:07 -07:00
Leonardo de Moura
e8c09015ad Move elaborator to lean default frontend. It is getting too specific 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-01 18:22:24 -07:00
Leonardo de Moura
42be7a4989 Add coercion declarations 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-01 18:11:28 -07:00
Leonardo de Moura
598daa40bc Refactor elaborator for supporting overloads 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-01 10:24:10 -07:00