-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathChangeLog
190 lines (117 loc) · 6.11 KB
/
ChangeLog
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
2023-01-24 John D. Ramsdell <[email protected]>
* getopt.ml, getopt.mli: Added these sources files to this
distribution so that they could be updated to work with OCaml 5.0.
The original version accessed Pervasives.incr which has
disappeared in OCaml 5.0. Also added the COPYING notice in
ocaml-getopt into getopt.ml as a comment.
* version.ml (version): Updated number to 1.5.
2020-11-27 John D. Ramsdell <[email protected]>
* chase.opam (version): Tagged as version 1.4.
2020-11-18 John D. Ramsdell <[email protected]>
* herald.ml (parse_herald): Added input_order to the kinds of
runtime parameters that can be specified in a source file.
2020-11-17 John D. Ramsdell <[email protected]>
* chaseformsused: Added script that extracts the formulas used
during a run of Chase.
2020-11-10 John D. Ramsdell <[email protected]>
* solve.ml (solve): Added input order mode (-i) as an option. In
input order mode, formulas are tried in the order they are given in
the input source file, otherwise, the order is dynamically changed
to prevent starvation of some rules.
* version.ml (version): Updated number to 1.4.
2020-02-25 John D. Ramsdell <[email protected]>
* chase.opam (version): Tagged as version 1.3.
2020-02-22 John D. Ramsdell <[email protected]>
* markdown/*: Added literate theory examples in Markdown syntax.
2020-02-22 John D. Ramsdell <[email protected]>
* version.ml, chase.opam, README.md, chase.xhtml: Updated version
number to 1.3. Field url in chase.opam not yet updated.
2020-01-26 John D. Ramsdell <[email protected]>
* reader.ml (read_lexbuf): When the input file name has the
extension ".md", the input syntax is treated as Markdown, and
Chase input is extracted from fenced code blocks.
2019-10-21 John D. Ramsdell <[email protected]>
* version.ml (version): Updated to 1.2.
2019-10-03 John D. Ramsdell <[email protected]>
* parser.mly, quant_printer.ml: Removed syntax that allows empty
antecedents and consequences in quantifier syntax.
2019-09-26 John D. Ramsdell <[email protected]>
* parser.mly: Removed syntax that allows empty antecedents and
consequences.
2019-09-22 John D. Ramsdell <[email protected]>
* chase.ml (run): Made reference to Main.margin field explicit
because 4.09 introduced the Format.margin field.
2019-09-19 John D. Ramsdell <[email protected]>
* sym.ml (namings): Improved the asymptotic performance of
printing contexts by using int maps for namings.
2019-09-18 John D. Ramsdell <[email protected]>
* parser.mly (form): Allowed formulas to omit the => operator when
the antecedent of a formula is empty or true.
2019-08-20 John D. Ramsdell <[email protected]>
* version.ml (version): Updated to 1.1.
2019-07-17 John D. Ramsdell <[email protected]>
* unflatten.ml (make_subst): Fixed function so that unflatten
followed by flattening is an isomorphism.
2019-06-19 John D. Ramsdell <[email protected]>
* sexpr_printer.ml (print_frame): Added a space after key "facts"
in a structure.
2019-02-07 John D. Ramsdell <[email protected]>
* chase.ml (carefully_set_margin): Set the maximum margin when
setting the margin so that line breaks occur only at break
hints. This fixes a bug in chasetree which caused facts to be
printed in bold even when the fact is in the parent structure.
The documentation in the standard library Format module is
unhelpful about the need for this code. A bug report has been
submitted.
2019-01-29 John D. Ramsdell <[email protected]>
* chase.mk, chase.xhtml: Added a makefile rule that preprocesses
files with extension .glm using m4. This allows file inclusion.
2019-01-17 John D. Ramsdell <[email protected]>
* fact_printer.ml (print_arg): Special cased the printing of single
argument function application so as to avoid some bad breaks that
confuse chasetree, and cause it to think some facts are new when
they are not. The program still has a bug in that it can break
"prec(a,b)" after the open parenthesis.
2019-01-12 John D. Ramsdell <[email protected]>
* chasetree.ml (header): Added Javascript that scrolls the initial
diagram view so that it includes the first structure.
2019-01-11 John D. Ramsdell <[email protected]>
* chasetree.ml (strong): Added emphasis for facts that are new in
a tree node.
2019-01-09 John D. Ramsdell <[email protected]>
* quant_parser.mly (body): Enabled universal quantifiers for
variables that occur only in the consequent of a sequent.
2019-01-08 John D. Ramsdell <[email protected]>
* structure.ml (structure): Added support for universal
quantification in the consequent of a sequent.
2018-12-28 John D. Ramsdell <[email protected]>
* solve.ml (loop): Prioritize lightweight formulas during the
chase.
2018-12-18 John D. Ramsdell <[email protected]>
* fact_printer.ml (print_compact): Added the -c option that
prints structures compactly.
2018-12-14 John D. Ramsdell <[email protected]>
* id.ml, match.ml: Changed the representation of atomic formulas
to use tries for the relations.
2018-12-13 John D. Ramsdell <[email protected]>
* main.ml (show_time): Added the -p option that shows processor
time used in a run.
2018-12-12 John D. Ramsdell <[email protected]>
* id.ml (IdHashtbl): Added hash tables for IDs and used them for
structures.
* reader.ml (from_atom): Restricted predicates symbols to ones
that are not capitalized.
2018-12-08 John D. Ramsdell <[email protected]>
* src/chase/solve.ml (solve): Added a mode in which the chase
successfully terminates after finding just one model.
2018-12-01 John D. Ramsdell <[email protected]>
* main.ml (cmdline): Use getopt for command line processing.
2018-11-15 John D. Ramsdell <[email protected]>
* cong_close.ml (intern): Corrected a serious bug in which intern
failed to put terms that involved function application into the
same equivalence class when it should have.
2018-11-12 John D. Ramsdell <[email protected]>
* solve.ml (rules): Disable a fact whenever it has been used
once. A fact is a rule with a true antecedent.
2018-06-12 John D. Ramsdell <[email protected]>
* version.ml (version): updated to 1.0.