You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
There are wellformedness checks that need to be performed before a theory is translated (e.g., for accountability and SAPiC).
However, these cannot currently be performed in src/Web/Theory.hs since the theory is already closed at this point.
See the relevant code:
++ checkPreTransWellformedness (openTheory thy) -- FIXME: openTheory doesn't contain translated items, hence no warning is shown in the interactive mode
Possible solutions:
Cache the wellformedness report and include it in TheoryInfo
Since I cannot think of a way a report can be invalided once a theory is loaded, this should be sound.
Problem: WfErrorReport doesn't provide a Binary instance which is needed for inclusion in TheoryInfo
Store the OpenTheory in TheoryInfo
The text was updated successfully, but these errors were encountered:
There are wellformedness checks that need to be performed before a theory is translated (e.g., for accountability and SAPiC).
However, these cannot currently be performed in
src/Web/Theory.hs
since the theory is already closed at this point.See the relevant code:
tamarin-prover/src/Web/Theory.hs
Lines 1058 to 1059 in ba992bc
Possible solutions:
Cache the wellformedness report and include it in
TheoryInfo
Since I cannot think of a way a report can be invalided once a theory is loaded, this should be sound.
Problem:
WfErrorReport
doesn't provide aBinary
instance which is needed for inclusion inTheoryInfo
Store the
OpenTheory
inTheoryInfo
The text was updated successfully, but these errors were encountered: