Better location information for saw-script type error messages

[brianhuffman]

When the saw-script type checker reports an error message, it only reports the location of the top-level definition in which the error occurred. This is not very helpful, especially if your script consists mainly of one big main function with lots of statements inside. It would be much better if the error message could provide at least the location of the statement containing the error.

Currently pattern variables are the only parts of the saw-script parser AST that have location information (specifically, this includes the x in let x = ... and x <- ...). We need to extend the AST and lexer to save location information for more things, e.g. statements that don't bind a new variable. This would make it possible to report much more accurate locations for errors.

[ntc2]

I just got a type error that doesn't even include a top-level location:

$ saw test.saw 
Loading module Cryptol
Loading file "/var/tmp/saw-bug-floating-point/test.saw"
saw: user error (type mismatch: LLVMSetup () -> t.0 and [LLVMMethodSpec] -> LLVMSetup () -> TopLevel LLVMMethodSpec
 at "_" (REPL)
mismatched type constructors: <Block> and ([])

)

where the content of test.saw is

m <- llvm_load_module "test.bc";

let f_spec = do {
  llvm_return {{ 1 : [32] }};
  llvm_sat_branches true;
  llvm_verify_tactic yices;
};

llvm_verify m "f" f_spec;

(The problem of course is that I forgot the overrides; the last line should be llvm_verify m "f" [] f_spec;.)

[atomb]

I think this may be fixed by some of the latest work by @david-christiansen .

[brianhuffman]

This is probably not worth the effort at this point, as we are planning to move over to the new python-based saw-script frontend.