Skip to content

Commit

Permalink
Generate fewer defunctionalization symbols for local definitions
Browse files Browse the repository at this point in the history 
We can exploit the fact that defunctionalization symbols are never partially
applied to local variables to generate fewer defunctionalization symbols for
definitions where local variables are in scope. I've written up the details in
a new part of `Note [Defunctionalization game plan] (Wrinkle 1: Partial kinds)`
in `D.S.TH.Promote.Defun`.

This has no effect on any user-visible behavior—it is just an optimization.

Fixes #592.
  • Loading branch information
@RyanGlScott
RyanGlScott committed May 19, 2024
1 parent 33f2992 commit 755da39
Show file tree
Hide file tree
Showing 24 changed files with 798 additions and 2,287 deletions.
54 changes: 5 additions & 49 deletions singletons-base/tests/compile-and-dump/GradingClient/Database.golden
View file
Original file line number Diff line number Diff line change
Expand Up @@ -405,52 +405,8 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
type SchSym1 :: [Attribute] -> Schema
type family SchSym1 (a0123456789876543210 :: [Attribute]) :: Schema where
SchSym1 a0123456789876543210 = Sch a0123456789876543210
data Let0123456789876543210Scrutinee_0123456789876543210Sym0 name0123456789876543210
where
Let0123456789876543210Scrutinee_0123456789876543210Sym0KindInference :: SameKind (Apply Let0123456789876543210Scrutinee_0123456789876543210Sym0 arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym1 arg) =>
Let0123456789876543210Scrutinee_0123456789876543210Sym0 name0123456789876543210
type instance Apply Let0123456789876543210Scrutinee_0123456789876543210Sym0 name0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210Sym1 name0123456789876543210
instance SuppressUnusedWarnings Let0123456789876543210Scrutinee_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd
((,)
Let0123456789876543210Scrutinee_0123456789876543210Sym0KindInference
())
data Let0123456789876543210Scrutinee_0123456789876543210Sym1 name0123456789876543210 name'0123456789876543210
where
Let0123456789876543210Scrutinee_0123456789876543210Sym1KindInference :: SameKind (Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym1 name0123456789876543210) arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym2 name0123456789876543210 arg) =>
Let0123456789876543210Scrutinee_0123456789876543210Sym1 name0123456789876543210 name'0123456789876543210
type instance Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym1 name0123456789876543210) name'0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210Sym2 name0123456789876543210 name'0123456789876543210
instance SuppressUnusedWarnings (Let0123456789876543210Scrutinee_0123456789876543210Sym1 name0123456789876543210) where
suppressUnusedWarnings
= snd
((,)
Let0123456789876543210Scrutinee_0123456789876543210Sym1KindInference
())
data Let0123456789876543210Scrutinee_0123456789876543210Sym2 name0123456789876543210 name'0123456789876543210 u0123456789876543210
where
Let0123456789876543210Scrutinee_0123456789876543210Sym2KindInference :: SameKind (Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym2 name0123456789876543210 name'0123456789876543210) arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym3 name0123456789876543210 name'0123456789876543210 arg) =>
Let0123456789876543210Scrutinee_0123456789876543210Sym2 name0123456789876543210 name'0123456789876543210 u0123456789876543210
type instance Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym2 name0123456789876543210 name'0123456789876543210) u0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210Sym3 name0123456789876543210 name'0123456789876543210 u0123456789876543210
instance SuppressUnusedWarnings (Let0123456789876543210Scrutinee_0123456789876543210Sym2 name0123456789876543210 name'0123456789876543210) where
suppressUnusedWarnings
= snd
((,)
Let0123456789876543210Scrutinee_0123456789876543210Sym2KindInference
())
data Let0123456789876543210Scrutinee_0123456789876543210Sym3 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210
where
Let0123456789876543210Scrutinee_0123456789876543210Sym3KindInference :: SameKind (Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym3 name0123456789876543210 name'0123456789876543210 u0123456789876543210) arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym4 name0123456789876543210 name'0123456789876543210 u0123456789876543210 arg) =>
Let0123456789876543210Scrutinee_0123456789876543210Sym3 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210
type instance Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym3 name0123456789876543210 name'0123456789876543210 u0123456789876543210) attrs0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210
instance SuppressUnusedWarnings (Let0123456789876543210Scrutinee_0123456789876543210Sym3 name0123456789876543210 name'0123456789876543210 u0123456789876543210) where
suppressUnusedWarnings
= snd
((,)
Let0123456789876543210Scrutinee_0123456789876543210Sym3KindInference
())
type family Let0123456789876543210Scrutinee_0123456789876543210Sym4 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210 where
Let0123456789876543210Scrutinee_0123456789876543210Sym4 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210
type family Let0123456789876543210Scrutinee_0123456789876543210Sym0 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210 where
Let0123456789876543210Scrutinee_0123456789876543210Sym0 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210
type family Let0123456789876543210Scrutinee_0123456789876543210 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210 where
Let0123456789876543210Scrutinee_0123456789876543210 name name' u attrs = Apply (Apply (==@#@$) name) name'
type family Case_0123456789876543210 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210 t where
Expand Down Expand Up @@ -554,7 +510,7 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
type Lookup :: [AChar] -> Schema -> U
type family Lookup (a :: [AChar]) (a :: Schema) :: U where
Lookup _ (Sch '[]) = UndefinedSym0
Lookup name (Sch ('(:) (Attr name' u) attrs)) = Case_0123456789876543210 name name' u attrs (Let0123456789876543210Scrutinee_0123456789876543210Sym4 name name' u attrs)
Lookup name (Sch ('(:) (Attr name' u) attrs)) = Case_0123456789876543210 name name' u attrs (Let0123456789876543210Scrutinee_0123456789876543210Sym0 name name' u attrs)
type Occurs :: [AChar] -> Schema -> Bool
type family Occurs (a :: [AChar]) (a :: Schema) :: Bool where
Occurs _ (Sch '[]) = FalseSym0
Expand Down Expand Up @@ -1446,12 +1402,12 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
(sAttrs :: Sing attrs)))
= let
sScrutinee_0123456789876543210 ::
Sing @_ (Let0123456789876543210Scrutinee_0123456789876543210Sym4 name name' u attrs)
Sing @_ (Let0123456789876543210Scrutinee_0123456789876543210Sym0 name name' u attrs)
sScrutinee_0123456789876543210
= applySing (applySing (singFun2 @(==@#@$) (%==)) sName) sName'
in
GHC.Internal.Base.id
@(Sing (Case_0123456789876543210 name name' u attrs (Let0123456789876543210Scrutinee_0123456789876543210Sym4 name name' u attrs)))
@(Sing (Case_0123456789876543210 name name' u attrs (Let0123456789876543210Scrutinee_0123456789876543210Sym0 name name' u attrs)))
(case sScrutinee_0123456789876543210 of
STrue -> sU
SFalse
Expand Down
43 changes: 5 additions & 38 deletions singletons-base/tests/compile-and-dump/InsertionSort/InsertionSortImp.golden
View file
Original file line number Diff line number Diff line change
Expand Up @@ -61,41 +61,8 @@ InsertionSort/InsertionSortImp.hs:(0,0)-(0,0): Splicing declarations
insertionSort :: [Nat] -> [Nat]
insertionSort [] = []
insertionSort (h : t) = insert h (insertionSort t)
data Let0123456789876543210Scrutinee_0123456789876543210Sym0 n0123456789876543210
where
Let0123456789876543210Scrutinee_0123456789876543210Sym0KindInference :: SameKind (Apply Let0123456789876543210Scrutinee_0123456789876543210Sym0 arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym1 arg) =>
Let0123456789876543210Scrutinee_0123456789876543210Sym0 n0123456789876543210
type instance Apply Let0123456789876543210Scrutinee_0123456789876543210Sym0 n0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210Sym1 n0123456789876543210
instance SuppressUnusedWarnings Let0123456789876543210Scrutinee_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd
((,)
Let0123456789876543210Scrutinee_0123456789876543210Sym0KindInference
())
data Let0123456789876543210Scrutinee_0123456789876543210Sym1 n0123456789876543210 h0123456789876543210
where
Let0123456789876543210Scrutinee_0123456789876543210Sym1KindInference :: SameKind (Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym1 n0123456789876543210) arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym2 n0123456789876543210 arg) =>
Let0123456789876543210Scrutinee_0123456789876543210Sym1 n0123456789876543210 h0123456789876543210
type instance Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym1 n0123456789876543210) h0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210Sym2 n0123456789876543210 h0123456789876543210
instance SuppressUnusedWarnings (Let0123456789876543210Scrutinee_0123456789876543210Sym1 n0123456789876543210) where
suppressUnusedWarnings
= snd
((,)
Let0123456789876543210Scrutinee_0123456789876543210Sym1KindInference
())
data Let0123456789876543210Scrutinee_0123456789876543210Sym2 n0123456789876543210 h0123456789876543210 t0123456789876543210
where
Let0123456789876543210Scrutinee_0123456789876543210Sym2KindInference :: SameKind (Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym2 n0123456789876543210 h0123456789876543210) arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym3 n0123456789876543210 h0123456789876543210 arg) =>
Let0123456789876543210Scrutinee_0123456789876543210Sym2 n0123456789876543210 h0123456789876543210 t0123456789876543210
type instance Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym2 n0123456789876543210 h0123456789876543210) t0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210 n0123456789876543210 h0123456789876543210 t0123456789876543210
instance SuppressUnusedWarnings (Let0123456789876543210Scrutinee_0123456789876543210Sym2 n0123456789876543210 h0123456789876543210) where
suppressUnusedWarnings
= snd
((,)
Let0123456789876543210Scrutinee_0123456789876543210Sym2KindInference
())
type family Let0123456789876543210Scrutinee_0123456789876543210Sym3 n0123456789876543210 h0123456789876543210 t0123456789876543210 where
Let0123456789876543210Scrutinee_0123456789876543210Sym3 n0123456789876543210 h0123456789876543210 t0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210 n0123456789876543210 h0123456789876543210 t0123456789876543210
type family Let0123456789876543210Scrutinee_0123456789876543210Sym0 n0123456789876543210 h0123456789876543210 t0123456789876543210 where
Let0123456789876543210Scrutinee_0123456789876543210Sym0 n0123456789876543210 h0123456789876543210 t0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210 n0123456789876543210 h0123456789876543210 t0123456789876543210
type family Let0123456789876543210Scrutinee_0123456789876543210 n0123456789876543210 h0123456789876543210 t0123456789876543210 where
Let0123456789876543210Scrutinee_0123456789876543210 n h t = Apply (Apply LeqSym0 n) h
type family Case_0123456789876543210 n0123456789876543210 h0123456789876543210 t0123456789876543210 t where
Expand Down Expand Up @@ -158,7 +125,7 @@ InsertionSort/InsertionSortImp.hs:(0,0)-(0,0): Splicing declarations
type Insert :: Nat -> [Nat] -> [Nat]
type family Insert (a :: Nat) (a :: [Nat]) :: [Nat] where
Insert n '[] = Apply (Apply (:@#@$) n) NilSym0
Insert n ('(:) h t) = Case_0123456789876543210 n h t (Let0123456789876543210Scrutinee_0123456789876543210Sym3 n h t)
Insert n ('(:) h t) = Case_0123456789876543210 n h t (Let0123456789876543210Scrutinee_0123456789876543210Sym0 n h t)
type Leq :: Nat -> Nat -> Bool
type family Leq (a :: Nat) (a :: Nat) :: Bool where
Leq 'Zero _ = TrueSym0
Expand All @@ -185,12 +152,12 @@ InsertionSort/InsertionSortImp.hs:(0,0)-(0,0): Splicing declarations
sInsert (sN :: Sing n) (SCons (sH :: Sing h) (sT :: Sing t))
= let
sScrutinee_0123456789876543210 ::
Sing @_ (Let0123456789876543210Scrutinee_0123456789876543210Sym3 n h t)
Sing @_ (Let0123456789876543210Scrutinee_0123456789876543210Sym0 n h t)
sScrutinee_0123456789876543210
= applySing (applySing (singFun2 @LeqSym0 sLeq) sN) sH
in
id
@(Sing (Case_0123456789876543210 n h t (Let0123456789876543210Scrutinee_0123456789876543210Sym3 n h t)))
@(Sing (Case_0123456789876543210 n h t (Let0123456789876543210Scrutinee_0123456789876543210Sym0 n h t)))
(case sScrutinee_0123456789876543210 of
STrue
-> applySing
Expand Down
Loading

0 comments on commit 755da39

Please sign in to comment.