core

type App struct {
	CoreNode
	Func CoreExpr
	Args []CoreExpr // All must be atomic in ANF
}

type Array struct {
	CoreNode
	Elements []CoreExpr // All must be atomic in ANF
}

type BinOp struct {
	CoreNode
	Op    string
	Left  CoreExpr // Must be atomic in ANF
	Right CoreExpr // Must be atomic in ANF
}

type ConstructorPattern struct {
	Name string
	Args []CorePattern
}

type Contract struct {
	Kind     ContractKind // requires, ensures, or invariant
	Expr     CoreExpr     // The predicate expression (elaborated to Core)
	Message  string       // User-provided or auto-generated message
	Location string       // Source location "file.ail:42"
}

type ContractKind int

type CoreExpr interface {
	ID() uint64
	Span() ast.Pos         // Core span
	OriginalSpan() ast.Pos // Surface origin
	String() string
	// contains filtered or unexported methods
}

type CoreNode struct {
	NodeID   uint64  // Stable identifier assigned by elaborator
	CoreSpan ast.Pos // Position in Core AST
	OrigSpan ast.Pos // Original surface position for diagnostics
}

type CorePattern interface {
	String() string
	// contains filtered or unexported methods
}

type DeclMeta struct {
	Name        string
	IsExport    bool
	IsPure      bool
	SID         string      // Source ID for tracing
	Contracts   []*Contract // M-VERIFY: Contract clauses (requires/ensures)
	VerifyDepth int         // Per-function SMT verify depth override (0 = use global default)
}

type DictAbs struct {
	CoreNode
	Params []DictParam // Dictionary parameters in canonical order
	Body   CoreExpr    // Body with dictionaries available
}

type DictApp struct {
	CoreNode
	Dict   CoreExpr   // Dictionary reference (must be a Var in ANF)
	Method string     // Method name: "add", "eq", "lt", etc.
	Args   []CoreExpr // Method arguments
}

type DictParam struct {
	Name      string // e.g., "dict_Num_α"
	ClassName string // e.g., "Num"
	Type      string // String representation of type
}

type DictRef struct {
	CoreNode
	ClassName string // e.g., "Num", "Ord"
	TypeName  string // Normalized type: "Int", "Float", etc.
}

type DictValue struct {
	TypeClass string                 // Type class name (e.g., "Num", "Eq")
	Type      string                 // Type the instance is for (e.g., "Int", "Float")
	Methods   map[string]interface{} // Method implementations
	Provides  []string               // Other instances this provides (e.g., Ord provides Eq)
}

type Expr interface {
	String() string
}

type Forall struct {
	CoreNode
	Var  string   // Bound variable
	Lo   CoreExpr // Lower bound (inclusive)
	Hi   CoreExpr // Upper bound (exclusive)
	Body CoreExpr // Quantified body (boolean predicate)
}

type GlobalRef struct {
	Module string // e.g., "math/gcd"
	Name   string // e.g., "gcd"
}

type If struct {
	CoreNode
	Cond CoreExpr // Must be atomic in ANF
	Then CoreExpr
	Else CoreExpr
}

type Intrinsic struct {
	CoreNode
	Op   IntrinsicOp
	Args []CoreExpr // [left, right] for binary, [operand] for unary
}

type IntrinsicOp int

type Lam struct {
	CoreNode
	Param string
	Body  Expr
}

type Lambda struct {
	CoreNode
	Params []string
	Body   CoreExpr
}

type Let struct {
	CoreNode
	Name  string
	Value CoreExpr // In ANF: atomic or simple call
	Body  CoreExpr
}

type LetRec struct {
	CoreNode
	Bindings []RecBinding
	Body     CoreExpr
}

type List struct {
	CoreNode
	Elements []CoreExpr // All must be atomic in ANF
}

type ListPattern struct {
	Elements []CorePattern
	Tail     *CorePattern // For ... patterns
}

type Lit struct {
	CoreNode
	Kind  LitKind
	Value interface{}
}

type LitKind int

type LitPattern struct {
	Value interface{}
}

type Match struct {
	CoreNode
	Scrutinee  CoreExpr // Must be atomic in ANF
	Arms       []MatchArm
	Exhaustive bool // Set by elaborator/typechecker
}

type MatchArm struct {
	Pattern CorePattern
	Guard   CoreExpr // Optional, must be atomic
	Body    CoreExpr
}

type Program struct {
	Decls []CoreExpr           // Top-level declarations
	Meta  map[string]*DeclMeta // Metadata for top-level declarations
	Flags ProgramFlags         // Compilation state flags
}

type ProgramFlags struct {
	Lowered bool // Set after OpLowering pass
	Linked  bool // Set after linking
}

type RecBinding struct {
	Name  string
	Value CoreExpr // Usually Lambda for recursion
}

type Record struct {
	CoreNode
	Fields map[string]CoreExpr // All values must be atomic
}

type RecordAccess struct {
	CoreNode
	Record CoreExpr // Must be atomic in ANF
	Field  string
}

type RecordPattern struct {
	Fields map[string]CorePattern
}

type RecordUpdate struct {
	CoreNode
	Base    CoreExpr            // Must be atomic in ANF
	Updates map[string]CoreExpr // All values must be atomic
}

type Tuple struct {
	CoreNode
	Elements []CoreExpr // All must be atomic in ANF
}

type TuplePattern struct {
	Elements []CorePattern
}

type UnOp struct {
	CoreNode
	Op      string
	Operand CoreExpr // Must be atomic in ANF
}

type Var struct {
	CoreNode
	Name string
}

type VarGlobal struct {
	CoreNode
	Ref GlobalRef
}

type VarPattern struct {
	Name string
}

type WildcardPattern struct{}