Leonardo de Moura
|
f5e0150db3
|
Allow notation to be associated with arbitrary expression (instead of only constants).
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-08-19 20:05:56 -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
|
986d9635e1
|
Add syntax sugar for forall/exists expressions. Fix problem when pretty printing nested equalities.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-08-19 15:48:07 -07:00 |
|
Leonardo de Moura
|
de80db3985
|
Add support for pretty printing Dags. Find unused prefix for naming shared expressions.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-08-19 12:04:40 -07:00 |
|
Leonardo de Moura
|
7a9319b72e
|
Pretty print let expressions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-08-18 15:25:20 -07:00 |
|
Leonardo de Moura
|
7ec7b4dce8
|
Fix bug in pretty printer
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-08-18 11:02:29 -07:00 |
|
Leonardo de Moura
|
80ec48c93d
|
Make sure formatter can be used even when associated frontend is not in scope.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-08-17 12:33:19 -07:00 |
|
Leonardo de Moura
|
6edae938b7
|
Improve list iterator
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-08-17 11:31:36 -07:00 |
|
Leonardo de Moura
|
a6f36ba546
|
Improve formatter usage. Fix bug in object printer.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-08-17 11:29:43 -07:00 |
|
Leonardo de Moura
|
0f3af23778
|
Fix crash when trying to format an object created by a different frontend.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-08-17 11:04:22 -07:00 |
|
Leonardo de Moura
|
b633c866e6
|
Expose environment API in the frontend object. Add support for formatting objects.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-08-17 10:55:42 -07:00 |
|
Leonardo de Moura
|
15c1c97873
|
Refactor frontend pretty printer
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-08-16 20:40:39 -07:00 |
|
Leonardo de Moura
|
111cdd4e62
|
Remove pretty printer from kernel. Add basic printing capability to exprlib module.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-08-16 20:40:39 -07:00 |
|
Leonardo de Moura
|
4560527058
|
Conjunction and Disjunction are right associative. Add notation for implication. Use Isabelle precendence levels.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-08-16 09:26:05 -07:00 |
|
Leonardo de Moura
|
d002074419
|
Fix uninitialized variables bug
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-08-16 09:02:07 -07:00 |
|
Leonardo de Moura
|
07946f9e32
|
Fix bug in pretty printer
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-08-15 20:10:00 -07:00 |
|
Leonardo de Moura
|
efbf3a434d
|
Highlight assignment keyword
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-08-15 20:00:12 -07:00 |
|
Leonardo de Moura
|
43fa55723a
|
Pretty print condensed definitions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-08-15 19:56:29 -07:00 |
|
Leonardo de Moura
|
790d4a4447
|
Move pretty printer to frontend. Add support for mixfix pretty printing
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-08-15 19:02:28 -07:00 |
|