-- Same as `PartialApp`, but for Maybe instead of List.
open import Agda.Builtin.Maybe using (Maybe; nothing; just)
{-# FOREIGN AGDA2RUST
#[path = "Agda/Builtin/Maybe.rs"] mod MaybeMod;
use self::MaybeMod::Maybe;
#-}

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 (` ) 

{-# FOREIGN AGDA2RUST
pub fn main() {
  println!("{}:\t\t {} | {} | {} | {} | {} | {} | {} | {} | {}", module_path!(),
    constNat(42, 41),
    testPartialAdd(),
    testIncr(),
    testIncr2(),
    testPartialAdd2(),
    testConstNat(),
    testSumWith(),
    testSumWithConst(),
    testSomeNat(),
  );
}
#-}