From dc34ae7ac7514e1b3072e71f4142c49010d6b56d Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Fri, 30 Aug 2024 13:38:10 +0200 Subject: [PATCH] qualified names --- .../Backend/Isabelle/Translation/FromTyped.hs | 21 +++++++++++++++++-- src/Juvix/Parser/Error.hs | 2 +- tests/positive/Isabelle/M/Main.juvix | 6 ++++++ tests/positive/Isabelle/M/N.juvix | 5 +++++ tests/positive/Isabelle/N.juvix | 5 +++++ tests/positive/Isabelle/Program.juvix | 5 ++++- tests/positive/Isabelle/isabelle/M_Main.thy | 9 ++++++++ tests/positive/Isabelle/isabelle/M_N.thy | 8 +++++++ tests/positive/Isabelle/isabelle/N.thy | 8 +++++++ tests/positive/Isabelle/isabelle/Program.thy | 5 ++++- 10 files changed, 69 insertions(+), 5 deletions(-) create mode 100644 tests/positive/Isabelle/M/Main.juvix create mode 100644 tests/positive/Isabelle/M/N.juvix create mode 100644 tests/positive/Isabelle/N.juvix create mode 100644 tests/positive/Isabelle/isabelle/M_Main.thy create mode 100644 tests/positive/Isabelle/isabelle/M_N.thy create mode 100644 tests/positive/Isabelle/isabelle/N.thy diff --git a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs index f5d524f650..3b3b255bd4 100644 --- a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs +++ b/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) diff --git a/src/Juvix/Parser/Error.hs b/src/Juvix/Parser/Error.hs index d464a50115..8c88ea85e1 100644 --- a/src/Juvix/Parser/Error.hs +++ b/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 = [] } diff --git a/tests/positive/Isabelle/M/Main.juvix b/tests/positive/Isabelle/M/Main.juvix new file mode 100644 index 0000000000..b8e8ac4086 --- /dev/null +++ b/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; diff --git a/tests/positive/Isabelle/M/N.juvix b/tests/positive/Isabelle/M/N.juvix new file mode 100644 index 0000000000..092cfc76c8 --- /dev/null +++ b/tests/positive/Isabelle/M/N.juvix @@ -0,0 +1,5 @@ +module M.N; + +import Stdlib.Prelude open; + +g (a : Nat) : Nat := a + 1; diff --git a/tests/positive/Isabelle/N.juvix b/tests/positive/Isabelle/N.juvix new file mode 100644 index 0000000000..db6ae1ffe4 --- /dev/null +++ b/tests/positive/Isabelle/N.juvix @@ -0,0 +1,5 @@ +module N; + +import Stdlib.Prelude open; + +g (a : Nat) : Nat := a * 2; diff --git a/tests/positive/Isabelle/Program.juvix b/tests/positive/Isabelle/Program.juvix index 7e7db6324b..217bae8939 100644 --- a/tests/positive/Isabelle/Program.juvix +++ b/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; diff --git a/tests/positive/Isabelle/isabelle/M_Main.thy b/tests/positive/Isabelle/isabelle/M_Main.thy new file mode 100644 index 0000000000..2a6d0c82a8 --- /dev/null +++ b/tests/positive/Isabelle/isabelle/M_Main.thy @@ -0,0 +1,9 @@ +theory M_Main +imports Main + M_N +begin + +fun f :: "nat \ nat" where + "f a = (g a)" + +end diff --git a/tests/positive/Isabelle/isabelle/M_N.thy b/tests/positive/Isabelle/isabelle/M_N.thy new file mode 100644 index 0000000000..76d2300fbd --- /dev/null +++ b/tests/positive/Isabelle/isabelle/M_N.thy @@ -0,0 +1,8 @@ +theory M_N +imports Main +begin + +fun g :: "nat \ nat" where + "g a = (a + 1)" + +end diff --git a/tests/positive/Isabelle/isabelle/N.thy b/tests/positive/Isabelle/isabelle/N.thy new file mode 100644 index 0000000000..1e706f594a --- /dev/null +++ b/tests/positive/Isabelle/isabelle/N.thy @@ -0,0 +1,8 @@ +theory N +imports Main +begin + +fun g :: "nat \ nat" where + "g a = (a * 2)" + +end diff --git a/tests/positive/Isabelle/isabelle/Program.thy b/tests/positive/Isabelle/isabelle/Program.thy index 2d7324f431..fec5012e10 100644 --- a/tests/positive/Isabelle/isabelle/Program.thy +++ b/tests/positive/Isabelle/isabelle/Program.thy @@ -1,5 +1,8 @@ theory Program imports Main + N + M_N + M_Main begin definition id0 :: "nat \ nat" where @@ -25,7 +28,7 @@ fun f :: "nat \ nat \ nat \ nat" where "f x y z = ((z + 1) * x + y)" fun g :: "nat \ nat \ 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 \ nat" where "inc x = (Suc x)"