Rework stdlib clones.

[strub]

No description provided.

[vbgl]

I can confirm that in this branch, it is possible to clone and use the PolyReduce.PolyReduce. Any chance to get it merged in the main branch?

Note that what I expected to be able to write was:

clone import PolyReduce.PolyReduce as P with
type coeff <= int,
theory Coeff <= Ring.IntID,
op n <- 256.

But that failed with

unknown symbol: Top.Ring.IntID.t

Workaround was to define my own IntID theory using

clone include Ring.IDomain with
  type t <= int,

when Ring.ec reads:

clone include IDomain with
  type t <- int,

[fdupress]

I didn't review this because it was still draft, but happy to do so after it's rebased.

As a side note, given what we now know about how cloning works (and doesn't), perhaps it's time to emit a warning when the user clones a theory that does not contain modules and uses <- to instantiate things? (It would certainly help review this for thoroughness of the replacement.)

We could also (later) have a [final] option on clones, that deactivates the warning but prevents further instantiation—with a more meaningful error message than that currently emitted.

[strub]

I can confirm that in this branch, it is possible to clone and use the PolyReduce.PolyReduce. Any chance to get it merged in the main branch?

Note that what I expected to be able to write was:

clone import PolyReduce.PolyReduce as P with
type coeff <= int,
theory Coeff <= Ring.IntID,
op n <- 256.

But that failed with

unknown symbol: Top.Ring.IntID.t

Workaround was to define my own IntID theory using

clone include Ring.IDomain with
  type t <= int,

when Ring.ec reads:

clone include IDomain with
  type t <- int,

IMO, that's a mistake a IntID to remove the t type definition.

[strub]

Merging. Not perfect but will continue working in a different PR.