packages feed

ghc-justdoit (empty) → 0.1

raw patch · 10 files changed

+603/−0 lines, 10 filesdep +basedep +ghcdep +ghc-justdoitsetup-changed

Dependencies added: base, ghc, ghc-justdoit, hashable, inspection-testing

Files

+ ChangeLog.md view
@@ -0,0 +1,5 @@+# Revision history for ghc-justdoit++## 0.1 -- YYYY-mm-dd++* First version. Released on an unsuspecting world.
+ GHC/JustDoIt.hs view
@@ -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'
+ GHC/JustDoIt/Plugin.hs view
@@ -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
+ GHC/JustDoIt/Solver.hs view
@@ -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
+ GHC/LJT.hs view
@@ -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
+ LICENSE view
@@ -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.
+ README.md view
@@ -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++
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ examples/Demo.hs view
@@ -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 "☺"
+ ghc-justdoit.cabal view
@@ -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+    .+    @+    &#123;&#45;\# OPTIONS_GHC -fplugin GHC.JustDoIt.Plugin \#&#45;&#125;+    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 <https://github.com/nomeata/ghc-justdoit/blob/master/examples/Demo.hs examples/Demo.hs>+    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