From 3a018fbf16f576cc32700825396d85adf7994140 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Sun, 18 Feb 2018 12:49:36 -0500
Subject: [PATCH] Start of FirstClassFunctions

---
 FirstClassFunctions.v | 73 +++++++++++++++++++++++++++++++++++++++++++
 README.md             |  1 +
 2 files changed, 74 insertions(+)
 create mode 100644 FirstClassFunctions.v

diff --git a/FirstClassFunctions.v b/FirstClassFunctions.v
new file mode 100644
index 0000000..d26a542
--- /dev/null
+++ b/FirstClassFunctions.v
@@ -0,0 +1,73 @@
+(** Formal Reasoning About Programs <http://adam.chlipala.net/frap/>
+  * Supplementary Coq material: first-class functions and continuations
+  * Author: Adam Chlipala
+  * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *)
+
+Require Import Frap.
+
+Set Implicit Arguments.
+
+
+(** * Classic list functions *)
+
+Fixpoint map {A B : Set} (f : A -> B) (ls : list A) : list B :=
+  match ls with
+  | nil => nil
+  | x :: ls' => f x :: map f ls'
+  end.
+
+Fixpoint filter {A : Set} (f : A -> bool) (ls : list A) : list A :=
+  match ls with
+  | nil => nil
+  | x :: ls' => if f x then x :: filter f ls' else filter f ls'
+  end.
+
+Fixpoint foldl {A B : Set} (f : A -> B -> B) (acc : B) (ls : list A) : B :=
+  match ls with
+  | nil => acc
+  | x :: ls' => foldl f (f x acc) ls'
+  end.
+
+Record programming_languages := {
+  Name : string;
+  PurelyFunctional : bool;
+  AppearedInYear : nat
+}.
+
+Definition pascal := {|
+  Name := "Pascal";
+  PurelyFunctional := false;
+  AppearedInYear := 1970
+|}.
+
+Definition c := {|
+  Name := "C";
+  PurelyFunctional := false;
+  AppearedInYear := 1972
+|}.
+
+Definition gallina := {|
+  Name := "Gallina";
+  PurelyFunctional := true;
+  AppearedInYear := 1989
+|}.
+
+Definition haskell := {|
+  Name := "Haskell";
+  PurelyFunctional := true;
+  AppearedInYear := 1990
+|}.
+
+Definition ocaml := {|
+  Name := "OCaml";
+  PurelyFunctional := false;
+  AppearedInYear := 1996
+|}.
+
+Definition languages := [pascal; c; gallina; haskell; ocaml].
+
+Compute map Name languages.
+Compute map Name (filter PurelyFunctional languages).
+Compute foldl max 0 (map AppearedInYear languages).
+Compute foldl max 0 (map AppearedInYear (filter PurelyFunctional languages)).
+
diff --git a/README.md b/README.md
index 99f12d1..e22dfb9 100644
--- a/README.md
+++ b/README.md
@@ -12,6 +12,7 @@ The main narrative, also present in the book PDF, presents standard program-proo
   * `Polymorphism.v`: polymorphism and generic data structures
 * Chapter 3: `DataAbstraction.v`
 * Chapter 4: `Interpreters.v`
+  * `FirstClassFunctions.v`: functions as data; continuations and continuation-passing style
 * Chapter 5: `TransitionSystems.v`
   * `IntroToProofScripting.v`: writing scripts to find proofs in Coq
 * Chapter 6: `ModelChecking.v`