Re: [open-axiom-help] PropositionalFormula and CCC

[Gabriel D. R. <gd...@cs...>]

Martin Baker <ax...@ma...> writes:

| On Sunday 23 Oct 2011 17:13:32 Gabriel Dos Reis wrote:
| > The operation 'constructor' does what its documentation says:
| > 
| >       ++ constructor(d) returns the domain constructor that is
| >       ++ instantiated to the domain object `d'.
| > 
| > Similarly, `reflect' does what its documentation says:
| > 
| >       ++ reify(d) returns the abstract syntax for the domain `x'.
| > 
| > Similarly, the operation `reflect' does what its documentation says:
| > 
| >       ++ reflect cc returns the domain object designated by the
| >       ++ ConstructorCall syntax `cc'.  The constructor implied
| >       ++ by `cc' must be known to the system since it is instantiated.
| > 
| > Similarly, the operation `showSummary' does what its documentation says:
| > 
| >       ++ showSummary(d) prints out implementation detail information
| >       ++ of domain `d'.
| 
| Is it just me?

You left out a good part of the explanation germane to this discussion.

If you need my help for something specific, tell me. If it is something
else, I do not what it is.

| Would anyone else like to look at:
| 
| http://svn.open-axiom.org/viewvc/open-
| axiom/1.4.x/src/algebra/domain.spad.pamphlet?revision=2347&view=markup
| 
| and say whether they would like to use/maintain/extend this code?

 1. If you want to extend that domain, you would need to understand how
    the AXIOM runtime system works, especially the domain as object part. 
    I provided a great deal of references and explanation in my previous
    message.  Since you are specific about the extension you want, I am
    not sure you took my advice (from previous message) seriously.

 2.  If you want to maintain that domain, see 1.

 3.  Now, we are left with "use".  Specifically what do you want to use
     it for?  You have not been very specific.

I had a sense that you wanted help, but now I am not sure you just
wanted to vent something else.  There is no point in complaining in way
that puts off people who want to help you.

-- Gaby