From 678607afa0f17ca3e7b65312db9e1c14389b37d2 Mon Sep 17 00:00:00 2001
From: "William J. Bowman" <wjb@williamjbowman.com>
Date: Thu, 10 Sep 2015 19:24:32 -0400
Subject: [PATCH] Working on interactive tactic

Currently, due to multiple uses of eval, can't get this to work. Need to
redesign/reorganize tactics
---
 redex-curnel.rkt   |  2 ++
 stdlib/tactics.rkt | 43 +++++++++++++++++++++++++++++++++++++------
 2 files changed, 39 insertions(+), 6 deletions(-)

diff --git a/redex-curnel.rkt b/redex-curnel.rkt
index 7cbe3eb..f61e27f 100644
--- a/redex-curnel.rkt
+++ b/redex-curnel.rkt
@@ -949,6 +949,7 @@
     only-in
     all-defined-out
     rename-in
+    submod
     #%module-begin
     begin
     (rename-out
@@ -975,6 +976,7 @@
     ;; DYI syntax extension
     define-syntax
     begin-for-syntax
+    define-for-syntax
     (for-syntax (all-from-out syntax/parse))
     syntax-case
     syntax-rules
diff --git a/stdlib/tactics.rkt b/stdlib/tactics.rkt
index 03d2cf0..39ff76c 100644
--- a/stdlib/tactics.rkt
+++ b/stdlib/tactics.rkt
@@ -118,7 +118,6 @@
                   (syntax-local-eval
                     ;; Thread proof state through tactic calls, and eval
                     ;; at compile-time.
-
                     #`(let* ([ps (new-proof-state #'#,t)]
                              [ps (f #'args* ... ps)]
                              ...)
@@ -143,9 +142,8 @@
   (syntax-case syn ()
     [(_ (name args ... ps) body ...)
      (quasisyntax/loc syn
-        (begin-for-syntax
-          (define (name args ... ps)
-                  body ...)))]
+        (define-for-syntax (name args ... ps)
+          body ...))]
     [(_ name function)
      (raise-syntax-error "Syntax not yet defined")]))
 
@@ -202,7 +200,37 @@
       [current-goal (proof-state-original-goal ps)]
       [current-proof empty-proof]))
 
-(define-tactic (print ps) (print-proof-state ps) ps)
+(define-tactic (show ps) (print-proof-state ps) ps)
+
+(begin-for-syntax
+  (define-namespace-anchor a))
+
+;; Interactive you say? Sure whatevs, DIY
+(define-tactic (interactive ps)
+  (printf "Starting interactive tactic session:~n")
+  (let loop ([ps ps] [cmds '()])
+    (show ps)
+    (let ([cmd (read-syntax)])
+      (syntax-case cmd (quit)
+        [(quit)
+         (begin
+           (printf "Your tactic script:~n")
+           (pretty-print cmds)
+           (newline)
+           ps)]
+        ;; TODO: eval is bad. Maybe use (read-eval-print-loop) and its
+        ;; TODO: config parameters.
+        [(tactic arg ...)
+          (with-handlers (#;[exn:fail:syntax?
+                            (lambda (e)
+                                    (printf "~a is not a tactic.~n"
+                                            (syntax->datum #'tactic))
+                                    (loop ps cmds))])
+            (displayln (syntax-local-eval #'(begin tactic)))
+            (loop (apply (eval-syntax #'tactic
+                           (namespace-anchor->namespace a))
+                         (append (syntax->list #'(arg ...)) (list ps)))
+                  (cons cmd cmds)))]))))
 
 ;; TODO:
 ;; Open interactive REPL for tactic DSL; exit with QED command, which
@@ -218,13 +246,16 @@
   (define-theorem meow1 (forall (x : bool) bool))
   (proof
     (obvious)
-    (print))
+    (show))
   (define-theorem meow2 (forall (x : bool) bool))
   (proof
     (intro x)
     (restart)
     (intro x)
     (by-assumption))
+  ;(define-theorem meow3 (forall (x : bool) bool))
+  ;(proof
+  ;  (interactive))
   ;; TODO: Add check-cur-equal? for unit testing?
   #;(check-pred (curry cur-equal? '(lambda (x : bool) x)))
   )