[abstract] Make Iden use references instead of Name

src/MiniJuvix/Syntax/Abstract/Language.hs

@@ -25,6 +25,9 @@ type InductiveName = S.Symbol
 
 type AxiomName = S.Symbol
 
+-- TODO: Perhaps we could use a different Name type
+--  that just includes fields (nameId + debug info)
+-- requried in future passes.
 type Name = S.Name
 
 type TopModule = Module C.TopModulePath
@@ -59,12 +62,29 @@ data FunctionClause = FunctionClause
   }
   deriving stock (Show, Eq)
 
+newtype FunctionRef = FunctionRef
+  { _functionRefName :: Name }
+  deriving stock (Show, Eq)
+  deriving newtype Hashable
+
+newtype ConstructorRef = ConstructorRef
+  { _constructorRefName :: Name }
+  deriving stock (Show, Eq)
+
+newtype InductiveRef = InductiveRef
+  { _inductiveRefName :: Name }
+  deriving stock (Show, Eq)
+
+newtype AxiomRef = AxiomRef
+  { _axiomRefName :: Name }
+  deriving stock (Show, Eq)
+
 data Iden
-  = IdenFunction Name
-  | IdenConstructor Name
+  = IdenFunction FunctionRef
+  | IdenConstructor ConstructorRef
   | IdenVar VarName
-  | IdenInductive Name
-  | IdenAxiom Name
+  | IdenInductive InductiveRef
+  | IdenAxiom AxiomRef
   deriving stock (Show, Eq)
 
 data Expression
@@ -134,7 +154,7 @@ instance HasAtomicity Function where
 
 -- | Fully applied constructor in a pattern.
 data ConstructorApp = ConstructorApp
-  { _constrAppConstructor :: Name,
+  { _constrAppConstructor :: ConstructorRef,
     _constrAppParameters :: [Pattern]
   }
   deriving stock (Show, Eq)
@@ -176,3 +196,15 @@ makeLenses ''InductiveDef
 makeLenses ''ModuleBody
 makeLenses ''InductiveConstructorDef
 makeLenses ''ConstructorApp
+makeLenses ''FunctionRef
+makeLenses ''ConstructorRef
+makeLenses ''InductiveRef
+makeLenses ''AxiomRef
+
+idenName :: Iden -> Name
+idenName = \case
+    IdenFunction n -> n ^. functionRefName
+    IdenConstructor n -> n ^. constructorRefName
+    IdenInductive n -> n ^. inductiveRefName
+    IdenVar n -> S.unqualifiedSymbol n
+    IdenAxiom n -> n ^. axiomRefName

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

@@ -43,7 +43,7 @@ viewExpressionAsPattern e = case viewApp e of
     | Just v <- getVariable f -> Just (PatternVariable v)
   _ -> Nothing
   where
-    getConstructor :: Expression -> Maybe Name
+    getConstructor :: Expression -> Maybe ConstructorRef
     getConstructor f = case f of
       ExpressionIden (IdenConstructor n) -> Just n
       _ -> Nothing

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

@@ -52,12 +52,7 @@ runPrettyCode :: PrettyCode c => Options -> c -> Doc Ann
 runPrettyCode opts = run . runReader opts . ppCode
 
 instance PrettyCode Iden where
-  ppCode i = case i of
-    IdenFunction n -> ppSCode n
-    IdenConstructor n -> ppSCode n
-    IdenInductive n -> ppSCode n
-    IdenVar n -> ppSCode n
-    IdenAxiom n -> ppSCode n
+  ppCode = ppSCode . idenName
 
 instance PrettyCode Application where
   ppCode (Application l r) = do
@@ -119,6 +114,18 @@ instance PrettyCode Function where
     funReturn' <- ppRightExpression funFixity _funReturn
     return $ funParameter' <+> kwTo <+> funReturn'
 
+instance PrettyCode FunctionRef where
+  ppCode FunctionRef {..} = ppSCode _functionRefName
+
+instance PrettyCode ConstructorRef where
+  ppCode ConstructorRef {..} = ppSCode _constructorRefName
+
+instance PrettyCode InductiveRef where
+  ppCode InductiveRef {..} = ppSCode _inductiveRefName
+
+instance PrettyCode AxiomRef where
+  ppCode AxiomRef {..} = ppSCode _axiomRefName
+
 parensCond :: Bool -> Doc Ann -> Doc Ann
 parensCond t d = if t then parens d else d
 

src/MiniJuvix/Termination/CallGraph.hs

@@ -63,11 +63,11 @@ composeEdge a b = do
         _edgeMatrices = multiplyMany (a ^. edgeMatrices) (b ^. edgeMatrices)
       }
 
-fromFunCall :: FunctionName -> FunCall -> Call
+fromFunCall :: FunctionRef -> FunCall -> Call
 fromFunCall caller fc =
   Call
-    { _callFrom = caller,
-      _callTo = fc ^. callName,
+    { _callFrom = S.nameUnqualify (caller ^. functionRefName),
+      _callTo = S.nameUnqualify (fc ^. callRef . functionRefName),
       _callMatrix = map fst (fc ^. callArgs)
     }
 

src/MiniJuvix/Termination/CallMap.hs

@@ -7,8 +7,8 @@ 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 MiniJuvix.Termination.Types
+import MiniJuvix.Syntax.Concrete.Scoped.Name (unqualifiedSymbol)
 
 -- | i = SizeInfo [v] ⇔ v is smaller than argument i of the caller function.
 -- Indexes are 0 based
@@ -55,23 +55,23 @@ viewCall e = case e of
     return (Just (singletonCall x))
   _ -> return Nothing
   where
-    singletonCall :: Name -> FunCall
-    singletonCall n = FunCall (S.nameUnqualify n) []
+    singletonCall :: FunctionRef -> FunCall
+    singletonCall r = FunCall r []
 
-addCall :: FunctionName -> FunCall -> CallMap -> CallMap
+addCall :: FunctionRef -> 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 :: FunCall -> Maybe (HashMap FunctionRef [FunCall]) -> HashMap FunctionRef [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]
+    singl :: FunCall -> HashMap FunctionRef [FunCall]
+    singl f = HashMap.singleton (f ^. callRef) [f]
+    addFunCall :: FunCall -> HashMap FunctionRef [FunCall] -> HashMap FunctionRef [FunCall]
+    addFunCall fc = HashMap.insertWith (flip (<>)) (fc ^. callRef) [fc]
 
 registerCall ::
-  Members '[State CallMap, Reader FunctionName, Reader SizeInfo] r =>
+  Members '[State CallMap, Reader FunctionRef, Reader SizeInfo] r =>
   FunCall ->
   Sem r ()
 registerCall c = do
@@ -93,11 +93,11 @@ checkLocalModule :: Members '[State CallMap] r => LocalModule -> Sem r ()
 checkLocalModule m = checkModuleBody (m ^. moduleBody)
 
 checkFunctionDef :: Members '[State CallMap] r => FunctionDef -> Sem r ()
-checkFunctionDef def = runReader (def ^. funDefName) $ do
+checkFunctionDef def = runReader (FunctionRef (unqualifiedSymbol (def ^. funDefName))) $ do
   checkTypeSignature (def ^. funDefTypeSig)
   mapM_ checkFunctionClause (def ^. funDefClauses)
 
-checkTypeSignature :: Members '[State CallMap, Reader FunctionName] r => Expression -> Sem r ()
+checkTypeSignature :: Members '[State CallMap, Reader FunctionRef] r => Expression -> Sem r ()
 checkTypeSignature = runReader (emptySizeInfo :: SizeInfo) . checkExpression
 
 emptySizeInfo :: SizeInfo
@@ -117,14 +117,14 @@ mkSizeInfo ps = SizeInfo {..}
         ]
 
 checkFunctionClause ::
-  Members '[State CallMap, Reader FunctionName] r =>
+  Members '[State CallMap, Reader FunctionRef] 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 :: Members '[State CallMap, Reader FunctionRef, Reader SizeInfo] r => Expression -> Sem r ()
 checkExpression e = do
   mc <- viewCall e
   case mc of
@@ -139,7 +139,7 @@ checkExpression e = do
       ExpressionLiteral {} -> return ()
 
 checkApplication ::
-  Members '[State CallMap, Reader FunctionName, Reader SizeInfo] r =>
+  Members '[State CallMap, Reader FunctionRef, Reader SizeInfo] r =>
   Application ->
   Sem r ()
 checkApplication (Application l r) = do
@@ -147,7 +147,7 @@ checkApplication (Application l r) = do
   checkExpression r
 
 checkFunction ::
-  Members '[State CallMap, Reader FunctionName, Reader SizeInfo] r =>
+  Members '[State CallMap, Reader FunctionRef, Reader SizeInfo] r =>
   Function ->
   Sem r ()
 checkFunction (Function l r) = do
@@ -155,7 +155,7 @@ checkFunction (Function l r) = do
   checkExpression r
 
 checkFunctionParameter ::
-  Members '[State CallMap, Reader FunctionName, Reader SizeInfo] r =>
+  Members '[State CallMap, Reader FunctionRef, Reader SizeInfo] r =>
   FunctionParameter ->
   Sem r ()
 checkFunctionParameter p = checkExpression (p ^. paramType)

src/MiniJuvix/Termination/Types.hs

@@ -11,14 +11,16 @@ import MiniJuvix.Syntax.Abstract.Pretty.Base
 import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
 import MiniJuvix.Termination.Types.SizeRelation
 import Prettyprinter as PP
+import MiniJuvix.Syntax.Abstract.Language (functionRefName)
+import MiniJuvix.Syntax.Concrete.Scoped.Name (nameUnqualify)
 
 newtype CallMap = CallMap
-  { _callMap :: HashMap A.FunctionName (HashMap A.FunctionName [FunCall])
+  { _callMap :: HashMap A.FunctionRef (HashMap A.FunctionRef [FunCall])
   }
   deriving newtype (Semigroup, Monoid)
 
 data FunCall = FunCall
-  { _callName :: A.FunctionName,
+  { _callRef :: A.FunctionRef,
     _callArgs :: [(CallRow, A.Expression)]
   }
 
@@ -46,7 +48,7 @@ instance PrettyCode FunCall where
   ppCode :: forall r. Members '[Reader Options] r => FunCall -> Sem r (Doc Ann)
   ppCode (FunCall f args) = do
     args' <- mapM ppArg args
-    f' <- ppSCode f
+    f' <- ppCode f
     return $ f' <+> hsep args'
     where
       ppArg :: (CallRow, A.Expression) -> Sem r (Doc Ann)
@@ -72,9 +74,9 @@ 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 :: (A.FunctionRef, HashMap A.FunctionRef [FunCall]) -> Sem r (Doc Ann)
       ppEntry (fun, mcalls) = do
-        fun' <- annotate AnnImportant <$> ppSCode fun
+        fun' <- annotate AnnImportant <$> ppCode fun
         calls' <- vsep <$> mapM ppCode calls
         return $ fun' <+> waveFun <+> align calls'
         where
@@ -99,4 +101,4 @@ instance PrettyCode CallMatrix where
   ppCode l = vsep <$> mapM ppCode l
 
 filterCallMap :: Foldable f => f Text -> CallMap -> CallMap
-filterCallMap funNames = over callMap (HashMap.filterWithKey (\k _ -> S.symbolText k `elem` funNames))
+filterCallMap funNames = over callMap (HashMap.filterWithKey (\k _ -> S.symbolText (nameUnqualify (k ^. functionRefName)) `elem` funNames))

src/MiniJuvix/Translation/AbstractToMicroJuvix.hs

@@ -64,7 +64,7 @@ goTypeIden i = case i of
   A.IdenFunction {} -> unsupported "functions in types"
   A.IdenConstructor {} -> unsupported "constructors in types"
   A.IdenVar {} -> unsupported "type variables"
-  A.IdenInductive d -> TypeIdenInductive (goName d)
+  A.IdenInductive d -> TypeIdenInductive (goName (d ^. A.inductiveRefName))
   A.IdenAxiom {} -> unsupported "axioms in types"
 
 goFunctionParameter :: A.FunctionParameter -> Type
@@ -102,7 +102,7 @@ goPattern p = case p of
 goConstructorApp :: A.ConstructorApp -> ConstructorApp
 goConstructorApp c =
   ConstructorApp
-    (goName (c ^. A.constrAppConstructor))
+    (goName (c ^. A.constrAppConstructor . A.constructorRefName))
     (map goPattern (c ^. A.constrAppParameters))
 
 goType :: A.Expression -> Type
@@ -118,8 +118,8 @@ goApplication (A.Application f x) = Application (goExpression f) (goExpression x
 
 goIden :: A.Iden -> Iden
 goIden i = case i of
-  A.IdenFunction n -> IdenFunction (goName n)
-  A.IdenConstructor c -> IdenConstructor (goName c)
+  A.IdenFunction n -> IdenFunction (goName (n ^. A.functionRefName))
+  A.IdenConstructor c -> IdenConstructor (goName (c ^. A.constructorRefName))
   A.IdenVar v -> IdenVar (goSymbol v)
   A.IdenAxiom {} -> unsupported "axiom identifier"
   A.IdenInductive {} -> unsupported "inductive identifier"

src/MiniJuvix/Translation/ScopedToAbstract.hs

@@ -141,11 +141,11 @@ goExpression e = case e of
   where
     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)
+      ScopedAxiom a -> A.IdenAxiom (A.AxiomRef (a ^. C.axiomRefName))
+      ScopedInductive i -> A.IdenInductive (A.InductiveRef (i ^. C.inductiveRefName))
       ScopedVar v -> A.IdenVar v
-      ScopedFunction fun -> A.IdenFunction (fun ^. C.functionRefName)
-      ScopedConstructor c -> A.IdenConstructor (c ^. C.constructorRefName)
+      ScopedFunction fun -> A.IdenFunction (A.FunctionRef (fun ^. C.functionRefName))
+      ScopedConstructor c -> A.IdenConstructor (A.ConstructorRef (c ^. C.constructorRefName))
 
     goApplication :: Application -> Sem r A.Application
     goApplication (Application l r) = do
@@ -199,19 +199,19 @@ goInfixPatternApplication a = uncurry A.ConstructorApp <$> viewApp (PatternInfix
 goPostfixPatternApplication :: forall r. Members '[Error Err] r => PatternPostfixApp -> Sem r A.ConstructorApp
 goPostfixPatternApplication a = uncurry A.ConstructorApp <$> viewApp (PatternPostfixApplication a)
 
-viewApp :: forall r. Members '[Error Err] r => Pattern -> Sem r (A.Name, [A.Pattern])
+viewApp :: forall r. Members '[Error Err] r => Pattern -> Sem r (A.ConstructorRef, [A.Pattern])
 viewApp p = case p of
-  PatternConstructor c -> return (c ^. constructorRefName, [])
+  PatternConstructor c -> return (goConstructorRef c, [])
   PatternApplication (PatternApp l r) -> do
     r' <- goPattern r
     second (`snoc` r') <$> viewApp l
   PatternInfixApplication (PatternInfixApp l c r) -> do
     l' <- goPattern l
     r' <- goPattern r
-    return (c ^. constructorRefName, [l', r'])
+    return (goConstructorRef c, [l', r'])
   PatternPostfixApplication (PatternPostfixApp l c) -> do
     l' <- goPattern l
-    return (c ^. constructorRefName, [l'])
+    return (goConstructorRef c, [l'])
   PatternVariable {} -> err
   PatternWildcard {} -> err
   PatternEmpty {} -> err
@@ -219,6 +219,9 @@ viewApp p = case p of
     err :: Sem r a
     err = throw ("constructor expected on the left of a pattern application" :: Err)
 
+goConstructorRef :: ConstructorRef -> A.ConstructorRef
+goConstructorRef (ConstructorRef' n) = A.ConstructorRef n
+
 goPattern :: forall r. Members '[Error Err] r => Pattern -> Sem r A.Pattern
 goPattern p = case p of
   PatternVariable a -> return $ A.PatternVariable a