After some experiments, I've finally solved this issue while keeping
generic types used in signatures. After comparing the two options:
functors taking structures and functions taking records, I decided to
revert to functors taking structures, because the signatures of the
structures gives me generic types, and this makes code much easier to
maintain (it's fine to use functions taking records if one don't care
generic types). I've tried two different ways, and I prefer the second one.
The first method is that inside a functor, I make a computation function
take and return records. For example, I have three structures: a program
P, a state A, and a computation C. Their relationship is as follows:
structure P = ProgramStruct;
structure A = StateFunctor(structure P = P);
structure C = ComputationFunctor(structure P = P and A = A);
Their computation functions are:
P.initProg: code_piece -> P_record
A.initState: P_record -> A_record
C.compute: (P_record, A_record) -> result
For example, the computation function--compute--in ComputationFunctor
takes a record of program and a record of state, which provides
necessary info for the computation. The problem is that the record types
have to be incorporated in the signatures of program and state structures.
I don't like the idea of placing data into signatures very much, so I
take another approach. A signature only has types and function values.
The structure of the signature has data values as "references." I use an
initialization function for each structure to set corresponding values,
and the computation functions in the functors do not take records
anymore. My code now become:
Outside the automation function, I declare structures:
structure P = ProgramStruct;
structure A = StateFunctor(structure P = P);
structure C = ComputationFunctor(structure P = P and A = A);
and inside the automation function, I call a function with the following
sequence again and again:
val _ = P.initProg(code);
val _ = A.initState();
val result = C.compute();
Some people may not like the idea of using references in functional
programming, but it gives a nicer interface in this case.
Cheers!
Lu
Lu Zhao wrote:
> 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
------------------------------------------------------------------------------
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
