Demote compare

docs/ProgrammingCryptol/crashCourse/CrashCourse.tex

@@ -791,7 +791,7 @@ \subsection{Appending and indexing}
   []
   invalid sequence index: 12
    -- Backtrace --
-  (Cryptol::@) called at Cryptol:870:14--870:20
+  (Cryptol::@) called at Cryptol:888:14--888:20
   (Cryptol::@@) called at <interactive>:9:1--9:28
   [9, 8, 7, 6, 5, 4, 3, 2, 1, 0]
   9

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 ->

src/Cryptol/Eval/Reference.lhs

@@ -895,6 +895,18 @@ by corresponding type classes:
 >                        do _ <- evalString s -- evaluate and ignore s
 >                           _ <- x -- evaluate and ignore x
 >                           y
+>
+>   , "compareEq"  ~> VNumPoly $ \m -> pure $
+>                     VNumPoly $ \n -> pure $
+>                     VBit (m == n)
+>
+>   , "compareLt"  ~> VNumPoly $ \m -> pure $
+>                     VNumPoly $ \n -> pure $
+>                     VBit (m < n)
+>
+>   , "compareLeq" ~> VNumPoly $ \m -> pure $
+>                     VNumPoly $ \n -> pure $
+>                     VBit (m <= n)
 >   ]
 >
 >

src/Cryptol/ModuleSystem/Renamer.hs

@@ -32,7 +32,7 @@ import Prelude.Compat
 import Data.Either(partitionEithers)
 import Data.Maybe(fromJust)
 import Data.List(find,foldl')
-import Data.Foldable(toList)
+import Data.Foldable(toList, traverse_)
 import Data.Map.Strict(Map)
 import qualified Data.Map.Strict as Map
 import qualified Data.Set as Set
@@ -500,9 +500,21 @@ rnLocated f loc = withLoc loc $
   do a' <- f (thing loc)
      return loc { thing = a' }
 
+touchSigParams :: Schema Name -> RenameM ()
+touchSigParams (Forall params _props _tp _loc) =
+  mapM_ (recordUse . tpName) params
+
 instance Rename Decl where
   rename d      = case d of
-    DBind b           -> DBind <$> rename b
+    DBind b ->
+      case thing (bDef b) of
+        DExpr _ -> DBind <$> rename b
+        DPrim ->
+          do b' <- rename b
+             -- Record an additional use for each type parameter of primitives.
+             -- This prevents "unused name" warnings for primitive declarations.
+             traverse_ touchSigParams (bSignature b')
+             return (DBind b')
 
     DType syn         -> DType         <$> rename syn
     DProp syn         -> DProp         <$> rename syn

tests/issues/T146.icry.stdout

@@ -4,15 +4,15 @@ Loading module Main
 
 [error] at T146.cry:1:18--6:10:
   The type ?a is not sufficiently polymorphic.
-    It cannot depend on quantified variables: fv`828
+    It cannot depend on quantified variables: fv`854
     When checking type of field 'v0'
   where
   ?a is type argument 'fv' of 'Main::ec_v1' at T146.cry:4:19--4:24
-  fv`828 is signature variable 'fv' at T146.cry:11:10--11:12
+  fv`854 is signature variable 'fv' at T146.cry:11:10--11:12
 [error] at T146.cry:5:19--5:24:
   The type ?b is not sufficiently polymorphic.
-    It cannot depend on quantified variables: fv`828
+    It cannot depend on quantified variables: fv`854
     When checking signature variable 'fv'
   where
   ?b is type argument 'fv' of 'Main::ec_v2' at T146.cry:5:19--5:24
-  fv`828 is signature variable 'fv' at T146.cry:11:10--11:12
+  fv`854 is signature variable 'fv' at T146.cry:11:10--11:12

tests/issues/issue1024.icry.stdout

@@ -13,20 +13,20 @@ Loading module Main
     Unused name: g
 
 [error] at issue1024a.cry:1:6--1:11:
-  Illegal kind assigned to type variable: f`825
+  Illegal kind assigned to type variable: f`851
   Unexpected: # -> *
   where
-  f`825 is signature variable 'f' at issue1024a.cry:1:12--1:24
+  f`851 is signature variable 'f' at issue1024a.cry:1:12--1:24
 [error] at issue1024a.cry:2:6--2:13:
-  Illegal kind assigned to type variable: f`826
+  Illegal kind assigned to type variable: f`852
   Unexpected: Prop
   where
-  f`826 is signature variable 'f' at issue1024a.cry:2:14--2:24
+  f`852 is signature variable 'f' at issue1024a.cry:2:14--2:24
 [error] at issue1024a.cry:4:13--4:49:
-  Illegal kind assigned to type variable: f`828
+  Illegal kind assigned to type variable: f`854
   Unexpected: # -> *
   where
-  f`828 is signature variable 'f' at issue1024a.cry:4:22--4:32
+  f`854 is signature variable 'f' at issue1024a.cry:4:22--4:32
 Loading module Cryptol
 Loading module Main
 0xffff

tests/issues/issue103.icry.stdout

@@ -2,7 +2,7 @@ Loading module Cryptol
 
 Run-time error: undefined
 -- Backtrace --
-Cryptol::error called at Cryptol:1040:13--1040:18
+Cryptol::error called at Cryptol:1058:13--1058:18
 Cryptol::undefined called at issue103.icry:1:9--1:18
 Using exhaustive testing.
 Testing... ERROR for the following inputs:

tests/issues/issue226.icry.stdout

@@ -115,6 +115,10 @@ Symbols
     assert : {a, n} (fin n) => Bit -> String n -> a -> a
     carry : {n} (fin n) => [n] -> [n] -> Bit
     ceiling : {a} (Round a) => a -> Integer
+    coerceSize : {m, n, a} [m]a -> [n]a
+    compareEq : {m, n} Bit
+    compareLeq : {m, n} Bit
+    compareLt : {m, n} Bit
     complement : {a} (Logic a) => a -> a
     curry : {a, b, c} ((a, b) -> c) -> a -> b -> c
     deepseq : {a, b} (Eq a) => a -> b -> b

tests/issues/issue290v2.icry.stdout

@@ -4,9 +4,9 @@ Loading module Main
 
 [error] at issue290v2.cry:2:1--2:19:
   Unsolved constraints:
-    • n`825 == 1
+    • n`851 == 1
         arising from
         checking a pattern: type of 1st argument of Main::minMax
         at issue290v2.cry:2:8--2:11
   where
-  n`825 is signature variable 'n' at issue290v2.cry:1:11--1:12
+  n`851 is signature variable 'n' at issue290v2.cry:1:11--1:12

tests/issues/issue723.icry.stdout

@@ -10,9 +10,9 @@ Loading module Main
       assuming
         • fin k
       the following constraints hold:
-        • k == n`825
+        • k == n`851
             arising from
             matching types
             at issue723.cry:7:17--7:19
   where
-  n`825 is signature variable 'n' at issue723.cry:1:6--1:7
+  n`851 is signature variable 'n' at issue723.cry:1:6--1:7

tests/modsys/T16.icry.stdout

@@ -5,5 +5,5 @@ Loading module T16::B
 
 [error] at ./T16/B.cry:5:5--5:11
     Multiple definitions for symbol: update
-    (at Cryptol:894:11--894:17, update)
+    (at Cryptol:912:11--912:17, update)
     (at ./T16/A.cry:3:1--3:7, T16::A::update)

tests/regression/safety.icry.stdout

@@ -3,7 +3,7 @@ Counterexample
 (\x -> assert x "asdf" "asdf") False ~> ERROR
 Run-time error: asdf
 -- Backtrace --
-Cryptol::error called at Cryptol:1048:41--1048:46
+Cryptol::error called at Cryptol:1066:41--1066:46
 Cryptol::assert called at safety.icry:3:14--3:20
 <interactive>::it called at safety.icry:3:7--3:37
 Counterexample

tests/regression/tc-errors.icry.stdout

@@ -83,19 +83,19 @@ Loading module Main
 
 [error] at tc-errors-5.cry:2:5--2:7:
   Inferred type is not sufficiently polymorphic.
-    Quantified variable: a`825
+    Quantified variable: a`851
     cannot match type: [0]?a
     When checking the type of 'Main::f'
   where
   ?a is type of sequence member at tc-errors-5.cry:2:5--2:7
-  a`825 is signature variable 'a' at tc-errors-5.cry:1:6--1:7
+  a`851 is signature variable 'a' at tc-errors-5.cry:1:6--1:7
 Loading module Cryptol
 Loading module Main
 
 [error] at tc-errors-6.cry:4:7--4:8:
   The type ?a is not sufficiently polymorphic.
-    It cannot depend on quantified variables: b`829
+    It cannot depend on quantified variables: b`855
     When checking the type of 'g'
   where
   ?a is the type of 'x' at tc-errors-6.cry:1:3--1:4
-  b`829 is signature variable 'b' at tc-errors-6.cry:3:8--3:9
+  b`855 is signature variable 'b' at tc-errors-6.cry:3:8--3:9