| ;; | |
| ;; General definitions | |
| ;; | |
| ;; General variables | |
| syntax N = nat ;; hack | |
| syntax n = nat ;; hack | |
| syntax m = nat ;; hack | |
| ;; General constants | |
| def $Ki : nat | |
| def $Ki = 1024 | |
| ;; General numeric functions | |
| def $min(nat, nat) : nat | |
| def $min(i, j) = i -- if $(i <= j) | |
| def $min(i, j) = j -- otherwise | |
| def $sum(nat*) : nat ;; TODO: hint | |
| def $sum(eps) = 0 | |
| def $sum(n n'*) = $(n + $sum(n'*)) | |
| ;; General sequence functions | |
| def $opt_(syntax X, X*) : X? hint(show %2) hint(partial) | |
| def $opt_(syntax X, eps) = eps | |
| def $opt_(syntax X, w) = w | |
| def $list_(syntax X, X?) : X* hint(show %2) | |
| def $list_(syntax X, eps) = eps | |
| def $list_(syntax X, w) = w | |
| def $concat_(syntax X, (X*)*) : X* hint(show $concat(%2)) hint(inverse $inv_concat_) | |
| def $concat_(syntax X, eps) = eps | |
| def $concat_(syntax X, (w*) (w'*)*) = w* $concat_(X, (w'*)*) | |
| def $inv_concat_(syntax X, X*) : (X*)* | |
| def $inv_concat_ hint(builtin) | |
| ;; [{1, 2}, {a, b, c}] -> {[1, a], [1, b], [1, c], [2, a], [2, b], [2, c]} | |
| def $setproduct_(syntax X, (X*)*) : (X*)* hint(show %latex("{\\Large\\times}") %2) | |
| def $setproduct1_(syntax X, X*, (X*)*) : (X*)* | |
| def $setproduct2_(syntax X, X, (X*)*) : (X*)* | |
| def $setproduct_(syntax X, eps) = (eps) | |
| def $setproduct_(syntax X, (w_1*) (w*)*) = $setproduct1_(X, w_1*, $setproduct_(X, (w*)*)) | |
| def $setproduct1_(syntax X, eps, (w*)*) = eps | |
| def $setproduct1_(syntax X, w_1 w'*, (w*)*) = $setproduct2_(X, w_1, (w*)*) ++ $setproduct1_(X, w'*, (w*)*) | |
| def $setproduct2_(syntax X, w_1, eps) = eps | |
| def $setproduct2_(syntax X, w_1, (w'*) (w*)*) = (w_1 w'*) ++ $setproduct2_(X, w_1, (w*)*) |