Cofree Annotation

走り書きメモ

code:Expr.hs

module Expr

where

import Numeric.Natural

import Data.Functor.Foldable

import Control.Comonad.Cofree

import Control.Comonad.Trans.Cofree ( headF, tailF )

import GHC.Generics

data Term

= TmTrue

| TmFalse

| TmZero

| TmSucc Term

| TmPred Term

| TmIsZero Term

| TmIf Term Term Term

deriving ( Generic, Eq, Show )

dispatchOnTerm

:: b

-> b

-> b

-> (Term -> b)

-> (Term -> b)

-> (Term -> b)

-> (Term -> Term -> Term -> b)

-> (Term -> b)

dispatchOnTerm atTrue atFalse atZero atSucc atPred atIsZero atIf

= \ case

TmTrue -> atTrue

TmFalse -> atFalse

TmZero -> atZero

TmSucc s -> atSucc s

TmPred s -> atPred s

TmIsZero s -> atIsZero s

TmIf s t u -> atIf s t u

data TermF r

= TmTrueF

| TmFalseF

| TmIfF r r r

| TmZeroF

| TmSuccF r

| TmPredF r

| TmIsZeroF r

deriving ( Generic, Functor, Foldable, Traversable )

dispatchOnTermF

:: b

-> b

-> b

-> (a -> b)

-> (a -> b)

-> (a -> b)

-> (a -> a -> a -> b)

-> (TermF a -> b)

dispatchOnTermF atTrue atFalse atZero atSucc atPred atIsZero atIf

= \ case

TmTrueF -> atTrue

TmFalseF -> atFalse

TmZeroF -> atZero

TmSuccF s -> atSucc s

TmPredF s -> atPred s

TmIsZeroF s -> atIsZero s

TmIfF s t u -> atIf s t u

type instance Base Term = TermF

instance Recursive Term where

project = dispatchOnTerm TmTrueF TmFalseF TmZeroF TmSuccF TmPredF TmIsZeroF TmIfF

instance Corecursive Term where

embed = dispatchOnTermF TmTrue TmFalse TmZero TmSucc TmPred TmIsZero TmIf

size :: Term -> Natural

size = cata sizeF

sizeF :: TermF Natural -> Natural

sizeF = dispatchOnTermF (succ 0) (succ 0) (succ 0) succ succ succ (\ i j k -> succ (i + j + k))

depth :: Term -> Natural

depth = cata depthF

depthF :: TermF Natural -> Natural

depthF = dispatchOnTermF

(succ 0)

(succ 0)

(succ 0)

succ

succ

succ

type AnnTerm = Cofree TermF

size' :: AnnTerm a -> Natural

size' = cata (sizeF . tailF)

depth' :: AnnTerm a -> Natural

depth' = cata (depthF . tailF)

type ATerm = AnnTerm Info

type Info = Int -- e.g. line number in concrete syntax