djinn-ghc 0.0.1 → 0.0.2

raw patch · 2 files changed

+57/−18 lines, 2 filesdep +asyncdep +transformersdep ~djinn-libdep ~mtlPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: async, transformers

Dependency ranges changed: djinn-lib, mtl

API changes (from Hackage documentation)

Files

• djinn-ghc.cabal +5/−3
• src/Djinn/GHC.hs +52/−15

@@ -1,5 +1,5 @@ name:           djinn-ghc-version:        0.0.1+version:        0.0.2 synopsis:       Generate Haskell code from a type. Bridge from Djinn to GHC API. description:    Djinn uses an theorem prover for intuitionistic propositional logic                 to generate a Haskell expression when given a type.@@ -15,8 +15,10 @@ library   exposed-modules:  Djinn.GHC   build-depends:    base >= 4 && < 5,-                    mtl < 2.2,+                    mtl,                     ghc,                     containers,-                    djinn-lib == 0.0.1+                    transformers,+                    djinn-lib >= 0.0.1.1,+                    async   hs-source-dirs:   src

@@ -1,12 +1,16 @@-{-# LANGUAGE PatternGuards #-}-module Djinn.GHC (djinn) where+{-# LANGUAGE PatternGuards, BangPatterns #-}+module Djinn.GHC (Environment, MaxSolutions(..), djinn) where +import Control.Concurrent+import Control.Concurrent.Async import Control.Monad (forM)+import Data.Maybe (isJust) import Data.Set (Set, insert, union, unions, empty, toList)  import qualified Djinn.HTypes as D import qualified Djinn.LJT as D +import MonadUtils import qualified DataCon as G import qualified GHC as G import qualified Name as G@@ -19,10 +23,12 @@  getConTs :: G.Type -> Set G.Name getConTs t | Just (_, i)  <- G.splitForAllTy_maybe t = getConTs i+getConTs t | Just (t1,t2) <- G.splitFunTy_maybe t    = getConTs t1 `union` getConTs t2 getConTs t | Just (c, ts) <- G.splitTyConApp_maybe t =    let args = unions $ map getConTs ts    in if G.isTupleTyCon c then args else insert (G.getName c) args getConTs t | Just (t1,t2) <- G.splitAppTy_maybe t    = getConTs t1 `union` getConTs t2+getConTs t | Just _       <- G.getTyVar_maybe t      = empty getConTs _                                           = empty  hType :: G.Type -> D.HType@@ -39,12 +45,12 @@ hType t | Just var <- G.getTyVar_maybe t          = D.HTVar (toHSymbol var) hType _                                           = error "Unimplemented" -environment :: G.GhcMonad m => G.Type -> m HEnvironment-environment = fmap concat . mapM environment1 . toList . getConTs+environment :: G.GhcMonad m => Maybe G.ModuleInfo -> G.Type -> m HEnvironment+environment minfo = fmap concat . mapM (environment1 minfo) . toList . getConTs -environment1 :: G.GhcMonad m => G.Name -> m HEnvironment-environment1 name = do-  thing <- G.lookupGlobalName name+environment1 :: G.GhcMonad m => Maybe G.ModuleInfo -> G.Name -> m HEnvironment+environment1 minfo name = do+  thing <- lookupNameEverywhere minfo name   case thing of     Just (G.ATyCon tycon) | G.isAlgTyCon tycon -> do       let tyconName = toHSymbol $ G.tyConName tycon@@ -53,7 +59,7 @@       dtypes <- forM datacons $ \dcon -> do         let dconN = toHSymbol $ G.dataConName dcon             (_,_,dconT,_) = G.dataConSig dcon-        dconE <- mapM environment dconT+        dconE <- mapM (environment minfo) dconT         return ((dconN, map hType dconT), dconE)       let dtypesT = map fst dtypes           dtypesE = concatMap snd dtypes@@ -65,20 +71,51 @@           varsH = map toHSymbol vars           htype = hType defn       -- Recursively obtain it for the environment of the type-      defnEnv <- environment defn+      defnEnv <- environment minfo defn       return $ (tyconName, (varsH, htype, NoExtraInfo)) : defnEnv     _ -> return [] +lookupNameEverywhere :: G.GhcMonad m => Maybe G.ModuleInfo -> G.Name -> m (Maybe G.TyThing)+lookupNameEverywhere (Just minfo) name = do+  thing <- G.modInfoLookupName minfo name+  if isJust thing then return thing else G.lookupGlobalName name+lookupNameEverywhere Nothing    name = G.lookupGlobalName name+ toHSymbol :: G.NamedThing a => a -> D.HSymbol toHSymbol = G.getOccString +toLJTSymbol :: G.NamedThing a => a -> D.Symbol+toLJTSymbol = D.Symbol . G.getOccString++-- |Bindings which are in scope at a specific point.+type Environment = [(G.Name, G.Type)]++-- |Obtain a maximum number of solutions.+newtype MaxSolutions = Max Int+ -- |Obtain the list of expressions which could fill -- something with the given type. -- The first flag specifies whether to return one -- or more solutions to the problem.-djinn :: G.GhcMonad m => Bool -> G.Type -> m [String]-djinn multi ty = do-  env <- environment ty-  let form = D.hTypeToFormula env (hType ty)-      prfs = D.prove multi [] form-  return $ map show prfs+djinn :: G.GhcMonad m => Bool -> Maybe G.ModuleInfo -> Environment -> G.Type -> MaxSolutions -> Int -> m [String]+djinn multi minfo env ty (Max mx) microsec = do+  tyEnv <- environment minfo ty+  let form = D.hTypeToFormula tyEnv (hType ty)+      envF = map (\(n,t) -> (toLJTSymbol n, D.hTypeToFormula tyEnv (hType t))) env+      prfs = D.prove multi envF form+      trms = map (D.hPrExpr . D.termToHExpr) prfs+  liftIO $ cropList trms microsec mx++cropList :: [a] -> Int -> Int -> IO [a]+cropList _   _  0 = return []+cropList lst ms n = withAsync (let !l = lst in return l) $ \a -> do+                      threadDelay ms+                      res <- poll a+                      case res of+                        Just r -> case r of+                          Right (x:xs) -> do ys <- cropList xs ms (n-1)+                                             return $ x : ys+                          _            -> return []+                        Nothing -> do cancel a+                                      return []+