Kibit와 clojure.core.logic

Clojure Advent Calendar 2020 20일째 보도다.(하지만, 25일을 대폭 연기했다. 메리 크리스마스.
예전에 정적 해석 도구인 키비트를 봤으면 코어.logic를 사용했기 때문에 어떻게 사용했는지.
논리 프로그래밍 언어는 규칙을 선언적으로 제정하고 해역하는 데 전문적으로 쓰이는 언어다.
나는 Proog라는 언어가 매우 유명하다고 생각한다.
그리고 코어.logic는 Scheme의 논리 프로그램 설계 DSL이고 미니 Kanren의 Clojure가 실현한다.
core.나는 다른 logic의 실용적인 예를 보았지만 낡은 것이 많아서 깊이 파고들지 못했다.
언어 처리 시스템의 예에서 코어 날짜, 시간 라이브러리의 규칙을 풀 수 있습니다.로직으로 기술해서 계산을 해결하는 용법인 것 같습니다.

Kibit

Kibit는 Clojure의 정적 분석 도구입니다.
입력한 소스 코드가 좋지 않은 부분을 찾으면 수정 방법을 되돌려줍니다.
내부에서 전용 기법을 사용하여 원본 코드의 좋지 않은 예를 모델로 기술하고 좋은 예도 마찬가지로 기술하며 미리 그룹으로 유지한다(있다).
그리고 입력한 원본 코드가 기술 모드에 부합되면 알려 줍니다.
패턴의 기법례는 이렇다.
이것은 (+ x 1) 등 코드를 (inc x) 모델로 설정한 코드다.?x처럼?시작 기호는 모든 표현식이 일치하는 와일드카드입니다.
그리고 좋은 코드의 패턴은 같습니까?시작 기호가 있으면 일치하는 기호를 삽입합니다.

(defrules rules
  [(+ ?x 1) (inc ?x)]
  略)

이 일치하는 부분에 코어를 배치합니다.logic 을 사용합니다.
core.logic에서 앞에서 설명한 어댑터 부분은 논리 변수로 다음과 같다.
x는 논리 변수다.

(run* [x] (== (list '+ x 1) '(+ (* 2 3) 1)));=> ((* 2 3))

kibit의 모드 기법의?시작된 기호는 내부에 있습니다.logic의 논리 변수 (lvar) 로 변환해서 사용합니다.이 전환은closure입니다.core.logic.unifier/prep 함수를 사용합니다.sequence의 재난?시작된 symbol을 lvar로 변환합니다.
다음은 전개에 관한 부분이다.
마찬가지로 논리 변수를 좋은 코드 모드에 삽입하고 이전의 나쁜 코드 모드가 제약하는 논리 변수와 대응하는 부분을 삽입한다.그 다음은 결과에 대응하도록 하는 것이다.

(run* [res]
  (fresh [x]
    (== (list '+ x 1) '(+ (* 2 3) 1))
    (== (list 'inc x) res)))
;-> ((inc (* 2 3)))