Mercurial > cpdt > repo

comparison src/Generic.v @ 195:3676acc40ce1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Pretty-printing
author Adam Chlipala <adamc@hcoop.net>
date Fri, 28 Nov 2008 11:42:07 -0500
parents 063b5741c248
children b4ea71b6bf94
comparison
equal deleted inserted replaced
194:063b5741c248 195:3676acc40ce1
6 * The license text is available at: 6 * The license text is available at:
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/ 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
8 *) 8 *)
9 9
10 (* begin hide *) 10 (* begin hide *)
11 Require Import List. 11 Require Import String List.
12 12
13 Require Import Tactics DepList. 13 Require Import Tactics DepList.
14 14
15 Set Implicit Arguments. 15 Set Implicit Arguments.
16 (* end hide *) 16 (* end hide *)
21 \chapter{Generic Programming}% *) 21 \chapter{Generic Programming}% *)
22 22
23 (** TODO: Prose for this chapter *) 23 (** TODO: Prose for this chapter *)
24 24
25 25
26 (** * Simple Algebraic Datatypes *) 26 (** * Reflecting Datatype Definitions *)
27 27
28 Record constructor : Type := Con { 28 Record constructor : Type := Con {
29 nonrecursive : Type; 29 nonrecursive : Type;
30 recursive : nat 30 recursive : nat
31 }. 31 }.
73 Definition list_den (A : Type) : datatypeDenote (list A) (list_dt A) := 73 Definition list_den (A : Type) : datatypeDenote (list A) (list_dt A) :=
74 [!, ! ~> nil] ::: [x, r # 1 ~> x :: hd r] ::: hnil. 74 [!, ! ~> nil] ::: [x, r # 1 ~> x :: hd r] ::: hnil.
75 Definition tree_den (A : Type) : datatypeDenote (tree A) (tree_dt A) := 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. 76 [v, ! ~> Leaf v] ::: [!, r # 2 ~> Node (hd r) (hd (tl r))] ::: hnil.
77 77
78
79 (** * Recursive Definitions *)
80
78 Definition fixDenote (T : Type) (dt : datatype) := 81 Definition fixDenote (T : Type) (dt : datatype) :=
79 forall (R : Type), datatypeDenote R dt -> (T -> R). 82 forall (R : Type), datatypeDenote R dt -> (T -> R).
80 83
81 Definition size T dt (fx : fixDenote T dt) : T -> nat := 84 Definition size T dt (fx : fixDenote T dt) : T -> nat :=
82 fx nat (hmake (B := constructorDenote nat) (fun _ _ r => foldr plus 1 r) dt). 85 fx nat (hmake (B := constructorDenote nat) (fun _ _ r => foldr plus 1 r) dt).
116 match t with 119 match t with
117 | Leaf x => (fst cases) x inil 120 | Leaf x => (fst cases) x inil
118 | Node t1 t2 => (fst (snd cases)) tt (icons (F t1) (icons (F t2) inil)) 121 | Node t1 t2 => (fst (snd cases)) tt (icons (F t1) (icons (F t2) inil))
119 end. 122 end.
120 Eval cbv beta iota delta -[plus] in fun A => size (@tree_fix A). 123 Eval cbv beta iota delta -[plus] in fun A => size (@tree_fix A).
124
125
126 (** ** Pretty-Printing *)
127
128 Record print_constructor (c : constructor) : Type := PI {
129 printName : string;
130 printNonrec : nonrecursive c -> string
131 }.
132
133 Notation "^" := (PI (Con _ _)).
134
135 Definition print_datatype := hlist print_constructor.
136
137 Open Local Scope string_scope.
138
139 Definition print T dt (pr : print_datatype dt) (fx : fixDenote T dt) : T -> string :=
140 fx string (hmap (B1 := print_constructor) (B2 := constructorDenote string)
141 (fun _ pc x r => printName pc ++ "(" ++ printNonrec pc x
142 ++ foldr (fun s acc => ", " ++ s ++ acc) ")" r) pr).
143
144 Eval compute in print hnil Empty_set_fix.
145 Eval compute in print (^ "tt" (fun _ => "") ::: hnil) unit_fix.
146 Eval compute in print (^ "true" (fun _ => "")
147 ::: ^ "false" (fun _ => "")
148 ::: hnil) bool_fix.
149
150 Definition print_nat := print (^ "O" (fun _ => "")
151 ::: ^ "S" (fun _ => "")
152 ::: hnil) nat_fix.
153 Eval cbv beta iota delta -[append] in print_nat.
154 Eval simpl in print_nat 0.
155 Eval simpl in print_nat 1.
156 Eval simpl in print_nat 2.
157
158 Eval cbv beta iota delta -[append] in fun A (pr : A -> string) =>
159 print (^ "nil" (fun _ => "")
160 ::: ^ "cons" pr
161 ::: hnil) (@list_fix A).
162 Eval cbv beta iota delta -[append] in fun A (pr : A -> string) =>
163 print (^ "Leaf" pr
164 ::: ^ "Node" (fun _ => "")
165 ::: hnil) (@tree_fix A).