{-# OPTIONS --type-in-type --no-termination-check #-}
module ssgip.main where
open import Data.Unit
open import Data.Sum hiding (map)
open import Data.Nat
open import Data.List hiding (map; zipWith; replicate)
open import Data.Product hiding (map)
open import Relation.Binary.PropositionalEquality
infixl 50 _⊛_
infixl 50 _<>_
data Bool : Set where
true : Bool
false : Bool
_∧_ : Bool → Bool → Bool
true ∧ true = true
_ ∧ _ = false
if_then_else : ∀ { A } → Bool → A → A → A
if true then e1 else e2 = e1
if false then e1 else e2 = e2
replicate : ∀ {A} → ℕ → A → List A
replicate zero x = []
replicate (suc n) x = (x ∷ replicate n x)
replicate-spec : ∀ {A} → (x : A) → (n : ℕ)
→ length (replicate n x) ≡ n
replicate-spec x zero = refl
replicate-spec x (suc n) with replicate-spec x n
... | pf = cong suc pf
data Vec (A : Set) : ℕ → Set where
[] : Vec A zero
_∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)
repeat : ∀ {A} → (n : ℕ) → A → Vec A n
repeat zero x = []
repeat (suc n) x = x ∷ repeat n x
postulate error : ∀ {A} → A
_<>_ : ∀ {A B} → List (A → B) → List A → List B
[] <> [] = []
(a ∷ As) <> (b ∷ Bs) = (a b ∷ As <> Bs)
_ <> _ = error
_⊛_ : ∀ {A B n} → Vec (A → B) n → Vec A n → Vec B n
[] ⊛ [] = []
(a ∷ As) ⊛ (b ∷ Bs) = (a b ∷ As ⊛ Bs)
zerox : (Bool → Bool) → Bool → Bool
zerox f x = x
onex : (Bool → Bool) → Bool → Bool
onex f x = f x
twox : (Bool → Bool) → Bool → Bool
twox f x = f (f x)
nx : ℕ → (Bool → Bool) → Bool → Bool
nx zero f x = x
nx (suc n) f x = nx n f (f x)
app-nat : (ℕ → ℕ) → ℕ → ℕ
app-nat f x = f x
app-bool : (Bool → Bool) → Bool → Bool
app-bool f x = f x
app : ∀ {A} → (A → A) → A → A
app f x = f x
eq-nat : ℕ → ℕ → Bool
eq-nat zero zero = true
eq-nat (suc n) (suc m) = eq-nat n m
eq-nat _ _ = false
eq-bool : Bool → Bool → Bool
eq-bool false false = true
eq-bool true true = true
eq-bool _ _ = false
⟦_⟧ : Bool → Set
⟦ b ⟧ = if b then ℕ else Bool
eq-nat-bool : (b : Bool) → ⟦ b ⟧ → ⟦ b ⟧ → Bool
eq-nat-bool true = eq-nat
eq-nat-bool false = eq-bool
data Type : Set where
nat : Type
bool : Type
pair : Type → Type → Type
zeroApp : ∀ {A B} → B → A → B
zeroApp f x = f
oneApp : ∀ {A B} → (A → B) → A → B
oneApp f x = f x
twoApp : ∀ {A B} → (A → A → B) → A → B
twoApp f x = f x x
NAPP : ℕ → Set → Set → Set
NAPP zero A B = B
NAPP (suc n) A B = A → NAPP n A B
nApp : ∀ {A B} → (n : ℕ) → NAPP n A B → A → B
nApp zero f x = f
nApp (suc n) f x = nApp n (f x) x
f : (b : Bool) → if b then ℕ else Bool
f true = 0
f false = false
anything : ∀ {A} → A
anything = anything
head : ∀ {A n} → Vec A (suc n) → A
head ( x ∷ xs ) = x