fix: Generate dummy constraint for newtypes to enable axiom generation
#4190
Conversation
|
Before merging we need to figure out how to pass the wellformedness check, now that we don't conveniently skip it anymore. The test fails, because we lose track of the witness. |
Test/git-issues/git-issue-4188.dfy
Outdated
| // RUN: %baredafny verify %args "%s" > "%t" | ||
| // RUN: %diff "%s.expect" "%t" | ||
|
|
||
| newtype Int = nat |
There was a problem hiding this comment.
I suggest making two more variations of this example, namely the ones mentioned in the Issue discussion (newtype Int = int and newtype Int = n: nat | true, perhaps also with newtype Int = x: int | 0 <= x).
| dd.Var ??= new BoundVar(dd.tok, "x", dd.BaseType) { IsTypeExplicit = true }; | ||
| dd.Constraint ??= Expression.CreateBoolLiteral(dd.tok, true); | ||
|
|
||
| AddWellformednessCheck(dd); | ||
| currentModule = dd.EnclosingModuleDefinition; | ||
| // Add $Is and $IsAlloc axioms for the newtype | ||
| AddRedirectingTypeDeclAxioms(false, dd, dd.FullName); | ||
| AddRedirectingTypeDeclAxioms(true, dd, dd.FullName); | ||
| currentModule = null; |
There was a problem hiding this comment.
Well identified! These type axioms are what's missing. However, it's not a good idea to change the AST at this time. Also, I think it's fine to continue to omit a well-formedness check for these var-less newtypes (hence, addressing your question in the PR comment).
So, I suggest making the if (dd.Var != null) control only whether or not AddWellformednessCheck is called. Then, do the other lines in either case (as you have in your new L1281-L1285).
Then, adjust AddRedirectingTypeDeclAxioms so that it's able to handle the dd.Var == null case. Instead of dd.Var.Type (which occurs many times in that method), use baseType defined as
var baseType = dd.Var != null ? dd.Var.Type : ((NewtypeDecl)(object)dd).BaseType;One of the method's preconditions thus needs to change to
Contract.Requires((dd.Var != null && dd.Constraint != null) || dd is NewtypeDecl);There are two other occurrences of dd.Var that you'll need to handle in some way.
FInally, if dd.Constraint is null, use Bpl.Expr.True instead of etran.TrExpr(dd.Constraint).
Revert unnecessary change.
Fixes #4188.