better implementation of strings #100

Closed
xrchz opened this Issue Feb 13, 2016 · 4 comments

Projects

None yet

1 participant

@xrchz
Member
xrchz commented Feb 13, 2016

Change the implementation of strings to target something that wastes less space (and is still efficient). This probably means a change in pat_to_clos, as well as some more operations required in closLang and below.

I believe the current target is that string = CharVector.vector (and char = CharVector.elem), as in SML, but we need to implement the monomorphic vectors better. (We would probably get Word8Vector almost for free out of this, although char and word8 are still distinct at the top level semantics.)

Context:
Discussion: starting with https://lists.cakeml.org/private/dev/2015-June/000949.html
Wiki page: https://wiki.cakeml.org/Standard%20Library

@xrchz
Member
xrchz commented May 13, 2016

#49 is related

@xrchz xrchz self-assigned this Dec 5, 2016
@xrchz
Member
xrchz commented Dec 5, 2016 edited

@myreen suggests the easiest way to change the representation is to do it in clos_to_bvl, by adding a new ByteVector value to closLang which gets compiled into byte arrays in BVL. This would be better than doing it in the obvious place (pat_to_clos) since that proof is not set up to add new references or stubs (we might want string append to be a new primitive). The clos_to_bvl proof is set up for adding new references and new stubs.

@xrchz
Member
xrchz commented Jan 18, 2017

more specific implementation notes: make ByteArray take a bool in BVL indicating whether it is mutable or not (this is necessary for the equality semantics)

@xrchz xrchz added a commit that referenced this issue Jan 18, 2017
@xrchz xrchz Start adding ByteVectors to closLang
Towards Issue #100
a4e6a7f
@xrchz xrchz added a commit that referenced this issue Jan 20, 2017
@xrchz xrchz Update some clos proofs for ByteVector
More preliminary work on #100
9a9ada8
@xrchz xrchz added a commit that referenced this issue Jan 20, 2017
@xrchz xrchz Add String op to closLang, fix pat_to_closProof
Plus fix various other closLang-related proofs.
The big missing thing is clos_to_bvl and anything below that.

So, there are 4 new operators in closLang. I think they are all
necessary:
  - create a (compile-time) constant string
  - create a string from a list
  - get the length of a string
  - get the nth char from a string

For issue #100.
17777aa
@xrchz xrchz added a commit that referenced this issue Jan 23, 2017
@xrchz xrchz Update clos_to_bvlProof for immutable ByteArrays
As part of this, fix the BVL equality semantics (to follow the RefPtrs
to check if they need to be compared-by-contents).

Towards issue #100
710022f
@xrchz xrchz added a commit that referenced this issue Jan 24, 2017
@xrchz xrchz Update bvl_to_bviProof
For Issue #100
053cd83
@xrchz
Member
xrchz commented Jan 25, 2017

The remaining work here is updating equality in wordLang and also implementing the strings in wordLang. However, to make it easier, what should be done is: implement String and FromListByte in bvl_to_bvi (as part of the compile_op, possibly requiring a stub).

@xrchz xrchz added a commit that referenced this issue Jan 27, 2017
@xrchz xrchz Start making RefByte take a flag
To support making both immutable and mutable byte arrays in BVI, so that
String and FromListByte can be compiled away as stubs in BVL-to-BVI
(avoiding new stubs in data-to-word).

For Issue #100
c29b159
@xrchz xrchz added a commit that referenced this issue Jan 31, 2017
@xrchz xrchz Implement and partially verify FromListByte in BVI
For issue #100
dfe1a1e
@xrchz xrchz added a commit that referenced this issue Jan 31, 2017
@xrchz xrchz Finish verifying FromListByte
issue #100
f6ea25c
@xrchz xrchz added a commit that referenced this issue Jan 31, 2017
@xrchz xrchz Fix some proofs in bvi_to_dataProof
issue #100
2351adb
@xrchz xrchz added a commit that referenced this issue Feb 1, 2017
@xrchz xrchz Start updating data_to_wordProps for strings
Unfortunately, it looks like some of the implicit conditions on what a
byte array's header tag can look like are not being met by the scheme
I am trying. It may be necessary to rewrite the equality algorithm
first, to make sense of this.

For issue #100
eaff86c
@xrchz xrchz added a commit that referenced this issue Feb 3, 2017
@xrchz xrchz Continue updating data_to_wordProps
Including with help from Magnus.
The tagging scheme seems workable.

Changed the representation of byte arrays slightly (the last word needs
to be zeroed out beyond the last byte) so we can reuse the word_cmp_loop
test when comparing byte arrays (which compares a whole word a at a
time).

There is cheat in word_eq_thm about using word_cmp_loop. And the
compiler needs to be changed for RefByte.

(issue #100)
57abfd8
@xrchz xrchz added a commit that referenced this issue Feb 6, 2017
@xrchz xrchz Prove cheat in data_to_wordProps
for issue #100
55cfd99
@xrchz xrchz added a commit that referenced this issue Feb 8, 2017
@xrchz xrchz Work in progress updating RefByte_thm
work on evaluate_WriteLastBytes

for issue #100
af19110
@xrchz xrchz added a commit that referenced this issue Feb 9, 2017
@xrchz xrchz Finish RefByte_thm
for issue #100
6088ba8
@xrchz xrchz added a commit that referenced this issue Feb 10, 2017
@xrchz xrchz Fix Equal_code and its proof
for issue #100
dea4a63
@xrchz xrchz closed this in #220 Feb 13, 2017
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment