v0.1.1 (#15)

* add references to the syntax and cleanup code

* [make] add .PHONY to Makefile targets

* [parser] add parser / pretty for axiom backends

* Pairing progress

* [scoper] Add support for Axiom backends

* [parser] Fix foreign block parsing

* [ app ] adds --no-colors flag for the scope command

* [ghc] upgrade to ghc 9.2.2

* use GHC2021

* [doc] Remove out-of-date comment

* [test] Add ambiguity tests

* [scoper] Improve resolution of local symbols

* [error] WIP improving ambiguity error messages

* [ clean-up ] new lab folder for experimentation

* [ app ] ixes the lint warning

* [ Termination ] removes Alga dependency

* [error] Add message for ambiguous symbol error

* [error] Add ambiguous module message

* [scoper] Remove ErrGeneric

* [test] Add test to suite

* [test] show diff when ast's are different

* [ lab ] folder organization

* [ Makefile ] add targets with --watch option (stack cmds) and remove unused things

* [ app ] add --version flag and fixed warnings and formatting

* [test] remove fromRightIO to fix ambiguity error

* [test] Add test of shadowing public open

* [scoper] Add visibility annotation for Name

* prepare buildIntoTable

* [ Concrete ] add instance of hashable for refs.

* add InfoTableBuilder effect

* [ scoper ] add InfoTableBuilder effect

* [ CHANGELOG ] updated v0.1.1

* [ README ] org version now

Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
Co-authored-by: Paul Cadman <git@paulcadman.dev>

CHANGELOG.md

@@ -1,11 +0,0 @@
-# Changelog
-
-`MiniJuvix` uses [PVP Versioning][1].
-The changelog is available [on GitHub][2].
-
-## 0.0.0.0
-
-* Initially created.
-
-[1]: https://pvp.haskell.org
-[2]: https://github.com/heliaxdev/MiniJuvix/releases

CHANGELOG.org

@@ -0,0 +1,16 @@
+* Changelog
+
+MiniJuvix uses [[https://pvp.haskell.org][PVP Versioning]]. The
+changelog is available
+[[https://github.com/heliaxdev/MiniJuvix/releases][on GitHub]].
+
+** 0.1.1
+
+- Add support in the parser/scoper for Axiom backends
+- Add support for =foreign= keyword
+- New flag =--no-colors= for the scope command
+- Upgrade to GHC 9.2.2
+- Improve resolution of local symbols in the scoper
+- Several new tests related to ambiguous symbols
+- Add =--version= flag
+- Add InfoTableBuilder effect for the scoper

Makefile

@@ -2,9 +2,6 @@ PWD=$(CURDIR)
 PREFIX="$(PWD)/.stack-work/prefix"
 UNAME := $(shell uname)
 
-AGDA_FILES := $(wildcard ./src/MiniJuvix/Syntax/*.agda)
-GEN_HS := $(patsubst %.agda, %.hs, $(AGDA_FILES))
-
 ifeq ($(UNAME), Darwin)
 	THREADS := $(shell sysctl -n hw.logicalcpu)
 else ifeq ($(UNAME), Linux)
@@ -40,26 +37,18 @@ docs :
 	cd docs ; \
 	sh conv.sh
 
+.PHONY : build
+build:
+	stack build --fast --jobs $(THREADS)
+
+build-watch:
+	stack build --fast --file-watch
+
+
 .PHONY : cabal
 cabal :
 	cabal build all
 
-.PHONY : stan
-stan :
-	stan check --include --filter-all --directory=src
-
-setup:
-	stack build --only-dependencies --jobs $(THREADS)
-
-stack:
-	stack build --fast --jobs $(THREADS)
-
-stack-build-watch:
-	stack build --fast --file-watch
-
-repl:
-	stack ghci MiniJuvix:lib
-
 clean:
 	cabal clean
 	stack clean
@@ -67,31 +56,28 @@ clean:
 clean-full:
 	stack clean --full
 
+.PHONY : test
+test:
+	stack test --fast --jobs $(THREADS)
+
+.PHONY : test-watch
+test-watch:
+	stack test --fast --jobs $(THREADS) --file-watch
+
 format:
-	find ./src/ -name "*.hs" -exec ormolu --mode inplace {} --ghc-opt -XStandaloneDeriving --ghc-opt -XUnicodeSyntax --ghc-opt -XDerivingStrategies --ghc-opt -XMultiParamTypeClasses  --ghc-opt  -XTemplateHaskell \;
+	find . -path './src/**/*.hs' -or -path './app/**/*.hs' -exec ormolu --mode inplace {} --ghc-opt -XStandaloneDeriving --ghc-opt -XUnicodeSyntax --ghc-opt -XDerivingStrategies --ghc-opt -XMultiParamTypeClasses  --ghc-opt  -XTemplateHaskell \;
+
+.PHONY : install
+install:
+	stack install --fast --jobs $(THREADS)
+
+.PHONY : install-watch
+install-watch:
+	stack install --fast --jobs $(THREADS) --file-watch
+
+repl:
+	stack ghci MiniJuvix:lib
+
 
 prepare-push:
-	make checklines && make hlint && make format
-
-.PHONY: install-agda
-install-agda:
-	git clone https://github.com/agda/agda.git
-	cd agda
-	cabal update
-	cabal install --overwrite-policy=always --ghc-options='-O2 +RTS -M6G -RTS' alex-3.2.6
-	cabal install --overwrite-policy=always --ghc-options='-O2 +RTS -M6G -RTS' happy-1.19.12
-	pwd
-	cabal install --overwrite-policy=always --ghc-options='-O2 +RTS -M6G -RTS' -foptimise-heavily
-
-.PHONY : install-agda2hs
-install-agda2hs:
-	git clone https://github.com/agda/agda2hs.git
-	cd agda2hs &&	cabal new-install --overwrite-policy=always
-	mkdir -p .agda/
-	touch .agda/libraries
-	echo "agda2hs/agda2hs.agda-lib" > ~/.agda/libraries
-
-.PHONY : agda
-agda :
-	agda2hs ./src/MiniJuvix/Syntax/Core.agda -o src -XUnicodeSyntax -XStandaloneDeriving -XDerivingStrategies -XMultiParamTypeClasses
-	agda2hs ./src/MiniJuvix/Syntax/Eval.agda -o src -XUnicodeSyntax -XStandaloneDeriving -XDerivingStrategies -XMultiParamTypeClasses
+	make checklines && make hlint && make format

README.org

@@ -0,0 +1,63 @@
+MiniJuvix
+[[file:LICENSE][[[https://img.shields.io/badge/license-GPL--3.0--only-blue.svg]]]]
+[[https://github.com/heliaxdev/MiniJuvix/actions/workflows/ci.yml][[[https://github.com/heliaxdev/MiniJuvix/actions/workflows/ci.yml/badge.svg?branch=qtt]]]]
+====
+
+** Description
+
+MiniJuvix is a dependently functional programming language for writing
+efficient formally-verified
+[[https://anoma.network/blog/validity-predicates/][validity
+predicates]], which can be deployed to various distributed ledgers. This
+is a software released for experimentation and research purposes only.
+No warranty is provided or implied.
+
+MiniJuvix addresses many issues that we have experienced while trying to
+write and deploy decentralised applications present in the ecosystem of
+smart-contracts:
+
+- the difficulty of adequate program verification,
+- the ceiling of compositional complexity,
+- the illegibility of execution costs, and
+- the lock-in to particular backends.
+
+** Quick Start
+
+To install MiniJuvix, you can download its sources using
+[[http://git-scm.com/][Git]] from the
+[[https://github.com/anoma/juvix.git][Github repository]]. Then, the
+program can be downloaded and installed with the following commands. You
+will need to have installed [[https://haskellstack.org][Stack]].
+
+#+begin_src shell
+   $ git clone https://github.com/heliaxdev/minijuvix.git
+   $ cd minijuvix
+   $ stack install
+#+end_src
+
+If the installation succeeds, you must be able to run the =minijuvix=
+command from any location. To get the complete list of commands, please
+run =minijuvix --help=.
+
+- How to install [[https://haskellstack.org][Stack]]:? if it's not
+  installed.
+
+  - For Ubuntu : =apt install stack=
+  - For Debian : =apt install haskell-stack=
+  - For Arch Linux : =pacman -S stack=
+  - For macOS : =brew install haskell-stack=
+  - For Windows, following the instructions
+    [[https://docs.haskellstack.org/en/stable/install_and_upgrade/#windows][here]].
+
+It is required at least 8GB RAM for =stack= installation.
+
+- To test everything works correctly, you can run the following command:
+
+#+begin_src shell
+  $ stack test
+#+end_src
+
+** Community
+
+We would love to hear what you think of MiniJuvix! Join us on
+[[https://discord.gg/nsGaCZzJ][Discord]]

agda-proofs/minijuvix-proofs.agda-lib

@@ -1,4 +0,0 @@
-name: minijuvix-proofs
-depend: standard-library
-include: proofs
-flags:

agda-proofs/proofs/Algebra/Structures/StarSemiring.agda

@@ -1,16 +0,0 @@
-open import Relation.Binary using (Rel)
-
-module Algebra.Structures.StarSemiring
-  {a ℓ} {A : Set a}  -- The underlying set
-  (_≈_ : Rel A ℓ)    -- The underlying equality relation
-  where
-
-open import Base
-open import Algebra.Structures {A = A} _≡_
-
-
-record IsStarSemiring (_+_ _*_ : Op₂ A) (★ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where
-  field
-    isSemiring : IsSemiring _+_ _*_ 0# 1#
-    ★-cond-1 : ∀ a → ★ a ≈ (1# + (a * ★ a))
-    ★-cond-2 : ∀ a → ★ a ≈ (1# + (★ a * a))

agda-proofs/proofs/Base.agda

@@ -1,6 +0,0 @@
-module Base where
-
-open import Level using (Level; _⊔_) renaming (suc to lsuc; zero to lzero) public
-open import Relation.Binary.PropositionalEquality using (_≡_; refl; subst; trans; sym; cong) public
-open import Algebra.Core public
-open import Data.Product public

agda-proofs/proofs/Termination/FunctionCall.agda

@@ -1,328 +0,0 @@
-module Termination.FunctionCall where
-
-open import Base
-open import Relation.Binary.PropositionalEquality.Properties as ≡
-open import Data.Product.Properties
-open import Data.Product
-import Termination.SizeRelation as S
-open S using (S)
-import Termination.SizeRelation.Properties as S
-open import Data.Nat using (ℕ)
-open import Axiom.Extensionality.Propositional
-
-module Matrix where
-  open import Data.Fin using (Fin; zero; suc; inject₁; fromℕ; _≟_)
-  open import Data.Nat using (ℕ)
-  open import Data.Vec using (Vec; tabulate)
-  open import Function.Base using (case_of_)
-  open import Relation.Nullary
-
-  -- Square matrix
-  Matrix : (A : Set) → ℕ → Set
-  Matrix A n = Vec (Vec A n) n
-
-  diagonal : {A : Set} → (zero diag : A) → (n : ℕ) → Matrix A n
-  diagonal z diag n = tabulate (λ i → tabulate (λ j →
-    case i ≟ j of λ {(yes _) → diag; (no _) → z}))
-
-
-module Square (n : ℕ) where
-  open import Data.Fin using (Fin; zero; suc; inject₁; fromℕ)
-  open import Data.Vec
-  open Matrix
-
-  -- All calls are assumed to be of arity n
-  Call : Set
-  Call = Vec S n
-
-  -- All edges are assumed to have n calls
-  Edge : Set
-  Edge = Matrix S n
-
-  Call-⁇ : Call
-  Call-⁇ = replicate S.⁇
-
-  -- Call-∼ : Call
-  -- Call-∼ = replicate S.∼
-
-  ⁇ : Edge
-  ⁇ = replicate (replicate S.⁇)
-
-  ∼ : Edge
-  ∼ = diagonal S.⁇ S.∼ n
-
-  infixl 6 _+_
-  infixl 7 _*_
-
-  sumRow : Call → S
-  sumRow = foldr _ S._+_ S.⁇
-
-  _*_ : Op₂ Edge
-  _*_ a b = tabulate (λ i → tabulate (λ j → sumRow (zipWith S._*_ (lookup a i) (lookup (transpose b) j))))
-
-  -- pointwise
-  _+_ : Op₂ Edge
-  (a + b) = tabulate (λ i → tabulate (λ j → lookup (lookup a i) j S.+ lookup (lookup b i) j))
-
-  -- ★ : Op₁ Edge
-  -- ★ a = tabulate (λ i → tabulate (λ j → S.★ (lookup (lookup a i) j)))
-
-
-module 2by2 where
-  open Square 2
-  open import Data.Vec
-  open S.★1 renaming (★ to S★)
-
-  ★ : Op₁ Edge
-  ★ ((b ∷ c ∷ []) ∷ (d ∷ e ∷ []) ∷ []) =
-    let ★b = S★ b
-        Δ = e S.+ (d S.* ★b S.* c)
-        ★Δ = S★ Δ
-
-        b' = ★b S.+ ★b S.* c S.* ★Δ S.* d S.* ★b
-        b'' = S★ (b S.+ c S.* S★ e S.* d)
-        c' = ★b S.* c S.* ★Δ
-        d' = ★Δ S.* d S.* ★b
-        e' = ★Δ
-    in ((b'' ∷ c' ∷ []) ∷
-        (d' ∷ e' ∷ [])
-        ∷ [])
-
-  -- TODO See definition of Call matrix!
-  ★-condition-1 : (a : Edge) → ★ a ≡ ∼ + a * ★ a
-  ★-condition-1 ((S.⁇ ∷ S.⁇ ∷ []) ∷ (S.⁇ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.⁇ ∷ []) ∷ (S.⁇ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.⁇ ∷ []) ∷ (S.⁇ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.⁇ ∷ []) ∷ (S.≺ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.⁇ ∷ []) ∷ (S.≺ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.⁇ ∷ []) ∷ (S.≺ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.⁇ ∷ []) ∷ (S.∼ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.⁇ ∷ []) ∷ (S.∼ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.⁇ ∷ []) ∷ (S.∼ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.≺ ∷ []) ∷ (S.⁇ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.≺ ∷ []) ∷ (S.⁇ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.≺ ∷ []) ∷ (S.⁇ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.≺ ∷ []) ∷ (S.≺ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.≺ ∷ []) ∷ (S.≺ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.≺ ∷ []) ∷ (S.≺ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.≺ ∷ []) ∷ (S.∼ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.≺ ∷ []) ∷ (S.∼ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.≺ ∷ []) ∷ (S.∼ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.∼ ∷ []) ∷ (S.⁇ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.∼ ∷ []) ∷ (S.⁇ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.∼ ∷ []) ∷ (S.⁇ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.∼ ∷ []) ∷ (S.≺ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.∼ ∷ []) ∷ (S.≺ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.∼ ∷ []) ∷ (S.≺ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.∼ ∷ []) ∷ (S.∼ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.∼ ∷ []) ∷ (S.∼ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.∼ ∷ []) ∷ (S.∼ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.⁇ ∷ []) ∷ (S.⁇ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.⁇ ∷ []) ∷ (S.⁇ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.⁇ ∷ []) ∷ (S.⁇ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.⁇ ∷ []) ∷ (S.≺ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.⁇ ∷ []) ∷ (S.≺ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.⁇ ∷ []) ∷ (S.≺ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.⁇ ∷ []) ∷ (S.∼ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.⁇ ∷ []) ∷ (S.∼ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.⁇ ∷ []) ∷ (S.∼ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.≺ ∷ []) ∷ (S.⁇ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.≺ ∷ []) ∷ (S.⁇ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.≺ ∷ []) ∷ (S.⁇ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.≺ ∷ []) ∷ (S.≺ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.≺ ∷ []) ∷ (S.≺ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.≺ ∷ []) ∷ (S.≺ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.≺ ∷ []) ∷ (S.∼ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.≺ ∷ []) ∷ (S.∼ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.≺ ∷ []) ∷ (S.∼ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.∼ ∷ []) ∷ (S.⁇ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.∼ ∷ []) ∷ (S.⁇ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.∼ ∷ []) ∷ (S.⁇ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.∼ ∷ []) ∷ (S.≺ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.∼ ∷ []) ∷ (S.≺ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.∼ ∷ []) ∷ (S.≺ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.∼ ∷ []) ∷ (S.∼ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.∼ ∷ []) ∷ (S.∼ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.∼ ∷ []) ∷ (S.∼ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.⁇ ∷ []) ∷ (S.⁇ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.⁇ ∷ []) ∷ (S.⁇ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.⁇ ∷ []) ∷ (S.⁇ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.⁇ ∷ []) ∷ (S.≺ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.⁇ ∷ []) ∷ (S.≺ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.⁇ ∷ []) ∷ (S.≺ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.⁇ ∷ []) ∷ (S.∼ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.⁇ ∷ []) ∷ (S.∼ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.⁇ ∷ []) ∷ (S.∼ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.≺ ∷ []) ∷ (S.⁇ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.≺ ∷ []) ∷ (S.⁇ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.≺ ∷ []) ∷ (S.⁇ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.≺ ∷ []) ∷ (S.≺ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.≺ ∷ []) ∷ (S.≺ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.≺ ∷ []) ∷ (S.≺ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.≺ ∷ []) ∷ (S.∼ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.≺ ∷ []) ∷ (S.∼ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.≺ ∷ []) ∷ (S.∼ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.∼ ∷ []) ∷ (S.⁇ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.∼ ∷ []) ∷ (S.⁇ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.∼ ∷ []) ∷ (S.⁇ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.∼ ∷ []) ∷ (S.≺ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.∼ ∷ []) ∷ (S.≺ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.∼ ∷ []) ∷ (S.≺ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.∼ ∷ []) ∷ (S.∼ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.∼ ∷ []) ∷ (S.∼ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.∼ ∷ []) ∷ (S.∼ ∷ S.∼ ∷ []) ∷ []) = refl
-
-
-
--- Simplified version
-module SingleCall where
-  open S.★1 renaming (★ to S★)
-
-  -- All calls have exactly 2 arguments
-  Call₂ : Set
-  Call₂ = S × S
-
-  -- An edge is a single function call
-  Edge₁ : Set
-  Edge₁ = Call₂
-
-  ⁇ : Edge₁
-  ⁇ = S.⁇ , S.⁇
-
-  ∼ : Edge₁
-  ∼ = S.∼ , S.∼
-
-  infixl 6 _+_
-  infixl 7 _*_
-
-  _*_ : Op₂ Edge₁
-  _*_ (a , b) (a' , b') = a S.* a' , b S.* b'
-
-  _+_ : Op₂ Edge₁
-  (a , b) + (a' , b') = a S.+ a' , b S.+ b'
-
-  open import Algebra.Structures {A = Call₂} _≡_
-  open import Algebra.Definitions {A = Call₂} _≡_
-  open import Algebra.Structures.StarSemiring {A = Call₂} _≡_
-
-  ×-≡,≡→≡ : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} → {p₁@(a₁ , b₁) p₂@(a₂ , b₂) : A × B} → (a₁ ≡ a₂ × b₁ ≡ b₂) → p₁ ≡ p₂
-  ×-≡,≡→≡ (refl , refl) = refl
-
-  +-Commutative : Commutative _+_
-  +-Commutative a b = ×-≡,≡→≡
-    (S.+-Commutative (proj₁ a) (proj₁ b)
-    , S.+-Commutative (proj₂ a) (proj₂ b))
-
-  +-Associative : Associative _+_
-  +-Associative a b c = ×-≡,≡→≡
-     (S.+-Associative (proj₁ a) _ _
-     , S.+-Associative (proj₂ a) _ _)
-
-  +-IsMagma : IsMagma _+_
-  +-IsMagma = record
-    { isEquivalence = ≡.isEquivalence ;
-    ∙-cong = λ { refl refl → refl }}
-
-  +-IsSemigroup : IsSemigroup _+_
-  +-IsSemigroup = record { isMagma = +-IsMagma ; assoc = +-Associative }
-
-  +-Identityˡ : LeftIdentity ⁇ _+_
-  +-Identityˡ _ = refl
-
-  +-Identityʳ : RightIdentity ⁇ _+_
-  +-Identityʳ (fst , snd) = ×-≡,≡→≡ (S.+-Identityʳ _ , S.+-Identityʳ _)
-
-  +-Identity : Identity ⁇ _+_
-  +-Identity = +-Identityˡ , +-Identityʳ
-
-  +-IsMonoid : IsMonoid _+_ ⁇
-  +-IsMonoid = record { isSemigroup = +-IsSemigroup ; identity = +-Identity }
-
-  +-IsCommutativeMonoid : IsCommutativeMonoid _+_ ⁇
-  +-IsCommutativeMonoid = record
-    { isMonoid = +-IsMonoid ;
-    comm = +-Commutative }
-
-  -- Proofs on _*_
-
-  *-Associative : Associative _*_
-  *-Associative a b c = ×-≡,≡→≡
-     (S.*-Associative (proj₁ a) _ _
-     , S.*-Associative (proj₂ a) _ _)
-
-  *-Identityˡ : LeftIdentity ∼ _*_
-  *-Identityˡ _ = refl
-
-  *-Identityʳ : RightIdentity ∼ _*_
-  *-Identityʳ (fst , snd) = ×-≡,≡→≡ (S.*-Identityʳ _ , S.*-Identityʳ _)
-
-  *-Identity : Identity ∼ _*_
-  *-Identity = *-Identityˡ , *-Identityʳ
-
-  -- Proofs on + and *
-
-  *-DistributesOverˡ-+ : _*_ DistributesOverˡ _+_
-  *-DistributesOverˡ-+ a b c = ×-≡,≡→≡
-   (S.*-DistributesOverˡ-+ (proj₁ a) _ _
-   , S.*-DistributesOverˡ-+ (proj₂ a) _ _)
-
-  *-DistributesOverʳ-+ : _*_ DistributesOverʳ _+_
-  *-DistributesOverʳ-+ a b c = ×-≡,≡→≡
-   (S.*-DistributesOverʳ-+ (proj₁ a) (proj₁ b) _
-   , S.*-DistributesOverʳ-+ (proj₂ a) (proj₂ b) _)
-
-  *-DistributesOver-+ : _*_ DistributesOver _+_
-  *-DistributesOver-+ = *-DistributesOverˡ-+ , *-DistributesOverʳ-+
-
-  *-IsMagma : IsMagma _*_
-  *-IsMagma = record
-   { isEquivalence = ≡.isEquivalence
-    ; ∙-cong = λ {refl refl → refl }}
-
-  *-IsSemigroup : IsSemigroup _*_
-  *-IsSemigroup = record { isMagma = *-IsMagma ; assoc = *-Associative }
-
-  *-IsMonoid : IsMonoid _*_ ∼
-  *-IsMonoid = record { isSemigroup = *-IsSemigroup ; identity = *-Identity }
-
-  +-*-IsSemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero _+_ _*_ ⁇ ∼
-  +-*-IsSemiringWithoutAnnihilatingZero = record
-    { +-isCommutativeMonoid = +-IsCommutativeMonoid
-    ; *-isMonoid = *-IsMonoid
-    ; distrib = *-DistributesOver-+
-    }
-
-  *-LeftZero : LeftZero ⁇ _*_
-  *-LeftZero _ = refl
-
-  *-RightZero : RightZero ⁇ _*_
-  *-RightZero x = ×-≡,≡→≡
-    (S.*-RightZero (proj₁ x)
-    , S.*-RightZero (proj₂ x))
-
-  *-Zero : Zero ⁇ _*_
-  *-Zero = *-LeftZero , *-RightZero
-
-  +-*-IsSemiring : IsSemiring _+_ _*_ ⁇ ∼
-  +-*-IsSemiring = record
-    { isSemiringWithoutAnnihilatingZero = +-*-IsSemiringWithoutAnnihilatingZero
-    ; zero = *-Zero }
-
-  ★ : Op₁ Edge₁
-  ★ (a , b) = S★ a , S★ b
-
-  ★-condition-1 : (a : Edge₁) → ★ a ≡ ∼ + a * ★ a
-  ★-condition-1 a = ×-≡,≡→≡
-    (S.★-condition-1 (proj₁ a)
-    , S.★-condition-1 (proj₂ a))
-
-  ★-condition-2 : (a : Edge₁) → ★ a ≡ ∼ + ★ a * a
-  ★-condition-2 a = ×-≡,≡→≡
-    (S.★-condition-2 (proj₁ a)
-    , S.★-condition-2 (proj₂ a))
-
-  +-*-★-IsStarSemiring : IsStarSemiring _+_ _*_ ★ ⁇ ∼
-  +-*-★-IsStarSemiring = record
-    { isSemiring = +-*-IsSemiring
-    ; ★-cond-1 = ★-condition-1
-    ; ★-cond-2 = ★-condition-2 }

agda-proofs/proofs/Termination/SizeRelation.agda

@@ -1,60 +0,0 @@
-module Termination.SizeRelation where
-
-open import Base
-open import Relation.Binary.PropositionalEquality.Properties as ≡
-
-data S : Set where
-  ⁇ : S
-  ≺ : S
-  ∼ : S
-
-infixl 6 _+_
-infixl 7 _*_
-
-_*_ : Op₂ S
-⁇ * _ = ⁇
-∼ * a = a
-≺ * ⁇ = ⁇
-≺ * ∼ = ≺
-≺ * ≺ = ≺
-
-_+_ : Op₂ S
-≺ + _ = ≺
-∼ + ≺ = ≺
-∼ + ∼ = ∼
-∼ + ⁇ = ∼
-⁇ + b = b
-
-module ★1 where
-  ★ : Op₁ S
-  ★ ⁇ = ∼
-  ★ ≺ = ≺
-  ★ ∼ = ∼
-
-  private
-    ★-condition-1 : (a : S) → ★ a ≡ ∼ + a * ★ a
-    ★-condition-1 ⁇ = refl
-    ★-condition-1 ≺ = refl
-    ★-condition-1 ∼ = refl
-
-    ★-condition-2 : (a : S) → ★ a ≡ ∼ + ★ a * a
-    ★-condition-2 ⁇ = refl
-    ★-condition-2 ≺ = refl
-    ★-condition-2 ∼ = refl
-
-module ★2 where
-  ★ : Op₁ S
-  ★ ⁇ = ∼
-  ★ ≺ = ≺
-  ★ ∼ = ≺
-
-  private
-    ★-condition-1 : (a : S) → ★ a ≡ ∼ + a * ★ a
-    ★-condition-1 ⁇ = refl
-    ★-condition-1 ≺ = refl
-    ★-condition-1 ∼ = refl
-
-    ★-condition-2 : (a : S) → ★ a ≡ ∼ + ★ a * a
-    ★-condition-2 ⁇ = refl
-    ★-condition-2 ≺ = refl
-    ★-condition-2 ∼ = refl

agda-proofs/proofs/Termination/SizeRelation/Properties.agda

@@ -1,185 +0,0 @@
-module Termination.SizeRelation.Properties where
-
-open import Base
-open import Relation.Binary.PropositionalEquality.Properties as ≡
-open import Termination.SizeRelation
-
-open import Algebra.Structures {A = S} _≡_
-open import Algebra.Definitions {A = S} _≡_
-open import Algebra.Structures.StarSemiring {A = S} _≡_
-
--- Proofs on _+_
-
-+-Commutative : Commutative _+_
-+-Commutative ⁇ ⁇ = refl
-+-Commutative ⁇ ≺ = refl
-+-Commutative ⁇ ∼ = refl
-+-Commutative ≺ ⁇ = refl
-+-Commutative ≺ ≺ = refl
-+-Commutative ≺ ∼ = refl
-+-Commutative ∼ ⁇ = refl
-+-Commutative ∼ ≺ = refl
-+-Commutative ∼ ∼ = refl
-
-+-Associative : Associative _+_
-+-Associative ⁇ _ _ = refl
-+-Associative ≺ _ _ = refl
-+-Associative ∼ ⁇ _ = refl
-+-Associative ∼ ≺ _ = refl
-+-Associative ∼ ∼ ⁇ = refl
-+-Associative ∼ ∼ ≺ = refl
-+-Associative ∼ ∼ ∼ = refl
-
-+-IsMagma : IsMagma _+_
-+-IsMagma = record
-  { isEquivalence = ≡.isEquivalence ;
-  ∙-cong = λ { refl refl → refl }}
-
-+-IsSemigroup : IsSemigroup _+_
-+-IsSemigroup = record { isMagma = +-IsMagma ; assoc = +-Associative }
-
-+-Identityˡ : LeftIdentity ⁇ _+_
-+-Identityˡ _ = refl
-
-+-Identityʳ : RightIdentity ⁇ _+_
-+-Identityʳ ⁇ = refl
-+-Identityʳ ≺ = refl
-+-Identityʳ ∼ = refl
-
-+-Identity : Identity ⁇ _+_
-+-Identity = +-Identityˡ , +-Identityʳ
-
-+-IsMonoid : IsMonoid _+_ ⁇
-+-IsMonoid = record { isSemigroup = +-IsSemigroup ; identity = +-Identity }
-
-+-IsCommutativeMonoid : IsCommutativeMonoid _+_ ⁇
-+-IsCommutativeMonoid = record
-  { isMonoid = +-IsMonoid ;
-   comm = +-Commutative }
-
--- Proofs on _*_
-
-*-Associative : Associative _*_
-*-Associative ⁇ _ _ = refl
-*-Associative ≺ ⁇ _ = refl
-*-Associative ≺ ≺ ⁇ = refl
-*-Associative ≺ ≺ ≺ = refl
-*-Associative ≺ ≺ ∼ = refl
-*-Associative ≺ ∼ _ = refl
-*-Associative ∼ _ _ = refl
-
-*-Commutative : Commutative _*_
-*-Commutative ⁇ ⁇ = refl
-*-Commutative ⁇ ≺ = refl
-*-Commutative ⁇ ∼ = refl
-*-Commutative ≺ ⁇ = refl
-*-Commutative ≺ ≺ = refl
-*-Commutative ≺ ∼ = refl
-*-Commutative ∼ ⁇ = refl
-*-Commutative ∼ ≺ = refl
-*-Commutative ∼ ∼ = refl
-
-*-Identityˡ : LeftIdentity ∼ _*_
-*-Identityˡ _ = refl
-
-*-Identityʳ : RightIdentity ∼ _*_
-*-Identityʳ ⁇ = refl
-*-Identityʳ ≺ = refl
-*-Identityʳ ∼ = refl
-
-*-Identity : Identity ∼ _*_
-*-Identity = *-Identityˡ , *-Identityʳ
-
--- Proofs on + and *
-
-*-DistributesOverˡ-+ : _*_ DistributesOverˡ _+_
-*-DistributesOverˡ-+ ⁇ _ _ = refl
-*-DistributesOverˡ-+ ≺ ⁇ _ = refl
-*-DistributesOverˡ-+ ≺ ≺ _ = refl
-*-DistributesOverˡ-+ ≺ ∼ ⁇ = refl
-*-DistributesOverˡ-+ ≺ ∼ ≺ = refl
-*-DistributesOverˡ-+ ≺ ∼ ∼ = refl
-*-DistributesOverˡ-+ ∼ _ _ = refl
-
-*-DistributesOverʳ-+ : _*_ DistributesOverʳ _+_
-*-DistributesOverʳ-+ ⁇ ⁇ _ = refl
-*-DistributesOverʳ-+ ⁇ ≺ ⁇ = refl
-*-DistributesOverʳ-+ ⁇ ≺ ≺ = refl
-*-DistributesOverʳ-+ ⁇ ≺ ∼ = refl
-*-DistributesOverʳ-+ ⁇ ∼ ⁇ = refl
-*-DistributesOverʳ-+ ⁇ ∼ ≺ = refl
-*-DistributesOverʳ-+ ⁇ ∼ ∼ = refl
-*-DistributesOverʳ-+ ≺ ⁇ _ = refl
-*-DistributesOverʳ-+ ≺ ≺ _ = refl
-*-DistributesOverʳ-+ ≺ ∼ ⁇ = refl
-*-DistributesOverʳ-+ ≺ ∼ ≺ = refl
-*-DistributesOverʳ-+ ≺ ∼ ∼ = refl
-*-DistributesOverʳ-+ ∼ ⁇ _ = refl
-*-DistributesOverʳ-+ ∼ ≺ _ = refl
-*-DistributesOverʳ-+ ∼ ∼ ⁇ = refl
-*-DistributesOverʳ-+ ∼ ∼ ≺ = refl
-*-DistributesOverʳ-+ ∼ ∼ ∼ = refl
-
-*-DistributesOver-+ : _*_ DistributesOver _+_
-*-DistributesOver-+ = *-DistributesOverˡ-+ , *-DistributesOverʳ-+
-
-*-IsMagma : IsMagma _*_
-*-IsMagma = record
-  { isEquivalence = ≡.isEquivalence
-   ; ∙-cong = λ {refl refl → refl }}
-
-*-IsSemigroup : IsSemigroup _*_
-*-IsSemigroup = record { isMagma = *-IsMagma
-  ; assoc = *-Associative }
-
-*-IsMonoid : IsMonoid _*_ ∼
-*-IsMonoid = record
-   { isSemigroup = *-IsSemigroup
-   ; identity = *-Identity }
-
-+-*-IsSemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero _+_ _*_ ⁇ ∼
-+-*-IsSemiringWithoutAnnihilatingZero = record
-  { +-isCommutativeMonoid = +-IsCommutativeMonoid
-  ; *-isMonoid = *-IsMonoid
-  ; distrib = *-DistributesOver-+
-  }
-
-*-LeftZero : LeftZero ⁇ _*_
-*-LeftZero _ = refl
-
-*-RightZero : RightZero ⁇ _*_
-*-RightZero ⁇ = refl
-*-RightZero ≺ = refl
-*-RightZero ∼ = refl
-
-*-Zero : Zero ⁇ _*_
-*-Zero = *-LeftZero , *-RightZero
-
-+-*-IsSemiring : IsSemiring _+_ _*_ ⁇ ∼
-+-*-IsSemiring = record
-  { isSemiringWithoutAnnihilatingZero = +-*-IsSemiringWithoutAnnihilatingZero
-  ; zero = *-Zero }
-
-+-*-IsCommutativeSemiring : IsCommutativeSemiring _+_ _*_ ⁇ ∼
-+-*-IsCommutativeSemiring =
-  record { isSemiring = +-*-IsSemiring
-  ; *-comm = *-Commutative }
-
--- Proofs on ★
-open ★1
-
-★-condition-1 : (a : S) → ★ a ≡ ∼ + a * ★ a
-★-condition-1 ⁇ = refl
-★-condition-1 ≺ = refl
-★-condition-1 ∼ = refl
-
-★-condition-2 : (a : S) → ★ a ≡ ∼ + ★ a * a
-★-condition-2 ⁇ = refl
-★-condition-2 ≺ = refl
-★-condition-2 ∼ = refl
-
-+-*-★-IsStarSemiring : IsStarSemiring _+_ _*_ ★ ⁇ ∼
-+-*-★-IsStarSemiring = record
-   { isSemiring = +-*-IsSemiring
-   ; ★-cond-1 = ★-condition-1
-   ; ★-cond-2 = ★-condition-2 }

app/Commands/Extra.hs

@@ -1,12 +1,12 @@
 module Commands.Extra where
 
-import Options.Applicative
 import MiniJuvix.Prelude hiding (Doc)
+import Options.Applicative
 
 parseInputFile :: Parser FilePath
 parseInputFile =
- argument
-      str
-      ( metavar "MINIJUVIX_FILE"
-          <> help "Path to a .mjuvix file"
-      )
+  argument
+    str
+    ( metavar "MINIJUVIX_FILE"
+        <> help "Path to a .mjuvix file"
+    )

app/Commands/MicroJuvix.hs

@@ -1,9 +1,10 @@
 {-# LANGUAGE ApplicativeDo #-}
+
 module Commands.MicroJuvix where
 
 import Commands.Extra
-import Options.Applicative
 import MiniJuvix.Prelude hiding (Doc)
+import Options.Applicative
 
 newtype MicroJuvixOptions = MicroJuvixOptions
   { _mjuvixInputFile :: FilePath

app/Commands/MiniHaskell.hs

@@ -1,9 +1,10 @@
 {-# LANGUAGE ApplicativeDo #-}
+
 module Commands.MiniHaskell where
 
 import Commands.Extra
-import Options.Applicative
 import MiniJuvix.Prelude hiding (Doc)
+import Options.Applicative
 
 newtype MiniHaskellOptions = MiniHaskellOptions
   { _mhaskellInputFile :: FilePath

app/Commands/Termination.hs

@@ -1,15 +1,16 @@
 {-# LANGUAGE ApplicativeDo #-}
+
 module Commands.Termination where
 
 import Commands.Extra
-import qualified Data.Text as Text
 import Control.Monad.Extra
-import Options.Applicative
-import qualified MiniJuvix.Syntax.Abstract.Pretty.Base as A
+import qualified Data.Text as Text
 import MiniJuvix.Prelude hiding (Doc)
+import qualified MiniJuvix.Syntax.Abstract.Pretty.Base as A
+import Options.Applicative
 
-data TerminationCommand =
-  Calls CallsOptions
+data TerminationCommand
+  = Calls CallsOptions
   | CallGraph CallGraphOptions
 
 data CallsOptions = CallsOptions
@@ -33,14 +34,18 @@ parseCalls = do
           <> help "Show the unique number of each identifier"
       )
   _callsFunctionNameFilter <-
-    fmap msum . optional $ nonEmpty . Text.words <$> option str
-      ( long "function"
-          <> short 'f'
-          <> metavar "fun1 fun2 ..."
-          <> help "Only shows the specified functions"
-      )
+    fmap msum . optional $
+      nonEmpty . Text.words
+        <$> option
+          str
+          ( long "function"
+              <> short 'f'
+              <> metavar "fun1 fun2 ..."
+              <> help "Only shows the specified functions"
+          )
   _callsShowDecreasingArgs <-
-    option decrArgsParser
+    option
+      decrArgsParser
       ( long "show-decreasing-args"
           <> short 'd'
           <> value A.ArgRel
@@ -48,24 +53,26 @@ parseCalls = do
       )
   pure CallsOptions {..}
   where
-  decrArgsParser :: ReadM A.ShowDecrArgs
-  decrArgsParser = eitherReader $ \s ->
-    case map toLower s of
-      "argument" -> return A.OnlyArg
-      "relation" -> return A.OnlyRel
-      "both" -> return A.ArgRel
-      _ -> Left "bad argument"
-
+    decrArgsParser :: ReadM A.ShowDecrArgs
+    decrArgsParser = eitherReader $ \s ->
+      case map toLower s of
+        "argument" -> return A.OnlyArg
+        "relation" -> return A.OnlyRel
+        "both" -> return A.ArgRel
+        _ -> Left "bad argument"
 
 parseCallGraph :: Parser CallGraphOptions
 parseCallGraph = do
   _graphInputFile <- parseInputFile
   _graphFunctionNameFilter <-
-    fmap msum . optional $ nonEmpty . Text.words <$> option str
-      ( long "function"
-          <> short 'f'
-          <> help "Only shows the specified function"
-      )
+    fmap msum . optional $
+      nonEmpty . Text.words
+        <$> option
+          str
+          ( long "function"
+              <> short 'f'
+              <> help "Only shows the specified function"
+          )
   pure CallGraphOptions {..}
 
 parseTerminationCommand :: Parser TerminationCommand

app/Main.hs

@@ -1,30 +1,35 @@
 {-# LANGUAGE ApplicativeDo #-}
+
 module Main (main) where
 
+--------------------------------------------------------------------------------
+
+import Commands.Extra
+import Commands.MicroJuvix
+import Commands.MiniHaskell
+import Commands.Termination as T
 import Control.Monad.Extra
+import MiniJuvix.Prelude hiding (Doc)
+import qualified MiniJuvix.Syntax.Abstract.Pretty.Ansi as A
 import qualified MiniJuvix.Syntax.Concrete.Language as M
 import qualified MiniJuvix.Syntax.Concrete.Parser as M
 import qualified MiniJuvix.Syntax.Concrete.Scoped.Pretty.Ansi as M
-import qualified MiniJuvix.Syntax.MiniHaskell.Pretty.Ansi as H
+import MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base (defaultOptions)
+import qualified MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base as M
+import MiniJuvix.Syntax.Concrete.Scoped.Pretty.Html
+import qualified MiniJuvix.Syntax.Concrete.Scoped.Pretty.Text as T
+import qualified MiniJuvix.Syntax.Concrete.Scoped.Scoper as M
 import qualified MiniJuvix.Syntax.MicroJuvix.Pretty.Ansi as Micro
 import qualified MiniJuvix.Termination as T
-import qualified MiniJuvix.Translation.ScopedToAbstract as A
-import qualified MiniJuvix.Translation.AbstractToMicroJuvix as Micro
-import qualified MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base as M
 import qualified MiniJuvix.Termination.CallGraph as A
-import qualified MiniJuvix.Syntax.Abstract.Pretty.Base as A
-import qualified MiniJuvix.Syntax.Concrete.Scoped.Scoper as M
-import MiniJuvix.Prelude hiding (Doc)
+import qualified MiniJuvix.Translation.AbstractToMicroJuvix as Micro
+import qualified MiniJuvix.Translation.ScopedToAbstract as A
+import MiniJuvix.Utils.Version (runDisplayVersion)
 import Options.Applicative
 import Options.Applicative.Help.Pretty
 import Text.Show.Pretty hiding (Html)
-import MiniJuvix.Syntax.Concrete.Scoped.Pretty.Html
-import MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base (defaultOptions)
-import qualified MiniJuvix.Syntax.Abstract.Pretty.Ansi as A
-import Commands.Extra
-import Commands.Termination as T
-import Commands.MiniHaskell
-import Commands.MicroJuvix
+
+--------------------------------------------------------------------------------
 
 data Command
   = Scope ScopeOptions
@@ -33,12 +38,14 @@ data Command
   | Termination TerminationCommand
   | MiniHaskell MiniHaskellOptions
   | MicroJuvix MicroJuvixOptions
+  | DisplayVersion
 
 data ScopeOptions = ScopeOptions
   { _scopeRootDir :: FilePath,
     _scopeInputFiles :: [FilePath],
     _scopeShowIds :: Bool,
-    _scopeInlineImports :: Bool
+    _scopeInlineImports :: Bool,
+    _scopeNoColors :: Bool
   }
 
 data ParseOptions = ParseOptions
@@ -60,21 +67,22 @@ parseHtml = do
       ( long "recursive"
           <> help "export imported modules recursively"
       )
-  _htmlTheme <- option (eitherReader parseTheme)
+  _htmlTheme <-
+    option
+      (eitherReader parseTheme)
       ( long "theme"
           <> metavar "THEME"
-          <> value Nord
+          <> value Ayu
           <> showDefault
           <> help "selects a theme: ayu (light); nord (dark)"
       )
   pure HtmlOptions {..}
   where
-  parseTheme :: String -> Either String Theme
-  parseTheme s = case s of
-    "nord" -> Right Nord
-    "ayu" -> Right Ayu
-    _ -> Left $ "unrecognised theme: " <> s
-
+    parseTheme :: String -> Either String Theme
+    parseTheme s = case s of
+      "nord" -> Right Nord
+      "ayu" -> Right Ayu
+      _ -> Left $ "unrecognised theme: " <> s
 
 parseParse :: Parser ParseOptions
 parseParse = do
@@ -98,11 +106,12 @@ parseScope = do
           <> help "Root directory"
       )
   _scopeInputFiles <-
-    some $ argument
-      str
-      ( metavar "MINIJUVIX_FILE(s)"
-          <> help "Path to one ore more .mjuvix files"
-      )
+    some $
+      argument
+        str
+        ( metavar "MINIJUVIX_FILE(s)"
+            <> help "Path to one ore more MiniJuvix files"
+        )
   _scopeShowIds <-
     switch
       ( long "show-name-ids"
@@ -113,8 +122,19 @@ parseScope = do
       ( long "inline-imports"
           <> help "Show the code of imported modules next to the import statement"
       )
+  _scopeNoColors <-
+    switch
+      ( long "no-colors"
+          <> help "Disable ANSI formatting"
+      )
   pure ScopeOptions {..}
 
+parseDisplayVersion :: Parser Command
+parseDisplayVersion =
+  flag'
+    DisplayVersion
+    (long "version" <> short 'v' <> help "Print the version and exit")
+
 descr :: ParserInfo Command
 descr =
   info
@@ -127,20 +147,23 @@ descr =
   where
     headDoc :: Doc
     headDoc = dullblue $ bold $ underline "MiniJuvix help"
+
     foot :: Doc
-    foot = bold "maintainers: " <> "jan@heliax.dev; jonathan@heliax.dev"
+    foot = bold "maintainers: " <> "The MiniJuvix Team"
 
 parseCommand :: Parser Command
 parseCommand =
-  hsubparser $
-    mconcat
-      [ commandParse,
-        commandScope,
-        commandHtml,
-        commandTermination,
-        commandMicroJuvix,
-        commandMiniHaskell
-      ]
+  parseDisplayVersion
+    <|> ( hsubparser $
+            mconcat
+              [ commandParse,
+                commandScope,
+                commandHtml,
+                commandTermination,
+                commandMicroJuvix,
+                commandMiniHaskell
+              ]
+        )
   where
     commandMicroJuvix :: Mod CommandFields Command
     commandMicroJuvix = command "microjuvix" minfo
@@ -149,7 +172,7 @@ parseCommand =
         minfo =
           info
             (MicroJuvix <$> parseMicroJuvix)
-            (progDesc "Translate a .mjuvix file to MicroJuvix")
+            (progDesc "Translate a MiniJuvix file to MicroJuvix")
 
     commandMiniHaskell :: Mod CommandFields Command
     commandMiniHaskell = command "minihaskell" minfo
@@ -158,7 +181,7 @@ parseCommand =
         minfo =
           info
             (MiniHaskell <$> parseMiniHaskell)
-            (progDesc "Translate a .mjuvix file to MiniHaskell")
+            (progDesc "Translate a MiniJuvix file to MiniHaskell")
 
     commandParse :: Mod CommandFields Command
     commandParse = command "parse" minfo
@@ -167,7 +190,7 @@ parseCommand =
         minfo =
           info
             (Parse <$> parseParse)
-            (progDesc "Parse a .mjuvix file")
+            (progDesc "Parse a MiniJuvix file")
 
     commandHtml :: Mod CommandFields Command
     commandHtml = command "html" minfo
@@ -176,7 +199,8 @@ parseCommand =
         minfo =
           info
             (Html <$> parseHtml)
-            (progDesc "Generate html for a .mjuvix file")
+            (progDesc "Generate HTML for a MiniJuvix file")
+
     commandScope :: Mod CommandFields Command
     commandScope = command "scope" minfo
       where
@@ -184,7 +208,8 @@ parseCommand =
         minfo =
           info
             (Scope <$> parseScope)
-            (progDesc "Parse and scope a .mjuvix file")
+            (progDesc "Parse and scope a MiniJuvix file")
+
     commandTermination :: Mod CommandFields Command
     commandTermination = command "termination" minfo
       where
@@ -194,7 +219,6 @@ parseCommand =
             (Termination <$> parseTerminationCommand)
             (progDesc "Subcommands related to termination checking")
 
-
 mkScopePrettyOptions :: ScopeOptions -> M.Options
 mkScopePrettyOptions ScopeOptions {..} =
   M.defaultOptions
@@ -205,50 +229,48 @@ mkScopePrettyOptions ScopeOptions {..} =
 parseModuleIO :: FilePath -> IO (M.Module 'M.Parsed 'M.ModuleTop)
 parseModuleIO = fromRightIO id . M.runModuleParserIO
 
-fromRightIO' :: (e -> IO ()) -> IO (Either e r) -> IO r
-fromRightIO' pp = do
-  eitherM ifLeft return
-  where
-  ifLeft e = pp e >> exitFailure
-
-fromRightIO :: (e -> Text) -> IO (Either e r) -> IO r
-fromRightIO pp = fromRightIO' (putStrLn . pp)
-
 go :: Command -> IO ()
 go c = do
   root <- getCurrentDirectory
   case c of
+    DisplayVersion -> runDisplayVersion
     Scope opts@ScopeOptions {..} -> do
       forM_ _scopeInputFiles $ \scopeInputFile -> do
         m <- parseModuleIO scopeInputFile
-        s <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m
-        M.printPrettyCode (mkScopePrettyOptions opts) s
+        (_ , s) <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m
+        printer (mkScopePrettyOptions opts) s
+      where
+        printer :: M.Options -> M.Module 'M.Scoped 'M.ModuleTop -> IO ()
+        printer
+          | not _scopeNoColors = M.printPrettyCode
+          | otherwise = T.printPrettyCode
     Parse ParseOptions {..} -> do
       m <- parseModuleIO _parseInputFile
       if _parseNoPrettyShow then print m else pPrint m
     Html HtmlOptions {..} -> do
       m <- parseModuleIO _htmlInputFile
-      s <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m
+      (_ , s) <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m
       genHtml defaultOptions _htmlRecursive _htmlTheme s
     MicroJuvix MicroJuvixOptions {..} -> do
       m <- parseModuleIO _mjuvixInputFile
-      s <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m
+      (_, s) <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m
       a <- fromRightIO' putStrLn (return $ A.translateModule s)
       let mini = Micro.translateModule a
       Micro.printPrettyCodeDefault mini
     MiniHaskell MiniHaskellOptions {..} -> do
       m <- parseModuleIO _mhaskellInputFile
-      s <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m
-      a <- fromRightIO' putStrLn (return $ A.translateModule s)
+      (_ , s) <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m
+      -- a <- fromRightIO' putStrLn (return $ A.translateModule s)
+      _ <- fromRightIO' putStrLn (return $ A.translateModule s)
       -- let mini = Micro.translateModule a
       -- Micro.printPrettyCodeDefault mini
       -- TODO
       error "todo"
     Termination (Calls opts@CallsOptions {..}) -> do
       m <- parseModuleIO _callsInputFile
-      s <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m
+      (_ , s) <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m
       a <- fromRightIO' putStrLn (return $ A.translateModule s)
-      let callMap0 =  T.buildCallMap a
+      let callMap0 = T.buildCallMap a
           callMap = case _callsFunctionNameFilter of
             Nothing -> callMap0
             Just f -> T.filterCallMap f callMap0
@@ -257,7 +279,7 @@ go c = do
       putStrLn ""
     Termination (CallGraph CallGraphOptions {..}) -> do
       m <- parseModuleIO _graphInputFile
-      s <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m
+      (_ , s) <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m
       a <- fromRightIO' putStrLn (return $ A.translateModule s)
       let callMap = T.buildCallMap a
           opts' = A.defaultOptions

lab/Syntax/Core.hs

@@ -6,9 +6,9 @@ module MiniJuvix.Syntax.Core where
 
 --------------------------------------------------------------------------------
 
+-- import Algebra.Graph.Label (Semiring (..))
 import MiniJuvix.Prelude hiding (Local)
 import Numeric.Natural (Natural)
-import Algebra.Graph.Label (Semiring(..))
 
 --------------------------------------------------------------------------------
 -- Quantity (a.k.a. Usage)

lab/Syntax/Eval.hs

@@ -2,8 +2,8 @@
 
 module MiniJuvix.Syntax.Eval where
 
-import MiniJuvix.Syntax.Core
 import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Core
 
 --------------------------------------------------------------------------------
 -- Values and neutral terms

lab/Syntax/Makefile

@@ -0,0 +1,86 @@
+PWD=$(CURDIR)
+PREFIX="$(PWD)/.stack-work/prefix"
+UNAME := $(shell uname)
+
+AGDA_FILES := $(wildcard ./*.agda)
+GEN_HS := $(patsubst %.agda, %.hs, $(AGDA_FILES))
+
+ifeq ($(UNAME), Darwin)
+	THREADS := $(shell sysctl -n hw.logicalcpu)
+else ifeq ($(UNAME), Linux)
+	THREADS := $(shell nproc)
+else
+	THREADS := $(shell echo %NUMBER_OF_PROCESSORS%)
+endif
+
+all:
+	make prepare-push
+
+.PHONY : checklines
+checklines :
+	@grep '.\{81,\}' \
+		--exclude=*.agda \
+		-l --recursive src; \
+		status=$$?; \
+		if [ $$status = 0 ] ; \
+		then echo "Lines were found with more than 80 characters!" >&2 ; \
+		else echo "Succeed!"; \
+		fi
+
+.PHONY : hlint
+hlint :
+	hlint src
+
+.PHONY : haddock
+haddock :
+	cabal --docdir=docs/ --htmldir=docs/ haddock --enable-documentation
+
+.PHONY : docs
+docs :
+	cd docs ; \
+	sh conv.sh
+
+.PHONY : cabal
+cabal :
+	cabal build all
+
+.PHONY : stan
+stan :
+	stan check --include --filter-all --directory=src
+
+setup:
+	stack build --only-dependencies --jobs $(THREADS)
+
+.PHONY : build
+build:
+	stack build --fast --jobs $(THREADS)
+
+clean:
+	cabal clean
+	stack clean
+
+clean-full:
+	stack clean --full
+
+.PHONY: install-agda
+install-agda:
+	git clone https://github.com/agda/agda.git
+	cd agda
+	cabal update
+	cabal install --overwrite-policy=always --ghc-options='-O2 +RTS -M6G -RTS' alex-3.2.6
+	cabal install --overwrite-policy=always --ghc-options='-O2 +RTS -M6G -RTS' happy-1.19.12
+	pwd
+	cabal install --overwrite-policy=always --ghc-options='-O2 +RTS -M6G -RTS' -foptimise-heavily
+
+.PHONY : install-agda2hs
+install-agda2hs:
+	git clone https://github.com/agda/agda2hs.git
+	cd agda2hs &&	cabal new-install --overwrite-policy=always
+	mkdir -p .agda/
+	touch .agda/libraries
+	echo "agda2hs/agda2hs.agda-lib" > ~/.agda/libraries
+
+.PHONY : agda
+agda :
+	agda2hs ./Core.agda -o src -XUnicodeSyntax -XStandaloneDeriving -XDerivingStrategies -XMultiParamTypeClasses
+	agda2hs ./Eval.agda -o src -XUnicodeSyntax -XStandaloneDeriving -XDerivingStrategies -XMultiParamTypeClasses

lab/Termination/CallGraphOld.hs

@@ -0,0 +1,210 @@
+module MiniJuvix.Termination.CallGraphOld
+  ( module MiniJuvix.Termination.Types,
+    module MiniJuvix.Termination.CallGraphOld,
+  )
+where
+
+import qualified Data.HashMap.Strict as HashMap
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Abstract.Language.Extra
+import MiniJuvix.Syntax.Abstract.Pretty.Base
+import MiniJuvix.Termination.Types
+import Prettyprinter as PP
+
+type Edges = HashMap (FunctionName, FunctionName) Edge
+
+data Edge = Edge
+  { _edgeFrom :: FunctionName,
+    _edgeTo :: FunctionName,
+    _edgeMatrices :: [CallMatrix]
+  }
+
+newtype CompleteCallGraph = CompleteCallGraph Edges
+
+data ReflexiveEdge = ReflexiveEdge
+  { _redgeFun :: FunctionName,
+    _redgeMatrices :: [CallMatrix]
+  }
+
+data RecursiveBehaviour = RecursiveBehaviour
+  { _recBehaviourFunction :: FunctionName,
+    _recBehaviourMatrix :: [[Rel]]
+  }
+
+makeLenses ''RecursiveBehaviour
+makeLenses ''Edge
+makeLenses ''ReflexiveEdge
+
+multiply :: CallMatrix -> CallMatrix -> CallMatrix
+multiply a b = map sumProdRow a
+  where
+    rowB :: Int -> CallRow
+    rowB i = CallRow $ case b !? i of
+      Just (CallRow (Just c)) -> Just c
+      _ -> Nothing
+    sumProdRow :: CallRow -> CallRow
+    sumProdRow (CallRow mr) = CallRow $ do
+      (ki, ra) <- mr
+      (j, rb) <- _callRow (rowB ki)
+      return (j, mul' ra rb)
+
+multiplyMany :: [CallMatrix] -> [CallMatrix] -> [CallMatrix]
+multiplyMany r s = [multiply a b | a <- r, b <- s]
+
+composeEdge :: Edge -> Edge -> Maybe Edge
+composeEdge a b = do
+  guard (a ^. edgeTo == b ^. edgeFrom)
+  return
+    Edge
+      { _edgeFrom = a ^. edgeFrom,
+        _edgeTo = b ^. edgeTo,
+        _edgeMatrices = multiplyMany (a ^. edgeMatrices) (b ^. edgeMatrices)
+      }
+
+fromFunCall :: FunctionName -> FunCall -> Call
+fromFunCall caller fc =
+  Call
+    { _callFrom = caller,
+      _callTo = fc ^. callName,
+      _callMatrix = map fst (fc ^. callArgs)
+    }
+
+completeCallGraph :: CallMap -> CompleteCallGraph
+completeCallGraph cm = CompleteCallGraph (go startingEdges)
+  where
+    startingEdges :: Edges
+    startingEdges = foldr insertCall mempty allCalls
+      where
+        insertCall :: Call -> Edges -> Edges
+        insertCall Call {..} = HashMap.alter (Just . aux) (_callFrom, _callTo)
+          where
+            aux :: Maybe Edge -> Edge
+            aux me = case me of
+              Nothing -> Edge _callFrom _callTo [_callMatrix]
+              Just e -> over edgeMatrices (_callMatrix :) e
+    allCalls :: [Call]
+    allCalls =
+      [ fromFunCall caller funCall
+        | (caller, callerMap) <- HashMap.toList (cm ^. callMap),
+          (_, funCalls) <- HashMap.toList callerMap,
+          funCall <- funCalls
+      ]
+
+    go :: Edges -> Edges
+    go m
+      | edgesCount m == edgesCount m' = m
+      | otherwise = go m'
+      where
+        m' = step m
+
+    step :: Edges -> Edges
+    step s = edgesUnion (edgesCompose s startingEdges) s
+
+    fromEdgeList :: [Edge] -> Edges
+    fromEdgeList l = HashMap.fromList [((e ^. edgeFrom, e ^. edgeTo), e) | e <- l]
+
+    edgesCompose :: Edges -> Edges -> Edges
+    edgesCompose a b =
+      fromEdgeList $
+        catMaybes
+          [composeEdge ea eb | ea <- toList a, eb <- toList b]
+    edgesUnion :: Edges -> Edges -> Edges
+    edgesUnion = HashMap.union
+    edgesCount :: Edges -> Int
+    edgesCount = HashMap.size
+
+reflexiveEdges :: CompleteCallGraph -> [ReflexiveEdge]
+reflexiveEdges (CompleteCallGraph es) = mapMaybe reflexive (toList es)
+  where
+    reflexive :: Edge -> Maybe ReflexiveEdge
+    reflexive e
+      | e ^. edgeFrom == e ^. edgeTo =
+        Just $ ReflexiveEdge (e ^. edgeFrom) (e ^. edgeMatrices)
+      | otherwise = Nothing
+
+callMatrixDiag :: CallMatrix -> [Rel]
+callMatrixDiag m = [col i r | (i, r) <- zip [0 :: Int ..] m]
+  where
+    col :: Int -> CallRow -> Rel
+    col i (CallRow row) = case row of
+      Nothing -> RNothing
+      Just (j, r')
+        | i == j -> RJust r'
+        | otherwise -> RNothing
+
+recursiveBehaviour :: ReflexiveEdge -> RecursiveBehaviour
+recursiveBehaviour re =
+  RecursiveBehaviour
+    (re ^. redgeFun)
+    (map callMatrixDiag (re ^. redgeMatrices))
+
+findOrder :: RecursiveBehaviour -> Maybe LexOrder
+findOrder rb = LexOrder <$> listToMaybe (mapMaybe (isLexOrder >=> nonEmpty) allPerms)
+  where
+    b0 :: [[Rel]]
+    b0 = rb ^. recBehaviourMatrix
+    indexed = map (zip [0 :: Int ..] . take minLength) b0
+      where
+        minLength = minimum (map length b0)
+
+    startB = removeUselessColumns indexed
+
+    -- removes columns that don't have at least one ≺ in them
+    removeUselessColumns :: [[(Int, Rel)]] -> [[(Int, Rel)]]
+    removeUselessColumns = transpose . filter (any (isLess . snd)) . transpose
+
+    isLexOrder :: [Int] -> Maybe [Int]
+    isLexOrder = go startB
+      where
+        go :: [[(Int, Rel)]] -> [Int] -> Maybe [Int]
+        go [] _ = Just []
+        go b perm = case perm of
+          [] -> error "The permutation should have one element at least!"
+          (p0 : ptail)
+            | Just r <- find (isLess . snd . (!! p0)) b,
+              all (notNothing . snd . (!! p0)) b,
+              Just perm' <- go (b' p0) (map pred ptail) ->
+              Just (fst (r !! p0) : perm')
+            | otherwise -> Nothing
+          where
+            b' i = map r' (filter (not . isLess . snd . (!! i)) b)
+              where
+                r' r = case splitAt i r of
+                  (x, y) -> x ++ drop 1 y
+
+    notNothing = (RNothing /=)
+    isLess = (RJust RLe ==)
+
+    allPerms :: [[Int]]
+    allPerms = case nonEmpty startB of
+      Nothing -> []
+      Just s -> permutations [0 .. length (head s) - 1]
+
+instance PrettyCode Edge where
+  ppCode Edge {..} = do
+    fromFun <- ppSCode _edgeFrom
+    toFun <- ppSCode _edgeTo
+    matrices <- indent 2 . ppMatrices . zip [0 :: Int ..] <$> mapM ppCode _edgeMatrices
+    return $
+      pretty ("Edge" :: Text) <+> fromFun <+> waveFun <+> toFun <> line
+        <> matrices
+    where
+      ppMatrices = vsep2 . map ppMatrix
+      ppMatrix (i, t) =
+        pretty ("Matrix" :: Text) <+> pretty i <> colon <> line
+          <> t
+
+instance PrettyCode CompleteCallGraph where
+  ppCode :: forall r. Members '[Reader Options] r => CompleteCallGraph -> Sem r (Doc Ann)
+  ppCode (CompleteCallGraph edges) = do
+    es <- vsep2 <$> mapM ppCode (toList edges)
+    return $ pretty ("Complete Call Graph:" :: Text) <> line <> es
+
+instance PrettyCode RecursiveBehaviour where
+  ppCode :: forall r. Members '[Reader Options] r => RecursiveBehaviour -> Sem r (Doc Ann)
+  ppCode (RecursiveBehaviour f m) = do
+    f' <- ppSCode f
+    let m' = vsep (map (PP.list . map pretty) m)
+    return $
+      pretty ("Recursive behaviour of " :: Text) <> f' <> colon <> line
+        <> indent 2 (align m')

package.yaml

@@ -1,34 +1,35 @@
 name:            minijuvix
-version:         0.0.0.0
+version:         0.1.0
 license:         GPL-3.0-only
 license-file:    LICENSE
-copyright:       (c) 2021-2022 Heliax AG.
+copyright:       (c) 2022- Heliax AG.
 maintainer:      The PLT Team at Heliax AG <hello@heliax.dev>
-author:          [ Jonathan Prieto-Cubides , Jan Mas Rovira ]
-tested-with:     ghc == 9.0.2
-homepage:        https://github.com/heliaxdev/MiniJuvix
-bug-reports:     https://github.com/heliaxdev/MiniJuvix/issues
-description:     A tiny dependent typed programming language for experimentation.
+author:          [ Jonathan Prieto-Cubides , Jan Mas Rovira , Paul Cadman ]
+tested-with:     ghc == 9.2.2
+homepage:        https://github.com/heliaxdev/minijuvix
+bug-reports:     https://github.com/heliaxdev/minijuvix/issues
+description:     The MiniJuvix compiler
 category:        Compilers/Interpreters
-github:          heliaxdev/MiniJuvix
+github:          heliaxdev/minijuvix
 
 extra-source-files:
 - README.md
 - CHANGELOG.md
 
+# TODO: make sections for dependency
 dependencies:
 - aeson == 2.0.*
-- algebraic-graphs == 0.6.*
-- base == 4.15.*
+- base == 4.16.*
 - blaze-html == 0.9.*
 - blaze-markup == 0.8.*
-- bytestring == 0.10.*
+- bytestring == 0.11.*
 - containers == 0.6.*
 - directory == 1.3.*
 - edit-distance == 0.2.*
 - extra == 1.7.*
 - filepath == 1.4.*
-- hashable == 1.3.*
+- gitrev == 1.3.*
+- hashable == 1.4.*
 - megaparsec == 9.2.*
 - microlens-platform == 0.4.*
 - parser-combinators == 1.3.*
@@ -39,9 +40,9 @@ dependencies:
 - process == 1.6.*
 - semirings == 0.6.*
 - singletons == 3.0.*
-- singletons-th == 3.0.*
+- singletons-th == 3.1.*
 - Stream == 0.4.*
-- template-haskell == 2.17.*
+- template-haskell == 2.18.*
 - text == 1.2.*
 - th-utilities == 0.2.*
 - unordered-containers == 0.2.*
@@ -50,7 +51,10 @@ dependencies:
 # when running the tests. Is there a better solution?
 - tasty
 - tasty-hunit
+- Diff == 0.4.*
+- pretty-show == 1.10.*
 
+# TODO organize this
 ghc-options:
 - -fhide-source-paths
 - -O2 -flate-specialise -fspecialise-aggressively
@@ -62,33 +66,24 @@ ghc-options:
 
 default-extensions:
 - DataKinds
-- DeriveFoldable
-- DeriveGeneric
-- DeriveLift
-- DeriveTraversable
 - DerivingStrategies
-- FlexibleContexts
-- FlexibleInstances
 - GADTs
-- GeneralizedNewtypeDeriving
-- InstanceSigs
-- KindSignatures
 - LambdaCase
 - NoImplicitPrelude
 - OverloadedStrings
-- PolyKinds
 - QuasiQuotes
 - RecordWildCards
-- ScopedTypeVariables
-- StandaloneDeriving
 - TemplateHaskell
-- TypeApplications
 - TypeFamilyDependencies
-- TypeOperators
 - UnicodeSyntax
 
+# verbatim:
+#   default-language: GHC2021
+
 library:
   source-dirs: src
+  verbatim:
+    default-language: GHC2021
 
 executables:
   minijuvix:
@@ -96,8 +91,9 @@ executables:
     source-dirs: app
     dependencies:
     - minijuvix
-    - optparse-applicative == 0.16.*
-    - pretty-show == 1.10.*
+    - optparse-applicative == 0.17.*
+    verbatim:
+      default-language: GHC2021
 
 tests:
   minijuvix-test:
@@ -105,3 +101,5 @@ tests:
     source-dirs:         test
     dependencies:
     - minijuvix
+    verbatim:
+      default-language: GHC2021

src/MiniJuvix/Internal/Strings.hs

@@ -26,6 +26,18 @@ in_ = "in"
 inductive :: IsString s => s
 inductive = "inductive"
 
+function :: IsString s => s
+function = "function"
+
+constructor :: IsString s => s
+constructor = "constructor"
+
+topModule :: IsString s => s
+topModule = "top module"
+
+localModule :: IsString s => s
+localModule = "local module"
+
 infix_ :: IsString s => s
 infix_ = "infix"
 
@@ -127,3 +139,6 @@ colonZero = ":0"
 
 ghc :: IsString s => s
 ghc = "ghc"
+
+agda :: IsString s => s
+agda = "agda"

src/MiniJuvix/Prelude.hs

@@ -1,7 +1,8 @@
-module MiniJuvix.Prelude (
-  module MiniJuvix.Prelude.Base,
-  module MiniJuvix.Prelude.Error
-  ) where
+module MiniJuvix.Prelude
+  ( module MiniJuvix.Prelude.Base,
+    module MiniJuvix.Prelude.Error,
+  )
+where
 
 import MiniJuvix.Prelude.Base
 import MiniJuvix.Prelude.Error

src/MiniJuvix/Prelude/Base.hs

@@ -1,51 +1,53 @@
 module MiniJuvix.Prelude.Base
   ( module MiniJuvix.Prelude.Base,
+    module Control.Applicative,
     module Control.Monad.Extra,
-    module Data.Char,
-    module Data.Typeable,
-    module Data.Either.Extra,
-    module Data.Function,
-    module Data.List.Extra,
-    module Data.Maybe,
-    module Data.String,
-    module Data.Text.Encoding,
-    module GHC.Real,
-    module Data.Tuple.Extra,
-    module Data.Void,
-    module GHC.Enum,
-    module System.Directory,
-    module Prettyprinter,
-    module System.FilePath,
-    module Data.Singletons,
-    module Data.Singletons.TH,
-    module Data.Singletons.Sigma,
-    module Data.Hashable,
-    module Lens.Micro.Platform,
-    module GHC.Generics,
+    module Control.Monad.Fix,
     module Data.Bool,
-    module Data.List.NonEmpty.Extra,
-    module Data.Traversable,
-    module Data.Monoid,
-    module Polysemy,
-    module Polysemy.Reader,
-    module Data.Text.IO,
-    module Polysemy.State,
-    module Polysemy.Error,
-    module Polysemy.Embed,
-    module Text.Show,
+    module Data.Char,
+    module Data.Either.Extra,
     module Data.Eq,
+    module Data.Foldable,
+    module Data.Function,
+    module Data.Functor,
+    module Data.Hashable,
+    module Data.Int,
+    module Data.List.Extra,
+    module Data.List.NonEmpty.Extra,
+    module Data.Maybe,
+    module Data.Monoid,
     module Data.Ord,
     module Data.Semigroup,
+    module Data.Singletons,
+    module Data.Singletons.Sigma,
+    module Data.Singletons.TH,
     module Data.Stream,
-    module GHC.Num,
+    module Data.String,
+    module Data.Text.Encoding,
+    module Data.Text.IO,
+    module Data.Traversable,
+    module Data.Tuple.Extra,
+    module Data.Typeable,
+    module Data.Void,
     module Data.Word,
-    module Data.Functor,
-    module Data.Int,
+    module GHC.Enum,
+    module GHC.Generics,
+    module GHC.Num,
+    module GHC.Real,
+    module Lens.Micro.Platform,
+    module Polysemy,
+    module Polysemy.Embed,
+    module Polysemy.Error,
+    module Polysemy.Fixpoint,
+    module Polysemy.Reader,
+    module Polysemy.State,
     module Polysemy.View,
+    module Prettyprinter,
+    module System.Directory,
     module System.Exit,
+    module System.FilePath,
     module System.IO,
-    module Control.Applicative,
-    module Data.Foldable,
+    module Text.Show,
     Data,
     Text,
     pack,
@@ -62,8 +64,8 @@ where
 --------------------------------------------------------------------------------
 
 import Control.Applicative
-import Data.Typeable hiding (TyCon)
 import Control.Monad.Extra
+import Control.Monad.Fix
 import Data.Bool
 import Data.ByteString.Lazy (ByteString)
 import Data.Char
@@ -74,27 +76,28 @@ import Data.Eq
 import Data.Foldable hiding (minimum, minimumBy)
 import Data.Function
 import Data.Functor
-import Prettyprinter (Doc, (<+>))
 import Data.HashMap.Strict (HashMap)
 import Data.HashSet (HashSet)
 import Data.Hashable
 import Data.Int
 import Data.List.Extra hiding (head, last)
-import Data.List.NonEmpty.Extra (NonEmpty (..), head, last, nonEmpty, minimum1, minimumOn1, maximum1, maximumOn1, some1)
 import qualified Data.List.NonEmpty as NonEmpty
+import Data.List.NonEmpty.Extra (NonEmpty (..), head, last, maximum1, maximumOn1, minimum1, minimumOn1, nonEmpty, some1)
 import Data.Maybe
-import Data.Singletons.Sigma
 import Data.Monoid
 import Data.Ord
 import Data.Semigroup (Semigroup, (<>))
 import Data.Singletons
+import Data.Singletons.Sigma
 import Data.Singletons.TH (genSingletons)
 import Data.Stream (Stream)
 import Data.String
 import Data.Text (Text, pack, strip, unpack)
 import Data.Text.Encoding
+import Data.Text.IO
 import Data.Traversable
 import Data.Tuple.Extra
+import Data.Typeable hiding (TyCon)
 import Data.Void
 import Data.Word
 import GHC.Enum
@@ -107,15 +110,16 @@ import Lens.Micro.Platform hiding (both)
 import Polysemy
 import Polysemy.Embed
 import Polysemy.Error hiding (fromEither)
+import Polysemy.Fixpoint
 import Polysemy.Reader
 import Polysemy.State
 import Polysemy.View
+import Prettyprinter (Doc, (<+>))
 import System.Directory
 import System.Exit
 import System.FilePath
-import System.IO hiding (putStr, putStrLn, hPutStr, hPutStrLn, writeFile, hGetContents, interact, readFile, getContents, getLine, appendFile, hGetLine, readFile')
+import System.IO hiding (appendFile, getContents, getLine, hGetContents, hGetLine, hPutStr, hPutStrLn, interact, putStr, putStrLn, readFile, readFile', writeFile)
 import Text.Show (Show)
-import Data.Text.IO
 import qualified Text.Show as Show
 
 --------------------------------------------------------------------------------
@@ -209,16 +213,18 @@ impossible = Err.error "impossible"
 --------------------------------------------------------------------------------
 
 infixl 7 <+?>
+
 (<+?>) :: Doc ann -> Maybe (Doc ann) -> Doc ann
 (<+?>) a = maybe a (a <+>)
 
 infixl 7 <?>
+
 (<?>) :: Semigroup m => m -> Maybe m -> m
 (<?>) a = maybe a (a <>)
 
-data Indexed a = Indexed {
-  _indexedIx :: Int,
-  _indexedThing :: a
+data Indexed a = Indexed
+  { _indexedIx :: Int,
+    _indexedThing :: a
   }
   deriving stock (Show, Eq, Ord, Foldable, Traversable)
 
@@ -226,3 +232,18 @@ instance Functor Indexed where
   fmap f (Indexed i a) = Indexed i (f a)
 
 makeLenses ''Indexed
+
+minimumMaybe :: (Foldable t, Ord a) => t a -> Maybe a
+minimumMaybe l = if null l then Nothing else Just (minimum l)
+
+fromText :: IsString a => Text -> a
+fromText = fromString . unpack
+
+fromRightIO' :: (e -> IO ()) -> IO (Either e r) -> IO r
+fromRightIO' pp = do
+  eitherM ifLeft return
+  where
+    ifLeft e = pp e >> exitFailure
+
+fromRightIO :: (e -> Text) -> IO (Either e r) -> IO r
+fromRightIO pp = fromRightIO' (putStrLn . pp)

src/MiniJuvix/Prelude/Error.hs

@@ -9,20 +9,20 @@ data AJuvixError = forall e. JuvixError e => AJuvixError e
 
 -- | Minimal interface of an minijuvix error.
 class Typeable e => JuvixError e where
-   -- | Print the to stderr with Ansi formatting.
-   printErrorAnsi :: e -> IO ()
-   printErrorAnsi = hPutStrLn stderr . renderAnsiText
+  -- | Print the to stderr with Ansi formatting.
+  printErrorAnsi :: e -> IO ()
+  printErrorAnsi = hPutStrLn stderr . renderAnsiText
 
-   -- | Print the to stderr without formatting.
-   printErrorText :: e -> IO ()
-   printErrorText = hPutStrLn stderr . renderText
+  -- | Print the to stderr without formatting.
+  printErrorText :: e -> IO ()
+  printErrorText = hPutStrLn stderr . renderText
 
-   -- | Render the error to Text.
-   renderText :: e -> Text
+  -- | Render the error to Text.
+  renderText :: e -> Text
 
-   -- | Render the error with Ansi formatting (if any).
-   renderAnsiText :: e -> Text
-   renderAnsiText = renderText
+  -- | Render the error with Ansi formatting (if any).
+  renderAnsiText :: e -> Text
+  renderAnsiText = renderText
 
 toAJuvixError :: JuvixError e => e -> AJuvixError
 toAJuvixError = AJuvixError

src/MiniJuvix/Syntax/Abstract/Language.hs

@@ -1,11 +1,11 @@
 module MiniJuvix.Syntax.Abstract.Language
   ( module MiniJuvix.Syntax.Abstract.Language,
-    module MiniJuvix.Syntax.Concrete.Language
+    module MiniJuvix.Syntax.Concrete.Language,
   )
 where
 
 import MiniJuvix.Prelude
-import MiniJuvix.Syntax.Concrete.Language (Usage, Literal(..), ForeignBlock(..))
+import MiniJuvix.Syntax.Concrete.Language (ForeignBlock (..), Literal (..), Usage, BackendItem)
 import qualified MiniJuvix.Syntax.Concrete.Name as C
 import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
 import MiniJuvix.Syntax.Fixity
@@ -41,7 +41,7 @@ data ModuleBody = ModuleBody
   { _moduleInductives :: HashMap InductiveName (Indexed InductiveDef),
     _moduleFunctions :: HashMap FunctionName (Indexed FunctionDef),
     _moduleImports :: [Indexed TopModule],
-    _moduleForeign :: [Indexed ForeignBlock],
+    _moduleForeigns :: [Indexed ForeignBlock],
     _moduleLocalModules :: HashMap LocalModuleName (Indexed LocalModule)
   }
   deriving stock (Show, Eq)
@@ -60,7 +60,7 @@ data FunctionClause = FunctionClause
   deriving stock (Show, Eq)
 
 data Iden
-  = IdenDefined Name
+  = IdenFunction Name
   | IdenConstructor Name
   | IdenVar VarName
   | IdenInductive Name
@@ -162,7 +162,8 @@ data InductiveConstructorDef = InductiveConstructorDef
 
 data AxiomDef = AxiomDef
   { _axiomName :: AxiomName,
-    _axiomType :: Expression
+    _axiomType :: Expression,
+    _axiomBackendItems :: [BackendItem]
   }
   deriving stock (Show, Eq)
 

src/MiniJuvix/Syntax/Abstract/Language/Extra.hs

@@ -1,10 +1,11 @@
-module MiniJuvix.Syntax.Abstract.Language.Extra (
-  module MiniJuvix.Syntax.Abstract.Language,
-  module MiniJuvix.Syntax.Abstract.Language.Extra
-                                       ) where
+module MiniJuvix.Syntax.Abstract.Language.Extra
+  ( module MiniJuvix.Syntax.Abstract.Language,
+    module MiniJuvix.Syntax.Abstract.Language.Extra,
+  )
+where
 
-import MiniJuvix.Syntax.Abstract.Language
 import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Abstract.Language
 
 smallerPatternVariables :: Pattern -> [VarName]
 smallerPatternVariables p = case p of
@@ -13,15 +14,15 @@ smallerPatternVariables p = case p of
   PatternEmpty {} -> []
   PatternConstructorApp app -> appVariables app
   where
-  appVariables :: ConstructorApp -> [VarName]
-  appVariables (ConstructorApp _ ps) = concatMap patternVariables ps
+    appVariables :: ConstructorApp -> [VarName]
+    appVariables (ConstructorApp _ ps) = concatMap patternVariables ps
 
-  patternVariables :: Pattern -> [VarName]
-  patternVariables pat = case pat of
-    PatternVariable v -> [v]
-    PatternWildcard {} -> []
-    PatternEmpty {} -> []
-    PatternConstructorApp app -> appVariables app
+    patternVariables :: Pattern -> [VarName]
+    patternVariables pat = case pat of
+      PatternVariable v -> [v]
+      PatternWildcard {} -> []
+      PatternEmpty {} -> []
+      PatternConstructorApp app -> appVariables app
 
 viewApp :: Expression -> (Expression, [Expression])
 viewApp e = case e of
@@ -35,18 +36,18 @@ viewApp e = case e of
 viewExpressionAsPattern :: Expression -> Maybe Pattern
 viewExpressionAsPattern e = case viewApp e of
   (f, args)
-   | Just c <- getConstructor f -> do
-        args' <- mapM viewExpressionAsPattern args
-        Just $ PatternConstructorApp (ConstructorApp c args')
+    | Just c <- getConstructor f -> do
+      args' <- mapM viewExpressionAsPattern args
+      Just $ PatternConstructorApp (ConstructorApp c args')
   (f, [])
-   | Just v <- getVariable f -> Just (PatternVariable v)
+    | Just v <- getVariable f -> Just (PatternVariable v)
   _ -> Nothing
   where
-  getConstructor :: Expression -> Maybe Name
-  getConstructor f = case f of
-    ExpressionIden (IdenConstructor n) -> Just n
-    _ -> Nothing
-  getVariable :: Expression -> Maybe VarName
-  getVariable f = case f of
-    ExpressionIden (IdenVar n) -> Just n
-    _ -> Nothing
+    getConstructor :: Expression -> Maybe Name
+    getConstructor f = case f of
+      ExpressionIden (IdenConstructor n) -> Just n
+      _ -> Nothing
+    getVariable :: Expression -> Maybe VarName
+    getVariable f = case f of
+      ExpressionIden (IdenVar n) -> Just n
+      _ -> Nothing

src/MiniJuvix/Syntax/Abstract/Pretty/Ann.hs

@@ -1,12 +1,11 @@
 module MiniJuvix.Syntax.Abstract.Pretty.Ann where
 
-
+import MiniJuvix.Prelude
 import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
 import qualified MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base as S
-import MiniJuvix.Prelude
 
-data Ann =
-  AnnKind S.NameKind
+data Ann
+  = AnnKind S.NameKind
   | AnnKeyword
   | AnnImportant
   | AnnLiteralString

src/MiniJuvix/Syntax/Abstract/Pretty/Ansi.hs

@@ -1,11 +1,12 @@
-module MiniJuvix.Syntax.Abstract.Pretty.Ansi (
-module MiniJuvix.Syntax.Abstract.Pretty.Base,
 module MiniJuvix.Syntax.Abstract.Pretty.Ansi
-                                             ) where
+  ( module MiniJuvix.Syntax.Abstract.Pretty.Base,
+    module MiniJuvix.Syntax.Abstract.Pretty.Ansi,
+  )
+where
 
-import MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind
-import MiniJuvix.Syntax.Abstract.Pretty.Base
 import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Abstract.Pretty.Base
+import MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind
 import Prettyprinter
 import Prettyprinter.Render.Terminal
 
@@ -22,8 +23,11 @@ renderPrettyCode :: PrettyCode c => Options -> c -> Text
 renderPrettyCode opts = renderStrict . docStream opts
 
 docStream :: PrettyCode c => Options -> c -> SimpleDocStream AnsiStyle
-docStream opts = reAnnotateS stylize . layoutPretty defaultLayoutOptions
-    . run . runReader opts . ppCode
+docStream opts =
+  reAnnotateS stylize . layoutPretty defaultLayoutOptions
+    . run
+    . runReader opts
+    . ppCode
 
 stylize :: Ann -> AnsiStyle
 stylize a = case a of

src/MiniJuvix/Syntax/Abstract/Pretty/Base.hs

@@ -1,23 +1,21 @@
-module MiniJuvix.Syntax.Abstract.Pretty.Base (
-  module MiniJuvix.Syntax.Abstract.Pretty.Base,
-  module MiniJuvix.Syntax.Abstract.Pretty.Ann
-                                             ) where
-
-import MiniJuvix.Syntax.Fixity
-import MiniJuvix.Syntax.Usage
-import MiniJuvix.Syntax.Universe
-import Prettyprinter
-import MiniJuvix.Prelude
-
-import qualified MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base as S
-import MiniJuvix.Syntax.Abstract.Language
-import MiniJuvix.Syntax.Abstract.Pretty.Ann
+module MiniJuvix.Syntax.Abstract.Pretty.Base
+  ( module MiniJuvix.Syntax.Abstract.Pretty.Base,
+    module MiniJuvix.Syntax.Abstract.Pretty.Ann,
+  )
+where
 
 import qualified MiniJuvix.Internal.Strings as Str
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Abstract.Language
+import MiniJuvix.Syntax.Abstract.Pretty.Ann
+import qualified MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base as S
+import MiniJuvix.Syntax.Fixity
+import MiniJuvix.Syntax.Universe
+import MiniJuvix.Syntax.Usage
+import Prettyprinter
 
 data Options = Options
-  {
-    _optShowNameId :: Bool,
+  { _optShowNameId :: Bool,
     _optIndent :: Int,
     _optShowDecreasingArgs :: ShowDecrArgs
   }
@@ -25,10 +23,11 @@ data Options = Options
 data ShowDecrArgs = OnlyArg | OnlyRel | ArgRel
 
 toSOptions :: Options -> S.Options
-toSOptions Options {..} = S.defaultOptions {
-  S._optShowNameId = _optShowNameId,
-  S._optIndent = _optIndent
-  }
+toSOptions Options {..} =
+  S.defaultOptions
+    { S._optShowNameId = _optShowNameId,
+      S._optIndent = _optIndent
+    }
 
 class PrettyCode c where
   ppCode :: Members '[Reader Options] r => c -> Sem r (Doc Ann)
@@ -41,8 +40,7 @@ ppSCode c = do
 defaultOptions :: Options
 defaultOptions =
   Options
-    {
-      _optShowNameId = False,
+    { _optShowNameId = False,
       _optIndent = 2,
       _optShowDecreasingArgs = OnlyRel
     }
@@ -55,7 +53,7 @@ runPrettyCode opts = run . runReader opts . ppCode
 
 instance PrettyCode Iden where
   ppCode i = case i of
-    IdenDefined n -> ppSCode n
+    IdenFunction n -> ppSCode n
     IdenConstructor n -> ppSCode n
     IdenInductive n -> ppSCode n
     IdenVar n -> ppSCode n
@@ -101,9 +99,9 @@ kwColonOmega = keyword Str.colonOmegaUnicode
 
 instance PrettyCode Usage where
   ppCode u = return $ case u of
-     UsageNone -> kwColonZero
-     UsageOnce -> kwColonOne
-     UsageOmega -> kwColon
+    UsageNone -> kwColonZero
+    UsageOnce -> kwColonOne
+    UsageOmega -> kwColon
 
 instance PrettyCode FunctionParameter where
   ppCode FunctionParameter {..} = do
@@ -124,24 +122,36 @@ instance PrettyCode Function where
 parensCond :: Bool -> Doc Ann -> Doc Ann
 parensCond t d = if t then parens d else d
 
-ppPostExpression ::(PrettyCode a, HasAtomicity a, Member (Reader Options) r)  =>
-  Fixity -> a -> Sem r (Doc Ann)
+ppPostExpression ::
+  (PrettyCode a, HasAtomicity a, Member (Reader Options) r) =>
+  Fixity ->
+  a ->
+  Sem r (Doc Ann)
 ppPostExpression = ppLRExpression isPostfixAssoc
 
-ppRightExpression :: (PrettyCode a, HasAtomicity a, Member (Reader Options) r) =>
-  Fixity -> a -> Sem r (Doc Ann)
+ppRightExpression ::
+  (PrettyCode a, HasAtomicity a, Member (Reader Options) r) =>
+  Fixity ->
+  a ->
+  Sem r (Doc Ann)
 ppRightExpression = ppLRExpression isRightAssoc
 
-ppLeftExpression :: (PrettyCode a, HasAtomicity a, Member (Reader Options) r) =>
-  Fixity -> a -> Sem r (Doc Ann)
+ppLeftExpression ::
+  (PrettyCode a, HasAtomicity a, Member (Reader Options) r) =>
+  Fixity ->
+  a ->
+  Sem r (Doc Ann)
 ppLeftExpression = ppLRExpression isLeftAssoc
 
-ppLRExpression
-  :: (HasAtomicity a, PrettyCode a, Member (Reader Options) r) =>
-     (Fixity -> Bool) -> Fixity -> a -> Sem r (Doc Ann)
+ppLRExpression ::
+  (HasAtomicity a, PrettyCode a, Member (Reader Options) r) =>
+  (Fixity -> Bool) ->
+  Fixity ->
+  a ->
+  Sem r (Doc Ann)
 ppLRExpression associates fixlr e =
   parensCond (atomParens associates (atomicity e) fixlr)
-      <$> ppCode e
+    <$> ppCode e
 
 ppCodeAtom :: (HasAtomicity c, PrettyCode c, Members '[Reader Options] r) => c -> Sem r (Doc Ann)
 ppCodeAtom c = do

src/MiniJuvix/Syntax/Concrete/Base.hs

@@ -8,8 +8,8 @@ module MiniJuvix.Syntax.Concrete.Base
 where
 
 import Control.Monad.Combinators.Expr
-import Control.Monad.Combinators.NonEmpty (sepBy1, some, sepEndBy1)
+import Control.Monad.Combinators.NonEmpty (sepBy1, sepEndBy1, some)
 import Data.List.NonEmpty (NonEmpty)
 import MiniJuvix.Prelude hiding (some)
-import Text.Megaparsec hiding (sepBy1, some, sepEndBy1)
+import Text.Megaparsec hiding (sepBy1, sepEndBy1, some)
 import Text.Megaparsec.Char

src/MiniJuvix/Syntax/Concrete/Language.hs

@@ -3,44 +3,70 @@ module MiniJuvix.Syntax.Concrete.Language
   ( module MiniJuvix.Syntax.Concrete.Language,
     module MiniJuvix.Syntax.Concrete.Name,
     module MiniJuvix.Syntax.Concrete.Loc,
+    module MiniJuvix.Syntax.Concrete.Scoped.VisibilityAnn,
     module MiniJuvix.Syntax.Concrete.PublicAnn,
+    module MiniJuvix.Syntax.Concrete.ModuleIsTop,
     module MiniJuvix.Syntax.Concrete.Language.Stage,
     module MiniJuvix.Syntax.Fixity,
     module MiniJuvix.Syntax.Usage,
-    module MiniJuvix.Syntax.Universe
+    module MiniJuvix.Syntax.Universe,
   )
 where
 
 --------------------------------------------------------------------------------
 
 import qualified Data.Kind as GHC
-import MiniJuvix.Syntax.Universe
-import MiniJuvix.Syntax.Fixity
-import MiniJuvix.Syntax.Usage
-import MiniJuvix.Syntax.Concrete.Name
-import MiniJuvix.Syntax.Concrete.Loc
-import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
-import MiniJuvix.Syntax.Concrete.PublicAnn
+import MiniJuvix.Prelude hiding (show)
 import MiniJuvix.Syntax.Concrete.Language.Stage
-import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Concrete.Loc
+import MiniJuvix.Syntax.Concrete.ModuleIsTop
+import MiniJuvix.Syntax.Concrete.Name
+import MiniJuvix.Syntax.Concrete.Scoped.VisibilityAnn
+import MiniJuvix.Syntax.Concrete.PublicAnn
+import MiniJuvix.Syntax.Concrete.Scoped.Name (unqualifiedSymbol)
+import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
+import MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind
+import MiniJuvix.Syntax.Fixity
+import MiniJuvix.Syntax.Universe
+import MiniJuvix.Syntax.Usage
+import Prelude (show)
 
 --------------------------------------------------------------------------------
 -- Parsing stages
 --------------------------------------------------------------------------------
 
-type family SymbolType (s :: Stage) :: (res :: GHC.Type) | res -> s where
+type RefNameType :: S.IsConcrete -> GHC.Type
+type family RefNameType c = res | res -> c where
+  RefNameType 'S.Concrete = S.Name
+  RefNameType 'S.NotConcrete = S.Name' ()
+
+type SymbolType :: Stage -> GHC.Type
+type family SymbolType s = res | res -> s where
   SymbolType 'Parsed = Symbol
   SymbolType 'Scoped = S.Symbol
 
-type family NameType (s :: Stage) :: (res :: GHC.Type) | res -> s where
-  NameType 'Parsed = Name
-  NameType 'Scoped = S.Name
+type ModuleRefType :: Stage -> GHC.Type
+type family ModuleRefType s = res | res -> s where
+  ModuleRefType 'Parsed = Name
+  ModuleRefType 'Scoped = ModuleRef
 
-type family ExpressionType (s :: Stage) :: (res :: GHC.Type) | res -> s where
+type IdentifierType :: Stage -> GHC.Type
+type family IdentifierType s = res | res -> s where
+  IdentifierType 'Parsed = Name
+  IdentifierType 'Scoped = ScopedIden
+
+type PatternAtomIdenType :: Stage -> GHC.Type
+type family PatternAtomIdenType s = res | res -> s where
+  PatternAtomIdenType 'Parsed = Name
+  PatternAtomIdenType 'Scoped = PatternScopedIden
+
+type ExpressionType :: Stage -> GHC.Type
+type family ExpressionType s = res | res -> s where
   ExpressionType 'Parsed = ExpressionAtoms 'Parsed
   ExpressionType 'Scoped = Expression
 
-type family PatternType (s :: Stage) :: (res :: GHC.Type) | res -> s where
+type PatternType :: Stage -> GHC.Type
+type family PatternType s = res | res -> s where
   PatternType 'Parsed = PatternAtom 'Parsed
   PatternType 'Scoped = Pattern
 
@@ -48,9 +74,8 @@ type family ImportType (s :: Stage) :: GHC.Type where
   ImportType 'Parsed = TopModulePath
   ImportType 'Scoped = Module 'Scoped 'ModuleTop
 
-type family
-  ModulePathType (s :: Stage) (t :: ModuleIsTop) ::
-    (res :: GHC.Type) | res -> t s
+type ModulePathType :: Stage -> ModuleIsTop -> GHC.Type
+type family ModulePathType s t = res | res -> t s
   where
   ModulePathType 'Parsed 'ModuleTop = TopModulePath
   ModulePathType 'Scoped 'ModuleTop = S.TopModulePath
@@ -73,14 +98,14 @@ data Statement (s :: Stage)
   | StatementEval (Eval s)
   | StatementPrint (Print s)
   | StatementForeign ForeignBlock
-  | StatementCompile (CompileDef s)
 
 deriving stock instance
   ( Show (ImportType s),
     Show (ModulePathType s 'ModuleLocal),
     Show (PatternType s),
     Show (SymbolType s),
-    Show (NameType s),
+    Show (IdentifierType s),
+    Show (ModuleRefType s),
     Show (ExpressionType s)
   ) =>
   Show (Statement s)
@@ -90,7 +115,8 @@ deriving stock instance
     Eq (PatternType s),
     Eq (ModulePathType s 'ModuleLocal),
     Eq (SymbolType s),
-    Eq (NameType s),
+    Eq (IdentifierType s),
+    Eq (ModuleRefType s),
     Eq (ExpressionType s)
   ) =>
   Eq (Statement s)
@@ -100,23 +126,15 @@ deriving stock instance
     Ord (PatternType s),
     Ord (ModulePathType s 'ModuleLocal),
     Ord (SymbolType s),
-    Ord (NameType s),
+    Ord (IdentifierType s),
+    Ord (ModuleRefType s),
     Ord (ExpressionType s)
   ) =>
   Ord (Statement s)
 
-data CompileDef (s :: Stage) = CompileDef {
-  _compileAxiom :: SymbolType s,
-  _compileBackend :: Backend,
-  _compileCode :: Text
-  }
-deriving stock instance (Eq (SymbolType s)) => Eq (CompileDef s)
-deriving stock instance (Ord (SymbolType s)) => Ord (CompileDef s)
-deriving stock instance (Show (SymbolType s)) => Show (CompileDef s)
-
-data ForeignBlock = ForeignBlock {
-  _foreignBackend :: Backend,
-  _foreignCode :: Text
+data ForeignBlock = ForeignBlock
+  { _foreignBackend :: Backend,
+    _foreignCode :: Text
   }
   deriving stock (Eq, Ord, Show)
 
@@ -171,7 +189,8 @@ deriving stock instance (Ord (ExpressionType s), Ord (SymbolType s)) => Ord (Typ
 
 data AxiomDef (s :: Stage) = AxiomDef
   { _axiomName :: SymbolType s,
-    _axiomType :: ExpressionType s
+    _axiomType :: ExpressionType s,
+    _axiomBackendItems :: [BackendItem]
   }
 
 deriving stock instance (Show (ExpressionType s), Show (SymbolType s)) => Show (AxiomDef s)
@@ -189,8 +208,8 @@ type InductiveConstructorName s = SymbolType s
 type InductiveName s = SymbolType s
 
 data InductiveConstructorDef (s :: Stage) = InductiveConstructorDef
-  { constructorName :: InductiveConstructorName s,
-    constructorType :: ExpressionType s
+  { _constructorName :: InductiveConstructorName s,
+    _constructorType :: ExpressionType s
   }
 
 deriving stock instance (Show (ExpressionType s), Show (SymbolType s)) => Show (InductiveConstructorDef s)
@@ -228,37 +247,33 @@ deriving stock instance (Ord (ExpressionType s), Ord (SymbolType s)) => Ord (Ind
 --------------------------------------------------------------------------------
 
 data PatternApp = PatternApp
-  {
-    patAppLeft :: Pattern,
-    patAppRight :: Pattern
+  { _patAppLeft :: Pattern,
+    _patAppRight :: Pattern
   }
   deriving stock (Show, Eq, Ord)
 
-
 data PatternInfixApp = PatternInfixApp
-  {
-    patInfixLeft :: Pattern,
-    patInfixConstructor :: NameType 'Scoped,
-    patInfixRight :: Pattern
+  { _patInfixLeft :: Pattern,
+    _patInfixConstructor :: ConstructorRef,
+    _patInfixRight :: Pattern
   }
   deriving stock (Show, Eq, Ord)
 
 instance HasFixity PatternInfixApp where
-  getFixity (PatternInfixApp  _ op _) = fromMaybe impossible (op ^. S.nameFixity)
+  getFixity (PatternInfixApp _ op _) = fromMaybe impossible (_constructorRefName op ^. S.nameFixity)
 
 data PatternPostfixApp = PatternPostfixApp
-  {
-    patPostfixParameter :: Pattern,
-    patPostfixConstructor :: NameType 'Scoped
+  { _patPostfixParameter :: Pattern,
+    _patPostfixConstructor :: ConstructorRef
   }
   deriving stock (Show, Eq, Ord)
 
 instance HasFixity PatternPostfixApp where
-  getFixity (PatternPostfixApp  _ op) = fromMaybe impossible (op ^. S.nameFixity)
+  getFixity (PatternPostfixApp _ op) = fromMaybe impossible (_constructorRefName op ^. S.nameFixity)
 
 data Pattern
   = PatternVariable (SymbolType 'Scoped)
-  | PatternConstructor (NameType 'Scoped)
+  | PatternConstructor ConstructorRef
   | PatternApplication PatternApp
   | PatternInfixApplication PatternInfixApp
   | PatternPostfixApplication PatternPostfixApp
@@ -267,7 +282,7 @@ data Pattern
   deriving stock (Show, Eq, Ord)
 
 instance HasAtomicity Pattern where
- atomicity e = case e of
+  atomicity e = case e of
     PatternVariable {} -> Atom
     PatternConstructor {} -> Atom
     PatternApplication {} -> Aggregate appFixity
@@ -280,8 +295,13 @@ instance HasAtomicity Pattern where
 -- Pattern section
 --------------------------------------------------------------------------------
 
+data PatternScopedIden
+  = PatternScopedVar S.Symbol
+  | PatternScopedConstructor ConstructorRef
+  deriving stock (Show, Ord, Eq)
+
 data PatternAtom (s :: Stage)
-  = PatternAtomName (NameType s)
+  = PatternAtomIden (PatternAtomIdenType s)
   | PatternAtomWildcard
   | PatternAtomEmpty
   | PatternAtomParens (PatternAtoms s)
@@ -291,21 +311,24 @@ instance HasAtomicity (PatternAtom 'Parsed) where
 
 deriving stock instance
   ( Show (ExpressionType s),
-    Show (NameType s),
+    Show (IdentifierType s),
+    Show (PatternAtomIdenType s),
     Show (PatternType s)
   ) =>
   Show (PatternAtom s)
 
 deriving stock instance
   ( Eq (ExpressionType s),
-    Eq (NameType s),
+    Eq (IdentifierType s),
+    Eq (PatternAtomIdenType s),
     Eq (PatternType s)
   ) =>
   Eq (PatternAtom s)
 
 deriving stock instance
   ( Ord (ExpressionType s),
-    Ord (NameType s),
+    Ord (IdentifierType s),
+    Ord (PatternAtomIdenType s),
     Ord (PatternType s)
   ) =>
   Ord (PatternAtom s)
@@ -315,21 +338,24 @@ newtype PatternAtoms (s :: Stage)
 
 deriving stock instance
   ( Show (ExpressionType s),
-    Show (NameType s),
+    Show (IdentifierType s),
+    Show (PatternAtomIdenType s),
     Show (PatternType s)
   ) =>
   Show (PatternAtoms s)
 
 deriving stock instance
   ( Eq (ExpressionType s),
-    Eq (NameType s),
+    Eq (IdentifierType s),
+    Eq (PatternAtomIdenType s),
     Eq (PatternType s)
   ) =>
   Eq (PatternAtoms s)
 
 deriving stock instance
   ( Ord (ExpressionType s),
-    Ord (NameType s),
+    Ord (IdentifierType s),
+    Ord (PatternAtomIdenType s),
     Ord (PatternType s)
   ) =>
   Ord (PatternAtoms s)
@@ -349,7 +375,8 @@ data FunctionClause (s :: Stage) = FunctionClause
 
 deriving stock instance
   ( Show (PatternType s),
-    Show (NameType s),
+    Show (IdentifierType s),
+    Show (ModuleRefType s),
     Show (SymbolType s),
     Show (ExpressionType s)
   ) =>
@@ -357,7 +384,8 @@ deriving stock instance
 
 deriving stock instance
   ( Eq (PatternType s),
-    Eq (NameType s),
+    Eq (IdentifierType s),
+    Eq (ModuleRefType s),
     Eq (SymbolType s),
     Eq (ExpressionType s)
   ) =>
@@ -365,7 +393,8 @@ deriving stock instance
 
 deriving stock instance
   ( Ord (PatternType s),
-    Ord (NameType s),
+    Ord (IdentifierType s),
+    Ord (ModuleRefType s),
     Ord (SymbolType s),
     Ord (ExpressionType s)
   ) =>
@@ -375,22 +404,6 @@ deriving stock instance
 -- Module declaration
 --------------------------------------------------------------------------------
 
-data ModuleIsTop = ModuleTop | ModuleLocal
-
--- The following Singleton related definitions could be scrapped if we depended
--- on the singletons-th library.
-data SModuleIsTop (t :: ModuleIsTop) where
-  SModuleTop :: SModuleIsTop 'ModuleTop
-  SModuleLocal :: SModuleIsTop 'ModuleLocal
-
-type instance Sing = SModuleIsTop
-
-instance SingI 'ModuleTop where
-  sing = SModuleTop
-
-instance SingI 'ModuleLocal where
-  sing = SModuleLocal
-
 type LocalModuleName s = SymbolType s
 
 data Module (s :: Stage) (t :: ModuleIsTop) = Module
@@ -404,7 +417,8 @@ deriving stock instance
     Show (ModulePathType s 'ModuleLocal),
     Show (ImportType s),
     Show (PatternType s),
-    Show (NameType s),
+    Show (IdentifierType s),
+    Show (ModuleRefType s),
     Show (SymbolType s),
     Show (ExpressionType s)
   ) =>
@@ -415,7 +429,8 @@ deriving stock instance
     Eq (ModulePathType s 'ModuleLocal),
     Eq (ImportType s),
     Eq (PatternType s),
-    Eq (NameType s),
+    Eq (IdentifierType s),
+    Eq (ModuleRefType s),
     Eq (SymbolType s),
     Eq (ExpressionType s)
   ) =>
@@ -426,7 +441,8 @@ deriving stock instance
     Ord (ModulePathType s 'ModuleLocal),
     Ord (ImportType s),
     Ord (PatternType s),
-    Ord (NameType s),
+    Ord (IdentifierType s),
+    Ord (ModuleRefType s),
     Ord (SymbolType s),
     Ord (ExpressionType s)
   ) =>
@@ -437,31 +453,91 @@ data UsingHiding
   | Hiding (NonEmpty Symbol)
   deriving stock (Show, Eq, Ord)
 
-data OpenModule (s :: Stage) = OpenModule
-  { openModuleName :: NameType s,
-    openParameters :: [ExpressionType s],
-    openUsingHiding :: Maybe UsingHiding,
-    openPublic :: PublicAnn
+type ModuleRef = ModuleRef' 'S.Concrete
+
+newtype ModuleRef' (c :: S.IsConcrete) = ModuleRef'
+  { _unModuleRef' :: Σ ModuleIsTop (TyCon1 (ModuleRef'' c))
   }
+
+-- | TODO can this be derived?
+instance SingI c => Show (ModuleRef' c) where
+  show (ModuleRef' (isTop :&: r)) = case isTop of
+    SModuleLocal -> case sing :: S.SIsConcrete c of
+      S.SConcrete -> show r
+      S.SNotConcrete -> show r
+    SModuleTop -> case sing :: S.SIsConcrete c of
+      S.SConcrete -> show r
+      S.SNotConcrete -> show r
+
+getNameRefId :: forall c. SingI c => RefNameType c -> S.NameId
+getNameRefId = case sing :: S.SIsConcrete c of
+  S.SConcrete -> S._nameId
+  S.SNotConcrete -> S._nameId
+
+getModuleExportInfo :: ModuleRef' c -> ExportInfo
+getModuleExportInfo = projSigma2 _moduleExportInfo . _unModuleRef'
+
+getModuleRefNameType :: ModuleRef' c -> RefNameType c
+getModuleRefNameType = projSigma2 _moduleRefName . _unModuleRef'
+
+instance SingI c => Eq (ModuleRef' c) where
+  (==) = (==) `on` (getNameRefId . getModuleRefNameType)
+
+instance SingI c => Ord (ModuleRef' c) where
+  compare = compare `on` (getNameRefId . getModuleRefNameType)
+
+-- TODO find a better name
+data ModuleRef'' (c :: S.IsConcrete) (t :: ModuleIsTop) = ModuleRef''
+  { _moduleRefName :: RefNameType c,
+    _moduleExportInfo :: ExportInfo,
+    _moduleRefModule :: Module 'Scoped t
+  }
+
+instance Show (RefNameType s) => Show (ModuleRef'' s t) where
+  show = show . _moduleRefName
+
+data SymbolEntry
+  = EntryAxiom (AxiomRef' 'S.NotConcrete)
+  | EntryInductive (InductiveRef' 'S.NotConcrete)
+  | EntryFunction (FunctionRef' 'S.NotConcrete)
+  | EntryConstructor (ConstructorRef' 'S.NotConcrete)
+  | EntryModule (ModuleRef' 'S.NotConcrete)
+  deriving stock (Show)
+
+-- | Symbols that a module exports
+newtype ExportInfo = ExportInfo
+  { _exportSymbols :: HashMap Symbol SymbolEntry
+  }
+  deriving stock (Show)
+
+data OpenModule (s :: Stage) = OpenModule
+  { _openModuleName :: ModuleRefType s,
+    _openParameters :: [ExpressionType s],
+    _openUsingHiding :: Maybe UsingHiding,
+    _openPublic :: PublicAnn
+  }
+
 deriving stock instance
-  (
-    Eq (NameType s),
+  ( Eq (IdentifierType s),
     Eq (SymbolType s),
+    Eq (ModuleRefType s),
     Eq (PatternType s),
     Eq (ExpressionType s)
   ) =>
   Eq (OpenModule s)
+
 deriving stock instance
-  (
-    Ord (NameType s),
+  ( Ord (IdentifierType s),
     Ord (SymbolType s),
     Ord (PatternType s),
+    Ord (ModuleRefType s),
     Ord (ExpressionType s)
   ) =>
   Ord (OpenModule s)
+
 deriving stock instance
-  (
-    Show (NameType s),
+  ( Show (IdentifierType s),
+    Show (ModuleRefType s),
     Show (ExpressionType s)
   ) =>
   Show (OpenModule s)
@@ -470,41 +546,111 @@ deriving stock instance
 -- Expression
 --------------------------------------------------------------------------------
 
-data AxiomRef = AxiomRef {
-  _axiomRefName :: NameType 'Scoped,
-  _axiomRefBackends :: HashMap Backend Text
-  }
-  deriving stock (Show, Eq, Ord)
+type AxiomRef = AxiomRef' 'S.Concrete
 
-data InductiveRef = InductiveRef {
-  _inductiveRefName :: NameType 'Scoped,
-  _inductiveRefDef :: InductiveDef 'Scoped
-  }
-  deriving stock (Show, Eq, Ord)
+newtype AxiomRef' (n :: S.IsConcrete) = AxiomRef'
+  { _axiomRefName :: RefNameType n}
 
-data FunctionRef = FunctionRef {
-  _functionRefName :: NameType 'Scoped,
-  _functionRefSig :: Expression
-  }
-  deriving stock (Show, Eq, Ord)
+instance Hashable (RefNameType s) => Hashable (AxiomRef' s) where
+  hashWithSalt i = hashWithSalt i . _axiomRefName
 
-data ConstructorRef = ConstructorRef {
-  _constructorRefName :: NameType 'Scoped,
-  _constructorSig :: Expression
-  }
-  deriving stock (Show, Eq, Ord)
+instance Eq (RefNameType s) => Eq (AxiomRef' s) where
+  (==) = (==) `on` _axiomRefName
 
-data ScopedIden =
-  ScopedAxiom AxiomRef
-  | ScopedInductive InductiveRef
-  | ScopedVar (NameType 'Scoped)
-  | ScopedFunction FunctionRef
-  | ScopedConstructor ConstructorRef
-  deriving stock (Show, Eq, Ord)
+instance Ord (RefNameType s) => Ord (AxiomRef' s) where
+  compare = compare `on` _axiomRefName
+
+instance Show (RefNameType s) => Show (AxiomRef' s) where
+  show = show . _axiomRefName
+
+type InductiveRef = InductiveRef' 'S.Concrete
+
+newtype InductiveRef' (n :: S.IsConcrete) = InductiveRef'
+  { _inductiveRefName :: RefNameType n
+  }
+
+instance Hashable (RefNameType s) => Hashable (InductiveRef' s) where
+  hashWithSalt i = hashWithSalt i . _inductiveRefName
+
+instance Eq (RefNameType s) => Eq (InductiveRef' s) where
+  (==) = (==) `on` _inductiveRefName
+
+instance Ord (RefNameType s) => Ord (InductiveRef' s) where
+  compare = compare `on` _inductiveRefName
+
+instance Show (RefNameType s) => Show (InductiveRef' s) where
+  show = show . _inductiveRefName
+
+type FunctionRef = FunctionRef' 'S.Concrete
+
+newtype FunctionRef' (n :: S.IsConcrete) = FunctionRef'
+  { _functionRefName :: RefNameType n
+  }
+
+instance Hashable (RefNameType s) => Hashable (FunctionRef' s) where
+  hashWithSalt i = hashWithSalt i . _functionRefName
+
+instance Eq (RefNameType s) => Eq (FunctionRef' s) where
+  (==) = (==) `on` _functionRefName
+
+instance Ord (RefNameType s) => Ord (FunctionRef' s) where
+  compare = compare `on` _functionRefName
+
+instance Show (RefNameType s) => Show (FunctionRef' s) where
+  show = show . _functionRefName
+
+type ConstructorRef = ConstructorRef' 'S.Concrete
+
+newtype ConstructorRef' (n :: S.IsConcrete) = ConstructorRef'
+  { _constructorRefName :: RefNameType n
+  }
+
+instance Hashable (RefNameType s) => Hashable (ConstructorRef' s) where
+  hashWithSalt i = hashWithSalt i . _constructorRefName
+
+instance Eq (RefNameType s) => Eq (ConstructorRef' s) where
+  (==) = (==) `on` _constructorRefName
+
+instance Ord (RefNameType s) => Ord (ConstructorRef' s) where
+  compare = compare `on` _constructorRefName
+
+instance Show (RefNameType s) => Show (ConstructorRef' s) where
+  show = show . _constructorRefName
+
+type ScopedIden = ScopedIden' 'S.Concrete
+
+data ScopedIden' (n :: S.IsConcrete)
+  = ScopedAxiom (AxiomRef' n)
+  | ScopedInductive (InductiveRef' n)
+  | ScopedVar S.Symbol
+  | ScopedFunction (FunctionRef' n)
+  | ScopedConstructor (ConstructorRef' n)
+
+deriving stock instance
+  (Eq (RefNameType s)) => Eq (ScopedIden' s)
+
+deriving stock instance
+  (Ord (RefNameType s)) => Ord (ScopedIden' s)
+
+deriving stock instance
+  (Show (RefNameType s)) => Show (ScopedIden' s)
+
+identifierName :: forall n. SingI n => ScopedIden' n -> RefNameType n
+identifierName = \case
+  ScopedAxiom a -> _axiomRefName a
+  ScopedInductive i -> _inductiveRefName i
+  ScopedVar v ->
+    ( case sing :: S.SIsConcrete n of
+        S.SConcrete -> id
+        S.SNotConcrete -> set S.nameConcrete ()
+    )
+      (unqualifiedSymbol v)
+  ScopedFunction f -> _functionRefName f
+  ScopedConstructor c -> _constructorRefName c
 
 data Expression
   = ExpressionIdentifier ScopedIden
-  | ExpressionParensIdentifier (NameType 'Scoped)
+  | ExpressionParensIdentifier ScopedIden
   | ExpressionApplication Application
   | ExpressionInfixApplication InfixApplication
   | ExpressionPostfixApplication PostfixApplication
@@ -522,7 +668,7 @@ instance HasAtomicity Literal where
     LitString {} -> Atom
 
 instance HasAtomicity Expression where
- atomicity e = case e of
+  atomicity e = case e of
     ExpressionIdentifier {} -> Atom
     ExpressionParensIdentifier {} -> Atom
     ExpressionApplication {} -> Aggregate appFixity
@@ -539,14 +685,14 @@ instance HasAtomicity Expression where
 -- Expression atom
 --------------------------------------------------------------------------------
 
-data Literal =
-  LitString Text
+data Literal
+  = LitString Text
   | LitInteger Integer
   deriving stock (Show, Eq, Ord)
 
 -- | Expressions without application
 data ExpressionAtom (s :: Stage)
-  = AtomIdentifier (NameType s)
+  = AtomIdentifier (IdentifierType s)
   | AtomLambda (Lambda s)
   | AtomLetBlock (LetBlock s)
   | AtomUniverse Universe
@@ -558,7 +704,8 @@ data ExpressionAtom (s :: Stage)
 
 deriving stock instance
   ( Show (ExpressionType s),
-    Show (NameType s),
+    Show (IdentifierType s),
+    Show (ModuleRefType s),
     Show (SymbolType s),
     Show (PatternType s)
   ) =>
@@ -566,7 +713,8 @@ deriving stock instance
 
 deriving stock instance
   ( Eq (ExpressionType s),
-    Eq (NameType s),
+    Eq (IdentifierType s),
+    Eq (ModuleRefType s),
     Eq (SymbolType s),
     Eq (PatternType s)
   ) =>
@@ -574,7 +722,8 @@ deriving stock instance
 
 deriving stock instance
   ( Ord (ExpressionType s),
-    Ord (NameType s),
+    Ord (IdentifierType s),
+    Ord (ModuleRefType s),
     Ord (SymbolType s),
     Ord (PatternType s)
   ) =>
@@ -586,14 +735,15 @@ newtype ExpressionAtoms (s :: Stage)
 
 instance HasAtomicity (ExpressionAtoms 'Parsed) where
   atomicity (ExpressionAtoms l) = case l of
-    (_  :| []) -> Atom
-    (_  :| _)
+    (_ :| []) -> Atom
+    (_ :| _)
       | AtomFunArrow `elem` l -> Aggregate funFixity
       | otherwise -> Aggregate appFixity
 
 deriving stock instance
   ( Show (ExpressionType s),
-    Show (NameType s),
+    Show (IdentifierType s),
+    Show (ModuleRefType s),
     Show (SymbolType s),
     Show (PatternType s)
   ) =>
@@ -601,7 +751,8 @@ deriving stock instance
 
 deriving stock instance
   ( Eq (ExpressionType s),
-    Eq (NameType s),
+    Eq (IdentifierType s),
+    Eq (ModuleRefType s),
     Eq (SymbolType s),
     Eq (PatternType s)
   ) =>
@@ -609,7 +760,8 @@ deriving stock instance
 
 deriving stock instance
   ( Ord (ExpressionType s),
-    Ord (NameType s),
+    Ord (IdentifierType s),
+    Ord (ModuleRefType s),
     Ord (SymbolType s),
     Ord (PatternType s)
   ) =>
@@ -702,7 +854,8 @@ newtype WhereBlock (s :: Stage) = WhereBlock
 
 deriving stock instance
   ( Show (PatternType s),
-    Show (NameType s),
+    Show (IdentifierType s),
+    Show (ModuleRefType s),
     Show (SymbolType s),
     Show (ExpressionType s)
   ) =>
@@ -710,7 +863,8 @@ deriving stock instance
 
 deriving stock instance
   ( Eq (PatternType s),
-    Eq (NameType s),
+    Eq (IdentifierType s),
+    Eq (ModuleRefType s),
     Eq (SymbolType s),
     Eq (ExpressionType s)
   ) =>
@@ -718,7 +872,8 @@ deriving stock instance
 
 deriving stock instance
   ( Ord (PatternType s),
-    Ord (NameType s),
+    Ord (IdentifierType s),
+    Ord (ModuleRefType s),
     Ord (SymbolType s),
     Ord (ExpressionType s)
   ) =>
@@ -731,7 +886,8 @@ data WhereClause (s :: Stage)
 
 deriving stock instance
   ( Show (PatternType s),
-    Show (NameType s),
+    Show (IdentifierType s),
+    Show (ModuleRefType s),
     Show (SymbolType s),
     Show (ExpressionType s)
   ) =>
@@ -739,7 +895,8 @@ deriving stock instance
 
 deriving stock instance
   ( Eq (PatternType s),
-    Eq (NameType s),
+    Eq (IdentifierType s),
+    Eq (ModuleRefType s),
     Eq (SymbolType s),
     Eq (ExpressionType s)
   ) =>
@@ -747,7 +904,8 @@ deriving stock instance
 
 deriving stock instance
   ( Ord (PatternType s),
-    Ord (NameType s),
+    Ord (IdentifierType s),
+    Ord (ModuleRefType s),
     Ord (SymbolType s),
     Ord (ExpressionType s)
   ) =>
@@ -816,24 +974,22 @@ data Application = Application
 
 data InfixApplication = InfixApplication
   { infixAppLeft :: ExpressionType 'Scoped,
-    infixAppOperator :: NameType 'Scoped,
+    infixAppOperator :: IdentifierType 'Scoped,
     infixAppRight :: ExpressionType 'Scoped
   }
   deriving stock (Show, Eq, Ord)
 
 instance HasFixity InfixApplication where
-  getFixity (InfixApplication  _ op _) = fromMaybe impossible (op ^. S.nameFixity)
-
+  getFixity (InfixApplication _ op _) = fromMaybe impossible (identifierName op ^. S.nameFixity)
 
 data PostfixApplication = PostfixApplication
-  {
-    postfixAppParameter :: ExpressionType 'Scoped,
-    postfixAppOperator :: NameType 'Scoped
+  { postfixAppParameter :: ExpressionType 'Scoped,
+    postfixAppOperator :: IdentifierType 'Scoped
   }
   deriving stock (Show, Eq, Ord)
 
 instance HasFixity PostfixApplication where
-  getFixity (PostfixApplication _ op) = fromMaybe impossible (op ^. S.nameFixity)
+  getFixity (PostfixApplication _ op) = fromMaybe impossible (identifierName op ^. S.nameFixity)
 
 --------------------------------------------------------------------------------
 -- Let block expression
@@ -846,7 +1002,8 @@ data LetBlock (s :: Stage) = LetBlock
 
 deriving stock instance
   ( Show (PatternType s),
-    Show (NameType s),
+    Show (IdentifierType s),
+    Show (ModuleRefType s),
     Show (SymbolType s),
     Show (ExpressionType s)
   ) =>
@@ -854,7 +1011,8 @@ deriving stock instance
 
 deriving stock instance
   ( Eq (PatternType s),
-    Eq (NameType s),
+    Eq (IdentifierType s),
+    Eq (ModuleRefType s),
     Eq (SymbolType s),
     Eq (ExpressionType s)
   ) =>
@@ -862,7 +1020,8 @@ deriving stock instance
 
 deriving stock instance
   ( Ord (PatternType s),
-    Ord (NameType s),
+    Ord (IdentifierType s),
+    Ord (ModuleRefType s),
     Ord (SymbolType s),
     Ord (ExpressionType s)
   ) =>
@@ -874,7 +1033,8 @@ data LetClause (s :: Stage)
 
 deriving stock instance
   ( Show (PatternType s),
-    Show (NameType s),
+    Show (IdentifierType s),
+    Show (ModuleRefType s),
     Show (SymbolType s),
     Show (ExpressionType s)
   ) =>
@@ -882,7 +1042,8 @@ deriving stock instance
 
 deriving stock instance
   ( Eq (PatternType s),
-    Eq (NameType s),
+    Eq (IdentifierType s),
+    Eq (ModuleRefType s),
     Eq (SymbolType s),
     Eq (ExpressionType s)
   ) =>
@@ -890,7 +1051,8 @@ deriving stock instance
 
 deriving stock instance
   ( Ord (PatternType s),
-    Ord (NameType s),
+    Ord (IdentifierType s),
+    Ord (ModuleRefType s),
     Ord (SymbolType s),
     Ord (ExpressionType s)
   ) =>
@@ -900,7 +1062,13 @@ deriving stock instance
 -- Backends
 --------------------------------------------------------------------------------
 
-data Backend = BackendGhc
+data Backend = BackendGhc | BackendAgda
+  deriving stock (Show, Eq, Ord)
+
+data BackendItem = BackendItem
+  { _backendItemBackend :: Backend,
+    _backendItemCode :: Text
+  }
   deriving stock (Show, Eq, Ord)
 
 --------------------------------------------------------------------------------
@@ -943,10 +1111,60 @@ deriving stock instance
   Ord (Print s)
 
 makeLenses ''InductiveDef
+makeLenses ''InductiveConstructorDef
 makeLenses ''Module
 makeLenses ''TypeSignature
 makeLenses ''AxiomDef
 makeLenses ''FunctionClause
 makeLenses ''InductiveParameter
-makeLenses ''CompileDef
 makeLenses ''ForeignBlock
+makeLenses ''AxiomRef'
+makeLenses ''InductiveRef'
+makeLenses ''ModuleRef'
+makeLenses ''ModuleRef''
+makeLenses ''FunctionRef'
+makeLenses ''ConstructorRef'
+makeLenses ''BackendItem
+makeLenses ''OpenModule
+makeLenses ''PatternApp
+makeLenses ''PatternInfixApp
+makeLenses ''PatternPostfixApp
+
+idenOverName :: (forall s. S.Name' s -> S.Name' s) -> ScopedIden -> ScopedIden
+idenOverName f = \case
+  ScopedAxiom a -> ScopedAxiom (over axiomRefName f a)
+  ScopedInductive i -> ScopedInductive (over inductiveRefName f i)
+  ScopedVar v -> ScopedVar (f v)
+  ScopedFunction fun -> ScopedFunction (over functionRefName f fun)
+  ScopedConstructor c -> ScopedConstructor (over constructorRefName f c)
+
+entryPrism :: (S.Name' () -> S.Name' ()) -> SymbolEntry -> (S.Name' (), SymbolEntry)
+entryPrism f = \case
+  EntryAxiom a -> (a ^. axiomRefName, EntryAxiom (over axiomRefName f a))
+  EntryInductive i -> (i ^. inductiveRefName, EntryInductive (over inductiveRefName f i))
+  EntryFunction fun -> (fun ^. functionRefName, EntryFunction (over functionRefName f fun))
+  EntryConstructor c -> (c ^. constructorRefName, EntryConstructor (over constructorRefName f c))
+  EntryModule m -> (getModuleRefNameType m, EntryModule (overModuleRef'' (over moduleRefName f) m))
+
+entryOverName :: (S.Name' () -> S.Name' ()) -> SymbolEntry -> SymbolEntry
+entryOverName f = snd . entryPrism f
+
+entryName :: SymbolEntry -> S.Name' ()
+entryName = fst . entryPrism id
+
+instance HasLoc SymbolEntry where
+  getLoc = S._nameDefined . entryName
+
+overModuleRef'' :: forall s s'. (forall t. ModuleRef'' s t -> ModuleRef'' s' t) -> ModuleRef' s -> ModuleRef' s'
+overModuleRef'' f = over unModuleRef' (\(t :&: m'') -> t :&: f m'')
+
+symbolEntryToSName :: SymbolEntry -> S.Name' ()
+symbolEntryToSName = \case
+  EntryAxiom a -> a ^. axiomRefName
+  EntryInductive i -> i ^. inductiveRefName
+  EntryFunction f -> f ^. functionRefName
+  EntryConstructor c -> c ^. constructorRefName
+  EntryModule m -> getModuleRefNameType m
+
+instance HasNameKind SymbolEntry where
+  getNameKind = getNameKind . entryName

src/MiniJuvix/Syntax/Concrete/Language/Stage.hs

@@ -1,4 +1,5 @@
 {-# LANGUAGE StandaloneKindSignatures #-}
+
 module MiniJuvix.Syntax.Concrete.Language.Stage where
 
 import MiniJuvix.Prelude

src/MiniJuvix/Syntax/Concrete/Lexer.hs

@@ -2,14 +2,14 @@ module MiniJuvix.Syntax.Concrete.Lexer where
 
 --------------------------------------------------------------------------------
 
-import GHC.Unicode
-import MiniJuvix.Syntax.Concrete.Base hiding (space, Pos)
-import qualified MiniJuvix.Syntax.Concrete.Base as P
-import MiniJuvix.Prelude
-import qualified Text.Megaparsec.Char.Lexer as L
-import MiniJuvix.Syntax.Concrete.Loc
-import qualified MiniJuvix.Internal.Strings as Str
 import qualified Data.Text as Text
+import GHC.Unicode
+import qualified MiniJuvix.Internal.Strings as Str
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Concrete.Base hiding (Pos, space)
+import qualified MiniJuvix.Syntax.Concrete.Base as P
+import MiniJuvix.Syntax.Concrete.Loc
+import qualified Text.Megaparsec.Char.Lexer as L
 
 --------------------------------------------------------------------------------
 
@@ -45,12 +45,19 @@ integer = do
   nat <- lexeme L.decimal
   case minus of
     Nothing -> return nat
-    _ -> return (- nat)
+    _ -> return (-nat)
 
 -- | TODO allow escaping { inside the string using \{
 bracedString :: MonadParsec e Text m => m Text
 bracedString =
-  Text.strip . pack <$> (char '{' >> manyTill anySingle (char '}'))
+  Text.strip . unIndent . pack <$> (char '{' >> manyTill anySingle (char '}'))
+  where
+    unIndent :: Text -> Text
+    unIndent t = Text.unlines (Text.drop (fromMaybe 0 (indentIdx t)) <$> Text.lines t)
+    indentIdx :: Text -> Maybe Int
+    indentIdx = minimumMaybe . mapMaybe firstNonBlankChar . Text.lines
+    firstNonBlankChar :: Text -> Maybe Int
+    firstNonBlankChar = Text.findIndex (not . isSpace)
 
 string :: MonadParsec e Text m => m Text
 string = pack <$> (char '"' >> manyTill L.charLiteral (char '"'))
@@ -58,11 +65,11 @@ string = pack <$> (char '"' >> manyTill L.charLiteral (char '"'))
 mkLoc :: SourcePos -> Loc
 mkLoc SourcePos {..} = Loc {..}
   where
-  _locFile = sourceName
-  _locFileLoc = FileLoc {..}
-    where
-    _locLine = fromPos sourceLine
-    _locCol = fromPos sourceColumn
+    _locFile = sourceName
+    _locFileLoc = FileLoc {..}
+      where
+        _locLine = fromPos sourceLine
+        _locCol = fromPos sourceColumn
 
 curLoc :: MonadParsec e Text m => m Loc
 curLoc = mkLoc <$> getSourcePos
@@ -99,9 +106,9 @@ bareIdentifier = interval $ do
           c `elem` extraAllowedChars
         ]
       where
-      extraAllowedChars :: [Char]
-      extraAllowedChars = "_'-*,&"
-      cat = generalCategory c
+        extraAllowedChars :: [Char]
+        extraAllowedChars = "_'-*,&"
+        cat = generalCategory c
 
 dot :: forall e m. MonadParsec e Text m => m Char
 dot = P.char '.'
@@ -256,3 +263,6 @@ kwWildcard = symbol Str.underscore
 
 ghc :: MonadParsec e Text m => m ()
 ghc = symbol Str.ghc
+
+agda :: MonadParsec e Text m => m ()
+agda = symbol Str.agda

src/MiniJuvix/Syntax/Concrete/Loc.hs

@@ -12,8 +12,8 @@ instance Semigroup Pos where
 instance Monoid Pos where
   mempty = Pos 0
 
-data FileLoc = FileLoc {
-  -- | Line number
+data FileLoc = FileLoc
+  { -- | Line number
     _locLine :: !Pos,
     -- | Column number
     _locCol :: !Pos
@@ -32,10 +32,10 @@ data Loc = Loc
   deriving stock (Show, Eq, Ord)
 
 -- | Inclusive interval
-data Interval = Interval {
-  _intFile :: FilePath,
-  _intStart :: FileLoc,
-  _intEnd :: FileLoc
+data Interval = Interval
+  { _intFile :: FilePath,
+    _intStart :: FileLoc,
+    _intEnd :: FileLoc
   }
   deriving stock (Show, Ord, Eq)
 
@@ -56,7 +56,7 @@ instance Pretty Pos where
 
 instance Pretty FileLoc where
   pretty :: FileLoc -> Doc a
-  pretty FileLoc {..}  =
+  pretty FileLoc {..} =
     pretty _locLine <> colon <> pretty _locCol
 
 instance Pretty Loc where
@@ -68,14 +68,15 @@ instance Pretty Interval where
   pretty :: Interval -> Doc a
   pretty Interval {..} =
     pretty _intFile <> colon
-    <> ppPosRange (_locLine _intStart, _locLine _intEnd) <> colon
-    <> ppPosRange (_locCol _intStart, _locCol _intEnd)
+      <> ppPosRange (_locLine _intStart, _locLine _intEnd)
+      <> colon
+      <> ppPosRange (_locCol _intStart, _locCol _intEnd)
     where
-    hyphen = pretty '-'
-    ppPosRange :: (Pos, Pos) -> Doc a
-    ppPosRange (s, e)
-      | s == e = pretty s
-      | otherwise = pretty s <> hyphen <> pretty e
+      hyphen = pretty '-'
+      ppPosRange :: (Pos, Pos) -> Doc a
+      ppPosRange (s, e)
+        | s == e = pretty s
+        | otherwise = pretty s <> hyphen <> pretty e
 
 makeLenses ''Interval
 makeLenses ''Loc

src/MiniJuvix/Syntax/Concrete/ModuleIsTop.hs

@@ -0,0 +1,10 @@
+{-# LANGUAGE StandaloneKindSignatures #-}
+
+module MiniJuvix.Syntax.Concrete.ModuleIsTop where
+
+import MiniJuvix.Prelude
+
+data ModuleIsTop = ModuleTop | ModuleLocal
+  deriving stock (Eq, Ord, Show)
+
+$(genSingletons [''ModuleIsTop])

src/MiniJuvix/Syntax/Concrete/Name.hs

@@ -1,14 +1,15 @@
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
+
 module MiniJuvix.Syntax.Concrete.Name where
 
+import qualified Data.List.NonEmpty.Extra as NonEmpty
 import MiniJuvix.Prelude
 import MiniJuvix.Syntax.Concrete.Loc
-import qualified Data.List.NonEmpty.Extra as NonEmpty
 import Prettyprinter
 
-data Symbol = Symbol {
-  _symbolText :: Text,
-  _symbolLoc :: Interval
+data Symbol = Symbol
+  { _symbolText :: Text,
+    _symbolLoc :: Interval
   }
   deriving stock (Show)
 
@@ -77,16 +78,22 @@ instance HasLoc TopModulePath where
 topModulePathToFilePath :: FilePath -> TopModulePath -> FilePath
 topModulePathToFilePath = topModulePathToFilePath' (Just ".mjuvix")
 
-topModulePathToFilePath'
-  :: Maybe String -> FilePath -> TopModulePath -> FilePath
+topModulePathToFilePath' ::
+  Maybe String -> FilePath -> TopModulePath -> FilePath
 topModulePathToFilePath' ext root mp = absPath
   where
-  relDirPath = foldr ((</>) . toPath) mempty (_modulePathDir mp)
-  relFilePath = relDirPath </> toPath (_modulePathName mp)
-  absPath = case ext of
-    Nothing -> root </> relFilePath
-    Just e -> root </> relFilePath <.> e
-  toPath :: Symbol -> FilePath
-  toPath Symbol{..} = unpack _symbolText
+    relDirPath = foldr ((</>) . toPath) mempty (_modulePathDir mp)
+    relFilePath = relDirPath </> toPath (_modulePathName mp)
+    absPath = case ext of
+      Nothing -> root </> relFilePath
+      Just e -> root </> relFilePath <.> e
+    toPath :: Symbol -> FilePath
+    toPath Symbol {..} = unpack _symbolText
+
+topModulePathToDottedPath :: IsString s => TopModulePath -> s
+topModulePathToDottedPath (TopModulePath l r) =
+  fromText $ mconcat $ intersperse "." $ map fromSymbol $ l ++ [r]
+  where
+    fromSymbol Symbol {..} = _symbolText
 
 instance Hashable TopModulePath

src/MiniJuvix/Syntax/Concrete/Parser.hs

@@ -6,11 +6,11 @@ import qualified Data.List.NonEmpty.Extra as NonEmpty
 import Data.Singletons
 import qualified Data.Text as Text
 import qualified Data.Text.IO as Text
+import MiniJuvix.Prelude
 import MiniJuvix.Syntax.Concrete.Base (MonadParsec)
 import qualified MiniJuvix.Syntax.Concrete.Base as P
 import MiniJuvix.Syntax.Concrete.Language
 import MiniJuvix.Syntax.Concrete.Lexer hiding (symbol)
-import MiniJuvix.Prelude
 
 --------------------------------------------------------------------------------
 -- Running the parser
@@ -78,7 +78,6 @@ statement =
     <|> (StatementInductive <$> inductiveDef)
     <|> (StatementPrint <$> printS)
     <|> (StatementForeign <$> foreignBlock)
-    <|> (StatementCompile <$> compileDef)
     <|> (StatementModule <$> moduleDef)
     <|> (StatementAxiom <$> axiomDef)
     <|> ( either StatementTypeSignature StatementFunctionClause
@@ -86,11 +85,12 @@ statement =
         )
 
 --------------------------------------------------------------------------------
--- Foreign and compile
+-- Foreign
 --------------------------------------------------------------------------------
 
 backend :: forall e m. MonadParsec e Text m => m Backend
 backend = ghc $> BackendGhc
+  <|> agda $> BackendAgda
 
 foreignBlock :: forall e m. MonadParsec e Text m => m ForeignBlock
 foreignBlock = do
@@ -99,14 +99,6 @@ foreignBlock = do
   _foreignCode <- bracedString
   return ForeignBlock {..}
 
-compileDef :: forall e m. MonadParsec e Text m => m (CompileDef 'Parsed)
-compileDef = do
-  kwCompile
-  _compileAxiom <- symbol
-  _compileBackend <- backend
-  _compileCode <- string
-  return CompileDef {..}
-
 --------------------------------------------------------------------------------
 -- Operator syntax declaration
 --------------------------------------------------------------------------------
@@ -147,7 +139,7 @@ import_ = do
 expressionAtom :: MonadParsec e Text m => m (ExpressionAtom 'Parsed)
 expressionAtom =
   do
-     AtomLiteral <$> P.try literal
+    AtomLiteral <$> P.try literal
     <|> AtomIdentifier <$> name
     <|> (AtomUniverse <$> universe)
     <|> (AtomLambda <$> lambda)
@@ -166,8 +158,8 @@ expressionAtoms = ExpressionAtoms <$> P.some expressionAtom
 
 literal :: MonadParsec e Text m => m Literal
 literal =
-      LitInteger <$> integer
-  <|> LitString <$> string
+  LitInteger <$> integer
+    <|> LitString <$> string
 
 --------------------------------------------------------------------------------
 -- Match expression
@@ -250,7 +242,15 @@ axiomDef = do
   _axiomName <- symbol
   kwColon
   _axiomType <- expressionAtoms
+  _axiomBackendItems <- fromMaybe [] <$> optional backends
   return AxiomDef {..}
+  where
+    backends = toList <$> braces (P.sepEndBy1 backendItem kwSemicolon)
+    backendItem = do
+      _backendItemBackend <- backend
+      kwMapsTo
+      _backendItemCode <- string
+      return BackendItem {..}
 
 --------------------------------------------------------------------------------
 -- Function expression
@@ -319,7 +319,7 @@ lambdaClause = do
 lambda :: MonadParsec e Text m => m (Lambda 'Parsed)
 lambda = do
   kwLambda
-  lambdaClauses ← braces (P.sepEndBy lambdaClause kwSemicolon)
+  lambdaClauses <- braces (P.sepEndBy lambdaClause kwSemicolon)
   return Lambda {..}
 
 -------------------------------------------------------------------------------
@@ -344,9 +344,9 @@ inductiveParam = parens $ do
 
 constructorDef :: MonadParsec e Text m => m (InductiveConstructorDef 'Parsed)
 constructorDef = do
-  constructorName <- symbol
+  _constructorName <- symbol
   kwColon
-  constructorType <- expressionAtoms
+  _constructorType <- expressionAtoms
   return InductiveConstructorDef {..}
 
 --------------------------------------------------------------------------------
@@ -355,7 +355,7 @@ constructorDef = do
 
 patternAtom :: forall e m. MonadParsec e Text m => m (PatternAtom 'Parsed)
 patternAtom =
-  PatternAtomName <$> name
+  PatternAtomIden <$> name
     <|> PatternAtomWildcard <$ kwWildcard
     <|> (PatternAtomParens <$> parens patternAtoms)
 
@@ -415,16 +415,16 @@ atomicExpression = do
 openModule :: forall e m. MonadParsec e Text m => m (OpenModule 'Parsed)
 openModule = do
   kwOpen
-  openModuleName <- name
-  openParameters <- many atomicExpression
-  openUsingHiding <- optional usingOrHiding
-  openPublic <- maybe NoPublic (const Public) <$> optional kwPublic
+  _openModuleName <- name
+  _openParameters <- many atomicExpression
+  _openUsingHiding <- optional usingOrHiding
+  _openPublic <- maybe NoPublic (const Public) <$> optional kwPublic
   return OpenModule {..}
   where
-  usingOrHiding :: m UsingHiding
-  usingOrHiding =
-    (kwUsing >> (Using <$> symbolList))
-     <|> (kwHiding >> (Hiding <$> symbolList))
+    usingOrHiding :: m UsingHiding
+    usingOrHiding =
+      (kwUsing >> (Using <$> symbolList))
+        <|> (kwHiding >> (Hiding <$> symbolList))
 
 --------------------------------------------------------------------------------
 -- Debugging statements

src/MiniJuvix/Syntax/Concrete/PublicAnn.hs

@@ -2,9 +2,9 @@ module MiniJuvix.Syntax.Concrete.PublicAnn where
 
 import MiniJuvix.Prelude
 
-data PublicAnn =
-  -- | Explicit public annotation
-  Public
-  -- | No annotation. Do not confuse this with 'not public' or 'private'.
-  | NoPublic
+data PublicAnn
+  = -- | Explicit public annotation
+    Public
+  | -- | No annotation. Do not confuse this with 'not public' or 'private'.
+    NoPublic
   deriving stock (Show, Eq, Ord)

src/MiniJuvix/Syntax/Concrete/Scoped/Error.hs

@@ -1,13 +1,14 @@
-module MiniJuvix.Syntax.Concrete.Scoped.Error (
-  module MiniJuvix.Syntax.Concrete.Scoped.Error.Types,
-  module MiniJuvix.Syntax.Concrete.Scoped.Error,
-  module MiniJuvix.Syntax.Concrete.Scoped.Error.Pretty
-  ) where
+module MiniJuvix.Syntax.Concrete.Scoped.Error
+  ( module MiniJuvix.Syntax.Concrete.Scoped.Error.Types,
+    module MiniJuvix.Syntax.Concrete.Scoped.Error,
+    module MiniJuvix.Syntax.Concrete.Scoped.Error.Pretty,
+  )
+where
 
-import MiniJuvix.Syntax.Concrete.Scoped.Error.Types
 import MiniJuvix.Prelude
 import MiniJuvix.Syntax.Concrete.Scoped.Error.Pretty
 import qualified MiniJuvix.Syntax.Concrete.Scoped.Error.Pretty as P
+import MiniJuvix.Syntax.Concrete.Scoped.Error.Types
 import Prettyprinter
 
 -- | An error that happens during scope checking. Note that it is defined here
@@ -30,14 +31,11 @@ data ScopeError
   | ErrAmbiguousModuleSym AmbiguousModuleSym
   | ErrUnusedOperatorDef UnusedOperatorDef
   | ErrWrongTopModuleName WrongTopModuleName
-  -- | Eventually this needs to go away
-  | ErrGeneric Text
   deriving stock (Show)
 
 ppScopeError :: ScopeError -> Doc Eann
 ppScopeError s = case s of
   ErrParser txt -> ppError txt
-  ErrGeneric txt -> pretty txt
   ErrInfixParser e -> ppError e
   ErrInfixPattern e -> ppError e
   ErrMultipleDeclarations e -> ppError e

src/MiniJuvix/Syntax/Concrete/Scoped/Error/Pretty.hs

@@ -1,10 +1,10 @@
-module MiniJuvix.Syntax.Concrete.Scoped.Error.Pretty (
-  module MiniJuvix.Syntax.Concrete.Scoped.Error.Pretty.Base,
-  module MiniJuvix.Syntax.Concrete.Scoped.Error.Pretty.Ansi,
-  module MiniJuvix.Syntax.Concrete.Scoped.Error.Pretty.Text
-  ) where
+module MiniJuvix.Syntax.Concrete.Scoped.Error.Pretty
+  ( module MiniJuvix.Syntax.Concrete.Scoped.Error.Pretty.Base,
+    module MiniJuvix.Syntax.Concrete.Scoped.Error.Pretty.Ansi,
+    module MiniJuvix.Syntax.Concrete.Scoped.Error.Pretty.Text,
+  )
+where
 
+import MiniJuvix.Syntax.Concrete.Scoped.Error.Pretty.Ansi
 import MiniJuvix.Syntax.Concrete.Scoped.Error.Pretty.Base
 import MiniJuvix.Syntax.Concrete.Scoped.Error.Pretty.Text
-import MiniJuvix.Syntax.Concrete.Scoped.Error.Pretty.Ansi
-

src/MiniJuvix/Syntax/Concrete/Scoped/Error/Pretty/Ansi.hs

@@ -1,9 +1,11 @@
 module MiniJuvix.Syntax.Concrete.Scoped.Error.Pretty.Ansi where
 
-import Prettyprinter
 import MiniJuvix.Prelude
-import Prettyprinter.Render.Terminal
 import MiniJuvix.Syntax.Concrete.Scoped.Error.Pretty.Base
+import qualified MiniJuvix.Syntax.Concrete.Scoped.Pretty.Ansi as S
+
+import Prettyprinter
+import Prettyprinter.Render.Terminal
 
 renderAnsi :: SimpleDocStream Eann -> Text
 renderAnsi = renderStrict . reAnnotateS stylize
@@ -11,3 +13,4 @@ renderAnsi = renderStrict . reAnnotateS stylize
 stylize :: Eann -> AnsiStyle
 stylize a = case a of
   Highlight -> colorDull Red
+  ScopedAnn s -> S.stylize s

src/MiniJuvix/Syntax/Concrete/Scoped/Error/Pretty/Base.hs

@@ -1,17 +1,19 @@
 module MiniJuvix.Syntax.Concrete.Scoped.Error.Pretty.Base where
 
-import Prettyprinter
+import qualified Data.HashMap.Strict as HashMap
+import qualified Data.HashSet as HashSet
+import qualified Data.List.NonEmpty.Extra as NonEmpty
 import MiniJuvix.Prelude
+import qualified MiniJuvix.Syntax.Concrete.Language as L
 import MiniJuvix.Syntax.Concrete.Scoped.Error.Types
+import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
 import qualified MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base as P
 import MiniJuvix.Syntax.Concrete.Scoped.Scope
-import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
+import Prettyprinter
 import Text.EditDistance
-import qualified Data.HashSet as HashSet
-import qualified Data.HashMap.Strict as HashMap
-import qualified Data.List.NonEmpty.Extra as NonEmpty
 
 data Eann = Highlight
+  | ScopedAnn P.Ann
 
 highlight :: Doc Eann -> Doc Eann
 highlight = annotate Highlight
@@ -20,15 +22,17 @@ ppSymbolT :: Text -> Doc Eann
 ppSymbolT = highlight . pretty
 
 ppCode :: P.PrettyCode c => c -> Doc Eann
-ppCode = unAnnotate . P.runPrettyCode P.defaultOptions
+ppCode = reAnnotate ScopedAnn . P.runPrettyCode P.defaultOptions
 
 indent' :: Doc ann -> Doc ann
 indent' = indent 2
 
 textDistance :: Text -> Text -> Int
 textDistance a b =
-  restrictedDamerauLevenshteinDistance defaultEditCosts
-  (unpack a) (unpack b)
+  restrictedDamerauLevenshteinDistance
+    defaultEditCosts
+    (unpack a)
+    (unpack b)
 
 class PrettyError e where
   ppError :: e -> Doc Eann
@@ -36,9 +40,9 @@ class PrettyError e where
 instance PrettyError MultipleDeclarations where
   ppError MultipleDeclarations {..} =
     "Multiple declarations of" <+> ppSymbolT _multipleDeclSymbol <> line
-    <> "Declared at:" <+> align (vsep ints)
+      <> "Declared at:" <+> align (vsep ints)
     where
-    ints = map pretty [S._nameDefined _multipleDeclEntry, _multipleDeclSecond]
+      ints = map pretty [S._nameDefined (L.symbolEntryToSName _multipleDeclEntry), _multipleDeclSecond]
 
 instance PrettyError InfixError where
   ppError InfixError {..} =
@@ -55,69 +59,74 @@ infixErrorAux kind pp =
 
 instance PrettyError LacksFunctionClause where
   ppError LacksFunctionClause {..} =
-     pretty loc <> line <>
-     "There is a type signature with no function clause:" <> line
-     <> indent' (highlight (ppCode _lacksFunctionClause))
+    pretty loc <> line
+      <> "There is a type signature with no function clause:"
+      <> line
+      <> indent' (highlight (ppCode _lacksFunctionClause))
     where
-    loc = getLoc $ _sigName _lacksFunctionClause
+      loc = getLoc $ _sigName _lacksFunctionClause
 
 instance PrettyError LacksTypeSig where
   ppError LacksTypeSig {..} =
-     pretty loc <> line <>
-     "There is a declaration with a missing type signature:" <> line
-     <> indent' (highlight (ppCode _lacksTypeSigClause))
+    pretty loc <> line
+      <> "There is a declaration with a missing type signature:"
+      <> line
+      <> indent' (highlight (ppCode _lacksTypeSigClause))
     where
-    loc = getLoc $ _clauseOwnerFunction _lacksTypeSigClause
+      loc = getLoc $ _clauseOwnerFunction _lacksTypeSigClause
 
 instance PrettyError ImportCycle where
   ppError ImportCycle {..} =
     "There is an import cycle:" <> line
-    <> indent' lst
+      <> indent' lst
     where
-    lst = vsep $ intersperse "⇓" (map pp (toList (tie _importCycleImports)))
-    pp :: Import 'Parsed -> Doc Eann
-    pp t = ppCode t <+> parens ("at" <+> pretty (getLoc t))
-    tie :: NonEmpty a -> NonEmpty a
-    tie x = x <> pure (NonEmpty.head x)
+      lst = vsep $ intersperse "⇓" (map pp (toList (tie _importCycleImports)))
+      pp :: Import 'Parsed -> Doc Eann
+      pp t = ppCode t <+> parens ("at" <+> pretty (getLoc t))
+      tie :: NonEmpty a -> NonEmpty a
+      tie x = x <> pure (NonEmpty.head x)
 
 instance PrettyError NotInScope where
   ppError NotInScope {..} =
-    pretty loc <> line <>
-    "Symbol not in scope:" <+> highlight (ppCode _notInScopeSymbol)  <?>
-    ((line <>) <$> suggestion)
+    pretty loc <> line
+      <> "Symbol not in scope:" <+> highlight (ppCode _notInScopeSymbol)
+      <?> ((line <>) <$> suggestion)
     where
-    suggestion
-       | null suggestions = Nothing
-       | otherwise = Just $ "Perhaps you meant:" <+> align (vsep suggestions)
-    loc = getLoc _notInScopeSymbol
-    sym = _symbolText _notInScopeSymbol
-    maxDist :: Int
-    maxDist = 2
-    suggestions :: [Doc a]
-    suggestions =
+      suggestion
+        | null suggestions = Nothing
+        | otherwise = Just $ "Perhaps you meant:" <+> align (vsep suggestions)
+      loc = getLoc _notInScopeSymbol
+      sym = _symbolText _notInScopeSymbol
+      maxDist :: Int
+      maxDist = 2
+      suggestions :: [Doc a]
+      suggestions =
         map (pretty . fst) $
-        sortOn snd
-        [ (c, dist)  | c <- toList candidates
-          , let dist =  textDistance sym c, dist <= maxDist ]
-    candidates :: HashSet Text
-    candidates = HashSet.fromList (map _symbolText (HashMap.keys $ _localVars _notInScopeLocal)) <>
-      HashSet.fromList (map _symbolText (HashMap.keys $ _scopeSymbols _notInScopeScope))
+          sortOn
+            snd
+            [ (c, dist) | c <- toList candidates, let dist = textDistance sym c, dist <= maxDist
+            ]
+      candidates :: HashSet Text
+      candidates =
+        HashSet.fromList (map _symbolText (HashMap.keys $ _localVars _notInScopeLocal))
+          <> HashSet.fromList (map _symbolText (HashMap.keys $ _scopeSymbols _notInScopeScope))
 
 instance PrettyError BindGroupConflict where
   ppError BindGroupConflict {..} =
     "The symbol" <+> highlight (ppCode _bindGroupFirst)
-      <+> "appears twice in the same binding group:" <> line
-    <> indent' (align locs)
+      <+> "appears twice in the same binding group:"
+      <> line
+      <> indent' (align locs)
     where
-      locs = vsep $ map (pretty . getLoc) [_bindGroupFirst , _bindGroupSecond]
+      locs = vsep $ map (pretty . getLoc) [_bindGroupFirst, _bindGroupSecond]
 
 instance PrettyError DuplicateFixity where
   ppError DuplicateFixity {..} =
     "Multiple fixity declarations for symbol" <+> highlight (ppCode sym) <> ":" <> line
-     <> indent' (align locs)
+      <> indent' (align locs)
     where
       sym = opSymbol _dupFixityFirst
-      locs = vsep $ map (pretty . getLoc) [_dupFixityFirst , _dupFixityFirst]
+      locs = vsep $ map (pretty . getLoc) [_dupFixityFirst, _dupFixityFirst]
 
 instance PrettyError MultipleExportConflict where
   ppError MultipleExportConflict {..} =
@@ -134,19 +143,26 @@ instance PrettyError MegaParsecError where
 instance PrettyError WrongTopModuleName where
   ppError WrongTopModuleName {..} =
     "The top module" <+> ppCode _wrongTopModuleNameActualName <+> "is defined in the file:" <> line
-    <> highlight (pretty _wrongTopModuleNameActualPath) <> line
-    <> "But it should be in the file:" <> line
-    <> pretty _wrongTopModuleNameExpectedPath
+      <> highlight (pretty _wrongTopModuleNameActualPath)
+      <> line
+      <> "But it should be in the file:"
+      <> line
+      <> pretty _wrongTopModuleNameExpectedPath
 
 instance PrettyError UnusedOperatorDef where
   ppError UnusedOperatorDef {..} =
     "Unused operator syntax definition:" <> line
-    <> ppCode _unusedOperatorDef
+      <> ppCode _unusedOperatorDef
 
 instance PrettyError AmbiguousSym where
-  ppError AmbiguousSym {} =
-    "TODO Ambiguous symbol"
+  ppError AmbiguousSym {..} = ambiguousMessage _ambiguousSymName _ambiguousSymEntires
 
 instance PrettyError AmbiguousModuleSym where
-  ppError AmbiguousModuleSym {} =
-    "TODO Ambiguous module symbol"
+  ppError AmbiguousModuleSym {..} = ambiguousMessage _ambiguousModName _ambiguousModSymEntires
+
+ambiguousMessage :: Name -> [SymbolEntry] -> Doc Eann
+ambiguousMessage n es =
+    "The symbol" <+> ppCode n <+> "at" <+> pretty (getLoc n) <+> "is ambiguous." <> line
+      <> "It could be any of:"
+      <> line
+      <> indent' (vsep (map ppCode es))

src/MiniJuvix/Syntax/Concrete/Scoped/Error/Pretty/Text.hs

@@ -1,8 +1,8 @@
 module MiniJuvix.Syntax.Concrete.Scoped.Error.Pretty.Text where
 
-import Prettyprinter
 import MiniJuvix.Prelude
 import MiniJuvix.Syntax.Concrete.Scoped.Error.Pretty.Base
+import Prettyprinter
 import Prettyprinter.Render.Text
 
 renderText :: SimpleDocStream Eann -> Text

src/MiniJuvix/Syntax/Concrete/Scoped/Error/Types.hs

@@ -1,104 +1,107 @@
-module MiniJuvix.Syntax.Concrete.Scoped.Error.Types (
-  module MiniJuvix.Syntax.Concrete.Language,
-  module MiniJuvix.Syntax.Concrete.Scoped.Error.Types
-                                                    ) where
+module MiniJuvix.Syntax.Concrete.Scoped.Error.Types
+  ( module MiniJuvix.Syntax.Concrete.Language,
+    module MiniJuvix.Syntax.Concrete.Scoped.Error.Types,
+  )
+where
 
 import MiniJuvix.Prelude
 import MiniJuvix.Syntax.Concrete.Language
-import MiniJuvix.Syntax.Concrete.Scoped.Scope
 import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
+import MiniJuvix.Syntax.Concrete.Scoped.Scope
 
-data MultipleDeclarations = MultipleDeclarations {
-  _multipleDeclEntry :: SymbolEntry,
-  _multipleDeclSymbol :: Text,
-  _multipleDeclSecond :: Interval
+data MultipleDeclarations = MultipleDeclarations
+  { _multipleDeclEntry :: SymbolEntry,
+    _multipleDeclSymbol :: Text,
+    _multipleDeclSecond :: Interval
   }
- deriving stock (Show)
+  deriving stock (Show)
 
 -- | megaparsec error while resolving infixities.
-newtype InfixError = InfixError {
-  _infixErrAtoms :: ExpressionAtoms 'Scoped
+newtype InfixError = InfixError
+  { _infixErrAtoms :: ExpressionAtoms 'Scoped
   }
- deriving stock (Show)
+  deriving stock (Show)
 
 -- | megaparsec error while resolving infixities of patterns.
-newtype InfixErrorP = InfixErrorP {
-  _infixErrAtomsP :: PatternAtom 'Scoped
+newtype InfixErrorP = InfixErrorP
+  { _infixErrAtomsP :: PatternAtom 'Scoped
   }
- deriving stock (Show)
+  deriving stock (Show)
 
 -- | function clause without a type signature.
-newtype LacksTypeSig = LacksTypeSig {
-  _lacksTypeSigClause :: FunctionClause 'Parsed
+newtype LacksTypeSig = LacksTypeSig
+  { _lacksTypeSigClause :: FunctionClause 'Parsed
   }
- deriving stock (Show)
+  deriving stock (Show)
 
 -- | type signature without a function clause
-newtype LacksFunctionClause = LacksFunctionClause {
-  _lacksFunctionClause :: TypeSignature 'Scoped
+newtype LacksFunctionClause = LacksFunctionClause
+  { _lacksFunctionClause :: TypeSignature 'Scoped
   }
- deriving stock (Show)
+  deriving stock (Show)
 
-newtype ImportCycle = ImportCycle {
-  -- | If we have [a, b, c] it means that a import b imports c imports a.
-  _importCycleImports :: NonEmpty (Import 'Parsed)
+newtype ImportCycle = ImportCycle
+  { -- | If we have [a, b, c] it means that a import b imports c imports a.
+    _importCycleImports :: NonEmpty (Import 'Parsed)
   }
- deriving stock (Show)
+  deriving stock (Show)
 
-data BindGroupConflict = BindGroupConflict {
- _bindGroupFirst :: Symbol,
- _bindGroupSecond :: Symbol
- }
- deriving stock (Show)
-
-data DuplicateFixity = DuplicateFixity {
- _dupFixityFirst :: OperatorSyntaxDef,
- _dupFixitySecond :: OperatorSyntaxDef
- }
- deriving stock (Show)
-
-data MultipleExportConflict = MultipleExportConflict {
-  _multipleExportModule :: S.AbsModulePath,
-  _multipleExportSymbol :: Symbol,
-  _multipleExportEntries :: NonEmpty SymbolEntry
+data BindGroupConflict = BindGroupConflict
+  { _bindGroupFirst :: Symbol,
+    _bindGroupSecond :: Symbol
   }
- deriving stock (Show)
+  deriving stock (Show)
 
-data NotInScope = NotInScope {
- _notInScopeSymbol :: Symbol,
- _notInScopeLocal :: LocalVars,
- _notInScopeScope :: Scope
- }
- deriving stock (Show)
-
-newtype ModuleNotInScope = ModuleNotInScope {
-  _moduleNotInScopeName :: Name
+data DuplicateFixity = DuplicateFixity
+  { _dupFixityFirst :: OperatorSyntaxDef,
+    _dupFixitySecond :: OperatorSyntaxDef
   }
- deriving stock (Show)
+  deriving stock (Show)
 
-newtype MegaParsecError = MegaParsecError {
-  _megaParsecError :: Text
+data MultipleExportConflict = MultipleExportConflict
+  { _multipleExportModule :: S.AbsModulePath,
+    _multipleExportSymbol :: Symbol,
+    _multipleExportEntries :: NonEmpty SymbolEntry
   }
- deriving stock (Show)
+  deriving stock (Show)
 
-newtype UnusedOperatorDef = UnusedOperatorDef {
-  _unusedOperatorDef :: OperatorSyntaxDef
+data NotInScope = NotInScope
+  { _notInScopeSymbol :: Symbol,
+    _notInScopeLocal :: LocalVars,
+    _notInScopeScope :: Scope
   }
- deriving stock (Show)
+  deriving stock (Show)
 
-data WrongTopModuleName = WrongTopModuleName {
-  _wrongTopModuleNameExpectedPath :: FilePath,
-  _wrongTopModuleNameActualPath :: FilePath,
-  _wrongTopModuleNameActualName :: TopModulePath
+newtype ModuleNotInScope = ModuleNotInScope
+  { _moduleNotInScopeName :: Name
   }
- deriving stock (Show)
+  deriving stock (Show)
 
-newtype AmbiguousSym = AmbiguousSym {
-  _ambiguousSymEntires :: [SymbolEntry]
+newtype MegaParsecError = MegaParsecError
+  { _megaParsecError :: Text
   }
- deriving stock (Show)
+  deriving stock (Show)
 
-newtype AmbiguousModuleSym = AmbiguousModuleSym {
-  _ambiguousModSymEntires :: [SymbolEntry]
+newtype UnusedOperatorDef = UnusedOperatorDef
+  { _unusedOperatorDef :: OperatorSyntaxDef
   }
- deriving stock (Show)
+  deriving stock (Show)
+
+data WrongTopModuleName = WrongTopModuleName
+  { _wrongTopModuleNameExpectedPath :: FilePath,
+    _wrongTopModuleNameActualPath :: FilePath,
+    _wrongTopModuleNameActualName :: TopModulePath
+  }
+  deriving stock (Show)
+
+data AmbiguousSym = AmbiguousSym
+  { _ambiguousSymName :: Name,
+    _ambiguousSymEntires :: [SymbolEntry]
+  }
+  deriving stock (Show)
+
+data AmbiguousModuleSym = AmbiguousModuleSym
+  { _ambiguousModName :: Name,
+    _ambiguousModSymEntires :: [SymbolEntry]
+  }
+  deriving stock (Show)

src/MiniJuvix/Syntax/Concrete/Scoped/Name.hs

@@ -1,22 +1,29 @@
-module MiniJuvix.Syntax.Concrete.Scoped.Name (
-module MiniJuvix.Syntax.Concrete.Scoped.Name,
-module MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind
-                                             ) where
+{-# LANGUAGE StandaloneKindSignatures #-}
+
+module MiniJuvix.Syntax.Concrete.Scoped.Name
+  ( module MiniJuvix.Syntax.Concrete.Scoped.Name,
+    module MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind,
+  )
+where
 
 import Data.Stream (Stream (Cons))
 import Lens.Micro.Platform
-import qualified MiniJuvix.Syntax.Fixity as C
-import qualified MiniJuvix.Syntax.Concrete.Name as C
-import MiniJuvix.Syntax.Concrete.Loc
 import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Concrete.Loc
+import qualified MiniJuvix.Syntax.Concrete.Name as C
+import MiniJuvix.Syntax.Concrete.Scoped.VisibilityAnn
 import MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind
-import MiniJuvix.Syntax.Concrete.PublicAnn
+import qualified MiniJuvix.Syntax.Fixity as C
 import Prettyprinter
 
 --------------------------------------------------------------------------------
 -- Names
 --------------------------------------------------------------------------------
 
+data IsConcrete = NotConcrete | Concrete
+
+$(genSingletons [''IsConcrete])
+
 newtype NameId = NameId Word64
   deriving stock (Show, Eq, Ord, Generic)
 
@@ -58,13 +65,13 @@ allNameIds = NameId <$> ids
 instance Hashable NameId
 
 -- | Why a symbol is in scope.
-data WhyInScope =
-  -- | Inherited from the parent module.
-  BecauseInherited WhyInScope
-  -- | Opened or imported in this module.
-  | BecauseImportedOpened
-  -- | Defined in this module.
-  | BecauseDefined
+data WhyInScope
+  = -- | Inherited from the parent module.
+    BecauseInherited WhyInScope
+  | -- | Opened or imported in this module.
+    BecauseImportedOpened
+  | -- | Defined in this module.
+    BecauseDefined
   deriving stock (Show)
 
 type Name = Name' C.Name
@@ -76,17 +83,19 @@ type TopModulePath = Name' C.TopModulePath
 type ModuleNameId = NameId
 
 data Name' n = Name'
-  {
-    _nameConcrete :: n,
+  { _nameConcrete :: n,
     _nameId :: NameId,
     _nameDefined :: Interval,
     _nameKind :: NameKind,
     _nameDefinedIn :: AbsModulePath,
     _nameFixity :: Maybe C.Fixity,
     _nameWhyInScope :: WhyInScope,
-    _namePublicAnn :: PublicAnn
+    _nameVisibilityAnn :: VisibilityAnn,
+    -- | The textual representation of the name at the binding site
+    _nameVerbatim :: Text
   }
   deriving stock (Show)
+
 makeLenses ''Name'
 
 instance HasNameKind (Name' n) where
@@ -112,12 +121,15 @@ topModulePathName = over nameConcrete C._modulePathName
 symbolText :: Symbol -> Text
 symbolText = C._symbolText . _nameConcrete
 
+unqualifiedSymbol :: Symbol -> Name
+unqualifiedSymbol = over nameConcrete C.NameUnqualified
+
 nameUnqualify :: Name -> Symbol
 nameUnqualify Name' {..} = Name' {_nameConcrete = unqual, ..}
   where
-  unqual = case _nameConcrete of
-       C.NameUnqualified s -> s
-       C.NameQualified q -> fromQualifiedName q
+    unqual = case _nameConcrete of
+      C.NameUnqualified s -> s
+      C.NameQualified q -> fromQualifiedName q
 
 instance Eq (Name' n) where
   (==) = (==) `on` _nameId

src/MiniJuvix/Syntax/Concrete/Scoped/Name/NameKind.hs

@@ -28,13 +28,13 @@ instance HasNameKind NameKind where
 
 isExprKind :: HasNameKind a => a -> Bool
 isExprKind k = case getNameKind k of
-    KNameConstructor -> True
-    KNameInductive -> True
-    KNameFunction -> True
-    KNameLocal -> True
-    KNameAxiom -> True
-    KNameLocalModule -> False
-    KNameTopModule -> False
+  KNameConstructor -> True
+  KNameInductive -> True
+  KNameFunction -> True
+  KNameLocal -> True
+  KNameAxiom -> True
+  KNameLocalModule -> False
+  KNameTopModule -> False
 
 isModuleKind :: HasNameKind a => a -> Bool
 isModuleKind k = case getNameKind k of
@@ -54,10 +54,10 @@ canHaveFixity k = case getNameKind k of
 
 nameKindAnsi :: NameKind -> AnsiStyle
 nameKindAnsi k = case k of
-    KNameConstructor -> colorDull Magenta
-    KNameInductive -> colorDull Green
-    KNameAxiom -> colorDull Red
-    KNameLocalModule -> mempty
-    KNameFunction -> colorDull Yellow
-    KNameLocal -> mempty
-    KNameTopModule -> mempty
+  KNameConstructor -> colorDull Magenta
+  KNameInductive -> colorDull Green
+  KNameAxiom -> colorDull Red
+  KNameLocalModule -> color Cyan
+  KNameFunction -> colorDull Yellow
+  KNameLocal -> mempty
+  KNameTopModule -> color Cyan

src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Ann.hs

@@ -1,7 +1,7 @@
 module MiniJuvix.Syntax.Concrete.Scoped.Pretty.Ann where
 
-import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
 import MiniJuvix.Syntax.Concrete.Language (TopModulePath)
+import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
 
 data Ann
   = AnnKind S.NameKind

src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Ansi.hs

@@ -1,8 +1,8 @@
 module MiniJuvix.Syntax.Concrete.Scoped.Pretty.Ansi where
 
+import MiniJuvix.Prelude
 import MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind
 import MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base
-import MiniJuvix.Prelude
 import Prettyprinter
 import Prettyprinter.Render.Terminal
 
@@ -19,8 +19,11 @@ renderPrettyCode :: PrettyCode c => Options -> c -> Text
 renderPrettyCode opts = renderStrict . docStream opts
 
 docStream :: PrettyCode c => Options -> c -> SimpleDocStream AnsiStyle
-docStream opts = reAnnotateS stylize . layoutPretty defaultLayoutOptions
-    . run . runReader opts . ppCode
+docStream opts =
+  reAnnotateS stylize . layoutPretty defaultLayoutOptions
+    . run
+    . runReader opts
+    . ppCode
 
 stylize :: Ann -> AnsiStyle
 stylize a = case a of

src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Base.hs

@@ -1,29 +1,28 @@
-module MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base (
-  module MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base,
-  module MiniJuvix.Syntax.Concrete.Scoped.Pretty.Ann
-                                                    ) where
+module MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base
+  ( module MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base,
+    module MiniJuvix.Syntax.Concrete.Scoped.Pretty.Ann,
+  )
+where
 
-import MiniJuvix.Syntax.Concrete.Language
-import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
-import MiniJuvix.Prelude
 import qualified Data.List.NonEmpty.Extra as NonEmpty
-import Prettyprinter hiding (braces, parens)
-import MiniJuvix.Syntax.Concrete.Scoped.Pretty.Ann
-import MiniJuvix.Syntax.Concrete.Scoped.Name (AbsModulePath)
 import MiniJuvix.Internal.Strings as Str
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Concrete.Language
+import MiniJuvix.Syntax.Concrete.Scoped.Name (AbsModulePath)
+import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
+import MiniJuvix.Syntax.Concrete.Scoped.Pretty.Ann
+import Prettyprinter hiding (braces, parens)
 
 data Options = Options
-  {
-    _optShowNameId :: Bool,
+  { _optShowNameId :: Bool,
     _optInlineImports :: Bool,
     _optIndent :: Int
-  }
+}
 
 defaultOptions :: Options
 defaultOptions =
   Options
-    {
-      _optShowNameId = False,
+    { _optShowNameId = False,
       _optInlineImports = False,
       _optIndent = 2
     }
@@ -67,6 +66,9 @@ kwLambda = keyword Str.lambdaUnicode
 kwGhc :: Doc Ann
 kwGhc = keyword Str.ghc
 
+kwAgda :: Doc Ann
+kwAgda = keyword Str.agda
+
 kwWhere :: Doc Ann
 kwWhere = keyword Str.where_
 
@@ -176,15 +178,21 @@ parens = enclose kwParenL kwParenR
 doubleQuotes :: Doc Ann -> Doc Ann
 doubleQuotes = enclose kwDQuote kwDQuote
 
-ppModulePathType :: forall t s r. (SingI t, SingI s, Members '[Reader Options] r) =>
-  ModulePathType s t -> Sem r (Doc Ann)
+annotateKind :: S.NameKind -> Doc Ann -> Doc Ann
+annotateKind k = (annotate . AnnKind) k
+
+ppModulePathType ::
+  forall t s r.
+  (SingI t, SingI s, Members '[Reader Options] r) =>
+  ModulePathType s t ->
+  Sem r (Doc Ann)
 ppModulePathType x = case sing :: SStage s of
   SParsed -> case sing :: SModuleIsTop t of
     SModuleLocal -> ppCode x
     SModuleTop -> ppCode x
   SScoped -> case sing :: SModuleIsTop t of
     SModuleLocal -> annSDef x <$> ppCode x
-    SModuleTop ->  annSDef x <$> ppCode x
+    SModuleTop -> annSDef x <$> ppCode x
 
 ppUnkindedSymbol :: Members '[Reader Options] r => Symbol -> Sem r (Doc Ann)
 ppUnkindedSymbol = fmap (annotate AnnUnkindedSym) . ppSymbol
@@ -197,63 +205,64 @@ ppSymbol = case sing :: SStage s of
 groupStatements :: forall s. SingI s => [Statement s] -> [[Statement s]]
 groupStatements = reverse . map reverse . uncurry cons . foldl' aux ([], [])
   where
-  aux :: ([Statement s], [[Statement s]]) -> Statement s
-      -> ([Statement s], [[Statement s]])
-  aux ([], acc) s = ([s], acc)
-  aux (gr@(a : _), acc) b
-    | g a b = (b : gr, acc)
-    | otherwise = ([b], gr : acc)
-  -- | Decides if statements a and b should be next to each other without a
-  -- blank line
-  g :: Statement s -> Statement s -> Bool
-  g a b = case (a, b) of
-    (StatementCompile _, StatementCompile _) -> True
-    (StatementCompile _, _) -> False
-    (StatementForeign _, _) -> False
-    (StatementOperator _, StatementOperator _) -> True
-    (StatementOperator o, s) -> definesSymbol (opSymbol o) s
-    (StatementImport _, StatementImport _) -> True
-    (StatementImport i, StatementOpenModule o) -> case sing :: SStage s of
-      SParsed -> True
-      SScoped ->
-        S._nameId (_modulePath (importModule i)) ==
-        S._nameId (openModuleName o)
-    (StatementImport _, _) -> False
-    (StatementOpenModule {}, StatementOpenModule {}) -> True
-    (StatementOpenModule {}, _) -> False
-    (StatementInductive {}, _) -> False
-    (StatementModule {}, _) -> False
-    (StatementAxiom {}, StatementAxiom {}) -> True
-    (StatementAxiom {}, _) -> False
-    (StatementEval {}, StatementEval {}) -> True
-    (StatementEval {}, _) -> False
-    (StatementPrint {}, StatementPrint {}) -> True
-    (StatementPrint {}, _) -> False
-    (StatementTypeSignature sig, StatementFunctionClause fun) ->
-      case sing :: SStage s of
-        SParsed -> _sigName sig == _clauseOwnerFunction fun
-        SScoped -> _sigName sig == _clauseOwnerFunction fun
-    (StatementTypeSignature {}, _) -> False
-    (StatementFunctionClause fun1, StatementFunctionClause fun2) ->
-      case sing :: SStage s of
-        SParsed -> _clauseOwnerFunction fun1 == _clauseOwnerFunction fun2
-        SScoped -> _clauseOwnerFunction fun1 == _clauseOwnerFunction fun2
-    (StatementFunctionClause {}, _) -> False
-  definesSymbol :: Symbol -> Statement s -> Bool
-  definesSymbol n s = case s of
-    StatementTypeSignature sig ->
-      let sym = case sing :: SStage s of
-            SParsed -> _sigName sig
-            SScoped -> S._nameConcrete $ _sigName sig
-      in n == sym
-    StatementInductive d -> n `elem` syms d
-    _ -> False
-    where
-    syms :: InductiveDef s -> [Symbol]
-    syms InductiveDef {..} = case sing :: SStage s of
-      SParsed -> _inductiveName : map constructorName _inductiveConstructors
-      SScoped -> S._nameConcrete _inductiveName :
-          map (S._nameConcrete . constructorName) _inductiveConstructors
+    aux ::
+      ([Statement s], [[Statement s]]) ->
+      Statement s ->
+      ([Statement s], [[Statement s]])
+    aux ([], acc) s = ([s], acc)
+    aux (gr@(a : _), acc) b
+      | g a b = (b : gr, acc)
+      | otherwise = ([b], gr : acc)
+    -- Decides if statements a and b should be next to each other without a
+    -- blank line
+    g :: Statement s -> Statement s -> Bool
+    g a b = case (a, b) of
+      (StatementForeign _, _) -> False
+      (StatementOperator _, StatementOperator _) -> True
+      (StatementOperator o, s) -> definesSymbol (opSymbol o) s
+      (StatementImport _, StatementImport _) -> True
+      (StatementImport i, StatementOpenModule o) -> case sing :: SStage s of
+        SParsed -> True
+        SScoped ->
+          S._nameId (_modulePath (importModule i))
+            == S._nameId (projSigma2 _moduleRefName (o ^. openModuleName . unModuleRef'))
+      (StatementImport _, _) -> False
+      (StatementOpenModule {}, StatementOpenModule {}) -> True
+      (StatementOpenModule {}, _) -> False
+      (StatementInductive {}, _) -> False
+      (StatementModule {}, _) -> False
+      (StatementAxiom {}, StatementAxiom {}) -> True
+      (StatementAxiom {}, _) -> False
+      (StatementEval {}, StatementEval {}) -> True
+      (StatementEval {}, _) -> False
+      (StatementPrint {}, StatementPrint {}) -> True
+      (StatementPrint {}, _) -> False
+      (StatementTypeSignature sig, StatementFunctionClause fun) ->
+        case sing :: SStage s of
+          SParsed -> _sigName sig == _clauseOwnerFunction fun
+          SScoped -> _sigName sig == _clauseOwnerFunction fun
+      (StatementTypeSignature {}, _) -> False
+      (StatementFunctionClause fun1, StatementFunctionClause fun2) ->
+        case sing :: SStage s of
+          SParsed -> _clauseOwnerFunction fun1 == _clauseOwnerFunction fun2
+          SScoped -> _clauseOwnerFunction fun1 == _clauseOwnerFunction fun2
+      (StatementFunctionClause {}, _) -> False
+    definesSymbol :: Symbol -> Statement s -> Bool
+    definesSymbol n s = case s of
+      StatementTypeSignature sig ->
+        let sym = case sing :: SStage s of
+              SParsed -> _sigName sig
+              SScoped -> S._nameConcrete $ _sigName sig
+         in n == sym
+      StatementInductive d -> n `elem` syms d
+      _ -> False
+      where
+        syms :: InductiveDef s -> [Symbol]
+        syms InductiveDef {..} = case sing :: SStage s of
+          SParsed -> _inductiveName : map _constructorName _inductiveConstructors
+          SScoped ->
+            S._nameConcrete _inductiveName :
+            map (S._nameConcrete . _constructorName) _inductiveConstructors
 
 instance SingI s => PrettyCode [Statement s] where
   ppCode ss = joinGroups <$> mapM (fmap mkGroup . mapM (fmap endSemicolon . ppCode)) (groupStatements ss)
@@ -273,31 +282,36 @@ instance SingI s => PrettyCode (Statement s) where
     StatementAxiom a -> ppCode a
     StatementEval e -> ppCode e
     StatementPrint p -> ppCode p
-    StatementCompile p -> ppCode p
     StatementForeign p -> ppCode p
 
 instance PrettyCode Backend where
   ppCode = \case
     BackendGhc -> return kwGhc
+    BackendAgda -> return kwAgda
 
 instance PrettyCode ForeignBlock where
   ppCode ForeignBlock {..} = do
     _foreignBackend' <- ppCode _foreignBackend
-    return $ kwForeign <+> _foreignBackend' <+> lbrace <> line
-        <> pretty _foreignCode <> line <> rbrace
+    return $
+      kwForeign <+> _foreignBackend' <+> lbrace <> line
+        <> pretty _foreignCode
+        <> line
+        <> rbrace
 
-instance SingI s => PrettyCode (CompileDef s) where
-  ppCode CompileDef {..} = do
-    _compileAxiom' <- ppSymbol _compileAxiom
-    _compileBackend' <- ppCode _compileBackend
-    _compileBackend' <- ppCode _compileBackend
-    return $ kwCompile <+> _compileAxiom' <+> _compileBackend' <+> ppStringLit _compileCode
+instance PrettyCode BackendItem where
+  ppCode BackendItem {..} = do
+    backend <- ppCode _backendItemBackend
+    return $
+      backend <+> kwMapsto <+> ppStringLit _backendItemCode
 
 ppStringLit :: Text -> Doc Ann
 ppStringLit = annotate AnnLiteralString . doubleQuotes . pretty
 
-ppTopModulePath :: forall s r. (SingI s, Members '[Reader Options] r) =>
-  ModulePathType s 'ModuleTop -> Sem r (Doc Ann)
+ppTopModulePath ::
+  forall s r.
+  (SingI s, Members '[Reader Options] r) =>
+  ModulePathType s 'ModuleTop ->
+  Sem r (Doc Ann)
 ppTopModulePath = case sing :: SStage s of
   SParsed -> ppCode
   SScoped -> ppCode
@@ -322,27 +336,29 @@ instance PrettyCode AbsModulePath where
     absTopModulePath' <- ppCode absTopModulePath
     return $ dotted (absTopModulePath' : absLocalPath')
 
-ppInductiveParameters :: (SingI s, Members '[Reader Options] r)
-    => [InductiveParameter s] -> Sem r (Maybe (Doc Ann))
+ppInductiveParameters ::
+  (SingI s, Members '[Reader Options] r) =>
+  [InductiveParameter s] ->
+  Sem r (Maybe (Doc Ann))
 ppInductiveParameters ps
   | null ps = return Nothing
   | otherwise = Just <$> ppCode ps
 
 instance (SingI s, SingI t) => PrettyCode (Module s t) where
   ppCode Module {..} = do
-      moduleBody' <- ppCode _moduleBody >>= indented
-      modulePath' <- ppModulePathType _modulePath
-      moduleParameters' <- ppInductiveParameters _moduleParameters
-      return $
-        kwModule <+> modulePath' <+?> moduleParameters' <> kwSemicolon <> line
-          <> moduleBody'
-          <> line
-          <> kwEnd
-          <?> lastSemicolon
-      where
-        lastSemicolon = case sing :: SModuleIsTop t of
-          SModuleLocal -> Nothing
-          SModuleTop -> Just kwSemicolon
+    moduleBody' <- ppCode _moduleBody >>= indented
+    modulePath' <- ppModulePathType _modulePath
+    moduleParameters' <- ppInductiveParameters _moduleParameters
+    return $
+      kwModule <+> modulePath' <+?> moduleParameters' <> kwSemicolon <> line
+        <> moduleBody'
+        <> line
+        <> kwEnd
+        <?> lastSemicolon
+    where
+      lastSemicolon = case sing :: SModuleIsTop t of
+        SModuleLocal -> Nothing
+        SModuleTop -> Just (kwSemicolon <> line)
 
 instance PrettyCode Precedence where
   ppCode p = return $ case p of
@@ -358,11 +374,11 @@ instance PrettyCode Fixity where
 
 instance PrettyCode OperatorArity where
   ppCode fixityArity = return $ case fixityArity of
-   Unary {} -> kwPostfix
-   Binary p -> case p of
-     AssocRight -> kwInfixr
-     AssocLeft -> kwInfixl
-     AssocNone -> kwInfix
+    Unary {} -> kwPostfix
+    Binary p -> case p of
+      AssocRight -> kwInfixr
+      AssocLeft -> kwInfixl
+      AssocNone -> kwInfix
 
 instance PrettyCode OperatorSyntaxDef where
   ppCode OperatorSyntaxDef {..} = do
@@ -372,8 +388,8 @@ instance PrettyCode OperatorSyntaxDef where
 
 instance SingI s => PrettyCode (InductiveConstructorDef s) where
   ppCode InductiveConstructorDef {..} = do
-    constructorName' <- annDef constructorName <$> ppSymbol constructorName
-    constructorType' <- ppExpression constructorType
+    constructorName' <- annDef _constructorName <$> ppSymbol _constructorName
+    constructorType' <- ppExpression _constructorType
     return $ constructorName' <+> kwColon <+> constructorType'
 
 instance SingI s => PrettyCode (InductiveDef s) where
@@ -400,7 +416,7 @@ instance PrettyCode QualifiedName where
     let symbols = pathParts _qualifiedPath NonEmpty.|> _qualifiedSymbol
     dotted <$> mapM ppSymbol symbols
 
-ppName :: forall s r. (SingI s, Members '[Reader Options] r) => NameType s -> Sem r (Doc Ann)
+ppName :: forall s r. (SingI s, Members '[Reader Options] r) => IdentifierType s -> Sem r (Doc Ann)
 ppName = case sing :: SStage s of
   SParsed -> ppCode
   SScoped -> ppCode
@@ -430,43 +446,49 @@ instance PrettyCode Name where
 
 instance PrettyCode n => PrettyCode (S.Name' n) where
   ppCode S.Name' {..} = do
-    nameConcrete' <- annotate (AnnKind _nameKind) <$> ppCode _nameConcrete
+    nameConcrete' <- annotateKind _nameKind <$> ppCode _nameConcrete
     showNameId <- asks _optShowNameId
     uid <- if showNameId then ("@" <>) <$> ppCode _nameId else return mempty
     return $ annSRef (nameConcrete' <> uid)
-      where
+    where
       annSRef :: Doc Ann -> Doc Ann
       annSRef = annotate (AnnRef (S.absTopModulePath _nameDefinedIn) _nameId)
 
+instance PrettyCode ModuleRef where
+  ppCode = ppCode . projSigma2 _moduleRefName . (^. unModuleRef')
+
 instance SingI s => PrettyCode (OpenModule s) where
   ppCode :: forall r. Members '[Reader Options] r => OpenModule s -> Sem r (Doc Ann)
   ppCode OpenModule {..} = do
-    openModuleName' <- ppName openModuleName
-    openUsingHiding' <- sequence $ ppUsingHiding <$> openUsingHiding
+    openModuleName' <- case sing :: SStage s of
+      SParsed -> ppCode _openModuleName
+      SScoped -> ppCode _openModuleName
+    openUsingHiding' <- sequence $ ppUsingHiding <$> _openUsingHiding
     openParameters' <- ppOpenParams
     let openPublic' = ppPublic
     return $ keyword "open" <+> openModuleName' <+?> openParameters' <+?> openUsingHiding' <+?> openPublic'
     where
-    ppAtom' = case sing :: SStage s of
-      SParsed -> ppCodeAtom
-      SScoped -> ppCodeAtom
-    ppOpenParams :: Sem r (Maybe (Doc Ann))
-    ppOpenParams = case openParameters of
-      [] -> return Nothing
-      _ -> Just . hsep <$> mapM ppAtom' openParameters
-    ppUsingHiding :: UsingHiding -> Sem r (Doc Ann)
-    ppUsingHiding uh = do
-      bracedList <- encloseSep kwBraceL kwBraceR kwSemicolon . toList
-        <$> mapM ppUnkindedSymbol syms
-      return $ kw <+> bracedList
-      where
-        (kw, syms) = case uh of
-          Using s -> (kwUsing, s)
-          Hiding s -> (kwHiding, s)
-    ppPublic :: Maybe (Doc Ann)
-    ppPublic = case openPublic of
-      Public -> Just kwPublic
-      NoPublic -> Nothing
+      ppAtom' = case sing :: SStage s of
+        SParsed -> ppCodeAtom
+        SScoped -> ppCodeAtom
+      ppOpenParams :: Sem r (Maybe (Doc Ann))
+      ppOpenParams = case _openParameters of
+        [] -> return Nothing
+        _ -> Just . hsep <$> mapM ppAtom' _openParameters
+      ppUsingHiding :: UsingHiding -> Sem r (Doc Ann)
+      ppUsingHiding uh = do
+        bracedList <-
+          encloseSep kwBraceL kwBraceR kwSemicolon . toList
+            <$> mapM ppUnkindedSymbol syms
+        return $ kw <+> bracedList
+        where
+          (kw, syms) = case uh of
+            Using s -> (kwUsing, s)
+            Hiding s -> (kwHiding, s)
+      ppPublic :: Maybe (Doc Ann)
+      ppPublic = case _openPublic of
+        Public -> Just kwPublic
+        NoPublic -> Nothing
 
 instance SingI s => PrettyCode (TypeSignature s) where
   ppCode TypeSignature {..} = do
@@ -568,7 +590,10 @@ instance SingI s => PrettyCode (AxiomDef s) where
   ppCode AxiomDef {..} = do
     axiomName' <- ppSymbol _axiomName
     axiomType' <- ppExpression _axiomType
-    return $ kwAxiom <+> axiomName' <+> kwColon <+> axiomType'
+    axiomBackendItems' <- case _axiomBackendItems of
+      [] -> return Nothing
+      bs -> Just <$> ppBlock bs
+    return $ kwAxiom <+> axiomName' <+> kwColon <+> axiomType' <+?> axiomBackendItems'
 
 instance SingI s => PrettyCode (Eval s) where
   ppCode (Eval p) = do
@@ -587,22 +612,30 @@ instance SingI s => PrettyCode (Import s) where
     inlineImport' <- inlineImport
     return $ kwImport <+> modulePath' <+?> inlineImport'
     where
-    ppModulePath = case sing :: SStage s of
-      SParsed -> ppCode m
-      SScoped -> ppTopModulePath (m ^. modulePath)
-    jumpLines :: Doc Ann -> Doc Ann
-    jumpLines x = line <> x <> line
-    inlineImport :: Sem r (Maybe (Doc Ann))
-    inlineImport = do
-      b <- asks _optInlineImports
-      if b then case sing :: SStage s of
-        SParsed -> return Nothing
-        SScoped -> ppCode m >>= fmap (Just . braces . jumpLines) . indented
-        else return Nothing
+      ppModulePath = case sing :: SStage s of
+        SParsed -> ppCode m
+        SScoped -> ppTopModulePath (m ^. modulePath)
+      jumpLines :: Doc Ann -> Doc Ann
+      jumpLines x = line <> x <> line
+      inlineImport :: Sem r (Maybe (Doc Ann))
+      inlineImport = do
+        b <- asks _optInlineImports
+        if b
+          then case sing :: SStage s of
+            SParsed -> return Nothing
+            SScoped -> ppCode m >>= fmap (Just . braces . jumpLines) . indented
+          else return Nothing
+
+instance PrettyCode PatternScopedIden where
+  ppCode = \case
+    PatternScopedVar v -> ppCode v
+    PatternScopedConstructor c -> ppCode c
 
 instance SingI s => PrettyCode (PatternAtom s) where
   ppCode a = case a of
-    PatternAtomName n -> ppName n
+    PatternAtomIden n -> case sing :: SStage s of
+      SParsed -> ppCode n
+      SScoped -> ppCode n
     PatternAtomWildcard -> return kwWildcard
     PatternAtomEmpty -> return $ parens mempty
     PatternAtomParens p -> parens <$> ppCode p
@@ -610,12 +643,12 @@ instance SingI s => PrettyCode (PatternAtom s) where
 instance SingI s => PrettyCode (PatternAtoms s) where
   ppCode (PatternAtoms ps) = hsep . toList <$> mapM ppCode ps
 
-ppPattern :: forall s r. (SingI s,  Members '[Reader Options] r) => PatternType s -> Sem r (Doc Ann)
+ppPattern :: forall s r. (SingI s, Members '[Reader Options] r) => PatternType s -> Sem r (Doc Ann)
 ppPattern = case sing :: SStage s of
   SParsed -> ppCode
   SScoped -> ppCode
 
-ppPatternAtom :: forall s r. (SingI s,  Members '[Reader Options] r) => PatternType s -> Sem r (Doc Ann)
+ppPatternAtom :: forall s r. (SingI s, Members '[Reader Options] r) => PatternType s -> Sem r (Doc Ann)
 ppPatternAtom = case sing :: SStage s of
   SParsed -> ppCodeAtom
   SScoped -> ppCodeAtom
@@ -644,6 +677,26 @@ instance PrettyCode Literal where
     LitInteger n -> return $ annotate AnnLiteralInteger (pretty n)
     LitString s -> return $ ppStringLit s
 
+instance PrettyCode AxiomRef where
+  ppCode a = ppCode (a ^. axiomRefName)
+
+instance PrettyCode InductiveRef where
+  ppCode a = ppCode (a ^. inductiveRefName)
+
+instance PrettyCode FunctionRef where
+  ppCode a = ppCode (a ^. functionRefName)
+
+instance PrettyCode ConstructorRef where
+  ppCode a = ppCode (a ^. constructorRefName)
+
+instance PrettyCode ScopedIden where
+  ppCode = \case
+    ScopedAxiom a -> ppCode a
+    ScopedInductive i -> ppCode i
+    ScopedVar n -> ppCode n
+    ScopedFunction f -> ppCode f
+    ScopedConstructor c -> ppCode c
+
 instance PrettyCode Expression where
   ppCode e = case e of
     ExpressionIdentifier n -> ppCode n
@@ -672,40 +725,52 @@ instance PrettyCode Pattern where
     PatternInfixApplication i -> ppPatternInfixApp i
     PatternPostfixApplication i -> ppPatternPostfixApp i
     where
-    ppPatternInfixApp :: PatternInfixApp -> Sem r (Doc Ann)
-    ppPatternInfixApp p@PatternInfixApp {..} = do
-      patInfixConstructor' <- ppCode patInfixConstructor
-      patInfixLeft' <- ppLeftExpression (getFixity p) patInfixLeft
-      patInfixRight' <- ppRightExpression (getFixity p) patInfixRight
-      return $ patInfixLeft' <+> patInfixConstructor' <+> patInfixRight'
+      ppPatternInfixApp :: PatternInfixApp -> Sem r (Doc Ann)
+      ppPatternInfixApp p@PatternInfixApp {..} = do
+        patInfixConstructor' <- ppCode _patInfixConstructor
+        patInfixLeft' <- ppLeftExpression (getFixity p) _patInfixLeft
+        patInfixRight' <- ppRightExpression (getFixity p) _patInfixRight
+        return $ patInfixLeft' <+> patInfixConstructor' <+> patInfixRight'
 
-    ppPatternPostfixApp :: PatternPostfixApp -> Sem r (Doc Ann)
-    ppPatternPostfixApp p@PatternPostfixApp {..} = do
-      patPostfixConstructor' <- ppCode patPostfixConstructor
-      patPostfixParameter' <- ppLeftExpression (getFixity p) patPostfixParameter
-      return $ patPostfixParameter' <+> patPostfixConstructor'
+      ppPatternPostfixApp :: PatternPostfixApp -> Sem r (Doc Ann)
+      ppPatternPostfixApp p@PatternPostfixApp {..} = do
+        patPostfixConstructor' <- ppCode _patPostfixConstructor
+        patPostfixParameter' <- ppLeftExpression (getFixity p) _patPostfixParameter
+        return $ patPostfixParameter' <+> patPostfixConstructor'
 
 parensCond :: Bool -> Doc Ann -> Doc Ann
 parensCond t d = if t then parens d else d
 
-ppPostExpression ::(PrettyCode a, HasAtomicity a, Member (Reader Options) r)  =>
-  Fixity -> a -> Sem r (Doc Ann)
+ppPostExpression ::
+  (PrettyCode a, HasAtomicity a, Member (Reader Options) r) =>
+  Fixity ->
+  a ->
+  Sem r (Doc Ann)
 ppPostExpression = ppLRExpression isPostfixAssoc
 
-ppRightExpression :: (PrettyCode a, HasAtomicity a, Member (Reader Options) r) =>
-  Fixity -> a -> Sem r (Doc Ann)
+ppRightExpression ::
+  (PrettyCode a, HasAtomicity a, Member (Reader Options) r) =>
+  Fixity ->
+  a ->
+  Sem r (Doc Ann)
 ppRightExpression = ppLRExpression isRightAssoc
 
-ppLeftExpression :: (PrettyCode a, HasAtomicity a, Member (Reader Options) r) =>
-  Fixity -> a -> Sem r (Doc Ann)
+ppLeftExpression ::
+  (PrettyCode a, HasAtomicity a, Member (Reader Options) r) =>
+  Fixity ->
+  a ->
+  Sem r (Doc Ann)
 ppLeftExpression = ppLRExpression isLeftAssoc
 
-ppLRExpression
-  :: (HasAtomicity a, PrettyCode a, Member (Reader Options) r) =>
-     (Fixity -> Bool) -> Fixity -> a -> Sem r (Doc Ann)
+ppLRExpression ::
+  (HasAtomicity a, PrettyCode a, Member (Reader Options) r) =>
+  (Fixity -> Bool) ->
+  Fixity ->
+  a ->
+  Sem r (Doc Ann)
 ppLRExpression associates fixlr e =
   parensCond (atomParens associates (atomicity e) fixlr)
-      <$> ppCode e
+    <$> ppCode e
 
 ppCodeAtom :: (HasAtomicity c, PrettyCode c, Members '[Reader Options] r) => c -> Sem r (Doc Ann)
 ppCodeAtom c = do
@@ -731,3 +796,18 @@ ppExpression :: forall s r. (SingI s, Members '[Reader Options] r) => Expression
 ppExpression = case sing :: SStage s of
   SScoped -> ppCode
   SParsed -> ppCode
+
+instance PrettyCode SymbolEntry where
+  ppCode ent = return (kindTag <+> pretty (entryName ent ^. S.nameVerbatim)
+    <+> "defined at" <+> pretty (getLoc ent))
+    where
+    pretty' :: Text -> Doc a
+    pretty' = pretty
+    kindTag = case ent of
+      EntryAxiom _ -> annotateKind S.KNameAxiom (pretty' Str.axiom)
+      EntryInductive _ -> annotateKind S.KNameInductive (pretty' Str.inductive)
+      EntryFunction _ -> annotateKind S.KNameFunction (pretty' Str.function)
+      EntryConstructor _ -> annotateKind S.KNameConstructor (pretty' Str.constructor)
+      EntryModule (ModuleRef' (isTop :&: _))
+        | SModuleTop <- isTop -> annotateKind S.KNameTopModule (pretty' Str.topModule)
+        | SModuleLocal <- isTop -> annotateKind S.KNameLocalModule (pretty' Str.localModule)

src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Html.hs

@@ -1,22 +1,22 @@
-module MiniJuvix.Syntax.Concrete.Scoped.Pretty.Html (genHtml, Theme(..)) where
+module MiniJuvix.Syntax.Concrete.Scoped.Pretty.Html (genHtml, Theme (..)) where
 
-import MiniJuvix.Syntax.Concrete.Language
-import MiniJuvix.Syntax.Concrete.Scoped.Utils
-import           Prettyprinter.Render.Util.SimpleDocTree
-import MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base
-import MiniJuvix.Prelude
-import Prettyprinter
-import qualified Text.Blaze.Html.Renderer.Text           as Html
-import           Text.Blaze.Html5                       as Html hiding (map)
-import qualified Text.Blaze.Html5.Attributes             as Attr
 import qualified Data.Text as Text
 import qualified Data.Text.IO as Text
 import Data.Text.Lazy (toStrict)
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Concrete.Language
 import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
+import MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base
+import MiniJuvix.Syntax.Concrete.Scoped.Utils
 import MiniJuvix.Utils.Paths
+import Prettyprinter
+import Prettyprinter.Render.Util.SimpleDocTree
+import qualified Text.Blaze.Html.Renderer.Text as Html
+import Text.Blaze.Html5 as Html hiding (map)
+import qualified Text.Blaze.Html5.Attributes as Attr
 
-data Theme =
-  Nord
+data Theme
+  = Nord
   | Ayu
   deriving stock (Show)
 
@@ -27,58 +27,65 @@ genHtml opts recursive theme entry = do
   withCurrentDirectory htmlPath $ do
     mapM_ outputModule allModules
   where
-  allModules
-    | recursive = toList $ getAllModules entry
-    | otherwise = pure entry
-  htmlPath = "html"
+    allModules
+      | recursive = toList $ getAllModules entry
+      | otherwise = pure entry
+    htmlPath = "html"
 
-  copyAssetFiles :: IO ()
-  copyAssetFiles = do
-    createDirectoryIfMissing True toAssetsDir
-    mapM_ cpFile assetFiles
-    where
-    fromAssetsDir = $(assetsDir)
-    toAssetsDir = htmlPath </> "assets"
-    cpFile (fromDir, name, toDir) = copyFile (fromDir </> name) (toDir </> name)
-    assetFiles = [ (fromAssetsDir, name, toAssetsDir)
-                | name <- ["highlight.js"
-                          , "source-ayu-light.css"
-                          , "source-nord.css"]]
+    copyAssetFiles :: IO ()
+    copyAssetFiles = do
+      createDirectoryIfMissing True toAssetsDir
+      mapM_ cpFile assetFiles
+      where
+        fromAssetsDir = $(assetsDir)
+        toAssetsDir = htmlPath </> "assets"
+        cpFile (fromDir, name, toDir) = copyFile (fromDir </> name) (toDir </> name)
+        assetFiles =
+          [ (fromAssetsDir, name, toAssetsDir)
+            | name <-
+                [ "highlight.js",
+                  "source-ayu-light.css",
+                  "source-nord.css"
+                ]
+          ]
 
-  outputModule :: Module 'Scoped 'ModuleTop -> IO ()
-  outputModule m = do
-    createDirectoryIfMissing True (takeDirectory htmlFile)
-    putStrLn $ "Writing " <> pack htmlFile
-    Text.writeFile htmlFile (genModule opts theme m)
-   where
-   htmlFile = dottedPath (S._nameConcrete (_modulePath m)) <.> ".html"
+    outputModule :: Module 'Scoped 'ModuleTop -> IO ()
+    outputModule m = do
+      createDirectoryIfMissing True (takeDirectory htmlFile)
+      putStrLn $ "Writing " <> pack htmlFile
+      Text.writeFile htmlFile (genModule opts theme m)
+      where
+        htmlFile = topModulePathToDottedPath (S._nameConcrete (_modulePath m)) <.> ".html"
 
 genModule :: Options -> Theme -> Module 'Scoped 'ModuleTop -> Text
 genModule opts theme m =
-  toStrict $ Html.renderHtml $
-  docTypeHtml ! Attr.xmlns "http://www.w3.org/1999/xhtml" $
-  mhead
-  <> mbody
+  toStrict $
+    Html.renderHtml $
+      docTypeHtml ! Attr.xmlns "http://www.w3.org/1999/xhtml" $
+        mhead
+          <> mbody
   where
-  themeCss = case theme of
-    Ayu -> ayuCss
-    Nord -> nordCss
-  prettySrc = (pre ! Attr.id "src-content")
-    $ renderTree $ treeForm $ docStream opts m
+    themeCss = case theme of
+      Ayu -> ayuCss
+      Nord -> nordCss
+    prettySrc =
+      (pre ! Attr.id "src-content") $
+        renderTree $ treeForm $ docStream opts m
 
-  mheader :: Html
-  mheader = Html.div ! Attr.id "package-header"
-    $ (Html.span ! Attr.class_ "caption" $ "")
+    mheader :: Html
+    mheader =
+      Html.div ! Attr.id "package-header" $
+        (Html.span ! Attr.class_ "caption" $ "")
 
-  mhead :: Html
-  mhead =
-    metaUtf8
-    <> themeCss
-    <> highlightJs
-  mbody :: Html
-  mbody =
-    mheader
-    <> prettySrc
+    mhead :: Html
+    mhead =
+      metaUtf8
+        <> themeCss
+        <> highlightJs
+    mbody :: Html
+    mbody =
+      mheader
+        <> prettySrc
 
 docStream :: Options -> Module 'Scoped 'ModuleTop -> SimpleDocStream Ann
 docStream opts m = layoutPretty defaultLayoutOptions (runPrettyCode opts m)
@@ -88,65 +95,61 @@ renderTree = go
 
 go :: SimpleDocTree Ann -> Html
 go sdt = case sdt of
-    STEmpty -> mempty
-    STChar c -> toHtml c
-    STText _ t -> toHtml t
-    STLine s -> "\n" <> toHtml (textSpaces s)
-    STAnn ann content -> putTag ann (go content)
-    STConcat l -> mconcatMap go l
-    where
+  STEmpty -> mempty
+  STChar c -> toHtml c
+  STText _ t -> toHtml t
+  STLine s -> "\n" <> toHtml (textSpaces s)
+  STAnn ann content -> putTag ann (go content)
+  STConcat l -> mconcatMap go l
+  where
     textSpaces :: Int -> Text
     textSpaces n = Text.replicate n (Text.singleton ' ')
 
-fromText :: IsString a => Text -> a
-fromText = fromString . unpack
-
 putTag :: Ann -> Html -> Html
 putTag ann x = case ann of
-   AnnKind k -> tagKind k x
-   AnnLiteralInteger -> Html.span ! Attr.class_ "ju-number" $ x
-   AnnLiteralString -> Html.span ! Attr.class_ "ju-string" $ x
-   AnnKeyword -> Html.span ! Attr.class_ "ju-keyword" $ x
-   AnnUnkindedSym -> Html.span ! Attr.class_ "ju-var" $ x
-   AnnDelimiter -> Html.span ! Attr.class_ "ju-delimiter" $ x
-   AnnDef tmp ni -> tagDef tmp ni
-   AnnRef tmp ni -> tagRef tmp ni
-
+  AnnKind k -> tagKind k x
+  AnnLiteralInteger -> Html.span ! Attr.class_ "ju-number" $ x
+  AnnLiteralString -> Html.span ! Attr.class_ "ju-string" $ x
+  AnnKeyword -> Html.span ! Attr.class_ "ju-keyword" $ x
+  AnnUnkindedSym -> Html.span ! Attr.class_ "ju-var" $ x
+  AnnDelimiter -> Html.span ! Attr.class_ "ju-delimiter" $ x
+  AnnDef tmp ni -> tagDef tmp ni
+  AnnRef tmp ni -> tagRef tmp ni
   where
-  tagDef :: TopModulePath -> S.NameId -> Html
-  tagDef tmp nid = Html.span ! Attr.id (nameIdAttr nid)
-    $ tagRef tmp nid
+    tagDef :: TopModulePath -> S.NameId -> Html
+    tagDef tmp nid =
+      Html.span ! Attr.id (nameIdAttr nid) $
+        tagRef tmp nid
 
-  tagRef tmp ni = Html.span ! Attr.class_ "annot"
-                  $ a ! Attr.href (nameIdAttrRef tmp ni)
-                  $ x
-  tagKind k = Html.span ! Attr.class_
-     (case k of
-      S.KNameConstructor -> "ju-constructor"
-      S.KNameInductive -> "ju-inductive"
-      S.KNameFunction -> "ju-function"
-      S.KNameLocal -> "ju-var"
-      S.KNameAxiom -> "ju-axiom"
-      S.KNameLocalModule -> "ju-var"
-      S.KNameTopModule -> "ju-var")
-
-dottedPath :: IsString s => TopModulePath -> s
-dottedPath (TopModulePath l r) =
-  fromText $ mconcat $ intersperse "." $ map fromSymbol $ l ++ [r]
-  where
-  fromSymbol Symbol {..} = _symbolText
+    tagRef tmp ni =
+      Html.span ! Attr.class_ "annot" $
+        a ! Attr.href (nameIdAttrRef tmp ni) $
+          x
+    tagKind k =
+      Html.span
+        ! Attr.class_
+          ( case k of
+              S.KNameConstructor -> "ju-constructor"
+              S.KNameInductive -> "ju-inductive"
+              S.KNameFunction -> "ju-function"
+              S.KNameLocal -> "ju-var"
+              S.KNameAxiom -> "ju-axiom"
+              S.KNameLocalModule -> "ju-var"
+              S.KNameTopModule -> "ju-var"
+          )
 
 nameIdAttr :: S.NameId -> AttributeValue
 nameIdAttr (S.NameId k) = fromString . show $ k
 
 nameIdAttrRef :: TopModulePath -> S.NameId -> AttributeValue
 nameIdAttrRef tp s =
-  dottedPath tp <> ".html" <> preEscapedToValue '#' <> nameIdAttr s
+  topModulePathToDottedPath tp <> ".html" <> preEscapedToValue '#' <> nameIdAttr s
 
 cssLink :: AttributeValue -> Html
-cssLink css = link ! Attr.href css
-        ! Attr.rel "stylesheet"
-        ! Attr.type_ "text/css"
+cssLink css =
+  link ! Attr.href css
+    ! Attr.rel "stylesheet"
+    ! Attr.type_ "text/css"
 
 ayuCss :: Html
 ayuCss = cssLink "assets/source-ayu-light.css"
@@ -155,9 +158,10 @@ nordCss :: Html
 nordCss = cssLink "assets/source-nord.css"
 
 highlightJs :: Html
-highlightJs = script ! Attr.src "assets/highlight.js"
-        ! Attr.type_ "text/javascript"
-        $ mempty
+highlightJs =
+  script ! Attr.src "assets/highlight.js"
+    ! Attr.type_ "text/javascript"
+    $ mempty
 
 metaUtf8 :: Html
 metaUtf8 = meta ! Attr.charset "UTF-8"

src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Text.hs

@@ -1,7 +1,7 @@
 module MiniJuvix.Syntax.Concrete.Scoped.Pretty.Text where
 
-import MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base
 import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base
 import Prettyprinter
 import Prettyprinter.Render.Text
 
@@ -21,5 +21,8 @@ renderPrettyCode :: PrettyCode c => Options -> c -> Text
 renderPrettyCode opts = renderStrict . docStream opts
 
 docStream :: PrettyCode c => Options -> c -> SimpleDocStream Ann
-docStream opts = layoutPretty defaultLayoutOptions
-    . run . runReader opts . ppCode
+docStream opts =
+  layoutPretty defaultLayoutOptions
+    . run
+    . runReader opts
+    . ppCode

src/MiniJuvix/Syntax/Concrete/Scoped/Scope.hs

@@ -3,6 +3,7 @@ module MiniJuvix.Syntax.Concrete.Scoped.Scope where
 import MiniJuvix.Prelude
 import MiniJuvix.Syntax.Concrete.Language
 import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
+import qualified Data.HashMap.Strict as HashMap
 
 newtype LocalVariable = LocalVariable
   { variableName :: S.Symbol
@@ -22,45 +23,60 @@ newtype SymbolInfo = SymbolInfo
   }
   deriving newtype (Show, Semigroup, Monoid)
 
-type SymbolEntry = S.Name' ()
-
--- data SymbolEntry' = SymbolEntry' {
---   _entryNameInfo :: NameInfo
-
---   }
-
--- | Symbols that a module exports
-newtype ExportInfo = ExportInfo {
-   _exportSymbols :: HashMap Symbol SymbolEntry
-  }
-
--- | A module entry for either a local or a top module.
-type ModuleEntry = Σ ModuleIsTop (TyCon1 ModuleEntry')
-
-mkModuleEntry :: SingI t => ModuleEntry' t -> ModuleEntry
-mkModuleEntry = (sing :&:)
-
-data ModuleEntry' (t :: ModuleIsTop) = ModuleEntry' {
-  _moduleEntryExport :: ExportInfo,
-  _moduleEntryScoped :: Module 'Scoped t
-  }
+mkModuleRef' :: SingI t => ModuleRef'' 'S.NotConcrete t -> ModuleRef' 'S.NotConcrete
+mkModuleRef' m = ModuleRef' (sing :&: m)
 
 data Scope = Scope
   { _scopePath :: S.AbsModulePath,
     _scopeFixities :: HashMap Symbol OperatorSyntaxDef,
     _scopeSymbols :: HashMap Symbol SymbolInfo,
-    _scopeTopModules :: HashMap TopModulePath S.ModuleNameId,
+    _scopeTopModules :: HashMap TopModulePath (ModuleRef'' 'S.NotConcrete 'ModuleTop),
     _scopeBindGroup :: HashMap Symbol LocalVariable
   }
- deriving stock (Show)
+  deriving stock (Show)
+
+
+newtype FunctionInfo = FunctionInfo {
+  _functionInfoType :: Expression
+  }
+
+newtype ConstructorInfo = ConstructorInfo {
+  _constructorInfoType :: Expression
+  }
+
+data AxiomInfo = AxiomInfo {
+  _axiomInfoType :: Expression,
+  _axiomInfoBackends :: [BackendItem]
+  }
+
+newtype InductiveInfo = InductiveInfo {
+  _inductiveInfoDef :: InductiveDef 'Scoped
+  }
+
+data InfoTable = InfoTable {
+  _infoConstructors :: HashMap ConstructorRef ConstructorInfo,
+  _infoAxioms :: HashMap AxiomRef AxiomInfo,
+  _infoInductives :: HashMap InductiveRef InductiveInfo,
+  _infoFunctions :: HashMap FunctionRef FunctionInfo
+  }
+
+instance Semigroup InfoTable where
+  (<>) = undefined
+instance Monoid InfoTable where
+  mempty = undefined
+
 makeLenses ''ExportInfo
+makeLenses ''InfoTable
+makeLenses ''InductiveInfo
+makeLenses ''ConstructorInfo
+makeLenses ''AxiomInfo
+makeLenses ''FunctionInfo
 makeLenses ''SymbolInfo
 makeLenses ''LocalVars
 makeLenses ''Scope
-makeLenses ''ModuleEntry'
 
 newtype ModulesCache = ModulesCache
-  { _cachedModules :: HashMap TopModulePath (ModuleEntry' 'ModuleTop)
+  { _cachedModules :: HashMap TopModulePath (ModuleRef'' 'S.NotConcrete 'ModuleTop)
   }
 
 makeLenses ''ModulesCache
@@ -73,20 +89,31 @@ data ScopeParameters = ScopeParameters
     -- | Used for import cycle detection.
     _scopeTopParents :: [Import 'Parsed]
   }
+
 makeLenses ''ScopeParameters
 
 data ScoperState = ScoperState
   { _scoperModulesCache :: ModulesCache,
     _scoperFreeNames :: Stream S.NameId,
-    _scoperModules :: HashMap S.ModuleNameId ModuleEntry
+    _scoperModules :: HashMap S.ModuleNameId (ModuleRef' 'S.NotConcrete)
   }
+
 makeLenses ''ScoperState
 
 emptyScope :: S.AbsModulePath -> Scope
-emptyScope absPath = Scope
-        { _scopePath = absPath,
-          _scopeFixities = mempty,
-          _scopeSymbols = mempty,
-          _scopeTopModules = mempty,
-          _scopeBindGroup = mempty
-        }
+emptyScope absPath =
+  Scope
+    { _scopePath = absPath,
+      _scopeFixities = mempty,
+      _scopeSymbols = mempty,
+      _scopeTopModules = mempty,
+      _scopeBindGroup = mempty
+    }
+
+emptyInfoTable :: InfoTable
+emptyInfoTable = InfoTable {
+  _infoConstructors = mempty,
+  _infoAxioms = mempty,
+  _infoInductives = mempty,
+  _infoFunctions = mempty
+  }

src/MiniJuvix/Syntax/Concrete/Scoped/Scoper/Files.hs

@@ -1,7 +1,7 @@
 module MiniJuvix.Syntax.Concrete.Scoped.Scoper.Files where
 
-import MiniJuvix.Prelude
 import qualified Data.HashMap.Strict as HashMap
+import MiniJuvix.Prelude
 
 data Files m a where
   ReadFile' :: FilePath -> Files m Text
@@ -20,8 +20,11 @@ runFilesIO = interpret $ \case
 runFilesPure :: HashMap FilePath Text -> Sem (Files ': r) a -> Sem r a
 runFilesPure fs = interpret $ \case
   (ReadFile' f) -> case HashMap.lookup f fs of
-      Nothing -> error $ pack $ "file " <> f <> " does not exist." <>
-        "\nThe contents of the mocked file system are:\n" <>
-        unlines (HashMap.keys fs)
-      Just c -> return c
+    Nothing ->
+      error $
+        pack $
+          "file " <> f <> " does not exist."
+            <> "\nThe contents of the mocked file system are:\n"
+            <> unlines (HashMap.keys fs)
+    Just c -> return c
   (EqualPaths' _ _) -> return Nothing

src/MiniJuvix/Syntax/Concrete/Scoped/Scoper/InfoTableBuilder.hs

@@ -0,0 +1,67 @@
+module MiniJuvix.Syntax.Concrete.Scoped.Scoper.InfoTableBuilder where
+
+import qualified Data.HashMap.Strict as HashMap
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Concrete.Language
+import MiniJuvix.Syntax.Concrete.Language
+import MiniJuvix.Syntax.Concrete.Scoped.Scope
+import MiniJuvix.Syntax.Concrete.Scoped.Name
+
+data InfoTableBuilder m a where
+  RegisterAxiom :: AxiomDef 'Scoped -> InfoTableBuilder m ()
+  RegisterConstructor :: InductiveConstructorDef 'Scoped -> InfoTableBuilder m ()
+  RegisterInductive :: InductiveDef 'Scoped -> InfoTableBuilder m ()
+  RegisterFunction :: TypeSignature 'Scoped -> InfoTableBuilder m ()
+
+makeSem ''InfoTableBuilder
+
+registerFunction' ::
+  Member InfoTableBuilder r =>
+  TypeSignature 'Scoped -> Sem r (TypeSignature 'Scoped)
+registerFunction' ts = registerFunction ts $> ts
+
+registerInductive' :: Member InfoTableBuilder r =>
+  InductiveDef 'Scoped -> Sem r (InductiveDef 'Scoped)
+registerInductive' i = registerInductive i $> i
+
+registerConstructor' :: Member InfoTableBuilder r =>
+  InductiveConstructorDef 'Scoped -> Sem r (InductiveConstructorDef 'Scoped)
+registerConstructor' c = registerConstructor c $> c
+
+registerAxiom' :: Member InfoTableBuilder r =>
+  AxiomDef 'Scoped -> Sem r (AxiomDef 'Scoped)
+registerAxiom' a = registerAxiom a $> a
+
+toState :: Sem (InfoTableBuilder ': r) a -> Sem (State InfoTable ': r) a
+toState = reinterpret $ \case
+  RegisterAxiom d ->
+    let ref = AxiomRef' (unqualifiedSymbol (d ^. axiomName))
+        info = AxiomInfo {
+          _axiomInfoType = d ^. axiomType,
+          _axiomInfoBackends = d ^. axiomBackendItems
+          }
+    in modify (over infoAxioms (HashMap.insert ref info))
+  RegisterConstructor c -> let
+      ref = ConstructorRef' (unqualifiedSymbol (c ^. constructorName))
+      info = ConstructorInfo {
+        _constructorInfoType = c ^. constructorType
+      }
+      in modify (over infoConstructors  (HashMap.insert ref info)
+   )
+  RegisterInductive ity -> let
+        ref = InductiveRef' (unqualifiedSymbol (ity ^. inductiveName))
+        info = InductiveInfo {
+          _inductiveInfoDef = ity
+        }
+      in modify (over infoInductives  (HashMap.insert ref info)
+   )
+  RegisterFunction f -> let
+      ref = FunctionRef' (unqualifiedSymbol (f ^. sigName))
+      info = FunctionInfo {
+        _functionInfoType = f ^. sigType
+      }
+      in modify (over infoFunctions  (HashMap.insert ref info)
+   )
+
+runInfoTableBuilder :: Sem (InfoTableBuilder ': r) a -> Sem r (InfoTable, a)
+runInfoTableBuilder = runState emptyInfoTable . toState

src/MiniJuvix/Syntax/Concrete/Scoped/Utils.hs

@@ -1,9 +1,9 @@
 module MiniJuvix.Syntax.Concrete.Scoped.Utils where
 
+import qualified Data.HashMap.Strict as HashMap
+import MiniJuvix.Prelude
 import MiniJuvix.Syntax.Concrete.Language
 import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
-import MiniJuvix.Prelude
-import qualified Data.HashMap.Strict as HashMap
 
 data ScopedModule = forall t. MkScopedModule (SModuleIsTop t) (Module 'Scoped t)
 
@@ -12,14 +12,14 @@ mkScopedModule = MkScopedModule sing
 
 getAllModules :: Module 'Scoped 'ModuleTop -> HashMap S.NameId (Module 'Scoped 'ModuleTop)
 getAllModules m =
-   HashMap.fromList $ singl m : [ singl n | Import n <- allImports (mkScopedModule m) ]
+  HashMap.fromList $ singl m : [singl n | Import n <- allImports (mkScopedModule m)]
   where
-  allImports :: ScopedModule -> [Import 'Scoped]
-  allImports (MkScopedModule _ w) =
-    concat [ i : allImports (mkScopedModule t) | StatementImport i@(Import t) <- _moduleBody w ]
-    <> concatMap (allImports . mkScopedModule ) [ l | StatementModule l <- _moduleBody w]
-  singl :: Module 'Scoped 'ModuleTop -> (S.NameId, Module 'Scoped 'ModuleTop)
-  singl n = (S._nameId (_modulePath n), n)
+    allImports :: ScopedModule -> [Import 'Scoped]
+    allImports (MkScopedModule _ w) =
+      concat [i : allImports (mkScopedModule t) | StatementImport i@(Import t) <- _moduleBody w]
+        <> concatMap (allImports . mkScopedModule) [l | StatementModule l <- _moduleBody w]
+    singl :: Module 'Scoped 'ModuleTop -> (S.NameId, Module 'Scoped 'ModuleTop)
+    singl n = (S._nameId (_modulePath n), n)
 
 getModuleFilePath :: Module 'Scoped 'ModuleTop -> FilePath
 getModuleFilePath = _intFile . getLoc . _modulePath

src/MiniJuvix/Syntax/Concrete/Scoped/VisibilityAnn.hs

@@ -0,0 +1,8 @@
+module MiniJuvix.Syntax.Concrete.Scoped.VisibilityAnn where
+
+import MiniJuvix.Prelude
+
+data VisibilityAnn
+  = VisPublic
+  | VisPrivate
+  deriving stock (Show, Eq, Ord)

src/MiniJuvix/Syntax/Fixity.hs

@@ -3,8 +3,8 @@ module MiniJuvix.Syntax.Fixity where
 import Language.Haskell.TH.Syntax (Lift)
 import MiniJuvix.Prelude
 
-data Precedence =
-  PrecMinusOmega
+data Precedence
+  = PrecMinusOmega
   | PrecNat Natural
   | PrecOmega
   deriving stock (Show, Eq, Lift)
@@ -40,8 +40,8 @@ data Fixity = Fixity
   }
   deriving stock (Show, Eq, Ord, Lift)
 
-data Atomicity =
-  Atom
+data Atomicity
+  = Atom
   | Aggregate Fixity
 
 class HasAtomicity a where
@@ -52,18 +52,18 @@ class HasFixity a where
 
 isLeftAssoc :: Fixity -> Bool
 isLeftAssoc opInf = case fixityArity opInf of
-    Binary AssocLeft -> True
-    _ -> False
+  Binary AssocLeft -> True
+  _ -> False
 
 isRightAssoc :: Fixity -> Bool
 isRightAssoc opInf = case fixityArity opInf of
-    Binary AssocRight -> True
-    _ -> False
+  Binary AssocRight -> True
+  _ -> False
 
 isPostfixAssoc :: Fixity -> Bool
 isPostfixAssoc opInf = case fixityArity opInf of
-    Unary AssocPostfix -> True
-    _ -> False
+  Unary AssocPostfix -> True
+  _ -> False
 
 appFixity :: Fixity
 appFixity = Fixity PrecOmega (Binary AssocLeft)
@@ -75,10 +75,10 @@ atomParens :: (Fixity -> Bool) -> Atomicity -> Fixity -> Bool
 atomParens associates argAtom opInf = case argAtom of
   Atom -> False
   Aggregate argInf
-   | argInf > opInf -> False
-   | argInf < opInf -> True
-   | associates opInf -> False
-   | otherwise -> True
+    | argInf > opInf -> False
+    | argInf < opInf -> True
+    | associates opInf -> False
+    | otherwise -> True
 
 isAtomic :: HasAtomicity a => a -> Bool
 isAtomic x = case atomicity x of

src/MiniJuvix/Syntax/MicroJuvix/Language.hs

@@ -1,25 +1,30 @@
-module MiniJuvix.Syntax.MicroJuvix.Language (
-  module MiniJuvix.Syntax.MicroJuvix.Language,
-  module MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind,
-  module MiniJuvix.Syntax.Concrete.Scoped.Name
-   ) where
+module MiniJuvix.Syntax.MicroJuvix.Language
+  ( module MiniJuvix.Syntax.MicroJuvix.Language,
+    module MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind,
+    module MiniJuvix.Syntax.Concrete.Scoped.Name,
+  )
+where
 
 import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Concrete.Language (ForeignBlock (..))
+import MiniJuvix.Syntax.Concrete.Scoped.Name (NameId (..))
 import MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind
-import MiniJuvix.Syntax.Concrete.Language (ForeignBlock(..))
-import MiniJuvix.Syntax.Concrete.Scoped.Name (NameId(..))
 import MiniJuvix.Syntax.Fixity
 
 type FunctionName = Name
+
 type VarName = Name
+
 type ConstrName = Name
+
 type InductiveName = Name
 
-data Name = Name {
-    _nameText :: Text,
+data Name = Name
+  { _nameText :: Text,
     _nameId :: NameId,
     _nameKind :: NameKind
-    }
+  }
+
 makeLenses ''Name
 
 instance Eq Name where
@@ -39,25 +44,25 @@ data Module = Module
     _moduleBody :: ModuleBody
   }
 
-data ModuleBody = ModuleBody {
-  _moduleInductives :: HashMap InductiveName (Indexed InductiveDef),
-  _moduleFunctions :: HashMap FunctionName (Indexed FunctionDef),
-  _moduleForeign :: [Indexed ForeignBlock]
+data ModuleBody = ModuleBody
+  { _moduleInductives :: HashMap InductiveName (Indexed InductiveDef),
+    _moduleFunctions :: HashMap FunctionName (Indexed FunctionDef),
+    _moduleForeigns :: [Indexed ForeignBlock]
   }
 
-data FunctionDef = FunctionDef {
-   _funDefName :: FunctionName,
-   _funDefTypeSig :: Type,
-   _funDefClauses :: NonEmpty FunctionClause
+data FunctionDef = FunctionDef
+  { _funDefName :: FunctionName,
+    _funDefTypeSig :: Type,
+    _funDefClauses :: NonEmpty FunctionClause
   }
 
-data FunctionClause = FunctionClause {
-    _clausePatterns :: [Pattern],
+data FunctionClause = FunctionClause
+  { _clausePatterns :: [Pattern],
     _clauseBody :: Expression
   }
 
-data Iden =
-  IdenDefined Name
+data Iden
+  = IdenFunction Name
   | IdenConstructor Name
   | IdenVar VarName
 
@@ -65,20 +70,20 @@ data Expression
   = ExpressionIden Iden
   | ExpressionApplication Application
 
-data Application = Application {
-  _appLeft :: Expression,
-  _appRight :: Expression
+data Application = Application
+  { _appLeft :: Expression,
+    _appRight :: Expression
   }
 
-data Function = Function {
-  _funLeft :: Type,
-  _funRight :: Type
+data Function = Function
+  { _funLeft :: Type,
+    _funRight :: Type
   }
 
 -- | Fully applied constructor in a pattern.
-data ConstructorApp = ConstructorApp {
-  _constrAppConstructor :: Name,
-  _constrAppParameters :: [Pattern]
+data ConstructorApp = ConstructorApp
+  { _constrAppConstructor :: Name,
+    _constrAppParameters :: [Pattern]
   }
 
 data Pattern
@@ -96,12 +101,12 @@ data InductiveConstructorDef = InductiveConstructorDef
     _constructorParameters :: [Type]
   }
 
-newtype TypeIden =
-  TypeIdenInductive InductiveName
+newtype TypeIden
+  = TypeIdenInductive InductiveName
 
-data Type =
-  TypeIden TypeIden
- | TypeFunction Function
+data Type
+  = TypeIden TypeIden
+  | TypeFunction Function
 
 makeLenses ''Module
 makeLenses ''Function
@@ -114,18 +119,20 @@ makeLenses ''InductiveConstructorDef
 makeLenses ''ConstructorApp
 
 instance Semigroup ModuleBody where
-  a <> b = ModuleBody {
-    _moduleInductives = a ^. moduleInductives <> b ^. moduleInductives,
-    _moduleFunctions = a ^. moduleFunctions <> b ^. moduleFunctions,
-    _moduleForeign = a ^. moduleForeign <> b ^. moduleForeign
-    }
+  a <> b =
+    ModuleBody
+      { _moduleInductives = a ^. moduleInductives <> b ^. moduleInductives,
+        _moduleFunctions = a ^. moduleFunctions <> b ^. moduleFunctions,
+        _moduleForeigns = a ^. moduleForeigns <> b ^. moduleForeigns
+      }
 
 instance Monoid ModuleBody where
-  mempty = ModuleBody {
-    _moduleInductives = mempty,
-    _moduleForeign = mempty,
-    _moduleFunctions = mempty
-    }
+  mempty =
+    ModuleBody
+      { _moduleInductives = mempty,
+        _moduleForeigns = mempty,
+        _moduleFunctions = mempty
+      }
 
 instance HasAtomicity Application where
   atomicity = const (Aggregate appFixity)
@@ -145,8 +152,8 @@ instance HasAtomicity Type where
 
 instance HasAtomicity ConstructorApp where
   atomicity (ConstructorApp _ args)
-   | null args = Atom
-   | otherwise = Aggregate appFixity
+    | null args = Atom
+    | otherwise = Aggregate appFixity
 
 instance HasAtomicity Pattern where
   atomicity p = case p of

src/MiniJuvix/Syntax/MicroJuvix/Pretty/Ann.hs

@@ -2,8 +2,8 @@ module MiniJuvix.Syntax.MicroJuvix.Pretty.Ann where
 
 import MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind
 
-data Ann =
-  AnnKind NameKind
+data Ann
+  = AnnKind NameKind
   | AnnKeyword
   | AnnLiteralString
   | AnnLiteralInteger

src/MiniJuvix/Syntax/MicroJuvix/Pretty/Ansi.hs

@@ -1,9 +1,9 @@
 module MiniJuvix.Syntax.MicroJuvix.Pretty.Ansi where
 
-import MiniJuvix.Syntax.MicroJuvix.Language
-import MiniJuvix.Syntax.MicroJuvix.Pretty.Base
-import MiniJuvix.Syntax.MicroJuvix.Pretty.Ann
 import MiniJuvix.Prelude
+import MiniJuvix.Syntax.MicroJuvix.Language
+import MiniJuvix.Syntax.MicroJuvix.Pretty.Ann
+import MiniJuvix.Syntax.MicroJuvix.Pretty.Base
 import Prettyprinter
 import Prettyprinter.Render.Terminal
 
@@ -20,8 +20,11 @@ renderPrettyCode :: PrettyCode c => Options -> c -> Text
 renderPrettyCode opts = renderStrict . docStream opts
 
 docStream :: PrettyCode c => Options -> c -> SimpleDocStream AnsiStyle
-docStream opts = reAnnotateS stylize . layoutPretty defaultLayoutOptions
-    . run . runReader opts . ppCode
+docStream opts =
+  reAnnotateS stylize . layoutPretty defaultLayoutOptions
+    . run
+    . runReader opts
+    . ppCode
 
 stylize :: Ann -> AnsiStyle
 stylize a = case a of

src/MiniJuvix/Syntax/MicroJuvix/Pretty/Base.hs

@@ -1,39 +1,39 @@
 -- TODO handle capital letters and characters not supported by Haskell.
 module MiniJuvix.Syntax.MicroJuvix.Pretty.Base where
 
-
-import MiniJuvix.Prelude
-import Prettyprinter
-import MiniJuvix.Syntax.Fixity
-import MiniJuvix.Syntax.MicroJuvix.Pretty.Ann
-import MiniJuvix.Syntax.MicroJuvix.Language
-import MiniJuvix.Syntax.Concrete.Language (ForeignBlock(..))
 import qualified MiniJuvix.Internal.Strings as Str
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Concrete.Language (Backend (..), ForeignBlock (..))
+import MiniJuvix.Syntax.Fixity
+import MiniJuvix.Syntax.MicroJuvix.Language
+import MiniJuvix.Syntax.MicroJuvix.Pretty.Ann
+import Prettyprinter
 
 newtype Options = Options
-  {
-    _optIndent :: Int
+  { _optIndent :: Int
   }
 
 defaultOptions :: Options
-defaultOptions = Options {
-  _optIndent = 2
-  }
+defaultOptions =
+  Options
+    { _optIndent = 2
+    }
 
 class PrettyCode c where
   ppCode :: Member (Reader Options) r => c -> Sem r (Doc Ann)
 
 instance PrettyCode Name where
   ppCode n =
-    return $ annotate (AnnKind (n ^. nameKind))
-           $ pretty (n ^. nameText) <> "_" <> pretty (n ^. nameId)
+    return $
+      annotate (AnnKind (n ^. nameKind)) $
+        pretty (n ^. nameText) <> "_" <> pretty (n ^. nameId)
 
 instance PrettyCode Iden where
   ppCode :: Member (Reader Options) r => Iden -> Sem r (Doc Ann)
   ppCode i = case i of
-   IdenDefined na -> ppCode na
-   IdenConstructor na -> ppCode na
-   IdenVar na -> ppCode na
+    IdenFunction na -> ppCode na
+    IdenConstructor na -> ppCode na
+    IdenVar na -> ppCode na
 
 instance PrettyCode Application where
   ppCode a = do
@@ -52,6 +52,16 @@ keyword = annotate AnnKeyword . pretty
 kwArrow :: Doc Ann
 kwArrow = keyword Str.toAscii
 
+kwForeign :: Doc Ann
+kwForeign = keyword Str.foreign_
+
+kwAgda :: Doc Ann
+kwAgda = keyword Str.agda
+
+kwGhc :: Doc Ann
+kwGhc = keyword Str.ghc
+
+
 kwData :: Doc Ann
 kwData = keyword Str.data_
 
@@ -119,60 +129,84 @@ instance PrettyCode FunctionDef where
     funDefName' <- ppCode (f ^. funDefName)
     funDefTypeSig' <- ppCode (f ^. funDefTypeSig)
     clauses' <- mapM (ppClause funDefName') (f ^. funDefClauses)
-    return $ funDefName' <+> kwColonColon <+> funDefTypeSig' <> line
-      <> vsep (toList clauses')
-     where
-     ppClause fun c = do
-       clausePatterns' <- mapM ppCodeAtom (c ^. clausePatterns)
-       clauseBody' <- ppCode (c ^. clauseBody)
-       return $ fun <+> hsep clausePatterns' <+> kwEquals <+> clauseBody'
+    return $
+      funDefName' <+> kwColonColon <+> funDefTypeSig' <> line
+        <> vsep (toList clauses')
+    where
+      ppClause fun c = do
+        clausePatterns' <- mapM ppCodeAtom (c ^. clausePatterns)
+        clauseBody' <- ppCode (c ^. clauseBody)
+        return $ fun <+> hsep clausePatterns' <+> kwEquals <+> clauseBody'
+
+instance PrettyCode Backend where
+  ppCode = \case
+    BackendGhc  -> return kwGhc
+    BackendAgda -> return kwAgda
 
 instance PrettyCode ForeignBlock where
   ppCode ForeignBlock {..} = do
     _foreignBackend' <- ppCode _foreignBackend
-    return $ kwForeign <+> _foreignBackend' <+> lbrace <> line
-        <> pretty _foreignCode <> line <> rbrace
-
+    return $
+      kwForeign <+> _foreignBackend' <+> lbrace <> line
+        <> pretty _foreignCode
+        <> line
+        <> rbrace
 
 -- TODO Jonathan review
 instance PrettyCode ModuleBody where
   ppCode m = do
     types' <- mapM (mapM ppCode) (toList (m ^. moduleInductives))
     funs' <- mapM (mapM ppCode) (toList (m ^. moduleFunctions))
-    let foreigns' = m ^. moduleForeign
-    let everything = map (^. indexedThing) (sortOn (^. indexedIx) (types' ++ funs'))
+    foreigns' <- mapM (mapM ppCode) (toList (m ^. moduleForeigns))
+    let everything = map (^. indexedThing) (sortOn (^. indexedIx) (types' ++ funs' ++ foreigns'))
     return $ vsep2 everything
     where
-    vsep2 = concatWith (\a b -> a <> line <> line <> b)
+      vsep2 = concatWith (\a b -> a <> line <> line <> b)
 
 instance PrettyCode Module where
   ppCode m = do
     name' <- ppCode (m ^. moduleName)
     body' <- ppCode (m ^. moduleBody)
-    return $ kwModule <+> name' <+> kwWhere
-      <> line <> line <> body' <> line
+    return $
+      kwModule <+> name' <+> kwWhere
+        <> line
+        <> line
+        <> body'
+        <> line
 
 parensCond :: Bool -> Doc Ann -> Doc Ann
 parensCond t d = if t then parens d else d
 
-ppPostExpression ::(PrettyCode a, HasAtomicity a, Member (Reader Options) r)  =>
-  Fixity -> a -> Sem r (Doc Ann)
+ppPostExpression ::
+  (PrettyCode a, HasAtomicity a, Member (Reader Options) r) =>
+  Fixity ->
+  a ->
+  Sem r (Doc Ann)
 ppPostExpression = ppLRExpression isPostfixAssoc
 
-ppRightExpression :: (PrettyCode a, HasAtomicity a, Member (Reader Options) r) =>
-  Fixity -> a -> Sem r (Doc Ann)
+ppRightExpression ::
+  (PrettyCode a, HasAtomicity a, Member (Reader Options) r) =>
+  Fixity ->
+  a ->
+  Sem r (Doc Ann)
 ppRightExpression = ppLRExpression isRightAssoc
 
-ppLeftExpression :: (PrettyCode a, HasAtomicity a, Member (Reader Options) r) =>
-  Fixity -> a -> Sem r (Doc Ann)
+ppLeftExpression ::
+  (PrettyCode a, HasAtomicity a, Member (Reader Options) r) =>
+  Fixity ->
+  a ->
+  Sem r (Doc Ann)
 ppLeftExpression = ppLRExpression isLeftAssoc
 
-ppLRExpression
-  :: (HasAtomicity a, PrettyCode a, Member (Reader Options) r) =>
-     (Fixity -> Bool) -> Fixity -> a -> Sem r (Doc Ann)
+ppLRExpression ::
+  (HasAtomicity a, PrettyCode a, Member (Reader Options) r) =>
+  (Fixity -> Bool) ->
+  Fixity ->
+  a ->
+  Sem r (Doc Ann)
 ppLRExpression associates fixlr e =
   parensCond (atomParens associates (atomicity e) fixlr)
-      <$> ppCode e
+    <$> ppCode e
 
 ppCodeAtom :: (HasAtomicity c, PrettyCode c, Members '[Reader Options] r) => c -> Sem r (Doc Ann)
 ppCodeAtom c = do

src/MiniJuvix/Syntax/MiniHaskell/Language.hs

@@ -1,23 +1,28 @@
-module MiniJuvix.Syntax.MiniHaskell.Language (
-  module MiniJuvix.Syntax.MiniHaskell.Language,
-  module MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind,
-  module MiniJuvix.Syntax.Concrete.Scoped.Name
-   ) where
+module MiniJuvix.Syntax.MiniHaskell.Language
+  ( module MiniJuvix.Syntax.MiniHaskell.Language,
+    module MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind,
+    module MiniJuvix.Syntax.Concrete.Scoped.Name,
+  )
+where
 
 import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Concrete.Scoped.Name (NameId (..))
 import MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind
-import MiniJuvix.Syntax.Concrete.Scoped.Name (NameId(..))
 import MiniJuvix.Syntax.Fixity
 
 type FunctionName = Name
+
 type VarName = Name
+
 type ConstrName = Name
+
 type InductiveName = Name
 
-data Name = Name {
-    _nameText :: Text,
+data Name = Name
+  { _nameText :: Text,
     _nameKind :: NameKind
-    }
+  }
+
 makeLenses ''Name
 
 instance HasNameKind Name where
@@ -28,23 +33,23 @@ data Module = Module
     _moduleBody :: ModuleBody
   }
 
-newtype ModuleBody = ModuleBody {
-  _moduleStatements :: [Statement]
+newtype ModuleBody = ModuleBody
+  { _moduleStatements :: [Statement]
   }
   deriving newtype (Monoid, Semigroup)
 
-data Statement =
-  StatementInductiveDef InductiveDef
+data Statement
+  = StatementInductiveDef InductiveDef
   | StatementFunctionDef FunctionDef
 
-data FunctionDef = FunctionDef {
-   _funDefName :: FunctionName,
-   _funDefTypeSig :: Type,
-   _funDefClauses :: NonEmpty FunctionClause
+data FunctionDef = FunctionDef
+  { _funDefName :: FunctionName,
+    _funDefTypeSig :: Type,
+    _funDefClauses :: NonEmpty FunctionClause
   }
 
-data FunctionClause = FunctionClause {
-    _clausePatterns :: [Pattern],
+data FunctionClause = FunctionClause
+  { _clausePatterns :: [Pattern],
     _clauseBody :: Expression
   }
 
@@ -53,22 +58,23 @@ type Iden = Name
 data Expression
   = ExpressionIden Iden
   | ExpressionApplication Application
-  -- TODO Add a constructor for literals
 
-data Application = Application {
-  _appLeft :: Expression,
-  _appRight :: Expression
+-- TODO Add a constructor for literals
+
+data Application = Application
+  { _appLeft :: Expression,
+    _appRight :: Expression
   }
 
-data Function = Function {
-  _funLeft :: Type,
-  _funRight :: Type
+data Function = Function
+  { _funLeft :: Type,
+    _funRight :: Type
   }
 
 -- | Fully applied constructor in a pattern.
-data ConstructorApp = ConstructorApp {
-  _constrAppConstructor :: Name,
-  _constrAppParameters :: [Pattern]
+data ConstructorApp = ConstructorApp
+  { _constrAppConstructor :: Name,
+    _constrAppParameters :: [Pattern]
   }
 
 data Pattern
@@ -88,9 +94,9 @@ data InductiveConstructorDef = InductiveConstructorDef
 
 type TypeIden = InductiveName
 
-data Type =
-  TypeIden TypeIden
- | TypeFunction Function
+data Type
+  = TypeIden TypeIden
+  | TypeFunction Function
 
 makeLenses ''Module
 makeLenses ''Function
@@ -120,8 +126,8 @@ instance HasAtomicity Type where
 
 instance HasAtomicity ConstructorApp where
   atomicity (ConstructorApp _ args)
-   | null args = Atom
-   | otherwise = Aggregate appFixity
+    | null args = Atom
+    | otherwise = Aggregate appFixity
 
 instance HasAtomicity Pattern where
   atomicity p = case p of

src/MiniJuvix/Syntax/MiniHaskell/Pretty/Ann.hs

@@ -2,8 +2,8 @@ module MiniJuvix.Syntax.MiniHaskell.Pretty.Ann where
 
 import MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind
 
-data Ann =
-  AnnKind NameKind
+data Ann
+  = AnnKind NameKind
   | AnnKeyword
   | AnnLiteralString
   | AnnLiteralInteger

src/MiniJuvix/Syntax/MiniHaskell/Pretty/Ansi.hs

@@ -1,9 +1,9 @@
 module MiniJuvix.Syntax.MiniHaskell.Pretty.Ansi where
 
-import MiniJuvix.Syntax.MiniHaskell.Language
-import MiniJuvix.Syntax.MiniHaskell.Pretty.Base
-import MiniJuvix.Syntax.MiniHaskell.Pretty.Ann
 import MiniJuvix.Prelude
+import MiniJuvix.Syntax.MiniHaskell.Language
+import MiniJuvix.Syntax.MiniHaskell.Pretty.Ann
+import MiniJuvix.Syntax.MiniHaskell.Pretty.Base
 import Prettyprinter
 import Prettyprinter.Render.Terminal
 
@@ -20,8 +20,11 @@ renderPrettyCode :: PrettyCode c => Options -> c -> Text
 renderPrettyCode opts = renderStrict . docStream opts
 
 docStream :: PrettyCode c => Options -> c -> SimpleDocStream AnsiStyle
-docStream opts = reAnnotateS stylize . layoutPretty defaultLayoutOptions
-    . run . runReader opts . ppCode
+docStream opts =
+  reAnnotateS stylize . layoutPretty defaultLayoutOptions
+    . run
+    . runReader opts
+    . ppCode
 
 stylize :: Ann -> AnsiStyle
 stylize a = case a of