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