On Sun, Jul 10, 2022 at 09:59:12AM +0100, Paul Onions wrote:
> Hi Waldek,
>
> On 22 Jun 2022, at 09:10, Waldek Hebisch <[email protected]>
> wrote:
> >
> > Well, primary info is in domain vectors. For fully specified domain
> > one can view it using routines in 'showimp.boot', for example using
> >
> > )boot showSummary(FreeModule(Integer(), Symbol()))
>
> I’d like to be able to invoke the showImp boot function from Frimacs by
> passing a fully specified domain name that the user supplies. However, the
> problem I have is that showImp, like your showSummary example above, expects
> empty trailing parenthesis on parameter-less domain names. This is rather
> unnatural for a user to do — it’s not natural SPAD code.
>
> I think there must be some existing boot code somewhere that will help me
> parse a SPAD-like type expression and convert it into something that showImp
> would accept, but I’m having trouble finding such a thing.
>
> I considered doing it myself in elisp, but I expect there are corner cases to
> consider.
>
> Is it possible for you to point me in the right direction?
Well, 'postAtom' in 'postpar.boot' has as last two lines:
IDENTP x and GETDATABASE(x,'NILADIC) => LIST x
x
ATM valid type expression is always Lisp list. Wrapping
non-types in list would mangle values. The code above
essentialy makes parameterless constructor names reserved:
if symbol names a parameterless constructor constructor
(this is what GETDATABASE(x,'NILADIC) is checking) it
will be wrapped in list.
However, 'showSummary' really expects a Spad type. In
my example type expression works because arguments
are evaluated by Boot before calling 'showSummary'.
'showSummary' will work with many unevaluated type
expressions but using it in such way really is abuse
and will fail in corner cases.
At Spad level one could do:
show_imp_summary(t : Type) : Void == showSummary(t)$Lisp
(wrapping it in appropriate package).
Big (and still not full resolved) trouble with type
expressions is that there may be type errors inside
type expression. So we can not depend on type
expression being well-formed and we can not use
normal type rules to exclude wrong stuff.
Related trouble is that Boot code in several
places passes junk to various routines. Due
to small number of checks junk goes trough
and in simple cases look "working". But there
a lot of work to make our type machinery
really robust.
Anyway, once you have type, it passed all checks
that we have so you can be resonably confident
that type is correct (there are known bugs in
corner cases). With type expression all this
work to check type is before you. You could
probably cop out and use interpreter to evaluate
types, but ATM there are some traps, interpreter
is handling types slightly different than Spad
compiler (and our runtime system).
--
Waldek Hebisch
--
You received this message because you are subscribed to the Google Groups
"FriCAS - computer algebra system" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/fricas-devel/20220710132822.GA17439%40fricas.math.uni.wroc.pl.
