Modelling Domains.

Domains.idr

module Domains

allLTE : List Int -> Bool
allLTE Nil        = True
allLTE (x::Nil)   = True
allLTE (x::y::xs) = x < y && allLTE (y::xs)

data VRange : Int -> Int -> Bool -> Type where
  MkVRange  : VRange x y (x <= y)


data VSparse : List Int -> Bool -> Type where
  MkVSparse : (xs : List Int)
           -> {auto prf : NonEmpty xs}
           -> VSparse xs (allLTE xs)

data Domain : Int -> Int -> Type where
  Bool  : Domain 0 1
  Bound : (x : Int)
       -> (y : Int)
       -> {auto prf : VRange x y True}
       -> Domain x y
  Discrete : (x : Int)
          -> (y : Int)
          -> {auto prf : VRange x y True}
          -> Domain x y
  Sparse : (xs : List Int)
        -> {auto p : NonEmpty xs}
        -> {auto prf : VSparse xs True}
        -> Domain (head xs) (last xs)

getBounds : Domain x y -> Pair Int Int
getBounds _ {x} {y} = (x,y)