HORIZON HASKELLDocslts/ghc-9.10.x248f8f02026-10-05Search names, modules, packages, or :: a typeCtrl K

GHC 9.10.3 · lts/ghc-9.10.x · 248f8f0 · 2026-10-05

ModuleAgda-2.7.0.1Haskell2010

Agda.Syntax.Treeless

The treeless syntax is intended to be used as input for the compiler backends. It is more low-level than Internal syntax and is not used for type checking.

Some of the features of treeless syntax are: - case expressions instead of case trees - no instantiated datatypes / constructors

  • 10 types
  • 1 class
  • 20 values
  • PackageAgda-2.7.0.1
  • Exports33
  • LanguageHaskell2010
  • LicenceMIT
  • SourceTreeless.hs

module Agda.Syntax.Abstract.Name

datadata ArgUsage
#

Usage status of function arguments in treeless code.

ArgUsedArgUnused
Instances6Eq, Ord, Show, Generic, NFData, Rep
valuefilterUsed :: [ArgUsage] -> [a] -> [a]
#

filterUsed used args drops those args which are labelled ArgUnused in list used.

Specification:

  filterUsed used args = [ a | (a, ArgUsed) <- zip args $ used ++ repeat ArgUsed ]

Examples:

  filterUsed []                 == id
  filterUsed (repeat ArgUsed)   == id
  filterUsed (repeat ArgUnused) == const []
datadata TTerm
#

Treeless Term. All local variables are using de Bruijn indices.

Constructors

Instances13Eq, Ord, Show, Generic, NFData, Pretty, …
datadata Compiled
#

Constructors

Instances9Eq, Ord, Show, Generic, NFData, Pretty, …
datadata TPrim
#

Compiler-related primitives. This are NOT the same thing as primitives in Agda's surface or internal syntax! Some of the primitives have a suffix indicating which type of arguments they take, using the following naming convention: Char | Type C | Character F | Float I | Integer Q | QName S | String

PAddPAdd64PSubPSub64PMulPMul64PQuotPQuot64PRemPRem64PGeqPLtPLt64PEqIPEq64PEqFPEqSPEqCPEqQPIfPSeqPITo64P64ToI
Instances6Eq, Ord, Show, Generic, NFData, Rep
datadata CaseInfo
#

Constructors

Instances7Eq, Ord, Show, Generic, NFData, NamesIn, …
datadata TAlt
#

Constructors

Instances11Eq, Ord, Show, Generic, NFData, Unreachable, …
datadata TError
#

Constructors

  • TUnreachable

    Code which is unreachable. E.g. absurd branches or missing case defaults. Runtime behaviour of unreachable code is undefined, but preferably the program will exit with an error message. The compiler is free to assume that this code is unreachable and to remove it.

  • TMeta String

    Code which could not be obtained because of a hole in the program. This should throw a runtime error. The string gives some information about the meta variable that got compiled.

Instances6Eq, Ord, Show, Generic, NFData, Rep
valuecoerceAppView :: TTerm -> ((Bool, TTerm), [TTerm])
#

Expose the format coerce f args.

We fuse coercions, even if interleaving with applications. We assume that coercion is powerful enough to satisfy coerce (coerce f a) b = coerce f a b

datadata CaseType
#

Constructors

Instances7Eq, Ord, Show, Generic, NFData, NamesIn, …