MiniKanren core reify-s
Returns a reified-name substitution in which each variable in v is associated with its reified name.
(define reify-s
(lambda (v s) ;; v refers to our variables, s are our substiutions
(let ((v (walk v s)))
(cond
((var? v) ;; If v is a unbound variable,
(ext-s v (reify-name (size-s s)) s)) ;; Extend the substitution list s to include its reified name
;; Here we use (size-s s) as the variable hash, since whenever we
;; add a new variable (size-s s) is updated
;; Thus for every new variable we add, it has a unique
;; reified name
((pair? v) ;; Otherwise if v is a pair,
(reify-s (cdr v) ;; reify the tail of the pair with
(reify-s (car v) s))) ;; Updated `s`
(else s))))) ;; Otherwise we can just return our old list of substitutions,
;; since there is nothing to substituteExamples
(let (r (w x y)) ;; bind r to (w x y)
(walk* (reify-s r empty-s))) ;; Generate 3 unique reified names for these
;; (_0 _1 _2)(let (r (u (v (w x) y) x))
(walk* r (reify-s r empty-s)))
;; (_0 (_1 (_2 _3) _4) _3);; We use UPPERCASE letters to denote symbols
(let ((s ((y . (z w C w)) (x . y) (z . A)))) ;; initial substitution
(let ((r (walk* x s))) ;; r associates to the list (A w C w)
(walk* r (reify-s r empty-s)))) ;; (reify-s r empty-s) becomes ((w . _0))
;; walk* (A w C w) ((w . _0))
;; becomes (A _0 c _0)