diff --git a/lib/Cryptol.cry b/lib/Cryptol.cry index 81b74ff0..a30c6e39 100644 --- a/lib/Cryptol.cry +++ b/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. diff --git a/src/Cryptol/Prims/Eval.hs b/src/Cryptol/Prims/Eval.hs index 2907140b..53fd3911 100644 --- a/src/Cryptol/Prims/Eval.hs +++ b/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' diff --git a/src/Cryptol/Symbolic/Prims.hs b/src/Cryptol/Symbolic/Prims.hs index e740f3d7..9a62bf18 100644 --- a/src/Cryptol/Symbolic/Prims.hs +++ b/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) diff --git a/tests/issues/issue290v2.icry.stdout b/tests/issues/issue290v2.icry.stdout index 25d9768a..2f248b81 100644 --- a/tests/issues/issue290v2.icry.stdout +++ b/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 diff --git a/tests/mono-binds/test04.icry.stdout b/tests/mono-binds/test04.icry.stdout index a4e94b4e..a260b0fe 100644 --- a/tests/mono-binds/test04.icry.stdout +++ b/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