(* bits-un.rml
   
   Ill-typed `add' function (see bits.rml) with union types.
*)

(*[
  datasort bits : pos <= std; std <= bits
  datacon E : std(0)
  datacon Zero : -all len : nat- pos(len) -> pos(len+1)
                                     &  bits(len) -> bits(len+1) 
  datacon One : -all len : nat- std(len)  -> pos(len+1)
                                    &  bits(len) -> bits(len+1)
  datatype bits with nat
 ]*)
datatype bits =
   E
 | Zero of bits
 | One of bits
;

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

(*[ val whatever : unit -> bot ]*)
fun whatever x = whatever x

(*[ val add : -all len1, len2 : nat-
                   bits(len1) * bits(len2)
              ->
                   bits(len1)
                \/ bits(len1 + 1)
                \/ bits(len2)
                \/ bits(len2 + 1)
]*)
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'))