Initial commit

.gitignore

@@ -0,0 +1,11 @@
+# Temporary directories
+disabled/
+
+# OS crap
+.DS_Store
+Thumbs.db
+
+# Build artifacts
+*.hi
+*.o
+dist/

CPS/Syntax.hs

@@ -0,0 +1,2 @@
+module CPS.Syntax where
+

GHC/Coercion.hs

@@ -0,0 +1,59 @@
+module GHC.Coercion where
+
+import GHC.Var
+import GHC.Type
+
+import Utilities
+
+
+data Coercion = CoVarCo CoVarId
+              | ReflCo Type
+              | AppCo Coercion Coercion
+              | SymCo Coercion
+              | TransCo Coercion Coercion
+              | NthCo Int Coercion
+              | ForAllCo TyVar Coercion
+              | InstCo Coercion Type
+              | UnsafeCo Type Type -- Also used for instantiated axioms
+              deriving (Eq, Show)
+
+instance Pretty Coercion where
+    pPrint _ = text "co" -- FIXME
+
+
+mkCoercionType :: Type -> Type -> Type
+mkCoercionType ty1 ty2 = mkTyConAppTy (eqHashTyCon (typeKind ty1)) [ty1, ty2]
+
+splitCoercionType :: Type -> (Type, Type)
+splitCoercionType ty = case splitTyConAppTy_maybe ty of
+    Just (tc, [ty1, ty2]) | tc == eqHashTyCon (typeKind ty1) -> (ty1, ty2)
+    _ -> error "splitCoercionType"
+
+
+coVarIdType' :: CoVarId -> (Type, Type)
+coVarIdType' = splitCoercionType . idType
+
+coercionType :: Coercion -> Type
+coercionType = uncurry mkCoercionType . coercionType'
+
+coercionType' :: Coercion -> (Type, Type)
+coercionType' (CoVarCo x)     = coVarIdType' x
+coercionType' (ReflCo ty)     = (ty, ty)
+coercionType' (AppCo co1 co2) = (ty1a `AppTy` ty2a, ty1b `AppTy` ty2b)
+  where (ty1a, ty1b) = coercionType' co1
+        (ty2a, ty2b) = coercionType' co2
+coercionType' (SymCo co) = (ty2, ty1)
+  where (ty1, ty2) = coercionType' co
+coercionType' (TransCo co1 co2) = (ty1a, ty2b)
+  where (ty1a, _ty1b) = coercionType' co1
+        (_ty2a, ty2b) = coercionType' co2
+coercionType' (NthCo n co) = (f ty1, f ty2)
+  where (ty1, ty2) = coercionType' co
+        f ty = case splitTyConAppTy_maybe ty of
+            Just (_, tys) | n < length tys -> tys !! n
+            _ -> error "coercionType': NthCo"
+coercionType' (ForAllCo a co) = (ForAllTy a ty1, ForAllTy a ty2)
+  where (ty1, ty2) = coercionType' co
+coercionType' (InstCo co ty) = (instTy ty1 ty, instTy ty2 ty)
+  where (ty1, ty2) = coercionType' co
+coercionType' (UnsafeCo ty1 ty2) = (ty1, ty2)

GHC/Data.hs

@@ -0,0 +1,70 @@
+module GHC.Data where
+
+import GHC.Type
+import GHC.Var
+
+import Utilities
+
+
+typefulId :: Type -> Id
+typefulId = Id (error "typefulId: not meant to be used in a context where the Id name matters") -- FIXME?
+
+
+type Arity = Int
+data DataCon = DataCon {
+    dataConName      :: String,
+    dataConBinders   :: [Var], -- Mixture of TyVar and Id binders (including coercions for GADTs)..
+    dataConTyCon     :: TyCon, -- ..scoping over this..
+    dataConTyConArgs :: [Type] -- ..applied to these
+  } deriving (Show)
+
+instance Eq DataCon where
+    (==) = (==) `on` dataConName
+
+instance Ord DataCon where
+    compare = compare `on` dataConName
+
+instance Pretty DataCon where
+    pPrint = text . dataConName
+
+dataConType :: DataCon -> Type
+dataConType dc = mkPiTys (dataConBinders dc) (mkTyConAppTy (dataConTyCon dc) (dataConTyConArgs dc))
+
+
+pairDataCon :: DataCon
+pairDataCon = DataCon {
+    dataConName      = "(,)",
+    dataConBinders   = [ATyVar a_tv, ATyVar b_tv, AnId (typefulId a_ty), AnId (typefulId b_ty)],
+    dataConTyCon     = pairTyCon,
+    dataConTyConArgs = [a_ty, b_ty]
+  } where ([a_tv, b_tv], [a_ty, b_ty]) = shadowyTyVars [("a", LiftedTypeKind), ("b", LiftedTypeKind)]
+
+unboxedPairDataCon :: DataCon
+unboxedPairDataCon = DataCon {
+    dataConName      = "(#,#)",
+    dataConBinders   = [ATyVar a_tv, ATyVar b_tv, AnId (typefulId a_ty), AnId (typefulId b_ty)],
+    dataConTyCon     = unboxedPairTyCon,
+    dataConTyConArgs = [a_ty, b_ty]
+  } where ([a_tv, b_tv], [a_ty, b_ty]) = shadowyTyVars [("a", OpenTypeKind), ("b", OpenTypeKind)]
+
+iHashDataCon :: DataCon
+iHashDataCon = DataCon {
+    dataConName      = "I#",
+    dataConBinders   = [AnId (typefulId intHashTy)],
+    dataConTyCon     = intTyCon,
+    dataConTyConArgs = []
+  }
+
+trueDataCon, falseDataCon :: DataCon
+trueDataCon = DataCon {
+    dataConName      = "True",
+    dataConBinders   = [],
+    dataConTyCon     = boolTyCon,
+    dataConTyConArgs = []
+  }
+falseDataCon = DataCon {
+    dataConName      = "False",
+    dataConBinders   = [],
+    dataConTyCon     = boolTyCon,
+    dataConTyConArgs = []
+  }

GHC/Syntax.hs

@@ -0,0 +1,175 @@
+{-# LANGUAGE PatternGuards, ViewPatterns, TypeSynonymInstances, FlexibleInstances, Rank2Types #-}
+module GHC.Syntax where
+
+import GHC.Coercion
+import GHC.Data
+import GHC.Type
+import GHC.Var
+
+import Name
+import Utilities
+
+
+data PrimOp = Add | Subtract | Multiply | Divide | Modulo | Equal | LessThan | LessThanEqual
+            deriving (Eq, Ord, Show)
+
+data AltCon = DataAlt DataCon [Var] | LiteralAlt Literal | DefaultAlt
+            deriving (Eq, Show)
+
+-- Note [Case wildcards]
+-- ~~~~~~~~~~~~~~~~~~~~~
+--
+-- Simon thought that I should use the variable in the DefaultAlt to agressively rewrite occurences of a scrutinised variable.
+-- The motivation is that this lets us do more inlining above the case. For example, take this code fragment from foldl':
+--
+--   let n' = c n y
+--   in case n' of wild -> foldl' c n' ys
+--
+-- If we rewrite, n' becomes linear:
+--
+--   let n' = c n y
+--   in case n' of wild -> foldl c wild ys
+--
+-- This lets us potentially inline n' directly into the scrutinee position (operationally, this prevent creation of a thunk for n').
+-- However, I don't think that this particular form of improving linearity helps the supercompiler. We only want to inline n' in
+-- somewhere if it meets some interesting context, with which it can cancel. But if we are creating an update frame for n' at all,
+-- it is *probably* because we had no information about what it evaluated to.
+--
+-- An interesting exception is when n' binds a case expression:
+--
+--   let n' = case unk of T -> F; F -> T
+--   in case (case n' of T -> F; F -> T) of
+--        wild -> e[n']
+--
+-- You might think that we want n' to be linear so we can inline it into the case on it. However, the splitter will save us and produce:
+--
+--   case unk of
+--     T -> let n' = F
+--          in case (case n' of T -> F; F -> T) of wild -> e[n']
+--     F -> let n' = T
+--          in case (case n' of T -> F; F -> T) of wild -> e[n']
+--
+-- Since we now know the form of n', everything works out nicely.
+--
+-- Conclusion: I don't think rewriting to use the case wildcard buys us anything at all.
+
+data Literal = Int Integer
+             deriving (Eq, Show)
+
+data Term = Var Id
+          | Value Value
+          | App Term Id
+          | TyApp Term Type
+          | PrimOp PrimOp [Term]
+          | Case Term Type Id [Alt]
+          | LetRec [(Id, Term)] Term
+          | Cast Term Coercion
+          deriving (Eq, Show)
+
+type Alt = (AltCon, Term)
+
+data Value = Coercion Coercion | Lambda Var Term | Data DataCon [Var] | Literal Literal
+            deriving (Eq, Show)
+
+instance Pretty PrimOp where
+    pPrint Add           = text "(+)"
+    pPrint Subtract      = text "(-)"
+    pPrint Multiply      = text "(*)"
+    pPrint Divide        = text "div"
+    pPrint Modulo        = text "mod"
+    pPrint Equal         = text "(==)"
+    pPrint LessThan      = text "(<)"
+    pPrint LessThanEqual = text "(<=)"
+
+instance Pretty Literal where
+    pPrintPrec level prec (Int i) | level == haskellLevel = prettyParen (prec >= appPrec) $ pPrintPrec level appPrec i <+> text ":: Int"
+                                  | otherwise             = pPrintPrec level prec i
+
+instance Pretty Term where
+    pPrintPrec level prec e = case e of
+        LetRec xes e    -> pPrintPrecLetRec level prec xes e
+        Var x           -> pPrintPrec level prec x
+        Value v         -> pPrintPrec level prec v
+        App e1 x2       -> pPrintPrecApp level prec e1 x2
+        TyApp e1 ty2    -> pPrintPrecApp level prec e1 ty2
+        PrimOp pop xs   -> pPrintPrecPrimOp level prec pop xs
+        Case e _ x alts -> pPrintPrecCase level prec e x alts
+        Cast e co       -> pPrintPrecCast level prec e co
+
+pPrintPrecPrimOp :: (Pretty a, Pretty b) => PrettyLevel -> Rational -> a -> [b] -> Doc
+pPrintPrecPrimOp level prec pop xs = pPrintPrecApps level prec pop xs
+
+pPrintPrecCase :: (Pretty a, Pretty b, Pretty c, Pretty d) => PrettyLevel -> Rational -> a -> d -> [(b, c)] -> Doc
+pPrintPrecCase level prec e x alts = prettyParen (prec > noPrec) $ hang (text "case" <+> pPrintPrec level noPrec e <> text "@" <> pPrintPrec level noPrec x <+> text "of") 2 $ vcat (map (pPrintPrecAlt level noPrec) alts)
+
+pPrintPrecAlt :: (Pretty a, Pretty b) => PrettyLevel -> Rational -> (a, b) -> Doc
+pPrintPrecAlt level _ (alt_con, alt_e) = hang (pPrintPrec level noPrec alt_con <+> text "->") 2 (pPrintPrec level noPrec alt_e)
+
+pPrintPrecCast :: (Pretty a, Pretty b) => PrettyLevel -> Rational -> a -> b -> Doc
+pPrintPrecCast level prec e co = prettyParen (prec >= appPrec) $ pPrintPrec level opPrec e <+> text "|>" <+> pPrintPrec level appPrec co
+
+pPrintPrecLetRec :: (Pretty a, Pretty b, Pretty c) => PrettyLevel -> Rational -> [(a, b)] -> c -> Doc
+pPrintPrecLetRec level prec xes e_body
+  | [] <- xes = pPrintPrec level prec e_body
+  | otherwise = prettyParen (prec > noPrec) $ hang (if level == haskellLevel then text "let" else text "letrec") 2 (vcat [pPrintPrec level noPrec x <+> text "=" <+> pPrintPrec level noPrec e | (x, e) <- xes]) $$ text "in" <+> pPrintPrec level noPrec e_body
+
+instance Pretty AltCon where
+    pPrintPrec level prec altcon = case altcon of
+        DataAlt dc xs -> prettyParen (prec >= appPrec) $ pPrintPrec level noPrec dc <+> hsep (map (pPrintPrec level appPrec) xs)
+        LiteralAlt l  -> pPrint l
+        DefaultAlt    -> text "_"
+
+instance Pretty Value where
+    pPrintPrec level prec v = case v of
+        -- Unfortunately, this nicer pretty-printing doesn't work for general (TermF ann):
+        --Lambda x e    -> pPrintPrecLam level prec (x:xs) e'
+        --  where (xs, e') = collectLambdas e
+        Lambda x e    -> pPrintPrecLam level prec [x] e
+        Data dc xs    -> pPrintPrecApps level prec dc xs
+        Literal l     -> pPrintPrec level prec l
+        Coercion co   -> pPrintPrec level prec co
+
+pPrintPrecLam :: Pretty a => PrettyLevel -> Rational -> [Var] -> a -> Doc
+pPrintPrecLam level prec xs e = prettyParen (prec > noPrec) $ text "\\" <> hsep [pPrintPrec level appPrec y | y <- xs] <+> text "->" <+> pPrintPrec level noPrec e
+
+
+termType :: Term -> Type
+termType (Var x) = idType x
+termType (Value v) = valueType v
+termType (App e _) = funResTy (termType e)
+termType (TyApp e ty) = instTy (termType e) ty
+termType (PrimOp pop es) = case (pop, map termType es) of
+    (pop, [ty1, ty2])
+      | pop `elem` [Add, Subtract, Multiply, Divide, Modulo]
+      , ty1 == intTy
+      , ty2 == intTy
+      -> intTy
+      | pop `elem` [Equal, LessThan, LessThanEqual]
+      , ty1 == intTy
+      , ty2 == intTy
+      -> boolTy
+    _ -> error "termType: PrimOp"
+termType (Case _ ty _ _) = ty
+termType (LetRec _ e) = termType e
+termType (Cast _ co) = snd $ coercionType' co
+
+valueType :: Value -> Type
+valueType (Coercion co) = coercionType co
+valueType (Lambda x e)  = mkPiTy x (termType e)
+valueType (Data dc xs)  = instPiTys (dataConType dc) xs
+valueType (Literal l)   = literalType l
+
+literalType :: Literal -> Type
+literalType (Int _) = intTy
+
+
+freshFloatId :: UniqueSupply -> String -> Term -> (UniqueSupply, Maybe (Id, Term), Id)
+freshFloatId ids _ (Var x) = (ids,  Nothing,     x)
+freshFloatId ids s e       = (ids', Just (y, e), y)
+  where (ids', n) = freshName ids s
+        y = Id n (termType e)
+
+freshFloatIds :: UniqueSupply -> String -> [Term] -> (UniqueSupply, [(Id, Term)], [Id])
+freshFloatIds ids s es = reassociate $ mapAccumL (\ids -> associate . freshFloatId ids s) ids es
+  where reassociate (ids, unzip -> (mb_floats, xs)) = (ids, catMaybes mb_floats, xs)
+        associate (ids, mb_float, x) = (ids, (mb_float, x))