Simplified .hgignore
Simplified .hgignore
Simplified .hgignore
Simplified the .hgignore
Simplified the .hgignore
Simplified the .hgignore. Disabled one proof implementation. Note tests currently don’t work without --enable-128
Simplified .hgignore
Simplified .hgignore
CVC4 couldn’t solve lemma_exp2_halving_regrouping instead, so use lemma_div_by_exp_regrouping and avoid CVC4 here.
Temporarily disable a proof implementation.
Remove dependence on exp2_proofs.sats
Note that this isn’t really implemented.
Field access routines.
Switch back from size_t to uint32, and also change how the head pointer works. Some further ideas.
Start a new branch.
Wrote ‘make_new_node’.
Call ‘uint32’ by the name ‘ui’. Then we can more easily change it to ‘uint64’, ‘size_t’, or whatever.
Checking in work for reference, before abandoning it.
Added a ‘starting_node_size’ function.
Added a comment about the implementation.
Bug fixes and some minor changes.
A small change.
Use C11 static_assert() to check that atomic_flag is not larger than uint32.
Another new start.
Layouts and basic documentation.
Let the C compiler figure out padding sizes!
I forgot to include some standard ATS headers. Including them let me get rid of the need for SIZEOF_VOID_P.
A new and more efficient way of doing things.
Close this branch.
Got rid of unsafe.sats.
Change a type to size_t.
Some basics that I want to check in so they do not get lost. They required some work and thought.
Be a little more realistic about run-time checks.
A new approach.
A few minor changes.
Further improvements made possible by discovery of my error.
Change ui=uint32 to ui=size_t.
Added an effects mask.
Initial commit, with empty content.
Use DSATS2 Byte Vectors alignment support, instead of playing tricks with C structs.
Add a note to the README that the library is not yet ready.
Initial README.md
.hgignore created online with Bitbucket
It compiles. I still want to make more modifications from the original code taken from Sorts Mill Core Library.
Checking in before I break something. No, it does not work yet. Too many changes in Postiats since I wrote it.
A few more changes, while it still compiles.
Put $effmask_exn around all the assertlocs that are there in lieu of proofs.
A few more changes.
Eliminate more ‘extern fn/implement’ in favor of ‘fn’, in vector_tries.dats.
Passes test.
One does not need to staload array_misc.sats.
More minor modifications.
Add an staload.hats.
get_chunk isn’t needed anymore.
I managed to get ‘left dense’ preconditions set in some places, to help guarantee correct code.
Got rid of one place where an assertloc was masked.
A clarifying reversal of sense of some tests.
Got rid of another assertloc, by using a proof that was already available.
Another step in the process.
A start of eliminating another assertloc.
Fix my broken mod and div functions.
We have managed to get rid of another assertloc.
Make tail length more informative.
I got rid of the remaining assertloc. Yay.
An extra use of a particular proof no longer is necessary.
Fixed Emacs header.
I got rid of another assertloc, although in an ugly way.
Fix emacs header.
Fixes to some proofs I kind of broke.
Interfaces for ‘sets’ functions updated.
I got rid of memset_unsafe.
Eliminated one of the memcpy_unsafe calls.
Got rid of another memcpy_unsafe.
No need for the $STRING library, now.
Oops. I left in some code I didn’t want.
Oops, bad unsafe typecast.
I forgot to check in some files.
Slice and slice-append functions revised.
A few more tightenings of effects.
Revised the pop functions.
I have finished a certain sort of revisions.
Add the generic C version.
Make distcheck work, again.
Minor change to a comment.
Relax the effects but leave a note saying I might have relaxed them too much.
Get rid of array_v(.,.,.) notation in favor of the builtin @[.][.] @ .
Be stricter with !ref effects.
Hash function added, but not yet with tests.
Use exceptions from DSATS2 Modules.
Regression testing of hashing now is included.
Remove an obsolete comment.
Remove ‘entry refs’ as too complex, and also all traces of cursors, as probably not worth it.
Implementation of vector trie modules, so far.
Vector modules have left-right sense, now.
I removed call-by-value array operations.
More opposite-sense functions.
vector slices and appends.
A few little tests.
Add a module reversal function and write some of the testing for it.