Add some basis support for refinements

[robsimmons]

This update adds "true" and "false" refinements, "some" and "none" refinements, and "conslist" refinements - adding "conslist" isn't too expensive, but in the L10 code additionally having a "nillist" was quite expensive, so I'm not putting that in this library.

[rowandavies]

Some good stuff there. I'll probably pull it later today.

I suspect 'a none will sometimes cause similar issues - it's highly dependent on what you instantiate the parameter too. And that means that a program that uses NONE with type "((bool -> bool) -> bool) Option" will be highly sensitive even to the innocent looking refinements of bool. Adding sort annotations will generally fix the issue, but this seems an unreasonable burden for those parts of the program that don't depend on the refinements.

(Hmmm - a tactic I just thought of: try checking opaquely sealed structures containing potentially expensive expressions like "NONE" without the defined refinements first.)

These efficiency issues may best be handled by letting the programmer select the set of refinements to include for each part of their program - so maybe what we want is a library of "mix and match" modules of refinement declarations so that (e.g.) nillist can be included, carefully, when it's actually needed. Doing this currently is difficult - datasort definitions are generative via SML style elaboration to "sort names" with scope extruded to "the rest of the program". (I'm going to have a look at how to improve this for some common situations.) Currently you can start from a clean basis by using a separate MLB file, and I may add an MLB annotation that similarly forces starting from scratch.

BTW, your CIDRE stubs that throw exceptions are "old school". :-) You probably saw it, but just in case the new style is to use the following STREXP:

   struct (*[ assumesig <SIGEXP> ]*)  <IGNORED_STRUCTDEC> end

For basis stubs, there's not much point having the IGNORED_STRUCTDEC, I generally just put:

   structure s = struct  (*[ assumesig S where etc=etc ]*)  end

It works fine for functors and inline signatures as well.

Cheers

• Rowan

On Tue, Oct 18, 2011 at 2:10 AM, Robert J. Simmons < reply@reply.github.com>wrote:

This update adds "true" and "false" refinements, "some" and "none" refinements, and "conslist" refinements - adding "conslist" isn't too expensive, but in the L10 code additionally having a "nillist" was quite expensive, so I'm not putting that in this library.

You can merge this Pull Request by running:

git pull https://github.com/robsimmons/sml-cidre master

Or you can view, comment on it, or merge it online at:

https://github.com/rowandavies/sml-cidre/pull/1

-- Commit Summary --

• Add 'refined basis' bits, might be totally bogus for the moment
• Actually run stuff

-- File Changes --

A lib/refined-basis/basis.mlb (4) A lib/refined-basis/bool.sml (2) A lib/refined-basis/intinf.sml (1) A lib/refined-basis/list.sml (68) A lib/refined-basis/option.sml (3)

-- Patch Links --

https://github.com/rowandavies/sml-cidre/pull/1.patch https://github.com/rowandavies/sml-cidre/pull/1.diff

Reply to this email directly or view it on GitHub: https://github.com/rowandavies/sml-cidre/pull/1

[robsimmons]

Okay - I was actually planning on replacing the exception-throwing code with real code to show that the implementation (or "an implementation") met the specification, since one of the ones I wrote was wrong (before I fixed it).

I previously had nillist and conslist, and that was indeed making certain code slow. I imagine you'll want not one refined basis but a family of refined bases that make different tradeoffs - one of the reason that GitHub's fork-modify-push cycle can be helpful! The question of how mix-and-match versus lots-of-monolithic refined bases this situation ends up is one I am happy to let you resolve as CIDRE's benevolent dictator.