Skip to content

Commit

Permalink
WIP
Browse files Browse the repository at this point in the history
  • Loading branch information
@dougalm
dougalm committed Oct 25, 2023
1 parent d80f318 commit 8dd4017
Show file tree
Hide file tree
Showing 8 changed files with 740 additions and 837 deletions.
192 changes: 92 additions & 100 deletions src/lib/Builder.hs
View file

Large diffs are not rendered by default.

281 changes: 130 additions & 151 deletions src/lib/CheapReduction.hs
View file

Large diffs are not rendered by default.

35 changes: 4 additions & 31 deletions src/lib/Core.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -428,33 +428,6 @@ fromNaryForExpr maxDepth = \case
return (d + 1, LamExpr (Nest b bs) body2)
_ -> Nothing

mkConsListTy :: [Type r n] -> Type r n
mkConsListTy = foldr PairTy UnitTy

mkConsList :: [Atom r n] -> Atom r n
mkConsList = foldr PairVal UnitVal

fromConsListTy :: (IRRep r, Fallible m) => Type r n -> m [Type r n]
fromConsListTy ty = case ty of
UnitTy -> return []
PairTy t rest -> (t:) <$> fromConsListTy rest
_ -> throw CompilerErr $ "Not a pair or unit: " ++ show ty

-- ((...((ans & x{n}) & x{n-1})... & x2) & x1) -> (ans, [x1, ..., x{n}])
fromLeftLeaningConsListTy :: (IRRep r, Fallible m) => Int -> Type r n -> m (Type r n, [Type r n])
fromLeftLeaningConsListTy depth initTy = go depth initTy []
where
go 0 ty xs = return (ty, reverse xs)
go remDepth ty xs = case ty of
PairTy lt rt -> go (remDepth - 1) lt (rt : xs)
_ -> throw CompilerErr $ "Not a pair: " ++ show xs

fromConsList :: (IRRep r, Fallible m) => Atom r n -> m [Atom r n]
fromConsList xs = case xs of
UnitVal -> return []
PairVal x rest -> (x:) <$> fromConsList rest
_ -> throw CompilerErr $ "Not a pair or unit: " ++ show xs

type BundleDesc = Int -- length

bundleFold :: a -> (a -> a -> a) -> [a] -> (a, BundleDesc)
Expand All @@ -465,15 +438,15 @@ bundleFold emptyVal pair els = case els of
where (tb, td) = bundleFold emptyVal pair t

mkBundleTy :: [Type r n] -> (Type r n, BundleDesc)
mkBundleTy = bundleFold UnitTy PairTy
mkBundleTy = bundleFold UnitTy (\x y -> TyCon (ProdType [x, y]))

mkBundle :: [Atom r n] -> (Atom r n, BundleDesc)
mkBundle = bundleFold UnitVal PairVal
mkBundle = bundleFold UnitVal (\x y -> Con (ProdCon [x, y]))

trySelectBranch :: IRRep r => Atom r n -> Maybe (Int, Atom r n)
trySelectBranch e = case e of
SumVal _ i value -> Just (i, value)
NewtypeCon con e' | isSumCon con -> trySelectBranch e'
Con (SumCon _ i value) -> Just (i, value) -- TODO: do we need this case?
Con (NewtypeCon con e') | isSumCon con -> trySelectBranch e'
_ -> Nothing

freeAtomVarsList :: forall r e n. (IRRep r, HoistableE e) => e n -> [Name (AtomNameC r) n]
Expand Down
98 changes: 45 additions & 53 deletions src/lib/PPrint.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -209,17 +209,18 @@ instance IRRep r => PrettyPrec (LamExpr r n) where
instance IRRep r => Pretty (IxType r n) where
pretty (IxType ty dict) = parens $ "IxType" <+> pretty ty <> prettyIxDict dict

instance Pretty (DictCon n) where
pretty d = case d of
instance IRRep r => Pretty (Dict r n) where
pretty = \case
DictCon con -> pretty con
StuckDict _ stuck -> pretty stuck

instance IRRep r => Pretty (DictCon r n) where
pretty = \case
InstanceDict _ name args -> "Instance" <+> p name <+> p args
IxFin _ n -> "Ix (Fin" <+> p n <> ")"
DataData _ a -> "Data " <+> p a

instance IRRep r => Pretty (IxDict r n) where
pretty = \case
IxDictAtom x -> p x
IxDictRawFin n -> "Ix (RawFin " <> p n <> ")"
IxDictSpecialized _ d xs -> p d <+> p xs
IxRawFin n -> "Ix (RawFin " <> p n <> ")"
IxSpecialized _ d xs -> p d <+> p xs

instance Pretty (DictType n) where
pretty (DictType classSourceName _ params) =
Expand All @@ -236,47 +237,33 @@ instance Pretty (CoreLamExpr n) where
instance IRRep r => Pretty (Atom r n) where pretty = prettyFromPrettyPrec
instance IRRep r => PrettyPrec (Atom r n) where
prettyPrec atom = case atom of
Stuck e -> prettyPrec e
Lam lam -> atPrec LowestPrec $ p lam
DepPair x y _ -> atPrec ArgPrec $ align $ group $
parens $ p x <+> ",>" <+> p y
Con e -> prettyPrec e
Eff e -> atPrec ArgPrec $ p e
PtrVar _ v -> atPrec ArgPrec $ p v
DictCon d -> atPrec LowestPrec $ p d
RepValAtom x -> atPrec LowestPrec $ pretty x
NewtypeCon con x -> prettyPrecNewtype con x
SimpInCore x -> prettyPrec x
TypeAsAtom ty -> prettyPrec ty
Stuck _ e -> prettyPrec e

instance IRRep r => Pretty (Type r n) where pretty = prettyFromPrettyPrec
instance IRRep r => PrettyPrec (Type r n) where
prettyPrec = \case
Pi piType -> atPrec LowestPrec $ align $ p piType
TabPi piType -> atPrec LowestPrec $ align $ p piType
DepPairTy ty -> prettyPrec ty
TC e -> prettyPrec e
DictTy t -> atPrec LowestPrec $ p t
NewtypeTyCon con -> prettyPrec con
StuckTy e -> prettyPrec e
TyCon e -> prettyPrec e
StuckTy _ e -> prettyPrec e

instance IRRep r => Pretty (Stuck r n) where pretty = prettyFromPrettyPrec
instance IRRep r => PrettyPrec (Stuck r n) where
prettyPrec = \case
StuckVar v -> atPrec ArgPrec $ p v
StuckProject _ i v -> atPrec LowestPrec $ "StuckProject" <+> p i <+> p v
StuckTabApp _ f xs -> atPrec AppPrec $ pArg f <> "." <> pArg xs
StuckUnwrap _ v -> atPrec LowestPrec $ "StuckUnwrap" <+> p v
InstantiatedGiven _ v args -> atPrec LowestPrec $ "Given" <+> p v <+> p (toList args)
SuperclassProj _ d' i -> atPrec LowestPrec $ "SuperclassProj" <+> p d' <+> p i

instance Pretty (SimpInCore n) where pretty = prettyFromPrettyPrec
instance PrettyPrec (SimpInCore n) where
prettyPrec = \case
LiftSimp ty x -> atPrec ArgPrec $ "<embedded-simp-atom " <+> p x <+> " : " <+> p ty <+> ">"
LiftSimpFun ty x -> atPrec ArgPrec $ "<embedded-simp-function " <+> p x <+> " : " <+> p ty <+> ">"
ACase e alts _ -> atPrec AppPrec $ "acase" <+> p e <+> p alts
TabLam _ _ -> atPrec AppPrec $ "tablam"
Var v -> atPrec ArgPrec $ p v
StuckProject i v -> atPrec LowestPrec $ "StuckProject" <+> p i <+> p v
StuckTabApp f xs -> atPrec AppPrec $ pArg f <> "." <> pArg xs
StuckUnwrap v -> atPrec LowestPrec $ "StuckUnwrap" <+> p v
InstantiatedGiven v args -> atPrec LowestPrec $ "Given" <+> p v <+> p (toList args)
SuperclassProj d' i -> atPrec LowestPrec $ "SuperclassProj" <+> p d' <+> p i
-- RepValAtom x -> atPrec LowestPrec $ pretty x
-- SimpInCore x -> prettyPrec x
-- instance Pretty (SimpInCore n) where pretty = prettyFromPrettyPrec
-- instance PrettyPrec (SimpInCore n) where
-- prettyPrec = \case
-- LiftSimp ty x -> atPrec ArgPrec $ "<embedded-simp-atom " <+> p x <+> " : " <+> p ty <+> ">"
-- LiftSimpFun ty x -> atPrec ArgPrec $ "<embedded-simp-function " <+> p x <+> " : " <+> p ty <+> ">"
-- ACase e alts _ -> atPrec AppPrec $ "acase" <+> p e <+> p alts
-- TabLam _ _ -> atPrec AppPrec $ "tablam"

instance IRRep r => Pretty (RepVal r n) where
pretty (RepVal ty tree) = "<RepVal " <+> p tree <+> ":" <+> p ty <> ">"
Expand Down Expand Up @@ -326,14 +313,9 @@ withExplParens (Inferred _ (Synth _)) x = brackets x
instance IRRep r => Pretty (TabPiType r n) where
pretty (TabPiType dict (b:>ty) body) = let
prettyBody = case body of
Pi subpi -> pretty subpi
TyCon (Pi subpi) -> pretty subpi
_ -> pLowest body
prettyBinder = case dict of
IxDictRawFin n -> if binderName b `isFreeIn` body
then parens $ p b <> ":" <> prettyTy
else prettyTy
where prettyTy = "RawFin" <+> p n
_ -> prettyBinderHelper (b:>ty) body
prettyBinder = prettyBinderHelper (b:>ty) body
in prettyBinder <> prettyIxDict dict <> (group $ line <> "=>" <+> prettyBody)

-- A helper to let us turn dict printing on and off. We mostly want it off to
Expand Down Expand Up @@ -820,8 +802,8 @@ instance PrettyPrec ScalarBaseType where
Word32Type -> "Word32"
Word64Type -> "Word64"

instance IRRep r => Pretty (TC r n) where pretty = prettyFromPrettyPrec
instance IRRep r => PrettyPrec (TC r n) where
instance IRRep r => Pretty (TyCon r n) where pretty = prettyFromPrettyPrec
instance IRRep r => PrettyPrec (TyCon r n) where
prettyPrec con = case con of
BaseType b -> prettyPrec b
ProdType [] -> atPrec ArgPrec $ "()"
Expand All @@ -832,6 +814,11 @@ instance IRRep r => PrettyPrec (TC r n) where
RefType h a -> atPrec AppPrec $ pAppArg "Ref" [h] <+> p a
TypeKind -> atPrec ArgPrec "Type"
HeapType -> atPrec ArgPrec "Heap"
-- Pi piType -> atPrec LowestPrec $ align $ p piType
-- TabPi piType -> atPrec LowestPrec $ align $ p piType
-- DepPairTy ty -> prettyPrec ty
-- DictTy t -> atPrec LowestPrec $ p t
-- NewtypeTyCon con -> prettyPrec con

prettyPrecNewtype :: NewtypeCon n -> CAtom n -> DocPrec ann
prettyPrecNewtype con x = case (con, x) of
Expand Down Expand Up @@ -866,6 +853,14 @@ instance IRRep r => PrettyPrec (Con r n) where
SumCon _ tag payload -> atPrec ArgPrec $
"(" <> p tag <> "|" <+> pApp payload <+> "|)"
HeapVal -> atPrec ArgPrec "HeapValue"
-- Lam lam -> atPrec LowestPrec $ p lam
-- DepPair x y _ -> atPrec ArgPrec $ align $ group $
-- parens $ p x <+> ",>" <+> p y
-- Eff e -> atPrec ArgPrec $ p e
-- PtrVar _ v -> atPrec ArgPrec $ p v
-- DictCon d -> atPrec LowestPrec $ p d
-- NewtypeCon con x -> prettyPrecNewtype con x
-- TyConAtom ty -> prettyPrec ty

instance IRRep r => Pretty (PrimOp r n) where pretty = prettyFromPrettyPrec
instance IRRep r => PrettyPrec (PrimOp r n) where
Expand Down Expand Up @@ -934,10 +929,7 @@ instance IRRep r => PrettyPrec (DAMOp r n) where
prettyPrec op = atPrec LowestPrec case op of
Seq _ ann d c lamExpr -> case lamExpr of
UnaryLamExpr b body -> do
let rawFinPretty = case d of
IxType _ (IxDictRawFin n) -> parens $ "RawFin" <+> p n
_ -> mempty
"seq" <+> rawFinPretty <+> pApp ann <+> pApp c <+> prettyLam (p b <> ".") body
"seq" <+> pApp ann <+> pApp c <+> prettyLam (p b <> ".") body
_ -> p (show op) -- shouldn't happen, but crashing pretty printers make debugging hard
RememberDest _ x y -> "rememberDest" <+> pArg x <+> pArg y
Place r v -> pApp r <+> "r:=" <+> pApp v
Expand Down
Loading

0 comments on commit 8dd4017

Please sign in to comment.