|
adamc@114
|
1 (* Copyright (c) 2008, Adam Chlipala
|
|
adamc@114
|
2 *
|
|
adamc@114
|
3 * This work is licensed under a
|
|
adamc@114
|
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
|
|
adamc@114
|
5 * Unported License.
|
|
adamc@114
|
6 * The license text is available at:
|
|
adamc@114
|
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
|
|
adamc@114
|
8 *)
|
|
adamc@114
|
9
|
|
adamc@114
|
10 (* Dependent list types presented in Chapter 8 *)
|
|
adamc@114
|
11
|
|
adamc@114
|
12 Require Import List.
|
|
adamc@114
|
13
|
|
adamc@114
|
14 Set Implicit Arguments.
|
|
adamc@114
|
15
|
|
adamc@114
|
16
|
|
adamc@114
|
17 Section ilist.
|
|
adamc@114
|
18 Variable A : Set.
|
|
adamc@114
|
19
|
|
adamc@114
|
20 Fixpoint ilist (n : nat) : Set :=
|
|
adamc@114
|
21 match n with
|
|
adamc@114
|
22 | O => unit
|
|
adamc@114
|
23 | S n' => A * ilist n'
|
|
adamc@114
|
24 end%type.
|
|
adamc@114
|
25
|
|
adamc@114
|
26 Fixpoint index (n : nat) : Set :=
|
|
adamc@114
|
27 match n with
|
|
adamc@114
|
28 | O => Empty_set
|
|
adamc@114
|
29 | S n' => option (index n')
|
|
adamc@114
|
30 end.
|
|
adamc@114
|
31
|
|
adamc@114
|
32 Fixpoint get (n : nat) : ilist n -> index n -> A :=
|
|
adamc@114
|
33 match n return ilist n -> index n -> A with
|
|
adamc@114
|
34 | O => fun _ idx => match idx with end
|
|
adamc@114
|
35 | S n' => fun ls idx =>
|
|
adamc@114
|
36 match idx with
|
|
adamc@114
|
37 | None => fst ls
|
|
adamc@114
|
38 | Some idx' => get n' (snd ls) idx'
|
|
adamc@114
|
39 end
|
|
adamc@114
|
40 end.
|
|
adamc@114
|
41 End ilist.
|
|
adamc@114
|
42
|
|
adamc@114
|
43 Implicit Arguments get [A n].
|
|
adamc@114
|
44
|
|
adamc@114
|
45 Section hlist.
|
|
adamc@114
|
46 Variable A : Type.
|
|
adamc@114
|
47 Variable B : A -> Type.
|
|
adamc@114
|
48
|
|
adamc@114
|
49 Fixpoint hlist (ls : list A) : Type :=
|
|
adamc@114
|
50 match ls with
|
|
adamc@114
|
51 | nil => unit
|
|
adamc@114
|
52 | x :: ls' => B x * hlist ls'
|
|
adamc@114
|
53 end%type.
|
|
adamc@114
|
54
|
|
adamc@114
|
55 Variable elm : A.
|
|
adamc@114
|
56
|
|
adamc@114
|
57 Fixpoint member (ls : list A) : Type :=
|
|
adamc@114
|
58 match ls with
|
|
adamc@114
|
59 | nil => Empty_set
|
|
adamc@114
|
60 | x :: ls' => (x = elm) + member ls'
|
|
adamc@114
|
61 end%type.
|
|
adamc@114
|
62
|
|
adamc@114
|
63 Fixpoint hget (ls : list A) : hlist ls -> member ls -> B elm :=
|
|
adamc@114
|
64 match ls return hlist ls -> member ls -> B elm with
|
|
adamc@114
|
65 | nil => fun _ idx => match idx with end
|
|
adamc@114
|
66 | _ :: ls' => fun mls idx =>
|
|
adamc@114
|
67 match idx with
|
|
adamc@114
|
68 | inl pf => match pf with
|
|
adamc@114
|
69 | refl_equal => fst mls
|
|
adamc@114
|
70 end
|
|
adamc@114
|
71 | inr idx' => hget ls' (snd mls) idx'
|
|
adamc@114
|
72 end
|
|
adamc@114
|
73 end.
|
|
adamc@114
|
74 End hlist.
|
|
adamc@114
|
75
|
|
adamc@114
|
76 Implicit Arguments hget [A B elm ls].
|
