Skip to content

Commit

Permalink
contract
Browse files Browse the repository at this point in the history
  • Loading branch information
zaoqi committed Aug 28, 2017
1 parent a5cd41f commit b2bfe55
Show file tree
Hide file tree
Showing 3 changed files with 17 additions and 11 deletions.
12 changes: 6 additions & 6 deletions constraint.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -22,17 +22,17 @@
define-constraints-
define-constraints
get-constraints-
constraintv/c
constraintsv/c
constraintv?
constraintsv?
)
(require "id.rkt")
(require "types.rkt")
(require "contract.rkt")

#| ConstraintV = Any |#
(define constraintv/c any/c)
(define constraintv? any/c)
#| ConstraintsV = Any |#
(define constraintsv/c any/c)
(define constraintsv? any/c)

#| ID →
ConstraintsV →
Expand All @@ -50,8 +50,8 @@ Constraints |#
(State → Symbol × [Any]) →
Constraints |#
(define/contract (new-constraints empty add check clean show)
(-> constraintsv/c
(-> constraintsv/c state? (maybe (cons/c state? (listof var?))))
(-> constraintsv?
(-> constraintsv? state? (maybe (cons/c state? (listof var?))))
(-> (listof var?) state? boolean?)
(-> state? (maybe state?))
(-> state? (cons/c symbol? list?))
Expand Down
12 changes: 8 additions & 4 deletions state.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -108,7 +108,8 @@
(define (define-state-cleaner- f) (set! cleanc (cons f cleanc)))

#| State → State |#
(define (clean-state s)
(define/contract (clean-state s)
(-> state? state?)
(let loop ([cs cleanc] [s s])
(if (null? cs)
s
Expand All @@ -118,7 +119,8 @@
(loop (cdr cleanc) s))))))

#| State → [StatePatch] → SizedStream State |#
(define (patch+ s p)
(define/contract (patch+ s p)
(-> state? (listof state-patch?) (sizedstream/c state?))
(if (null? p)
(sizedstream s)
(sizedstream-bind (patch s (car p)) (λ (ns) (patch+ ns (cdr p))))))
Expand All @@ -131,11 +133,13 @@
(state-c s)))

#| State → Constraints → ConstraintsV |#
(define (get-constraintsv s cs) (hash-ref (state-c s) (constraints-id cs) (constraints-empty cs)))
(define/contract (get-constraintsv s cs)
(-> state? constraints? constraintsv?)
(hash-ref (state-c s) (constraints-id cs) (constraints-empty cs)))

#| State → Constraints → ConstraintsV → State |#
(define/contract (set-constraintsv s cs v)
(-> state? constraints? constraintsv/c state?)
(-> state? constraints? constraintsv? state?)
(state (state-g s) (hash-set (state-c s) (constraints-id cs) v)))

#| Goal ... → State |#
Expand Down
4 changes: 3 additions & 1 deletion zk.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -74,7 +74,9 @@
(sizedstream-map state-c (pass* (new-state+ g))))

#| Goal+ → SizedStream (Hash ID ConstraintsV) |#
(define (run-+ g) (run- (goal+-s g)))
(define/contract (run-+ g)
(-> goal+? (sizedstream/c hash?))
(run- (goal+-s g)))

#| ID → (... → Goal) → (... → DGoal) |#
(define ((goalf->dgoalf id f) . args) (new-dgoal id args (run-goal (apply f args))))
Expand Down

0 comments on commit b2bfe55

Please sign in to comment.