[Agda] Problem with inductively defined type having (simulated) partial constructors

[Tristan Wibberley]

Hi all,

I'm defining an octet type to support bitwise operators and I've defined
data Octet using optional conditions.

I've  got unexpected problems in the definition of _or_ that the
compiler can't deduce that the conditions are true in any cases.

Anybody got any hints?



===========================================
module octet where

data Nat : Set where
  zero : Nat
  succ : Nat -> Nat

_+_ : Nat -> Nat -> Nat
zero + b = b
(succ a) + b = a + (succ b)

one = (succ zero)
two = one + one
four = two + two
eight = four + four
sixteen = eight + eight
thirtytwo = sixteen + sixteen
sixtyfour = thirtytwo + thirtytwo
onetwoeight = sixtyfour + sixtyfour
twofivesix = onetwoeight + onetwoeight

data Bool : Set where
  True : Bool
  False : Bool

data Bottom : Set where
record Top : Set where

_IsTrue : Bool -> Set
True IsTrue = Top
False IsTrue = Bottom

_IsFalse : Bool -> Set
True IsFalse = Bottom
False IsFalse = Top

_<_ : Nat -> Nat -> Bool
zero < zero = False
(succ a) < zero = False
zero < (succ b) = True
(succ a) < (succ b) = a < b 

mutual
  data Octet : Set where
    allzeros : Octet
    _orone : (o : Octet) -> {_ : (even o) IsTrue} -> Octet
    _shifted : (o : Octet) -> {_ : (room (two + four) o) IsTrue} ->
                              {_ : (hasaone o) IsTrue} -> Octet
  hasaone : Octet -> Bool
  hasaone allzeros = False
  hasaone (_ orone) = True
  hasaone (a shifted) = hasaone a

  even : Octet -> Bool
  even allzeros = True
  even (_ orone) = False
  even (_ shifted) = True

  room : Nat -> Octet -> Bool
  room _ allzeros = True
  room n (a orone) = room n a
  room zero (_ shifted) = False
  room (succ n) (a shifted) = room n a

zerob = allzeros
oneb = zerob orone
twob = oneb shifted
fourb = twob shifted
eightb = fourb shifted
sixteenb = eightb shifted
thirtytwob = sixteenb shifted
sixtyfourb = thirtytwob shifted
onetwoeightb = sixtyfourb shifted

_or_ : Octet -> Octet -> Octet
allzeros or b = b
(a orone) or allzeros  = a orone
(a orone) or (b shifted) = (a or (b shifted)) orone
(a orone) or (b orone) = (a or b) orone
(a shifted) or allzeros = a shifted
(a shifted) or (b orone) = ((a shifted) or b) orone
(a shifted) or (b shifted) = (a or b) shifted


-- 
Tristan Wibberley

Any opinion expressed is mine (or else I'm playing devils advocate for
the sake of a good argument). My employer had nothing to do with this
communication.