TermAnalysis

Returns the set of free variable names in a term.

A variable is free if it is not bound by an enclosing lambda abstraction. This is used by the partial evaluator to determine if a term is closed (has no free variables) and can therefore be evaluated at compile time.

Checks if this term is pure (guaranteed not to fail during evaluation).

A term is pure if evaluating it cannot produce an error or halt evaluation. Pure terms have no observable side effects and can be safely:

• Eliminated if their result is unused (dead code elimination)
• Duplicated (e.g., inlining)
• Reordered relative to other pure terms

==Pure Terms==

The following terms are guaranteed to be pure:

• '''Variables''' (Var): References to bound variables
• '''Constants''' (Const): Literal values (integers, strings, etc.)
• '''Builtins''' (Builtin): Builtin functions (unapplied)
• '''Lambda abstractions''' (LamAbs): Function definitions
• '''Delays''' (Delay): Suspended computations
• '''Force of Delay''': Force(Delay(t)) is pure for any t because it's essentially a no-op that evaluates to t
• '''Forced polymorphic builtins''': Force(Builtin(bn)) where the builtin expects type arguments (e.g., Force(HeadList) is pure because HeadList needs a type argument before it can be applied)
• '''Partially applied builtins''': Builtin applications where not all required arguments are provided yet (e.g., AddInteger $ 1 is pure because it needs one more argument). These cannot fail until fully saturated.
• '''Beta-redexes with pure parts''': Apply(LamAbs(_, body), arg) where both body and arg are pure
• '''Constructors with pure arguments''': Constr(tag, args) where all args are pure
• '''Case expressions with pure parts''': Case(scrut, cases) where the scrutinee and all case branches are pure

==Impure Terms (Can Fail)==

The following terms are considered impure because they can halt evaluation:

• '''Error''' (Error): Always fails with an error
• '''Force of non-delayed, non-builtin terms''': Force(t) where t is not Delay(_) and not a builtin awaiting type arguments. Forcing a non-delayed term will error at runtime. For example, Force(Const(1)) will fail because you cannot force a constant. However, Force(Delay(t)) is pure because it's a no-op.
• '''Saturated partial builtin applications''': Builtin applications where all required type and value arguments are provided and the builtin is not total. These may fail depending on the arguments (e.g., DivideInteger $ 1 $ 0 will error due to division by zero). Note: saturated ''total'' builtins like AddInteger $ 1 $ 2 are pure.
• '''Apply/Case with impure subterms''': If any subterm is impure, the whole term is considered impure

==Usage in Optimization Passes==

'''Dead Code Elimination''' (Inliner):

// Safe to eliminate unused pure arguments
if occurrences == 0 && inlinedArg.isPure then
 go(body, env)  // eliminate the argument

'''Eta Reduction''' (EtaReduce):

// Safe to perform eta-reduction if the function is pure
case LamAbs(x, Apply(f, Var(x))) if !freeNames(f).contains(x) && f.isPure =>
 f  // reduce λx. f x to f

==Examples==

Const(Integer(42)).isPure              // true - constant
Var(NamedDeBruijn("x", 0)).isPure      // true - variable
LamAbs("x", Var("x")).isPure           // true - lambda
Delay(Const(1)).isPure                 // true - delay
Force(Delay(Const(1))).isPure          // true - Force(Delay) is a no-op

Force(Const(1)).isPure                 // false - forcing non-delayed term
Error.isPure                           // false - always fails

// Builtins
Builtin(AddInteger).isPure             // true - unapplied builtin
Apply(Builtin(AddInteger), Const(1)).isPure  // true - partial application
Apply(Apply(Builtin(AddInteger), Const(1)), Const(2)).isPure  // true - saturated total
Apply(Apply(Builtin(DivideInteger), Const(1)), Const(0)).isPure  // false - saturated partial

Force(Builtin(HeadList)).isPure        // true - builtin needs type arg
Apply(Force(Builtin(HeadList)), list).isPure  // depends on list.isPure

// Constructors and Cases
Constr(0, List(Const(1), Const(2))).isPure  // true - pure args
Constr(0, List(Error, Const(2))).isPure     // false - impure arg

Whether the term is in value form (weak head normal form).

A value requires no further computation to evaluate. This is used by:

• PartialEvaluator to skip terms that are already fully reduced
• Inliner to decide if a term is safe to inline in guarded positions

Value forms include:

• Variables, constants, lambda abstractions, delays, and unapplied builtins
• Constructors with all-value arguments (Constr(tag, args) where each arg is a value)
• Unsaturated builtin applications: Force/Apply chains over a Builtin that have not yet received all required arguments (e.g., Force(Builtin(HeadList)), Apply(Builtin(AddInteger), Const(1)), Apply(Force(Builtin(MkCons)), Const(d)))