[Agda] Unicode in Standard Library

[Nils Anders Danielsson]

On Feb 12, 2008 10:27 AM, Andrés Sicard-Ramírez <andres.sicard at gmail.com> wrote:
>
> On 12/02/2008, Andreas Abel <abel at cs.chalmers.se> wrote:
> >
> > the new standard library seems quite nice, with ambitious use of unicode
> > characters.  My tiny problem is:  how can I use it when I have no key
> > for ℕ on my keyboard?
>
> I had the same tiny problem some weeks ago and this was the Nils's answer:
> >
> > Either you can modify the TeX input method so that it handles these
> > characters (see the Agda README file), or you can use C-u C-x = with
> > another input method active (for instance ucs or rfc1345) to see how
> > to enter the characters using that method. A third option is to find
> > the Unicode code point for the character (listed as U+XXXX) and enter
> > the character using M-x ucs-insert.

This is taken slightly out of context; I was explaining how one can
write Unicode characters which do not already have a suitable
keybinding in the TeX input method.

One approach for finding out how to write a character is the
following:

⑴ Position the cursor over the character, press C-u C-x =. For
  instance, for ℕ I get the following:

      character: ℕ (342741, #o1235325, #x53ad5, U+2115)
        charset: mule-unicode-0100-24ff (Unicode characters of the
range U+0100..U+24FF.)
     code point: #x75 #x55
         syntax: w 	which means: word
       to input: type "\N" or "\Bbb{N}" with TeX
    buffer code: #x9C #xF4 #xF5 #xD5
      file code: #xE2 #x84 #x95 (encoded by coding system mule-utf-8-unix)
        display: by this font (glyph code)
         -Misc-Fixed-Medium-R-Normal--15-140-75-75-C-90-ISO10646-1 (#x2115)

  Here it says that I can type \N or \Bbb{N} with the TeX input
  method. (I have defined the \N binding myself, since the other one
  is a bit long-winded for a character I type rather often.)

⑵ If there is no "to input" line (which may be the case with Oxford
  brackets, ⟦⟧, for instance), then you can try using C-u C-x = with
  other input methods. For instance, you may find that you prefer the
  rfc1345 input method. However, this input method also lacks a
  binding for Oxford brackets.

⑶ If there is no suitable binding, and you don't want to type in the
  Unicode code point manually, then you can update your favourite
  input method with a new binding. For instance, to add Oxford
  brackets to the TeX input method, written using their LaTeX command
  names, put the following in your .emacs:

    (mapc (lambda (pair)
            (quail-defrule (car pair) (cadr pair) "TeX"))
       '(("\\llbracket" "⟦")
         ("\\rrbracket" "⟧")))

  You can add more bindings in the obvious way.

We have thought about creating an input method targeted specifically
at Agda, but have not done it yet. One reason is that names that are
easy to remember are often long, and therefore inefficient to type. I
want to have short mnemonics for frequently occurring characters, but
I don't expect others to want to learn the mnemonics I've chosen.

However, if someone else wants to design an Agda-specific input
method, largely based on the TeX input method, that would be great.
Some notes:

* The TeX input method code is most likely GPL-ed, so if you base your
  work on it, don't put a copy in the Agda source repository without
  further discussion.

* The binding for -- in the TeX input method (–) is annoying; two
  dashes should start a comment. It might be a good idea to let _all_
  special bindings start with a (configurable?) prefix character.

As an alternative to defining an input method it is also possible to
define a list of "abbrevs" for Agda. An abbrev list is basically a
finite map from abbreviations to expanded words; in our case it might
be the other way around, though. Example:

  Nat       ⟶ ℕ
  llbracket ⟶ ⟦
            ⋮

An abbrev is expanded by typing a key combination with the cursor to
the right of the abbreviation. This has the advantage that it does not
matter if you make a small mistake when typing the abbreviation; with
the TeX input method small mistakes often force you to start typing
the abbreviation from scratch again.

There are some issues with abbrevs:

○ What should happen if you type CoNat? (If you want Coℕ you have to
  type some key combination after Co.)

○ I think that only "word characters" can make up an abbreviation.
  This can be worked around, though, if necessary.

I believe that using abbrevs may actually be more convenient for us;
assuming that someone takes care of setting up the abbreviation table.

-- 
/NAD