module demo.AgdaDemoSERENE where


data color : Set where
 Red : color
 Green : color
 Blue : color




swapColor : color → color
swapColor Red = Green
swapColor Green = Red


swapColor Blue = Red




data ℕ : Set where
 zero : ℕ
 succ : ℕ → ℕ



_+_ : ℕ → ℕ → ℕ
zero    +  m  =  m
succ n  +  m  =  succ (n + m)



double : ℕ → ℕ
double zero = zero
double (succ n) = succ (double n)



fib : ℕ → ℕ
fib zero = zero
fib (succ zero) = succ zero
fib (succ (succ n)) = fib n + fib (succ n)



open import Coinduction using (♯_ ; ♭ ; ∞)
open import Size renaming  (∞ to ∞')


data stream : Set where
 _::_ : ℕ → ∞ stream → stream



stream₀ : stream
stream₀ = zero :: (♯ stream₀)



inc : ℕ → stream
inc n = n :: (♯ inc (succ n))



addStream : stream → stream → stream
addStream (x :: x₁) (y :: y₁) = (x + y) :: (♯ addStream (♭ x₁) (♭ y₁))



mutual
 record ∞Delay (i : Size) (A : Set) : Set where
   coinductive
   field
    force : {j : Size< i} → Delay j A

 data Delay (i : Size) (A : Set) : Set  where
    now : A → Delay i A
    later : ∞Delay i A → Delay i A







data Bool : Set where
 true : Bool
 false : Bool





_or_ : Bool → Bool → Bool
false  or  m   =  m
true   or  m   =  true



postulate _and_ : Bool → Bool → Bool
postulate if_then_else_ : Bool → Bool → Bool → Bool



infixl    _or_
infixl    _and_
infixl    if_then_else_



data 𝔹 : Set where
 true   :  𝔹
 false  :  𝔹



_∨_ : 𝔹 → 𝔹 → 𝔹
true   ∨  true   =  true
true   ∨  false  =  true
false  ∨  true   =  true
false  ∨  false  =  false



id : {A : Set} → A → A
id x = x



id₁ : (A : Set) → A → A
id₁ A x = x




True : Bool
True = id true


Zero : ℕ
Zero = id zero




Zero₁ : ℕ
Zero₁ = id₁ ℕ zero


true₁ : Bool
true₁ = id₁ Bool true


-- \maine

data Fin : ℕ → Set where
  zero :  {n : ℕ}  →  Fin (succ n)
  suc  :  {n : ℕ}  →  Fin n → Fin (succ n)


--  constructor pair

record AB : Set where 
  field
    a : ℕ
    b : Fin a

open AB

postulate x : ℕ
postulate y : Fin x


n2 : AB


n2 = record{a = x; b = y}



n3 : AB

a  n3  =  x
b  n3  =  y






postulate A  : Set
postulate a' : A
postulate _==_  :  A → A → Set
postulate _>'_  :  A → A → Set



data List (A : Set) : Set where
 [] : List A
 _::_ : A → List A → List A




revList : (A : Set) → List A → List A
revList A list = refAux list []
       where
        refAux :  List A → List A  → List A
        refAux  []         xy  =  xy
        refAux  (x :: xs)  xy  =  refAux xs (x :: xy)




mutual
 data  Even : Set where
  zero : Even
  suc : Odd → Even

 data Odd : Set where
  suc : Even → Odd




data  Even' : Set
data  Odd'  : Set

data  Even' where
  zero : Even'
  suc  : Odd' → Even'

data  Odd' where
  suc : Even' → Odd'



_<_ : ℕ → ℕ → Bool
_ < zero = false
zero < succ m = true
succ n < succ m = n < m




Minℕ : ℕ → ℕ → ℕ
Minℕ x y with (x < y)
Minℕ x y | true = x
Minℕ x y | false = y






--open import Data.Nat

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

--{-# BUILTIN NATURAL Nat #-}

--{-# BUILTIN NATURAL ℕ #-}

{-
aa₁ : ℕ
aa₁ = 0
-}


{-
{-# BUILTIN LIST List  #-}
{-# BUILTIN NIL  []    #-}
{-# BUILTIN CONS  _::_ #-}
-}





data List₀ (A : Set) : Set where
 [] : List₀ A
 _::_ : A → List₀ A → List₀ A


--{-# COMPILED_DATA List List [] (::) #-}


{-# FOREIGN GHC type AgdaList a = [a] #-}
{-# COMPILE GHC List = data AgdaList ([] | (:)) #-}




postulate IO : Set → Set

--{-#  COMPILED_TYPE IO IO #-}
-- {-# FOREIGN GHC type AgdaIO a = IO a #-}
-- {-# COMPILE GHC IO = type AgdaIO #-}

{-# COMPILE GHC IO = type IO #-}



data Unit : Set where
 unit : Unit


--{-#  COMPILED_DATA Unit () () #-}


{-# COMPILE GHC Unit = data () (()) #-}



postulate String : Set
-- {-# BUILTIN STRING String #-}

postulate putStrLn : String → IO Unit
{-# COMPILE GHC putStrLn = (\ s -> putStrLn (Data.Text.unpack s)) #-}

-- {-# COMPILED putStrLn (\ _ s -> Data.Text.IO.putStrLn s) #-}

--{-# COMPILED_TYPE String String #-}

--{-# COMPILED putStrLn putStrLn #-}



data ⊥ : Set where



data ⊤ : Set where
 triv : ⊤



mutual
 data U : Set where
   ⊥'     :  U
   ⊤'     :  U
   Bool'  :  U
   Π'     :  (a : U)(b : T₀ a → U) → U

 T₀  : U → Set
 T₀  ⊥'        =  ⊥
 T₀  ⊤'        =  ⊤
 T₀  Bool'     =  Bool
 T₀  (Π' a b)  =  (x : T₀ a) → T₀ (b x)








record Stream (i : Size) : Set where
  coinductive
  field
    head  :  ℕ
    tail  :  {j : Size< i} → Stream j






open Stream




cons : ∀ {i} → ℕ →  Stream i → Stream (↑ i)
head  (cons n s)  =  n
tail  (cons n s)  =  s










_+s_ : ∀ {i} → Stream i → Stream i → Stream i
head  (s  +s  s')  =  head  s  +   head  s'
tail  (s  +s  s')  =  tail  s  +s  tail  s'





T : Bool → Set
T true =  ⊤
T false =  ⊥



infix  _≡_

-- \maine

data _≡_ {a} {A : Set a} (x : A) : A → Set a where
  instance refl : x ≡ x




+0' : ∀ n → n + zero ≡ n
+0' zero = refl
+0' (succ n) with n + zero | +0' n
+0' (succ n) | .n | refl = refl