Mercurial > cpdt > repo

comparison src/DataStruct.v @ 205:f05514cc6c0d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
'make doc' works with 8.2
author Adam Chlipala <adamc@hcoop.net>
date Fri, 06 Nov 2009 12:15:05 -0500
parents cbf2f74a5130
children f8bcd33bdd91
comparison
equal deleted inserted replaced
204:cbf2f74a5130 205:f05514cc6c0d
53 match idx with 53 match idx with
54 | First _ => x 54 | First _ => x
55 | Next _ idx' => get ls' idx' 55 | Next _ idx' => get ls' idx'
56 end 56 end
57 end. 57 end.
58
59 ]]
58 60
59 We apply the usual wisdom of delaying arguments in [Fixpoint]s so that they may be included in [return] clauses. This still leaves us with a quandary in each of the [match] cases. First, we need to figure out how to take advantage of the contradiction in the [Nil] case. Every [index] has a type of the form [S n], which cannot unify with the [O] value that we learn for [n] in the [Nil] case. The solution we adopt is another case of [match]-within-[return]. 61 We apply the usual wisdom of delaying arguments in [Fixpoint]s so that they may be included in [return] clauses. This still leaves us with a quandary in each of the [match] cases. First, we need to figure out how to take advantage of the contradiction in the [Nil] case. Every [index] has a type of the form [S n], which cannot unify with the [O] value that we learn for [n] in the [Nil] case. The solution we adopt is another case of [match]-within-[return].
60 62
61 [[ 63 [[
62 Fixpoint get n (ls : ilist n) {struct ls} : index n -> A := 64 Fixpoint get n (ls : ilist n) {struct ls} : index n -> A :=
74 | First _ => x 76 | First _ => x
75 | Next _ idx' => get ls' idx' 77 | Next _ idx' => get ls' idx'
76 end 78 end
77 end. 79 end.
78 80
81 ]]
82
79 Now the first [match] case type-checks, and we see that the problem with the [Cons] case is that the pattern-bound variable [idx'] does not have an apparent type compatible with [ls']. We need to use [match] annotations to make the relationship explicit. Unfortunately, the usual trick of postponing argument binding will not help us here. We need to match on both [ls] and [idx]; one or the other must be matched first. To get around this, we apply a trick that we will call "the convoy pattern," introducing a new function and applying it immediately, to satisfy the type checker. 83 Now the first [match] case type-checks, and we see that the problem with the [Cons] case is that the pattern-bound variable [idx'] does not have an apparent type compatible with [ls']. We need to use [match] annotations to make the relationship explicit. Unfortunately, the usual trick of postponing argument binding will not help us here. We need to match on both [ls] and [idx]; one or the other must be matched first. To get around this, we apply a trick that we will call "the convoy pattern," introducing a new function and applying it immediately, to satisfy the type checker.
80 84
81 [[ 85 [[
82 Fixpoint get n (ls : ilist n) {struct ls} : index n -> A := 86 Fixpoint get n (ls : ilist n) {struct ls} : index n -> A :=
83 match ls in ilist n return index n -> A with 87 match ls in ilist n return index n -> A with
94 | First _ => fun _ => x 98 | First _ => fun _ => x
95 | Next _ idx' => fun ls' => get ls' idx' 99 | Next _ idx' => fun ls' => get ls' idx'
96 end ls' 100 end ls'
97 end. 101 end.
98 102
103 ]]
104
99 There is just one problem left with this implementation. Though we know that the local [ls'] in the [Next] case is equal to the original [ls'], the type-checker is not satisfied that the recursive call to [get] does not introduce non-termination. We solve the problem by convoy-binding the partial application of [get] to [ls'], rather than [ls'] by itself. *) 105 There is just one problem left with this implementation. Though we know that the local [ls'] in the [Next] case is equal to the original [ls'], the type-checker is not satisfied that the recursive call to [get] does not introduce non-termination. We solve the problem by convoy-binding the partial application of [get] to [ls'], rather than [ls'] by itself. *)
100 106
101 Fixpoint get n (ls : ilist n) {struct ls} : index n -> A := 107 Fixpoint get n (ls : ilist n) {struct ls} : index n -> A :=
102 match ls in ilist n return index n -> A with 108 match ls in ilist n return index n -> A with
103 | Nil => fun idx => 109 | Nil => fun idx =>
431 | inl _ => fst mls 437 | inl _ => fst mls
432 | inr idx' => fhget ls' (snd mls) idx' 438 | inr idx' => fhget ls' (snd mls) idx'
433 end 439 end
434 end. 440 end.
435 441
442 ]]
443
436 Only one problem remains. The expression [fst mls] is not known to have the proper type. To demonstrate that it does, we need to use the proof available in the [inl] case of the inner [match]. *) 444 Only one problem remains. The expression [fst mls] is not known to have the proper type. To demonstrate that it does, we need to use the proof available in the [inl] case of the inner [match]. *)
437 445
438 Fixpoint fhget (ls : list A) : fhlist ls -> fmember ls -> B elm := 446 Fixpoint fhget (ls : list A) : fhlist ls -> fmember ls -> B elm :=
439 match ls return fhlist ls -> fmember ls -> B elm with 447 match ls return fhlist ls -> fmember ls -> B elm with
440 | nil => fun _ idx => match idx with end 448 | nil => fun _ idx => match idx with end
539 (** [[ 547 (** [[
540 548
541 Inductive tree : Set := 549 Inductive tree : Set :=
542 | Leaf : A -> tree 550 | Leaf : A -> tree
543 | Node : forall n, filist tree n -> tree. 551 | Node : forall n, filist tree n -> tree.
552
553 ]]
544 554
545 [[ 555 [[
546 556
547 Error: Non strictly positive occurrence of "tree" in 557 Error: Non strictly positive occurrence of "tree" in
548 "forall n : nat, filist tree n -> tree" 558 "forall n : nat, filist tree n -> tree"