Skip to content

Instantly share code, notes, and snippets.

@xgrommx
Created July 8, 2021 10:49
Show Gist options
  • Save xgrommx/cdc576b0b6be882efae1776c018c1fb4 to your computer and use it in GitHub Desktop.
Save xgrommx/cdc576b0b6be882efae1776c018c1fb4 to your computer and use it in GitHub Desktop.
Main
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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment