Lueng의 RegExp 라이브러리가 Isabelle/ML에서 작동합니까? Isabelle/ML에 사용할 regex lib devs가 있습니까?

Question

1 : 누구나 알고 있습니까? Lueng's RegExp library은 Isabelle/ML과 함께 작동합니까?

Q2 : 개발자가 Isabelle/ML 용으로 사용하는 표준 정규식 라이브러리가 있습니까?

필자는 스칼라를 배우기위한 큰 계획을 가지고 있었는데, 나의 주요 응용 프로그램은 TEX 파일을 생성하기 위해 THY를 처리하려고했다.

나는 스칼라에 대한 생각을 좋아하지만, 그것이 얼마나 위대한 지에 대해 생각한 후에, 나는 그것을 배우는 동기가 전혀 없다. 왜냐하면 그 힘에 대해 배우는 것은 몇 달 간의 일과 계속되는 연구를 포함하기 때문이다. 내 목표는 프로그래밍을 배우는 것이 아니라 이자벨 (Isabelle)과 수학을 공부하는 것입니다.

저는 이사벨/ML에 큰 변화를주었습니다. ML을 배우고 몇 개월 동안 계속해서 공부하면 이사벨 증명과 저수준 설정에 사용할 수있는 거대한 도구가 될 것이기 때문에 문법 같은 것.

시작하기 전에 ML을 선택하지 않은 이유는 스크립팅을위한 스칼라의 모든 이점을 가지고 있지 않기 때문입니다.하지만 ML 작업을 할 수 있어야합니다.

거대한 걱정이 하나 있습니다. 그래야 정규 표현식 라이브러리를 사용할 수 있습니다. 정규 표현식을 사용하지 않으면 반복 할 수 없습니다. 위의 정규식 라이브러리의 페이지에서

는 웹 페이지에이 말한다 :이 섹션의

모든 코드는 뉴저지의 표준 ML의 최신 작업 버전에서 실행됩니다.

좋은 징조인지 아니면 나쁜 징조인지는 확실하지 않습니다. 이 시점에서 Isabelle/ML에 대한 간단한 정보를 아는 것은 어렵습니다. 그 중 가장 위대한 ML{*...*}과 ML "..." 명령과 내가 PIDE의 다음 릴리스에서 보았던 ML 지원에 대한 의견이 있습니다.

수 주일이 걸릴 수도 있지만, 나 자신을 위해이 모든 것을 알아낼 것입니다.하지만 누군가가 작동하는지 지금 알 수 있으면 걱정할 필요가 없습니다.

많은 사람들이 이것을 알게 될 것입니다. 그러나 다른 사람들의 기고와 함께 Christian Urban의 Isabelle Programming Tutorial이 있습니다. 거기에 무엇이 있는지를 아는 것이 좋을 것입니다.

Answer 1

뉴저지의 표준 ML에 대한 라이브러리입니다. 이름에는 "표준 ML"이 있지만 컴파일 관리자 CM과 같은 많은 비표준 부가 기능이 있습니다.

나는 Isabelle/ML을 위해 너무 많은 시간을 할 가치가 있다고 생각하지 않는다. 예 : 파서 결합 자 (structure Scan)는 스타일이 약간 더 일반적이고 기능적입니다.

Answer 2

나는 이것도 살펴 보았고 기본 라이브러리가 아닌 SML/NJ의 비표준 Array 라이브러리를 사용하는 것으로 보입니다. 변환은 아마도 그러나 아주 간단합니다.