move: move/affinity 검사 — v0 fast path 완성
보안 정리 (ii) — safe code에서 capability는 복제·위조되지 않는다 — 를 코드로 닫는다. 검사는 전부 함수 로컬 데이터플로우이고 전역 분석이 없다. affinity의 뿌리는 capability다. 필드로 가진 타입은 전이적으로 affine이며 고정점까지 돌려 상호 재귀 타입도 유도한다. 이 전이가 없으면 wrapper 하나를 복사해 capability가 사실상 복제되므로 정리가 깨진다. copyable 선언과 affine 필드의 공존은 오류다. 구현한 규칙: - affine 값은 소유 자리로 갈 때 move된다(own 파라미터, 반환, struct 저장, 컨테이너 삽입, let 바인딩, by-move capture). moved 이후 사용은 오류이고 진단이 어디서 소비됐는지를 말한다 - 분기 병합은 보수적 합집합. 한 분기에서라도 moved면 병합 이후 moved - 빌린 값은 탈출하지 못한다: 반환, struct 저장, 소유 자리로 넘기기 전부 거부 - use의 전염: 빌린 값을 capture한 클로저는 그 자체가 빌린 값이라 소유 자리로 갈 수 없다. 별도의 nonescaping 개념 없이 use 규칙 하나로 닫힌다 - callable affinity: affine 값을 capture한 클로저는 affine fn이며 fn 자리에 갈 수 없다 자율 결정 둘: - 클로저는 mut 바인딩을 capture할 수 없다. spawn만 막는 특수 규칙 대신 일반 규칙으로 뒀다 — v0에 참조가 없으므로 별칭도 조용한 복사도 만들 수 없고, spawn 제한은 이 규칙의 특수 사례가 된다 - v0에 부분 move는 없다. 필드 접근은 빌림이고 결과도 빌린 값이다. affine 필드만 꺼내려면 부분 move 상태 추적이 필요한데 v0가 살 복잡도가 아니다 05를 자족적으로 다시 썼다. affinity의 뿌리가 capability라 자원 타입을 모듈 안에서 정의해야 검사기가 affine임을 유도할 수 있다. 외부 타입은 affine임을 증명할 수 없으므로 copyable로 본다. 이로써 fast path(L0 parse / L1 type·effect·capability·ownership)가 완성됐다. cool check가 처음으로 성공을 선언한다 — 01~04, 06, 07이 exit 0으로 통과한다. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019ZVDeU6KLuUVL3gs18Hm3E
This commit is contained in:
+21
-27
@@ -69,19 +69,27 @@ let typecheck (file : string) : (unit, error list) result =
|
||||
{ file; line = e.pos.line; col = e.pos.col; message = e.msg })
|
||||
rerrors)
|
||||
| [] -> (
|
||||
match Typecheck.check m with
|
||||
let terrors =
|
||||
List.map
|
||||
(fun (e : Typecheck.error) ->
|
||||
{ file; line = e.pos.line; col = e.pos.col; message = e.msg })
|
||||
(Typecheck.check m)
|
||||
in
|
||||
(* move/affinity는 타입·effect와 달리 별도 순회다. 소유하는 성질이
|
||||
다르고 해소를 공유할 지점도 없기 때문이다. *)
|
||||
let merrors =
|
||||
List.map
|
||||
(fun (e : Move.error) ->
|
||||
{ file; line = e.pos.line; col = e.pos.col; message = e.msg })
|
||||
(Move.check m)
|
||||
in
|
||||
match
|
||||
List.sort
|
||||
(fun a b -> compare (a.line, a.col) (b.line, b.col))
|
||||
(terrors @ merrors)
|
||||
with
|
||||
| [] -> Ok ()
|
||||
| terrors ->
|
||||
Error
|
||||
(List.map
|
||||
(fun (e : Typecheck.error) ->
|
||||
{
|
||||
file;
|
||||
line = e.pos.line;
|
||||
col = e.pos.col;
|
||||
message = e.msg;
|
||||
})
|
||||
terrors)))
|
||||
| errors -> Error errors))
|
||||
|
||||
let check (files : string list) : (unit, error list) result =
|
||||
match files with
|
||||
@@ -94,21 +102,7 @@ let check (files : string list) : (unit, error list) result =
|
||||
files
|
||||
|> List.concat
|
||||
in
|
||||
if errors <> [] then Error errors
|
||||
else
|
||||
(* effect 검사까지는 통과했다. 통과했다고 말하지 않는다 — 파이프라인의
|
||||
나머지가 아직 없으므로 검사되지 않은 것이다. *)
|
||||
Error
|
||||
(List.map
|
||||
(fun f ->
|
||||
{
|
||||
file = f;
|
||||
line = 0;
|
||||
col = 0;
|
||||
message =
|
||||
"effect/capability 검사까지 통과. move/affinity 검사가 아직 구현되지 않았습니다";
|
||||
})
|
||||
files)
|
||||
if errors <> [] then Error errors else Ok ()
|
||||
|
||||
let run (file : string) : (unit, error list) result =
|
||||
Error [ { file; line = 0; col = 0; message = "interpreter가 아직 구현되지 않았습니다" } ]
|
||||
|
||||
Reference in New Issue
Block a user