Merge pull request #14 from heliaxdev/wip3

v0.1.1
2024-12-15 01:52:11 +03:00 · 2022-03-25 18:15:37 +01:00 · 2022-03-25 18:15:37 +01:00 · eee91cbb43
commit eee91cbb43
parent 37bafc7b55 674559d069
92 changed files with 1052 additions and 1088 deletions
--- a/CHANGELOG.md
+++ b/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
--- a/CHANGELOG.org
+++ b/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
--- a/77
+++ b/77
@ -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,34 +37,17 @@ 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 : test
-test:
-	stack test --fast --jobs $(THREADS)
-
-.PHONY : install
-install:
-	stack install --fast --jobs $(THREADS)
-
 .PHONY : build
 build:
 	stack build --fast --jobs $(THREADS)

-stack-build-watch:
+build-watch:
 	stack build --fast --file-watch

-repl:
-	stack ghci MiniJuvix:lib
+
+.PHONY : cabal
+cabal :
+	cabal build all

 clean:
 	cabal clean
@ -76,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
--- a/README.org
+++ b/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]]
--- a/agda-proofs/minijuvix-proofs.agda-lib
+++ b/agda-proofs/minijuvix-proofs.agda-lib
@ -1,4 +0,0 @@
-name: minijuvix-proofs
-depend: standard-library
-include: proofs
-flags:
--- a/agda-proofs/proofs/Algebra/Structures/StarSemiring.agda
+++ b/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))
--- a/agda-proofs/proofs/Base.agda
+++ b/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
--- a/agda-proofs/proofs/Termination/FunctionCall.agda
+++ b/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 }
--- a/agda-proofs/proofs/Termination/SizeRelation.agda
+++ b/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
--- a/agda-proofs/proofs/Termination/SizeRelation/Properties.agda
+++ b/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 }
--- a/app/Commands/Extra.hs
+++ b/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"
+    )
--- a/app/Commands/MicroJuvix.hs
+++ b/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
--- a/app/Commands/MiniHaskell.hs
+++ b/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
--- a/app/Commands/Termination.hs
+++ b/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
--- a/app/Main.hs
+++ b/app/Main.hs
@ -1,29 +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 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
@ -32,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
@ -59,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
@ -97,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"
@ -112,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
@ -126,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
@ -148,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
@ -157,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
@ -166,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
@ -175,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
@ -183,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
@ -193,7 +219,6 @@ parseCommand =
            (Termination <$> parseTerminationCommand)
            (progDesc "Subcommands related to termination checking")

-
 mkScopePrettyOptions :: ScopeOptions -> M.Options
 mkScopePrettyOptions ScopeOptions {..} =
  M.defaultOptions
@ -204,51 +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
+      (_ , s) <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m
      -- a <- fromRightIO' putStrLn (return $ A.translateModule s)
-      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
--- a/src/MiniJuvix/Syntax/Core.agda
+++ b/src/MiniJuvix/Syntax/Core.agda
--- a/src/MiniJuvix/Syntax/Core.hs
+++ b/src/MiniJuvix/Syntax/Core.hs
@ -6,7 +6,7 @@ module MiniJuvix.Syntax.Core where

 --------------------------------------------------------------------------------

-import Algebra.Graph.Label (Semiring (..))
+-- import Algebra.Graph.Label (Semiring (..))
 import MiniJuvix.Prelude hiding (Local)
 import Numeric.Natural (Natural)

--- a/src/MiniJuvix/Syntax/Eval.agda
+++ b/src/MiniJuvix/Syntax/Eval.agda
--- a/src/MiniJuvix/Syntax/Eval.hs
+++ b/src/MiniJuvix/Syntax/Eval.hs
--- a/lab/Syntax/Makefile
+++ b/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
--- a/lab/Syntax/minijuvix.agda-lib
+++ b/lab/Syntax/minijuvix.agda-lib
--- a/src/MiniJuvix/Termination/CallGraphOld.hs
+++ b/src/MiniJuvix/Termination/CallGraphOld.hs
--- a/lab/docs/Agda.css
+++ b/lab/docs/Agda.css
--- a/lab/docs/README.md
+++ b/lab/docs/README.md
--- a/lab/docs/_config.yml
+++ b/lab/docs/_config.yml
--- a/lab/docs/conv.sh
+++ b/lab/docs/conv.sh
--- a/lab/docs/examples/Example1.mjuvix
+++ b/lab/docs/examples/Example1.mjuvix
--- a/lab/docs/examples/Example2.mjuvix
+++ b/lab/docs/examples/Example2.mjuvix
--- a/lab/docs/examples/Example3.mjuvix
+++ b/lab/docs/examples/Example3.mjuvix
--- a/lab/docs/examples/FirstMilestone.mjuvix
+++ b/lab/docs/examples/FirstMilestone.mjuvix
--- a/lab/docs/examples/declarations/module/Makefile
+++ b/lab/docs/examples/declarations/module/Makefile
--- a/lab/docs/examples/declarations/module/examples/A.mjuvix
+++ b/lab/docs/examples/declarations/module/examples/A.mjuvix
--- a/lab/docs/examples/declarations/module/examples/AA.mjuvix
+++ b/lab/docs/examples/declarations/module/examples/AA.mjuvix
--- a/lab/docs/examples/declarations/module/examples/E0.mjuvix
+++ b/lab/docs/examples/declarations/module/examples/E0.mjuvix
--- a/lab/docs/examples/declarations/module/examples/E1.mjuvix
+++ b/lab/docs/examples/declarations/module/examples/E1.mjuvix
--- a/lab/docs/examples/declarations/module/examples/E2.mjuvix
+++ b/lab/docs/examples/declarations/module/examples/E2.mjuvix
--- a/lab/docs/examples/declarations/module/examples/E3.mjuvix
+++ b/lab/docs/examples/declarations/module/examples/E3.mjuvix
--- a/lab/docs/examples/declarations/module/examples/T.mjuvix
+++ b/lab/docs/examples/declarations/module/examples/T.mjuvix
--- a/lab/docs/examples/declarations/module/fail/E0.test
+++ b/lab/docs/examples/declarations/module/fail/E0.test
--- a/lab/docs/examples/declarations/module/fail/E1.test
+++ b/lab/docs/examples/declarations/module/fail/E1.test
--- a/lab/docs/examples/declarations/module/fail/E2.test
+++ b/lab/docs/examples/declarations/module/fail/E2.test
--- a/lab/docs/examples/declarations/module/fail/E3.test
+++ b/lab/docs/examples/declarations/module/fail/E3.test
--- a/lab/docs/examples/declarations/module/fail/T.test
+++ b/lab/docs/examples/declarations/module/fail/T.test
--- a/lab/docs/examples/declarations/module/succeed/A.test
+++ b/lab/docs/examples/declarations/module/succeed/A.test
--- a/lab/docs/examples/declarations/module/succeed/T.test
+++ b/lab/docs/examples/declarations/module/succeed/T.test
--- a/lab/docs/examples/syntax.miniju
+++ b/lab/docs/examples/syntax.miniju
--- a/lab/docs/examples/token.mjuvix
+++ b/lab/docs/examples/token.mjuvix
--- a/lab/docs/main.css
+++ b/lab/docs/main.css
--- a/lab/docs/minijuvix.png
+++ b/lab/docs/minijuvix.png
--- a/lab/docs/notes/Example.agda
+++ b/lab/docs/notes/Example.agda
--- a/lab/docs/notes/forTesting.md
+++ b/lab/docs/notes/forTesting.md
--- a/lab/docs/notes/module-scoping.org
+++ b/lab/docs/notes/module-scoping.org
--- a/lab/docs/notes/tooling.md
+++ b/lab/docs/notes/tooling.md
--- a/lab/docs/template.html5
+++ b/lab/docs/template.html5
--- a/package.yaml
+++ b/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,34 +66,24 @@ ghc-options:

 default-extensions:
 - DataKinds
- DeriveFoldable
- DeriveGeneric
- DeriveLift
- DeriveTraversable
 - DerivingStrategies
- FlexibleContexts
- FlexibleInstances
 - GADTs
- GeneralizedNewtypeDeriving
- InstanceSigs
- KindSignatures
 - LambdaCase
 - NoImplicitPrelude
 - OverloadedStrings
- PolyKinds
 - QuasiQuotes
- RankNTypes
 - RecordWildCards
- ScopedTypeVariables
- StandaloneDeriving
 - TemplateHaskell
- TypeApplications
 - TypeFamilyDependencies
- TypeOperators
 - UnicodeSyntax

+# verbatim:
+#   default-language: GHC2021
+
 library:
  source-dirs: src
+  verbatim:
+    default-language: GHC2021

 executables:
  minijuvix:
@ -97,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:
@ -106,3 +101,5 @@ tests:
    source-dirs:         test
    dependencies:
    - minijuvix
+    verbatim:
+      default-language: GHC2021
--- a/src/MiniJuvix/Internal/Strings.hs
+++ b/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"

--- a/src/MiniJuvix/Prelude/Base.hs
+++ b/src/MiniJuvix/Prelude/Base.hs
@ -1,53 +1,53 @@
 module MiniJuvix.Prelude.Base
  ( module MiniJuvix.Prelude.Base,
+    module Control.Applicative,
    module Control.Monad.Extra,
-    module Data.Char,
    module Control.Monad.Fix,
-    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 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.Fixpoint,
-    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,
@ -232,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)
--- a/src/MiniJuvix/Syntax/Concrete/Language.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Language.hs
@ -1,9 +1,9 @@
 {-# LANGUAGE UndecidableInstances #-}
-
 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,
@ -21,6 +21,7 @@ import MiniJuvix.Syntax.Concrete.Language.Stage
 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
@ -33,31 +34,39 @@ import Prelude (show)
 --------------------------------------------------------------------------------
 -- Parsing stages
 --------------------------------------------------------------------------------
-type family RefNameType (c :: S.IsConcrete) :: (res :: GHC.Type) | res -> c 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 family SymbolType (s :: Stage) :: (res :: GHC.Type) | res -> s where
+type SymbolType :: Stage -> GHC.Type
+type family SymbolType s = res | res -> s where
  SymbolType 'Parsed = Symbol
  SymbolType 'Scoped = S.Symbol

-type family ModuleRefType (s :: Stage) :: (res :: GHC.Type) | res -> s where
+type ModuleRefType :: Stage -> GHC.Type
+type family ModuleRefType s = res | res -> s where
  ModuleRefType 'Parsed = Name
  ModuleRefType 'Scoped = ModuleRef

-type family IdentifierType (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 family PatternAtomIdenType (s :: Stage) :: (res :: GHC.Type) | res -> s where
+type PatternAtomIdenType :: Stage -> GHC.Type
+type family PatternAtomIdenType s = res | res -> s where
  PatternAtomIdenType 'Parsed = Name
  PatternAtomIdenType 'Scoped = PatternScopedIden

-type family ExpressionType (s :: Stage) :: (res :: GHC.Type) | res -> s where
+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

@ -65,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
@ -200,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)
@ -239,15 +247,15 @@ 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 :: ConstructorRef,
-    patInfixRight :: Pattern
+  { _patInfixLeft :: Pattern,
+    _patInfixConstructor :: ConstructorRef,
+    _patInfixRight :: Pattern
  }
  deriving stock (Show, Eq, Ord)

@ -255,8 +263,8 @@ instance HasFixity PatternInfixApp where
  getFixity (PatternInfixApp _ op _) = fromMaybe impossible (_constructorRefName op ^. S.nameFixity)

 data PatternPostfixApp = PatternPostfixApp
-  { patPostfixParameter :: Pattern,
-    patPostfixConstructor :: ConstructorRef
+  { _patPostfixParameter :: Pattern,
+    _patPostfixConstructor :: ConstructorRef
  }
  deriving stock (Show, Eq, Ord)

@ -493,8 +501,7 @@ data SymbolEntry
  | EntryInductive (InductiveRef' 'S.NotConcrete)
  | EntryFunction (FunctionRef' 'S.NotConcrete)
  | EntryConstructor (ConstructorRef' 'S.NotConcrete)
-  | -- | TODO does this ever contain top modules?
-    EntryModule (ModuleRef' 'S.NotConcrete)
+  | EntryModule (ModuleRef' 'S.NotConcrete)
  deriving stock (Show)

 -- | Symbols that a module exports
@ -504,10 +511,10 @@ newtype ExportInfo = ExportInfo
  deriving stock (Show)

 data OpenModule (s :: Stage) = OpenModule
-  { openModuleName :: ModuleRefType s,
-    openParameters :: [ExpressionType s],
-    openUsingHiding :: Maybe UsingHiding,
-    openPublic :: PublicAnn
+  { _openModuleName :: ModuleRefType s,
+    _openParameters :: [ExpressionType s],
+    _openUsingHiding :: Maybe UsingHiding,
+    _openPublic :: PublicAnn
  }

 deriving stock instance
@ -541,11 +548,11 @@ deriving stock instance

 type AxiomRef = AxiomRef' 'S.Concrete

-data AxiomRef' (n :: S.IsConcrete) = AxiomRef'
-  { _axiomRefName :: RefNameType n,
-    _axiomRefType :: Expression,
-    _axiomRefBackends :: HashMap Backend Text
-  }
+newtype AxiomRef' (n :: S.IsConcrete) = AxiomRef'
+  { _axiomRefName :: RefNameType n}
+
+instance Hashable (RefNameType s) => Hashable (AxiomRef' s) where
+  hashWithSalt i = hashWithSalt i . _axiomRefName

 instance Eq (RefNameType s) => Eq (AxiomRef' s) where
  (==) = (==) `on` _axiomRefName
@ -558,11 +565,13 @@ instance Show (RefNameType s) => Show (AxiomRef' s) where

 type InductiveRef = InductiveRef' 'S.Concrete

-data InductiveRef' (n :: S.IsConcrete) = InductiveRef'
-  { _inductiveRefName :: RefNameType n,
-    _inductiveRefDef :: InductiveDef 'Scoped
+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

@ -574,11 +583,13 @@ instance Show (RefNameType s) => Show (InductiveRef' s) where

 type FunctionRef = FunctionRef' 'S.Concrete

-data FunctionRef' (n :: S.IsConcrete) = FunctionRef'
-  { _functionRefName :: RefNameType n,
-    _functionRefSig :: Expression
+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

@ -590,11 +601,13 @@ instance Show (RefNameType s) => Show (FunctionRef' s) where

 type ConstructorRef = ConstructorRef' 'S.Concrete

-data ConstructorRef' (n :: S.IsConcrete) = ConstructorRef'
-  { _constructorRefName :: RefNameType n,
-    _constructorSig :: Expression
+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

@ -1098,6 +1111,7 @@ deriving stock instance
  Ord (Print s)

 makeLenses ''InductiveDef
+makeLenses ''InductiveConstructorDef
 makeLenses ''Module
 makeLenses ''TypeSignature
 makeLenses ''AxiomDef
@ -1111,6 +1125,10 @@ 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
@ -1134,6 +1152,9 @@ 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'')

--- a/src/MiniJuvix/Syntax/Concrete/Lexer.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Lexer.hs
@ -50,7 +50,14 @@ integer = do
 -- | TODO allow escaping { inside the string using \{
 bracedString :: MonadParsec e Text m => m Text
 bracedString =
-  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 '"'))
--- a/src/MiniJuvix/Syntax/Concrete/Name.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Name.hs
@ -90,4 +90,10 @@ topModulePathToFilePath' ext root mp = absPath
    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
--- a/src/MiniJuvix/Syntax/Concrete/Parser.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Parser.hs
@ -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 {..}

 --------------------------------------------------------------------------------
@ -415,10 +415,10 @@ 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
--- a/src/MiniJuvix/Syntax/Concrete/Scoped/Error.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Error.hs
@ -31,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
--- a/src/MiniJuvix/Syntax/Concrete/Scoped/Error/Pretty/Ansi.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Error/Pretty/Ansi.hs
@ -2,6 +2,8 @@ module MiniJuvix.Syntax.Concrete.Scoped.Error.Pretty.Ansi where

 import MiniJuvix.Prelude
 import MiniJuvix.Syntax.Concrete.Scoped.Error.Pretty.Base
+import qualified MiniJuvix.Syntax.Concrete.Scoped.Pretty.Ansi as S
+
 import Prettyprinter
 import Prettyprinter.Render.Terminal

@ -11,3 +13,4 @@ renderAnsi = renderStrict . reAnnotateS stylize
 stylize :: Eann -> AnsiStyle
 stylize a = case a of
  Highlight -> colorDull Red
+  ScopedAnn s -> S.stylize s
--- a/src/MiniJuvix/Syntax/Concrete/Scoped/Error/Pretty/Base.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Error/Pretty/Base.hs
@ -13,6 +13,7 @@ import Prettyprinter
 import Text.EditDistance

 data Eann = Highlight
+  | ScopedAnn P.Ann

 highlight :: Doc Eann -> Doc Eann
 highlight = annotate Highlight
@ -21,7 +22,7 @@ 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
@ -154,9 +155,14 @@ instance PrettyError UnusedOperatorDef where
      <> 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))
--- a/src/MiniJuvix/Syntax/Concrete/Scoped/Error/Types.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Error/Types.hs
@ -94,12 +94,14 @@ data WrongTopModuleName = WrongTopModuleName
  }
  deriving stock (Show)

-newtype AmbiguousSym = AmbiguousSym
-  { _ambiguousSymEntires :: [SymbolEntry]
+data AmbiguousSym = AmbiguousSym
+  { _ambiguousSymName :: Name,
+    _ambiguousSymEntires :: [SymbolEntry]
  }
  deriving stock (Show)

-newtype AmbiguousModuleSym = AmbiguousModuleSym
-  { _ambiguousModSymEntires :: [SymbolEntry]
+data AmbiguousModuleSym = AmbiguousModuleSym
+  { _ambiguousModName :: Name,
+    _ambiguousModSymEntires :: [SymbolEntry]
  }
  deriving stock (Show)
--- a/src/MiniJuvix/Syntax/Concrete/Scoped/Name.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Name.hs
@ -11,7 +11,7 @@ import Lens.Micro.Platform
 import MiniJuvix.Prelude
 import MiniJuvix.Syntax.Concrete.Loc
 import qualified MiniJuvix.Syntax.Concrete.Name as C
-import MiniJuvix.Syntax.Concrete.PublicAnn
+import MiniJuvix.Syntax.Concrete.Scoped.VisibilityAnn
 import MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind
 import qualified MiniJuvix.Syntax.Fixity as C
 import Prettyprinter
@ -90,7 +90,9 @@ data Name' n = Name'
    _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)

--- a/src/MiniJuvix/Syntax/Concrete/Scoped/Name/NameKind.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Name/NameKind.hs
@ -57,7 +57,7 @@ nameKindAnsi k = case k of
  KNameConstructor -> colorDull Magenta
  KNameInductive -> colorDull Green
  KNameAxiom -> colorDull Red
-  KNameLocalModule -> mempty
+  KNameLocalModule -> color Cyan
  KNameFunction -> colorDull Yellow
  KNameLocal -> mempty
-  KNameTopModule -> mempty
+  KNameTopModule -> color Cyan
--- a/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Base.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Base.hs
@ -17,7 +17,7 @@ data Options = Options
  { _optShowNameId :: Bool,
    _optInlineImports :: Bool,
    _optIndent :: Int
-  }
+}

 defaultOptions :: Options
 defaultOptions =
@ -178,6 +178,9 @@ parens = enclose kwParenL kwParenR
 doubleQuotes :: Doc Ann -> Doc Ann
 doubleQuotes = enclose kwDQuote kwDQuote

+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) =>
@ -222,7 +225,7 @@ groupStatements = reverse . map reverse . uncurry cons . foldl' aux ([], [])
        SParsed -> True
        SScoped ->
          S._nameId (_modulePath (importModule i))
-            == S._nameId (projSigma2 _moduleRefName (openModuleName o ^. unModuleRef'))
+            == S._nameId (projSigma2 _moduleRefName (o ^. openModuleName . unModuleRef'))
      (StatementImport _, _) -> False
      (StatementOpenModule {}, StatementOpenModule {}) -> True
      (StatementOpenModule {}, _) -> False
@ -256,10 +259,10 @@ groupStatements = reverse . map reverse . uncurry cons . foldl' aux ([], [])
      where
        syms :: InductiveDef s -> [Symbol]
        syms InductiveDef {..} = case sing :: SStage s of
-          SParsed -> _inductiveName : map constructorName _inductiveConstructors
+          SParsed -> _inductiveName : map _constructorName _inductiveConstructors
          SScoped ->
            S._nameConcrete _inductiveName :
-            map (S._nameConcrete . constructorName) _inductiveConstructors
+            map (S._nameConcrete . _constructorName) _inductiveConstructors

 instance SingI s => PrettyCode [Statement s] where
  ppCode ss = joinGroups <$> mapM (fmap mkGroup . mapM (fmap endSemicolon . ppCode)) (groupStatements ss)
@ -290,8 +293,9 @@ instance PrettyCode ForeignBlock where
  ppCode ForeignBlock {..} = do
    _foreignBackend' <- ppCode _foreignBackend
    return $
-      kwForeign <+> _foreignBackend' <+> lbrace
+      kwForeign <+> _foreignBackend' <+> lbrace <> line
        <> pretty _foreignCode
+        <> line
        <> rbrace

 instance PrettyCode BackendItem where
@ -354,7 +358,7 @@ instance (SingI s, SingI t) => PrettyCode (Module s t) where
    where
      lastSemicolon = case sing :: SModuleIsTop t of
        SModuleLocal -> Nothing
-        SModuleTop -> Just kwSemicolon
+        SModuleTop -> Just (kwSemicolon <> line)

 instance PrettyCode Precedence where
  ppCode p = return $ case p of
@ -384,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
@ -442,7 +446,7 @@ 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)
@ -457,9 +461,9 @@ instance SingI s => PrettyCode (OpenModule s) where
  ppCode :: forall r. Members '[Reader Options] r => OpenModule s -> Sem r (Doc Ann)
  ppCode OpenModule {..} = do
    openModuleName' <- case sing :: SStage s of
-      SParsed -> ppCode openModuleName
-      SScoped -> ppCode openModuleName
-    openUsingHiding' <- sequence $ ppUsingHiding <$> openUsingHiding
+      SParsed -> ppCode _openModuleName
+      SScoped -> ppCode _openModuleName
+    openUsingHiding' <- sequence $ ppUsingHiding <$> _openUsingHiding
    openParameters' <- ppOpenParams
    let openPublic' = ppPublic
    return $ keyword "open" <+> openModuleName' <+?> openParameters' <+?> openUsingHiding' <+?> openPublic'
@ -468,9 +472,9 @@ instance SingI s => PrettyCode (OpenModule s) where
        SParsed -> ppCodeAtom
        SScoped -> ppCodeAtom
      ppOpenParams :: Sem r (Maybe (Doc Ann))
-      ppOpenParams = case openParameters of
+      ppOpenParams = case _openParameters of
        [] -> return Nothing
-        _ -> Just . hsep <$> mapM ppAtom' openParameters
+        _ -> Just . hsep <$> mapM ppAtom' _openParameters
      ppUsingHiding :: UsingHiding -> Sem r (Doc Ann)
      ppUsingHiding uh = do
        bracedList <-
@ -482,7 +486,7 @@ instance SingI s => PrettyCode (OpenModule s) where
            Using s -> (kwUsing, s)
            Hiding s -> (kwHiding, s)
      ppPublic :: Maybe (Doc Ann)
-      ppPublic = case openPublic of
+      ppPublic = case _openPublic of
        Public -> Just kwPublic
        NoPublic -> Nothing

@ -723,15 +727,15 @@ instance PrettyCode Pattern where
    where
      ppPatternInfixApp :: PatternInfixApp -> Sem r (Doc Ann)
      ppPatternInfixApp p@PatternInfixApp {..} = do
-        patInfixConstructor' <- ppCode patInfixConstructor
-        patInfixLeft' <- ppLeftExpression (getFixity p) patInfixLeft
-        patInfixRight' <- ppRightExpression (getFixity p) patInfixRight
+        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
+        patPostfixConstructor' <- ppCode _patPostfixConstructor
+        patPostfixParameter' <- ppLeftExpression (getFixity p) _patPostfixParameter
        return $ patPostfixParameter' <+> patPostfixConstructor'

 parensCond :: Bool -> Doc Ann -> Doc Ann
@ -792,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)
--- a/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Html.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Html.hs
@ -55,7 +55,7 @@ genHtml opts recursive theme entry = do
      putStrLn $ "Writing " <> pack htmlFile
      Text.writeFile htmlFile (genModule opts theme m)
      where
-        htmlFile = dottedPath (S._nameConcrete (_modulePath m)) <.> ".html"
+        htmlFile = topModulePathToDottedPath (S._nameConcrete (_modulePath m)) <.> ".html"

 genModule :: Options -> Theme -> Module 'Scoped 'ModuleTop -> Text
 genModule opts theme m =
@ -105,9 +105,6 @@ go sdt = case sdt of
    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
@ -141,18 +138,12 @@ putTag ann x = case ann of
              S.KNameTopModule -> "ju-var"
          )

-dottedPath :: IsString s => TopModulePath -> s
-dottedPath (TopModulePath l r) =
-  fromText $ mconcat $ intersperse "." $ map fromSymbol $ l ++ [r]
-  where
-    fromSymbol Symbol {..} = _symbolText
-
 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 =
--- a/src/MiniJuvix/Syntax/Concrete/Scoped/Scope.hs
+++ b/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
@ -34,7 +35,42 @@ data Scope = Scope
  }
  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
@ -73,3 +109,11 @@ emptyScope absPath =
      _scopeTopModules = mempty,
      _scopeBindGroup = mempty
    }
+
+emptyInfoTable :: InfoTable
+emptyInfoTable = InfoTable {
+  _infoConstructors = mempty,
+  _infoAxioms = mempty,
+  _infoInductives = mempty,
+  _infoFunctions = mempty
+  }
--- a/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper.hs
@ -1,8 +1,6 @@
 -- | Limitations:
 -- 1. A symbol introduced by a type signature can only be used once per Module.
 --
-- Efficiency considerations:
-- 1. The expression parser should be cached somehow. Consider Polysemy.View
 module MiniJuvix.Syntax.Concrete.Scoped.Scoper where

 import qualified Control.Monad.Combinators.Expr as P
@ -18,31 +16,34 @@ import MiniJuvix.Syntax.Concrete.Language
 import MiniJuvix.Syntax.Concrete.Parser (runModuleParser)
 import MiniJuvix.Syntax.Concrete.Scoped.Error
 import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
+import qualified MiniJuvix.Syntax.Concrete.Name as N
 import MiniJuvix.Syntax.Concrete.Scoped.Scope
 import MiniJuvix.Syntax.Concrete.Scoped.Scoper.Files
+import MiniJuvix.Syntax.Concrete.Scoped.Scoper.InfoTableBuilder

 --------------------------------------------------------------------------------

-scopeCheck1IO :: FilePath -> Module 'Parsed 'ModuleTop -> IO (Either ScopeError (Module 'Scoped 'ModuleTop))
+scopeCheck1IO :: FilePath -> Module 'Parsed 'ModuleTop -> IO (Either ScopeError (InfoTable, Module 'Scoped 'ModuleTop))
 scopeCheck1IO root = runFinal . embedToFinal @IO . runFilesIO . fixpointToFinal @IO . scopeCheck1 root

-scopeCheck1Pure :: HashMap FilePath Text -> FilePath -> Module 'Parsed 'ModuleTop -> Either ScopeError (Module 'Scoped 'ModuleTop)
+scopeCheck1Pure :: HashMap FilePath Text -> FilePath -> Module 'Parsed 'ModuleTop -> Either ScopeError (InfoTable, Module 'Scoped 'ModuleTop)
 scopeCheck1Pure fs root = runIdentity . runFinal . runFilesPure fs . fixpointToFinal @Identity . scopeCheck1 root

 scopeCheck1 ::
  Members [Files, Fixpoint] r =>
  FilePath ->
  Module 'Parsed 'ModuleTop ->
-  Sem r (Either ScopeError (Module 'Scoped 'ModuleTop))
-scopeCheck1 root m = fmap head <$> scopeCheck root (pure m)
+  Sem r (Either ScopeError (InfoTable, Module 'Scoped 'ModuleTop))
+scopeCheck1 root m = fmap (second head) <$> scopeCheck root (pure m)

 scopeCheck ::
  Members [Files, Fixpoint] r =>
  FilePath ->
  NonEmpty (Module 'Parsed 'ModuleTop) ->
-  Sem r (Either ScopeError (NonEmpty (Module 'Scoped 'ModuleTop)))
+  Sem r (Either ScopeError (InfoTable, NonEmpty (Module 'Scoped 'ModuleTop)))
 scopeCheck root modules =
  runError $
+   runInfoTableBuilder $
    runReader scopeParameters $
      evalState iniScoperState $
        mapM checkTopModule_ modules
@ -84,7 +85,8 @@ freshSymbol _nameKind _nameConcrete = do
  _nameDefinedIn <- gets _scopePath
  let _nameDefined = getLoc _nameConcrete
      _nameWhyInScope = S.BecauseDefined
-      _namePublicAnn = NoPublic
+      _nameVisibilityAnn = VisPublic
+      _nameVerbatim = _symbolText _nameConcrete
  _nameFixity <- fixity
  return S.Name' {..}
  where
@ -148,44 +150,39 @@ bindSymbolOf k e s = do

 bindFunctionSymbol ::
  Members '[Error ScopeError, State ScoperState, State Scope] r =>
-  Expression ->
  Symbol ->
  Sem r S.Symbol
-bindFunctionSymbol sig =
+bindFunctionSymbol =
  bindSymbolOf
    S.KNameFunction
-    (\s' -> EntryFunction (FunctionRef' s' sig))
+    (\s' -> EntryFunction (FunctionRef' s'))

 bindInductiveSymbol ::
  Members '[Error ScopeError, State ScoperState, State Scope] r =>
-  InductiveDef 'Scoped ->
  Symbol ->
  Sem r S.Symbol
-bindInductiveSymbol def =
+bindInductiveSymbol =
  bindSymbolOf
    S.KNameInductive
-    (\s' -> EntryInductive (InductiveRef' s' def))
+    (\s' -> EntryInductive (InductiveRef' s'))

 bindAxiomSymbol ::
  Members '[Error ScopeError, State ScoperState, State Scope] r =>
-  HashMap Backend Text ->
-  Expression ->
  Symbol ->
  Sem r S.Symbol
-bindAxiomSymbol backends ty =
+bindAxiomSymbol =
  bindSymbolOf
    S.KNameAxiom
-    (\s' -> EntryAxiom (AxiomRef' s' ty backends))
+    (\s' -> EntryAxiom (AxiomRef' s'))

 bindConstructorSymbol ::
  Members '[Error ScopeError, State ScoperState, State Scope] r =>
-  Expression ->
  Symbol ->
  Sem r S.Symbol
-bindConstructorSymbol sig =
+bindConstructorSymbol =
  bindSymbolOf
    S.KNameConstructor
-    (\s' -> EntryConstructor (ConstructorRef' s' sig))
+    (\s' -> EntryConstructor (ConstructorRef' s'))

 bindLocalModuleSymbol ::
  Members '[Error ScopeError, State ScoperState, State Scope] r =>
@ -200,7 +197,7 @@ bindLocalModuleSymbol _moduleExportInfo _moduleRefModule =

 checkImport ::
  forall r.
-  Members '[Error ScopeError, State Scope, Reader ScopeParameters, Files, State ScoperState, Fixpoint] r =>
+  Members '[Error ScopeError, State Scope, Reader ScopeParameters, Files, State ScoperState, Fixpoint, InfoTableBuilder] r =>
  Import 'Parsed ->
  Sem r (Import 'Scoped)
 checkImport import_@(Import path) = do
@ -249,12 +246,9 @@ lookupSymbolAux modules final = do
      case modules of
        [] -> do
          r <- HashMap.lookup final <$> gets _scopeSymbols
-          case r of
-            Nothing -> return []
-            Just SymbolInfo {..} -> case toList _symbolInfo of
-              [] -> return []
-              [e] -> return [e]
-              es -> throw (ErrAmbiguousSym (AmbiguousSym es))
+          return $ case r of
+            Nothing -> []
+            Just SymbolInfo {..} -> toList _symbolInfo
        (p : ps) ->
          mapMaybe (lookInExport final ps . getModuleExportInfo) . concat . maybeToList . fmap (mapMaybe getModuleRef . toList . _symbolInfo)
            . HashMap.lookup p
@ -321,14 +315,11 @@ checkQualifiedExpr q@(QualifiedName (Path p) sym) = do
  case es of
    [] -> notInScope
    [e] -> return (entryToScopedIden q' e)
-    _ -> throw (ErrAmbiguousSym (AmbiguousSym es))
+    _ -> throw (ErrAmbiguousSym (AmbiguousSym q' es))
  where
    q' = NameQualified q
    notInScope = throw (ErrQualSymNotInScope q)

-unqualifiedSName :: S.Symbol -> S.Name
-unqualifiedSName = over S.nameConcrete NameUnqualified
-
 entryToScopedIden :: Name -> SymbolEntry -> ScopedIden
 entryToScopedIden name = \case
  EntryAxiom ref -> ScopedAxiom (set (axiomRefName . S.nameConcrete) name ref)
@ -350,9 +341,7 @@ exportScope Scope {..} = do
    getExportSymbols = HashMap.fromList <$> mapMaybeM entry (HashMap.toList _scopeSymbols)
      where
        shouldExport :: SymbolEntry -> Bool
-        shouldExport ent =
-          _nameDefinedIn == _scopePath
-            || _namePublicAnn == Public
+        shouldExport ent = _nameVisibilityAnn == VisPublic
          where
            S.Name' {..} = entryName ent

@ -403,34 +392,30 @@ checkOperatorSyntaxDef s@OperatorSyntaxDef {..} = do
        (\s' -> throw (ErrDuplicateFixity (DuplicateFixity s' s)))

 checkTypeSignature ::
-  Members '[Error ScopeError, State Scope, State ScoperState, Reader LocalVars] r =>
+  Members '[Error ScopeError, State Scope, State ScoperState, Reader LocalVars , InfoTableBuilder] r =>
  TypeSignature 'Parsed ->
  Sem r (TypeSignature 'Scoped)
 checkTypeSignature TypeSignature {..} = do
  sigType' <- checkParseExpressionAtoms _sigType
-  sigName' <- bindFunctionSymbol sigType' _sigName
-  return
-    TypeSignature
-      { _sigName = sigName',
-        _sigType = sigType'
-      }
+  sigName' <- bindFunctionSymbol _sigName
+  registerFunction' TypeSignature {_sigName = sigName', _sigType = sigType'}

 checkConstructorDef ::
-  Members '[Error ScopeError, Reader LocalVars, State Scope, State ScoperState] r =>
+  Members '[Error ScopeError, Reader LocalVars, State Scope, State ScoperState , InfoTableBuilder] r =>
  InductiveConstructorDef 'Parsed ->
  Sem r (InductiveConstructorDef 'Scoped)
 checkConstructorDef InductiveConstructorDef {..} = do
-  constructorType' <- checkParseExpressionAtoms constructorType
-  constructorName' <- bindConstructorSymbol constructorType' constructorName
-  return
+  constructorType' <- checkParseExpressionAtoms _constructorType
+  constructorName' <- bindConstructorSymbol _constructorName
+  registerConstructor'
    InductiveConstructorDef
-      { constructorName = constructorName',
-        constructorType = constructorType'
+      { _constructorName = constructorName',
+        _constructorType = constructorType'
      }

 withParams ::
  forall r a.
-  Members '[Reader LocalVars, Error ScopeError, State Scope, State ScoperState] r =>
+  Members '[Reader LocalVars, Error ScopeError, State Scope, State ScoperState , InfoTableBuilder] r =>
  [InductiveParameter 'Parsed] ->
  ([InductiveParameter 'Scoped] -> Sem r a) ->
  Sem r a
@ -455,33 +440,32 @@ withParams xs a = go [] xs

 checkInductiveDef ::
  forall r.
-  Members '[Error ScopeError, State Scope, State ScoperState, Fixpoint, Reader LocalVars] r =>
+  Members '[Error ScopeError, State Scope, State ScoperState, Reader LocalVars, InfoTableBuilder] r =>
  InductiveDef 'Parsed ->
  Sem r (InductiveDef 'Scoped)
 checkInductiveDef InductiveDef {..} = do
  withParams _inductiveParameters $ \inductiveParameters' -> do
    inductiveType' <- sequence (checkParseExpressionAtoms <$> _inductiveType)
-    mfix $ \scopedDef -> do
-      inductiveName' <- bindInductiveSymbol scopedDef _inductiveName
-      inductiveConstructors' <- mapM checkConstructorDef _inductiveConstructors
-      return
-        InductiveDef
-          { _inductiveName = inductiveName',
-            _inductiveParameters = inductiveParameters',
-            _inductiveType = inductiveType',
-            _inductiveConstructors = inductiveConstructors'
-          }
+    inductiveName' <- bindInductiveSymbol _inductiveName
+    inductiveConstructors' <- mapM checkConstructorDef _inductiveConstructors
+    registerInductive'
+      InductiveDef
+        { _inductiveName = inductiveName',
+          _inductiveParameters = inductiveParameters',
+          _inductiveType = inductiveType',
+          _inductiveConstructors = inductiveConstructors'
+        }

 checkTopModule_ ::
  forall r.
-  Members '[Error ScopeError, Reader ScopeParameters, Files, State ScoperState, Fixpoint] r =>
+  Members '[Error ScopeError, Reader ScopeParameters, Files, State ScoperState, Fixpoint , InfoTableBuilder] r =>
  Module 'Parsed 'ModuleTop ->
  Sem r (Module 'Scoped 'ModuleTop)
 checkTopModule_ = fmap (^. moduleRefModule) . checkTopModule

 checkTopModule ::
  forall r.
-  Members '[Error ScopeError, Reader ScopeParameters, Files, State ScoperState, Fixpoint] r =>
+  Members '[Error ScopeError, Reader ScopeParameters, Files, State ScoperState, Fixpoint , InfoTableBuilder ] r =>
  Module 'Parsed 'ModuleTop ->
  Sem r (ModuleRef'' 'S.NotConcrete 'ModuleTop)
 checkTopModule m@(Module path params body) = do
@ -514,8 +498,10 @@ checkTopModule m@(Module path params body) = do
          _nameDefined = getLoc (_modulePathName path)
          _nameKind = S.KNameTopModule
          _nameFixity = Nothing
-          _namePublicAnn = NoPublic
+          -- This visibility annotation is not relevant
+          _nameVisibilityAnn = VisPublic
          _nameWhyInScope = S.BecauseDefined
+          _nameVerbatim = N.topModulePathToDottedPath path
      return S.Name' {..}
    iniScope :: Scope
    iniScope = emptyScope (getTopModulePath m)
@ -544,7 +530,7 @@ withScope ma = do

 checkModuleBody ::
  forall r.
-  Members '[Error ScopeError, State Scope, Reader ScopeParameters, State ScoperState, Files, Reader LocalVars, Fixpoint] r =>
+  Members '[Error ScopeError, State Scope, Reader ScopeParameters, State ScoperState, Files, Reader LocalVars, Fixpoint , InfoTableBuilder ] r =>
  [Statement 'Parsed] ->
  Sem r (ExportInfo, [Statement 'Scoped])
 checkModuleBody body = do
@ -556,7 +542,7 @@ checkModuleBody body = do

 checkLocalModule ::
  forall r.
-  Members '[Error ScopeError, State Scope, Reader ScopeParameters, State ScoperState, Files, Reader LocalVars, Fixpoint] r =>
+  Members '[Error ScopeError, State Scope, Reader ScopeParameters, State ScoperState, Files, Reader LocalVars, Fixpoint , InfoTableBuilder ] r =>
  Module 'Parsed 'ModuleLocal ->
  Sem r (Module 'Scoped 'ModuleLocal)
 checkLocalModule Module {..} = do
@ -591,7 +577,7 @@ checkLocalModule Module {..} = do
        inheritSymbol :: SymbolInfo -> SymbolInfo
        inheritSymbol (SymbolInfo s) = SymbolInfo (fmap inheritEntry s)
        inheritEntry :: SymbolEntry -> SymbolEntry
-        inheritEntry = entryOverName (over S.nameWhyInScope S.BecauseInherited)
+        inheritEntry = entryOverName (over S.nameWhyInScope S.BecauseInherited . set S.nameVisibilityAnn VisPrivate)

 checkClausesExist :: forall r. Members '[Error ScopeError, State Scope] r => [Statement 'Scoped] -> Sem r ()
 checkClausesExist ss = whenJust msig (throw . ErrLacksFunctionClause . LacksFunctionClause)
@ -625,7 +611,7 @@ lookupModuleSymbol n = do
  case mapMaybe getModuleRef es of
    [] -> notInScope
    [x] -> return (overModuleRef'' (set (moduleRefName . S.nameConcrete) n) x)
-    _ -> throw (ErrAmbiguousModuleSym (AmbiguousModuleSym es))
+    _ -> throw (ErrAmbiguousModuleSym (AmbiguousModuleSym n es))
  where
    notInScope = throw (ErrModuleNotInScope (ModuleNotInScope n))
    (path, sym) = case n of
@ -651,19 +637,18 @@ getExportInfo modId = do

 checkOpenModule ::
  forall r.
-  Members '[Error ScopeError, State Scope, State ScoperState, Reader LocalVars] r =>
+  Members '[Error ScopeError, State Scope, State ScoperState, Reader LocalVars , InfoTableBuilder] r =>
  OpenModule 'Parsed ->
  Sem r (OpenModule 'Scoped)
 checkOpenModule OpenModule {..} = do
-  openModuleName'@(ModuleRef' (_ :&: moduleRef'')) <- lookupModuleSymbol openModuleName
-  openParameters' <- mapM checkParseExpressionAtoms openParameters
+  openModuleName'@(ModuleRef' (_ :&: moduleRef'')) <- lookupModuleSymbol _openModuleName
+  openParameters' <- mapM checkParseExpressionAtoms _openParameters
  mergeScope (alterScope (moduleRef'' ^. moduleExportInfo))
  return
    OpenModule
-      { openModuleName = openModuleName',
-        openParameters = openParameters',
-        openUsingHiding = openUsingHiding,
-        openPublic = openPublic
+      { _openModuleName = openModuleName',
+        _openParameters = openParameters',
+        ..
      }
  where
    mergeScope :: ExportInfo -> Sem r ()
@ -675,7 +660,7 @@ checkOpenModule OpenModule {..} = do
          modify
            (over scopeSymbols (HashMap.insertWith (<>) s (symbolInfoSingle entry)))
    setsUsingHiding :: Maybe (Either (HashSet Symbol) (HashSet Symbol))
-    setsUsingHiding = case openUsingHiding of
+    setsUsingHiding = case _openUsingHiding of
      Just (Using l) -> Just (Left (HashSet.fromList (toList l)))
      Just (Hiding l) -> Just (Right (HashSet.fromList (toList l)))
      Nothing -> Nothing
@ -683,9 +668,14 @@ checkOpenModule OpenModule {..} = do
    alterScope = alterEntries . filterScope
      where
        alterEntry :: SymbolEntry -> SymbolEntry
-        alterEntry = entryOverName (set S.nameWhyInScope S.BecauseImportedOpened . set S.namePublicAnn openPublic)
+        alterEntry = entryOverName (set S.nameWhyInScope S.BecauseImportedOpened
+                                    . set S.nameVisibilityAnn (publicAnnToVis _openPublic))
        alterEntries :: ExportInfo -> ExportInfo
        alterEntries = over exportSymbols (fmap alterEntry)
+        publicAnnToVis :: PublicAnn -> VisibilityAnn
+        publicAnnToVis = \case
+          Public -> VisPublic
+          NoPublic -> VisPrivate
        filterScope :: ExportInfo -> ExportInfo
        filterScope = over exportSymbols filterTable
          where
@ -699,14 +689,15 @@ checkOpenModule OpenModule {..} = do

 checkWhereBlock ::
  forall r.
-  Members '[Error ScopeError, State Scope, State ScoperState, Reader LocalVars] r =>
+  Members '[Error ScopeError, State Scope, State ScoperState, Reader LocalVars , InfoTableBuilder
+  ] r =>
  WhereBlock 'Parsed ->
  Sem r (WhereBlock 'Scoped)
 checkWhereBlock WhereBlock {..} = WhereBlock <$> mapM checkWhereClause whereClauses

 checkWhereClause ::
  forall r.
-  Members '[Error ScopeError, State Scope, State ScoperState, Reader LocalVars] r =>
+  Members '[Error ScopeError, State Scope, State ScoperState, Reader LocalVars, InfoTableBuilder] r =>
  WhereClause 'Parsed ->
  Sem r (WhereClause 'Scoped)
 checkWhereClause c = case c of
@ -716,7 +707,7 @@ checkWhereClause c = case c of

 checkFunctionClause ::
  forall r.
-  Members '[Error ScopeError, State Scope, State ScoperState, Reader LocalVars] r =>
+  Members '[Error ScopeError, State Scope, State ScoperState, Reader LocalVars , InfoTableBuilder] r =>
  FunctionClause 'Parsed ->
  Sem r (FunctionClause 'Scoped)
 checkFunctionClause clause@FunctionClause {..} = do
@ -761,37 +752,32 @@ lookupLocalEntry sym = do
    HashMap.lookup path _symbolInfo

 checkAxiomDef ::
-  Members '[Error ScopeError, State Scope, State ScoperState] r =>
+  Members '[InfoTableBuilder, Error ScopeError, State Scope, State ScoperState] r =>
  AxiomDef 'Parsed ->
  Sem r (AxiomDef 'Scoped)
 checkAxiomDef AxiomDef {..} = do
  axiomType' <- localScope $ checkParseExpressionAtoms _axiomType
-  axiomName' <- bindAxiomSymbol undefined axiomType' _axiomName
-  return
-    AxiomDef
-      { _axiomName = axiomName',
-        _axiomType = axiomType',
-        ..
-      }
+  axiomName' <- bindAxiomSymbol _axiomName
+  registerAxiom' AxiomDef {_axiomName = axiomName', _axiomType = axiomType', ..}

 localScope :: Sem (Reader LocalVars : r) a -> Sem r a
 localScope = runReader (LocalVars mempty)

 checkEval ::
-  Members '[Error ScopeError, State Scope, State ScoperState] r =>
+  Members '[Error ScopeError, State Scope, State ScoperState , InfoTableBuilder] r =>
  Eval 'Parsed ->
  Sem r (Eval 'Scoped)
 checkEval (Eval s) = Eval <$> localScope (checkParseExpressionAtoms s)

 checkPrint ::
-  Members '[Error ScopeError, State Scope, State ScoperState] r =>
+  Members '[Error ScopeError, State Scope, State ScoperState, InfoTableBuilder] r =>
  Print 'Parsed ->
  Sem r (Print 'Scoped)
 checkPrint (Print s) = Print <$> localScope (checkParseExpressionAtoms s)

 checkFunction ::
  forall r.
-  Members '[Error ScopeError, State Scope, State ScoperState, Reader LocalVars] r =>
+  Members '[Error ScopeError, State Scope, State ScoperState, Reader LocalVars , InfoTableBuilder] r =>
  Function 'Parsed ->
  Sem r (Function 'Scoped)
 checkFunction Function {..} = do
@ -823,23 +809,16 @@ checkFunction Function {..} = do
          Nothing -> return Nothing
          Just s -> Just <$> freshVariable s

-- | Like a regular type signature?
-checkLocalTypeSig ::
-  Members '[Error ScopeError, State Scope, State ScoperState, Reader LocalVars] r =>
-  TypeSignature 'Parsed ->
-  Sem r (TypeSignature 'Scoped)
-checkLocalTypeSig = checkTypeSignature
-
 checkLetClause ::
-  Members '[Error ScopeError, State Scope, State ScoperState, Reader LocalVars] r =>
+  Members '[Error ScopeError, State Scope, State ScoperState, Reader LocalVars , InfoTableBuilder] r =>
  LetClause 'Parsed ->
  Sem r (LetClause 'Scoped)
 checkLetClause lc = case lc of
-  LetTypeSig t -> LetTypeSig <$> checkLocalTypeSig t
+  LetTypeSig t -> LetTypeSig <$> checkTypeSignature t
  LetFunClause c -> LetFunClause <$> checkFunctionClause c

 checkLetBlock ::
-  Members '[Error ScopeError, State Scope, State ScoperState, Reader LocalVars] r =>
+  Members '[Error ScopeError, State Scope, State ScoperState, Reader LocalVars , InfoTableBuilder] r =>
  LetBlock 'Parsed ->
  Sem r (LetBlock 'Scoped)
 checkLetBlock LetBlock {..} = do
@ -854,13 +833,13 @@ checkLetBlock LetBlock {..} = do
      }

 checkLambda ::
-  Members '[Error ScopeError, State Scope, State ScoperState, Reader LocalVars] r =>
+  Members '[Error ScopeError, State Scope, State ScoperState, Reader LocalVars , InfoTableBuilder] r =>
  Lambda 'Parsed ->
  Sem r (Lambda 'Scoped)
 checkLambda Lambda {..} = Lambda <$> mapM checkLambdaClause lambdaClauses

 checkLambdaClause ::
-  Members '[Error ScopeError, State Scope, State ScoperState, Reader LocalVars] r =>
+  Members '[Error ScopeError, State Scope, State ScoperState, Reader LocalVars , InfoTableBuilder] r =>
  LambdaClause 'Parsed ->
  Sem r (LambdaClause 'Scoped)
 checkLambdaClause LambdaClause {..} = do
@ -891,8 +870,10 @@ checkUnqualified s = do
          <$> lookupQualifiedSymbol ([], s)
      case entries of
        [] -> err
-        [x] -> return (entryToScopedIden (NameUnqualified s) x)
-        es -> throw (ErrAmbiguousSym (AmbiguousSym es))
+        [x] -> return (entryToScopedIden n x)
+        es -> throw (ErrAmbiguousSym (AmbiguousSym n es))
+      where
+        n = NameUnqualified s

 checkPatternName ::
  forall r.
@ -917,7 +898,7 @@ checkPatternName n = do
          Nothing -> return Nothing -- There is no constructor with such a name
          Just pth -> throw (ErrQualSymNotInScope (QualifiedName pth sym))
        [e] -> return (Just (set (constructorRefName . S.nameConcrete) n e)) -- There is one constructor with such a name
-        _ -> throw $ ErrGeneric "There is more than one constructor with such a name"
+        es -> throw (ErrAmbiguousSym (AmbiguousSym n (map EntryConstructor es)))
    getConstructor :: SymbolEntry -> Maybe (ConstructorRef' 'S.NotConcrete)
    getConstructor = \case
      EntryConstructor r -> Just r
@ -998,7 +979,7 @@ checkName n = case n of
  NameUnqualified s -> checkUnqualified s

 checkExpressionAtom ::
-  Members '[Error ScopeError, State Scope, State ScoperState, Reader LocalVars] r =>
+  Members '[Error ScopeError, State Scope, State ScoperState, Reader LocalVars , InfoTableBuilder] r =>
  ExpressionAtom 'Parsed ->
  Sem r (ExpressionAtom 'Scoped)
 checkExpressionAtom e = case e of
@ -1013,7 +994,7 @@ checkExpressionAtom e = case e of
  AtomMatch match -> AtomMatch <$> checkMatch match

 checkParens ::
-  Members '[Error ScopeError, State Scope, State ScoperState, Reader LocalVars] r =>
+  Members '[Error ScopeError, State Scope, State ScoperState, Reader LocalVars , InfoTableBuilder] r =>
  ExpressionAtoms 'Parsed ->
  Sem r Expression
 checkParens e@(ExpressionAtoms as) = case as of
@ -1024,7 +1005,7 @@ checkParens e@(ExpressionAtoms as) = case as of
  _ -> checkParseExpressionAtoms e

 checkMatchAlt ::
-  Members '[Error ScopeError, State Scope, Reader LocalVars, State ScoperState] r =>
+  Members '[Error ScopeError, State Scope, Reader LocalVars, State ScoperState , InfoTableBuilder ] r =>
  MatchAlt 'Parsed ->
  Sem r (MatchAlt 'Scoped)
 checkMatchAlt MatchAlt {..} = do
@ -1037,7 +1018,7 @@ checkMatchAlt MatchAlt {..} = do
      }

 checkMatch ::
-  Members '[Error ScopeError, State Scope, Reader LocalVars, State ScoperState] r =>
+  Members '[Error ScopeError, State Scope, Reader LocalVars, State ScoperState , InfoTableBuilder] r =>
  Match 'Parsed ->
  Sem r (Match 'Scoped)
 checkMatch Match {..} = do
@ -1050,13 +1031,13 @@ checkMatch Match {..} = do
      }

 checkExpressionAtoms ::
-  Members '[Error ScopeError, State Scope, State ScoperState, Reader LocalVars] r =>
+  Members '[Error ScopeError, State Scope, State ScoperState, Reader LocalVars , InfoTableBuilder] r =>
  ExpressionAtoms 'Parsed ->
  Sem r (ExpressionAtoms 'Scoped)
 checkExpressionAtoms (ExpressionAtoms l) = ExpressionAtoms <$> mapM checkExpressionAtom l

 checkParseExpressionAtoms ::
-  Members '[Error ScopeError, State Scope, State ScoperState, Reader LocalVars] r =>
+  Members '[Error ScopeError, State Scope, State ScoperState, Reader LocalVars, InfoTableBuilder ] r =>
  ExpressionAtoms 'Parsed ->
  Sem r Expression
 checkParseExpressionAtoms = checkExpressionAtoms >=> parseExpressionAtoms
@ -1068,7 +1049,7 @@ checkParsePatternAtom ::
 checkParsePatternAtom = checkPatternAtom >=> parsePatternAtom

 checkStatement ::
-  Members '[Error ScopeError, Reader ScopeParameters, Files, State Scope, State ScoperState, Reader LocalVars, Fixpoint] r =>
+  Members '[Error ScopeError, Reader ScopeParameters, Files, State Scope, State ScoperState, Reader LocalVars, Fixpoint , InfoTableBuilder] r =>
  Statement 'Parsed ->
  Sem r (Statement 'Scoped)
 checkStatement s = case s of
@ -1295,7 +1276,7 @@ makePatternTable atom = [appOp] : operators
    mkSymbolTable = reverse . map (map snd) . groupSortOn fst . mapMaybe unqualifiedSymbolOp
      where
        unqualifiedSymbolOp :: ConstructorRef -> Maybe (Precedence, P.Operator ParsePat Pattern)
-        unqualifiedSymbolOp (ConstructorRef' (S.Name' {..}) _)
+        unqualifiedSymbolOp (ConstructorRef' (S.Name' {..}))
          | Just Fixity {..} <- _nameFixity,
            _nameKind == S.KNameConstructor = Just $
            case fixityArity of
--- a/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper/InfoTableBuilder.hs
+++ b/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
--- a/src/MiniJuvix/Syntax/Concrete/Scoped/VisibilityAnn.hs
+++ b/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)
--- a/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Base.hs
+++ b/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Base.hs
@ -55,9 +55,13 @@ 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_

@ -136,7 +140,8 @@ instance PrettyCode FunctionDef where

 instance PrettyCode Backend where
  ppCode = \case
-    BackendGhc -> return kwGhc
+    BackendGhc  -> return kwGhc
+    BackendAgda -> return kwAgda

 instance PrettyCode ForeignBlock where
  ppCode ForeignBlock {..} = do
--- a/src/MiniJuvix/Termination/Types/SizeRelation.hs
+++ b/src/MiniJuvix/Termination/Types/SizeRelation.hs
@ -1,9 +1,13 @@
 module MiniJuvix.Termination.Types.SizeRelation where

-import Algebra.Graph.Label
+--------------------------------------------------------------------------------
+
+import Data.Semiring
 import MiniJuvix.Prelude
 import Prettyprinter

+--------------------------------------------------------------------------------
+
 data Rel
  = RJust Rel'
  | RNothing
@ -47,12 +51,11 @@ star_ (RJust REq) = RJust REq
 instance Semigroup Rel where
  (<>) = add

-instance Monoid Rel where
-  mempty = RNothing
-
 instance Semiring Rel where
  one = RJust REq
-  (<.>) = mul
+  zero = RNothing
+  plus = add
+  times = mul

 instance Pretty Rel where
  pretty r = case r of
--- a/src/MiniJuvix/Utils/Version.hs
+++ b/src/MiniJuvix/Utils/Version.hs
@ -1,40 +1,78 @@
-module MiniJuvix.Utils.Version (getVersion) where
+module MiniJuvix.Utils.Version
+  ( branch,
+    commit,
+    commitDate,
+    infoVersionRepo,
+    progName,
+    progNameVersion,
+    progNameVersionTag,
+    runDisplayVersion,
+    shortHash,
+    versionDoc,
+    versionTag,
+)
+where

 ------------------------------------------------------------------------------

-import Control.Exception (IOException)
-import qualified Control.Exception as Exception
-import qualified Data.List as List
-import Data.Version (Version (versionTags))
-import MiniJuvix.Prelude
-import System.Exit
-import System.Process (readProcessWithExitCode)
+import Data.Version (showVersion)
+import Development.GitRev (gitBranch, gitCommitDate, gitHash)
+import MiniJuvix.Prelude hiding (Doc)
+import qualified Paths_minijuvix
+import Prettyprinter as PP
+import Prettyprinter.Render.Text (renderIO)
+import System.Environment (getProgName)

 ------------------------------------------------------------------------------

-tryIO :: IO a -> IO (Either IOException a)
-tryIO = Exception.try
+versionDoc :: Doc Text
+versionDoc = PP.pretty (showVersion Paths_minijuvix.version)

-commitInfo :: IO (Maybe String)
-commitInfo = do
-  res <-
-    tryIO $
-      readProcessWithExitCode "git" ["log", "--format=%h", "-n", "1"] ""
-  case res of
-    Right (ExitSuccess, hash, _) -> do
-      (_, _, _) <- readProcessWithExitCode "git" ["diff", "--quiet"] ""
-      return $ Just (List.init hash)
-    _ -> return Nothing
+branch :: Doc Text
+branch = PP.pretty (pack $(gitBranch))

-gitVersion :: Version -> String -> Version
-gitVersion version hash = version {versionTags = [take 7 hash]}
+commit :: Doc Text
+commit = PP.pretty (pack $(gitHash))

-- | If inside a `git` repository, then @'getVersion' x@ will return
-- @x@ plus the hash of the top commit used for
-- compilation. Otherwise, only @x@ will be returned.
-getVersion :: Version -> IO Version
-getVersion version = do
-  commit <- commitInfo
-  case commit of
-    Nothing -> return version
-    Just rev -> return $ gitVersion version rev
+commitDate :: Doc Text
+commitDate = PP.pretty (pack $(gitCommitDate))
+
+shortHash :: Doc Text
+shortHash = PP.pretty (pack (take 7 $(gitHash)))
+
+versionTag :: Doc Text
+versionTag = versionDoc <> "-" <> shortHash
+
+progName :: IO (Doc Text)
+progName = PP.pretty . pack . toUpperFirst <$> getProgName
+
+progNameVersion :: IO (Doc Text)
+progNameVersion = do
+  pName <- progName
+  pure (pName <+> "version" <+> versionDoc)
+
+progNameVersionTag :: IO (Doc Text)
+progNameVersionTag = do
+  progNameV <- progNameVersion
+  pure (progNameV <> "-" <> shortHash)
+
+infoVersionRepo :: IO (Doc Text)
+infoVersionRepo = do
+  pNameTag <- progNameVersionTag
+  pure
+    ( pNameTag <> line
+        <> "Branch"
+        <> colon <+> branch
+        <> line
+        <> "Commit"
+        <> colon <+> commit
+        <> line
+        <> "Date"
+        <> colon <+> commitDate
+        <> line
+    )
+
+runDisplayVersion :: IO ()
+runDisplayVersion = do
+  v <- layoutPretty defaultLayoutOptions <$> infoVersionRepo
+  renderIO stdout v
--- a/stack.yaml
+++ b/stack.yaml
@ -1,4 +1,4 @@
-resolver: nightly-2022-02-27
-extra-deps:
- polysemy-1.7.1.0
- polysemy-plugin-0.4.3.0
+ghc-options:
+  "$locals": -optP-Wno-nonportable-include-path
+resolver: nightly-2022-03-23
+extra-deps: []
--- a/test/Base.hs
+++ b/test/Base.hs
@ -18,17 +18,8 @@ parseModuleIO = fromRightIO id . M.runModuleParserIO
 parseTextModuleIO :: Text -> IO (M.Module 'M.Parsed 'M.ModuleTop)
 parseTextModuleIO = fromRightIO id . return . M.runModuleParser "literal string"

-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)
-
 scopeModuleIO :: M.Module 'M.Parsed 'M.ModuleTop -> IO (M.Module 'M.Scoped 'M.ModuleTop)
-scopeModuleIO = fromRightIO' printErrorAnsi . M.scopeCheck1IO "."
+scopeModuleIO = fmap snd . fromRightIO' printErrorAnsi . M.scopeCheck1IO "."

 data AssertionDescr =
  Single Assertion
--- a/test/Scope/Negative.hs
+++ b/test/Scope/Negative.hs
@ -106,4 +106,19 @@ tests = [
   "WrongModuleName.mjuvix" $ \case
      ErrWrongTopModuleName {} -> Nothing
      _ -> wrongError
+  ,  NegTest "Ambiguous export"
+    "."
+   "AmbiguousExport.mjuvix" $ \case
+      ErrMultipleExport {} -> Nothing
+      _ -> wrongError
+  ,  NegTest "Ambiguous nested modules"
+    "."
+   "AmbiguousModule.mjuvix" $ \case
+      ErrAmbiguousModuleSym {} -> Nothing
+      _ -> wrongError
+  ,  NegTest "Ambiguous nested constructors"
+    "."
+   "AmbiguousConstructor.mjuvix" $ \case
+      ErrAmbiguousSym {} -> Nothing
+      _ -> wrongError
  ]
--- a/test/Scope/Positive.hs
+++ b/test/Scope/Positive.hs
@ -5,6 +5,9 @@ import qualified MiniJuvix.Syntax.Concrete.Scoped.Pretty.Text as M
 import qualified MiniJuvix.Syntax.Concrete.Scoped.Scoper as M
 import MiniJuvix.Syntax.Concrete.Scoped.Utils
 import qualified Data.HashMap.Strict as HashMap
+import Text.Show.Pretty hiding (Html)
+import Data.Algorithm.Diff
+import Data.Algorithm.DiffOutput


 data PosTest = PosTest {
@ -41,14 +44,25 @@ testDescr PosTest {..} = TestDescr {
    parsedPretty' <- parseTextModuleIO parsedPretty

    step "Scope again"
-    s' <- fromRightIO' printErrorAnsi $ return (M.scopeCheck1Pure fs "." p')
+    (_ , s') <- fromRightIO' printErrorAnsi $ return (M.scopeCheck1Pure fs "." p')

    step "Checks"
-    assertBool "check: scope . parse . pretty . scope . parse = scope . parse" (s == s')
-    assertBool "check: parse . pretty . scope . parse = parse" (p == p')
-    assertBool "check: parse . pretty . parse = parse" (p == parsedPretty')
+    assertEqDiff "check: scope . parse . pretty . scope . parse = scope . parse" s s'
+    assertEqDiff "check: parse . pretty . scope . parse = parse" p p'
+    assertEqDiff "check: parse . pretty . parse = parse" p parsedPretty'
  }

+assertEqDiff :: (Eq a, Show a) => String -> a -> a -> Assertion
+assertEqDiff msg a b
+  | a == b = return ()
+  | otherwise = do
+      putStrLn (pack $ ppDiff (getGroupedDiff pa pb))
+      putStrLn "End diff"
+      fail msg
+    where
+    pa = lines $ ppShow a
+    pb = lines $ ppShow b
+
 allTests :: TestTree
 allTests = testGroup "Scope positive tests"
  (map (mkTest . testDescr) tests)
@ -75,4 +89,16 @@ tests = [
     "." "Literals.mjuvix"
  , PosTest "Hello World backends"
     "." "HelloWorld.mjuvix"
+  , PosTest "Axiom with backends"
+     "." "Axiom.mjuvix"
+  , PosTest "Foreign block parsing"
+     "." "Foreign.mjuvix"
+  , PosTest "Multiple modules non-ambiguous symbol - same file"
+     "QualifiedSymbol" "M.mjuvix"
+  , PosTest "Multiple modules non-ambiguous symbol"
+     "QualifiedSymbol2" "N.mjuvix"
+  , PosTest "Multiple modules constructor non-ambiguous symbol"
+     "QualifiedConstructor" "M.mjuvix"
+  , PosTest "open overrides open public"
+     "." "ShadowPublicOpen.mjuvix"
 ]
--- a/tests/negative/AmbiguousConstructor.mjuvix
+++ b/tests/negative/AmbiguousConstructor.mjuvix
@ -0,0 +1,19 @@
+module AmbiguousConstructor;
+  module M;
+    inductive T1 {
+      A : T1;
+    };
+  end;
+
+  module N;
+    inductive T2 {
+      A : T2;
+    };
+  end;
+
+  open M;
+  open N;
+
+  f : T1 -> T2;
+  f A ≔ N.A;
+end;
--- a/tests/negative/AmbiguousExport.mjuvix
+++ b/tests/negative/AmbiguousExport.mjuvix
@ -0,0 +1,16 @@
+module AmbiguousExport;
+
+  module N;
+    module O;
+      inductive T {
+        A : T;
+      };
+    end;
+  end;
+
+  open N public;
+
+  module O;
+    axiom A : Type;
+  end;
+end;
--- a/tests/negative/AmbiguousModule.mjuvix
+++ b/tests/negative/AmbiguousModule.mjuvix
@ -0,0 +1,9 @@
+module AmbiguousModule;
+  module M;
+    module M;
+    end;
+  end;
+
+  open M;
+  open M;
+end;
--- a/tests/negative/AmbiguousSymbol.mjuvix
+++ b/tests/negative/AmbiguousSymbol.mjuvix
@ -1,10 +1,18 @@
 module AmbiguousSymbol;

  axiom A : Type;
+
+  module O;
+    inductive T {
+      A : T;
+    };
+  end;
+  open O;
+
  module M;
    axiom A : Type;
  end;
  open M;

  axiom B : A;
-end;
+end;
--- a/tests/positive/Axiom.mjuvix
+++ b/tests/positive/Axiom.mjuvix
@ -0,0 +1,8 @@
+module Axiom;
+
+axiom Action : Type {
+ ghc ↦ "IO ()";
+ agda ↦ "IO Unit";
+};
+
+end;
--- a/tests/positive/Foreign.mjuvix
+++ b/tests/positive/Foreign.mjuvix
@ -0,0 +1,27 @@
+module Foreign;
+
+foreign ghc {};
+
+foreign ghc { import Foo.Bar };
+
+foreign agda { import Foo.Bar };
+
+foreign ghc { import Foo.Bar
+  import Foo.Baz };
+
+foreign ghc {
+  import Foo.Bar
+  import Foo.Baz };
+
+foreign ghc {
+  import Foo.Bar
+  import Foo.Baz
+};
+
+foreign ghc {
+  import Foo.Bar
+
+     import Foo.Baz
+};
+
+end;
--- a/tests/positive/HelloWorld.mjuvix
+++ b/tests/positive/HelloWorld.mjuvix
@ -15,7 +15,7 @@ import Data.Text.IO

 axiom Action : Type {
 ghc ↦ "IO ()";
- c   ↦ "void";
+ agda   ↦ "void";
 };

 axiom String : Type;
@ -31,4 +31,4 @@ axiom putStr : String -> Action;
 -- main : Action;
 -- main := putStr "hello world";

-end;
+end;
--- a/tests/positive/QualifiedConstructor/M.mjuvix
+++ b/tests/positive/QualifiedConstructor/M.mjuvix
@ -0,0 +1,21 @@
+module M;
+
+  module O;
+    axiom A : Type;
+  end;
+
+  open O;
+
+  module N;
+    module O;
+      inductive T {
+        A : T;
+      };
+    end;
+  end;
+
+  open N.O;
+
+  fun : T → T;
+  fun A ≔ T;
+end;
--- a/tests/positive/QualifiedSymbol/M.mjuvix
+++ b/tests/positive/QualifiedSymbol/M.mjuvix
@ -0,0 +1,14 @@
+module M;
+
+  module N;
+    module O;
+      axiom A : Type;
+    end;
+  end;
+  open N;
+
+  module O;
+  end;
+
+  axiom B : O.A;
+end;
--- a/tests/positive/QualifiedSymbol2/M.mjuvix
+++ b/tests/positive/QualifiedSymbol2/M.mjuvix
@ -0,0 +1,3 @@
+module M;
+
+end;
--- a/tests/positive/QualifiedSymbol2/N.mjuvix
+++ b/tests/positive/QualifiedSymbol2/N.mjuvix
@ -0,0 +1,10 @@
+module N;
+  import M;
+
+  module M;
+    axiom A : Type;
+  end;
+
+  axiom B : M.A;
+
+end;
--- a/tests/positive/ShadowPublicOpen.mjuvix
+++ b/tests/positive/ShadowPublicOpen.mjuvix
@ -0,0 +1,10 @@
+module ShadowPublicOpen;
+  module M;
+    module N;
+      axiom A : Type;
+    end;
+    open N public;
+  end;
+  open M;
+  axiom A : Type;
+end;