From 2deb098adc8d2930714e0c34775989f21cf99684 Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Fri, 30 Aug 2024 18:20:19 +0200
Subject: [PATCH] use fully qualified names instead of aliases

---
 .../Backend/Isabelle/Translation/FromTyped.hs | 40 +++++++++++++------
 1 file changed, 27 insertions(+), 13 deletions(-)

diff --git a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
index 3b3b255bd4..a738a80bb9 100644
--- a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
+++ b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
@@ -196,8 +196,8 @@ goModule onlyTypes infoTable Internal.Module {..} =
                 }
       where
         argnames =
-          map (overNameText quote) $ filterTypeArgs 0 ty $ map (fromMaybe (defaultName (getLoc name) "_") . (^. Internal.argInfoName)) argsInfo
-        name' = overNameText quote name
+          map quoteName $ filterTypeArgs 0 ty $ map (fromMaybe (defaultName (getLoc name) "_") . (^. Internal.argInfoName)) argsInfo
+        name' = quoteName name
         loc = getLoc name
 
     isFunction :: [Name] -> Internal.Expression -> Maybe Internal.Expression -> Bool
@@ -377,18 +377,18 @@ goModule onlyTypes infoTable Internal.Module {..} =
 
     goTypeIden :: Internal.Iden -> Type
     goTypeIden = \case
-      Internal.IdenFunction name -> mkIndType (overNameText quote name) []
+      Internal.IdenFunction name -> mkIndType (quoteName name) []
       Internal.IdenConstructor name -> error ("unsupported type: constructor " <> Internal.ppTrace name)
-      Internal.IdenVar name -> TyVar $ TypeVar (overNameText quote name)
-      Internal.IdenAxiom name -> mkIndType (overNameText quote name) []
-      Internal.IdenInductive name -> mkIndType (overNameText quote name) []
+      Internal.IdenVar name -> TyVar $ TypeVar (quoteName name)
+      Internal.IdenAxiom name -> mkIndType (quoteName name) []
+      Internal.IdenInductive name -> mkIndType (quoteName name) []
 
     goTypeApp :: Internal.Application -> Type
     goTypeApp app = mkIndType name params
       where
         (ind, args) = Internal.unfoldApplication app
         params = map goType (toList args)
-        name = overNameText quote $ case ind of
+        name = quoteName $ case ind of
           Internal.ExpressionIden (Internal.IdenFunction n) -> n
           Internal.ExpressionIden (Internal.IdenAxiom n) -> n
           Internal.ExpressionIden (Internal.IdenInductive n) -> n
@@ -417,8 +417,8 @@ goModule onlyTypes infoTable Internal.Module {..} =
               setNameText "None" name
             Just Internal.BuiltinMaybeJust ->
               setNameText "Some" name
-            _ -> overNameText quote name
-        Nothing -> overNameText quote name
+            _ -> quoteName name
+        Nothing -> quoteName name
 
     getArgtys :: Internal.ConstructorInfo -> [Internal.FunctionParameter]
     getArgtys ctrInfo = fst $ Internal.unfoldFunType $ ctrInfo ^. Internal.constructorInfoType
@@ -431,8 +431,8 @@ goModule onlyTypes infoTable Internal.Module {..} =
             Just funInfo ->
               case funInfo ^. Internal.functionInfoPragmas . pragmasIsabelleFunction of
                 Just PragmaIsabelleFunction {..} -> setNameText _pragmaIsabelleFunctionName name
-                Nothing -> overNameText quote name
-            Nothing -> overNameText quote name
+                Nothing -> quoteName name
+            Nothing -> quoteName name
       x -> x
 
     lookupName :: forall r. (Member (Reader NameMap) r) => Name -> Sem r Expression
@@ -491,8 +491,8 @@ goModule onlyTypes infoTable Internal.Module {..} =
               Nothing -> return $ ExprIden (goConstrName name)
           Internal.IdenVar name -> do
             lookupName name
-          Internal.IdenAxiom name -> return $ ExprIden (overNameText quote name)
-          Internal.IdenInductive name -> return $ ExprIden (overNameText quote name)
+          Internal.IdenAxiom name -> return $ ExprIden (quoteName name)
+          Internal.IdenInductive name -> return $ ExprIden (quoteName name)
 
         goApplication :: Internal.Application -> Sem r Expression
         goApplication app@Internal.Application {..}
@@ -1218,6 +1218,20 @@ goModule onlyTypes infoTable Internal.Module {..} =
                 ++ map (^. Internal.inductiveInfoName . namePretty) (HashMap.elems (infoTable ^. Internal.infoInductives))
                 ++ map (^. Internal.axiomInfoDef . Internal.axiomName . namePretty) (HashMap.elems (infoTable ^. Internal.infoAxioms))
 
+    quoteName :: Name -> Name
+    quoteName name = overNameText goNameText name
+      where
+        goNameText :: Text -> Text
+        goNameText txt
+          | Text.elem '.' txt =
+              let idenName = snd $ Text.breakOnEnd "." txt
+                  modulePath = name ^. nameId . nameIdModuleId . moduleIdPath
+                  modulePathText = Text.intercalate "." (modulePath ^. modulePathKeyDir ++ [modulePath ^. modulePathKeyName])
+                  moduleName' = toIsabelleTheoryName modulePathText
+                  idenName' = quote idenName
+               in moduleName' <> "." <> idenName'
+          | otherwise = quote txt
+
     quote :: Text -> Text
     quote txt0
       | Text.elem '.' txt0 = moduleName' <> "." <> idenName'