Mercurial > cpdt > repo

comparison src/Generic.v @ 193:8e9499e27b6c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Start of Generic
author Adam Chlipala <adamc@hcoop.net>
date Fri, 28 Nov 2008 09:55:56 -0500
parents
children 063b5741c248
comparison
equal deleted inserted replaced
192:32ce9b28d7e7 193:8e9499e27b6c
1 (* Copyright (c) 2008, Adam Chlipala
2 *
3 * This work is licensed under a
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
5 * Unported License.
6 * The license text is available at:
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
8 *)
9
10 (* begin hide *)
11 Require Import List.
12
13 Require Import Tactics DepList.
14
15 Set Implicit Arguments.
16 (* end hide *)
17
18
19 (** %\part{Chapters to be Moved Earlier}
20
21 \chapter{Generic Programming}% *)
22
23 (** TODO: Prose for this chapter *)
24
25
26 (** * Simple Algebraic Datatypes *)
27
28 Record constructor : Type := Con {
29 nonrecursive : Type;
30 recursive : nat
31 }.
32
33 Definition datatype := list constructor.
34
35 Definition Empty_set_dt : datatype := nil.
36 Definition unit_dt : datatype := Con unit 0 :: nil.
37 Definition bool_dt : datatype := Con unit 0 :: Con unit 0 :: nil.
38 Definition nat_dt : datatype := Con unit 0 :: Con unit 1 :: nil.
39 Definition list_dt (A : Type) : datatype := Con unit 0 :: Con A 1 :: nil.
40
41 Section tree.
42 Variable A : Type.
43
44 Inductive tree : Type :=
45 | Leaf : A -> tree
46 | Node : tree -> tree -> tree.
47 End tree.
48
49 Definition tree_dt (A : Type) : datatype := Con A 0 :: Con unit 2 :: nil.
50
51 Section denote.
52 Variable T : Type.
53
54 Definition constructorDenote (c : constructor) :=
55 nonrecursive c -> ilist T (recursive c) -> T.
56
57 Definition datatypeDenote := hlist constructorDenote.
58 End denote.
59
60 Notation "[ ! , ! ~> x ]" := ((fun _ _ => x) : constructorDenote _ (Con _ _)).
61 Notation "[ v , ! ~> x ]" := ((fun v _ => x) : constructorDenote _ (Con _ _)).
62 Notation "[ ! , r # n ~> x ]" := ((fun _ r => x) : constructorDenote _ (Con _ n)).
63 Notation "[ v , r # n ~> x ]" := ((fun v r => x) : constructorDenote _ (Con _ n)).
64
65 Definition Empty_set_den : datatypeDenote Empty_set Empty_set_dt :=
66 hnil.
67 Definition unit_den : datatypeDenote unit unit_dt :=
68 [!, ! ~> tt] ::: hnil.
69 Definition bool_den : datatypeDenote bool bool_dt :=
70 [!, ! ~> true] ::: [!, ! ~> false] ::: hnil.
71 Definition nat_den : datatypeDenote nat nat_dt :=
72 [!, ! ~> O] ::: [!, r # 1 ~> S (hd r)] ::: hnil.
73 Definition list_den (A : Type) : datatypeDenote (list A) (list_dt A) :=
74 [!, ! ~> nil] ::: [x, r # 1 ~> x :: hd r] ::: hnil.
75 Definition tree_den (A : Type) : datatypeDenote (tree A) (tree_dt A) :=
76 [v, ! ~> Leaf v] ::: [!, r # 2 ~> Node (hd r) (hd (tl r))] ::: hnil.