0 | ||| N-ary dependent functions using telescopes
 1 | |||
 2 | ||| Compare with `base/Data.Fun` and:
 3 | ||| Guillaume Allais. 2019. Generic level polymorphic n-ary functions. TyDe 2019.
 4 | module Data.Telescope.Fun
 5 |
 6 | import Data.Telescope.Telescope
 7 | import Data.Telescope.Segment
 8 | import Data.Telescope.SimpleFun
 9 |
10 | public export
11 | 0 Fun : (env : Left.Environment gamma) -> {n : Nat} -> (0 delta : Segment n gamma)
12 |      -> (cod : SimpleFun env delta Type)
13 |      -> Type
14 | Fun env {n = 0  } []            cod = cod
15 | Fun env {n = S n} (ty :: delta) cod = (x : ty env) -> Fun (env ** x) delta (cod x)
16 |
17 | public export
18 | uncurry : {0 n : Nat} -> {0 env : Left.Environment gamma} -> {0 delta : Segment n gamma}
19 |        -> {0 cod : SimpleFun env delta Type}
20 |        -> (f : Fun env delta cod) -> (ext : Environment env delta)
21 |        -> uncurry cod ext
22 | uncurry f Empty     = f
23 | uncurry f (x .= xs) = Fun.uncurry (f x) xs
24 |
25 | public export
26 | curry : {n : Nat} -> {0 env : Left.Environment gamma} -> {0 delta : Segment n gamma}
27 |      -> {0 cod : SimpleFun env delta Type}
28 |      -> ((ext : Environment env delta) -> SimpleFun.uncurry cod ext)
29 |      -> Fun env delta cod
30 | curry {n = 0  } {delta = []         } f = f Empty
31 | curry {n = S n} {delta = ty :: delta} f = \x => Fun.curry (\xs => f (x .= xs))
32 |