From d60bcccffb65eb2d84d14871b8a19d0275e6cb6b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=C5=81ukasz=20Czajka?=
 <62751+lukaszcz@users.noreply.github.com>
Date: Wed, 14 Aug 2024 15:24:42 +0200
Subject: [PATCH] Isabelle/HOL name quoting (#2951)

* Closes #2941
* Depends on #2950
---
 .../Backend/Isabelle/Translation/FromTyped.hs | 44 ++++++++++++++++---
 tests/positive/Isabelle/Program.juvix         |  2 +-
 tests/positive/Isabelle/isabelle/Program.thy  | 10 ++---
 3 files changed, 43 insertions(+), 13 deletions(-)

diff --git a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
index c34872f7e3..7c66fc1c23 100644
--- a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
+++ b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
@@ -882,15 +882,45 @@ goModule onlyTypes infoTable Internal.Module {..} =
     names :: HashSet Text
     names =
       HashSet.fromList $
-        map (^. Internal.functionInfoName . namePretty) (filter (not . (^. Internal.functionInfoIsLocal)) (HashMap.elems (infoTable ^. Internal.infoFunctions)))
-          ++ map (^. Internal.constructorInfoName . namePretty) (HashMap.elems (infoTable ^. Internal.infoConstructors))
-          ++ map (^. Internal.inductiveInfoName . namePretty) (HashMap.elems (infoTable ^. Internal.infoInductives))
-          ++ map (^. Internal.axiomInfoDef . Internal.axiomName . namePretty) (HashMap.elems (infoTable ^. Internal.infoAxioms))
+        map quote $
+          map (^. Internal.functionInfoName . namePretty) (filter (not . (^. Internal.functionInfoIsLocal)) (HashMap.elems (infoTable ^. Internal.infoFunctions)))
+            ++ map (^. Internal.constructorInfoName . namePretty) (HashMap.elems (infoTable ^. Internal.infoConstructors))
+            ++ map (^. Internal.inductiveInfoName . namePretty) (HashMap.elems (infoTable ^. Internal.infoInductives))
+            ++ map (^. Internal.axiomInfoDef . Internal.axiomName . namePretty) (HashMap.elems (infoTable ^. Internal.infoAxioms))
 
     quote :: Text -> Text
-    quote txt = case Text.uncons txt of
-      Just (c, txt') | not (isLetter c) -> txt'
-      _ -> txt
+    quote = quote' . Text.filter isLatin1 . Text.filter (isLetter .||. isDigit .||. (== '_') .||. (== '\''))
+
+    quote' :: Text -> Text
+    quote' txt
+      | HashSet.member txt reservedNames = quote' (prime txt)
+      | txt == "_" = "v"
+      | otherwise = case Text.uncons txt of
+          Just (c, _) | not (isLetter c) -> quote' ("v_" <> txt)
+          _ -> case Text.unsnoc txt of
+            Just (_, c) | not (isAlphaNum c || c == '\'') -> quote' (txt <> "'")
+            _ -> txt
+
+    reservedNames :: HashSet Text
+    reservedNames =
+      HashSet.fromList
+        [ "begin",
+          "bool",
+          "case",
+          "else",
+          "end",
+          "if",
+          "imports",
+          "in",
+          "int",
+          "let",
+          "list",
+          "nat",
+          "of",
+          "option",
+          "theory",
+          "then"
+        ]
 
     filterTypeArgs :: Int -> Internal.Expression -> [a] -> [a]
     filterTypeArgs paramsNum ty args =
diff --git a/tests/positive/Isabelle/Program.juvix b/tests/positive/Isabelle/Program.juvix
index 973cd3eba3..69d15bdb4e 100644
--- a/tests/positive/Isabelle/Program.juvix
+++ b/tests/positive/Isabelle/Program.juvix
@@ -53,7 +53,7 @@ qfst : {A : Type} → Queue A → List A
   | (queue x _) := x;
 
 qsnd : {A : Type} → Queue A → List A
-  | (queue _ x) := x;
+  | (queue _ v) := v;
 
 pop_front {A} (q : Queue A) : Queue A :=
     let
diff --git a/tests/positive/Isabelle/isabelle/Program.thy b/tests/positive/Isabelle/isabelle/Program.thy
index 68d2f13efa..df548c13df 100644
--- a/tests/positive/Isabelle/isabelle/Program.thy
+++ b/tests/positive/Isabelle/isabelle/Program.thy
@@ -55,10 +55,10 @@ datatype 'A Queue
   = queue "'A list" "'A list"
 
 fun qfst :: "'A Queue \<Rightarrow> 'A list" where
-  "qfst (queue x ω) = x"
+  "qfst (queue x v) = x"
 
 fun qsnd :: "'A Queue \<Rightarrow> 'A list" where
-  "qsnd (queue ω x) = x"
+  "qsnd (queue v v') = v'"
 
 fun pop_front :: "'A Queue \<Rightarrow> 'A Queue" where
   "pop_front q =
@@ -66,7 +66,7 @@ fun pop_front :: "'A Queue \<Rightarrow> 'A Queue" where
        q' = queue (tl (qfst q)) (qsnd q)
      in case qfst q' of
           [] \<Rightarrow> queue (rev (qsnd q')) [] |
-          ω \<Rightarrow> q')"
+          v \<Rightarrow> q')"
 
 fun push_back :: "'A Queue \<Rightarrow> 'A \<Rightarrow> 'A Queue" where
   "push_back q x =
@@ -80,8 +80,8 @@ fun is_empty :: "'A Queue \<Rightarrow> bool" where
        [] \<Rightarrow>
          (case qsnd q of
             [] \<Rightarrow> True |
-            ω \<Rightarrow> False) |
-       ω \<Rightarrow> False)"
+            v \<Rightarrow> False) |
+       v \<Rightarrow> False)"
 
 definition empty :: "'A Queue" where
   "empty = queue [] []"