Rework `CTerm` initializer

[tothtamas28]

Instead of taking a KInner, it should be:

def __init__(self, config: KInner, constraints: Iterable[KInner] = ()) -> None:
    check_config(config)
    constraints = self._normalize_constraints(constraints)
    object.__setattr__(self, 'config', config)
    object.__setattr__(self, 'constraints', constraints)

and

@staticmethod
def from_term(term: KInner) -> 'CTerm':
    config, constraint = split_config_and_constraints(term)
    return CTerm(config, constraints)

Edit: added implementation of from_term for unambiguity.

Rationale

CTerm is often instantiated as

CTerm(mlAnd([config] + constraints))

[ehildenb]

I would like to maintain the original functionality too though, because it's convenient to pass in the entire kinner that we get, and have it handle splitting the config and constraints.

So maybe we could do this, but continue to call split_config_and_constraints on the config portion, and move the constarints over to the list. It allows for both patters, where you pass in the entire constrained term as a single KInner, or where you have additional constraints you want to pass in.

[tothtamas28]

I would like to maintain the original functionality too

The original functionality would be maintained as

@staticmethod
def from_term(term: KInner) -> 'CTerm':
    ...

So maybe we could do this, but continue to call split_config_and_constraints on the config portion, and move the constarints over to the list.

I think that would cause confusion, the two ways of initialization are quite different (one is constructing, other is deconstructing). It's also more readable to be explicit.

This issue suggests a breaking change, but we can introduce it in two steps:

1. def __init__(self, config: KInner, constraints: Iterable[KInner])
2. def __init__(self, config: KInner, constraints: Iterable[KInner] = ())

The point is that step 1 causes type errors downstreams, which makes it easy to change CTerm(term) to from_term(term).

[ehildenb]

What's wrong with just calling split_config_and_constraints on the config though? And also, in your signature, what's to stop someone from calling CTerm(config) with a config that contains constraints? Would we add an extra check?

I also want to introduce split_subst_and_constraints(...) for use in CSubst, because if we get back a predicate from the haskell backend, part of the predicate may be a substitution that can be pull out into its own storage.

[ehildenb]

from_term is OK, I just don't see why we can't have the original and the new functionality both in the constructor.

[tothtamas28]

I just don't see why we can't have the original and the new functionality both in the constructor

We could, but then consider e.g. CTerm(term), CTerm(term, ()). These two calls would be different, but it's not obvious by looking at the code.

what's to stop someone from calling CTerm(config) with a config that contains constraints? Would we add an extra check?

Yes, that's a cheap check:

def __init__(self, config: KInner, constraints: Iterable[KInner] = ()) -> None:
    check_config(config)
    ...

[ehildenb]

How do CTerm(term) and CTerm(term, ()) differ? Both of them would call split_config_and_constraints, and both should end up with the same config and same constraints? What I would propose is:

def __init__(self, config: KInner, constraints: Iterable[KInner] = ()) -> None:
    _config, *_constraints = split_config_and_constraints(config)
    self.config = _config
    self.constraints = CTerm.normalize_constraints(list(constraints) + _constraints)

[tothtamas28]

How do CTerm(term) and CTerm(term, ()) differ? Both of them would call split_config_and_constraints

Ok, I see now. My understanding was the goal is to distinguish between the two initialization methods based on the signature (i.e. whether constraints is provided or not). Sorry for the confusion.

Still, I think it's safer to not make this implicit conversion: if config is constrained but the programmer thinks it's a configuration, CTerm(config, constraints) propagates the error. If the intention is to add constraints, there is add_constraints. If the intention is to deconstruct, there is from_term.

[ehildenb]

I still don't see the reasoning. I don't think if you have a KInner you should usually be making any assumptions about its shape, that's what CTerm is exactly for, is to destruct it for you and make it available via a nice interface. Basically, what I'm saying is, the way that you are trying to stop people from using CTerm is exactly how I have been using it, and how I like to use it. It takes a raw KInner and decomposes it into sensible pieces.

The signature I propose above also gives the saner access directly to adding constraints to an existing constrained term, rather than the CTerm(mlAnd([config] + constraints)) approach, so I'm all for that. But I don't see why we have to also say "and the normal way of using CTerm is not allowed anymore". Is there some specific typing benefit we get from it? Or is it just aesthetic?

[tothtamas28]

the way that you are trying to stop people from using CTerm

and the normal way of using CTerm is not allowed anymore

There are two conceptual ways of creating a CTerm:

1. by constructing from parts
2. by deconstructing a term

My point is to not expose these under a single function (see above). I suggest __init__ for method 1 and from_term for method 2:

def __init__(self, config: KInner, constraints: Iterable[KInner] = ()):
    check_config(config)
    constraints = self._normalize_constraints(constraints)
    object.__setattr__(self, 'config', config)
    object.__setattr__(self, 'constraints', constraints)

@staticmethod
def from_term(term: KInner) -> 'CTerm':
    config, constraint = split_config_and_constraints(term)
    return CTerm(config, constraints)

Note that from_term does exactly what __init__ did so far, so I don't think this change stops anyone from doing anything that was possible before. And it's also not my intention.

But you could argue why I suggest __init__ for method 1 and not vice versa. The reason is, CTerm is a dataclass, and this signiture (building from parts) is closer to the default dataclass initializer than the other.

I don't think if you have a KInner you should usually be making any assumptions about its shape

I agree, and it's possible that from_term will be used more often that CTerm. But there are cases where we know a KInner is a configuration (which is also easy to check), in particular, when it comes from a CTerm. And accordingly, there are a lot of usages where we do CTerm(mlAnd([config] + constraints)), hence the issue.

[ehildenb]

Ok, I'm convinced, we can go with the approach you suggest.