module preprocess

-- 전처리 파이프라인의 단계
abstract sig Stage {
  order: one Int
}

one sig Embed extends Stage {} { order = 1 }
one sig PrivateTag extends Stage {} { order = 2 }
one sig WikilinkReplace extends Stage {} { order = 3 }
one sig SmartQuote extends Stage {} { order = 4 }

-- 마크다운 토큰: 코드 블록 내부이거나 아니거나
sig Token {
  inCodeBlock: one Bool,
  processedBy: set Stage
}

-- 코드 블록 내부의 토큰은 wikilink 변환 대상이 아님
fact codeBlockProtection {
  all t: Token | t.inCodeBlock = True implies
    WikilinkReplace not in t.processedBy
}

-- 임베딩은 항상 private 태그보다 먼저 처리됨
-- (임베딩된 콘텐츠의 prv 태그가 올바르게 제거되려면)
fact embedBeforePrivate {
  Embed.order < PrivateTag.order
}

-- private 태그는 wikilink보다 먼저 처리됨
-- (prv 태그 안의 wikilink가 불필요하게 변환되지 않으려면)
fact privateBeforeWikilink {
  PrivateTag.order < WikilinkReplace.order
}

-- 코드 블록 보호가 위반되면: wikilink가 코드 안에서도 변환됨
assert codeBlockSafe {
  no t: Token | t.inCodeBlock = True and WikilinkReplace in t.processedBy
}

-- 파이프라인 순서가 전순서(total order)임
assert pipelineIsTotalOrder {
  all disj s1, s2: Stage | s1.order != s2.order
}

check codeBlockSafe for 5
check pipelineIsTotalOrder for 5 but 6 Int

abstract sig Bool {}
one sig True, False extends Bool {}