aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorTom Smeding <t.j.smeding@uu.nl>2024-08-28 16:12:15 +0200
committerTom Smeding <t.j.smeding@uu.nl>2024-08-28 16:12:15 +0200
commit2870da310256a137971a6a661801dcdf9dedd818 (patch)
treed55359df3d6d1f9b25a9a0bee8e5f636277972da /src
parent5a0ce21e12e765125ad8068e919cf97b70df8257 (diff)
Rename "lifting" to "floating"
The paper calls it floating, and that's a less overloaded term.
Diffstat (limited to 'src')
-rw-r--r--src/Data/Expr/SharingRecovery.hs34
1 files changed, 16 insertions, 18 deletions
diff --git a/src/Data/Expr/SharingRecovery.hs b/src/Data/Expr/SharingRecovery.hs
index f9d27e6..d7d2313 100644
--- a/src/Data/Expr/SharingRecovery.hs
+++ b/src/Data/Expr/SharingRecovery.hs
@@ -183,9 +183,7 @@ pruneExpr' = \case
PHOASVar ty tag -> pure (PVar ty tag, 1)
--- TODO: Replace "lift" with "float"
-
--- | Lifted expression: a bunch of to-be let bound expressions on top of an
+-- | 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.
@@ -198,9 +196,9 @@ data LExpr' typ f t where -- TODO: this could be an instantiation of (a general
prettyLExpr :: Traversable1 f => Int -> LExpr typ f t -> ShowS
prettyLExpr d (LExpr [] e) = prettyLExpr' d e
-prettyLExpr d (LExpr lifted e) =
+prettyLExpr d (LExpr floated e) =
showString "["
- . foldr (.) id (intersperse (showString ", ") (map (\(Some e') -> prettyLExpr 0 e') lifted))
+ . foldr (.) id (intersperse (showString ", ") (map (\(Some e') -> prettyLExpr 0 e') floated))
. showString "] " . prettyLExpr' d e
prettyLExpr' :: Traversable1 f => Int -> LExpr' typ f t -> ShowS
@@ -218,13 +216,13 @@ prettyLExpr' d = \case
showString ("λ" ++ showStableName name ++ " x" ++ show tag ++ ". ") . prettyLExpr 0 body
LVar _ (Tag tag) -> showString ("x" ++ show tag)
-liftExpr :: Traversable1 f => OccMap typ f -> PExpr typ f t -> LExpr typ f t
-liftExpr totals term = snd (liftExpr' totals term)
+floatExpr :: Traversable1 f => OccMap typ f -> PExpr typ f t -> LExpr typ f t
+floatExpr totals term = snd (floatExpr' totals term)
newtype FoundMap typ f = FoundMap
(HashMap (SomeNameFor typ f)
(Natural -- how many times seen
- ,Maybe (Some (LExpr typ f), Natural))) -- the lifted subterm with its height (once seen)
+ ,Maybe (Some (LExpr typ f), Natural))) -- the floated subterm with its height (once seen)
instance Semigroup (FoundMap typ f) where
FoundMap m1 <> FoundMap m2 = FoundMap $
@@ -233,23 +231,23 @@ instance Semigroup (FoundMap typ f) where
instance Monoid (FoundMap typ f) where
mempty = FoundMap HM.empty
-liftExpr' :: Traversable1 f => OccMap typ f -> PExpr typ f t -> (FoundMap typ f, LExpr typ f t)
-liftExpr' _totals (PStub name ty) =
+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))
-liftExpr' _totals (PVar ty tag) =
+floatExpr' _totals (PVar ty tag) =
-- trace ("Found var: " ++ show tag) $
(mempty, LExpr [] (LVar ty tag))
-liftExpr' totals term =
+floatExpr' totals term =
let (FoundMap foundmap, name, termty, term') = case term of
POp n ty args ->
- let (fm, args') = traverse1 (liftExpr' totals) 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') = liftExpr' totals body
+ let (fm, body') = floatExpr' totals body
in (fm, n, tyf, LLam n tyf tyarg tag body')
-- TODO: perhaps this HM.toList together with the foldr HM.delete can be a single traversal of the HashMap
@@ -301,9 +299,9 @@ lowerExpr' :: forall typ f t. Functor1 f
-> HashMap SomeTag Int -- ^ tag |-> De Bruijn level of defining binding
-> Int -- ^ Number of variables already in scope
-> LExpr typ f t -> UBExpr typ f t
-lowerExpr' namelvl taglvl curlvl (LExpr lifted ex) =
- let (namelvl', prefix) = buildPrefix namelvl curlvl lifted
- curlvl' = curlvl + length lifted
+lowerExpr' namelvl taglvl curlvl (LExpr floated ex) =
+ let (namelvl', prefix) = buildPrefix namelvl curlvl floated
+ curlvl' = curlvl + length floated
in prefix $
case ex of
LStub name ty ->
@@ -418,7 +416,7 @@ retypeExpr' env (UBVar ty idx) =
sharingRecovery :: (Traversable1 f, TestEquality typ) => (forall v. PHOASExpr typ v f t) -> BExpr typ '[] f t
sharingRecovery e =
let (occmap, pexpr) = pruneExpr e
- lexpr = liftExpr occmap pexpr
+ lexpr = floatExpr occmap pexpr
ubexpr = lowerExpr lexpr
in -- trace ("PExpr: " ++ prettyPExpr 0 pexpr "") $
-- trace ("LExpr: " ++ prettyLExpr 0 lexpr "") $