# Semantic Analysis

Even after passing the lexical and syntax analysis, there are still erros: correct usage of variables, objects, functions.
**Semantic Analysis** ensures that the program satisfies a set of rules regarding the usage of programming constructs.

There are two main categories of semantic analysis:
* Scopes
* Types

## Scope

Lexical scope is textual region in the program.
Scope of an identifier is the lexical scope its declaration refers to

### Symbol Tables

Symantic checks refer to properties of identifier in the program; it need an environment to store identifier info: **symbol table**.

In symbol tables each entry contains name of an identifier and additional info.

### Implementing Symbol Tables

Five operations:
* `Insert Scope`
* `Exit Scope`
* `Find Symbol(x)`
* `Add Symbol(x)`
* `Check Scope(x)`

We can build the symbol tables during parsing or after constructing the AST. The symbol tables should be generated before semantic analysis.


### Function Declaration and Usage Types

* Declare the functions before usage(`cminus`)
* Can use functions before declaration(`py`)
* Separate body declaration(`C`)

### Scope Analysis

* Generate Symbol Table and do Scope Analysis
* Simultaneously

## Types

* Type Checking: A set of rules which ensures the type consistency of different construct in the program.
* Type inferencing: fill missing type info.

### Type Checking

Semantic checking to enforce the type safety of the program.

There are three types of types.
* Statically typed
* Dynamically typed
* Untyped

Static Type Checking does not require additional type checking instructions at runtime. It guarantees that the executions are safe at compile time. But modern languages require both static and dynamic type checking (union, void pointer).

A **type** is a description of a set of values and a set of allowed operations on those values.
**Type expression** is the description the possible types in the program.
**Type System** defines types for language construct like nodes in AST.

Language usually have basic types aka primitive types. Using these types to build type expressions.

### Type Comparison Implementation

There are two options:
1. Implement a method `Equals(T1, T2)`.
It must compare type trees of T1 and T2. For OOP languages also need sub-types


### Type Checking Methodology
Type checking means verifying whether expressions are given proper types
1. Implement using Syntax-Directed Definitions(SDD)
2. First build the AST, then implement type checking by recursive traversal of the AST nodes

#### SDD

SDD associates semantic rules for the productions in the CFG. It checks types based on the semantic rules associated with the production rules.

#### AST Traversal

Type Checking During AST Traversal.

중간에 새로운 타입이 생길 수 있음.

By Recursive Traversal of the AST nodes, inferencing types of AST nodes.

### Inference

$$\frac{\vdash H_1 \vdash H_2 \vdash H_3}{\vdash \text{conclusion}}[\text{rule name}]$$

#### Soundness

항상 참이 되는 타입

$e : T$ means that $e$ is a sound expression of type $T$, that is $e$ is always the type $T$.

for non expression statements use special unit type (like void or empty type)

$S: \text{void}$

#### Proof Tree

$$\frac{
  \frac{1 \text{ is a integer literal}}{\vdash 1: \text{int}} [\text{int}] \;
  \frac{2 \text{ is an integer literal}}{\vdash 2: \text{int}} [\text{int}]
  }{\vdash 1 + 2 : \text{int}} [\text{int add}]
  $$

Proof Tree는 AST를 뒤집은 모양.

If-then-else는 가질 수 있는데, If-then은 타입을 가질 수 없음.



#### Type Environment

어떻게 $x$가 variable이라고 할때 어떤 타입을 가지는지 알 수가 없음.

Type Environment gives types for **free variables**.

$$O \vdash e: T$$
* $O$ is essentially **symbol table**.

Complex Example of Declaration:
```c
for (T1 i = 0;;) {
  exp
}
```
$$\frac{O[T1/i] \vdash \text{exp}: T2}{O\vdash \texttt{for}(i: T1) \set{\text{exp}: T2}}$$

Complex Example of Class Attrs

$$O_C(x) = T$$
* forall attrs $x: T$ in class C
$$O_C$$

Complex Example of Class Methods

### Subtyping