[ Pobierz całość w formacie PDF ]
.The symbol is used to separate a declaration in from the resultingJUDGEMENT constraint system and type environment.A judgement of the formDec asserts that, under the assumptions in and , processing thedeclarationDecresults in an enhanced type constraint system,  , and type 10.2 Syntax and type-checking rules 187environment, .This notation makes it clear that the result of processing adeclaration is changes to the type constraint system and type environment.The processing rules for declarations are written similarly to the type-checking rules for the lambda calculus given in Chapter 8:AxiomName Decif the rule is not dependent on hypotheses, orDec DecRuleNameDecwhere the conclusion is written below the line, and the hypotheses are abovethe line.Typically, the expressions appearing in judgements above the line inrules are subexpressions of the expressions appearing in judgements belowthe line.We read the rules starting from the bottom and then proceeding from leftto right across the top.For example, the sample rule can be read as stating, from the type assumptions in and , processingDecresults in a richercollection of type assumptions , if processingDec from and resultsin ,., and processingDec from results in.The type-checking rules for declarations can be found in Figure 10.7.Theyare relatively straightforward.By rule TypeDef, processing a type definitionresults in adding the definition to , but no changes to the type environment,.In contrast, rule ConstDef indicates that processing a constant declarationresults in adding the constant name and its type to the type environment, butno change to the type constraint system,.A list of type or constant declara-tions is processed by processing the first declaration to get an enriched typeenvironment, and then processing the rest of the declarations recursively toget the final type environment.Type-checking rules for non-declarations are written similarly.A judge-ment of the form exp Tasserts that, under the type assumptions in, , the expressionexphas typeT.We introduce a special notation to makewriting type-checking rules easier.IfRTypeis a record type of the formx T x T , weletRTyperef = x RefT x RefT.We will give type-checking rules for each of the other syntactic categoriesof.We start by providing the type-checking rules for expressions inFigure 10.8.Most of these rules are straightforward.By rule Identifier, anidentifier canbe deduced to have the type that is specified for it in the type environment, 188 10 , a Simple Object-Oriented LanguageTDefLstTypeSectype TDefLstt T TDefLstTypeDefLstt T TDefLstTypeDef t T t T ift domCDefLstConstSecconst CDefLstid T E CDefLstConstDefListid T E CDefLstE T id domConstDefid T E id TFigure 10.7 Type checking rules for declarations.In reporting the type of the identifier, all of the type identifiers in the typeare replaced by their definitions in.This is done by writing the resultingtype as (T).Because all user-introduced names will be replaced by theirdefinitions during type-checking, uses structural rather than nameequivalence of types [Lou93].By rule Const, built-in constants are assigned the type that is provided inthe language definition.The expression()is the only value of typeVoid.The expressionnilis unusual in that it can have any object type.Whichtype it is assigned will depend on context.IfEhas typeT, thenrefEis areference toE, and hence has typeRefT.IfEhas typeRefT, i.e., is avariableholding values of typeT, thenvalEhas typeT.Type checking function definitions is only a bit more complicated.By theFunction rule, a function has typeT T T iff the body has typeT under the added assumptions (in ) that the parameters have typesTthroughT.The assumption on the types of formal parameters is necessarysince the function body may involve the formal parameters.Similarly if afunction has typeT T T , and the actual parameters havetypesT throughT , theApplication rule indicates that the result of applyingthe function to the actual parameters has typeT. 10.2 Syntax and type-checking rules 189Identifier id T id TConstant c CwhereCis the pre-assigned type for built-in constantc.Void VoidNil nil ObjectTypeME RefTValuevalE Tid T id T Block TFunctionfunction id T id T T is BlockT T TE T T T E T E TApplicationE E E TE TReferencerefE RefTinst IV meth MClassclass inst meth ClassType IV MwhereSelfType VisObjectType IVref M ,self SelfType close SelfType ObjectType M , andSelfTypedoes not occur inIVorM.E ClassType IV MNewnewE ObjectType ME ObjectType m T m TMessageE m TFigure 10.8 Type-checking rules for expressions of , part 1. 190 10 , a Simple Object-Oriented LanguageThe type checking of classes is more challenging.A class of the formclass inst meth has typeClassType(IV,M), if two conditions hold.First, the record of instance variables,inst, must havetypeIV.Second, therecord of methods,meth, must have typeM.There is a complication, however.Because method bodies may contain oc-currences ofself, we need to type check methods in a context that allows usto assign a type to all expressions involvingself.We assign the typeSelf-Typetoself, whereSelfType=VisObjectType(IVref ,M).Recall thatthetypeexpressionIVref represents a record type formed fromIVby addingRefbefore the type of each field type.That is, ifIV= l T l T ,thenIVref = l RefT l RefT.Whileinstwith typeIVis the record of initial values of instance vari-ables, the typeSelfTypeofselfincludes the types of the instance variablesthemselves.That is, ifxis an instance variable and the class contains an ini-tial value ofxof typeT, then the corresponding type in the visible object typeisRef T [ Pobierz całość w formacie PDF ]

  • zanotowane.pl
  • doc.pisz.pl
  • pdf.pisz.pl
  • funlifepok.htw.pl

    •