Press n or j to go to the next uncovered block, b, p or k for the previous block.
| 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 | 1x 1x 1x 1x 1x 1x 1x 1x 1x 1x 1x 1x 1x 1x 1x 1x 10x 10x 10x 10x 10x 10x 10x 10x 10x 20x 10x 10x 10x 9x 9x 9x 9x 20x 9x 9x 9x 9x 9x 9x 9x 9x 9x 9x 9x 9x 9x 9x 9x 9x 9x 9x 9x 9x 9x 9x 10x 10x 10x | import type { ConstructionState, IntersectionCandidate } from '../types'
import type { FactStore } from './factStore'
import type { EqualityFact } from './facts'
import { distancePair } from './facts'
import { addFact } from './factStore'
import { getCircle, getPoint } from './constructionState'
/**
* When a point is marked as an intersection involving circles,
* auto-derive Def.15 facts: dist(center, newPoint) = dist(center, radiusPoint)
*
* For each element in [candidate.ofA, candidate.ofB] that is a circle:
* - Look up circle.centerId, circle.radiusPointId
* - Add fact: dist(centerId, newPointId) = dist(centerId, radiusPointId)
*/
export function deriveDef15Facts(
candidate: IntersectionCandidate,
newPointId: string,
state: ConstructionState,
store: FactStore,
atStep: number
): EqualityFact[] {
const allNewFacts: EqualityFact[] = []
for (const elementId of [candidate.ofA, candidate.ofB]) {
if (!elementId.startsWith('cir-')) continue
const circle = getCircle(state, elementId)
if (!circle) continue
const center = getPoint(state, circle.centerId)
const radiusPt = getPoint(state, circle.radiusPointId)
const newPt = getPoint(state, newPointId)
if (!center || !radiusPt || !newPt) continue
const left = distancePair(circle.centerId, newPointId)
const right = distancePair(circle.centerId, circle.radiusPointId)
const centerLabel = center.label
const newLabel = newPt.label
const radiusLabel = radiusPt.label
const statement = `${centerLabel}${newLabel} = ${centerLabel}${radiusLabel}`
const justification = `Def.15: ${newLabel} lies on circle centered at ${centerLabel} through ${radiusLabel}`
const newFacts = addFact(
store,
left,
right,
{ type: 'def15', circleId: elementId },
statement,
justification,
atStep
)
allNewFacts.push(...newFacts)
}
return allNewFacts
}
|