Have tests for evaluation

[Blaisorblade]

I was screwing with names and evaluation for Blaisorblade/pts#1, and after a testsuite pass I got this:

$ time pts --quiet --instance uu UU.lpts
./UU/D/Term.lpts:70: Type error: we expected two terms to be equivalent but they are not.
  A variable from the environment has an unexpected type.
  Checked term: S
  Actual type: **
  But we expected type: *** -> Q *
  Difference
    actual:   **
    expected: *** -> Q *

./UU/D/Term.lpts:81: Unbound identifier: dplace

  assert dplace : Pi (Q : TRep)
         ^^^^^^^

./UU/D/Term.lpts:97: Unbound identifier: dplace

./UU/D/build.lpts:25: Unbound identifier: dplace

  body (dplace Q tfun1 tfun2 tfun3 tfun4 R S name)
        ^^^^^^^

./UU/D/build.lpts:29: Type error: we expected two terms to be equivalent but they are not.
  A variable from the environment has an unexpected type.
  Checked term: S2
  Actual type: **
  But we expected type: *** -> Q *
  Difference
    actual:   **
    expected: *** -> Q *

./UU/D/build.lpts:47: Type error: we expected two terms to be equivalent but they are not.
  A variable from the environment has an unexpected type.
  Checked term: S2
  Actual type: **
  But we expected type: *** -> Q *
  Difference
    actual:   **
    expected: *** -> Q *

./UU/D/build.lpts:62: Type error: we expected two terms to be equivalent but they are not.
  A variable from the environment has an unexpected type.
  Checked term: S2
  Actual type: **
  But we expected type: *** -> Q *
  Difference
    actual:   **
    expected: *** -> Q *

./UU/D/build.lpts:78: Type error: we expected two terms to be equivalent but they are not.
  A variable from the environment has an unexpected type.
  Checked term: S2
  Actual type: **
  But we expected type: *** -> Q *
  Difference
    actual:   **
    expected: *** -> Q *

./UU/D/build.lpts:93: Type error: we expected two terms to be equivalent but they are not.
  A variable from the environment has an unexpected type.
  Checked term: S2
  Actual type: **
  But we expected type: *** -> Q *
  Difference
    actual:   **
    expected: *** -> Q *

./UU/D/build.lpts:109: Type error: we expected two terms to be equivalent but they are not.
  A variable from the environment has an unexpected type.
  Checked term: S
  Actual type: **
  But we expected type: *** -> Q *
  Difference
    actual:   **
    expected: *** -> Q *

./UU/D/build.lpts:124: Type error: we expected two terms to be equivalent but they are not.
  A variable from the environment has an unexpected type.
  Checked term: S
  Actual type: **
  But we expected type: *** -> Q *
  Difference
    actual:   **
    expected: *** -> Q *

./UU/D/build.lpts:147: Unbound identifier: dbuildAbs1

  assert dbuildAbs1 :
         ^^^^^^^^^^^

./UU/D/build.lpts:154: Unbound identifier: dbuildApp1

  assert dbuildApp1 :
         ^^^^^^^^^^^

./UU/D/build.lpts:161: Unbound identifier: dbuildAbs2

  assert dbuildAbs2 :
         ^^^^^^^^^^^

./UU/D/build.lpts:168: Unbound identifier: dbuildApp2

  assert dbuildApp2 :
         ^^^^^^^^^^^

./UU/D/build.lpts:175: Unbound identifier: dbuildAbs3

  assert dbuildAbs3 :
         ^^^^^^^^^^^

./UU/D/build.lpts:182: Unbound identifier: dbuildApp3

  assert dbuildApp3 :
         ^^^^^^^^^^^

./UU/D/build.lpts:189: Unbound identifier: dbuildAbs4

  assert dbuildAbs4 :
         ^^^^^^^^^^^

./UU/D/build.lpts:196: Unbound identifier: dbuildApp4

  assert dbuildApp4 :
         ^^^^^^^^^^^

./UU/D/build.lpts:212: Type error: we expected two terms to be equivalent but they are not.
  A variable from the environment has an unexpected type.
  Checked term: S
  Actual type: **
  But we expected type: ***
  Difference
    actual:   **
    expected: ***

./UU/D/build.lpts:228: Unbound identifier: dbuildAbs1

./UU/D/build.lpts:229: Unbound identifier: dbuildApp1

./UU/D/build.lpts:230: Unbound identifier: dbuildAbs2

./UU/D/build.lpts:231: Unbound identifier: dbuildApp2

./UU/D/build.lpts:232: Unbound identifier: dbuildAbs3

./UU/D/build.lpts:233: Unbound identifier: dbuildApp3

./UU/D/build.lpts:234: Unbound identifier: dbuildAbs4

./UU/D/build.lpts:235: Unbound identifier: dbuildApp4

./UU/D/build.lpts:236: Unbound identifier: dbuild

./UU.lpts:69: Unbound identifier: dbuild

  assert dbuild : Pi (A : TTerm *) . DTerm A -> DTerm A;
         ^^^^^^^

real    0m1.199s
user    0m1.148s
sys 0m0.025s

Low priority. Maybe we should just run pts on some existing code (e.g. examples/) as part of the Travis testing?

[Toxaris]

cabal test runs pts on the code in the examples folder, see src-test/tests.hs.

Maybe there should be more and harder examples? However, I don't want to copy the UU stuff to the examples folder just yet, because that code is currently not public.

[Blaisorblade]

OK, so we have one more reason to need more examples (#21).

[Blaisorblade]

21 is enough to track this. Closing.