Merge pull request #239 from LPCIC/fix-linear

fix regexp for linear variable silencing
LPCIC · Jun 25, 2024 · c272d5f · c272d5f
2 parents 40b1bc5 + 2cff654
commit c272d5f
Show file tree

Hide file tree

Showing 3 changed files with 15 additions and 2 deletions.
diff --git a/src/elpi-checker.elpi b/src/elpi-checker.elpi
@@ -275,11 +275,14 @@ infix >>> 141.
 type (>>>) term -> int -> entry.
 type variable term -> prop.
 
+pred silence-linear-warning i:string.
+silence-linear-warning VN :- rex_match "^_.*" VN ; rex_match ".*_$" VN.
+
 mode (report-linear i).
 report-linear [].
 report-linear [(V >>> 1 + uvar) |NS] :- !,
   pp V VN,
-  if (not(rex_match "_" VN), not(rex_match ".*_" VN))
+  if (not(silence-linear-warning VN))
     (checking LOC,
      MSG is VN ^" is linear: name it _" ^ VN ^
          " (discard) or " ^ VN ^ "_ (fresh variable)",
@@ -288,7 +291,7 @@ report-linear [(V >>> 1 + uvar) |NS] :- !,
   report-linear NS.
 report-linear [(V >>> uvar) |NS] :-
   pp V VN,
-  if (not(rex_match "_" VN), not(rex_match ".*_" VN))
+  if (not(silence-linear-warning VN))
     (checking LOC, MSG is VN ^" is unused", warning LOC MSG)
     true,
   report-linear NS.

diff --git a/tests/sources/linear.elpi b/tests/sources/linear.elpi
@@ -0,0 +1,2 @@
+main :-
+  X = Foo_Bar.
diff --git a/tests/suite/elpi_specific.ml b/tests/suite/elpi_specific.ml
@@ -284,6 +284,14 @@ X0 || X2 && X3 ==> X4
 |})))
   ()
 
+let () = declare "linear"
+  ~source_elpi:"linear.elpi"
+  ~description:"linear variable check"
+  ~typecheck:true
+  ~expectation:Test.(SuccessOutput (Str.regexp_string "Foo_Bar is linear"))
+  ()
+
+
 let () = declare "IO_COLON"
   ~source_elpi:"io_colon.elpi"
   ~description:"IO_COLON token"