*** Convolver specification with n=4 and k=0
fmod CONV-SPEC is
    protecting INT .

    sort IntStr .

    op _(_) : IntStr Int -> Int [prec 1] .

    op U : -> Int .

    ops W1 W2 W3 W4 : -> Int . *** n=4 in this example

    op convSpec : IntStr -> IntStr .

    vars X : IntStr .
    var T : Int .

    *** Output is U if we have not read in enough inputs
    ceq convSpec(X)(T) = U if T < 4 .
    
    *** Otherwise compute convolution
    eq convSpec(X)(T) = W1 * X(T - 3) + W2 * X(T - 2) +
                         W3 * X(T - 1) + W4 * X(T)
                      [owise] .
endfm

*** Restrict values of W, X to 1, -1 and
*** Convolver becomes a pattern matcher
fmod CONV-RUN is
    protecting CONV-SPEC .
    
    op x : -> IntStr .
    
    eq W1 = 1 .
    eq W2 = -1 .
    eq W3 = 1 .
    eq W4 = -1 .
    
    eq x(0) = 1 .
    eq x(1) = -1 .
    eq x(2) = 1 .
    eq x(3) = -1 .
    eq x(4) = 1 .
    eq x(5) = -1 .
    eq x(6) = 1 .
    eq x(7) = -1 .
endfm

reduce convSpec(x)(0) .
reduce convSpec(x)(1) .
reduce convSpec(x)(2) .
reduce convSpec(x)(3) .
reduce convSpec(x)(4) .
reduce convSpec(x)(5) .
reduce convSpec(x)(6) .
reduce convSpec(x)(7) .