aboutsummaryrefslogtreecommitdiff
path: root/src/Data
diff options
context:
space:
mode:
Diffstat (limited to 'src/Data')
-rw-r--r--src/Data/Expr/SharingRecovery.hs3
-rw-r--r--src/Data/Expr/SharingRecovery/Internal.hs217
2 files changed, 123 insertions, 97 deletions
diff --git a/src/Data/Expr/SharingRecovery.hs b/src/Data/Expr/SharingRecovery.hs
index 02b3e3e..95524dd 100644
--- a/src/Data/Expr/SharingRecovery.hs
+++ b/src/Data/Expr/SharingRecovery.hs
@@ -1,10 +1,13 @@
module Data.Expr.SharingRecovery (
-- * Sharing recovery
sharingRecovery,
+ sharingRecoveryUnsafe,
-- * 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 0089454..9d00355 100644
--- a/src/Data/Expr/SharingRecovery/Internal.hs
+++ b/src/Data/Expr/SharingRecovery/Internal.hs
@@ -78,7 +78,10 @@ class Functor1 f => Traversable1 f where
--
-- * @v@ is the type of variables in the expression. A PHOAS expression is
-- required to be parametric in the @v@ parameter; the only place you will
--- obtain a @v@ is inside a @PHOASLam@ function body.
+-- obtain a @v@ is inside a @PHOASLam@ function body. Even if you use
+-- 'sharingRecoveryUnsafe' which allows you to pass in a monomorphic
+-- expression with 'Tag', it is expressly disallowed to inspect or
+-- manipulate 'Tag' values.
--
-- * @f@ should be your type of operations for your language. It is indexed by
-- the type of subexpressions and the result type of the operation; thus, it
@@ -100,7 +103,7 @@ class Functor1 f => Traversable1 f where
--
-- Note furthermore that @Oper@ is /not/ a recursive type. Subexpressions
-- are again 'PHOASExpr's, and 'sharingRecovery' needs to be able to see
--- them. Hence, you should call back to back to @r@ instead of recursing
+-- them. Hence, you should call back to @r@ instead of recursing
-- manually.
--
-- * @t@ is the result type of this expression.
@@ -109,6 +112,12 @@ data PHOASExpr typ v f t where
PHOASLam :: typ (a -> b) -> typ a -> (v a -> PHOASExpr typ v f b) -> PHOASExpr typ v f (a -> b)
PHOASVar :: typ t -> v t -> PHOASExpr typ v f t
+-- | Tag values identify a variable, and are created in the sharing recovery
+-- process (in 'pruneExpr'). Applying the sharing recovery algorithm to a term
+-- with manually constructed Tag values, or inspecting Tag values in the
+-- expression and computing with them or branching based on them, results in
+-- "impossible terms" and behaviour of the sharing recovery algorithm is
+-- undefined. Consider Tag an opaque value.
newtype Tag t = Tag Natural
deriving (Show, Eq)
deriving (Hashable) via Natural
@@ -125,16 +134,26 @@ 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
-- detecting sharing for variable references, because that would only introduce
-- a redundant variable indirection.
-data PExpr typ f t where
- PStub :: NameFor typ f t -> typ t -> PExpr typ f t
- POp :: NameFor typ f t -> typ t -> f (PExpr typ f) t -> PExpr typ f t
- PLam :: NameFor typ f (a -> b) -> typ (a -> b) -> typ a -> Tag a -> PExpr typ f b -> PExpr typ f (a -> b)
- PVar :: typ a -> Tag a -> PExpr typ f a
+--
+-- This is defined as a base functor; @r@ is the recursive position.
+data PExpr r typ f t where
+ PStub :: NameFor typ f t -> typ t -> PExpr r typ f t
+ POp :: NameFor typ f t -> typ t -> f (r typ f) t -> PExpr r typ f t
+ PLam :: NameFor typ f (a -> b) -> typ (a -> b) -> typ a -> Tag a -> r typ f b -> PExpr r typ f (a -> b)
+ PVar :: typ a -> Tag a -> PExpr r typ f a
+
+-- | Fixpoint of 'PExpr'
+newtype PExpr0 typ f t = PExpr0 (PExpr PExpr0 typ f t)
data SomeNameFor typ f = forall t. SomeNameFor {-# UNPACK #-} !(NameFor typ f t)
@@ -144,19 +163,22 @@ instance Eq (SomeNameFor typ f) where
instance Hashable (SomeNameFor typ f) where
hashWithSalt salt (SomeNameFor name) = hashWithSalt salt name
-prettyPExpr :: Traversable1 f => Int -> PExpr typ f t -> ShowS
-prettyPExpr d = \case
+prettyPExpr0 :: Traversable1 f => Int -> PExpr0 typ f t -> ShowS
+prettyPExpr0 d (PExpr0 ex) = prettyPExpr prettyPExpr0 d ex
+
+prettyPExpr :: Traversable1 f => (forall a. Int -> r typ f a -> ShowS) -> Int -> PExpr r typ f t -> ShowS
+prettyPExpr recur d = \case
PStub (NameFor name) _ -> showString (showStableName name)
POp (NameFor name) _ args ->
let (argslist, _) = traverse1 (\arg -> ([Some arg], Const ())) args
- argslist' = map (\(Some arg) -> prettyPExpr 0 arg) argslist
+ argslist' = map (\(Some arg) -> recur 0 arg) argslist
in showParen (d > 10) $
showString ("<" ++ showStableName name ++ ">(")
. foldr (.) id (intersperse (showString ", ") argslist')
. showString ")"
PLam (NameFor name) _ _ (Tag tag) body ->
showParen (d > 0) $
- showString ("λ" ++ showStableName name ++ " x" ++ show tag ++ ". ") . prettyPExpr 0 body
+ showString ("λ" ++ showStableName name ++ " x" ++ show tag ++ ". ") . recur 0 body
PVar _ (Tag tag) -> showString ("x" ++ show tag)
-- | For each name:
@@ -170,13 +192,19 @@ prettyPExpr d = \case
-- Missing names have not been seen yet, and have unknown height.
type OccMap typ f = HashMap (SomeNameFor typ f) (Natural, Natural)
-pruneExpr :: Traversable1 f => (forall v. PHOASExpr typ v f t) -> (OccMap typ f, PExpr typ f t)
+pruneExpr :: Traversable1 f => (forall v. PHOASExpr typ v f t) -> (OccMap typ f, PExpr0 typ f t)
pruneExpr term =
let ((term', _), (_, mp)) = runState (pruneExpr' term) (0, mempty)
in (mp, term')
+pruneExprUnsafe :: Traversable1 f => PHOASExpr typ Tag f t -> (OccMap typ f, PExpr0 typ f t)
+pruneExprUnsafe term =
+ let ((term', _), (_, mp)) = runState (pruneExpr' term) (0, mempty)
+ in (mp, term')
+
-- | Returns pruned expression with its height.
-pruneExpr' :: Traversable1 f => PHOASExpr typ Tag f t -> State (Natural, OccMap typ f) (PExpr typ f t, Natural)
+-- State: (ID generator, occurrence map being accumulated)
+pruneExpr' :: Traversable1 f => PHOASExpr typ Tag f t -> State (Natural, OccMap typ f) (PExpr0 typ f t, Natural)
pruneExpr' = \case
orig@(PHOASOp ty args) -> do
let name = makeStableName' orig
@@ -185,7 +213,7 @@ pruneExpr' = \case
-- already visited
Just height -> do
modify (second (HM.adjust (first (+1)) (SomeNameFor (NameFor name))))
- pure (PStub (NameFor name) ty, height)
+ pure (PExpr0 (PStub (NameFor name) ty), height)
-- first visit
Nothing -> do
-- Traverse the arguments, collecting the maximum height in an
@@ -193,13 +221,14 @@ pruneExpr' = \case
(args', maxhei) <-
withMoreState 0 $
traverse1 (\arg -> do
+ -- drop the extra state for the recursive call
(arg', hei) <- withLessState id (,) (pruneExpr' arg)
- modify (second (hei `max`))
+ modify (second (hei `max`)) -- modify the extra state
return arg')
args
-- Record this node
modify (second (HM.insert (SomeNameFor (NameFor name)) (1, 1 + maxhei)))
- pure (POp (NameFor name) ty args', 1 + maxhei)
+ pure (PExpr0 (POp (NameFor name) ty args'), 1 + maxhei)
orig@(PHOASLam tyf tyarg f) -> do
let name = makeStableName' orig
@@ -208,7 +237,7 @@ pruneExpr' = \case
-- already visited
Just height -> do
modify (second (HM.adjust (first (+1)) (SomeNameFor (NameFor name))))
- pure (PStub (NameFor name) tyf, height)
+ pure (PExpr0 (PStub (NameFor name) tyf), height)
-- first visit
Nothing -> do
tag <- Tag <$> gets fst
@@ -216,45 +245,24 @@ pruneExpr' = \case
let body = f tag
(body', bodyhei) <- pruneExpr' body
modify (second (HM.insert (SomeNameFor (NameFor name)) (1, 1 + bodyhei)))
- pure (PLam (NameFor name) tyf tyarg tag body', 1 + bodyhei)
+ pure (PExpr0 (PLam (NameFor name) tyf tyarg tag body'), 1 + bodyhei)
- PHOASVar ty tag -> pure (PVar ty tag, 1)
+ PHOASVar ty tag -> pure (PExpr0 (PVar ty tag), 1)
--- | Floated expression: a bunch of to-be let bound expressions on top of an
--- LExpr'. Because LExpr' is really just PExpr with the recursive positions
--- replaced by LExpr, LExpr should be seen as PExpr with a bunch of to-be let
--- bound expressions on top of every node.
-data LExpr typ f t = LExpr [Some (LExpr typ f)] (LExpr' typ f t)
-data LExpr' typ f t where -- TODO: this could be an instantiation of (a generalisation of) PExpr
- LStub :: NameFor typ f t -> typ t -> LExpr' typ f t
- LOp :: NameFor typ f t -> typ t -> f (LExpr typ f) t -> LExpr' typ f t
- LLam :: NameFor typ f (a -> b) -> typ (a -> b) -> typ a -> Tag a -> LExpr typ f b -> LExpr' typ f (a -> b)
- LVar :: typ a -> Tag a -> LExpr' typ f a
+-- | Floated expression: again a 'PExpr' (it's a fixpoint over the same base
+-- functor), but now with a bunch of to-be let bound expressions on top of
+-- every node.
+data LExpr typ f t = LExpr [Some (LExpr typ f)] (PExpr LExpr typ f t)
prettyLExpr :: Traversable1 f => Int -> LExpr typ f t -> ShowS
-prettyLExpr d (LExpr [] e) = prettyLExpr' d e
+prettyLExpr d (LExpr [] e) = prettyPExpr prettyLExpr d e
prettyLExpr d (LExpr floated e) =
showString "["
. foldr (.) id (intersperse (showString ", ") (map (\(Some e') -> prettyLExpr 0 e') floated))
- . showString "] " . prettyLExpr' d e
-
-prettyLExpr' :: Traversable1 f => Int -> LExpr' typ f t -> ShowS
-prettyLExpr' d = \case
- LStub (NameFor name) _ -> showString (showStableName name)
- LOp (NameFor name) _ args ->
- let (argslist, _) = traverse1 (\arg -> ([Some arg], Const ())) args
- argslist' = map (\(Some arg) -> prettyLExpr 0 arg) argslist
- in showParen (d > 10) $
- showString ("<" ++ showStableName name ++ ">(")
- . foldr (.) id (intersperse (showString ", ") argslist')
- . showString ")"
- LLam (NameFor name) _ _ (Tag tag) body ->
- showParen (d > 0) $
- showString ("λ" ++ showStableName name ++ " x" ++ show tag ++ ". ") . prettyLExpr 0 body
- LVar _ (Tag tag) -> showString ("x" ++ show tag)
+ . showString "] " . prettyPExpr prettyLExpr d e
-floatExpr :: Traversable1 f => OccMap typ f -> PExpr typ f t -> LExpr typ f t
+floatExpr :: Traversable1 f => OccMap typ f -> PExpr0 typ f t -> LExpr typ f t
floatExpr totals term = snd (floatExpr' totals term)
newtype FoundMap typ f = FoundMap
@@ -269,46 +277,47 @@ instance Semigroup (FoundMap typ f) where
instance Monoid (FoundMap typ f) where
mempty = FoundMap HM.empty
-floatExpr' :: Traversable1 f => OccMap typ f -> PExpr typ f t -> (FoundMap typ f, LExpr typ f t)
-floatExpr' _totals (PStub name ty) =
- -- trace ("Found stub: " ++ (case name of NameFor n -> showStableName n)) $
- (FoundMap $ HM.singleton (SomeNameFor name) (1, Nothing)
- ,LExpr [] (LStub name ty))
+floatExpr' :: Traversable1 f => OccMap typ f -> PExpr0 typ f t -> (FoundMap typ f, LExpr typ f t)
+floatExpr' totals (PExpr0 term) = case term of
+ PStub name ty ->
+ -- trace ("Found stub: " ++ (case name of NameFor n -> showStableName n)) $
+ (FoundMap $ HM.singleton (SomeNameFor name) (1, Nothing)
+ ,LExpr [] (PStub name ty))
-floatExpr' _totals (PVar ty tag) =
- -- trace ("Found var: " ++ show tag) $
- (mempty, LExpr [] (LVar ty tag))
+ PVar ty tag ->
+ -- trace ("Found var: " ++ show tag) $
+ (mempty, LExpr [] (PVar ty tag))
-floatExpr' totals term =
- let (FoundMap foundmap, name, termty, term') = case term of
- POp n ty args ->
- let (fm, args') = traverse1 (floatExpr' totals) args
- in (fm, n, ty, LOp n ty args')
- PLam n tyf tyarg tag body ->
- let (fm, body') = floatExpr' totals body
- in (fm, n, tyf, LLam n tyf tyarg tag body')
+ _ ->
+ let (FoundMap foundmap, name, termty, term') = case term of
+ POp n ty args ->
+ let (fm, args') = traverse1 (floatExpr' totals) args
+ in (fm, n, ty, POp n ty args')
+ PLam n tyf tyarg tag body ->
+ let (fm, body') = floatExpr' totals body
+ in (fm, n, tyf, PLam n tyf tyarg tag body')
- -- TODO: perhaps this HM.toList together with the foldr HM.delete can be a single traversal of the HashMap
- saturated = [case mterm of
- Just t -> (nm, t)
- Nothing -> case nm of
- SomeNameFor (NameFor n) ->
- error $ "Name saturated (count=" ++ show count ++ ", totalcount=" ++ show totalcount ++ ") but no term found: " ++ showStableName n
- | (nm, (count, mterm)) <- HM.toList foundmap
- , let totalcount = fromMaybe 0 (fst <$> HM.lookup nm totals)
- , count == totalcount]
+ -- TODO: perhaps this HM.toList together with the foldr HM.delete can be a single traversal of the HashMap
+ saturated = [case mterm of
+ Just t -> (nm, t)
+ Nothing -> case nm of
+ SomeNameFor (NameFor n) ->
+ error $ "Name saturated (count=" ++ show count ++ ", totalcount=" ++ show totalcount ++ ") but no term found: " ++ showStableName n
+ | (nm, (count, mterm)) <- HM.toList foundmap
+ , let totalcount = fromMaybe 0 (fst <$> HM.lookup nm totals)
+ , count == totalcount]
- foundmap' = foldr HM.delete foundmap (map fst saturated)
+ foundmap' = foldr HM.delete foundmap (map fst saturated)
- lterm = LExpr (map fst (sortBy (comparing snd) (map snd saturated))) term'
+ lterm = LExpr (map fst (sortBy (comparing snd) (map snd saturated))) term'
- in case HM.findWithDefault (0, undefined) (SomeNameFor name) totals of
- (1, _) -> (FoundMap foundmap', lterm)
- (tot, height)
- | tot > 1 -> -- trace ("Inserting " ++ (case name of NameFor n -> showStableName n) ++ " into foundmap") $
- (FoundMap (HM.insert (SomeNameFor name) (1, Just (Some lterm, height)) foundmap')
- ,LExpr [] (LStub name termty))
- | otherwise -> error "Term does not exist, yet we have it in hand"
+ in case HM.findWithDefault (0, undefined) (SomeNameFor name) totals of
+ (1, _) -> (FoundMap foundmap', lterm)
+ (tot, height)
+ | tot > 1 -> -- trace ("Inserting " ++ (case name of NameFor n -> showStableName n) ++ " into foundmap") $
+ (FoundMap (HM.insert (SomeNameFor name) (1, Just (Some lterm, height)) foundmap')
+ ,LExpr [] (PStub name termty))
+ | otherwise -> error "Term does not exist, yet we have it in hand"
-- | Untyped De Bruijn expression. No more names: there are lets now, and
@@ -342,15 +351,15 @@ lowerExpr' namelvl taglvl curlvl (LExpr floated ex) =
curlvl' = curlvl + length floated
in prefix $
case ex of
- LStub name ty ->
+ PStub name ty ->
case HM.lookup (SomeNameFor name) namelvl' of
Just lvl -> UBVar ty (curlvl - lvl - 1)
Nothing -> error "Name variable out of scope"
- LOp _ ty args ->
+ POp _ ty args ->
UBOp ty (fmap1 (lowerExpr' namelvl' taglvl curlvl') args)
- LLam _ tyf tyarg tag body ->
+ PLam _ tyf tyarg tag body ->
UBLam tyf tyarg (lowerExpr' namelvl' (HM.insert (SomeTag tag) curlvl' taglvl) (curlvl' + 1) body)
- LVar ty tag ->
+ PVar ty tag ->
case HM.lookup (SomeTag tag) taglvl of
Just lvl -> UBVar ty (curlvl - lvl - 1)
Nothing -> error "Tag variable out of scope"
@@ -363,17 +372,17 @@ lowerExpr' namelvl taglvl curlvl (LExpr floated ex) =
buildPrefix namelvl' _ [] = (namelvl', id)
buildPrefix namelvl' lvl (Some rhs@(LExpr _ rhs') : rhss) =
let name = case rhs' of
- LStub n _ -> n
- LOp n _ _ -> n
- LLam n _ _ _ _ -> n
- LVar _ _ -> error "Recovering sharing of a tag is useless"
+ PStub n _ -> n
+ POp n _ _ -> n
+ PLam n _ _ _ _ -> n
+ PVar _ _ -> error "Recovering sharing of a tag is useless"
ty = case rhs' of
- LStub{} -> error "Recovering sharing of a stub is useless"
- LOp _ t _ -> t
- LLam _ t _ _ _ -> t
- LVar t _ -> t
+ PStub{} -> error "Recovering sharing of a stub is useless"
+ POp _ t _ -> t
+ PLam _ t _ _ _ -> t
+ PVar t _ -> t
prefix = UBLet ty (lowerExpr' namelvl' taglvl lvl rhs)
- in (prefix .) <$> buildPrefix (HM.insert (SomeNameFor name) lvl namelvl') (lvl + 1) rhss
+ in second (prefix .) $ buildPrefix (HM.insert (SomeNameFor name) lvl namelvl') (lvl + 1) rhss
-- | A typed De Bruijn index.
@@ -399,7 +408,7 @@ envLookupU = go id
go f 0 (EPush _ t) = Just (Some (Pair t (f IZ)))
go f i (EPush e _) = go (f . IS) (i - 1) e
--- | Typed De Bruijn expression. This is the resu,t of sharing recovery. It is
+-- | Typed De Bruijn expression. This is the result of sharing recovery. It is
-- not higher-order any more, and furthermore has explicit let-bindings ('BLet')
-- that denote the sharing inside the term. This is a normal AST.
--
@@ -418,6 +427,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
@@ -466,8 +481,16 @@ retypeExpr' env (UBVar ty idx) =
-- abstract syntax form to a well-typed well-scoped De Bruijn expression with
-- explicit let-bindings.
sharingRecovery :: (Traversable1 f, TestEquality typ) => (forall v. PHOASExpr typ v f t) -> BExpr typ '[] f t
-sharingRecovery e =
- let (occmap, pexpr) = pruneExpr e
+sharingRecovery = sharingRecoveryUnsafe
+
+-- | The 'sharingRecovery' function instantiates the @v@ parameter to 'Tag',
+-- and this function is provided as a convenience in case constructing a
+-- polymorphic expression value is difficult. However, it is /disallowed/ to
+-- inspect or manipulate 'Tag' values obtained by lambda abstraction inside the
+-- expression. Violating this rule results in undefined behaviour.
+sharingRecoveryUnsafe :: (Traversable1 f, TestEquality typ) => PHOASExpr typ Tag f t -> BExpr typ '[] f t
+sharingRecoveryUnsafe e =
+ let (occmap, pexpr) = pruneExprUnsafe e
lexpr = floatExpr occmap pexpr
ubexpr = lowerExpr lexpr
in -- trace ("PExpr: " ++ prettyPExpr 0 pexpr "") $
generated by cgit v1.2.3-70-g09d2 (git 2.51.2) at 2025-12-15 10:02:35 +0100