add references to the syntax and cleanup code

Makefile

@@ -51,7 +51,13 @@ stan :
 setup:
 	stack build --only-dependencies --jobs $(THREADS)
 
-stack:
+test:
+	stack test --fast --jobs $(THREADS)
+
+install:
+	stack install --fast --jobs $(THREADS)
+
+build:
 	stack build --fast --jobs $(THREADS)
 
 stack-build-watch:
@@ -94,4 +100,4 @@ install-agda2hs:
 .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
+	agda2hs ./src/MiniJuvix/Syntax/Eval.agda -o src -XUnicodeSyntax -XStandaloneDeriving -XDerivingStrategies -XMultiParamTypeClasses

app/Main.hs

@@ -5,7 +5,6 @@ import Control.Monad.Extra
 import qualified MiniJuvix.Syntax.Concrete.Language as M
 import qualified MiniJuvix.Syntax.Concrete.Parser as M
 import qualified MiniJuvix.Syntax.Concrete.Scoped.Pretty.Ansi as M
-import qualified MiniJuvix.Syntax.MiniHaskell.Pretty.Ansi as H
 import qualified MiniJuvix.Syntax.MicroJuvix.Pretty.Ansi as Micro
 import qualified MiniJuvix.Termination as T
 import qualified MiniJuvix.Translation.ScopedToAbstract as A
@@ -239,7 +238,8 @@ go c = do
     MiniHaskell MiniHaskellOptions {..} -> do
       m <- parseModuleIO _mhaskellInputFile
       s <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m
-      a <- fromRightIO' putStrLn (return $ A.translateModule s)
+      -- a <- fromRightIO' putStrLn (return $ A.translateModule s)
+      fromRightIO' putStrLn (return $ A.translateModule s)
       -- let mini = Micro.translateModule a
       -- Micro.printPrettyCodeDefault mini
       -- TODO

package.yaml

@@ -78,6 +78,7 @@ default-extensions:
 - OverloadedStrings
 - PolyKinds
 - QuasiQuotes
+- RankNTypes
 - RecordWildCards
 - ScopedTypeVariables
 - StandaloneDeriving

src/MiniJuvix/Prelude.hs

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

src/MiniJuvix/Prelude/Base.hs

@@ -2,6 +2,7 @@ module MiniJuvix.Prelude.Base
   ( module MiniJuvix.Prelude.Base,
     module Control.Monad.Extra,
     module Data.Char,
+    module Control.Monad.Fix,
     module Data.Typeable,
     module Data.Either.Extra,
     module Data.Function,
@@ -30,6 +31,7 @@ module MiniJuvix.Prelude.Base
     module Polysemy.Reader,
     module Data.Text.IO,
     module Polysemy.State,
+    module Polysemy.Fixpoint,
     module Polysemy.Error,
     module Polysemy.Embed,
     module Text.Show,
@@ -62,8 +64,8 @@ where
 --------------------------------------------------------------------------------
 
 import Control.Applicative
-import Data.Typeable hiding (TyCon)
 import Control.Monad.Extra
+import Control.Monad.Fix
 import Data.Bool
 import Data.ByteString.Lazy (ByteString)
 import Data.Char
@@ -74,27 +76,28 @@ import Data.Eq
 import Data.Foldable hiding (minimum, minimumBy)
 import Data.Function
 import Data.Functor
-import Prettyprinter (Doc, (<+>))
 import Data.HashMap.Strict (HashMap)
 import Data.HashSet (HashSet)
 import Data.Hashable
 import Data.Int
 import Data.List.Extra hiding (head, last)
-import Data.List.NonEmpty.Extra (NonEmpty (..), head, last, nonEmpty, minimum1, minimumOn1, maximum1, maximumOn1, some1)
 import qualified Data.List.NonEmpty as NonEmpty
+import Data.List.NonEmpty.Extra (NonEmpty (..), head, last, maximum1, maximumOn1, minimum1, minimumOn1, nonEmpty, some1)
 import Data.Maybe
-import Data.Singletons.Sigma
 import Data.Monoid
 import Data.Ord
 import Data.Semigroup (Semigroup, (<>))
 import Data.Singletons
+import Data.Singletons.Sigma
 import Data.Singletons.TH (genSingletons)
 import Data.Stream (Stream)
 import Data.String
 import Data.Text (Text, pack, strip, unpack)
 import Data.Text.Encoding
+import Data.Text.IO
 import Data.Traversable
 import Data.Tuple.Extra
+import Data.Typeable hiding (TyCon)
 import Data.Void
 import Data.Word
 import GHC.Enum
@@ -107,15 +110,16 @@ import Lens.Micro.Platform hiding (both)
 import Polysemy
 import Polysemy.Embed
 import Polysemy.Error hiding (fromEither)
+import Polysemy.Fixpoint
 import Polysemy.Reader
 import Polysemy.State
 import Polysemy.View
+import Prettyprinter (Doc, (<+>))
 import System.Directory
 import System.Exit
 import System.FilePath
-import System.IO hiding (putStr, putStrLn, hPutStr, hPutStrLn, writeFile, hGetContents, interact, readFile, getContents, getLine, appendFile, hGetLine, readFile')
+import System.IO hiding (appendFile, getContents, getLine, hGetContents, hGetLine, hPutStr, hPutStrLn, interact, putStr, putStrLn, readFile, readFile', writeFile)
 import Text.Show (Show)
-import Data.Text.IO
 import qualified Text.Show as Show
 
 --------------------------------------------------------------------------------
@@ -209,16 +213,18 @@ impossible = Err.error "impossible"
 --------------------------------------------------------------------------------
 
 infixl 7 <+?>
+
 (<+?>) :: Doc ann -> Maybe (Doc ann) -> Doc ann
 (<+?>) a = maybe a (a <+>)
 
 infixl 7 <?>
+
 (<?>) :: Semigroup m => m -> Maybe m -> m
 (<?>) a = maybe a (a <>)
 
-data Indexed a = Indexed {
-  _indexedIx :: Int,
-  _indexedThing :: a
+data Indexed a = Indexed
+  { _indexedIx :: Int,
+    _indexedThing :: a
   }
   deriving stock (Show, Eq, Ord, Foldable, Traversable)
 

src/MiniJuvix/Prelude/Error.hs

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

src/MiniJuvix/Syntax/Abstract/Language.hs

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

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

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

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

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

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

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

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

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

src/MiniJuvix/Syntax/Concrete/Base.hs

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

src/MiniJuvix/Syntax/Concrete/Language.hs

@@ -1,40 +1,57 @@
 {-# 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.PublicAnn,
+    module MiniJuvix.Syntax.Concrete.ModuleIsTop,
     module MiniJuvix.Syntax.Concrete.Language.Stage,
     module MiniJuvix.Syntax.Fixity,
     module MiniJuvix.Syntax.Usage,
-    module MiniJuvix.Syntax.Universe
+    module MiniJuvix.Syntax.Universe,
   )
 where
 
 --------------------------------------------------------------------------------
 
 import qualified Data.Kind as GHC
-import MiniJuvix.Syntax.Universe
-import MiniJuvix.Syntax.Fixity
-import MiniJuvix.Syntax.Usage
-import MiniJuvix.Syntax.Concrete.Name
-import MiniJuvix.Syntax.Concrete.Loc
-import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
-import MiniJuvix.Syntax.Concrete.PublicAnn
+import MiniJuvix.Prelude hiding (show)
 import MiniJuvix.Syntax.Concrete.Language.Stage
-import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Concrete.Loc
+import MiniJuvix.Syntax.Concrete.ModuleIsTop
+import MiniJuvix.Syntax.Concrete.Name
+import MiniJuvix.Syntax.Concrete.PublicAnn
+import MiniJuvix.Syntax.Concrete.Scoped.Name (unqualifiedSymbol)
+import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
+import MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind
+import MiniJuvix.Syntax.Fixity
+import MiniJuvix.Syntax.Universe
+import MiniJuvix.Syntax.Usage
+import Prelude (show)
 
 --------------------------------------------------------------------------------
 -- Parsing stages
 --------------------------------------------------------------------------------
+type family RefNameType (c :: S.IsConcrete) :: (res :: GHC.Type) | res -> c where
+  RefNameType 'S.Concrete = S.Name
+  RefNameType 'S.NotConcrete = S.Name' ()
 
 type family SymbolType (s :: Stage) :: (res :: GHC.Type) | res -> s where
   SymbolType 'Parsed = Symbol
   SymbolType 'Scoped = S.Symbol
 
-type family NameType (s :: Stage) :: (res :: GHC.Type) | res -> s where
-  NameType 'Parsed = Name
-  NameType 'Scoped = S.Name
+type family ModuleRefType (s :: Stage) :: (res :: GHC.Type) | res -> s where
+  ModuleRefType 'Parsed = Name
+  ModuleRefType 'Scoped = ModuleRef
+
+type family IdentifierType (s :: Stage) :: (res :: GHC.Type) | res -> s where
+  IdentifierType 'Parsed = Name
+  IdentifierType 'Scoped = ScopedIden
+
+type family PatternAtomIdenType (s :: Stage) :: (res :: GHC.Type) | res -> s where
+  PatternAtomIdenType 'Parsed = Name
+  PatternAtomIdenType 'Scoped = PatternScopedIden
 
 type family ExpressionType (s :: Stage) :: (res :: GHC.Type) | res -> s where
   ExpressionType 'Parsed = ExpressionAtoms 'Parsed
@@ -80,7 +97,8 @@ deriving stock instance
     Show (ModulePathType s 'ModuleLocal),
     Show (PatternType s),
     Show (SymbolType s),
-    Show (NameType s),
+    Show (IdentifierType s),
+    Show (ModuleRefType s),
     Show (ExpressionType s)
   ) =>
   Show (Statement s)
@@ -90,7 +108,8 @@ deriving stock instance
     Eq (PatternType s),
     Eq (ModulePathType s 'ModuleLocal),
     Eq (SymbolType s),
-    Eq (NameType s),
+    Eq (IdentifierType s),
+    Eq (ModuleRefType s),
     Eq (ExpressionType s)
   ) =>
   Eq (Statement s)
@@ -100,23 +119,27 @@ deriving stock instance
     Ord (PatternType s),
     Ord (ModulePathType s 'ModuleLocal),
     Ord (SymbolType s),
-    Ord (NameType s),
+    Ord (IdentifierType s),
+    Ord (ModuleRefType s),
     Ord (ExpressionType s)
   ) =>
   Ord (Statement s)
 
-data CompileDef (s :: Stage) = CompileDef {
-  _compileAxiom :: SymbolType s,
-  _compileBackend :: Backend,
-  _compileCode :: Text
+data CompileDef (s :: Stage) = CompileDef
+  { _compileAxiom :: SymbolType s,
+    _compileBackend :: Backend,
+    _compileCode :: Text
   }
+
 deriving stock instance (Eq (SymbolType s)) => Eq (CompileDef s)
+
 deriving stock instance (Ord (SymbolType s)) => Ord (CompileDef s)
+
 deriving stock instance (Show (SymbolType s)) => Show (CompileDef s)
 
-data ForeignBlock = ForeignBlock {
-  _foreignBackend :: Backend,
-  _foreignCode :: Text
+data ForeignBlock = ForeignBlock
+  { _foreignBackend :: Backend,
+    _foreignCode :: Text
   }
   deriving stock (Eq, Ord, Show)
 
@@ -228,37 +251,33 @@ deriving stock instance (Ord (ExpressionType s), Ord (SymbolType s)) => Ord (Ind
 --------------------------------------------------------------------------------
 
 data PatternApp = PatternApp
-  {
-    patAppLeft :: Pattern,
+  { patAppLeft :: Pattern,
     patAppRight :: Pattern
   }
   deriving stock (Show, Eq, Ord)
 
-
 data PatternInfixApp = PatternInfixApp
-  {
-    patInfixLeft :: Pattern,
-    patInfixConstructor :: NameType 'Scoped,
+  { patInfixLeft :: Pattern,
+    patInfixConstructor :: ConstructorRef,
     patInfixRight :: Pattern
   }
   deriving stock (Show, Eq, Ord)
 
 instance HasFixity PatternInfixApp where
-  getFixity (PatternInfixApp  _ op _) = fromMaybe impossible (op ^. S.nameFixity)
+  getFixity (PatternInfixApp _ op _) = fromMaybe impossible (_constructorRefName op ^. S.nameFixity)
 
 data PatternPostfixApp = PatternPostfixApp
-  {
-    patPostfixParameter :: Pattern,
-    patPostfixConstructor :: NameType 'Scoped
+  { patPostfixParameter :: Pattern,
+    patPostfixConstructor :: ConstructorRef
   }
   deriving stock (Show, Eq, Ord)
 
 instance HasFixity PatternPostfixApp where
-  getFixity (PatternPostfixApp  _ op) = fromMaybe impossible (op ^. S.nameFixity)
+  getFixity (PatternPostfixApp _ op) = fromMaybe impossible (_constructorRefName op ^. S.nameFixity)
 
 data Pattern
   = PatternVariable (SymbolType 'Scoped)
-  | PatternConstructor (NameType 'Scoped)
+  | PatternConstructor ConstructorRef
   | PatternApplication PatternApp
   | PatternInfixApplication PatternInfixApp
   | PatternPostfixApplication PatternPostfixApp
@@ -267,7 +286,7 @@ data Pattern
   deriving stock (Show, Eq, Ord)
 
 instance HasAtomicity Pattern where
- atomicity e = case e of
+  atomicity e = case e of
     PatternVariable {} -> Atom
     PatternConstructor {} -> Atom
     PatternApplication {} -> Aggregate appFixity
@@ -280,8 +299,13 @@ instance HasAtomicity Pattern where
 -- Pattern section
 --------------------------------------------------------------------------------
 
+data PatternScopedIden
+  = PatternScopedVar S.Symbol
+  | PatternScopedConstructor ConstructorRef
+  deriving stock (Show, Ord, Eq)
+
 data PatternAtom (s :: Stage)
-  = PatternAtomName (NameType s)
+  = PatternAtomIden (PatternAtomIdenType s)
   | PatternAtomWildcard
   | PatternAtomEmpty
   | PatternAtomParens (PatternAtoms s)
@@ -291,21 +315,24 @@ instance HasAtomicity (PatternAtom 'Parsed) where
 
 deriving stock instance
   ( Show (ExpressionType s),
-    Show (NameType s),
+    Show (IdentifierType s),
+    Show (PatternAtomIdenType s),
     Show (PatternType s)
   ) =>
   Show (PatternAtom s)
 
 deriving stock instance
   ( Eq (ExpressionType s),
-    Eq (NameType s),
+    Eq (IdentifierType s),
+    Eq (PatternAtomIdenType s),
     Eq (PatternType s)
   ) =>
   Eq (PatternAtom s)
 
 deriving stock instance
   ( Ord (ExpressionType s),
-    Ord (NameType s),
+    Ord (IdentifierType s),
+    Ord (PatternAtomIdenType s),
     Ord (PatternType s)
   ) =>
   Ord (PatternAtom s)
@@ -315,21 +342,24 @@ newtype PatternAtoms (s :: Stage)
 
 deriving stock instance
   ( Show (ExpressionType s),
-    Show (NameType s),
+    Show (IdentifierType s),
+    Show (PatternAtomIdenType s),
     Show (PatternType s)
   ) =>
   Show (PatternAtoms s)
 
 deriving stock instance
   ( Eq (ExpressionType s),
-    Eq (NameType s),
+    Eq (IdentifierType s),
+    Eq (PatternAtomIdenType s),
     Eq (PatternType s)
   ) =>
   Eq (PatternAtoms s)
 
 deriving stock instance
   ( Ord (ExpressionType s),
-    Ord (NameType s),
+    Ord (IdentifierType s),
+    Ord (PatternAtomIdenType s),
     Ord (PatternType s)
   ) =>
   Ord (PatternAtoms s)
@@ -349,7 +379,8 @@ data FunctionClause (s :: Stage) = FunctionClause
 
 deriving stock instance
   ( Show (PatternType s),
-    Show (NameType s),
+    Show (IdentifierType s),
+    Show (ModuleRefType s),
     Show (SymbolType s),
     Show (ExpressionType s)
   ) =>
@@ -357,7 +388,8 @@ deriving stock instance
 
 deriving stock instance
   ( Eq (PatternType s),
-    Eq (NameType s),
+    Eq (IdentifierType s),
+    Eq (ModuleRefType s),
     Eq (SymbolType s),
     Eq (ExpressionType s)
   ) =>
@@ -365,7 +397,8 @@ deriving stock instance
 
 deriving stock instance
   ( Ord (PatternType s),
-    Ord (NameType s),
+    Ord (IdentifierType s),
+    Ord (ModuleRefType s),
     Ord (SymbolType s),
     Ord (ExpressionType s)
   ) =>
@@ -375,22 +408,6 @@ deriving stock instance
 -- Module declaration
 --------------------------------------------------------------------------------
 
-data ModuleIsTop = ModuleTop | ModuleLocal
-
--- The following Singleton related definitions could be scrapped if we depended
--- on the singletons-th library.
-data SModuleIsTop (t :: ModuleIsTop) where
-  SModuleTop :: SModuleIsTop 'ModuleTop
-  SModuleLocal :: SModuleIsTop 'ModuleLocal
-
-type instance Sing = SModuleIsTop
-
-instance SingI 'ModuleTop where
-  sing = SModuleTop
-
-instance SingI 'ModuleLocal where
-  sing = SModuleLocal
-
 type LocalModuleName s = SymbolType s
 
 data Module (s :: Stage) (t :: ModuleIsTop) = Module
@@ -404,7 +421,8 @@ deriving stock instance
     Show (ModulePathType s 'ModuleLocal),
     Show (ImportType s),
     Show (PatternType s),
-    Show (NameType s),
+    Show (IdentifierType s),
+    Show (ModuleRefType s),
     Show (SymbolType s),
     Show (ExpressionType s)
   ) =>
@@ -415,7 +433,8 @@ deriving stock instance
     Eq (ModulePathType s 'ModuleLocal),
     Eq (ImportType s),
     Eq (PatternType s),
-    Eq (NameType s),
+    Eq (IdentifierType s),
+    Eq (ModuleRefType s),
     Eq (SymbolType s),
     Eq (ExpressionType s)
   ) =>
@@ -426,7 +445,8 @@ deriving stock instance
     Ord (ModulePathType s 'ModuleLocal),
     Ord (ImportType s),
     Ord (PatternType s),
-    Ord (NameType s),
+    Ord (IdentifierType s),
+    Ord (ModuleRefType s),
     Ord (SymbolType s),
     Ord (ExpressionType s)
   ) =>
@@ -437,31 +457,92 @@ data UsingHiding
   | Hiding (NonEmpty Symbol)
   deriving stock (Show, Eq, Ord)
 
+type ModuleRef = ModuleRef' 'S.Concrete
+
+newtype ModuleRef' (c :: S.IsConcrete) = ModuleRef'
+  { _unModuleRef' :: Σ ModuleIsTop (TyCon1 (ModuleRef'' c))
+  }
+
+-- | TODO can this be derived?
+instance SingI c => Show (ModuleRef' c) where
+  show (ModuleRef' (isTop :&: r)) = case isTop of
+    SModuleLocal -> case sing :: S.SIsConcrete c of
+      S.SConcrete -> show r
+      S.SNotConcrete -> show r
+    SModuleTop -> case sing :: S.SIsConcrete c of
+      S.SConcrete -> show r
+      S.SNotConcrete -> show r
+
+getNameRefId :: forall c. SingI c => RefNameType c -> S.NameId
+getNameRefId = case sing :: S.SIsConcrete c of
+  S.SConcrete -> S._nameId
+  S.SNotConcrete -> S._nameId
+
+getModuleExportInfo :: ModuleRef' c -> ExportInfo
+getModuleExportInfo = projSigma2 _moduleExportInfo . _unModuleRef'
+
+getModuleRefNameType :: ModuleRef' c -> RefNameType c
+getModuleRefNameType = projSigma2 _moduleRefName . _unModuleRef'
+
+instance SingI c => Eq (ModuleRef' c) where
+  (==) = (==) `on` (getNameRefId . getModuleRefNameType)
+
+instance SingI c => Ord (ModuleRef' c) where
+  compare = compare `on` (getNameRefId . getModuleRefNameType)
+
+-- TODO find a better name
+data ModuleRef'' (c :: S.IsConcrete) (t :: ModuleIsTop) = ModuleRef''
+  { _moduleRefName :: RefNameType c,
+    _moduleExportInfo :: ExportInfo,
+    _moduleRefModule :: Module 'Scoped t
+  }
+
+instance Show (RefNameType s) => Show (ModuleRef'' s t) where
+  show = show . _moduleRefName
+
+data SymbolEntry
+  = EntryAxiom (AxiomRef' 'S.NotConcrete)
+  | EntryInductive (InductiveRef' 'S.NotConcrete)
+  | EntryFunction (FunctionRef' 'S.NotConcrete)
+  | EntryConstructor (ConstructorRef' 'S.NotConcrete)
+  | -- | TODO does this ever contain top modules?
+    EntryModule (ModuleRef' 'S.NotConcrete)
+  deriving stock (Show)
+
+-- | Symbols that a module exports
+newtype ExportInfo = ExportInfo
+  { _exportSymbols :: HashMap Symbol SymbolEntry
+  }
+  deriving stock (Show)
+
 data OpenModule (s :: Stage) = OpenModule
-  { openModuleName :: NameType s,
+  { openModuleName :: ModuleRefType s,
     openParameters :: [ExpressionType s],
     openUsingHiding :: Maybe UsingHiding,
     openPublic :: PublicAnn
   }
+
 deriving stock instance
-  (
-    Eq (NameType s),
+  ( Eq (IdentifierType s),
     Eq (SymbolType s),
+    Eq (ModuleRefType s),
     Eq (PatternType s),
     Eq (ExpressionType s)
   ) =>
   Eq (OpenModule s)
+
 deriving stock instance
-  (
-    Ord (NameType s),
+  ( Ord (IdentifierType s),
     Ord (SymbolType s),
     Ord (PatternType s),
+    Ord (ModuleRefType s),
     Ord (ExpressionType s)
   ) =>
   Ord (OpenModule s)
+
 deriving stock instance
-  (
-    Show (NameType s),
+  ( Show (IdentifierType s),
+    Show (ModuleRefType s),
     Show (ExpressionType s)
   ) =>
   Show (OpenModule s)
@@ -470,41 +551,105 @@ deriving stock instance
 -- Expression
 --------------------------------------------------------------------------------
 
-data AxiomRef = AxiomRef {
-  _axiomRefName :: NameType 'Scoped,
-  _axiomRefBackends :: HashMap Backend Text
-  }
-  deriving stock (Show, Eq, Ord)
+type AxiomRef = AxiomRef' 'S.Concrete
 
-data InductiveRef = InductiveRef {
-  _inductiveRefName :: NameType 'Scoped,
-  _inductiveRefDef :: InductiveDef 'Scoped
+data AxiomRef' (n :: S.IsConcrete) = AxiomRef'
+  { _axiomRefName :: RefNameType n,
+    _axiomRefType :: Expression,
+    _axiomRefBackends :: HashMap Backend Text
   }
-  deriving stock (Show, Eq, Ord)
 
-data FunctionRef = FunctionRef {
-  _functionRefName :: NameType 'Scoped,
-  _functionRefSig :: Expression
+instance Eq (RefNameType s) => Eq (AxiomRef' s) where
+  (==) = (==) `on` _axiomRefName
+
+instance Ord (RefNameType s) => Ord (AxiomRef' s) where
+  compare = compare `on` _axiomRefName
+
+instance Show (RefNameType s) => Show (AxiomRef' s) where
+  show = show . _axiomRefName
+
+type InductiveRef = InductiveRef' 'S.Concrete
+
+data InductiveRef' (n :: S.IsConcrete) = InductiveRef'
+  { _inductiveRefName :: RefNameType n,
+    _inductiveRefDef :: InductiveDef 'Scoped
   }
-  deriving stock (Show, Eq, Ord)
 
-data ConstructorRef = ConstructorRef {
-  _constructorRefName :: NameType 'Scoped,
-  _constructorSig :: Expression
+instance Eq (RefNameType s) => Eq (InductiveRef' s) where
+  (==) = (==) `on` _inductiveRefName
+
+instance Ord (RefNameType s) => Ord (InductiveRef' s) where
+  compare = compare `on` _inductiveRefName
+
+instance Show (RefNameType s) => Show (InductiveRef' s) where
+  show = show . _inductiveRefName
+
+type FunctionRef = FunctionRef' 'S.Concrete
+
+data FunctionRef' (n :: S.IsConcrete) = FunctionRef'
+  { _functionRefName :: RefNameType n,
+    _functionRefSig :: Expression
   }
-  deriving stock (Show, Eq, Ord)
 
-data ScopedIden =
-  ScopedAxiom AxiomRef
-  | ScopedInductive InductiveRef
-  | ScopedVar (NameType 'Scoped)
-  | ScopedFunction FunctionRef
-  | ScopedConstructor ConstructorRef
-  deriving stock (Show, Eq, Ord)
+instance Eq (RefNameType s) => Eq (FunctionRef' s) where
+  (==) = (==) `on` _functionRefName
+
+instance Ord (RefNameType s) => Ord (FunctionRef' s) where
+  compare = compare `on` _functionRefName
+
+instance Show (RefNameType s) => Show (FunctionRef' s) where
+  show = show . _functionRefName
+
+type ConstructorRef = ConstructorRef' 'S.Concrete
+
+data ConstructorRef' (n :: S.IsConcrete) = ConstructorRef'
+  { _constructorRefName :: RefNameType n,
+    _constructorSig :: Expression
+  }
+
+instance Eq (RefNameType s) => Eq (ConstructorRef' s) where
+  (==) = (==) `on` _constructorRefName
+
+instance Ord (RefNameType s) => Ord (ConstructorRef' s) where
+  compare = compare `on` _constructorRefName
+
+instance Show (RefNameType s) => Show (ConstructorRef' s) where
+  show = show . _constructorRefName
+
+type ScopedIden = ScopedIden' 'S.Concrete
+
+data ScopedIden' (n :: S.IsConcrete)
+  = ScopedAxiom (AxiomRef' n)
+  | ScopedInductive (InductiveRef' n)
+  | ScopedVar S.Symbol
+  | ScopedFunction (FunctionRef' n)
+  | ScopedConstructor (ConstructorRef' n)
+
+deriving stock instance
+  (Eq (RefNameType s)) => Eq (ScopedIden' s)
+
+deriving stock instance
+  (Ord (RefNameType s)) => Ord (ScopedIden' s)
+
+deriving stock instance
+  (Show (RefNameType s)) => Show (ScopedIden' s)
+
+identifierName :: forall n. SingI n => ScopedIden' n -> RefNameType n
+identifierName = \case
+  ScopedAxiom a -> _axiomRefName a
+  ScopedInductive i -> _inductiveRefName i
+  ScopedVar v ->
+    ( case sing :: S.SIsConcrete n of
+        S.SConcrete -> id
+        S.SNotConcrete -> set S.nameConcrete ()
+    )
+      (unqualifiedSymbol v)
+  ScopedFunction f -> _functionRefName f
+  ScopedConstructor c -> _constructorRefName c
 
 data Expression
   = ExpressionIdentifier ScopedIden
-  | ExpressionParensIdentifier (NameType 'Scoped)
+  | ExpressionParensIdentifier ScopedIden
   | ExpressionApplication Application
   | ExpressionInfixApplication InfixApplication
   | ExpressionPostfixApplication PostfixApplication
@@ -522,7 +667,7 @@ instance HasAtomicity Literal where
     LitString {} -> Atom
 
 instance HasAtomicity Expression where
- atomicity e = case e of
+  atomicity e = case e of
     ExpressionIdentifier {} -> Atom
     ExpressionParensIdentifier {} -> Atom
     ExpressionApplication {} -> Aggregate appFixity
@@ -539,14 +684,14 @@ instance HasAtomicity Expression where
 -- Expression atom
 --------------------------------------------------------------------------------
 
-data Literal =
-  LitString Text
+data Literal
+  = LitString Text
   | LitInteger Integer
   deriving stock (Show, Eq, Ord)
 
 -- | Expressions without application
 data ExpressionAtom (s :: Stage)
-  = AtomIdentifier (NameType s)
+  = AtomIdentifier (IdentifierType s)
   | AtomLambda (Lambda s)
   | AtomLetBlock (LetBlock s)
   | AtomUniverse Universe
@@ -558,7 +703,8 @@ data ExpressionAtom (s :: Stage)
 
 deriving stock instance
   ( Show (ExpressionType s),
-    Show (NameType s),
+    Show (IdentifierType s),
+    Show (ModuleRefType s),
     Show (SymbolType s),
     Show (PatternType s)
   ) =>
@@ -566,7 +712,8 @@ deriving stock instance
 
 deriving stock instance
   ( Eq (ExpressionType s),
-    Eq (NameType s),
+    Eq (IdentifierType s),
+    Eq (ModuleRefType s),
     Eq (SymbolType s),
     Eq (PatternType s)
   ) =>
@@ -574,7 +721,8 @@ deriving stock instance
 
 deriving stock instance
   ( Ord (ExpressionType s),
-    Ord (NameType s),
+    Ord (IdentifierType s),
+    Ord (ModuleRefType s),
     Ord (SymbolType s),
     Ord (PatternType s)
   ) =>
@@ -586,14 +734,15 @@ newtype ExpressionAtoms (s :: Stage)
 
 instance HasAtomicity (ExpressionAtoms 'Parsed) where
   atomicity (ExpressionAtoms l) = case l of
-    (_  :| []) -> Atom
-    (_  :| _)
+    (_ :| []) -> Atom
+    (_ :| _)
       | AtomFunArrow `elem` l -> Aggregate funFixity
       | otherwise -> Aggregate appFixity
 
 deriving stock instance
   ( Show (ExpressionType s),
-    Show (NameType s),
+    Show (IdentifierType s),
+    Show (ModuleRefType s),
     Show (SymbolType s),
     Show (PatternType s)
   ) =>
@@ -601,7 +750,8 @@ deriving stock instance
 
 deriving stock instance
   ( Eq (ExpressionType s),
-    Eq (NameType s),
+    Eq (IdentifierType s),
+    Eq (ModuleRefType s),
     Eq (SymbolType s),
     Eq (PatternType s)
   ) =>
@@ -609,7 +759,8 @@ deriving stock instance
 
 deriving stock instance
   ( Ord (ExpressionType s),
-    Ord (NameType s),
+    Ord (IdentifierType s),
+    Ord (ModuleRefType s),
     Ord (SymbolType s),
     Ord (PatternType s)
   ) =>
@@ -702,7 +853,8 @@ newtype WhereBlock (s :: Stage) = WhereBlock
 
 deriving stock instance
   ( Show (PatternType s),
-    Show (NameType s),
+    Show (IdentifierType s),
+    Show (ModuleRefType s),
     Show (SymbolType s),
     Show (ExpressionType s)
   ) =>
@@ -710,7 +862,8 @@ deriving stock instance
 
 deriving stock instance
   ( Eq (PatternType s),
-    Eq (NameType s),
+    Eq (IdentifierType s),
+    Eq (ModuleRefType s),
     Eq (SymbolType s),
     Eq (ExpressionType s)
   ) =>
@@ -718,7 +871,8 @@ deriving stock instance
 
 deriving stock instance
   ( Ord (PatternType s),
-    Ord (NameType s),
+    Ord (IdentifierType s),
+    Ord (ModuleRefType s),
     Ord (SymbolType s),
     Ord (ExpressionType s)
   ) =>
@@ -731,7 +885,8 @@ data WhereClause (s :: Stage)
 
 deriving stock instance
   ( Show (PatternType s),
-    Show (NameType s),
+    Show (IdentifierType s),
+    Show (ModuleRefType s),
     Show (SymbolType s),
     Show (ExpressionType s)
   ) =>
@@ -739,7 +894,8 @@ deriving stock instance
 
 deriving stock instance
   ( Eq (PatternType s),
-    Eq (NameType s),
+    Eq (IdentifierType s),
+    Eq (ModuleRefType s),
     Eq (SymbolType s),
     Eq (ExpressionType s)
   ) =>
@@ -747,7 +903,8 @@ deriving stock instance
 
 deriving stock instance
   ( Ord (PatternType s),
-    Ord (NameType s),
+    Ord (IdentifierType s),
+    Ord (ModuleRefType s),
     Ord (SymbolType s),
     Ord (ExpressionType s)
   ) =>
@@ -816,24 +973,22 @@ data Application = Application
 
 data InfixApplication = InfixApplication
   { infixAppLeft :: ExpressionType 'Scoped,
-    infixAppOperator :: NameType 'Scoped,
+    infixAppOperator :: IdentifierType 'Scoped,
     infixAppRight :: ExpressionType 'Scoped
   }
   deriving stock (Show, Eq, Ord)
 
 instance HasFixity InfixApplication where
-  getFixity (InfixApplication  _ op _) = fromMaybe impossible (op ^. S.nameFixity)
-
+  getFixity (InfixApplication _ op _) = fromMaybe impossible (identifierName op ^. S.nameFixity)
 
 data PostfixApplication = PostfixApplication
-  {
-    postfixAppParameter :: ExpressionType 'Scoped,
-    postfixAppOperator :: NameType 'Scoped
+  { postfixAppParameter :: ExpressionType 'Scoped,
+    postfixAppOperator :: IdentifierType 'Scoped
   }
   deriving stock (Show, Eq, Ord)
 
 instance HasFixity PostfixApplication where
-  getFixity (PostfixApplication _ op) = fromMaybe impossible (op ^. S.nameFixity)
+  getFixity (PostfixApplication _ op) = fromMaybe impossible (identifierName op ^. S.nameFixity)
 
 --------------------------------------------------------------------------------
 -- Let block expression
@@ -846,7 +1001,8 @@ data LetBlock (s :: Stage) = LetBlock
 
 deriving stock instance
   ( Show (PatternType s),
-    Show (NameType s),
+    Show (IdentifierType s),
+    Show (ModuleRefType s),
     Show (SymbolType s),
     Show (ExpressionType s)
   ) =>
@@ -854,7 +1010,8 @@ deriving stock instance
 
 deriving stock instance
   ( Eq (PatternType s),
-    Eq (NameType s),
+    Eq (IdentifierType s),
+    Eq (ModuleRefType s),
     Eq (SymbolType s),
     Eq (ExpressionType s)
   ) =>
@@ -862,7 +1019,8 @@ deriving stock instance
 
 deriving stock instance
   ( Ord (PatternType s),
-    Ord (NameType s),
+    Ord (IdentifierType s),
+    Ord (ModuleRefType s),
     Ord (SymbolType s),
     Ord (ExpressionType s)
   ) =>
@@ -874,7 +1032,8 @@ data LetClause (s :: Stage)
 
 deriving stock instance
   ( Show (PatternType s),
-    Show (NameType s),
+    Show (IdentifierType s),
+    Show (ModuleRefType s),
     Show (SymbolType s),
     Show (ExpressionType s)
   ) =>
@@ -882,7 +1041,8 @@ deriving stock instance
 
 deriving stock instance
   ( Eq (PatternType s),
-    Eq (NameType s),
+    Eq (IdentifierType s),
+    Eq (ModuleRefType s),
     Eq (SymbolType s),
     Eq (ExpressionType s)
   ) =>
@@ -890,7 +1050,8 @@ deriving stock instance
 
 deriving stock instance
   ( Ord (PatternType s),
-    Ord (NameType s),
+    Ord (IdentifierType s),
+    Ord (ModuleRefType s),
     Ord (SymbolType s),
     Ord (ExpressionType s)
   ) =>
@@ -950,3 +1111,45 @@ makeLenses ''FunctionClause
 makeLenses ''InductiveParameter
 makeLenses ''CompileDef
 makeLenses ''ForeignBlock
+makeLenses ''AxiomRef'
+makeLenses ''InductiveRef'
+makeLenses ''ModuleRef'
+makeLenses ''ModuleRef''
+makeLenses ''FunctionRef'
+makeLenses ''ConstructorRef'
+
+idenOverName :: (forall s. S.Name' s -> S.Name' s) -> ScopedIden -> ScopedIden
+idenOverName f = \case
+  ScopedAxiom a -> ScopedAxiom (over axiomRefName f a)
+  ScopedInductive i -> ScopedInductive (over inductiveRefName f i)
+  ScopedVar v -> ScopedVar (f v)
+  ScopedFunction fun -> ScopedFunction (over functionRefName f fun)
+  ScopedConstructor c -> ScopedConstructor (over constructorRefName f c)
+
+entryPrism :: (S.Name' () -> S.Name' ()) -> SymbolEntry -> (S.Name' (), SymbolEntry)
+entryPrism f = \case
+  EntryAxiom a -> (a ^. axiomRefName, EntryAxiom (over axiomRefName f a))
+  EntryInductive i -> (i ^. inductiveRefName, EntryInductive (over inductiveRefName f i))
+  EntryFunction fun -> (fun ^. functionRefName, EntryFunction (over functionRefName f fun))
+  EntryConstructor c -> (c ^. constructorRefName, EntryConstructor (over constructorRefName f c))
+  EntryModule m -> (getModuleRefNameType m, EntryModule (overModuleRef'' (over moduleRefName f) m))
+
+entryOverName :: (S.Name' () -> S.Name' ()) -> SymbolEntry -> SymbolEntry
+entryOverName f = snd . entryPrism f
+
+entryName :: SymbolEntry -> S.Name' ()
+entryName = fst . entryPrism id
+
+overModuleRef'' :: forall s s'. (forall t. ModuleRef'' s t -> ModuleRef'' s' t) -> ModuleRef' s -> ModuleRef' s'
+overModuleRef'' f = over unModuleRef' (\(t :&: m'') -> t :&: f m'')
+
+symbolEntryToSName :: SymbolEntry -> S.Name' ()
+symbolEntryToSName = \case
+  EntryAxiom a -> a ^. axiomRefName
+  EntryInductive i -> i ^. inductiveRefName
+  EntryFunction f -> f ^. functionRefName
+  EntryConstructor c -> c ^. constructorRefName
+  EntryModule m -> getModuleRefNameType m
+
+instance HasNameKind SymbolEntry where
+  getNameKind = getNameKind . entryName

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

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

src/MiniJuvix/Syntax/Concrete/Lexer.hs

@@ -2,14 +2,14 @@ module MiniJuvix.Syntax.Concrete.Lexer where
 
 --------------------------------------------------------------------------------
 
-import GHC.Unicode
-import MiniJuvix.Syntax.Concrete.Base hiding (space, Pos)
-import qualified MiniJuvix.Syntax.Concrete.Base as P
-import MiniJuvix.Prelude
-import qualified Text.Megaparsec.Char.Lexer as L
-import MiniJuvix.Syntax.Concrete.Loc
-import qualified MiniJuvix.Internal.Strings as Str
 import qualified Data.Text as Text
+import GHC.Unicode
+import qualified MiniJuvix.Internal.Strings as Str
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Concrete.Base hiding (Pos, space)
+import qualified MiniJuvix.Syntax.Concrete.Base as P
+import MiniJuvix.Syntax.Concrete.Loc
+import qualified Text.Megaparsec.Char.Lexer as L
 
 --------------------------------------------------------------------------------
 
@@ -45,7 +45,7 @@ integer = do
   nat <- lexeme L.decimal
   case minus of
     Nothing -> return nat
-    _ -> return (- nat)
+    _ -> return (-nat)
 
 -- | TODO allow escaping { inside the string using \{
 bracedString :: MonadParsec e Text m => m Text
@@ -58,11 +58,11 @@ string = pack <$> (char '"' >> manyTill L.charLiteral (char '"'))
 mkLoc :: SourcePos -> Loc
 mkLoc SourcePos {..} = Loc {..}
   where
-  _locFile = sourceName
-  _locFileLoc = FileLoc {..}
-    where
-    _locLine = fromPos sourceLine
-    _locCol = fromPos sourceColumn
+    _locFile = sourceName
+    _locFileLoc = FileLoc {..}
+      where
+        _locLine = fromPos sourceLine
+        _locCol = fromPos sourceColumn
 
 curLoc :: MonadParsec e Text m => m Loc
 curLoc = mkLoc <$> getSourcePos
@@ -99,9 +99,9 @@ bareIdentifier = interval $ do
           c `elem` extraAllowedChars
         ]
       where
-      extraAllowedChars :: [Char]
-      extraAllowedChars = "_'-*,&"
-      cat = generalCategory c
+        extraAllowedChars :: [Char]
+        extraAllowedChars = "_'-*,&"
+        cat = generalCategory c
 
 dot :: forall e m. MonadParsec e Text m => m Char
 dot = P.char '.'

src/MiniJuvix/Syntax/Concrete/Loc.hs

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

src/MiniJuvix/Syntax/Concrete/ModuleIsTop.hs

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

src/MiniJuvix/Syntax/Concrete/Name.hs

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

src/MiniJuvix/Syntax/Concrete/Parser.hs

@@ -6,11 +6,11 @@ import qualified Data.List.NonEmpty.Extra as NonEmpty
 import Data.Singletons
 import qualified Data.Text as Text
 import qualified Data.Text.IO as Text
+import MiniJuvix.Prelude
 import MiniJuvix.Syntax.Concrete.Base (MonadParsec)
 import qualified MiniJuvix.Syntax.Concrete.Base as P
 import MiniJuvix.Syntax.Concrete.Language
 import MiniJuvix.Syntax.Concrete.Lexer hiding (symbol)
-import MiniJuvix.Prelude
 
 --------------------------------------------------------------------------------
 -- Running the parser
@@ -147,7 +147,7 @@ import_ = do
 expressionAtom :: MonadParsec e Text m => m (ExpressionAtom 'Parsed)
 expressionAtom =
   do
-     AtomLiteral <$> P.try literal
+    AtomLiteral <$> P.try literal
     <|> AtomIdentifier <$> name
     <|> (AtomUniverse <$> universe)
     <|> (AtomLambda <$> lambda)
@@ -166,8 +166,8 @@ expressionAtoms = ExpressionAtoms <$> P.some expressionAtom
 
 literal :: MonadParsec e Text m => m Literal
 literal =
-      LitInteger <$> integer
-  <|> LitString <$> string
+  LitInteger <$> integer
+    <|> LitString <$> string
 
 --------------------------------------------------------------------------------
 -- Match expression
@@ -319,7 +319,7 @@ lambdaClause = do
 lambda :: MonadParsec e Text m => m (Lambda 'Parsed)
 lambda = do
   kwLambda
-  lambdaClauses ← braces (P.sepEndBy lambdaClause kwSemicolon)
+  lambdaClauses <- braces (P.sepEndBy lambdaClause kwSemicolon)
   return Lambda {..}
 
 -------------------------------------------------------------------------------
@@ -355,7 +355,7 @@ constructorDef = do
 
 patternAtom :: forall e m. MonadParsec e Text m => m (PatternAtom 'Parsed)
 patternAtom =
-  PatternAtomName <$> name
+  PatternAtomIden <$> name
     <|> PatternAtomWildcard <$ kwWildcard
     <|> (PatternAtomParens <$> parens patternAtoms)
 
@@ -421,10 +421,10 @@ openModule = do
   openPublic <- maybe NoPublic (const Public) <$> optional kwPublic
   return OpenModule {..}
   where
-  usingOrHiding :: m UsingHiding
-  usingOrHiding =
-    (kwUsing >> (Using <$> symbolList))
-     <|> (kwHiding >> (Hiding <$> symbolList))
+    usingOrHiding :: m UsingHiding
+    usingOrHiding =
+      (kwUsing >> (Using <$> symbolList))
+        <|> (kwHiding >> (Hiding <$> symbolList))
 
 --------------------------------------------------------------------------------
 -- Debugging statements

src/MiniJuvix/Syntax/Concrete/PublicAnn.hs

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

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

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

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

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

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

@@ -1,9 +1,9 @@
 module MiniJuvix.Syntax.Concrete.Scoped.Error.Pretty.Ansi where
 
-import Prettyprinter
 import MiniJuvix.Prelude
-import Prettyprinter.Render.Terminal
 import MiniJuvix.Syntax.Concrete.Scoped.Error.Pretty.Base
+import Prettyprinter
+import Prettyprinter.Render.Terminal
 
 renderAnsi :: SimpleDocStream Eann -> Text
 renderAnsi = renderStrict . reAnnotateS stylize

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@@ -1,20 +1,20 @@
-module MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base (
-  module MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base,
-  module MiniJuvix.Syntax.Concrete.Scoped.Pretty.Ann
-                                                    ) where
+module MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base
+  ( module MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base,
+    module MiniJuvix.Syntax.Concrete.Scoped.Pretty.Ann,
+  )
+where
 
-import MiniJuvix.Syntax.Concrete.Language
-import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
-import MiniJuvix.Prelude
 import qualified Data.List.NonEmpty.Extra as NonEmpty
-import Prettyprinter hiding (braces, parens)
-import MiniJuvix.Syntax.Concrete.Scoped.Pretty.Ann
-import MiniJuvix.Syntax.Concrete.Scoped.Name (AbsModulePath)
 import MiniJuvix.Internal.Strings as Str
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Concrete.Language
+import MiniJuvix.Syntax.Concrete.Scoped.Name (AbsModulePath)
+import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
+import MiniJuvix.Syntax.Concrete.Scoped.Pretty.Ann
+import Prettyprinter hiding (braces, parens)
 
 data Options = Options
-  {
-    _optShowNameId :: Bool,
+  { _optShowNameId :: Bool,
     _optInlineImports :: Bool,
     _optIndent :: Int
   }
@@ -22,8 +22,7 @@ data Options = Options
 defaultOptions :: Options
 defaultOptions =
   Options
-    {
-      _optShowNameId = False,
+    { _optShowNameId = False,
       _optInlineImports = False,
       _optIndent = 2
     }
@@ -176,15 +175,18 @@ parens = enclose kwParenL kwParenR
 doubleQuotes :: Doc Ann -> Doc Ann
 doubleQuotes = enclose kwDQuote kwDQuote
 
-ppModulePathType :: forall t s r. (SingI t, SingI s, Members '[Reader Options] r) =>
-  ModulePathType s t -> Sem r (Doc Ann)
+ppModulePathType ::
+  forall t s r.
+  (SingI t, SingI s, Members '[Reader Options] r) =>
+  ModulePathType s t ->
+  Sem r (Doc Ann)
 ppModulePathType x = case sing :: SStage s of
   SParsed -> case sing :: SModuleIsTop t of
     SModuleLocal -> ppCode x
     SModuleTop -> ppCode x
   SScoped -> case sing :: SModuleIsTop t of
     SModuleLocal -> annSDef x <$> ppCode x
-    SModuleTop ->  annSDef x <$> ppCode x
+    SModuleTop -> annSDef x <$> ppCode x
 
 ppUnkindedSymbol :: Members '[Reader Options] r => Symbol -> Sem r (Doc Ann)
 ppUnkindedSymbol = fmap (annotate AnnUnkindedSym) . ppSymbol
@@ -197,63 +199,66 @@ ppSymbol = case sing :: SStage s of
 groupStatements :: forall s. SingI s => [Statement s] -> [[Statement s]]
 groupStatements = reverse . map reverse . uncurry cons . foldl' aux ([], [])
   where
-  aux :: ([Statement s], [[Statement s]]) -> Statement s
-      -> ([Statement s], [[Statement s]])
-  aux ([], acc) s = ([s], acc)
-  aux (gr@(a : _), acc) b
-    | g a b = (b : gr, acc)
-    | otherwise = ([b], gr : acc)
-  -- | Decides if statements a and b should be next to each other without a
-  -- blank line
-  g :: Statement s -> Statement s -> Bool
-  g a b = case (a, b) of
-    (StatementCompile _, StatementCompile _) -> True
-    (StatementCompile _, _) -> False
-    (StatementForeign _, _) -> False
-    (StatementOperator _, StatementOperator _) -> True
-    (StatementOperator o, s) -> definesSymbol (opSymbol o) s
-    (StatementImport _, StatementImport _) -> True
-    (StatementImport i, StatementOpenModule o) -> case sing :: SStage s of
-      SParsed -> True
-      SScoped ->
-        S._nameId (_modulePath (importModule i)) ==
-        S._nameId (openModuleName o)
-    (StatementImport _, _) -> False
-    (StatementOpenModule {}, StatementOpenModule {}) -> True
-    (StatementOpenModule {}, _) -> False
-    (StatementInductive {}, _) -> False
-    (StatementModule {}, _) -> False
-    (StatementAxiom {}, StatementAxiom {}) -> True
-    (StatementAxiom {}, _) -> False
-    (StatementEval {}, StatementEval {}) -> True
-    (StatementEval {}, _) -> False
-    (StatementPrint {}, StatementPrint {}) -> True
-    (StatementPrint {}, _) -> False
-    (StatementTypeSignature sig, StatementFunctionClause fun) ->
-      case sing :: SStage s of
-        SParsed -> _sigName sig == _clauseOwnerFunction fun
-        SScoped -> _sigName sig == _clauseOwnerFunction fun
-    (StatementTypeSignature {}, _) -> False
-    (StatementFunctionClause fun1, StatementFunctionClause fun2) ->
-      case sing :: SStage s of
-        SParsed -> _clauseOwnerFunction fun1 == _clauseOwnerFunction fun2
-        SScoped -> _clauseOwnerFunction fun1 == _clauseOwnerFunction fun2
-    (StatementFunctionClause {}, _) -> False
-  definesSymbol :: Symbol -> Statement s -> Bool
-  definesSymbol n s = case s of
-    StatementTypeSignature sig ->
-      let sym = case sing :: SStage s of
-            SParsed -> _sigName sig
-            SScoped -> S._nameConcrete $ _sigName sig
-      in n == sym
-    StatementInductive d -> n `elem` syms d
-    _ -> False
-    where
-    syms :: InductiveDef s -> [Symbol]
-    syms InductiveDef {..} = case sing :: SStage s of
-      SParsed -> _inductiveName : map constructorName _inductiveConstructors
-      SScoped -> S._nameConcrete _inductiveName :
-          map (S._nameConcrete . constructorName) _inductiveConstructors
+    aux ::
+      ([Statement s], [[Statement s]]) ->
+      Statement s ->
+      ([Statement s], [[Statement s]])
+    aux ([], acc) s = ([s], acc)
+    aux (gr@(a : _), acc) b
+      | g a b = (b : gr, acc)
+      | otherwise = ([b], gr : acc)
+    -- Decides if statements a and b should be next to each other without a
+    -- blank line
+    g :: Statement s -> Statement s -> Bool
+    g a b = case (a, b) of
+      (StatementCompile _, StatementCompile _) -> True
+      (StatementCompile _, _) -> False
+      (StatementForeign _, _) -> False
+      (StatementOperator _, StatementOperator _) -> True
+      (StatementOperator o, s) -> definesSymbol (opSymbol o) s
+      (StatementImport _, StatementImport _) -> True
+      (StatementImport i, StatementOpenModule o) -> case sing :: SStage s of
+        SParsed -> True
+        SScoped ->
+          S._nameId (_modulePath (importModule i))
+            == S._nameId (projSigma2 _moduleRefName (openModuleName o ^. unModuleRef'))
+      (StatementImport _, _) -> False
+      (StatementOpenModule {}, StatementOpenModule {}) -> True
+      (StatementOpenModule {}, _) -> False
+      (StatementInductive {}, _) -> False
+      (StatementModule {}, _) -> False
+      (StatementAxiom {}, StatementAxiom {}) -> True
+      (StatementAxiom {}, _) -> False
+      (StatementEval {}, StatementEval {}) -> True
+      (StatementEval {}, _) -> False
+      (StatementPrint {}, StatementPrint {}) -> True
+      (StatementPrint {}, _) -> False
+      (StatementTypeSignature sig, StatementFunctionClause fun) ->
+        case sing :: SStage s of
+          SParsed -> _sigName sig == _clauseOwnerFunction fun
+          SScoped -> _sigName sig == _clauseOwnerFunction fun
+      (StatementTypeSignature {}, _) -> False
+      (StatementFunctionClause fun1, StatementFunctionClause fun2) ->
+        case sing :: SStage s of
+          SParsed -> _clauseOwnerFunction fun1 == _clauseOwnerFunction fun2
+          SScoped -> _clauseOwnerFunction fun1 == _clauseOwnerFunction fun2
+      (StatementFunctionClause {}, _) -> False
+    definesSymbol :: Symbol -> Statement s -> Bool
+    definesSymbol n s = case s of
+      StatementTypeSignature sig ->
+        let sym = case sing :: SStage s of
+              SParsed -> _sigName sig
+              SScoped -> S._nameConcrete $ _sigName sig
+         in n == sym
+      StatementInductive d -> n `elem` syms d
+      _ -> False
+      where
+        syms :: InductiveDef s -> [Symbol]
+        syms InductiveDef {..} = case sing :: SStage s of
+          SParsed -> _inductiveName : map constructorName _inductiveConstructors
+          SScoped ->
+            S._nameConcrete _inductiveName :
+            map (S._nameConcrete . constructorName) _inductiveConstructors
 
 instance SingI s => PrettyCode [Statement s] where
   ppCode ss = joinGroups <$> mapM (fmap mkGroup . mapM (fmap endSemicolon . ppCode)) (groupStatements ss)
@@ -283,8 +288,11 @@ instance PrettyCode Backend where
 instance PrettyCode ForeignBlock where
   ppCode ForeignBlock {..} = do
     _foreignBackend' <- ppCode _foreignBackend
-    return $ kwForeign <+> _foreignBackend' <+> lbrace <> line
-        <> pretty _foreignCode <> line <> rbrace
+    return $
+      kwForeign <+> _foreignBackend' <+> lbrace <> line
+        <> pretty _foreignCode
+        <> line
+        <> rbrace
 
 instance SingI s => PrettyCode (CompileDef s) where
   ppCode CompileDef {..} = do
@@ -296,8 +304,11 @@ instance SingI s => PrettyCode (CompileDef s) where
 ppStringLit :: Text -> Doc Ann
 ppStringLit = annotate AnnLiteralString . doubleQuotes . pretty
 
-ppTopModulePath :: forall s r. (SingI s, Members '[Reader Options] r) =>
-  ModulePathType s 'ModuleTop -> Sem r (Doc Ann)
+ppTopModulePath ::
+  forall s r.
+  (SingI s, Members '[Reader Options] r) =>
+  ModulePathType s 'ModuleTop ->
+  Sem r (Doc Ann)
 ppTopModulePath = case sing :: SStage s of
   SParsed -> ppCode
   SScoped -> ppCode
@@ -322,27 +333,29 @@ instance PrettyCode AbsModulePath where
     absTopModulePath' <- ppCode absTopModulePath
     return $ dotted (absTopModulePath' : absLocalPath')
 
-ppInductiveParameters :: (SingI s, Members '[Reader Options] r)
-    => [InductiveParameter s] -> Sem r (Maybe (Doc Ann))
+ppInductiveParameters ::
+  (SingI s, Members '[Reader Options] r) =>
+  [InductiveParameter s] ->
+  Sem r (Maybe (Doc Ann))
 ppInductiveParameters ps
   | null ps = return Nothing
   | otherwise = Just <$> ppCode ps
 
 instance (SingI s, SingI t) => PrettyCode (Module s t) where
   ppCode Module {..} = do
-      moduleBody' <- ppCode _moduleBody >>= indented
-      modulePath' <- ppModulePathType _modulePath
-      moduleParameters' <- ppInductiveParameters _moduleParameters
-      return $
-        kwModule <+> modulePath' <+?> moduleParameters' <> kwSemicolon <> line
-          <> moduleBody'
-          <> line
-          <> kwEnd
-          <?> lastSemicolon
-      where
-        lastSemicolon = case sing :: SModuleIsTop t of
-          SModuleLocal -> Nothing
-          SModuleTop -> Just kwSemicolon
+    moduleBody' <- ppCode _moduleBody >>= indented
+    modulePath' <- ppModulePathType _modulePath
+    moduleParameters' <- ppInductiveParameters _moduleParameters
+    return $
+      kwModule <+> modulePath' <+?> moduleParameters' <> kwSemicolon <> line
+        <> moduleBody'
+        <> line
+        <> kwEnd
+        <?> lastSemicolon
+    where
+      lastSemicolon = case sing :: SModuleIsTop t of
+        SModuleLocal -> Nothing
+        SModuleTop -> Just kwSemicolon
 
 instance PrettyCode Precedence where
   ppCode p = return $ case p of
@@ -358,11 +371,11 @@ instance PrettyCode Fixity where
 
 instance PrettyCode OperatorArity where
   ppCode fixityArity = return $ case fixityArity of
-   Unary {} -> kwPostfix
-   Binary p -> case p of
-     AssocRight -> kwInfixr
-     AssocLeft -> kwInfixl
-     AssocNone -> kwInfix
+    Unary {} -> kwPostfix
+    Binary p -> case p of
+      AssocRight -> kwInfixr
+      AssocLeft -> kwInfixl
+      AssocNone -> kwInfix
 
 instance PrettyCode OperatorSyntaxDef where
   ppCode OperatorSyntaxDef {..} = do
@@ -400,7 +413,7 @@ instance PrettyCode QualifiedName where
     let symbols = pathParts _qualifiedPath NonEmpty.|> _qualifiedSymbol
     dotted <$> mapM ppSymbol symbols
 
-ppName :: forall s r. (SingI s, Members '[Reader Options] r) => NameType s -> Sem r (Doc Ann)
+ppName :: forall s r. (SingI s, Members '[Reader Options] r) => IdentifierType s -> Sem r (Doc Ann)
 ppName = case sing :: SStage s of
   SParsed -> ppCode
   SScoped -> ppCode
@@ -434,39 +447,45 @@ instance PrettyCode n => PrettyCode (S.Name' n) where
     showNameId <- asks _optShowNameId
     uid <- if showNameId then ("@" <>) <$> ppCode _nameId else return mempty
     return $ annSRef (nameConcrete' <> uid)
-      where
+    where
       annSRef :: Doc Ann -> Doc Ann
       annSRef = annotate (AnnRef (S.absTopModulePath _nameDefinedIn) _nameId)
 
+instance PrettyCode ModuleRef where
+  ppCode = ppCode . projSigma2 _moduleRefName . (^. unModuleRef')
+
 instance SingI s => PrettyCode (OpenModule s) where
   ppCode :: forall r. Members '[Reader Options] r => OpenModule s -> Sem r (Doc Ann)
   ppCode OpenModule {..} = do
-    openModuleName' <- ppName openModuleName
+    openModuleName' <- case sing :: SStage s of
+      SParsed -> ppCode openModuleName
+      SScoped -> ppCode openModuleName
     openUsingHiding' <- sequence $ ppUsingHiding <$> openUsingHiding
     openParameters' <- ppOpenParams
     let openPublic' = ppPublic
     return $ keyword "open" <+> openModuleName' <+?> openParameters' <+?> openUsingHiding' <+?> openPublic'
     where
-    ppAtom' = case sing :: SStage s of
-      SParsed -> ppCodeAtom
-      SScoped -> ppCodeAtom
-    ppOpenParams :: Sem r (Maybe (Doc Ann))
-    ppOpenParams = case openParameters of
-      [] -> return Nothing
-      _ -> Just . hsep <$> mapM ppAtom' openParameters
-    ppUsingHiding :: UsingHiding -> Sem r (Doc Ann)
-    ppUsingHiding uh = do
-      bracedList <- encloseSep kwBraceL kwBraceR kwSemicolon . toList
-        <$> mapM ppUnkindedSymbol syms
-      return $ kw <+> bracedList
-      where
-        (kw, syms) = case uh of
-          Using s -> (kwUsing, s)
-          Hiding s -> (kwHiding, s)
-    ppPublic :: Maybe (Doc Ann)
-    ppPublic = case openPublic of
-      Public -> Just kwPublic
-      NoPublic -> Nothing
+      ppAtom' = case sing :: SStage s of
+        SParsed -> ppCodeAtom
+        SScoped -> ppCodeAtom
+      ppOpenParams :: Sem r (Maybe (Doc Ann))
+      ppOpenParams = case openParameters of
+        [] -> return Nothing
+        _ -> Just . hsep <$> mapM ppAtom' openParameters
+      ppUsingHiding :: UsingHiding -> Sem r (Doc Ann)
+      ppUsingHiding uh = do
+        bracedList <-
+          encloseSep kwBraceL kwBraceR kwSemicolon . toList
+            <$> mapM ppUnkindedSymbol syms
+        return $ kw <+> bracedList
+        where
+          (kw, syms) = case uh of
+            Using s -> (kwUsing, s)
+            Hiding s -> (kwHiding, s)
+      ppPublic :: Maybe (Doc Ann)
+      ppPublic = case openPublic of
+        Public -> Just kwPublic
+        NoPublic -> Nothing
 
 instance SingI s => PrettyCode (TypeSignature s) where
   ppCode TypeSignature {..} = do
@@ -587,22 +606,30 @@ instance SingI s => PrettyCode (Import s) where
     inlineImport' <- inlineImport
     return $ kwImport <+> modulePath' <+?> inlineImport'
     where
-    ppModulePath = case sing :: SStage s of
-      SParsed -> ppCode m
-      SScoped -> ppTopModulePath (m ^. modulePath)
-    jumpLines :: Doc Ann -> Doc Ann
-    jumpLines x = line <> x <> line
-    inlineImport :: Sem r (Maybe (Doc Ann))
-    inlineImport = do
-      b <- asks _optInlineImports
-      if b then case sing :: SStage s of
-        SParsed -> return Nothing
-        SScoped -> ppCode m >>= fmap (Just . braces . jumpLines) . indented
-        else return Nothing
+      ppModulePath = case sing :: SStage s of
+        SParsed -> ppCode m
+        SScoped -> ppTopModulePath (m ^. modulePath)
+      jumpLines :: Doc Ann -> Doc Ann
+      jumpLines x = line <> x <> line
+      inlineImport :: Sem r (Maybe (Doc Ann))
+      inlineImport = do
+        b <- asks _optInlineImports
+        if b
+          then case sing :: SStage s of
+            SParsed -> return Nothing
+            SScoped -> ppCode m >>= fmap (Just . braces . jumpLines) . indented
+          else return Nothing
+
+instance PrettyCode PatternScopedIden where
+  ppCode = \case
+    PatternScopedVar v -> ppCode v
+    PatternScopedConstructor c -> ppCode c
 
 instance SingI s => PrettyCode (PatternAtom s) where
   ppCode a = case a of
-    PatternAtomName n -> ppName n
+    PatternAtomIden n -> case sing :: SStage s of
+      SParsed -> ppCode n
+      SScoped -> ppCode n
     PatternAtomWildcard -> return kwWildcard
     PatternAtomEmpty -> return $ parens mempty
     PatternAtomParens p -> parens <$> ppCode p
@@ -610,12 +637,12 @@ instance SingI s => PrettyCode (PatternAtom s) where
 instance SingI s => PrettyCode (PatternAtoms s) where
   ppCode (PatternAtoms ps) = hsep . toList <$> mapM ppCode ps
 
-ppPattern :: forall s r. (SingI s,  Members '[Reader Options] r) => PatternType s -> Sem r (Doc Ann)
+ppPattern :: forall s r. (SingI s, Members '[Reader Options] r) => PatternType s -> Sem r (Doc Ann)
 ppPattern = case sing :: SStage s of
   SParsed -> ppCode
   SScoped -> ppCode
 
-ppPatternAtom :: forall s r. (SingI s,  Members '[Reader Options] r) => PatternType s -> Sem r (Doc Ann)
+ppPatternAtom :: forall s r. (SingI s, Members '[Reader Options] r) => PatternType s -> Sem r (Doc Ann)
 ppPatternAtom = case sing :: SStage s of
   SParsed -> ppCodeAtom
   SScoped -> ppCodeAtom
@@ -644,6 +671,26 @@ instance PrettyCode Literal where
     LitInteger n -> return $ annotate AnnLiteralInteger (pretty n)
     LitString s -> return $ ppStringLit s
 
+instance PrettyCode AxiomRef where
+  ppCode a = ppCode (a ^. axiomRefName)
+
+instance PrettyCode InductiveRef where
+  ppCode a = ppCode (a ^. inductiveRefName)
+
+instance PrettyCode FunctionRef where
+  ppCode a = ppCode (a ^. functionRefName)
+
+instance PrettyCode ConstructorRef where
+  ppCode a = ppCode (a ^. constructorRefName)
+
+instance PrettyCode ScopedIden where
+  ppCode = \case
+    ScopedAxiom a -> ppCode a
+    ScopedInductive i -> ppCode i
+    ScopedVar n -> ppCode n
+    ScopedFunction f -> ppCode f
+    ScopedConstructor c -> ppCode c
+
 instance PrettyCode Expression where
   ppCode e = case e of
     ExpressionIdentifier n -> ppCode n
@@ -672,40 +719,52 @@ instance PrettyCode Pattern where
     PatternInfixApplication i -> ppPatternInfixApp i
     PatternPostfixApplication i -> ppPatternPostfixApp i
     where
-    ppPatternInfixApp :: PatternInfixApp -> Sem r (Doc Ann)
-    ppPatternInfixApp p@PatternInfixApp {..} = do
-      patInfixConstructor' <- ppCode patInfixConstructor
-      patInfixLeft' <- ppLeftExpression (getFixity p) patInfixLeft
-      patInfixRight' <- ppRightExpression (getFixity p) patInfixRight
-      return $ patInfixLeft' <+> patInfixConstructor' <+> patInfixRight'
+      ppPatternInfixApp :: PatternInfixApp -> Sem r (Doc Ann)
+      ppPatternInfixApp p@PatternInfixApp {..} = do
+        patInfixConstructor' <- ppCode patInfixConstructor
+        patInfixLeft' <- ppLeftExpression (getFixity p) patInfixLeft
+        patInfixRight' <- ppRightExpression (getFixity p) patInfixRight
+        return $ patInfixLeft' <+> patInfixConstructor' <+> patInfixRight'
 
-    ppPatternPostfixApp :: PatternPostfixApp -> Sem r (Doc Ann)
-    ppPatternPostfixApp p@PatternPostfixApp {..} = do
-      patPostfixConstructor' <- ppCode patPostfixConstructor
-      patPostfixParameter' <- ppLeftExpression (getFixity p) patPostfixParameter
-      return $ patPostfixParameter' <+> patPostfixConstructor'
+      ppPatternPostfixApp :: PatternPostfixApp -> Sem r (Doc Ann)
+      ppPatternPostfixApp p@PatternPostfixApp {..} = do
+        patPostfixConstructor' <- ppCode patPostfixConstructor
+        patPostfixParameter' <- ppLeftExpression (getFixity p) patPostfixParameter
+        return $ patPostfixParameter' <+> patPostfixConstructor'
 
 parensCond :: Bool -> Doc Ann -> Doc Ann
 parensCond t d = if t then parens d else d
 
-ppPostExpression ::(PrettyCode a, HasAtomicity a, Member (Reader Options) r)  =>
-  Fixity -> a -> Sem r (Doc Ann)
+ppPostExpression ::
+  (PrettyCode a, HasAtomicity a, Member (Reader Options) r) =>
+  Fixity ->
+  a ->
+  Sem r (Doc Ann)
 ppPostExpression = ppLRExpression isPostfixAssoc
 
-ppRightExpression :: (PrettyCode a, HasAtomicity a, Member (Reader Options) r) =>
-  Fixity -> a -> Sem r (Doc Ann)
+ppRightExpression ::
+  (PrettyCode a, HasAtomicity a, Member (Reader Options) r) =>
+  Fixity ->
+  a ->
+  Sem r (Doc Ann)
 ppRightExpression = ppLRExpression isRightAssoc
 
-ppLeftExpression :: (PrettyCode a, HasAtomicity a, Member (Reader Options) r) =>
-  Fixity -> a -> Sem r (Doc Ann)
+ppLeftExpression ::
+  (PrettyCode a, HasAtomicity a, Member (Reader Options) r) =>
+  Fixity ->
+  a ->
+  Sem r (Doc Ann)
 ppLeftExpression = ppLRExpression isLeftAssoc
 
-ppLRExpression
-  :: (HasAtomicity a, PrettyCode a, Member (Reader Options) r) =>
-     (Fixity -> Bool) -> Fixity -> a -> Sem r (Doc Ann)
+ppLRExpression ::
+  (HasAtomicity a, PrettyCode a, Member (Reader Options) r) =>
+  (Fixity -> Bool) ->
+  Fixity ->
+  a ->
+  Sem r (Doc Ann)
 ppLRExpression associates fixlr e =
   parensCond (atomParens associates (atomicity e) fixlr)
-      <$> ppCode e
+    <$> ppCode e
 
 ppCodeAtom :: (HasAtomicity c, PrettyCode c, Members '[Reader Options] r) => c -> Sem r (Doc Ann)
 ppCodeAtom c = do

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

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

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

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

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

@@ -22,45 +22,25 @@ newtype SymbolInfo = SymbolInfo
   }
   deriving newtype (Show, Semigroup, Monoid)
 
-type SymbolEntry = S.Name' ()
-
--- data SymbolEntry' = SymbolEntry' {
---   _entryNameInfo :: NameInfo
-
---   }
-
--- | Symbols that a module exports
-newtype ExportInfo = ExportInfo {
-   _exportSymbols :: HashMap Symbol SymbolEntry
-  }
-
--- | A module entry for either a local or a top module.
-type ModuleEntry = Σ ModuleIsTop (TyCon1 ModuleEntry')
-
-mkModuleEntry :: SingI t => ModuleEntry' t -> ModuleEntry
-mkModuleEntry = (sing :&:)
-
-data ModuleEntry' (t :: ModuleIsTop) = ModuleEntry' {
-  _moduleEntryExport :: ExportInfo,
-  _moduleEntryScoped :: Module 'Scoped t
-  }
+mkModuleRef' :: SingI t => ModuleRef'' 'S.NotConcrete t -> ModuleRef' 'S.NotConcrete
+mkModuleRef' m = ModuleRef' (sing :&: m)
 
 data Scope = Scope
   { _scopePath :: S.AbsModulePath,
     _scopeFixities :: HashMap Symbol OperatorSyntaxDef,
     _scopeSymbols :: HashMap Symbol SymbolInfo,
-    _scopeTopModules :: HashMap TopModulePath S.ModuleNameId,
+    _scopeTopModules :: HashMap TopModulePath (ModuleRef'' 'S.NotConcrete 'ModuleTop),
     _scopeBindGroup :: HashMap Symbol LocalVariable
   }
- deriving stock (Show)
+  deriving stock (Show)
+
 makeLenses ''ExportInfo
 makeLenses ''SymbolInfo
 makeLenses ''LocalVars
 makeLenses ''Scope
-makeLenses ''ModuleEntry'
 
 newtype ModulesCache = ModulesCache
-  { _cachedModules :: HashMap TopModulePath (ModuleEntry' 'ModuleTop)
+  { _cachedModules :: HashMap TopModulePath (ModuleRef'' 'S.NotConcrete 'ModuleTop)
   }
 
 makeLenses ''ModulesCache
@@ -73,20 +53,23 @@ data ScopeParameters = ScopeParameters
     -- | Used for import cycle detection.
     _scopeTopParents :: [Import 'Parsed]
   }
+
 makeLenses ''ScopeParameters
 
 data ScoperState = ScoperState
   { _scoperModulesCache :: ModulesCache,
     _scoperFreeNames :: Stream S.NameId,
-    _scoperModules :: HashMap S.ModuleNameId ModuleEntry
+    _scoperModules :: HashMap S.ModuleNameId (ModuleRef' 'S.NotConcrete)
   }
+
 makeLenses ''ScoperState
 
 emptyScope :: S.AbsModulePath -> Scope
-emptyScope absPath = Scope
-        { _scopePath = absPath,
-          _scopeFixities = mempty,
-          _scopeSymbols = mempty,
-          _scopeTopModules = mempty,
-          _scopeBindGroup = mempty
-        }
+emptyScope absPath =
+  Scope
+    { _scopePath = absPath,
+      _scopeFixities = mempty,
+      _scopeSymbols = mempty,
+      _scopeTopModules = mempty,
+      _scopeBindGroup = mempty
+    }

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

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

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

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

src/MiniJuvix/Syntax/Core.hs

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

src/MiniJuvix/Syntax/Eval.hs

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

src/MiniJuvix/Syntax/Fixity.hs

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

src/MiniJuvix/Syntax/MicroJuvix/Language.hs

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

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

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

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

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

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

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

src/MiniJuvix/Syntax/MiniHaskell/Language.hs

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

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

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

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

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

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

@@ -1,31 +1,31 @@
 -- TODO handle capital letters and characters not supported by Haskell.
 module MiniJuvix.Syntax.MiniHaskell.Pretty.Base where
 
-
-import MiniJuvix.Prelude
-import Prettyprinter
-import MiniJuvix.Syntax.Fixity
-import MiniJuvix.Syntax.MiniHaskell.Pretty.Ann
-import MiniJuvix.Syntax.MiniHaskell.Language
 import qualified MiniJuvix.Internal.Strings as Str
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Fixity
+import MiniJuvix.Syntax.MiniHaskell.Language
+import MiniJuvix.Syntax.MiniHaskell.Pretty.Ann
+import Prettyprinter
 
 newtype Options = Options
-  {
-    _optIndent :: Int
+  { _optIndent :: Int
   }
 
 defaultOptions :: Options
-defaultOptions = Options {
-  _optIndent = 2
-  }
+defaultOptions =
+  Options
+    { _optIndent = 2
+    }
 
 class PrettyCode c where
   ppCode :: Member (Reader Options) r => c -> Sem r (Doc Ann)
 
 instance PrettyCode Name where
   ppCode n =
-    return $ annotate (AnnKind (n ^. nameKind))
-           $ pretty (n ^. nameText)
+    return $
+      annotate (AnnKind (n ^. nameKind)) $
+        pretty (n ^. nameText)
 
 instance PrettyCode Application where
   ppCode a = do
@@ -111,13 +111,14 @@ instance PrettyCode FunctionDef where
     funDefName' <- ppCode (f ^. funDefName)
     funDefTypeSig' <- ppCode (f ^. funDefTypeSig)
     clauses' <- mapM (ppClause funDefName') (f ^. funDefClauses)
-    return $ funDefName' <+> kwColonColon <+> funDefTypeSig' <> line
-      <> vsep (toList clauses')
-     where
-     ppClause fun c = do
-       clausePatterns' <- mapM ppCodeAtom (c ^. clausePatterns)
-       clauseBody' <- ppCode (c ^. clauseBody)
-       return $ fun <+> hsep clausePatterns' <+> kwEquals <+> clauseBody'
+    return $
+      funDefName' <+> kwColonColon <+> funDefTypeSig' <> line
+        <> vsep (toList clauses')
+    where
+      ppClause fun c = do
+        clausePatterns' <- mapM ppCodeAtom (c ^. clausePatterns)
+        clauseBody' <- ppCode (c ^. clauseBody)
+        return $ fun <+> hsep clausePatterns' <+> kwEquals <+> clauseBody'
 
 instance PrettyCode Statement where
   ppCode = \case
@@ -129,36 +130,52 @@ instance PrettyCode ModuleBody where
     statements' <- mapM ppCode (m ^. moduleStatements)
     return $ vsep2 statements'
     where
-    vsep2 = concatWith (\a b -> a <> line <> line <> b)
+      vsep2 = concatWith (\a b -> a <> line <> line <> b)
 
 instance PrettyCode Module where
   ppCode m = do
     name' <- ppCode (m ^. moduleName)
     body' <- ppCode (m ^. moduleBody)
-    return $ kwModule <+> name' <+> kwWhere
-      <> line <> line <> body' <> line
+    return $
+      kwModule <+> name' <+> kwWhere
+        <> line
+        <> line
+        <> body'
+        <> line
 
 parensCond :: Bool -> Doc Ann -> Doc Ann
 parensCond t d = if t then parens d else d
 
-ppPostExpression ::(PrettyCode a, HasAtomicity a, Member (Reader Options) r)  =>
-  Fixity -> a -> Sem r (Doc Ann)
+ppPostExpression ::
+  (PrettyCode a, HasAtomicity a, Member (Reader Options) r) =>
+  Fixity ->
+  a ->
+  Sem r (Doc Ann)
 ppPostExpression = ppLRExpression isPostfixAssoc
 
-ppRightExpression :: (PrettyCode a, HasAtomicity a, Member (Reader Options) r) =>
-  Fixity -> a -> Sem r (Doc Ann)
+ppRightExpression ::
+  (PrettyCode a, HasAtomicity a, Member (Reader Options) r) =>
+  Fixity ->
+  a ->
+  Sem r (Doc Ann)
 ppRightExpression = ppLRExpression isRightAssoc
 
-ppLeftExpression :: (PrettyCode a, HasAtomicity a, Member (Reader Options) r) =>
-  Fixity -> a -> Sem r (Doc Ann)
+ppLeftExpression ::
+  (PrettyCode a, HasAtomicity a, Member (Reader Options) r) =>
+  Fixity ->
+  a ->
+  Sem r (Doc Ann)
 ppLeftExpression = ppLRExpression isLeftAssoc
 
-ppLRExpression
-  :: (HasAtomicity a, PrettyCode a, Member (Reader Options) r) =>
-     (Fixity -> Bool) -> Fixity -> a -> Sem r (Doc Ann)
+ppLRExpression ::
+  (HasAtomicity a, PrettyCode a, Member (Reader Options) r) =>
+  (Fixity -> Bool) ->
+  Fixity ->
+  a ->
+  Sem r (Doc Ann)
 ppLRExpression associates fixlr e =
   parensCond (atomParens associates (atomicity e) fixlr)
-      <$> ppCode e
+    <$> ppCode e
 
 ppCodeAtom :: (HasAtomicity c, PrettyCode c, Members '[Reader Options] r) => c -> Sem r (Doc Ann)
 ppCodeAtom c = do

src/MiniJuvix/Termination.hs

@@ -1,9 +1,10 @@
-module MiniJuvix.Termination (
-  module MiniJuvix.Termination.Types,
-  module MiniJuvix.Termination.CallMap,
-  module MiniJuvix.Termination.CallGraph
-  ) where
+module MiniJuvix.Termination
+  ( module MiniJuvix.Termination.Types,
+    module MiniJuvix.Termination.CallMap,
+    module MiniJuvix.Termination.CallGraph,
+  )
+where
 
-import MiniJuvix.Termination.Types
-import MiniJuvix.Termination.CallMap
 import MiniJuvix.Termination.CallGraph
+import MiniJuvix.Termination.CallMap
+import MiniJuvix.Termination.Types

src/MiniJuvix/Termination/CallGraph.hs

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

src/MiniJuvix/Termination/CallGraphOld.hs

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

src/MiniJuvix/Termination/CallMap.hs

@@ -1,74 +1,79 @@
-module MiniJuvix.Termination.CallMap (
-  module MiniJuvix.Termination.Types,
-  module MiniJuvix.Termination.CallMap
-                                       ) where
+module MiniJuvix.Termination.CallMap
+  ( module MiniJuvix.Termination.Types,
+    module MiniJuvix.Termination.CallMap,
+  )
+where
 
+import qualified Data.HashMap.Strict as HashMap
 import MiniJuvix.Prelude
 import MiniJuvix.Syntax.Abstract.Language.Extra
 import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
-import qualified Data.HashMap.Strict as HashMap
 import MiniJuvix.Termination.Types
 
-
 -- | i = SizeInfo [v] ⇔ v is smaller than argument i of the caller function.
 -- Indexes are 0 based
-data SizeInfo = SizeInfo {
-  _sizeSmaller :: HashMap VarName Int,
-  _sizeEqual :: [Pattern]
-       }
+data SizeInfo = SizeInfo
+  { _sizeSmaller :: HashMap VarName Int,
+    _sizeEqual :: [Pattern]
+  }
 
-viewCall :: forall r. Members '[Reader SizeInfo] r
-   => Expression -> Sem r (Maybe FunCall)
+viewCall ::
+  forall r.
+  Members '[Reader SizeInfo] r =>
+  Expression ->
+  Sem r (Maybe FunCall)
 viewCall e = case e of
   ExpressionApplication (Application f x) -> do
     c <- viewCall f
     x' <- callArg
-    return $ over callArgs (`snoc`x') <$> c
+    return $ over callArgs (`snoc` x') <$> c
     where
-    callArg :: Sem r (CallRow, Expression)
-    callArg =  do
-      lt <- lessThan
-      eq <- equalTo
-      return (CallRow (_callRow lt `mplus` _callRow eq), x)
-      where
-      lessThan :: Sem r CallRow
-      lessThan = case x of
-        ExpressionIden (IdenVar v) -> do
-          s <- asks (HashMap.lookup v . _sizeSmaller)
-          return $ case s of
-            Nothing -> CallRow Nothing
-            Just s' -> CallRow (Just (s', RLe) )
-        _ -> return (CallRow Nothing)
-      equalTo :: Sem r CallRow
-      equalTo = do
-        case viewExpressionAsPattern x of
-          Just x' -> do
-            s <- asks (elemIndex x' . _sizeEqual)
-            return $ case s of
-              Nothing -> CallRow Nothing
-              Just s' -> CallRow (Just (s', REq) )
-          _ -> return (CallRow Nothing)
-  ExpressionIden (IdenDefined x) ->
-     return (Just (singletonCall x))
+      callArg :: Sem r (CallRow, Expression)
+      callArg = do
+        lt <- lessThan
+        eq <- equalTo
+        return (CallRow (_callRow lt `mplus` _callRow eq), x)
+        where
+          lessThan :: Sem r CallRow
+          lessThan = case x of
+            ExpressionIden (IdenVar v) -> do
+              s <- asks (HashMap.lookup v . _sizeSmaller)
+              return $ case s of
+                Nothing -> CallRow Nothing
+                Just s' -> CallRow (Just (s', RLe))
+            _ -> return (CallRow Nothing)
+          equalTo :: Sem r CallRow
+          equalTo = do
+            case viewExpressionAsPattern x of
+              Just x' -> do
+                s <- asks (elemIndex x' . _sizeEqual)
+                return $ case s of
+                  Nothing -> CallRow Nothing
+                  Just s' -> CallRow (Just (s', REq))
+              _ -> return (CallRow Nothing)
+  ExpressionIden (IdenFunction x) ->
+    return (Just (singletonCall x))
   _ -> return Nothing
   where
-  singletonCall :: Name -> FunCall
-  singletonCall n = FunCall (S.nameUnqualify n) []
+    singletonCall :: Name -> FunCall
+    singletonCall n = FunCall (S.nameUnqualify n) []
 
 addCall :: FunctionName -> FunCall -> CallMap -> CallMap
 addCall fun c = over callMap (HashMap.alter (Just . insertCall c) fun)
   where
-  insertCall :: FunCall -> Maybe (HashMap FunctionName [FunCall]) -> HashMap FunctionName [FunCall]
-  insertCall f m = case m of
-    Nothing -> singl f
-    Just m' -> addFunCall f m'
-  singl :: FunCall -> HashMap FunctionName [FunCall]
-  singl f = HashMap.singleton (f ^. callName) [f]
-  addFunCall :: FunCall -> HashMap FunctionName [FunCall] -> HashMap FunctionName [FunCall]
-  addFunCall fc = HashMap.insertWith (flip (<>)) (fc ^. callName) [fc]
+    insertCall :: FunCall -> Maybe (HashMap FunctionName [FunCall]) -> HashMap FunctionName [FunCall]
+    insertCall f m = case m of
+      Nothing -> singl f
+      Just m' -> addFunCall f m'
+    singl :: FunCall -> HashMap FunctionName [FunCall]
+    singl f = HashMap.singleton (f ^. callName) [f]
+    addFunCall :: FunCall -> HashMap FunctionName [FunCall] -> HashMap FunctionName [FunCall]
+    addFunCall fc = HashMap.insertWith (flip (<>)) (fc ^. callName) [fc]
 
-registerCall :: Members '[State CallMap, Reader FunctionName, Reader SizeInfo] r
-   => FunCall -> Sem r ()
+registerCall ::
+  Members '[State CallMap, Reader FunctionName, Reader SizeInfo] r =>
+  FunCall ->
+  Sem r ()
 registerCall c = do
   fun <- ask
   modify (addCall fun c)
@@ -96,30 +101,36 @@ checkTypeSignature :: Members '[State CallMap, Reader FunctionName] r => Express
 checkTypeSignature = runReader (emptySizeInfo :: SizeInfo) . checkExpression
 
 emptySizeInfo :: SizeInfo
-emptySizeInfo = SizeInfo {
-  _sizeEqual = mempty,
-  _sizeSmaller = mempty
-  }
+emptySizeInfo =
+  SizeInfo
+    { _sizeEqual = mempty,
+      _sizeSmaller = mempty
+    }
 
 mkSizeInfo :: [Pattern] -> SizeInfo
 mkSizeInfo ps = SizeInfo {..}
   where
-  _sizeEqual = ps
-  _sizeSmaller = HashMap.fromList
-    [ (v, i) | (i, p) <- zip [0..] ps,
-      v <- smallerPatternVariables p]
+    _sizeEqual = ps
+    _sizeSmaller =
+      HashMap.fromList
+        [ (v, i) | (i, p) <- zip [0 ..] ps, v <- smallerPatternVariables p
+        ]
 
-checkFunctionClause :: Members '[State CallMap, Reader FunctionName] r =>
-  FunctionClause -> Sem r ()
-checkFunctionClause cl = runReader (mkSizeInfo (cl ^. clausePatterns))
-  $ checkExpression (cl ^. clauseBody)
+checkFunctionClause ::
+  Members '[State CallMap, Reader FunctionName] r =>
+  FunctionClause ->
+  Sem r ()
+checkFunctionClause cl =
+  runReader (mkSizeInfo (cl ^. clausePatterns)) $
+    checkExpression (cl ^. clauseBody)
 
 checkExpression :: Members '[State CallMap, Reader FunctionName, Reader SizeInfo] r => Expression -> Sem r ()
 checkExpression e = do
   mc <- viewCall e
   case mc of
-    Just c -> do registerCall c
-                 mapM_ (checkExpression . snd) (c ^. callArgs)
+    Just c -> do
+      registerCall c
+      mapM_ (checkExpression . snd) (c ^. callArgs)
     Nothing -> case e of
       ExpressionApplication a -> checkApplication a
       ExpressionIden {} -> return ()
@@ -127,18 +138,24 @@ checkExpression e = do
       ExpressionFunction f -> checkFunction f
       ExpressionLiteral {} -> return ()
 
-checkApplication :: Members '[State CallMap, Reader FunctionName, Reader SizeInfo] r
-  => Application -> Sem r ()
+checkApplication ::
+  Members '[State CallMap, Reader FunctionName, Reader SizeInfo] r =>
+  Application ->
+  Sem r ()
 checkApplication (Application l r) = do
   checkExpression l
   checkExpression r
 
-checkFunction :: Members '[State CallMap, Reader FunctionName, Reader SizeInfo] r
-  => Function -> Sem r ()
+checkFunction ::
+  Members '[State CallMap, Reader FunctionName, Reader SizeInfo] r =>
+  Function ->
+  Sem r ()
 checkFunction (Function l r) = do
   checkFunctionParameter l
   checkExpression r
 
-checkFunctionParameter :: Members '[State CallMap, Reader FunctionName, Reader SizeInfo] r
-   => FunctionParameter -> Sem r ()
+checkFunctionParameter ::
+  Members '[State CallMap, Reader FunctionName, Reader SizeInfo] r =>
+  FunctionParameter ->
+  Sem r ()
 checkFunctionParameter p = checkExpression (p ^. paramType)

src/MiniJuvix/Termination/Types.hs

@@ -1,28 +1,29 @@
-module MiniJuvix.Termination.Types (
-  module MiniJuvix.Termination.Types.SizeRelation,
-  module MiniJuvix.Termination.Types
-                                             ) where
+module MiniJuvix.Termination.Types
+  ( module MiniJuvix.Termination.Types.SizeRelation,
+    module MiniJuvix.Termination.Types,
+  )
+where
 
+import qualified Data.HashMap.Strict as HashMap
 import MiniJuvix.Prelude
 import qualified MiniJuvix.Syntax.Abstract.Language as A
-import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
-import qualified Data.HashMap.Strict as HashMap
-import Prettyprinter as PP
-import MiniJuvix.Termination.Types.SizeRelation
 import MiniJuvix.Syntax.Abstract.Pretty.Base
+import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
+import MiniJuvix.Termination.Types.SizeRelation
+import Prettyprinter as PP
 
-newtype CallMap = CallMap {
-  _callMap :: HashMap A.FunctionName (HashMap A.FunctionName [FunCall]) }
+newtype CallMap = CallMap
+  { _callMap :: HashMap A.FunctionName (HashMap A.FunctionName [FunCall])
+  }
   deriving newtype (Semigroup, Monoid)
 
-
-data FunCall = FunCall {
-  _callName :: A.FunctionName,
-  _callArgs :: [(CallRow, A.Expression)]
+data FunCall = FunCall
+  { _callName :: A.FunctionName,
+    _callArgs :: [(CallRow, A.Expression)]
   }
 
-newtype CallRow = CallRow {
-  _callRow :: Maybe (Int, Rel')
+newtype CallRow = CallRow
+  { _callRow :: Maybe (Int, Rel')
   }
   deriving stock (Eq, Show, Generic)
 
@@ -30,11 +31,12 @@ instance Hashable CallRow
 
 type CallMatrix = [CallRow]
 
-data Call = Call {
-  _callFrom :: A.FunctionName,
-  _callTo :: A.FunctionName,
-  _callMatrix :: CallMatrix
+data Call = Call
+  { _callFrom :: A.FunctionName,
+    _callTo :: A.FunctionName,
+    _callMatrix :: CallMatrix
   }
+
 newtype LexOrder = LexOrder (NonEmpty Int)
 
 makeLenses ''FunCall
@@ -47,36 +49,36 @@ instance PrettyCode FunCall where
     f' <- ppSCode f
     return $ f' <+> hsep args'
     where
-    ppArg :: (CallRow, A.Expression) -> Sem r (Doc Ann)
-    ppArg (CallRow mi, a) =
-      case mi of
-        Just (i, r) -> relAux (Just i) (RJust r)
-        Nothing -> relAux Nothing RNothing
-      where
-      relAux mayIx r = do
-        showDecr <- asks _optShowDecreasingArgs
-        let pi = annotate AnnImportant . pretty <$> mayIx
-            pr = annotate AnnKeyword (pretty r)
-        case showDecr of
-          OnlyArg -> ppCodeAtom a
-          OnlyRel -> return $ dbrackets (pr <+?> pi)
-          ArgRel -> do
-            a' <- ppCode a
-            return $ dbrackets (a' <+> pr <+?> pi)
-    dbrackets :: Doc a -> Doc a
-    dbrackets x = pretty '⟦' <> x <> pretty '⟧'
+      ppArg :: (CallRow, A.Expression) -> Sem r (Doc Ann)
+      ppArg (CallRow mi, a) =
+        case mi of
+          Just (i, r) -> relAux (Just i) (RJust r)
+          Nothing -> relAux Nothing RNothing
+        where
+          relAux mayIx r = do
+            showDecr <- asks _optShowDecreasingArgs
+            let pi = annotate AnnImportant . pretty <$> mayIx
+                pr = annotate AnnKeyword (pretty r)
+            case showDecr of
+              OnlyArg -> ppCodeAtom a
+              OnlyRel -> return $ dbrackets (pr <+?> pi)
+              ArgRel -> do
+                a' <- ppCode a
+                return $ dbrackets (a' <+> pr <+?> pi)
+      dbrackets :: Doc a -> Doc a
+      dbrackets x = pretty '⟦' <> x <> pretty '⟧'
 
 instance PrettyCode CallMap where
   ppCode :: forall r. Members '[Reader Options] r => CallMap -> Sem r (Doc Ann)
   ppCode (CallMap m) = vsep <$> mapM ppEntry (HashMap.toList m)
     where
-    ppEntry :: (A.FunctionName, HashMap A.FunctionName [FunCall]) -> Sem r (Doc Ann)
-    ppEntry (fun, mcalls) = do
-      fun' <- annotate AnnImportant <$> ppSCode fun
-      calls' <- vsep <$> mapM ppCode calls
-      return $ fun' <+> waveFun <+> align calls'
-      where
-      calls = concat (HashMap.elems mcalls)
+      ppEntry :: (A.FunctionName, HashMap A.FunctionName [FunCall]) -> Sem r (Doc Ann)
+      ppEntry (fun, mcalls) = do
+        fun' <- annotate AnnImportant <$> ppSCode fun
+        calls' <- vsep <$> mapM ppCode calls
+        return $ fun' <+> waveFun <+> align calls'
+        where
+          calls = concat (HashMap.elems mcalls)
 
 kwQuestion :: Doc Ann
 kwQuestion = annotate AnnKeyword "?"

src/MiniJuvix/Termination/Types/SizeRelation.hs

@@ -1,20 +1,21 @@
 module MiniJuvix.Termination.Types.SizeRelation where
 
-import MiniJuvix.Prelude
 import Algebra.Graph.Label
+import MiniJuvix.Prelude
 import Prettyprinter
 
-data Rel =
-  RJust Rel'
+data Rel
+  = RJust Rel'
   | RNothing
   deriving stock (Eq, Show, Generic)
 
-data Rel' =
-  REq
+data Rel'
+  = REq
   | RLe
   deriving stock (Eq, Show, Generic)
 
 instance Hashable Rel'
+
 instance Hashable Rel
 
 toRel :: Rel' -> Rel

src/MiniJuvix/Translation/AbstractToMicroJuvix.hs

@@ -1,17 +1,18 @@
 module MiniJuvix.Translation.AbstractToMicroJuvix where
 
+import qualified Data.HashMap.Strict as HashMap
 import MiniJuvix.Prelude
 import qualified MiniJuvix.Syntax.Abstract.Language.Extra as A
-import qualified MiniJuvix.Syntax.Usage as A
-import MiniJuvix.Syntax.MicroJuvix.Language
 import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
-import qualified Data.HashMap.Strict as HashMap
+import MiniJuvix.Syntax.MicroJuvix.Language
+import qualified MiniJuvix.Syntax.Usage as A
 
 translateModule :: A.TopModule -> Module
-translateModule m = Module {
-  _moduleName = goTopModuleName (m ^. A.moduleName),
-  _moduleBody = goModuleBody (m ^. A.moduleBody)
-  }
+translateModule m =
+  Module
+    { _moduleName = goTopModuleName (m ^. A.moduleName),
+      _moduleBody = goModuleBody (m ^. A.moduleBody)
+    }
 
 goTopModuleName :: A.TopModuleName -> Name
 goTopModuleName = goSymbol . S.topModulePathName
@@ -20,11 +21,12 @@ goName :: S.Name -> Name
 goName = goSymbol . S.nameUnqualify
 
 goSymbol :: S.Symbol -> Name
-goSymbol s = Name {
-  _nameText = S.symbolText s,
-  _nameId = S._nameId s,
-  _nameKind = getNameKind s
- }
+goSymbol s =
+  Name
+    { _nameText = S.symbolText s,
+      _nameId = S._nameId s,
+      _nameKind = getNameKind s
+    }
 
 unsupported :: Text -> a
 unsupported thing = error ("Not yet supported: " <> thing)
@@ -34,21 +36,27 @@ goImport m = goModuleBody (m ^. A.moduleBody)
 
 goModuleBody :: A.ModuleBody -> ModuleBody
 goModuleBody b
- | not (HashMap.null (b ^. A.moduleLocalModules)) = unsupported "local modules"
- | otherwise = ModuleBody {
-     _moduleInductives = HashMap.fromList
-       [ (d ^. indexedThing . inductiveName, d)
-        | d <- map (fmap goInductiveDef) (toList (b ^. A.moduleInductives))],
-     _moduleFunctions = HashMap.fromList
-        [ (f ^. indexedThing . funDefName, f) |
-          f <- map (fmap goFunctionDef) (toList (b ^. A.moduleFunctions)) ],
-     _moduleForeign = b ^. A.moduleForeign
-     }
-     -- <> mconcatMap goImport (b ^. A.moduleImports)
+  | not (HashMap.null (b ^. A.moduleLocalModules)) = unsupported "local modules"
+  | otherwise =
+    ModuleBody
+      { _moduleInductives =
+          HashMap.fromList
+            [ (d ^. indexedThing . inductiveName, d)
+              | d <- map (fmap goInductiveDef) (toList (b ^. A.moduleInductives))
+            ],
+        _moduleFunctions =
+          HashMap.fromList
+            [ (f ^. indexedThing . funDefName, f)
+              | f <- map (fmap goFunctionDef) (toList (b ^. A.moduleFunctions))
+            ],
+        _moduleForeigns = b ^. A.moduleForeigns
+      }
+
+-- <> mconcatMap goImport (b ^. A.moduleImports)
 
 goTypeIden :: A.Iden -> TypeIden
 goTypeIden i = case i of
-  A.IdenDefined {} -> unsupported "functions in types"
+  A.IdenFunction {} -> unsupported "functions in types"
   A.IdenConstructor {} -> unsupported "constructors in types"
   A.IdenVar {} -> unsupported "type variables"
   A.IdenInductive d -> TypeIdenInductive (goName d)
@@ -65,17 +73,19 @@ goFunction :: A.Function -> Function
 goFunction (A.Function l r) = Function (goFunctionParameter l) (goType r)
 
 goFunctionDef :: A.FunctionDef -> FunctionDef
-goFunctionDef f = FunctionDef {
-  _funDefName = goSymbol (f ^. A.funDefName),
-  _funDefTypeSig = goType (f ^. A.funDefTypeSig),
-  _funDefClauses = fmap goFunctionClause (f ^. A.funDefClauses)
-  }
+goFunctionDef f =
+  FunctionDef
+    { _funDefName = goSymbol (f ^. A.funDefName),
+      _funDefTypeSig = goType (f ^. A.funDefTypeSig),
+      _funDefClauses = fmap goFunctionClause (f ^. A.funDefClauses)
+    }
 
 goFunctionClause :: A.FunctionClause -> FunctionClause
-goFunctionClause c = FunctionClause {
-  _clausePatterns = map goPattern (c ^. A.clausePatterns),
-  _clauseBody = goExpression (c ^. A.clauseBody)
-  }
+goFunctionClause c =
+  FunctionClause
+    { _clausePatterns = map goPattern (c ^. A.clausePatterns),
+      _clauseBody = goExpression (c ^. A.clauseBody)
+    }
 
 goPattern :: A.Pattern -> Pattern
 goPattern p = case p of
@@ -85,8 +95,10 @@ goPattern p = case p of
   A.PatternEmpty -> unsupported "pattern empty"
 
 goConstructorApp :: A.ConstructorApp -> ConstructorApp
-goConstructorApp c = ConstructorApp (goName (c ^. A.constrAppConstructor))
-  (map goPattern (c ^. A.constrAppParameters))
+goConstructorApp c =
+  ConstructorApp
+    (goName (c ^. A.constrAppConstructor))
+    (map goPattern (c ^. A.constrAppParameters))
 
 goType :: A.Expression -> Type
 goType e = case e of
@@ -101,7 +113,7 @@ goApplication (A.Application f x) = Application (goExpression f) (goExpression x
 
 goIden :: A.Iden -> Iden
 goIden i = case i of
-  A.IdenDefined n -> IdenDefined (goName n)
+  A.IdenFunction n -> IdenFunction (goName n)
   A.IdenConstructor c -> IdenConstructor (goName c)
   A.IdenVar v -> IdenVar (goSymbol v)
   A.IdenAxiom {} -> unsupported "axiom identifier"
@@ -118,19 +130,21 @@ goExpression e = case e of
 goInductiveDef :: A.InductiveDef -> InductiveDef
 goInductiveDef i = case i ^. A.inductiveType of
   Just {} -> unsupported "inductive indices"
-  _ -> InductiveDef {
-    _inductiveName = indName,
-    _inductiveConstructors = map goConstructorDef (i ^. A.inductiveConstructors)
-  }
+  _ ->
+    InductiveDef
+      { _inductiveName = indName,
+        _inductiveConstructors = map goConstructorDef (i ^. A.inductiveConstructors)
+      }
   where
-  indName = goSymbol (i ^. A.inductiveName)
-  goConstructorDef :: A.InductiveConstructorDef -> InductiveConstructorDef
-  goConstructorDef c = InductiveConstructorDef {
-    _constructorName = goSymbol (c ^. A.constructorName),
-    _constructorParameters = goConstructorType (c ^. A.constructorType)
-    }
-  goConstructorType :: A.Expression -> [Type]
-  goConstructorType = fst . viewExpressionFunctionType
+    indName = goSymbol (i ^. A.inductiveName)
+    goConstructorDef :: A.InductiveConstructorDef -> InductiveConstructorDef
+    goConstructorDef c =
+      InductiveConstructorDef
+        { _constructorName = goSymbol (c ^. A.constructorName),
+          _constructorParameters = goConstructorType (c ^. A.constructorType)
+        }
+    goConstructorType :: A.Expression -> [Type]
+    goConstructorType = fst . viewExpressionFunctionType
 
 -- TODO: add docs or an example
 viewExpressionFunctionType :: A.Expression -> ([Type], Type)
@@ -143,4 +157,5 @@ viewExpressionFunctionType e = case e of
 
 viewFunctionType :: A.Function -> (NonEmpty Type, Type)
 viewFunctionType (A.Function p r) = (goFunctionParameter p :| args, ret)
-  where (args, ret) = viewExpressionFunctionType r
+  where
+    (args, ret) = viewExpressionFunctionType r

src/MiniJuvix/Translation/ScopedToAbstract.hs

@@ -1,11 +1,11 @@
 module MiniJuvix.Translation.ScopedToAbstract where
 
-import MiniJuvix.Prelude
-import MiniJuvix.Syntax.Concrete.Language
-import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
-import qualified MiniJuvix.Syntax.Abstract.Language as A
 import qualified Data.HashMap.Strict as HashMap
-
+import MiniJuvix.Prelude
+import qualified MiniJuvix.Syntax.Abstract.Language as A
+import MiniJuvix.Syntax.Concrete.Language
+import qualified MiniJuvix.Syntax.Concrete.Language as C
+import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
 
 type Err = Text
 
@@ -32,85 +32,102 @@ goModuleBody ss' = do
   _moduleLocalModules <- locals
   _moduleFunctions <- functions
   _moduleImports <- imports
-  _moduleForeign <- foreigns
+  _moduleForeigns <- foreigns
   return A.ModuleBody {..}
   where
-  ss :: [Indexed (Statement 'Scoped)]
-  ss = zipWith Indexed [0 ..] ss'
-  inductives :: Sem r (HashMap A.InductiveName (Indexed A.InductiveDef))
-  inductives = sequence $ HashMap.fromList
-    [ (def ^. inductiveName, Indexed i <$> goInductive def)
-    | Indexed i (StatementInductive def) <- ss ]
-  locals :: Sem r (HashMap A.InductiveName (Indexed A.LocalModule))
-  locals = sequence $ HashMap.fromList
-    [ (m ^. modulePath, Indexed i <$> goLocalModule m)
-    | Indexed i (StatementModule m) <- ss ]
-  foreigns :: Sem r [Indexed ForeignBlock]
-  foreigns = return
-    [ Indexed i f
-    | Indexed i (StatementForeign f) <- ss ]
-  imports :: Sem r [Indexed A.TopModule]
-  imports = sequence $
-    [ Indexed i <$> goModule m
-    | Indexed i (StatementImport (Import m)) <- ss ]
-  functions :: Sem r (HashMap A.FunctionName (Indexed A.FunctionDef))
-  functions = do
-    sequence $ HashMap.fromList
-     [ (name, Indexed i <$> funDef)
-     | Indexed i sig <- sigs,
-       let name = sig ^. sigName,
-       let clauses = mapM goFunctionClause (getClauses name),
-       let funDef = liftA2 (A.FunctionDef name) (goExpression (sig ^. sigType)) clauses ]
-    where
-    getClauses :: S.Symbol -> NonEmpty (FunctionClause 'Scoped)
-    getClauses name = fromMaybe impossible $
-       nonEmpty [ c | StatementFunctionClause c <- ss',
-                  name == c ^.clauseOwnerFunction ]
-    sigs :: [Indexed (TypeSignature 'Scoped)]
-    sigs = [ Indexed i t | (Indexed i (StatementTypeSignature t)) <- ss ]
-
+    ss :: [Indexed (Statement 'Scoped)]
+    ss = zipWith Indexed [0 ..] ss'
+    inductives :: Sem r (HashMap A.InductiveName (Indexed A.InductiveDef))
+    inductives =
+      sequence $
+        HashMap.fromList
+          [ (def ^. inductiveName, Indexed i <$> goInductive def)
+            | Indexed i (StatementInductive def) <- ss
+          ]
+    locals :: Sem r (HashMap A.InductiveName (Indexed A.LocalModule))
+    locals =
+      sequence $
+        HashMap.fromList
+          [ (m ^. modulePath, Indexed i <$> goLocalModule m)
+            | Indexed i (StatementModule m) <- ss
+          ]
+    foreigns :: Sem r [Indexed ForeignBlock]
+    foreigns =
+      return
+        [ Indexed i f
+          | Indexed i (StatementForeign f) <- ss
+        ]
+    imports :: Sem r [Indexed A.TopModule]
+    imports =
+      sequence $
+        [ Indexed i <$> goModule m
+          | Indexed i (StatementImport (Import m)) <- ss
+        ]
+    functions :: Sem r (HashMap A.FunctionName (Indexed A.FunctionDef))
+    functions = do
+      sequence $
+        HashMap.fromList
+          [ (name, Indexed i <$> funDef)
+            | Indexed i sig <- sigs,
+              let name = sig ^. sigName,
+              let clauses = mapM goFunctionClause (getClauses name),
+              let funDef = liftA2 (A.FunctionDef name) (goExpression (sig ^. sigType)) clauses
+          ]
+      where
+        getClauses :: S.Symbol -> NonEmpty (FunctionClause 'Scoped)
+        getClauses name =
+          fromMaybe impossible $
+            nonEmpty
+              [ c | StatementFunctionClause c <- ss', name == c ^. clauseOwnerFunction
+              ]
+        sigs :: [Indexed (TypeSignature 'Scoped)]
+        sigs = [Indexed i t | (Indexed i (StatementTypeSignature t)) <- ss]
 
 goFunctionClause :: forall r. Members '[Error Err] r => FunctionClause 'Scoped -> Sem r A.FunctionClause
 goFunctionClause FunctionClause {..} = do
   _clausePatterns' <- mapM goPattern _clausePatterns
   _clauseBody' <- goExpression _clauseBody
   goWhereBlock _clauseWhere
-  return A.FunctionClause {
-    _clausePatterns = _clausePatterns',
-    _clauseBody = _clauseBody'
-    }
+  return
+    A.FunctionClause
+      { _clausePatterns = _clausePatterns',
+        _clauseBody = _clauseBody'
+      }
 
 goWhereBlock :: forall r. Members '[Error Err] r => Maybe (WhereBlock 'Scoped) -> Sem r ()
 goWhereBlock w = case w of
- Just _ ->  unsupported "where block"
- Nothing -> return ()
+  Just _ -> unsupported "where block"
+  Nothing -> return ()
 
 goInductiveParameter :: Members '[Error Err] r => InductiveParameter 'Scoped -> Sem r A.FunctionParameter
 goInductiveParameter InductiveParameter {..} = do
   paramType' <- goExpression _inductiveParameterType
-  return A.FunctionParameter {
-    _paramType = paramType',
-    _paramName = Just _inductiveParameterName,
-    _paramUsage = UsageOmega
-    }
+  return
+    A.FunctionParameter
+      { _paramType = paramType',
+        _paramName = Just _inductiveParameterName,
+        _paramUsage = UsageOmega
+      }
 
 goInductive :: Members '[Error Err] r => InductiveDef 'Scoped -> Sem r A.InductiveDef
 goInductive InductiveDef {..} = do
   _inductiveParameters' <- mapM goInductiveParameter _inductiveParameters
   _inductiveType' <- sequence $ goExpression <$> _inductiveType
   _inductiveConstructors' <- mapM goConstructorDef _inductiveConstructors
-  return A.InductiveDef {
-    _inductiveParameters = _inductiveParameters',
-    _inductiveName = _inductiveName,
-    _inductiveType = _inductiveType',
-    _inductiveConstructors = _inductiveConstructors'
-    }
+  return
+    A.InductiveDef
+      { _inductiveParameters = _inductiveParameters',
+        _inductiveName = _inductiveName,
+        _inductiveType = _inductiveType',
+        _inductiveConstructors = _inductiveConstructors'
+      }
 
 goConstructorDef :: Members '[Error Err] r => InductiveConstructorDef 'Scoped -> Sem r A.InductiveConstructorDef
 goConstructorDef (InductiveConstructorDef c ty) = A.InductiveConstructorDef c <$> goExpression ty
 
 goExpression :: forall r. Members '[Error Err] r => Expression -> Sem r A.Expression
 goExpression e = case e of
+  -- TODO: Continue here
   ExpressionIdentifier nt -> return (goIden nt)
   ExpressionParensIdentifier nt -> return (goIden nt)
   ExpressionApplication a -> A.ExpressionApplication <$> goApplication a
@@ -123,41 +140,32 @@ goExpression e = case e of
   ExpressionUniverse uni -> return $ A.ExpressionUniverse (goUniverse uni)
   ExpressionFunction func -> A.ExpressionFunction <$> goFunction func
   where
-  goIden :: S.Name -> A.Expression
-  goIden = A.ExpressionIden . goName
-  goName :: S.Name -> A.Iden
-  goName nm = case nm ^. S.nameKind of
-     S.KNameConstructor -> A.IdenConstructor nm
-     S.KNameFunction -> A.IdenDefined nm
-     S.KNameInductive -> A.IdenInductive nm
-     S.KNameLocal -> A.IdenVar (fromUnqualified nm)
-     S.KNameAxiom -> A.IdenAxiom nm
-     S.KNameLocalModule -> impossible
-     S.KNameTopModule -> impossible
-    where
-    fromUnqualified :: S.Name -> S.Symbol
-    fromUnqualified = over S.nameConcrete (\c -> case c of
-      NameQualified {} -> impossible
-      NameUnqualified u -> u)
+    goIden :: C.ScopedIden -> A.Expression
+    goIden x = A.ExpressionIden $ case x of
+      ScopedAxiom a -> A.IdenAxiom (a ^. C.axiomRefName)
+      ScopedInductive i -> A.IdenInductive (i ^. C.inductiveRefName)
+      ScopedVar v -> A.IdenVar v
+      ScopedFunction fun -> A.IdenFunction (fun ^. C.functionRefName)
+      ScopedConstructor c -> A.IdenConstructor (c ^. C.constructorRefName)
 
-  goApplication :: Application -> Sem r A.Application
-  goApplication (Application l r) = do
-    l' <- goExpression l
-    r' <- goExpression r
-    return (A.Application l' r')
+    goApplication :: Application -> Sem r A.Application
+    goApplication (Application l r) = do
+      l' <- goExpression l
+      r' <- goExpression r
+      return (A.Application l' r')
 
-  goPostfix :: PostfixApplication -> Sem r A.Application
-  goPostfix (PostfixApplication l op) = do
-    l' <- goExpression l
-    let op' = goIden op
-    return (A.Application op' l')
+    goPostfix :: PostfixApplication -> Sem r A.Application
+    goPostfix (PostfixApplication l op) = do
+      l' <- goExpression l
+      let op' = goIden op
+      return (A.Application op' l')
 
-  goInfix :: InfixApplication -> Sem r A.Application
-  goInfix (InfixApplication l op r) = do
-    l' <- goExpression l
-    let op' = goIden op
-    r' <- goExpression r
-    return $ A.Application (A.ExpressionApplication (A.Application op' l')) r'
+    goInfix :: InfixApplication -> Sem r A.Application
+    goInfix (InfixApplication l op r) = do
+      l' <- goExpression l
+      let op' = goIden op
+      r' <- goExpression r
+      return $ A.Application (A.ExpressionApplication (A.Application op' l')) r'
 
 goUniverse :: Universe -> Universe
 goUniverse = id
@@ -183,7 +191,7 @@ goFunctionParameter (FunctionParameter _paramName u ty) = do
 goPatternApplication :: forall r. Members '[Error Err] r => PatternApp -> Sem r A.ConstructorApp
 goPatternApplication a = uncurry A.ConstructorApp <$> viewApp (PatternApplication a)
 
-goPatternConstructor :: forall r. Members '[Error Err] r => S.Name -> Sem r A.ConstructorApp
+goPatternConstructor :: forall r. Members '[Error Err] r => ConstructorRef -> Sem r A.ConstructorApp
 goPatternConstructor a = uncurry A.ConstructorApp <$> viewApp (PatternConstructor a)
 
 goInfixPatternApplication :: forall r. Members '[Error Err] r => PatternInfixApp -> Sem r A.ConstructorApp
@@ -194,27 +202,23 @@ goPostfixPatternApplication a = uncurry A.ConstructorApp <$> viewApp (PatternPos
 
 viewApp :: forall r. Members '[Error Err] r => Pattern -> Sem r (A.Name, [A.Pattern])
 viewApp p = case p of
-  PatternConstructor c -> checkConstructorKind c $> (c, [])
+  PatternConstructor c -> return (c ^. constructorRefName, [])
   PatternApplication (PatternApp l r) -> do
     r' <- goPattern r
     second (`snoc` r') <$> viewApp l
   PatternInfixApplication (PatternInfixApp l c r) -> do
-    checkConstructorKind c
     l' <- goPattern l
     r' <- goPattern r
-    return (c, [l', r'])
-  PatternPostfixApplication  (PatternPostfixApp l c) -> do
-    checkConstructorKind c
+    return (c ^. constructorRefName, [l', r'])
+  PatternPostfixApplication (PatternPostfixApp l c) -> do
     l' <- goPattern l
-    return (c, [l'])
+    return (c ^. constructorRefName, [l'])
   PatternVariable {} -> err
   PatternWildcard {} -> err
   PatternEmpty {} -> err
   where
-  err :: Sem r a
-  err = throw ("constructor expected on the left of a pattern application" :: Err)
-  checkConstructorKind :: S.Name -> Sem r ()
-  checkConstructorKind n = unless (S.isConstructor n) err
+    err :: Sem r a
+    err = throw ("constructor expected on the left of a pattern application" :: Err)
 
 goPattern :: forall r. Members '[Error Err] r => Pattern -> Sem r A.Pattern
 goPattern p = case p of

src/MiniJuvix/Utils/Paths.hs

@@ -1,8 +1,8 @@
 module MiniJuvix.Utils.Paths where
 
+import Language.Haskell.TH.Syntax as TH
 import MiniJuvix.Prelude
 import TH.RelativePaths
-import Language.Haskell.TH.Syntax as TH
 
 assetsDir :: Q Exp
 assetsDir = pathRelativeToCabalPackage "assets" >>= TH.lift

test/Scope/Positive.hs

@@ -41,7 +41,7 @@ testDescr PosTest {..} = TestDescr {
     parsedPretty' <- parseTextModuleIO parsedPretty
 
     step "Scope again"
-    s' <- fromRightIO' printErrorAnsi $ 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')