(* Oukseh Lee Copyright(c) 2000-2004 KAIST/SNU Research On Program Analysis System (National Creative Research Initiative Center 1998-2003) http://ropas.snu.ac.kr/n All rights reserved. This file is distributed under the terms of an Open Source License. *) structure TyError = struct open Info.StringInfo open Format structure A = String_ast.Ast type class = Var | Typ | Tv | Str | Sig | Fct type id = string type lid = id list type gid = class * lid (* type id = Varid of A.varlongid | Tyid of A.tylongid | Tvid of tyvarinfo | Strid of A.strlongid | Sigid of sigidinfo | Fctid of fctidinfo *) type match = Domain of gid | Value of id * Ty.scheme * Ty.scheme | Type of id * tymatch and tymatch = Arity of int * int | Unknown | Name of Ty.Tn.t * Ty.Tn.t | String of Ty.TS.t * Ty.TS.t | Constype of id * (Ty.scheme option) * (Ty.scheme option) | Consexist of id | Consreq of id type cases = SS | FI | FS type t = Unbound of gid | Duplicate of gid | UnifyFail of Ty.ty * Ty.ty | TsApply of lid * int * int | Match of cases * lid option * lid option * (id list * match) | RecursiveType of id list | ConstraintSig of lid | RConstraintSig of lid | FunName of id * id | FunLength of int * int type w = Overload exception TM of tymatch exception M of id list * match exception T of t * Location.t exception W of w * Location.t fun to_lid (a,(b,_),_) = (List.map (fn (x,_) => x) a)@[b] fun to_gid class x = (class, to_lid x) fun to_id (b,_) = b fun add_str str (x,y) = (x,str@y) fun unbound_var (id as (_,_,l)) = raise T(Unbound(to_gid Var id),l) fun unbound_ty (id as (_,_,l)) = raise T(Unbound(to_gid Typ id),l) fun unbound_str (id as (_,_,l)) = raise T(Unbound(to_gid Str id),l) fun unbound_tyvar (id,l) = raise T(Unbound(Tv,[id]),l) fun unbound_sig (id,l) = raise T(Unbound(Sig,[id]),l) fun unbound_fct (id,l) = raise T(Unbound(Fct,[id]),l) fun duplicate_var (id,l) = raise T(Duplicate(Var, [id]), l) fun ts_apply x y z l = raise T(TsApply(to_lid x,y,z),l) fun constraint_sig (id as (_,_,l)) = raise T(ConstraintSig(to_lid id),l) fun redundant_constraint_sig (id as (_,_,l)) = raise T(RConstraintSig(to_lid id),l) fun pp_error() = printf "@[<6>오류: " fun pp_scheme ((n,t):Ty.scheme) = (printf "@["; TyPrint.typ t; printf "@]") fun pp_list f g [] = () | pp_list f g [h] = f h | pp_list f g (h::t) = (f h; g(); pp_list f g t) fun pp_lid lid = pp_list (printf "%s") (fn _ => printf ".") lid fun pp' (t,l) = let fun fv (class, x) = let val hd = fn (Var | Typ) => "" | Str => "모듈 " | Sig => "모듈타입 " | Fct => "모듈함수 " | Tv => "타입 변수 " val tl = fn Typ => " 타입" | _ => " " in printf "%s" (hd class); pp_lid x; printf "%s" (tl class) end fun fvtail (x,_) = case x of Typ => printf "을" | _ => printf "을(를)" fun fvtaili (x,_) = case x of Typ => printf "이" | _ => printf "이(가)" fun fnum 0 s1 s2 = printf "%s" s2 | fnum i s1 s2 = s1 i fun fopt None _ g = g() | fopt (Some t) f _ = f t fun fstropt x = fopt x (fn s => fv(Str, s)) (fn _ => printf "모듈") fun fsigopt x = fopt x (fn s => fv(Sig, s)) (fn _ => printf "모듈타입") fun ffctopt x = fopt x (fn s => fv(Fct, s)) (fn _ => printf "모듈함수") (* fun pt _ = pp_ty *) fun ps _ = pp_scheme fun pv _ = fv and pvtail _ = fvtail and pvtaili _ = fvtaili fun pstropt _ = fstropt and psigopt _ = fsigopt and pfctopt _ = ffctopt fun pstrtaili _ None = printf "이" | pstrtaili _ _ = printf "이(가)" fun f (Unbound s) = printf "%a%a 모릅니다." pv s pvtail s | f (Duplicate s) = printf "%a%a 중복 되었습니다." pv s pvtaili s | f (UnifyFail(t1,t2)) = ( TyPrint.start(); printf "@[@["; TyPrint.typ' t1; printf "@]@ 타입이어야@ 하는데@]@ @[@["; TyPrint.typ' t2; printf "@]@ 타입입니다.@]"; TyPrint.ending()) | f (TsApply(id,n,m)) = ( printf "%a의@ 인자가@ " pv (Typ,id); printf "%t야 하는데@ " (fn _ => fnum n (printf "%d 개") "없어"); printf "%t니다." (fn _ => fnum m (printf "%d 개입") "없습")) | f (RecursiveType [a,b]) = ( fv(Typ, [a]); printf "과@ "; fv(Typ, [b]); printf "의@ 정의가@ 서로 맞물려 있습니다.") | f (RecursiveType ids) = ( printf "다음 타입들의 정의가@ 서로 맞물려 있습니다:@ "; pp_list (fn s => printf "%s" s) (fn _ => printf ",@ ") ids; printf ".") | f (ConstraintSig id) = ( fv(Typ, id); printf "은@ 이미 모듈타입 내에 정의되어@ 제한할 수 없습니다.") | f (RConstraintSig id) = ( fv(Typ, id); printf "은@ 이미 제한되어@ 반복해서 제한할 수 없습니다.") | f (FunName(id1,id2)) = printf "%s 를(을) 정의하는 도중@ %s 를(을) 정의했습니다." id1 id2 | f (FunLength(n1,n2)) = printf "%d 개의 패턴이어야 하는데@ %d 개가 왔습니다." n1 n2 | f (Match(c,st,sg,(l,m))) = let val s1 = case c of FS => "정의" | _ => "모듈" val s2 = case c of FI => "접속방안" | _ => "모듈타입" in (case c of SS => printf "%a%a@ %a에@ 맞지 않습니다.@;" pstropt st pstrtaili st psigopt sg | FI => printf "%a%a@ %a의 입력으로@ 부적당합니다.@;" pstropt st pstrtaili st pfctopt sg | FS => printf "%a의 정의가@ %a에@ 맞지 않습니다.@;" pfctopt st psigopt sg); (case m of Value(x,t,s) => printf "%a의 타입이@ 적응 안되기 때문입니다.@\n" pv (Var,l@[x]); printf "@[<4>- %s에서는@ %a 이고@]@\n@[<4>- %s에서는@ %a 입니다.@]" s1 ps t s2 ps s | Domain x => let val x' = add_str l x in printf "%a%a %s에 없기 때문입니다." pv x' pvtaili x' s1 end | Type(t,r) => let val t' = (Typ, l@[t]) in case r of Arity(i,j) => let fun f1 _ = fnum i (printf "%d 개인데") "없는데" fun f2 _ = fnum j (printf "%d 개이") "없" in printf "%a의 인자가 %s에는@ %t@ %s에는@ %t기 때문입니다." pv t' s1 f1 s2 f2 end | Constype(c,sc1,sc2) => printf "%a의 데이타 구성자 %s 의 인자 타입이 다르기 때문입니다.@\n" pv t' c; printf "@[<4>- %s에서는@ " s1; fopt sc1 (printf "%a 이고" ps) (fn _ => printf "인자가 없고"); printf "@]@\n@[<4>- %s에서는@ " s2; fopt sc2 (printf "%a 입니다." ps) (fn _ => printf "인자가 없습니다") | Consexist c => printf "%a의@ 데이타 구성자 %s 가@ %s에는@ 없기 때문입니다." pv t' c s2 | Consreq c => printf "%a의@ 데이타 구성자 %s 가@ %s에@ 없기 때문입니다." pv t' c s1 | _ => printf "%a이@ 다르기 때문입니다." pv t' end) end in Location.print Format.std_formatter l; printf "@[<6>오류:@ "; f t; printf "@]" end fun pp x = pp' x fun warning (x,l) = let fun message Overload = "정수형으로 간주합니다." val ppf = Format.std_formatter val msg = "주의: "^message x val newlines = ref 0 (* val _ = for i=0; i