qualified names

src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs

@@ -80,7 +80,7 @@ goModule onlyTypes infoTable Internal.Module {..} =
   where
     toIsabelleTheoryName :: Text -> Text
     toIsabelleTheoryName name =
-      Text.intercalate "_" $ filter (/= "") $ T.splitOn "." name
+      quote . Text.intercalate "_" $ filter (/= "") $ T.splitOn "." name
 
     isTypeDef :: Statement -> Bool
     isTypeDef = \case
@@ -1219,8 +1219,25 @@ goModule onlyTypes infoTable Internal.Module {..} =
                 ++ map (^. Internal.axiomInfoDef . Internal.axiomName . namePretty) (HashMap.elems (infoTable ^. Internal.infoAxioms))
 
     quote :: Text -> Text
-    quote = quote' . Text.filter isLatin1 . Text.filter (isLetter .||. isDigit .||. (== '_') .||. (== '\''))
+    quote txt0
+      | Text.elem '.' txt0 = moduleName' <> "." <> idenName'
+      | otherwise = quote'' txt0
       where
+        (moduleName, idenName) = Text.breakOnEnd "." txt0
+        moduleName' = toIsabelleTheoryName (removeLastDot moduleName)
+        idenName' = quote'' idenName
+
+        removeLastDot :: Text -> Text
+        removeLastDot txt
+          | Text.last txt == '.' = Text.init txt
+          | otherwise = txt
+
+        quote'' :: Text -> Text
+        quote'' =
+          quote'
+            . Text.filter isLatin1
+            . Text.filter (isLetter .||. isDigit .||. (== '_') .||. (== '\''))
+
         quote' :: Text -> Text
         quote' txt
           | HashSet.member txt reservedNames = quote' (prime txt)

src/Juvix/Parser/Error.hs

@@ -177,7 +177,7 @@ instance ToGenericError StdinOrFileError where
   genericError StdinOrFileError =
     return
       GenericError
-        { _genericErrorLoc = singletonInterval (mkInitialLoc formatStdinPath),
+        { _genericErrorLoc = singletonInterval (mkInitialLoc noFile),
           _genericErrorMessage = prettyError "Neither JUVIX_FILE_OR_PROJECT nor --stdin option is chosen",
           _genericErrorIntervals = []
         }

tests/positive/Isabelle/M/Main.juvix

@@ -0,0 +1,6 @@
+module M.Main;
+
+import Stdlib.Prelude open;
+import M.N open;
+
+f (a : Nat) : Nat := g a;

tests/positive/Isabelle/M/N.juvix

@@ -0,0 +1,5 @@
+module M.N;
+
+import Stdlib.Prelude open;
+
+g (a : Nat) : Nat := a + 1;

tests/positive/Isabelle/N.juvix

@@ -0,0 +1,5 @@
+module N;
+
+import Stdlib.Prelude open;
+
+g (a : Nat) : Nat := a * 2;

tests/positive/Isabelle/Program.juvix

@@ -1,6 +1,9 @@
 module Program;
 
 import Stdlib.Prelude open;
+import N;
+import M.N;
+import M.Main as Main;
 
 id0 : Nat -> Nat := id;
 
@@ -23,7 +26,7 @@ f (x y : Nat) : Nat -> Nat
 
 g (x y : Nat) : Bool :=
   if
-    | x == y := false
+    | x == f x (N.g y) (M.N.g (Main.f y)) := false
     | else := true;
 
 inc (x : Nat) : Nat := suc x;

tests/positive/Isabelle/isabelle/M_Main.thy

@@ -0,0 +1,9 @@
+theory M_Main
+imports Main
+        M_N
+begin
+
+fun f :: "nat \<Rightarrow> nat" where
+  "f a = (g a)"
+
+end

tests/positive/Isabelle/isabelle/M_N.thy

@@ -0,0 +1,8 @@
+theory M_N
+imports Main
+begin
+
+fun g :: "nat \<Rightarrow> nat" where
+  "g a = (a + 1)"
+
+end

tests/positive/Isabelle/isabelle/N.thy

@@ -0,0 +1,8 @@
+theory N
+imports Main
+begin
+
+fun g :: "nat \<Rightarrow> nat" where
+  "g a = (a * 2)"
+
+end

tests/positive/Isabelle/isabelle/Program.thy

@@ -1,5 +1,8 @@
 theory Program
 imports Main
+        N
+        M_N
+        M_Main
 begin
 
 definition id0 :: "nat \<Rightarrow> nat" where
@@ -25,7 +28,7 @@ fun f :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where
   "f x y z = ((z + 1) * x + y)"
 
 fun g :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
-  "g x y = (if x = y then False else True)"
+  "g x y = (if x = f x (N.g y) (M_N.g (M_Main.f y)) then False else True)"
 
 fun inc :: "nat \<Rightarrow> nat" where
   "inc x = (Suc x)"