-
Notifications
You must be signed in to change notification settings - Fork 502
Open
Description
Look at this:
returnCek (FrameCases env cs ctx) e = case e of
(VConstr i _) | fromIntegral @_ @Integer i > fromIntegral @Int @Integer maxBound ->
throwErrorDischarged (StructuralError (MissingCaseBranchMachineError i)) eWhy do we only tell about e to the user? Why not the Case as well?
Look at this:
applyEvaluate !ctx (VBuiltin fun term runtime) arg = do
let argTerm = dischargeCekValue arg
term' = Apply () term argTerm
case runtime of
BuiltinExpectArgument f ->
evalBuiltinApp ctx fun term' $ f arg
_ ->
throwErrorWithCause (StructuralError UnexpectedBuiltinTermArgumentMachineError) term'
applyEvaluate !_ val _ =
throwErrorDischarged (StructuralError NonFunctionalApplicationMachineError) valIn the VBuiltin clause we report the whole application, but in the catch-all case we only report the function and ignore the argument. Why?
We should just report the whole thing, including the context, but when pretty-printing the error cut off the AST whenever it reaches a certain depth. The current errors are neither compact (values contain arbitrary terms and therefore can be arbitrarily large) nor as helpful as they could be (because we sometimes remove important pieces of the context and sometimes don't). This needs an intelligent approach.