Mercurial > cpdt > repo
comparison src/Generic.v @ 195:3676acc40ce1
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). |