jacinda 3.0.0.0 → 3.0.1.0
raw patch · 11 files changed
+151/−97 lines, 11 files
Files
- CHANGELOG.md +5/−0
- README.md +2/−0
- doc/guide.pdf binary
- jacinda.cabal +1/−1
- man/ja.1 +2/−0
- src/A.hs +4/−3
- src/Jacinda/Backend/T.hs +130/−87
- src/L.x +3/−6
- src/Parser.y +2/−0
- src/Parser/Rw.hs +1/−0
- src/Ty.hs +1/−0
CHANGELOG.md view
@@ -1,3 +1,8 @@+# 3.0.1.0++ * Add `,,` (bookend)+ * Add `$>`; stream-and-report+ # 3.0.0.0 * Rewrite backend to always stream/not blow up memory
README.md view
@@ -95,4 +95,6 @@ # Contributing +I have rewritten the code several times so forking and applying patches is fraught!+ Bug reports are welcome contributions.
doc/guide.pdf view
binary file changed (75246 → 75903 bytes)
jacinda.cabal view
@@ -1,6 +1,6 @@ cabal-version: 2.2 name: jacinda-version: 3.0.0.0+version: 3.0.1.0 license: AGPL-3.0-only license-file: COPYING maintainer: vamchale@gmail.com
man/ja.1 view
@@ -191,6 +191,8 @@ else .PP \f[B]<pattern>,,<pattern> <expr>\f[R] Bookend a stream+.PP+\f[B] $> \f[R] Print stream and summary result .SS DECLARATIONS \f[B]:set fs=/REGEX/;\f[R] Set field separator .PP
src/A.hs view
@@ -59,7 +59,7 @@ infixr 0 :$ data T = TyB { tyBuiltin :: TB }- | (:$) { tyApp0 :: T, tyApp1 :: T } -- TODO: :$+ | (:$) { tyApp0 :: T, tyApp1 :: T } | TyArr { tyArr0 :: T, tyArr1 :: T } | TyVar { tyVar :: Nm () } | TyTup { tyTups :: [T] }@@ -150,6 +150,7 @@ | Prior | DedupOn | MapMaybe | Filter | Fold1 | Match | Sprintf+ | Report deriving (Eq) instance Pretty BBin where@@ -160,7 +161,7 @@ pretty Max = "max"; pretty Min = "min"; pretty Prior = "\\."; pretty Filter = "#." pretty Split = "split"; pretty Splitc = "splitc"; pretty Sprintf = "sprintf" pretty Match = "match"; pretty MapMaybe = ":?"; pretty Fold1 = "|>"- pretty Exp = "**"; pretty DedupOn = "~.*"+ pretty Exp = "**"; pretty DedupOn = "~.*"; pretty Report = "$>" data DfnVar = X | Y deriving (Eq) @@ -205,7 +206,6 @@ | Cond { eLoc :: a, eIf :: E a, eThen :: E a, eElse :: E a } | In { oop :: E a, ip :: Maybe (E a), mm :: Maybe (E a), istream :: E a } | RwB { eLoc :: a, eBin :: BBin } | RwT { eLoc :: a, eTer :: BTer }- -- TODO: "Report" aka $> print stream + display summary expression deriving (Functor, Generic) instance Recursive (E a) where@@ -269,6 +269,7 @@ mPrec Leq = Just 4 mPrec Matches = Just 4 mPrec NotMatches = Just 4+mPrec Report = Just 4 mPrec And = Just 3 mPrec Or = Just 2 mPrec _ = Nothing
src/Jacinda/Backend/T.hs view
@@ -5,7 +5,7 @@ import A import A.I import Control.Exception (Exception, throw)-import Control.Monad ((<=<))+import Control.Monad (zipWithM, (<=<)) import Control.Monad.State.Strict (State, evalState, runState, state) import qualified Data.ByteString as BS import Data.ByteString.Builder (hPutBuilder)@@ -49,13 +49,13 @@ -- TODO: dedup... tracking env! type Env = IM.IntMap (Maybe (E T)); type I=Int-data Σ = Σ !I Env (IM.IntMap (S.Set BS.ByteString)) (IM.IntMap IS.IntSet) (IM.IntMap (S.Set Double))+data Σ = Σ !I Env (IM.IntMap (S.Set BS.ByteString)) (IM.IntMap IS.IntSet) (IM.IntMap (S.Set Double)) IS.IntSet type Tmp = Int type Β = IM.IntMap (E T) mE :: (Env -> Env) -> Σ -> Σ-mE f (Σ i e d di df) = Σ i (f e) d di df-gE (Σ _ e _ _ _) = e+mE f (Σ i e d di df b) = Σ i (f e) d di df b+gE (Σ _ e _ _ _ _) = e at :: V.Vector a -> Int -> a v `at` ix = case v V.!? (ix-1) of {Just x -> x; Nothing -> throw $ IndexOutOfBounds ix}@@ -82,32 +82,55 @@ nN :: T -> MM (Nm T) nN t = do {u <- nI; pure (Nm "fold_hole" (U u) t)} +pSF :: Bool -> (Maybe Tmp, [Tmp]) -> [Env] -> IO ()+pSF flush (Just t, tt) [e] = do+ traverse_ (traverse_ (pS flush).(e !)) tt+ traverse_ (pS flush) (e!t)+pSF flush c@(_, tt) (e:es) = do+ traverse_ (traverse_ (pS flush)) [e!t|t <- tt]+ pSF flush c es+pSF _ _ [] = pure ()+ run :: RurePtr -> Bool -> Int -> E T -> [BS.ByteString] -> IO ()-run _ _ _ e _ | TyB TyUnit <- eLoc e = undefined+run r flush j e bs | TyB TyUnit <- eLoc e = (\(s, f, env) -> pSF flush (s,f) env) $ flip evalState j $ do+ (res, tt, iEnv, μ) <- unit e+ u <- nI+ let ctxs=zipWith (\ ~(x,y) z -> (x,y,z)) [(b, splitBy r b) | b <- bs] [1..]+ outs=μ<$>ctxs; es'=scanl' (&) (Σ u iEnv IM.empty IM.empty IM.empty IS.empty) outs+ pure (res, tt, gE<$>es') run r flush j e bs | TyB TyStream:$_ <- eLoc e = traverse_ (traverse_ (pS flush)).flip evalState j $ do t <- nI (iEnv, μ) <- ctx e t u <- nI let ctxs=zipWith (\ ~(x,y) z -> (x,y,z)) [(b, splitBy r b) | b <- bs] [1..]- outs=μ<$>ctxs; es=scanl' (&) (Σ u iEnv IM.empty IM.empty IM.empty) outs+ outs=μ<$>ctxs; es=scanl' (&) (Σ u iEnv IM.empty IM.empty IM.empty IS.empty) outs pure ((! t).gE<$>es)-run r _ j e bs = pDocLn $ evalState (summar r e bs) j+run r _ j e bs = pDocLn $ flip evalState j $ do+ (iEnv, g, e0) <- collect e+ u <- nI+ let ctxs=zipWith (\ ~(x,y) z -> (x,y,z)) [(b, splitBy r b) | b <- bs] [1..]+ updates=g<$>ctxs+ finEnv=foldl' (&) (Σ u iEnv IM.empty IM.empty IM.empty IS.empty) updates+ e0@>(fromMaybe (throw EmptyFold)<$>gE finEnv) +unit :: E T -> MM (Maybe Tmp, [Tmp], Env, LineCtx -> Σ -> Σ)+unit (Anchor _ es) = do+ tt <- traverse (\_ -> nI) es+ (iEnvs, μs) <- unzip <$> zipWithM ctx es tt+ pure (Nothing, tt, fold iEnvs, ts μs)+unit (EApp _ (EApp _ (BB _ Report) es) e) = do+ r <- nI+ t <- nI+ (iEnv, μ) <- ctx es t+ (rEnv, g) <- φ e r+ pure (Just r, [t], iEnv<>rEnv, \l -> μ l.g l)+ pS p = if p then (*>fflush).pDocLn else pDocLn where fflush = hFlush stdout pDocLn :: E T -> IO () pDocLn (Lit _ (FLit f)) = hPutBuilder stdout (doubleDec f <> "\n") pDocLn e = putDoc (pretty e <> hardline) -summar :: RurePtr -> E T -> [BS.ByteString] -> MM (E T)-summar r e bs = do- (iEnv, g, e0) <- collect e- u <- nI- let ctxs=zipWith (\ ~(x,y) z -> (x,y,z)) [(b, splitBy r b) | b <- bs] [1..]- updates=g<$>ctxs- finEnv=foldl' (&) (Σ u iEnv IM.empty IM.empty IM.empty) updates- e0@>(fromMaybe (throw EmptyFold)<$>gE finEnv)- collect :: E T -> MM (Env, LineCtx -> Σ -> Σ, E T) collect e@(EApp ty (EApp _ (EApp _ (TB _ Fold) _) _) _) = do v <- nN ty@@ -121,14 +144,22 @@ (seedEnvs, updates, es') <- unzip3 <$> traverse collect es pure (fold seedEnvs, ts updates, Tup ty es') collect (EApp ty0 (EApp ty1 op@BB{} e0) e1) = do- (env0, f0, e0') <- collect e0 (env1, f1, e1') <- collect e1+ (env0, f0, e0') <- collect e0 pure (env0<>env1, \l -> f1 l.f0 l, EApp ty0 (EApp ty1 op e0') e1')+collect (EApp ty0 (EApp ty1 (EApp ty2 op@TB{} e0) e1) e2) = do+ (env2, f2, e2') <- collect e2+ (env1, f1, e1') <- collect e1+ (env0, f0, e0') <- collect e0+ pure (env0<>env1<>env2, f2@.f1@.f0, EApp ty0 (EApp ty1 (EApp ty2 op e0') e1') e2') collect (EApp ty f@UB{} e) = do (env, fϵ, eϵ) <- collect e pure (env, fϵ, EApp ty f eϵ) collect e@Lit{} = pure (IM.empty, const id, e)+-- TODO: cond +f @. g = \l -> f l.g l+ ts :: [LineCtx -> Σ -> Σ] -> LineCtx -> Σ -> Σ ts = foldl' (\f g l -> f l.g l) (const id) @@ -175,27 +206,28 @@ na=IM.alter go where go Nothing = Just Nothing; go x@Just{} = x ctx :: E T -> Tmp -> MM (Env, LineCtx -> Σ -> Σ)-ctx AllColumn{} res = pure (ni res, \ ~(b, _, _) -> mE$IM.insert res (Just$!mkStr b))-ctx (ParseAllCol (_:$TyB TyI)) res = pure (ni res, \ ~(b, _, _) -> mE$IM.insert res (Just$!parseAsEInt b))-ctx (ParseAllCol (_:$TyB TyFloat)) res = pure (ni res, \ ~(b, _, _) -> mE$IM.insert res (Just$!parseAsF b))-ctx FParseAllCol{} res = pure (ni res, \ ~(b, _, _) -> mE$IM.insert res (Just$!parseAsF b))-ctx IParseAllCol{} res = pure (ni res, \ ~(b, _, _) -> mE$IM.insert res (Just$!parseAsEInt b))-ctx (Column _ i) res = pure (ni res, \ ~(b, bs, _) -> mE$IM.insert res (Just$mkStr (fieldOf bs b i)))-ctx (FParseCol _ i) res = pure (ni res, \ ~(b, bs, _) -> mE$IM.insert res (Just$!parseAsF (fieldOf bs b i)))-ctx (IParseCol _ i) res = pure (ni res, \ ~(b, bs, _) -> mE$IM.insert res (Just$!parseAsEInt (fieldOf bs b i)))-ctx (ParseCol (_:$TyB TyFloat) i) res = pure (ni res, \ ~(b, bs, _) -> mE$IM.insert res (Just$!parseAsF (fieldOf bs b i)))-ctx (ParseCol (_:$TyB TyI) i) res = pure (ni res, \ ~(b, bs, _) -> mE$IM.insert res (Just$!parseAsEInt (fieldOf bs b i)))-ctx (EApp _ (EApp _ (BB _ Map) f) xs) o = do {t <- nI; (env, sb) <- ctx xs t; pure (na o env, \l->wM f t o.sb l)}-ctx (EApp _ (EApp _ (BB _ MapMaybe) f) xs) o = do {t <- nI; (env, sb) <- ctx xs t; pure (na o env, \l->wMM f t o.sb l)}-ctx (EApp _ (UB _ CatMaybes) xs) o = do {t <- nI; (env, sb) <- ctx xs t; pure (na o env, \l->wCM t o.sb l)}-ctx (EApp _ (EApp _ (BB _ Filter) p) xs) o = do {t <- nI; (env, sb) <- ctx xs t; pure (na o env, \l->wP p t o.sb l)}-ctx (Guarded _ p e) o = pure (ni o, wG (p, e) o)-ctx (Implicit _ e) o = pure (ni o, wI e o)-ctx (EApp _ (EApp _ (EApp _ (TB _ Scan) op) seed) xs) o = do {t <- nI; (env, sb) <- ctx xs t; seed' <- seed@>mempty; pure (IM.insert o (Just$!seed') env, \l->wF op t o.sb l)}-ctx (EApp _ (EApp _ (EApp _ (TB _ ZipW) op) xs) ys) o = do {t0 <- nI; t1 <- nI; (env0, sb0) <- ctx xs t0; (env1, sb1) <- ctx ys t1; pure (na o (env0<>env1), \l->wZ op t0 t1 o.sb0 l.sb1 l)}-ctx (EApp _ (EApp _ (BB _ Prior) op) xs) o = do {t <- nI; (env, sb) <- ctx xs t; pt <- nI; pure (na o (IM.insert pt Nothing env), \l -> wΠ op pt t o.sb l)}-ctx (EApp (_:$TyB ty) (UB _ Dedup) xs) o = do {k <- nI; t <- nI; (env, sb) <- ctx xs t; pure (na o env, \l->wD ty k t o.sb l)}-ctx (EApp _ (EApp _ (BB _ DedupOn) f) xs) o = do {k <- nI; t <- nI; (env, sb) <- ctx xs t; pure (na o env, \l->wDOp f k t o.sb l)}+ctx AllColumn{} res = pure (ni res, \ ~(b, _, _) -> mE$IM.insert res (Just$!mkStr b))+ctx (ParseAllCol (_:$TyB TyI)) res = pure (ni res, \ ~(b, _, _) -> mE$IM.insert res (Just$!parseAsEInt b))+ctx (ParseAllCol (_:$TyB TyFloat)) res = pure (ni res, \ ~(b, _, _) -> mE$IM.insert res (Just$!parseAsF b))+ctx FParseAllCol{} res = pure (ni res, \ ~(b, _, _) -> mE$IM.insert res (Just$!parseAsF b))+ctx IParseAllCol{} res = pure (ni res, \ ~(b, _, _) -> mE$IM.insert res (Just$!parseAsEInt b))+ctx (Column _ i) res = pure (ni res, \ ~(b, bs, _) -> mE$IM.insert res (Just$mkStr (fieldOf bs b i)))+ctx (FParseCol _ i) res = pure (ni res, \ ~(b, bs, _) -> mE$IM.insert res (Just$!parseAsF (fieldOf bs b i)))+ctx (IParseCol _ i) res = pure (ni res, \ ~(b, bs, _) -> mE$IM.insert res (Just$!parseAsEInt (fieldOf bs b i)))+ctx (ParseCol (_:$TyB TyFloat) i) res = pure (ni res, \ ~(b, bs, _) -> mE$IM.insert res (Just$!parseAsF (fieldOf bs b i)))+ctx (ParseCol (_:$TyB TyI) i) res = pure (ni res, \ ~(b, bs, _) -> mE$IM.insert res (Just$!parseAsEInt (fieldOf bs b i)))+ctx (EApp _ (EApp _ (BB _ Map) f) xs) o = do {t <- nI; (env, sb) <- ctx xs t; pure (na o env, \l->wM f t o.sb l)}+ctx (EApp _ (EApp _ (BB _ MapMaybe) f) xs) o = do {t <- nI; (env, sb) <- ctx xs t; pure (na o env, \l->wMM f t o.sb l)}+ctx (EApp _ (UB _ CatMaybes) xs) o = do {t <- nI; (env, sb) <- ctx xs t; pure (na o env, \l->wCM t o.sb l)}+ctx (EApp _ (EApp _ (BB _ Filter) p) xs) o = do {t <- nI; (env, sb) <- ctx xs t; pure (na o env, \l->wP p t o.sb l)}+ctx (Guarded _ p e) o = pure (ni o, wG (p, e) o)+ctx (Implicit _ e) o = pure (ni o, wI e o)+ctx (EApp _ (EApp _ (EApp _ (TB _ Scan) op) seed) xs) o = do {t <- nI; (env, sb) <- ctx xs t; seed' <- seed@>mempty; pure (IM.insert o (Just$!seed') env, \l->wF op t o.sb l)}+ctx (EApp _ (EApp _ (EApp _ (TB _ ZipW) op) xs) ys) o = do {t0 <- nI; t1 <- nI; (env0, sb0) <- ctx xs t0; (env1, sb1) <- ctx ys t1; pure (na o (env0<>env1), \l->wZ op t0 t1 o.sb0 l.sb1 l)}+ctx (EApp _ (EApp _ (BB _ Prior) op) xs) o = do {t <- nI; (env, sb) <- ctx xs t; pt <- nI; pure (na o (IM.insert pt Nothing env), \l -> wΠ op pt t o.sb l)}+ctx (EApp (_:$TyB ty) (UB _ Dedup) xs) o = do {k <- nI; t <- nI; (env, sb) <- ctx xs t; pure (na o env, \l->wD ty k t o.sb l)}+ctx (EApp _ (EApp _ (BB _ DedupOn) f) xs) o = do {k <- nI; t <- nI; (env, sb) <- ctx xs t; pure (na o env, \l->wDOp f k t o.sb l)}+ctx (EApp _ (EApp _ (EApp _ (TB _ Bookend) e0) e1) xs) o = do {k <- nI; t <- nI; (env, sb) <- ctx xs t; r0 <- e0@>mempty; r1<- e1@>mempty; pure (na o env, \l->wB (r0,r1) k t o.sb l)} type LineCtx = (BS.ByteString, V.Vector BS.ByteString, Integer) -- line number @@ -431,78 +463,78 @@ ms (Nm _ (U i) _) = IM.singleton i wCM :: Tmp -> Tmp -> Σ -> Σ-wCM src tgt (Σ u env d di df) =+wCM src tgt (Σ u env d di df b) = let xϵ=env!src in Σ u (case xϵ of Just y -> case asM y of {Nothing -> IM.insert tgt Nothing env; Just yϵ -> IM.insert tgt (Just$!yϵ) env}- Nothing -> IM.insert tgt Nothing env) d di df+ Nothing -> IM.insert tgt Nothing env) d di df b wMM :: E T -> Tmp -> Tmp -> Σ -> Σ-wMM (Lam _ n e) src tgt (Σ j env d di df) =+wMM (Lam _ n e) src tgt (Σ j env d di df b) = let xϵ=env!src in case xϵ of Just x -> let be=ms n x; (y,k)=e@!(j,be) in Σ k (case asM y of Just yϵ -> IM.insert tgt (Just$!yϵ) env- Nothing -> IM.insert tgt Nothing env) d di df- Nothing -> Σ j (IM.insert tgt Nothing env) d di df+ Nothing -> IM.insert tgt Nothing env) d di df b+ Nothing -> Σ j (IM.insert tgt Nothing env) d di df b wMM e _ _ _ = throw$InternalArityOrEta 1 e wZ :: E T -> Tmp -> Tmp -> Tmp -> Σ -> Σ-wZ (Lam _ n0 (Lam _ n1 e)) src0 src1 tgt (Σ j env d di df) =+wZ (Lam _ n0 (Lam _ n1 e)) src0 src1 tgt (Σ j env d di df b) = let x0ϵ=env!src0; x1ϵ=env!src1 in (case (x0ϵ, x1ϵ) of (Just x, Just y) -> let be=me [(n0, x), (n1, y)]; (z,k)=e@!(j,be) in Σ k (IM.insert tgt (Just$!z) env)- (Nothing, Nothing) -> Σ j (IM.insert tgt Nothing env)) d di df+ (Nothing, Nothing) -> Σ j (IM.insert tgt Nothing env)) d di df b wZ e _ _ _ _ = throw$InternalArityOrEta 2 e wM :: E T -> Tmp -> Tmp -> Σ -> Σ-wM (Lam _ n e) src tgt (Σ j env d di df) =+wM (Lam _ n e) src tgt (Σ j env d di df b) = let xϵ=env!src in case xϵ of Just x -> let be=ms n x; (y,k)=e@!(j,be)- in Σ k (IM.insert tgt (Just$!y) env) d di df- Nothing -> Σ j (IM.insert tgt Nothing env) d di df+ in Σ k (IM.insert tgt (Just$!y) env) d di df b+ Nothing -> Σ j (IM.insert tgt Nothing env) d di df b wM e _ _ _ = throw$InternalArityOrEta 1 e wI :: E T -> Tmp -> LineCtx -> Σ -> Σ-wI e tgt line (Σ j env d di df) =- let e'=e `κ` line; (e'',k)=e'$@j in Σ k (IM.insert tgt (Just$!e'') env) d di df+wI e tgt line (Σ j env d di df b) =+ let e'=e `κ` line; (e'',k)=e'$@j in Σ k (IM.insert tgt (Just$!e'') env) d di df b wG :: (E T, E T) -> Tmp -> LineCtx -> Σ -> Σ-wG (p, e) tgt line (Σ j env d di df) =+wG (p, e) tgt line (Σ j env d di df b) = let p'=p `κ` line; (p'',k)=p'$@j- in if asB p''- then let e'=e `κ` line; (e'',u) =e'$@k in Σ u (IM.insert tgt (Just$!e'') env) d di df- else Σ k (IM.insert tgt Nothing env) d di df+ in (if asB p''+ then let e'=e `κ` line; (e'',u) =e'$@k in Σ u (IM.insert tgt (Just$!e'') env)+ else Σ k (IM.insert tgt Nothing env)) d di df b wDOp :: E T -> Int -> Tmp -> Tmp -> Σ -> Σ-wDOp (Lam (TyArr _ (TyB TyStr)) n e) key src tgt (Σ i env d di df) =+wDOp (Lam (TyArr _ (TyB TyStr)) n e) key src tgt (Σ i env d di df b) = let x=env!src in case x of- Nothing -> Σ i (IM.insert tgt Nothing env) d di df+ Nothing -> Σ i (IM.insert tgt Nothing env) d di df b Just xϵ -> case IM.lookup key d of- Nothing -> Σ k (IM.insert tgt (Just$!y) env) (IM.insert key (S.singleton e') d) di df- Just ss -> (if e' `S.member` ss then Σ k (IM.insert tgt Nothing env) d else Σ k (IM.insert tgt (Just$!y) env) (IM.alter go key d)) di df+ Nothing -> Σ k (IM.insert tgt (Just$!y) env) (IM.insert key (S.singleton e') d) di df b+ Just ss -> (if e' `S.member` ss then Σ k (IM.insert tgt Nothing env) d else Σ k (IM.insert tgt (Just$!y) env) (IM.alter go key d)) di df b where (y,k)=e@!(i,be); be=ms n xϵ e'=asS y go Nothing = Just$!S.singleton e' go (Just s) = Just$!S.insert e' s-wDOp (Lam (TyArr _ (TyB TyI)) n e) key src tgt (Σ i env d di df) =+wDOp (Lam (TyArr _ (TyB TyI)) n e) key src tgt (Σ i env d di df b) = let x=env!src in case x of- Nothing -> Σ i (IM.insert tgt Nothing env) d di df+ Nothing -> Σ i (IM.insert tgt Nothing env) d di df b Just xϵ -> case IM.lookup key di of- Nothing -> Σ k (IM.insert tgt (Just$!y) env) d (IM.insert key (IS.singleton e') di) df- Just ds -> (if e' `IS.member` ds then Σ k (IM.insert tgt Nothing env) d di else Σ k (IM.insert tgt (Just$!y) env) d (IM.alter go key di)) df+ Nothing -> Σ k (IM.insert tgt (Just$!y) env) d (IM.insert key (IS.singleton e') di) df b+ Just ds -> (if e' `IS.member` ds then Σ k (IM.insert tgt Nothing env) d di else Σ k (IM.insert tgt (Just$!y) env) d (IM.alter go key di)) df b where (y,k)=e@!(i,be); be=ms n xϵ@@ -510,76 +542,87 @@ go Nothing = Just$!IS.singleton e' go (Just s) = Just$!IS.insert e' s-wDOp (Lam (TyArr _ (TyB TyFloat)) n e) key src tgt (Σ i env d di df) =+wDOp (Lam (TyArr _ (TyB TyFloat)) n e) key src tgt (Σ i env d di df b) = let x=env!src in case x of- Nothing -> Σ i (IM.insert tgt Nothing env) d di df+ Nothing -> Σ i (IM.insert tgt Nothing env) d di df b Just xϵ -> case IM.lookup key df of- Nothing -> Σ k (IM.insert tgt (Just$!y) env) d di (IM.insert key (S.singleton e') df)- Just ds -> if e' `S.member` ds then Σ k (IM.insert tgt Nothing env) d di df else Σ k (IM.insert tgt (Just$!y) env) d di (IM.alter go key df)+ Nothing -> Σ k (IM.insert tgt (Just$!y) env) d di (IM.insert key (S.singleton e') df) b+ Just ds -> if e' `S.member` ds then Σ k (IM.insert tgt Nothing env) d di df b else Σ k (IM.insert tgt (Just$!y) env) d di (IM.alter go key df) b where (y,k)=e@!(i,be); be=ms n xϵ e'=asF y - go Nothing = Just$!S.singleton e'+ go Nothing = Just$!S.singleton e' go (Just s) = Just$!S.insert e' s wDOp e _ _ _ _ = throw $ InternalArityOrEta 1 e +wB :: (E T, E T) -> Int -> Tmp -> Tmp -> Σ -> Σ+wB (e0, e1) key src tgt (Σ i env d di df b) =+ let x=env!src+ in case x of+ Nothing -> Σ i (IM.insert tgt Nothing env) d di df b+ Just xϵ -> let xS=asS xϵ in if key `IS.member` b+ then if isMatch' r1 xS then Σ i (IM.insert tgt (Just$!xϵ) env) d di df (IS.delete key b) else Σ i (IM.insert tgt (Just$!xϵ) env) d di df b+ else if isMatch' r0 xS then Σ i (IM.insert tgt (Just$!xϵ) env) d di df (IS.insert key b) else Σ i (IM.insert tgt Nothing env) d di df b+ where+ r0=asR e0; r1=asR e1+ wD :: TB -> Int -> Tmp -> Tmp -> Σ -> Σ-wD TyStr key src tgt (Σ i env d di df) =+wD TyStr key src tgt (Σ i env d di df b) = let x=env!src in case x of- Nothing -> Σ i (IM.insert tgt Nothing env) d di df+ Nothing -> Σ i (IM.insert tgt Nothing env) d di df b Just e -> case IM.lookup key d of- Nothing -> Σ i (IM.insert tgt (Just$!e) env) (IM.insert key (S.singleton e') d) di df- Just ds -> (if e' `S.member` ds then Σ i (IM.insert tgt Nothing env) d else Σ i (IM.insert tgt (Just$!e) env) (IM.alter go key d)) di df+ Nothing -> Σ i (IM.insert tgt (Just$!e) env) (IM.insert key (S.singleton e') d) di df b+ Just ds -> (if e' `S.member` ds then Σ i (IM.insert tgt Nothing env) d else Σ i (IM.insert tgt (Just$!e) env) (IM.alter go key d)) di df b where go Nothing = Just$!S.singleton e' go (Just s) = Just$!S.insert e' s e'=asS e-wD TyI key src tgt (Σ i env d di df) =+wD TyI key src tgt (Σ i env d di df b) = let x=env!src in case x of- Nothing -> Σ i (IM.insert tgt Nothing env) d di df+ Nothing -> Σ i (IM.insert tgt Nothing env) d di df b Just e -> case IM.lookup key di of- Nothing -> Σ i (IM.insert tgt (Just$!e) env) d (IM.insert key (IS.singleton e') di) df- Just ds -> (if e' `IS.member` ds then Σ i (IM.insert tgt Nothing env) d di else Σ i (IM.insert tgt (Just$!e) env) d (IM.alter go key di)) df+ Nothing -> Σ i (IM.insert tgt (Just$!e) env) d (IM.insert key (IS.singleton e') di) df b+ Just ds -> (if e' `IS.member` ds then Σ i (IM.insert tgt Nothing env) d di else Σ i (IM.insert tgt (Just$!e) env) d (IM.alter go key di)) df b where e'=fromIntegral$asI e go Nothing = Just$!IS.singleton e' go (Just s) = Just$!IS.insert e' s-wD TyFloat key src tgt (Σ i env d di df) =+wD TyFloat key src tgt (Σ i env d di df b) = let x=env!src in case x of- Nothing -> Σ i (IM.insert tgt Nothing env) d di df+ Nothing -> Σ i (IM.insert tgt Nothing env) d di df b Just e -> case IM.lookup key df of- Nothing -> Σ i (IM.insert tgt (Just$!e) env) d di (IM.insert key (S.singleton e') df)- Just ds -> if e' `S.member` ds then Σ i (IM.insert tgt Nothing env) d di df else Σ i (IM.insert tgt (Just$!e) env) d di (IM.alter go key df)+ Nothing -> Σ i (IM.insert tgt (Just$!e) env) d di (IM.insert key (S.singleton e') df) b+ Just ds -> (if e' `S.member` ds then Σ i (IM.insert tgt Nothing env) d di df else Σ i (IM.insert tgt (Just$!e) env) d di (IM.alter go key df)) b where e'=asF e - go Nothing = Just$!S.singleton e'+ go Nothing = Just$!S.singleton e' go (Just s) = Just$!S.insert e' s wP :: E T -> Tmp -> Tmp -> Σ -> Σ-wP (Lam _ n e) src tgt (Σ j env d di df) =+wP (Lam _ n e) src tgt (Σ j env d di df b) = let xϵ=env!src in case xϵ of Just x -> let be=ms n x; (p,k)=e@!(j,be)- in Σ k (IM.insert tgt (if asB p then Just$!x else Nothing) env) d di df- Nothing -> Σ j (IM.insert tgt Nothing env) d di df+ in Σ k (IM.insert tgt (if asB p then Just$!x else Nothing) env) d di df b+ Nothing -> Σ j (IM.insert tgt Nothing env) d di df b wP e _ _ _ = throw $ InternalArityOrEta 1 e wΠ :: E T -> Tmp -> Tmp -> Tmp -> Σ -> Σ-wΠ (Lam _ nn (Lam _ nprev e)) pt src tgt (Σ j env d di df) =+wΠ (Lam _ nn (Lam _ nprev e)) pt src tgt (Σ j env d di df b) = let prevϵ=env!pt; xϵ=env!src in (case (prevϵ, xϵ) of (Just prev, Just x) ->@@ -588,11 +631,11 @@ in Σ u (IM.insert pt (Just$!x) (IM.insert tgt (Just$!res) env)) (Nothing, Nothing) -> Σ j (IM.insert tgt Nothing env) (Nothing, Just x) -> Σ j (IM.insert pt (Just$!x) (IM.insert tgt Nothing env))- (Just{}, Nothing) -> Σ j (IM.insert tgt Nothing env)) d di df+ (Just{}, Nothing) -> Σ j (IM.insert tgt Nothing env)) d di df b wΠ e _ _ _ _ = throw $ InternalArityOrEta 2 e wF :: E T -> Tmp -> Tmp -> Σ -> Σ-wF (Lam _ nacc (Lam _ nn e)) src tgt (Σ j env d di df) =+wF (Lam _ nacc (Lam _ nn e)) src tgt (Σ j env d di df b) = let accϵ = env!tgt; xϵ = env!src in (case (accϵ, xϵ) of (Just acc, Just x) ->@@ -601,5 +644,5 @@ in Σ u (IM.insert tgt (Just$!res) env) (Just acc, Nothing) -> Σ j (IM.insert tgt (Just$!acc) env) (Nothing, Nothing) -> Σ j (IM.insert tgt Nothing env)- (Nothing, Just x) -> Σ j (IM.insert tgt (Just$!x) env)) d di df+ (Nothing, Just x) -> Σ j (IM.insert tgt (Just$!x) env)) d di df b wF e _ _ _ = throw $ InternalArityOrEta 2 e
src/L.x view
@@ -369,14 +369,11 @@ | KwAsv | KwUsv -- | Reserved/special variables-data Var = VarX- | VarY+data Var = VarX | VarY | VarFs | VarRs | VarOfs | VarOrs- | VarIx- | VarMin- | VarMax- | VarNf+ | VarIx | VarNf+ | VarMin | VarMax instance Pretty Var where pretty VarX = "x"
src/Parser.y view
@@ -65,6 +65,7 @@ ceilSym { TokSym $$ CeilSym } dedup { TokSym $$ DedupTok } dedupon { TokSym $$ DedupOnTok }+ report { TokSym $$ IceCreamCone } plus { TokSym $$ PlusTok } minus { TokSym $$ MinusTok }@@ -206,6 +207,7 @@ | fold1 { Fold1 } | exp { Exp } | dedupon { DedupOn }+ | report { Report } Bind :: { (Nm AlexPosn, E AlexPosn) } : val name defEq E { ($2, $4) }
src/Parser/Rw.hs view
@@ -41,6 +41,7 @@ mFi Match = Nothing mFi Prior = Just 5 mFi DedupOn = Just 5+mFi Report = Just 4 isPre :: BUn -> Bool isPre At{} = False
src/Ty.hs view
@@ -395,6 +395,7 @@ tyES s (UB _ FParse) = pure (UB (tyArr tyStr tyF) FParse, s) tyES s (UB _ Floor) = pure (UB (tyArr tyF tyI) Floor, s) tyES s (UB _ Ceiling) = pure (UB (tyF ~> tyI) Ceiling, s)+tyES s (BB _ Report) = do {a <- var <$> freshN "a"; b <- var <$> freshN "b"; pure (BB (tyStream a ~> b ~> TyB TyUnit) Report, s)} tyES s (UB _ TallyList) = do {a <- var <$> freshN "a"; pure (UB (a ~> tyI) TallyList, s)} tyES s (UB l Negate) = do {a <- freshN "a"; modify (mapCV (addC a (IsNum, l))); let a'=var a in pure (UB (tyArr a' a') Negate, s)} tyES s (UB _ Some) = do {a <- var <$> freshN "a"; pure (UB (tyArr a (tyOpt a)) Some, s)}