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
(assigning @FTRobbin)
Currently, we allow looking up non-constructor functions (i.e., functions whose output is not an EqSort or have a :merge function) in actions. This can cause actions to fail and make the database end up in an intermediate state.
(function f () i64)
(function g () i64 :merge (min old new))
(datatype E)
(function h () E :merge old)
(rule ()
((let x (f))))
(rule ()
((let x (g))))
(rule ()
((let x (h))))
(run 1)
Moreover, in principle, we don't want actions in a rule to observe the database, because such an implicit dependency implies that if the database changes, the rule needs to be fired again on the database. This is why our desugaring phase needs special handling for our semi-naive evaluation to be sound.
A fix to this is that we should disallow looking up values of functions in actions. By doing so, we can also remove the special handling for our semi-naive evaluation. Note that we should still allow global actions to look up functions, so the following program should still be allowed:
(function f () i64)
(let x (f)) ;; typechecks and throws a run-time error
The text was updated successfully, but these errors were encountered:
(assigning @FTRobbin)
Currently, we allow looking up non-constructor functions (i.e., functions whose output is not an EqSort or have a
:merge
function) in actions. This can cause actions to fail and make the database end up in an intermediate state.Moreover, in principle, we don't want actions in a rule to observe the database, because such an implicit dependency implies that if the database changes, the rule needs to be fired again on the database. This is why our desugaring phase needs special handling for our semi-naive evaluation to be sound.
A fix to this is that we should disallow looking up values of functions in actions. By doing so, we can also remove the special handling for our semi-naive evaluation. Note that we should still allow global actions to look up functions, so the following program should still be allowed:
The text was updated successfully, but these errors were encountered: