Mercurial > cpdt > repo

annotate src/DepList.v @ 114:2f97c8177172

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
DepList
author Adam Chlipala <adamc@hcoop.net>
date Tue, 14 Oct 2008 14:49:51 -0400
parents
children 9ccd215e5112
rev   line source
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].