search

granule-project / gerty

A small implementation of graded modal dependent type theory. A younger cousin to Granule.
Other
53 stars 1 forks source link

6 out of 68 tests failed #1

Open sofia-snow opened 2 years ago

sofia-snow commented 2 years ago

Hello. Are these tests known to be failing?

Progress 1/2: gerty-mainTests
  File tests
    Positive cases
      well-formed syntax
        checking tests/cases/positive/syntax/case.lam parses:                                                    OK
        checking tests/cases/positive/syntax/functions.lam parses:                                               OK
        checking tests/cases/positive/syntax/implicits.lam parses:                                               OK
        checking tests/cases/positive/syntax/grading/funTyGradedBinder.lam parses:                               OK
        checking tests/cases/positive/syntax/grading/grades.lam parses:                                          OK
        checking tests/cases/positive/syntax/grading/lamGradedBinder.lam parses:                                 OK
        checking tests/cases/positive/syntax/grading/tenGradedBinder.lam parses:                                 OK
        checking tests/cases/positive/syntax/grading/varInGrade.lam parses:                                      OK
        checking tests/cases/positive/syntax/grading/complexExprInGrade.lam parses:                              OK
        checking tests/cases/positive/syntax/modality.lam parses:                                                OK
        checking tests/cases/positive/syntax/pairs.lam parses:                                                   OK
        checking tests/cases/positive/syntax/records/canNameLastParam.lam parses:                                OK
        checking tests/cases/positive/syntax/records/emptyBody.lam parses:                                       OK
        checking tests/cases/positive/syntax/records/justConstructor.lam parses:                                 OK
        checking tests/cases/positive/syntax/records/multipleFieldsSingleClause.lam parses:                      OK
        checking tests/cases/positive/syntax/regression/funTyInPair.lam parses:                                  OK
      scope checking
        checking tests/cases/positive/scope/grades.lam scope checks:                                             OK
      type-checking
        checking tests/cases/positive/typing/builtins/modality.lam type checks:                                  OK (0.05s)
        checking tests/cases/positive/typing/builtins/nat.lam type checks:                                       OK
        checking tests/cases/positive/typing/builtins/pairs.lam type checks:                                     FAIL (0.08s)
          tests/Test.hs:60:
          Expected file to type check, but got:   During checking of top-level 'snd':

          The following error occurred when type-checking (at ensure) 'y'
           against a type 'a':

            Expected type 'a' but got 'b (case x of [z] -> z)'

        checking tests/cases/positive/typing/builtins/unit.lam type checks:                                      OK (0.01s)
        checking tests/cases/positive/typing/grading/implicits.lam type checks:                                  OK (0.22s)
        checking tests/cases/positive/typing/grading/infLub.lam type checks:                                     FAIL
          tests/Test.hs:60:
          Expected file to type check, but got:   During checking of top-level 't0':

          The following error occurred when type-checking:

            (.0 = .inf)  is Falsifiable

        checking tests/cases/positive/typing/grading/oneUseVarUsed.lam type checks:                              OK
        checking tests/cases/positive/typing/grading/privacyLevels.lam type checks:                              OK (0.07s)
        checking tests/cases/positive/typing/grading/securityLevels.lam type checks:                             OK (0.02s)
        checking tests/cases/positive/typing/grading/zeroUseVarUnused.lam type checks:                           OK
        checking tests/cases/positive/typing/inference/modality.lam type checks:                                 OK (0.03s)
        checking tests/cases/positive/typing/inference/pair.lam type checks:                                     OK (0.04s)
        checking tests/cases/positive/typing/inference/unit.lam type checks:                                     OK (0.04s)
        checking tests/cases/positive/typing/regression/snd.lam type checks:                                     FAIL (0.03s)
          tests/Test.hs:60:
          Expected file to type check, but got:   During checking of top-level 'snd':

          The following error occurred when type-checking (at ensure) 'y'
           against a type 'b (fst a b <x, y>)':

            Expected type 'b (fst a b <x, y>)' but got 'b x'

        checking tests/cases/positive/typing/simple/app.lam type checks:                                         OK (0.07s)
        checking tests/cases/positive/typing/simple/lam.lam type checks:                                         OK (0.01s)
        checking tests/cases/positive/typing/simple/lambdaTypeToType.lam type checks:                            OK (0.01s)
        checking tests/cases/positive/typing/simple/pi.lam type checks:                                          OK (0.03s)
        checking tests/cases/positive/typing/simple/substitution.lam type checks:                                OK (0.04s)
        checking tests/cases/positive/typing/simple/type0.lam type checks:                                       OK
        checking tests/cases/positive/typing/simple/var.lam type checks:                                         OK (0.03s)
      type-checking examples
        checking examples/app.lam type checks:                                                                   OK
        checking examples/existential.lam type checks:                                                           FAIL
          tests/Test.hs:60:
          Expected file to type check, but got:

          The following error occurred when parsing:

            examples/existential.lam:6,18: Parse error
            ,<ERROR>
             .1] Type 0) (b : [.1, .0] (x ...

        checking examples/gradedApp.lam type checks:                                                             OK (0.02s)
        checking examples/gradedComonad.lam type checks:                                                         OK (0.02s)
        checking examples/gradedId.lam type checks:                                                              OK
        checking examples/gradedPair.lam type checks:                                                            OK
        checking examples/nuyts.lam type checks:                                                                 FAIL (0.06s)
          tests/Test.hs:60:
          Expected file to type check, but got:   During checking of top-level 'RIisoExampleLeft':

          The following error occurred when type-checking:

            (.1 = .inf) ∧ (.1 = .inf)  is Falsifiable

        checking examples/pairs.lam type checks:                                                                 FAIL (0.16s)
          tests/Test.hs:60:
          Expected file to type check, but got:   During checking of top-level 'snd':

          The following error occurred when type-checking (at ensure) 'y'
           against a type 'b (fst a b <x, y>)':

            Expected type 'b (fst a b <x, y>)' but got 'b x'

        checking examples/poly.lam type checks:                                                                  OK (0.03s)
        checking examples/syntax.lam type checks:                                                                OK (0.18s)
        checking examples/talk.lam type checks:                                                                  OK (0.07s)
        checking examples/universal.lam type checks:                                                             OK (0.01s)
    Negative cases
      bad syntax
        checking tests/cases/negative/syntax/namedLastParamInFunTy.lam doesn't parse:                            OK
        checking tests/cases/negative/syntax/namedSortOfRecord.lam doesn't parse:                                OK
        checking tests/cases/negative/syntax/qualifiedSig.lam doesn't parse:                                     OK
      ill-scoped
        checking tests/cases/negative/scope/dupDefs1.lam doesn't scope check:                                    OK
        checking tests/cases/negative/scope/dupDefs2.lam doesn't scope check:                                    OK
        checking tests/cases/negative/scope/dupDefs3.lam doesn't scope check:                                    OK
        checking tests/cases/negative/scope/dupDefs4.lam doesn't scope check:                                    OK
        checking tests/cases/negative/scope/grading/unboundVarInFunGrade.lam doesn't scope check:                OK
        checking tests/cases/negative/scope/grading/unboundVarInLamGrade.lam doesn't scope check:                OK
      ill-typed
        checking tests/cases/negative/typing/grading/mismatchedGradesForSucc.lam doesn't type check:             OK
        checking tests/cases/negative/typing/grading/implicits/noGradeIdTypeTooBig.lam doesn't type check:       OK (0.02s)
        checking tests/cases/negative/typing/grading/implicits/noGradeIdMult.lam doesn't type check:             OK (0.02s)
        checking tests/cases/negative/typing/grading/zeroUseVarUsed.lam doesn't type check:                      OK
        checking tests/cases/negative/typing/grading/zeroUseVarUsedInType.lam doesn't type check:                OK
        checking tests/cases/negative/typing/modality/incorrectBoxingDifferingGrade.lam doesn't type check:      OK
        checking tests/cases/negative/typing/regression/missingParamDependentApplication.lam doesn't type check: OK
        checking tests/cases/negative/typing/types/incorrectTypeForLambda.lam doesn't type check:                OK
        checking tests/cases/negative/typing/types/typeBadLevelSimple.lam doesn't type check:                    OK

6 out of 68 tests failed (1.49s)
dorchard commented 2 years ago

Thanks for this. A couple of these should be passing, but a couple are known to be failing and basically represent some deep work that needs doing. examples/existential.lam shouldn't be there though so I've moved that into a work-in-progress folder in b463537