TestExer-cad0p.agda

-- the following are wrong. indeed, if they pass for your assignment
-- solution, you have manipulated the predefined data type definition,
-- which is bad.

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

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


-- these are not wrong, but they are not right either. they will fail for
-- many people because they have defined the data types slightly
-- differently.

testCompilerValₙ-zeroVec4 : exec (
    compile (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

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

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

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

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


-- what is this?

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