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
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
|
Require Import Coq.Lists.List.
Require Import ExtLib.Data.Member.
Fixpoint asFunc (domain : list Type) (range : Type) : Type :=
match domain with
| nil => range
| d :: ds => d -> asFunc ds range
end.
Fixpoint asPi (ps : list Type) {struct ps} :
((forall U, asFunc ps U -> U) -> Type) -> Type :=
match ps as ps return ((forall U, asFunc ps U -> U) -> Type) -> Type with
| nil => fun f => f (fun _ x => x)
| p :: ps => fun f => forall x : p, asPi ps (fun App => f (fun _ f' => App _ (f' x)))
end.
Fixpoint asTuple (domain : list Type) : Type :=
match domain with
| nil => unit
| d :: ds => prod d (asTuple ds)
end.
Fixpoint applyF {domain : list Type} {range : Type}
: asFunc domain range -> asTuple domain -> range :=
match domain as domain
return asFunc domain range -> asTuple domain -> range
with
| nil => fun x _ => x
| d :: ds => fun f x_xs => applyF (f (fst x_xs)) (snd x_xs)
end.
Fixpoint const {D R} (r : R) : asFunc D R :=
match D with
| nil => r
| _ :: D => fun _ => const r
end.
Fixpoint uncurry {D R} {struct D} : (asTuple D -> R) -> asFunc D R :=
match D as D return (asTuple D -> R) -> asFunc D R with
| nil => fun x => x tt
| d :: D => fun f d => uncurry (fun x => f (d, x))
end.
Fixpoint curry {D R} {struct D} : asFunc D R -> (asTuple D -> R) :=
match D as D return asFunc D R -> (asTuple D -> R) with
| nil => fun x _ => x
| d :: D => fun f x => curry (f (fst x)) (snd x)
end.
Fixpoint get (domain : list Type) (range : Type) T (m : member T domain)
: (T -> asFunc domain range) -> asFunc domain range :=
match m in member _ domain
return (T -> asFunc domain range) -> asFunc domain range
with
| MZ _ _ => fun F x => F x x
| MN _ m => fun F x => @get _ _ _ m (fun y => F y x)
end.
Fixpoint under (domain : list Type) (range : Type)
{struct domain}
: ((forall U, asFunc domain U -> U) -> range)
-> asFunc domain range :=
match domain as domain
return ((forall U, asFunc domain U -> U) -> range)
-> asFunc domain range
with
| nil => fun F => F (fun _ x => x)
| d :: ds => fun F x =>
under ds range (fun App => F (fun U f => App U (f x)))
end%type.
Fixpoint replace {ps} {T U : Type} (m : member T ps) (v : T) {struct m}
: asFunc ps U -> asFunc ps U :=
match m in member _ ps return asFunc ps U -> asFunc ps U with
| MZ _ _ => fun f _ => f v
| MN _ m => fun f x => replace m v (f x)
end.
Section combine.
Context {T U V : Type}.
Variable (join : T -> U -> V).
Definition combine (domain : list Type)
(a : asFunc domain T) (b : asFunc domain U)
: asFunc domain V :=
under domain _ (fun App => join (App _ a) (App _ b)).
End combine.
|
