1open List; 2open Fnlib Config Mixture Const Smlexc; 3open Globals Location Units Asynt Asyntfn Types; 4open Primdec Smlprim; 5 6 7type UEnv = (string * Type) list; (* Syntax TyVars to TypeVars *) 8 9val piRef = mkPrimInfo 1 MLPref; 10 11fun mkPrimStatus arity name = 12 PRIMname(mkPrimInfo arity (findPrimitive arity name)) 13; 14 15(* --- Warning printing --- *) 16 17fun isFunType tau = 18 case normType tau of 19 ARROWt _ => true 20 | _ => false 21; 22 23fun unitResultExpected exp tau = 24 if isFunType tau then 25 (msgIBlock 0; 26 errLocation (xLR exp); 27 errPrompt "Warning: function-type result is being discarded."; 28 msgEOL(); msgEOL(); 29 msgEBlock()) 30 else () 31; 32 33(* --- Error printing --- *) 34 35fun typeClash tau1 tau2 reason = 36 under_binder 37 (fn (tau1,tau2,reason) => 38 let fun isEqVar tau = case normType tau of 39 VARt var => #tvEqu (!var) 40 | _ => false 41 fun isExVar tau = case normType tau of 42 VARt var => isExplicit var 43 | _ => false 44 fun msgTy tau = 45 if (case reason of 46 UnifyEquality => true 47 | _ => false) 48 andalso isEqVar tau then 49 (msgString "equality type "; printNextType tau) 50 else if (case reason of 51 UnifyExplicit => true 52 | UnifyOther => true 53 | UnifyEquality => true 54 | UnifyScope _ => true 55 | _ => false) 56 andalso isExVar tau then 57 (msgString "explicit type "; printNextType tau) 58 else 59 (msgString "type"; msgEOL(); 60 errPrompt " "; printNextType tau) 61 in 62 collectExplicitVars tau1; 63 collectExplicitVars tau2; 64 msgString " of "; msgTy tau1; msgEOL(); 65 errPrompt "cannot have "; msgTy tau2; msgEOL(); 66 (case reason of 67 UnifyCircular => 68 (errPrompt "because of circularity"; msgEOL()) 69 | UnifyEquality => () 70 | UnifyExplicit => () 71 | UnifyScope (var,TYNAMEsv tn) => 72 (errPrompt "because of a scope violation:"; 73 msgEOL(); 74 errPrompt "the type constructor "; 75 prTyName false tn; 76 msgString " is a parameter " ; 77 msgEOL(); 78 errPrompt "that is declared within \ 79 \the scope of "; 80 prTypeVar var; 81 msgEOL()) 82 | UnifyScope (var,TYPEVARsv tv) => 83 (errPrompt "because of a scope violation:"; 84 msgEOL(); 85 errPrompt "the type variable "; 86 prTypeVar tv; 87 msgString " is a parameter " ; 88 msgEOL(); 89 errPrompt "that is declared within \ 90 \the scope of "; 91 prTypeVar var; 92 msgEOL()) 93 | UnifyTup => 94 (errPrompt "because the tuple has the\ 95 \ wrong number of components"; 96 msgEOL()) 97 | UnifyRec lab => 98 (errPrompt "because record label "; 99 printLab lab; msgString " is missing"; msgEOL()) 100 | UnifyMod (reasonopt,reasonopt') => 101 (case reasonopt of 102 NONE => () 103 | SOME reason => 104 (errPrompt "because the first module type \ 105 \does not match the second module type ..."; 106 msgEOL(); 107 errMatchReason "first module type" "second module type" reason); 108 case reasonopt' of 109 NONE => () 110 | SOME reason => 111 (errPrompt "because the second module type \ 112 \does not match the first module type ..."; 113 msgEOL(); 114 errMatchReason "second module type" "first module type" reason)) 115 | UnifyOther => ()) 116 end) 117 (tau1,tau2,reason); 118 119fun typeClashId (ii : IdInfo) tau1 tau2 reason = 120 let val {qualid, info} = ii in 121 msgIBlock 0; 122 errLocation (#idLoc info); 123 errPrompt "Type clash: identifier "; msgString (showQualId qualid); 124 typeClash tau1 tau2 reason; 125 msgEBlock(); 126 raise Toplevel 127 end 128; 129 130fun unifyId ii tau1 tau2 = 131 unify tau1 tau2 132 handle Unify reason => typeClashId ii tau1 tau2 reason 133; 134 135fun typeClashPat pat tau1 tau2 reason = 136( 137 msgIBlock 0; 138 errLocation (xLR pat); 139 errPrompt "Type clash: pattern"; 140 typeClash tau1 tau2 reason; 141 msgEBlock(); 142 raise Toplevel 143); 144 145fun unifyPat pat tau1 tau2 = 146 unify tau1 tau2 147 handle Unify reason => typeClashPat pat tau1 tau2 reason 148; 149 150fun typeClashExp exp tau1 tau2 reason = 151( 152 msgIBlock 0; 153 errLocation (xLR exp); 154 errPrompt "Type clash: expression"; 155 typeClash tau1 tau2 reason; 156 msgEBlock(); 157 raise Toplevel 158); 159 160fun unifyExp exp tau1 tau2 = 161 unify tau1 tau2 162 handle Unify reason => typeClashExp exp tau1 tau2 reason 163; 164 165fun unifyMatch mrules tau1 tau2 = 166 unify tau1 tau2 167 handle Unify reason => 168 let val MRule(ref pats, exp) = hd mrules in 169 msgIBlock 0; 170 errLocation (xxLR (hd pats) exp); 171 errPrompt "Type clash: match rule"; 172 typeClash tau1 tau2 reason; 173 msgEBlock(); 174 raise Toplevel 175 end 176; 177 178fun looksLikeInfixId (ii : IdInfo) = 179 case ii of 180 {qualid={qual="", id = [_]}, info={withOp=false, ...}} => true 181 | _ => false 182; 183 184fun isPairPat (_, pat') = 185 case pat' of 186 RECpat(ref (RECrp(fs, NONE))) => isPairRow fs 187 | _ => false 188; 189 190(* 191fun looksLikeInfixExp (_, exp') = 192 case exp' of 193 VARexp(ref(RESve{qualid={qual=[],...}, info={withOp=false,...}})) 194 => true 195 | VARexp(ref(OVLve({qualid={qual=[],...}, info={withOp=false,...}}, _, _))) 196 => true 197 | _ => false 198; 199*) 200 201fun looksLikeInfixExp (_, exp') = 202 case exp' of 203 VIDPATHexp(ref(RESvidpath ({qualid={qual="",id=[_]}, info={withOp=false,...}}))) 204 => true 205 | VIDPATHexp(ref(OVLvidpath ({qualid={qual="",id=[_]}, info={withOp=false,...}}, _, _))) 206 => true 207 | _ => false 208; 209 210 211 212fun isPairExp (_, exp') = 213 case exp' of 214 RECexp(ref (RECre fs)) => isPairRow fs 215 | _ => false 216; 217 218fun newUnknownPair() = type_pair (newUnknown()) (newUnknown()); 219 220infix 6 U; infix 7 \\; 221 222fun list_union [] ys = ys 223 | list_union (x :: xs) ys = 224 if member x ys then (list_union xs ys) else (x :: list_union xs ys) 225 226fun list_subtract xs [] = xs 227 | list_subtract xs ys = 228 let fun h [] = [] 229 | h (x :: xs) = if member x ys then (h xs) else (x :: h xs) 230 in h xs end 231; 232 233fun xs U ys = list_union xs ys; 234fun U_map f = foldR_map list_union f []; 235fun xs \\ ys = list_subtract xs ys; 236 237infix 7 without; 238 239fun xs without (tyvarseq:TyVarSeq) = 240 xs \\ (map (fn ii => hd(#id(#qualid ii))) tyvarseq); 241 242fun unguardedExp (_, exp') = 243 case exp' of 244 SCONexp _ => [] 245 | VIDPATHexp (ref (RESvidpath (_))) => [] 246 | VIDPATHexp (ref (OVLvidpath (_,ovlty,ty))) => [] 247 | RECexp(ref (RECre fields)) => 248 U_map (fn(_, e) => unguardedExp e) fields 249 | RECexp(ref (TUPLEre es)) => 250 U_map unguardedExp es 251 | VECexp es => 252 U_map unguardedExp es 253 | LETexp(dec, exp) => 254 unguardedDec dec U unguardedExp exp 255 | PARexp exp => unguardedExp exp 256 | APPexp(exp1, exp2) => 257 unguardedExp exp1 U unguardedExp exp2 258 | INFIXexp (ref (UNRESinfixexp es)) => 259 U_map unguardedExp es 260 | INFIXexp (ref (RESinfixexp e)) => unguardedExp e 261 | TYPEDexp(exp, ty) => 262 unguardedExp exp U unguardedTy ty 263 | ANDALSOexp(exp1, exp2) => 264 unguardedExp exp1 U unguardedExp exp2 265 | ORELSEexp(exp1, exp2) => 266 unguardedExp exp1 U unguardedExp exp2 267 | HANDLEexp(exp, mrules) => 268 unguardedExp exp U U_map unguardedMRule mrules 269 | RAISEexp exp => 270 unguardedExp exp 271 | IFexp(e0, e1, e2) => 272 unguardedExp e0 U unguardedExp e1 U unguardedExp e2 273 | FNexp mrules => 274 U_map unguardedMRule mrules 275 | WHILEexp(exp1, exp2) => 276 unguardedExp exp1 U unguardedExp exp2 277 | SEQexp(exp1, exp2) => 278 unguardedExp exp1 U unguardedExp exp2 279 | STRUCTUREexp(modexp,sigexp,_) => 280 unguardedModExp modexp U unguardedSigExp sigexp 281 | FUNCTORexp(modexp,sigexp,_) => 282 unguardedModExp modexp U unguardedSigExp sigexp 283and unguardedMRule (MRule(ref pats, exp)) = 284 U_map unguardedPat pats U unguardedExp exp 285and unguardedPat (_, pat') = 286 case pat' of 287 SCONpat _ => [] 288 | VARpat _ => [] 289 | WILDCARDpat => [] 290 | NILpat _ => [] 291 | CONSpat(_, p) => unguardedPat p 292 | EXNILpat _ => [] 293 | EXCONSpat(_,p) => unguardedPat p 294 | EXNAMEpat _ => fatalError "unguardedPat" 295(* cvr: TODO review *) 296 | REFpat p => unguardedPat p 297 | RECpat(ref (RECrp(fs, _))) => 298 U_map (fn(_, p) => unguardedPat p) fs 299 | RECpat(ref (TUPLErp _)) => fatalError "unguardedPat" 300(* cvr: TODO review *) 301 | VECpat ps => 302 U_map unguardedPat ps 303 | INFIXpat (ref (RESinfixpat p)) => unguardedPat p 304 | INFIXpat (ref (UNRESinfixpat _)) => fatalError "unguardedPat" 305(* cvr: TODO review *) 306 | PARpat pat => unguardedPat pat 307 | TYPEDpat(pat, ty) => 308 unguardedPat pat U unguardedTy ty 309 | LAYEREDpat(pat1, pat2) => 310 unguardedPat pat1 U unguardedPat pat2 311 312and unguardedDec (_, dec') = 313 case dec' of 314 VALdec _ => [] 315 | PRIM_VALdec _ => [] 316 | FUNdec (ref (UNRESfundec (tyvarseq, fvbds))) => fatalError "unguardedDec" 317(* cvr: TODO review *) 318 | FUNdec (ref (RESfundec dec)) => unguardedDec dec 319 | TYPEdec tbds => 320 U_map unguardedTypBind tbds 321 | PRIM_TYPEdec _ => [] 322 | DATATYPEdec (dbds,SOME tbds) => 323 (U_map unguardedDatBind dbds) U 324 (U_map unguardedTypBind tbds) 325 | DATATYPEdec (dbds,NONE) => 326 U_map unguardedDatBind dbds 327 | DATATYPErepdec (tycon, tyconpath) => 328 unguardedTyConPath tyconpath 329 | ABSTYPEdec(dbds,SOME tbds,dec) => 330 (U_map unguardedDatBind dbds) U 331 (U_map unguardedTypBind tbds) U 332 unguardedDec dec 333 | ABSTYPEdec(dbds,NONE,dec) => 334 (U_map unguardedDatBind dbds) U 335 unguardedDec dec 336 | EXCEPTIONdec ebs => 337 U_map unguardedExBind ebs 338 | LOCALdec (dec1, dec2) => 339 unguardedDec dec1 U unguardedDec dec2 340 | OPENdec _ => [] 341 | EMPTYdec => [] 342 | SEQdec (dec1, dec2) => 343 unguardedDec dec1 U unguardedDec dec2 344 | FIXITYdec _ => [] 345 | STRUCTUREdec mbds => 346 U_map unguardedModBind mbds 347 | FUNCTORdec fbds => 348 U_map unguardedFunBind fbds 349 | SIGNATUREdec sbds => 350 U_map unguardedSigBind sbds 351and unguardedExBind (EXDECexbind(_, SOME ty)) = unguardedTy ty 352 | unguardedExBind (EXDECexbind(_, NONE)) = [] 353 | unguardedExBind (EXEQUALexbind(_,_)) = [] 354and unguardedValBind (ValBind(ref pat, exp)) = 355 unguardedPat pat U unguardedExp exp 356and unguardedPrimValBindList (pbs) = 357 (U_map (fn (ii,ty,arity,n) => unguardedTy ty) pbs) 358and unguardedValDec (pvbs, rvbs) = 359 (U_map unguardedValBind pvbs) U 360 (U_map unguardedValBind rvbs) 361and unguardedTy (_, ty') = 362 case ty' of 363 TYVARty ii => [hd(#id(#qualid ii))] 364 | RECty fs => 365 U_map (fn(_, ty) => unguardedTy ty) fs 366 | CONty(tys, tyconpath) => 367 (U_map unguardedTy tys) U unguardedTyConPath tyconpath 368 | FNty(ty1, ty2) => 369 unguardedTy ty1 U unguardedTy ty2 370 | PACKty(sigexp) => 371 unguardedSigExp sigexp 372 | PARty(ty) => 373 unguardedTy ty 374and unguardedModBind (MODBINDmodbind(modid,modexp)) = 375 unguardedModExp modexp 376 | unguardedModBind (ASmodbind(modid,sigexp,exp)) = 377 (unguardedSigExp sigexp U 378 unguardedExp exp) 379and unguardedSigBind (SIGBINDsigbind(sigid,sigexp)) = 380 unguardedSigExp sigexp 381and unguardedFunBind (FUNBINDfunbind(funid,modexp)) = 382 unguardedModExp modexp 383 | unguardedFunBind (ASfunbind(funid,sigexp,exp)) = 384 (unguardedSigExp sigexp U 385 unguardedExp exp) 386and unguardedModExp (_,(modexp,_)) = 387 case modexp of 388 DECmodexp dec => 389 unguardedDec dec 390 | LONGmodexp _ => [] 391 | LETmodexp (dec,modexp) => 392 unguardedDec dec U unguardedModExp modexp 393 | PARmodexp modexp => 394 unguardedModExp modexp 395 | CONmodexp (modexp,sigexp) => 396 unguardedModExp modexp U unguardedSigExp sigexp 397 | ABSmodexp (modexp,sigexp) => 398 unguardedModExp modexp U unguardedSigExp sigexp 399 | FUNCTORmodexp (_,modid,_, sigexp, modexp) => 400 unguardedSigExp sigexp U unguardedModExp modexp 401 | APPmodexp (modexp,modexp') => 402 unguardedModExp modexp U unguardedModExp modexp' 403 | RECmodexp (modid,_,sigexp, modexp) => 404 unguardedSigExp sigexp U unguardedModExp modexp 405and unguardedSigExp (_,sigexp) = 406 case sigexp of 407 SPECsigexp spec => unguardedSpec spec 408 | SIGIDsigexp _ => [] 409 | WHEREsigexp (sigexp, tyvarseq, longtycon, ty) => 410 (unguardedSigExp sigexp U (unguardedTy ty without tyvarseq)) 411 | FUNSIGsigexp (_,modid, sigexp,sigexp') => 412 (unguardedSigExp sigexp U unguardedSigExp sigexp') 413 | RECsigexp (modid, sigexp,sigexp') => 414 (unguardedSigExp sigexp U unguardedSigExp sigexp') 415and unguardedSpec (_, spec') = 416 case spec' of 417 VALspec _ => [] 418 | PRIM_VALspec _ => [] 419 | TYPEDESCspec _ => [] 420 | TYPEspec tbds => U_map unguardedTypBind tbds 421 | DATATYPEspec (dbds,SOME tbds) => 422 (U_map unguardedDatBind dbds) U 423 (U_map unguardedTypBind tbds) 424 | DATATYPEspec (dbds,NONE) => 425 U_map unguardedDatBind dbds 426 | DATATYPErepspec (tycon, tyconpath) => 427 unguardedTyConPath tyconpath 428 | EXCEPTIONspec eds => U_map unguardedExDesc eds 429 | LOCALspec(spec1, spec2) => 430 unguardedSpec spec1 U unguardedSpec spec2 431 | OPENspec _ => [] 432 | EMPTYspec => [] 433 | SEQspec(spec1, spec2) => 434 unguardedSpec spec1 U unguardedSpec spec2 435 | INCLUDEspec sigexp => 436 unguardedSigExp sigexp 437 | STRUCTUREspec moddescs => 438 U_map unguardedModDesc moddescs 439 | FUNCTORspec fundescs => 440 U_map unguardedFunDesc fundescs 441 | SHARINGTYPEspec (spec, longtycons) => 442 unguardedSpec spec 443 | SHARINGspec (spec, longmodids) => 444 unguardedSpec spec 445 | FIXITYspec _ => 446 [] 447 | SIGNATUREspec sigdescs => 448 U_map unguardedSigBind sigdescs 449and unguardedModDesc (MODDESCmoddesc(modid,sigexp)) = 450 unguardedSigExp sigexp 451and unguardedFunDesc (FUNDESCfundesc(funid,sigexp)) = 452 unguardedSigExp sigexp 453and unguardedTyConPath (_,LONGtyconpath _) = [] 454 | unguardedTyConPath (_,WHEREtyconpath (_,_,modexp)) = 455 unguardedModExp modexp 456and unguardedTypBind (tyvarseq,tycon,ty) = 457 unguardedTy ty without tyvarseq 458and unguardedExDesc (_,SOME ty) = 459 unguardedTy ty 460 | unguardedExDesc (_,NONE) = [] 461and unguardedDatBind (tyvarseq, tycon, cbds) = 462 (U_map unguardedConBind cbds) without tyvarseq 463and unguardedConBind (ConBind (ii, NONE)) = [] 464 | unguardedConBind (ConBind (ii, SOME ty)) = unguardedTy ty 465and unguardedValDescList (vds) = 466 (U_map (fn (ii,ty) => unguardedTy ty) vds) 467; 468 469(* cvr: TODO the original definition of scopedTyVars appears to be wrong, 470 since a variable in pars will not be scoped, 471 if it is already scoped in UE 472fun scopedTyVars UE pars unguardedTyVars = 473 list_subtract (pars U unguardedTyVars) (map fst UE) 474; 475*) 476(* cvr: REVIEW I think the correct definitions should be: *) 477fun scopedTyVars loc UE pars unguardedTyVars = 478 let val scopedtyvars = map fst UE 479 in 480 if (!currentCompliance) <> Liberal 481 then (app (fn v => 482 if member v scopedtyvars 483 then case !currentCompliance of 484 Orthodox => 485 (msgIBlock 0; 486 errLocation loc; 487 errPrompt "Compliance Error: ";msgEOL(); 488 errPrompt "The phrase, although accepted as a Moscow ML extension,";msgEOL(); 489 errPrompt "is not supported by the Definition of Standard ML:"; msgEOL(); 490 errPrompt "the explicit type variable ";msgEOL(); 491 errPrompt " "; msgString v;msgEOL(); 492 errPrompt "is already in scope and should not be redeclared"; 493 msgEOL(); 494 msgEBlock(); 495 raise Toplevel) 496 | Conservative => 497 (msgIBlock 0; 498 errLocation loc; 499 errPrompt "Compliance Warning: ";msgEOL(); 500 errPrompt "The phrase, although accepted as a Moscow ML extension,";msgEOL(); 501 errPrompt "is not supported by the Definition of Standard ML:"; msgEOL(); 502 errPrompt "the explicit type variable ";msgEOL(); 503 errPrompt " "; msgString v;msgEOL(); 504 errPrompt "is already in scope and should not be redeclared"; 505 msgEOL(); 506 msgEBlock()) 507 | _ => () 508 else ()) 509 pars) 510 else (); 511 (pars U (list_subtract unguardedTyVars scopedtyvars)) 512 end 513 514; 515 516fun incrUE tyvars = 517 map (fn tv => (tv, TypeOfTypeVar(newExplicitTypeVar tv))) tyvars 518; 519 520(* Modified to allow more forms of non-expansive expressions: *) 521 522fun isExpansiveExp (_, exp') = 523 case exp' of 524 SCONexp _ => false 525 | VIDPATHexp (ref (RESvidpath (_))) => false 526 | VIDPATHexp (ref (OVLvidpath (_,ovlty,ty))) => false 527 | PARexp exp => isExpansiveExp exp 528 | TYPEDexp(exp,_) => isExpansiveExp exp 529 | FNexp _ => false 530 | RECexp (ref (RECre exprow)) => 531 exists (fn (_, e) => isExpansiveExp e) exprow 532 | RECexp (ref (TUPLEre explist)) => 533 exists isExpansiveExp explist 534 | APPexp((_, VIDPATHexp (ref(RESvidpath ii))), exp) => 535 isExpansiveExp exp orelse 536 let val {info = {idKind, ...}, ...} = ii 537 in case !idKind of 538 {info = CONik _, qualid = {id, qual}} => id = ["ref"] 539 | {info = EXCONik _, ...} => false 540 | _ => true 541 end 542 | APPexp((_,VIDPATHexp (ref(OVLvidpath(ii,_,_)))),exp) => 543 isExpansiveExp exp orelse 544 let val {info = {idKind, ...}, ...} = ii 545 in case !idKind of 546 {info = CONik _, qualid = {id, qual}} => id = ["ref"] 547 | {info = EXCONik _, ...} => false 548 | _ => true 549 end 550 | INFIXexp (ref (RESinfixexp e)) => 551 isExpansiveExp e 552 | INFIXexp (ref (UNRESinfixexp _)) => fatalError "isExpansiveExp: unresolved infix exp" 553 | STRUCTUREexp (modexp,_,_) => isExpansiveModExp modexp 554 | FUNCTORexp (modexp,_,_) => isExpansiveModExp modexp 555 | _ => true 556and isExpansiveModExp (_, (modexp',_)) = 557 case modexp' of 558 DECmodexp _ => true 559 | LONGmodexp _ => false 560 | LETmodexp _ => true 561 | PARmodexp modexp => isExpansiveModExp modexp 562 | CONmodexp (modexp,_) => isExpansiveModExp modexp 563 | ABSmodexp (modexp,_) => isExpansiveModExp modexp 564 | FUNCTORmodexp _ => false 565 | APPmodexp _ => true 566 | RECmodexp (_,_,_, modexp) => isExpansiveModExp modexp 567; 568 569 570fun expansiveIdsInValBind (ValBind(ref pat, exp)) acc = 571 if (isExpansiveExp exp) then (domPatAcc pat acc) else acc 572; 573 574(* Bug fix 2004-05-24 from Claudio; bug from Andrzej Wasowski *) 575 576fun renameScheme scheme = Types.copyTypeScheme [] [] scheme 577 578fun closeValBindVE loc (pvbs: ValBind list) VE = 579 let val exIds = foldR expansiveIdsInValBind [] pvbs in 580 mapEnv (fn id => fn {qualid, info = (t,sc)} => 581 {qualid=qualid,info = (renameScheme(generalization (member id 582exIds) t),sc)}) VE 583 end 584; 585 586 587(* 588fun closeValBindVE loc (pvbs: ValBind list) VE = 589 let val exIds = foldR expansiveIdsInValBind [] pvbs in 590 mapEnv (fn id => fn {qualid, info = (t,sc)} => 591 {qualid=qualid,info = (generalization (member id exIds) t,sc)}) VE 592 end 593; 594*) 595 596fun findAndMentionStrSig loc i = 597 let val cu = findAndMentionSig loc i 598 in case modeOfSig cu of 599 STRmode => cu 600 | TOPDECmode => (* cvr: TODO in the near future this should be an error, not just a warning *) 601 ((msgIBlock 0; 602 errLocation loc; 603 errPrompt "Warning: this unit was compiled as a sequence of toplevel declarations,";msgEOL(); 604 errPrompt "but is being used as if it had been compiled as a structure.";msgEOL(); 605 msgEBlock()); 606 cu) 607 end 608; 609 610fun findLongModIdForOpen ME loc q = 611 case q of 612 {qual, id = []} => fatalError "findLongModIdForOpen" 613 | {qual, id = [i] } => 614 (let val {qualid,info=RS} = lookupEnv ME i 615 val S = SofRecStr RS 616 in 617 ([],{qualid = qualid, 618 info = (MEofStr S, 619 FEofStr S, 620 NILenv, 621 VEofStr S, 622 TEofStr S)}) 623 end handle Subscript => 624 let val i = normalizedUnitName i (* cvr: REVIEW *) 625 in 626 if i = #uName(!currentSig) then 627 (msgIBlock 0; 628 errLocation loc; 629 errPrompt "the free structure identifier may not refer to the current unit: "; 630 printQualId q; msgEOL(); 631 msgEBlock(); 632 raise Toplevel) 633 else 634 let val cu = findAndMentionStrSig loc i (* cvr: REVIEW maybe findAndMention? *) 635 in 636 ([],{qualid = {qual = i,id = []}, 637 info = (bindTopInEnv NILenv (#uModEnv cu), 638 bindTopInEnv NILenv (#uFunEnv cu), 639 bindTopInEnv NILenv (#uSigEnv cu), 640 bindTopInEnv NILenv (#uVarEnv cu), 641 bindTopInEnv NILenv (#uTyEnv cu)) 642 }) 643 end 644 end) 645 | _ => let val (fields,{qualid,info=RS}) = findLongModId ME loc q 646 val S = SofRecStr RS 647 in 648 (fields,{qualid = qualid, 649 info = (MEofStr S, 650 FEofStr S, 651 NILenv, 652 VEofStr S, 653 TEofStr S)}) 654 end 655and findLongModId ME loc q = 656 case q of 657 {qual, id = []} => fatalError "findLongModId" 658 | {qual, id = [i] } => 659 (let val modglobal = lookupEnv ME i 660 in ([],modglobal) 661 end handle Subscript => 662 let val i = normalizedUnitName i (* cvr: REVIEW *) 663 in 664 if i = #uName(!currentSig) then 665 (msgIBlock 0; 666 errLocation loc; 667 errPrompt "the free structure identifier may not refer to the current unit: "; 668 printQualId q; msgEOL(); 669 msgEBlock(); 670 raise Toplevel) 671 else 672 let val cu = findAndMentionStrSig loc i 673 in 674 ([],{qualid = {qual = i,id = []}, 675 info = 676 NONrec (STRstr(bindTopInEnv NILenv (#uModEnv cu), 677 bindTopInEnv NILenv (#uFunEnv cu), 678 bindTopInEnv NILenv (#uSigEnv cu), 679 bindTopInEnv NILenv (#uTyEnv cu), 680 bindTopInEnv NILenv (#uVarEnv cu))) 681 }) 682 end 683 end) 684 | {qual, id = i::id} => 685 let val (fields,{qualid = {qual = qual',id = id'}, info = RS}) = findLongModId ME loc {qual = qual , id = id} 686 in 687 let val (field,modglobal) = lookupMEofStr (SofRecStr RS) i 688 in if isGlobalName (#qualid modglobal) 689 then ([],modglobal) 690 else (field::fields, 691 {qualid = {qual = qual', id = i::id'}, 692 info = #info modglobal}) 693 end handle Subscript => 694 errorMsg loc ("Unbound structure component: "^(showQualId q)) 695 end 696; 697 698 699fun findLongVId ME VE loc q = 700 case q of 701 {qual, id = []} => fatalError "findLongVId" 702 | {qual, id = [i] } => 703 (([],lookupEnv VE i) 704 handle Subscript => 705 errorMsg loc ("Unbound value identifier: "^(showQualId q))) 706 | {qual, id = i::id} => 707 let val (fields,{qualid = {qual = qual', id = id'},info = RS}) = 708 findLongModId ME loc {qual = qual , id = id} 709 in 710 let val (field,info) = lookupVEofStr (SofRecStr RS) i 711 in if isGlobalName (#qualid info) 712 then ([],info) (* inline globals *) 713 else (field::fields, 714 {qualid = {qual = qual', id = i::id'}, 715 info = #info info}) 716 end handle Subscript => 717 errorMsg loc ("Unbound value component: "^(showQualId q)) 718 end 719; 720 721fun findLongFunId ME FE loc q = 722 case q of 723 {qual, id = []} => fatalError "findLongFunId" 724 | {qual, id = [i] } => 725 (([],lookupEnv FE i) 726 handle Subscript => 727 errorMsg loc ("Unbound functor identifier: "^(showQualId q))) 728 | {qual, id = i::id} => 729 let val (fields,{qualid = {qual = qual', id = id'},info = RS}) = 730 findLongModId ME loc {qual = qual , id = id} 731 in 732 let val (field,info) = lookupFEofStr (SofRecStr RS) i 733 in if isGlobalName (#qualid info) 734 then ([],info) (* inline globals *) 735 else (field::fields, 736 {qualid = {qual = qual', id = i::id'}, 737 info = #info info}) 738 end handle Subscript => 739 errorMsg loc ("Unbound functor component: "^(showQualId q)) 740 end 741; 742 743(* cvr: *) 744fun findLongTyCon ME TE loc q = 745 case q of 746 {qual, id = []} => fatalError "findLongTyCon" 747 | {qual, id = [i] } => 748 ((lookupEnv TE i) 749 handle Subscript => 750 errorMsg loc ("Unbound type constructor: "^(showQualId q))) 751 | {qual, id = i::id} => 752 let val (_,{info = RS,...}) = findLongModId ME loc {qual = qual, id = id} 753 in 754 ((lookupEnv (TEofStr (SofRecStr RS)) i) 755 handle Subscript => 756 errorMsg loc ("Unbound type component: "^(showQualId q))) 757 end 758; 759 760fun findLongModIdInStr S loc q = 761 case q of 762 {qual, id = []} => fatalError "findLongModIdInStr" 763 | {qual, id = [i] } => 764 (let val (field,modglobal) = lookupMEofStr S i 765 in if isGlobalName (#qualid modglobal) 766 then ([],modglobal) 767 else ([field],modglobal) 768 end handle Subscript => 769 errorMsg loc ("Unbound structure component: "^(showQualId q))) 770 | {qual, id = i::id} => 771 let val (fields,{qualid = {qual = qual',id = id'}, info = RS'}) = 772 findLongModIdInStr S loc {qual = qual,id = id} 773 in 774 let val (field,modglobal) = lookupMEofStr (SofRecStr RS') i 775 in if isGlobalName (#qualid modglobal) 776 then ([],modglobal) 777 else (field::fields, 778 {qualid = {qual = qual', id = i::id'}, 779 info = #info modglobal}) 780 end handle Subscript => 781 errorMsg loc ("Unbound structure component: "^(showQualId q)) 782 end 783; 784 785fun findLongTyConInStr S loc q = 786 case q of 787 {qual, id = []} => fatalError "findLongTyConInStr" 788 | {qual, id = [i] } => 789 ((lookupEnv (TEofStr S) i) 790 handle Subscript => 791 errorMsg loc ("Unbound type component: "^(showQualId q))) 792 | {qual, id = i::id} => 793 let val (_,{info = RS',...}) = findLongModIdInStr S loc {qual = qual, id = id} 794 in 795 ((lookupEnv (TEofStr (SofRecStr RS')) i) 796 handle Subscript => 797 errorMsg loc ("Unbound type component: "^(showQualId q))) 798 end 799; 800 801 802fun findSigId GE loc sigid = 803 lookupEnv GE sigid 804 handle Subscript => 805 let val i = normalizedUnitName sigid (* cvr: TODO review *) 806 in 807 if i = #uName(!currentSig) then 808 (msgIBlock 0; 809 errLocation loc; 810 errPrompt "The free signature identifier may not refer to the current unit: "; 811 msgString sigid; msgEOL(); 812 msgEBlock(); 813 raise Toplevel) 814 else 815 let val cu = findAndMentionStrSig loc i 816 (* cvr: TODO review - using the unit's signature 817 probably shouldn't imply using its implementation *) 818 in 819 case !(strOptOfSig cu) of 820 NONE => 821 (msgIBlock 0; 822 errLocation loc; 823 errPrompt "The signature identifier\ 824 \ refers to a unit interface, \ 825 \ but the unit was not defined \ 826 \ with an explicit signature."; 827 msgEOL(); 828 msgEBlock(); 829 raise Toplevel) 830 | SOME RS => 831 {qualid = {qual = i,id = []}, 832 info = (* cvr: remove copySig [] [] *) 833 (LAMBDAsig(!(tyNameSetOfSig cu), 834 STRmod RS))} 835 end 836 end 837; 838 839(* Expectations are used by elabModExp to resolve 840 ambiguous longmodid's either longstrids or longfunids 841*) 842 843datatype Expectation = FUNexpected | STRexpected | MODexpected; 844 845fun expectMod (STRmod S) = STRexpected 846| expectMod (FUNmod F) = FUNexpected 847; 848 849fun resolveExpectation (MODexpected,true) = FUNexpected 850| resolveExpectation (MODexpected,false) = STRexpected 851| resolveExpectation (expectation,_) = expectation 852; 853 854fun reportExpectation expectation ({info = {withOp,...},qualid}:LongModId) = 855 case expectation of 856 MODexpected => 857 let val (expected,intended) = 858 case withOp of 859 false => ("structure.","functor") 860 | true => ("functor.","structure") in 861 msgIBlock 0; 862 errPrompt "(In this context,\ 863 \ it is assumed that "; 864 msgEOL(); 865 errPrompt " "; 866 (if withOp then msgString "op " else ()); 867 msgString (showQualId qualid); 868 msgEOL(); 869 errPrompt " refers to a "; msgString expected; msgEOL(); 870 errPrompt " If you actually meant the "; 871 msgString intended; 872 msgString " of the same name,"; 873 msgEOL(); 874 errPrompt " you must use the syntax: "; 875 msgEOL(); 876 errPrompt " "; 877 (if withOp then () else msgString "op "); 878 msgString (showQualId qualid); 879 msgEOL(); 880 errPrompt " to indicate this.)";msgEOL(); 881 raise Toplevel 882 end 883 | _ => raise Toplevel 884; 885 886fun lookup_VE (ME:ModEnv) (VE : VarEnv) (ii : IdInfo) = 887 let val {qualid, info} = ii 888 val {idLoc, ...} = info 889 in 890 let val (_,{ qualid = csqualid, info = (sch,_)}) = 891 findLongVId ME VE idLoc qualid 892 in 893 specialization(sch) 894 end 895 handle Subscript => 896 fatalError "lookup_VE" 897 end; 898 899 900fun lookup_UE (UE : UEnv) loc (ii : IdInfo) = 901 let val id = hd(#id(#qualid ii)) in 902 lookup id UE 903 handle Subscript => errorMsg loc ("Unbound type variable: " ^ id) 904 end; 905 906fun lookup_VEForPat ME VE (ii : IdInfo) = 907 let val { qualid, info } = ii 908 val { idLoc = loc, ... } = info 909 in 910 case qualid of 911 {qual, id = []} => fatalError "lookup_VEForPat" 912 | {qual, id = [i] } => 913 (let val {qualid = csqualid, info = (_,cs)} = lookupEnv VE i 914 in ([],{qualid = csqualid, info = cs}) 915 end 916 (* Otherwise ii is being defined in the pattern... *) 917 handle Subscript => 918 ([],{ qualid = qualid, info=VARname REGULARo })) 919 | {qual, id = id as (_::_)} => 920 let val (fields,{qualid = csqualid, info = (_,cs)}) = 921 (findLongVId ME VE loc qualid) 922 in (fields,{qualid = csqualid, info = cs}) 923 end 924 end 925; 926 927(* syntactic checks *) 928 929fun appOpt f u (SOME x) = f x 930 | appOpt f u NONE = u 931; 932 933fun illegalVal id = 934 id = "true" orelse id = "false" 935 orelse id = "nil" orelse id = "::" orelse id = "ref" 936 937fun illegalCon id = illegalVal id orelse id = "it" 938 939fun checkRebinding illegal ({qualid={id=lid, ...}, info = {idLoc, ...}} : IdInfo) = 940 if illegal (longIdentAsIdent lid "checkRebinding") then 941 errorMsg idLoc "Illegal rebinding or respecification" 942 else 943 (); 944 945fun checkAsPatSource (loc, pat') = 946 case pat' of 947 VARpat _ => () 948 | TYPEDpat((_, VARpat _), _) => () 949 | INFIXpat (ref (UNRESinfixpat _)) => fatalError "checkAsPatSource" 950 | INFIXpat (ref (RESinfixpat p)) => 951 checkAsPatSource p 952 | _ => errorMsg loc "Ill-formed source of a layered pattern" 953; 954 955fun checkRecTy (loc, fs) = 956 if duplicates (map fst fs) then 957 errorMsg loc "The same label is bound twice in a record type" 958 else () 959; 960 961 962fun checkRecPat (loc, fs) = 963 if duplicates (map fst fs) then 964 errorMsg loc "The same label is bound twice in a record pattern" 965 else () 966; 967 968fun isFnExp (_, exp') = 969 case exp' of 970 PARexp exp => isFnExp exp 971 | TYPEDexp(exp, ty) => isFnExp exp 972 | FNexp _ => true 973 | _ => false 974; 975 976fun checkFnExp exp = 977 if isFnExp exp then () else 978 errorMsg (xLR exp) "Non-functional rhs expression in val rec declaration" 979; 980 981fun inIds (ii : IdInfo) (iis : IdInfo list) = 982 exists (fn ii' => #id(#qualid ii) = #id(#qualid ii')) iis; 983 984 985 986fun checkDuplIds (iis : IdInfo list) msg = 987 case iis of 988 [] => () 989 | ii :: iis' => 990 if inIds ii iis' then 991 errorMsg (#idLoc (#info ii)) msg 992 else checkDuplIds iis' msg 993; 994 995fun checkAllIdsIn loc [] iis desc = () 996| checkAllIdsIn loc (v::vs) iis desc = 997 (if exists (fn (ii':IdInfo) => [v] = #id(#qualid ii')) iis 998 then () 999 else (case (!currentCompliance) of 1000 Orthodox => 1001 (msgIBlock 0; 1002 errLocation loc; 1003 errPrompt "Compliance Error: ";msgEOL(); 1004 errPrompt "The phrase, although accepted as a Moscow ML extension,";msgEOL(); 1005 errPrompt "is not supported by the Definition of Standard ML:"; msgEOL(); 1006 errPrompt "the type variable";msgEOL(); 1007 errPrompt " "; msgString v;msgEOL(); 1008 errPrompt "should be a parameter of the "; 1009 msgString desc;msgEOL(); 1010 msgEBlock(); 1011 raise Toplevel) 1012 | Conservative => 1013 (msgIBlock 0; 1014 errLocation loc; 1015 errPrompt "Compliance Warning: ";msgEOL(); 1016 errPrompt "The phrase, although accepted as a Moscow ML extension,";msgEOL(); 1017 errPrompt "is not supported by the Definition of Standard ML:"; msgEOL(); 1018 errPrompt "the type variable";msgEOL(); 1019 errPrompt " "; msgString v;msgEOL(); 1020 errPrompt "should be a parameter of the "; 1021 msgString desc;msgEOL(); 1022 msgEBlock(); 1023 checkAllIdsIn loc (drop (fn v' => v = v') vs) iis desc) 1024 | _ => ())) 1025; 1026 1027fun checkTypBind (tyvars, tycon, ty as (loc,_)) = 1028( checkDuplIds tyvars 1029 "Duplicate parameter in a type binding"; 1030 if (!currentCompliance) <> Liberal 1031 then checkAllIdsIn loc (unguardedTy ty) tyvars "type binding" 1032 else () 1033); 1034 1035fun checkDatBind (tyvars, tycon, cbs) = 1036( 1037 app (fn ConBind(ii, SOME (ty as (loc,_))) => 1038 (if (!currentCompliance)<> Liberal 1039 then checkAllIdsIn loc (unguardedTy ty) tyvars "datatype binding" 1040 else ()) 1041 | ConBind(ii, NONE) => ()) 1042 cbs; 1043 checkDuplIds tyvars 1044 "Duplicate parameter in a datatype binding" 1045); 1046 1047fun checkTypDesc (tyvars, tycon) = 1048 checkDuplIds tyvars 1049 "Duplicate parameter in a prim_type binding" 1050; 1051 1052 1053(* checkApplicativeModExp dec is used to ensures that module values are 1054 not opened at top-level within (both generative and applicative) functor bodies 1055 (doing so is unsound in the presence of applicative functors). 1056*) 1057fun checkApplicativeModExp (_,(modexp,_)) = 1058 case modexp of 1059 DECmodexp dec => 1060 checkApplicativeDec dec 1061 | LONGmodexp _ => () 1062 | LETmodexp (dec,modexp) => 1063 (checkApplicativeDec dec; 1064 checkApplicativeModExp modexp) 1065 | PARmodexp modexp => 1066 checkApplicativeModExp modexp 1067 | CONmodexp (modexp,sigexp) => 1068 checkApplicativeModExp modexp 1069 | ABSmodexp (modexp,sigexp) => 1070 checkApplicativeModExp modexp 1071 | FUNCTORmodexp (_,modid,_, sigexp, modexp) => 1072 () 1073 (* checkApplicativeModExp modexp is already ensured by the 1074 elaboration of modexp *) 1075 | APPmodexp (modexp,modexp') => 1076 (checkApplicativeModExp modexp; 1077 checkApplicativeModExp modexp') 1078 | RECmodexp (modid,_,sigexp, modexp) => 1079 checkApplicativeModExp modexp 1080and checkApplicativeDec (loc,dec') = 1081 case dec' of 1082 ABSTYPEdec(_, _, dec2) => 1083 checkApplicativeDec dec2 1084 | LOCALdec (dec1, dec2) => 1085 (checkApplicativeDec dec1;checkApplicativeDec dec2) 1086 | SEQdec (dec1, dec2) => 1087 (checkApplicativeDec dec1;checkApplicativeDec dec2) 1088 | STRUCTUREdec mbs => 1089 app (fn ASmodbind ((loc,_),_,_) => 1090 errorMsg loc "Illegal structure binding: \ 1091 \a structure value cannot be opened in a functor body" 1092 | MODBINDmodbind (_,modexp') => 1093 checkApplicativeModExp modexp') 1094 mbs 1095 | FUNCTORdec fbs => 1096 app (fn ASfunbind ((loc,_),_,_) => 1097 errorMsg loc "Illegal functor binding: \ 1098 \a functor value cannot be opened in a functor body" 1099 | FUNBINDfunbind (_,modexp') => 1100 checkApplicativeModExp modexp') 1101 fbs 1102 | _ => () 1103; 1104 1105fun checkApplicativeMod loc (STRmod recstr) = 1106 checkApplicativeRecStr loc recstr 1107| checkApplicativeMod loc (FUNmod F) = 1108 checkApplicativeFun loc F 1109and checkApplicativeFun loc (forall,dom,(EXISTSexmod(exists,rng))) = 1110 case exists of 1111 [] => checkApplicativeMod loc rng 1112 | _ => errorMsg loc "Illegal applicative functor argument: \ 1113 \the signature specifies a generative functor \ 1114 \in a positive position" 1115and checkApplicativeRecStr loc (RECrec(fwd,bdy)) = 1116 checkApplicativeRecStr loc bdy 1117| checkApplicativeRecStr loc (NONrec str) = 1118 checkApplicativeStr loc str 1119and checkApplicativeStr loc (STRstr (ME,FE,GE,TE,VE)) = 1120 (traverseEnv (fn modid => fn {info=recstr,...} => 1121 checkApplicativeRecStr loc recstr) 1122 ME; 1123 traverseEnv (fn funid => fn {info=F,...} => 1124 checkApplicativeFun loc F) 1125 FE) 1126| checkApplicativeStr loc (SEQstr(S1,S2)) = 1127 (checkApplicativeStr loc S1; 1128 checkApplicativeStr loc S2) 1129 1130(* semantic checks *) 1131 1132val bindOnceInEnv = fn env => fn (loc,id) => fn info => fn msg => 1133 (lookupEnv env id; 1134 errorMsg loc ("Illegal rebinding of "^id^": "^msg) 1135 ) 1136 handle Subscript => bindInEnv env id info 1137; 1138 1139local 1140(* cvr: TODO share code *) 1141fun checkNoRebindingsTyEnv loc ids VE msg = 1142 foldEnv (fn id => fn _ => fn ids => 1143 if member id ids 1144 then (errorMsg loc 1145 ("Illegal rebinding of type constructor "^id^": "^msg)) 1146 else id::ids) ids VE 1147and checkNoRebindingsModEnv loc modids ME msg = 1148 foldEnv (fn id => fn _ => fn ids => 1149 if member id ids 1150 then errorMsg loc ("Illegal rebinding of structure identifier "^id^": "^msg) 1151 else id::ids) modids ME 1152and checkNoRebindingsVarEnv loc vids VE msg = 1153 foldEnv (fn id => fn _ => fn ids => 1154 if member id ids 1155 then errorMsg loc ("Illegal rebinding of value identifier "^id^": "^msg) 1156 else id::ids) vids VE 1157and checkNoRebindingsFunEnv loc funids FE msg = 1158 foldEnv (fn id => fn _ => fn ids => 1159 if member id ids 1160 then errorMsg loc ("Illegal rebinding of functor identifier "^id^": "^msg) 1161 else id::ids) funids FE 1162and checkNoRebindingsSigEnv loc sigids GE msg = 1163 foldEnv (fn id => fn _ => fn ids => 1164 if member id ids 1165 then errorMsg loc ("Illegal rebinding of signature identifier "^id^": "^msg) 1166 else id::ids) sigids GE 1167and checkNoRebindingsStr loc (modids,funids,sigids,tycons,vids) S msg = 1168 case S of 1169 STRstr (ME,FE,GE,TE,VE) => 1170 (checkNoRebindingsModEnv loc modids ME msg, 1171 checkNoRebindingsFunEnv loc funids FE msg, 1172 checkNoRebindingsSigEnv loc sigids GE msg, 1173 checkNoRebindingsTyEnv loc tycons TE msg, 1174 checkNoRebindingsVarEnv loc vids VE msg) 1175 | SEQstr (S,S') => 1176 checkNoRebindingsStr loc (checkNoRebindingsStr loc (modids,funids,sigids,tycons,vids) S msg) S' msg 1177in 1178 val checkNoRebindingsStr = fn loc => fn S => fn msg => (checkNoRebindingsStr loc ([],[],[],[],[]) S msg;()) 1179 val checkNoRebindingsTyEnv = fn loc => fn TE => fn msg => (checkNoRebindingsTyEnv loc [] TE msg;()) 1180 val checkNoRebindingsVarEnv = fn loc => fn VE => fn msg => (checkNoRebindingsVarEnv loc [] VE msg;()) 1181end 1182; 1183 1184fun errorVarAsCon (ii : IdInfo) = 1185 errorMsg (#idLoc (#info ii)) "A constructor name expected" 1186; 1187 1188fun errorPrimAsCon (ii : IdInfo) = 1189 errorMsg (#idLoc (#info ii)) "A constructor name expected" 1190; 1191 1192fun resolvePatCon ME VE (pat as (loc, pat')) = 1193 case pat' of 1194 SCONpat _ => pat 1195 | VARpat ii => 1196 let val (fields,cs) = lookup_VEForPat ME VE ii 1197 val {qualid, info} = ii 1198 in 1199 case #info cs of 1200 VARname _ => 1201 (if #qual qualid <> "" orelse 1202 case #id qualid of [_] => false | _ => true 1203 then 1204 errorMsg (#idLoc info) 1205 "Variable names in patterns cannot be qualified" 1206 else (); 1207 pat) 1208 | PRIMname _ => 1209 (if #qual qualid <> "" orelse 1210 case #id qualid of [_] => false | _ => true 1211 then 1212 errorMsg (#idLoc info) 1213 "Variable names in patterns cannot be qualified" 1214 else (); 1215 pat) 1216 | CONname ci => 1217 (if #conArity(!ci) <> 0 then 1218 errorMsg (#idLoc info) 1219 "Unary constructor in the pattern needs an argument" 1220 else (); 1221 #idKind info := { qualid= #qualid cs, info=CONik ci }; 1222 (loc, NILpat ii)) 1223 | EXNname ei => 1224 (if #exconArity(!ei) <> 0 then 1225 errorMsg (#idLoc info) 1226 "Unary exception constructor in the pattern needs an argument" 1227 else (); 1228 #idKind info := { qualid= #qualid cs, info=EXCONik ei }; 1229 #idFields info := fields; 1230 (loc, EXNILpat ii)) 1231 | REFname => 1232 errorMsg (#idLoc info) "`ref` is used as a variable" 1233 end 1234 | WILDCARDpat => pat 1235 | NILpat ii => fatalError "resolvePatCon" 1236 | CONSpat(ii, p) => 1237 let val (fields,cs) = lookup_VEForPat ME VE ii 1238 val {qualid, info} = ii 1239 in 1240 case #info cs of 1241 VARname _ => errorVarAsCon ii 1242 | PRIMname _ => errorPrimAsCon ii 1243 | CONname ci => 1244 (if #conArity(!ci) = 0 then 1245 errorMsg (#idLoc info) 1246 "Nullary constructor in a pattern cannot be applied" 1247 else (); 1248 #idKind info := { qualid= #qualid cs, info=CONik ci }; 1249 (loc, CONSpat(ii, resolvePatCon ME VE p))) 1250 | EXNname ei => 1251 (#idKind info := { qualid= #qualid cs, info=EXCONik ei }; 1252 #idFields info := fields; 1253 (loc, EXCONSpat(ii, resolvePatCon ME VE p))) 1254 | REFname => (loc, REFpat (resolvePatCon ME VE p)) 1255 end 1256 | EXNILpat _ => fatalError "resolvePatCon" 1257 | EXCONSpat _ => fatalError "resolvePatCon" 1258 | EXNAMEpat _ => fatalError "resolvePatCon" 1259 | REFpat _ => fatalError "resolvePatCon" 1260 | RECpat(ref (RECrp(fs, dots))) => 1261 (loc, RECpat(ref (RECrp(map_fields (resolvePatCon ME VE) fs, dots)))) 1262 | RECpat(ref (TUPLErp _)) => fatalError "resolvePatCon" 1263 | VECpat ps => 1264 (loc, VECpat (map (resolvePatCon ME VE) ps)) 1265 | PARpat p => 1266 (loc, PARpat (resolvePatCon ME VE p)) 1267 | INFIXpat (ref (UNRESinfixpat _)) => fatalError "resolvePatCon" 1268 | INFIXpat (ref (RESinfixpat p)) => 1269 resolvePatCon ME VE p 1270 | TYPEDpat(p,t) => 1271 (loc, TYPEDpat(resolvePatCon ME VE p, t)) 1272 | LAYEREDpat(pat1, pat2) => 1273 (loc, LAYEREDpat(resolvePatCon ME VE pat1, resolvePatCon ME VE pat2)) 1274; 1275 1276 1277fun resolvePatConRec ME VE (pat as (loc, pat')) = 1278 case pat' of 1279 VARpat ii => 1280 let val {qualid, info} = ii 1281 in 1282 if #qual qualid <> "" orelse 1283 case #id qualid of [_] => false | _ => true 1284 then 1285 errorMsg (#idLoc info) 1286 "Variable names in patterns cannot be qualified" 1287 else 1288 (checkRebinding illegalVal ii; 1289 pat) 1290 end 1291 | WILDCARDpat => 1292 pat 1293 | PARpat p => 1294 (loc, PARpat (resolvePatConRec ME VE p)) 1295 | TYPEDpat(p,t) => 1296 (loc, TYPEDpat(resolvePatConRec ME VE p, t)) 1297 | LAYEREDpat(pat1, pat2) => 1298 (loc, LAYEREDpat(resolvePatConRec ME VE pat1, resolvePatConRec ME VE pat2)) 1299 | INFIXpat (ref (RESinfixpat p)) => 1300 resolvePatConRec ME VE p 1301 (* Other errors will be caught later by Synchk.checkRecFnPat *) 1302 | _ => errorMsg loc "Ill-formed left hand side in recursive binding"; 1303 1304 1305local (* to implement the derived form for structure sharing, 1306 adapted from the MLKit 1307 *) 1308 (* cvr: TODO the error messages could be further 1309 improved by highlighting the 1310 location of the longmodid that causes the error *) 1311 fun update(a,b,m) = (let val bs = lookupEnv m a 1312 in 1313 bindInEnv m a (b::bs) 1314 end) 1315 handle Subscript => bindInEnv m a [b]; 1316 1317 (* We first collect a list of tyname lists which must be identified. *) 1318 1319 fun collect_TE (loc,T0 : TyName list, path, TEs, acc) : TyName list list = 1320 let val tcmap = foldL (fn TE => fn acc => 1321 foldEnv (fn tycon => fn tystr => fn acc => 1322 update(tycon,tystr,acc)) 1323 acc 1324 TE) 1325 NILenv 1326 TEs 1327 1328 (* Eliminate entries with less than two component, check 1329 * arities and flexibility of involved tynames. Further, 1330 * extract tynames from type structures. *) 1331 1332 in 1333 foldEnv (fn tycon => fn tystrs => fn acc => 1334 case tystrs of 1335 [] => acc 1336 | [tystr] => acc 1337 | tystrs => 1338 let fun tystr_to_tyname (tyfun,_) = 1339 (choose (equalsTyFunTyName tyfun) T0) 1340 handle Subscript => 1341 errorMsg loc 1342 ("Illegal sharing abbreviation: \ 1343 \the type constructor "^ 1344 (showQualId {qual="",id=tycon::path})^ 1345 " does not denote an opaque type in each equated structure") 1346 val tynames = map tystr_to_tyname tystrs 1347 val kind = case tynames of 1348 tn :: _ => kindTyName tn 1349 | _ => fatalError "collect_TE:2" 1350 (* we know that there are more than zero *) 1351 val _ = app (fn tn => if kindTyName tn = kind 1352 then 1353 () 1354 else errorMsg loc 1355 ("Illegal sharing abbreviation: \ 1356 \the type constructor "^ 1357 (showQualId {qual="",id=tycon::path})^ 1358 " does not have the same arity in \ 1359 \each equated structure")) 1360 tynames 1361 in tynames::acc 1362 end) acc tcmap 1363 end 1364 1365 fun collect_S (loc,T0, path, Ss, acc) : TyName list list = 1366 let val (MEs, TEs) = foldL(fn RS => fn (MEs, TEs) => 1367 let val S = SofRecStr RS 1368 val ME = MEofStr S 1369 val TE = TEofStr S 1370 in (ME::MEs,TE::TEs) 1371 end) ([],[]) Ss 1372 val acc = collect_ME(loc,T0,path, MEs, acc) 1373 in collect_TE(loc,T0, path, TEs, acc) 1374 end 1375 1376 and collect_ME (loc, T0, path, MEs, acc) : TyName list list = 1377 let val smap = foldL (fn ME => 1378 fn acc => 1379 foldEnv (fn modid => 1380 fn {qualid,info=S} => 1381 fn acc => 1382 update(modid,S,acc) 1383 ) 1384 acc 1385 ME) 1386 NILenv 1387 MEs 1388 in 1389 foldEnv (fn strid => fn Ss => fn acc => 1390 case Ss of 1391 [] => acc (* Eliminate entries with *) 1392 | [S] => acc (* less than two components. *) 1393 | Ss => collect_S(loc,T0, strid::path,Ss,acc)) 1394 acc smap 1395 end 1396 1397 1398 (* Collapse tynames set if any candidates identify two such *) 1399 1400 fun emptyIntersection T = fn [] => true 1401 | (tn::T') => not(exists (isEqTN tn) T) 1402 andalso emptyIntersection T T' 1403 fun union T = fn [] => T 1404 | tn::T' => if exists (isEqTN tn) T 1405 then union T T' 1406 else union (tn::T) T' 1407 1408 fun collapse ([], Ts) : TyName list list = Ts 1409 | collapse (T::Ts, Ts') = 1410 let fun split ([], no, yes) = (no, yes) 1411 | split (T'::Ts'', no, yes) = 1412 if emptyIntersection T' T then split(Ts'',T'::no, yes) 1413 else split(Ts'',no, T'::yes) 1414 in case split(Ts,[],[]) 1415 of (no, []) => collapse(no, T::Ts') 1416 | (no, yes) => 1417 let val Tnew = foldL union T yes (*cvr: ?*) 1418 in collapse(Tnew::no, Ts') 1419 end 1420 end 1421 1422 (* build the realisation *) 1423 1424 fun build T0 Ts : TyName list = 1425 case Ts of 1426 [] => [] 1427 | (T::Ts) => let val T = (* cvr: re-order T as T0 *) 1428 foldR (fn tn => fn acc => 1429 (((choose (isEqTN tn) T)::acc) 1430 handle Subscript => acc)) 1431 [] 1432 T0 1433 val (tn,T') = case T of 1434 [] => fatalError "build" 1435 | tn::T' => (tn,T') 1436 val equ = foldR (fn tn => fn equ => 1437 if (#tnEqu (!(#info tn))) <> FALSEequ 1438 then TRUEequ (* cvr: TODO should we worry about REFequ? *) 1439 else equ) 1440 FALSEequ 1441 T 1442 val _ = setTnEqu (#info tn) equ 1443 val () = app (fn {qualid,info} => setTnSort info (REAts (APPtyfun (NAMEtyapp(tn))))) T' 1444 (* cvr: TODO revise - 1445 can't we identify type names 1446 just by identifying their info 1447 fields? *) 1448 val T'' = build T0 Ts 1449 in T' @ T'' 1450 end 1451in 1452 fun share (loc,T0:TyName list, Ss : RecStr list) : TyName list = 1453 let val Ts = collect_S (loc,T0,[],Ss,[]) 1454 val Ts : TyName list list = collapse(Ts,[]) 1455 val T = build T0 Ts 1456 in 1457 drop (fn t => exists (isEqTN t) T) T0 1458 end 1459end; 1460 1461val elabModExpRef = 1462 let fun dummyElabModExp (e:Expectation) (ME:ModEnv) (FE:FunEnv) (GE:SigEnv) (UE:UEnv) (VE:VarEnv) (TE:TyEnv) (modexp:ModExp) : Globals.ExMod = fatalError "dummyElabModExp" 1463 in ref dummyElabModExp 1464 end; 1465 1466fun elabTyConPath ME FE GE UE VE TE (loc,tyconpath') = 1467 case tyconpath' of 1468 LONGtyconpath longtycon => 1469 findLongTyCon ME TE loc (#qualid longtycon) 1470 | WHEREtyconpath (longtycon,(_,modid),modexp) => 1471 let 1472 val EXISTSexmod(T,M) = 1473 (!elabModExpRef) STRexpected ME FE GE UE VE TE modexp 1474 val S = case M of 1475 FUNmod _ => errorMsg loc "Illegal projection: this module expression should be\ 1476 \ a structure but is actually a functor" 1477 | STRmod S => S 1478 val modidinfo = {qualid = mkLocalName modid, info = S} val tyStr = findLongTyCon (bindInEnv ME modid modidinfo) 1479 TE loc (#qualid longtycon) 1480 val (fns,_,_) = freeVarsTyStr [] [] ([],[],[]) tyStr 1481 in 1482 app (fn tn => 1483 if exists (isEqTN tn) T 1484 then errorMsg loc "Illegal projection: this projection\ 1485 \ causes an existential type constructor\ 1486 \ to escape its scope" else ()) fns; 1487 tyStr 1488 end; 1489; 1490 1491fun applyTyConPath ME FE GE UE VE TE ((tyconpath as (loc,_)) : TyConPath) ts = 1492 let val (tyfun,_) = elabTyConPath ME FE GE UE VE TE tyconpath 1493 val arity = List.length ts 1494 in 1495 if kindTyFun tyfun <> (ARITYkind arity) then 1496 errorMsg loc ("Arity mismatch! ") 1497 else (); 1498 case tyfun of 1499 APPtyfun tyapp => 1500 CONt(ts, tyapp) 1501 | TYPEtyfun(pars, body) => 1502 type_subst (zip2 pars ts) body 1503(* cvr: TODO would this improve sharing? *) 1504(* | TYPEtyfun(pars, body) => 1505 let val tyname = 1506 {qualid = {qual="",id = [""]}, 1507 info = ref {tnKind = ARITYkind arity, 1508 tnEqu = TRUEequ, (* cvr: TODO revise *) 1509 tnSort = REAts tyfun, 1510 tnStamp = newTyNameStamp(), 1511 tnLevel = currentBindingLevel(), 1512 tnConEnv = ref NONE}} 1513 in 1514 CONt(ts, NAMEtyapp tyname) 1515 end 1516*) 1517(* cvr: end *) 1518 | LAMtyfun _ => fatalError "applyTyConpath" 1519 end; 1520 1521val elabSigExpRef = 1522 let fun dummyElabSigExp (ME:ModEnv) (FE:FunEnv) (GE:SigEnv) (UE:UEnv) (VE:VarEnv) (TE:TyEnv) (sigexp:SigExp) : Globals.Sig = fatalError "dummyElabSigExp" 1523 in ref dummyElabSigExp 1524 end; 1525 1526 1527fun elabTy (ME:ModEnv) (FE:FunEnv) (GE:SigEnv) (UE : UEnv) (VE:VarEnv) (TE : TyEnv) (loc, ty') = 1528 case ty' of 1529 TYVARty ii => 1530 lookup_UE UE loc ii 1531 | RECty fs => 1532 (checkRecTy (loc,fs); 1533 type_rigid_record (map_fields (elabTy ME FE GE UE VE TE) fs)) 1534 | CONty(ty_list,tyconpath) => 1535 applyTyConPath ME FE GE UE VE TE tyconpath 1536 (map (elabTy ME FE GE UE VE TE) ty_list) 1537 | FNty(ty,ty') => 1538 type_arrow (elabTy ME FE GE UE VE TE ty) 1539 (elabTy ME FE GE UE VE TE ty') 1540 | PACKty(sigexp) => 1541 let val LAMBDAsig (T,M) = (!elabSigExpRef) ME FE GE UE VE TE sigexp 1542 in 1543 PACKt (EXISTSexmod(T,M)) 1544 end 1545 | PARty(ty) => 1546 elabTy ME FE GE UE VE TE ty 1547; 1548 1549fun elabSCon (INTscon i, _ ) = type_int 1550 | elabSCon (CHARscon c, _ ) = type_char 1551 | elabSCon (WORDscon c, tyOptRef) = 1552 let val ty = VARt (newTypeVar false false true) 1553 (* nonequ nonimp overloaded *) 1554 in tyOptRef := SOME ty; ty end 1555 | elabSCon (REALscon r, _ ) = type_real 1556 | elabSCon (STRINGscon s, _ ) = type_string 1557; 1558 1559fun elabPat (ME:ModEnv) (FE:FunEnv) (GE:SigEnv) (UE : UEnv) (VE : VarEnv) (TE : TyEnv) (pat as (loc, pat')) (pat_t : Type) (PE : VarEnv) = 1560 case pat' of 1561 SCONpat scon => 1562 (unifyPat pat (elabSCon scon) pat_t; PE) 1563 | VARpat ii => 1564 (case ii of 1565 {qualid = {id = [id],...}, info={idLoc,...}} => 1566 let val q = mkLocalName id 1567 val vi = { qualid=q, info=REGULARo } 1568 in bindOnceInEnv PE (idLoc,id) 1569 {qualid=q, info= (trivial_scheme pat_t,VARname REGULARo)} 1570 "the same value identifier is bound twice in a pattern" 1571 end 1572 | {qualid = {id = _,...},...} => fatalError "elabPat: VARpat") 1573 (* longvid variables are illegal *) 1574 | WILDCARDpat => PE 1575 | NILpat ii => (unifyPat pat (lookup_VE ME VE ii) pat_t; PE) 1576 | CONSpat(ii, p) => 1577 let val id_t = lookup_VE ME VE ii 1578 val p_t = newUnknown() 1579 val res_t = newUnknown() 1580 in 1581 unifyId ii id_t (type_arrow p_t res_t); 1582 if (looksLikeInfixId ii) andalso (isPairPat p) then 1583 (unify p_t (newUnknownPair()) 1584 handle Unify reason => 1585 typeClashId ii id_t (type_arrow (newUnknownPair()) res_t) reason) 1586 else (); 1587 unifyPat pat res_t pat_t; 1588 elabPat ME FE GE UE VE TE p p_t PE 1589 end 1590 | EXNILpat ii => 1591 let val id_t = lookup_VE ME VE ii 1592 in 1593 unifyId ii id_t type_exn; 1594 unifyPat pat type_exn pat_t; 1595 PE 1596 end 1597 | EXCONSpat(ii, p) => 1598 let val id_t = lookup_VE ME VE ii 1599 val p_t = newUnknown() 1600 in 1601 unifyId ii id_t (type_arrow p_t type_exn); 1602 if looksLikeInfixId ii andalso isPairPat p then 1603 (unify p_t (newUnknownPair()) 1604 handle Unify reason => 1605 typeClashId ii id_t (type_arrow (newUnknownPair()) type_exn) reason) 1606 else (); 1607 unifyPat pat type_exn pat_t; 1608 elabPat ME FE GE UE VE TE p p_t PE 1609 end 1610 | EXNAMEpat _ => fatalError "elabPat:1" 1611 | REFpat p => 1612 let val p_t = newUnknown() in 1613 unifyPat pat (type_ref p_t) pat_t; 1614 elabPat ME FE GE UE VE TE p p_t PE 1615 end 1616 | RECpat(ref (RECrp(fs, dots))) => 1617 let val _ = checkRecPat (loc,fs) 1618 val ls = map fst fs 1619 val ps = map snd fs 1620 val ts = map (fn _ => newUnknown()) ps 1621 val fs_t = zip2 ls ts 1622 fun reportClash isRigid reason = 1623 let val ts' = map (fn _ => newUnknown()) ps 1624 val fs_t' = zip2 ls ts' 1625 in 1626 if isRigid then 1627 typeClashPat pat (type_rigid_record fs_t') pat_t reason 1628 else 1629 typeClashPat pat 1630 (type_flexible_record fs_t' (fresh3DotType())) pat_t reason 1631 end 1632 in 1633 (case dots of 1634 NONE => (unify (type_rigid_record fs_t) pat_t 1635 handle Unify reason => reportClash true reason) 1636 | SOME rho => (unify (type_flexible_record fs_t rho) pat_t 1637 handle Unify reason => reportClash false reason)); 1638 foldL_zip (elabPat ME FE GE UE VE TE ) PE ps ts 1639 end 1640 | RECpat(ref (TUPLErp _)) => fatalError "elabPat:2" 1641 | VECpat ps => 1642 let val p_t = newUnknown() in 1643 unifyPat pat (type_vector p_t) pat_t; 1644 foldL (fn p => fn PE => elabPat ME FE GE UE VE TE p p_t PE) PE ps 1645 end 1646 | PARpat p => 1647 elabPat ME FE GE UE VE TE p pat_t PE 1648 | INFIXpat _ => fatalError "elabPat:3" 1649 | TYPEDpat(p,ty) => 1650 let val ty_t = elabTy ME FE GE UE VE TE ty 1651 val PE' = elabPat ME FE GE UE VE TE p pat_t PE 1652 in 1653 unifyPat p pat_t ty_t; 1654 PE' 1655 end 1656 | LAYEREDpat(p1,p2) => 1657 (checkAsPatSource p1; 1658 elabPat ME FE GE UE VE TE p2 pat_t 1659 (elabPat ME FE GE UE VE TE p1 pat_t PE)) 1660; 1661 1662 1663fun freshTyName tycon kind = 1664 ({qualid = mkLocalName tycon, 1665 info = ref {tnKind = kind, 1666 tnStamp = newTyNameStamp(), 1667 tnEqu = TRUEequ, 1668 tnSort = PARAMETERts, 1669 tnLevel = currentBindingLevel(), 1670 tnConEnv = ref NONE 1671 } 1672 } 1673 : TyName) 1674; 1675 1676fun makeTyName tyvar_list tycon = 1677 let val arity = List.length tyvar_list 1678 in freshTyName tycon (ARITYkind arity) end 1679; 1680 1681fun initialDatBindTE (dbs : DatBind list)= 1682 foldL 1683 (fn (datbind as (tyvar_list, loctycon as (loc,tycon), _)) => fn (LAMBDA(T,env)) => 1684 let val _ = checkDatBind datbind 1685 val tyname = makeTyName tyvar_list tycon 1686 in 1687 LAMBDA(tyname::T, 1688 bindOnceInEnv env loctycon 1689 (APPtyfun (NAMEtyapp tyname),ConEnv []) 1690 "the same type constructor is bound twice\ 1691 \ in a datatype declaration or specification") 1692 end) 1693 (LAMBDA([],NILenv)) dbs 1694; 1695 1696fun absTE (TE : TyEnv) = 1697 mapEnv 1698 (fn id => 1699 (fn (APPtyfun (NAMEtyapp tyname),ConEnv CE) => 1700 let val {info, ...} = tyname in 1701 case !(#tnConEnv(!info)) of 1702 SOME (ConEnv CE) => 1703 (setTnEqu info FALSEequ; 1704 #tnConEnv(!info):= NONE; 1705 (APPtyfun (NAMEtyapp tyname),ConEnv [])) 1706 | _ => fatalError "absTE:1" 1707 end 1708 | _ => fatalError "absTE:2")) 1709 TE 1710; 1711 1712fun elabTypBind (ME:ModEnv) (FE:FunEnv) (GE:SigEnv) (UE:UEnv) (VE:VarEnv) 1713 (TE : TyEnv) (tb as (tyvars, loctycon, ty) : TypBind) = 1714 let val _ = checkTypBind tb 1715 val (_,id) = loctycon 1716 val pars = map (fn tyvar => hd(#id(#qualid tyvar))) tyvars 1717 val _ = incrBindingLevel(); 1718 val vs = map (fn tv => newExplicitTypeVar tv) pars 1719 val us = map TypeOfTypeVar vs 1720 val UE' = (zip2 pars us) @ UE 1721 val ty = elabTy ME FE GE UE' VE TE ty 1722 val _ = decrBindingLevel(); 1723 val tyname = makeTyName tyvars id 1724 val tyfun = APPtyfun (NAMEtyapp(tyname)) 1725 in 1726 setTnSort (#info tyname) (REAts (TYPEtyfun(vs, ty))); 1727 (loctycon, (tyfun,ConEnv [])) 1728 end 1729; 1730 1731fun elabTypBindList (ME:ModEnv) (FE:FunEnv) (GE:SigEnv) (UE:UEnv) (VE:VarEnv) 1732 (TE : TyEnv) (tbs : TypBind list) = 1733 foldL_map (fn (locid, tyname) => fn env => 1734 bindOnceInEnv env locid tyname 1735 "the same type constructor is bound twice in a type declaration") 1736 (elabTypBind ME FE GE UE VE TE) NILenv tbs 1737; 1738 1739fun elabTypBindList_opt (ME:ModEnv) (FE:FunEnv) (GE:SigEnv) (UE:UEnv) (VE:VarEnv) (TE : TyEnv) = fn 1740 SOME tbs => elabTypBindList ME FE GE UE VE TE tbs 1741 | NONE => NILenv 1742; 1743 1744fun elabPrimTypBind equ (typdesc as (tyvars, loctycon) : TypDesc) = 1745 let val _ = checkTypDesc typdesc 1746 val (_,id) = loctycon 1747 val tyname = makeTyName tyvars id 1748 val tyfun = APPtyfun (NAMEtyapp(tyname)) 1749 in 1750 setTnEqu (#info tyname) equ; 1751 LAMBDA([tyname],(loctycon, (tyfun, ConEnv []))) 1752 end; 1753 1754fun elabPrimTypBindList equ (tbs : TypDesc list) = 1755 foldL_map (fn LAMBDA(T',(locid, tystr)) => fn (LAMBDA(T,env)) => 1756 LAMBDA(T@T',bindOnceInEnv env locid tystr 1757 "The same tycon is bound twice\ 1758 \ in a prim_type declaration")) 1759 (elabPrimTypBind equ) (LAMBDA([],NILenv)) tbs 1760; 1761 1762fun closeEE EE = 1763 mapEnv (fn excon => fn {qualid, info =(t,csd)} => 1764 {qualid = qualid, info = (generalization true t,csd)}) EE 1765; 1766 1767fun openVE VE = 1768 mapEnv (fn id => fn {qualid, info = (sch,csd)} => 1769 {qualid=qualid, info = (TypeOfScheme sch,csd)}) VE 1770; 1771 1772fun isRecTy (loc, ty') = 1773 case ty' of 1774 RECty [] => false 1775 | RECty _ => true 1776 | _ => false 1777; 1778 1779fun arityOfRecTy (loc, ty') = 1780 case ty' of 1781 RECty fs => List.length fs 1782 | _ => fatalError "arityOfRecTy" 1783; 1784 1785 1786fun elabConBind (ME:ModEnv) (FE:FunEnv) (GE:SigEnv) (UE : UEnv) (VE : VarEnv) (TE : TyEnv) tvs res_t = fn 1787 ConBind(ii, SOME ty) => 1788 let val _ = checkRebinding illegalCon ii; 1789 val {qualid, info} = ii 1790 val ci = getConInfo ii 1791 val _ = setConArity ci 1 1792 val arg_t = (elabTy ME FE GE UE VE TE ty) 1793 in 1794 setConType ci 1795 (mkScheme tvs (type_arrow arg_t res_t)); 1796 if #conSpan(!ci) <> 1 andalso isRecTy ty then 1797 (setConArity ci (arityOfRecTy ty); 1798 setConIsGreedy ci true) 1799 else (); 1800 { qualid= #qualid(!(#idKind(#info ii))), info=ci } 1801 end 1802 | ConBind(ii, NONE) => 1803 let val _ = checkRebinding illegalCon ii; 1804 val {qualid, info} = ii 1805 val ci = getConInfo ii 1806 val _ = setConArity ci 0 1807 in 1808 setConType ci 1809 (mkScheme tvs res_t); 1810 { qualid= #qualid(!(#idKind(#info ii))), info=ci } 1811 end 1812; 1813 1814 1815fun setEquality (TE :TyEnv) = 1816 traverseEnv 1817 (fn _ => fn (tyfun,_) => 1818 case tyfun of 1819 APPtyfun (NAMEtyapp tyname) => 1820 let val {info, ...} = tyname in 1821 case #tnSort (!info) of 1822 REAts tyfun => 1823 setTnEqu info (EqualityOfTyFun tyfun) 1824 | VARIABLEts => fatalError "setEquality" 1825 | PARAMETERts => fatalError "setEquality" 1826 end 1827 | _ => fatalError "setEquality") 1828 TE 1829; 1830 1831val equAttrReset = ref false; 1832 1833fun maximizeEquality (TE : TyEnv) = 1834( 1835 equAttrReset := true; 1836 while !equAttrReset do 1837 (equAttrReset := false; 1838 traverseEnv 1839 (fn _ => fn tystr => 1840 (case tystr of 1841 (APPtyfun (NAMEtyapp tyname),ConEnv CE) => 1842 let val {info, ...} = tyname in 1843 case #tnEqu(!info) of 1844 FALSEequ => () 1845 | TRUEequ => 1846 if exists (fn ci => schemeViolatesEquality 1847 (#conType (!(#info ci)))) 1848 CE 1849 then 1850 (setTnEqu info FALSEequ; equAttrReset := true) 1851 else () 1852 | _ => fatalError "maximizeEquality:1" 1853 end 1854 | _ => fatalError "maximizeEquality:2") 1855 ) 1856 TE) 1857); 1858 1859 1860fun setTags (cbs : ConBind list) = 1861 let prim_val string_of_int : int -> string = 1 "sml_string_of_int"; 1862 val span = List.length cbs 1863 fun loop n = fn 1864 [] => () 1865 | (ConBind(ii, _)) :: rest => 1866 let val {qualid = {id = lid,...},info} = ii 1867 val id = longIdentAsIdent lid "setTags:1" 1868 val {idLoc,...} = info 1869 val _ = app (fn (ConBind ({qualid = {id = lid',...},info = {idLoc=idLoc',...}},_)) => 1870 if id = (longIdentAsIdent lid' "setTags:2") then 1871 errorMsg idLoc' "Illegal constructor specification: \ 1872 \the constructor cannot be specified twice \ 1873 \for the same datatype" 1874 else ()) 1875 rest (* cvr: should this check go elsewhere ? *) 1876 val () = 1877 if n > maxBlockTag then 1878 errorMsg idLoc ("Implementation restriction:\n \ 1879 \A datatype cannot declare more than "^ 1880 string_of_int (maxBlockTag + 1) ^ 1881 " constructors.") 1882 else (); 1883 val ci = mkConInfo() 1884 val q = mkGlobalName id 1885 val _ = #idKind info := { qualid=q, info=CONik ci } 1886 in 1887 setConTag ci n; 1888 setConSpan ci span; 1889 loop (n+1) rest 1890 end 1891 in loop 0 cbs end 1892; 1893 1894 1895fun cons x xs = x :: xs; 1896 1897fun elabDatBind (ME:ModEnv) (FE:FunEnv) (GE:SigEnv) (UE:UEnv) (VE:VarEnv) (TE:TyEnv) 1898 (datbind as (tyvars, loctycon as (loc,tycon), conbind_list) : DatBind) = 1899 let val pars = map (fn ii => hd(#id(#qualid ii))) tyvars 1900 val conbind_list = 1901 Sort.sort (fn ConBind(ii,_) => fn ConBind(ii',_) => 1902 hd(#id(#qualid ii))<=hd(#id(#qualid ii'))) conbind_list 1903 val () = setTags conbind_list 1904 val () = incrBindingLevel() 1905 val vs = map (fn tv => newExplicitTypeVar tv) pars 1906 val us = map TypeOfTypeVar vs 1907 val UE' = (zip2 pars us) @ UE 1908 val (tyfun,_) = lookupEnv TE tycon 1909 val tyname = case tyfun of 1910 APPtyfun(NAMEtyapp tyname) => tyname 1911 | _ => fatalError "elabDatBind" 1912 val t = type_con us tyname 1913 val CE = ConEnv (foldR_map cons (elabConBind ME FE GE UE' VE TE vs t) [] conbind_list) 1914 in 1915 decrBindingLevel(); 1916 setTnConEnv (#info tyname) (ref (SOME CE)); 1917 (VEofCE CE,(loctycon,(tyfun,CE))) 1918 end 1919; 1920 1921fun elabDatBindList (ME:ModEnv) (FE:FunEnv) (GE:SigEnv) (UE:UEnv) (VE:VarEnv) (TE : TyEnv) (dbs : DatBind list) = 1922 foldL_map (fn (VE',(loctycon,tystr)) => fn (VE,TE) => 1923 (plusEnv VE VE', 1924 bindOnceInEnv TE loctycon tystr 1925 "The same type constructor is declared twice in a\ 1926 \ datatype declaration")) 1927 (elabDatBind ME FE GE UE VE TE) (NILenv,NILenv) dbs 1928; 1929 1930fun elabExBind (ME:ModEnv) (FE:FunEnv) (GE:SigEnv) (UE : UEnv) (VE : VarEnv) (TE : TyEnv) = fn 1931 EXDECexbind(ii, SOME ty) => 1932 let val _ = checkRebinding illegalCon ii 1933 val {qualid, info = {idLoc,idKind,...}} = ii 1934 val id = longIdentAsIdent (#id qualid) "elabExBind" 1935 val ei = mkExConInfo() 1936 val q = mkLocalName id 1937 val _ = idKind := { qualid=q, info=EXCONik ei }; 1938 val _ = setExConArity ei 1 1939 val arg_t = (elabTy ME FE GE UE VE TE ty) 1940 in 1941 if typeIsImperative arg_t then () 1942 else errorMsg (xLR ty) "Non-imperative exception type"; 1943 ((idLoc,id), {qualid = q,info = (type_arrow arg_t type_exn, EXNname ei)}) 1944 end 1945 | EXDECexbind(ii, NONE) => 1946 let val _ = checkRebinding illegalCon ii 1947 val {qualid, info = {idLoc,idKind,...}} = ii 1948 val id = longIdentAsIdent (#id qualid) "elabDec:EXDECexbind" 1949 val ei = mkExConInfo() 1950 val q = mkLocalName id 1951 val _ = idKind := { qualid=q, info=EXCONik ei }; 1952 val _ = setExConArity ei 0 1953 in 1954 ((idLoc,id), {qualid = q, info = (type_exn, EXNname ei)}) 1955 end 1956 | EXEQUALexbind(ii, ii') => 1957 let val _ = checkRebinding illegalCon ii 1958 val {qualid, info={idLoc,idKind,...}} = ii 1959 val id = longIdentAsIdent (#id qualid) "elabDec:EXEQUALexbind" 1960 val {qualid=qualid', info=info'} = ii' 1961 val {idLoc=loc', ...} = info' 1962 val (fields,{qualid = csqualid, info = (sigma,cs)}) = findLongVId ME VE loc' qualid' 1963 in 1964 case cs of 1965 VARname _ => errorMsg loc' 1966 ("Variable "^showQualId qualid' ^" is used as an exception name") 1967 | PRIMname _ => errorMsg loc' 1968 ("Primitive "^showQualId qualid' ^" is used as an exception name") 1969 | CONname _ => errorMsg loc' 1970 ("Constructor "^showQualId qualid' ^" is used as an exception name") 1971 | REFname => errorMsg loc' 1972 "`ref' is used as an exception name" 1973 | EXNname ei' => (* cvr: TODO review *) 1974 let val q = mkLocalName id in 1975 #idKind info' := { qualid= csqualid, info=EXCONik ei' }; 1976 #idFields info' := fields; 1977 idKind := { qualid= q, info=EXCONik ei' }; 1978 ((idLoc,id), {qualid = q, info = (specialization(sigma), EXNname ei')}) 1979 end 1980 1981 end 1982; 1983 1984fun elabExBindList (ME:ModEnv) (FE:FunEnv) (GE:SigEnv) (UE : UEnv) (VE : VarEnv) (TE : TyEnv) ebs = 1985 closeEE (foldL_map (fn (locid, tau) => fn env => 1986 bindOnceInEnv env locid tau 1987 "The same exception constructor is declared\ 1988 \ twice in an exception declaration" ) 1989 (elabExBind ME FE GE UE VE TE ) NILenv ebs) 1990; 1991 1992(* OVL1TXXo is not a true overloaded type, *) 1993(* because it needn't be resolved to `int', `real', or `string'. *) 1994(* This is only a hack to catch the type inferred by the *) 1995(* type-checker... Thus the attribute `overloaded' mustn't be *) 1996(* turned on in the type variable. *) 1997(* The same is true of OVL1TPUo (installPP) and OVL2EEBo (=, <>). *) 1998 1999fun elabOvlExp t ovltype = 2000 case ovltype of 2001 REGULARo => 2002 fatalError "elabOvlExp" 2003 | OVL1NNo => 2004 (setCurrentBindingLevel true t; 2005 type_arrow t t) 2006 | OVL1NSo => 2007 (setCurrentBindingLevel true t; 2008 type_arrow t type_string) 2009 | OVL2NNBo => 2010 (setCurrentBindingLevel true t; 2011 type_arrow (type_pair t t) type_bool) 2012 | OVL2NNNo => 2013 (setCurrentBindingLevel true t; 2014 type_arrow (type_pair t t) t) 2015 | OVL1TXXo => 2016 (setCurrentBindingLevel false t; 2017 type_arrow t t) 2018 | OVL1TPUo => 2019 (setCurrentBindingLevel false t; 2020 type_arrow 2021 (type_arrow type_ppstream (type_arrow t type_unit)) 2022 type_unit) 2023 | OVL2EEBo => 2024 (setCurrentBindingLevel false t; 2025 makeEquality t; 2026 type_arrow (type_pair t t) type_bool) 2027; 2028 2029fun elabExp (ME:ModEnv) (FE:FunEnv) (GE:SigEnv) (UE : UEnv) (VE : VarEnv) (TE : TyEnv) 2030 (exp as (loc, exp')) exp_t = 2031 case exp' of 2032 SCONexp scon => 2033 unifyExp exp (elabSCon scon) exp_t 2034(* cvr: TODO 2035 | VARexp(ref (RESve ii)) => 2036 unifyExp exp (lookup_VE VE ii) exp_t 2037 | VARexp(ref (OVLve(_, ovltype, tau))) => 2038 unifyExp exp (elabOvlExp tau ovltype) exp_t 2039*) 2040 | VIDPATHexp (r as (ref (RESvidpath ii))) => 2041 let 2042 val {qualid, info} = ii 2043 val {idKind, idFields,... } = info 2044 val (fields,{qualid = csqualid, info = (scheme,cs)}) = 2045 findLongVId ME VE loc qualid 2046 val tau = specialization(scheme) 2047 in 2048 case cs of 2049 VARname REGULARo => 2050 (idKind := { qualid=csqualid, info=VARik }; 2051 idFields := fields; 2052 unifyExp exp tau exp_t) 2053 | VARname ovltype => 2054 let val tau = newUnknown() in 2055 r := OVLvidpath (ii, ovltype, tau); 2056 unifyExp exp (elabOvlExp tau ovltype) exp_t 2057 end 2058 | PRIMname pi => 2059 (idKind := { qualid=csqualid, info=PRIMik pi }; 2060 idFields := fields; 2061 unifyExp exp tau exp_t) 2062 | CONname ci => 2063 (idKind := { qualid=csqualid, info=CONik ci }; 2064 idFields := fields; 2065 unifyExp exp tau exp_t) 2066 | EXNname ei => 2067 (idKind := { qualid=csqualid, info=EXCONik ei }; 2068 idFields := fields; 2069 unifyExp exp tau exp_t) 2070 | REFname => 2071 (idKind := { qualid=csqualid, info=PRIMik piRef }; 2072 idFields := fields; 2073 unifyExp exp tau exp_t) 2074 end 2075 | VIDPATHexp (ref (OVLvidpath _)) => 2076 fatalError "elabExp" 2077 | FNexp mrules => 2078 elabMatch ME FE GE UE VE TE mrules exp_t 2079 | APPexp(func, arg) => 2080 let val func_t = newUnknown() 2081 val () = elabExp ME FE GE UE VE TE func func_t 2082 val arg_t = newUnknown() 2083 val res_t = newUnknown() 2084 in 2085 unifyExp func func_t (type_arrow arg_t res_t); 2086 if looksLikeInfixExp func andalso isPairExp arg then 2087 (unify arg_t (newUnknownPair()) 2088 handle Unify reason => 2089 typeClashExp func func_t (type_arrow (newUnknownPair()) res_t) 2090 reason) 2091 else (); 2092 unifyExp exp res_t exp_t; 2093 elabExp ME FE GE UE VE TE arg arg_t 2094 end 2095 | LETexp(dec, body) => 2096 let val EXISTS(T,(ME',FE',GE', VE', TE')) = 2097 elabDec ME FE GE UE VE TE dec 2098 val () = incrBindingLevel(); 2099 val () = refreshTyNameSet PARAMETERts T; 2100 val tau = 2101 elabExp (plusEnv ME ME') (plusEnv FE FE') (plusEnv GE GE') UE 2102 (plusEnv VE VE') (plusEnv TE TE') body exp_t 2103 in decrBindingLevel() 2104 end 2105 | RECexp(ref (RECre fs)) => 2106 let val ls = map fst fs 2107 val _ = if duplicates ls then 2108 errorMsg loc "The same label is bound twice in a record expression" 2109 else () 2110 val es = map snd fs 2111 val ts = map (fn _ => newUnknown()) es 2112 val fs_t = zip2 ls ts 2113 in 2114 (unify (type_rigid_record fs_t) exp_t 2115 handle Unify reason => 2116 let val ts' = map (fn _ => newUnknown()) es 2117 val fs_t' = zip2 ls ts' 2118 in typeClashExp exp (type_rigid_record fs_t') exp_t reason end); 2119 app2 (elabExp ME FE GE UE VE TE) es ts 2120 end 2121 | RECexp(ref (TUPLEre _)) => fatalError "elabExp" 2122 | VECexp es => 2123 let val e_t = newUnknown() in 2124 app (fn e => elabExp ME FE GE UE VE TE e e_t) es; 2125 unifyExp exp (type_vector e_t) exp_t 2126 end 2127 | PARexp e => 2128 elabExp ME FE GE UE VE TE e exp_t 2129 | INFIXexp (ref (RESinfixexp e)) => 2130 elabExp ME FE GE UE VE TE e exp_t 2131 | INFIXexp (ref (UNRESinfixexp _)) => fatalError "elabExp: unresolved infix exp" 2132 | TYPEDexp(e,ty) => 2133 let val ty_t = elabTy ME FE GE UE VE TE ty in 2134 elabExp ME FE GE UE VE TE e exp_t; 2135 unifyExp e exp_t ty_t 2136 end 2137 | ANDALSOexp(e1, e2) => 2138 (elabExp ME FE GE UE VE TE e1 type_bool; 2139 elabExp ME FE GE UE VE TE e2 type_bool; 2140 unifyExp exp type_bool exp_t) 2141 | ORELSEexp(e1, e2) => 2142 (elabExp ME FE GE UE VE TE e1 type_bool; 2143 elabExp ME FE GE UE VE TE e2 type_bool; 2144 unifyExp exp type_bool exp_t) 2145 | HANDLEexp(e, mrules) => 2146 (elabExp ME FE GE UE VE TE e exp_t; 2147 elabMatch ME FE GE UE VE TE mrules (type_arrow type_exn exp_t)) 2148 | RAISEexp e => 2149 elabExp ME FE GE UE VE TE e type_exn 2150 | IFexp(e0, e1, e2) => 2151 (elabExp ME FE GE UE VE TE e0 type_bool; 2152 elabExp ME FE GE UE VE TE e1 exp_t; 2153 elabExp ME FE GE UE VE TE e2 exp_t) 2154 | WHILEexp(e1, e2) => 2155 let val e2_t = newUnknown() in 2156 elabExp ME FE GE UE VE TE e1 type_bool; 2157 elabExp ME FE GE UE VE TE e2 e2_t; 2158 unitResultExpected e2 e2_t; 2159 unifyExp exp type_unit exp_t 2160 end 2161 | SEQexp(e1, e2) => 2162 let val e1_t = newUnknown() in 2163 elabExp ME FE GE UE VE TE e1 e1_t; 2164 unitResultExpected e1 e1_t; 2165 elabExp ME FE GE UE VE TE e2 exp_t 2166 end 2167 | STRUCTUREexp(modexp,sigexp,r) => 2168 let val EXISTSexmod(T,M) = elabModExp STRexpected ME FE GE UE VE TE modexp 2169 val _ = case M of STRmod S => () 2170 | _ => errorMsg loc 2171 "The encapsulated module expression should be\ 2172 \ a structure but is actually a functor" 2173 val LAMBDAsig(T',M') = elabSigExp ME FE GE UE VE TE sigexp 2174 val _ = case M' of STRmod _ => () 2175 | _ => errorMsg loc 2176 "The signature expression should specify\ 2177 \ a structure but actually specifies a functor" 2178 in 2179 incrBindingLevel(); 2180 refreshTyNameSet PARAMETERts T; 2181 refreshTyNameSet VARIABLEts T'; 2182 (matchMod M M' 2183 handle MatchError matchReason => 2184 (msgIBlock 0; 2185 errLocation loc; 2186 errPrompt "Signature mismatch: \ 2187 \the structure does not match the signature ..."; 2188 msgEOL(); 2189 msgEBlock(); 2190 errMatchReason "structure" "signature" matchReason; 2191 raise Toplevel)); 2192 refreshTyNameSet PARAMETERts T'; (* forget the realisation *) 2193 decrBindingLevel(); 2194 let val X' = EXISTSexmod(T',normMod M') (* re-introduce the quantifier *) 2195 in 2196 r := SOME X'; 2197 unifyExp exp (PACKt (EXISTSexmod(T',M'))) exp_t 2198 (* ^^^^^^^^^^^^^^^^^^^^^^^^^^^ 2199 this type should *not* be normed 2200 because it will be used to match against 2201 *) 2202 end 2203 end 2204 | FUNCTORexp(modexp,sigexp,r) => 2205 let val EXISTSexmod(T,M) = elabModExp FUNexpected ME FE GE UE VE TE modexp 2206 val _ = case M of FUNmod _ => () 2207 | _ => errorMsg loc 2208 "The encapsulated module expression should be\ 2209 \ a functor but is actually a structure" 2210 val LAMBDAsig(T',M') = elabSigExp ME FE GE UE VE TE sigexp 2211 val _ = case M' of FUNmod _ => () 2212 | _ => errorMsg loc 2213 "The signature expression should specify\ 2214 \ a functor but actually specifies a structure" 2215 in 2216 incrBindingLevel(); 2217 refreshTyNameSet PARAMETERts T; 2218 refreshTyNameSet VARIABLEts T'; 2219 (matchMod M M' 2220 handle MatchError matchReason => 2221 (msgIBlock 0; 2222 errLocation loc; 2223 errPrompt "Signature mismatch: \ 2224 \the functor does not match the signature ..."; 2225 msgEOL(); 2226 msgEBlock(); 2227 errMatchReason "functor" "signature" matchReason; 2228 raise Toplevel)); 2229 refreshTyNameSet PARAMETERts T'; (* forget the realisation *) 2230 decrBindingLevel(); 2231 let val X' = EXISTSexmod(T',normMod M') (* re-introduce the quantifier *) 2232 in 2233 r := SOME X'; 2234 unifyExp exp (PACKt (EXISTSexmod(T',M'))) exp_t 2235 (* ^^^^^^^^^^^^^^^^^^^^^^^^^^^ 2236 this type should *not* be normed 2237 because it will be used to match against 2238 *) 2239 end 2240 end 2241 2242and elabExpSeq (ME:ModEnv) (FE:FunEnv) (GE:SigEnv) (UE:UEnv) (VE:VarEnv) 2243 (TE : TyEnv) es ts = 2244 let fun loop [] [] = () 2245 | loop (e :: es) (t :: ts) = 2246 (elabExp ME FE GE UE VE TE e t; loop es ts) 2247 | loop _ _ = fatalError "elabExpSeq" 2248 in loop es ts end 2249 2250and elabMatch (ME:ModEnv) (FE:FunEnv) (GE:SigEnv) (UE:UEnv) (VE:VarEnv) 2251 (TE : TyEnv) mrules match_t = 2252 let val _ = app (fn MRule(r as ref pats, _) => 2253 r := map (resolvePatCon ME VE) pats) 2254 mrules 2255 val MRule(ref pats1,_) = hd mrules 2256 val arg_ts = map (fn pat => newUnknown()) pats1 2257 val res_t = newUnknown() 2258 in 2259 unifyMatch mrules (foldR type_arrow res_t arg_ts) match_t; 2260 app (fn MRule(ref pats, exp) => elabMRule ME FE GE UE VE TE exp res_t pats arg_ts) 2261 mrules 2262 end 2263 2264and elabMRule (ME:ModEnv) (FE:FunEnv) (GE:SigEnv) (UE:UEnv) (VE:VarEnv) 2265 (TE : TyEnv) exp res_t pats arg_ts = 2266 case (pats, arg_ts) of 2267 ([], []) => elabExp ME FE GE UE VE TE exp res_t 2268 | (pat :: pats', arg_t :: arg_ts') => 2269 let val VE' = elabPat ME FE GE UE VE TE pat arg_t NILenv 2270 in elabMRule ME FE GE UE (plusEnv VE VE') TE exp res_t pats' arg_ts' end 2271 | (_, _) => fatalError "elabMRule" 2272 2273and elabDatatypeReplication (ME:ModEnv) (FE:FunEnv) (GE:SigEnv) 2274 (UE:UEnv) (VE:VarEnv) (TE : TyEnv) 2275 (loc,((_,tycon),tyconpath)) = 2276 let val tyStr as (tyfun,CE) = 2277 elabTyConPath ME FE GE UE VE TE tyconpath 2278 in (VEofCE CE,mk1Env tycon tyStr) 2279 end 2280and elabDec (ME:ModEnv) (FE:FunEnv) (GE:SigEnv) (UE:UEnv) (VE:VarEnv) 2281 (TE : TyEnv) (loc, dec') = 2282 case dec' of 2283 VALdec (tvs, (pvbs, rvbs)) => 2284 let val _ = checkDuplIds tvs "Duplicate explicit type variable" 2285 val pars = map (fn ii => hd(#id(#qualid ii))) tvs 2286 val tyvars = scopedTyVars loc UE pars (unguardedValDec (pvbs, rvbs)) 2287 val () = incrBindingLevel() 2288 val UE' = incrUE tyvars @ UE 2289 val VE' = elabValBind ME FE GE UE' VE TE pvbs 2290 val VE'' = elabRecValBind ME FE GE UE' VE TE rvbs 2291 in 2292 decrBindingLevel(); 2293 EXISTS([],(NILenv,NILenv,NILenv,closeValBindVE loc pvbs (plusEnv VE' VE''), NILenv)) 2294 end 2295 | PRIM_VALdec (tyvarseq,pbs) => 2296 let val _ = checkDuplIds tyvarseq "Duplicate explicit type variable" 2297 val pars = map (fn ii => hd(#id(#qualid ii))) tyvarseq 2298 val tyvars = scopedTyVars loc UE pars (unguardedPrimValBindList pbs) 2299 val () = incrBindingLevel() 2300 val tvs = map (fn tv => newExplicitTypeVar tv) tyvars 2301 val UE' = (zip2 tyvars (map TypeOfTypeVar tvs)) @ UE 2302 val VE' = 2303 foldL_map (fn(locid, info) => fn acc => 2304 bindOnceInEnv acc locid info 2305 "the same primitive is declared twice\ 2306 \ in a prim_val declaration") 2307 (elabPrimValBind ME FE GE UE' VE TE tvs) 2308 NILenv pbs 2309 in decrBindingLevel(); 2310 EXISTS([],(NILenv, NILenv, NILenv, VE',NILenv)) 2311 end 2312 | FUNdec (ref (UNRESfundec _)) => fatalError "elabDec" 2313 | FUNdec (ref (RESfundec dec)) => elabDec ME FE GE UE VE TE dec 2314 | TYPEdec tbs => 2315 let val tbsTE = elabTypBindList ME FE GE UE VE TE tbs 2316 in 2317 setEquality tbsTE; 2318 EXISTS([],(NILenv,NILenv,NILenv,NILenv, tbsTE)) 2319 end 2320 | PRIM_TYPEdec(equ, tbs) => 2321 let val LAMBDA(T',TE') = elabPrimTypBindList equ tbs 2322 in 2323 EXISTS(T',(NILenv,NILenv,NILenv,NILenv,TE')) 2324 end 2325 | DATATYPEdec(dbs, tbs_opt) => 2326 let val LAMBDA(T,dbsTE) = initialDatBindTE dbs 2327 val _ = incrBindingLevel(); 2328 val _ = refreshTyNameSet PARAMETERts T; 2329 val tbsTE = elabTypBindList_opt ME FE GE UE VE (plusEnv TE dbsTE) tbs_opt 2330 (* Here dbsTE will get destructively updated too. *) 2331 val _ = checkNoRebindingsTyEnv loc (plusEnv dbsTE tbsTE) 2332 "the same type constructor is defined twice in this datatype declaration" 2333 val (VE',dbsTE') = elabDatBindList ME FE GE UE VE (plusEnv (plusEnv TE dbsTE) tbsTE) dbs 2334 val _ = checkNoRebindingsVarEnv loc VE' 2335 "the same constructor is defined twice in this datatype declaration" 2336 in 2337 maximizeEquality dbsTE'; 2338 setEquality tbsTE; 2339 decrBindingLevel(); 2340 EXISTS(T,(NILenv,NILenv,NILenv,VE', plusEnv dbsTE' tbsTE)) 2341 end 2342 | DATATYPErepdec rep => 2343 let val (VE,TE) = elabDatatypeReplication ME FE GE UE VE TE (loc,rep) 2344 in 2345 EXISTS([],(NILenv,NILenv,NILenv,VE,TE)) 2346 end 2347 | ABSTYPEdec(dbs, tbs_opt, dec2) => 2348 let val LAMBDA(T1,dbsTE) = initialDatBindTE dbs 2349 val _ = incrBindingLevel(); 2350 val _ = refreshTyNameSet PARAMETERts T1; 2351 val tbsTE = elabTypBindList_opt ME FE GE UE VE (plusEnv TE dbsTE) tbs_opt 2352 (* Here dbsTE will get destructively updated too. *) 2353 val _ = checkNoRebindingsTyEnv loc (plusEnv dbsTE tbsTE) 2354 "the same type constructor is defined twice in this abstype declaration" 2355 val (VE',dbsTE') = elabDatBindList ME FE GE UE VE (plusEnv (plusEnv TE dbsTE) tbsTE) dbs 2356 val _ = checkNoRebindingsVarEnv loc VE' 2357 "the same constructor is bound twice in this abstype declaration" 2358 val () = maximizeEquality dbsTE' 2359 val () = setEquality tbsTE; 2360 val EXISTS(T2,(ME2,FE2,GE2,VE2, TE2)) = 2361 elabDec ME FE GE UE (plusEnv VE VE') 2362 (plusEnv (plusEnv TE dbsTE') tbsTE) dec2 2363 in 2364 (* Now let's destructively update the equality attributes *) 2365 (* and the lists of constructors! *) 2366 (* Here VE2 and TE2 will be implicitly influenced too. *) 2367 let val dbsTE2 = absTE dbsTE'; 2368 in 2369 setEquality tbsTE; (* cvr: TODO review why is this repeated? *) 2370 decrBindingLevel(); 2371 refreshExEnv(EXISTS(T1@T2,(ME2,FE2,GE2,VE2, plusEnv(plusEnv dbsTE2 tbsTE) TE2))) 2372 end 2373 (* cvr: *) 2374 end 2375 | EXCEPTIONdec ebs => 2376 EXISTS([],(NILenv,NILenv,NILenv,(elabExBindList ME FE GE UE VE TE ebs), NILenv)) 2377 | LOCALdec (dec1, dec2) => 2378 let val EXISTS(T',(ME',FE',GE',VE', TE')) = 2379 refreshExEnv(elabDec ME FE GE UE VE TE dec1) 2380 val _ = incrBindingLevel() 2381 val _ = refreshTyNameSet PARAMETERts T' 2382 val EXISTS(T'',(ME'', FE'', GE'', VE'',TE'')) = 2383 elabDec (plusEnv ME ME') (plusEnv FE FE') (plusEnv GE GE') 2384 UE (plusEnv VE VE') (plusEnv TE TE') dec2 2385 in decrBindingLevel(); 2386 refreshExEnv(EXISTS(T'@T'',(ME'', FE'', GE'', VE'', TE''))) 2387 end 2388 | OPENdec longmodidinfos => 2389 EXISTS([], 2390 foldL (fn (longmodid,envoptref) => fn (ME',FE',GE',VE',TE') => 2391 let val {qualid,info} = longmodid 2392 val {idKind, idFields,idLoc,... } = info 2393 val (fields,{qualid = csqualid, 2394 info = Env as (ME'',FE'',GE'',VE'',TE'')}) = 2395 findLongModIdForOpen ME idLoc qualid 2396 in 2397 idKind := { qualid=csqualid, info=STRik }; 2398 idFields := fields; 2399 envoptref := SOME Env; 2400 (plusEnv ME' ME'', 2401 plusEnv FE' FE'', 2402 plusEnv GE' GE'', 2403 plusEnv VE' VE'', 2404 plusEnv TE' TE'') 2405 end) 2406 (NILenv,NILenv,NILenv,NILenv,NILenv) 2407 longmodidinfos) 2408 | EMPTYdec => EXISTS([],(NILenv, NILenv,NILenv,NILenv, NILenv)) 2409 | SEQdec (dec1, dec2) => 2410 let val EXISTS(T',(ME',FE',GE',VE', TE')) = 2411 elabDec ME FE GE UE VE TE dec1 2412 val _ = incrBindingLevel(); 2413 val _ = refreshTyNameSet PARAMETERts T'; 2414 val EXISTS(T'',(ME'', FE'', GE'', VE'',TE'')) = 2415 elabDec (plusEnv ME ME') (plusEnv FE FE') (plusEnv GE GE') UE (plusEnv VE VE') (plusEnv TE TE') dec2 2416 in (decrBindingLevel(); 2417 (*cvr: is this refresh too expensive? *) 2418 refreshExEnv(EXISTS(T'@T'',(plusEnv ME' ME'', plusEnv FE' FE'',plusEnv GE' GE'',plusEnv VE' VE'', plusEnv TE' TE'')))) 2419 end 2420 | FIXITYdec _ => EXISTS([],(NILenv,NILenv,NILenv,NILenv,NILenv)) 2421 | STRUCTUREdec mbs => 2422 let val EXISTS(T,ME') = elabModBindList ME FE GE UE VE TE mbs 2423 in refreshExEnv(EXISTS(T,(ME',NILenv,NILenv,NILenv, NILenv))) 2424 end 2425 | FUNCTORdec fbs => 2426 let val EXISTS(T,FE') = elabFunBindList ME FE GE UE VE TE fbs 2427 in refreshExEnv(EXISTS(T,(NILenv,FE',NILenv,NILenv, NILenv))) 2428 end 2429 | SIGNATUREdec sbs => 2430 let val GE' = elabSigBindList ME FE GE UE VE TE sbs 2431 in EXISTS([],(NILenv,NILenv,GE',NILenv, NILenv)) 2432 end 2433and elabModBindList (ME:ModEnv) (FE:FunEnv) (GE:SigEnv) (UE : UEnv) 2434 (VE : VarEnv) (TE : TyEnv) mbs = 2435 foldL_map 2436 (fn EXISTS(T',(locmodid,M')) => fn (EXISTS(T,ME)) => 2437 EXISTS(T@T', bindOnceInEnv ME locmodid M' 2438 "the same structure identifier is declared twice\ 2439 \ in a structure declaration")) 2440 (elabModBind ME FE GE UE VE TE ) (EXISTS([],NILenv)) mbs 2441and elabModBind (ME:ModEnv) (FE:FunEnv) (GE:SigEnv) (UE : UEnv) 2442 (VE : VarEnv) (TE : TyEnv) 2443 (MODBINDmodbind (locmodid as (loc,modid),modexp as (loc',_))) = 2444 let val EXISTSexmod(T,M) = elabModExp STRexpected ME FE GE UE VE TE modexp 2445 val S = case M of 2446 STRmod S => S 2447 | FUNmod _ => 2448 errorMsg loc' 2449 "This module expression is actually a functor \ 2450 \but should be a structure" 2451 in 2452 EXISTS(T,(locmodid,{qualid = mkLocalName modid, info = S})) 2453 end 2454 | elabModBind (ME:ModEnv) (FE:FunEnv) (GE:SigEnv) (UE : UEnv) 2455 (VE : VarEnv) (TE : TyEnv) (ASmodbind (locmodid as (loc,modid),sigexp as (loc',_),exp)) = 2456 let val LAMBDAsig(T,M) = elabSigExp ME FE GE UE VE TE sigexp 2457 val S = case M of FUNmod _ => errorMsg loc' "This signature should specify a structure but actually specifies a functor" 2458 | STRmod S => normRecStr S 2459 val tau = elabExp ME FE GE UE VE TE exp (PACKt(EXISTSexmod(T,M))) 2460 in 2461 EXISTS(T,(locmodid,{qualid = mkLocalName modid, info = S})) 2462 end 2463and elabFunBindList (ME:ModEnv) (FE:FunEnv) (GE:SigEnv) (UE : UEnv) 2464 (VE : VarEnv) (TE : TyEnv) mbs = 2465 foldL_map 2466 (fn EXISTS(T',(locfunid,F')) => fn (EXISTS(T,FE)) => 2467 EXISTS(T@T', bindOnceInEnv FE locfunid F' 2468 "the same functor identifier is declared twice\ 2469 \ in a functor declaration")) 2470 (elabFunBind ME FE GE UE VE TE ) (EXISTS([],NILenv)) mbs 2471and elabFunBind (ME:ModEnv) (FE:FunEnv) (GE:SigEnv) (UE : UEnv) (VE : VarEnv) (TE : TyEnv) 2472 (FUNBINDfunbind (locfunid as (loc,funid),modexp as (loc',_))) = 2473 let val EXISTSexmod(T,M) = elabModExp FUNexpected ME FE GE UE VE TE modexp 2474 val F = case M of 2475 FUNmod F => F 2476 | STRmod _ => 2477 errorMsg loc' 2478 "This module expression is actually a structure \ 2479 \but should be a functor" 2480 in 2481 EXISTS(T,(locfunid,{qualid = mkLocalName funid, info = F})) 2482 end 2483| elabFunBind (ME:ModEnv) (FE:FunEnv) (GE:SigEnv) (UE : UEnv) (VE : VarEnv) (TE : TyEnv) 2484 (ASfunbind (locfunid as (loc,funid),sigexp as (loc',_),exp)) = 2485 let val LAMBDAsig(T,M) = elabSigExp ME FE GE UE VE TE sigexp 2486 val F = case M of 2487 STRmod _ => errorMsg loc' "This signature should specify a functor but actually specifies a structure" 2488 | FUNmod F => F 2489 val tau = elabExp ME FE GE UE VE TE exp (PACKt(EXISTSexmod(T,M))) 2490 in 2491 EXISTS(T,(locfunid,{qualid = mkLocalName funid, info = F})) 2492 end 2493and elabSigBindList (ME:ModEnv) (FE:FunEnv) (GE:SigEnv) (UE : UEnv) 2494 (VE : VarEnv) (TE : TyEnv) sbs = 2495 foldL_map (fn (locsigid,G) => fn GE => 2496 bindOnceInEnv GE locsigid G 2497 "the same signature identifier is declared twice\ 2498 \ in a signature declaration") 2499 (elabSigBind ME FE GE UE VE TE ) NILenv sbs 2500and elabSigBind (ME:ModEnv) (FE:FunEnv) (GE:SigEnv) (UE : UEnv) 2501 (VE : VarEnv) (TE : TyEnv) (SIGBINDsigbind (locsigid as (loc,sigid),sigexp)) = 2502 let val G = elabSigExp ME FE GE UE VE TE sigexp 2503 in 2504 (locsigid, {qualid = mkLocalName sigid, info = G}) 2505 end 2506and elabModExp expectation (ME:ModEnv) (FE:FunEnv) (GE:SigEnv) (UE : UEnv) 2507 (VE : VarEnv) (TE : TyEnv) (loc,(modexp',r)) = 2508 case modexp' of 2509 DECmodexp dec => 2510 let 2511 val EXISTS(T',(ME',FE',GE',VE',TE')) = elabDec ME FE GE UE VE TE dec 2512 val exmod = EXISTSexmod(T',(STRmod (NONrec (STRstr (sortEnv ME', 2513 sortEnv FE', 2514 NILenv, 2515 sortEnv TE', 2516 sortEnv VE'))))) 2517 in 2518 r := SOME exmod; 2519 exmod 2520 end 2521 | LONGmodexp (ii as {info={withOp,...},qualid}) => 2522 ((case resolveExpectation(expectation,withOp) of 2523 STRexpected => 2524 let val {qualid, info} = ii 2525 val {idKind, idFields,... } = info 2526 val (fields,{qualid=resqualid,info=S}) = 2527 findLongModId ME loc qualid 2528 val X = EXISTSexmod([],STRmod ((* cvr: avoid*) copyRecStr [] [] S)) 2529 in 2530 idKind := {qualid = resqualid, info = STRik}; 2531 idFields := fields; 2532 r := SOME X; 2533 X 2534 end 2535 | FUNexpected => 2536 let val {qualid, info} = ii 2537 val {idKind, idFields,... } = info 2538 val (fields,{qualid=resqualid,info=F}) = 2539 findLongFunId ME FE loc qualid 2540 val X = EXISTSexmod([],FUNmod ((* cvr: avoid*) copyGenFun [] [] F)) 2541 in 2542 idKind := {qualid = resqualid, info = FUNik}; 2543 idFields := fields; 2544 r := SOME X; 2545 X 2546 end 2547 | _ => fatalError "elabModExp:resolveExpectation") 2548 handle Toplevel => reportExpectation expectation ii) 2549 | CONmodexp (modexp,sigexp) => 2550 let 2551 val LAMBDAsig(T',M') = elabSigExp ME FE GE UE VE TE sigexp 2552 val EXISTSexmod(T,M) = elabModExp (expectMod M') ME FE GE UE VE TE modexp 2553 in 2554 incrBindingLevel(); 2555 refreshTyNameSet PARAMETERts T; 2556 refreshTyNameSet VARIABLEts T'; 2557 ((matchMod M M') 2558 handle MatchError matchReason => 2559 (msgIBlock 0; 2560 errLocation loc; 2561 errPrompt "Signature mismatch: \ 2562 \the module does not match the signature ..."; 2563 msgEOL(); 2564 msgEBlock(); 2565 errMatchReason "module" "signature" matchReason; 2566 raise Toplevel)); 2567 decrBindingLevel(); 2568 let val X' = EXISTSexmod(T,normMod M') 2569 in 2570 r := SOME X'; 2571 X' 2572 end 2573 end 2574 | ABSmodexp (modexp,sigexp) => 2575 let val LAMBDAsig(T',M') = elabSigExp ME FE GE UE VE TE sigexp 2576 val EXISTSexmod(T,M) = elabModExp (expectMod M') ME FE GE UE VE TE modexp 2577 in 2578 incrBindingLevel(); 2579 refreshTyNameSet PARAMETERts T; 2580 refreshTyNameSet VARIABLEts T'; 2581 ((matchMod M M') 2582 handle MatchError matchReason => 2583 (msgIBlock 0; 2584 errLocation loc; 2585 errPrompt "Signature mismatch: \ 2586 \the module does not match the signature ..."; 2587 msgEOL(); 2588 msgEBlock(); 2589 errMatchReason "module" "signature" matchReason; (* cvr: TODO improve descs*) 2590 raise Toplevel)); 2591 refreshTyNameSet PARAMETERts T'; (* forget the realisation *) 2592 (* cvr: REVIEW forgetting the realisation *only* works if 2593 we haven't done path compression on any realised type names in M that 2594 pointed to T' (usually because of sharing constraints), otherwise 2595 those names won't have their realisations forgotten *) 2596 decrBindingLevel(); 2597 let val X' = EXISTSexmod(T',normMod M') (* re-introduce the quantifier *) 2598 in 2599 r := SOME X'; 2600 X' 2601 end 2602 end 2603 | LETmodexp (dec, modexp) => 2604 let 2605 val EXISTS(T',(ME',FE',GE',VE', TE')) = 2606 elabDec ME FE GE UE VE TE dec; 2607 val _ = incrBindingLevel(); 2608 val _ = refreshTyNameSet PARAMETERts T'; 2609 val EXISTSexmod(T'',M) = 2610 elabModExp expectation (plusEnv ME ME') (plusEnv FE FE') (plusEnv GE GE') UE (plusEnv VE VE') (plusEnv TE TE') modexp 2611 in decrBindingLevel(); 2612 let val X' = EXISTSexmod(T'@T'',M) (* re-introduce the quantifier *) 2613 in 2614 r := SOME X'; 2615 X' 2616 end 2617 end 2618 | FUNCTORmodexp (Generative standard,(loc,modid),idKindDescRef,sigexp,modexp) => 2619 let val _ = checkApplicativeModExp modexp 2620 val LAMBDAsig (T,M) = elabSigExp ME FE GE UE VE TE sigexp 2621 val (ME',FE') = case M of 2622 STRmod S => 2623 (idKindDescRef := STRik; 2624 (bindInEnv ME modid {qualid=mkLocalName modid, 2625 info = normRecStr S}, 2626 FE)) 2627 | FUNmod F => 2628 (idKindDescRef := FUNik; 2629 (ME, 2630 bindInEnv FE modid {qualid=mkLocalName modid, 2631 info = F})) 2632 val _ = incrBindingLevel(); 2633 val _ = refreshTyNameSet PARAMETERts T; 2634 val X = elabModExp MODexpected ME' FE' GE UE VE TE modexp 2635 in 2636 decrBindingLevel(); 2637 let val X' = EXISTSexmod([],FUNmod(T,M,X)) 2638 in 2639 r := SOME X'; 2640 X' 2641 end 2642 end 2643 | FUNCTORmodexp (Applicative,(loc,modid),idKindDescRef,sigexp as (locsigexp,_),modexp) => 2644 let val _ = checkApplicativeModExp modexp 2645 val LAMBDAsig (T,M) = elabSigExp ME FE GE UE VE TE sigexp 2646 val _ = checkApplicativeMod locsigexp M 2647 val (ME',FE') = case M of 2648 STRmod S => 2649 (idKindDescRef := STRik; 2650 (bindInEnv ME modid {qualid=mkLocalName modid, 2651 info = normRecStr S}, 2652 FE)) 2653 | FUNmod F => 2654 (idKindDescRef := FUNik; 2655 (ME, 2656 bindInEnv FE modid {qualid=mkLocalName modid, 2657 info = F})) 2658 val _ = incrBindingLevel(); (* cvr: TODO review *) 2659 val _ = incrBindingLevel(); 2660 val _ = refreshTyNameSet PARAMETERts T; 2661 val EXISTSexmod(T',M') = elabModExp MODexpected ME' FE' GE UE VE TE modexp 2662 in 2663 decrBindingLevel(); 2664 let 2665 val (T'',T'toT'') = parameteriseTyNameSet T' T 2666 val X' = EXISTSexmod(T'',FUNmod(T,M,EXISTSexmod([],copyMod T'toT'' [] M'))) 2667 in 2668 decrBindingLevel(); 2669 r := SOME X'; 2670 X' 2671 end 2672 end 2673 | APPmodexp (funmodexp as (loc',_),modexp) => 2674 let 2675 val EXISTSexmod(T,M) = elabModExp FUNexpected ME FE GE UE VE TE funmodexp 2676 val (T',M',X) = case M of 2677 FUNmod F => copyGenFun [] [] F 2678 | STRmod _ => errorMsg loc' "Illegal application: this module expression \ 2679 \is a structure but should be a functor" 2680 val EXISTSexmod(T'',M'') = elabModExp (expectMod M') ME FE GE UE VE TE modexp 2681 2682 in 2683 incrBindingLevel(); 2684 refreshTyNameSet PARAMETERts T; 2685 refreshTyNameSet VARIABLEts T'; 2686 refreshTyNameSet PARAMETERts T''; 2687 (matchMod M'' M' 2688 handle MatchError matchReason => 2689 (msgIBlock 0; 2690 errLocation loc; 2691 errPrompt "Signature mismatch: \ 2692 \the argument module does not match the functor's domain ..."; 2693 msgEOL(); 2694 msgEBlock(); 2695 errMatchReason "actual argument" "formal argument" matchReason; 2696 raise Toplevel)); 2697 decrBindingLevel(); 2698 let val X' = let val EXISTSexmod(T''',M''') = X 2699 in 2700 EXISTSexmod(T@T''@T''',normMod M''') 2701 end 2702 in 2703 r := SOME X'; 2704 X' 2705 end 2706 end 2707 | PARmodexp modexp => 2708 let val X = elabModExp expectation ME FE GE UE VE TE modexp 2709 in r:= SOME X; 2710 X 2711 end 2712 | RECmodexp ((loc,modid),inforef, 2713 sigexp as (locsigexp,_), 2714 modexp as (locmodexp,_)) => 2715 let val LAMBDAsig (T,M) = elabSigExp ME FE GE UE VE TE sigexp 2716 val (ME',RS) = case M of 2717 STRmod RS => 2718 (let val normRS = normRecStr RS 2719 in 2720 inforef := SOME normRS; 2721 (bindInEnv ME modid {qualid=mkLocalName modid, 2722 info = normRS}, 2723 RS) 2724 end) 2725 | FUNmod F => 2726 errorMsg locsigexp "Illegal recursive structure: \ 2727 \the forward specification should specify \ 2728 \a structure but actually specifies a functor" 2729 val _ = incrBindingLevel(); 2730 val _ = refreshTyNameSet PARAMETERts T; 2731 val EXISTSexmod(T',M') = elabModExp STRexpected ME' FE GE UE VE TE modexp 2732 val RS' = case M' of 2733 STRmod RS' => 2734 RS' 2735 | FUNmod F => 2736 errorMsg locmodexp "Illegal recursive structure: \ 2737 \the body should be \ 2738 \a structure but is actually a functor" 2739 val _ = refreshTyNameSet PARAMETERts T'; 2740 val _ = matchMod (STRmod RS') (STRmod RS) 2741 handle MatchError matchReason => 2742 (msgIBlock 0; 2743 errLocation loc; 2744 errPrompt "Illegal recursive structure: \ 2745 \the body does not enrich the forward specification..."; 2746 msgEOL(); 2747 msgEBlock(); 2748 errMatchReason "body" "forward specification" matchReason; 2749 raise Toplevel) 2750 in 2751 decrBindingLevel(); 2752 let val X' = EXISTSexmod(T@T',STRmod (normRecStr RS')) 2753 in 2754 r := SOME X'; 2755 X' 2756 end 2757 end 2758 2759and elabValBind (ME:ModEnv) (FE:FunEnv) (GE:SigEnv) (UE : UEnv) (VE : VarEnv) 2760 (TE : TyEnv) (vbs : ValBind list) = 2761 let val _ = app (fn ValBind(r as ref p, e) => 2762 r := resolvePatCon ME VE p) 2763 vbs 2764 val ps = map (fn ValBind(ref p,e) => p) vbs 2765 val es = map (fn ValBind(ref p,e) => e) vbs 2766 val pts = map (fn _ => newUnknown()) ps 2767 val VE' = foldL_zip (elabPat ME FE GE UE VE TE ) NILenv ps pts 2768 val VE'' = mkHashEnv (length ps) VE' 2769 in 2770 app2 (elabExp ME FE GE UE VE TE) es pts; 2771 openVE VE'' 2772 end 2773 2774and elabRecValBind (ME:ModEnv) (FE:FunEnv) (GE:SigEnv) (UE : UEnv) (VE : VarEnv) (TE : TyEnv) (vbs : ValBind list) = 2775 let val _ = app (fn ValBind(r as ref p, e) => 2776 r := resolvePatConRec ME VE p) 2777 vbs 2778 val ps = map (fn ValBind(ref p,e) => p) vbs 2779 val es = map (fn ValBind(ref p,e) => e) vbs 2780 val _ = app checkFnExp es 2781 val pts = map (fn _ => newUnknown()) ps 2782 val VE' = foldL_zip (elabPat ME FE GE UE VE TE ) NILenv ps pts 2783 val VE'' = mkHashEnv (length ps) VE' 2784 val rec_VE = plusEnv VE VE'' 2785 in 2786 app2 (elabExp ME FE GE UE rec_VE TE) es pts; 2787 openVE VE'' 2788 end 2789and elabPrimValBind ME FE GE UE VE TE tvs (ii, ty, arity, n) = 2790 let (* cvr: REVIEW val _ = checkRebinding illegalVal ii 2791 *) 2792 val ty_t = elabTy ME FE GE UE VE TE ty 2793 val {qualid, info = {idLoc,...}} = ii 2794 val pid = longIdentAsIdent (#id qualid) "elabPrimValBind" 2795 val q = mkLocalName pid 2796 in ((idLoc,pid), 2797 {qualid =q, 2798 info=(mkScheme tvs ty_t,mkPrimStatus arity n)}) 2799 end 2800 2801 2802 2803 2804and elabValDesc (ME:ModEnv) (FE:FunEnv) (GE:SigEnv) (UE:UEnv) (VE:VarEnv) (TE : TyEnv) tvs ((ii, ty) : ValDesc) = 2805 let val _ = checkRebinding illegalVal ii 2806 val ty_t = elabTy ME FE GE UE VE TE ty 2807 val {qualid, info = {idLoc,...}} = ii 2808 val vid = longIdentAsIdent (#id qualid) "elabValDesc" 2809 val q = mkLocalName vid 2810 in ((idLoc,vid), {qualid = q, info = (mkScheme tvs ty_t,VARname (REGULARo))}) end 2811 2812and elabExDesc (ME:ModEnv) (FE:FunEnv) (GE:SigEnv) (UE : UEnv) (VE : VarEnv) (TE : TyEnv) 2813 ((ii, ty_opt) : ExDesc) = 2814 let val _ = checkRebinding illegalCon ii 2815 val {qualid, info = {idLoc,idKind,...}} = ii 2816 val eid = longIdentAsIdent (#id qualid) "elabExDesc" 2817 val ei = mkExConInfo() 2818 val q = mkLocalName eid 2819 in 2820 idKind := { qualid=q, info=EXCONik ei }; 2821 (case ty_opt of 2822 SOME _ => setExConArity ei 1 2823 | NONE => setExConArity ei 0); 2824 case ty_opt of 2825 SOME ty => 2826 let 2827 val arg_t = (elabTy ME FE GE UE VE TE ty) 2828 in 2829 if typeIsImperative arg_t then () 2830 else errorMsg (xLR ty) "Non-imperative exception type"; 2831 ((idLoc,eid), {qualid = q, info =(type_arrow arg_t type_exn, EXNname ei)}) 2832 end 2833 | NONE => 2834 ((idLoc,eid), {qualid = q, info = (type_exn,EXNname ei)}) 2835 end 2836 2837and elabExDescList (ME:ModEnv) (FE:FunEnv) (GE:SigEnv) (UE : UEnv) 2838 (VE : VarEnv) (TE : TyEnv) eds = 2839 closeEE (foldL_map (fn (locid, tau) => fn env => 2840 bindOnceInEnv env locid tau 2841 "the same exception constructor is specified twice\ 2842 \ in an exception specification") 2843 (elabExDesc ME FE GE UE VE TE ) NILenv eds) 2844 2845 2846and elabSigExp (ME:ModEnv) (FE:FunEnv) (GE:SigEnv) (UE:UEnv) (VE:VarEnv) (TE:TyEnv) 2847 (loc, sigexp) = 2848 (case sigexp of 2849 SPECsigexp spec => 2850 let val LAMBDA(T,S) = elabSpec ME FE GE UE VE TE spec 2851 val _ = checkNoRebindingsStr loc S 2852 "the same identifier is specified twice in the body of this signature" 2853 in LAMBDAsig (T,STRmod (NONrec (removeGEofStr S))) 2854 end 2855 | SIGIDsigexp (loc,sigid) => 2856 let val {qualid,info = G} = findSigId GE loc sigid 2857 in copySig [] [] G 2858 end 2859 | FUNSIGsigexp (Generative standard,(loc,modid),sigexp,sigexp') => 2860 let val LAMBDAsig(T,M) = elabSigExp ME FE GE UE VE TE sigexp 2861 val (ME',FE') = case M of 2862 STRmod S => 2863 (bindInEnv ME modid {qualid=mkLocalName modid, 2864 info = normRecStr S}, 2865 FE) 2866 | FUNmod F => 2867 (ME, 2868 bindInEnv FE modid {qualid=mkLocalName modid, 2869 info = F}) 2870 val _ = incrBindingLevel(); 2871 val _ = refreshTyNameSet PARAMETERts T; 2872 val LAMBDAsig(T',M') = elabSigExp ME' FE' GE UE VE TE sigexp' 2873 in 2874 (decrBindingLevel(); 2875 LAMBDAsig([],FUNmod (T,M,(EXISTSexmod(T',M'))))) 2876 end 2877 | FUNSIGsigexp (Applicative,(loc,modid),sigexp,sigexp') => 2878 let val LAMBDAsig(T,M) = elabSigExp ME FE GE UE VE TE sigexp 2879 val (ME',FE') = case M of 2880 STRmod S => 2881 (bindInEnv ME modid {qualid=mkLocalName modid, 2882 info = normRecStr S}, 2883 FE) 2884 | FUNmod F => 2885 (ME, 2886 bindInEnv FE modid {qualid=mkLocalName modid, 2887 info = F}) 2888 val _ = incrBindingLevel(); 2889 val _ = incrBindingLevel(); 2890 val _ = refreshTyNameSet PARAMETERts T; 2891 val LAMBDAsig(T',M') = elabSigExp ME' FE' GE UE VE TE sigexp' 2892 val _ = decrBindingLevel(); 2893 val (T'',T'toT'') = parameteriseTyNameSet T' T 2894 in decrBindingLevel(); 2895 (LAMBDAsig(T'',FUNmod (T,M,(EXISTSexmod([],copyMod T'toT'' [] M'))))) 2896 end 2897 | WHEREsigexp (sigexp, tyvarseq, longtycon,ty) => (* cvr: TODO review *) 2898 (* Unlike SML, we reject where type constraints that construct inconsistent signatures 2899 by equating a specified datatype with a non-equivalent type or datatype. 2900 In SML, an inconsistent signature can never be implemented, but in Mosml it 2901 can, by using a recursive structure, so we have to rule out inconsitent signatures from 2902 the start. 2903 *) 2904 (case (elabSigExp ME FE GE UE VE TE sigexp) of 2905 (LAMBDAsig(_,FUNmod _)) => 2906 errorMsg loc "Illegal where constraint: the constrained signature specifies a functor but should specify a structure" 2907 | (LAMBDAsig(T,STRmod RS)) => 2908 let val S = SofRecStr RS 2909 val _ = incrBindingLevel(); 2910 val _ = refreshTyNameSet PARAMETERts T; 2911 val _ = checkDuplIds tyvarseq "Duplicate type parameter" 2912 val pars = map (fn tyvar => hd(#id(#qualid tyvar))) tyvarseq 2913 val vs = map (fn tv => newExplicitTypeVar tv) pars 2914 val us = map TypeOfTypeVar vs 2915 val UE' = zip2 pars us 2916 val {qualid = qualid,info={idLoc,...}} = longtycon 2917 val tycon = hd (#id qualid) 2918 val tau = elabTy ME FE GE (UE' @ UE) VE TE ty 2919 val infTyFun = TYPEtyfun(vs,tau) 2920 val infTyStr = (infTyFun,ConEnv []) 2921 val _ = decrBindingLevel(); 2922 val specTyStr = findLongTyConInStr S idLoc qualid 2923 val specTyFun = normTyFun (#1 specTyStr) 2924 val tn = (choose (equalsTyFunTyName specTyFun) T) 2925 handle Subscript => 2926 (msgIBlock 0; 2927 errLocation loc; 2928 errPrompt "Illegal where constraint: the type constructor "; printQualId qualid;msgEOL(); 2929 errPrompt "refers to a transparent type specification";msgEOL(); 2930 errPrompt "but should refer to an opaque type or datatype specification";msgEOL(); 2931 msgEBlock(); 2932 raise Toplevel) 2933 exception IllFormed 2934 in 2935 setTnSort (#info tn) (VARIABLEts); 2936 ((realizeLongTyCon qualid infTyStr specTyStr) 2937 handle MatchError matchReason => 2938 (msgIBlock 0; 2939 errLocation loc; 2940 errPrompt "Illegal where constraint: the type constructor "; printQualId qualid;msgEOL(); 2941 errPrompt "cannot be constrained in this way because ...";msgEOL(); 2942 msgEBlock(); 2943 errMatchReason "constraint" "signature" matchReason; 2944 raise Toplevel)); 2945 ((case !(#tnConEnv(!(#info(tn)))) of (* check well-formedness *) 2946 NONE => () (* nothing to check *) 2947 | SOME specConEnv => 2948 (case normType tau of (* eta-equivalent to a type application? *) 2949 CONt(ts,tyapp) => 2950 let fun equal_args [] [] = () 2951 | equal_args ((VARt w)::ts) (v::vs) = 2952 if w = v 2953 then equal_args ts vs 2954 else raise IllFormed 2955 | equal_args _ _ = raise IllFormed 2956 in 2957 equal_args ts vs; 2958 case conEnvOfTyApp tyapp of 2959 NONE => raise IllFormed 2960 | SOME infConEnv => (* equivalent conenvs ? *) 2961 let 2962 val infMod = 2963 STRmod (NONrec (STRstr 2964 (NILenv,NILenv,NILenv, 2965 mk1Env tycon (infTyFun,infConEnv), 2966 (VEofCE infConEnv)))) 2967 val specMod = copyMod [(tn,tyapp)] [] 2968 (STRmod (NONrec (STRstr 2969 (NILenv,NILenv,NILenv, 2970 mk1Env tycon (specTyFun,specConEnv), 2971 (VEofCE specConEnv))))) 2972 in 2973 ((matchMod infMod specMod) 2974 handle MatchError matchReason => 2975 (msgIBlock 0; 2976 errLocation loc; 2977 errPrompt "Illegal where constraint: the datatype constructor "; 2978 printQualId qualid;msgEOL(); 2979 errPrompt "cannot be constrained in this way because ";msgEOL(); 2980 errPrompt "the constraint's constructor environment \ 2981 \does not match the specification's constructor environment";msgEOL(); 2982 msgEBlock(); 2983 errMatchReason "constraint" "specification" matchReason; 2984 raise Toplevel); 2985 (matchMod specMod infMod) 2986 handle MatchError matchReason => 2987 (msgIBlock 0; 2988 errLocation loc; 2989 errPrompt "Illegal where constraint: the datatype constructor "; 2990 printQualId qualid;msgEOL(); 2991 errPrompt "cannot be constrained in this way because ";msgEOL(); 2992 errPrompt "the specification's constructor environment \ 2993 \does not match the constraint's constructor environment";msgEOL(); 2994 msgEBlock(); 2995 errMatchReason "specification" "constraint" matchReason; 2996 raise Toplevel)) 2997 end 2998 end 2999 | _ => raise IllFormed)) 3000 handle IllFormed => 3001 (msgIBlock 0; 3002 errLocation loc; 3003 errPrompt "Illegal where constraint: the type constructor ";printQualId qualid;msgEOL(); 3004 errPrompt "is specified as a datatype"; msgEOL(); 3005 errPrompt "but its constraint is not a datatype";msgEOL(); 3006 msgEBlock(); 3007 raise Toplevel)); 3008 LAMBDAsig(remove tn T,STRmod RS) 3009 end) 3010 | RECsigexp ((_,modid),sigexp as (locforward,_),sigexp' as (locbody,_)) => 3011 let val LAMBDAsig(T,M) = elabSigExp ME FE GE UE VE TE sigexp 3012 val (ME',RS) = 3013 case M of STRmod RS => 3014 (bindInEnv ME modid {qualid=mkLocalName modid, 3015 info = normRecStr RS}, 3016 RS) 3017 | FUNmod F => 3018 errorMsg locforward 3019 "Illegal recursive signature: \ 3020 \the forward specification should specify \ 3021 \a structure but actually specifies a functor" 3022 val _ = incrBindingLevel(); 3023 val _ = refreshTyNameSet PARAMETERts T; 3024 val LAMBDAsig(T',M') = elabSigExp ME' FE GE UE VE TE sigexp' 3025 val RS' = 3026 case M' of 3027 STRmod RS' => RS' 3028 | FUNmod F => 3029 errorMsg locbody 3030 "Illegal recursive signature: \ 3031 \the body should specify a structure \ 3032 \but actually specifies a functor" 3033 val _ = refreshTyNameSet VARIABLEts T; 3034 val _ = refreshTyNameSet PARAMETERts T'; 3035 val _ = matchMod (STRmod RS') (STRmod RS) 3036 handle MatchError matchReason => 3037 (msgIBlock 0; 3038 errLocation loc; 3039 errPrompt "Illegal recursive signature: \ 3040 \the body does not match the \ 3041 \forward specification..."; 3042 msgEOL(); 3043 msgEBlock(); 3044 errMatchReason "body" "forward specification" matchReason; 3045 raise Toplevel) 3046 in 3047 (decrBindingLevel(); 3048 LAMBDAsig(T',STRmod (RECrec(RS,RS')))) 3049 end) 3050 3051and elabModDesc (ME:ModEnv) (FE:FunEnv) (GE:SigEnv) (UE:UEnv) (VE:VarEnv) (TE : TyEnv) (MODDESCmoddesc (locmodid as (loc,modid), sigexp as (loc',_)) : ModDesc)= 3052 let val LAMBDAsig(T,M) = elabSigExp ME FE GE UE VE TE sigexp 3053 val S = case M of 3054 STRmod S => S 3055 | FUNmod _ => 3056 errorMsg loc' 3057 "This signature actually specifies a functor \ 3058 \but should specify a structure" 3059 in LAMBDA(T,(locmodid,{qualid = mkLocalName modid, info = S})) end 3060 3061and elabModDescList (ME:ModEnv) (FE:FunEnv) (GE:SigEnv) (UE:UEnv) (VE:VarEnv) (TE : TyEnv) mds = 3062 foldL_map 3063 (fn (LAMBDA(T',(locmodid,M))) => fn LAMBDA(T,ME) => 3064 LAMBDA(T@T', bindOnceInEnv ME locmodid M 3065 "the same structure identifier is specified twice\ 3066 \ in a structure specification")) 3067 (elabModDesc ME FE GE UE VE TE ) (LAMBDA([],NILenv)) mds 3068and elabFunDesc (ME:ModEnv) (FE:FunEnv) (GE:SigEnv) (UE:UEnv) (VE:VarEnv) (TE : TyEnv) 3069 (FUNDESCfundesc (locmodid as (loc,modid), sigexp as (loc',_)) : FunDesc)= 3070 let val LAMBDAsig(T,M) = elabSigExp ME FE GE UE VE TE sigexp 3071 val F = case M of 3072 FUNmod F => F 3073 | STRmod _ => 3074 errorMsg loc' 3075 "This signature actually specifies a structure \ 3076 \but should specify a functor" 3077 in LAMBDA(T,(locmodid,{qualid = mkLocalName modid, info = F})) end 3078 3079and elabFunDescList (ME:ModEnv) (FE:FunEnv) (GE:SigEnv) (UE:UEnv) (VE:VarEnv) (TE : TyEnv) mds = 3080 foldL_map 3081 (fn (LAMBDA(T',(locfunid,F))) => fn LAMBDA(T,FE) => 3082 LAMBDA(T@T', bindOnceInEnv FE locfunid F 3083 "the same functor identifier is specified twice\ 3084 \ in a functor specification")) 3085 (elabFunDesc ME FE GE UE VE TE ) (LAMBDA([],NILenv)) mds 3086and elabSpec (ME:ModEnv) (FE:FunEnv) (GE:SigEnv) (UE : UEnv) (VE : VarEnv) (TE : TyEnv) (loc, spec') = 3087 case spec' of 3088 VALspec (tyvarseq,vds) => 3089 let val _ = checkDuplIds tyvarseq "Duplicate explicit type variable" 3090 val pars = map (fn ii => hd(#id(#qualid ii))) tyvarseq 3091 val tyvars = scopedTyVars loc UE pars (unguardedValDescList vds) 3092 val () = incrBindingLevel() 3093 val tvs = map (fn tv => newExplicitTypeVar tv) tyvars 3094 val UE' = (zip2 tyvars (map TypeOfTypeVar tvs)) @ UE 3095 val VE' = 3096 foldL_map (fn(locid, info) => fn acc => 3097 bindOnceInEnv acc locid info 3098 "the same value identifier is specified twice\ 3099 \ in a value specification") 3100 (elabValDesc ME FE GE UE' VE TE tvs) 3101 NILenv vds 3102 in decrBindingLevel(); 3103 LAMBDA([],STRstr (NILenv, NILenv,NILenv, NILenv, VE')) 3104 end 3105 | PRIM_VALspec (tyvarseq,pbs) => 3106 let val _ = checkDuplIds tyvarseq "Duplicate explicit type variable" 3107 val pars = map (fn ii => hd(#id(#qualid ii))) tyvarseq 3108 val tyvars = scopedTyVars loc UE pars (unguardedPrimValBindList pbs) 3109 val () = incrBindingLevel() 3110 val tvs = map (fn tv => newExplicitTypeVar tv) tyvars 3111 val UE' = (zip2 tyvars (map TypeOfTypeVar tvs)) @ UE 3112 val VE' = 3113 foldL_map (fn(locid, info) => fn acc => 3114 bindOnceInEnv acc locid info 3115 "the same value identifier is specified twice\ 3116 \ in a value specification") 3117 (elabPrimValBind ME FE GE UE' VE TE tvs) 3118 NILenv pbs 3119 in decrBindingLevel(); 3120 LAMBDA([],STRstr (NILenv, NILenv,NILenv, NILenv, VE')) 3121 end 3122 | TYPEDESCspec(equ, tds) => 3123 let val LAMBDA(T',TE') = elabPrimTypBindList equ tds 3124 in 3125 LAMBDA(T',STRstr(NILenv, NILenv, NILenv, TE',NILenv)) 3126 end 3127 | TYPEspec tbs => 3128 let val tbsTE = elabTypBindList ME FE GE UE VE TE tbs 3129 in 3130 setEquality tbsTE; 3131 LAMBDA([],STRstr(NILenv, NILenv, NILenv, tbsTE, NILenv)) 3132 end 3133 | DATATYPEspec(dbs, tbs_opt) => 3134 let val LAMBDA(T,dbsTE) = initialDatBindTE dbs 3135 val _ = incrBindingLevel(); 3136 val _ = refreshTyNameSet PARAMETERts T; 3137 val tbsTE = elabTypBindList_opt ME FE GE UE VE (plusEnv TE dbsTE) tbs_opt 3138 (* Here dbsTE will get destructively updated too. *) 3139 val _ = checkNoRebindingsTyEnv loc (plusEnv dbsTE tbsTE) 3140 "the same type constructur is specified twice in this datatype specification" 3141 val (VE',dbsTE') = elabDatBindList ME FE GE UE VE (plusEnv (plusEnv TE dbsTE) tbsTE) dbs 3142 val _ = checkNoRebindingsVarEnv loc VE' 3143 "the same constructor is specified twice in this datatype declaration" 3144 in 3145 maximizeEquality dbsTE'; 3146 setEquality tbsTE; 3147 decrBindingLevel(); 3148 LAMBDA(T,STRstr(NILenv, NILenv, NILenv, plusEnv dbsTE' tbsTE,VE')) 3149 end 3150 | DATATYPErepspec rep => 3151 let val (VE,TE) = elabDatatypeReplication ME FE GE UE VE TE (loc,rep) 3152 in 3153 LAMBDA([],STRstr(NILenv, NILenv, NILenv, TE, VE)) 3154 end 3155 | EXCEPTIONspec eds => 3156 (if U_map unguardedExDesc eds <> [] then 3157 errorMsg loc "Type variables in an exception description" 3158 else (); (* cvr: TODO can be relaxed? *) 3159 LAMBDA([],STRstr(NILenv, NILenv, NILenv, NILenv,elabExDescList ME FE GE [] VE TE eds))) 3160 | STRUCTUREspec mds => 3161 let val LAMBDA(T,ME') = elabModDescList ME FE GE UE VE TE mds 3162 in LAMBDA(T,STRstr (ME', NILenv, NILenv, NILenv, NILenv)) end 3163 | FUNCTORspec mds => 3164 let val LAMBDA(T,FE') = elabFunDescList ME FE GE UE VE TE mds 3165 in LAMBDA(T,STRstr (NILenv, FE', NILenv, NILenv, NILenv)) end 3166 | LOCALspec (spec1, spec2) => 3167 let val (ME',FE',GE',VE', TE') = elabLocalSpec ME FE GE UE VE TE spec1 3168 in 3169 elabSpec (plusEnv ME ME') (plusEnv FE FE') (plusEnv GE GE') UE (plusEnv VE VE') (plusEnv TE TE') spec2 3170 end 3171 | EMPTYspec => LAMBDA([],STRstr(NILenv, NILenv, NILenv, NILenv, NILenv)) 3172 | INCLUDEspec sigexp => 3173 let val LAMBDAsig(T,M) = elabSigExp ME FE GE UE VE TE sigexp 3174 in case M of 3175 FUNmod _ => 3176 errorMsg loc "Illegal include: the included \ 3177 \signature must specify a structure, not a functor" 3178 | STRmod (NONrec S) => LAMBDA(T,S) 3179 | _ => errorMsg loc "Illegal include: the included \ 3180 \signature may not be recursive" 3181 end 3182 | SHARINGTYPEspec (spec,longtyconlist) => 3183 let val LAMBDA(T,S) = elabSpec ME FE GE UE VE TE spec 3184 val _ = incrBindingLevel(); 3185 val _ = refreshTyNameSet PARAMETERts T; 3186 val LocTyFunOfLongTyCon = 3187 let val S' = STRstr(MEofStr S,FEofStr S,GEofStr S,TEofStr S,VEofStr S) 3188 (* this step flattens S' once, instead of once for each find *) 3189 in 3190 fn longtycon as {qualid,info = {idLoc,...},...} => 3191 (idLoc,#1 (findLongTyConInStr S' idLoc qualid)) 3192 end 3193 val LocTyFuns = map LocTyFunOfLongTyCon longtyconlist 3194 fun orderAsT LocT = foldR (fn tn => fn acc => 3195 ((choose (fn (loc,tn') => isEqTN tn tn') LocT)::acc) 3196 handle Subscript => acc) 3197 [] T 3198 val LocT' (* as ((loc,tn)::LocT'') *) = 3199 orderAsT 3200 (map (fn (loc,tyfun) => 3201 ((loc,choose (equalsTyFunTyName tyfun) T) 3202 handle Subscript => 3203 errorMsg loc "Illegal sharing spec: \ 3204 \this type constructor does not denote \ 3205 \an opaque type of the specification")) 3206 LocTyFuns) 3207 val ((loc,tn),LocT'') = case LocT' of 3208 (loctn::LocT'') => (loctn,LocT'') 3209 | _ => fatalError "elabSpec" 3210 val kind = kindTyName tn 3211 val _ = app (fn (loc,tn'') => 3212 if kindTyName tn'' = kind 3213 then () 3214 else errorMsg loc "Illegal sharing spec: \ 3215 \the arity of this type constructor differs from the preceding ones") 3216 (LocT'') 3217 val TminusT'' = foldR (fn (loc,tn) => fn TminusT'' => 3218 remove tn TminusT'') 3219 T LocT'' 3220 val equ = foldR (fn (_,tn) => fn equ => 3221 if (#tnEqu (!(#info tn))) <> FALSEequ 3222 then TRUEequ (* cvr: TODO should we worry about REFequ? *) 3223 else equ) 3224 FALSEequ LocT' 3225 val _ = setTnEqu (#info tn) equ 3226 val _ = app (fn (_,tn'') => setTnSort (#info tn'') 3227 (REAts (APPtyfun(NAMEtyapp tn)))) 3228 LocT'' 3229 in 3230 decrBindingLevel(); 3231 LAMBDA(TminusT'', S) 3232 end 3233 | SEQspec (spec1, spec2) => 3234 let val LAMBDA(T',S) = elabSpec ME FE GE UE VE TE spec1 3235 val _ = incrBindingLevel(); 3236 val _ = refreshTyNameSet PARAMETERts T'; 3237 val LAMBDA(T'',S') = 3238 elabSpec (plusEnv ME (MEofStr S)) 3239 (plusEnv FE (FEofStr S)) 3240 (plusEnv GE (GEofStr S)) 3241 UE 3242 (plusEnv VE (VEofStr S)) 3243 (plusEnv TE (TEofStr S)) 3244 3245 spec2 3246 in decrBindingLevel(); 3247 LAMBDA(T'@T'',SEQstr(S,S')) 3248 end 3249 | SHARINGspec (spec1, (loc',longmodids)) => 3250 let val LAMBDA(T, S) = elabSpec ME FE GE UE VE TE spec1 3251 val _ = incrBindingLevel(); 3252 val _ = refreshTyNameSet PARAMETERts T; 3253 val Ss = 3254 foldR 3255 (fn longmodid as {qualid,info={idLoc,...}} => 3256 (fn Ss => 3257 let val (_,{info = S_i,qualid}) = findLongModIdInStr S idLoc qualid 3258 in 3259 S_i::Ss 3260 end)) 3261 [] longmodids 3262 in let val T' = share (loc',T,Ss) 3263 in 3264 decrBindingLevel(); 3265 LAMBDA(T', S) 3266 end 3267 end 3268 | FIXITYspec _ => 3269 LAMBDA([],STRstr (NILenv,NILenv,NILenv,NILenv, NILenv)) 3270 | SIGNATUREspec sigbinds => 3271 let val GE' = elabSigBindList ME FE GE UE VE TE sigbinds 3272 in LAMBDA([],STRstr(NILenv,NILenv,GE',NILenv, NILenv)) 3273 end 3274 | _ => errorMsg loc "Illegal specification: this form of specification can only \ 3275 \ appear within a local specification" 3276and elabLocalSpec ME FE GE UE VE TE (loc,spec) = 3277 case spec of 3278 EMPTYspec => (NILenv,NILenv,NILenv,NILenv, NILenv) 3279 | SEQspec (spec1, spec2) => 3280 let val (ME',FE',GE',VE',TE') = 3281 elabLocalSpec ME FE GE UE VE TE spec1 3282 val (ME'',FE'',GE'',VE'',TE'') = 3283 elabLocalSpec (plusEnv ME ME') (plusEnv FE FE') 3284 (plusEnv GE GE') UE 3285 (plusEnv VE VE') (plusEnv TE TE') spec2 3286 in (plusEnv ME' ME'', plusEnv FE' FE'', plusEnv GE' GE'', 3287 plusEnv VE' VE'', plusEnv TE' TE'') end 3288 | OPENspec longmodidinfos => 3289 foldL (fn (longmodid,envoptref) => fn (ME',FE',GE',VE',TE') => 3290 let val {qualid,info} = longmodid 3291 val {idKind, idFields,... } = info 3292 val (fields,{qualid = csqualid, 3293 info = Env as (ME'',FE'',GE'',VE'',TE'')}) = 3294 findLongModIdForOpen ME loc qualid 3295 in 3296 idKind := { qualid=csqualid, info=VARik }; 3297 idFields := fields; 3298 (* this should be unnecessary 3299 envoptref := SOME Env; *) 3300 (plusEnv ME' ME'', 3301 plusEnv FE' FE'', 3302 plusEnv GE' GE'', 3303 plusEnv VE' VE'', 3304 plusEnv TE' TE'') 3305 end) 3306 (NILenv,NILenv,NILenv,NILenv,NILenv) 3307 longmodidinfos 3308 | TYPEspec tbs => 3309 let val tbsTE = elabTypBindList ME FE GE UE VE TE tbs in 3310 setEquality tbsTE; 3311 (NILenv,NILenv,NILenv,NILenv, tbsTE) 3312 end 3313 | LOCALspec (spec1, spec2) => 3314 let val (ME',FE',GE',VE', TE') = elabLocalSpec ME FE GE UE VE TE spec1 3315 in 3316 elabLocalSpec (plusEnv ME ME') (plusEnv FE FE') (plusEnv GE GE') UE (plusEnv VE VE') (plusEnv TE TE') spec2 3317 end 3318 | _ => errorMsg loc "Illegal local specification: this form of specification cannot \ 3319 \ appear as a local specification" 3320; 3321 3322 3323fun elabToplevelDec (dec : Dec) = 3324 (if unguardedDec dec <> [] then 3325 errorMsg (xLR dec) "Unguarded type variables at the top-level" 3326 else (); 3327 let val EXISTS(T',(ME',FE',GE',VE',TE')) = 3328 elabDec (mkGlobalME()) (mkGlobalFE()) (mkGlobalGE()) [] 3329 (mkGlobalVE()) (mkGlobalTE()) dec 3330 val _ = if (!currentCompliance) <> Liberal 3331 then Synchk.compliantTopDec dec 3332 else () 3333 in EXISTS(T',(cleanEnv ME', 3334 cleanEnv FE', 3335 cleanEnv GE', 3336 cleanEnv VE', 3337 cleanEnv TE')) 3338 end); 3339 3340fun elabStrDec (dec : Dec) = 3341 (if unguardedDec dec <> [] then 3342 errorMsg (xLR dec) "Unguarded type variables at the top-level" 3343 else (); 3344 let val EXISTS(T',(ME',FE',GE',VE',TE')) = 3345 elabDec (mkGlobalME()) (mkGlobalFE()) (mkGlobalGE()) [] 3346 (mkGlobalVE()) (mkGlobalTE()) dec 3347 val _ = if (!currentCompliance) <> Liberal 3348 then Synchk.compliantStrDec dec 3349 else () 3350 in 3351 EXISTS(T',(cleanEnv ME', 3352 cleanEnv FE', 3353 cleanEnv GE', 3354 cleanEnv VE', 3355 cleanEnv TE')) 3356 end) 3357 3358fun elabToplevelSigExp (sigexp as (loc,_) : SigExp) = 3359 let val LAMBDAsig(T,M) = 3360 elabSigExp (mkGlobalME()) 3361 (mkGlobalFE()) 3362 (mkGlobalGE()) 3363 [] 3364 (mkGlobalVE()) 3365 (mkGlobalTE()) 3366 sigexp 3367 in case M of 3368 FUNmod _ => 3369 errorMsg loc "Illegal unit signature: the signature \ 3370 \must specify a structure, not a functor" 3371 | STRmod RS => 3372 (if (!currentCompliance) <> Liberal 3373 then Synchk.compliantSigExp sigexp 3374 else (); 3375 LAMBDA(T,RS)) 3376 end 3377 3378fun elabToplevelSpec (spec : Spec) = 3379 let val StrSig = 3380 elabSpec (mkGlobalME()) (mkGlobalFE()) 3381 (mkGlobalGE()) [] 3382 (mkGlobalVE()) (mkGlobalTE()) 3383 spec 3384 in 3385 (* we could, but don't, check compliance since toplevel-mode .sig files don't need to be ported 3386 if (!currentCompliance) <> Liberal 3387 then Synchk.compliantTopSpec spec 3388 else (); *) 3389 StrSig 3390 end 3391 3392fun elabSigSpec (spec : Spec) = 3393 let val StrSig = 3394 elabSpec (mkGlobalME()) (mkGlobalFE()) 3395 (mkGlobalGE()) [] 3396 (mkGlobalVE()) (mkGlobalTE()) 3397 spec 3398 in 3399 if (!currentCompliance) <> Liberal 3400 then Synchk.compliantSpec spec 3401 else (); 3402 StrSig 3403 end 3404 3405 3406 3407(* tie the knot *) 3408 3409(* cvr: TODO remove in favour of mutual recursion *) 3410 3411val () = elabSigExpRef := elabSigExp; 3412val () = elabModExpRef := elabModExp; 3413 3414 3415 3416 3417 3418 3419 3420 3421