The All.agda file

The All.agda file (located in backend/src) contains the Agda and Haskell modules to be imported.

It is a key element of the framework, as both build systems work by calling agda2hs on All.agda and then running GHC on the resulting All.hs. This also explains its structure: it contains several Agda imports followed by several Haskell imports (in a foreign pragma).

The All.agda file in the skeleton looks like this:

{-# OPTIONS --erasure --guardedness #-}

module All where

import AppState
import Interaction
import Logic

import Tool.ErasureProduct
import Tool.Cheat
import Tool.PropositionalEquality
import Tool.Relation
import Tool.Future

import Test.ExampleTest
import Test.Haskell.ExampleTest

import Platform.Win32
import Platform.Posix

-- And now, we also copy them into the Haskell source;
-- this way, we can compile everything by compiling All.hs.
{-# FOREIGN AGDA2HS
{-# LANGUAGE CPP #-}
import AppState
import Interaction
import Logic

import Tool.ErasureProduct
import Tool.Future
import Platform
#-}

Where to include what?

• Add an Agda import for a module which is written in Agda (of course) and you want to get checked by the Agda typechecker. Pretty much, this means every Agda file you add. Only modules that are already written in .hs files should be excluded (like Platform in the skeleton).

• Add a Haskell import for modules you want to run GHC on. This means you should omit Agda modules that contain no agda2hs pragmas: agda2hs does not generate a Haskell file for them (as it would be empty anyway) and GHC would fail if it were to look for them. This includes, for example, the equality tools under the Tool directory. However, you should add modules pre-written in Haskell (like Platform.hs).

Actually, if an Agda import contains further Agda imports, you need not include them in All.agda; similarly, if a Haskell module imports something by itself, you can omit it here.