NetworkVerification/nv

Include not processed when file starts with a multi-line comment

alberdingk-thijm opened this issue · 2 comments

The following code does not process the include when it's run.

Code

(* Comment --
*)

include "examples/utils.nv"
(* include isn't processed: defines mapo, mapbetter *)

type attribute = option[int]

let nodes = 2

let edges = { 0=1; }

let trans e x = mapo (fun x -> x + 1) x

let merge n x y = mapbetter (fun x y -> if x < y then x else y) x y

let init n = match n with
  | 0n -> Some 0
  | _ -> None

let assert n x = !(x = None)

Error

Processing comments-mwe.nv

In comments-mwe.nv:

12|  let trans e x = mapo (fun x -> x + 1) x
                     ~~~~

error: comments-mwe.nv: unbound variable mapo~0

Fatal error: exception Nv_lang__Console.Error("unbound variable mapo~0")
Raised at file "src/lib/lang/Console.ml", line 104, characters 2-19
Called from file "src/lib/lang/Typing.ml", line 561, characters 23-52
Called from file "src/lib/lang/Typing.ml", line 561, characters 23-52
Called from file "src/lib/lang/Typing.ml", line 551, characters 8-59
Called from file "src/lib/lang/Typing.ml", line 551, characters 8-59
Called from file "src/lib/lang/Typing.ml", line 858, characters 13-41
Called from file "src/lib/lang/Typing.ml", line 829, characters 19-59
Called from file "src/lib/lang/Typing.ml", line 830, characters 10-58
Called from file "src/lib/lang/Typing.ml", line 830, characters 10-58
Called from file "src/lib/lang/Typing.ml", line 830, characters 10-58
Called from file "src/lib/lang/Typing.ml", line 830, characters 10-58
Called from file "src/lib/lang/Typing.ml", line 830, characters 10-58
Called from file "src/lib/Main_defs.ml", line 343, characters 14-50
Called from file "src/exe/Main.ml", line 6, characters 31-51
Called from file "src/lib/utils/Profile.ml", line 10, characters 12-16
Called from file "src/exe/Main.ml", line 32, characters 2-67

Resolution

Removing the multi-line comment, or moving it after the include fixes this bug.
Multiple single-line comments do not have this problem.
If single-line comments precede the multi-line comment and the include, the include is also not processed:

(* Comment 1 *)
(* Comment 2 *)
(* Multi-
 * line
 *)
include "examples/utils.nv"

Yes, we currently expect that includes are at the beginning of the file. IIRC, the only things allowed before an include statement are empty lines and single-line comments. We could implement a more robust include system, but so far it hasn't been worth the effort.

Gotcha. If I find the time later this month, I can make it work for multi-line comments.