Certified Programming with Dependent Types: src/Generic.v comparison

comparison src/Generic.v @ 302:7b38729be069

Tweak mark-up to support coqdoc 8.3

author	Adam Chlipala <adam@chlipala.net>
date	Mon, 17 Jan 2011 15:12:30 -0500
parents	540a09187193
children	d5787b70cf48

comparison

equal deleted inserted replaced

-:f4768d5a75eb
+:7b38729be069
 else (hhd (htl cases)) tt INil.
 Eval compute in size bool_fix.
 (** %\vspace{-.15in}% [[
 = fun b : bool => if b then 1 else 1
 : bool -> nat
-]] *)
+]]
+*)
 Definition nat_fix : fixDenote nat nat_dt :=
 fun R cases => fix F (n : nat) : R :=
 match n with
 | O => (hhd cases) tt INil
 = fix F (n : nat) : nat := match n with
 | 0 => 1
 | S n' => F n' + 1
 end
 : nat -> nat
-]] *)
+]]
+*)
 Definition list_fix (A : Type) : fixDenote (list A) (list_dt A) :=
 fun R cases => fix F (ls : list A) : R :=
 match ls with
 | nil => (hhd cases) tt INil
 match ls with
 | nil => 1
 | _ :: ls' => F ls' + 1
 end
 : forall A : Type, list A -> nat
-]] *)
+]]
+*)
 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 => (hhd cases) x INil
 match t with
 | Leaf _ => 1
 | Node t1 t2 => F t1 + (F t2 + 1)
 end
 : forall A : Type, tree A -> n
-]] *)
+]]
+*)
 (* end thide *)
 (** ** Pretty-Printing *)
 (** %\vspace{-.15in}% [[
 hmap
 : forall (A : Type) (B1 B2 : A -> Type),
 (forall x : A, B1 x -> B2 x) ->
 forall ls : list A, hlist B1 ls -> hlist B2 ls
-]] *)
+]]
+*)
 Definition print T dt (pr : print_datatype dt) (fx : fixDenote T dt) : T -> string :=
 fx string (hmap (B1 := print_constructor) (B2 := constructorDenote string)
 (fun _ pc x r => printName pc ++ "(" ++ printNonrec pc x
 ++ foldr (fun s acc => ", " ++ s ++ acc) ")" r) pr).
 Eval compute in print HNil Empty_set_fix.
 (** %\vspace{-.15in}% [[
 = fun emp : Empty_set => match emp return string with
 end
 : Empty_set -> string
-]] *)
+]]
+*)
 Eval compute in print (^ "tt" (fun _ => "") ::: HNil) unit_fix.
 (** %\vspace{-.15in}% [[
 = fun _ : unit => "tt()"
 : unit -> string
-]] *)
+]]
+*)
 Eval compute in print (^ "true" (fun _ => "")
 ::: ^ "false" (fun _ => "")
 ::: HNil) bool_fix.
 (** %\vspace{-.15in}% [[
 = fun b : bool => if b then "true()" else "false()"
 : bool -> s
-]] *)
+]]
+*)
 Definition print_nat := print (^ "O" (fun _ => "")
 ::: ^ "S" (fun _ => "")
 ::: HNil) nat_fix.
 Eval cbv beta iota delta -[append] in print_nat.
 match n with
 | 0%nat => "O" ++ "(" ++ "" ++ ")"
 | S n' => "S" ++ "(" ++ "" ++ ", " ++ F n' ++ ")"
 end
 : nat -> string
-]] *)
+]]
+*)
 Eval simpl in print_nat 0.
 (** %\vspace{-.15in}% [[
 = "O()"
 : string
-]] *)
+]]
+*)
 Eval simpl in print_nat 1.
 (** %\vspace{-.15in}% [[
 = "S(, O())"
 : string
-]] *)
+]]
+*)
 Eval simpl in print_nat 2.
 (** %\vspace{-.15in}% [[
 = "S(, S(, O()))"
 : string
-]] *)
+]]
+*)
 Eval cbv beta iota delta -[append] in fun A (pr : A -> string) =>
 print (^ "nil" (fun _ => "")
 ::: ^ "cons" pr
 ::: HNil) (@list_fix A).
 match ls with
 | nil => "nil" ++ "(" ++ "" ++ ")"
 | x :: ls' => "cons" ++ "(" ++ pr x ++ ", " ++ F ls' ++ ")"
 end
 : forall A : Type, (A -> string) -> list A -> string
-]] *)
+]]
+*)
 Eval cbv beta iota delta -[append] in fun A (pr : A -> string) =>
 print (^ "Leaf" pr
 ::: ^ "Node" (fun _ => "")
 ::: HNil) (@tree_fix A).
 | Leaf x => "Leaf" ++ "(" ++ pr x ++ ")"
 | Node t1 t2 =>
 "Node" ++ "(" ++ "" ++ ", " ++ F t1 ++ ", " ++ F t2 ++ ")"
 end
 : forall A : Type, (A -> string) -> tree A -> string
-]] *)
+]]
+*)
 (** ** Mapping *)
 (* EX: Define a generic [map] function. *)
 (** %\vspace{-.15in}% [[
 = fun (_ : Empty_set -> Empty_set) (emp : Empty_set) =>
 match emp return Empty_set with
 end
 : (Empty_set -> Empty_set) -> Empty_set -> Empty_set
-]] *)
+]]
+*)
 Eval compute in map unit_den unit_fix.
 (** %\vspace{-.15in}% [[
 = fun (f : unit -> unit) (_ : unit) => f tt
 : (unit -> unit) -> unit -> unit
-]] *)
+]]
+*)
 Eval compute in map bool_den bool_fix.
 (** %\vspace{-.15in}% [[
 = fun (f : bool -> bool) (b : bool) => if b then f true else f false
 : (bool -> bool) -> bool -> bool
-]] *)
+]]
+*)
 Eval compute in map nat_den nat_fix.
 (** %\vspace{-.15in}% [[
 = fun f : nat -> nat =>
 fix F (n : nat) : nat :=
 match n with
 | 0%nat => f 0%nat
 | S n' => f (S (F n'))
 end
 : (nat -> nat) -> nat -> nat
-]] *)
+]]
+*)
 Eval compute in fun A => map (list_den A) (@list_fix A).
 (** %\vspace{-.15in}% [[
 = fun (A : Type) (f : list A -> list A) =>
 fix F (ls : list A) : list A :=
 match ls with
 | nil => f nil
 | x :: ls' => f (x :: F ls')
 end
 : forall A : Type, (list A -> list A) -> list A -> list A
-]] *)
+]]
+*)
 Eval compute in fun A => map (tree_den A) (@tree_fix A).
 (** %\vspace{-.15in}% [[
 = fun (A : Type) (f : tree A -> tree A) =>
 fix F (t : tree A) : tree A :=
 match t with
 | Leaf x => f (Leaf x)
 | Node t1 t2 => f (Node (F t1) (F t2))
 end
 : forall A : Type, (tree A -> tree A) -> tree A -> tree A
-]] *)
+]]
+*)
 Definition map_nat := map nat_den nat_fix.
 Eval simpl in map_nat S 0.
 (** %\vspace{-.15in}% [[
 = 1%nat
 : nat
-]] *)
+]]
+*)
 Eval simpl in map_nat S 1.
 (** %\vspace{-.15in}% [[
 = 3%nat
 : nat
-]] *)
+]]
+*)
 Eval simpl in map_nat S 2.
 (** %\vspace{-.15in}% [[
 = 5%nat
 : nat
-]] *)
+]]
+*)
 (** * Proving Theorems about Recursive Definitions *)
 (** We would like to be able to prove theorems about our generic functions.  To do so, we need to establish additional well-formedness properties that must hold of pieces of evidence. *)
 fx nat
 (hmake
 (fun (x : constructor) (_ : nonrecursive x)
 (r : ilist nat (recursive x)) => foldr plus 1%nat r) dt) t > 0) v
-]] *)
+]]
+*)
 apply dok; crush.
 (** [[
 H : forall i : fin (recursive c),
 fx nat

Mercurial > cpdt > repo

comparison src/Generic.v @ 302:7b38729be069