Commit Graph

126 Commits

Author SHA1 Message Date
499fa0c667 Add option to specify output color choice 2020-05-22 19:33:06 +02:00
739cae1f7c Rename “assert” statement to “spec” 2020-05-22 18:34:59 +02:00
116f74f63e Minor clean-up 2020-05-22 18:17:00 +02:00
0578e99dc2 Finish basic simplifications 2020-05-22 18:14:56 +02:00
3b3f9017ba Determine variable IDs correctly 2020-05-22 02:42:38 +02:00
81ddfd450a Use custom foliage flavor
With this patch, properties specific to variable, function, and
predicate declarations are directly stored within those objects rather
than external maps that need to be queried via traits. This greatly
simplifies many parts of the logic.

This is made possible by implementing a custom foliage flavor, which
makes it possible to swap the built-in declaration types for extended
versions of those types that fulfill certain requirements.
2020-05-22 02:25:00 +02:00
b62c379b97 Properly handle input/output errors 2020-05-19 13:10:31 +02:00
efe354faad Clean up unused struct 2020-05-19 13:02:12 +02:00
efa5656e39 Clean up unused struct 2020-05-19 13:01:04 +02:00
d88ac89b01 Add prime number example 2020-05-19 12:57:09 +02:00
86d2857494 Start implementation of simplifications 2020-05-19 12:56:46 +02:00
d77c7648b3 Ensure that statements are proven in right order 2020-05-19 12:56:21 +02:00
34b8dce9be Ignore built-in predicates in completion 2020-05-19 12:54:51 +02:00
7020bc0bf0 Address unused variable 2020-05-19 12:53:37 +02:00
0229adef78 Add to-do notes 2020-05-19 12:49:57 +02:00
c1038b398c Improve warning when using private predicates in specification 2020-05-19 12:47:24 +02:00
3bf981236a Only warn if private predicates are used in specification 2020-05-19 12:18:11 +02:00
4de4cc21da Fix gross bug in translation of division 2020-05-18 05:21:27 +02:00
80d39c8c0a Check that only input/output predicates are used in specification 2020-05-18 02:17:30 +02:00
e2281042c9 Rename example files for consistency 2020-05-18 01:46:16 +02:00
ce51d14a9e Minor formatting 2020-05-18 01:29:30 +02:00
58d89b4d07 Detect cyclic dependencies when hiding predicates 2020-05-18 01:19:59 +02:00
c0bfbc923c Do not add type declarations for built-ins 2020-05-18 01:19:46 +02:00
0cce3bf54d Rename status message for clarity 2020-05-18 01:19:00 +02:00
7361084eaf Rename variable in example for consistency 2020-05-18 01:09:15 +02:00
82422cc28f Support hiding auxiliary predicates 2020-05-13 08:02:04 +02:00
84031c483b Revert logic for building completed definitions 2020-05-13 03:27:47 +02:00
b308847ebd Add to-do note 2020-05-13 03:17:37 +02:00
d35d0d1d98 Use statement kind over section kind 2020-05-13 03:17:33 +02:00
0dbf30bb1b Work in progress 2020-05-13 02:24:13 +02:00
4d00fbeb97 Minor formatting 2020-05-13 01:40:44 +02:00
07fc6a7f85 Add to-do note 2020-05-13 01:28:25 +02:00
37f0fff09f Add comments to exact cover example 2020-05-12 06:39:50 +02:00
f39393ebce Add comments to example 2 2020-05-12 06:10:59 +02:00
9621cb1e0c Add to-do note 2020-05-12 06:10:52 +02:00
8153352b66 Support comments in specification file 2020-05-12 06:08:50 +02:00
e42fd92d4b Add parser support for output statements 2020-05-12 05:27:51 +02:00
32b18e2b63 Refactor parsing formulas 2020-05-12 05:20:48 +02:00
2f48e51244 Refactor parsing input statement terminator 2020-05-12 05:09:13 +02:00
0d63a721c7 Refactor parsing input statements 2020-05-12 05:05:49 +02:00
e5d8a8a96b Refactor parsing domain specifiers 2020-05-12 04:51:52 +02:00
222f8b535e Add specification for example 1 2020-05-12 04:51:52 +02:00
9ffd987e10 Add specification for example 0 2020-05-12 04:51:52 +02:00
7d06601c17 Color output 2020-05-12 04:51:51 +02:00
2de8a59b63 New output format 2020-05-11 05:03:59 +02:00
eab3520e44 Minor formatting 2020-05-11 04:15:05 +02:00
fed095ba5c Remove obsolete example 2020-05-11 04:09:52 +02:00
78935f7c4a Remove unnecessary lemma 2020-05-11 04:08:38 +02:00
674cee0e87 Remove obsolete to-do note 2020-05-11 04:00:51 +02:00
2ed1e6d89d Rename function 2020-05-11 04:00:06 +02:00