tress.idr

import Data.Vect

data Ast a = ASTLeaf a | NonASTLeaf a (Vect k $ Ast a)

data TypedAst : Type where
  LLeaf    : (a : String) -> TypedAst
  NonTLeaf : (a : String) -> Vect k TypedAst -> TypedAst

Op : Type
data IR = IRLeaf Op | NonLeaf Op (Vect k IR)

data TreeLike : Type -> Type where
  Leaf : (e) -> TreeLike e
  Node : (e) -> Vect (S k) (TreeLike e) -> TreeLike e

convertAST : Ast a -> TreeLike a
convertAST (ASTLeaf x) = Leaf x
convertAST (NonASTLeaf x []) = Leaf x
convertAST (NonASTLeaf x (y :: xs)) = Node x (map convertAST (y :: xs))

interface ASTConvertible (tree : Type -> Type)  where
  convertTree : (tree k) -> TreeLike k

ASTConvertible TreeLike where
  convertTree = id

ASTConvertible Ast where
  convertTree = convertAST

LiftedTypedAst : a -> Type
LiftedTypedAst x = TypedAst

data LiftConstructor : Type -> Type where
  Lift : TypedAst -> LiftConstructor String

ASTConvertible LiftConstructor where
  convertTree (Lift (LLeaf a)) = Leaf a
  convertTree (Lift (NonTLeaf a [])) = Leaf a
  convertTree (Lift (NonTLeaf a (x :: xs))) = Node a (map (convertTree . Lift) (x :: xs))


countViewAST : ASTConvertible tree => tree a -> Integer
countViewAST x with (convertTree x)
  countViewAST x | (Leaf y) = 1
  countViewAST x | (Node y xs) = let counts = map countViewAST xs in
                                     foldr (+) 1 counts