adamc@216: (* Copyright (c) 2008-2009, Adam Chlipala adamc@193: * adamc@193: * This work is licensed under a adamc@193: * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 adamc@193: * Unported License. adamc@193: * The license text is available at: adamc@193: * http://creativecommons.org/licenses/by-nc-nd/3.0/ adamc@193: *) adamc@193: adamc@193: (* begin hide *) adamc@195: Require Import String List. adamc@193: adamc@193: Require Import Tactics DepList. adamc@193: adamc@193: Set Implicit Arguments. adamc@193: (* end hide *) adamc@193: adamc@193: adamc@193: (** %\part{Chapters to be Moved Earlier} adamc@193: adamc@193: \chapter{Generic Programming}% *) adamc@193: adamc@193: (** TODO: Prose for this chapter *) adamc@193: adamc@193: adamc@195: (** * Reflecting Datatype Definitions *) adamc@193: adamc@198: (* EX: Define a reflected representation of simple algebraic datatypes. *) adamc@198: adamc@198: (* begin thide *) adamc@193: Record constructor : Type := Con { adamc@193: nonrecursive : Type; adamc@193: recursive : nat adamc@193: }. adamc@193: adamc@193: Definition datatype := list constructor. adamc@193: adamc@193: Definition Empty_set_dt : datatype := nil. adamc@193: Definition unit_dt : datatype := Con unit 0 :: nil. adamc@193: Definition bool_dt : datatype := Con unit 0 :: Con unit 0 :: nil. adamc@193: Definition nat_dt : datatype := Con unit 0 :: Con unit 1 :: nil. adamc@193: Definition list_dt (A : Type) : datatype := Con unit 0 :: Con A 1 :: nil. adamc@198: (* end thide *) adamc@193: adamc@193: Section tree. adamc@193: Variable A : Type. adamc@193: adamc@193: Inductive tree : Type := adamc@193: | Leaf : A -> tree adamc@193: | Node : tree -> tree -> tree. adamc@193: End tree. adamc@193: adamc@198: (* begin thide *) adamc@193: Definition tree_dt (A : Type) : datatype := Con A 0 :: Con unit 2 :: nil. adamc@193: adamc@193: Section denote. adamc@193: Variable T : Type. adamc@193: adamc@193: Definition constructorDenote (c : constructor) := adamc@193: nonrecursive c -> ilist T (recursive c) -> T. adamc@193: adamc@193: Definition datatypeDenote := hlist constructorDenote. adamc@193: End denote. adamc@198: (* end thide *) adamc@193: adamc@193: Notation "[ ! , ! ~> x ]" := ((fun _ _ => x) : constructorDenote _ (Con _ _)). adamc@193: Notation "[ v , ! ~> x ]" := ((fun v _ => x) : constructorDenote _ (Con _ _)). adamc@193: Notation "[ ! , r # n ~> x ]" := ((fun _ r => x) : constructorDenote _ (Con _ n)). adamc@193: Notation "[ v , r # n ~> x ]" := ((fun v r => x) : constructorDenote _ (Con _ n)). adamc@193: adamc@198: (* begin thide *) adamc@193: Definition Empty_set_den : datatypeDenote Empty_set Empty_set_dt := adamc@216: HNil. adamc@193: Definition unit_den : datatypeDenote unit unit_dt := adamc@216: [!, ! ~> tt] ::: HNil. adamc@193: Definition bool_den : datatypeDenote bool bool_dt := adamc@216: [!, ! ~> true] ::: [!, ! ~> false] ::: HNil. adamc@193: Definition nat_den : datatypeDenote nat nat_dt := adamc@216: [!, ! ~> O] ::: [!, r # 1 ~> S (hd r)] ::: HNil. adamc@193: Definition list_den (A : Type) : datatypeDenote (list A) (list_dt A) := adamc@216: [!, ! ~> nil] ::: [x, r # 1 ~> x :: hd r] ::: HNil. adamc@193: Definition tree_den (A : Type) : datatypeDenote (tree A) (tree_dt A) := adamc@216: [v, ! ~> Leaf v] ::: [!, r # 2 ~> Node (hd r) (hd (tl r))] ::: HNil. adamc@198: (* end thide *) adamc@194: adamc@195: adamc@195: (** * Recursive Definitions *) adamc@195: adamc@198: (* EX: Define a generic [size] function. *) adamc@198: adamc@198: (* begin thide *) adamc@194: Definition fixDenote (T : Type) (dt : datatype) := adamc@194: forall (R : Type), datatypeDenote R dt -> (T -> R). adamc@194: adamc@194: Definition size T dt (fx : fixDenote T dt) : T -> nat := adamc@194: fx nat (hmake (B := constructorDenote nat) (fun _ _ r => foldr plus 1 r) dt). adamc@194: adamc@194: Definition Empty_set_fix : fixDenote Empty_set Empty_set_dt := adamc@194: fun R _ emp => match emp with end. adamc@194: Eval compute in size Empty_set_fix. adamc@194: adamc@194: Definition unit_fix : fixDenote unit unit_dt := adamc@216: fun R cases _ => (hhd cases) tt INil. adamc@194: Eval compute in size unit_fix. adamc@194: adamc@194: Definition bool_fix : fixDenote bool bool_dt := adamc@194: fun R cases b => if b adamc@216: then (hhd cases) tt INil adamc@216: else (hhd (htl cases)) tt INil. adamc@194: Eval compute in size bool_fix. adamc@194: adamc@194: Definition nat_fix : fixDenote nat nat_dt := adamc@194: fun R cases => fix F (n : nat) : R := adamc@194: match n with adamc@216: | O => (hhd cases) tt INil adamc@216: | S n' => (hhd (htl cases)) tt (ICons (F n') INil) adamc@194: end. adamc@194: Eval cbv beta iota delta -[plus] in size nat_fix. adamc@194: adamc@194: Definition list_fix (A : Type) : fixDenote (list A) (list_dt A) := adamc@194: fun R cases => fix F (ls : list A) : R := adamc@194: match ls with adamc@216: | nil => (hhd cases) tt INil adamc@216: | x :: ls' => (hhd (htl cases)) x (ICons (F ls') INil) adamc@194: end. adamc@194: Eval cbv beta iota delta -[plus] in fun A => size (@list_fix A). adamc@194: adamc@194: Definition tree_fix (A : Type) : fixDenote (tree A) (tree_dt A) := adamc@194: fun R cases => fix F (t : tree A) : R := adamc@194: match t with adamc@216: | Leaf x => (hhd cases) x INil adamc@216: | Node t1 t2 => (hhd (htl cases)) tt (ICons (F t1) (ICons (F t2) INil)) adamc@194: end. adamc@194: Eval cbv beta iota delta -[plus] in fun A => size (@tree_fix A). adamc@198: (* end thide *) adamc@195: adamc@195: adamc@195: (** ** Pretty-Printing *) adamc@195: adamc@198: (* EX: Define a generic pretty-printing function. *) adamc@198: adamc@198: (* begin thide *) adamc@195: Record print_constructor (c : constructor) : Type := PI { adamc@195: printName : string; adamc@195: printNonrec : nonrecursive c -> string adamc@195: }. adamc@195: adamc@195: Notation "^" := (PI (Con _ _)). adamc@195: adamc@195: Definition print_datatype := hlist print_constructor. adamc@195: adamc@195: Open Local Scope string_scope. adamc@195: adamc@195: Definition print T dt (pr : print_datatype dt) (fx : fixDenote T dt) : T -> string := adamc@195: fx string (hmap (B1 := print_constructor) (B2 := constructorDenote string) adamc@195: (fun _ pc x r => printName pc ++ "(" ++ printNonrec pc x adamc@195: ++ foldr (fun s acc => ", " ++ s ++ acc) ")" r) pr). adamc@198: (* end thide *) adamc@195: adamc@216: Eval compute in print HNil Empty_set_fix. adamc@216: Eval compute in print (^ "tt" (fun _ => "") ::: HNil) unit_fix. adamc@195: Eval compute in print (^ "true" (fun _ => "") adamc@195: ::: ^ "false" (fun _ => "") adamc@216: ::: HNil) bool_fix. adamc@195: adamc@195: Definition print_nat := print (^ "O" (fun _ => "") adamc@195: ::: ^ "S" (fun _ => "") adamc@216: ::: HNil) nat_fix. adamc@195: Eval cbv beta iota delta -[append] in print_nat. adamc@195: Eval simpl in print_nat 0. adamc@195: Eval simpl in print_nat 1. adamc@195: Eval simpl in print_nat 2. adamc@195: adamc@195: Eval cbv beta iota delta -[append] in fun A (pr : A -> string) => adamc@195: print (^ "nil" (fun _ => "") adamc@195: ::: ^ "cons" pr adamc@216: ::: HNil) (@list_fix A). adamc@195: Eval cbv beta iota delta -[append] in fun A (pr : A -> string) => adamc@195: print (^ "Leaf" pr adamc@195: ::: ^ "Node" (fun _ => "") adamc@216: ::: HNil) (@tree_fix A). adamc@196: adamc@196: adamc@196: (** ** Mapping *) adamc@196: adamc@198: (* EX: Define a generic [map] function. *) adamc@198: adamc@198: (* begin thide *) adamc@196: Definition map T dt (dd : datatypeDenote T dt) (fx : fixDenote T dt) (f : T -> T) : T -> T := adamc@196: fx T (hmap (B1 := constructorDenote T) (B2 := constructorDenote T) adamc@196: (fun _ c x r => f (c x r)) dd). adamc@198: (* end thide *) adamc@196: adamc@196: Eval compute in map Empty_set_den Empty_set_fix. adamc@196: Eval compute in map unit_den unit_fix. adamc@196: Eval compute in map bool_den bool_fix. adamc@196: Eval compute in map nat_den nat_fix. adamc@196: Eval compute in fun A => map (list_den A) (@list_fix A). adamc@196: Eval compute in fun A => map (tree_den A) (@tree_fix A). adamc@196: adamc@196: Definition map_nat := map nat_den nat_fix. adamc@196: Eval simpl in map_nat S 0. adamc@196: Eval simpl in map_nat S 1. adamc@196: Eval simpl in map_nat S 2. adamc@196: adamc@196: adamc@196: (** * Proving Theorems about Recursive Definitions *) adamc@196: adamc@198: (* begin thide *) adamc@196: Section ok. adamc@196: Variable T : Type. adamc@196: Variable dt : datatype. adamc@196: adamc@196: Variable dd : datatypeDenote T dt. adamc@196: Variable fx : fixDenote T dt. adamc@196: adamc@196: Definition datatypeDenoteOk := adamc@196: forall P : T -> Prop, adamc@196: (forall c (m : member c dt) (x : nonrecursive c) (r : ilist T (recursive c)), adamc@215: (forall i : fin (recursive c), P (get r i)) adamc@196: -> P ((hget dd m) x r)) adamc@196: -> forall v, P v. adamc@196: adamc@196: Definition fixDenoteOk := adamc@196: forall (R : Type) (cases : datatypeDenote R dt) adamc@196: c (m : member c dt) adamc@196: (x : nonrecursive c) (r : ilist T (recursive c)), adamc@216: fx cases ((hget dd m) x r) adamc@216: = (hget cases m) x (imap (fx cases) r). adamc@196: End ok. adamc@196: adamc@196: Implicit Arguments datatypeDenoteOk [T dt]. adamc@196: adamc@196: Lemma foldr_plus : forall n (ils : ilist nat n), adamc@196: foldr plus 1 ils > 0. adamc@216: induction ils; crush. adamc@196: Qed. adamc@198: (* end thide *) adamc@196: adamc@197: Theorem size_positive : forall T dt adamc@197: (dd : datatypeDenote T dt) (fx : fixDenote T dt) adamc@197: (dok : datatypeDenoteOk dd) (fok : fixDenoteOk dd fx) adamc@196: (v : T), adamc@196: size fx v > 0. adamc@198: (* begin thide *) adamc@196: Hint Rewrite hget_hmake : cpdt. adamc@196: Hint Resolve foldr_plus. adamc@196: adamc@197: unfold size; intros; pattern v; apply dok; crush. adamc@196: Qed. adamc@198: (* end thide *) adamc@197: adamc@197: Theorem map_id : forall T dt adamc@197: (dd : datatypeDenote T dt) (fx : fixDenote T dt) adamc@197: (dok : datatypeDenoteOk dd) (fok : fixDenoteOk dd fx) adamc@197: (v : T), adamc@197: map dd fx (fun x => x) v = v. adamc@198: (* begin thide *) adamc@197: Hint Rewrite hget_hmap : cpdt. adamc@197: adamc@197: unfold map; intros; pattern v; apply dok; crush. adamc@197: match goal with adamc@197: | [ |- hget _ _ _ ?R1 = hget _ _ _ ?R2 ] => replace R1 with R2 adamc@197: end; crush. adamc@197: adamc@197: induction (recursive c); crush. adamc@216: dep_destruct r; reflexivity. adamc@216: dep_destruct r; crush. adamc@216: rewrite (H First). adamc@197: f_equal. adamc@197: apply IHn; crush. adamc@216: apply (H (Next i)). adamc@197: Qed. adamc@198: (* end thide *)