LINUX.ORG.RU
Форум — Development  

Idris & Unicode

 ,


0

3

Что то не пойму, как принтер в репле Идриса заставить отображать юникодные символы и строки, что в емаксе (*idris-repl*), что в репле:

$ locale
LANG="en_US.UTF-8"
LC_COLLATE="en_US.UTF-8"
LC_CTYPE="en_US.UTF-8"
LC_MESSAGES="en_US.UTF-8"
LC_MONETARY="en_US.UTF-8"
LC_NUMERIC="en_US.UTF-8"
LC_TIME="en_US.UTF-8"
LC_ALL="en_US.UTF-8"

$ idris
     ____    __     _                                          
    /  _/___/ /____(_)____                                     
    / // __  / ___/ / ___/     Version 1.1.1
  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/      
 /___/\__,_/_/  /_/____/       Type :? for help               

Idris is free software with ABSOLUTELY NO WARRANTY.            
For details type :warranty.

Idris> ("Привет ЛОР!", 'λ')
("\1055\1088\1080\1074\1077\1090 \1051\1054\1056!", '\955') : (String, Char)

Что подкрутить?

← Суицидальная тема в Spring Boot
Не отображает список →

Хмм, в GHCi тоже также. Это баг или фича? И если не баг, то почему по-человечески не пeчатать юникодную строку?

mimimimi
() автор топика

Ну, да! Прикольно

$ ghci
GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
Prelude> s = "Привет!"
Prelude> s
"\1055\1088\1080\1074\1077\1090!"
Prelude> show s
"\"\\1055\\1088\\1080\\1074\\1077\\1090!\""
Prelude> print s
"\1055\1088\1080\1074\1077\1090!"
Prelude> :t s
s :: [Char]
Prelude> putStrLn s
Привет!
Prelude>
dave ★★★★★
()
Ответ на: комментарий от dave

Возможно, что интерпретатор Идриса использует хаскеллевские примитивы для IO, отсюда и одинаковый вывод.

mimimimi
() автор топика
Ответ на: комментарий от mimimimi

В том же CL сделано по-человечески: 

sbcl
This is SBCL 1.4.2, an implementation of ANSI Common Lisp.
More information about SBCL is available at <http://www.sbcl.org/>.

SBCL is free software, provided as is, with absolutely no warranty.
It is mostly in the public domain; some portions are provided under
BSD-style licenses.  See the CREDITS and COPYING files in the
distribution for more information.
* (cons "Привет ЛОР!" #\λ)

("Привет ЛОР!" . #\GREEK_SMALL_LETTER_LAMDA)
* (princ *)
(Привет ЛОР! . λ)
("Привет ЛОР!" . #\GREEK_SMALL_LETTER_LAMDA)
*

mimimimi
() автор топика

Стандартный show для Char использует только некие printable characters, экранируя всё, что им не является. К счастью, у GHCi есть возможность указать свою собственную функцию для отображения значений:

> let myPrint v = putStrLn ("lol: " <> show v)
> :set -interactive-print=myPrint
> 42
lol: 42


Также есть пакет unicode-show, который решает именно озвученную проблему:

[quote] import qualified Text.Show.Unicode[br] :set -interactive-print=Text.Show.Unicode.uprint[br] ("Привет ЛОР!", 'λ')[br][/quote]("Привет ЛОР!",'λ')


Идрис, по всей видимости, сделан так же, как и хаскель, но про interactive-print в идрисе ничего сказать не могу.

Laz ★★★★★
()
Ответ на: комментарий от mimimimi

В том же CL сделано по-человечески

Осталось зделать человеческий синтаксис.

anonymous
()
Ответ на: комментарий от Laz

Как то так, но ИМХО это костыли:

Idris> :let v = ("Привет ЛОР!", 'λ')
Idris> :x putStrLn (fst v)
Привет ЛОР!
MkIO (\w => prim_io_pure ()) : IO' (MkFFI C_Types String String)
                                   ()
Idris> :x putChar (snd v)
λMkIO (\w => prim__IO _ ()) : IO' (MkFFI C_Types String String)
                                 ()
Idris> :x putStrLn (show v)
("\1055\1088\1080\1074\1077\1090 \1051\1054\1056!", '\955')
MkIO (\w => prim_io_pure ()) : IO' (MkFFI C_Types String String)
                                   ()

Для проверки хватит, но нет мощи лиспового репла. И только выборочно печать строки или символы.

mimimimi
() автор топика

Хм, а в Agda всё нормально с unicode 

module HelloWorld where

open import IO 

main = putStr "Привет, мир!"

.IO.♯-16
('П' .Data.Colist.Colist.∷
 .Data.Colist.♯-2 'П'
 ('р' .Agda.Builtin.List.List.∷
  'и' .Agda.Builtin.List.List.∷
  'в' .Agda.Builtin.List.List.∷
  'е' .Agda.Builtin.List.List.∷
  'т' .Agda.Builtin.List.List.∷
  ',' .Agda.Builtin.List.List.∷
  ' ' .Agda.Builtin.List.List.∷
  'м' .Agda.Builtin.List.List.∷
  'и' .Agda.Builtin.List.List.∷
  'р' .Agda.Builtin.List.List.∷
  '!' .Agda.Builtin.List.List.∷ .Agda.Builtin.List.List.[]))

Unununij ★★★★
()
Последнее исправление: Unununij (всего исправлений: 1)
Вы не можете добавлять комментарии в эту тему. Тема перемещена в архив.
← Суицидальная тема в Spring Boot
Development
Не отображает список →