Remove unicode from Isabelle/HOL output (#2950)

* Closes #2942

juvix-stdlib

@@ -1 +1 @@
-Subproject commit 5424a487b4ca20f94c108ef4c41acf5dcc575fd0
+Subproject commit 30e42ac73eace577be93d5200a0bec156abe2c69

src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs

@@ -7,7 +7,7 @@ import Juvix.Compiler.Backend.Isabelle.Pretty.Options
 import Juvix.Data.CodeAnn
 
 arrow :: Doc Ann
-arrow = "⇒"
+arrow = "\\<Rightarrow>"
 
 class PrettyCode c where
   ppCode :: (Member (Reader Options) r) => c -> Sem r (Doc Ann)
@@ -58,7 +58,7 @@ instance PrettyCode Inductive where
     IndList -> return $ primitive "list"
     IndString -> return $ primitive "string"
     IndOption -> return $ primitive "option"
-    IndTuple -> return $ primitive "×"
+    IndTuple -> return $ primitive "\\<times>"
     IndUser name -> ppCode name
 
 instance PrettyCode IndApp where
@@ -178,7 +178,7 @@ instance PrettyCode Lambda where
     mty <- maybe (return Nothing) (ppCode >=> return . Just) _lambdaType
     body <- ppCode _lambdaBody
     let ty = fmap (\t -> colon <> colon <+> t) mty
-    return $ kwLambda <+> name <+?> ty <+> dot <+> body
+    return $ "\\<lambda>" <+> name <+?> ty <+> dot <+> body
 
 instance PrettyCode Statement where
   ppCode = \case

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

@@ -503,10 +503,10 @@ goModule onlyTypes infoTable Internal.Module {..} =
                 case funInfo ^. Internal.functionInfoBuiltin of
                   Just Internal.BuiltinBoolAnd
                     | (arg1 :| [arg2]) <- args ->
-                        Just (defaultName "∧", andFixity, arg1, arg2)
+                        Just (defaultName "\\<and>", andFixity, arg1, arg2)
                   Just Internal.BuiltinBoolOr
                     | (arg1 :| [arg2]) <- args ->
-                        Just (defaultName "∨", orFixity, arg1, arg2)
+                        Just (defaultName "\\<or>", orFixity, arg1, arg2)
                   _ -> Nothing
               Nothing -> Nothing
           _ -> Nothing

tests/positive/Isabelle/Program.juvix

@@ -95,3 +95,9 @@ type R := mkR {
   r1 : Nat;
   r2 : Nat;
 };
+
+-- Standard library
+
+bf (b1 b2 : Bool) : Bool := not (b1 && b2);
+
+nf (n1 n2 : Int) : Bool := n1 - n2 >= n1 || n2 <= n1 + n2;

tests/positive/Isabelle/isabelle/Program.thy

@@ -2,97 +2,97 @@ theory Program
 imports Main
 begin
 
-definition id0 :: "nat ⇒ nat" where
+definition id0 :: "nat \<Rightarrow> nat" where
   "id0 = id"
 
-definition id1 :: "nat list ⇒ nat list" where
+definition id1 :: "nat list \<Rightarrow> nat list" where
   "id1 = id"
 
-definition id2 :: "'A ⇒ 'A" where
+definition id2 :: "'A \<Rightarrow> 'A" where
   "id2 = id"
 
-fun add_one :: "nat list ⇒ nat list" where
+fun add_one :: "nat list \<Rightarrow> nat list" where
   "add_one [] = []" |
   "add_one (x # xs) = ((x + 1) # add_one xs)"
 
-fun sum :: "nat list ⇒ nat" where
+fun sum :: "nat list \<Rightarrow> nat" where
   "sum [] = 0" |
   "sum (x # xs) = (x + sum xs)"
 
-fun f :: "nat ⇒ nat ⇒ nat ⇒ nat" where
+fun f :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where
   "f x y z = ((z + 1) * x + y)"
 
-fun g :: "nat ⇒ nat ⇒ bool" where
+fun g :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
   "g x y = (if x = y then False else True)"
 
-fun inc :: "nat ⇒ nat" where
+fun inc :: "nat \<Rightarrow> nat" where
   "inc x = (Suc x)"
 
-fun dec :: "nat ⇒ nat" where
+fun dec :: "nat \<Rightarrow> nat" where
   "dec 0 = 0" |
   "dec (Suc x) = x"
 
-fun dec' :: "nat ⇒ nat" where
+fun dec' :: "nat \<Rightarrow> nat" where
   "dec' x =
     (case x of
-       0 ⇒ 0 |
-       (Suc y) ⇒ y)"
+       0 \<Rightarrow> 0 |
+       (Suc y) \<Rightarrow> y)"
 
-fun optmap :: "('A ⇒ 'A) ⇒ 'A option ⇒ 'A option" where
+fun optmap :: "('A \<Rightarrow> 'A) \<Rightarrow> 'A option \<Rightarrow> 'A option" where
   "optmap f' None = None" |
   "optmap f' (Some x) = (Some (f' x))"
 
-fun pboth :: "('A ⇒ 'A') ⇒ ('B ⇒ 'B') ⇒ 'A × 'B ⇒ 'A' × 'B'" where
+fun pboth :: "('A \<Rightarrow> 'A') \<Rightarrow> ('B \<Rightarrow> 'B') \<Rightarrow> 'A \<times> 'B \<Rightarrow> 'A' \<times> 'B'" where
   "pboth f' g' (x, y) = (f' x, g' y)"
 
-fun bool_fun :: "bool ⇒ bool ⇒ bool ⇒ bool" where
-  "bool_fun x y z = (x ∧ (y ∨ z))"
+fun bool_fun :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool" where
+  "bool_fun x y z = (x \<and> (y \<or> z))"
 
-fun bool_fun' :: "bool ⇒ bool ⇒ bool ⇒ bool" where
-  "bool_fun' x y z = (x ∧ y ∨ z)"
+fun bool_fun' :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool" where
+  "bool_fun' x y z = (x \<and> y \<or> z)"
 
 datatype 'A Queue
   = queue "'A list" "'A list"
 
-fun qfst :: "'A Queue ⇒ 'A list" where
+fun qfst :: "'A Queue \<Rightarrow> 'A list" where
   "qfst (queue x ω) = x"
 
-fun qsnd :: "'A Queue ⇒ 'A list" where
+fun qsnd :: "'A Queue \<Rightarrow> 'A list" where
   "qsnd (queue ω x) = x"
 
-fun pop_front :: "'A Queue ⇒ 'A Queue" where
+fun pop_front :: "'A Queue \<Rightarrow> 'A Queue" where
   "pop_front q =
     (let
        q' = queue (tl (qfst q)) (qsnd q)
      in case qfst q' of
-          [] ⇒ queue (rev (qsnd q')) [] |
-          ω ⇒ q')"
+          [] \<Rightarrow> queue (rev (qsnd q')) [] |
+          ω \<Rightarrow> q')"
 
-fun push_back :: "'A Queue ⇒ 'A ⇒ 'A Queue" where
+fun push_back :: "'A Queue \<Rightarrow> 'A \<Rightarrow> 'A Queue" where
   "push_back q x =
     (case qfst q of
-       [] ⇒ queue [x] (qsnd q) |
-       q' ⇒ queue q' (x # qsnd q))"
+       [] \<Rightarrow> queue [x] (qsnd q) |
+       q' \<Rightarrow> queue q' (x # qsnd q))"
 
-fun is_empty :: "'A Queue ⇒ bool" where
+fun is_empty :: "'A Queue \<Rightarrow> bool" where
   "is_empty q =
     (case qfst q of
-       [] ⇒
+       [] \<Rightarrow>
          (case qsnd q of
-            [] ⇒ True |
-            ω ⇒ False) |
-       ω ⇒ False)"
+            [] \<Rightarrow> True |
+            ω \<Rightarrow> False) |
+       ω \<Rightarrow> False)"
 
 definition empty :: "'A Queue" where
   "empty = queue [] []"
 
-fun funkcja :: "nat ⇒ nat" where
+fun funkcja :: "nat \<Rightarrow> nat" where
   "funkcja n =
     (let
        nat1 = 1;
        nat2 = 2;
-       plusOne = λ x0 . case x0 of
-                          n' ⇒ n' + 1
+       plusOne = \<lambda> x0 . case x0 of
+                                  n' \<Rightarrow> n' + 1
      in plusOne n + nat1 + nat2)"
 
 datatype ('A, 'B) Either'
@@ -103,10 +103,16 @@ record R =
   r1 :: nat
   r2 :: nat
 
-fun r1 :: "R ⇒ nat" where
+fun r1 :: "R \<Rightarrow> nat" where
   "r1 (mkR r1' r2') = r1'"
 
-fun r2 :: "R ⇒ nat" where
+fun r2 :: "R \<Rightarrow> nat" where
   "r2 (mkR r1' r2') = r2'"
 
+fun bf :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
+  "bf b1 b2 = (\<not> (b1 \<and> b2))"
+
+fun nf :: "int \<Rightarrow> int \<Rightarrow> bool" where
+  "nf n1 n2 = (n1 - n2 \<ge> n1 \<or> n2 \<le> n1 + n2)"
+
 end