-- Same as `PartialApp`, but for Maybe instead of List.
open import Agda.Builtin.Maybe using (Maybe; nothing; just)

private variable A B C : Set

map : (A → B) → Maybe A → Maybe B
map f nothing  = nothing
map f (just x) = just (f x)

zipWith : (A → B → C) → Maybe A → Maybe B → Maybe C
zipWith f nothing  _        = nothing
zipWith f _        nothing  = nothing
zipWith f (just a) (just b) = just (f a b)

open import Agda.Builtin.Nat using (Nat; _+_)

incr : Maybe Nat → Maybe Nat
incr xs = map (_+ ) xs

incr2 : Maybe Nat → Maybe Nat
incr2 = map (_+ )

sum : Maybe Nat → Nat
sum nothing  = 
sum (just x) = x

pattern [_] x = just x

testPartialAdd : Nat
testPartialAdd = sum (map (_+ ) [  ])

testIncr : Nat
testIncr = sum (incr [  ])

testIncr2 : Nat
testIncr2 = sum (incr2 [  ])

testPartialAdd2 : Nat
testPartialAdd2 = sum (zipWith _+_ [  ] [  ])

constNat : Nat → Nat → Nat
constNat x _ = x

testConstNat : Nat
testConstNat = sum (map (constNat ) [  ])

sumWith : (Nat → Nat) → Maybe Nat → Nat
sumWith f xs = sum (map f xs)

testSumWith : Nat
testSumWith = sumWith (_+ ) [  ]

sumWithConst : (Nat → Nat → Nat) → Maybe Nat → Nat
sumWithConst f xs = sum (map (f ) xs)

testSumWithConst : Nat
testSumWithConst = sumWithConst constNat [  ]

record SomeNat : Set where
  constructor `_
  field someNat : Nat

addSomeNat : SomeNat → (Nat → Nat)
addSomeNat (` n) = n +_

testSomeNat : Nat
testSomeNat = addSomeNat (` ) 

open import Agda.Builtin.Nat

test : Nat
test
  = constNat  
  + testPartialAdd
  + testIncr
  + testIncr2
  + testPartialAdd2
  + testConstNat
  + testSumWith
  + testSumWithConst
  + testSomeNat
{-# COMPILE AGDA2LAMBOX test #-}