@@ -90,29 +90,50 @@ const noSucc: readonly string[] = [];
9090 * overflow, and 3-colours each variable so it is visited once: O(vars + total value size), like Hyperon's
9191 * bitset walk. `atomVars` is cached by object identity, so a DAG-shared value is scanned once. */
9292export function hasLoop ( b : Bindings ) : boolean {
93+ const quick = relQuickLoop ( b , b . length ) ;
94+ if ( quick !== undefined ) return quick ;
95+ const vals = firstVals ( b ) ;
96+ return loopReachableFrom ( vals , vals . keys ( ) ) ;
97+ }
98+
99+ // The self-relation quick checks over the first `count` relations: a self-equality or self-value is a
100+ // loop outright (true); no non-ground value among them means no graph edge to walk (false); otherwise
101+ // the colour DFS must decide (undefined).
102+ function relQuickLoop ( b : Bindings , count : number ) : boolean | undefined {
93103 let needsGraph = false ;
94- for ( const r of b ) {
104+ for ( let i = 0 ; i < count ; i ++ ) {
105+ const r = b [ i ] ! ;
95106 if ( r . tag === "eq" ) {
96107 if ( r . x === r . y ) return true ;
97108 } else {
98109 if ( r . a . kind === "var" && r . a . name === r . x ) return true ;
99110 if ( ! r . a . ground ) needsGraph = true ;
100111 }
101112 }
102- if ( ! needsGraph ) return false ;
113+ return needsGraph ? undefined : false ;
114+ }
115+
116+ // First (most recently prepended) value per variable, matching `lookupVal`'s precedence.
117+ function firstVals ( b : Bindings ) : Map < string , Atom > {
103118 const vals = new Map < string , Atom > ( ) ;
104119 for ( const r of b ) if ( r . tag === "val" && ! vals . has ( r . x ) ) vals . set ( r . x , r . a ) ;
105- // 3-colour iterative DFS over the variable graph. A variable's successors are the distinct variables in
106- // its bound value; a grey (on the current path) revisit is a back-edge, i.e. a cycle. color: 1 = grey
107- // (on path), 2 = black (done); absent = white (unvisited).
120+ return vals ;
121+ }
122+
123+ // 3-colour iterative DFS over the variable graph, rooted at `seeds`. A variable's successors are the
124+ // distinct variables in its bound value; a grey (on the current path) revisit is a back-edge, i.e. a
125+ // cycle. color: 1 = grey (on path), 2 = black (done); absent = white (unvisited). Seeds bound to a
126+ // ground value (or unbound) root nothing.
127+ function loopReachableFrom ( vals : ReadonlyMap < string , Atom > , seeds : Iterable < string > ) : boolean {
108128 const color = new Map < string , 1 | 2 > ( ) ;
109129 const succ = ( x : string ) : readonly string [ ] => {
110130 const v = vals . get ( x ) ;
111131 return v === undefined || v . ground ? noSucc : atomVars ( v ) ;
112132 } ;
113133 const stack : Array < { v : string ; kids : readonly string [ ] ; i : number } > = [ ] ;
114- for ( const [ x , a ] of vals ) {
115- if ( a . ground ) continue ;
134+ for ( const x of seeds ) {
135+ const a = vals . get ( x ) ;
136+ if ( a === undefined || a . ground ) continue ;
116137 if ( color . get ( x ) === 2 ) continue ;
117138 color . set ( x , 1 ) ;
118139 stack . push ( { v : x , kids : succ ( x ) , i : 0 } ) ;
@@ -134,6 +155,41 @@ export function hasLoop(b: Bindings): boolean {
134155 return false ;
135156}
136157
158+ /** `hasLoop` for a `merge` result whose base was already loop-free.
159+ *
160+ * `merge` builds every output by prepending relations onto its base: `addVarBinding` prepends a value
161+ * relation only for a variable the current set leaves unbound (a bound variable either no-ops or goes
162+ * through `reconcile`, whose own extensions bottom out in the same prepend-or-no-op steps), and
163+ * `addVarEquality` prepends an equality. The base is therefore a reference-identical suffix of the
164+ * result, no prepend can shadow a base variable's first value, and the base's first-value graph embeds
165+ * unchanged in the result's. A cycle in the result must then pass through a prepended value binding,
166+ * so running the colour DFS only from the prepended variables is answer-equivalent to the full scan.
167+ * The self-relation quick checks run on the prepended prefix alone for the same reason. Anything that
168+ * is not a reference-identical suffix extension falls back to the full `hasLoop`.
169+ *
170+ * Callers must pass the exact base the result was merged from, and that base must itself be loop-free;
171+ * the equivalence fuzz in match.test.ts pins this predicate to `hasLoop` over merge outputs. */
172+ export function hasLoopFromBase ( merged : Bindings , base : Bindings ) : boolean {
173+ const added = merged . length - base . length ;
174+ if ( merged === base || added === 0 ) return false ; // no-op merge: the base was loop-free
175+ if (
176+ added < 0 ||
177+ ( base . length > 0 &&
178+ ( merged [ added ] !== base [ 0 ] || merged [ merged . length - 1 ] !== base [ base . length - 1 ] ) )
179+ )
180+ return hasLoop ( merged ) ; // not a suffix extension of `base`: no incremental argument
181+ // Quick checks over the prepended prefix only; all-ground prepends add no edges, and the base's
182+ // graph is acyclic by precondition.
183+ const quick = relQuickLoop ( merged , added ) ;
184+ if ( quick !== undefined ) return quick ;
185+ const seeds : string [ ] = [ ] ;
186+ for ( let i = 0 ; i < added ; i ++ ) {
187+ const r = merged [ i ] ! ;
188+ if ( r . tag === "val" && ! r . a . ground ) seeds . push ( r . x ) ;
189+ }
190+ return loopReachableFrom ( firstVals ( merged ) , seeds ) ;
191+ }
192+
137193/** Bind `$x ← a`, dropping any previous value binding for `$x`. Raw: no consistency check. */
138194export function addValRaw ( b : Bindings , x : string , a : Atom ) : Bindings {
139195 const first = firstValIndex ( b , x ) ;
0 commit comments