Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
To: chou@edu.ucla.cs
Cc: info-hol@edu.uidaho.cs.ted
Subject: Re: [] problem
In-Reply-To: Your message of Sat, 28 Mar 92 22:55:30 -0800. <9203290655.AA09438@maui.cs.ucla.edu>
Date: Sun, 29 Mar 92 17:34:38 +0100
From: John Harrison <John.Harrison@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.379:29.02.92.16.34.44"@cl.cam.ac.uk>


chou@edu.ucla.cs (Ching Tsun) asks about:

> #[] ;;
> [] : * list
>
> #[ ] ;;
> [] : * list
>
> #new_special_symbol `[]` ;;
> () : void
>
> #[] ;;
>
> unbound or non-assignable variable []
> 1 error in typing
> typecheck failed

This is because the "new_special_symbol" call affects both term parsing *and*
ML parsing. For example, continuing your session, the following works:

+ #let [] = 2;;
+ [] = 2 : int
+
+ #[];;
+ 2 : int

Maybe the dual role is a bit unfortunate.

> Also, how to make HOL print the empty list as NIL instead of []
> in quotations after I have defined [] to be something else?
> Set_interface_map doesn't work:
>
> #set_interface_map [(`NIL`, `[]`)] ;;
> evaluation failed     NIL would become hidden

As the error message suggests, you aren't allowed to hide an existing constant.
However all you need to do is provide an arbitrary name not already used for a
constant name, viz:

+ #new_definition(`two`,"[] = 2");;
+ |- [] = 2
+
+ #set_interface_map [(`arbitrary_name`,`NIL`); (`NIL`, `[]`)] ;;
+ [] : (string # string) list

However this doesn't fix the printing problem. I think this is owing to the
fact that "[]" does not really exist as a constant (prior to the above
definition); it's purely a parsing and printing interface itself, though of
a special kind. For example, with no interface map set up:

+ #"[]:(*)list";;
+ "[]" : term
+
+ #dest_const it;;
+ (`NIL`, ":(*)list") : (string # type)

There's a similar problem about being unable to use numerals in an interface
map. Perhaps someone more knowledgeable will be able to suggest a way round
the problem.

John.