Implement compareEq, compareLt and compareLeq primitives.

These allow users to test equalites between type variables and
branch on the results.  This could nearly be accomplished by
instead demoting the value of the numeric expressions to integers
and comparing them as integers.  However, this required `fin`
constraints on the expressions, which is sometimes undesirable.

We also implement the `coerceSize` operation discussed in
issue #704.  We may decide to make this a primitive at a
later time.

lib/Cryptol.cry

@@ -192,6 +192,24 @@ demote = number`{val}
 length : {n, a, b} (fin n, Literal n b) => [n]a -> b
 length _ = `n
 
+/**
+ * Compare the given numeric types, returing
+ * 'True' when 'm == n' and 'False' otherwise.
+ */
+primitive compareEq : { m : #, n : # } Bit
+
+/**
+ * Compare the given numeric types, returning
+ * 'True' when 'm < n' and 'False' otherwise.
+ */
+primitive compareLt : { m : #, n : # } Bit
+
+/**
+ * Compare the given numeric types, returning
+ * 'True' when 'm <= n' and 'False' otherwise.
+ */
+primitive compareLeq : { m : #, n : # } Bit
+
 /**
  * A finite sequence counting up from 'first' to 'last'.
  *
@@ -1081,6 +1099,23 @@ traceVal : {n, a} (fin n) => String n -> a -> a
 traceVal msg x = trace msg x x
 
 
+/**
+ * Force a sequence to be recognized at another size.
+ * When `m == n`, this function is a no-op and passes the given
+ * sequence through unchanged.  When `m` is distinct from `n`,
+ * this function instead raises an error.
+ *
+ * This function is primarily useful when the typechecker cannot
+ * be convinced that certain equalites between size expressions holds.
+ * Inserting an explicit coercion instead allows the typechecker to
+ * skip proving the equation at the cost of performing dynamic checks
+ * at runtime.
+ */
+coerceSize : {m, n, a} [m]a -> [n]a
+coerceSize xs =
+  assert compareEq`{m,n} "coerceSize: size mismatch"
+         [ xs@i | i <- [0..<n] ]
+
 /* Functions previously in Cryptol::Extras */
 
 /**

src/Cryptol/Eval/Generic.hs

@@ -88,6 +88,27 @@ ecNumberV sym =
              , show ty
              ]
 
+{-# INLINE compareEqV #-}
+compareEqV :: Backend sym => sym -> Prim sym
+compareEqV sym =
+  PNumPoly \m ->
+  PNumPoly \n ->
+  PVal . VBit $! bitLit sym (m == n)
+
+{-# INLINE compareLtV #-}
+compareLtV :: Backend sym => sym -> Prim sym
+compareLtV sym =
+  PNumPoly \m ->
+  PNumPoly \n ->
+  PVal . VBit $! bitLit sym (m < n)
+
+{-# INLINE compareLeqV #-}
+compareLeqV :: Backend sym => sym -> Prim sym
+compareLeqV sym =
+  PNumPoly \m ->
+  PNumPoly \n ->
+  PVal . VBit $! bitLit sym (m <= n)
+
 
 {-# SPECIALIZE intV :: Concrete -> Integer -> TValue -> Eval (GenValue Concrete)
   #-}
@@ -1971,6 +1992,10 @@ genericPrimTable sym getEOpts =
                     ratioV sym)
   , ("fraction"   , ecFractionV sym)
 
+  , ("compareEq"  , {-# SCC "Prelude::compareEq" #-}  compareEqV sym)
+  , ("compareLt"  , {-# SCC "Prelude::compareLt" #-}  compareLtV sym)
+  , ("compareLeq" , {-# SCC "Prelude::compareLeq" #-} compareLeqV sym)
+
     -- Zero
   , ("zero"       , {-# SCC "Prelude::zero" #-}
                     PTyPoly \ty ->