blob: 21a684bd7e7ecbe6677ad49766af4be3b128e3f8 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
|
module Data.Fun.Nary
import Data.Vect
%default total
public export
data Visibility = Visible | Hidden | Auto
public export
Pi : Visibility -> (a : Type) -> (a -> Type) -> Type
Pi Visible a b = (x : a) -> b x
Pi Hidden a b = {x : a} -> b x
Pi Auto a b = {auto x : a} -> b x
public export
lam : (vis : Visibility) -> (0 b : a -> Type) ->
((x : a) -> b x) -> Pi vis a b
lam Visible b f = f
lam Hidden b f = f _
lam Auto b f = f %search
public export
app : (vis : Visibility) -> (0 b : a -> Type) ->
Pi vis a b -> ((x : a) -> b x)
app Visible b f x = f x
app Hidden b f x = f
app Auto b f x = f
public export
PI : (n : Nat) -> Visibility -> (a : Type) -> (Vect n a -> Type) -> Type
PI Z vis a b = b []
PI (S n) vis a b = Pi vis a (\ x => PI n vis a (b . (x ::)))
public export
curry : (n : Nat) -> (vis : Visibility) ->
(0 b : Vect n a -> Type) ->
((as : Vect n a) -> b as) ->
PI n vis a b
curry 0 vis b f = f []
curry (S n) vis b f
= lam vis _ $ \ x => curry n vis (b . (x ::)) (\ xs => f (x :: xs))
public export
uncurry : (n : Nat) -> (vis : Visibility) ->
(0 b : Vect n a -> Type) ->
PI n vis a b ->
(as : Vect n a) -> b as
uncurry 0 vis b f [] = f
uncurry (S n) vis b f (x :: xs)
= uncurry n vis (b . (x ::)) (app vis _ f x) xs
|
