Add app builtin constructor to generated Init.Expr category

[joehendrix]

Summary

• Adds an app builtin constructor to the generated Init.Expr category in #strata_gen, alongside fvar and bvar
• Fixes a bug where ofAst silently discarded arguments when bvar/fvar appeared as the head of an HNF-flattened application chain
• The app constructor uses Expr α (not ArgF α) for both arguments — toAst wraps the arg with ArgF.expr, and ofAst folds HNF args back into Expr.app chains

Test plan

• Round-trip tests for Expr.app in StrataTest/DDM/Integration/Lean/Gen.lean
• Updated #guard_msgs for #print Expr in Gen.lean and DDMTranslate.lean
• lake build passes
• Investigate polymorphic function calls (type args on fvar)

🤖 Generated with Claude Code

[joehendrix]

Polymorphic type arguments missing from parsed expression tree

When a polymorphic function like identity<a>(x : a) : a is called as identity(42), the type argument is completely absent from the generated concrete expression tree. The call parses as:

Expr.app (Expr.fvar 0) (Expr.natToInt 42)

but should include an explicit type application, e.g.:

Expr.app (Expr.app (Expr.fvar 0) (type int)) (Expr.natToInt 42)

This means ofAst's handling of ArgF.type on fvar/bvar heads (which currently throws) may need to be revisited.

Minimal repro

import Strata.Languages.Core.DDMTransform.Parse

namespace Strata.PolymorphicParsingBug

def pgm : Program :=
#strata
program Core;

function identity<a>(x : a) : a;

procedure Test() returns () {
  var x : int;
  x := identity(42);
};
#end

-- Show the raw concrete type for the procedure (commands[1])
#eval Strata.CoreDDM.Command.ofAst <| pgm.commands[1]!

end Strata.PolymorphicParsingBug

The #eval output shows Expr.app (Expr.fvar 0) (Expr.natToInt 42) with no type argument.

[joehendrix]

Just to follow up on this. The representation is by design; polymorphic functions do not resolve their type arguments in the DDM currently.