coolguyandClaude Opus 5
410363b230
프로그램을 쓰되 돌리지 않는 방식을 시작한다. std가 원래 선언-전용이므로 실행만 빼고 전부 진짜로 검사된다 — 종이 스케치가 아니라 컴파일러가 검증한 설계다. 합격 기준을 둘로 잡았다: check exit 0 + 모듈이 실제로 해소될 것. 후자가 없으면 전자가 공허한데, 그것을 첫 시도에서 겪었다. D1 — 상대 경로 import가 패키지로 오인됐다. is_package가 첫 세그먼트에 점이 있는지만 봐서 ".."이 걸렸다. 무서운 것은 버그가 아니라 결과였다: import가 해소되지 않으면 그 모듈의 이름이 전부 불투명해지고, "모르는 것을 틀렸다고 말하지 않는다"는 원칙에 따라 무엇이든 통과한다. 첫 check가 exit 0이었는데 없는 메서드를 불러도 통과하는 상태였다. D2 — 값 있는 식을 문으로 버릴 수 있었다. fs.remove(path)를 문으로 쓰면 Result가 조용히 사라졌다. 즉 실패를 버리는 방법이 있었고, 내가 개밥 먹기 1차 보고서와 투어에 "이 언어에는 실패를 버릴 방법이 없다"고 적은 것은 틀렸다 — List.each 하나의 좁은 사실을 언어 전체로 일반화했다. 이제 오류이고, 일부러 버리려면 let _ = 로 적는다. 부산물로 정리 경로의 관용구가 생겼다. D3(본체) — ?를 자원과 함께 쓸 수 없다. naive.cool 18줄은 조기 반환으로 핸들을 누수하는데 통과한다(v0 정책). 제대로 정리한 careful.cool은 58줄이고 5단 중첩 match이며 ?를 한 번도 못 쓴다. 3.2배다. resource/with가 필요한 이유가 여기 숫자로 있다. 열어둔 것: 함수 타입에 own이 없어 고차 경계에서 소유권이 뚫린다(D5). Mini Shell과 DB Pool이 정면으로 걸리므로 그 둘 전에 결정해야 한다. 문자 접근이 없어 어휘 분석을 못 쓴다(D6). 소유권 검사가 잡는 것은 확인했다: 두 번 닫기, 닫은 뒤 쓰기, 빌린 핸들 반환. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019ZVDeU6KLuUVL3gs18Hm3E
891 lines
33 KiB
OCaml
891 lines
33 KiB
OCaml
(* 타입 검사.
|
|
|
|
범위: 이 모듈 안에서 아는 것만 검사한다. 외부 이름은 TUnknown이 되어
|
|
무엇과도 맞는다 — 모르는 것을 틀렸다고 말하지 않는다.
|
|
|
|
제네릭 해소는 호출 지점의 지역 unification이다. 함수 하나를 넘어가지
|
|
않으므로 전역 추론이 아니다. *)
|
|
|
|
open Ast
|
|
module T = Types
|
|
|
|
type error = { pos : Token.pos; msg : string }
|
|
|
|
type scheme = {
|
|
s_gen : string list; (* 타입 파라미터 *)
|
|
s_eff_gen : string list; (* effect 파라미터 *)
|
|
s_params : T.t list;
|
|
s_eff : T.eff; (* 이 함수를 부르면 수행되는 effect *)
|
|
s_ret : T.t;
|
|
}
|
|
|
|
type env = {
|
|
structs : (string, string list * (string * T.t) list) Hashtbl.t;
|
|
enums : (string, string list * (string * T.t list) list) Hashtbl.t;
|
|
caps : (string, (string * scheme) list) Hashtbl.t;
|
|
fns : (string, scheme) Hashtbl.t;
|
|
consts : (string, T.t) Hashtbl.t;
|
|
ctors : (string, string) Hashtbl.t; (* variant -> enum *)
|
|
(* 가져온 모듈의 별칭. `Alias.x`는 "Alias.x"라는 하나의 키로 찾는다 —
|
|
별칭은 식별자에 쓸 수 없는 점(.)을 포함하므로 지역 이름과 충돌하지 않는다. *)
|
|
aliases : string list;
|
|
mutable locals : (string * T.t) list list;
|
|
mutable ret : T.t; (* 현재 함수의 선언된 반환 타입 *)
|
|
(* 현재 본문이 수행한 effect. 위치를 같이 들고 다녀야 "어디서 수행했는지"를
|
|
말할 수 있다. 클로저에 들어가면 저장하고 비운다 — 클로저의 effect는
|
|
정의한 자리가 아니라 부르는 자리에서 일어난다. *)
|
|
mutable performed : (T.atom * Token.pos) list;
|
|
(* 이 본문에서 모르는 것을 만났는가. 과잉 선언 판정에만 쓴다 — 외부 타입의
|
|
메서드는 effect를 알 수 없으므로 "수행하지 않았다"고 말할 근거가 없다. *)
|
|
mutable saw_unknown : bool;
|
|
mutable errors : error list;
|
|
}
|
|
|
|
let err env pos msg = env.errors <- { pos; msg } :: env.errors
|
|
|
|
let expr_pos (e : expr) : Token.pos =
|
|
match e with
|
|
| E_lit (_, p)
|
|
| E_ident (_, p)
|
|
| E_list (_, p)
|
|
| E_struct { pos = p; _ }
|
|
| E_if { pos = p; _ }
|
|
| E_match { pos = p; _ }
|
|
| E_scope { pos = p; _ }
|
|
| E_call { pos = p; _ }
|
|
| E_field { pos = p; _ }
|
|
| E_inst { pos = p; _ }
|
|
| E_try { pos = p; _ }
|
|
| E_unary { pos = p; _ }
|
|
| E_binary { pos = p; _ }
|
|
| E_crash { pos = p; _ } ->
|
|
p
|
|
| E_closure c -> c.cl_pos
|
|
| E_block b -> b.block_pos
|
|
|
|
let mismatch env pos expected got what =
|
|
err env pos
|
|
(Printf.sprintf "%s: %s이(가) 필요한데 %s입니다" what (T.show expected) (T.show got))
|
|
|
|
let push env = env.locals <- [] :: env.locals
|
|
let pop env = match env.locals with _ :: r -> env.locals <- r | [] -> ()
|
|
|
|
let bind env n t =
|
|
match env.locals with
|
|
| s :: r -> env.locals <- ((n, t) :: s) :: r
|
|
| [] -> env.locals <- [ [ (n, t) ] ]
|
|
|
|
let lookup env n =
|
|
let rec go = function
|
|
| [] -> None
|
|
| s :: r -> (
|
|
match List.assoc_opt n s with Some t -> Some t | None -> go r)
|
|
in
|
|
go env.locals
|
|
|
|
(* ------------------------------------------------------------------ *)
|
|
(* Ast.ty -> Types.t *)
|
|
(* ------------------------------------------------------------------ *)
|
|
|
|
let conv_eff_atom (a : Ast.eff_atom) : T.eff =
|
|
match a with
|
|
| Eff_var v -> [ T.A_var v ]
|
|
| Eff_set names -> List.map (fun { cap; meth } -> T.A_name (cap, meth)) names
|
|
|
|
let conv_eff_result (atoms : Ast.eff_result) : T.eff =
|
|
T.eff_resolve (List.concat_map conv_eff_atom atoms)
|
|
|
|
let rec conv env (gen : string list) (t : Ast.ty) : T.t =
|
|
match t with
|
|
| T_named { modl; name; args; _ } -> (
|
|
let args =
|
|
List.filter_map
|
|
(function TA_ty t -> Some (conv env gen t) | TA_eff _ -> None)
|
|
args
|
|
in
|
|
let name = match modl with Some a -> a ^ "." ^ name | None -> name in
|
|
if modl = None && List.mem name gen then T.TVar name
|
|
else
|
|
match if modl = None then name else "" with
|
|
| "Int" -> T.TInt
|
|
| "Bool" -> T.TBool
|
|
| "String" -> T.TString
|
|
| "Unit" -> T.TUnit
|
|
| "List" | "Option" | "Result" -> T.TCon (name, args)
|
|
| _ ->
|
|
if
|
|
Hashtbl.mem env.structs name
|
|
|| Hashtbl.mem env.enums name || Hashtbl.mem env.caps name
|
|
then T.TCon (name, args)
|
|
else T.TUnknown)
|
|
| T_fn { affine; params; eff; ret; _ } ->
|
|
T.TFn
|
|
{
|
|
affine;
|
|
params = List.map (conv env gen) params;
|
|
eff = (match eff with None -> [] | Some a -> conv_eff_atom a);
|
|
ret = (match ret with None -> T.TUnit | Some r -> conv env gen r);
|
|
}
|
|
|
|
let scheme_of env (d : fn_decl) : scheme =
|
|
let gen =
|
|
List.filter_map
|
|
(fun g -> if g.gp_effect then None else Some g.gp_name)
|
|
d.fn_gen
|
|
in
|
|
let egen =
|
|
List.filter_map
|
|
(fun g -> if g.gp_effect then Some g.gp_name else None)
|
|
d.fn_gen
|
|
in
|
|
{
|
|
s_gen = gen;
|
|
s_eff_gen = egen;
|
|
s_params = List.map (fun p -> conv env gen p.p_ty) d.fn_params;
|
|
s_eff =
|
|
(match d.fn_eff with None -> [] | Some atoms -> conv_eff_result atoms);
|
|
s_ret = (match d.fn_ret with None -> T.TUnit | Some r -> conv env gen r);
|
|
}
|
|
|
|
(* 호출 지점 인스턴스화: 타입 파라미터마다 새 미지수 *)
|
|
let instantiate (s : scheme) =
|
|
let sub = List.map (fun v -> (v, T.fresh ())) s.s_gen in
|
|
let esub = List.map (fun v -> (v, T.fresh_eff ())) s.s_eff_gen in
|
|
( List.map (T.subst sub esub) s.s_params,
|
|
T.subst_eff esub s.s_eff,
|
|
T.subst sub esub s.s_ret )
|
|
|
|
let instantiate_with (s : scheme) (args : T.t list) =
|
|
let sub = List.map2 (fun v a -> (v, a)) s.s_gen args in
|
|
let esub = List.map (fun v -> (v, T.fresh_eff ())) s.s_eff_gen in
|
|
( List.map (T.subst sub esub) s.s_params,
|
|
T.subst_eff esub s.s_eff,
|
|
T.subst sub esub s.s_ret )
|
|
|
|
(* ------------------------------------------------------------------ *)
|
|
(* 내장 생성자 *)
|
|
(* ------------------------------------------------------------------ *)
|
|
|
|
let builtin_ctor = function
|
|
| "Ok" ->
|
|
let a = T.fresh () and b = T.fresh () in
|
|
Some ([ a ], T.TCon ("Result", [ a; b ]))
|
|
| "Err" ->
|
|
let a = T.fresh () and b = T.fresh () in
|
|
Some ([ b ], T.TCon ("Result", [ a; b ]))
|
|
| "Some" ->
|
|
let a = T.fresh () in
|
|
Some ([ a ], T.TCon ("Option", [ a ]))
|
|
| _ -> None
|
|
|
|
(* ------------------------------------------------------------------ *)
|
|
(* 식 *)
|
|
(* ------------------------------------------------------------------ *)
|
|
|
|
let rec infer env (e : expr) : T.t =
|
|
match e with
|
|
(* crash는 돌아오지 않는다. 타입은 Never이고 어떤 자리에도 놓인다 *)
|
|
| E_crash { msg; pos } ->
|
|
let t = infer env msg in
|
|
if not (T.unify t T.TString) then
|
|
mismatch env pos T.TString t "crash의 메시지";
|
|
T.TNever
|
|
| E_lit (L_int _, _) -> T.TInt
|
|
| E_lit (L_str _, _) -> T.TString
|
|
| E_lit (L_bool _, _) -> T.TBool
|
|
| E_ident (n, _) -> (
|
|
match lookup env n with
|
|
| Some t -> t
|
|
| None -> (
|
|
match Hashtbl.find_opt env.consts n with
|
|
| Some t -> t
|
|
| None -> (
|
|
match n with
|
|
| "unit" -> T.TUnit
|
|
| "None" -> T.TCon ("Option", [ T.fresh () ])
|
|
| _ -> (
|
|
match Hashtbl.find_opt env.fns n with
|
|
| Some s ->
|
|
let params, eff, ret = instantiate s in
|
|
T.TFn { affine = false; params; eff; ret }
|
|
| None -> (
|
|
match Hashtbl.find_opt env.ctors n with
|
|
| Some enum -> nullary_ctor env enum n
|
|
| None ->
|
|
env.saw_unknown <- true;
|
|
T.TUnknown)))))
|
|
| E_list (xs, pos) ->
|
|
let elem = T.fresh () in
|
|
List.iter
|
|
(fun x ->
|
|
let t = infer env x in
|
|
if not (T.unify elem t) then
|
|
mismatch env pos elem t "리스트 원소의 타입이 서로 다릅니다")
|
|
xs;
|
|
T.TCon ("List", [ elem ])
|
|
| E_struct { name; fields; pos } -> infer_struct env name fields pos
|
|
| E_closure c -> infer_closure env c None
|
|
| E_if { cond; then_; else_; pos } -> (
|
|
let c = infer env cond in
|
|
if not (T.unify c T.TBool) then mismatch env pos T.TBool c "if의 조건";
|
|
let t1 = infer_block env then_ in
|
|
match else_ with
|
|
| None ->
|
|
if not (T.unify t1 T.TUnit) then
|
|
err env pos "else가 없는 if의 본문은 값을 남길 수 없습니다";
|
|
T.TUnit
|
|
| Some e2 ->
|
|
let t2 = infer env e2 in
|
|
if not (T.unify t1 t2) then mismatch env pos t1 t2 "if의 두 분기 타입이 다릅니다";
|
|
t1)
|
|
| E_match { scrutinee; arms; pos } ->
|
|
let s = infer env scrutinee in
|
|
let result = T.fresh () in
|
|
List.iter
|
|
(fun a ->
|
|
push env;
|
|
check_pattern env s a.arm_pat;
|
|
let t = infer env a.arm_body in
|
|
if not (T.unify result t) then
|
|
mismatch env a.arm_pos result t "match 팔의 타입이 서로 다릅니다";
|
|
pop env)
|
|
arms;
|
|
if arms = [] then err env pos "match에 팔이 없습니다";
|
|
check_exhaustive env s arms pos;
|
|
result
|
|
| E_scope { name; parent; body; pos } ->
|
|
(match lookup env parent with
|
|
| Some t when not (T.unify t (T.TCon ("TaskScope", []))) ->
|
|
if T.resolve t <> T.TUnknown then
|
|
mismatch env pos (T.TCon ("TaskScope", [])) t "scope의 부모"
|
|
| _ -> ());
|
|
push env;
|
|
bind env name (T.TCon ("TaskScope", []));
|
|
let t = infer_block env body in
|
|
pop env;
|
|
t
|
|
| E_block b ->
|
|
push env;
|
|
let t = infer_block env b in
|
|
pop env;
|
|
t
|
|
| E_call { callee; args; pos } -> infer_call env callee args pos
|
|
| E_field { obj; name; pos } -> infer_field env obj name pos
|
|
| E_inst { callee; args; pos } -> infer_inst env callee args pos
|
|
| E_try { inner; pos } -> (
|
|
let t = infer env inner in
|
|
match T.resolve t with
|
|
| T.TUnknown -> T.TUnknown
|
|
| T.TCon ("Result", [ ok; _ ]) ->
|
|
(match T.resolve env.ret with
|
|
| T.TCon ("Result", _) | T.TUnknown -> ()
|
|
| r ->
|
|
err env pos
|
|
(Printf.sprintf "?는 Result를 반환하는 함수 안에서만 쓸 수 있습니다 (현재 반환 타입 %s)"
|
|
(T.show r)));
|
|
ok
|
|
| other ->
|
|
err env pos
|
|
(Printf.sprintf "?는 Result에만 쓸 수 있습니다 (%s에 쓰였습니다)" (T.show other));
|
|
T.TUnknown)
|
|
| E_unary { op; operand; pos } ->
|
|
let t = infer env operand in
|
|
let want = match op with U_not -> T.TBool | U_neg -> T.TInt in
|
|
if not (T.unify t want) then mismatch env pos want t "단항 연산자의 피연산자";
|
|
want
|
|
| E_binary { op; lhs; rhs; pos } -> (
|
|
let a = infer env lhs and b = infer env rhs in
|
|
match op with
|
|
| B_or | B_and ->
|
|
if not (T.unify a T.TBool) then mismatch env pos T.TBool a "논리 연산자";
|
|
if not (T.unify b T.TBool) then mismatch env pos T.TBool b "논리 연산자";
|
|
T.TBool
|
|
| B_add | B_sub | B_mul | B_div | B_rem ->
|
|
if not (T.unify a T.TInt) then mismatch env pos T.TInt a "산술 연산자";
|
|
if not (T.unify b T.TInt) then mismatch env pos T.TInt b "산술 연산자";
|
|
T.TInt
|
|
| B_lt | B_le | B_gt | B_ge ->
|
|
if not (T.unify a T.TInt) then mismatch env pos T.TInt a "비교 연산자";
|
|
if not (T.unify b T.TInt) then mismatch env pos T.TInt b "비교 연산자";
|
|
T.TBool
|
|
| B_eq | B_ne ->
|
|
if not (T.unify a b) then mismatch env pos a b "같은 타입끼리만 비교할 수 있습니다";
|
|
T.TBool)
|
|
|
|
(* exhaustiveness: 철학 1의 대표 항목이자 interface hash가 enum 본문을
|
|
입력으로 삼는 이유다 *)
|
|
and check_exhaustive env scrutinee arms pos =
|
|
let eenv : Exhaust.env =
|
|
{
|
|
variants =
|
|
(fun name args ->
|
|
match Hashtbl.find_opt env.enums name with
|
|
| None -> None
|
|
| Some (gen, variants) ->
|
|
let sub =
|
|
try List.map2 (fun v a -> (v, a)) gen args
|
|
with Invalid_argument _ -> []
|
|
in
|
|
Some
|
|
(List.map
|
|
(fun (n, tys) -> (n, List.map (T.subst sub []) tys))
|
|
variants));
|
|
is_ctor =
|
|
(fun n ->
|
|
Hashtbl.mem env.ctors n || List.mem n [ "Ok"; "Err"; "Some"; "None" ]);
|
|
}
|
|
in
|
|
let r = Exhaust.check eenv scrutinee (List.map (fun a -> a.arm_pat) arms) in
|
|
(match r.missing with
|
|
| None -> ()
|
|
| Some w -> err env pos (Printf.sprintf "match가 모든 경우를 덮지 않습니다 (빠진 경우: %s)" w));
|
|
List.iter
|
|
(fun i ->
|
|
match List.nth_opt arms i with
|
|
| Some a -> err env a.arm_pos "이 팔은 앞의 팔들에 가려 도달할 수 없습니다"
|
|
| None -> ())
|
|
r.unreachable
|
|
|
|
and nullary_ctor env enum name =
|
|
match Hashtbl.find_opt env.enums enum with
|
|
| None -> T.TUnknown
|
|
| Some (gen, variants) -> (
|
|
let sub = List.map (fun v -> (v, T.fresh ())) gen in
|
|
match List.assoc_opt name variants with
|
|
| Some [] -> T.TCon (enum, List.map snd sub)
|
|
| _ -> T.TCon (enum, List.map snd sub))
|
|
|
|
and infer_struct env name fields pos =
|
|
match Hashtbl.find_opt env.structs name with
|
|
| None ->
|
|
List.iter (fun (_, e) -> ignore (infer env e)) fields;
|
|
T.TUnknown
|
|
| Some (gen, decl_fields) ->
|
|
let sub = List.map (fun v -> (v, T.fresh ())) gen in
|
|
List.iter
|
|
(fun (fname, fe) ->
|
|
match List.assoc_opt fname decl_fields with
|
|
| None -> err env pos (Printf.sprintf "%s에 %s 필드가 없습니다" name fname)
|
|
| Some ft ->
|
|
let want = T.subst sub [] ft in
|
|
let got = infer env fe in
|
|
if not (T.unify want got) then
|
|
mismatch env pos want got (Printf.sprintf "%s.%s 필드" name fname))
|
|
fields;
|
|
List.iter
|
|
(fun (fname, _) ->
|
|
if not (List.mem_assoc fname fields) then
|
|
err env pos (Printf.sprintf "%s의 %s 필드가 빠졌습니다" name fname))
|
|
decl_fields;
|
|
T.TCon (name, List.map snd sub)
|
|
|
|
and infer_closure env (c : closure) (expected : T.t option) =
|
|
let expected_params, expected_ret =
|
|
match Option.map T.resolve expected with
|
|
| Some (T.TFn { params; ret; _ })
|
|
when List.length params = List.length c.cl_params ->
|
|
(List.map Option.some params, Some ret)
|
|
| _ -> (List.map (fun _ -> None) c.cl_params, None)
|
|
in
|
|
push env;
|
|
let param_tys =
|
|
List.map2
|
|
(fun (n, ann) exp ->
|
|
let t =
|
|
match ann with
|
|
| Some a -> conv env [] a
|
|
| None -> ( match exp with Some t -> t | None -> T.TUnknown)
|
|
in
|
|
bind env n t;
|
|
t)
|
|
c.cl_params expected_params
|
|
in
|
|
let declared_ret = Option.map (conv env []) c.cl_ret in
|
|
let saved_ret = env.ret in
|
|
env.ret <-
|
|
(match declared_ret with
|
|
| Some t -> t
|
|
| None -> ( match expected_ret with Some t -> t | None -> T.TUnknown));
|
|
(* 클로저 본문의 effect는 바깥 함수가 수행하는 것이 아니다. 저장하고 비운다. *)
|
|
let saved_perf = env.performed in
|
|
env.performed <- [];
|
|
let body = infer_block env c.cl_body in
|
|
let inner = env.performed in
|
|
env.performed <- saved_perf;
|
|
let declared_eff = Option.map conv_eff_atom c.cl_eff in
|
|
let eff =
|
|
match declared_eff with
|
|
| Some d ->
|
|
(* 클로저가 effects를 명시했으면 본문이 그 안에 들어야 한다 *)
|
|
List.iter
|
|
(fun (a, pos) ->
|
|
List.iter
|
|
(fun m ->
|
|
err env pos
|
|
(Printf.sprintf "클로저가 선언하지 않은 effect %s을(를) 수행합니다 (선언: %s)"
|
|
(T.atom_show m) (T.eff_show d)))
|
|
(T.eff_missing ~declared:d ~performed:[ a ]))
|
|
inner;
|
|
d
|
|
| None -> T.eff_resolve (List.map fst inner)
|
|
in
|
|
(match declared_ret with
|
|
| Some t when not (T.unify t body) -> mismatch env c.cl_pos t body "클로저의 반환"
|
|
| _ -> ());
|
|
let ret = match declared_ret with Some t -> t | None -> body in
|
|
env.ret <- saved_ret;
|
|
pop env;
|
|
T.TFn { affine = false; params = param_tys; eff; ret }
|
|
|
|
and infer_call env callee args pos =
|
|
let fn_ty =
|
|
match callee with
|
|
| E_ident (n, _) when lookup env n = None -> (
|
|
match Hashtbl.find_opt env.ctors n with
|
|
| Some enum -> Some (ctor_fn env enum n)
|
|
| None -> (
|
|
match builtin_ctor n with
|
|
| Some (params, ret) ->
|
|
Some (T.TFn { affine = false; params; eff = []; ret })
|
|
| None -> (
|
|
match Hashtbl.find_opt env.fns n with
|
|
| Some s ->
|
|
let params, eff, ret = instantiate s in
|
|
Some (T.TFn { affine = false; params; eff; ret })
|
|
| None -> None)))
|
|
| _ -> (
|
|
match T.resolve (infer env callee) with
|
|
| T.TFn _ as t -> Some t
|
|
| _ -> None)
|
|
in
|
|
match fn_ty with
|
|
| None ->
|
|
env.saw_unknown <- true;
|
|
List.iter (fun a -> ignore (infer env a)) args;
|
|
T.TUnknown
|
|
| Some (T.TFn { params; eff; ret; _ }) ->
|
|
List.iter
|
|
(fun a -> env.performed <- (a, pos) :: env.performed)
|
|
(T.eff_resolve eff);
|
|
if List.length params <> List.length args then (
|
|
err env pos
|
|
(Printf.sprintf "인자 %d개가 필요한데 %d개가 주어졌습니다" (List.length params)
|
|
(List.length args));
|
|
List.iter (fun a -> ignore (infer env a)) args)
|
|
else
|
|
List.iter2
|
|
(fun p a ->
|
|
let got =
|
|
match a with
|
|
| E_closure c -> infer_closure env c (Some p)
|
|
| _ -> infer env a
|
|
in
|
|
(* 먼저 unify한다. 결정 위치의 effect 변수는 여기서 인자의
|
|
effect로 묶인다 — 제약이 아니라 해소다. 그 뒤에 남는 차이만이
|
|
진짜 위반이다. *)
|
|
if not (T.unify p got) then mismatch env pos p got "인자";
|
|
match (T.resolve p, T.resolve got) with
|
|
| T.TFn pf, T.TFn gf ->
|
|
let missing =
|
|
T.eff_missing ~declared:pf.eff ~performed:gf.eff
|
|
in
|
|
if missing <> [] then
|
|
err env pos
|
|
(Printf.sprintf
|
|
"넘긴 함수가 %s을(를) 수행하는데 파라미터가 허용한 effect는 %s입니다"
|
|
(String.concat ", " (List.map T.atom_show missing))
|
|
(T.eff_show pf.eff))
|
|
| _ -> ())
|
|
params args;
|
|
ret
|
|
| Some _ -> T.TUnknown
|
|
|
|
and ctor_fn env enum name =
|
|
match Hashtbl.find_opt env.enums enum with
|
|
| None -> T.TUnknown
|
|
| Some (gen, variants) ->
|
|
let sub = List.map (fun v -> (v, T.fresh ())) gen in
|
|
let params =
|
|
match List.assoc_opt name variants with
|
|
| Some ts -> List.map (T.subst sub []) ts
|
|
| None -> []
|
|
in
|
|
T.TFn
|
|
{
|
|
affine = false;
|
|
params;
|
|
eff = [];
|
|
ret = T.TCon (enum, List.map snd sub);
|
|
}
|
|
|
|
and infer_field env obj name pos =
|
|
(* capability 메서드는 값을 통해서만 부를 수 있다. 타입 이름으로 부를 수 있으면
|
|
capability 없이 effect를 수행하게 되어 보안 정리 (i)이 무너진다. *)
|
|
(match obj with
|
|
| E_ident (n, _) when lookup env n = None && Hashtbl.mem env.caps n ->
|
|
err env pos
|
|
(Printf.sprintf
|
|
"capability %s의 메서드는 값을 통해서만 부를 수 있습니다 (%s를 파라미터로 받아야 합니다)" n n)
|
|
| _ -> ());
|
|
match obj with
|
|
| E_ident (a, _) when lookup env a = None && List.mem a env.aliases -> (
|
|
(* 모듈 별칭을 통한 접근. 가져온 표면은 "Alias.name" 키로 들어와 있다. *)
|
|
let key = a ^ "." ^ name in
|
|
let unknown () =
|
|
err env pos (Printf.sprintf "%s에 %s이(가) 없습니다" a name);
|
|
T.TUnknown
|
|
in
|
|
match Hashtbl.find_opt env.consts key with
|
|
| Some t -> t
|
|
| None -> (
|
|
match Hashtbl.find_opt env.fns key with
|
|
| Some s ->
|
|
let params, eff, ret = instantiate s in
|
|
T.TFn { affine = false; params; eff; ret }
|
|
| None -> (
|
|
match Hashtbl.find_opt env.ctors key with
|
|
| Some enum -> (
|
|
match Hashtbl.find_opt env.enums enum with
|
|
| Some (_, variants)
|
|
when List.assoc_opt key variants = Some [] ->
|
|
nullary_ctor env enum key
|
|
| Some _ -> ctor_fn env enum key
|
|
| None -> T.TUnknown)
|
|
| None -> unknown ())))
|
|
| _ -> (
|
|
let t = infer env obj in
|
|
match T.resolve t with
|
|
| T.TUnknown -> T.TUnknown
|
|
| T.TCon (cname, args) -> (
|
|
match Hashtbl.find_opt env.structs cname with
|
|
| Some (gen, fields) -> (
|
|
let sub = List.map2 (fun v a -> (v, a)) gen (adjust gen args) in
|
|
match List.assoc_opt name fields with
|
|
| Some ft -> T.subst sub [] ft
|
|
| None ->
|
|
err env pos (Printf.sprintf "%s에 %s 필드가 없습니다" cname name);
|
|
T.TUnknown)
|
|
| None -> (
|
|
match Hashtbl.find_opt env.caps cname with
|
|
| Some methods -> (
|
|
match List.assoc_opt name methods with
|
|
| Some s ->
|
|
let params, eff, ret = instantiate s in
|
|
T.TFn { affine = false; params; eff; ret }
|
|
| None ->
|
|
err env pos
|
|
(Printf.sprintf "capability %s에 %s 메서드가 없습니다" cname name);
|
|
T.TUnknown)
|
|
| None -> T.TUnknown))
|
|
| other ->
|
|
err env pos (Printf.sprintf "%s에는 필드가 없습니다" (T.show other));
|
|
T.TUnknown)
|
|
|
|
and adjust gen args =
|
|
let n = List.length gen in
|
|
let rec take k xs =
|
|
if k = 0 then []
|
|
else
|
|
match xs with
|
|
| [] -> T.fresh () :: take (k - 1) []
|
|
| x :: r -> x :: take (k - 1) r
|
|
in
|
|
take n args
|
|
|
|
and infer_inst env callee args pos =
|
|
let tys =
|
|
List.filter_map
|
|
(function TA_ty t -> Some (conv env [] t) | TA_eff _ -> None)
|
|
args
|
|
in
|
|
match callee with
|
|
| E_ident (n, _) when lookup env n = None -> (
|
|
match Hashtbl.find_opt env.fns n with
|
|
| None -> T.TUnknown
|
|
| Some s ->
|
|
if List.length tys <> List.length s.s_gen then (
|
|
err env pos
|
|
(Printf.sprintf "타입 인자 %d개가 필요한데 %d개가 주어졌습니다"
|
|
(List.length s.s_gen) (List.length tys));
|
|
T.TUnknown)
|
|
else
|
|
let params, eff, ret = instantiate_with s tys in
|
|
T.TFn { affine = false; params; eff; ret })
|
|
| _ -> T.TUnknown
|
|
|
|
and check_pattern env (scrutinee : T.t) (p : pattern) =
|
|
match p with
|
|
| P_wild _ -> ()
|
|
| P_lit (l, pos) ->
|
|
let t =
|
|
match l with
|
|
| L_int _ -> T.TInt
|
|
| L_str _ -> T.TString
|
|
| L_bool _ -> T.TBool
|
|
in
|
|
if not (T.unify scrutinee t) then mismatch env pos scrutinee t "패턴의 리터럴"
|
|
| P_bind (n, _) -> (
|
|
match Hashtbl.find_opt env.ctors n with
|
|
| Some enum ->
|
|
check_ctor env scrutinee enum n [] Token.{ line = 0; col = 0 }
|
|
| None -> bind env n scrutinee)
|
|
| P_ctor { modl; name; args; pos } -> (
|
|
let name = match modl with Some a -> a ^ "." ^ name | None -> name in
|
|
match Hashtbl.find_opt env.ctors name with
|
|
| Some enum -> check_ctor env scrutinee enum name args pos
|
|
| None -> List.iter (check_pattern env T.TUnknown) args)
|
|
|
|
and check_ctor env scrutinee enum name args pos =
|
|
match Hashtbl.find_opt env.enums enum with
|
|
| None -> ()
|
|
| Some (gen, variants) ->
|
|
let sub = List.map (fun v -> (v, T.fresh ())) gen in
|
|
let ety = T.TCon (enum, List.map snd sub) in
|
|
if not (T.unify scrutinee ety) then
|
|
mismatch env pos scrutinee ety "패턴이 match 대상과 다른 타입입니다";
|
|
let fields =
|
|
match List.assoc_opt name variants with Some ts -> ts | None -> []
|
|
in
|
|
if List.length fields = List.length args then
|
|
List.iter2
|
|
(fun ft ap -> check_pattern env (T.subst sub [] ft) ap)
|
|
fields args
|
|
|
|
(* ------------------------------------------------------------------ *)
|
|
(* 문과 블록 *)
|
|
(* ------------------------------------------------------------------ *)
|
|
|
|
and infer_block env (b : block) : T.t =
|
|
let rec go = function
|
|
| [] -> T.TUnit
|
|
| [ S_expr e ] -> infer env e
|
|
| s :: rest ->
|
|
check_stmt env s;
|
|
go rest
|
|
in
|
|
go b.stmts
|
|
|
|
and check_stmt env = function
|
|
(* 꼬리가 아닌 자리의 식은 값을 남기면 안 된다. 남긴 값은 버려지는데,
|
|
그 값이 Result면 실패가 조용히 사라진다 — 철학 1과 정면으로 부딪힌다.
|
|
일부러 버리려면 let _ = 로 적는다. 버린다는 사실이 코드에 보여야 한다. *)
|
|
| S_expr e -> (
|
|
let t = infer env e in
|
|
match T.resolve t with
|
|
| T.TUnit | T.TUnknown | T.TNever -> ()
|
|
| other ->
|
|
err env (expr_pos e)
|
|
(Printf.sprintf "이 식이 남기는 %s이(가) 버려집니다 (일부러 버리려면 let _ = 로 적으십시오)"
|
|
(T.show other)))
|
|
| S_let { pat; ty; value; pos; _ } ->
|
|
let declared = Option.map (conv env []) ty in
|
|
let got =
|
|
match (value, declared) with
|
|
| E_closure c, Some t -> infer_closure env c (Some t)
|
|
| _ -> infer env value
|
|
in
|
|
let t =
|
|
match declared with
|
|
| None -> got
|
|
| Some d ->
|
|
if not (T.unify d got) then mismatch env pos d got "let의 타입 주석";
|
|
d
|
|
in
|
|
check_pattern env t pat
|
|
| S_return { value; pos } ->
|
|
let got = match value with None -> T.TUnit | Some e -> infer env e in
|
|
if not (T.unify env.ret got) then mismatch env pos env.ret got "return의 값"
|
|
| S_assign { place; value; pos } ->
|
|
let p = infer env place in
|
|
let v = infer env value in
|
|
if not (T.unify p v) then mismatch env pos p v "대입"
|
|
|
|
(* ------------------------------------------------------------------ *)
|
|
(* 모듈 *)
|
|
(* ------------------------------------------------------------------ *)
|
|
|
|
let check_fn env (d : fn_decl) =
|
|
match d.fn_body with
|
|
| None -> ()
|
|
| Some body ->
|
|
let gen =
|
|
List.filter_map
|
|
(fun g -> if g.gp_effect then None else Some g.gp_name)
|
|
d.fn_gen
|
|
in
|
|
push env;
|
|
List.iter (fun p -> bind env p.p_name (conv env gen p.p_ty)) d.fn_params;
|
|
let declared =
|
|
match d.fn_ret with None -> T.TUnit | Some r -> conv env gen r
|
|
in
|
|
env.ret <- declared;
|
|
env.performed <- [];
|
|
env.saw_unknown <- false;
|
|
let got = infer_block env body in
|
|
if not (T.unify declared got) then
|
|
mismatch env d.fn_pos declared got
|
|
(Printf.sprintf "%s의 본문이 남기는 값" d.fn_name);
|
|
(* 미선언 effect = compile error (철학 1).
|
|
수행한 자리를 알고 있으므로 그 자리에 진단을 붙인다. *)
|
|
let declared_eff =
|
|
match d.fn_eff with None -> [] | Some atoms -> conv_eff_result atoms
|
|
in
|
|
List.iter
|
|
(fun (a, pos) ->
|
|
match T.eff_missing ~declared:declared_eff ~performed:[ a ] with
|
|
| [] -> ()
|
|
| missing ->
|
|
List.iter
|
|
(fun m ->
|
|
err env pos
|
|
(Printf.sprintf "선언되지 않은 effect %s (%s의 effects 절은 %s입니다)"
|
|
(T.atom_show m) d.fn_name (T.eff_show declared_eff)))
|
|
missing)
|
|
(List.rev env.performed);
|
|
(* 과잉 선언도 오류다. 선언한 effect를 수행하지 않으면 호출자는 하지도
|
|
않는 일에 대한 의무를 진다 — 자기 effects 절을 넓히거나 capability를
|
|
받아오게 된다. 시그니처는 실제보다 좁아도 안 되고 넓어도 안 된다.
|
|
|
|
effect 변수가 있으면 판정하지 않는다. e에 무엇이 묶일지는 호출
|
|
지점이 정하고, 본문만 보고는 알 수 없다 — 모르는 것을 틀렸다고
|
|
말하지 않는다. *)
|
|
let has_var =
|
|
List.exists (function T.A_var _ -> true | _ -> false) declared_eff
|
|
in
|
|
if (not has_var) && not env.saw_unknown then
|
|
List.iter
|
|
(fun a ->
|
|
match a with
|
|
| T.A_name (cap, meth) ->
|
|
let performed = List.map fst env.performed |> T.eff_resolve in
|
|
if
|
|
not
|
|
(List.exists
|
|
(function
|
|
| T.A_name (c, m) -> c = cap && m = meth
|
|
| T.A_var _ | T.A_meta _ -> true)
|
|
performed)
|
|
then
|
|
err env d.fn_pos
|
|
(Printf.sprintf
|
|
"%s은(는) %s을(를) 선언했지만 수행하지 않습니다 (effects 절에서 지우십시오)"
|
|
d.fn_name (T.atom_show a))
|
|
| _ -> ())
|
|
declared_eff;
|
|
env.performed <- [];
|
|
pop env
|
|
|
|
let check ?(imports : item list = []) (m : modul) : error list =
|
|
let env =
|
|
{
|
|
structs = Hashtbl.create 16;
|
|
enums = Hashtbl.create 16;
|
|
caps = Hashtbl.create 16;
|
|
fns = Hashtbl.create 16;
|
|
consts = Hashtbl.create 16;
|
|
ctors = Hashtbl.create 16;
|
|
(* 표면을 실제로 받아온 별칭만 안다. 해소되지 않은 모듈(예: 아직 가져오지
|
|
못한 패키지)의 별칭은 모르는 것이므로 그 아래 이름을 틀렸다고 말하지
|
|
않는다. *)
|
|
aliases =
|
|
List.sort_uniq compare
|
|
(List.filter_map
|
|
(fun it ->
|
|
let n =
|
|
match it with
|
|
| I_fn { decl; _ } -> decl.fn_name
|
|
| I_struct { name; _ }
|
|
| I_enum { name; _ }
|
|
| I_capability { name; _ }
|
|
| I_const { name; _ } ->
|
|
name
|
|
| _ -> ""
|
|
in
|
|
match String.index_opt n '.' with
|
|
| Some i -> Some (String.sub n 0 i)
|
|
| None -> None)
|
|
imports);
|
|
locals = [];
|
|
ret = T.TUnit;
|
|
performed = [];
|
|
saw_unknown = false;
|
|
errors = [];
|
|
}
|
|
in
|
|
(* 1차: 타입과 생성자 이름부터 (선언 순서에 의존하지 않는다) *)
|
|
List.iter
|
|
(fun it ->
|
|
match it with
|
|
| I_struct { name; gen; _ } ->
|
|
Hashtbl.replace env.structs name
|
|
(List.map (fun g -> g.gp_name) gen, [])
|
|
| I_enum { name; gen; variants; _ } ->
|
|
Hashtbl.replace env.enums name (List.map (fun g -> g.gp_name) gen, []);
|
|
List.iter (fun v -> Hashtbl.replace env.ctors v.v_name name) variants
|
|
| I_capability { name; _ } -> Hashtbl.replace env.caps name []
|
|
| _ -> ())
|
|
(imports @ m.items);
|
|
(* 2차: 본문을 채운다 *)
|
|
List.iter
|
|
(fun it ->
|
|
match it with
|
|
| I_struct { name; gen; fields; _ } ->
|
|
let g = List.map (fun x -> x.gp_name) gen in
|
|
Hashtbl.replace env.structs name
|
|
(g, List.map (fun f -> (f.f_name, conv env g f.f_ty)) fields)
|
|
| I_enum { name; gen; variants; _ } ->
|
|
let g = List.map (fun x -> x.gp_name) gen in
|
|
Hashtbl.replace env.enums name
|
|
( g,
|
|
List.map
|
|
(fun v -> (v.v_name, List.map (conv env g) v.v_args))
|
|
variants )
|
|
| I_capability { name; methods; _ } ->
|
|
Hashtbl.replace env.caps name
|
|
(List.map (fun d -> (d.fn_name, scheme_of env d)) methods)
|
|
| I_fn { decl; _ } ->
|
|
Hashtbl.replace env.fns decl.fn_name (scheme_of env decl)
|
|
| I_const { name; ty; _ } ->
|
|
Hashtbl.replace env.consts name (conv env [] ty)
|
|
| _ -> ())
|
|
(imports @ m.items);
|
|
(* 3차: 본문 검사 *)
|
|
List.iter
|
|
(fun it ->
|
|
env.locals <- [];
|
|
match it with
|
|
| I_fn { decl; _ } -> check_fn env decl
|
|
| I_const { ty; value; pos; _ } ->
|
|
let want = conv env [] ty in
|
|
let got = infer env value in
|
|
if not (T.unify want got) then mismatch env pos want got "상수의 값"
|
|
(* 테스트는 파라미터 없고 effect 없는 함수와 같다. 검사도 같다 —
|
|
일반 코드와 다른 규칙을 주면 테스트만 통과하는 코드가 생긴다 *)
|
|
| I_test { name; body; pos } ->
|
|
env.locals <- [];
|
|
push env;
|
|
env.ret <- T.TUnit;
|
|
env.performed <- [];
|
|
env.saw_unknown <- false;
|
|
let got = infer_block env body in
|
|
if not (T.unify T.TUnit got) then
|
|
mismatch env pos T.TUnit got (Printf.sprintf "테스트 \"%s\"의 본문" name);
|
|
List.iter
|
|
(fun (a, apos) ->
|
|
err env apos
|
|
(Printf.sprintf
|
|
"테스트는 effect를 수행할 수 없습니다 (%s) — 테스트는 capability를 받지 않습니다"
|
|
(T.atom_show a)))
|
|
(List.rev (T.eff_resolve (List.map fst env.performed))
|
|
|> List.map (fun a -> (a, pos)));
|
|
env.performed <- [];
|
|
pop env
|
|
| _ -> ())
|
|
m.items;
|
|
List.sort
|
|
(fun a b ->
|
|
compare
|
|
(a.pos.Token.line, a.pos.Token.col)
|
|
(b.pos.Token.line, b.pos.Token.col))
|
|
(List.rev env.errors)
|