Mercurial > cpdt > repo
diff src/Generic.v @ 193:8e9499e27b6c
Start of Generic
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Fri, 28 Nov 2008 09:55:56 -0500 |
parents | |
children | 063b5741c248 |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Generic.v Fri Nov 28 09:55:56 2008 -0500 @@ -0,0 +1,76 @@ +(* Copyright (c) 2008, Adam Chlipala + * + * This work is licensed under a + * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 + * Unported License. + * The license text is available at: + * http://creativecommons.org/licenses/by-nc-nd/3.0/ + *) + +(* begin hide *) +Require Import List. + +Require Import Tactics DepList. + +Set Implicit Arguments. +(* end hide *) + + +(** %\part{Chapters to be Moved Earlier} + +\chapter{Generic Programming}% *) + +(** TODO: Prose for this chapter *) + + +(** * Simple Algebraic Datatypes *) + +Record constructor : Type := Con { + nonrecursive : Type; + recursive : nat +}. + +Definition datatype := list constructor. + +Definition Empty_set_dt : datatype := nil. +Definition unit_dt : datatype := Con unit 0 :: nil. +Definition bool_dt : datatype := Con unit 0 :: Con unit 0 :: nil. +Definition nat_dt : datatype := Con unit 0 :: Con unit 1 :: nil. +Definition list_dt (A : Type) : datatype := Con unit 0 :: Con A 1 :: nil. + +Section tree. + Variable A : Type. + + Inductive tree : Type := + | Leaf : A -> tree + | Node : tree -> tree -> tree. +End tree. + +Definition tree_dt (A : Type) : datatype := Con A 0 :: Con unit 2 :: nil. + +Section denote. + Variable T : Type. + + Definition constructorDenote (c : constructor) := + nonrecursive c -> ilist T (recursive c) -> T. + + Definition datatypeDenote := hlist constructorDenote. +End denote. + +Notation "[ ! , ! ~> x ]" := ((fun _ _ => x) : constructorDenote _ (Con _ _)). +Notation "[ v , ! ~> x ]" := ((fun v _ => x) : constructorDenote _ (Con _ _)). +Notation "[ ! , r # n ~> x ]" := ((fun _ r => x) : constructorDenote _ (Con _ n)). +Notation "[ v , r # n ~> x ]" := ((fun v r => x) : constructorDenote _ (Con _ n)). + +Definition Empty_set_den : datatypeDenote Empty_set Empty_set_dt := + hnil. +Definition unit_den : datatypeDenote unit unit_dt := + [!, ! ~> tt] ::: hnil. +Definition bool_den : datatypeDenote bool bool_dt := + [!, ! ~> true] ::: [!, ! ~> false] ::: hnil. +Definition nat_den : datatypeDenote nat nat_dt := + [!, ! ~> O] ::: [!, r # 1 ~> S (hd r)] ::: hnil. +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.