-- argument specialization
module test056;

import Stdlib.Prelude open;

{-# specialize: [f] #-}
mymap {A B} (f : A -> B) : List A -> List B
  | nil := nil
  | (x :: xs) := f x :: mymap f xs;

{-# specialize: [2, 5], inline: false #-}
myf
  : {A B : Type}
    -> A
    -> (A -> A -> B)
    -> A
    -> B
    -> Bool
    -> B
  | a0 f a b true := f a0 a
  | a0 f a b false := b;

{-# inline: false #-}
myf'
  : {A B : Type} -> A -> (A -> A -> A -> B) -> A -> B -> B
  | a0 f a b := myf a0 (f a0) a b true;

sum : List Nat -> Nat
  | xs := for (acc := 0) (x in xs) {x + acc};

funa : {A : Type} -> (A -> A) -> A -> A
  | {A} f a :=
    let
      {-# specialize-by: [f] #-}
      go : Nat -> A
        | zero := a
        | (suc n) := f (go n);
    in go 10;

{-# specialize: true #-}
type Additive A := mkAdditive {add : A -> A -> A};

type Multiplicative A :=
  mkMultiplicative {mul : A -> A -> A};

addNat : Additive Nat := mkAdditive (+);

{-# specialize: true #-}
mulNat : Multiplicative Nat := mkMultiplicative (*);

{-# inline: false #-}
fadd {A} (a : Additive A) (x y : A) : A :=
  Additive.add a x y;

{-# inline: false #-}
fmul {A} (m : Multiplicative A) (x y : A) : A :=
  Multiplicative.mul m x y;

main : Nat :=
  sum (mymap λ {x := x + 3} (1 :: 2 :: 3 :: 4 :: nil))
    + sum
      (flatten
        (mymap
          (mymap λ {x := x + 2})
          ((1 :: nil) :: (2 :: 3 :: nil) :: nil)))
    + myf 3 (*) 2 5 true
    + myf 1 (+) 2 0 false
    + myf' 7 (const (+)) 2 0
    + funa ((+) 1) 5
    + fadd addNat 1 2
    + fmul mulNat 1 2;