diff --git a/ChangeLog.md b/ChangeLog.md new file mode 100644 --- /dev/null +++ b/ChangeLog.md @@ -0,0 +1,5 @@ +# Revision history for ghc-justdoit + +## 0.1 -- YYYY-mm-dd + +* First version. Released on an unsuspecting world. diff --git a/GHC/JustDoIt.hs b/GHC/JustDoIt.hs new file mode 100644 --- /dev/null +++ b/GHC/JustDoIt.hs @@ -0,0 +1,9 @@ +module GHC.JustDoIt ( JustDoIt, justDoIt, (…) ) where + +class JustDoIt a where justDoIt' :: a + +justDoIt :: JustDoIt a => a +justDoIt = justDoIt' + +(…) :: JustDoIt a => a +(…) = justDoIt' diff --git a/GHC/JustDoIt/Plugin.hs b/GHC/JustDoIt/Plugin.hs new file mode 100644 --- /dev/null +++ b/GHC/JustDoIt/Plugin.hs @@ -0,0 +1,73 @@ +{-# LANGUAGE CPP, TupleSections #-} +module GHC.JustDoIt.Plugin ( plugin ) +where + +-- external +import Data.Maybe +import Control.Monad + +-- GHC API +import Module (mkModuleName) +import OccName (mkTcOcc) +import Plugins (Plugin (..), defaultPlugin) +import TcEvidence +import TcPluginM +import TcRnTypes +import Class +import CoreUtils +import MkCore +import TyCon +import Type +import CoreSyn + +import GHC.JustDoIt.Solver + +plugin :: Plugin +plugin = defaultPlugin { tcPlugin = const (Just jdiPlugin) } + +jdiPlugin :: TcPlugin +jdiPlugin = + TcPlugin { tcPluginInit = lookupJDITyCon + , tcPluginSolve = solveJDI + , tcPluginStop = const (return ()) + } + +lookupJDITyCon :: TcPluginM Class +lookupJDITyCon = do + Found _ md <- findImportedModule jdiModule Nothing + jdiTcNm <- lookupOrig md (mkTcOcc "JustDoIt") + tcLookupClass jdiTcNm + where + jdiModule = mkModuleName "GHC.JustDoIt" + +wrap :: Class -> CoreExpr -> EvTerm +wrap cls = EvExpr . appDc + where + tyCon = classTyCon cls + dc = tyConSingleDataCon tyCon + appDc x = mkCoreConApps dc [Type (exprType x), x] + +findClassConstraint :: Class -> Ct -> Maybe (Ct, Type) +findClassConstraint cls ct = do + (cls', [t]) <- getClassPredTys_maybe (ctPred ct) + guard (cls' == cls) + return (ct, t) + +solveJDI :: Class -- ^ JDI's TyCon + -> [Ct] -- ^ [G]iven constraints + -> [Ct] -- ^ [D]erived constraints + -> [Ct] -- ^ [W]anted constraints + -> TcPluginM TcPluginResult +solveJDI jdiCls _ _ wanteds = + return $! case result of + Left x -> TcPluginContradiction [x] + Right solved -> TcPluginOk solved [] + where + our_wanteds = mapMaybe (findClassConstraint jdiCls) wanteds + result = partitionMaybe (fmap (wrap jdiCls) . solve) our_wanteds + +partitionMaybe :: (b -> Maybe c) -> [(a,b)] -> Either a [(c,a)] +partitionMaybe _ [] = Right [] +partitionMaybe f ((k,v):xs) = case f v of + Nothing -> Left k + Just y -> ((y,k):) <$> partitionMaybe f xs diff --git a/GHC/JustDoIt/Solver.hs b/GHC/JustDoIt/Solver.hs new file mode 100644 --- /dev/null +++ b/GHC/JustDoIt/Solver.hs @@ -0,0 +1,12 @@ +module GHC.JustDoIt.Solver ( solve ) where + +import Type +import CoreSyn + +import GHC.LJT + +import Data.Maybe + +-- | Central place to plug additional solvers in. For now, we just do "GHC.LJT" +solve :: Type -> Maybe CoreExpr +solve = listToMaybe . ljt diff --git a/GHC/LJT.hs b/GHC/LJT.hs new file mode 100644 --- /dev/null +++ b/GHC/LJT.hs @@ -0,0 +1,220 @@ +-- | An implementation of LJT proof search directly on Core terms. +module GHC.LJT where + +import FastString +import Unique +import Type +import Id +import Var +import CoreSyn +import Outputable +import TyCoRep +import TyCon +import DataCon +import MkCore +import MkId +import CoreUtils +import TysWiredIn +import BasicTypes +import NameEnv +import NameSet + +import Data.List +import Data.Hashable +import Control.Monad +import Data.Bifunctor + +ljt :: Type -> [CoreExpr] +ljt t = [] ==> t + + +(==>) :: [Id] -> Type -> [CoreExpr] + +-- Rule Axiom +-- (TODO: The official algorithm restricts this rule to atoms. Why?) +ante ==> goal + | Just v <- find (\v -> idType v `eqType` goal) ante + = pure $ Var v + +-- Rule f⇒ +ante ==> goal + | Just v <- find (\v -> isEmptyTy (idType v)) ante + = pure $ mkWildCase (Var v) (idType v) goal [] + +-- Rule →⇒2 +ante ==> goal + | Just ((v,((tys, build, _destruct),_r)),ante') <- anyA (funLeft isProdType) ante + = let vs = map newVar tys + expr = mkLams vs (App (Var v) (build (map Var vs))) + v' = newVar (exprType expr) + in mkLetNonRec v' expr <$> (v' : ante') ==> goal + +-- Rule →⇒3 +ante ==> goal + | Just ((v,((tys, injs, _destruct),_r)),ante') <- anyA (funLeft isSumType) ante + = let es = [ lam ty (\vx -> App (Var v) (inj (Var vx))) | (ty,inj) <- zip tys injs ] + in letsA es $ \vs -> (vs ++ ante') ==> goal + +-- Rule ∧⇒ +ante ==> goal + | Just ((v,(tys, _build, destruct)),ante') <- anyA isProdType ante + = let pats = map newVar tys + in destruct (Var v) pats <$> (pats ++ ante') ==> goal + +-- Rule ⇒∧ +ante ==> goal + | Just (tys, build, _destruct) <- isProdType goal + = build <$> sequence [ante ==> ty | ty <- tys] + +-- Rule ∨⇒ +ante ==> goal + | Just ((vAorB, (tys, _injs, destruct)),ante') <- anyA isSumType ante + = let vs = map newVar tys in + destruct (Var vAorB) vs <$> sequence [ (v:ante') ==> goal | v <- vs] + +-- Rule ⇒→ +ante ==> FunTy t1 t2 + = Lam v <$> (v : ante) ==> t2 + where + v = newVar t1 + +-- Rule →⇒1 +-- (TODO: The official algorithm restricts this rule to atoms. Why?) +ante ==> goal + | let isInAnte a = find (\v -> idType v `eqType` a) ante + , Just ((vAB, (vA,_)), ante') <- anyA (funLeft isInAnte) ante + = letA (App (Var vAB) (Var vA)) $ \vB -> (vB : ante') ==> goal + +-- Rule ⇒∨ +ante ==> goal + | Just (tys, injs, _destruct) <- isSumType goal + = msum [ inj <$> ante ==> ty | (ty,inj) <- zip tys injs ] + +-- Rule →⇒4 +ante ==> goal + | Just ((vABC, ((a,b),_)), ante') <- anyA (funLeft (funLeft Just)) ante + = do + let eBC = lam b $ \vB -> App (Var vABC) (lam a $ \_ -> Var vB) + eAB <- letA eBC $ \vBC -> (vBC : ante') ==> FunTy a b + letA (App (Var vABC) eAB) $ \vC -> (vC : ante') ==> goal + +-- Nothing found :-( +_ante ==> _goal + = -- pprTrace "go" (vcat [ ppr (idType v) | v <- ante] $$ text "------" $$ ppr goal) $ + mzero + +-- Smart constructors + +newVar :: Type -> Id +newVar ty = mkSysLocal (mkFastString "x") (mkBuiltinUnique i) ty + where i = hash (showSDocUnsafe (ppr ty)) + -- We don’t mind if variables with equal types shadow each other, + -- so let’s just derive the unique from the type + +lam :: Type -> (Id -> CoreExpr) -> CoreExpr +lam ty gen = Lam v $ gen v + where v = newVar ty + +lamA :: Applicative f => Type -> (Id -> f CoreExpr) -> f CoreExpr +lamA ty gen = Lam v <$> gen v + where v = newVar ty + +let_ :: CoreExpr -> (Id -> CoreExpr) -> CoreExpr +let_ e gen = mkLetNonRec v e $ gen v + where v = newVar (exprType e) + +letA :: Applicative f => CoreExpr -> (Id -> f CoreExpr) -> f CoreExpr +letA e gen = mkLetNonRec v e <$> gen v + where v = newVar (exprType e) + +letsA :: Applicative f => [CoreExpr] -> ([Id] -> f CoreExpr) -> f CoreExpr +letsA es gen = mkLets (zipWith NonRec vs es) <$> gen vs + where vs = map (newVar . exprType) es + +-- Predicate on types + +isProdType :: Type -> Maybe ([Type], [CoreExpr] -> CoreExpr, CoreExpr -> [Id] -> CoreExpr -> CoreExpr) +isProdType ty + | Just (tc, _, dc, repargs) <- splitDataProductType_maybe ty + , not (isRecTyCon tc) + = Just ( repargs + , \args -> mkConApp dc (map Type repargs ++ args) + , \scrut pats rhs -> mkWildCase scrut ty (exprType rhs) [(DataAlt dc, pats, rhs)] + ) + | Just (tc, ty_args) <- splitTyConApp_maybe ty + , Just dc <- newTyConDataCon_maybe tc + , not (isRecTyCon tc) + , let repargs = dataConInstArgTys dc ty_args + = Just ( repargs + , \[arg] -> wrapNewTypeBody tc ty_args arg + , \scrut [pat] rhs -> + mkLetNonRec pat (unwrapNewTypeBody tc ty_args scrut) rhs + ) +isProdType _ = Nothing + +-- Haskell sum constructors can have multiple parameters. For our purposes, if +-- so, we wrap them in a product. +isSumType :: Type -> Maybe ([Type], [CoreExpr -> CoreExpr], CoreExpr -> [Id] -> [CoreExpr] -> CoreExpr) +isSumType ty + | Just (tc, ty_args) <- splitTyConApp_maybe ty + , Just dcs <- isDataSumTyCon_maybe tc + , not (isRecTyCon tc) + = let tys = [ mkTupleTy Boxed (dataConInstArgTys dc ty_args) | dc <- dcs ] + injs = [ + let vtys = dataConInstArgTys dc ty_args + vs = map newVar vtys + in \ e -> mkSmallTupleCase vs (mkConApp dc (map Type ty_args ++ map Var vs)) + (mkWildValBinder (exprType e)) e + | dc <- dcs] + destruct = \e vs alts -> + Case e (mkWildValBinder (exprType e)) (exprType (head alts)) + [ let pats = map newVar (dataConInstArgTys dc ty_args) in + (DataAlt dc, pats, mkLetNonRec v (mkCoreVarTup pats) rhs) + | (dc,v,rhs) <- zip3 dcs vs alts ] + in Just (tys, injs, destruct) +isSumType _ = Nothing + +-- We don’t want to look into recursive type cons. +-- Which ones are recursive? Surely those that get mentioned in their +-- arguments. Or in type cons in their arguments. +-- But that is not enough, because of higher kinded arguments. So prohibit +-- those as well. + +isRecTyCon :: TyCon -> Bool +isRecTyCon tc = go emptyNameSet tc + where + go seen tc | tyConName tc `elemNameSet` seen = True + | any isHigherKind paramKinds = False + | any (go seen') mentionedTyCons = True + | otherwise = False + where mentionedTyCons = concatMap getTyCons $ concatMap dataConOrigArgTys $ tyConDataCons tc + paramKinds = map varType (tyConTyVars tc) + seen' = seen `extendNameSet` tyConName tc + + isHigherKind :: Kind -> Bool + isHigherKind k = not (k `eqType` liftedTypeKind) + + getTyCons :: Type -> [TyCon] + getTyCons = nameEnvElts . go + where + go (TyConApp tc tys) = unitNameEnv (tyConName tc) tc `plusNameEnv` go_s tys + go (LitTy _) = emptyNameEnv + go (TyVarTy _) = emptyNameEnv + go (AppTy a b) = go a `plusNameEnv` go b + go (FunTy a b) = go a `plusNameEnv` go b + go (ForAllTy _ ty) = go ty + go (CastTy ty _) = go ty + go (CoercionTy co) = emptyNameEnv + go_s = foldr (plusNameEnv . go) emptyNameEnv + + +-- Combinators to search for matching things + +funLeft :: (Type -> Maybe a) -> Type -> Maybe (a,Type) +funLeft p (FunTy t1 t2) = (\x -> (x,t2)) <$> p t1 +funLeft _ _ = Nothing + +anyA :: (Type -> Maybe a) -> [Id] -> Maybe ((Id, a), [Id]) +anyA _ [] = Nothing +anyA p (v:vs) | Just x <- p (idType v) = Just ((v,x), vs) + | otherwise = second (v:) <$> anyA p vs diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,20 @@ +Copyright (c) 2018 Joachim Breitner + +Permission is hereby granted, free of charge, to any person obtaining +a copy of this software and associated documentation files (the +"Software"), to deal in the Software without restriction, including +without limitation the rights to use, copy, modify, merge, publish, +distribute, sublicense, and/or sell copies of the Software, and to +permit persons to whom the Software is furnished to do so, subject to +the following conditions: + +The above copyright notice and this permission notice shall be included +in all copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. +IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY +CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, +TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE +SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,50 @@ +ghc-justdoit: a GHC plugin to write the code for you +========================================= + +This is a prototype of a code synthesis plugin for GHC, which uses LJT proof +search to instantiate a type. + +Synopsis +-------- + + {-# OPTIONS_GHC -fplugin=GHC.JustDoIt.Plugin #-} + module Test where + + import GHC.JustDoIt + + foo :: ((a -> r) -> r) -> (a -> ((b -> r) -> r)) -> ((b -> r) -> r) + foo = (…) + +Missing bits +------------ + + * The LJT might not be complete, due to insufficient backtracking. + * The implementation is very much unoptimized. + * It returns one solution, but not necessary the “best” one. But what is the “best” one? + * It ignores any recursive type, so it cannot do anything with lists. It would be much more useful if it could do some best-effort thing her as well. + +If someone wants to pick it up from here, that’d be great! + + +Related work +------------ + + * [Djinn](http://hackage.haskell.org/package/djinn) and [djinn-ghc](http://hackage.haskell.org/package/djinn-ghc) + * [exference](http://hackage.haskell.org/package/exference) + * [curryhoward](https://github.com/Chymyst/curryhoward) for Scala + +Contact +------- + +Please reports bugs and missing features at the [GitHub bugtracker]. This is +also where you can find the [source code]. + +`bSpokeLight` was written by [Joachim Breitner] and is licensed under a +permissive MIT [license]. + +[GitHub bugtracker]: https://github.com/nomeata/ghc-justdoit/issues +[source code]: https://github.com/nomeata/ghc-justdoit +[Joachim Breitner]: http://www.joachim-breitner.de/ +[license]: https://github.com/nomeata/ghc-justdoit/blob/LICENSE + + diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/examples/Demo.hs b/examples/Demo.hs new file mode 100644 --- /dev/null +++ b/examples/Demo.hs @@ -0,0 +1,157 @@ +{-# OPTIONS_GHC -fplugin=GHC.JustDoIt.Plugin #-} +{-# OPTIONS_GHC -fplugin=Test.Inspection.Plugin #-} +{-# LANGUAGE TemplateHaskell, LambdaCase, EmptyCase #-} +import GHC.JustDoIt +import Test.Inspection (inspect, (===), (==-)) + +import Prelude hiding (id, flip, const, curry) + +-- Some auxillary definitions + +data Unit = Unit +data Void +data MyLargeSum a b c d e = MkA a | MkB b | MkC c | MkD d | MkE e +newtype Id a = Id a +data Result a b = Failure a | Success b +newtype ErrRead r e a = ErrRead { unErrRead :: r -> Result e a } + +-- All these functions have basically one sensible implementation. +-- With GHC.JustDoIt, we don’t have to write them. + +id :: a -> a +id = justDoIt + +const :: a -> b -> a +const = (…) + +flip :: (a -> b -> c) -> (b -> a -> c) +flip = (…) + +dup :: a -> (a,a) +dup = (…) + +pair :: a -> b -> (a,b) +pair = (…) + +tripl :: a -> b -> c -> (a,b,c) +tripl = (…) + +proj :: (a,b,c,d) -> c +proj = (…) + +curry :: ((a,b) -> c) -> a -> b -> c +curry = (…) + +curryFlip :: ((a,b) -> c) -> b -> a -> c +curryFlip = (…) + +contBind :: ((a -> r) -> r) -> (a -> ((b -> r) -> r)) -> ((b -> r) -> r) +contBind = (…) + +contAp :: (((a -> b) -> r) -> r) -> ((a -> r) -> r) -> ((b -> r) -> r) +contAp = (…) + +errReadBind :: (r -> Either e a) -> (a -> (r -> Either e b)) -> (r -> Either e b) +errReadBind = (…) + +errReadBindTup :: (r -> Either e a) -> (a -> (r -> Either e b)) -> (r -> Either e (a,b)) +errReadBindTup = (…) + +errReadAp :: (r -> Either e (a -> b)) -> (r -> Either e a) -> (r -> Either e b) +errReadAp = (…) + +errReadBindTup2 :: ErrRead r e a -> (a -> ErrRead r e b) -> ErrRead r e (a,b) +errReadBindTup2 = (…) + +unit :: Unit +unit = (…) + +swapEither :: Either a b -> Either b a +swapEither = (…) + +swapEitherCont :: (((Either a b) -> r) -> r) -> (((Either b a) -> r) -> r) +swapEitherCont = (…) + +randomCrap :: (a -> b) -> (a,c,d) -> (d,b,b) +randomCrap = (…) + +absurd :: Void -> a +absurd = (…) + +convert :: MyLargeSum a b c d e -> Either a (Either b (Either c (Either d e))) +convert = (…) + +mapId :: (a -> b) -> Id a -> Id b +mapId = (…) + +-- Just for comparison, here are the implementations that you might write by +-- hand + +id' x = x +const' x _= x +flip' f a b = f b a +dup' x = (x,x) +pair' x y = (x,y) +tripl' x y z = (x,y,z) +proj' (_,_,c,_) = c +curry' f a b = f (a,b) +curryFlip' f a b = f (b,a) +unit' = Unit +mapId' f (Id x) = Id (f x) +contBind' :: ((a -> r) -> r) -> (a -> ((b -> r) -> r)) -> ((b -> r) -> r) +contBind' ca cb k = ca (\a -> cb a k) +swapEither' (Left a) = (Right a) +swapEither' (Right a) = (Left a) +swapEitherCont' :: (((Either a b) -> r) -> r) -> (((Either b a) -> r) -> r) +swapEitherCont' ca k = ca $ \case Left a -> k (Right a) + Right a -> k (Left a) +absurd' :: Void -> a +absurd' = \case{} +errReadBind' m1 m2 r = case m1 r of Left e -> Left e + Right a -> m2 a r +errReadBindTup' m1 m2 r = case m1 r of + Left e -> Left e + Right a -> case m2 a r of Left e -> Left e + Right b -> Right (a,b) + +errReadBindTup2' :: ErrRead r e a -> (a -> ErrRead r e b) -> ErrRead r e (a,b) +errReadBindTup2' m1 m2 = ErrRead $ \r -> case unErrRead m1 r of + Failure e -> Failure e + Success a -> case unErrRead (m2 a) r of Failure e -> Failure e + Success b -> Success (a,b) + +-- Here are functions where we do not infer the expected code, due to the order +-- things are looked at. +errReadAp' m1 m2 r = case m2 r of Left e -> case m1 r of Left e -> Left e + Right _ -> Left e + Right x -> case m1 r of Left e -> Left e + Right f -> Right (f x) +contAp' :: (((a -> b) -> r) -> r) -> ((a -> r) -> r) -> ((b -> r) -> r) +contAp' ca cb k = cb (\x -> ca (\f -> k (f x))) + +-- And here we use inspection-testing to check that these are indeed the +-- definitions that GHC.JustDoIt created for us. + +inspect $ 'id === 'id' +inspect $ 'const === 'const' +inspect $ 'flip === 'flip' +inspect $ 'dup === 'dup' +inspect $ 'pair === 'pair' +inspect $ 'tripl === 'tripl' +inspect $ 'proj === 'proj' +inspect $ 'curry === 'curry' +inspect $ 'curryFlip === 'curryFlip' +inspect $ 'unit === 'unit' +inspect $ 'contBind === 'contBind' +inspect $ 'contAp === 'contAp' +inspect $ 'swapEither === 'swapEither' +inspect $ 'swapEitherCont === 'swapEitherCont' +inspect $ 'absurd === 'absurd' +inspect $ 'mapId === 'mapId' +inspect $ 'errReadBind === 'errReadBind' +inspect $ 'errReadBindTup === 'errReadBindTup' +inspect $ 'errReadBindTup2 ==- 'errReadBindTup2' -- type variable order differences +inspect $ 'errReadAp === 'errReadAp' + +main :: IO () +main = putStrLn "☺" diff --git a/ghc-justdoit.cabal b/ghc-justdoit.cabal new file mode 100644 --- /dev/null +++ b/ghc-justdoit.cabal @@ -0,0 +1,55 @@ +name: ghc-justdoit +version: 0.1 +synopsis: A magic typeclass that just does it +description: + This plugin allows you to write + . + @ + {-\# OPTIONS_GHC -fplugin GHC.JustDoIt.Plugin \#-} + module Test where + . + import GHC.JustDoIt + . + foo :: ((a -> r) -> r) -> (a -> ((b -> r) -> r)) -> ((b -> r) -> r) + foo = (…) + @ + . + without having to write the actual implementation of `foo`. + . + See + for a few examples of what this plugin can do for you. + +homepage: https://github.com/nomeata/ghc-justdoit +license: MIT +license-file: LICENSE +author: Joachim Breitner +maintainer: mail@joachim-breitner.de +copyright: 2018 Joachim Breitner +category: Language +build-type: Simple +extra-source-files: ChangeLog.md, README.md +cabal-version: >=1.10 +tested-with: GHC ==8.5.* + +library + exposed-modules: GHC.LJT + exposed-modules: GHC.JustDoIt + exposed-modules: GHC.JustDoIt.Plugin + exposed-modules: GHC.JustDoIt.Solver + build-depends: base >=4.11 && <4.12 + build-depends: hashable + build-depends: ghc >=8.5 + default-language: Haskell2010 + +test-suite demo + type: exitcode-stdio-1.0 + main-is: Demo.hs + hs-source-dirs: examples/ + build-depends: base + build-depends: ghc-justdoit + build-depends: inspection-testing + default-language: Haskell2010 + +source-repository head + type: git + location: git://github.com/nomeata/ghc-justdoit.git