
\documentclass[9pt,xcolor=dvipsnames,unknownkeysallowed]{beamer}
%\documentclass[handout,9pt,xcolor=dvipsnames,unknownkeysallowed]{beamer}

\input{../Common/common}
\newcommand{\seqexp}{\mathit{seqexp}}
\newcommand{\queryexp}{\mathit{queryexp}}



\title % (optional, use only with long paper titles)
{02157 Functional Programming}

\subtitle
{Sequences and Sequence Expressions} % (optional)

\date {MRH 21/11/2024}% (optional)


\begin{document}

\begin{frame}
  \titlepage


\end{frame}

\begin{frame}
%
%
\begin{itemize}
	\item {\Large\darkgreen Sequences and Sequence expressions}
%	
	\bigskip
%	
	\item {\Large\darkgreen Property-based testing}
	\begin{itemize}
	\item Rehearsal of trees

    \item Examples with sequences

    \item Properties, generators and Shrinkers

    \item A look at computation expressions for generators\\
     resembles sequence expressions
 	
	\end{itemize}
%	
%	
\end{itemize}
%
\end{frame}


\begin{frame}[fragile]

{\redbrown Sequence:} a possibly infinite, ordered collection
of elements, where the elements are computed by {\blue demand only}

\medskip

\begin{itemize}
\item the sequence concept

\item standard sequence functions -- the \texttt{\blue Seq} library

\item sequence expressions -- {\darkgreen computation expressions} used generate sequences in a step by step manner

\end{itemize}

\bigskip

{\darkgreen Computation expressions}: provide a mean to express specific kinds of computations where low-level details are hidden. See Chapter 12.

\end{frame}

\begin{frame}{Sequences (or Lazy Lists)}

\begin{itemize}
\item {\em\redbrown lazy evaluation} or {\em\redbrown delayed
evaluation} is the technique of delaying a computation until the
result of the computation is needed.
\end{itemize}
\ \hfill Default in lazy languages like Haskell
\bigskip

\pause
\begin{center}\redbrown It is occasionally efficient to be lazy.
\end{center}

\bigskip
\pause

A special form of this is a {\em\redbrown sequence}, where the
elements are not evaluated until their values are required by the
rest of the program.

\begin{itemize}
\item a {\em\redbrown sequence} may be infinite\\
\ \hfill \hfill just a finite part is
used in computations
\end{itemize}

\bigskip

\pause
Example:
\begin{itemize}

\item Consider the sequence of all prime numbers: $\blue 2,3, 5,7,
11, 13, 17, 19, 23, \ldots$

\item the first $\redbrown 5$ are $\blue 2,3,5,7,11$\\
\ \hfill {\darkgreen Sieve of Eratosthenes}

\end{itemize}


\end{frame}

\begin{frame}[fragile]
\frametitle{Delayed computations in {\darkgreen eager languages}}

The computation of the value of $\blue e$ can be delayed by "packing" it into a function (a {\redbrown closure}):
\[\blue \verb!fun () ->!\ e \]

\pause

Example:
\begin{alltt}
fun () -> 3+4;;
\ett{val it : unit -> int = <fun:clo@10-2>}

it();;
\ett{val it : int = 7}
\end{alltt}

The addition is deferred until the closure is applied.


\bigskip 

\begin{center}
	\redbrown How can we convince ourselves that the addition is deferred?
\end{center}

\end{frame}


\begin{frame}[fragile]
\frametitle{Example continued}
A use of {\darkgreen side effects} may reveal when computations are performed:
\begin{alltt}\blue
let idWithPrint i = let _ ={\darkgreen printfn "\%d" i}
                    i;;
\ett{val idWithPrint : int -> int}

idWithPrint 3;;
\ett{3}
\ett{val it : int = 3}
\end{alltt}
The value is printed before it is returned.

\medskip
\pause

\begin{alltt}\blue
fun () -> (idWithPrint 3) + (idWithPrint 4);;
\ett{val it : unit -> int = <fun:clo@14-3>}
\end{alltt}
Nothing is printed yet.

\medskip
\pause

\begin{alltt}\redbrown
it();;
\ett{3}
\ett{4}
\ett{val it : int = 7}
\end{alltt}


\end{frame}


\begin{frame}[fragile]
\frametitle{Sequences in F\#}

A lazy list or {\em\redbrown sequence} in F\# is a possibly infinite, ordered collection of elements, where the elements are computed {\redbrown by demand} only.

\bigskip
\pause

The natural number sequence $\blue 0, 1, 2, \ldots$ is created as follows:
\begin{alltt}\blue
let nat ={\redbrown Seq.initInfinite} id;;
\ett{val nat : seq<int>}
\end{alltt}

where $\blue \verb|id:'a->'a|$ is the built-in {\blue identity function}, i.e. $\blue \verb|id|(x) = x$
\pause
\bigskip

\begin{center}
\redbrown No element in the sequence is generated yet!
\end{center}

\pause
\bigskip

\begin{center}
	\darkgreen The type {\blue \texttt{seq<'a>}} is an abstract datatype. \\
	
	\bigskip\pause
	
	Programs on sequences are constructed from \texttt{\blue Seq}-library functions 
\end{center}


\end{frame}

\begin{frame}[fragile]
\frametitle{Explicit sequences and conversions for finite sequences}

Two conversion functions 
\begin{alltt}\blue 
Seq.toList: seq<'a> -> 'a list

Seq.ofList: 'a list -> seq<'a>
\end{alltt}

\medskip

with examples

\medskip
\begin{alltt}\blue 
let sq = Seq.ofList ['a' .. 'f'];;
\ett{val sq : seq<char> = ['a'; 'b'; 'c'; 'd'; 'e'; 'f']}

let cs = Seq.toList sq;;
\ett{val cs : char list = ['a'; 'b'; 'c'; 'd'; 'e'; 'f']}
\end{alltt}

\pause\bigskip

Alternatively, a finite sequence can written as follows:
\begin{alltt}\blue 
let sq = seq ['a' .. 'f'];;
\ett{val sq : seq<char> = ['a'; 'b'; 'c'; 'd'; 'e'; 'f']}
\end{alltt}


\pause
Notice
\begin{itemize}	
\item {\blue Seq.toList} -- does not terminate for infinite sequences
\item {\blue seq $[x_1; \ldots; x_n]$} is a finite sequence with $\blue n\ge 0$ elements	
\end{itemize}



\end{frame}


\begin{frame}[fragile]
	\frametitle{Selected functions from the library: \blue Seq}
	
\begin{itemize}
	\item $\blue \verb|initInfinite: (int ->'a) -> seq<'a>|$.\\
	\quad $\blue \verb|initInfinite|\, f$ generates the sequence $\blue f(0), f(1), f(2), \ldots$ \\[3mm]
	
	\item $\blue \verb|delay: (unit->seq<'a>) -> seq<'a>|$.\\
	\quad	$\blue \verb|delay|\, g$ generates the elements of $\blue g()$ lazily \\[3mm]
	
	\item $\blue \verb|collect: ('a->seq<'b>) -> seq<'a> -> seq<'b>|$.\\
	\quad	$\blue \verb|collect|\, f\, \,sq$ generates the sequence obtained by\\ 
	\quad appending the sequences: $\blue f(sq_0), f(sq_1), f(sq_2), \ldots$ \\[3mm]
\end{itemize}	

\pause
\bigskip 

The {\blue Seq} library contains functions, e.g. $\blue \verb|collect|$, that are sequence variants of functions from the {\blue List} library. Other examples are:
\begin{itemize}
 	\item $\blue \verb|item: int -> seq<'a> -> 'a|$\\ %[3mm]
 	
 	\item $\blue \verb|head: seq<'a> -> 'a|$\\ %[3mm]
 	
 	\item $\blue \verb|tail: seq<'a> -> seq<'a>|$\\ %[3mm]
 	
 	\item $\blue \verb|append: seq<'a> -> seq<'a> -> seq<'a>|$\\ %[3mm]
 	
 	\item $\blue \verb|take: int -> seq<'a> -> seq<'a>|$\\ %[3mm]
 	
 	\item $\blue \verb|filter: ('a->bool) -> seq<'a> -> seq<'b>|$.\\

\end{itemize}	
	

\end{frame}

\begin{frame}[fragile]
	\frametitle{Example continued}
A \verb!nat! element is computed by demand only:
\begin{alltt}\blue
let nat = Seq.initInfinite idWithPrint;;
\ett{val nat : seq<int>}
\end{alltt}
--- using $\blue \verb|idWithPrint|$ to inspect element generation.

\pause
\bigskip
Demanding an element of the sequence:
\begin{alltt}\blue
Seq.item 4 nat;;
4
val it : int = 4
\end{alltt}


\pause
\bigskip

\begin{center}
	\redbrown Just the 5th element is generated
\end{center}
%\pause
%\medskip

%\begin{itemize}
%\item Lists and Array are specializations of Sequences (in an OO-sense). Hence these libraries have many similarities.
%\end{itemize}

\end{frame}

\begin{frame}[fragile]
\frametitle{Further examples}

A sequence of even natural numbers is easily obtained:
\begin{alltt}\blue
let even = Seq.filter (fun n -> n\%2=0) nat;;
\ett{val even : seq<int>}

Seq.toList(Seq.take 4 even);; \pause
\ett{0}
\ett{1}
\ett{2}
\ett{3}
\ett{4}
\ett{5}
\ett{6}
\ett{val it : int list ={\redbrown [0; 2; 4; 6]}}
\end{alltt}

\pause
\medskip

Demanding the first 4 even numbers requires a computation of the first 7 natural numbers.

\end{frame}



\begin{frame}{Sieve of Eratosthenes}

Greek mathematician (194 -- 176 BC)

\medskip

Computation of prime numbers

\begin{itemize}
\item start with the sequence $\blue 2, 3, 4, 5, 6, ...$\\
select head ($\blue 2$), and remove multiples of $2$ from the
sequence\\
\ \hfill $\redbrown 2$


\item<2-> next sequence $\blue 3, 5, 7, 9, 11, ...$\\
select head ($\blue 3$), and remove multiples of $3$ from the sequence\\
\ \hfill $\redbrown 2, 3$

\item<3-> next sequence $\blue 5, 7, 11, 13, 17, ...$\\
select head ($\blue 5$), and remove multiples of $5$ from the sequence\\
\ \hfill $\redbrown 2, 3, 5$

\item<3-> $\redbrown \vdots$
\end{itemize}

\end{frame}


\begin{frame}[fragile]
\frametitle{Sieve of Eratosthenes in F\# (I)}

Remove multiples of $\blue a$ from sequence $\blue sq$: {\blue
\begin{alltt}
let sift a sq = Seq.filter (fun n -> n % a <> 0) sq;;
\ett{val sift : int -> seq<int> -> seq<int>}
\end{alltt}
}

\pause
\medskip

Select head and remove multiples of head from the tail -- {\redbrown recursively}:

{\blue
\begin{alltt}
let rec sieve sq =
   Seq.delay (fun () ->
                let p = Seq.head sq
                Seq.append
                    (seq [p])
                    (sieve(sift p (Seq.tail sq))));;	
\ett{val sieve : seq<int> -> seq<int>}
\end{alltt}
}

\pause
\bigskip

\begin{itemize}

\item A delay is needed to avoid infinite recursion \hfill \pause {\redbrown Why?}

\end{itemize}

\pause
\begin{center}
\darkgreen Sequence expressions support a more natural formulation 
\end{center}

\end{frame}

\begin{frame}[fragile]
\frametitle{Examples}
The sequence of prime numbers and the $\blue n$'th prime number:
{\blue
\begin{alltt}
let primes = sieve(Seq.initInfinite (fun n -> n+2));;
\ett{val primes : seq<int>}

let nthPrime n = Seq.item n primes;;
\ett{val nthPrime : int -> int}

nthPrime 100;;
\ett{val it : int = 547}
\end{alltt}
}

\pause
\medskip

Re-computation can be avoided by using cached sequences:
{\blue
\begin{alltt}
let primesCached ={\redbrown} Seq.cache primes;;

let nthPrime' n = Seq.item n primesCached;;
\ett{val nthPrime' : int -> int}
\end{alltt}}
Computing the 700'th prime number takes about 4.5s;
a subsequent computation of the 705'th is fast since that computation starts from the 700 prime number
\end{frame}


\begin{frame}[fragile]
\frametitle{Sieve of Eratosthenes using Sequence Expressions}

{\redbrown Sequence expressions} can be used for defining sequences in a step-by-step generation manner.

\pause
\medskip

The sieve of Erastothenes:

{\blue
\begin{alltt}
let rec sieve sq =
  {\redbrown seq \{} let p = Seq.head sq
        {\redbrown yield} p
        {\redbrown yield!} sieve(sift p (Seq.tail sq)){\redbrown \}};;
\ett{val sieve : seq<int> -> seq<int>}
\end{alltt}
}

\pause


\begin{itemize}

\item<3-> By construction lazy -- no need to use \verb!Seq.delay!

\item<4-> $\redbrown \verb!yield!\ x$  adds the element $\blue x$ to the generated sequence

\item<5-> $\redbrown \verb:yield!:\ \mathit{sq}$ adds the sequence $\blue \mathit{sq}$ to the generated sequence

\item<6-> \mbox{$\redbrown \begin{array}{l}
\seqexp_1\\
\seqexp_2
\end{array}
$}
appends the sequences $\blue \seqexp_1$ and
$\blue \seqexp_2$
\end{itemize}
\end{frame}

\begin{frame}[fragile]
\frametitle{Defining {\blue sift} using Sequence Expressions}

The sift function can be defined using an {\redbrown iteration}:
\begin{alltt}\redbrown
for \(pat\) in \(exp\) do \(seqexp\)
\end{alltt}
and a {\redbrown filter}:
\begin{alltt}\redbrown
if \(exp\) then \(seqexp\)
\end{alltt}
\medskip
as follows:
\medskip
\begin{alltt}\blue
let sift a sq = seq \{ for n in sq do
                          if n % a <> 0 then
                                 yield n       \};;
\ett{val sift : int -> seq<int> -> seq<int>}
\end{alltt}

\end{frame}

\begin{frame}[fragile]
\frametitle{Example: Catalogue search (I)}

Extract (recursively) the sequence of all files in a directory:
\begin{alltt}\blue\small
open System.IO ;;

let rec allFiles dir =
  seq \{yield! Directory.GetFiles dir
       yield! Seq.collect allFiles (Directory.GetDirectories dir)\};;
\ett{val allFiles : string -> seq<string>}
\end{alltt}
where $\blue \verb!Seq.collect: ('a -> seq<'c>) -> seq<'a> -> seq<'c>!$ combines a 'map' and 'concatenate' functionality.

\pause
\bigskip

\begin{alltt}\blue\small
Directory.SetCurrentDirectory @"C:{\ttbsl}mrh{\ttbsl}Forskning{\ttbsl}Cambridge{\ttbsl}";;
let files = allFiles ".";;
\ett{val files : seq<string>}

Seq.item 100 files;;
\ett{val it : string = ".{\ttbsl}BOOK{\ttbsl}Satisfiability.fs"}
\end{alltt}
Nothing is computed beyond element 100.

\end{frame}


\begin{frame}[fragile]
\frametitle{Summary}

\begin{itemize}

\item Anonymous functions \texttt{\blue fun () -> $e$}
can be used to {\blue delay the computation} of $\blue e$.

\item<2-> Possibly infinite sequences provide natural and useful abstractions

\item<3-> Functions from the {\blue Seq}-library

\item<4> Sequence expressions -- step-wise sequence generation

\end{itemize}



\bigskip
\pause[5]
The type  {\blue \verb!seq<'a>!} is a synonym for the .NET type {\blue \verb!IEnumerable<'a>!}.

\medskip

Any .NET type that implements this interface can be used as a sequence.
\begin{itemize}
\item Lists and arrays, for example.
\end{itemize}
\end{frame}

\begin{frame}
	%
	%

{\Large\darkgreen Property-based testing}
		\begin{itemize}
			\item Rehearsal of trees
			
			\item Examples with sequences
			
			\item Properties, generators and Shrinkers
			
			\item A look at computation expressions for generators\\
			resembles sequence expressions
			
		\end{itemize}
		
		Consult \url{https://fscheck.github.io/FsCheck/} concerning installation and resources
		%	
		%	
\end{frame}

\begin{frame}[fragile]\frametitle{An example}
	
Consider the expressions:
\begin{tabular}{l}
{\blue let x = y + z + 3}\\ 
{\blue   in x + y + 4} 	
\end{tabular}	

\bigskip

%Suppose {\blue y} is {\blue 1} and {\blue z} is {\blue 2}, that is {\blue y + z + 3} is {\blue 6}. 
The following expressions have the same value when {\blue y = 1} and {\blue z = 2}:
\begin{alltt}\blue
6 + y + 4                    y + z + 3 + y + 4   	\darkgreen\pause
substitute 6 for x           substitute y + z + 3 for x 
in x + y + 4                 in x + y + 4
\end{alltt}

\pause	
\bigskip
	
Suppose we have functions:
\begin{itemize}
\item $\blue \verb|eval: E->Env->int|$ that evaluates $\blue e$ in environment $\blue m$
\item $\blue \verb|subst: string->E->E->E|$ that performs substitutions  	
\end{itemize}

\bigskip
		
The property \hfill {\redbrown substitution preserves meaning}
\begin{alltt}\blue 
let substOK1(x, e1, e2, m) = // {\darkgreen "let x = e1 in e2 , m"}
   let v1 = eval e1 m          
   let e2' = subst x (C v1) e2 
   let e2'' = subst x e1 e2     
   eval e2'' m = eval e2' m;; 	
\end{alltt}
should hold for all expressions and environments that {\redbrown fit} together.

\end{frame}

\begin{frame}[fragile]\frametitle{Scenarios for substitution}

Remember: $\blue \verb|subst|\ x\ e_1\, e_2$ substitutes $\blue e_1$ for $\blue x$ in $\blue e_2$
 
\bigskip
 
Example 1:
\begin{alltt}\blue 
let x = y+z             "subst x (y+z) (x+let x=6 in x)" 
in x+let x=6 in x         		
\end{alltt}
	
\begin{itemize}
\item Only {\blue free occurrences} of {\blue x} in $\blue e_2$ should be substituted  
\end{itemize}

\begin{alltt}\blue 
"subst x (y+z) (x+let x=6 in x)" = "y+z + let x=6 in x)"
\end{alltt}

\bigskip
\pause

Example 2:
\begin{alltt}\blue 
let x=y                   "subst x y (let y=6 in x+y)" 
in let y=6 in x+y         		
\end{alltt}

\begin{itemize}
\item Avoid that a free variable of $\blue e_1$ is captured by a let-binding in $\blue e_2$. \hfill Rename bound variables.  
\end{itemize}

\begin{alltt}\blue 
"subst x y (let y=6 in x+y)" = "let y1=6 in y+y1"
\end{alltt}
where {\blue \verb|y1|} is a "new" variable 
\end{frame}

\begin{frame}\frametitle{Test and Verification}
	
	Tests:
	\begin{itemize}
		\item easy to write
		\item can reveal errors
		\item show correctness of a very limited number of concrete cases
	\end{itemize}
	\ \hfill low level of abstraction  
	
	\vspace{3cm}
	\pause
	
	Verification:
	\begin{itemize}
		\item complicated to complete
		\item provide guarantees
		\item focus of correctness properties
	\end{itemize}
	\ \hfill high level of abstraction 
	
\end{frame}

\begin{frame}\frametitle{Between Test and Verification}
	
	Tests: ...\\[.4cm]
	
	\vfill
	Property-based testing
	\begin{itemize}
		\item<1-> focus on properties of programs \hfill enhances understanding
		\item<2-> construction of programs
		\item<3-> a randomly generated sample covers edge cases and typical situations 
		\item<4-> Short counter-examples are useful
		\item<5-> gives high confidence
		\item<6-> limited effort
	\end{itemize}
	\ \hfill high level of abstraction \\[.4cm]
	
	
	
	\vfill
	\onslide<1->{ 
		Verification: ... }
\end{frame}


\begin{frame}[fragile]\frametitle{Correctness properties are Boolean-valued functions}
	
	A {\redbrown property} is a Boolean-valued function with type 
	\[\darkgreen \tau_1 \to \cdots \to \tau_n \to \verb-bool-\]
	
	\pause
	Append is associative:
	\begin{alltt}\blue 
		let appendAssocProp xs ys zs =
		xs @ (ys @ zs) = (xs @ ys) @ zs
		\ett{'a list -> 'a list -> 'a list -> bool when 'a : equality}     
	\end{alltt}
	
	\pause
	\medskip
	
	The associative law can be tested on some examples:
	\begin{alltt}\blue 	
		let test = appendAssocProp [1;2] [3;4;5] [6;7;8;9];;
	\end{alltt}
	
	\begin{itemize}
		\item But it requires discipline to come out with a suitable test suite
	\end{itemize}
	
	\bigskip
	\pause
	
	How can we get confidence in tests that should validate that
	\begin{alltt}\blue
		appendAssocProp xs ys zs
	\end{alltt}
	holds for all lists $\blue xs$, $\blue ys$ and $\blue zs$?
	
\end{frame}

\begin{frame}[fragile]\frametitle{Property-based testing}
	
	Given 
	\begin{itemize}
		\item property $\blue F$ with type $\darkgreen \tau_1 \to \cdots \to \tau_n \to \verb|bool|$ 
		\item with input variable $\blue x_1, ..., x_n$
	\end{itemize}
	the library FsCheck supports
	\begin{itemize}
		\item<2-> generation of random values for $\blue x_1, ..., x_n$
		\item<3-> test whether $\blue F$ holds for all sample values
		\item<4-> presentation of a short counter-example when $F$ is falsified 
	\end{itemize}
	where $\blue x_i$ can have any {\darkgreen monomorphic type}.
	
	\pause
	\medskip  
	
	\begin{alltt}\blue 
		open FsCheck
		
		let appendAssocProp (xs:{\darkgreen int list}) ys zs = 
		xs @ (ys @ zs) = (xs @ ys) @ zs;;
		
		\redbrown{Check.Quick} appendAssocProp;;
		\ett{Ok, passed 100 tests.}
		\ett{val it : unit = ()}
	\end{alltt}
\end{frame}


\begin{frame}[fragile]\frametitle{PBT of substitution}
	
\begin{alltt}\blue 

#r "nuget: FsCheck";; open FsCheck;;
...
let substOK1(x, e1, e2, m) = // {\darkgreen "let x = e1 in e2 , m"}
   let v1 = eval e1 m          
   let e2' = subst x (C v1) e2 
   let e2'' = subst x e1 e2     
   eval e2'' m = eval e2' m;; 	

Check.Quick substOK1;;
(* ...
Original:
(null, C 0, V "", map [])
with exception:
System.Collections.Generic.KeyNotFoundException: The given key was not present in the dictionary.
... *)
\end{alltt}

\pause
\medskip
	
\begin{itemize}
\item Necessary: Values for $\blue x, e1, e2, m$ must fit together

\item Convenient: ``natural'' variable names 
\end{itemize}
\pause 

\medskip	
\begin{center}
		\darkgreen Custom generators are needed
	\end{center}

\end{frame}

\begin{frame}[fragile]\frametitle{The types {\blue \texttt{Arbitrary<'a>}} and {\blue \texttt{Gen<'a>}}}
	
	An  {\blue \verb|Arbitrary<'a>|} instance comprises a 
	\begin{itemize}
		\item a generator $\blue g$ of type {\blue \verb|Gen<'a>|} and
		\item a shrinker $\blue f$ of type {\blue \verb|'a -> seq<'a>|}
	\end{itemize}
	to be used when testing properties.
	
	\bigskip
	
	Good default implementation exists for most types. 
	
	\bigskip
	\pause
	
	A generator $\blue g: \verb|Gen<'a>|$ can be considered 
	\begin{itemize}
		\item a computation of a random value of type {\blue \verb|'a|}
	\end{itemize}
	
	\bigskip
	\pause
	
	A shrinker $\blue f$ is a function that, for a given counter example, returns a sequence of smaller/simpler values.
	
	
	\pause
	\bigskip
	
	The module {\blue Gen} can be considered a library for forming new generators
	
	\pause
	\bigskip
	
	New generators can also be formed using F\#'s computation expressions \\
	\qquad {\blue \verb|Gen<'a>|} is a monad using Haskell terminology 
	
\end{frame}

\begin{frame}[fragile]\frametitle{Selected pre-defined generators}
	
	\begin{alltt}\blue
		Gen.constant: 'a -> Gen<'a>	
		
		Gen.oneof: seq<Gen<'a>> -> Gen<'a>
		
		Gen.map2: ('a->'b->'c) -> Gen<'a> -> Gen<'b> -> Gen<'c>	
		
		Gen.sized: (int -> Gen<'a>) -> Gen<'a>
	\end{alltt}
	
	
Some examples
\begin{alltt}
> let g10 = seq \{for i in 1 ..10 do 
	                  yield Gen.constant i\};;
val g10: Gen<int> seq

> let g = Gen.oneof g10;;
val g: Gen<int> = Gen <fun:Bind@88>

> Gen.sample 1 5 g;;
val it: int list = [9; 3; 9; 3; 4]
> Gen.sample 1 5 g;;
val it: int list = [2; 7; 5; 4; 7]

> Gen.sample 1 5 g;;
val it: int list = [8; 2; 8; 2; 7]
\end{alltt}		
	
	
%	\begin{itemize}
%		\item Self-explaining using names and types  
%	\end{itemize}
	
\end{frame}

\begin{frame}[fragile]\frametitle{Generators for substitution property}

Two mail generators	
\begin{alltt}\blue
myEnvGen: string list -> Gen<Env>

myEGen: string list -> Gen<E> 
\end{alltt}
where
\begin{itemize}
\item $\blue\verb|myEGen|\ vs$ generates an expression where only variables in $\blue vs$ can occur free.  
	
\item 	$\blue\verb|myEnvGen|\ vs$ generates an environment for variables $\blue vs$
\end{itemize}

\bigskip
\pause

Putting the pieces together:
\begin{alltt}\blue
type Subst = string * E * E * Env  

mySubstGen: Gen<Subst>
\end{alltt}
where $\blue \verb|mySubstGen|$ generates a tuple $\blue (x,e_1,e_2,m)$ satisfying   \[\blue 
dom\ m = free\ e_1 \cup free\ e_2
\]

\pause

Property $\blue\verb|substOK1((x,e1,e2,m):Subst)|$ can now be checked.

\medskip

\begin{center}\darkgreen 
Let us have a look at the programs
\end{center}
\end{frame}

\begin{frame}[fragile]\frametitle{Further properties}
	

\begin{alltt}\blue


\end{alltt}
	where
	\begin{itemize}
		\item $\blue\verb|myEGen|\ vs$ generates an expression where only variables in $\blue vs$ can occur free.  
		
		\item 	$\blue\verb|myEnvGen|\ vs$ generates an environment for variables $\blue vs$
	\end{itemize}
	
	\bigskip
	\pause
	
	Putting the pieces together:
	\begin{alltt}\blue
		type Subst = string * E * E * Env  
		
		mySubstGen: Gen<Subst>
	\end{alltt}
	where $\blue \verb|mySubstGen|$ generates a tuple $\blue (x,e_1,e_2,m)$ satisfying   \[\blue 
	dom\ m = free\ e_1 \cup free\ e_2
	\]
	
	\pause
	
	Property $\blue\verb|substOK1((x,e1,e2,m):Subst)|$ can now be checked.
	
	\medskip
	
	\begin{center}\darkgreen 
		Let us have a look at the programs
	\end{center}
\end{frame}

\begin{frame}[fragile]\frametitle{Further properties}
	
\begin{alltt}\blue 
let rec elimLet e = 
   match e with
   | Add(e1,e2)   -> Add(elimLet e1, elimLet e2)
   | Let(x,e1,e2) -> elimLet (subst x e1 e2)
   | e            -> e;;

let elimLetOK1((e,m): EwithEnv) = 
       eval e m = eval (elimLet e) m;; 

Check.Quick elimLetOK1;;		

\pause
// substEnv: Env -> E -> E 
let substEnv m e = 
   Map.foldBack subst (Map.map (fun _ n -> C n) m) e;;

let substOK2((e,m): EwithEnv) = 
   eval e m = eval (substEnv m e) Map.empty;;

Check.Quick substOK2;;
\end{alltt}
	
	
\end{frame}

\begin{frame}


PBT is a useful technique for software validation

\bigskip 

Fundamental properties of programs can be validated \\
--- provided they can be implemented. 

\bigskip
	
Libraries supporting PBT exist for many languages:
\url{https://en.wikipedia.org/wiki/QuickCheck}.


\end{frame}


\end{document}

