Mercurial > cpdt > repo

annotate 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
rev   line source
adamc@193 1 (* Copyright (c) 2008, Adam Chlipala
adamc@193 2 *
adamc@193 3 * This work is licensed under a
adamc@193 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@193 5 * Unported License.
adamc@193 6 * The license text is available at:
adamc@193 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@193 8 *)
adamc@193 9
adamc@193 10 (* begin hide *)
adamc@195 11 Require Import String List.
adamc@193 12
adamc@193 13 Require Import Tactics DepList.
adamc@193 14
adamc@193 15 Set Implicit Arguments.
adamc@193 16 (* end hide *)
adamc@193 17
adamc@193 18
adamc@193 19 (** %\part{Chapters to be Moved Earlier}
adamc@193 20
adamc@193 21 \chapter{Generic Programming}% *)
adamc@193 22
adamc@193 23 (** TODO: Prose for this chapter *)
adamc@193 24
adamc@193 25
adamc@195 26 (** * Reflecting Datatype Definitions *)
adamc@193 27
adamc@193 28 Record constructor : Type := Con {
adamc@193 29 nonrecursive : Type;
adamc@193 30 recursive : nat
adamc@193 31 }.
adamc@193 32
adamc@193 33 Definition datatype := list constructor.
adamc@193 34
adamc@193 35 Definition Empty_set_dt : datatype := nil.
adamc@193 36 Definition unit_dt : datatype := Con unit 0 :: nil.
adamc@193 37 Definition bool_dt : datatype := Con unit 0 :: Con unit 0 :: nil.
adamc@193 38 Definition nat_dt : datatype := Con unit 0 :: Con unit 1 :: nil.
adamc@193 39 Definition list_dt (A : Type) : datatype := Con unit 0 :: Con A 1 :: nil.
adamc@193 40
adamc@193 41 Section tree.
adamc@193 42 Variable A : Type.
adamc@193 43
adamc@193 44 Inductive tree : Type :=
adamc@193 45 | Leaf : A -> tree
adamc@193 46 | Node : tree -> tree -> tree.
adamc@193 47 End tree.
adamc@193 48
adamc@193 49 Definition tree_dt (A : Type) : datatype := Con A 0 :: Con unit 2 :: nil.
adamc@193 50
adamc@193 51 Section denote.
adamc@193 52 Variable T : Type.
adamc@193 53
adamc@193 54 Definition constructorDenote (c : constructor) :=
adamc@193 55 nonrecursive c -> ilist T (recursive c) -> T.
adamc@193 56
adamc@193 57 Definition datatypeDenote := hlist constructorDenote.
adamc@193 58 End denote.
adamc@193 59
adamc@193 60 Notation "[ ! , ! ~> x ]" := ((fun _ _ => x) : constructorDenote _ (Con _ _)).
adamc@193 61 Notation "[ v , ! ~> x ]" := ((fun v _ => x) : constructorDenote _ (Con _ _)).
adamc@193 62 Notation "[ ! , r # n ~> x ]" := ((fun _ r => x) : constructorDenote _ (Con _ n)).
adamc@193 63 Notation "[ v , r # n ~> x ]" := ((fun v r => x) : constructorDenote _ (Con _ n)).
adamc@193 64
adamc@193 65 Definition Empty_set_den : datatypeDenote Empty_set Empty_set_dt :=
adamc@193 66 hnil.
adamc@193 67 Definition unit_den : datatypeDenote unit unit_dt :=
adamc@193 68 [!, ! ~> tt] ::: hnil.
adamc@193 69 Definition bool_den : datatypeDenote bool bool_dt :=
adamc@193 70 [!, ! ~> true] ::: [!, ! ~> false] ::: hnil.
adamc@193 71 Definition nat_den : datatypeDenote nat nat_dt :=
adamc@193 72 [!, ! ~> O] ::: [!, r # 1 ~> S (hd r)] ::: hnil.
adamc@193 73 Definition list_den (A : Type) : datatypeDenote (list A) (list_dt A) :=
adamc@193 74 [!, ! ~> nil] ::: [x, r # 1 ~> x :: hd r] ::: hnil.
adamc@193 75 Definition tree_den (A : Type) : datatypeDenote (tree A) (tree_dt A) :=
adamc@193 76 [v, ! ~> Leaf v] ::: [!, r # 2 ~> Node (hd r) (hd (tl r))] ::: hnil.
adamc@194 77
adamc@195 78
adamc@195 79 (** * Recursive Definitions *)
adamc@195 80
adamc@194 81 Definition fixDenote (T : Type) (dt : datatype) :=
adamc@194 82 forall (R : Type), datatypeDenote R dt -> (T -> R).
adamc@194 83
adamc@194 84 Definition size T dt (fx : fixDenote T dt) : T -> nat :=
adamc@194 85 fx nat (hmake (B := constructorDenote nat) (fun _ _ r => foldr plus 1 r) dt).
adamc@194 86
adamc@194 87 Definition Empty_set_fix : fixDenote Empty_set Empty_set_dt :=
adamc@194 88 fun R _ emp => match emp with end.
adamc@194 89 Eval compute in size Empty_set_fix.
adamc@194 90
adamc@194 91 Definition unit_fix : fixDenote unit unit_dt :=
adamc@194 92 fun R cases _ => (fst cases) tt inil.
adamc@194 93 Eval compute in size unit_fix.
adamc@194 94
adamc@194 95 Definition bool_fix : fixDenote bool bool_dt :=
adamc@194 96 fun R cases b => if b
adamc@194 97 then (fst cases) tt inil
adamc@194 98 else (fst (snd cases)) tt inil.
adamc@194 99 Eval compute in size bool_fix.
adamc@194 100
adamc@194 101 Definition nat_fix : fixDenote nat nat_dt :=
adamc@194 102 fun R cases => fix F (n : nat) : R :=
adamc@194 103 match n with
adamc@194 104 | O => (fst cases) tt inil
adamc@194 105 | S n' => (fst (snd cases)) tt (icons (F n') inil)
adamc@194 106 end.
adamc@194 107 Eval cbv beta iota delta -[plus] in size nat_fix.
adamc@194 108
adamc@194 109 Definition list_fix (A : Type) : fixDenote (list A) (list_dt A) :=
adamc@194 110 fun R cases => fix F (ls : list A) : R :=
adamc@194 111 match ls with
adamc@194 112 | nil => (fst cases) tt inil
adamc@194 113 | x :: ls' => (fst (snd cases)) x (icons (F ls') inil)
adamc@194 114 end.
adamc@194 115 Eval cbv beta iota delta -[plus] in fun A => size (@list_fix A).
adamc@194 116
adamc@194 117 Definition tree_fix (A : Type) : fixDenote (tree A) (tree_dt A) :=
adamc@194 118 fun R cases => fix F (t : tree A) : R :=
adamc@194 119 match t with
adamc@194 120 | Leaf x => (fst cases) x inil
adamc@194 121 | Node t1 t2 => (fst (snd cases)) tt (icons (F t1) (icons (F t2) inil))
adamc@194 122 end.
adamc@194 123 Eval cbv beta iota delta -[plus] in fun A => size (@tree_fix A).
adamc@195 124
adamc@195 125
adamc@195 126 (** ** Pretty-Printing *)
adamc@195 127
adamc@195 128 Record print_constructor (c : constructor) : Type := PI {
adamc@195 129 printName : string;
adamc@195 130 printNonrec : nonrecursive c -> string
adamc@195 131 }.
adamc@195 132
adamc@195 133 Notation "^" := (PI (Con _ _)).
adamc@195 134
adamc@195 135 Definition print_datatype := hlist print_constructor.
adamc@195 136
adamc@195 137 Open Local Scope string_scope.
adamc@195 138
adamc@195 139 Definition print T dt (pr : print_datatype dt) (fx : fixDenote T dt) : T -> string :=
adamc@195 140 fx string (hmap (B1 := print_constructor) (B2 := constructorDenote string)
adamc@195 141 (fun _ pc x r => printName pc ++ "(" ++ printNonrec pc x
adamc@195 142 ++ foldr (fun s acc => ", " ++ s ++ acc) ")" r) pr).
adamc@195 143
adamc@195 144 Eval compute in print hnil Empty_set_fix.
adamc@195 145 Eval compute in print (^ "tt" (fun _ => "") ::: hnil) unit_fix.
adamc@195 146 Eval compute in print (^ "true" (fun _ => "")
adamc@195 147 ::: ^ "false" (fun _ => "")
adamc@195 148 ::: hnil) bool_fix.
adamc@195 149
adamc@195 150 Definition print_nat := print (^ "O" (fun _ => "")
adamc@195 151 ::: ^ "S" (fun _ => "")
adamc@195 152 ::: hnil) nat_fix.
adamc@195 153 Eval cbv beta iota delta -[append] in print_nat.
adamc@195 154 Eval simpl in print_nat 0.
adamc@195 155 Eval simpl in print_nat 1.
adamc@195 156 Eval simpl in print_nat 2.
adamc@195 157
adamc@195 158 Eval cbv beta iota delta -[append] in fun A (pr : A -> string) =>
adamc@195 159 print (^ "nil" (fun _ => "")
adamc@195 160 ::: ^ "cons" pr
adamc@195 161 ::: hnil) (@list_fix A).
adamc@195 162 Eval cbv beta iota delta -[append] in fun A (pr : A -> string) =>
adamc@195 163 print (^ "Leaf" pr
adamc@195 164 ::: ^ "Node" (fun _ => "")
adamc@195 165 ::: hnil) (@tree_fix A).