Support Real literal patterns in BSV

src/comp/Parser/BSV/CVParser.lhs

@@ -2761,6 +2761,9 @@ Parse a pattern and return it
 >                                     base = maybeBase }) =
 >               Just $ CPLit $ CLiteral pos $ LInt $ ilDec 0
 >           accept (SV_Token_Number { start_position = pos,
+>                                     value = SV_NUM_Real num }) =
+>               Just $ CPLit $ CLiteral pos $ LReal num
+>           accept (SV_Token_Number { start_position = pos,
 >                                     value = SV_NUM_Mixed bs,
 >                                     base = maybeBase })
 >            | (all (not . isXZ . snd) bs) =
@@ -2782,12 +2785,6 @@ Parse a pattern and return it
 >                                          value = SV_NUM_Mixed _,
 >                                          originalText = txt }) =
 >               Just (pos, EUnsupportedNumUndetermined txt)
->           acceptError (SV_Token_Number { start_position = pos,
->                                          value = SV_NUM_Real _,
->                                          originalText = txt }) =
->               -- equality of real numbers is tricky, so require users
->               -- to express their meaning of equality via a guard
->               Just (pos, EUnsupportedNumReal txt)
 >           acceptError _ = Nothing
 
 > pStringLiteralPattern :: SV_Parser CPat

testsuite/bsc.real/evaluator/PatternReal.bsv

@@ -0,0 +1,26 @@
+function Bit#(3) classifyReal(Real x);
+   return (case (x) matches
+              -1.5: 0;
+               0.0: 1;
+               1.5: 2;
+               default: 3;
+           endcase);
+endfunction
+
+(* synthesize *)
+module sysPatternReal();
+   function m(s) = $display(message(s, s));
+
+   rule r;
+      if (classifyReal(-1.5) == 0)
+         m("negative Real pattern");
+      if (classifyReal(0.0) == 1)
+         m("zero Real pattern");
+      if (classifyReal(-0.0) == 1)
+         m("negative zero uses numeric equality");
+      if (classifyReal(1.5) == 2)
+         m("positive Real pattern");
+      if (classifyReal(2.5) == 3)
+         m("Real pattern default");
+   endrule
+endmodule

testsuite/bsc.real/evaluator/PatternReal.bsv.bsc-vcomp-out.expected

@@ -0,0 +1,10 @@
+checking package dependencies
+compiling PatternReal.bsv
+code generation for sysPatternReal starts
+Compilation message: "PatternReal.bsv", line 16, column 12: negative Real pattern
+Compilation message: "PatternReal.bsv", line 18, column 12: zero Real pattern
+Compilation message: "PatternReal.bsv", line 20, column 12: negative zero uses numeric equality
+Compilation message: "PatternReal.bsv", line 22, column 12: positive Real pattern
+Compilation message: "PatternReal.bsv", line 24, column 12: Real pattern default
+Verilog file created: sysPatternReal.v
+All packages are up to date.

testsuite/bsc.real/evaluator/evaluator.exp

@@ -6,6 +6,13 @@ if { $vtest == 1 } {
 compile_verilog_pass LiteralEqOrd.bsv
 compare_file [make_bsc_vcomp_output_name LiteralEqOrd.bsv]
 
+# ---------------
+# Test positive and negative Real patterns.  Haskell-style numeric patterns
+# use overloaded conversion and equality; in particular, -0.0 matches 0.0.
+
+compile_verilog_pass PatternReal.bsv
+compare_file [make_bsc_vcomp_output_name PatternReal.bsv]
+
 # ---------------
 # Test basic Arith instance operators
 

testsuite/bsc.typechecker/patterncheck/RealPatterns.bsv

@@ -0,0 +1,49 @@
+function Bool incompleteReal(Real x);
+   return (case (x) matches
+              0.0: False;
+              1.0: True;
+           endcase);
+endfunction
+
+// Numeric equality identifies positive and negative zero.
+function Bool redundantSignedZero(Real x);
+   return (case (x) matches
+              0.0: False;
+              -0.0: True;
+              default: True;
+           endcase);
+endfunction
+
+// Prelude's Literal Real conversion is closed and canonicalizes 1 to 1.0.
+function Bool redundantIntegerReal(Real x);
+   return (case (x) matches
+              1: False;
+              1.0: True;
+              default: True;
+           endcase);
+endfunction
+
+function Bool completeReal(Real x);
+   return (case (x) matches
+              0.0: False;
+              default: True;
+           endcase);
+endfunction
+
+typedef struct {
+   Bit#(1) value;
+} TinyReal deriving (Bits, Eq);
+
+instance RealLiteral#(TinyReal);
+   function TinyReal fromReal(Real x);
+      return TinyReal { value: 0 };
+   endfunction
+endinstance
+
+// A custom conversion is arbitrary and therefore deliberately opaque.
+function Bool opaqueCustomReal(TinyReal x);
+   return (case (x) matches
+              1.0: False;
+              2.0: True;
+           endcase);
+endfunction

testsuite/bsc.typechecker/patterncheck/patterncheck.exp

@@ -125,6 +125,12 @@ compile_pass_warning StringLiteralOpaque.bsv T0165 1
 erase StringLiteralOpaque.bo
 compile_pass_warning StringLiteralOpaque.bsv T0166 1
 
+# Concrete Real patterns use numeric equality (including signed zero and the
+# closed Integer-to-Real conversion); custom RealLiteral targets stay opaque.
+compile_pass_warning RealPatterns.bsv T0165 1
+erase RealPatterns.bo
+compile_pass_warning RealPatterns.bsv T0166 2
+
 # Int#(0) has the singleton literal domain {0}; BSV singleton-string Char
 # patterns use the closed Prelude conversion and retain exact equality.
 compile_pass_no_warning ZeroWidthInt.bsv