From e6e3585f8ecf584f608964abbdb456b424c8f07d Mon Sep 17 00:00:00 2001
From: Cynthia Shen <58400192+cyntsh@users.noreply.github.com>
Date: Fri, 6 Aug 2021 17:18:53 -0400
Subject: [PATCH 01/17] Create arithmetic-coding.dx

---
 examples/arithmetic-coding.dx | 84 +++++++++++++++++++++++++++++++++++
 1 file changed, 84 insertions(+)
 create mode 100644 examples/arithmetic-coding.dx

diff --git a/examples/arithmetic-coding.dx b/examples/arithmetic-coding.dx
new file mode 100644
index 000000000..e67c7749a
--- /dev/null
+++ b/examples/arithmetic-coding.dx
@@ -0,0 +1,84 @@
+'### [Arithmetic coding](https://en.wikipedia.org/wiki/Arithmetic_coding)
+
+Alphabet = Fin 26
+Interval = (Float&Float)
+top:Interval = (0.,1.)
+
+def charToIdx (c: Word8) : Int = W8ToI c - W8ToI 'a'
+def idxToChar (i: Int) : Word8 = IToW8 (i + (W8ToI 'a'))
+
+def cumProb (ps: n=>Float) : n=>Float =
+  withState 0.0 \total.
+    for i. if ps.i > 0. 
+      then
+        currTotal = get total
+        newTotal = currTotal + ps.i
+        total := newTotal
+        currTotal
+      else 0.
+
+def getFrequency (str: (Fin l)=>Word8) : Alphabet=>Int =
+  a: Alphabet => Int = zero
+  yieldState a \ref. for i. 
+    i' = (charToIdx str.i)@_
+    ref!i' := (get ref).i' + 1
+
+def getProbability (l: Int) (freq: Alphabet=>Int) : Alphabet=>(Float&Float) =
+  probs = for i. IToF freq.i / IToF l
+  cums = cumProb probs
+  for i. (probs.i, cums.i)
+
+def getUpdateRule (p: Alphabet=>(Float&Float)) : Alphabet=>(Interval->Interval) =
+  for i. 
+    case p.i == (0.,0.) of
+      True -> id
+      False ->
+        \(x, w).
+          x' = x + w*(snd p.i)
+          w' = w*(fst p.i)
+          (x', w')
+
+def subdivide (str: (Fin l)=>Word8) 
+              (rule: Alphabet=>(Interval->Interval)) 
+              (i: (Fin l)) (in: Interval) : Interval =
+  updateInterval = rule.((charToIdx str.i)@_)
+  updateInterval in
+
+def encode (str: (Fin l)=>Word8) (rule: Alphabet=>(Interval->Interval)) : Float =
+  update = subdivide str rule
+  finalInterval = fold top update
+  fst finalInterval + (snd finalInterval)/2.
+
+def findInterval  (l: Int) 
+                  (code: Float) 
+                  (rule: Alphabet=>(Interval->Interval))
+                  (i: (Fin l))
+                  ((str,in): (List Word8 & Interval)) : (List Word8 & Interval) =
+  (letter, in') = boundedIter (size Alphabet) (' ', top) \j.
+    case rule.(j@_) in == in of
+      True -> Continue
+      False ->
+        (x, w) = rule.(j@_) in 
+        case code >= x && code < (x+w) of
+          True -> Done (idxToChar j, (x,w))
+          False -> Continue
+  (str <> AsList 1 [letter], in')
+
+def decode (l: Int) (code: Float) (rule: Alphabet=>(Interval->Interval)) : List Word8 =
+  update = findInterval l code rule
+  initStr: List Word8 = AsList _ []
+  fst $ fold (initStr, top) update
+
+str' = "abbadcabccdd"
+(AsList l str) = str'
+
+p = getProbability l $ getFrequency str
+r = getUpdateRule p
+
+code = encode str r
+code
+
+decoded = decode l code r
+decoded == str'
+
+

From edcf280dbeb65e35eadb72960ad8b4551a115dff Mon Sep 17 00:00:00 2001
From: Cynthia Shen <58400192+cyntsh@users.noreply.github.com>
Date: Fri, 6 Aug 2021 18:44:50 -0400
Subject: [PATCH 02/17] Clean up

---
 examples/arithmetic-coding.dx | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/examples/arithmetic-coding.dx b/examples/arithmetic-coding.dx
index e67c7749a..6d4005e60 100644
--- a/examples/arithmetic-coding.dx
+++ b/examples/arithmetic-coding.dx
@@ -69,6 +69,8 @@ def decode (l: Int) (code: Float) (rule: Alphabet=>(Interval->Interval)) : List
   initStr: List Word8 = AsList _ []
   fst $ fold (initStr, top) update
 
+'Lossless compression on a test string
+
 str' = "abbadcabccdd"
 (AsList l str) = str'
 
@@ -77,8 +79,10 @@ r = getUpdateRule p
 
 code = encode str r
 code
+> 0.081569
 
 decoded = decode l code r
 decoded == str'
+> True
 
 

From 84b5fa8ea28c6e8c423a3a4f55b91c3fe09979d7 Mon Sep 17 00:00:00 2001
From: Cynthia Shen <58400192+cyntsh@users.noreply.github.com>
Date: Tue, 10 Aug 2021 15:53:45 -0400
Subject: [PATCH 03/17] switch from floating point to integer arithmetic

---
 examples/arithmetic-coding.dx | 143 ++++++++++++++++++++++++----------
 1 file changed, 103 insertions(+), 40 deletions(-)

diff --git a/examples/arithmetic-coding.dx b/examples/arithmetic-coding.dx
index 6d4005e60..337277d89 100644
--- a/examples/arithmetic-coding.dx
+++ b/examples/arithmetic-coding.dx
@@ -1,21 +1,36 @@
-'### [Arithmetic coding](https://en.wikipedia.org/wiki/Arithmetic_coding)
+'### Arithmetic coding (WIP)
+A finite-precision variant based on [this](https://web.stanford.edu/class/ee398a/handouts/papers/WittenACM87ArithmCoding.pdf) paper by Ian H. Witten et al.
 
 Alphabet = Fin 26
-Interval = (Float&Float)
-top:Interval = (0.,1.)
+Interval = (Int&Int)
+maxBits = 7
+maxInt = intpow2 maxBits
+half = idiv maxInt 2
 
 def charToIdx (c: Word8) : Int = W8ToI c - W8ToI 'a'
 def idxToChar (i: Int) : Word8 = IToW8 (i + (W8ToI 'a'))
+def intToBin (i: Int) : List Word8 = "WIP"
 
-def cumProb (ps: n=>Float) : n=>Float =
-  withState 0.0 \total.
-    for i. if ps.i > 0. 
+'Statistical modelling
+
+def normalize (freq: Int) (l: Int) (w: Int) : Int = FToI $ IToF freq / IToF l * IToF w
+
+def getCumFreq (fs: Alphabet=>Int) : Alphabet=>Int =
+  withState zero \total.
+    for i. if fs.i /= zero
       then
-        currTotal = get total
-        newTotal = currTotal + ps.i
+        newTotal = get total + fs.i
         total := newTotal
-        currTotal
-      else 0.
+        newTotal
+      else zero
+
+def getIntervals (xs: Alphabet=>Int) : Alphabet=>Interval =
+  withState (0,0) \ref.
+    for i. if xs.i /= zero
+      then
+        ref := ((snd (get ref)), xs.i)
+        get ref
+      else (0,0)
 
 def getFrequency (str: (Fin l)=>Word8) : Alphabet=>Int =
   a: Alphabet => Int = zero
@@ -23,31 +38,74 @@ def getFrequency (str: (Fin l)=>Word8) : Alphabet=>Int =
     i' = (charToIdx str.i)@_
     ref!i' := (get ref).i' + 1
 
-def getProbability (l: Int) (freq: Alphabet=>Int) : Alphabet=>(Float&Float) =
-  probs = for i. IToF freq.i / IToF l
-  cums = cumProb probs
-  for i. (probs.i, cums.i)
-
-def getUpdateRule (p: Alphabet=>(Float&Float)) : Alphabet=>(Interval->Interval) =
-  for i. 
-    case p.i == (0.,0.) of
+def model (str: (Fin l)=>Word8) : Alphabet=>(Interval->Interval) =
+  freq = getFrequency str
+  cumFreq = getCumFreq freq
+  inFreq = getIntervals cumFreq
+  for i.
+    case inFreq.i == (0,0) of
       True -> id
       False ->
-        \(x, w).
-          x' = x + w*(snd p.i)
-          w' = w*(fst p.i)
-          (x', w')
-
-def subdivide (str: (Fin l)=>Word8) 
-              (rule: Alphabet=>(Interval->Interval)) 
-              (i: (Fin l)) (in: Interval) : Interval =
-  updateInterval = rule.((charToIdx str.i)@_)
-  updateInterval in
-
-def encode (str: (Fin l)=>Word8) (rule: Alphabet=>(Interval->Interval)) : Float =
-  update = subdivide str rule
-  finalInterval = fold top update
-  fst finalInterval + (snd finalInterval)/2.
+        (fLow, fHigh) = inFreq.i
+        \(low, high).
+          w = high-low+1
+          low' = low + normalize fLow l w
+          high' = low-1 + normalize fHigh l w
+          (low', high')
+
+'Encoding arithmetic
+
+def appendBit (b: Int) (code: Int) (numBits: Int) : Int =
+  half = intpow2 numBits
+  case b==1 of 
+    True -> %or code half
+    False -> code
+
+appendBit 1 3 3
+
+def intervalRef (ref: Ref h (a&b&c&d)) : Ref h a = %fstRef ref
+def codeRef (ref: Ref h (a&b&c&d)) : Ref h b = %fstRef (%sndRef ref)
+def bitsRef (ref: Ref h (a&b&c&d)) : Ref h c = %fstRef (%sndRef (%sndRef ref))
+def tallyRef (ref: Ref h (a&b&c&d)) : Ref h d = %sndRef (%sndRef (%sndRef ref))
+
+def getInterval (ref: Ref h (a&b&c&d)) : {State h} a = %get (intervalRef ref)
+def getCode (ref: Ref h (a&b&c&d)) : {State h} b = %get (codeRef ref)
+def getBits (ref: Ref h (a&b&c&d)) : {State h} c = %get (bitsRef ref)
+def getTally (ref: Ref h (a&b&c&d)) : {State h} d = %get (tallyRef ref)
+
+def buildCode (str: (Fin l)=>Word8) 
+              (model: Alphabet=>(Interval->Interval)) 
+              (i: (Fin l)) 
+              (params: (Interval&Int&Int&Int)) : (Interval&Int&Int&Int) =
+  yieldState params \ref.
+    (low, high) = model.((charToIdx str.i)@_) (getInterval ref)
+    sharedBits = %xor low high
+    tally' = getTally ref
+    case (%and sharedBits half)/=0 of
+      True -> tallyRef ref := getTally ref + 1
+      False ->
+        yieldState half \mask.
+          boundedIter maxBits (get ref) \_.
+            case (%and sharedBits (get mask))/=0 of
+              True -> Done (get ref)
+              False -> 
+                codeRef ref := case (%and low (get mask))==0 of
+                  True -> appendBit 0 (getCode ref) (getBits ref)
+                  False -> appendBit 1 (getCode ref) (getBits ref)
+                bitsRef ref := getBits ref + 1
+                mask := %shr (get mask) 1
+                Continue
+        bit = select ((%and low half)==0) 0 1
+        for i:(Fin tally').
+          codeRef ref := appendBit bit (getCode ref) (getBits ref)
+          bitsRef ref := getBits ref + 1
+        tallyRef ref := 0
+
+def encode (str: (Fin l)=>Word8) (model: Alphabet=>(Interval->Interval)) : Int =
+  update = buildCode str model
+  initInterval = (0,maxInt-1)
+  result = fold (initInterval,0,0,0) update
+  fst (snd result)
 
 def findInterval  (l: Int) 
                   (code: Float) 
@@ -71,18 +129,23 @@ def decode (l: Int) (code: Float) (rule: Alphabet=>(Interval->Interval)) : List
 
 'Lossless compression on a test string
 
-str' = "abbadcabccdd"
+str' = "abccedac"
 (AsList l str) = str'
-
-p = getProbability l $ getFrequency str
-r = getUpdateRule p
-
-code = encode str r
+initInterval = (0,maxInt-1)
+m = model str
+m.(0@_) initInterval
+m.(1@_) initInterval
+m.(2@_) initInterval
+m.(3@_) initInterval
+m.(4@_) initInterval
+
+code = encode str m
 code
 > 0.081569
 
-decoded = decode l code r
+decoded = decode l code m
 decoded == str'
 > True
 
 
+

From 72b12027faecb7181c7f7866b1460e927b2ad6a7 Mon Sep 17 00:00:00 2001
From: Cynthia Shen <58400192+cyntsh@users.noreply.github.com>
Date: Tue, 10 Aug 2021 21:03:10 -0400
Subject: [PATCH 04/17] Some refactoring

---
 examples/arithmetic-coding.dx | 93 +++++++++++++++++------------------
 1 file changed, 45 insertions(+), 48 deletions(-)

diff --git a/examples/arithmetic-coding.dx b/examples/arithmetic-coding.dx
index 337277d89..4ec834bb0 100644
--- a/examples/arithmetic-coding.dx
+++ b/examples/arithmetic-coding.dx
@@ -1,11 +1,14 @@
-'### Arithmetic coding (WIP)
+'### Arithmetic coding
 A finite-precision variant based on [this](https://web.stanford.edu/class/ee398a/handouts/papers/WittenACM87ArithmCoding.pdf) paper by Ian H. Witten et al.
 
 Alphabet = Fin 26
 Interval = (Int&Int)
+Code = (Int&Int&Int)
 maxBits = 7
 maxInt = intpow2 maxBits
 half = idiv maxInt 2
+fstQuarter = idiv half 2
+thdQuarter = fstQuarter * 3
 
 def charToIdx (c: Word8) : Int = W8ToI c - W8ToI 'a'
 def idxToChar (i: Int) : Word8 = IToW8 (i + (W8ToI 'a'))
@@ -55,63 +58,55 @@ def model (str: (Fin l)=>Word8) : Alphabet=>(Interval->Interval) =
 
 'Encoding arithmetic
 
-def appendBit (b: Int) (code: Int) (numBits: Int) : Int =
+def appendBit (b: Int) ((code, numBits, tally): Code) : Code =
   half = intpow2 numBits
   case b==1 of 
-    True -> %or code half
-    False -> code
+    True -> (%or code half, numBits+tally+1, 0)
+    False -> 
+      (code', numBits') = yieldState (code, numBits+1) \ref. for i:(Fin tally).
+        (code', numBits') = get ref
+        half' = intpow2 numBits'
+        ref := (%or code' half', numBits'+1)
+      (code', numBits', 0)
 
-appendBit 1 3 3
+appendBit 1 (2,5,0)
 
-def intervalRef (ref: Ref h (a&b&c&d)) : Ref h a = %fstRef ref
-def codeRef (ref: Ref h (a&b&c&d)) : Ref h b = %fstRef (%sndRef ref)
-def bitsRef (ref: Ref h (a&b&c&d)) : Ref h c = %fstRef (%sndRef (%sndRef ref))
-def tallyRef (ref: Ref h (a&b&c&d)) : Ref h d = %sndRef (%sndRef (%sndRef ref))
+def intervalRef (ref: Ref h (a&b)) : Ref h a = %fstRef ref
+def codeRef (ref: Ref h (a&b)) : Ref h b = %sndRef ref
+def tallyRef (ref: Ref h (a&(b&c&d))) : Ref h d = %sndRef (%sndRef (%sndRef ref))
 
-def getInterval (ref: Ref h (a&b&c&d)) : {State h} a = %get (intervalRef ref)
-def getCode (ref: Ref h (a&b&c&d)) : {State h} b = %get (codeRef ref)
-def getBits (ref: Ref h (a&b&c&d)) : {State h} c = %get (bitsRef ref)
-def getTally (ref: Ref h (a&b&c&d)) : {State h} d = %get (tallyRef ref)
+def getInterval (ref: Ref h (a&b)) : {State h} a = %get (intervalRef ref)
+def getCode (ref: Ref h (a&b)) : {State h} b = %get (codeRef ref)
+def getTally (ref: Ref h (a&(b&c&d))) : {State h} d = %get (tallyRef ref)
 
-def buildCode (str: (Fin l)=>Word8) 
+def shiftInterval (str: (Fin l)=>Word8) 
               (model: Alphabet=>(Interval->Interval)) 
               (i: (Fin l)) 
-              (params: (Interval&Int&Int&Int)) : (Interval&Int&Int&Int) =
+              (params: (Interval&Code)) : (Interval&Code) =
   yieldState params \ref.
     (low, high) = model.((charToIdx str.i)@_) (getInterval ref)
-    sharedBits = %xor low high
-    tally' = getTally ref
-    case (%and sharedBits half)/=0 of
-      True -> tallyRef ref := getTally ref + 1
-      False ->
-        yieldState half \mask.
-          boundedIter maxBits (get ref) \_.
-            case (%and sharedBits (get mask))/=0 of
-              True -> Done (get ref)
-              False -> 
-                codeRef ref := case (%and low (get mask))==0 of
-                  True -> appendBit 0 (getCode ref) (getBits ref)
-                  False -> appendBit 1 (getCode ref) (getBits ref)
-                bitsRef ref := getBits ref + 1
-                mask := %shr (get mask) 1
-                Continue
-        bit = select ((%and low half)==0) 0 1
-        for i:(Fin tally').
-          codeRef ref := appendBit bit (getCode ref) (getBits ref)
-          bitsRef ref := getBits ref + 1
-        tallyRef ref := 0
-
-def encode (str: (Fin l)=>Word8) (model: Alphabet=>(Interval->Interval)) : Int =
-  update = buildCode str model
+    (low', high') = if high < half
+      then
+        codeRef ref := appendBit 0 (getCode ref)
+        (low, high)
+      else if low > half
+        then
+          codeRef ref := appendBit 1 (getCode ref)
+          (low-half, high-half)
+        else
+          tallyRef ref := getTally ref + 1
+          (low-fstQuarter, high-fstQuarter)
+    intervalRef ref := (2*low', 2*(high'+1)-1) -- high is an open boundary
+
+def encode (str: (Fin l)=>Word8) (model: Alphabet=>(Interval->Interval)) : Code =
+  update = shiftInterval str model
   initInterval = (0,maxInt-1)
-  result = fold (initInterval,0,0,0) update
-  fst (snd result)
+  snd $ fold (initInterval,(0,0,0)) update
 
-def findInterval  (l: Int) 
-                  (code: Float) 
+def findInterval  (l: Int)
                   (rule: Alphabet=>(Interval->Interval))
                   (i: (Fin l))
-                  ((str,in): (List Word8 & Interval)) : (List Word8 & Interval) =
+                  (params: (Interval&Code&List Word8)) : (Interval&Code&List Word8) =
   (letter, in') = boundedIter (size Alphabet) (' ', top) \j.
     case rule.(j@_) in == in of
       True -> Continue
@@ -122,14 +117,15 @@ def findInterval  (l: Int)
           False -> Continue
   (str <> AsList 1 [letter], in')
 
-def decode (l: Int) (code: Float) (rule: Alphabet=>(Interval->Interval)) : List Word8 =
-  update = findInterval l code rule
+def decode (l: Int) (code: Int) (model: Alphabet=>(Interval->Interval)) : List Word8 =
+  update = findInterval l code model
   initStr: List Word8 = AsList _ []
-  fst $ fold (initStr, top) update
+  initInterval = (0,maxInt-1)
+  snd $ fold (initInterval, code, initStr) update
 
 'Lossless compression on a test string
 
-str' = "abccedac"
+str' = "abccedacabccedac"
 (AsList l str) = str'
 initInterval = (0,maxInt-1)
 m = model str
@@ -149,3 +145,4 @@ decoded == str'
 
 
 
+

From 7f6530775ea8fc074f415a86c6a085418bc8f616 Mon Sep 17 00:00:00 2001
From: Cynthia Shen <58400192+cyntsh@users.noreply.github.com>
Date: Tue, 10 Aug 2021 23:49:56 -0400
Subject: [PATCH 05/17] Another WIP

---
 examples/arithmetic-coding.dx | 72 ++++++++++++++++++++---------------
 1 file changed, 42 insertions(+), 30 deletions(-)

diff --git a/examples/arithmetic-coding.dx b/examples/arithmetic-coding.dx
index 4ec834bb0..cb1e4a033 100644
--- a/examples/arithmetic-coding.dx
+++ b/examples/arithmetic-coding.dx
@@ -56,11 +56,11 @@ def model (str: (Fin l)=>Word8) : Alphabet=>(Interval->Interval) =
           high' = low-1 + normalize fHigh l w
           (low', high')
 
-'Encoding arithmetic
+'Coding via integer arithmetic
 
-def appendBit (b: Int) ((code, numBits, tally): Code) : Code =
+def enqueue (bit: Int) ((code, numBits, tally): Code) : Code =
   half = intpow2 numBits
-  case b==1 of 
+  case bit==1 of 
     True -> (%or code half, numBits+tally+1, 0)
     False -> 
       (code', numBits') = yieldState (code, numBits+1) \ref. for i:(Fin tally).
@@ -69,7 +69,16 @@ def appendBit (b: Int) ((code, numBits, tally): Code) : Code =
         ref := (%or code' half', numBits'+1)
       (code', numBits', 0)
 
-appendBit 1 (2,5,0)
+def dequeue ((code, numBits, tally): Code) : (Code&Int) = 
+  ((%shr code 1, numBits-1, tally), %and 1 code)
+
+-- tests
+enqueue 1 (2,5,0)
+> (34, (6, 0))
+dequeue (34,6,0)
+> ((17, (5, 0)), 0)
+dequeue (17,5,0)
+> ((8, (4, 0)), 1)
 
 def intervalRef (ref: Ref h (a&b)) : Ref h a = %fstRef ref
 def codeRef (ref: Ref h (a&b)) : Ref h b = %sndRef ref
@@ -79,53 +88,58 @@ def getInterval (ref: Ref h (a&b)) : {State h} a = %get (intervalRef ref)
 def getCode (ref: Ref h (a&b)) : {State h} b = %get (codeRef ref)
 def getTally (ref: Ref h (a&(b&c&d))) : {State h} d = %get (tallyRef ref)
 
-def shiftInterval (str: (Fin l)=>Word8) 
+def encodeSymbol (str: (Fin l)=>Word8) 
               (model: Alphabet=>(Interval->Interval)) 
               (i: (Fin l)) 
               (params: (Interval&Code)) : (Interval&Code) =
-  yieldState params \ref.
-    (low, high) = model.((charToIdx str.i)@_) (getInterval ref)
+  yieldState params \p.
+    (low, high) = model.((charToIdx str.i)@_) (getInterval p)
     (low', high') = if high < half
       then
-        codeRef ref := appendBit 0 (getCode ref)
+        codeRef p := enqueue 0 (getCode p)
         (low, high)
-      else if low > half
+      else if low >= half
         then
-          codeRef ref := appendBit 1 (getCode ref)
+          codeRef p := enqueue 1 (getCode p)
           (low-half, high-half)
         else
-          tallyRef ref := getTally ref + 1
+          tallyRef p := getTally p + 1
           (low-fstQuarter, high-fstQuarter)
-    intervalRef ref := (2*low', 2*(high'+1)-1) -- high is an open boundary
+    intervalRef p := (2*low', 2*(high'+1)-1)
 
 def encode (str: (Fin l)=>Word8) (model: Alphabet=>(Interval->Interval)) : Code =
-  update = shiftInterval str model
+  update = encodeSymbol str model
   initInterval = (0,maxInt-1)
   snd $ fold (initInterval,(0,0,0)) update
 
-def findInterval  (l: Int)
-                  (rule: Alphabet=>(Interval->Interval))
+def decodeSymbol  (l: Int)
+                  (model: Alphabet=>(Interval->Interval))
                   (i: (Fin l))
-                  (params: (Interval&Code&List Word8)) : (Interval&Code&List Word8) =
-  (letter, in') = boundedIter (size Alphabet) (' ', top) \j.
-    case rule.(j@_) in == in of
-      True -> Continue
-      False ->
-        (x, w) = rule.(j@_) in 
-        case code >= x && code < (x+w) of
-          True -> Done (idxToChar j, (x,w))
-          False -> Continue
-  (str <> AsList 1 [letter], in')
+                  (params: ((Interval&Code)&List Word8)) : ((Interval&Code)&List Word8) =
+  yieldState params \ref.
+    fstRef := yieldState (fst params) \p.
+      (code, bit) = dequeue (getCode p)
+      codeRef p := code
+      interv = getInterval p
+      symbol = boundedIter (size Alphabet) (' ') \j.
+        case model.(j@_) interv == interv of
+          True -> Continue
+          False ->
+            (low, high) = model.(j@_) interv 
+            case code >= x && code < (x+w) of
+              True -> Done (idxToChar j, (x,w))
+              False -> Continue
+      sndRef := (str <> AsList 1 [symbol], in')
 
 def decode (l: Int) (code: Int) (model: Alphabet=>(Interval->Interval)) : List Word8 =
-  update = findInterval l code model
+  update = decodeSymbol l code model
   initStr: List Word8 = AsList _ []
   initInterval = (0,maxInt-1)
-  snd $ fold (initInterval, code, initStr) update
+  snd $ fold ((initInterval, code), initStr) update
 
 'Lossless compression on a test string
 
-str' = "abccedacabccedac"
+str' = "abccedac"
 (AsList l str) = str'
 initInterval = (0,maxInt-1)
 m = model str
@@ -144,5 +158,3 @@ decoded == str'
 > True
 
 
-
-

From 8003af5c37e5c2155960f56cf4eec3f41e2be26c Mon Sep 17 00:00:00 2001
From: Cynthia Shen <58400192+cyntsh@users.noreply.github.com>
Date: Wed, 11 Aug 2021 11:51:53 -0400
Subject: [PATCH 06/17] Encoding algo completed

---
 examples/arithmetic-coding.dx | 58 +++++++++++++++++++++++++----------
 1 file changed, 42 insertions(+), 16 deletions(-)

diff --git a/examples/arithmetic-coding.dx b/examples/arithmetic-coding.dx
index cb1e4a033..a7259d167 100644
--- a/examples/arithmetic-coding.dx
+++ b/examples/arithmetic-coding.dx
@@ -81,10 +81,14 @@ dequeue (17,5,0)
 > ((8, (4, 0)), 1)
 
 def intervalRef (ref: Ref h (a&b)) : Ref h a = %fstRef ref
+def lowRef (ref: Ref h ((a&b)&c)) : Ref h a = %fstRef (%fstRef ref)
+def highRef (ref: Ref h ((a&b)&c)) : Ref h b = %sndRef (%fstRef ref)
 def codeRef (ref: Ref h (a&b)) : Ref h b = %sndRef ref
 def tallyRef (ref: Ref h (a&(b&c&d))) : Ref h d = %sndRef (%sndRef (%sndRef ref))
 
 def getInterval (ref: Ref h (a&b)) : {State h} a = %get (intervalRef ref)
+def getLow (ref: Ref h ((a&b)&c)) : {State h} a = %get (lowRef ref)
+def getHigh (ref: Ref h ((a&b)&c)) : {State h} b = %get (highRef ref)
 def getCode (ref: Ref h (a&b)) : {State h} b = %get (codeRef ref)
 def getTally (ref: Ref h (a&(b&c&d))) : {State h} d = %get (tallyRef ref)
 
@@ -93,19 +97,24 @@ def encodeSymbol (str: (Fin l)=>Word8)
               (i: (Fin l)) 
               (params: (Interval&Code)) : (Interval&Code) =
   yieldState params \p.
-    (low, high) = model.((charToIdx str.i)@_) (getInterval p)
-    (low', high') = if high < half
-      then
-        codeRef p := enqueue 0 (getCode p)
-        (low, high)
-      else if low >= half
-        then
-          codeRef p := enqueue 1 (getCode p)
-          (low-half, high-half)
-        else
-          tallyRef p := getTally p + 1
-          (low-fstQuarter, high-fstQuarter)
-    intervalRef p := (2*low', 2*(high'+1)-1)
+    intervalRef p := model.((charToIdx str.i)@_) (getInterval p)
+    boundedIter maxBits (getInterval p) \_.
+      case getHigh p < half of
+        True ->
+          codeRef p := enqueue 0 (getCode p)
+          intervalRef p := (2*(getLow p), 2*(getHigh p)+1) -- or, 2*(getHigh p + 1)-1
+          Continue
+        False -> case getLow p >= half of
+          True ->
+            codeRef p := enqueue 1 (getCode p)
+            intervalRef p := (2*(getLow p - half), 2*(getHigh p - half)+1)
+            Continue
+          False -> case getHigh p < thdQuarter && getLow p >= fstQuarter of
+            True ->
+              tallyRef p := getTally p + 1
+              intervalRef p := (2*(getLow p - fstQuarter), 2*(getHigh p - fstQuarter)+1)
+              Continue
+            False -> Done (getInterval p)
 
 def encode (str: (Fin l)=>Word8) (model: Alphabet=>(Interval->Interval)) : Code =
   update = encodeSymbol str model
@@ -120,16 +129,32 @@ def decodeSymbol  (l: Int)
     fstRef := yieldState (fst params) \p.
       (code, bit) = dequeue (getCode p)
       codeRef p := code
-      interv = getInterval p
+      interval = getInterval p
       symbol = boundedIter (size Alphabet) (' ') \j.
-        case model.(j@_) interv == interv of
+        case model.(j@_) interval == interval of
           True -> Continue
           False ->
-            (low, high) = model.(j@_) interv 
+            (low, high) = model.(j@_) interval 
             case code >= x && code < (x+w) of
               True -> Done (idxToChar j, (x,w))
               False -> Continue
       sndRef := (str <> AsList 1 [symbol], in')
+  
+
+'yieldState params \ref.
+  (low, high) = model.((charToIdx str.i)@_) (getInterval ref)
+  (low', high') = if high < half
+    then
+      codeRef %fst ref := enqueue 0 (getCode ref)
+      (low, high)
+    else if low >= half
+      then
+        codeRef ref := enqueue 1 (getCode ref)
+        (low-half, high-half)
+      else
+        tallyRef ref := getTally ref + 1
+        (low-fstQuarter, high-fstQuarter)
+  intervalRef ref := (2*low', 2*(high'+1)-1)
 
 def decode (l: Int) (code: Int) (model: Alphabet=>(Interval->Interval)) : List Word8 =
   update = decodeSymbol l code model
@@ -158,3 +183,4 @@ decoded == str'
 > True
 
 
+

From 3c934e7f8ce208ef03483674950f2cc35ee49959 Mon Sep 17 00:00:00 2001
From: Cynthia Shen <58400192+cyntsh@users.noreply.github.com>
Date: Wed, 11 Aug 2021 15:03:38 -0400
Subject: [PATCH 07/17] First working version. ish.

---
 examples/arithmetic-coding.dx | 136 ++++++++++++++++++----------------
 1 file changed, 72 insertions(+), 64 deletions(-)

diff --git a/examples/arithmetic-coding.dx b/examples/arithmetic-coding.dx
index a7259d167..f82ba16d5 100644
--- a/examples/arithmetic-coding.dx
+++ b/examples/arithmetic-coding.dx
@@ -4,6 +4,7 @@ A finite-precision variant based on [this](https://web.stanford.edu/class/ee398a
 Alphabet = Fin 26
 Interval = (Int&Int)
 Code = (Int&Int&Int)
+Buffer = Int
 maxBits = 7
 maxInt = intpow2 maxBits
 half = idiv maxInt 2
@@ -16,7 +17,8 @@ def intToBin (i: Int) : List Word8 = "WIP"
 
 'Statistical modelling
 
-def normalize (freq: Int) (l: Int) (w: Int) : Int = FToI $ IToF freq / IToF l * IToF w
+def norm (freq: Int) (l: Int) (w: Int) : Int = FToI $ IToF freq / IToF l * IToF w
+def inverseNorm (norm: Int) (l: Int) (w: Int) : Int = FToI $ IToF norm / IToF w * IToF l
 
 def getCumFreq (fs: Alphabet=>Int) : Alphabet=>Int =
   withState zero \total.
@@ -52,8 +54,8 @@ def model (str: (Fin l)=>Word8) : Alphabet=>(Interval->Interval) =
         (fLow, fHigh) = inFreq.i
         \(low, high).
           w = high-low+1
-          low' = low + normalize fLow l w
-          high' = low-1 + normalize fHigh l w
+          low' = low + norm fLow l w
+          high' = low-1 + norm fHigh l w
           (low', high')
 
 'Coding via integer arithmetic
@@ -69,52 +71,49 @@ def enqueue (bit: Int) ((code, numBits, tally): Code) : Code =
         ref := (%or code' half', numBits'+1)
       (code', numBits', 0)
 
-def dequeue ((code, numBits, tally): Code) : (Code&Int) = 
-  ((%shr code 1, numBits-1, tally), %and 1 code)
+def dequeue (code: Int) : (Int&Int) = (%shr code 1, %and 1 code)
 
 -- tests
 enqueue 1 (2,5,0)
 > (34, (6, 0))
-dequeue (34,6,0)
-> ((17, (5, 0)), 0)
-dequeue (17,5,0)
-> ((8, (4, 0)), 1)
+dequeue 34
+> (17, 0)
+dequeue 17
+> (8, 1)
 
+-- Helper functions for stateful computations on nested pairs. 
+-- Alternatively can use records, but it's not supported for state effects yet.
 def intervalRef (ref: Ref h (a&b)) : Ref h a = %fstRef ref
 def lowRef (ref: Ref h ((a&b)&c)) : Ref h a = %fstRef (%fstRef ref)
 def highRef (ref: Ref h ((a&b)&c)) : Ref h b = %sndRef (%fstRef ref)
 def codeRef (ref: Ref h (a&b)) : Ref h b = %sndRef ref
 def tallyRef (ref: Ref h (a&(b&c&d))) : Ref h d = %sndRef (%sndRef (%sndRef ref))
-
-def getInterval (ref: Ref h (a&b)) : {State h} a = %get (intervalRef ref)
-def getLow (ref: Ref h ((a&b)&c)) : {State h} a = %get (lowRef ref)
-def getHigh (ref: Ref h ((a&b)&c)) : {State h} b = %get (highRef ref)
-def getCode (ref: Ref h (a&b)) : {State h} b = %get (codeRef ref)
-def getTally (ref: Ref h (a&(b&c&d))) : {State h} d = %get (tallyRef ref)
+def bufferRef (ref: Ref h ((a&b)&c&d)) : Ref h c = %fstRef (%sndRef ref)
+def strRef (ref: Ref h ((a&b)&c&d)) : Ref h d = %sndRef (%sndRef ref)
 
 def encodeSymbol (str: (Fin l)=>Word8) 
               (model: Alphabet=>(Interval->Interval)) 
               (i: (Fin l)) 
               (params: (Interval&Code)) : (Interval&Code) =
   yieldState params \p.
-    intervalRef p := model.((charToIdx str.i)@_) (getInterval p)
-    boundedIter maxBits (getInterval p) \_.
-      case getHigh p < half of
+    intervalRef p := model.((charToIdx str.i)@_) (get (intervalRef p))
+    boundedIter maxBits (get (intervalRef p)) \_.
+      case get (highRef p) < half of
         True ->
-          codeRef p := enqueue 0 (getCode p)
-          intervalRef p := (2*(getLow p), 2*(getHigh p)+1) -- or, 2*(getHigh p + 1)-1
+          codeRef p := enqueue 0 (get (codeRef p))
+          intervalRef p := (2*(get (lowRef p)), 2*(get (highRef p))+1)
           Continue
-        False -> case getLow p >= half of
+        False -> case get (lowRef p) >= half of
           True ->
-            codeRef p := enqueue 1 (getCode p)
-            intervalRef p := (2*(getLow p - half), 2*(getHigh p - half)+1)
+            codeRef p := enqueue 1 (get (codeRef p))
+            intervalRef p := (2*(get (lowRef p) - half), 2*(get (highRef p) - half)+1)
             Continue
-          False -> case getHigh p < thdQuarter && getLow p >= fstQuarter of
+          False -> case get (highRef p) < thdQuarter && get (lowRef p) >= fstQuarter of
             True ->
-              tallyRef p := getTally p + 1
-              intervalRef p := (2*(getLow p - fstQuarter), 2*(getHigh p - fstQuarter)+1)
+              tallyRef p := get (tallyRef p) + 1
+              intervalRef p := (2*(get (lowRef p) - fstQuarter), 2*(get (highRef p) - fstQuarter)+1)
               Continue
-            False -> Done (getInterval p)
+            False -> Done (get (intervalRef p))
 
 def encode (str: (Fin l)=>Word8) (model: Alphabet=>(Interval->Interval)) : Code =
   update = encodeSymbol str model
@@ -124,43 +123,54 @@ def encode (str: (Fin l)=>Word8) (model: Alphabet=>(Interval->Interval)) : Code
 def decodeSymbol  (l: Int)
                   (model: Alphabet=>(Interval->Interval))
                   (i: (Fin l))
-                  (params: ((Interval&Code)&List Word8)) : ((Interval&Code)&List Word8) =
-  yieldState params \ref.
-    fstRef := yieldState (fst params) \p.
-      (code, bit) = dequeue (getCode p)
-      codeRef p := code
-      interval = getInterval p
-      symbol = boundedIter (size Alphabet) (' ') \j.
+                  (params: ((Interval&Int)&Buffer&List Word8)) : ((Interval&Int)&Buffer&List Word8) =
+  yieldState params \p'.
+    fstRef p' := yieldState (fst params) \p.
+      interval = get (intervalRef p)
+      buff = get (bufferRef p')
+      (symbol, interval') = boundedIter (size Alphabet) (' ',(0,0)) \j.
         case model.(j@_) interval == interval of
           True -> Continue
           False ->
-            (low, high) = model.(j@_) interval 
-            case code >= x && code < (x+w) of
-              True -> Done (idxToChar j, (x,w))
+            (low, high) = model.(j@_) interval
+            case buff >= low && buff < high of
+              True -> Done (idxToChar j, (low,high))
               False -> Continue
-      sndRef := (str <> AsList 1 [symbol], in')
-  
-
-'yieldState params \ref.
-  (low, high) = model.((charToIdx str.i)@_) (getInterval ref)
-  (low', high') = if high < half
-    then
-      codeRef %fst ref := enqueue 0 (getCode ref)
-      (low, high)
-    else if low >= half
-      then
-        codeRef ref := enqueue 1 (getCode ref)
-        (low-half, high-half)
-      else
-        tallyRef ref := getTally ref + 1
-        (low-fstQuarter, high-fstQuarter)
-  intervalRef ref := (2*low', 2*(high'+1)-1)
+      strRef p' := get (strRef p') <> AsList 1 [symbol]
+      intervalRef p := interval'
+      (code, bit) = dequeue (get (codeRef p))
+      codeRef p := code
+      boundedIter maxBits (get (intervalRef p)) \_.
+        (code, bit) = dequeue (get (codeRef p))
+        case get (highRef p) < half of
+          True ->
+            codeRef p := code
+            bufferRef p' := 2*(get (bufferRef p')) + bit
+            intervalRef p := (2*(get (lowRef p)), 2*(get (highRef p))+1)
+            Continue
+          False -> case get (lowRef p) >= half of
+            True ->
+              codeRef p := code
+              bufferRef p' := 2*(get (bufferRef p') - half) + bit
+              intervalRef p := (2*(get (lowRef p) - half), 2*(get (highRef p) - half)+1)
+              Continue
+            False -> case get (highRef p) < thdQuarter && get (lowRef p) >= fstQuarter of
+              True ->
+                codeRef p := code
+                bufferRef p' := 2*(get (bufferRef p') - fstQuarter) + bit
+                intervalRef p := (2*(get (lowRef p) - fstQuarter), 2*(get (highRef p) - fstQuarter)+1)
+                Continue
+              False -> Done (get (intervalRef p))
 
 def decode (l: Int) (code: Int) (model: Alphabet=>(Interval->Interval)) : List Word8 =
-  update = decodeSymbol l code model
+  update = decodeSymbol l model
   initStr: List Word8 = AsList _ []
   initInterval = (0,maxInt-1)
-  snd $ fold ((initInterval, code), initStr) update
+  (initBuffer, initCode) = yieldState (0,code) \ref. for i:(Fin maxBits). 
+    (code', bit) = dequeue (get (sndRef ref))
+    fstRef ref := 2*(get (fstRef ref))+bit
+    sndRef ref := code'
+  snd $ snd $ fold ((initInterval, initCode), initBuffer, initStr) update
 
 'Lossless compression on a test string
 
@@ -168,19 +178,17 @@ str' = "abccedac"
 (AsList l str) = str'
 initInterval = (0,maxInt-1)
 m = model str
-m.(0@_) initInterval
-m.(1@_) initInterval
-m.(2@_) initInterval
-m.(3@_) initInterval
-m.(4@_) initInterval
 
-code = encode str m
+code = fst $ encode str m
 code
-> 0.081569
+> 60584
 
 decoded = decode l code m
+decoded
+> (AsList 8 "abccadae")
 decoded == str'
-> True
+> False
+
 
 
 

From d616f7ff98c7a830c692f07436b4c8c2f155017b Mon Sep 17 00:00:00 2001
From: Cynthia Shen <58400192+cyntsh@users.noreply.github.com>
Date: Wed, 11 Aug 2021 17:53:58 -0400
Subject: [PATCH 08/17] Utter refactor

---
 examples/arithmetic-coding.dx | 187 +++++++++++++++++-----------------
 1 file changed, 95 insertions(+), 92 deletions(-)

diff --git a/examples/arithmetic-coding.dx b/examples/arithmetic-coding.dx
index f82ba16d5..63e8a48cb 100644
--- a/examples/arithmetic-coding.dx
+++ b/examples/arithmetic-coding.dx
@@ -1,4 +1,4 @@
-'### Arithmetic coding
+'## Arithmetic coding
 A finite-precision variant based on [this](https://web.stanford.edu/class/ee398a/handouts/papers/WittenACM87ArithmCoding.pdf) paper by Ian H. Witten et al.
 
 Alphabet = Fin 26
@@ -13,9 +13,8 @@ thdQuarter = fstQuarter * 3
 
 def charToIdx (c: Word8) : Int = W8ToI c - W8ToI 'a'
 def idxToChar (i: Int) : Word8 = IToW8 (i + (W8ToI 'a'))
-def intToBin (i: Int) : List Word8 = "WIP"
 
-'Statistical modelling
+'### Statistical modelling
 
 def norm (freq: Int) (l: Int) (w: Int) : Int = FToI $ IToF freq / IToF l * IToF w
 def inverseNorm (norm: Int) (l: Int) (w: Int) : Int = FToI $ IToF norm / IToF w * IToF l
@@ -58,7 +57,7 @@ def model (str: (Fin l)=>Word8) : Alphabet=>(Interval->Interval) =
           high' = low-1 + norm fHigh l w
           (low', high')
 
-'Coding via integer arithmetic
+'### Integer arithmetic
 
 def enqueue (bit: Int) ((code, numBits, tally): Code) : Code =
   half = intpow2 numBits
@@ -71,124 +70,128 @@ def enqueue (bit: Int) ((code, numBits, tally): Code) : Code =
         ref := (%or code' half', numBits'+1)
       (code', numBits', 0)
 
-def dequeue (code: Int) : (Int&Int) = (%shr code 1, %and 1 code)
-
--- tests
-enqueue 1 (2,5,0)
-> (34, (6, 0))
-dequeue 34
-> (17, 0)
-dequeue 17
-> (8, 1)
-
--- Helper functions for stateful computations on nested pairs. 
--- Alternatively can use records, but it's not supported for state effects yet.
-def intervalRef (ref: Ref h (a&b)) : Ref h a = %fstRef ref
-def lowRef (ref: Ref h ((a&b)&c)) : Ref h a = %fstRef (%fstRef ref)
-def highRef (ref: Ref h ((a&b)&c)) : Ref h b = %sndRef (%fstRef ref)
-def codeRef (ref: Ref h (a&b)) : Ref h b = %sndRef ref
-def tallyRef (ref: Ref h (a&(b&c&d))) : Ref h d = %sndRef (%sndRef (%sndRef ref))
-def bufferRef (ref: Ref h ((a&b)&c&d)) : Ref h c = %fstRef (%sndRef ref)
-def strRef (ref: Ref h ((a&b)&c&d)) : Ref h d = %sndRef (%sndRef ref)
+def dequeue ((code, buffer, tally): Code) : Code = (%shr code (1+tally), 2*buffer+%and 1 code, 0)
+
+'### Scaling functions
+
+def encodeInterval ((low, high): Interval) (code: Code) : (Int&Int&Code&(IterResult Int)) =
+  case high < half of
+    True ->
+      (2*low,
+       2*high+1,
+       enqueue 0 code,
+       Continue)
+    False -> case low >= half of
+      True ->
+        (2*(low - half),
+         2*(high - half)+1,
+         enqueue 1 code,
+         Continue)
+      False -> case high < thdQuarter && low >= fstQuarter of
+        True ->
+          (2*(low - fstQuarter), 
+           2*(high - fstQuarter)+1, 
+           (fst code, fst (snd code), snd (snd code) + 1), 
+           Continue)
+        False -> (low, high, code, Done 0)
 
 def encodeSymbol (str: (Fin l)=>Word8) 
               (model: Alphabet=>(Interval->Interval)) 
               (i: (Fin l)) 
               (params: (Interval&Code)) : (Interval&Code) =
   yieldState params \p.
-    intervalRef p := model.((charToIdx str.i)@_) (get (intervalRef p))
-    boundedIter maxBits (get (intervalRef p)) \_.
-      case get (highRef p) < half of
+    intervalRef = fstRef p
+    codeRef = sndRef p
+    intervalRef := model.((charToIdx str.i)@_) (get intervalRef)
+    boundedIter maxBits 0 \_.
+      (low, high, code, result) = encodeInterval (get intervalRef) (get codeRef)
+      intervalRef := (low, high)
+      codeRef := code
+      result
+
+def findInterval (interval: Interval) (buff: Int) (model: Alphabet=>(Interval->Interval)) : (Word8&Interval)=
+  boundedIter (size Alphabet) (' ',(0,0)) \j.
+    case model.(j@_) interval == interval of
+      True -> Continue
+      False ->
+        (low, high) = model.(j@_) interval
+        case buff >= low && buff < high of
+          True -> Done (idxToChar j, (low,high))
+          False -> Continue
+
+def decodeInterval ((low, high): Interval) (code: Code) : (Int&Int&Code&(IterResult Int)) =
+  case high < half of
+    True ->
+      (2*low,
+       2*high+1,
+       dequeue code,
+       Continue)
+    False -> case low >= half of
+      True ->
+        (x, buffer, z) = code
+        (2*(low-half),
+         2*(high-half)+1,
+         dequeue (x, buffer-half, z),
+         Continue)
+      False -> case high < thdQuarter && low >= fstQuarter of
         True ->
-          codeRef p := enqueue 0 (get (codeRef p))
-          intervalRef p := (2*(get (lowRef p)), 2*(get (highRef p))+1)
-          Continue
-        False -> case get (lowRef p) >= half of
-          True ->
-            codeRef p := enqueue 1 (get (codeRef p))
-            intervalRef p := (2*(get (lowRef p) - half), 2*(get (highRef p) - half)+1)
-            Continue
-          False -> case get (highRef p) < thdQuarter && get (lowRef p) >= fstQuarter of
-            True ->
-              tallyRef p := get (tallyRef p) + 1
-              intervalRef p := (2*(get (lowRef p) - fstQuarter), 2*(get (highRef p) - fstQuarter)+1)
-              Continue
-            False -> Done (get (intervalRef p))
-
-def encode (str: (Fin l)=>Word8) (model: Alphabet=>(Interval->Interval)) : Code =
-  update = encodeSymbol str model
-  initInterval = (0,maxInt-1)
-  snd $ fold (initInterval,(0,0,0)) update
+          (x, buffer, z) = code
+          (2*(low-fstQuarter),
+           2*(high-fstQuarter)+1,
+           dequeue (x, buffer-fstQuarter, z),
+           Continue)
+        False -> (low, high, code, Done 0)
 
 def decodeSymbol  (l: Int)
                   (model: Alphabet=>(Interval->Interval))
                   (i: (Fin l))
-                  (params: ((Interval&Int)&Buffer&List Word8)) : ((Interval&Int)&Buffer&List Word8) =
-  yieldState params \p'.
-    fstRef p' := yieldState (fst params) \p.
-      interval = get (intervalRef p)
-      buff = get (bufferRef p')
-      (symbol, interval') = boundedIter (size Alphabet) (' ',(0,0)) \j.
-        case model.(j@_) interval == interval of
-          True -> Continue
-          False ->
-            (low, high) = model.(j@_) interval
-            case buff >= low && buff < high of
-              True -> Done (idxToChar j, (low,high))
-              False -> Continue
-      strRef p' := get (strRef p') <> AsList 1 [symbol]
-      intervalRef p := interval'
-      (code, bit) = dequeue (get (codeRef p))
-      codeRef p := code
-      boundedIter maxBits (get (intervalRef p)) \_.
-        (code, bit) = dequeue (get (codeRef p))
-        case get (highRef p) < half of
-          True ->
-            codeRef p := code
-            bufferRef p' := 2*(get (bufferRef p')) + bit
-            intervalRef p := (2*(get (lowRef p)), 2*(get (highRef p))+1)
-            Continue
-          False -> case get (lowRef p) >= half of
-            True ->
-              codeRef p := code
-              bufferRef p' := 2*(get (bufferRef p') - half) + bit
-              intervalRef p := (2*(get (lowRef p) - half), 2*(get (highRef p) - half)+1)
-              Continue
-            False -> case get (highRef p) < thdQuarter && get (lowRef p) >= fstQuarter of
-              True ->
-                codeRef p := code
-                bufferRef p' := 2*(get (bufferRef p') - fstQuarter) + bit
-                intervalRef p := (2*(get (lowRef p) - fstQuarter), 2*(get (highRef p) - fstQuarter)+1)
-                Continue
-              False -> Done (get (intervalRef p))
+                  (params: (Interval&Code&List Word8)) : (Interval&Code&List Word8) =
+  yieldState params \p.
+    intervalRef = fstRef p
+    codeRef = fstRef (sndRef p)
+    strRef = sndRef (sndRef p)
+    bufferRef = fstRef (sndRef codeRef)
+    (symbol, interval) = findInterval (get intervalRef) (get bufferRef) model
+    strRef := get strRef <> AsList 1 [symbol]
+    intervalRef := interval
+    boundedIter maxBits 0 \_.
+      (low, high, code, result) = decodeInterval (get intervalRef) (get codeRef)
+      intervalRef := (low, high)
+      codeRef := code 
+      result
+
+'### Coding interface
+
+def encode (str: (Fin l)=>Word8) (model: Alphabet=>(Interval->Interval)) : Int =
+  update = encodeSymbol str model
+  initInterval = (0,maxInt-1)
+  fst $ snd $ fold (initInterval,(0,0,0)) update
 
 def decode (l: Int) (code: Int) (model: Alphabet=>(Interval->Interval)) : List Word8 =
   update = decodeSymbol l model
   initStr: List Word8 = AsList _ []
   initInterval = (0,maxInt-1)
-  (initBuffer, initCode) = yieldState (0,code) \ref. for i:(Fin maxBits). 
-    (code', bit) = dequeue (get (sndRef ref))
-    fstRef ref := 2*(get (fstRef ref))+bit
-    sndRef ref := code'
-  snd $ snd $ fold ((initInterval, initCode), initBuffer, initStr) update
+  initCode' = (code, 0, 0)
+  initCode = yieldState initCode' \ref. for i:(Fin maxBits). ref := dequeue (get ref)
+  snd $ snd $ fold (initInterval, initCode, initStr) update
 
-'Lossless compression on a test string
+'### Demo: Lossless compression on a test string
 
 str' = "abccedac"
 (AsList l str) = str'
-initInterval = (0,maxInt-1)
 m = model str
 
-code = fst $ encode str m
+code = encode str m
 code
 > 60584
 
 decoded = decode l code m
 decoded
-> (AsList 8 "abccadae")
+> (AsList 8 "abccedaa")
 decoded == str'
 > False
 
 
 
 
+

From 77341c96fd02f800503a0778ffdda187ec4f787d Mon Sep 17 00:00:00 2001
From: Cynthia Shen <58400192+cyntsh@users.noreply.github.com>
Date: Thu, 12 Aug 2021 15:40:48 -0400
Subject: [PATCH 09/17] Deal with enqueue overflow

---
 examples/arithmetic-coding.dx | 133 ++++++++++++++++++++++++----------
 1 file changed, 96 insertions(+), 37 deletions(-)

diff --git a/examples/arithmetic-coding.dx b/examples/arithmetic-coding.dx
index 63e8a48cb..d6270556c 100644
--- a/examples/arithmetic-coding.dx
+++ b/examples/arithmetic-coding.dx
@@ -3,11 +3,11 @@ A finite-precision variant based on [this](https://web.stanford.edu/class/ee398a
 
 Alphabet = Fin 26
 Interval = (Int&Int)
-Code = (Int&Int&Int)
-Buffer = Int
-maxBits = 7
-maxInt = intpow2 maxBits
-half = idiv maxInt 2
+Code = ((List Int)&Int&Int)
+maxBits = 31
+precision = 7
+top = intpow2 precision
+half = idiv top 2
 fstQuarter = idiv half 2
 thdQuarter = fstQuarter * 3
 
@@ -40,7 +40,7 @@ def getFrequency (str: (Fin l)=>Word8) : Alphabet=>Int =
   a: Alphabet => Int = zero
   yieldState a \ref. for i. 
     i' = (charToIdx str.i)@_
-    ref!i' := (get ref).i' + 1
+    ref!i' := get ref!i' + 1
 
 def model (str: (Fin l)=>Word8) : Alphabet=>(Interval->Interval) =
   freq = getFrequency str
@@ -59,18 +59,73 @@ def model (str: (Fin l)=>Word8) : Alphabet=>(Interval->Interval) =
 
 '### Integer arithmetic
 
-def enqueue (bit: Int) ((code, numBits, tally): Code) : Code =
-  half = intpow2 numBits
-  case bit==1 of 
-    True -> (%or code half, numBits+tally+1, 0)
-    False -> 
-      (code', numBits') = yieldState (code, numBits+1) \ref. for i:(Fin tally).
-        (code', numBits') = get ref
-        half' = intpow2 numBits'
-        ref := (%or code' half', numBits'+1)
-      (code', numBits', 0)
+def overflowing (numBits: Int) : Bool = 
+  mod numBits maxBits == 0 && numBits > maxBits
 
-def dequeue ((code, buffer, tally): Code) : Code = (%shr code (1+tally), 2*buffer+%and 1 code, 0)
+def existsOverflow (numBits: Int) : Bool =
+  mod numBits maxBits > 0 && numBits > maxBits
+
+def selectStream (numBits: Int) (code: Ref h Int) 
+                 (overflow: Ref h Int) : {State h} Unit =
+  numBits' = mod numBits maxBits
+  bitMask = intpow2 numBits'
+  case (numBits < maxBits) of 
+    True -> code := %or (get code) bitMask
+    False -> overflow := %or (get overflow) bitMask
+
+def enqueue (bit: Int) ((codeLst, numBits, tally): Code) : Code =
+  (AsList numInts intArr) = codeLst
+  code = intArr.((numInts-1)@_)
+  overflow = (0, AsList 0 [])
+
+  (code', overflow', numBits') = yieldState (code, overflow, numBits) \ref.
+    codeRef = fstRef ref
+    overflowRef = fstRef (fstRef (sndRef ref))
+    lstOverflowRef = sndRef (fstRef (sndRef ref))
+    bitsRef = sndRef (sndRef ref)
+
+    if bit==1 then selectStream (get bitsRef) codeRef overflowRef
+    bitsRef := (get bitsRef)+1
+    if overflowing (get bitsRef) then 
+      lstOverflowRef := (get lstOverflowRef) <> (AsList 1 [get overflowRef])
+      overflowRef := 0
+
+    for i:(Fin tally).
+      if bit==0 then selectStream (get bitsRef) codeRef overflowRef
+      bitsRef := (get bitsRef)+1
+      if overflowing (get bitsRef) then 
+        lstOverflowRef := (get lstOverflowRef) <> (AsList 1 [get overflowRef])
+        overflowRef := 0
+
+    if existsOverflow (get bitsRef) then
+      lstOverflowRef := (get lstOverflowRef) <> (AsList 1 [get overflowRef])
+
+  intArr' = yieldState intArr \arr. arr!((numInts-1)@_) := code'
+  codeLst' = (AsList numInts intArr') <> (snd overflow')
+  (codeLst', mod numBits' maxBits, 0)
+
+def dequeue ((codeLst, bitPos, tally): Code) (buffer: Int): (Code&Int) = 
+  (AsList numInts intArr) = codeLst
+  codePos = idiv (bitPos) maxBits -- initial bitPos is 1
+  code = intArr.(codePos@_)
+  bit = %and 1 code
+
+  (intArr', buffer', bitPos') = yieldState (intArr, 2*buffer+bit, bitPos) \ref.
+    arrRef = fstRef ref
+    bufferRef = fstRef (sndRef ref)
+    posRef = sndRef (sndRef ref) 
+    arrRef!(codePos@_) := %shr code 1
+
+    for i:(Fin tally).
+      codePos = idiv (get posRef) maxBits
+      code = get arrRef!(codePos@_)
+      bit = %and 1 code
+      bufferRef := 2*(get bufferRef) + bit
+      arrRef!(codePos@_) := %shr code 1
+      posRef := (get posRef) + 1
+
+  codeLst' = AsList numInts intArr'
+  ((codeLst', bitPos', 0), buffer')
 
 '### Scaling functions
 
@@ -103,23 +158,25 @@ def encodeSymbol (str: (Fin l)=>Word8)
     intervalRef = fstRef p
     codeRef = sndRef p
     intervalRef := model.((charToIdx str.i)@_) (get intervalRef)
-    boundedIter maxBits 0 \_.
+    boundedIter precision 0 \_.
       (low, high, code, result) = encodeInterval (get intervalRef) (get codeRef)
       intervalRef := (low, high)
       codeRef := code
       result
 
-def findInterval (interval: Interval) (buff: Int) (model: Alphabet=>(Interval->Interval)) : (Word8&Interval)=
+def findInterval (interval: Interval) (buffer: Int) 
+                 (model: Alphabet=>(Interval->Interval)) : (Word8&Interval)=
   boundedIter (size Alphabet) (' ',(0,0)) \j.
     case model.(j@_) interval == interval of
       True -> Continue
       False ->
         (low, high) = model.(j@_) interval
-        case buff >= low && buff < high of
+        case buffer >= low && buffer < high of
           True -> Done (idxToChar j, (low,high))
           False -> Continue
 
-def decodeInterval ((low, high): Interval) (code: Code) : (Int&Int&Code&(IterResult Int)) =
+def decodeInterval ((low, high): Interval) 
+                   (code: Code) (buffer: Int) : (Int&Int&Code&Int&(IterResult Int)) =
   case high < half of
     True ->
       (2*low,
@@ -145,16 +202,16 @@ def decodeInterval ((low, high): Interval) (code: Code) : (Int&Int&Code&(IterRes
 def decodeSymbol  (l: Int)
                   (model: Alphabet=>(Interval->Interval))
                   (i: (Fin l))
-                  (params: (Interval&Code&List Word8)) : (Interval&Code&List Word8) =
+                  (params: (Interval&Code&Int&List Word8)) : (Interval&Code&Int&List Word8) =
   yieldState params \p.
     intervalRef = fstRef p
     codeRef = fstRef (sndRef p)
-    strRef = sndRef (sndRef p)
-    bufferRef = fstRef (sndRef codeRef)
+    strRef = sndRef (sndRef (sndRef p))
+    bufferRef = fstRef (sndRef (sndRef p))
     (symbol, interval) = findInterval (get intervalRef) (get bufferRef) model
     strRef := get strRef <> AsList 1 [symbol]
     intervalRef := interval
-    boundedIter maxBits 0 \_.
+    boundedIter precision 0 \_.
       (low, high, code, result) = decodeInterval (get intervalRef) (get codeRef)
       intervalRef := (low, high)
       codeRef := code 
@@ -162,34 +219,36 @@ def decodeSymbol  (l: Int)
 
 '### Coding interface
 
-def encode (str: (Fin l)=>Word8) (model: Alphabet=>(Interval->Interval)) : Int =
+def encode (str: (Fin l)=>Word8) (model: Alphabet=>(Interval->Interval)) : List Int =
   update = encodeSymbol str model
-  initInterval = (0,maxInt-1)
-  fst $ snd $ fold (initInterval,(0,0,0)) update
+  initInterval = (0,top-1)
+  fst $ snd $ fold (initInterval,(AsList 1 [0],0,0)) update
 
-def decode (l: Int) (code: Int) (model: Alphabet=>(Interval->Interval)) : List Word8 =
+def decode (l: Int) (codeLst: List Int) (model: Alphabet=>(Interval->Interval)) : List Word8 =
   update = decodeSymbol l model
   initStr: List Word8 = AsList _ []
-  initInterval = (0,maxInt-1)
-  initCode' = (code, 0, 0)
-  initCode = yieldState initCode' \ref. for i:(Fin maxBits). ref := dequeue (get ref)
-  snd $ snd $ fold (initInterval, initCode, initStr) update
+  initInterval = (0,top-1)
+  initCode' = (codeLst, 1, 0)
+  initCode = yieldState initCode' \ref. for i:(Fin precision). ref := dequeue (get ref)
+  snd $ snd $ fold (initInterval, initCode, 0, initStr) update
 
 '### Demo: Lossless compression on a test string
 
-str' = "abccedac"
+str' = "edacg"
 (AsList l str) = str'
 m = model str
 
 code = encode str m
 code
-> 60584
+> (AsList 1 [821])
 
 decoded = decode l code m
 decoded
-> (AsList 8 "abccedaa")
+> 
 decoded == str'
-> False
+> 
+
+
 
 
 

From 31d0b37fd0f85e645e31bdb3e3ef216fd326908b Mon Sep 17 00:00:00 2001
From: Cynthia Shen <58400192+cyntsh@users.noreply.github.com>
Date: Thu, 12 Aug 2021 19:06:17 -0400
Subject: [PATCH 10/17] List of codes for dequeue + minor bugs

---
 examples/arithmetic-coding.dx | 62 +++++++++++++++++------------------
 1 file changed, 31 insertions(+), 31 deletions(-)

diff --git a/examples/arithmetic-coding.dx b/examples/arithmetic-coding.dx
index d6270556c..deb698d40 100644
--- a/examples/arithmetic-coding.dx
+++ b/examples/arithmetic-coding.dx
@@ -108,24 +108,10 @@ def dequeue ((codeLst, bitPos, tally): Code) (buffer: Int): (Code&Int) =
   (AsList numInts intArr) = codeLst
   codePos = idiv (bitPos) maxBits -- initial bitPos is 1
   code = intArr.(codePos@_)
-  bit = %and 1 code
-
-  (intArr', buffer', bitPos') = yieldState (intArr, 2*buffer+bit, bitPos) \ref.
-    arrRef = fstRef ref
-    bufferRef = fstRef (sndRef ref)
-    posRef = sndRef (sndRef ref) 
-    arrRef!(codePos@_) := %shr code 1
-
-    for i:(Fin tally).
-      codePos = idiv (get posRef) maxBits
-      code = get arrRef!(codePos@_)
-      bit = %and 1 code
-      bufferRef := 2*(get bufferRef) + bit
-      arrRef!(codePos@_) := %shr code 1
-      posRef := (get posRef) + 1
-
+  buffer' = 2*buffer + %and 1 code
+  intArr' = yieldState intArr \arr. arr!(codePos@_) := %shr code 1
   codeLst' = AsList numInts intArr'
-  ((codeLst', bitPos', 0), buffer')
+  ((codeLst', bitPos+1, 0), buffer')
 
 '### Scaling functions
 
@@ -179,26 +165,31 @@ def decodeInterval ((low, high): Interval)
                    (code: Code) (buffer: Int) : (Int&Int&Code&Int&(IterResult Int)) =
   case high < half of
     True ->
+      (code', buffer') = dequeue code buffer
       (2*low,
        2*high+1,
-       dequeue code,
+       code',
+       buffer',
        Continue)
     False -> case low >= half of
       True ->
-        (x, buffer, z) = code
+        (code', buffer') = dequeue code (buffer-half)
         (2*(low-half),
          2*(high-half)+1,
-         dequeue (x, buffer-half, z),
+         code',
+         buffer',
          Continue)
       False -> case high < thdQuarter && low >= fstQuarter of
         True ->
-          (x, buffer, z) = code
+          (code', buffer') = dequeue code (buffer-fstQuarter)
           (2*(low-fstQuarter),
            2*(high-fstQuarter)+1,
-           dequeue (x, buffer-fstQuarter, z),
+           code',
+           buffer',
            Continue)
-        False -> (low, high, code, Done 0)
+        False -> (low, high, code, buffer, Done 0)
 
+-- move state updates to helper functions
 def decodeSymbol  (l: Int)
                   (model: Alphabet=>(Interval->Interval))
                   (i: (Fin l))
@@ -212,9 +203,10 @@ def decodeSymbol  (l: Int)
     strRef := get strRef <> AsList 1 [symbol]
     intervalRef := interval
     boundedIter precision 0 \_.
-      (low, high, code, result) = decodeInterval (get intervalRef) (get codeRef)
+      (low, high, code, buffer, result) = decodeInterval (get intervalRef) (get codeRef) (get bufferRef)
       intervalRef := (low, high)
       codeRef := code 
+      bufferRef := buffer
       result
 
 '### Coding interface
@@ -222,31 +214,39 @@ def decodeSymbol  (l: Int)
 def encode (str: (Fin l)=>Word8) (model: Alphabet=>(Interval->Interval)) : List Int =
   update = encodeSymbol str model
   initInterval = (0,top-1)
-  fst $ snd $ fold (initInterval,(AsList 1 [0],0,0)) update
+  -- enqueue an extra 1 to the code to preserve length
+  fst $ enqueue 1 $ snd $ fold (initInterval,(AsList 1 [0],0,0)) update
 
 def decode (l: Int) (codeLst: List Int) (model: Alphabet=>(Interval->Interval)) : List Word8 =
   update = decodeSymbol l model
   initStr: List Word8 = AsList _ []
   initInterval = (0,top-1)
   initCode' = (codeLst, 1, 0)
-  initCode = yieldState initCode' \ref. for i:(Fin precision). ref := dequeue (get ref)
-  snd $ snd $ fold (initInterval, initCode, 0, initStr) update
+  initBuffer' = 0
+  (initCode, initBuffer) = yieldState (initCode',initBuffer') \ref. 
+    for i:(Fin precision). 
+      (code, buffer) = dequeue (get (fstRef ref)) (get (sndRef ref))
+      fstRef ref := code
+      sndRef ref := buffer
+  snd $ snd $ snd $ fold (initInterval, initCode, initBuffer, initStr) update
 
 '### Demo: Lossless compression on a test string
 
-str' = "edacg"
+str' = "biudngr"
 (AsList l str) = str'
 m = model str
 
 code = encode str m
 code
-> (AsList 1 [821])
+> (AsList 1 [11208])
 
 decoded = decode l code m
 decoded
-> 
+> (AsList 7 "biudngr")
 decoded == str'
-> 
+> True
+
+
 
 
 

From 2b48f4c358944ccb0e87b983721597c4da9d05da Mon Sep 17 00:00:00 2001
From: Cynthia Shen <58400192+cyntsh@users.noreply.github.com>
Date: Thu, 12 Aug 2021 23:43:34 -0400
Subject: [PATCH 11/17] WIP

---
 examples/arithmetic-coding.dx | 114 +++++++++++++++++++---------------
 1 file changed, 63 insertions(+), 51 deletions(-)

diff --git a/examples/arithmetic-coding.dx b/examples/arithmetic-coding.dx
index deb698d40..ceeb260ce 100644
--- a/examples/arithmetic-coding.dx
+++ b/examples/arithmetic-coding.dx
@@ -3,7 +3,7 @@ A finite-precision variant based on [this](https://web.stanford.edu/class/ee398a
 
 Alphabet = Fin 26
 Interval = (Int&Int)
-Code = ((List Int)&Int&Int)
+Code = ((List Int)&Int)
 maxBits = 31
 precision = 7
 top = intpow2 precision
@@ -73,81 +73,87 @@ def selectStream (numBits: Int) (code: Ref h Int)
     True -> code := %or (get code) bitMask
     False -> overflow := %or (get overflow) bitMask
 
-def enqueue (bit: Int) ((codeLst, numBits, tally): Code) : Code =
+def enqueue (bit: Int) ((codeLst, bitPos): Code) : Code =
   (AsList numInts intArr) = codeLst
-  code = intArr.((numInts-1)@_)
-  overflow = (0, AsList 0 [])
-
-  (code', overflow', numBits') = yieldState (code, overflow, numBits) \ref.
-    codeRef = fstRef ref
-    overflowRef = fstRef (fstRef (sndRef ref))
-    lstOverflowRef = sndRef (fstRef (sndRef ref))
-    bitsRef = sndRef (sndRef ref)
-
-    if bit==1 then selectStream (get bitsRef) codeRef overflowRef
-    bitsRef := (get bitsRef)+1
-    if overflowing (get bitsRef) then 
-      lstOverflowRef := (get lstOverflowRef) <> (AsList 1 [get overflowRef])
-      overflowRef := 0
-
-    for i:(Fin tally).
-      if bit==0 then selectStream (get bitsRef) codeRef overflowRef
-      bitsRef := (get bitsRef)+1
-      if overflowing (get bitsRef) then 
-        lstOverflowRef := (get lstOverflowRef) <> (AsList 1 [get overflowRef])
-        overflowRef := 0
-
-    if existsOverflow (get bitsRef) then
-      lstOverflowRef := (get lstOverflowRef) <> (AsList 1 [get overflowRef])
+  codePos = idiv (bitPos) maxBits 
+
+  (codeLst', _, numInts') = yieldState (codeLst, intArr, numInts) \ref.
+    lstRef = fstRef ref
+    arrRef = fstRef (sndRef ref)
+    numRef = sndRef (sndRef ref)
+    case codePos >= get numRef of
+      True -> 
+        numRef := (get numRef) + 1
+        lstRef := (get lstRef) <> (AsList 1 [bit])
+      False ->
+        if bit == 1 then 
+          code = get arrRef!(codePos@_)
+          numBits = mod bitPos maxBits
+          bitMask = intpow2 numBits
+          arrRef!(codePos@_) := %or code bitMask
+        lstRef := (AsList numInts (get arrRef))
 
-  intArr' = yieldState intArr \arr. arr!((numInts-1)@_) := code'
-  codeLst' = (AsList numInts intArr') <> (snd overflow')
-  (codeLst', mod numBits' maxBits, 0)
+  (codeLst', bitPos+1)
 
-def dequeue ((codeLst, bitPos, tally): Code) (buffer: Int): (Code&Int) = 
+def dequeue ((codeLst, bitPos): Code) (buffer: Int): (Code&Int) = 
   (AsList numInts intArr) = codeLst
-  codePos = idiv (bitPos) maxBits -- initial bitPos is 1
-  code = intArr.(codePos@_)
-  buffer' = 2*buffer + %and 1 code
-  intArr' = yieldState intArr \arr. arr!(codePos@_) := %shr code 1
+  codePos = idiv (bitPos) maxBits
+  (buffer', intArr') = case numInts > codePos of
+    True ->
+      code = intArr.(codePos@_)
+      intArr' = yieldState intArr \arr. arr!(codePos@_) := %shr code 1
+      (2*buffer + %and 1 code, intArr')
+    False -> (2*buffer, intArr)
   codeLst' = AsList numInts intArr'
-  ((codeLst', bitPos+1, 0), buffer')
+  ((codeLst', bitPos+1), buffer')
 
 '### Scaling functions
 
-def encodeInterval ((low, high): Interval) (code: Code) : (Int&Int&Code&(IterResult Int)) =
+def updateCode (bit: Int) (code: Code) (tally: Int) : Code =
+  yieldState code \ref.
+    ref := enqueue bit (get ref)
+    for i:(Fin tally).
+      ref := enqueue (%xor bit 1) (get ref)
+
+def encodeInterval ((low, high): Interval) 
+                   (code: Code) (tally: Int) : (Int&Int&Code&Int&(IterResult Int)) =
   case high < half of
     True ->
       (2*low,
        2*high+1,
-       enqueue 0 code,
+       updateCode 0 code tally,
+       0,
        Continue)
     False -> case low >= half of
       True ->
         (2*(low - half),
          2*(high - half)+1,
-         enqueue 1 code,
+         updateCode 1 code tally,
+         0,
          Continue)
       False -> case high < thdQuarter && low >= fstQuarter of
         True ->
           (2*(low - fstQuarter), 
            2*(high - fstQuarter)+1, 
-           (fst code, fst (snd code), snd (snd code) + 1), 
+           code, 
+           tally + 1,
            Continue)
-        False -> (low, high, code, Done 0)
+        False -> (low, high, code, tally, Done 0)
 
 def encodeSymbol (str: (Fin l)=>Word8) 
               (model: Alphabet=>(Interval->Interval)) 
               (i: (Fin l)) 
-              (params: (Interval&Code)) : (Interval&Code) =
+              (params: (Interval&Code&Int)) : (Interval&Code&Int) =
   yieldState params \p.
     intervalRef = fstRef p
-    codeRef = sndRef p
+    codeRef = fstRef (sndRef p)
+    tallyRef = sndRef (sndRef p)
     intervalRef := model.((charToIdx str.i)@_) (get intervalRef)
     boundedIter precision 0 \_.
-      (low, high, code, result) = encodeInterval (get intervalRef) (get codeRef)
+      (low, high, code, tally, result) = encodeInterval (get intervalRef) (get codeRef) (get tallyRef)
       intervalRef := (low, high)
       codeRef := code
+      tallyRef := tally
       result
 
 def findInterval (interval: Interval) (buffer: Int) 
@@ -211,17 +217,20 @@ def decodeSymbol  (l: Int)
 
 '### Coding interface
 
-def encode (str: (Fin l)=>Word8) (model: Alphabet=>(Interval->Interval)) : List Int =
+def encode (str: (Fin l)=>Word8) 
+           (model: Alphabet=>(Interval->Interval)) : List Int =
   update = encodeSymbol str model
   initInterval = (0,top-1)
   -- enqueue an extra 1 to the code to preserve length
-  fst $ enqueue 1 $ snd $ fold (initInterval,(AsList 1 [0],0,0)) update
+  fst $ fst $ snd $ fold (initInterval,(AsList 1 [0],0),0) update
 
-def decode (l: Int) (codeLst: List Int) (model: Alphabet=>(Interval->Interval)) : List Word8 =
+def decode (l: Int) (codeLst: List Int) 
+           (model: Alphabet=>(Interval->Interval)) : List Word8 =
   update = decodeSymbol l model
   initStr: List Word8 = AsList _ []
   initInterval = (0,top-1)
-  initCode' = (codeLst, 1, 0)
+  codeLst' = codeLst <> (AsList 1 [0])
+  initCode' = (codeLst', 0)
   initBuffer' = 0
   (initCode, initBuffer) = yieldState (initCode',initBuffer') \ref. 
     for i:(Fin precision). 
@@ -232,19 +241,22 @@ def decode (l: Int) (codeLst: List Int) (model: Alphabet=>(Interval->Interval))
 
 '### Demo: Lossless compression on a test string
 
-str' = "biudngr"
+str' = "abccedaczh"
 (AsList l str) = str'
 m = model str
 
 code = encode str m
 code
-> (AsList 1 [11208])
+> 
 
 decoded = decode l code m
 decoded
-> (AsList 7 "biudngr")
+> 
 decoded == str'
-> True
+> 
+
+
+
 
 
 

From 4d876f1cf65ebec11cde3e93ca5bda1f06525b5e Mon Sep 17 00:00:00 2001
From: Cynthia Shen <58400192+cyntsh@users.noreply.github.com>
Date: Fri, 13 Aug 2021 21:53:07 -0400
Subject: [PATCH 12/17] Relax interval constraint

---
 examples/arithmetic-coding.dx | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/examples/arithmetic-coding.dx b/examples/arithmetic-coding.dx
index ceeb260ce..457dcfebb 100644
--- a/examples/arithmetic-coding.dx
+++ b/examples/arithmetic-coding.dx
@@ -163,7 +163,7 @@ def findInterval (interval: Interval) (buffer: Int)
       True -> Continue
       False ->
         (low, high) = model.(j@_) interval
-        case buffer >= low && buffer < high of
+        case buffer < high of
           True -> Done (idxToChar j, (low,high))
           False -> Continue
 
@@ -266,3 +266,4 @@ decoded == str'
 
 
 
+

From d2dd11f72a7ab28375b5b4d1ae1ccbc1fd85ba31 Mon Sep 17 00:00:00 2001
From: Cynthia Shen <58400192+cyntsh@users.noreply.github.com>
Date: Tue, 24 Aug 2021 10:43:22 -0400
Subject: [PATCH 13/17] Revert and clean up

---
 examples/arithmetic-coding.dx | 291 +++++++---------------------------
 1 file changed, 57 insertions(+), 234 deletions(-)

diff --git a/examples/arithmetic-coding.dx b/examples/arithmetic-coding.dx
index 457dcfebb..89a5d21ce 100644
--- a/examples/arithmetic-coding.dx
+++ b/examples/arithmetic-coding.dx
@@ -1,269 +1,92 @@
-'## Arithmetic coding
-A finite-precision variant based on [this](https://web.stanford.edu/class/ee398a/handouts/papers/WittenACM87ArithmCoding.pdf) paper by Ian H. Witten et al.
+'## [Arithmetic coding](https://en.wikipedia.org/wiki/Arithmetic_coding)
 
 Alphabet = Fin 26
-Interval = (Int&Int)
-Code = ((List Int)&Int)
-maxBits = 31
-precision = 7
-top = intpow2 precision
-half = idiv top 2
-fstQuarter = idiv half 2
-thdQuarter = fstQuarter * 3
+Interval = (Float&Float)
+top:Interval = (0.,1.)
 
 def charToIdx (c: Word8) : Int = W8ToI c - W8ToI 'a'
 def idxToChar (i: Int) : Word8 = IToW8 (i + (W8ToI 'a'))
 
 '### Statistical modelling
 
-def norm (freq: Int) (l: Int) (w: Int) : Int = FToI $ IToF freq / IToF l * IToF w
-def inverseNorm (norm: Int) (l: Int) (w: Int) : Int = FToI $ IToF norm / IToF w * IToF l
-
-def getCumFreq (fs: Alphabet=>Int) : Alphabet=>Int =
-  withState zero \total.
-    for i. if fs.i /= zero
+def cumProb (ps: n=>Float) : n=>Float =
+  withState 0.0 \total.
+    for i. if ps.i > 0. 
       then
-        newTotal = get total + fs.i
+        currTotal = get total
+        newTotal = currTotal + ps.i
         total := newTotal
-        newTotal
-      else zero
-
-def getIntervals (xs: Alphabet=>Int) : Alphabet=>Interval =
-  withState (0,0) \ref.
-    for i. if xs.i /= zero
-      then
-        ref := ((snd (get ref)), xs.i)
-        get ref
-      else (0,0)
+        currTotal
+      else 0.
 
 def getFrequency (str: (Fin l)=>Word8) : Alphabet=>Int =
   a: Alphabet => Int = zero
   yieldState a \ref. for i. 
     i' = (charToIdx str.i)@_
-    ref!i' := get ref!i' + 1
-
-def model (str: (Fin l)=>Word8) : Alphabet=>(Interval->Interval) =
-  freq = getFrequency str
-  cumFreq = getCumFreq freq
-  inFreq = getIntervals cumFreq
-  for i.
-    case inFreq.i == (0,0) of
-      True -> id
-      False ->
-        (fLow, fHigh) = inFreq.i
-        \(low, high).
-          w = high-low+1
-          low' = low + norm fLow l w
-          high' = low-1 + norm fHigh l w
-          (low', high')
-
-'### Integer arithmetic
-
-def overflowing (numBits: Int) : Bool = 
-  mod numBits maxBits == 0 && numBits > maxBits
-
-def existsOverflow (numBits: Int) : Bool =
-  mod numBits maxBits > 0 && numBits > maxBits
-
-def selectStream (numBits: Int) (code: Ref h Int) 
-                 (overflow: Ref h Int) : {State h} Unit =
-  numBits' = mod numBits maxBits
-  bitMask = intpow2 numBits'
-  case (numBits < maxBits) of 
-    True -> code := %or (get code) bitMask
-    False -> overflow := %or (get overflow) bitMask
+    ref!i' := (get ref).i' + 1
 
-def enqueue (bit: Int) ((codeLst, bitPos): Code) : Code =
-  (AsList numInts intArr) = codeLst
-  codePos = idiv (bitPos) maxBits 
-
-  (codeLst', _, numInts') = yieldState (codeLst, intArr, numInts) \ref.
-    lstRef = fstRef ref
-    arrRef = fstRef (sndRef ref)
-    numRef = sndRef (sndRef ref)
-    case codePos >= get numRef of
-      True -> 
-        numRef := (get numRef) + 1
-        lstRef := (get lstRef) <> (AsList 1 [bit])
-      False ->
-        if bit == 1 then 
-          code = get arrRef!(codePos@_)
-          numBits = mod bitPos maxBits
-          bitMask = intpow2 numBits
-          arrRef!(codePos@_) := %or code bitMask
-        lstRef := (AsList numInts (get arrRef))
-
-  (codeLst', bitPos+1)
-
-def dequeue ((codeLst, bitPos): Code) (buffer: Int): (Code&Int) = 
-  (AsList numInts intArr) = codeLst
-  codePos = idiv (bitPos) maxBits
-  (buffer', intArr') = case numInts > codePos of
-    True ->
-      code = intArr.(codePos@_)
-      intArr' = yieldState intArr \arr. arr!(codePos@_) := %shr code 1
-      (2*buffer + %and 1 code, intArr')
-    False -> (2*buffer, intArr)
-  codeLst' = AsList numInts intArr'
-  ((codeLst', bitPos+1), buffer')
+def getProbability (l: Int) (freq: Alphabet=>Int) : Alphabet=>(Float&Float) =
+  probs = for i. IToF freq.i / IToF l
+  cums = cumProb probs
+  for i. (probs.i, cums.i)
 
 '### Scaling functions
 
-def updateCode (bit: Int) (code: Code) (tally: Int) : Code =
-  yieldState code \ref.
-    ref := enqueue bit (get ref)
-    for i:(Fin tally).
-      ref := enqueue (%xor bit 1) (get ref)
-
-def encodeInterval ((low, high): Interval) 
-                   (code: Code) (tally: Int) : (Int&Int&Code&Int&(IterResult Int)) =
-  case high < half of
-    True ->
-      (2*low,
-       2*high+1,
-       updateCode 0 code tally,
-       0,
-       Continue)
-    False -> case low >= half of
-      True ->
-        (2*(low - half),
-         2*(high - half)+1,
-         updateCode 1 code tally,
-         0,
-         Continue)
-      False -> case high < thdQuarter && low >= fstQuarter of
-        True ->
-          (2*(low - fstQuarter), 
-           2*(high - fstQuarter)+1, 
-           code, 
-           tally + 1,
-           Continue)
-        False -> (low, high, code, tally, Done 0)
-
-def encodeSymbol (str: (Fin l)=>Word8) 
-              (model: Alphabet=>(Interval->Interval)) 
-              (i: (Fin l)) 
-              (params: (Interval&Code&Int)) : (Interval&Code&Int) =
-  yieldState params \p.
-    intervalRef = fstRef p
-    codeRef = fstRef (sndRef p)
-    tallyRef = sndRef (sndRef p)
-    intervalRef := model.((charToIdx str.i)@_) (get intervalRef)
-    boundedIter precision 0 \_.
-      (low, high, code, tally, result) = encodeInterval (get intervalRef) (get codeRef) (get tallyRef)
-      intervalRef := (low, high)
-      codeRef := code
-      tallyRef := tally
-      result
-
-def findInterval (interval: Interval) (buffer: Int) 
-                 (model: Alphabet=>(Interval->Interval)) : (Word8&Interval)=
-  boundedIter (size Alphabet) (' ',(0,0)) \j.
-    case model.(j@_) interval == interval of
+def getUpdateRule (p: Alphabet=>(Float&Float)) : Alphabet=>(Interval->Interval) =
+  for i. 
+    case p.i == (0.,0.) of
+      True -> id
+      False ->
+        \(x, w).
+          x' = x + w*(snd p.i)
+          w' = w*(fst p.i)
+          (x', w')
+
+def subdivide (str: (Fin l)=>Word8) 
+              (rule: Alphabet=>(Interval->Interval)) 
+              (i: (Fin l)) (in: Interval) : Interval =
+  updateInterval = rule.((charToIdx str.i)@_)
+  updateInterval in
+
+def findInterval  (l: Int) 
+                  (code: Float) 
+                  (rule: Alphabet=>(Interval->Interval))
+                  (i: (Fin l))
+                  ((str,in): (List Word8 & Interval)) : (List Word8 & Interval) =
+  (letter, in') = boundedIter (size Alphabet) (' ', top) \j.
+    case rule.(j@_) in == in of
       True -> Continue
       False ->
-        (low, high) = model.(j@_) interval
-        case buffer < high of
-          True -> Done (idxToChar j, (low,high))
+        (x, w) = rule.(j@_) in 
+        case code >= x && code < (x+w) of
+          True -> Done (idxToChar j, (x,w))
           False -> Continue
-
-def decodeInterval ((low, high): Interval) 
-                   (code: Code) (buffer: Int) : (Int&Int&Code&Int&(IterResult Int)) =
-  case high < half of
-    True ->
-      (code', buffer') = dequeue code buffer
-      (2*low,
-       2*high+1,
-       code',
-       buffer',
-       Continue)
-    False -> case low >= half of
-      True ->
-        (code', buffer') = dequeue code (buffer-half)
-        (2*(low-half),
-         2*(high-half)+1,
-         code',
-         buffer',
-         Continue)
-      False -> case high < thdQuarter && low >= fstQuarter of
-        True ->
-          (code', buffer') = dequeue code (buffer-fstQuarter)
-          (2*(low-fstQuarter),
-           2*(high-fstQuarter)+1,
-           code',
-           buffer',
-           Continue)
-        False -> (low, high, code, buffer, Done 0)
-
--- move state updates to helper functions
-def decodeSymbol  (l: Int)
-                  (model: Alphabet=>(Interval->Interval))
-                  (i: (Fin l))
-                  (params: (Interval&Code&Int&List Word8)) : (Interval&Code&Int&List Word8) =
-  yieldState params \p.
-    intervalRef = fstRef p
-    codeRef = fstRef (sndRef p)
-    strRef = sndRef (sndRef (sndRef p))
-    bufferRef = fstRef (sndRef (sndRef p))
-    (symbol, interval) = findInterval (get intervalRef) (get bufferRef) model
-    strRef := get strRef <> AsList 1 [symbol]
-    intervalRef := interval
-    boundedIter precision 0 \_.
-      (low, high, code, buffer, result) = decodeInterval (get intervalRef) (get codeRef) (get bufferRef)
-      intervalRef := (low, high)
-      codeRef := code 
-      bufferRef := buffer
-      result
+  (str <> AsList 1 [letter], in')
 
 '### Coding interface
 
-def encode (str: (Fin l)=>Word8) 
-           (model: Alphabet=>(Interval->Interval)) : List Int =
-  update = encodeSymbol str model
-  initInterval = (0,top-1)
-  -- enqueue an extra 1 to the code to preserve length
-  fst $ fst $ snd $ fold (initInterval,(AsList 1 [0],0),0) update
+def encode (str: (Fin l)=>Word8) (rule: Alphabet=>(Interval->Interval)) : Float =
+  update = subdivide str rule
+  finalInterval = fold top update
+  fst finalInterval + (snd finalInterval)/2.
 
-def decode (l: Int) (codeLst: List Int) 
-           (model: Alphabet=>(Interval->Interval)) : List Word8 =
-  update = decodeSymbol l model
+def decode (l: Int) (code: Float) (rule: Alphabet=>(Interval->Interval)) : List Word8 =
+  update = findInterval l code rule
   initStr: List Word8 = AsList _ []
-  initInterval = (0,top-1)
-  codeLst' = codeLst <> (AsList 1 [0])
-  initCode' = (codeLst', 0)
-  initBuffer' = 0
-  (initCode, initBuffer) = yieldState (initCode',initBuffer') \ref. 
-    for i:(Fin precision). 
-      (code, buffer) = dequeue (get (fstRef ref)) (get (sndRef ref))
-      fstRef ref := code
-      sndRef ref := buffer
-  snd $ snd $ snd $ fold (initInterval, initCode, initBuffer, initStr) update
+  fst $ fold (initStr, top) update
 
 '### Demo: Lossless compression on a test string
 
-str' = "abccedaczh"
+str' = "abbadcabccdd"
 (AsList l str) = str'
-m = model str
 
-code = encode str m
+p = getProbability l $ getFrequency str
+r = getUpdateRule p
+
+code = encode str r
 code
-> 
+> 0.081569
 
-decoded = decode l code m
-decoded
-> 
+decoded = decode l code r
 decoded == str'
-> 
-
-
-
-
-
-
-
-
-
-
-
-
-
+> True

From 4c43d9b5294bb086f8b2e06e41916739af1840a7 Mon Sep 17 00:00:00 2001
From: Cynthia Shen <58400192+cyntsh@users.noreply.github.com>
Date: Wed, 25 Aug 2021 11:44:24 -0400
Subject: [PATCH 14/17] Add comments

---
 examples/arithmetic-coding.dx | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/examples/arithmetic-coding.dx b/examples/arithmetic-coding.dx
index 89a5d21ce..6bf229d36 100644
--- a/examples/arithmetic-coding.dx
+++ b/examples/arithmetic-coding.dx
@@ -1,4 +1,7 @@
 '## [Arithmetic coding](https://en.wikipedia.org/wiki/Arithmetic_coding)
+This demonstrates a lossless method for compression on a string of letters.
+Rather than assigning a code to each letter, the entire string is encoded
+into a single floating point number.
 
 Alphabet = Fin 26
 Interval = (Float&Float)
@@ -8,6 +11,7 @@ def charToIdx (c: Word8) : Int = W8ToI c - W8ToI 'a'
 def idxToChar (i: Int) : Word8 = IToW8 (i + (W8ToI 'a'))
 
 '### Statistical modelling
+First, model the probability of each letter given by the string to be encoded.
 
 def cumProb (ps: n=>Float) : n=>Float =
   withState 0.0 \total.
@@ -64,6 +68,11 @@ def findInterval  (l: Int)
   (str <> AsList 1 [letter], in')
 
 '### Coding interface
+Start from an initial interval, [0, 1). 
+For each letter encoded from the string, the current interval is divided based on the
+cumulative probability of all letters, then updated to the partition that matches
+the encoded letter.
+The decoding process retraces the steps of the encoding process to recover the correct letters.
 
 def encode (str: (Fin l)=>Word8) (rule: Alphabet=>(Interval->Interval)) : Float =
   update = subdivide str rule
@@ -90,3 +99,4 @@ code
 decoded = decode l code r
 decoded == str'
 > True
+

From 7ebc207c3e70821bcf5dd0eeb81bb7f4d24c1854 Mon Sep 17 00:00:00 2001
From: Cynthia Shen <58400192+cyntsh@users.noreply.github.com>
Date: Wed, 25 Aug 2021 11:48:05 -0400
Subject: [PATCH 15/17] Edit comments

---
 examples/arithmetic-coding.dx | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/examples/arithmetic-coding.dx b/examples/arithmetic-coding.dx
index 6bf229d36..62308ced3 100644
--- a/examples/arithmetic-coding.dx
+++ b/examples/arithmetic-coding.dx
@@ -1,7 +1,7 @@
 '## [Arithmetic coding](https://en.wikipedia.org/wiki/Arithmetic_coding)
 This demonstrates a lossless method for compression on a string of letters.
 Rather than assigning a code to each letter, the entire string is encoded
-into a single floating point number.
+into a single floating-point number.
 
 Alphabet = Fin 26
 Interval = (Float&Float)

From 6a9595bd23aa0d3828e51aafaf3b6284fc82ff4a Mon Sep 17 00:00:00 2001
From: Cynthia Shen <58400192+cyntsh@users.noreply.github.com>
Date: Wed, 5 Jan 2022 19:12:57 -0500
Subject: [PATCH 16/17] rANS

---
 examples/arithmetic-coding.dx | 204 ++++++++++++++++++++--------------
 1 file changed, 120 insertions(+), 84 deletions(-)

diff --git a/examples/arithmetic-coding.dx b/examples/arithmetic-coding.dx
index 62308ced3..6c4a310df 100644
--- a/examples/arithmetic-coding.dx
+++ b/examples/arithmetic-coding.dx
@@ -1,102 +1,138 @@
-'## [Arithmetic coding](https://en.wikipedia.org/wiki/Arithmetic_coding)
-This demonstrates a lossless method for compression on a string of letters.
-Rather than assigning a code to each letter, the entire string is encoded
-into a single floating-point number.
+'# Lossless compression
+Based on the implementation of [rANS](https://github.com/j-towns/ans-notes/blob/master/rans.py) by James Townsend.
+
+-- note: still some issues with using large integers, as with arithmetic coding
+-- likely a problem with Dex; need support for Int64 bitwise operations
+-- can either wait for improvements or use a bit array instead
+
+two: Float64 = FToF64 2.
+p_prec: Float64 = FToF64 3.
+p_int: Float64 = pow two p_prec
+s_prec: Float64 = FToF64 64.
+t_prec: Float64 = FToF64 32.
+t_mask: Float64 = (pow two t_prec) - one
+s_min: Float64  = pow two (s_prec - t_prec)
+s_max: Float64  = pow two s_prec
 
 Alphabet = Fin 26
-Interval = (Float&Float)
-top:Interval = (0.,1.)
+Interval = Fin (FToI (F64ToF p_int))
+Message = (Float64 & List Float64)
+
+'Utilities
 
 def charToIdx (c: Word8) : Int = W8ToI c - W8ToI 'a'
 def idxToChar (i: Int) : Word8 = IToW8 (i + (W8ToI 'a'))
+def mod64 (x: Float64) (y: Float64) : Float64 = x - (floor (divide x y)) * y
 
-'### Statistical modelling
-First, model the probability of each letter given by the string to be encoded.
-
-def cumProb (ps: n=>Float) : n=>Float =
-  withState 0.0 \total.
-    for i. if ps.i > 0. 
+def get_cs (ps: Alphabet=>Float64) : Alphabet=>Float64 =
+  withState zero \total.
+    for i. if ps.i > zero
       then
         currTotal = get total
         newTotal = currTotal + ps.i
         total := newTotal
         currTotal
-      else 0.
+      else zero
 
-def getFrequency (str: (Fin l)=>Word8) : Alphabet=>Int =
-  a: Alphabet => Int = zero
+def get_ps (str: (Fin l)=>Word8) : Alphabet=>Float64 =
+  a: Alphabet => Float64 = zero
   yieldState a \ref. for i. 
     i' = (charToIdx str.i)@_
     ref!i' := (get ref).i' + 1
 
-def getProbability (l: Int) (freq: Alphabet=>Int) : Alphabet=>(Float&Float) =
-  probs = for i. IToF freq.i / IToF l
-  cums = cumProb probs
-  for i. (probs.i, cums.i)
-
-'### Scaling functions
-
-def getUpdateRule (p: Alphabet=>(Float&Float)) : Alphabet=>(Interval->Interval) =
-  for i. 
-    case p.i == (0.,0.) of
-      True -> id
-      False ->
-        \(x, w).
-          x' = x + w*(snd p.i)
-          w' = w*(fst p.i)
-          (x', w')
-
-def subdivide (str: (Fin l)=>Word8) 
-              (rule: Alphabet=>(Interval->Interval)) 
-              (i: (Fin l)) (in: Interval) : Interval =
-  updateInterval = rule.((charToIdx str.i)@_)
-  updateInterval in
-
-def findInterval  (l: Int) 
-                  (code: Float) 
-                  (rule: Alphabet=>(Interval->Interval))
-                  (i: (Fin l))
-                  ((str,in): (List Word8 & Interval)) : (List Word8 & Interval) =
-  (letter, in') = boundedIter (size Alphabet) (' ', top) \j.
-    case rule.(j@_) in == in of
-      True -> Continue
-      False ->
-        (x, w) = rule.(j@_) in 
-        case code >= x && code < (x+w) of
-          True -> Done (idxToChar j, (x,w))
-          False -> Continue
-  (str <> AsList 1 [letter], in')
-
-'### Coding interface
-Start from an initial interval, [0, 1). 
-For each letter encoded from the string, the current interval is divided based on the
-cumulative probability of all letters, then updated to the partition that matches
-the encoded letter.
-The decoding process retraces the steps of the encoding process to recover the correct letters.
-
-def encode (str: (Fin l)=>Word8) (rule: Alphabet=>(Interval->Interval)) : Float =
-  update = subdivide str rule
-  finalInterval = fold top update
-  fst finalInterval + (snd finalInterval)/2.
-
-def decode (l: Int) (code: Float) (rule: Alphabet=>(Interval->Interval)) : List Word8 =
-  update = findInterval l code rule
-  initStr: List Word8 = AsList _ []
-  fst $ fold (initStr, top) update
-
-'### Demo: Lossless compression on a test string
-
-str' = "abbadcabccdd"
-(AsList l str) = str'
-
-p = getProbability l $ getFrequency str
-r = getUpdateRule p
-
-code = encode str r
-code
-> 0.081569
-
-decoded = decode l code r
-decoded == str'
+def get_cs_map (ps: Alphabet=>Float64) : Interval=>Word8 =
+  init: List Word8 = (AsList 0 [])
+  map' = yieldState init \map.
+    for i.
+      count = (FToI (F64ToF ps.i))
+      boundedIter count 0 \_.
+        map := (get map) <> (AsList 1 [idxToChar (ordinal i)])
+        Continue
+  (AsList _ map'') = map'
+  map = for i:Interval. map''.(unsafeFromOrdinal _ (ordinal i))
+  map
+
+xs' = "abbccddc"
+(AsList l xs) = xs'
+ps = get_ps xs
+cs = get_cs ps
+cs_map = get_cs_map ps
+
+def g (x: Word8) : (Float64 & Float64) =
+  x_idx = charToIdx x
+  (cs.(x_idx@_), ps.(x_idx@_))
+
+def f (s': Float64) : (Word8 & (Float64 & Float64)) =
+  x = cs_map.((FToI (F64ToF s'))@_)
+  (x, g x)
+
+def stack_pop ((AsList l' t'): List Float64) : (Float64 & List Float64) =
+  l'' = l' - 1
+  tail = slice t' 1 (Fin l'')
+  head = t'.(0@_)
+  (head, (AsList _ tail))
+
+def stack_push (t_top: Float64) (t: List Float64) : (List Float64) =
+  (AsList 1 [t_top]) <> t
+
+'Coding Interface
+
+def pop (m: Message) : (Message & Word8) =
+  (s, t) = m
+  s_bar = mod64 s p_int
+  (x, (c, p)) = f s_bar
+  s' = p * (floor (divide s (pow two p_prec))) + s_bar - c
+  -- TODO: use a while loop, not a do-while
+  m' = case s' < s_min of
+    True -> 
+      yieldState m \m'.
+        s'' = fstRef m'
+        t'' = sndRef m'
+        while do
+          (t_top, t') = stack_pop (get t'')
+          t'' := t'
+          s'' := (get s'') * (pow two t_prec) + t_top
+          (get s'') < s_min
+    False -> (s', t)
+  (m', x)
+
+def push ((s, t): Message) (x: Word8) : Message =
+  (c, p) = g x
+  (s', t') = case s >= (p * (pow two (s_prec - p_prec))) of
+    True ->
+      yieldState (s, t) \m'.
+        s' = fstRef m'
+        t' = sndRef m'
+        while do
+          t' := stack_push (mod64 (get s') (pow two t_prec)) (get t') 
+          s' := floor (divide (get s') (pow two t_prec))
+          get s' >= (p * (pow two (s_prec - p_prec)))
+    False -> (s, t)
+  s'' = (pow two p_prec) * (floor (divide s' p)) + (mod64 s' p) + c
+  (s'', t')
+
+
+'Demo 
+
+-- initialize message
+m_init: Message = (s_min, AsList 0 [])
+xs_init' = "abbcbcdcc"
+(AsList l' xs_init) = xs_init'
+
+m' = yieldState m_init \m.
+  for i:(Fin l').
+    m := push (get m) xs_init.i
+
+init_args: (Message & List Word8) = (m', AsList 0 [])
+args' = yieldState init_args \ref.
+  m = fstRef ref
+  xs_decoded = sndRef ref
+  for i:(Fin l').
+    (m', x) = pop (get m)
+    m := m'
+    xs_decoded := (AsList 1 [x]) <> (get xs_decoded)
+
+(AsList _ xs_decoded) = snd args'
+:p xs_decoded == xs_init
 > True
 

From 6b48407b36ac98e7907dd43f1ea9f222116a0f90 Mon Sep 17 00:00:00 2001
From: Cynthia Shen <58400192+cyntsh@users.noreply.github.com>
Date: Fri, 7 Jan 2022 00:02:14 -0500
Subject: [PATCH 17/17] Use Word64 type

---
 examples/arithmetic-coding.dx | 107 ++++++++++++++++++++--------------
 1 file changed, 63 insertions(+), 44 deletions(-)

diff --git a/examples/arithmetic-coding.dx b/examples/arithmetic-coding.dx
index 6c4a310df..9d2ebb936 100644
--- a/examples/arithmetic-coding.dx
+++ b/examples/arithmetic-coding.dx
@@ -1,32 +1,48 @@
 '# Lossless compression
 Based on the implementation of [rANS](https://github.com/j-towns/ans-notes/blob/master/rans.py) by James Townsend.
 
--- note: still some issues with using large integers, as with arithmetic coding
--- likely a problem with Dex; need support for Int64 bitwise operations
--- can either wait for improvements or use a bit array instead
-
-two: Float64 = FToF64 2.
-p_prec: Float64 = FToF64 3.
-p_int: Float64 = pow two p_prec
-s_prec: Float64 = FToF64 64.
-t_prec: Float64 = FToF64 32.
-t_mask: Float64 = (pow two t_prec) - one
-s_min: Float64  = pow two (s_prec - t_prec)
-s_max: Float64  = pow two s_prec
-
+-- prelude additions
+
+def lowWord'  (x : Word64) : Word8 = internalCast _ x
+-- W8ToI (lowWord' (IToW64 100))
+
+instance Integral Word64
+  idiv = \x y.  %idiv x y
+  rem  = \x y.  %irem x y
+
+instance Mul Word64
+  mul = \x y. %imul x y
+  one = IToW64 1
+
+instance Eq Word64
+  (==) = \x y. W8ToB $ %ieq x y
+
+instance Ord Word64
+  (>) = \x y. W8ToB $ %igt x y
+  (<) = \x y. W8ToB $ %ilt x y
+
+p_prec = 3
+s_prec = 64
+t_prec = 32
+p_int: Int = %shl 1 p_prec
+p_mask: Word64 = (one .<<. p_prec) - one
+t_mask: Word64 = (one .<<. t_prec) - one
+s_min: Word64  = one .<<. (s_prec - t_prec)
+s_max: Word64 = one .<<. s_prec
 Alphabet = Fin 26
-Interval = Fin (FToI (F64ToF p_int))
-Message = (Float64 & List Float64)
+Interval = Fin p_int
+Message = (Word64 & List Word64)
 
 'Utilities
 
+def mod' (x: Word64) (y: Word64) : Word64 = rem (y + rem x y) y
+
 def charToIdx (c: Word8) : Int = W8ToI c - W8ToI 'a'
 def idxToChar (i: Int) : Word8 = IToW8 (i + (W8ToI 'a'))
-def mod64 (x: Float64) (y: Float64) : Float64 = x - (floor (divide x y)) * y
 
-def get_cs (ps: Alphabet=>Float64) : Alphabet=>Float64 =
+def get_cs (ps: Alphabet=>Word64) : Alphabet=>Word64 =
   withState zero \total.
-    for i. if ps.i > zero
+    for i. if ps.i > zero 
       then
         currTotal = get total
         newTotal = currTotal + ps.i
@@ -34,17 +50,17 @@ def get_cs (ps: Alphabet=>Float64) : Alphabet=>Float64 =
         currTotal
       else zero
 
-def get_ps (str: (Fin l)=>Word8) : Alphabet=>Float64 =
-  a: Alphabet => Float64 = zero
+def get_ps (str: (Fin l)=>Word8) : Alphabet=>Word64 =
+  a: Alphabet => Word64 = zero
   yieldState a \ref. for i. 
     i' = (charToIdx str.i)@_
-    ref!i' := (get ref).i' + 1
+    ref!i' := (get ref).i' + one
 
-def get_cs_map (ps: Alphabet=>Float64) : Interval=>Word8 =
+def get_cs_map (ps: Alphabet=>Word64) : Interval=>Word8 =
   init: List Word8 = (AsList 0 [])
   map' = yieldState init \map.
     for i.
-      count = (FToI (F64ToF ps.i))
+      count = W8ToI $ lowWord' ps.i
       boundedIter count 0 \_.
         map := (get map) <> (AsList 1 [idxToChar (ordinal i)])
         Continue
@@ -52,63 +68,64 @@ def get_cs_map (ps: Alphabet=>Float64) : Interval=>Word8 =
   map = for i:Interval. map''.(unsafeFromOrdinal _ (ordinal i))
   map
 
+-- a string to prep the statistics
 xs' = "abbccddc"
 (AsList l xs) = xs'
 ps = get_ps xs
 cs = get_cs ps
 cs_map = get_cs_map ps
 
-def g (x: Word8) : (Float64 & Float64) =
+def g (x: Word8) : (Word64 & Word64) =
   x_idx = charToIdx x
   (cs.(x_idx@_), ps.(x_idx@_))
 
-def f (s': Float64) : (Word8 & (Float64 & Float64)) =
-  x = cs_map.((FToI (F64ToF s'))@_)
+def f (s': Word64) : (Word8 & (Word64 & Word64)) =
+  idx = W8ToI $ lowWord' s'
+  x = cs_map.(idx@_)
   (x, g x)
 
-def stack_pop ((AsList l' t'): List Float64) : (Float64 & List Float64) =
+def stack_pop ((AsList l' t'): List Word64) : (Word64 & List Word64) =
   l'' = l' - 1
   tail = slice t' 1 (Fin l'')
   head = t'.(0@_)
   (head, (AsList _ tail))
 
-def stack_push (t_top: Float64) (t: List Float64) : (List Float64) =
+def stack_push (t_top: Word64) (t: List Word64) : (List Word64) =
   (AsList 1 [t_top]) <> t
 
 'Coding Interface
 
-def pop (m: Message) : (Message & Word8) =
-  (s, t) = m
-  s_bar = mod64 s p_int
+def pop ((s, t): Message) : (Message & Word8) =
+  s_bar = s .&. p_mask
   (x, (c, p)) = f s_bar
-  s' = p * (floor (divide s (pow two p_prec))) + s_bar - c
+  s' = p * (s .>>. p_prec) + s_bar - c
   -- TODO: use a while loop, not a do-while
   m' = case s' < s_min of
     True -> 
-      yieldState m \m'.
+      yieldState (s', t) \m'.
         s'' = fstRef m'
         t'' = sndRef m'
         while do
           (t_top, t') = stack_pop (get t'')
           t'' := t'
-          s'' := (get s'') * (pow two t_prec) + t_top
+          s'' := ((get s'') .<<. t_prec) + t_top
           (get s'') < s_min
     False -> (s', t)
   (m', x)
 
 def push ((s, t): Message) (x: Word8) : Message =
   (c, p) = g x
-  (s', t') = case s >= (p * (pow two (s_prec - p_prec))) of
+  (s', t') = case s >= (p .<<. (s_prec - p_prec)) of
     True ->
       yieldState (s, t) \m'.
         s' = fstRef m'
         t' = sndRef m'
         while do
-          t' := stack_push (mod64 (get s') (pow two t_prec)) (get t') 
-          s' := floor (divide (get s') (pow two t_prec))
-          get s' >= (p * (pow two (s_prec - p_prec)))
+          t' := stack_push ((get s') .&. t_mask) (get t') 
+          s' := (get s') .>>. t_prec
+          get s' >= (p .<<. (s_prec - p_prec))
     False -> (s, t)
-  s'' = (pow two p_prec) * (floor (divide s' p)) + (mod64 s' p) + c
+  s'' = ((idiv s' p) .<<. p_prec) + (mod' s' p) + c
   (s'', t')
 
 
@@ -116,7 +133,7 @@ def push ((s, t): Message) (x: Word8) : Message =
 
 -- initialize message
 m_init: Message = (s_min, AsList 0 [])
-xs_init' = "abbcbcdcc"
+xs_init' = "abbcbcdccdccacbbacccdabbbaccccd"
 (AsList l' xs_init) = xs_init'
 
 m' = yieldState m_init \m.
@@ -124,15 +141,17 @@ m' = yieldState m_init \m.
     m := push (get m) xs_init.i
 
 init_args: (Message & List Word8) = (m', AsList 0 [])
-args' = yieldState init_args \ref.
+(_, xs_decoded) = yieldState init_args \ref.
   m = fstRef ref
   xs_decoded = sndRef ref
   for i:(Fin l').
     (m', x) = pop (get m)
     m := m'
     xs_decoded := (AsList 1 [x]) <> (get xs_decoded)
+    get ref
+
+(AsList _ xs'') = xs_decoded
+:p xs'' == xs_init
+
 
-(AsList _ xs_decoded) = snd args'
-:p xs_decoded == xs_init
-> True