This repository contains the supplementary material for the paper Beyond Trees: Calculating Graph-Based Compilers. The material includes Agda formalisations of all calculations in the paper. In addition, further examples and calculations are included as well

To typecheck all Agda files, use the included makefile by simply invoking make in this directory. All source files in this directory have been typechecked using version 2.6.3 of Agda and version 1.7.3 of the Agda standard library.

• Code.agda: Generic definitions of tree-structured code (Code) and graph-structured code (Codeᵍ) together with the corresponding definitions of unravelling and bisimilarity. All calculations for non-terminating languages (e.g. Repeat.agda) use this module instead of defining Code and Codeᵍ from scratch (since we need bisimilarity).
• Partial.agda: Definition of the partiality monad Partial + proofs of its laws (section 4).

• Cond.agda: Arithmetic expression language with conditionals (sections 2 and 3).
• Repeat.agda: Arithmetic expression language with simple loops (sections 4).
• WhileState.agda: Arithmetic expression language extended with While loops and a reference cell (section 5).

• While.agda: Arithmetic expression language with a while loop.
• Exception.agda: Arithmetic expression language extended with exceptions.
• Lambda.agda: Call-by-value lambda calculus.

In some cases, Agda's termination checker rejects the definition of the virtual machine exec. In these cases, the termination checker is disabled for exec (using the TERMINATING pragma) and termination is proved manually in the following modules:

• Termination/Exception.agda
• Termination/Lambda.agda

The directory DeBruijn contains an alternative formalisation that uses de Bruijn indices instead of parametric higher-order abstract syntax.

ExecG contains a calculation of the graph-based machine execG from the tree-based machine exec.

Examples gives some example compilation outputs for the While language.

In the paper, we use an idealised Haskell-like syntax for all definitions. Here we outline how this idealised syntax is translated into Agda.

In the paper, we use the codata syntax to distinguish coinductively defined data types from inductive data types. In particular, we use this for the coinductive Partial type:

codata Partial a = Now a | Later (Partial a)

In Agda we use coinductive record types to represent coinductive data types. Moreover, we use sized types to help the termination checker to recognize productive corecursive function definitions. Therefore, the Partial type has an additional parameter of type Size:

data Partial (A : Set) (i : Size) : Set where
  now   : A → Partial A i
  later : ∞Partial A i → Partial A i

record ∞Partial (A : Set) (i : Size) : Set where
  coinductive
  constructor delay
  field
    force : {j : Size< i} → Partial A j

eval :: Expr -> Partial Int
eval (Val n)      = return n
eval (Add x y)    = do m <- eval x; n <- eval y; return (m + n)
eval (Repeat x)   = do eval x; Later (eval (Repeat x))

mutual
  eval : ∀ {i} → Expr → Partial ℕ i
  eval (Val x) = return x
  eval (Add x y) =
    do n ← eval x
       m ← eval y
       return (n + m)
  eval (Repeat x) = eval x >> later (∞eval (Repeat x))

  ∞eval : ∀ {i} → Expr → ∞Partial ℕ i
  force (∞eval x) = eval x

data Code = HALT | REC (∞ Code) | ...

mutual
  data Code (i : Size) : Set where
    HALT : Code i
    REC' : ∞Code i → Code i
    ...
  
  record ∞Code (i : Size) : Set where
    coinductive
    constructor delay
    field
      force :  {j : Size< i} → Code j