WIP
This commit is contained in:
parent
68de150492
commit
e9aaa45d9b
151
os2.rkt
151
os2.rkt
|
@ -2,6 +2,11 @@
|
|||
;; Virtualized operating system, this time with presence.
|
||||
|
||||
(require racket/match)
|
||||
(require "relation.rkt")
|
||||
(require "unify.rkt")
|
||||
|
||||
;; Endpoints are the units of deduplication.
|
||||
;; Flows (in canonical form) are the units of presence.
|
||||
|
||||
;;---------------------------------------------------------------------------
|
||||
;; Data definitions
|
||||
|
@ -11,20 +16,21 @@
|
|||
|
||||
;; A QuasiQueue<X> is a list of Xs in *reversed* order.
|
||||
|
||||
(struct vm (processes ;; PID -> Process
|
||||
topics ;; Topic -> Set<Flow>
|
||||
flows ;; Flow -> Set<Route>
|
||||
(struct vm (processes ;; Hash<PID, Process>
|
||||
topic-flows ;; Relation<Topic, Flow>
|
||||
flow-topics ;; Relation<Flow, Topic>
|
||||
active-handlers ;; Relation<Topic, Endpoint>
|
||||
next-process-id ;; PID
|
||||
pending-actions ;; QuasiQueue<(cons PID Action)>
|
||||
) #:transparent)
|
||||
|
||||
;; (route PID SID Handlers)
|
||||
(struct route (process-id sid handlers) #:transparent)
|
||||
;; (endpoint PID SID Handlers)
|
||||
(struct endpoint (process-id sid handlers) #:transparent)
|
||||
|
||||
(struct process (id ;; PID
|
||||
state
|
||||
interests ;; SID -> List<Handlers>
|
||||
meta-interests ;; SID -> List<Handlers>
|
||||
interests ;; Relation<SID, Topic>
|
||||
meta-interests ;; Relation<SID, Topic>
|
||||
) #:transparent)
|
||||
|
||||
(struct topic (role pattern virtual?) #:prefab)
|
||||
|
@ -35,13 +41,13 @@
|
|||
;; PresenceHandler = Topic -> State -> Transition
|
||||
;; AbsenceHandler = Topic * Reason -> State -> Transition
|
||||
;; MessageHandler = Topic * Message -> State -> Transition
|
||||
(struct handlers (topic presence absence message) #:transparent)
|
||||
(struct handlers (presence absence message) #:transparent)
|
||||
|
||||
;; actions is a plain old List<Action>, not a QuasiQueue.
|
||||
(struct transition (state actions) #:transparent)
|
||||
|
||||
;; Preactions
|
||||
(struct add-role (sid handlers) #:prefab)
|
||||
(struct add-role (sid topic handlers) #:prefab)
|
||||
(struct delete-roles (sid) #:prefab)
|
||||
(struct send-message (topic body) #:prefab)
|
||||
(struct spawn (thunk) #:prefab)
|
||||
|
@ -68,6 +74,25 @@
|
|||
(for/list ([role (co-roles (topic-role t))])
|
||||
(struct-copy topic t [topic-role role])))
|
||||
|
||||
(define (refine-topic remote-topic new-pattern)
|
||||
(struct-copy topic remote-topic [pattern new-pattern]))
|
||||
|
||||
(define (roles-intersect? l r)
|
||||
(memq l (co-roles r)))
|
||||
|
||||
;; Both left and right must be canonicalized.
|
||||
(define (topic-intersection left right)
|
||||
(and (roles-intersect? (topic-role left) (topic-role right))
|
||||
(mgu-canonical (freshen (topic-pattern left)) (freshen (topic-pattern right)))))
|
||||
|
||||
;; True iff the flow between remote-topic and local-topic should be
|
||||
;; visible to the local peer. This is the case when either local-topic
|
||||
;; is virtual (in which case everything is seen) or otherwise if
|
||||
;; remote-topic is also not virtual.
|
||||
(define (flow-visible? local-topic remote-topic)
|
||||
(or (topic-virtual? local-topic)
|
||||
(not (topic-virtual? remote-topic))))
|
||||
|
||||
;;---------------------------------------------------------------------------
|
||||
|
||||
;; QuasiQueue<X>
|
||||
|
@ -93,8 +118,9 @@
|
|||
|
||||
(define (make-vm boot)
|
||||
(vm (hash)
|
||||
(hash)
|
||||
(hash)
|
||||
(relation)
|
||||
(relation)
|
||||
(relation)
|
||||
0
|
||||
(list->quasi-queue (list (spawn boot)))))
|
||||
|
||||
|
@ -118,18 +144,97 @@
|
|||
|
||||
(define (perform-action pid action state)
|
||||
(match action
|
||||
[(add-role sid handlers) ...]
|
||||
[(delete-roles sid) ...]
|
||||
[(send-message topic body) ...]
|
||||
[(spawn thunk)
|
||||
(match-define (transition initial-state initial-actions) (run-user-code (thunk)))
|
||||
(define new-pid (vm-next-process-id state))
|
||||
(struct-copy vm (enqueue-actions state new-pid initial-actions)
|
||||
[processes (hash-set (vm-processes state) new-pid (process new-pid
|
||||
initial-state
|
||||
(hash)
|
||||
(hash)))]
|
||||
[next-process-id (+ new-pid 1)])]))
|
||||
[(add-role sid topic handlers) (do-subscribe pid sid topic handlers state)]
|
||||
[(delete-roles sid) (do-unsubscribe pid sid state)]
|
||||
[(send-message topic body) (route-and-deliver topic body state)]
|
||||
[(spawn thunk) (do-spawn thunk state)]))
|
||||
|
||||
(define (install-flow state0 source-flow target-topic)
|
||||
(define state
|
||||
(struct-copy vm state0
|
||||
[topic-flows (relation-add (vm-topic-flows state0) target-topic source-flow)]
|
||||
[flow-topics (relation-add (vm-flow-topics state0) source-flow target-topic)]))
|
||||
(if (and (flow-visible? target-topic source-flow)
|
||||
;; Only notify if not previously notified, i.e., the routes were
|
||||
;; absent in state0.
|
||||
(not (relation-domain-member? (vm-flow-topics state0) source-flow)))
|
||||
(for/fold ([state state])
|
||||
([e (in-set (relation-ref (vm-active-handlers state) target-topic))])
|
||||
(run-ready state
|
||||
(endpoint-process-id e)
|
||||
((handlers-presence (endpoint-handlers e)) source-flow)))
|
||||
state))
|
||||
|
||||
(define ((add-interest sid topic) p)
|
||||
(struct-copy process p [interests (relation-add (process-interests p) sid topic)]))
|
||||
|
||||
(define (do-subscribe pid sid topic handlers state)
|
||||
(define e (endpoint pid sid handlers))
|
||||
(define topic-previously-known? (relation-domain-member? (vm-active-handlers state)))
|
||||
;; Install the handler.
|
||||
;; Update the process.
|
||||
(let ((state
|
||||
(struct-copy vm state
|
||||
[active-handlers (relation-add (vm-active-handlers state) topic e)]
|
||||
[processes (hash-update (vm-processes state) pid (add-interest sid topic))])))
|
||||
;; Add topic <--> flow mappings and fire the appropriate presence handlers.
|
||||
(if topic-previously-known?
|
||||
;; Just tell the local end. The other ends have already heard about this topic.
|
||||
(for/fold ([state state])
|
||||
([matching-flow (in-set (relation-ref (vm-topic-flows state) topic))])
|
||||
(install-flow state matching-flow topic))
|
||||
;; Compute intersections, and tell both ends.
|
||||
(for/fold ([state state])
|
||||
([matching-topic (in-set (vm-known-topics state))]
|
||||
[flow-pattern (in-value (topic-intersection topic matching-topic))]
|
||||
#:when flow-pattern) ;; We know that topic intersects matching-topic.
|
||||
(let* ((state (install-flow state (refine-topic topic flow-pattern) matching-topic))
|
||||
(state (install-flow state (refine-topic matching-topic flow-pattern) topic)))
|
||||
state)))))
|
||||
|
||||
(define (do-unsubscribe pid sid state)
|
||||
;; For each topic in the process's interests,
|
||||
;; - for each appropriate endpoint in active-handlers,
|
||||
;; - fire the absence handler
|
||||
;; - remove the endpoint
|
||||
;; - if no handlers remain in active-handlers for that topic,
|
||||
;; - for each flow in topic-flows for the topic,
|
||||
;; - remove the topic from flow-topics for the flow
|
||||
;; - if no topics remain for the flow,
|
||||
;; - dualize it using our source topic
|
||||
;; - ...??
|
||||
|
||||
(define (route-and-deliver message-topic body state)
|
||||
(define endpoints
|
||||
(for/set ([flow (in-relation-domain (vm-flow-topics state))]
|
||||
#:when (specialization? message-topic flow)
|
||||
[matching-flow (co-topics flow)]
|
||||
[matching-topic (in-set (relation-ref (vm-flow-topics state) matching-flow))]
|
||||
[matching-endpoint (in-set (relation-ref (vm-active-handlers state) matching-topic))])
|
||||
matching-endpoint))
|
||||
(for/fold ([state state]) ([e (in-set endpoints)])
|
||||
(run-ready state
|
||||
(endpoint-process-id e)
|
||||
((handlers-message (endpoint-handlers e)) message-topic body))))
|
||||
|
||||
(define (run-ready state pid interrupt-k)
|
||||
(define old-process (hash-ref (vm-processes state) pid))
|
||||
(match-define (transition new-process-state actions)
|
||||
(interrupt-k (process-state old-process-state)))
|
||||
(struct-copy vm (enqueue-actions state pid actions)
|
||||
[processes (hash-set (vm-processes state) pid
|
||||
(struct-copy process old-process
|
||||
[state new-process-state]))]))
|
||||
|
||||
(define (do-spawn thunk state)
|
||||
(match-define (transition initial-state initial-actions) (run-user-code (thunk)))
|
||||
(define new-pid (vm-next-process-id state))
|
||||
(struct-copy vm (enqueue-actions state new-pid initial-actions)
|
||||
[processes (hash-set (vm-processes state) new-pid (process new-pid
|
||||
initial-state
|
||||
(relation)
|
||||
(relation)))]
|
||||
[next-process-id (+ new-pid 1)]))
|
||||
|
||||
(define (enqueue-actions state pid actions)
|
||||
(struct-copy vm state
|
||||
|
|
42
relation.rkt
42
relation.rkt
|
@ -2,12 +2,16 @@
|
|||
;; Relations are equivalent to Hash<X, Set<Y>> and Set<Pair<X, Y>>.
|
||||
|
||||
(require racket/set)
|
||||
(require racket/match)
|
||||
|
||||
(provide (rename-out [make-relation relation])
|
||||
relation?
|
||||
relation->list
|
||||
list->relation
|
||||
|
||||
relation->hash
|
||||
in-relation-domain
|
||||
|
||||
relation-empty?
|
||||
relation-count
|
||||
|
||||
|
@ -16,9 +20,13 @@
|
|||
relation-remove
|
||||
relation-remove-all
|
||||
relation-ref
|
||||
relation-set
|
||||
relation-update
|
||||
relation-domain-member?
|
||||
relation-member?
|
||||
|
||||
relation-domain
|
||||
|
||||
relation-domain-eq?
|
||||
relation-domain-eqv?
|
||||
relation-domain-equal?
|
||||
|
@ -62,6 +70,12 @@
|
|||
[(cons (cons k v) rest) (loop rest (relation-add r k v))]
|
||||
[_ (error 'list->relation "Expected list of key/value pairs")])))
|
||||
|
||||
(define (relation->hash r)
|
||||
(relation-table r))
|
||||
|
||||
(define (in-relation-domain r)
|
||||
(in-hash-keys (relation-table r)))
|
||||
|
||||
(define (relation-empty? r)
|
||||
(zero? (hash-count (relation-table r))))
|
||||
|
||||
|
@ -70,17 +84,17 @@
|
|||
|
||||
(define (relation-add r k v)
|
||||
(struct-copy relation r
|
||||
[relation-table (hash-update (relation-table r)
|
||||
k
|
||||
(lambda (old-vs) (set-add old-vs v))
|
||||
(relation-set-constructor r))]))
|
||||
[table (hash-update (relation-table r)
|
||||
k
|
||||
(lambda (old-vs) (set-add old-vs v))
|
||||
(relation-set-constructor r))]))
|
||||
|
||||
(define (relation-add-all r k vs)
|
||||
(struct-copy relation r
|
||||
[relation-table (hash-update (relation-table r)
|
||||
k
|
||||
(lambda (old-vs) (set-union old-vs vs))
|
||||
(relation-set-constructor r))]))
|
||||
[table (hash-update (relation-table r)
|
||||
k
|
||||
(lambda (old-vs) (set-union old-vs vs))
|
||||
(relation-set-constructor r))]))
|
||||
|
||||
(define (relation-remove r k v)
|
||||
(define old-vs (hash-ref (relation-table r) k (relation-set-constructor r)))
|
||||
|
@ -96,10 +110,15 @@
|
|||
(hash-remove (relation-table r) k)
|
||||
(hash-set (relation-table r) k new-vs)))
|
||||
|
||||
(define (relation-ref r k
|
||||
[failure-result (lambda () (error 'relation-ref "Key not present: ~v" k))])
|
||||
(define (relation-ref r k [failure-result (relation-set-constructor r)])
|
||||
(hash-ref (relation-table r) k failure-result))
|
||||
|
||||
(define (relation-set r k vs)
|
||||
(hash-set (relation-table r) k vs))
|
||||
|
||||
(define (relation-update r k updater [failure-result (relation-set-constructor r)])
|
||||
(hash-update (relation-table r) k updater failure-result))
|
||||
|
||||
(define (relation-domain-member? r k)
|
||||
(hash-has-key? (relation-table r) k))
|
||||
|
||||
|
@ -107,6 +126,9 @@
|
|||
(and (relation-domain-member? r k)
|
||||
(set-member? (hash-ref (relation-table r) k) v)))
|
||||
|
||||
(define (relation-domain r)
|
||||
(hash-keys (relation-table r)))
|
||||
|
||||
(define (relation-domain-eq? r) (hash-eq? (relation-table r)))
|
||||
(define (relation-domain-eqv? r) (hash-eqv? (relation-table r)))
|
||||
(define (relation-domain-equal? r) (hash-equal? (relation-table r)))
|
||||
|
|
|
@ -0,0 +1,42 @@
|
|||
#lang racket/base
|
||||
|
||||
(provide current-struct-mappers
|
||||
install-struct-mapper!
|
||||
struct-map
|
||||
struct-map/accumulator)
|
||||
|
||||
;; Parameter<Hash<StructType,Mapper>>
|
||||
(define current-struct-mappers (make-parameter (hash)))
|
||||
|
||||
;; StructType Mapper -> Void
|
||||
(define (install-struct-mapper! struct-type m)
|
||||
(current-struct-mappers (hash-set (current-struct-mappers) struct-type m)))
|
||||
|
||||
;; (X -> Y) Struct<X> -> Struct<Y>
|
||||
(define (struct-map f x)
|
||||
(define-values (result acc)
|
||||
(struct-map* 'struct-map (lambda (v acc) (values (f v) acc)) (void) x))
|
||||
result)
|
||||
|
||||
;; (X Seed -> Y Seed) Seed Struct<X> -> Struct<Y> Seed
|
||||
(define (struct-map/accumulator f seed x)
|
||||
(struct-map* 'struct-map/accumulator f seed x))
|
||||
|
||||
(define (struct-map* name f seed x)
|
||||
(define-values (i skipped) (struct-info x))
|
||||
(when (not i) (error name "Cannot retrieve struct-info for ~v" x))
|
||||
(define m (hash-ref (current-struct-mappers)
|
||||
i
|
||||
(lambda ()
|
||||
(define key (prefab-struct-key x))
|
||||
(when (not key) (error name "No mapper for ~v" x))
|
||||
(prefab-struct-mapper key))))
|
||||
(m f seed x))
|
||||
|
||||
(define ((prefab-struct-mapper key) f initial-seed x)
|
||||
(define-values (new-fields final-seed)
|
||||
(for/fold ([new-fields '()] [old-seed initial-seed])
|
||||
([old-field (cdr (vector->list (struct->vector x)))])
|
||||
(define-values (new-field new-seed) (f old-field old-seed))
|
||||
(values (cons new-field new-fields) new-seed)))
|
||||
(values (apply make-prefab-struct key (reverse new-fields)) final-seed))
|
|
@ -0,0 +1,276 @@
|
|||
#lang racket/base
|
||||
|
||||
(require racket/set)
|
||||
(require racket/match)
|
||||
(require "struct-map.rkt")
|
||||
|
||||
(provide (struct-out variable)
|
||||
(struct-out canonical-variable)
|
||||
wild
|
||||
wild?
|
||||
non-wild?
|
||||
variables-in
|
||||
unify
|
||||
unify/env
|
||||
unify/vars
|
||||
unify-match/vars
|
||||
freshen
|
||||
canonicalize
|
||||
mgu-freshen
|
||||
mgu-canonical
|
||||
apply-subst
|
||||
specialization?
|
||||
upper-case-symbols->variables
|
||||
upper-case-symbols->canonical)
|
||||
|
||||
;; A Subst is a Maybe<AList<Variable,Any>>.
|
||||
;; TODO: semantics
|
||||
|
||||
;; Compared by eq?, not equal?. In particular, info is not involved in
|
||||
;; equivalence.
|
||||
(struct variable (info)
|
||||
#:property prop:custom-write
|
||||
(lambda (v port mode)
|
||||
(display "?" port)
|
||||
(write (variable-info v) port)))
|
||||
|
||||
;; Compared by equal?, not eq?. The number is a part of the
|
||||
;; appropriate equivalence relation for canonical-variables.
|
||||
(struct canonical-variable (index) #:transparent
|
||||
#:property prop:custom-write
|
||||
(lambda (v port mode)
|
||||
(display "?!" port)
|
||||
(write (canonical-variable-index v) port)))
|
||||
|
||||
;; -> Variable
|
||||
;; Create a fresh (and hence unconstrained) variable.
|
||||
(define (wild [base-name '_])
|
||||
(variable (gensym base-name)))
|
||||
|
||||
;; Any -> Boolean
|
||||
;; True iff the argument is a variable or canonical-variable.
|
||||
(define (wild? x)
|
||||
(or (variable? x) (canonical-variable? x)))
|
||||
|
||||
;; Any -> Boolean
|
||||
;; True iff the argument is neither a variable nor a canonical-variable.
|
||||
(define (non-wild? x)
|
||||
(not (wild? x)))
|
||||
|
||||
;; Any -> Set<Variable>
|
||||
(define (variables-in x)
|
||||
(let walk ((x x) (acc (set)))
|
||||
(cond
|
||||
[(variable? x) (set-add acc x)]
|
||||
[(pair? x) (walk (car x) (walk (cdr x) acc))]
|
||||
[(vector? x) (foldl walk acc (vector->list x))]
|
||||
[(struct? x) (walk (struct->vector x #f) acc)]
|
||||
[else acc])))
|
||||
|
||||
;; Variable Any -> Boolean
|
||||
(define (occurs? var val)
|
||||
(let walk ((x val))
|
||||
(cond
|
||||
[(eq? var x) #t]
|
||||
[(pair? x) (or (walk (car x)) (walk (cdr x)))]
|
||||
[(vector? x) (ormap walk (vector->list x))]
|
||||
[(struct? x) (walk (struct->vector x #f))]
|
||||
[else #f])))
|
||||
|
||||
;; Variable Any Subst -> Subst
|
||||
(define (extend-subst var val env)
|
||||
(cond
|
||||
[(eq? var val)
|
||||
;; Avoid trivial tautologies. Less trivial ones are not detected,
|
||||
;; but are harmless.
|
||||
env]
|
||||
[(occurs? var val)
|
||||
;; Occurs check.
|
||||
#f]
|
||||
[else
|
||||
(cons (cons var val) env)]))
|
||||
|
||||
;; Any Subst Set<Variable> -> Any
|
||||
(define (chase x env seen)
|
||||
(if (variable? x)
|
||||
(cond [(set-member? seen x) x]
|
||||
[(assq x env) => (lambda (cell) (chase (cdr cell) env (set-add seen x)))]
|
||||
[else x])
|
||||
x))
|
||||
|
||||
;; Any Any -> Subst
|
||||
(define (unify a b)
|
||||
(unify/env a b '()))
|
||||
|
||||
;; Any Any Subst -> Subst
|
||||
(define (unify/env a0 b0 env)
|
||||
(let walk ((a0 a0) (b0 b0) (env env))
|
||||
(and env
|
||||
(let ((a (chase a0 env (set)))
|
||||
(b (chase b0 env (set))))
|
||||
(cond
|
||||
[(variable? a) (extend-subst a b env)]
|
||||
[(variable? b) (extend-subst b a env)]
|
||||
[(and (pair? a) (pair? b))
|
||||
(walk (car a) (car b) (walk (cdr a) (cdr b) env))]
|
||||
[(and (vector? a) (vector? b) (= (vector-length a) (vector-length b)))
|
||||
(for/fold ([env env]) ([ea a] [eb b]) (walk ea eb env))]
|
||||
[(and (struct? a) (struct? b))
|
||||
(walk (struct->vector a #f) (struct->vector b #f) env)]
|
||||
[else (and (equal? a b) env)])))))
|
||||
|
||||
;; Any -> (values Any AList<Symbol,Variable>)
|
||||
;; Converts upper-case symbols to variables, making sure that
|
||||
;; eq? symbols map to eq? variables.
|
||||
(define (upper-case-symbols->variables x)
|
||||
(let walk ((x x) (env '()))
|
||||
(cond
|
||||
[(upper-case-symbol? x)
|
||||
(cond [(assq x env) => (lambda (cell) (values (cdr cell) env))]
|
||||
[else (let ((v (variable x))) (values v (cons (cons x v) env)))])]
|
||||
[(pair? x)
|
||||
(define-values (a env1) (walk (car x) env))
|
||||
(define-values (d env2) (walk (cdr x) env1))
|
||||
(values (cons a d) env2)]
|
||||
[(vector? x)
|
||||
(define result (make-vector (vector-length x)))
|
||||
(values result (for/fold ([env env]) ([i (vector-length x)])
|
||||
(define-values (val env1) (walk (vector-ref x i) env))
|
||||
(vector-set! result i val)
|
||||
env1))]
|
||||
[(struct? x) (struct-map/accumulator walk env x)]
|
||||
[else (values x env)])))
|
||||
|
||||
;; Any -> Any
|
||||
(define (upper-case-symbols->canonical t)
|
||||
(define env (make-hash)) ;; cheeky use of mutation
|
||||
(let walk ((t t))
|
||||
(cond
|
||||
[(or (upper-case-symbol? t) (wild? t))
|
||||
(cond [(hash-ref env t #f)]
|
||||
[else (define v (canonical-variable (hash-count env))) (hash-set! env t v) v])]
|
||||
[(pair? t) (cons (walk (car t)) (walk (cdr t)))]
|
||||
[(vector? t) (list->vector (map walk (vector->list t)))]
|
||||
[(struct? t) (struct-map walk t)]
|
||||
[else t])))
|
||||
|
||||
;; Any -> Boolean
|
||||
(define (upper-case-symbol? x)
|
||||
(and (symbol? x)
|
||||
(let ((name (symbol->string x)))
|
||||
(and (positive? (string-length name))
|
||||
(char-upper-case? (string-ref name 0))))))
|
||||
|
||||
;; AList<A,B> -> AList<B,A>
|
||||
(define (flip-env env)
|
||||
(map (lambda (x) (cons (cdr x) (car x))) env))
|
||||
|
||||
;; Any Any -> Subst
|
||||
;; Like unify after upper-case-symbols->variables on both arguments.
|
||||
(define (unify/vars a b)
|
||||
(define-values (processed env) (upper-case-symbols->variables (cons a b)))
|
||||
(define s (unify (car processed) (cdr processed)))
|
||||
(and s (apply-subst s env)))
|
||||
|
||||
;; Any Any -> Subst
|
||||
;; Like unify-match after upper-case-symbols->variables on both
|
||||
;; arguments, extracting bindings only from the first argument.
|
||||
(define (unify-match/vars a b)
|
||||
(define-values (pa a-env) (upper-case-symbols->variables a))
|
||||
(define-values (pb b-env) (upper-case-symbols->variables b))
|
||||
(define s (unify pa pb))
|
||||
(and s (apply-subst s a-env)))
|
||||
|
||||
;; Utility used by freshen and canonicalize below.
|
||||
;; Must visit the term in the order specified by canonicalize
|
||||
;; below. Here we rely both upon Racket's left-to-right evaluation
|
||||
;; order and upon defined struct-mappers traversing their arguments in
|
||||
;; some deterministic order.
|
||||
(define (freshen* t var-handler canon-handler)
|
||||
(define env (make-hash)) ;; cheeky use of mutation
|
||||
(let walk ((t t))
|
||||
(cond
|
||||
[(wild? t)
|
||||
(cond [(hash-ref env t #f)]
|
||||
[else (define v ((if (canonical-variable? t) canon-handler var-handler) t env))
|
||||
(hash-set! env t v)
|
||||
v])]
|
||||
[(pair? t) (cons (walk (car t)) (walk (cdr t)))]
|
||||
[(vector? t) (list->vector (map walk (vector->list t)))]
|
||||
[(struct? t) (struct-map walk t)]
|
||||
[else t])))
|
||||
|
||||
;; Any -> Any
|
||||
;;
|
||||
;; Freshens a term by substituting out variables in the term with
|
||||
;; fresh variables to produce an arbitrary member of the term's
|
||||
;; alpha-equivalence-class that shares no variables with the original.
|
||||
;;
|
||||
;; Treats canonical-variables just like regular ones, freshening them
|
||||
;; with new ordinary (non-canonical) variables.
|
||||
(define (freshen t)
|
||||
(freshen* t
|
||||
(lambda (var env) (variable (variable-info var)))
|
||||
(lambda (var env) (variable (canonical-variable-index var)))))
|
||||
|
||||
;; Any -> Any
|
||||
;;
|
||||
;; Canonicalizes a term by substituting out variables in the term with
|
||||
;; canonical-variables to produce a canonical member of the term's
|
||||
;; alpha-equivalence-class.
|
||||
;;
|
||||
;; Canonical variables are used in a structurally-determined order
|
||||
;; related to print order: generally, all unseen variables to the left
|
||||
;; of a term's print representation are given canonical equivalents
|
||||
;; before those to the right.
|
||||
;;
|
||||
;; Canonical-variables may not appear in the input term.
|
||||
(define (canonicalize t)
|
||||
(freshen* t
|
||||
(lambda (var env) (canonical-variable (hash-count env)))
|
||||
(lambda (var env) (canonical-variable (hash-count env)))))
|
||||
|
||||
;; Any Any -> Any
|
||||
;; If the arguments unify, applies the substitution to one of them,
|
||||
;; yielding a most general unifier, and then freshens the result.
|
||||
(define (mgu-freshen a b)
|
||||
(define sub (unify a b))
|
||||
(and sub (freshen (apply-subst sub a))))
|
||||
|
||||
;; Any Any -> Any
|
||||
;; If the arguments unify, applies the substitution to one of them,
|
||||
;; yielding a most general unifier, and then canonicalizes the result.
|
||||
(define (mgu-canonical a b)
|
||||
(define sub (unify a b))
|
||||
(and sub (canonicalize (apply-subst sub a))))
|
||||
|
||||
;; Subst Any -> Any
|
||||
(define (apply-subst env x)
|
||||
(let walk ((x0 x))
|
||||
(define x (chase x0 env (set)))
|
||||
(cond
|
||||
[(pair? x) (cons (walk (car x)) (walk (cdr x)))]
|
||||
[(vector? x) (list->vector (map walk (vector->list x)))]
|
||||
[(struct? x) (struct-map walk x)]
|
||||
[else x])))
|
||||
|
||||
;; True iff a is a specialization (or instance) of b.
|
||||
(define (specialization? a b)
|
||||
(let walk ((a a) (b b))
|
||||
(cond
|
||||
[(wild? b) #t]
|
||||
[(wild? a) #f]
|
||||
[(and (pair? a) (pair? b))
|
||||
(and (walk (car a) (car b)) (walk (cdr a) (cdr b)))]
|
||||
[(and (vector? a) (vector? b) (= (vector-length a) (vector-length b)))
|
||||
(for/and ([aa a] [bb b]) (walk aa bb))]
|
||||
[(and (struct? a) (struct? b))
|
||||
(walk (struct->vector a #f) (struct->vector b #f))]
|
||||
[else (equal? a b)])))
|
||||
|
||||
(require racket/trace)
|
||||
(trace ;;unify/env
|
||||
;;upper-case-symbols->variables
|
||||
;;apply-subst
|
||||
;;specialization?
|
||||
)
|
Loading…
Reference in New Issue