bail out (f1)

vmchale · Sep 3, 2023 · 25c882c · 25c882c
1 parent c121456
commit 25c882c
Show file tree

Hide file tree

Showing 2 changed files with 15 additions and 61 deletions.
diff --git a/src/Jacinda/Backend/P.hs b/src/Jacinda/Backend/P.hs
@@ -31,22 +31,34 @@ 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
 φ (Cond _ p e0 e1)                                                 = φ p+φ e0+φ e1
 φ (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
@@ -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