At present, Felix doesn't have a builtin boolean type.
However it does have a builtin tuple and sum combinator,
and we can define bool internally by:
bool = sum [ tuple[]; tuple []]
Bool therefore uses the representation at run time
that the above sum uses, which is carefully defined to
make it an int. [Interestingly g++ seems to use 1 byte int,
this hasn't cause any problems yet]
But now I have example which say this:
[EMAIL PROTECTED]:/work/felix/svn/felix/felix/trunk$ f tc
[flx_why] Can't find logic function 'lnot'
WARNING: flx_why cannot find 'lnot'
[flx_why] Can't find logic function 'eq'
WARNING: flx_why cannot find 'eq'
[flx_why] Can't find logic function 'implies'
WARNING: flx_why cannot find 'implies'
[flx_why] Can't find logic function 'lor'
WARNING: flx_why cannot find 'lor'
[flx_why] Can't find logic function 'land'
WARNING: flx_why cannot find 'land'
1
This is because the Why obligation generator needs to know
the symbol index of these logic functions for pattern
matching purposes, because it operates on bound code
(that is, free of string names). These functions are
defined by C++ in the library eg:
fun land: bool * bool -> bool = "$1&&$2";
so the integer index of 'land' is not known in advance.
This hackery is sometimes needed for other types, in particular
any type for which there is a literal used (eg 1, "Hello" etc).
Even though the literals are builtin to the compiler .. their
types are not: the library must supply an appropriate definition.
OK, now for bool it is a pain, because simple laws of logic
aren't known by the compiler, for example
not (not x) = x
can be specified in the library and used to do reductions,
but the compiler can't perform these operations.
Rather than define specific combinators like not, and, or, implies,
it would be nice to repeat the generic trick used for types,
and define something like 'finite_function' combinator. For example:
finite_function [
tuple [true; true], true;
tuple [true; false], false;
..
]
could be used to represent logical and. Note this is a
literal value of type
bool * bool -> bool
With this in place we could reduce:
goto label
if cond goto label
ifnot cond goto lable
which are currently 3 distinct instructions. Furthermore we
might actually be able to calculate constant arguments
which at present have to be deferred to run time.
For that reason most compilers treat bool as a builtin type
with known operations .. but that sucks, because it isn't
really general enough.
--
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net
-------------------------------------------------------------------------
This SF.net email is sponsored by DB2 Express
Download DB2 Express C - the FREE version of DB2 express and take
control of your XML. No limits. Just data. Click to get it now.
http://sourceforge.net/powerbar/db2/
_______________________________________________
Felix-language mailing list
Felix-language@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/felix-language
