Replace indexing primitives (!!) and (@@) with cryptol implementations.

lib/Cryptol.cry

@@ -374,7 +374,8 @@ primitive (@) : {a, b, c} (fin c) => [a]b -> [c] -> b
  * Bulk index operator.  The first argument is a sequence.  The second argument
  * is a sequence of the zero-based indices of the elements to select.
  */
-primitive (@@) : {a, b, c, d} (fin d) => [a]b -> [c][d] -> [c]b
+(@@) : {a, b, c, d} (fin d) => [a]b -> [c][d] -> [c]b
+xs @@ is = [ xs @ i | i <- is ]
 
 /**
  * Reverse index operator.  The first argument is a finite sequence.  The second
@@ -388,7 +389,8 @@ primitive (!) : {a, b, c} (fin a, fin c) => [a]b -> [c] -> b
  * second argument is a sequence of the zero-based indices of the elements to
  * select, starting from the end of the sequence.
  */
-primitive (!!) : {a, b, c, d} (fin a, fin d) => [a]b -> [c][d] -> [c]b
+(!!) : {a, b, c, d} (fin a, fin d) => [a]b -> [c][d] -> [c]b
+xs !! is = [ xs ! i | i <- is ]
 
 /**
  * Update the given sequence with new value at the given index position.

src/Cryptol/Prims/Eval.hs

@@ -134,13 +134,9 @@ primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
                     lam  $ \ r     -> join (ccatV front back elty <$> l <*> r))
 
   , ("@"          , {-# SCC "Prelude::(@)" #-}
-                    indexPrimOne  indexFront_bits indexFront)
-  , ("@@"         , {-# SCC "Prelude::(@@)" #-}
-                    indexPrimMany indexFront_bits indexFront)
+                    indexPrim indexFront_bits indexFront)
   , ("!"          , {-# SCC "Prelude::(!)" #-}
-                    indexPrimOne  indexBack_bits indexBack)
-  , ("!!"         , {-# SCC "Prelude::(!!)" #-}
-                    indexPrimMany indexBack_bits indexBack)
+                    indexPrim indexBack_bits indexBack)
 
   , ("update"     , {-# SCC "Prelude::update" #-}
                     updatePrim updateFront_word updateFront)
@@ -1212,12 +1208,12 @@ rotateRS w _ vs by = IndexSeqMap $ \i ->
 
 -- Sequence Primitives ---------------------------------------------------------
 
--- | Indexing operations that return one element.
-indexPrimOne :: BitWord b w i
-             => (Maybe Integer -> TValue -> SeqMap b w i -> Seq.Seq b -> Eval (GenValue b w i))
-             -> (Maybe Integer -> TValue -> SeqMap b w i -> w -> Eval (GenValue b w i))
-             -> GenValue b w i
-indexPrimOne bits_op word_op =
+-- | Indexing operations.
+indexPrim :: BitWord b w i
+          => (Maybe Integer -> TValue -> SeqMap b w i -> Seq.Seq b -> Eval (GenValue b w i))
+          -> (Maybe Integer -> TValue -> SeqMap b w i -> w -> Eval (GenValue b w i))
+          -> GenValue b w i
+indexPrim bits_op word_op =
   nlam $ \ n  ->
   tlam $ \ a ->
   nlam $ \ _i ->
@@ -1227,13 +1223,13 @@ indexPrimOne bits_op word_op =
                VWord _ w  -> w >>= \w' -> return $ IndexSeqMap (\i -> VBit <$> indexWordValue w' i)
                VSeq _ vs  -> return vs
                VStream vs -> return vs
-               _ -> evalPanic "Expected sequence value" ["indexPrimOne"]
+               _ -> evalPanic "Expected sequence value" ["indexPrim"]
       r >>= \case
          VWord _ w -> w >>= \case
            WordVal w' -> word_op (fromNat n) a vs w'
            BitsVal bs -> bits_op (fromNat n) a vs =<< sequence bs
            LargeBitsVal m xs -> bits_op (fromNat n) a vs . Seq.fromList =<< traverse (fromBit =<<) (enumerateSeqMap m xs)
-         _ -> evalPanic "Expected word value" ["indexPrimOne"]
+         _ -> evalPanic "Expected word value" ["indexPrim"]
 
 indexFront :: Maybe Integer -> TValue -> SeqValMap -> BV -> Eval Value
 indexFront mblen _a vs (bvVal -> ix) =
@@ -1255,32 +1251,6 @@ indexBack mblen _a vs (bvVal -> ix) =
 indexBack_bits :: Maybe Integer -> TValue -> SeqValMap -> Seq.Seq Bool -> Eval Value
 indexBack_bits mblen a vs = indexBack mblen a vs . packWord . Fold.toList
 
--- | Indexing operations that return many elements.
-indexPrimMany :: BitWord b w i
-              => (Maybe Integer -> TValue -> SeqMap b w i -> Seq.Seq b -> Eval (GenValue b w i))
-              -> (Maybe Integer -> TValue -> SeqMap b w i -> w -> Eval (GenValue b w i))
-              -> GenValue b w i
-indexPrimMany bits_op word_op =
-  nlam $ \ n  ->
-  tlam $ \ a  ->
-  nlam $ \ m  ->
-  nlam $ \ _i ->
-   lam $ \ l  -> return $
-   lam $ \ r  -> do
-     vs <- (l >>= \case
-               VWord _ w  -> w >>= \w' -> return $ IndexSeqMap (\i -> VBit <$> indexWordValue w' i)
-               VSeq _ vs  -> return vs
-               VStream vs -> return vs
-               _ -> evalPanic "Expected sequence value" ["indexPrimMany"])
-     ixs <- fromSeq "indexPrimMany idx" =<< r
-     mkSeq m a <$> memoMap (IndexSeqMap $ \i -> do
-       lookupSeqMap ixs i >>= \case
-         VWord _ w -> w >>= \case
-            WordVal w' -> word_op (fromNat n) a vs w'
-            BitsVal bs -> bits_op (fromNat n) a vs =<< sequence bs
-            LargeBitsVal o xs -> bits_op (fromNat n) a vs . Seq.fromList =<< traverse (fromBit =<<) (enumerateSeqMap o xs)
-         _ -> evalPanic "Expected word value" ["indexPrimMany"])
-
 
 updateFront
   :: Nat'

src/Cryptol/Symbolic/Prims.hs

@@ -36,7 +36,7 @@ import Cryptol.Prims.Eval (binary, unary, arithUnary,
                            ccatV, splitAtV, joinV, ecSplitV,
                            reverseV, infFromV, infFromThenV,
                            fromThenV, fromToV, fromThenToV,
-                           transposeV, indexPrimOne, indexPrimMany,
+                           transposeV, indexPrim,
                            ecIntegerV, ecToIntegerV, ecFromIntegerV,
                            ecDemoteV, updatePrim, randomV, liftWord,
                            cmpValue, lg2)
@@ -174,10 +174,8 @@ primTable  = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
   , ("infFrom"     , infFromV)
   , ("infFromThen" , infFromThenV)
 
-  , ("@"           , indexPrimOne  indexFront_bits indexFront)
-  , ("@@"          , indexPrimMany indexFront_bits indexFront)
-  , ("!"           , indexPrimOne  indexBack_bits indexBack)
-  , ("!!"          , indexPrimMany indexBack_bits indexBack)
+  , ("@"           , indexPrim indexFront_bits indexFront)
+  , ("!"           , indexPrim indexBack_bits indexBack)
 
   , ("update"      , updatePrim updateFrontSym_word updateFrontSym)
   , ("updateEnd"   , updatePrim updateBackSym_word updateBackSym)

tests/issues/issue290v2.icry.stdout

@@ -4,7 +4,7 @@ Loading module Main
 
 [error] at ./issue290v2.cry:2:1--2:19:
   Unsolved constraints:
-    a`583 == 1
+    a`601 == 1
       arising from
       checking a pattern: type of 1st argument of Main::minMax
       at ./issue290v2.cry:2:8--2:11

tests/mono-binds/test04.icry.stdout

@@ -25,8 +25,8 @@ Loading module test04
 [error] at ./test04.cry:3:19--3:21:
   Type mismatch:
     Expected type: ()
-    Inferred type: [?z22]
+    Inferred type: [?r23]
   where
-  ?z22 is type parameter 'bits'
+  ?r23 is type parameter 'bits'
           of literal or demoted expression
           at ./test04.cry:3:19--3:21