Update Syntax for Counter Example

This updates the syntax for the counter example to reflect how it
originally was written in Corset.  Thus, it is now demonstrating some of
the new features supported in `go-corset`.

pkg/corset/parser.go

@@ -917,5 +917,5 @@ func isIdentifierStart(c rune) bool {
 }
 
 func isIdentifierMiddle(c rune) bool {
-	return unicode.IsDigit(c) || isIdentifierStart(c) || c == '-'
+	return unicode.IsDigit(c) || isIdentifierStart(c) || c == '-' || c == '!'
 }

testdata/counter.lisp

@@ -1,3 +1,19 @@
+(defpurefun (vanishes! e0) e0)
+;;
+(defpurefun (next X) (shift X 1))
+(defpurefun (prev X) (shift X -1))
+;;
+(defpurefun (eq! x y) (- x y))
+;;
+(defpurefun (will-eq! e0 e1) (eq! (next e0) e1))
+(defpurefun (will-inc! e0 offset) (will-eq! e0 (+ e0 offset)))
+(defpurefun (will-remain-constant! e0) (will-eq! e0 e0))
+;;
+(defpurefun (if-eq-else x val then else) (if (eq! x val) then else))
+
+;; ===================================================
+;; Constraints
+;; ===================================================
 (defcolumns STAMP CT)
 
 ;; In the first row, STAMP is always zero.  This allows for an
@@ -6,30 +22,28 @@
 
 ;; In the last row of a valid frame, the counter must have its max
 ;; value.  This ensures that all non-padding frames are complete.
-(defconstraint last (:domain {-1}) (* STAMP (- 3 CT)))
+(defconstraint last (:domain {-1} :guard STAMP) (eq! CT 3))
 
 ;; STAMP either remains constant, or increments by one.
 (defconstraint increment () (*
                       ;; STAMP[k] == STAMP[k+1]
-                      (- STAMP (shift STAMP 1))
+                      (will-inc! STAMP 0)
                       ;; Or, STAMP[k]+1 == STAMP[k+1]
-                      (- (+ 1 STAMP) (shift STAMP 1))))
+                      (will-inc! STAMP 1)))
 
 ;; If STAMP changes, counter resets to zero.
 (defconstraint reset () (*
                   ;; STAMP[k] == STAMP[k+1]
-                  (- STAMP (shift STAMP 1))
+                  (will-remain-constant! STAMP)
                   ;; Or, CT[k+1] == 0
-                  (shift CT 1)))
+                  (vanishes! (next CT))))
 
 ;; If STAMP non-zero and reaches end-of-cycle, then stamp increments;
 ;; otherwise, counter increments.
-(defconstraint heartbeat ()
-  (if STAMP
-      0
-      ;; If CT == 3
-      (if (- 3 CT)
-          ;; Then, STAMP[k]+1 == STAMP[k]
-          (- (+ 1 STAMP) (shift STAMP 1))
-          ;; Else, CT[k]+1 == CT[k]
-          (- (+ 1 CT) (shift CT 1)))))
+(defconstraint heartbeat (:guard STAMP)
+  ;; If CT == 3
+  (if-eq-else CT 3
+      ;; Then, STAMP[k]+1 == STAMP[k]
+      (will-inc! STAMP 1)
+      ;; Else, CT[k]+1 == CT[k]
+      (will-inc! CT 1)))