From 1931c68ae2b9add3235b729b194ef4b4ce6938af Mon Sep 17 00:00:00 2001 From: Tom Smeding Date: Fri, 3 Oct 2025 23:06:05 +0200 Subject: Add typeOf functions --- src/Data/Expr/SharingRecovery.hs | 2 ++ src/Data/Expr/SharingRecovery/Internal.hs | 11 +++++++++++ 2 files changed, 13 insertions(+) diff --git a/src/Data/Expr/SharingRecovery.hs b/src/Data/Expr/SharingRecovery.hs index 02b3e3e..34fd4ec 100644 --- a/src/Data/Expr/SharingRecovery.hs +++ b/src/Data/Expr/SharingRecovery.hs @@ -4,7 +4,9 @@ module Data.Expr.SharingRecovery ( -- * Expressions PHOASExpr(..), + typeOfPHOAS, BExpr(..), + typeOfBExpr, Idx(..), -- * Traversing indexed structures diff --git a/src/Data/Expr/SharingRecovery/Internal.hs b/src/Data/Expr/SharingRecovery/Internal.hs index 9f7ca7d..adf655d 100644 --- a/src/Data/Expr/SharingRecovery/Internal.hs +++ b/src/Data/Expr/SharingRecovery/Internal.hs @@ -125,6 +125,11 @@ instance TestEquality (NameFor typ f) where unsafeCoerceRefl :: a :~: b -- restricted version of unsafeCoerce that only allows punting proofs unsafeCoerceRefl = unsafeCoerce Refl +typeOfPHOAS :: PHOASExpr typ v f t -> typ t +typeOfPHOAS (PHOASOp ty _) = ty +typeOfPHOAS (PHOASLam ty _ _) = ty +typeOfPHOAS (PHOASVar ty _) = ty + -- | Pruned expression. -- -- Note that variables do not, and will never, have a name: we don't bother @@ -408,6 +413,12 @@ data BExpr typ env f t where deriving instance (forall a. Show (typ a), forall a r. (forall b. Show (r b)) => Show (f r a)) => Show (BExpr typ env f t) +typeOfBExpr :: BExpr typ v f t -> typ t +typeOfBExpr (BOp ty _) = ty +typeOfBExpr (BLam ty _ _) = ty +typeOfBExpr (BLet _ _ e) = typeOfBExpr e +typeOfBExpr (BVar ty _) = ty + prettyBExpr :: (forall m env' a. Monad m => (forall b. Int -> BExpr typ env' f b -> m ShowS) -> Int -> f (BExpr typ env' f) a -> m ShowS) -> BExpr typ '[] f t -> String -- cgit v1.2.3-70-g09d2