clone import as abstract

[AntoineSere]

In the following, when using clone import , the theory Bar end up not being abstract:

abstract theory Foo.
  type t.
end Foo.

clone import Foo as Bar.

print Foo.
print Bar.

Is there a way currently in EasyCrypt to modify this example to make Bar abstact? If not, I think it may be good to have.

[chdoc]

Not sure what you're trying to achieve here. The idea of cloning an abstract theory is to turn it into a concrete theory. If the surrounding theory is abstract, the inner theory should also be effectively abstract.

[fdupress]

I can't EasyCrypt at the moment, but I'm here. Does abstract clone Foo as Bar work?

Note that you can't import an abstract theory (because it doesn't exist until made concrete), so abstract clone import Foo as Bar would fail in any case.

[chdoc]

Both clone abstract and abstract clone are parse errors. However, if you want a second abstract copy of Foo named Bar, how about:

abstract theory Bar.
  clone include Foo.
end Bar.

As mentioned above, you cannot import things that do not (yet) exist.

[fdupress]

Thanks for checking @chdoc.

If this is something that is useful generally (most of our theories do end up being semi-concrete anyway, and abstract sub-theories of concrete theories are useful to hide proof gunk), we should certainly parse abstract clone Foo as Bar with ... as

abstract theory Bar.
  clone include Foo with ...
end Bar.

@AntoineSere can you point to the file and general location in your branch that would benefit from this?

[chdoc]

I think this is slightly more complex than just parsing. If you want with ... you probably also want proof and then you have interactive parts before the end Bar. Given that the overhead for doing things with current mechanisms is minimal, I'm not sure this is really needed.

[AntoineSere]

Thanks for checking @chdoc.

If this is something that is useful generally (most of our theories do end up being semi-concrete anyway, and abstract sub-theories of concrete theories are useful to hide proof gunk), we should certainly parse abstract clone Foo as Bar with ... as

abstract theory Bar.
  clone include Foo with ...
end Bar.

@AntoineSere can you point to the file and general location in your branch that would benefit from this?

To support you first point, there already is an example of an abstract theory inside another abstract theory in the main branch, in the theory/algebra/Ideal.ec: there is an abstract theory called IdealRing that describes what ideals of a commutative ring are and their properties, and you can find inside a theory called RingQuotient that describes the ring structure obtained when quotienting by a given ideal. You need the inner theory to be abstract in this case, because you want to provide a specific ideal to it to work.

As for where it could be useful in my branch theory_finite_field, it may be useful to clean up what I added to this same file, namely the other abstract theories IDomainQuotient and FieldQuotient that describe the cases where your quotient by an ideal ends up being an integral domain, or a field. These last two theories could, up to some refactoring, simply be an abstract clone.

But I agree with @chdoc that given the solution you propose, having such a thing is not top priority and we can get by with your proposed fix for now.

[chdoc]

Can we close this issue then?