Scope and type rules for quirk21. [Revision 1] Revision history: Revision 1, 16 Sept 2004: Added type rule for the # unary operation. **************************************************************** The types needed for semantic analysis of quirk21 programs are generated by T --> VOID | BOOLEAN | CHAR | INT | FLOAT | I | T[] | (T1 * ... * Tm -> T0) | oneof {N1 : T1, ..., Nm : Tm} | allof {N1 : T1, ..., Nm : Tm} Each of these types will be represented by an abstract syntax tree for the corresponding quirk21 . For example: VOID = (makeVoidType n) BOOLEAN = (makeBoolType n) et cetera. **************************************************************** Abstract data types of types and type environments are used below to express the typing rules for quirk21. These ADTs are named Qtype and Tenv, and are specified as follows. Signature: var: T -> Qtype type: T -> Qtype isVar?: Qtype -> boolean isType?: Qtype -> boolean untagged: Qtype -> T empty: -> Tenv extend: Tenv x Qsymbol x Qtype -> Tenv lookup: Tenv x Qsymbol -> Qtype Algebraic specification: (isVar? (var t)) = true (isVar? (type t)) = false (isType? (var t)) = false (isType? (type t)) = true (untagged (var t)) = t (untagged (type t)) = t (lookup (empty) I) = type(VOID) (lookup (extend env I1 qt) I0) = qt if (Qsymbol.equals I1 I0) (lookup (extend env I1 qt) I0) = (lookup env I0) otherwise Notation: tenv[] means tenv. tenv[I1: qt1, ...] means (extend tenv I1 qt1)[...]. **************************************************************** The typing judgment tenv |- P means that the P contains no scope or type errors when checked relative to the initial environment tenv. The typing judgment tenv |- T means that, in the type environment tenv, the T contains no scope or type errors. (In practice, this means that all of the type identifiers that are mentioned within T are bound to types within tenv.) The typing judgment tenv |- M :: tenv2 means that, in the type environment tenv, the M contains no scope or type errors, and extends tenv to a type environment tenv2. The typing judgment tenv |- D :: tenv2 means that, in the type environment tenv, the D contains no scope or type errors, and extends tenv to a type environment tenv2. The typing judgment tenv |- E :: T means that, in the type environment tenv, the expression E has type T. **************************************************************** The scope and type rules of quirk21 are defined by the following inference rules. (There are no rules for for statements, boolean disjunctions or conjunctions, or parenthesized expressions because the parser translates those constructs into abstract syntax trees that are handled by the rules below.) Programs: tenv |- M1 :: tenv1 tenv1 |- M2 :: tenv2 ... tenv{n-1} |- Mn :: tenvn tenvn |- E :: T --------------------------- tenv |- E where M1 ... Mn Modules: I1, ..., Im are distinct tenv0 |- D1 :: tenv1 tenv1 |- D2 :: tenv2 ... tenv{n=1} |- Dn :: tenvn tenvn |- E1 :: T1 ... tenvn |- Ek :: Tk tenv = tenv0 [ I1 : lookup (tenvn, I1), ..., Im : lookup (tenvn, Im) ] ---------------------------------------------------------------------- tenv0 |- export I1, ..., Im from D1 ... Dn where E1; ...; Ek :: tenv Module-level declarations: tenv0 |- E1 :: T1 tenv1 = tenv0 [ I1 : var(T1) ] tenv1 |- E2 :: T2 tenv2 = tenv1 [ I2 : var(T2) ] ... tenv{n-1} |- En :: Tn tenvn = tenv{n-1} [ In : var(Tn) ] ---------------------------------------------- tenv0 |- variables I1 = E1 ... Im = Em :: tenvn I1, ..., Im are distinct tenv = tenv0 [ I1 : var(T1), ..., Im : var(Tm) ] tenv |- F1 :: T1 ... tenv |- Fm :: Tm ---------------------------------------------- tenv0 |- functions I1 = F1 ... Im = Fm :: tenv I1, ..., Im are distinct tenv = tenv0 [ I1 : type(T1), ..., Im : type(Tm) ] tenv |- T1 ... tenv |- Tm ------------------------------------------ tenv0 |- types I1 = T1 ... Im = Tm :: tenv Types: ------------ tenv |- void --------------- tenv |- boolean ------------ tenv |- char ----------- tenv |- int -------------- tenv |- float lookup (tenv, I) != type(VOID) ------------------------------ tenv |- I tenv |- T ------------ tenv |- T [] tenv |- T0 tenv |- T1 ... tenv |- Tm ------------------------------------------- tenv |- (T1 * ... * Tm -> T0) N1, ..., Nm are distinct tenv |- T1 ... tenv |- Tm ------------------------------------- tenv |- oneof {N1 : T1, ..., Nm : Tm} N1, ..., Nm are distinct tenv |- T1 ... tenv |- Tm ------------------------------------- tenv |- allof {N1 : T1, ..., Nm : Tm} Expressions: tenv [ I1 : var(T1), ..., Im : var(Tm) ] |- E0 :: T0 ------------------------------------------------------------------------- tenv |- lambda (I1 : T1, ..., Im : Tm) : T0 . E0 :: (T1 * ... * Tm -> T0) tenv [ I1 : var(T1), ..., Im : var(Tm) ] |- E0 :: T0 ---------------------------------------------------- tenv |- lambda (I1 : T1, ..., Im : Tm) : void . E0 :: (T1 * ... * Tm -> VOID) tenv |- E1 :: T1 tenv [ I1 : var(T1) ] |- E2 : T2 ... tenv [ I1 : var(T1), ..., I{m-1} : var(T{m-1}) ] |- Em :: Tm tenv [ I1 : var(T1), ..., Im : var(Tm) ] |- E0 :: T0 ---------------------------------------------------- tenv |- let I1 = E1 ... Im = Em in E0 :: T0 tenv0 = tenv [ I1 : var(T1), ..., Im : var(Tm) ] tenv0 |- F1 :: T1 ... tenv0 |- Fm :: Tm tenv0 |- E0 :: T0 ---------------------------------------------- tenv |- letrec I1 = F1 ... Im = Fm in E0 :: T0 lookup (tenv, I0) = type(T0) tenv |- E0 :: INT tenv |- E1 :: (INT -> T0) --------------------------------- tenv |- new I0 [ E0 ] E1 :: I0 [] lookup (tenv, I0) = type (oneof {N1 : T1, ..., Nm : Tm}) Ni is one of N1, ..., Nm tenv |- Ei :: Ti -------------------------------- tenv |- new I0 { Ni = Ei } :: I0 lookup (tenv, I0) = type (allof {N1 : T1, ..., Nm : Tm}) tenv |- E1 :: T1 ... tenv |- Em :: Tm ---------------------------------------------- tenv |- new I0 { N1 = E1, ..., Nm = Em } :: I0 tenv |- E0 :: I0 lookup (tenv, I0) = type (oneof {N1' : T1', ..., Nn' : Tn'}) {N1 : T1, ..., Nm : Tm} is a subset of {N1' : T1', ..., Nn' : Tn'} tenv[ I1 : var(T1) ] |- E1 :: T ... tenv[ Im : var(Tm) ] |- Em :: T tenv |- E{m+1} :: T ----------------------------------------------------------------------- tenv |- case E0 of N1 : I1 then E1 ... Nm : Im then Em else E{m+1} :: T tenv |- E0 :: boolean tenv |- E1 :: T tenv |- E2 :: T ---------------------------------- tenv |- if E0 then E1 else E2 :: T tenv |- E0 :: boolean tenv |- E1 :: T1 tenv |- E2 :: T2 T1 != T2 ------------------------------------- tenv |- if E0 then E1 else E2 :: VOID tenv |- E0 :: boolean tenv |- E1 :: T ------------------------------ tenv |- while E0 do E1 :: VOID tenv |- E1 :: T1 ... tenv |- Ek :: Tk ----------------------------------- tenv |- begin E1; ...; Ek end :: Tk tenv |- E0 :: T0 [] tenv |- E1 :: INT tenv |- E2 :: T0 ------------------------------- tenv |- E0 [ E1 ] := E2 :: VOID B is one of the following binary operations: == != tenv |- E1 :: BOOLEAN tenv |- E2 :: BOOLEAN -------------------------------------------- tenv |- E1 B E2 :: BOOLEAN B is one of the following binary operations: == != tenv |- E1 :: CHAR tenv |- E2 :: CHAR -------------------------------------------- tenv |- E1 B E2 :: BOOLEAN B is one of the following binary operations: == != < <= > >= tenv |- E1 :: INT tenv |- E2 :: INT -------------------------------------------- tenv |- E1 B E2 :: BOOLEAN B is one of the following binary operations: == != < <= > >= tenv |- E1 :: FLOAT tenv |- E2 :: FLOAT -------------------------------------------- tenv |- E1 B E2 :: BOOLEAN B is one of the following binary operations: + - * / tenv |- E1 :: INT tenv |- E2 :: INT -------------------------------------------- tenv |- E1 B E2 :: INT B is one of the following binary operations: + - * / tenv |- E1 :: FLOAT tenv |- E2 :: FLOAT -------------------------------------------- tenv |- E1 B E2 :: FLOAT B is one of the following binary operations: + - * / tenv |- E1 :: INT tenv |- E2 :: FLOAT -------------------------------------------- tenv |- E1 B E2 :: FLOAT B is one of the following binary operations: + - * / tenv |- E1 :: FLOAT tenv |- E2 :: INT -------------------------------------------- tenv |- E1 B E2 :: FLOAT tenv |- E1 :: BOOLEAN ---------------------- tenv |- ! E1 :: BOOLEAN tenv |- E1 :: INT ------------------ tenv |- - E1 :: INT tenv |- E1 :: FLOAT --------------------- tenv |- - E1 :: FLOAT tenv |- E1 :: T [] ! ------------------- ! tenv |- # E1 :: INT ! ---------------------- tenv |- true :: BOOLEAN ----------------------- tenv |- false :: BOOLEAN L is a charliteral ------------------ tenv |- L :: CHAR L is a stringliteral -------------------- tenv |- L :: CHAR [] L is an intliteral ------------------ tenv |- L :: INT L is a floatliteral ------------------- tenv |- L :: FLOAT lookup (tenv, I1) = var(T) VOID != T --------------- tenv |- I1 :: T tenv |- E0 :: var((T1 * ... * Tn -> T0)) tenv |- E1 :: T1 ... tenv |- En :: Tn ------------------------------ tenv |- E0 (E1, ..., En) :: T0 tenv |- E1 :: I1 lookup (tenv, I1) = type(allof {N1 : T1, ..., Nm : Tm}) N = Ni ------------------ tenv |- E1.N :: Ti tenv |- E1 :: T[] tenv |- E2 :: INT ---------------------- tenv |- E1 [ E2 ] :: T