Generic size examples

src/DepList.v

@@ -80,11 +80,27 @@ Section ilist.
         | S n' => fun ls1 ls2 => icons (f (hd ls1) (hd ls2)) (map2 _ (tl ls1) (tl ls2))
       end.
   End map2.
+
+  Section fold.
+    Variable B : Type.
+    Variable f : A -> B -> B.
+    Variable i : B.
+
+    Fixpoint foldr (n : nat) : ilist n -> B :=
+      match n return ilist n -> B with
+        | O => fun _ => i
+        | S n' => fun ils => f (hd ils) (foldr n' (tl ils))
+      end.
+  End fold.
 End ilist.
 
+Implicit Arguments inil [A].
+Implicit Arguments icons [A n].
+
 Implicit Arguments icons [A n].
 Implicit Arguments get [A n].
 Implicit Arguments map2 [A n].
+Implicit Arguments foldr [A B n].
 
 Section hlist.
   Variable A : Type.
@@ -130,12 +146,21 @@ Section hlist.
       | nil => fun _ hls2 => hls2
       | _ :: _ => fun hls1 hls2 => (fst hls1, happ _ _ (snd hls1) hls2)
     end.
+
+  Variable f : forall x, B x.
+
+  Fixpoint hmake (ls : list A) : hlist ls :=
+    match ls return hlist ls with
+      | nil => hnil
+      | x :: ls' => hcons _ (f x) (hmake ls')
+    end.
 End hlist.
 
 Implicit Arguments hnil [A B].
 Implicit Arguments hcons [A B x ls].
 Implicit Arguments hget [A B elm ls].
 Implicit Arguments happ [A B ls1 ls2].
+Implicit Arguments hmake [A B].
 
 Implicit Arguments hfirst [A elm x ls].
 Implicit Arguments hnext [A elm x ls].

src/Generic.v

@@ -74,3 +74,47 @@ Definition list_den (A : Type) : datatypeDenote (list A) (list_dt A) :=
   [!, ! ~> nil] ::: [x, r # 1 ~> x :: hd r] ::: hnil.
 Definition tree_den (A : Type) : datatypeDenote (tree A) (tree_dt A) :=
   [v, ! ~> Leaf v] ::: [!, r # 2 ~> Node (hd r) (hd (tl r))] ::: hnil.
+
+Definition fixDenote (T : Type) (dt : datatype) :=
+  forall (R : Type), datatypeDenote R dt -> (T -> R).
+
+Definition size T dt (fx : fixDenote T dt) : T -> nat :=
+  fx nat (hmake (B := constructorDenote nat) (fun _ _ r => foldr plus 1 r) dt).
+
+Definition Empty_set_fix : fixDenote Empty_set Empty_set_dt :=
+  fun R _ emp => match emp with end.
+Eval compute in size Empty_set_fix.
+
+Definition unit_fix : fixDenote unit unit_dt :=
+  fun R cases _ => (fst cases) tt inil.
+Eval compute in size unit_fix.
+
+Definition bool_fix : fixDenote bool bool_dt :=
+  fun R cases b => if b
+    then (fst cases) tt inil
+    else (fst (snd cases)) tt inil.
+Eval compute in size bool_fix.
+
+Definition nat_fix : fixDenote nat nat_dt :=
+  fun R cases => fix F (n : nat) : R :=
+    match n with
+      | O => (fst cases) tt inil
+      | S n' => (fst (snd cases)) tt (icons (F n') inil)
+    end.
+Eval cbv beta iota delta -[plus] in size nat_fix.
+
+Definition list_fix (A : Type) : fixDenote (list A) (list_dt A) :=
+  fun R cases => fix F (ls : list A) : R :=
+    match ls with
+      | nil => (fst cases) tt inil
+      | x :: ls' => (fst (snd cases)) x (icons (F ls') inil)
+    end.
+Eval cbv beta iota delta -[plus] in fun A => size (@list_fix A).
+
+Definition tree_fix (A : Type) : fixDenote (tree A) (tree_dt A) :=
+  fun R cases => fix F (t : tree A) : R :=
+    match t with
+      | Leaf x => (fst cases) x inil
+      | Node t1 t2 => (fst (snd cases)) tt (icons (F t1) (icons (F t2) inil))
+    end.
+Eval cbv beta iota delta -[plus] in fun A => size (@tree_fix A).