Separate syntax and semantics feedback

[patritzenfeld]

• adjustments to grade
• configurable frontier between phases through syntaxCutoff option

[patritzenfeld]

Actually, I'm a bit unsatisfied with the (b, Maybe b) result type of grade. After some consideration, it seems this should indeed just be b as before.

You mentioned the (b, Maybe b) having some documentary value in #38 (comment), but the context Monad already must have a failure mechanism build in, given we are passing a function with type (forall c . Doc -> m c) (the signature is required to be like this and cannot be simplified as you asked about in that same comment). So having that tuple result type with a Maybe seems very redundant in hindsight.

The concrete implementation of the eval argument also gets needlessly complicated because of this, due to needing to check the outcome of the syntax phase explicitly. If it is changed to b, it would be a much simpler call, e.g. for Autotool:

eval = runReason . (setReason Syntax >=> setReason Semantics))

Instead of having a case distinction that cannot use the composability of the Reporter Monad (this code is a bit raw):

eval checks = do
        (syntaxResult, syntaxOutput) <- runReason $ setReason Syntax checks
        case syntaxResult of
          Left r ->
            ...
          Right semantics -> do
            semanticsResult <- runReason $ setReason Semantics semantics
            return ...

I should probably have noticed this sooner, but I'd be in favour of changing this back to a plain b. What do you think?

[jvoigtlaender]

Okay, go ahead.

[jvoigtlaender]

Maybe deferred to a separate PR: a config option that can be set to turn off the semantics phase (whatever that phase is, according to the split-phases setting).

One use-case: configuring a task complete with test suite etc., but turning the semantics stuff off during an exam setting (not only hiding the semantics output, but really preventing its possibly costly computation), but being able to simply turn it on after the fact.

[jvoigtlaender]

As another iteration on the API here:

What about replacing eval :: (m (m ()) -> IO b) in the type of grade by two argument functions withSyntax :: m () -> m () and withSemantics :: m () -> m (), and letting grade overall return m () instead of IO b?

Instead of:

  eval $ do
    … 
    sequence_ syntax
    return $ sequence_ semantics

the implementation would then be:

  do
    … 
    withSyntax (sequence_ syntax)
    withSemantics (sequence_ semantics)

(Still need to consider whether the … part, or some steps in it, should also be wrapped in withSyntax or not. In the current implementation, that whole „preparation part“ is implicitly also annotated with the setReason Syntax bit. Is that adequate? Does it make a difference at all?)

In the test suite, the usage would be withSyntax = withSemantics = id (agreeing with join = id >=> id) and the grade call itself would be wrapped in execWriterT.

From Autotool, the usage would be withSyntax = setReason Syntax, withSemantics = setReason Semantics and the grade call itself would be wrapped in runReason (taken from your above eval definition for that case).

And the config option in #41 could be realized by conditionally setting withSemantics = const (pure ()).