test.maude

load "./regexp-proof-gen.maude"

mod TEST is
    protecting PROOF-GEN .
    protecting QID .

    sort TestResult .
    op passed : -> TestResult [ctor] .
    op _ _ : TestResult TestResult -> TestResult [assoc] .

    vars TR : TestResult .
    vars TestName : Qid .

    eq passed TR =  TR .
    eq TR passed =  TR .

    op test _ @ _ ?= _ ; : Qid Universal Universal -> TestResult [poly(2 3)] .
    **************************************************************************
    *** NOTE: MAKE SURE YOU DEFINE AN EQUATION BELOW FOR ANY SORT YOU USE! ***
    **************************************************************************
    eq test TestName @ Expected:Bool    ?= Expected:Bool    ; = passed .
    eq test TestName @ Expected:Pattern ?= Expected:Pattern ; = passed .

    op unit-tests : -> TestResult .
    eq unit-tests
     =  test 'true-is-true @ true ?= true ;
        test 'occurs-in-subset-1        @ occursIn('nCzD, sVar 'X C= sVar 'Y)        ?= false ;
        test 'occurs-in-subset-2        @ occursIn('nCzD, sVar 'X C= sVar 'nCzD)     ?= true ;
        test 'occurs-in-mu-1            @ occursIn('X, mu 'X (epsilon \/ (a .. sVar 'Y \/ b .. (mu 'Z (epsilon \/ (a .. sVar 'Z \/ b .. sVar 'Z))))))
                                                                                     ?= true ;
        test 'occurs-in-mu-1            @ occursIn('X, mu 'Y (epsilon \/ (a .. sVar 'Y \/ b .. (mu 'Z (epsilon \/ (a .. sVar 'X \/ b .. sVar 'Z))))))
                                                                                     ?= true ;
        test 's-subst                   @ substitute[sVar 'Z / 'X] in mu 'Y sVar 'X  ?= mu 'Y sVar 'Z ;
        test 's-subst-no-desugar-1      @ substitute[ mu 'ZZ sVar 'Phi / 'ZZ ]
                                            in [[ ctximp-app 'box (sVar 'box .. top-letter) (sVar 'Rho) ]]
                                          ?=   [[ ctximp-app 'box (sVar 'box .. top-letter) (sVar 'Rho) ]] ;
        test 's-subst-no-desugar-2      @ substitute[ mu 'ZZ sVar 'Phi / 'ZZ ]
                                            in [[ ctximp-app 'ZZ (sVar 'box .. top-letter) (sVar 'Rho) ]]
                                          ?=   [[ ctximp-app 'ZZ (sVar 'box .. top-letter) (sVar 'Rho) ]] ;
     .
endm