blob: 390745ab4e3005918887a9be9af917cfca6de0a1 (
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
52
53
54
55
|
module Inky.Data.Fun
import public Flap.Data.SnocList.Quantifiers
import Flap.Data.SnocList
public export
Fun : SnocList Type -> Type -> Type
Fun [<] b = b
Fun (as :< a) b = Fun as (a -> b)
public export
chain : (len : LengthOf as) -> (b -> c) -> Fun as b -> Fun as c
chain Z f x = f x
chain (S len) f g = chain len (f .) g
public export
DFun : (as : SnocList Type) -> Fun as Type -> Type
DFun [<] p = p
DFun (as :< a) p = DFun as (chain (lengthOf as) (\f => (x : a) -> f x) p)
public export
DIFun : (as : SnocList Type) -> Fun as Type -> Type
DIFun [<] p = p
DIFun (as :< a) p = DIFun as (chain (lengthOf as) (\f => {x : a} -> f x) p)
public export
curry : (len : LengthOf as) -> (HSnocList as -> b) -> Fun as b
curry Z f = f [<]
curry (S len) f = curry len (f .: (:<))
public export
uncurry : Fun as b -> HSnocList as -> b
uncurry f [<] = f
uncurry f (sx :< x) = uncurry f sx x
export
uncurryChain :
(0 g : b -> c) -> (0 f : Fun as b) -> (xs : HSnocList as) ->
uncurry (chain (lengthOf as) g f) xs = g (uncurry f xs)
uncurryChain g f [<] = Refl
uncurryChain g f (sx :< x) = cong (\f => f x) (uncurryChain (g .) f sx)
export
dcurry : (len : LengthOf as) -> ((xs : HSnocList as) -> uncurry p xs) -> DFun as p
dcurry Z f = f [<]
dcurry (S len) f =
dcurry len (\sx =>
replace {p = id} (sym $ uncurryChain (\f => (x : _) -> f x) p sx)
(\x => f (sx :< x)))
export
duncurry : DFun as p -> (sx : HSnocList as) -> uncurry p sx
duncurry f [<] = f
duncurry f (sx :< x) =
replace {p = id} (uncurryChain (\f => (x : _) -> f x) p sx) (duncurry f sx) x
|
