\documentclass[12pt]{beamer}
%include polycode.fmt 

\usepackage{alltt}
\usepackage{pgf}
\usepackage{tikz}
\usepackage{representations}
\usepackage{black}

\title{Testing a generic term rewrite framework}
\author{Chris Eidhof, Sebastiaan Visser}
\date{\today}

%format |-      = "\vdash"
%format Not     = "\neg"
%format :&&:    = "\land"
%format :||:    = "\lor"
%format :->:    = "\to"
%format :<->:   = "\leftrightarrow"
%format T       = "\texttt{T}"
%format F       = "\texttt{F}"
%format :~>:    = "\rightsquigarrow"
%format :+:     = "\nearrow"
%format <*>   = "\ \langle*\rangle\ "
%format <$>   = "\ \langle\$\rangle\ "

\begin{document}

\frame{
  \titlepage
  \begin{figure}
    \includegraphics[width=5cm]{duck}
  \end{figure}
}

\section{Introduction}

% -----------------------------------------------------------------------------
\frame{

\frametitle{Expression data type}

Suppose writing an interpreter for logical expressions:

\begin{columns}[c] 

\column{1.5in} 
\begin{code}
data Logic =
     Var String
  |  Logic :<->:  Logic
  |  Logic :->:   Logic
  |  Logic :&&:   Logic
  |  Logic :||:   Logic
  |  Not Logic
  |  T
  |  F
\end{code}

\pause

\column{2.8in} 

\hspace{0.3in}So you can write:

\begin{code}
(Var "x" :->: F) :&&: (Not T :||: Var "y")

(T :<->: F) :->: (F :->: Var "x") :&&: (T :->: F)

(F :||: T) :->: (T :||: F)
\end{code}

\hspace{0.3in}And evaluate:

\begin{code}
eval (T :||: F) :~>: T
\end{code}

\end{columns} 

}

% -----------------------------------------------------------------------------

\frame{

\frametitle{Express generic rewrite rules}

Using the generic rewriting library you can write:

\type{
\begin{code}
notNot, deMorganOr, deMorganAnd  :: Rule Expr
\end{code}
}

\begin{code}
notNot       {-"\uncover<2->{"-}x     ={-"}"-} Not (Not x)     |- x

deMorganOr   {-"\uncover<2->{"-}x y   ={-"}"-} Not (x :||: y)  |- Not x :&&: Not y

deMorganAnd  {-"\uncover<2->{"-}x y   ={-"}"-} Not (x :&&: y)  |- Not x :||: Not y
\end{code}

}

% -----------------------------------------------------------------------------

\frame{

\frametitle{Using the generic rewrite function}

\begin{code}
{-"\type{"-}rewriteM :: PFView a => Rule a -> a -> Maybe a{-"}"-}
rewriteM = ...
\end{code}

\begin{code}
rewriteM deMorganAnd (Not (T :&&: F)) 
    {-"\uncover<2->{"-}  :~>: (Not T :||: Not F) {-"}"-}
\end{code}

}

% -----------------------------------------------------------------------------

\frame[label=logicinst]{

\frametitle{Generics by fixpoint view}

\tiny
\type{
\begin{code}
{-"\regular{"-}instance{-"}"-} PFView Logic {-"\regular{"-}where{-"}"-}
  {-"\regular{"-}type{-"}"-} PF Logic {-"\ \regular{"-} ={-"}"-}
    C (Sum  (Sum  (Sum (Con (K String))    (Con (Prod Id Id)))
                  (Sum (Con (Prod Id Id))  (Con (Prod Id Id))))
            (Sum  (Sum (Con (Prod Id Id))  (Con Id))
                  (Sum (Con Unit)          (Con Unit))))
\end{code} }
\begin{code}
  from (Var x)       = C (Inl  (Inl  (Inl  (Co "Var"  (K x)))))
  from (p :<->:  q)  = C (Inl  (Inl  (Inr  (Con "<->"  (Prod (Id p) (Id q))))))
  from (p :->:   q)  = C (Inl  (Inr  (Inl  (Con "->"   (Prod (Id p) (Id q))))))
  from (p :&&:   q)  = C (Inl  (Inr  (Inr  (Con "&&"   (Prod (Id p) (Id q))))))
  from (p :||:   q)  = C (Inr  (Inl  (Inl  (Con "||"   (Prod (Id p) (Id q))))))
  from (Not p)       = C (Inr  (Inl  (Inr  (Con "Not"  (Id p)))))
  from T             = C (Inr  (Inr  (Inl  (Con "T"    Unit))))
  from F             = C (Inr  (Inr  (Inr  (Con "F"    Unit))))

  to (C (Inl  (Inl  (Inl  (Con _ (K x))))))                 = Var x
  to (C (Inl  (Inl  (Inr  (Con _ (Prod (Id p) (Id q)))))))  = p :<->:  q
  to (C (Inl  (Inr  (Inl  (Con _ (Prod (Id p) (Id q)))))))  = p :->:   q
  to (C (Inl  (Inr  (Inr  (Con _ (Prod (Id p) (Id q)))))))  = p :&&:   q
  to (C (Inr  (Inl  (Inl  (Con _ (Prod (Id p) (Id q)))))))  = p :||:   q
  to (C (Inr  (Inl  (Inr  (Con _ (Id p))))))                = Not p
  to (C (Inr  (Inr  (Inr  (Con _ Unit)))))                  = T
  to (C (Inr  (Inr  (Inl  (Con _ Unit)))))                  = F
\end{code}

}

% -----------------------------------------------------------------------------

\frame{

\frametitle{Possible problems}

Several properties of the framework need special attention:

\begin{itemize}
\item Correctness of the rewriting algorithm.
\item Soundness + completeness of embedding projection pairs.
\item Semantic soundness of rewriting rules.
\end{itemize}

}

% -----------------------------------------------------------------------------

\frame{

\frametitle{Our solution}

\begin{itemize}
\item Automated testing using QuickCheck properties.
\item More or less one property for each of the possible problems.
\pause
\item Using generically generated instances.
\end{itemize}

\pause
\type{
\begin{code}
garbitrary :: PFView a => Int -> Gen a
\end{code}
}

}

% -----------------------------------------------------------------------------

\frame{

\frametitle{Rewrite property}

\begin{code}
{-"\type{"-}prop_rewrite :: PFView a => Rule a -> a -> Bool{-"}"-}
prop_rewrite rule a =
  rewriteM rule (lhsR $ rule a) == Just (rhsR $ rule a)
\end{code}

\pause

\begin{code}
quickCheck (prop_rewrite deMorganOr)
\end{code}
\hspace{0.33in}\texttt{OK, passed 100 tests.}


%\begin{columns}[c]
%\column{3.0in} 
%\begin{enumerate}
%\item Get a rule and a arbitrary experssion.
%\item Plug the expression into both side of the rule, filling up all meta-variables.
%\item Get the \emph{lhs} of the rule.
%\item Rewrite \emph{lhs} using the rule.
%\item Check equality with \emph{rhs} hand side.
%\end{enumerate}
%\end{columns}

}

% -----------------------------------------------------------------------------

\frame{

\frametitle{View soundness}

Soundness:
\begin{code}
{-"\type{"-}prop_fromTo_Id :: PFView a => PF a -> Bool{-"}"-}
prop_fromTo_Id a = (from . to) a == a
\end{code}

\pause
Completeness?
\begin{code}
{-"\type{"-}prop_toFrom_Id :: PFView a => a -> Bool{-"}"-}
prop_toFrom_Id a = (to . from) a == a
\end{code}

\pause
No! Test depends on result!
}

\frame{

\frametitle{View soundness example}

\begin{code}
quickCheck (prop_fromTo_Id :: PF Logic -> Bool)
\end{code}
\pause
\hspace{0.33in}\texttt{
Falsifiable, after 6 tests:
...
}

}

\againframe{logicinst}


% -----------------------------------------------------------------------------

\frame{

\frametitle{Semantic soundness}

Does a rule preserve the domain specific semantics?

\begin{code}
{-"\type{"-}prop_semantics :: PFView a =>{-"}"-}
  {-"\type{"-}(a -> a -> Bool) -> Rule a -> a -> Bool{-"}"-}
prop_semantics eq rule a = let lhs = lhsR (rule a) in
  maybe False (eq lhs) (rewriteM rule lhs)
\end{code}

\pause
\begin{code}
{-"\type{"-}prop_logicSemantics :: Rule Logic -> Logic -> Bool{-"}"-}
prop_logicSemantics = prop_semantics eqLogic
  where eqLogic a b = eval a == eval b
\end{code}

}

\frame{

\frametitle{Semantic soundness example}

\begin{code}
quickCheck (prop_logicSemantics deMorganAnd)
\end{code}
\hspace{0.33in}\texttt{OK, passed 100 tests.}
\begin{code}
\end{code}

\pause
\begin{code}
quickCheck (prop_logicSemantics (\x -> x |- T))
\end{code}
\hspace{0.33in}\texttt{
Falsifiable, after 1 tests: F
}


}

% -----------------------------------------------------------------------------
% Time: 20 minutes
\section{Introduction} %             5 min
  \subsection{Rewriting}
  % Tell about the rewriting rules, they exist for every datatype, give
  % examples.
        
  % - assume we have logical expression data type
  % - 


  \subsection{Checking validity}
  % Three problems:
  %  - is the rewriting-algorithm correct?
  %  - is the view correct (sound and complete)?
  %  - are the rules correct? (i.e.: is the expression equivalent after
  %    transformation?)

  \subsection{Our solution}
  % - Automatic testing.
  \subsection{How can we do this}
  % - QuickCheck properties with generated instances.

\section{Technical details} %             12 min

  \subsection{Calculating fixpoints} % 3 min
  \frame{
    \frametitle{Tree fixpoints}
    \begin{spec}
    data Tree a = Leaf a | Branch (Tree a) (Tree a)
    \end{spec}
    \pause
    \begin{spec}
    instance {-"\type{"-}PFView (Tree a){-"}"-} where

      type {-"\type{"-}PF (Tree a){-"}"-} = {-"\type{"-}Sum (K a) (Prod Id Id) {-"}"-}
      ...
      \end{spec}
    \pause
    \treefixedpoints
  }
  \frame
  {
    \frametitle{Direction fixpoints}
    \begin{columns}[c]
    \column{2.3in} 
    \begin{spec}
    data Direction =
         North
      |  East
      |  South
      |  West
      |  Direction :+: Direction
    \end{spec}
    \pause
    \type{
    \begin{spec}
    {-"\regular{"-}instance {-"\type{"-}PFView Direction{-"}"-} where{-"}"-}
      {-"\regular{"-}type{-"}"-} PF Direction {-"\ \regular{"-} ={-"}"-}
            Sum  Unit 
                 (Sum  Unit 
                       (Sum  Unit 
                             (Sum Unit (Prod Id Id))))
    \end{spec}
    }
    \pause
    \column{1.7in} 
    \directionfixedpoints
    \end{columns}
  }
  \frame{
    \frametitle{Our solution: gfixpoints}
    \begin{spec}
    class GFixpoints f where
      gfixpoints' :: {-"\type{"-}f a -> Tree Int{-"}"-}
    \end{spec}
    \pause
    \begin{spec}
    gfixpoints (undefined :: {-"\type{"-}Direction{-"}"-})
    :~>: Branch   (Leaf 0) 
                  (Branch  (Leaf 0) 
                           (Branch  (Leaf 0) 
                                    (Branch  (Leaf 0) 
                                             (Leaf 2))))

    \end{spec}
  }
  \subsection{QuickCheck properties} % 3 min

  % - rewrite property
  %   test whether the algorithm is correct
  %   plug generated expression in rule, pull out, rewrite and eq

  % - view soundness
  %   what does "soundness and completeness" mean in this context
  %   we check for soundness of views
  %   completeness not possible within this framework
  %   views can be generated in the future, this gives us both soundness and completeness for free

  % - semantic soundness of rules
  %   using custom evaluator
  %   first show prop:semantic, then example of regular rule and buggy rule


  \subsection{QuickCheck instances} % 6 min
  % Give our implementation of GFixPoint
  % Give an example instance of List, Tree.
  % Give a formal definition of these instances (number of constructors, fixed
  % points)
  \frame{
    \frametitle{Arbitrary instances: Lists}

    \begin{spec}
     instance {-"\type{"-}Arbitrary a => Arbitrary [a]{-"}"-} where
       arbitrary = frequency
         [  (1,  pure  [])
         ,  (2,  (:) <$> arbitrary <*> arbitrary) 
         ]
    \end{spec}
  }
  \frame{
    \frametitle{Arbitrary instances: Trees}
    \begin{spec}
    data Tree a = Leaf a | Branch (Tree a) (Tree a)
    \end{spec}
    \begin{spec}
     instance {-"\type{"-}Arbitrary a => Arbitrary (Tree a){-"}"-} where
       arbitrary  =  sized arbTree
       arbTree 0  =  Leaf <$> arbitrary
       arbTree n  =  frequency
         [  (1  , Leaf    <$> arbitrary  )
         ,  (3  , Branch  <$> arbTree    (n `div` 2) 
                          <*> arbTree    (n `div` 2)) ]
    \end{spec}
  }
  \frame{
    \frametitle{Arbitrary instances: generically}
    \begin{spec}
    arbitary           = sized arbitary'
    arbitrary'    0    = oneof nonRecursiveValues
    arbitrary'    n    = frequency [(freq C, return C) ]
      where freq  C    = 1 + length (fixpoints C)
    \end{spec}
  }
  \subsection{GArbitrary}
  % TODO chris: f -> freq, s -> size of sz
  \frame{
    \frametitle{GArbitrary: specification}
    \begin{spec}
     class GArbitrary f where
       garbitrary'   :: {-"\type{"-}ArbParams a -> Int -> Gen (f a){-"}"-}
    \end{spec}
    \begin{spec}
     data ArbParams a = AP 
       {  rec      :: {-"\type{"-}ArbParams a -> Int -> Gen a{-"}"-}
       ,  divisor  :: {-"\type{"-}Int{-"}"-}
       }
     
    \end{spec}
  }

  % Give implementation of GArbitrary (for interesting cases)
  \frame{
    \frametitle{GArbitrary: Unit}
    \begin{spec}
    instance GArbitrary Unit where
      garbitrary' _ _ = pure Unit
    \end{spec}
  }
  \frame{
    \frametitle{GArbitrary: Prod}
    \begin{spec}
    instance (   GArbitrary f, GArbitrary g) 
             =>  GArbitrary (Prod f g) where
      garbitrary' p s = Prod <$> garbitrary' p s <*> garbitrary' p s
    \end{spec}
  }
  \frame{
    \frametitle{GArbitrary: Sum}
    This is where we choose:
    \begin{spec}
garbitrary' params size  =  frequency 
  [(  fr fpl  ,  Inl   <$> garbitrary' params {divisor = sum fpl  } size)
  ,(  fr fpr  ,  Inr   <$> garbitrary' params {divisor = sum fpr  } size)
  ]
  where  
    (Node fpl fpr)  =   gfixpoints' (undefined :: {-"\type{"-}Sum f g a{-"}"-})
    fr  ::  {-"\type{"-}Tree Int -> Int{-"}"-}
    fr  =   sum . fmap (freq size)
    \end{spec}
    \pause
    \begin{spec}
     freq  0  0  =  1 
     freq  0  _  =  0
     freq  _  x  =  x + 1
    \end{spec}
  }

\section{Conclusion} %             3 min

\frame{
  \frametitle{Summary}
  \begin{itemize}
    \item We have tested several properties of rewriting
    \item We have seen |gfixpoints|
    \item We have seen |garbitrary|
  \end{itemize}
}
\frame{
  \frametitle{Conclusion}
  \begin{itemize}
    \item We detect mistakes in views
    \item We detect mistakes in rules
    \item We detect mistakes in the rewriting algorithm
    \item Automated testing of properties is the way to go
  \end{itemize}
}

% TODO: chris types geel
\end{document}