0 | ||| N-ary simple (non-dependent) functions using telescopes
 1 | |||
 2 | ||| Compare with `base/Data.Fun` and `contrib/Data.Fun.Extra` and with:
 3 | ||| Guillaume Allais. 2019. Generic level polymorphic n-ary functions. TyDe 2019.
 4 | module Data.Telescope.SimpleFun
 5 |
 6 | import Data.Telescope.Telescope
 7 | import Data.Telescope.Segment
 8 |
 9 | ||| An n-ary function whose codomain does not depend on its
10 | ||| arguments. The arguments may have dependencies.
11 | public export
12 | 0 SimpleFun : (env : Left.Environment gamma) -> {n : Nat} -> (0 delta : Segment n gamma)
13 |            -> (cod : Type) -> Type
14 | SimpleFun env {n = 0  } [] cod = cod
15 | SimpleFun env {n = S n} (ty :: delta) cod = (x : ty env) -> SimpleFun (env ** x) delta cod
16 |
17 | public export
18 | target : {0 env : Left.Environment gamma} -> {0 delta : Segment n gamma} -> {cod : Type}
19 |       -> SimpleFun env delta cod -> Type
20 | target {cod} _ = cod
21 |
22 | public export
23 | uncurry : {n : Nat} -> {0 env : Left.Environment gamma} -> {0 delta : Segment n gamma}
24 |        -> (f : SimpleFun env delta cod) -> Environment env delta -> cod
25 | uncurry {n = Z}   {delta = []}     f xs        = f
26 | uncurry {n = S n} {delta = _ :: _} f (x .= xs) = uncurry (f x) xs
27 |
28 | public export
29 | curry : {n : Nat} -> {0 env : Left.Environment gamma} -> {0 delta : Segment n gamma}
30 |      -> (f : Environment env delta -> cod)
31 |      -> SimpleFun env delta cod
32 | curry {n = 0  } {delta = []         } f = f Empty
33 | curry {n = S n} {delta = ty :: delta} f = \x => curry (\xs => f (x .= xs))
34 |