fix: support between predicate in FOL dense DSL

- grammar.ts: add 'between' to isKeywordThatCanBePredicate() so the parser
  recognizes it as a valid predicate keyword in forall/exists formula bodies
- compiler.ts: add special case in compileDenseFOLToFormula for
  between(, min, max, dimension?) that extracts numeric args into
  options ({min, max, dimension}) instead of dropping them in the generic
  arg loop. The existing betweenPredicate evaluator already handles these.
- fol-dense-combinations.test.ts: replace GAP test with two verified-working
  tests for between and between with dimension
This commit is contained in:
John Dvorak
2026-05-22 10:48:26 -07:00
parent 1bc92e1f7d
commit 1ac30c6e18
3 changed files with 46 additions and 6 deletions
+29
View File
@@ -801,6 +801,35 @@ export function compileDenseFOLToFormula(dslFormula: DslFormulaNode): FormulaNod
}
case 'PredicateCall': {
const pc = node as DslPredicateCall
// between($x, min, max, dimension?): extract numeric args into
// options so the betweenPredicate evaluator can consume them.
// The generic arg loop drops numbers, so we handle this up-front.
if (pc.name === 'between') {
const options: Record<string, number | string> = {}
const compiledArgs: VariableRef[] = []
for (let i = 0; i < pc.args.length; i++) {
const arg = pc.args[i]
if (i === 0) {
compiledArgs.push(convertTerm(arg) as VariableRef)
} else if (typeof arg === 'number') {
if (i === 1) options.min = arg
else if (i === 2) options.max = arg
} else if (typeof arg === 'string') {
options.dimension = arg
}
}
return {
type: 'FormulaNode',
kind: 'predicate',
predicate: 'between',
args: compiledArgs,
...(Object.keys(options).length > 0 ? { options } : {}),
} as FormulaNode
}
const implicitBindings: TupleBinding[] = []
const compiledArgs: VariableRef[] = []
@@ -436,13 +436,24 @@ describe('FOL Dense DSL - Solver Formula Lowering', () => {
describe('FOL Dense DSL - Gap Detection', () => {
// These tests document known gaps in the dense DSL FOL support
it('GAP: dense DSL does not support size between assertions', () => {
// between is only in fluent API, not dense DSL grammar
it('between parses as predicate in dense DSL', () => {
const source = `forall $btn in elements('.button'):\n between($btn, 44, 100)`
const result = parseSpec(source)
// May parse as predicate call or fail
assert.ok(result.diagnostics.length > 0 || result.ast.children.length === 0,
'Expected parse failure or no formula for between in dense DSL')
assert.strictEqual(result.diagnostics.length, 0, `Expected no diagnostics but got: ${result.diagnostics.map(d => d.message).join(', ')}`)
const formula = getFormula(result.ast)
assert.ok(formula, 'Expected formula for between in dense DSL')
const compiled = compileDenseFOLToFormula(formula!)
assert.ok(compiled, 'Expected compiled formula for between')
})
it('between with dimension parses as predicate in dense DSL', () => {
const source = `forall $btn in elements('.button'):\n between($btn, 44, 100, 'width')`
const result = parseSpec(source)
assert.strictEqual(result.diagnostics.length, 0, `Expected no diagnostics but got: ${result.diagnostics.map(d => d.message).join(', ')}`)
const formula = getFormula(result.ast)
assert.ok(formula, 'Expected formula for between with dimension in dense DSL')
const compiled = compileDenseFOLToFormula(formula!)
assert.ok(compiled, 'Expected compiled formula for between with dimension')
})
it('separatedFrom parses as relation predicate in dense DSL', () => {
+1 -1
View File
@@ -665,7 +665,7 @@ export class GrammarParser {
// Spatial aliases
'beside', 'nextTo', 'adjacent', 'touching', 'near', 'under', 'within',
// Size predicates that can appear in FOL formula bodies
'width', 'height', 'size',
'width', 'height', 'size', 'between',
]
return predicateKinds.includes(kind)
}