Verificacao de Tipos

Regras de tipagem (notação de inferência):

    premissa₁   premissa₂
   ─────────────────────── (nome da regra)
         conclusão

Exemplo — regra para adição:

    Γ ⊢ e₁ : int    Γ ⊢ e₂ : int
   ─────────────────────────────── (T-Add-Int)
         Γ ⊢ e₁ + e₂ : int

    Γ ⊢ e₁ : float    Γ ⊢ e₂ : float
   ──────────────────────────────────── (T-Add-Float)
          Γ ⊢ e₁ + e₂ : float

    Γ ⊢ e₁ : int    Γ ⊢ e₂ : float
   ─────────────────────────────────── (T-Add-Promote)
         Γ ⊢ e₁ + e₂ : float

Onde Γ (gamma) é o ambiente de tipos (tabela de símbolos)
e "⊢" significa "no ambiente Γ, a expressão e tem tipo T".

Classificação de Sistemas de Tipos:

Static Typing (C, Java, Rust)        Dynamic Typing (Python, Ruby, JS)
+----------------------------+       +----------------------------+
| Tipos verificados em        |       | Tipos verificados em        |
| COMPILE-TIME                |       | RUNTIME                     |
| Erros antes de executar     |       | Erros durante execução      |
| Performance: sem checks     |       | Performance: checks em      |
|   em runtime                |       |   cada operação              |
| Exemplos: int x = "hello";  |       | Exemplos: x = "hello"       |
|   → ERRO de compilação      |       |   x + 1 → TypeError runtime  |
+----------------------------+       +----------------------------+

Strong Typing (Python, Rust)         Weak Typing (C, JavaScript)
- Não permite conversões implícitas   - Conversões implícitas
  perigosas                            "5" + 3 → "53" (JS)
- TypeError em operações inválidas     int* cast para void* (C)

Gradual Typing (TypeScript, Python + mypy)
- Combina static e dynamic: partes do programa
  são tipadas estaticamente, partes não.
- Tipo 'Any' serve como escape hatch.

Hierarquia de promoção em C (widening — sem perda de dados):

  char → short → int → long → float → double
                 ↑
                unsigned int → unsigned long

Exemplos de coerção implícita:
  int a = 5;
  float b = 2.5;
  float c = a + b;     // a é promovido a float: 5.0 + 2.5 = 7.5

  char ch = 'A';
  int x = ch + 1;      // ch promovido a int: 65 + 1 = 66

Narrowing (conversão com perda) — requer cast explícito:
  double d = 3.14159;
  int i = (int)d;       // trunca: i = 3 (perda de .14159)
  float f = (float)d;   // perde precisão

Regra do Dragon Book (Cap. 6.5):
  O resultado de uma operação aritmética entre tipos numéricos
  é o tipo "mais largo" (widest) entre os operandos.

from dataclasses import dataclass
from typing import List, Optional

# Hierarquia de promoção numérica
TYPE_HIERARCHY = {'char': 0, 'int': 1, 'float': 2, 'double': 3}

def wider_type(t1, t2):
    """Retorna o tipo mais largo entre dois tipos numéricos."""
    if t1 not in TYPE_HIERARCHY or t2 not in TYPE_HIERARCHY:
        return None  # tipos incompatíveis
    if TYPE_HIERARCHY[t1] >= TYPE_HIERARCHY[t2]:
        return t1
    return t2

class TypeChecker(ASTVisitor):
    """Verificador de tipos para expressões — estilo Dragon Book."""

    def __init__(self, symbol_table):
        self.symbols = symbol_table
        self.errors = []

    def visit_NumberLit(self, node):
        if isinstance(node.value, int):
            return 'int'
        return 'float'

    def visit_StringLit(self, node):
        return 'string'

    def visit_BoolLit(self, node):
        return 'bool'

    def visit_Identifier(self, node):
        info = self.symbols.lookup(node.name)
        return info['type']

    def visit_BinOp(self, node):
        left_type = self.visit(node.left)
        right_type = self.visit(node.right)

        # Regras de tipo para operações aritméticas
        if node.op in ('+', '-', '*', '/'):
            # Concatenação de strings
            if node.op == '+' and left_type == 'string' and right_type == 'string':
                return 'string'
            # Promoção de tipo numérico
            result = wider_type(left_type, right_type)
            if result is None:
                self.errors.append(
                    f"Operação '{node.op}' inválida entre {left_type} e {right_type}"
                )
                return 'error'
            return result

        # Divisão inteira vs. real
        if node.op == '//':
            return 'int'

        # Comparações retornam bool
        if node.op in ('==', '!=', '<', '>', '<=', '>='):
            if not self.types_comparable(left_type, right_type):
                self.errors.append(
                    f"Não é possível comparar {left_type} com {right_type}"
                )
            return 'bool'

        # Operadores lógicos
        if node.op in ('and', 'or'):
            if left_type != 'bool' or right_type != 'bool':
                self.errors.append(
                    f"Operador '{node.op}' requer operandos bool, recebi {left_type} e {right_type}"
                )
            return 'bool'

        return 'error'

    def visit_Assignment(self, node):
        value_type = self.visit(node.value)
        target_info = self.symbols.lookup(node.target.name)
        target_type = target_info['type']

        if target_type != value_type and value_type != 'error':
            if not self.is_compatible(target_type, value_type):
                self.errors.append(
                    f"Não é possível atribuir {value_type} a {target_type}"
                )
        return value_type

    def visit_FuncCall(self, node):
        """Verifica tipos dos argumentos de uma chamada de função."""
        func_info = self.symbols.lookup(node.name)
        if func_info['category'] != 'func':
            self.errors.append(f"'{node.name}' não é uma função")
            return 'error'

        expected_params = func_info.get('params', [])
        if len(node.args) != len(expected_params):
            self.errors.append(
                f"'{node.name}' espera {len(expected_params)} argumentos, "
                f"recebeu {len(node.args)}"
            )
        else:
            for i, (arg, param) in enumerate(zip(node.args, expected_params)):
                arg_type = self.visit(arg)
                if not self.is_compatible(param['type'], arg_type):
                    self.errors.append(
                        f"Argumento {i+1} de '{node.name}': esperado "
                        f"{param['type']}, recebeu {arg_type}"
                    )

        return func_info.get('return_type', 'void')

    def is_compatible(self, target, source):
        """Verifica se source pode ser atribuído a target."""
        if target == source:
            return True
        # Widening: int → float → double
        w = wider_type(target, source)
        return w == target if w else False

    def types_comparable(self, t1, t2):
        """Verifica se dois tipos podem ser comparados."""
        numeric = {'char', 'int', 'float', 'double'}
        if t1 in numeric and t2 in numeric:
            return True
        return t1 == t2

/* Verificação de tipos simplificada em C */
typedef enum {
    TYPE_INT, TYPE_FLOAT, TYPE_CHAR,
    TYPE_STRING, TYPE_BOOL, TYPE_VOID, TYPE_ERROR
} Type;

const char *type_names[] = {
    "int", "float", "char",
    "string", "bool", "void", "error"
};

/* Tabela de promoção: type_promote[t1][t2] = resultado */
static Type type_promote[4][4] = {
    /*            INT         FLOAT       CHAR        STRING  */
    /* INT    */ {TYPE_INT,   TYPE_FLOAT, TYPE_INT,   TYPE_ERROR},
    /* FLOAT  */ {TYPE_FLOAT, TYPE_FLOAT, TYPE_FLOAT, TYPE_ERROR},
    /* CHAR   */ {TYPE_INT,   TYPE_FLOAT, TYPE_CHAR,  TYPE_ERROR},
    /* STRING */ {TYPE_ERROR, TYPE_ERROR, TYPE_ERROR, TYPE_STRING},
};

Type check_binop(Type left, Type right, char op) {
    if (left >= 4 || right >= 4)
        return TYPE_ERROR;

    Type result = type_promote[left][right];

    if (result == TYPE_ERROR) {
        fprintf(stderr,
            "Erro de tipo: não é possível aplicar '%c' a %s e %s\n",
            op, type_names[left], type_names[right]);
    }

    /* Operadores de comparação sempre retornam bool */
    if (op == '<' || op == '>' || op == '=')
        return (result != TYPE_ERROR) ? TYPE_BOOL : TYPE_ERROR;

    return result;
}

# Inferência de tipos por restrições (simplificada)
# Fase 1: gerar restrições percorrendo a AST
# Fase 2: unificar restrições para resolver variáveis de tipo

class TypeVar:
    """Variável de tipo — tipo ainda não resolvido."""
    _counter = 0

    def __init__(self):
        TypeVar._counter += 1
        self.name = f"T{TypeVar._counter}"
        self.resolved = None

    def __repr__(self):
        if self.resolved:
            return str(self.resolved)
        return self.name

class TypeInferencer:
    """Inferência de tipos com unificação."""

    def __init__(self):
        self.constraints = []  # lista de (tipo1, tipo2) que devem ser iguais
        self.env = {}          # nome → tipo

    def infer(self, node):
        """Gera restrições e retorna o tipo inferido."""
        if isinstance(node, NumberLit):
            return 'int' if isinstance(node.value, int) else 'float'

        elif isinstance(node, StringLit):
            return 'string'

        elif isinstance(node, Identifier):
            if node.name in self.env:
                return self.env[node.name]
            # Criar variável de tipo para identificador desconhecido
            tv = TypeVar()
            self.env[node.name] = tv
            return tv

        elif isinstance(node, BinOp):
            lt = self.infer(node.left)
            rt = self.infer(node.right)
            result = TypeVar()
            # Restrição: operandos devem ser compatíveis
            self.constraints.append((lt, rt))
            self.constraints.append((result, wider_type(
                str(lt), str(rt)) or result))
            return result

        elif isinstance(node, Assignment):
            val_type = self.infer(node.value)
            self.env[node.target.name] = val_type
            return val_type

    def unify(self, t1, t2):
        """Unifica dois tipos — resolve variáveis de tipo."""
        if isinstance(t1, TypeVar) and t1.resolved:
            return self.unify(t1.resolved, t2)
        if isinstance(t2, TypeVar) and t2.resolved:
            return self.unify(t1, t2.resolved)
        if isinstance(t1, TypeVar):
            t1.resolved = t2
            return
        if isinstance(t2, TypeVar):
            t2.resolved = t1
            return
        if t1 != t2:
            raise TypeError(f"Não unifica: {t1} ≠ {t2}")

# Exemplo: inferir tipos sem anotações
# let x = 42         → infere x: int
# let y = x + 3.14   → infere y: float (promoção)
# let z = "hello"    → infere z: string

Equivalência de Tipos — dois tipos são o MESMO tipo?

  1. Equivalência Estrutural: dois tipos são iguais se têm
     a mesma estrutura interna.
     struct A { int x; float y; }
     struct B { int x; float y; }
     → A ≡ B em equivalência estrutural (mesmos campos)

  2. Equivalência por Nome: dois tipos são iguais somente
     se têm o mesmo nome.
     → A ≢ B em equivalência por nome (nomes diferentes)

  C usa: equivalência por nome para structs
  OCaml usa: equivalência estrutural
  TypeScript usa: equivalência estrutural (duck typing)

Compatibilidade de Tipos — um tipo pode ser usado onde
outro é esperado?

  float f = 3;    // int é COMPATÍVEL com float (widening)
  int i = 3.14;   // float NÃO é compatível com int (narrowing)

  Relação: se A ≡ B, então A é compatível com B.
  Mas A compatível com B NÃO implica A ≡ B.

# Schema validator para knowledge chunks do harness.os
# Análogo a type checking em compiladores

KNOWLEDGE_SCHEMA = {
    'title':   {'type': 'string', 'required': True},
    'domain':  {'type': 'string', 'required': True,
               'enum': ['build', 'product', 'operations', 'domain']},
    'concern': {'type': 'string', 'required': True,
               'enum': ['relational', 'governance', 'causal',
                       'metacognitive', 'security']},
    'content': {'type': 'string', 'required': True},
    'tokens':  {'type': 'int', 'required': False},
}

def validate_knowledge(chunk, schema=KNOWLEDGE_SCHEMA):
    """Type-check um knowledge chunk contra o schema."""
    errors = []
    for field, rules in schema.items():
        if rules['required'] and field not in chunk:
            errors.append(f"Campo obrigatório ausente: '{field}'")
            continue
        if field in chunk:
            value = chunk[field]
            expected = rules['type']
            actual = type(value).__name__
            if expected == 'string' and not isinstance(value, str):
                errors.append(f"'{field}': esperado string, achei {actual}")
            if 'enum' in rules and value not in rules['enum']:
                errors.append(f"'{field}': valor '{value}' não é válido. "
                              f"Opções: {rules['enum']}")
    return errors

# Testar
chunk_ok = {'title': 'Commit Hygiene', 'domain': 'build',
            'concern': 'governance', 'content': '...'}
print(validate_knowledge(chunk_ok))  # []

chunk_bad = {'title': 'Bad Chunk', 'domain': 'invalid'}
print(validate_knowledge(chunk_bad))
# ["'domain': valor 'invalid' não é válido...",
#  "Campo obrigatório ausente: 'concern'", ...]