Support externally declared relation names

README.md

@@ -88,7 +88,7 @@ order to conveniently generate characters and backstories for creative purposes.
                                            VillainHome) is Result))))
 
 ;; we generate lots of story strings; we query the first such string below
-(define solution-stream (all story-program))
+(define solution-stream (solve story-program))
 
 > (get (stream-first solution-stream) 'story)
 "The heroic TA Zack from CT worked with Ari to thwart the wicked prof Ben of NY"
@@ -120,4 +120,4 @@ Finally, you can run the tests with:
 
 ```
 raco test -p minidusa
-```
+```

private/compile.rkt

@@ -69,21 +69,25 @@
                           (rt:fact add1 (list (rt:variable 'X)) 2))))
      '()))
 
+;; An CompilerState is a
+;; (compiler-state MutSymbolTable SymbolSet SymbolSet), tracking which relation
+;; names are imported, external, and arities of the rest (internally defined)
+(struct compiler-state [arities imports externs])
+
 ;; this is the old compile-time function
-;; ImportsSyntax LogicSyntax -> RacketSyntax
-(define (compile-logic imports-stx logic-stx)
-  (define rel-arities (local-symbol-table))
-  (define imported-rel-vars (mutable-set))
-  ; add all imported symbols; later we use this to compile attibutes
-  (for ([stx-pair (syntax->list imports-stx)])
-    (syntax-parse stx-pair
-      [[rel-id _]
-       ; we want to put the symbols in our symbol table, not the identifiers,
-       ; otherwise we will not have the right notion of element equality
-       (set-add! imported-rel-vars (syntax->datum #'rel-id))]))
+;; ImportsSyntax IdsSyntax LogicSyntax -> RacketSyntax
+(define (compile-logic imports-stx externs-stx logic-stx)
+  (define arities (local-symbol-table))
+  (define imports
+    (apply immutable-symbol-set
+           ; grabs all of the ([rel-var _] ...)s
+           (map (lambda (stx-pair) (first (syntax->list stx-pair)))
+                (syntax->list imports-stx))))
+  (define externs (apply immutable-symbol-set (syntax->list externs-stx)))
+  (define state (compiler-state arities imports externs))
 
   (define body
-    (let ([compile-decl ((curry compile-decl) rel-arities imported-rel-vars)]
+    (let ([compile-decl ((curry compile-decl) state)]
           [logic-stx (flatten-decls logic-stx)])
       (syntax-parse logic-stx
         [(d ...)
@@ -128,36 +132,36 @@
     [[_ ((_ is? {_ ...+}) :- _ ...+)] #t]
     [_ #f]))
 
-;; MutSymbolTable MutSymbolSet DeclSyntax -> [ListOf RacketSyntax]
+;; CompilerState DeclSyntax -> [ListOf RacketSyntax]
 ;; This returns a list so that we can expand to multiple decls in the case of
 ;; a `decls` block.
 ;; Note that DeclSyntax _does_ include the expanded relation occurrence
-(define (compile-decl arities imports decl-stx)
+(define (compile-decl state decl-stx)
   ; partial application to thread around references to the symbol tables
-  (let ([compile-conc ((curry compile-conc) arities imports)]
-        [compile-decl ((curry compile-decl) arities imports)])
+  (let ([compile-conc ((curry compile-conc) state)]
+        [compile-decl ((curry compile-decl) state)])
     (syntax-parse decl-stx
       #:datum-literals (decls :-)
       [(decls d ...) (flatten (map compile-decl (attribute d)))]
       ;; get rid of the outer ref
       [[_ (conc :- prems ...+)]
        #:with (prem ...)
-       (map ((curry compile-prem) arities imports) (attribute prems))
+       (map ((curry compile-prem) state) (attribute prems))
        (list #`(rt:rule #,(compile-conc #'conc) (list prem ...)))]
       [[_ conc]
        (list #`(rt:rule #,(compile-conc #'conc) '()))])))
 
-;; MutSymbolTable MutSymbolSet ConclusionSyntax -> RacketSyntax
+;; CompilerState ConclusionSyntax -> RacketSyntax
 ;; throws a compile-time error when there is a binding
 ;; occurrence of a variable in the conclusion, which is disallowed
-(define (compile-conc arities imports conc-stx)
+(define (compile-conc state conc-stx)
   ;; shadowing to disallow compiling terms with binding occurrences
   (let ([compile-term ((curry compile-term)
                        #:forbid-binds "cannot bind variables in conclusions")]
-        [compile-rel-id ((curry compile-rel-id) arities imports)]
+        [compile-rel-id ((curry compile-rel-id) state)]
         [raise-if-imported!
          (lambda (name)
-           (when (set-member? imports (syntax->datum name))
+           (when (symbol-set-member? (compiler-state-imports state) name)
              (raise-syntax-error
               #f
               "imported relations cannot appear in conclusions"
@@ -180,26 +184,26 @@
        (raise-if-imported! #'name)
        #'(rt:rule-frag rel-var-comped (list comp-t ...) '() #f)])))
 
-;; MutSymbolTable MutSymbolSet PremiseSyntax -> RacketSyntax
-(define (compile-prem arities imports prem-stx)
-  (let ([compile-rel-id ((curry compile-rel-id) arities imports)]
+;; CompilerState PremiseSyntax -> RacketSyntax
+(define (compile-prem state prem-stx)
+  (let ([compile-rel-id ((curry compile-rel-id) state)]
         [compile-term-named
          (lambda (name)
            (curry compile-term
                   #:forbid-binds
-                  (and (set-member? imports name)
+                  (and (symbol-set-member? (compiler-state-imports state) name)
                        "cannot run imported relations backwards")))])
     (syntax-parse prem-stx
       #:datum-literals (is)
       [((name t ...) is ch)
        #:with (comp-t ...)
-       (map (compile-term-named (syntax->datum #'name)) (attribute t))
+       (map (compile-term-named #'name) (attribute t))
        #:with rel-var-comped (compile-rel-id #'name (length (attribute t)))
        #`(rt:fact rel-var-comped (list comp-t ...) #,(compile-term #'ch))]
       [(name t ...)
        #:with (comp-t ...) (map compile-term (attribute t))
        #:with rel-var-comped (compile-rel-id #'name (length (attribute t)))
-       (when (set-member? imports (syntax->datum #'name))
+       (when (symbol-set-member? (compiler-state-imports state) #'name)
          (raise-syntax-error #f
                              "imported relations must be used with 'is'"
                              #'name))
@@ -209,7 +213,7 @@
 ;; compiles to a reference to a bound procedure if it was imported;
 ;; otherwise checks the arity (if seen before, or sets arity otherwise)
 ;; and returns as the runtime representation of the name
-(define (compile-rel-id arities imports rel-id arity)
+(define (compile-rel-id state rel-id arity)
   (define rel-sym (syntax->datum rel-id))
 
   (when (member rel-sym RESERVED-NAMES)
@@ -222,12 +226,16 @@
         (symbol-table-ref table key)
         (begin (symbol-table-set! table key val #:allow-overwrite? #t)
                val)))
-
-  (if (set-member? imports rel-sym)
-      ; sets to arity if missing from the table -> will be equal
-      rel-id
-      (let ([expected-arity (symbol-table-ref! arities rel-id arity)])
-        (unless (= arity expected-arity)
+
+  (cond [(symbol-set-member? (compiler-state-imports state) rel-id)
+         rel-id]
+        [(symbol-set-member? (compiler-state-externs state) rel-id)
+         #`'#,rel-id]
+        [else
+         (define expected-arity
+           ; will add to the table if missing, which will pass equality check
+           (symbol-table-ref! (compiler-state-arities state) rel-id arity))
+         (unless (= arity expected-arity)
           (raise-syntax-error
            #f
            (format
@@ -236,7 +244,7 @@
             expected-arity
             arity)
            rel-id))
-        #`#'#,rel-id)))
+         #`#'#,rel-id]))
 
 ;; TermSyntax -> RacketSyntax
 (define (compile-term term-stx #:forbid-binds [message #f])

private/data.rkt

@@ -31,6 +31,13 @@
 ;; - Procedure, representing an imported relation
 ;; - Symbol, but only to allow users to interact with relations in facts
 
+;; rel=?: Relation Relation -> Bool
+(define (rel=? rel1 rel2)
+  (or (eq? rel1 rel2)  ; for symbols and procedures
+      (and (syntax? rel1)
+           (syntax? rel2)
+           (bound-identifier=? rel1 rel2))))
+
 ;; A Fact is a (fact Relation [ListOf Datum] [Option Datum]).
 ;; It represents a known fact (either given or deduced) in the database.
 ;; Currently, stored facts will never store a procedure for the relation,
@@ -43,10 +50,7 @@
   [(define (equal-proc self other rec)
      ;; this first check is a hack, so that symbol comparison works in tests...
      ;; TODO: fix this by implementing a more proper equality check
-     (and (or (eq? (fact-rel self) (fact-rel other))  ; for proc + symbols
-              (and (syntax? (fact-rel self))
-                   (syntax? (fact-rel other))
-                   (bound-identifier=? (fact-rel self) (fact-rel other))))
+     (and (rel=? (fact-rel self) (fact-rel other))
           (rec (fact-terms self) (fact-terms other))
           (rec (fact-value self) (fact-value other))))
    (define (hash-proc self rec)
@@ -64,17 +68,21 @@
 ;; fact-stx-original?: Fact -> Bool
 ;; determines whether the fact's relation is syntax coming from a macro or not
 (define (fact-stx-original? f)
-  ;; strip off layer of indirection from syntax-spec
-  (define from (and (syntax? (fact-rel f))
-                    (syntax-property (fact-rel f) 'compiled-from)))
-  (and from (syntax-original? from)))
+  (define rel (fact-rel f))
+  ;; strip off layer of indirection from syntax-spec, if it is a symbol
+  (define from-if-stx (and (syntax? rel)
+                           (syntax-property rel 'compiled-from)))
+  (or (symbol? rel)
+      (and from-if-stx (syntax-original? from-if-stx))))
 
 ;; smush-syntax/fact: Fact -> Fact
 ;; replaces the syntax object in a fact with its underlying symbol
 ;; (maybe the "signature" could be more descriptive, but this is clear imo)
 (define (smush-syntax/fact f)
   (define rel (fact-rel f))
-  (struct-copy fact f [rel (if (procedure? rel) rel (syntax->datum rel))]))
+  (struct-copy fact f [rel (if (or (symbol? rel) (procedure? rel))
+                               rel
+                               (syntax->datum rel))]))
 
 ;; A Variable is a (variable Symbol)
 (struct variable [name] #:transparent)
@@ -92,7 +100,7 @@
 (struct constraint [rel terms none-of]
   #:methods gen:equal+hash
   [(define (equal-proc self other rec)
-     (and (bound-identifier=? (constraint-rel self) (constraint-rel other))
+     (and (rel=? (constraint-rel self) (constraint-rel other))
           (rec (constraint-terms self) (constraint-terms other))
           (rec (constraint-none-of self) (constraint-none-of other))))
    (define (hash-proc self rec)
@@ -104,13 +112,14 @@
                         (rec (constraint-terms self))
                         (rec (constraint-none-of self))))])
 
-;; A RuleFragment is (rule-frag Syntax [ListOf Term] [ListOf Term] Boolean)
+;; A RuleFragment is (rule-frag Relation [ListOf Term] [ListOf Term] Boolean)
 ;; It is an _internal representation_ of the source syntax, which in
 ;; general may contain variables. These can be combined to form rules
 ;; or facts (closed rules with no premises).
 ;; Notably, a Term is an immediate, and does not have nested terms:
 ;; this is a difference from the surface <term> syntax; these nested
 ;; terms will be desugared in an ANF-like pass.
+;; The Relation here will not be a Procedure, currently.
 
 ;; A ClosedRuleFragment is
 ;; (rule-frag Syntax [ListOf Datum] [ListOf Datum] [OneOf Boolean 'tried])
@@ -121,11 +130,7 @@
 (struct rule-frag [name terms choices is??] #:transparent
   #:methods gen:equal+hash
   [(define (equal-proc self other rec)
-     (and (or (eq? (rule-frag-name self) (rule-frag-name other))
-              (and (syntax? (rule-frag-name self))
-                   (syntax? (rule-frag-name other))
-                   (bound-identifier=? (rule-frag-name self)
-                                       (rule-frag-name other))))
+     (and (rel=? (rule-frag-name self) (rule-frag-name other))
           (rec (rule-frag-terms self) (rule-frag-terms other))
           (rec (rule-frag-choices self) (rule-frag-choices other))
           (rec (rule-frag-is?? self) (rule-frag-is?? other))))

private/database.rkt

@@ -18,6 +18,10 @@
 (define (db-of . facts)
   (database (apply set facts) (set)))
 
+;; factset->db: [SetOf Fact] -> Database
+(define (factset->db factset)
+  (database factset (set)))
+
 ;; db-empty? : Database -> Boolean
 ;; Returns #f if the database contains facts.
 (define (db-empty? db)
@@ -43,8 +47,7 @@
             (for/set ([c (database-constraints db)]
                       #:when
                       (not (and (equal? (fact-terms f) (constraint-terms c))
-                                (bound-identifier=? (fact-rel f)
-                                                    (constraint-rel c)))))
+                                (rel=? (fact-rel f) (constraint-rel c)))))
               c)))
 
 ;; db-add-constraint : Constraint Database -> Database
@@ -74,7 +77,7 @@
   ;; Determine if the given fact has the same attribute as
   ;; rel and terms.
   (define (attr-like? f)
-    (and (bound-identifier=? (fact-rel f) rel)
+    (and (rel=? (fact-rel f) rel)
          (equal? (fact-terms f) terms)))
   (not (db-empty? (db-filter attr-like? db))))
 
@@ -102,14 +105,14 @@
   ;; different values.
   ;; This should only be called when to-add is a Fact.
   (define (fact-consistent? known)
-    (not (and (bound-identifier=? (fact-rel to-add) (fact-rel known))
+    (not (and (rel=? (fact-rel to-add) (fact-rel known))
               (equal? (fact-terms to-add) (fact-terms known))
               (not (equal? (fact-value to-add) (fact-value known))))))
 
   ;; constraint-valid? : Constraint Fact -> Boolean
   ;; Determine if the fact is consistent given the constraint c.
   (define (constraint-valid? c f)
-    (not (and (bound-identifier=? (fact-rel f) (constraint-rel c))
+    (not (and (rel=? (fact-rel f) (constraint-rel c))
               (equal? (fact-terms f) (constraint-terms c))
               (set-member? (constraint-none-of c) (fact-value f)))))
 

private/runtime.rkt

@@ -1,13 +1,14 @@
 #lang racket
 
-(provide all
+(provide (rename-out [solve-opt solve])
          has
          get
          soln->factset)
 
 (require racket/stream
          "data.rkt"
-         "database.rkt")
+         "database.rkt"
+         (for-syntax syntax/parse))
 
 ;; we have some database (D) of known facts
 ;; we want to evolve this database
@@ -61,11 +62,11 @@
 ;; sample : Logic -> [Maybe Solution]
 ;; Obtain one possible solution of the given program, if one exists.
 
-;; all : Logic -> [StreamOf Solution]
+;; all : Logic [SetOf Fact] -> [StreamOf Solution]
 ;; Obtain a stream of all possible solutions of the given program.
 ;; The stream may be infinite, and computing the next item may not
 ;; always terminate.
-(define (all prog)
+(define (solve-entry prog facts)
   ;; result->stream : SolutionResult -> [StreamOf Solution]
   ;; Processes a SolutionResult into a stream of Solution by recursively
   ;; backtracking through all possible intermediate choices.
@@ -78,7 +79,17 @@
   (define (collect-backtracked stack)
     (result->stream (backtrack prog stack)))
 
-  (result->stream (solve prog (db-of) '())))
+  (result->stream (solve prog (factset->db facts) '())))
+
+;; version of all that takes facts as an optional keyword argument
+(define-syntax solve-opt
+  (lambda (stx)
+    (syntax-parse stx
+      [(_ (~or* (~seq #:facts factset)
+                (~seq))
+          prog)
+       #:with facts (or (attribute factset) #'(set))
+       #'(solve-entry prog facts)])))
 
 ;; solve : Logic Database SearchStack -> SolutionResult
 ;; Given a search state and a database of currently known facts, obtain a
@@ -214,7 +225,7 @@
 
     ; 'tried = #t for our purposes
     (define (conclusion=? a b)
-      (and (bound-identifier=? (rule-frag-name a) (rule-frag-name b))
+      (and (rel=? (rule-frag-name a) (rule-frag-name b))
            (equal? (rule-frag-terms a) (rule-frag-terms b))
            (equal? (rule-frag-choices a) (rule-frag-choices b))
            (equal? (not (rule-frag-is?? a)) (not (rule-frag-is?? b)))))
@@ -299,7 +310,7 @@
 
   ;; looks-like? : Fact -> Boolean
   (define (looks-like? fact)
-    (and (bound-identifier=? (fact-rel open) (fact-rel fact))
+    (and (rel=? (fact-rel open) (fact-rel fact))
          (andmap similar?
                  (fact-terms open)
                  (fact-terms fact))
@@ -409,7 +420,7 @@
   (and (or (eq? (fact-rel f) rel)  ; for proc + symbols
            (and (syntax? (fact-rel f))
                 (syntax? rel)
-                (bound-identifier=? (fact-rel f) rel)))
+                (rel=? (fact-rel f) rel)))
        (equal? (fact-terms f) terms)))
 
 ;; has: Solution Symbol Datum ... -> Bool