Main

Main.purs

module Main where

import Prelude
import Type.Proxy
import Prim.Boolean as Boolean
import Type.Data.Peano as Peano
import Type.Data.Boolean (class If)
import Type.Data.Ordering (class Equals)
import Prim.Ordering (LT)

type TypeNatExpr :: forall k. k -> k -> Type
type TypeNatExpr k1 k2 = Proxy k1 -> Proxy k2 -> Type

infixr 4 type TypeNatExpr as ~>

class TNatEval :: forall f g a. (f ~> g) -> f a -> g a -> Constraint
class TNatEval nat f g | nat f -> g

proxyTNatEval :: forall nat f g. TNatEval nat f g => Proxy nat -> Proxy f -> Proxy g
proxyTNatEval _ _ = Proxy

foreign import data HTProject :: forall t h. t ~> h t

foreign import data HCata :: forall h f t. (t f ~> f) -> h ~> f

foreign import data HFMap :: forall h f g. (f ~> g) -> h f ~> h g

instance (TNatEval HTProject x p, TNatEval (HFMap (HCata halg)) p c, TNatEval halg c r) => TNatEval (HCata halg) x r

data Expr :: forall k. k -> Type
data Expr e

foreign import data ELit :: Peano.Nat -> Expr Peano.Nat
foreign import data EBool :: Boolean -> Expr Boolean
foreign import data EAdd :: Expr Peano.Nat -> Expr Peano.Nat -> Expr Peano.Nat
foreign import data ELessThan :: Expr Peano.Nat -> Expr Peano.Nat -> Expr Boolean
foreign import data EIf :: forall a. Expr Boolean -> Expr a -> Expr a -> Expr a

data ExprF :: forall k. (k -> Type) -> k -> Type
data ExprF a b

foreign import data ELitF :: forall h. Peano.Nat -> ExprF h Peano.Nat
foreign import data EBoolF :: forall h. Boolean -> ExprF h Boolean
foreign import data EAddF :: forall h. h Peano.Nat -> h Peano.Nat -> ExprF h Peano.Nat
foreign import data ELessThanF :: forall h. h Peano.Nat -> h Peano.Nat -> ExprF h Boolean
foreign import data EIfF :: forall h a. h Boolean -> h a -> h a -> ExprF h a

instance TNatEval (HFMap f) (ELitF x) (ELitF x)
instance TNatEval (HFMap f) (EBoolF x) (EBoolF x)
instance (TNatEval f x x', TNatEval f y y') => TNatEval (HFMap f) (EAddF x y) (EAddF x' y')
instance (TNatEval f x x', TNatEval f y y') => TNatEval (HFMap f) (ELessThanF x y) (ELessThanF x' y')
instance (TNatEval f x x', TNatEval f y y', TNatEval f z z') => TNatEval (HFMap f) (EIfF x y z) (EIfF x' y' z')

instance TNatEval HTProject (ELit a) (ELitF a)
instance TNatEval HTProject (EBool b) (EBoolF b)
instance TNatEval HTProject (EAdd x y) (EAddF x y)
instance TNatEval HTProject (ELessThan x y) (ELessThanF x y)
instance TNatEval HTProject (EIf c t f) (EIfF c t f)

data Value :: forall k. k -> Type
data Value a

foreign import data VInt :: Peano.Nat -> Value Peano.Nat
foreign import data VBool :: Boolean -> Value Boolean

foreign import data ExprVHAlg :: ExprF Value ~> Value

instance TNatEval ExprVHAlg (ELitF n) (VInt n)
instance TNatEval ExprVHAlg (EBoolF n) (VBool n)
instance (Peano.SumNat x y z) => TNatEval ExprVHAlg (EAddF (VInt x) (VInt y)) (VInt z)
instance (Peano.CompareNat x y z, Equals z LT t) => TNatEval ExprVHAlg (ELessThanF (VInt x) (VInt y)) (VBool t)
instance If c t f z => TNatEval ExprVHAlg (EIfF (VBool c) t f) z

foreign import data ExprV :: Expr ~> Value

instance TNatEval (HCata ExprVHAlg) t q => TNatEval ExprV t q

type E = EIf (EBool Boolean.False) (ELit Peano.D1) (EAdd (ELit Peano.D42) (ELit Peano.D45))

type T :: Value Peano.Nat
type T = VInt Peano.D87

e :: Proxy T
e = proxyTNatEval (Proxy :: _ ExprV) (Proxy :: _ E)