open import Agda.Builtin.List using (List; []; _∷_)
{-# FOREIGN AGDA2RUST
#[path = "Agda/Builtin/List.rs"] mod ListMod;
use self::ListMod::List;
#-}

private variable A B C : Set

map : (A → B) → List A → List B
map f [] = []
map f (x ∷ xs) = f x ∷ map f xs

zipWith : (A → B → C) → List A → List B → List C
zipWith f []       _        = []
zipWith f _        []       = []
zipWith f (a ∷ as) (b ∷ bs) = f a b ∷ zipWith f as bs

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

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

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

sum : List Nat → Nat
sum [] = 
sum (x ∷ xs) = x + sum xs

pattern [_] x = x ∷ []
pattern [_⨾_] x y = x ∷ [ y ]

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) → List Nat → Nat
sumWith f xs = sum (map f xs)

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

sumWithConst : (Nat → Nat → Nat) → List 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(),
  );
}
#-}