add simple stuff (e.g. haskell basics)

fogti
Aug 21, 2024, 10:30 AM
6XMVEBZAMRKHRYLFMJ6ZNSBM5ZXPTPK4YS4QUNGGPPUS4HLPO6GAC

Dependencies

Change contents

  • file addition: examples (d--r------)
    [4.1]
  • file addition: farkous (d--r------)
    [0.20]
  • file addition: 00.fks (----------)
    [0.41]
    (* 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 → {
    })
  • file addition: core (d--r------)
    [4.1]
  • file addition: lib (d--r------)
    [0.709]
  • file addition: GardGround (d--r------)
    [0.726]
  • file addition: Utils (d--r------)
    [0.750]
  • file addition: ListMaybe.hs (----------)
    [0.769]
    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 #-}
  • file addition: Fusion.hs (----------)
    [0.769]
    {-# 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)
  • file addition: gardground-core.cabal (----------)
    [0.709]
    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
  • file addition: cabal.project (----------)
    [4.1]
    packages: core/
  • edit in .ignore at line 4
    [2.103]
    [2.103]
    dist-newstyle