open Misc List Fnlib Mixture Config Const Smlprim Globals Location Units; (* cvr: operations on semantic structures *) fun SofRecStr RS = case RS of RECrec(RS,RS') => SofRecStr RS' | NONrec S => S ; fun MEofStr (STRstr (ME,_,_,_,_)) = ME | MEofStr (SEQstr (Str1,Str2)) = plusEnv (MEofStr Str1) (MEofStr Str2) fun FEofStr (STRstr (_,FE,_,_,_)) = FE | FEofStr (SEQstr (Str1,Str2)) = plusEnv (FEofStr Str1) (FEofStr Str2) fun GEofStr (STRstr (_,_,GE,_,_)) = GE | GEofStr (SEQstr (Str1,Str2)) = plusEnv (GEofStr Str1) (GEofStr Str2) fun TEofStr (STRstr (_,_,_,TE,_)) = TE | TEofStr (SEQstr (Str1,Str2)) = plusEnv (TEofStr Str1) (TEofStr Str2) fun VEofStr (STRstr (_,_,_,_,VE)) = VE | VEofStr (SEQstr (Str1,Str2)) = plusEnv (VEofStr Str1) (VEofStr Str2) fun removeGEofStr S = case S of STRstr (ME,FE,NILenv,TE,VE) => S (* share if possible *) | STRstr (ME,FE,GE,TE,VE) => STRstr (ME,FE,NILenv,TE,VE) | SEQstr (S1,S2) => SEQstr (removeGEofStr S1,removeGEofStr S2) (* cvr: TODO improve sharing? *); fun removeGEofRecStr RS = case RS of RECrec(_,_) => RS | NONrec S => NONrec (removeGEofStr S); fun VEofCE (ConEnv CE : ConEnv) = foldL (fn cs => fn env => let val {qualid, info} = cs in bindInEnv env (hd(#id qualid)) {qualid = qualid, info = (#conType (!info),CONname info)} end) NILenv CE | VEofCE _ = fatalError "VEofCE"; (* cvr: paths locate errors that occur during signature matching *)datatype path = NILpath | IDpath of string | DOTpath of path * string | DOMpath of path | RNGpath of path | UNITpath ; datatype ScopeViolation = TYNAMEsv of TyName | TYPEVARsv of TypeVar;(* unification *)datatype reason = UnifyCircular | UnifyEquality | UnifyExplicit | UnifyTup | UnifyRec of Lab | UnifyOther | UnifyMod of matchReason option * matchReason option | UnifyScope of TypeVar * ScopeViolationand matchReason = MissingValue of path * string * VarInfo| MissingStructure of path * string * ModInfo| MissingFunctor of path * string * FunInfo| MissingSignature of path * string * SigInfo| MissingType of path * string * TyInfo| MissingInfixStatus of path * string * InfixStatus| InfixStatusMismatch of path * string * InfixStatus * InfixStatus| SignatureMismatch of path * string * SigInfo * SigInfo * matchReason option * matchReason option| SchemeMismatch of path * string * VarInfo * VarInfo| StatusMismatch of path * string * VarInfo * VarInfo| ConEnvMismatch of path * string * TyInfo * TyInfo| ArityMismatch of path * string * TyInfo * TyInfo * int * int| RefEqualityMismatch of path * string * TyInfo * TyInfo| EqualityMismatch of path * string * TyInfo * TyInfo| TransparentMismatch of path * string * TyInfo * TyInfo| PatternMismatch of path * string * TyStr * TyStr * TyName * ScopeViolation| CircularMismatch of path * string * TyStr * TyStr * TyName| DatatypeMismatch of path * string * TyInfo * TyInfo| ModuleMismatch of path * string * string (* path * infDesc * specDesc *); exception Unify of reason; exception MatchError of matchReason; local (* cvr: REVISE?*) (* fun mktyname qual name info = {qualid={qual=qual, id=[name]}, info=ref info} : TyName; *) fun mktyname qual name info = {qualid={qual="General", id=[name]}, info=ref info} : TyName; fun mkSML name info = mktyname "General" name info; val mkSMLStamp = let val next_stamp = ref 0 in fn () => (incr (next_stamp); ("General",!next_stamp)) endin(* Some predefined type names *)val tyname_unit = mkSML "unit" {tnStamp=mkSMLStamp(), tnKind=ARITYkind 0, tnEqu=TRUEequ, tnSort=PARAMETERts, tnLevel=0, tnConEnv=ref NONE}and tyname_bool = mkSML "bool" {tnStamp=mkSMLStamp(), tnKind=ARITYkind 0, tnEqu=TRUEequ, tnSort=PARAMETERts, tnLevel=0, tnConEnv=ref NONE}and tyname_char = mktyname "Char" "char" {tnStamp=mkSMLStamp(), tnKind=ARITYkind 0, tnEqu=TRUEequ, tnSort=PARAMETERts, tnLevel=0, tnConEnv=ref NONE}and tyname_exn = mkSML "exn" {tnStamp=mkSMLStamp(), tnKind=ARITYkind 0, tnEqu=FALSEequ, tnSort=PARAMETERts, tnLevel=0, tnConEnv=ref NONE}and tyname_frag = mkSML "frag" {tnStamp=mkSMLStamp(), tnKind=ARITYkind 1, tnEqu=TRUEequ, tnSort=PARAMETERts, tnLevel=0, tnConEnv=ref NONE}and tyname_int = mktyname "Int" "int" {tnStamp=mkSMLStamp(), tnKind=ARITYkind 0, tnEqu=TRUEequ, tnSort=PARAMETERts, tnLevel=0, tnConEnv=ref NONE}and tyname_list = mkSML "list" {tnStamp=mkSMLStamp(), tnKind=ARITYkind 1, tnEqu=TRUEequ, tnSort=PARAMETERts, tnLevel=0, tnConEnv=ref NONE}and tyname_option = mkSML "option" {tnStamp=mkSMLStamp(), tnKind=ARITYkind 1, tnEqu=TRUEequ, tnSort=PARAMETERts, tnLevel=0, tnConEnv=ref NONE}and tyname_order = mkSML "order" {tnStamp=mkSMLStamp(), tnKind=ARITYkind 0, tnEqu=TRUEequ, tnSort=PARAMETERts, tnLevel=0, tnConEnv=ref NONE}and tyname_ppstream = mkSML "ppstream" {tnStamp=mkSMLStamp(), tnKind=ARITYkind 0, tnEqu=FALSEequ, tnSort=PARAMETERts, tnLevel=0, tnConEnv=ref NONE}and tyname_real = mktyname "Real" "real" {tnStamp=mkSMLStamp(), tnKind=ARITYkind 0, tnEqu=TRUEequ, tnSort=PARAMETERts, tnLevel=0, tnConEnv=ref NONE}and tyname_ref = mkSML "ref" {tnStamp=mkSMLStamp(), tnKind=ARITYkind 1, tnEqu=REFequ, tnSort=PARAMETERts, tnLevel=0, tnConEnv=ref NONE}and tyname_string = mktyname "String" "string" {tnStamp=mkSMLStamp(), tnKind=ARITYkind 0, tnEqu=TRUEequ, tnSort=PARAMETERts, tnLevel=0, tnConEnv=ref NONE}(* cvr: REVISE hardwiring Substring.substring and the other type names seems a horrible hack - can't we simplify this? *)and tyname_substring = mktyname "Substring" "substring" {tnStamp=("Substring",1), tnKind=ARITYkind 0, tnEqu=FALSEequ, tnSort=PARAMETERts, tnLevel=0, tnConEnv=ref NONE}and tyname_syserror = mktyname "OS" "syserror" {tnStamp=mkSMLStamp(), tnKind=ARITYkind 0, tnEqu=FALSEequ, tnSort=PARAMETERts, tnLevel=0, tnConEnv=ref NONE}and tyname_vector = mkSML "vector" {tnStamp=mkSMLStamp(), tnKind=ARITYkind 1, tnEqu=TRUEequ, tnSort=PARAMETERts, tnLevel=0, tnConEnv=ref NONE}and tyname_word = mktyname "Word" "word" {tnStamp=mkSMLStamp(), tnKind=ARITYkind 0, tnEqu=TRUEequ, tnSort=PARAMETERts, tnLevel=0, tnConEnv=ref NONE}and tyname_word8 = mktyname "Word8" "word8" {tnStamp=mkSMLStamp(), tnKind=ARITYkind 0, tnEqu=TRUEequ, tnSort=PARAMETERts, tnLevel=0, tnConEnv=ref NONE}val tyname_bogus = mkSML "bogus" {tnStamp=mkSMLStamp(), tnKind=ARITYkind 0, tnEqu=TRUEequ, tnSort=PARAMETERts, tnLevel=0, tnConEnv=ref NONE};end; val type_bogus = CONt([], NAMEtyapp tyname_bogus);val sc_bogus = TypeScheme{ tscParameters=[], tscBody=type_bogus }; fun mkConInfo () = ref{ conArity=(~1), conSpan=(~1), conIsGreedy=false, conTag=(~1), conType=sc_bogus }; fun mkExConInfo () = ref{ exconArity=(~1) }; fun mkPrimInfo arity prim = { primArity=arity, primOp=prim }; (* ps: fun isExConStatic (ei : ExConInfo) = case #exconTag(!ei) of SOME _ => true | NONE => false;*) fun isNilRowType rho = case !rho of NILrow => true | VARrow _ => false | _ => fatalError "isNilRowType"; fun normalizeRecType (r: RecType) = case !(#rho(!r)) of NILrow => () | VARrow _ => () | LINKrow rho' => (setRtRho r rho'; normalizeRecType r) | FIELDrow(lab, tau, rho') => (setRtFields r (insertField (lab, tau) (#fields(!r))); setRtRho r rho'; normalizeRecType r); (* Binding levels *) val binding_level = ref 0; fun resetBindingLevel() = binding_level := 0;fun incrBindingLevel() = incr binding_level;fun decrBindingLevel() = decr binding_level;fun currentBindingLevel() = !binding_level; (* cvr: added *) fun setCurrentBindingLevel isOverloaded = fn VARt var => (setTvOvl var isOverloaded; setTvLevel var (!binding_level)) | _ => fatalError "setCurrentBindingLevel"; fun newExplicitTypeVar syntaxTypeVar = let val tv = ref { tvKind = Explicit syntaxTypeVar, tvLevel = !binding_level, tvImp = !value_polymorphism, tvEqu = false, tvOvl = false } in (case explode syntaxTypeVar of #"'" :: #"'" :: #"_" :: _ => (setTvEqu tv true; setTvImp tv true) | #"'" :: #"'" :: _ => setTvEqu tv true | #"'" :: #"_" :: _ => setTvImp tv true | _ => ()); tv end; fun mkTypeVar equ imp ovl level = ref{ tvKind = NoLink, tvEqu = equ, tvImp = !value_polymorphism orelse imp, tvOvl = ovl, tvLevel = level}; fun newTypeVar equ imp ovl = mkTypeVar equ imp ovl (!binding_level); fun newTypeVars 0 = [] | newTypeVars n = newTypeVar false false false :: newTypeVars (n-1); fun refreshTypeVar (tv : TypeVar) = let val {tvEqu, tvImp, tvOvl, ...} = !tv in newTypeVar tvEqu tvImp tvOvl end; fun isExplicit (tv : TypeVar) = let val {tvKind, ...} = !tv in case tvKind of Explicit _ => true | _ => false end; fun newUnknown() = VARt (newTypeVar false false false); (* cvr: added *) (* type parameters *)fun mkTypeParameter name equ imp ovl level = ref{ tvKind = Explicit name, tvEqu = equ, tvImp = !value_polymorphism orelse imp, tvOvl = ovl, tvLevel = level}; fun newTypeParameter equ imp ovl = mkTypeParameter "" equ imp ovl (!binding_level); fun newTypeParameters [] = [] | newTypeParameters (h::t) = ((VARt (newTypeParameter false (* cvr: should this be true? *) false false) :: newTypeParameters t)); fun refreshTypeParameter (tv : TypeVar) = let val {tvKind, tvEqu, tvImp, tvOvl, ...} = !tv val tvName = case tvKind of Explicit name => name | _ => "" in mkTypeParameter tvName tvEqu tvImp tvOvl (!binding_level) end; (* *) fun TypeOfTypeVar tv = VARt tv; fun freshNilRowType() = ref NILrow; fun mkVarRowType equ imp level = ref (VARrow (ref {rvEqu=equ, rvImp=imp, rvLevel=level})); fun kindTyName (tn:TyName) = #tnKind (!(#info tn)); fun kindTyApp tyapp = case tyapp of NAMEtyapp tn => kindTyName tn | APPtyapp (tyapp,app) => (case kindTyApp tyapp of ARROWkind(k,k') => k' | _ => fatalError "kindTyApp")and kindTyFun tyfun = case tyfun of APPtyfun tyapp => kindTyApp tyapp | LAMtyfun (tn,tyfun) => ARROWkind(kindTyName tn,kindTyFun tyfun) | TYPEtyfun (vs,tau) => ARITYkind (List.length vs); fun equTyName (tn:TyName) = #tnEqu (!(#info tn)); fun etaExpandTyApp tyapp = case kindTyApp tyapp of ARITYkind n => let val _ = incrBindingLevel(); val vs = foldInt (fn n => fn vs => newTypeParameter false false false::vs) [] n in decrBindingLevel(); TYPEtyfun(vs,CONt(map TypeOfTypeVar vs,tyapp)) end | _ => fatalError "etaExpandTyApp";fun etaExpandTyFun tyfun = case tyfun of APPtyfun tyapp => etaExpandTyApp tyapp | TYPEtyfun _ => tyfun | LAMtyfun _ => fatalError "etaExpandTyFun"; (* cvr: new, optimized and highly dodgy copying *) local fun restrictBns bns1 bns2 = drop (fn (tn1,NAMEtyapp tn1') => exists (fn (tn2,NAMEtyapp tn2') => tn1 = tn2 andalso tn1' = tn2' | _ => false) bns2 | _ => false) bns1;fun restrictBvs bvs1 bvs2 = drop (fn (tv1,VARt tv1') => exists (fn (tv2,VARt tv2') => tv1 = tv2 andalso tv1' = tv2' | _ => false) bvs2 | _ => false) bvs1;fun copyAndRealiseTyName (tn:TyName) tyfun = case tn of {qualid,info = ref { tnKind,tnEqu,tnStamp,tnSort = _, tnLevel,tnConEnv}} => {qualid = qualid, info = ref {tnKind = tnKind, tnEqu = tnEqu, tnSort = REAts tyfun, tnStamp = newTyNameStamp(), tnLevel = tnLevel, tnConEnv = ref NONE}}; fun copyEnv copyInfo bns bvs env = case env of NILenv => (bns,bvs,true,env) | BNDenv(k, info, env') => let val (bns,bvs,sinfo,cinfo) = copyInfo bns bvs info val (bns,bvs,senv',cenv') = copyEnv copyInfo bns bvs env' in if sinfo andalso senv' then (bns,bvs,true,env) else (bns,bvs,false,BNDenv(k,cinfo,cenv')) end | COMPenv(env1, env2) => let val (bns,bvs,senv1,cenv1) = copyEnv copyInfo bns bvs env1 val (bns,bvs,senv2,cenv2) = copyEnv copyInfo bns bvs env2 in if senv1 andalso senv2 then (bns,bvs,true,env) else (bns,bvs,false,COMPenv(cenv1,cenv2)) end | TOPenv(t, env') => let val ct = Hasht.new 17 val (bns,bvs,st) = Hasht.fold (fn k => fn info => fn (bns,bvs,st) => let val (bns,bvs,sinfo,cinfo) = copyInfo bns bvs info in if sinfo then (Hasht.insert ct k cinfo; (bns,bvs,st)) else (Hasht.insert ct k cinfo; (bns,bvs,false)) end) (bns,bvs,true) t val ct = if st then t else ct val (bns,bvs,senv',cenv') = copyEnv copyInfo bns bvs env' in if st andalso senv' then (bns,bvs,true,env) else (bns,bvs,false,TOPenv(ct,cenv')) end; fun copyGlobal copyInfo bns bvs (global as {qualid,info}) = let val (bns,bvs,sinfo,cinfo) = copyInfo bns bvs info in if sinfo then (bns,bvs,true,global) else (bns,bvs,false,{qualid = qualid,info = cinfo}) end; fun copyTyNameSet tnSort bns bvs T = let val bns' = map (fn tn => case tn of {qualid,info = ref {tnKind,tnEqu,tnStamp,tnSort = _,tnLevel,tnConEnv}} => let val tn' = {qualid = qualid, info = ref {tnKind = tnKind, tnEqu = tnEqu, tnSort = tnSort, tnStamp = newTyNameStamp(), tnLevel= !binding_level, tnConEnv = ref NONE}} in (tn, NAMEtyapp tn') end) T val bns'' = bns'@bns fun copyConEnvs bns bvs [] = (bns,bvs,[]) | copyConEnvs bns bvs ((tn,NAMEtyapp tn')::bns') = (case !(#tnConEnv (!(#info tn))) of NONE => let val (bns,bvs,T') = copyConEnvs bns bvs bns' in (bns,bvs,tn'::T') end | SOME conenv => let val (bns,bvs,sconenv,cconenv) = copyConEnv bns bvs conenv val (bns,bvs,T') = copyConEnvs bns bvs bns' in if sconenv then setTnConEnv (#info tn') (#tnConEnv(!(#info tn))) else setTnConEnv (#info tn') (ref (SOME cconenv)); (bns,bvs,tn'::T') end) | copyConEnvs _ _ _ = fatalError "copyConEnvs" val (bns,bvs,T') = copyConEnvs bns'' bvs bns' in (restrictBns bns bns',bvs,T',bns') endand copyTyName tnSort bns bvs tn = case copyTyNameSet tnSort bns bvs [tn] of (bns,bvs,[tn'],[tn2tn']) => (bns,bvs,tn',tn2tn') | _ => fatalError "copyTyName"and copyType bns bvs tau = case tau of VARt var => (let val ctau = lookup var bvs val stau = case ctau of VARt var' => var = var' | _ => false in (bns,bvs,stau,ctau) end handle Subscript => (case #tvKind(!var) of NoLink => (bns,bvs,true,tau) | Explicit s => (bns,bvs,true,tau) | LinkTo tau' => let val (bns,bvs,shared,tau'') = copyType bns bvs tau' in if shared then (bns,(var,tau)::bvs,true,tau) else (bns,(var,tau'')::bvs,false,tau'') end)) | ARROWt(t,u) => let val (bns,bvs,st,ct) = copyType bns bvs t val (bns,bvs,su,cu) = copyType bns bvs u in if st andalso su then (bns,bvs,true,tau) else (bns,bvs,false,ARROWt(ct,cu)) end | CONt(ts, tyapp) => let val (bns,bvs,sts,cts) = copyTypeList bns bvs ts val (bns,bvs,styapp,ctyapp) = copyTyApp bns bvs tyappLines 1–500 of 3742. Load more
open Misc List Fnlib Mixture Config Const Smlprim Globals Location Units; (* cvr: operations on semantic structures *) fun SofRecStr RS = case RS of RECrec(RS,RS') => SofRecStr RS' | NONrec S => S ; fun MEofStr (STRstr (ME,_,_,_,_)) = ME | MEofStr (SEQstr (Str1,Str2)) = plusEnv (MEofStr Str1) (MEofStr Str2) fun FEofStr (STRstr (_,FE,_,_,_)) = FE | FEofStr (SEQstr (Str1,Str2)) = plusEnv (FEofStr Str1) (FEofStr Str2) fun GEofStr (STRstr (_,_,GE,_,_)) = GE | GEofStr (SEQstr (Str1,Str2)) = plusEnv (GEofStr Str1) (GEofStr Str2) fun TEofStr (STRstr (_,_,_,TE,_)) = TE | TEofStr (SEQstr (Str1,Str2)) = plusEnv (TEofStr Str1) (TEofStr Str2) fun VEofStr (STRstr (_,_,_,_,VE)) = VE | VEofStr (SEQstr (Str1,Str2)) = plusEnv (VEofStr Str1) (VEofStr Str2) fun removeGEofStr S = case S of STRstr (ME,FE,NILenv,TE,VE) => S (* share if possible *) | STRstr (ME,FE,GE,TE,VE) => STRstr (ME,FE,NILenv,TE,VE) | SEQstr (S1,S2) => SEQstr (removeGEofStr S1,removeGEofStr S2) (* cvr: TODO improve sharing? *) ; fun removeGEofRecStr RS = case RS of RECrec(_,_) => RS | NONrec S => NONrec (removeGEofStr S) ; fun VEofCE (ConEnv CE : ConEnv) = foldL (fn cs => fn env => let val {qualid, info} = cs in bindInEnv env (hd(#id qualid)) {qualid = qualid, info = (#conType (!info),CONname info)} end) NILenv CE | VEofCE _ = fatalError "VEofCE" ; (* cvr: paths locate errors that occur during signature matching *) datatype path = NILpath | IDpath of string | DOTpath of path * string | DOMpath of path | RNGpath of path | UNITpath ; datatype ScopeViolation = TYNAMEsv of TyName | TYPEVARsv of TypeVar; (* unification *) datatype reason = UnifyCircular | UnifyEquality | UnifyExplicit | UnifyTup | UnifyRec of Lab | UnifyOther | UnifyMod of matchReason option * matchReason option | UnifyScope of TypeVar * ScopeViolation and matchReason = MissingValue of path * string * VarInfo | MissingStructure of path * string * ModInfo | MissingFunctor of path * string * FunInfo | MissingSignature of path * string * SigInfo | MissingType of path * string * TyInfo | MissingInfixStatus of path * string * InfixStatus | InfixStatusMismatch of path * string * InfixStatus * InfixStatus | SignatureMismatch of path * string * SigInfo * SigInfo * matchReason option * matchReason option | SchemeMismatch of path * string * VarInfo * VarInfo | StatusMismatch of path * string * VarInfo * VarInfo | ConEnvMismatch of path * string * TyInfo * TyInfo | ArityMismatch of path * string * TyInfo * TyInfo * int * int | RefEqualityMismatch of path * string * TyInfo * TyInfo | EqualityMismatch of path * string * TyInfo * TyInfo | TransparentMismatch of path * string * TyInfo * TyInfo | PatternMismatch of path * string * TyStr * TyStr * TyName * ScopeViolation | CircularMismatch of path * string * TyStr * TyStr * TyName | DatatypeMismatch of path * string * TyInfo * TyInfo | ModuleMismatch of path * string * string (* path * infDesc * specDesc *) ; exception Unify of reason; exception MatchError of matchReason; local (* cvr: REVISE?*) (* fun mktyname qual name info = {qualid={qual=qual, id=[name]}, info=ref info} : TyName; *) fun mktyname qual name info = {qualid={qual="General", id=[name]}, info=ref info} : TyName; fun mkSML name info = mktyname "General" name info; val mkSMLStamp = let val next_stamp = ref 0 in fn () => (incr (next_stamp); ("General",!next_stamp)) end in (* Some predefined type names *) val tyname_unit = mkSML "unit" {tnStamp=mkSMLStamp(), tnKind=ARITYkind 0, tnEqu=TRUEequ, tnSort=PARAMETERts, tnLevel=0, tnConEnv=ref NONE} and tyname_bool = mkSML "bool" {tnStamp=mkSMLStamp(), tnKind=ARITYkind 0, tnEqu=TRUEequ, tnSort=PARAMETERts, tnLevel=0, tnConEnv=ref NONE} and tyname_char = mktyname "Char" "char" {tnStamp=mkSMLStamp(), tnKind=ARITYkind 0, tnEqu=TRUEequ, tnSort=PARAMETERts, tnLevel=0, tnConEnv=ref NONE} and tyname_exn = mkSML "exn" {tnStamp=mkSMLStamp(), tnKind=ARITYkind 0, tnEqu=FALSEequ, tnSort=PARAMETERts, tnLevel=0, tnConEnv=ref NONE} and tyname_frag = mkSML "frag" {tnStamp=mkSMLStamp(), tnKind=ARITYkind 1, tnEqu=TRUEequ, tnSort=PARAMETERts, tnLevel=0, tnConEnv=ref NONE} and tyname_int = mktyname "Int" "int" {tnStamp=mkSMLStamp(), tnKind=ARITYkind 0, tnEqu=TRUEequ, tnSort=PARAMETERts, tnLevel=0, tnConEnv=ref NONE} and tyname_list = mkSML "list" {tnStamp=mkSMLStamp(), tnKind=ARITYkind 1, tnEqu=TRUEequ, tnSort=PARAMETERts, tnLevel=0, tnConEnv=ref NONE} and tyname_option = mkSML "option" {tnStamp=mkSMLStamp(), tnKind=ARITYkind 1, tnEqu=TRUEequ, tnSort=PARAMETERts, tnLevel=0, tnConEnv=ref NONE} and tyname_order = mkSML "order" {tnStamp=mkSMLStamp(), tnKind=ARITYkind 0, tnEqu=TRUEequ, tnSort=PARAMETERts, tnLevel=0, tnConEnv=ref NONE} and tyname_ppstream = mkSML "ppstream" {tnStamp=mkSMLStamp(), tnKind=ARITYkind 0, tnEqu=FALSEequ, tnSort=PARAMETERts, tnLevel=0, tnConEnv=ref NONE} and tyname_real = mktyname "Real" "real" {tnStamp=mkSMLStamp(), tnKind=ARITYkind 0, tnEqu=TRUEequ, tnSort=PARAMETERts, tnLevel=0, tnConEnv=ref NONE} and tyname_ref = mkSML "ref" {tnStamp=mkSMLStamp(), tnKind=ARITYkind 1, tnEqu=REFequ, tnSort=PARAMETERts, tnLevel=0, tnConEnv=ref NONE} and tyname_string = mktyname "String" "string" {tnStamp=mkSMLStamp(), tnKind=ARITYkind 0, tnEqu=TRUEequ, tnSort=PARAMETERts, tnLevel=0, tnConEnv=ref NONE} (* cvr: REVISE hardwiring Substring.substring and the other type names seems a horrible hack - can't we simplify this? *) and tyname_substring = mktyname "Substring" "substring" {tnStamp=("Substring",1), tnKind=ARITYkind 0, tnEqu=FALSEequ, tnSort=PARAMETERts, tnLevel=0, tnConEnv=ref NONE} and tyname_syserror = mktyname "OS" "syserror" {tnStamp=mkSMLStamp(), tnKind=ARITYkind 0, tnEqu=FALSEequ, tnSort=PARAMETERts, tnLevel=0, tnConEnv=ref NONE} and tyname_vector = mkSML "vector" {tnStamp=mkSMLStamp(), tnKind=ARITYkind 1, tnEqu=TRUEequ, tnSort=PARAMETERts, tnLevel=0, tnConEnv=ref NONE} and tyname_word = mktyname "Word" "word" {tnStamp=mkSMLStamp(), tnKind=ARITYkind 0, tnEqu=TRUEequ, tnSort=PARAMETERts, tnLevel=0, tnConEnv=ref NONE} and tyname_word8 = mktyname "Word8" "word8" {tnStamp=mkSMLStamp(), tnKind=ARITYkind 0, tnEqu=TRUEequ, tnSort=PARAMETERts, tnLevel=0, tnConEnv=ref NONE} val tyname_bogus = mkSML "bogus" {tnStamp=mkSMLStamp(), tnKind=ARITYkind 0, tnEqu=TRUEequ, tnSort=PARAMETERts, tnLevel=0, tnConEnv=ref NONE}; end; val type_bogus = CONt([], NAMEtyapp tyname_bogus); val sc_bogus = TypeScheme{ tscParameters=[], tscBody=type_bogus }; fun mkConInfo () = ref{ conArity=(~1), conSpan=(~1), conIsGreedy=false, conTag=(~1), conType=sc_bogus } ; fun mkExConInfo () = ref{ exconArity=(~1) }; fun mkPrimInfo arity prim = { primArity=arity, primOp=prim } ; (* ps: fun isExConStatic (ei : ExConInfo) = case #exconTag(!ei) of SOME _ => true | NONE => false ; *) fun isNilRowType rho = case !rho of NILrow => true | VARrow _ => false | _ => fatalError "isNilRowType" ; fun normalizeRecType (r: RecType) = case !(#rho(!r)) of NILrow => () | VARrow _ => () | LINKrow rho' => (setRtRho r rho'; normalizeRecType r) | FIELDrow(lab, tau, rho') => (setRtFields r (insertField (lab, tau) (#fields(!r))); setRtRho r rho'; normalizeRecType r) ; (* Binding levels *) val binding_level = ref 0; fun resetBindingLevel() = binding_level := 0; fun incrBindingLevel() = incr binding_level; fun decrBindingLevel() = decr binding_level; fun currentBindingLevel() = !binding_level; (* cvr: added *) fun setCurrentBindingLevel isOverloaded = fn VARt var => (setTvOvl var isOverloaded; setTvLevel var (!binding_level)) | _ => fatalError "setCurrentBindingLevel" ; fun newExplicitTypeVar syntaxTypeVar = let val tv = ref { tvKind = Explicit syntaxTypeVar, tvLevel = !binding_level, tvImp = !value_polymorphism, tvEqu = false, tvOvl = false } in (case explode syntaxTypeVar of #"'" :: #"'" :: #"_" :: _ => (setTvEqu tv true; setTvImp tv true) | #"'" :: #"'" :: _ => setTvEqu tv true | #"'" :: #"_" :: _ => setTvImp tv true | _ => ()); tv end; fun mkTypeVar equ imp ovl level = ref { tvKind = NoLink, tvEqu = equ, tvImp = !value_polymorphism orelse imp, tvOvl = ovl, tvLevel = level }; fun newTypeVar equ imp ovl = mkTypeVar equ imp ovl (!binding_level) ; fun newTypeVars 0 = [] | newTypeVars n = newTypeVar false false false :: newTypeVars (n-1) ; fun refreshTypeVar (tv : TypeVar) = let val {tvEqu, tvImp, tvOvl, ...} = !tv in newTypeVar tvEqu tvImp tvOvl end ; fun isExplicit (tv : TypeVar) = let val {tvKind, ...} = !tv in case tvKind of Explicit _ => true | _ => false end; fun newUnknown() = VARt (newTypeVar false false false) ; (* cvr: added *) (* type parameters *) fun mkTypeParameter name equ imp ovl level = ref { tvKind = Explicit name, tvEqu = equ, tvImp = !value_polymorphism orelse imp, tvOvl = ovl, tvLevel = level }; fun newTypeParameter equ imp ovl = mkTypeParameter "" equ imp ovl (!binding_level) ; fun newTypeParameters [] = [] | newTypeParameters (h::t) = ((VARt (newTypeParameter false (* cvr: should this be true? *) false false) :: newTypeParameters t)) ; fun refreshTypeParameter (tv : TypeVar) = let val {tvKind, tvEqu, tvImp, tvOvl, ...} = !tv val tvName = case tvKind of Explicit name => name | _ => "" in mkTypeParameter tvName tvEqu tvImp tvOvl (!binding_level) end ; (* *) fun TypeOfTypeVar tv = VARt tv; fun freshNilRowType() = ref NILrow; fun mkVarRowType equ imp level = ref (VARrow (ref {rvEqu=equ, rvImp=imp, rvLevel=level})) ; fun kindTyName (tn:TyName) = #tnKind (!(#info tn)); fun kindTyApp tyapp = case tyapp of NAMEtyapp tn => kindTyName tn | APPtyapp (tyapp,app) => (case kindTyApp tyapp of ARROWkind(k,k') => k' | _ => fatalError "kindTyApp") and kindTyFun tyfun = case tyfun of APPtyfun tyapp => kindTyApp tyapp | LAMtyfun (tn,tyfun) => ARROWkind(kindTyName tn,kindTyFun tyfun) | TYPEtyfun (vs,tau) => ARITYkind (List.length vs) ; fun equTyName (tn:TyName) = #tnEqu (!(#info tn)); fun etaExpandTyApp tyapp = case kindTyApp tyapp of ARITYkind n => let val _ = incrBindingLevel(); val vs = foldInt (fn n => fn vs => newTypeParameter false false false::vs) [] n in decrBindingLevel(); TYPEtyfun(vs,CONt(map TypeOfTypeVar vs,tyapp)) end | _ => fatalError "etaExpandTyApp"; fun etaExpandTyFun tyfun = case tyfun of APPtyfun tyapp => etaExpandTyApp tyapp | TYPEtyfun _ => tyfun | LAMtyfun _ => fatalError "etaExpandTyFun"; (* cvr: new, optimized and highly dodgy copying *) local fun restrictBns bns1 bns2 = drop (fn (tn1,NAMEtyapp tn1') => exists (fn (tn2,NAMEtyapp tn2') => tn1 = tn2 andalso tn1' = tn2' | _ => false) bns2 | _ => false) bns1; fun restrictBvs bvs1 bvs2 = drop (fn (tv1,VARt tv1') => exists (fn (tv2,VARt tv2') => tv1 = tv2 andalso tv1' = tv2' | _ => false) bvs2 | _ => false) bvs1; fun copyAndRealiseTyName (tn:TyName) tyfun = case tn of {qualid,info = ref { tnKind,tnEqu,tnStamp,tnSort = _, tnLevel,tnConEnv}} => {qualid = qualid, info = ref {tnKind = tnKind, tnEqu = tnEqu, tnSort = REAts tyfun, tnStamp = newTyNameStamp(), tnLevel = tnLevel, tnConEnv = ref NONE}} ; fun copyEnv copyInfo bns bvs env = case env of NILenv => (bns,bvs,true,env) | BNDenv(k, info, env') => let val (bns,bvs,sinfo,cinfo) = copyInfo bns bvs info val (bns,bvs,senv',cenv') = copyEnv copyInfo bns bvs env' in if sinfo andalso senv' then (bns,bvs,true,env) else (bns,bvs,false,BNDenv(k,cinfo,cenv')) end | COMPenv(env1, env2) => let val (bns,bvs,senv1,cenv1) = copyEnv copyInfo bns bvs env1 val (bns,bvs,senv2,cenv2) = copyEnv copyInfo bns bvs env2 in if senv1 andalso senv2 then (bns,bvs,true,env) else (bns,bvs,false,COMPenv(cenv1,cenv2)) end | TOPenv(t, env') => let val ct = Hasht.new 17 val (bns,bvs,st) = Hasht.fold (fn k => fn info => fn (bns,bvs,st) => let val (bns,bvs,sinfo,cinfo) = copyInfo bns bvs info in if sinfo then (Hasht.insert ct k cinfo; (bns,bvs,st)) else (Hasht.insert ct k cinfo; (bns,bvs,false)) end) (bns,bvs,true) t val ct = if st then t else ct val (bns,bvs,senv',cenv') = copyEnv copyInfo bns bvs env' in if st andalso senv' then (bns,bvs,true,env) else (bns,bvs,false,TOPenv(ct,cenv')) end ; fun copyGlobal copyInfo bns bvs (global as {qualid,info}) = let val (bns,bvs,sinfo,cinfo) = copyInfo bns bvs info in if sinfo then (bns,bvs,true,global) else (bns,bvs,false,{qualid = qualid,info = cinfo}) end ; fun copyTyNameSet tnSort bns bvs T = let val bns' = map (fn tn => case tn of {qualid,info = ref {tnKind,tnEqu,tnStamp,tnSort = _,tnLevel,tnConEnv}} => let val tn' = {qualid = qualid, info = ref {tnKind = tnKind, tnEqu = tnEqu, tnSort = tnSort, tnStamp = newTyNameStamp(), tnLevel= !binding_level, tnConEnv = ref NONE}} in (tn, NAMEtyapp tn') end) T val bns'' = bns'@bns fun copyConEnvs bns bvs [] = (bns,bvs,[]) | copyConEnvs bns bvs ((tn,NAMEtyapp tn')::bns') = (case !(#tnConEnv (!(#info tn))) of NONE => let val (bns,bvs,T') = copyConEnvs bns bvs bns' in (bns,bvs,tn'::T') end | SOME conenv => let val (bns,bvs,sconenv,cconenv) = copyConEnv bns bvs conenv val (bns,bvs,T') = copyConEnvs bns bvs bns' in if sconenv then setTnConEnv (#info tn') (#tnConEnv(!(#info tn))) else setTnConEnv (#info tn') (ref (SOME cconenv)); (bns,bvs,tn'::T') end) | copyConEnvs _ _ _ = fatalError "copyConEnvs" val (bns,bvs,T') = copyConEnvs bns'' bvs bns' in (restrictBns bns bns',bvs,T',bns') end and copyTyName tnSort bns bvs tn = case copyTyNameSet tnSort bns bvs [tn] of (bns,bvs,[tn'],[tn2tn']) => (bns,bvs,tn',tn2tn') | _ => fatalError "copyTyName" and copyType bns bvs tau = case tau of VARt var => (let val ctau = lookup var bvs val stau = case ctau of VARt var' => var = var' | _ => false in (bns,bvs,stau,ctau) end handle Subscript => (case #tvKind(!var) of NoLink => (bns,bvs,true,tau) | Explicit s => (bns,bvs,true,tau) | LinkTo tau' => let val (bns,bvs,shared,tau'') = copyType bns bvs tau' in if shared then (bns,(var,tau)::bvs,true,tau) else (bns,(var,tau'')::bvs,false,tau'') end)) | ARROWt(t,u) => let val (bns,bvs,st,ct) = copyType bns bvs t val (bns,bvs,su,cu) = copyType bns bvs u in if st andalso su then (bns,bvs,true,tau) else (bns,bvs,false,ARROWt(ct,cu)) end | CONt(ts, tyapp) => let val (bns,bvs,sts,cts) = copyTypeList bns bvs ts val (bns,bvs,styapp,ctyapp) = copyTyApp bns bvs tyapp