(* bool-check-for-all problem example *)
let build_Vec := λ t: Type →
  let bv_intern := μ bv_intern →
    λ pvn: Nat → λ pv: Vec pvn t →
      λ n: Nat → match n {
        Z ⇒ pvn
        S n ⇒ λ x: t → bv_intern (S pvn) (Cons pv x) n
      };
  bv_intern Z Nil
let nat! := unary! Z S
let bcfamul :=
  μ bcfamul →
    λ n: Nat → λ f: (Vec n Bool → Bool) → match n {
      Z ⇒ f Nil;
      S n ⇒ bcfamul n (λ tv → do {
        f (Cons tv False);
        f (Cons tv True);
      })
    }
let n4 = nat! 4
bcfamul n4 (λ (build_Vec Bool n4 $a $b $c $d) : Vec n4 Bool → {
})

module GardGround.Utils.ListMaybe (
  ListMaybe(ListMaybe),
  push,
  fromList,
  toList
) where
data ListMaybe a = ListMaybe Int [(a, [a], Int)]
push :: Maybe a -> ListMaybe a -> ListMaybe a
push Nothing (ListMaybe i xs) = ListMaybe (i + 1) xs
push (Just x) (ListMaybe 0 ((y, ys, i):xs)) = ListMaybe 0 $ (x, y:ys, i):xs
push (Just x) (ListMaybe i xs) = ListMaybe 0 $ (x, [], i):xs
fromList :: [Maybe a] -> ListMaybe a
fromList = foldl (flip push) (ListMaybe 0 [])
toList :: ListMaybe a -> [Maybe a]
toList (ListMaybe 0 []) = []
toList (ListMaybe 0 ((y, [], i):xs)) = (Just y):(toList $ ListMaybe i xs)
toList (ListMaybe 0 ((y, y2:ys, i):xs)) = (Just y):(toList $ ListMaybe 0 $ (y2, ys, i):xs)
toList (ListMaybe i xs) = Nothing:(toList $ ListMaybe (i - 1) xs)
instance Functor ListMaybe where
    fmap f (ListMaybe i xs) = ListMaybe i (fmap (\(y, ys, j) -> (f y, fmap f ys, j)) xs)
    {-# INLINE fmap #-}

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE RankNTypes #-}
module GardGround.Utils.Fusion (
    Step(..),
    stepState,
    runSteps,
    StepFun(..),
    Stream,
    runStream,
    embedTfs,
    step
) where
import Control.Applicative (Alternative(..))
import Prelude hiding (filter)
import Data.Bifunctor
import qualified Data.Text.Internal.Fusion as TF
data Step s a = Done | Skip !s | Yield !a !s
instance Functor (Step s) where
    fmap _ Done = Done
    fmap _ (Skip s) = Skip s
    fmap f (Yield a s) = Yield (f a) s
    {-# INLINE fmap #-}
instance Bifunctor Step where
    bimap _ _ Done = Done
    bimap f _ (Skip s) = Skip (f s)
    bimap f g (Yield a s) = Yield (g a) (f s)
    {-# INLINE bimap #-}
stepState :: Step s a -> Maybe s
stepState Done = Nothing
stepState (Skip st) = Just st
stepState (Yield _ st) = Just st
data StepFun s a = StepFun (s -> Step s a)
instance Functor (StepFun s) where
    fmap f inif = inif >>= (\x -> pure (f x))
    {-# INLINE fmap #-}
instance Applicative (StepFun s) where
    pure x = StepFun $ \st -> Yield x st
    {-# INLINE pure #-}
    f <*> v = f >>= (\fx -> v >>= (\vx -> StepFun $ Yield (fx vx)))
instance Monad (StepFun s) where
    return = pure
    (StepFun f1) >>= f2 = StepFun go
      where
        go st = case f1 st of
          Done -> Done
          Skip st2 -> Skip st2
          Yield x st2 -> let (StepFun f3) = (f2 x) in f3 st2
-- this makes `guard` work
instance Alternative (StepFun s) where
    empty = StepFun $ Skip
    {-# INLINE empty #-}
    StepFun f1 <|> StepFun f2 = StepFun $ \st ->
      case f1 st of
        Yield a st2 -> Yield a st2
        -- backtracking
        Done -> f2 st
        Skip _ -> f2 st
runSteps :: StepFun s a -> s -> [a]
runSteps (StepFun sf) = go
  where
    go st = case sf st of
      Done -> []
      Skip st2 -> go st2
      Yield a st2 -> a:(go st2)
data Stream a = forall s. Stream
    (StepFun s a)   -- ^ stepper function
    !s              -- ^ current state
instance Functor Stream where
    fmap f (Stream step_ cst) = Stream (fmap f step_) cst
runStream :: Stream a -> [a]
runStream (Stream sf ctx) = runSteps sf ctx
{-# INLINE runStream #-}
smap :: TF.Step s a -> Step s a
smap  TF.Done         = Done
smap (TF.Skip st)     = Skip st
smap (TF.Yield av st) = Yield av st
-- | embed a stream from Data.Text into our stream type
embedTfs :: TF.Stream x -> Stream x
embedTfs (TF.Stream step_ st _) = Stream (StepFun (smap . step_)) st
-- | step an inner stream;
-- forwards skips and turns Done into Nothing-yields
step :: StepFun (Stream a) (Maybe a)
step = StepFun $ \(Stream (StepFun f) st) -> case f st of
    Done -> Yield Nothing (Stream (StepFun f) st)
    Skip st2 -> Skip (Stream (StepFun f) st2)
    Yield x st2 -> Yield (Just x) (Stream (StepFun f) st2)

cabal-version:   3.0
name:            gardground-core
version:         0.1.0.0
synopsis:        GardGround core and utilities
license:         Apache-2.0
author:          Alain Emilia Anna Zscheile
maintainer:      fogti+devel@ytrizja.de
category:        Dependent types
build-type:      Simple
common warnings
    ghc-options: -W -Wall
library
    import:      warnings
    exposed-modules:
        GardGround.Utils.Fusion
        GardGround.Utils.ListMaybe
    other-extensions:
        ExistentialQuantification
        RankNTypes
    build-depends:
        base         (>= 4.16.0.0 && <4.19)
      , bytestring   ^>= 0.11.0.0
      , deepseq      (>= 1.1 && <1.6)
      , generic-data ^>= 1.1.0.0
      -- , hashable     ^>= 1.4.3.0
      , mtl          ^>= 2.3.1
      , text         (>= 1.2.5.0 && < 2.2)
      -- , text-icu     ^>= 0.8.0.0
      -- , transformers ^>= 0.5.6.0
      , unordered-containers ^>= 0.2.17.0
      , utf8-string  ^>= 1.0.0
    hs-source-dirs:   lib
    default-language: Haskell2010

packages: core/

dist-newstyle