idris-0.11.2: test/interfaces005/interfaces005.idr

module Set
 
public export
interface SetSig a where
  data SetT : Type -> Type

  new : SetT a
  insert : a -> SetT a -> SetT a
  member : a -> SetT a -> Bool

Set : (a : Type) -> SetSig a => Type
Set (a) @{sig} = SetT @{sig} a

data Tree a = Leaf | Node (Tree a) a (Tree a)

mkTree : Type -> Type
mkTree = Tree

namespace TreeSet
  export
  [TreeSet] Ord a => SetSig a where

    SetT = Tree 

    new = Leaf

    insert x Leaf = Node Leaf x Leaf
    insert x (Node l val r) = case compare x val of
                                   LT => Node (insert x l) val r
                                   EQ => Node l val r
                                   GT => Node l val (insert x r)

    member x Leaf = False
    member x (Node l val r) = case compare x val of
                                   LT => member x l
                                   EQ => True
                                   GT => member x r

using implementation TreeSet

  test : Set Nat
  test = insert 3 $ 
         insert 2 $ 
         insert 7 $ 
         insert 3 $ 
         insert 4 $ 
         insert 5 new 

  foo : Bool
  foo = member 6 test

  bar : Bool
  bar = member 3 test