(* bits.rml -- Inductively defined bitstrings, with:

   (1) a datasort refinement:
      bits = any bitstring,
      std = "standardized" bitstrings, i.e. with no leading zeros,
      pos = standardized bitstrings of nonzero value (i.e. not the empty bitstring).

   (2) index refinement: (length, value) where
      length : nat = the length of the bitstring,
      value : nat = the number represented.        *)
(*[
  datasort bits : pos <= std; std <= bits
  datacon E : std(0, 0)
  datacon Zero : -all len, value : nat- pos(len, value) -> pos(len+1, 2*value)
                                     &  bits(len, value) -> bits(len+1, 2*value) 
  datacon One : -all len, value : nat- std(len, value)  -> pos(len+1, 2*value + 1)
                                    &  bits(len, value) -> bits(len+1, 2*value + 1)
  datatype bits with nat * nat
 ]*)
datatype bits =
   E
 | Zero of bits
 | One of bits
;

(*[ val xx : std(0, 0) ]*)    val xx = E
(*[ val yy : bits(2, 1) ]*)   val yy = One (Zero (E))   (* e01 : Leading zero *)
(*[ val zz : pos (2, 2) ]*)   val zz = Zero (One (E))   (* e10 : No leading zero *)
(*[ val zz' : pos(6, 43) ]*)  val zz' = One (One (Zero (One (Zero (One (E)))))) 
         (* e101011 : No leading zero *)

(*[ val inc : -all len, value : nat- 
                std(len, value)  -> pos(len, value+1) \/ pos(len+1, value+1)
             &  bits(len, value) -> bits(len, value+1) \/ bits(len+1, value+1)
]*)
fun inc n =
  case n of
    E => One E
  | Zero n => One n
  | One n => Zero (inc n)

(*[ val add : -all len1, len2, val1, val2 : nat-
                   bits(len1, val1) * bits(len2, val2)
             -> (-exists len : nat- [len >= len1 and len >= len2]
                   bits(len, val1 + val2))
]*)
fun add arg = case arg of
      (x, E) => x
    | (E, y) => y
    | (Zero x', Zero y') => Zero (add (x', y'))
    | (One x', Zero y') => One (add (x', y'))
    | (x, One y') => inc (add (x, Zero y'))

(*[ val toInt :! -all len, value : nat- bits(len, value) -> int(value)
]*)
fun toInt n = case n of
     E => 0
   | Zero n' => 2 * toInt n'
   | One n' => (2 * toInt n) + 1   (* BUG *)

(*[ val toInt : -all len, value : nat- bits(len, value) -> int(value)
]*)
fun toInt n = case n of
     E => 0
   | Zero n' => 2 * toInt n'
   | One n' => (2 * toInt n') + 1

(*[ val length : -all len, value : nat- bits(len, value) -> int(len)
]*)
fun length n = case n of
     E => 0
   | Zero n' => 1 + length n'
   | One n' => 1 + length n'

(* Can't properly check spec because
     div, mod not supported by constraint solver

   (*[ val fromInt : -all value : nat- int(value)
                              -> -exists len : nat- std(len, value)
   ]*)
*)
(* Weak specification: *)
(*[ val fromInt : int -> bits
]*)
fun fromInt n =
  if n = 0 then E
  else
      let val d = fromInt (n div 2)
          val r = n mod 2
      in
          if r = 0 then Zero d
          else One d
      end