FancyTerm.hs

{-# LANGUAGE GADTs #-}
module FancyTerm where 


data Tree a where 
    Leaf :: a -> Tree a 
    Node :: (Int -> (Tree a)) -> Tree a 

{-@ measure tsize :: Tree a -> Nat @-}
{-@ data size (Tree a) tsize @-}

{-@ data Tree a where 
      Leaf :: a -> {t:Tree a  | tsize t == 0 } 
      Node :: f:(Int -> Tree a) -> Tree a   @-}

{-@ mapTr :: (a -> a) -> t:Tree a -> o:Tree a / [tsize t] @-}
mapTr :: (a -> a) -> Tree a -> Tree a 
mapTr f (Leaf x) = Leaf $ f x 
mapTr f (Node n) = Node (\x -> mapTr f (n x)) 



-- With Nat invariant 
{-@ measure itsize :: ITree a -> Nat @-}
{-@ data size (ITree a) itsize @-}

data ITree a where 
    ILeaf :: a -> ITree a 
    INode :: (Int -> ITree a) -> ITree a 

{-@ data ITree a where 
      ILeaf :: a -> {t:ITree a  | itsize t == 0 } 
      INode :: f:(Int -> ITree a) 
            -> ITree a  @-}

{-@ imapTr :: (a -> a) -> t:ITree a -> o:ITree a / [itsize t] @-}
imapTr :: (a -> a) -> ITree a -> ITree a 
imapTr f (ILeaf x) = ILeaf $ f x 
imapTr f (INode n) = INode (\x -> imapTr f (n x))