diff --git a/src/Jacinda/Backend/P.hs b/src/Jacinda/Backend/P.hs index f94def22..615f42b4 100644 --- a/src/Jacinda/Backend/P.hs +++ b/src/Jacinda/Backend/P.hs @@ -31,9 +31,18 @@ import System.IO (hFlush, stdout) import Ty.Const import U +φ1 :: E T -> Int +φ1 (BB (TyArr _ (TyArr (TyApp (TyB TyStream) _) _)) Fold1) = 1 +φ1 (EApp _ e0 e1) = φ1 e0+φ1 e1 +φ1 (Tup _ es) = sum (φ1<$>es) +φ1 (OptionVal _ (Just e)) = φ1 e +φ1 (Cond _ p e0 e1) = φ1 p+φ1 e0+φ1 e1 +φ1 (Lam _ _ e) = φ1 e +φ1 _ = 0 + + φ :: E T -> Int φ (TB (TyArr _ (TyArr _ (TyArr (TyApp (TyB TyStream) _) _))) Fold) = 1 -φ (BB (TyArr _ (TyArr (TyApp (TyB TyStream) _) _)) Fold1) = 1 φ (EApp _ e0 e1) = φ e0+φ e1 φ (Tup _ es) = sum (φ<$>es) φ (OptionVal _ (Just e)) = φ e @@ -41,12 +50,15 @@ import U φ (Lam _ _ e) = φ e φ _ = 0 +noleak :: E T -> Bool +noleak e = φ e > 1 && φ1 e < 1 + runJac :: RurePtr -- ^ Record separator -> Bool -- ^ Flush output? -> Int -> E T -> Either StreamError ([BS.ByteString] -> IO ()) -runJac re f i e = ϝ (bsProcess re f) (if φ e > 1 then fuse i e else (e, i)) where ϝ = uncurry.flip +runJac re f i e = ϝ (bsProcess re f) (if noleak e then fuse i e else (e, i)) where ϝ = uncurry.flip data StreamError = NakedField deriving (Show) @@ -119,7 +131,6 @@ gf (Lam t n e) = Lam t n <$> gf e gf e@BB{} = pure e; gf e@TB{} = pure e; gf e@UB{} = pure e; gf e@NB{} = pure e gf e@StrLit{} = pure e; gf e@FLit{} = pure e; gf e@ILit{} = pure e; gf e@BLit{} = pure e gf e@RC{} = pure e; gf e@Var{} = pure e -gf In{} = error "Not yet implemented." ug :: IM.IntMap (E T) -> E T -> E T ug st (Var _ n@(Nm _ (U i) _)) = @@ -149,7 +160,7 @@ scanM op seed xs = sequence $ scanl' go (pure seed) xs where go seedϵ x = do {seedϵ' <- seedϵ; op seedϵ' x} eF :: Int -> RurePtr -> E T -> [BS.ByteString] -> E T -eF u r e | φ e > 1 = \bs -> +eF u r e | noleak e = \bs -> let (eHoley, (_, folds)) = runState (gf e) (0, []) (filledHoles, u') = foldAll u r folds bs in eB u' (pure.ug (IM.fromList filledHoles)) eHoley diff --git a/src/Jacinda/Fuse.hs b/src/Jacinda/Fuse.hs index ed0deb94..3b4d9a62 100644 --- a/src/Jacinda/Fuse.hs +++ b/src/Jacinda/Fuse.hs @@ -56,64 +56,7 @@ fM (EApp t0 (EApp t1 (EApp t2 ho@(TB _ Fold) op) seed) stream) | TyApp (TyB TySt fop=Lam fopT s (Lam popT x (EApp sTy (EApp undefined (EApp undefined (TB (TyArr sTy (TyArr undefined (TyArr xMT sTy))) Option) sE) (EApp undefined op sE)) xE)) fM (EApp sTy (EApp undefined (EApp undefined (TB (TyArr fopT (TyArr sTy (TyArr (TyApp (TyB TyStream) xMT) sTy))) Fold) fop) seed) xs) _ -> pure (EApp t0 (EApp t1 (EApp t2 ho op) seed) stream') -fM (EApp t0 (EApp t1 ho@(BB _ Fold1) op) stream) | TyApp (TyB TyStream) _ <- eLoc stream = do - stream' <- fM stream - case stream' of - (EApp _ (EApp _ (BB _ Filter) p) xs) -> - fM (In op (Just p) Nothing xs) - (EApp _ (EApp _ (BB _ MapMaybe) f) xs) -> - fM (In op Nothing (Just f) xs) - (Guarded t p e) -> do - let xT=eLoc e - x <- nN "x" xT - fM (In op (Just $ Lam (TyArr xT tyB) x p) Nothing (Implicit t e)) - (EApp _ (EApp _ (BB _ Map) f) (EApp _ (EApp _ (BB _ Filter) p) xs)) -> - undefined - (EApp _ (EApp _ (BB _ Map) f) (Guarded t p e)) -> - undefined - (EApp _ (UB _ CatMaybes) xs) -> - undefined - _ -> pure (EApp t0 (EApp t1 ho op) stream) -fM (In op mQ mG stream) = do - stream' <- fM stream - case stream' of - (EApp _ (EApp _ (BB _ Filter) p) xs) -> - case mQ of - Nothing -> fM (In op (Just p) mG xs) - Just q | TyArr xT _ <- eLoc q -> do - x <- nN "x" xT - let xE=Var xT x - fM (In op (Just $ Lam (TyArr xT tyB) x (EApp tyB p xE `andE` EApp tyB q xE)) mG xs) - (Guarded t p e) -> - case mQ of - Nothing -> do - let xT=eLoc e - x <- nN "x" xT - fM (In op (Just $ Lam (TyArr xT tyB) x p) Nothing (Implicit t e)) - Just q | TyArr xT _ <- eLoc q -> do - x <- nN "x" xT - let xE=Var xT x - fM (In op (Just $ Lam (TyArr xT tyB) x (p `andE` EApp tyB q xE)) mG (Implicit t e)) - (EApp _ (EApp _ (BB _ Map) f) (EApp _ (EApp _ (BB _ Filter) p) xs)) -> - undefined - (EApp _ (EApp _ (BB _ Map) f) (Guarded t p e)) -> - undefined - (EApp _ (UB _ CatMaybes) xs) -> - undefined - (EApp _ (EApp _ (BB _ MapMaybe) f) xs) -> - undefined - _ -> pure (In op mQ mG stream') fM (Tup t es) = Tup t <$> traverse fM es fM (EApp t e0 e1) = EApp t <$> fM e0 <*> fM e1 fM (Lam t n e) = Lam t n <$> fM e fM e = pure e - --- f <=< g -- λx. option None f (g x) -composeM :: E T -> E T -> M (E T) -composeM f g | TyArr xT yT <- eLoc g, TyArr _ cod <- eLoc f = do - x <- nN "x" xT - let xE=Var xT x - pure $ Lam (TyArr xT cod) x (EApp cod (EApp undefined (EApp undefined (TB undefined Option) (NB cod None)) f) (EApp yT g xE)) - -andE :: E T -> E T -> E T -andE x y | tX <- eLoc x, tY <- eLoc y = EApp tyB (EApp (TyArr tY tyB) (BB (TyArr tX (TyArr tY tyB)) Or) x) y