zelinskiy

data MailBox = MailBox {
  nmessages :: Int,
  size :: Int,
  maxsize :: Int,
  fmsg :: Message }
  deriving (Eq, Show, Read)

data Message = Message {
  msize :: Int,

zelinskiy

module Category where

open import Relation.Binary.Core using (_≡_)

record Category : Set1 where
  field
    Objects : Set
    Hom : (A B : Objects) → Set
    _∘_ : ∀ {A B C} → Hom B C → Hom A B → Hom A C
    ∘-assoc : ∀ {A B C D} → {f : Hom A B} → {g : Hom B C} → {h : Hom C D} →

zelinskiy

data R {A B : Set} (a : A) (b : B) : Set where

--Axiom of Choice!
ac : {A B : Set} →
  ((a : A) → Σ B (λ b → R a b )) →
  Σ (A → B) (λ f → ((a : A) → R a (f a)))
ac g = (λ a → π₁ (g a)) , (λ a → π₂ (g a))

zelinskiy

type Checkpointed a = (a -> Cont a a) -> Cont a a

checkpointed :: (a -> Bool) -> Checkpointed a -> Cont r a
checkpointed p  cp =
  pure $ evalCont $ cp $ \a ->
     cont $ \c ->
       if p $ c a then c a else a

addTens :: Int -> Checkpointed Int
addTens x1 checkpoint = do

zelinskiy

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE TypeOperators #-}

import Data.Char
import Control.Monad
import Data.Array.IArray
import Data.Array.MArray
import Data.Array.ST
import Data.List
import Data.Maybe

zelinskiy

import Data.List

inf = 1000000

mindist d x [] = inf
mindist d x (y:ys) | x == y = d
mindist d x (y:ys) = mindist (d+1) x ys

change _ _ [] = error "Empty List"
change x y (p : ps)

zelinskiy

import Data.List

-- https://en.wikipedia.org/wiki/Banker%27s_algorithm
-- https://uk.wikipedia.org/wiki/%D0%90%D0%BB%D0%B3%D0%BE%D1%80%D0%B8%D1%82%D0%BC_%D0%B1%D0%B0%D0%BD%D0%BA%D1%96%D1%80%D0%B0#cite_note-3

data Resource = Resource { nameR :: String, totalR :: Int } deriving (Eq, Show)
data ProcessResourceInfo = ProcessResourceInfo { resourceP :: Resource, usedP :: Int, maxresP :: Int } deriving (Eq, Show)
type Process = [ProcessResourceInfo] 

rA = Resource "A" 6

zelinskiy

{- A straightforward version of Church’s simple type theory is the following system T -}
module T where

open import Data.Nat

-- The type of contexts.
data Γ (X : Set) : Set where
  ε : Γ X
  _::_ : (γ : Γ X) → X → Γ X
infixl 4 _::_

zelinskiy

data ℕ : Set where
  Z : ℕ
  S : ℕ → ℕ

{-# BUILTIN NATURAL  ℕ  #-}

infix 4 _≅_

data _≅_ {ℓ} {A : Set ℓ} (x : A) : {B : Set ℓ} → B → Set ℓ where
   refl : x ≅ x

zelinskiy

{-# OPTIONS --copatterns #-}

module UntypedLambda where

open import Size
open import Function

mutual

  data Delay (A : Set) (i : Size) : Set where