A testing suite for Exercise 5: Agda of AFP 2022 at UU

TextExer-cad0p.agda

module TestExer-cad0p where

import Exercise
open Exercise

--- PREREQUISITES -----

-- You need to add this line at the top of Exercise.agda :

-- {-# OPTIONS --allow-unsolved-metas #-}

-- for this module to be able to import the other module.

-----------------------


------- TO COMPLETE ------

-- what is the function to add vectors?
_+v_ : {n : Nat} -> Vec Nat n -> Vec Nat n -> Vec Nat n
_+v_ = vadd

-- what is the function to add matrices?
_+m_ : {n m : Nat} -> Matrix Nat m n -> Matrix Nat m n -> Matrix Nat m n
_+m_ = madd


--------------------------


------ TESTING FUNCTIONS ------

-- we need to define another function to create a vector of 
-- size n with all 0s
zeroVec : (n : Nat) -> Vec Nat n
zeroVec Zero = Nil
zeroVec (Succ n) = Cons 0 (zeroVec n)

-- a function that maps i to n - i
-- this evaluates to Zero if n < i
compNat : Nat -> Nat -> Nat
compNat (Succ n) (Succ i) = compNat n i
compNat n i = n


-- creates a vector of size n with a 1 in position i, 0 < i <= n
-- idVec {1} 1 == Cons 1 Nil
idVec : {n : Nat} -> Nat -> Maybe (Vec Nat n)
idVec {Zero} Zero = Just Nil
idVec {Zero} (Succ i) = Nothing
idVec {Succ n} Zero = Nothing
idVec {Succ n} 1 = Just (Cons 1 (zeroVec n))
idVec {Succ n} (Succ i) with idVec {n} i
... | Just x = Just (Cons 0 x)
... | Nothing = Nothing


-- needed for Ex 1 <*> testing
vmapf : {a b : Set} {n : Nat} -> (a -> b) -> Vec (a -> b) n
vmapf {a} {b} {Zero} f = Nil
vmapf {a} {b} {Succ n} f = Cons f (vmapf f)


-- so I'm defining a function that simply returns the vector
-- for testing of the compiler
vreturn : {a : Set} {n : Nat} -> Vec a n -> Vec a n
vreturn v = v


----------------------------

----- TESTING OF TESTING FUNCTIONS -----

testZeroVec : zeroVec Zero == Nil
testZeroVec = Refl


testZeroVec2 : zeroVec 2 == Cons Zero (Cons Zero Nil)
testZeroVec2 = Refl

testIdVec : idVec {0} 0 == Just Nil
testIdVec = Refl

testIdVec1 : idVec {1} 1 == Just (Cons 1 Nil)
testIdVec1 = Refl

testIdVec2₀ : idVec {2} 0 == Nothing
testIdVec2₀ = Refl

testIdVec2₁ : idVec {2} 1 == Just (Cons 1 (Cons Zero Nil))
testIdVec2₁ = Refl

testIdVec2₂ : idVec {2} 2 == Just (Cons Zero (Cons 1 Nil))
testIdVec2₂ = Refl

testIdVec2₃ : idVec {2} 3 == Nothing
testIdVec2₃ = Refl


testCompNat2₀ : compNat 2 0 == 2
testCompNat2₀ = Refl

testCompNat2₁ : compNat 2 1 == 1
testCompNat2₁ = Refl

testCompNat2₂ : compNat 2 2 == 0
testCompNat2₂ = Refl

----------------------------------

----------------------
----- Exercise 1 -----
----------------------

testPure : pure {1} {Bool} True == {! Cons True Nil !}
testPure = Refl

testPure2 : pure {2} {Bool} True == {! Cons True (Cons True Nil) !}
testPure2 = Refl

test-<*> : (vmapf (λ b -> False) <*> Cons True (Cons False Nil)) == 
    {! Cons False (Cons False Nil) !}
test-<*> = Refl

testVmap : {a b : Set} {n : Nat} {v : Vec a n} {f : (a -> b)} ->
    ((vmapf f) <*> v) == vmap f v
testVmap {a} {b} {.0} {Nil} {f} = {! Refl !}
testVmap {a} {b} {Succ n} {Cons x v} {f} = 
    let ih = {! testVmap {a} {b} {n} {v} {f} !} in {! cong (Cons (f x)) testVmap !}

test-+v : (Cons 1 (Cons 2 Nil) +v Cons 3 (Cons 4 Nil)) == {! Cons 4 (Cons 6 Nil) !}
test-+v = Refl



----------------------
----- Exercise 2 -----
----------------------

testMatrix : Matrix Bool 1 1
testMatrix = Cons (Cons True Nil) Nil

testMatrixEmpty : Matrix Bool 0 0
testMatrixEmpty = Nil

matrix3₃ : Matrix Nat 3 3
matrix3₃ = 
    Cons (Cons 1 (Cons 2 (Cons 3 Nil)))(
    Cons (Cons 4 (Cons 5 (Cons 6 Nil)))(
    Cons (Cons 7 (Cons 8 (Cons 9 Nil))) 
    Nil))

matrix3₂ : Matrix Nat 3 2
matrix3₂ = 
    Cons (Cons 1 (Cons 2 (Cons 3 Nil)))(
    Cons (Cons 4 (Cons 5 (Cons 6 Nil))) 
    Nil)


test-+m : (matrix3₂ +m matrix3₂) == 
    {! Cons (Cons 2 (Cons 4 (Cons 6 Nil))) (
    Cons (Cons 8 (Cons 10 (Cons 12 Nil))) 
    Nil) !}
test-+m = Refl

testIdMatrix₀ : idMatrix {0} == {! Nil !}
testIdMatrix₀ = Refl

testIdMatrix₁ : idMatrix {1} == {! Cons (Cons 1 Nil) Nil !}
testIdMatrix₁ = Refl


testIdMatrix₂ : idMatrix {2} == 
    {! Cons (Cons 1 (Cons Zero Nil)) (
    Cons (Cons Zero (Cons 1 Nil)) 
    Nil) !}
testIdMatrix₂ = Refl

testIdMatrix₃ : idMatrix {3} == 
    {! Cons (Cons 1 (Cons Zero (Cons Zero Nil)))(
    Cons (Cons Zero (Cons 1 (Cons Zero Nil)))(
    Cons (Cons Zero (Cons Zero (Cons 1 Nil))) 
    Nil)) !}
testIdMatrix₃ = Refl



testTranspose3₃ : transpose matrix3₃ == 
    {! Cons (Cons 1 (Cons 4 (Cons 7 Nil))) (
    Cons (Cons 2 (Cons 5 (Cons 8 Nil))) (
    Cons (Cons 3 (Cons 6 (Cons 9 Nil))) 
    Nil)) !}
testTranspose3₃ = Refl

-- test that it works correctly on non-square matrices
testTranspose3₂ : transpose matrix3₂ == 
    {! Cons (Cons 1 (Cons 4 Nil)) (
    Cons (Cons 2 (Cons 5 Nil)) (
    Cons (Cons 3 (Cons 6 Nil)) 
    Nil)) !}
testTranspose3₂ = Refl


----------------------
----- Exercise 3 -----
----------------------



testPlan1 : plan {1} == {! Cons Fz Nil !}
testPlan1 = Refl

testPlan2 : plan {2} == {! Cons Fz (Cons (Fs Fz) Nil) !}
testPlan2 = Refl

testForget : forget {4} (Fs (Fs Fz)) == {! 2 !}
testForget = Refl

-- the test for embed is in the Exercise
-- it's called 'correct'
-- correct : {n : Nat} -> (i : Fin n) -> forget i == forget (embed i)


----------------------
----- Exercise 4 -----
----------------------


testCmp-₀≡₀ : cmp Zero Zero == {! Equal !}
testCmp-₀≡₀ = Refl

testCmp-₀<₁ : cmp Zero 1 == {! LessThan 1 !}
testCmp-₀<₁ = Refl

testCmp-₀<₃ : cmp Zero 3 == {! LessThan 3 !}
testCmp-₀<₃ = Refl

testCmp-₁>₀ : cmp 1 Zero == {! GreaterThan 1 !}
testCmp-₁>₀ = Refl

testCmp-₃>₀ : cmp 3 Zero == {! GreaterThan 3 !}
testCmp-₃>₀ = Refl


-- now with the recursive case
testCmp-₅≡₅ : cmp 5 5 == {! Equal !}
testCmp-₅≡₅ = Refl

testCmp-₅<₆ : cmp 5 6 == {! LessThan 1 !}
testCmp-₅<₆ = Refl

testCmp-₅<₈ : cmp 5 8 == {! LessThan 3 !}
testCmp-₅<₈ = Refl

testCmp-₆>₅ : cmp 6 5 == {! GreaterThan 1 !}
testCmp-₆>₅ = Refl

testCmp-₈>₅ : cmp 8 5 == {! GreaterThan 3 !}
testCmp-₈>₅ = Refl

-- now test difference

testDifference-|0-0| : difference Zero Zero == {! Zero !}
testDifference-|0-0| = Refl

testDifference-|0-1| : difference Zero 1 == {! 1 !}
testDifference-|0-1| = Refl

testDifference-|1-0| : difference 1 Zero == {! 1 !}
testDifference-|1-0| = Refl

testDifference-|0-5| : difference Zero 5 == {! 5 !}
testDifference-|0-5| = Refl

testDifference-|5-0| : difference 5 Zero == {! 5 !}
testDifference-|5-0| = Refl

testDifference-|5-5| : difference 5 5 == {! Zero !}
testDifference-|5-5| = Refl

testDifference-|8-5| : difference 8 5 == {! 3 !}
testDifference-|8-5| = Refl

testDifference-|5-8| : difference 5 8 == {! 3 !}
testDifference-|5-8| = Refl


----------------------
----- Exercise 5 -----
----------------------

-- check the exercise



----------------------
----- Exercise 6 -----
----------------------

-- check the exercise


----------------------
----- Exercise 7 -----
----------------------

-- check the exercise


----------------------
----- Exercise 8 -----
----------------------

-- check the exercise


----------------------
----- Exercise 9 -----
----------------------

-- in order to understand what is meant by the correctness
-- of the compiler, I will write here some tests

-- n should be equal to m
-- n is the compiler, m is how a correct compiler should behave

testCompilerValₙ : exec (compile (Val 1)) Nil == {! Cons 1 Nil !}
testCompilerValₙ = Refl

-- this he didn't like for some reason
-- Cons (eval (Val 1)) Nil == {!   !}
-- I previously used append Nil xs but it would flip the results
testCompilerValₘ : vreturn (Cons (eval (Val 1)) Nil) == Cons 1 Nil
testCompilerValₘ = Refl

-- now let's try with a zeroVec

testCompilerValₙ-zeroVec4 : exec (
    compile (Val 1)) ({! zeroVec 4 !}) ==
        {! Cons 1 (Cons Zero (Cons Zero (Cons Zero (Cons Zero Nil)))) !}
testCompilerValₙ-zeroVec4 = Refl

-- yay vreturn doesn't complain
testCompilerValₘ-zeroVec4 : vreturn (
    Cons (eval (Val 1)) (zeroVec 4)) == 
        Cons 1 (Cons Zero (Cons Zero (Cons Zero (Cons Zero Nil))))
testCompilerValₘ-zeroVec4 = Refl

testCompilerValₙ-zeroVec1 : exec 
    (compile (Val 1)) ({! zeroVec 1 !}) == 
        {! Cons 1 (Cons Zero Nil) !}
testCompilerValₙ-zeroVec1 = Refl

-- yay vreturn doesn't complain
testCompilerValₘ-zeroVec1 : vreturn 
    (Cons (eval (Val 1)) (zeroVec 1)) == 
        Cons 1 (Cons Zero Nil)
testCompilerValₘ-zeroVec1 = Refl

-- so from the above we conclude that 
-- the compiler is correct for Val


-- let's try the add constructor

addSimpleExpr : {! Expr 1 !}
addSimpleExpr = Add (Val 1) (Val 2)

testCompilerAddSimpleₙ : 
    exec (compile addSimpleExpr) Nil == {! Cons  3 Nil !}
testCompilerAddSimpleₙ = Refl


testCompilerAddSimpleₘ : 
    append Nil (Cons (eval addSimpleExpr) Nil) == Cons 3 Nil
testCompilerAddSimpleₘ = Refl


testCompilerAddSimpleₙ-zeroVec1 : 
    exec (compile addSimpleExpr) ({! zeroVec 1 !}) == 
        {! Cons  3  (Cons Zero Nil) !}
testCompilerAddSimpleₙ-zeroVec1 = Refl


testCompilerAddSimpleₘ-zeroVec1 : 
    vreturn (Cons (eval addSimpleExpr) (zeroVec 1)) == 
        Cons 3 (Cons Zero Nil)
testCompilerAddSimpleₘ-zeroVec1 = Refl 



-- add nested expressions...

addNestedExpr : {! Expr 2 !}
addNestedExpr = Add (Add (Val 1) (Val 2)) (Add (Val 3) (Val 4))



testCompilerAddNestedₙ : 
    exec (compile addNestedExpr) Nil == {! Cons 10 Nil !}
testCompilerAddNestedₙ = Refl


testCompilerAddNestedₘ : 
    append Nil (Cons (eval addNestedExpr) Nil) == Cons 10 Nil
testCompilerAddNestedₘ = Refl


-- deeply nested adds..

addNested₂Expr : {! Expr 3 !}
addNested₂Expr = Add addNestedExpr addNestedExpr


testCompilerAddNested₂ₙ : 
    exec (compile addNested₂Expr) Nil == {! Cons 20 Nil !}
testCompilerAddNested₂ₙ = Refl


testCompilerAddNested₂ₘ : 
    append Nil (Cons (eval addNested₂Expr) Nil) == Cons 20 Nil
testCompilerAddNested₂ₘ = Refl