Mercurial > cpdt > repo

comparison src/Generic.v @ 194:063b5741c248

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Generic size examples
author Adam Chlipala <adamc@hcoop.net>
date Fri, 28 Nov 2008 11:21:01 -0500
parents 8e9499e27b6c
children 3676acc40ce1
comparison
equal deleted inserted replaced
193:8e9499e27b6c 194:063b5741c248
72 [!, ! ~> O] ::: [!, r # 1 ~> S (hd r)] ::: hnil. 72 [!, ! ~> O] ::: [!, r # 1 ~> S (hd r)] ::: hnil.
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
78 Definition fixDenote (T : Type) (dt : datatype) :=
79 forall (R : Type), datatypeDenote R dt -> (T -> R).
80
81 Definition size T dt (fx : fixDenote T dt) : T -> nat :=
82 fx nat (hmake (B := constructorDenote nat) (fun _ _ r => foldr plus 1 r) dt).
83
84 Definition Empty_set_fix : fixDenote Empty_set Empty_set_dt :=
85 fun R _ emp => match emp with end.
86 Eval compute in size Empty_set_fix.
87
88 Definition unit_fix : fixDenote unit unit_dt :=
89 fun R cases _ => (fst cases) tt inil.
90 Eval compute in size unit_fix.
91
92 Definition bool_fix : fixDenote bool bool_dt :=
93 fun R cases b => if b
94 then (fst cases) tt inil
95 else (fst (snd cases)) tt inil.
96 Eval compute in size bool_fix.
97
98 Definition nat_fix : fixDenote nat nat_dt :=
99 fun R cases => fix F (n : nat) : R :=
100 match n with
101 | O => (fst cases) tt inil
102 | S n' => (fst (snd cases)) tt (icons (F n') inil)
103 end.
104 Eval cbv beta iota delta -[plus] in size nat_fix.
105
106 Definition list_fix (A : Type) : fixDenote (list A) (list_dt A) :=
107 fun R cases => fix F (ls : list A) : R :=
108 match ls with
109 | nil => (fst cases) tt inil
110 | x :: ls' => (fst (snd cases)) x (icons (F ls') inil)
111 end.
112 Eval cbv beta iota delta -[plus] in fun A => size (@list_fix A).
113
114 Definition tree_fix (A : Type) : fixDenote (tree A) (tree_dt A) :=
115 fun R cases => fix F (t : tree A) : R :=
116 match t with
117 | Leaf x => (fst cases) x inil
118 | Node t1 t2 => (fst (snd cases)) tt (icons (F t1) (icons (F t2) inil))
119 end.
120 Eval cbv beta iota delta -[plus] in fun A => size (@tree_fix A).