Position information for backend errors

[d-xo]

Parse / typecheck errors have nice position location, and can be pretty printed, however the position information is not passed down the chain pass the typechecker. This means that errors in the SMT backend (e.g. here), cannot provide a nice pretty printed output showing the user the source of the issue.

I'm not sure what the best way to deal with this is, dragging around the position information in the refined AST seems overly clunky. @kjekac @MrChico do you have any suggestions?

[kjekac]

How about a function which takes

• a refined AST
• an "address into the refined AST" (e.g. [Int], where each element tells us which constructor argument we should recurse on) which points to the place where the error occurred
• the original simple AST

and then matches the ASTs against each other to find the location of the error in the simple AST and returns the concrete syntax location? Maybe there's even a 1-1 mapping between well-typed simple ASTs and refined ASTs (modulo locations)? In that case we should only need the last two arguments.

[d-xo]

hmmmm, the refined AST produced by the typechecker has a bunch of additional conditions attached to it by the Enrich phase. Wouldn't that mess up the mapping (i.e. the addresses in each AST would lead to different places)?

[kjekac]

I'm not sure I understand. I'm thinking like this:

1. When working with a refined AST, it should be relatively easy to keep track of your current position in the tree and save that info to some addressing format whenever an error is encountered. This can then be used to find the error again, at least in the refined AST.
2. I think that it should be relatively easy to find the subtree s in a simple AST which corresponds to a given subtree r in a refined AST (of course assuming that it was refined from that particular simple AST)?

I guess it's step 2 you see as problematic, but in that case my question is: What information are we throwing away in Enrich (except for parser positions which should be unnecessary)? I thought we were only adding information during enrichment? Added information shouldn't pose a problem since we can just ignore that when running enrichment in reverse.

Alternatively, if my question seems misguided, what do you mean by "conditions attached to it"?

[d-xo]

hehe, I think I just hadn't fully understood your proposal 😀

I think that it should be relatively easy to find the subtree s in a simple AST which corresponds to a given subtree r in a refined AST (of course assuming that it was refined from that particular simple AST)?

I hadn't even considered this as a possibility. What would the algorithm look like?

[kjekac]

Something like this? But with waaaaay more cases. Kind of unsatisfactory in that way tbh...

import Syntax
import RefinedAst

type ExpPos = [Int]

getRefinedPos :: ExpPos -> Exp a -> Expr -> Pn
getRefinedPos []       _       e      = getPosn e
getRefinedPos (ix:ixs) refined simple = case ix of
  0 -> case (refined,simple) of
    (And e _, EAnd _ e' _) -> getRefinedPos ixs e e'
    (Or  e _, EOr  _ e' _) -> getRefinedPos ixs e e'
    _                      -> error $ "no first argument in " <> show refined
  1 -> case (refined,simple) of
    (And _ e, EAnd _ _ e') -> getRefinedPos ixs e e'
    (Or  _ e, EOr  _ _ e') -> getRefinedPos ixs e e'
    _                      -> error $ "no second argument in " <> show refined
  2 -> case (refined,simple) of
    (ITE _ _ e, EITE _ _ _ e')     -> getRefinedPos ixs e e'
    (Slice _ _ e, ESlice _ _ _ e') -> getRefinedPos ixs e e'
    _                              -> error $ "no third argument in " <> show refined

[kjekac]

But note that we don't need explicit cases for when refined and simple don't match. All of those can just be an error. So at least we don't need n^2 cases.

What I'm conceptually unclear on at this point is some constructors of Expr, namely Zoom, EntryExp, Func, ListConst, ENewAddr2, BYHash, BYAbiE, WildExp and EnvExp, since these don't seem to have any siblings in Exp a. But looking in Type.hs, it seems like many of these aren't even used?

[MrChico]

hmm, that option seems even more cumbersome than keeping around the position information in the refined context

[kjekac]

Yeah agreed tbh

[kjekac]

I guess one thing we could do is to create a Map ExpPos Pn at the same time as we refine the AST. So like

inferExpr :: Env -> Expr -> Err ReturnExp

becomes

inferExpr :: Env -> Expr -> WriterT (Map ExpPos Pn) Err ReturnExp