Remove deprecated type "Fin" along with "generate", "get", and "set".

Resolves #4.

prelude/Prelude.sawcore

@@ -468,21 +468,6 @@ natCase :: (p :: Nat -> sort 0) -> p Zero -> ((n :: Nat) -> p (Succ n)) -> (n ::
 natCase p z s Zero = z;
 natCase p z s (Succ n) = s n;
 
---------------------------------------------------------------------------------
--- Fin
-
--- | Natural numbers less than a given bound.
-data Fin :: (n :: Nat) -> sort 0 where {
-    -- Fin value contains the value v and the number r of additional values above it.
-     FinVal :: (v r :: Nat) -> Fin (Succ (addNat v r));
-  }
-
-finFront :: (n :: Nat) -> Fin n -> Nat;
-finFront _ (FinVal v _) = v;
-
-finEq :: (n :: Nat) -> (i j :: Fin n) -> Bool;
-finEq n i j = equalNat (finFront n i) (finFront n j);
-
 --------------------------------------------------------------------------------
 -- "Vec n a" is an array of n elements, each with type "a".
 data Vec :: Nat -> sort 0 -> sort 0 where {
@@ -902,30 +887,3 @@ axiom ite_join_cong :: (b :: Bool)
               -> Eq (Vec 384 Bool)
                     (join 12 32 Bool (ite (Vec 12 (Vec 32 Bool)) b x y))
                     (ite (Vec 384 Bool) b (join 12 32 Bool x) (join 12 32 Bool y));
-
---------------------------------------------------------------------------------
--- Deprecated items
-
--- Function for generating an array.
-primitive generate :: (n :: Nat) -> (a :: sort 0) -> (Fin n -> a) -> Vec n a;
-
--- Get and set an individual element in an array.
-get :: (n :: Nat) -> (a :: sort 0) -> Vec n a -> Fin n -> a;
-get _ _ (ConsVec _ e _ _) (FinVal Zero _) = e;
-get _ a (ConsVec _ _ _ r) (FinVal (Succ i) j) =
-  get (Succ (addNat i j)) a r (FinVal i j);
-
--- | Axiomatic rewrite rule.
-axiom get_generate :: (n :: Nat) -> (e :: sort 0) -> (f :: Fin n -> e) -> (i :: Fin n) ->
-                Eq e (get n e (generate n e f) i) (f i);
-
-set :: (n :: Nat) -> (a :: sort 0) -> Vec n a -> Fin n -> a -> Vec n a;
-set n a v i x = generate n a (\(j :: Fin n) -> ite a (finEq n i j) x (get n a v j));
-
--- | Take a prefix of a vector.
-vMove :: (a :: sort 0)
-      -> (m n :: Nat)
-      -> (Fin n -> Fin m)
-      -> Vec m a
-      -> Vec n a;
-vMove a m n f v = generate n a (\(j :: Fin n) -> get m a v (f j));

src/Verifier/SAW/Conversion.hs

@@ -62,7 +62,6 @@ module Verifier.SAW.Conversion
   , asLocalVar
     -- ** Prelude matchers
   , asBoolType
-  , asFinValLit
   , asSuccLit
   , asBvNatLit
     -- ** Matchable typeclass
@@ -94,7 +93,6 @@ module Verifier.SAW.Conversion
   , bvConversions
   , succ_NatLit
   , addNat_NatLit
-  , get_VecLit
   , append_VecLit
   , append_bvNat
   , bvAdd_bvNat
@@ -103,7 +101,6 @@ module Verifier.SAW.Conversion
   , bvult_bvNat
   , bvsle_bvNat
   , bvslt_bvNat
-  , get_bvNat
   , slice_bvNat
   , remove_coerce
   , remove_unsafeCoerce
@@ -328,10 +325,6 @@ asLocalVar = asVar $ \t -> do i <- R.asLocalVar t; return i
 asBoolType :: (Monad m, Termlike t) => Matcher m t ()
 asBoolType = asDataType "Prelude.Bool" asEmpty
 
-asFinValLit :: (Functor m, Monad m, Termlike t) => Matcher m t Prim.Fin
-asFinValLit = (\(i :*: j) -> Prim.FinVal i j)
-  <$> asCtor "Prelude.FinVal" (asAnyNatLit >: asAnyNatLit)
-
 asSuccLit :: (Functor m, Monad m, Termlike t) => Matcher m t Prim.Nat
 asSuccLit = asCtor "Prelude.Succ" asAnyNatLit
 
@@ -369,9 +362,6 @@ instance (Monad m, Termlike t) => Matchable m t Int where
 instance (Applicative m, Monad m, Termlike t) => Matchable m t Prim.BitVector where
     defaultMatcher = asBvNatLit
 
-instance (Functor m, Monad m, Termlike t) => Matchable m t Prim.Fin where
-    defaultMatcher = asFinValLit
-
 instance (Functor m, Monad m, Termlike t) => Matchable m t (Prim.Vec t t) where
     defaultMatcher = uncurry Prim.Vec <$> asAnyVecLit
 
@@ -589,11 +579,7 @@ equalNat_NatLit = globalConv "Prelude.equalNat" ((==) :: Nat -> Nat -> Bool)
 
 -- | Conversions for operations on vector literals
 vecConversions :: Termlike t => [Conversion t]
-vecConversions = [get_VecLit, at_VecLit, append_VecLit]
-
-get_VecLit :: forall t. Termlike t => Conversion t
-get_VecLit = globalConv "Prelude.get"
-    (Prim.get :: Int -> t -> Prim.Vec t t -> Prim.Fin -> t)
+vecConversions = [at_VecLit, append_VecLit]
 
 at_VecLit :: forall t. Termlike t => Conversion t
 at_VecLit = globalConv "Prelude.at"
@@ -633,7 +619,7 @@ bvConversions =
     , globalConv "Prelude.bvUExt"  Prim.bvUExt
     , globalConv "Prelude.bvSExt"  Prim.bvSExt
 
-    , get_bvNat, at_bvNat, slice_bvNat
+    , at_bvNat, slice_bvNat
     , take_bvNat, drop_bvNat
     ]
 
@@ -658,9 +644,6 @@ bvsge_bvNat = globalConv "Prelude.bvsge" Prim.bvsge
 bvslt_bvNat = globalConv "Prelude.bvslt" Prim.bvslt
 bvsle_bvNat = globalConv "Prelude.bvsle" Prim.bvsle
 
-get_bvNat :: Termlike t => Conversion t
-get_bvNat = globalConv "Prelude.get" Prim.get_bv
-
 at_bvNat :: Termlike t => Conversion t
 at_bvNat = globalConv "Prelude.at" Prim.at_bv
 

src/Verifier/SAW/Prelude.hs

@@ -16,10 +16,6 @@ module Verifier.SAW.Prelude
   , module Verifier.SAW.Prelude.Constants
   ) where
 
-#if !MIN_VERSION_base(4,8,0)
-import Control.Applicative ((<$>), (<*>))
-#endif
-import Control.Monad (join) 
 import Verifier.SAW.ParserUtils
 import Verifier.SAW.Prelude.Constants
 import Verifier.SAW.SharedTerm
@@ -29,15 +25,6 @@ $(runDecWriter $ do
     declareSharedModuleFns "Prelude" (decVal prelude)
  )
 
-scFinConst :: SharedContext s
-           -> Nat -- ^ Index
-           -> Nat -- ^ Bound n
-           -> IO (SharedTerm s)
-scFinConst sc i n | i < n = do
-  fv <- scApplyPrelude_FinVal sc
-  join $ fv <$> scNat sc i <*> scNat sc (n - (i + 1))
-scFinConst _ _ _ = error "illegal arguments to scFinConst"
-
 scEq :: SharedContext s -> SharedTerm s -> SharedTerm s -> IO (SharedTerm s)
 scEq sc x y = do
   xty <- scTypeOf sc x

src/Verifier/SAW/Prim.hs

@@ -15,7 +15,6 @@ module Verifier.SAW.Prim where
 #if !MIN_VERSION_base(4,8,0)
 import Control.Applicative
 #endif
-import Control.Exception (assert)
 import qualified Control.Exception as X
 import Data.Bits
 import Data.Typeable (Typeable)
@@ -110,52 +109,6 @@ widthNat :: Nat -> Nat
 widthNat 0 = 0
 widthNat n = 1 + widthNat (n `div` 2)
 
-------------------------------------------------------------
--- Finite indices
-
-data Fin = FinVal { finVal :: !Nat, finRem :: Nat }
-    deriving (Eq, Show)
-
-finFromBound :: Nat -> Nat -> Fin
-finFromBound i n
-  | i < n = FinVal i (pred (n - i))
-  | otherwise = error "finFromBound given out-of-range index."
-
-finSize :: Fin -> Nat
-finSize (FinVal x r) = succ (r + x)
-
-incFinBy :: Fin -> Nat -> Maybe Fin
-incFinBy x y
-   | r' < 0 = Nothing
-   | otherwise = Just x'
- where r' = toInteger (finRem x) - toInteger y
-       x' = FinVal (finVal x + y) (fromInteger r')
-
-instance Enum Fin where
-  succ (FinVal _ 0) = error "FinVal has no successor."
-  succ (FinVal x r) = FinVal (succ x) (pred r)
-  pred (FinVal 0 _) = error "FinVal has no predecessor."
-  pred (FinVal x r) = FinVal (pred x) (succ r)
-  toEnum x = FinVal (toEnum x) (error "FinVal.toEnum has no bound.")
-  fromEnum = fromEnum . finVal
-  enumFrom x | finRem x == 0 = [x]
-             | otherwise = x : enumFrom (succ x)
-
-  enumFromThen x y =
-    case incFinBy x (finVal y) of
-      Nothing -> [x]
-      Just x' -> x : enumFromThen x' y
-
-  enumFromTo x z = enumFromThenTo x (FinVal 1 (finSize x)) z
-
-  enumFromThenTo x0 y z =
-      assert (finSize x0 == finSize z) $
-      assert (finVal x0 <= finVal z) $
-      go x0
-    where go x = case incFinBy x (finVal y) of
-                   Nothing -> [x]
-                   Just x' -> x : go x'
-
 -- data Vec :: (n :: Nat) -> sort 0 -> sort 0
 data Vec t a = Vec t !(Vector a)
 
@@ -201,8 +154,8 @@ addNat :: Integer -> Integer -> Integer
 addNat = (+)
 
 -- get :: (n :: Nat) -> (e :: sort 0) -> Vec n e -> Fin n -> e;
-get :: Int -> t -> Vec t e -> Fin -> e
-get _ _ (Vec _ v) i = v ! fromEnum i
+--get :: Int -> t -> Vec t e -> Fin -> e
+--get _ _ (Vec _ v) i = v ! fromEnum i
 
 -- append :: (m n :: Nat) -> (e :: sort 0) -> Vec m e -> Vec n e -> Vec (addNat m n) e;
 append :: Int -> Int -> t -> Vec t e -> Vec t e -> Vec t e
@@ -259,8 +212,8 @@ bvsle _ x y = signed x <= signed y
 
 -- | @get@ specialized to BitVector (big-endian)
 -- get :: (n :: Nat) -> (a :: sort 0) -> Vec n a -> Fin n -> a;
-get_bv :: Int -> () -> BitVector -> Fin -> Bool
-get_bv _ _ x i = testBit (unsigned x) (width x - 1 - fromEnum i)
+--get_bv :: Int -> () -> BitVector -> Fin -> Bool
+--get_bv _ _ x i = testBit (unsigned x) (width x - 1 - fromEnum i)
 -- little-endian version:
 -- get_bv _ _ x i = testBit (unsigned x) (fromEnum i)
 
@@ -271,9 +224,9 @@ at_bv _ _ x i = testBit (unsigned x) (width x - 1 - fromIntegral i)
 
 -- | @set@ specialized to BitVector (big-endian)
 -- set :: (n :: Nat) -> (a :: sort 0) -> Vec n a -> Fin n -> a -> Vec n a;
-set_bv :: Int -> () -> BitVector -> Fin -> Bool -> BitVector
-set_bv _ _ x i b = BV (width x) $ f (unsigned x) (width x - 1 - fromEnum i)
-  where f = if b then setBit else clearBit
+--set_bv :: Int -> () -> BitVector -> Fin -> Bool -> BitVector
+--set_bv _ _ x i b = BV (width x) $ f (unsigned x) (width x - 1 - fromEnum i)
+--  where f = if b then setBit else clearBit
 
 -- | @append@ specialized to BitVector (big-endian)
 -- append :: (m n :: Nat) -> (a :: sort 0) -> Vec m a -> Vec n a -> Vec (addNat m n) a;

src/Verifier/SAW/Simulator/BitBlast.hs

@@ -231,9 +231,6 @@ beConstMap be = Map.fromList
   , ("Prelude.widthNat", Prims.widthNatOp)
   , ("Prelude.natCase", Prims.natCaseOp)
   -- Vectors
-  , ("Prelude.generate", Prims.generateOp)
-  , ("Prelude.get", getOp)
-  , ("Prelude.set", setOp)
   , ("Prelude.gen", Prims.genOp)
   , ("Prelude.at", Prims.atOp vFromLV AIG.at (lazyMux be (muxBVal be)))
   , ("Prelude.upd", Prims.updOp vFromLV (AIG.bvEq be) (AIG.bvFromInteger be) AIG.length (lazyMux be (muxBVal be)))
@@ -315,30 +312,6 @@ muxThunk be b x y = delay $ do x' <- force x; y' <- force y; muxBVal be b x' y'
 muxBExtra :: AIG.IsAIG l g => g s -> l s -> BExtra (l s) -> BExtra (l s) -> IO (BExtra (l s))
 muxBExtra _ _ _ _ = fail "Verifier.SAW.Simulator.BitBlast.iteOp: malformed arguments"
 
--- get :: (n :: Nat) -> (a :: sort 0) -> Vec n a -> Fin n -> a;
-getOp :: BValue l
-getOp =
-  constFun $
-  constFun $
-  strictFun $ \v -> return $
-  Prims.finFun $ \i ->
-    case v of
-      VVector xv -> force ((V.!) xv (fromEnum (finVal i)))
-      VWord lv -> return (vBool (AIG.at lv (fromEnum (finVal i))))
-      _ -> fail $ "Verifier.SAW.Simulator.BitBlast.getOp: expected vector, got " ++ show v
-
--- set :: (n :: Nat) -> (a :: sort 0) -> Vec n a -> Fin n -> a -> Vec n a;
-setOp :: BValue l
-setOp =
-  constFun $
-  constFun $
-  strictFun $ \v -> return $
-  Prims.finFun $ \i -> return $
-  VFun $ \y ->
-    case v of
-      VVector xv -> return $ VVector ((V.//) xv [(fromEnum (finVal i), y)])
-      _ -> fail $ "Verifier.SAW.Simulator.BitBlast.setOp: expected vector, got " ++ show v
-
 -- vZip :: (a b :: sort 0) -> (m n :: Nat) -> Vec m a -> Vec n b -> Vec (minNat m n) #(a, b);
 vZipOp :: BValue l
 vZipOp =

src/Verifier/SAW/Simulator/Concrete.hs

@@ -248,9 +248,6 @@ constMap = Map.fromList
   , ("Prelude.widthNat", Prims.widthNatOp)
   , ("Prelude.natCase", Prims.natCaseOp)
   -- Vectors
-  , ("Prelude.generate", Prims.generateOp)
-  , ("Prelude.get", getOp)
-  , ("Prelude.set", setOp)
   , ("Prelude.gen", Prims.genOp)
   , ("Prelude.at", Prims.atOp bvUnpack Prim.bvAt ite)
   , ("Prelude.upd", Prims.updOp bvUnpack (\x y -> return (Prim.bvEq undefined x y)) Prim.bv Prim.width ite)
@@ -289,30 +286,6 @@ iteOp =
   VFun $ \x -> return $
   VFun $ \y -> if toBool b then force x else force y
 
--- get :: (n :: Nat) -> (a :: sort 0) -> Vec n a -> Fin n -> a;
-getOp :: CValue
-getOp =
-  constFun $
-  constFun $
-  pureFun $ \v ->
-  Prims.finFun $ \i ->
-    case v of
-      VVector xv -> force $ (V.!) xv (fromEnum (Prim.finVal i))
-      VWord w -> return $ vBool (Prim.get_bv undefined undefined w i)
-      _ -> fail $ "Verifier.SAW.Simulator.Concrete.getOp: expected vector, got " ++ show v
-
--- set :: (n :: Nat) -> (a :: sort 0) -> Vec n a -> Fin n -> a -> Vec n a;
-setOp :: CValue
-setOp =
-  constFun $
-  constFun $
-  pureFun $ \v ->
-  Prims.finFun $ \i -> return $
-  VFun $ \y -> return $
-    case v of
-      VVector xv -> VVector ((V.//) xv [(fromEnum (Prim.finVal i), y)])
-      _ -> error $ "Verifier.SAW.Simulator.Concrete.setOp: expected vector, got " ++ show v
-
 bvUnpack :: BitVector -> V.Vector Bool
 bvUnpack x = V.generate (Prim.width x) (Prim.bvAt x)
 

src/Verifier/SAW/Simulator/Prims.hs

@@ -47,20 +47,6 @@ natFun f = strictFun g
   where g (VNat n) = f (fromInteger n)
         g _ = fail "expected Nat"
 
-vFin :: Monad m => Fin -> Value m b w e
-vFin (FinVal i j) = VCtorApp "Prelude.FinVal" $ V.fromList $ map (ready . vNat) [i, j]
-
-finFromValue :: Monad m => Value m b w e -> m Fin
-finFromValue (VCtorApp "Prelude.FinVal" (V.toList -> [x, y])) = do
-  i <- liftM natFromValue $ force x
-  j <- liftM natFromValue $ force y
-  return $ FinVal i j
-finFromValue _ = fail "finFromValue"
-
-finFun :: Monad m => (Fin -> m (Value m b w e)) -> Value m b w e
-finFun f = strictFun g
-  where g v = finFromValue v >>= f
-
 toBool :: Show e => Value m b w e -> b
 toBool (VBool b) = b
 toBool x = error $ unwords ["Verifier.SAW.Simulator.toBool", show x]
@@ -205,15 +191,6 @@ genOp =
     let g i = delay $ apply f (ready (VNat (fromIntegral i)))
     liftM VVector $ V.generateM (fromIntegral n) g
 
--- generate :: (n :: Nat) -> (e :: sort 0) -> (Fin n -> e) -> Vec n e;
-generateOp :: MonadLazy m => Value m b w e
-generateOp =
-  natFun' "generate1" $ \n -> return $
-  constFun $
-  strictFun $ \f -> do
-    let g i = delay $ apply f (ready (vFin (finFromBound (fromIntegral i) n)))
-    liftM VVector $ V.generateM (fromIntegral n) g
-
 -- zero :: (a :: sort 0) -> a;
 zeroOp :: (MonadLazy m, Show e) => (Integer -> m (Value m b w e))
        -> m (Value m b w e) -> Value m b w e -> Value m b w e