Introduced Sartactics!

* Added the Sartactics library, provides a sassy wrapper around the basic
  tactics.
* Added prefix-in, although it probably only works for macros
* Better syntax for define-tactic

redex-curnel.rkt

@@ -949,6 +949,7 @@
     only-in
     all-defined-out
     rename-in
+    prefix-in
     submod
     #%module-begin
     begin

stdlib/tactics/base.rkt

@@ -135,13 +135,15 @@
 ;;; Syntax for defining tactics.
 ;; (define-tactic command-name function)
 ;; (define-tactic (command-name args ... Proof-State) body)
+;; TODO: Srsly?
 (define-syntax (define-tactic syn)
   (syntax-case syn ()
     [(_ (name args ... ps) body ...)
      (quasisyntax/loc syn
        (define-for-syntax (name args ... ps) body ...))]
     [(_ name function)
-     (raise-syntax-error "Syntax not yet defined")]))
+     (quasisyntax/loc syn
+       (define-for-syntax name function))]))
 
 ;; (define-goal-tactic command-name function)
 ;; (define-goal-tactic (command-name args ... ctx goal-list current-goal) body)

stdlib/tactics/basic.rkt

@@ -9,6 +9,7 @@
     obvious
     restart
     forget
+    print
     by-assumption
     interactive))
 
@@ -126,7 +127,7 @@
   (proof (obvious))
   ;; TODO: Fix this unit test so it doesn't require interaction
   (define-theorem meow4 (forall (x : bool) bool))
-  (proof
+  #;(proof
     (interactive))
   ;; TODO: Add check-cur-equal? for unit testing?
   #;(check-pred (curry cur-equal? '(lambda (x : bool) x)))

stdlib/tactics/sartactics.rkt

@@ -0,0 +1,135 @@
+#lang s-exp "../../redex-curnel.rkt"
+(require
+  "base.rkt"
+  (prefix-in basic: "basic.rkt")
+  (for-syntax racket/syntax))
+
+(provide
+  (for-syntax
+    intro
+    interactive))
+
+;;; SARCASTIC INTERACTIVE TACTICS
+
+(begin-for-syntax
+  (define jabs
+    (list
+      "I don't think you know what you're doing."
+      "Does this look right to *you*?"
+      "Prove it."))
+
+  (define (random-ref ls)
+    (list-ref ls (random (length ls))))
+
+  (define (random-jab) (random-ref jabs))
+  )
+
+(define-tactic (print ps)
+  (basic:print ps)
+  (displayln (random-jab))
+  ps)
+
+(begin-for-syntax
+  (define intro-jabs
+    (list
+      "What a clever name."
+      "How original."
+      "I'm sure that seems like a good idea to *you*."
+      "Why don't you just assume false while you're at it?")))
+
+(define-tactic (intro name ps)
+  (displayln (random-ref intro-jabs))
+  (newline)
+  (basic:intro name ps))
+
+(define-tactic (forget ps)
+  (displayln "Like hell.")
+  ps)
+(define-tactic by-assumption basic:by-assumption)
+
+(begin-for-syntax
+  (define restart-jabs
+    (list
+      "Hahahahahahahaha."
+      "Lawl."
+      "Why don't you just do it right the first time?"
+      "Stupid human."
+      "I've been waiting for this.")))
+(define-tactic (restart ps)
+  (displayln (random-ref restart-jabs))
+  (basic:restart ps))
+
+(begin-for-syntax
+  (define denied-obvious-jabs
+    (list
+      "It's not obvious to me."
+      "You expect me to know this?"
+      "If it's so obvious then just finish the proof already."
+      "Maybe you should hire a grad student."))
+  (define accept-obvious-jabs
+    (list
+      "I wasn't going to say anything, but this was taking you forever."
+      "Finally."
+      "Let me show you how it's done."
+      "You're right, I am better at proving things than you are."
+      "Aw that was *sooo* tough...")))
+(define-tactic (obvious ps)
+  (if (< (random 10) 3)
+      (begin
+        (displayln (random-ref accept-obvious-jabs))
+        (newline)
+        (basic:obvious ps))
+      (begin
+        (displayln (random-ref denied-obvious-jabs))
+        (newline)
+        ps)))
+
+(begin-for-syntax
+  (define no-quit-jabs
+    (list
+      "Na."
+      "How about instead I just delete all your work?"
+      "I don't think your ready yet.")))
+(define-tactic (interactive ps)
+  (printf "Starting interactive tactic session. Prepared to be sassed:~n")
+  (printf "Type (quit) to quit.~n")
+  (let loop ([ps ps] [cmds '()])
+    (if (proof-complete? ps)
+        (basic:print ps)
+        (print ps))
+    (let ([cmd (read-syntax)])
+      (newline)
+      (syntax-case cmd (quit)
+        [(quit)
+         (if (< (random 10) 4)
+             (begin
+               (printf "Don't forget this. It took you long enough:~n")
+               (pretty-print (map syntax->datum cmds))
+               (newline)
+               ps)
+             (begin
+               (displayln (random-ref no-quit-jabs))
+               (loop ps cmds)))]
+        [(tactic arg ...)
+          (with-handlers (#;[exn:fail:contract?
+                            (lambda (e)
+                              (printf "tactic ~a expected different arguments.~n"
+                                (syntax->datum #'tactic))
+                              (loop ps cmds))]
+                          #;[exn:fail:syntax?
+                            (lambda (e)
+                              (printf "~a is not a tactic.~n"
+                                (syntax->datum #'tactic))
+                              (loop ps cmds))])
+            (loop (apply (lookup-tactic #'tactic)
+                    (append (syntax->list #'(arg ...)) (list ps)))
+                  (cons cmd cmds)))]))))
+
+(module+ test
+  (require
+    rackunit
+    "../bool.rkt")
+  (define-theorem meow (forall (x : bool) bool))
+  (proof
+    (interactive))
+  )