3742 lines · 122.1 KB · Standard ML
RawDownload
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 tyapp

Lines 1–500 of 3742.