Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Date: Thu, 21 Apr 94 9:19:20 EDT
From: reetz <reetz@ira.uka.de>
To: info-hol@cs.uidaho.edu
Subject: RE^2: overloaded constants
Message-Id: <"i80fs2.ira.764:21.03.94.07.19.26"@ira.uka.de>

> Answer of David Shepherd not repeated here...

I understand the parser runs into problems with
overloading :-( . However, I was able to build a term
with an overloaded variable and I didn't use
the parser to make an overloaded definition, but
it still failed. I again would like to point out
that overloaded variables ARE allowed, but 
overloaded constants are not. So then we don't
allow the definition of overloaded constants because
of possible parsing problems, why do we allow
overloaded variables?
I would also like to show an example where it
makes sense to have overloaded constants. The
example of David Sheperd shows one problem:
same represenations of values of different
types, namely the represenation of num/integer
by 1,2,3,... at the same time. That's a problem.
Well, addition for integer is defined as `plus'
and that solves it. But think of e.g. the
operation `xor' of VHDL. It works for booleans,
bits and one-dimensional arrays of booleans and
bits. Think of represenations `FALSE' and
`TRUE' for booleans, `L' and `H' for bits
and constants of the word library from W. Wong
as represenations for these one-dimensional arrays.
Then, writing e.g.

--`FALSE xor TRUE`--

--`L xor H`--

--`(WORD [FALSE]) xor (WORD[TRUE])`--

should not need additional typing and it
resembles to VHDL well. Of course, it's not
a problem do define `boolean_xor', `bit_xor'
and `array_xor'; or puting boolean, bit and word
together using type constructors `ABS_BOOLEAN',
`ABS_BIT', `ABS_ARRAY', but this leads to longer
and less readable terms, e.g.

--`FALSE boolean_xor TRUE`--

--`L bit_xor H`--

--`(WORD [FALSE]) array_xor (WORD[TRUE])`--

or

--`(ABS_BOOLEAN FALSE) xor (ABS_BOOLEAN TRUE)`--

--`(ABS_BIT L) xor (ABS_BIT H)`--

--`(ABS_ARRAY (WORD[FALSE])) xor (ABS_ARRAY (WORD[TRUE])--`

But that's clearly not as nice as overloading `xor'.
There doesn't seems to exist a quick and really nice-to-read
solution, but maybe some people programming hol might
like to consider this example as an argument to
consider overloading... ;-)

(*****************************************************************************)
(*                                                                           *)
(*  Ralf Reetz                            SFB 358 of the german research     *)
(*  reetz@ira.uka.de                      society (DFG)                      *)
(*  reetz@informatik.uni-karlsruhe.de     University of Karlsruhe, Germany   *)
(*                                                                           *)
(*****************************************************************************)