diff --git a/lib/datalog/scoreboard.json b/lib/datalog/scoreboard.json index c8a61bf7..4115dc2e 100644 --- a/lib/datalog/scoreboard.json +++ b/lib/datalog/scoreboard.json @@ -1,12 +1,12 @@ { "lang": "datalog", - "total_passed": 256, + "total_passed": 257, "total_failed": 0, - "total": 256, + "total": 257, "suites": [ {"name":"tokenize","passed":30,"failed":0,"total":30}, {"name":"parse","passed":22,"failed":0,"total":22}, - {"name":"unify","passed":28,"failed":0,"total":28}, + {"name":"unify","passed":29,"failed":0,"total":29}, {"name":"eval","passed":38,"failed":0,"total":38}, {"name":"builtins","passed":23,"failed":0,"total":23}, {"name":"semi_naive","passed":8,"failed":0,"total":8}, @@ -16,5 +16,5 @@ {"name":"magic","passed":36,"failed":0,"total":36}, {"name":"demo","passed":21,"failed":0,"total":21} ], - "generated": "2026-05-10T21:16:53+00:00" + "generated": "2026-05-11T07:20:07+00:00" } diff --git a/lib/datalog/scoreboard.md b/lib/datalog/scoreboard.md index 1055a8f9..3e5c0e4e 100644 --- a/lib/datalog/scoreboard.md +++ b/lib/datalog/scoreboard.md @@ -1,12 +1,12 @@ # datalog scoreboard -**256 / 256 passing** (0 failure(s)). +**257 / 257 passing** (0 failure(s)). | Suite | Passed | Total | Status | |-------|--------|-------|--------| | tokenize | 30 | 30 | ok | | parse | 22 | 22 | ok | -| unify | 28 | 28 | ok | +| unify | 29 | 29 | ok | | eval | 38 | 38 | ok | | builtins | 23 | 23 | ok | | semi_naive | 8 | 8 | ok | diff --git a/lib/datalog/tests/unify.sx b/lib/datalog/tests/unify.sx index 873cc655..3db114ed 100644 --- a/lib/datalog/tests/unify.sx +++ b/lib/datalog/tests/unify.sx @@ -129,6 +129,15 @@ ((s2 (dl-unify (quote Y) (quote tom) s1))) (dl-walk (quote X) s2))) (quote tom)) + + ;; Walk with circular substitution must not infinite-loop. + ;; Cycles return the current term unchanged. + (dl-ut-test! + "walk circular subst no hang" + (let ((s (dl-bind (quote B) (quote A) + (dl-bind (quote A) (quote B) (dl-empty-subst))))) + (dl-walk (quote A) s)) + (quote A)) (dl-ut-test! "apply subst on tuple" (let diff --git a/lib/datalog/unify.sx b/lib/datalog/unify.sx index 7313a603..d5de7eda 100644 --- a/lib/datalog/unify.sx +++ b/lib/datalog/unify.sx @@ -33,16 +33,28 @@ ;; variable. The result is either a non-variable term or an unbound var. (define dl-walk + (fn (term subst) (dl-walk-aux term subst (list)))) + +;; Internal: walk with a visited-var set so circular substitutions +;; (from raw dl-bind misuse) don't infinite-loop. Cycles return the +;; current term unchanged. +(define + dl-walk-aux (fn - (term subst) + (term subst visited) (if (dl-var? term) (let ((name (symbol->string term))) - (if - (and (dict? subst) (has-key? subst name)) - (dl-walk (get subst name) subst) - term)) + (cond + ((dl-member? name visited) term) + ((and (dict? subst) (has-key? subst name)) + (let ((seen (list))) + (do + (for-each (fn (v) (append! seen v)) visited) + (append! seen name) + (dl-walk-aux (get subst name) subst seen)))) + (else term))) term))) ;; Bind a variable symbol to a value in subst, returning a new subst.