open import Agda.Builtin.Nat using (Nat; _+_; _*_)
open import Agda.Builtin.Bool using (Bool; true; false)

-- ** top-level

add : Nat → Nat → Nat
add = _+_
-- add = λ x y → x + y
-- add(x,y) = x + y

add2l : Nat → Nat
add2l =  +_
-- add2l = λ x → 2 + x
-- add2l(x) = 2 + x

add2r : Nat → Nat
add2r = _+ 
-- add2r = λ x → x + 2
-- add2r(x) = x + 2

add3 : Nat → Nat → Nat → Nat
add3 x y = (x + y) +_
-- add3 = λ x y z → (x + y) + z
-- add3(x,y,z) = (x + y) + z

-- ** inner-level

maybeAddL : Bool → Nat → Nat
maybeAddL true  =  +_
maybeAddL false =  +_
-- maybeAddL = λ b → case b of
--   true  → λ x → 40 + x
--   false → λ x → 10 + x
-- maybeAddL = λ b x → case b of
--   true  → 40 + x
--   false → 10 + x
-- maybeAddL(b,x) = if b then 40 + x else 10 + x

maybeAddLb : Bool → Nat → Nat
maybeAddLb true  = λ x →  + x
maybeAddLb false = λ x →  + x
-- maybeAddLb(b,x) = if b then 40 + x else 10 + x

maybeAddR : Bool → Nat → Nat
maybeAddR true  = _+ 
maybeAddR false = _+ 
-- maybeAddR(b,x) = if b then x + 40 else x + 10

maybeAddRb : Bool → Nat → Nat
maybeAddRb true  = λ x → x + 
maybeAddRb false = λ x → x + 
-- maybeAddRb(b,x) = if b then x + 40 else x + 10

maybeAdd : Bool → Nat → Nat → Nat
maybeAdd true  = _+_
maybeAdd false = _*_

maybeAdd3 : Bool → Nat → Nat → Nat
maybeAdd3 true  x = _+ ( + x)
maybeAdd3 false x = _+ ( + x)
-- maybeAdd3(b,x) = λ y → if b then y + (40 + x) else y + (10 + x)
-- maybeAdd3(b,x,y) = if b then y + (40 + x) else y + (10 + x)

maybeAdd3b : Bool → Nat → Nat → Nat
maybeAdd3b true  x y = y + ( + x)
maybeAdd3b false x y = y + ( + x)
-- maybeAdd3b(b,x,y) = if b then y + (40 + x) else y + (10 + x)

data Maybe (A : Set) : Set where
  nothing : Maybe A
  just : A → Maybe A

maybeInc : Maybe Nat → Nat → Nat
maybeInc (just y) x = x + y
maybeInc nothing  x = x
-- maybeInc(m,x) = match m { Just y -> x + y, Nothing -> x }

maybeAddM : Maybe Nat → Nat → Nat → Nat
maybeAddM (just z) x y = x + y + z
maybeAddM nothing  x y = x + y
-- maybeAddM(m,x,y) = match m { Just z -> x + y + z, Nothing -> x + y }

maybeIncInc : Maybe (Maybe Nat) → Nat → Nat
maybeIncInc (just (just y)) x = x + y
maybeIncInc (just nothing)  x = x + 
maybeIncInc nothing         x = x
-- maybeIncInc(mm,x) = match m
--   { Just m -> match m
--     { Just y -> x + y
--     , Nothing -> x + 1 }
--   , Nothing -> x }

maybeIncInc2 : Maybe (Maybe Nat) → Nat → Nat → Nat
maybeIncInc2 (just (just z)) x y = x + y + z
maybeIncInc2 (just nothing)  x y = x + y + 
maybeIncInc2 nothing         x y = x + y
-- maybeIncInc2(mm,x,y) = match m
--   { Just m -> match m
--     { Just z -> x + y + z
--     , Nothing -> x + y + 1 }
--   , Nothing -> x + y }

-- ** non-app-free heads

{-
id : ∀ {A : Set} → A → A
id = λ x → x
-- id(x) = x

addId : Nat → Nat → Nat
addId = id _+_
-- addId = λ x y → id _+_ x y
-- ** cannot infer the arity of treeless terms..
-- addId(x,y) = id _+_ x y

addId2l : Nat → Nat
addId2l = id (2 +_)
-- addId2l = λ x → id (λ y → 2 + y) x
-- addId2l(x) = id (λ y → 2 + y) x

addId2r : Nat → Nat
addId2r = id (_+ 2)
-- addId2r = λ x → id (λ y → y + 2) x
-- addId2r(x) = id (λ y → y + 2) x

addId3 : Nat → Nat → Nat → Nat
addId3 x y = id ((x + y) +_)
-- addId3 = λ x y z → id (λ z → (x + y) + z) z
-- addId3(x,y,z) = id (λ z → (x + y) + z) z
-}

open import Agda.Builtin.Nat

test : Nat
test
  = add  
  + add2l 
  + add2r 
  + add3   

  + maybeAddL true 
  + maybeAddLb true 
  + maybeAddR true 
  + maybeAddRb true 
  + maybeAdd true  
  + maybeAdd false  
  + maybeAdd3 true  
  + maybeAdd3b true  

  + maybeInc (just ) 
  + maybeAddM (just )  
  + maybeIncInc (just (just )) 
  + maybeIncInc2 (just (just ))  
{-# COMPILE AGDA2LAMBOX test #-}