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)))
        ((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 substitute

MiniKanren core reify-name

scheme size-s


(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)