Represent array type lengths as BigInt

[ArquintL]

This is a subset of PR #531 in an attempt to make that PR's diff eventually smaller

[Copilot]

Pull request overview

This PR is a focused slice of #531 that changes how array type lengths are represented so they are treated as compile-time constants (BigInt) throughout the frontend → internal AST → Viper type encoding pipeline, making array types more consistent and removing the need to encode the length as an expression argument.

Changes:

• Make internal ArrayTExpr carry a BigInt length (instead of an Expr) and desugar frontend array type expressions using constant evaluation.
• Refine type-head modeling by making ArrayHD carry the array size (BigInt) and adjust type encoding / comparability logic accordingly.
• Add evalBool/evalInt/evalString/evalPerm convenience APIs on TypeInfo backed by existing constant evaluation.

Reviewed changes

Copilot reviewed 9 out of 9 changed files in this pull request and generated 1 comment.

Show a summary per file

File	Description
src/main/scala/viper/gobra/translator/encodings/interfaces/TypeComponentImpl.scala	Encodes array length into the type head serialization; simplifies typeToExpr and precise equality axiom generation accordingly.
src/main/scala/viper/gobra/frontend/info/implementation/property/ConstantEvaluation.scala	Adds eval* wrappers around existing constant evaluators.
src/main/scala/viper/gobra/frontend/info/TypeInfo.scala	Exposes the new eval* methods on the TypeInfo API.
src/main/scala/viper/gobra/frontend/Desugar.scala	Desugars PArrayType lengths via info.evalInt (constant) into internal ArrayTExpr.
src/main/scala/viper/gobra/ast/internal/transform/CGEdgesTerminationTransform.scala	Updates construction of ArrayTExpr to pass the BigInt length directly.
src/main/scala/viper/gobra/ast/internal/theory/TypeHead.scala	Changes ArrayHD from an object to case class ArrayHD(size: BigInt) and updates related logic.
src/main/scala/viper/gobra/ast/internal/theory/Comparability.scala	Updates pattern match for new ArrayHD form.
src/main/scala/viper/gobra/ast/internal/Program.scala	Changes ArrayTExpr(length: BigInt, ...) signature.
src/main/scala/viper/gobra/ast/internal/PrettyPrinter.scala	Prints array type expressions using BigInt length instead of expression pretty-printing.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[jcp19]

LGTM