Michael Norrish wrote:
> On 14/02/11 04:38, Lu Zhao wrote:
>
>> I wrote an SML functor to facilitate some proof automation. I have
>> several proof cases. For each case, I create a structure from the
>> functor and use the structure to prove the case. This seems fine until I
>> try to automate the entire process for the several cases. Since I need
>> to create a separate structure for each case, SML doesn't allow me to
>> create a structure inside a function. In addition, the number of cases
>> varies, and I need to create the structures dynamically. Is there a way
>> to solve this problem?
>
> It may not be possible depending on how clever your use of functors is,
> but in many cases, you should be able to convert a functor into a
> function that takes a record of functions as arguments.
>
> In the HOL sources, compare
>
> src/num/arith/src/GenPolyCanon.{sig,sml} (* function taking a record *)
>
> and
>
> src/num/arith/src/GenRelNorm.sml (* functor taking a struct *)
>
> Michael
I'm converting my functor taking structures to functions taking records,
but doing so I've lost the ability of using an
abstract type in a signature passed into the functor. For a function
with some generic computation (previously a functor taking a signature
with types), I can't use a generic type. For each concrete type, I have
to create a concrete record for that type and duplicate the entire
function. Is there a way to keep the type generality inside a signature
while using (functions taking) records?
Thanks.
Lu
------------------------------------------------------------------------------
The ultimate all-in-one performance toolkit: Intel(R) Parallel Studio XE:
Pinpoint memory and threading errors before they happen.
Find and fix more than 250 security defects in the development cycle.
Locate bottlenecks in serial and parallel code that limit performance.
http://p.sf.net/sfu/intel-dev2devfeb
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
