Mark, Yuhui,
On Feb 22, 2013, at 12:47 PM, "Mark" wrote:
> That's because ProofPower overwrites PolyML's ML structure List with its
> own, for holding theory about HOL lists. I'm not sure if anything can be
> done about this without alterning the ProofPower build process (and, say,
> creating a copy of PolyML's List with a name not used by ProofPower).
>
This is something we (i.e., me, Phil and, I would imagine, a certain Mark now
of Proof Technologies!) did think about. See below:
> Mark.
>
> on 22/2/13 12:33 PM, Yuhui Lin wrote:
>
>> Hi,
>>
>> I'm trying to build a programme on the top of proof power with the pp
>> interface. I need a full polyML library from the pp interface, but I can't
>> use some functions which are defined in polyML, e.g List.exists. Any
>> suggestion ?
>>
>> Thanks in advance.
>>
ProofPower was written long before the Standard Basis Library existed.
Unfortunately, some of the structure names used in ProofPower overwrite
structures in the Standard Basis Library. In this case, List in ProofPower is
the structure containing ML bindings relating to the theory of lists.
Many of the Standard Basis Library functions are available in ProofPower's own
library of ML utilities. See Chapters 2 and 3 of the HOL or Z Reference Manuals
(usr029 or usr030). There is an equivalent for List.exists called "any"
(actually ListUtilities.any, but the structure ListUtilities has been opened
for you).
ProofPower also provides a structure called SML97BasisLibrary that contains all
the Standard Basis Library structures. So you can get at List.exists as
SML97BasisLibrary.List.exists as an alternative to ListUtilities.any and you
can also get at things like List.tabulate that don't have any analogue in the
ProofPower utilities.
For future reference, you may need to be aware that most of the ProofPower ML
code that deals with strings is based on the SML'90 treatment of strings
whereby characters are handled as strings of length 1 rather than as a
separate type. Moving to the SML-97 way of handling strings throughout is a
change I am considering.
Regards,
Rob.
>> best,
>> Yuhui
>> --
>> The University of Edinburgh is a charitable body, registered in
>> Scotland, with registration number SC005336.
>>
>> ___
>> Proofpower mailing list
>> Proofpower@lemma-one.com
>> http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
>>
>>
>>
>
> ___
> Proofpower mailing list
> Proofpower@lemma-one.com
> http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
