Adding serialization of theories
This commit is contained in:
parent
61f628f2c6
commit
99fd3546be
|
@ -1,6 +1,8 @@
|
||||||
#lang racket
|
#lang racket
|
||||||
(require "runtime.rkt"
|
(require "runtime.rkt"
|
||||||
|
"serialize.rkt"
|
||||||
"stx.rkt")
|
"stx.rkt")
|
||||||
(provide make-theory
|
(provide make-theory
|
||||||
theory/c
|
theory/c
|
||||||
|
(all-from-out "serialize.rkt")
|
||||||
(all-from-out "stx.rkt"))
|
(all-from-out "stx.rkt"))
|
||||||
|
|
|
@ -54,6 +54,9 @@ The Datalog database can be directly used by Racket programs through this API.
|
||||||
|
|
||||||
@defproc[(make-theory) theory/c]{ Creates a theory for use with @racket[datalog]. }
|
@defproc[(make-theory) theory/c]{ Creates a theory for use with @racket[datalog]. }
|
||||||
|
|
||||||
|
@defproc[(write-theory [t theory/c]) void]{ Writes a theory to the current output port. Source location information is lost. }
|
||||||
|
@defproc[(read-theory) theory/c]{ Reads a theory from the current input port. }
|
||||||
|
|
||||||
@defform[(datalog thy-expr
|
@defform[(datalog thy-expr
|
||||||
stmt ...)
|
stmt ...)
|
||||||
#:contracts ([thy-expr theory/c])]{ Executes the statements on the theory given by @racket[thy-expr]. Returns the answers to the final query as a list of substitution dictionaries or returns @racket[empty]. }
|
#:contracts ([thy-expr theory/c])]{ Executes the statements on the theory given by @racket[thy-expr]. Returns the answers to the final query as a list of substitution dictionaries or returns @racket[empty]. }
|
||||||
|
|
37
collects/datalog/serialize.rkt
Normal file
37
collects/datalog/serialize.rkt
Normal file
|
@ -0,0 +1,37 @@
|
||||||
|
#lang racket/base
|
||||||
|
(require racket/contract
|
||||||
|
racket/match
|
||||||
|
racket/list
|
||||||
|
"runtime.rkt")
|
||||||
|
|
||||||
|
(define remove-stx-objs
|
||||||
|
(match-lambda
|
||||||
|
[(? hash? ht)
|
||||||
|
(for/hash ([(k v) (in-hash ht)])
|
||||||
|
(values k (remove-stx-objs v)))]
|
||||||
|
[(? cons? c)
|
||||||
|
(cons (remove-stx-objs (car c))
|
||||||
|
(remove-stx-objs (cdr c)))]
|
||||||
|
[(? prefab-struct-key s)
|
||||||
|
(apply make-prefab-struct
|
||||||
|
(prefab-struct-key s)
|
||||||
|
(remove-stx-objs (rest (vector->list (struct->vector s)))))]
|
||||||
|
[(? syntax? s)
|
||||||
|
#f]
|
||||||
|
[x x]))
|
||||||
|
|
||||||
|
(define (write-theory t)
|
||||||
|
(write (remove-stx-objs t)))
|
||||||
|
|
||||||
|
(define (hash->hash! ht)
|
||||||
|
(define ht! (make-hash))
|
||||||
|
(for ([(k v) (in-hash ht)])
|
||||||
|
(hash-set! ht! k v))
|
||||||
|
ht!)
|
||||||
|
|
||||||
|
(define (read-theory)
|
||||||
|
(hash->hash! (read)))
|
||||||
|
|
||||||
|
(provide/contract
|
||||||
|
[write-theory (-> theory/c void)]
|
||||||
|
[read-theory (-> theory/c)])
|
|
@ -2,7 +2,7 @@
|
||||||
(require datalog tests/eli-tester)
|
(require datalog tests/eli-tester)
|
||||||
|
|
||||||
(define parent (make-theory))
|
(define parent (make-theory))
|
||||||
|
|
||||||
(test
|
(test
|
||||||
(datalog parent
|
(datalog parent
|
||||||
(! (parent joseph2 joseph1))
|
(! (parent joseph2 joseph1))
|
||||||
|
@ -59,6 +59,21 @@
|
||||||
=>
|
=>
|
||||||
(list (hasheq 'X 2))
|
(list (hasheq 'X 2))
|
||||||
|
|
||||||
|
(let ()
|
||||||
|
(define new-parent
|
||||||
|
(with-input-from-bytes
|
||||||
|
(with-output-to-bytes (λ () (write-theory parent)))
|
||||||
|
(λ () (read-theory))))
|
||||||
|
(test
|
||||||
|
(datalog new-parent
|
||||||
|
(? (ancestor A B)))
|
||||||
|
=>
|
||||||
|
(list (hasheq 'A 'joseph3 'B 'joseph2)
|
||||||
|
(hasheq 'A 'joseph2 'B 'lucy)
|
||||||
|
(hasheq 'A 'joseph2 'B 'joseph1)
|
||||||
|
(hasheq 'A 'joseph3 'B 'lucy)
|
||||||
|
(hasheq 'A 'joseph3 'B 'joseph1))))
|
||||||
|
|
||||||
(local [(local-require tests/datalog/examples/ancestor)]
|
(local [(local-require tests/datalog/examples/ancestor)]
|
||||||
(datalog theory
|
(datalog theory
|
||||||
(? (ancestor A B))))
|
(? (ancestor A B))))
|
||||||
|
|
Loading…
Reference in New Issue
Block a user