GrammaticalFramework / gf-core

Grammatical Framework core: compiler, shell & runtimes
https://www.grammaticalframework.org
Other
131 stars 35 forks source link

Assertion errors in PGF2 not catchable exceptions #72

Closed johnjcamilleri closed 3 years ago

johnjcamilleri commented 4 years ago

Take this minimum working example:

import PGF2
import Control.Exception
import qualified Data.Map as Map

main :: IO ()
main = do
  pgf <- readPGF "Feedback.pgf"
  let Just eng = Map.lookup "FeedbackEng" (languages pgf)
  onException (do
    let expr = mkApp (mkCId "BaseFeature") []
    let s = linearize eng expr
    putStrLn s
    ) (putStrLn "Caught exception")

where:

BaseFeature : Feature -> Feature -> ListFeature

So in my code I am building an invalid tree and expect to get an error. What currently happens is that my program crashes with the following:

pgf_cnc_resolve_app (pgf/linearizer.c:176): assertion failed
    n_args == gu_seq_length(papply->args)

Is there any way this can be thrown as a Haskell exception so that it can be handled appropriately?

krangelov commented 4 years ago

If you generate expressions dynamically and you want to be sure that they are correct, then the right way to go is to use the typechecker. If an incorrect tree is sent to the runtime then it can fail in many different ways. Some of them might be captured by assertions but not all of them.

On Fri, 21 Aug 2020 at 00:30, John J. Camilleri notifications@github.com wrote:

Assigned #72 https://github.com/GrammaticalFramework/gf-core/issues/72 to @krangelov https://github.com/krangelov.

— You are receiving this because you were assigned. Reply to this email directly, view it on GitHub https://github.com/GrammaticalFramework/gf-core/issues/72#event-3677341105, or unsubscribe https://github.com/notifications/unsubscribe-auth/AEYFSZDRIIMQCBMHLXJJSZLSBWPWXANCNFSM4QGVCHVA .

johnjcamilleri commented 4 years ago

Ah I see, fair enough. I guess this can be better documented, I'll add something to the Haskell docs for PGF2.

anka-213 commented 3 years ago

Perhaps we should make a safer API that enforces that dynamically built expressions are type-checked before they can be used with linearize and similar functions? E.g by adding a newtype that can only be built by type-checking or by unsafeAssumeTypeChecked.

aarneranta commented 3 years ago

Yes, it is important to check trees before linearizing them, as the GF Shell does. A couple of issues should be taken into account:


From: Andreas Källberg @.***> Sent: Sunday, May 2, 2021 7:33:57 AM To: GrammaticalFramework/gf-core Cc: Subscribed Subject: Re: [GrammaticalFramework/gf-core] Assertion errors in PGF2 not catchable exceptions (#72)

Perhaps we should make a safer API that enforces that dynamically built expressions are type-checked before they can be used with linearize and similar functions? E.g by adding a newtype that can only be built by type-checking or by unsafeAssumeTypeChecked.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHubhttps://github.com/GrammaticalFramework/gf-core/issues/72#issuecomment-830746564, or unsubscribehttps://github.com/notifications/unsubscribe-auth/AAWBQXKVC6MU2XBTWXVC2OLTLTP4LANCNFSM4QGVCHVA.

anka-213 commented 3 years ago

I guess the major question is how large the performance penalty of type-checking would be. If it is minimal, we could just always do type checking before linearizing and add an unsafe variant that doesn't type check first.