Started documenting the tactics library

scribblings/cur.scrbl

@@ -44,3 +44,4 @@ Everything else in @racketmodname[cur] is provided by untrusted user-land code--
 
 @include-section{curnel.scrbl}
 @include-section{reflection.scrbl}
+@include-section{stdlib.scrbl}

scribblings/stdlib.scrbl

@@ -0,0 +1,10 @@
+#lang scribble/manual
+@(require
+   "defs.rkt")
+
+@title[#:style '(toc)]{Standard Library}
+Cur has a small standard library, primary for demonstration purposes.
+
+@local-table-of-contents[]
+
+@include-section{stdlib/tactics.scrbl}

scribblings/stdlib/tactics.scrbl

@@ -0,0 +1,65 @@
+#lang scribble/manual
+
+@(require "../defs.rkt")
+
+@title{Tactics}
+As Coq has shown, tactics have proven useful for doing complex proofs. In Cur, tactics are not
+built-in or provided by the language. However, any user can use meta-programming to add tactics to
+Cur. A tactic system ships in the standard library, written entirely in user-land code.
+
+@section{Proof State and Defining Tactics}
+In Cur, a @deftech{tactic} is a Racket function from @tech{proof state} to @tech{proof state} that
+runs at @gtech{phase} 1.
+
+@defproc[(proof? [p any/c])
+         boolean?]{
+Returns @racket[#t] if @racket[p] is a proof, and @racket[#f] otherwise.
+A @deftech{proof} is either a Cur term as a syntax object, or a procedure expecting a proof to plug
+into the holes of the existing partial proof.
+}
+
+@defproc[(complete-proof? [p any/c])
+         boolean?]{
+Returns @racket[#t] is the proof @racket[p] has no holes, i.e., is a syntax object, and @racket[#f]
+otherwise.
+}
+
+@defproc[(new-proof)
+         proof?]{
+Returns an empty partial @tech{proof}, i.e., the identity function.
+}
+
+@defstruct[proof-state ([env dict?]
+                        [goals dict?]
+                        [current-goal natural-number/c]
+                        [proof (or/c syntax? procedure?)]
+                        [theorem syntax?])]{
+The environment @racket[env] is a map of assumptions local to the theorem from symbols (names) to the
+type of the assumption as a syntax object.
+The list of goals @racket[goals] is a map from natural numbers to goals, types as syntax objects.
+The current goal @racket[current-goal] is a natural number indexing into @racket[goals], representing
+the goal currently in focus.
+The @racket[proof] is the @tech{proof} of the theorem so far. The @racket[proof] is either a
+syntax object if complete, or a procedure which expects a proof to replace the current holes in the
+@racket[proof].
+The @racket[theorem] is the original statement of the theorem to be proved.
+}
+
+@defproc[(new-proof-state [prop syntax?])
+         proof-state?]{
+Returns a @racket[proof-state?] initialized with an empty environment, the list of goals initialized with
+@racket[prop], the current-goal set to @racket[0], an empty proof via @racket[(new-proof)], and the
+theorem set to @racket[prop].
+}
+
+@defproc[(proof-state-proof-complete? [ps proof-state?])
+         boolean?]{
+Returns @racket[#t] is the proof of the @racket[proof-state?] @racket[ps] is a
+@racket[complete-proof?], and @racket[#f] otherwise.
+}
+
+@section{Standard Tactics}
+
+@section{Interactive Tactic}
+
+@section{SarTactic (Sarcastic Tactics)}

stdlib/tactics/base.rkt

@@ -73,9 +73,16 @@
 ;;; TODO: I'm partially implementing lens here.
 ;;; TODO: Interface is mildly inconsistent.
 (begin-for-syntax
+  (define new-proof values)
+
+  (define (proof? p)
+    (or (syntax? p) (procedure? p)))
+
+  (define (complete-proof? p)
+    (syntax? p))
+
   (define-struct proof-state (env goals current-goal proof theorem))
 
-  (define new-proof values)
 
   (define (new-proof-state prop)
     (proof-state
@@ -87,7 +94,7 @@
 
   ;; Given a Proof-State, return #t if the current-proof is complete
   ;; (i.e. is a Expr and not a Ctxt), #f otherwise.
-  (define (proof-state-proof-complete? ps) (not (procedure? (proof-state-proof ps))))
+  (define (proof-state-proof-complete? ps) (complete-proof? (proof-state-proof ps)))
 
   ;;; Extra accessors