해석없이 로케일에서 코드 생성

Question

해석없이 직접 locale 정의의 코드를 생성하고 싶습니다. 예 :

(* A locale, from the code point of view, similar to a class *) 
locale MyTest = 
    fixes L :: "string list" 
    assumes distinctL: "distinct L" 
    begin 
    definition isInL :: "string => bool" where 
     "isInL s = (s ∈ set L)" 
    end 

가정 사항 MyTest 대한 실행 인스턴스화 그들을

definition "can_instance_MyTest L = distinct L" 
lemma "can_instance_MyTest L = MyTest L" 
    by(simp add: MyTest_def can_instance_MyTest_def) 
export_code can_instance_MyTest in Scala file - 

I 임의 MyTest 대한 isInL 정의를 실행하는 함수를 정의 할 수 위해 I 코드를 생성 할 수있다.

definition code_isInL :: "string list ⇒ string ⇒ bool option" where 
"code_isInL L s = (if can_instance_MyTest L then Some (MyTest.isInL L s) else None)" 

lemma "code_isInL L s = Some b ⟷ MyTest L ∧ MyTest.isInL L s = b" 
    by(simp add: code_isInL_def MyTest_def can_instance_MyTest_def) 

그러나, 코드 내보내기 실패

export_code code_isInL in Scala file - 
No code equations for MyTest.isInL 

가 왜 그런 일을 할 하시겠습니까? 예 : valid_graph의 문맥에서 locale으로 작업하고 있습니다. here하지만 한정되어 있습니다. 그래프가 유효한지 테스트하는 것은 쉽습니다. 이제 그래프 알고리즘의 코드를 Scala로 내보내려고합니다. 물론 코드는 임의의 유효한 그래프에서 실행되어야합니다.

나는이 같은 유사 스칼라 비유 생각 해요 :이 불변을 사용하여 데이터 형식 정제입니다 해결하기

class MyTest(L: List[String]) { 
require(L.distinct) 
def isInL(s: String): Bool = L contains s 
} 

Answer 1

한 가지 방법 (isabelle doc codegen 3.3 절 참조). 따라서 유효성 가정 (귀하의 경우 distinct L)을 새로운 유형으로 옮길 수 있습니다. 다음 예제를 고려하십시오.

typedef 'a dlist = "{xs::'a list. distinct xs}" 
morphisms undlist dlist 
proof 
    show "[] ∈ ?dlist" by auto 
qed 

이 요소는 고유 한 요소가있는 모든 목록 인 새 형식을 정의합니다. 코드 생성기에이 새로운 유형을 명시 적으로 설정해야합니다.

lemma [code abstype]: "dlist (undlist d) = d" 
    by (fact undlist_inverse) 

다음, 로케일에서 우리는 (새로운 유형의 모든 요소가 그것을 보장하기 때문에 "무료"가정을 가지고 있지만, 어떤 점에서 우리는 별개의 요소 목록에서 작업의 기본 설정을 들어 내야 ~'a dlist s).

이 시점에서 우리는 (무조건적인) 방정식을 코드 생성기에 제공 할 수 있습니다.

lemma [code]: "MyTest.isInL L s ⟷ s ∈ set (undlist L)" 
    by (fact MyTest.isInL_def) 

export_code MyTest.isInL in Haskell file - 

Answer 2

나는 chris의 조언 덕분에 방법을 발견했다.

인스턴스화 전제/가정 테스트 함수를 정의 MyTest

definition "can_instance_MyTest L = distinct L" 

term MyTest가 MyTest 이것이 MyTest에 파라미터 테스트 경우 소요 술어가 있음을 의미 형 string list => bool, 인 것이 밝혀 명령 이 매개 변수는 MyTest의 가정을 충족시킵니다. MyTest을 실행 가능한 인스턴스 테스터로 대체하는 코드 공식 ([code])을 소개합니다. 코드 생성기는 다음과 같은 경우에 대한 코드를 생성 할 수 있습니다.

def myTest(l: List[String]): Boolean = l.isDistinct 

이제 우리는 isInL에 대한 실행 코드가 필요합니다

def can_instance_MyTest[A : HOL.equal](l: List[A]): Boolean = 
    Lista.distinct[A](l) 

def myTest: (List[String]) => Boolean = 
    (a: List[String]) => can_instance_MyTest[String](a) 

더 읽기 의사 코드 :

lemma [code]: "MyTest = can_instance_MyTest" 
    by(simp add:fun_eq_iff MyTest_def can_instance_MyTest_def) 

export_code MyTest in Scala file - 

MyTest [a,b,c] 우리는 항복 (나는 가독성에 대한 String로 List[Char] 대체) . 사전 정의 된 상수 undefined을 사용합니다. L이 명확하지 않으면이 코드는 예외를 throw합니다.

definition code_isInL :: "string list ⇒ string ⇒ bool" where 
"code_isInL L s = (if can_instance_MyTest L then s ∈ set L else undefined)" 

export_code code_isInL in Scala file - 

우리가 얻을 :

def code_isInL(l: List[String], s:String): Boolean = 
    (if (can_instance_MyTest[String](l)) Lista.member[String](l, s) 
    else sys.error("undefined"))*) 

우리는 단지 code_isInL가 올바른지 보여줄 필요가 :

lemma "b ≠ undefined ⟹ code_isInL L s = b ⟷ MyTest L ∧ MyTest.isInL L s = b" 
    by(simp add: code_isInL_def MyTest_def can_instance_MyTest_def MyTest.isInL_def) 


(* Unfortunately, the other direction does not hold. The price of undefined. *) 
lemma "¬ MyTest L ⟹ code_isInL L s = undefined" 
    by(simp add: code_isInL_def can_instance_MyTest_def MyTest_def)