Add primitive Nat-based variant of 'generate' to saw-core prelude.

GaloisInc · May 29, 2015 · 6778846 · 6778846
1 parent 9075635
commit 6778846
Show file tree

Hide file tree

Showing 5 changed files with 15 additions and 0 deletions.
diff --git a/prelude/Prelude.sawcore b/prelude/Prelude.sawcore
@@ -635,6 +635,9 @@ data Vec :: Nat -> sort 0 -> sort 0 where {
   }
 --TODO
 
+-- Primitive function for generating an array.
+gen :: (n :: Nat) -> (a :: sort 0) -> (Nat -> a) -> Vec n a;
+
 at :: (n :: Nat) -> (a :: sort 0) -> Vec n a -> Nat -> a;
 at _ _ (ConsVec a x n xs) Zero = x;
 at _ _ (ConsVec a x n xs) (Succ i) = at n a xs i;

diff --git a/src/Verifier/SAW/Simulator/BitBlast.hs b/src/Verifier/SAW/Simulator/BitBlast.hs
@@ -239,6 +239,7 @@ beConstMap be = Map.fromList
   , ("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)))
   , ("Prelude.append", Prims.appendOp vFromLV (AIG.++))

diff --git a/src/Verifier/SAW/Simulator/Concrete.hs b/src/Verifier/SAW/Simulator/Concrete.hs
@@ -256,6 +256,7 @@ constMap = Map.fromList
   , ("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)
   , ("Prelude.append", Prims.appendOp bvUnpack (Prim.append_bv undefined undefined undefined))

diff --git a/src/Verifier/SAW/Simulator/Prims.hs b/src/Verifier/SAW/Simulator/Prims.hs
@@ -238,6 +238,15 @@ natSplitFinOp =
     then VCtorApp "Prelude.Left" (V.fromList $ map ready [VType, VType, vFin (FinVal i (pred (n - i)))])
     else VCtorApp "Prelude.Right" (V.fromList $ map ready [VType, VType, vNat (i - n)])
 
+-- gen :: (n :: Nat) -> (a :: sort 0) -> (Nat -> a) -> Vec n a;
+genOp :: MonadLazy m => Value m b w e
+genOp =
+  natFun' "gen1" $ \n -> return $
+  constFun $
+  strictFun $ \f -> do
+    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 =

diff --git a/src/Verifier/SAW/Simulator/SBV.hs b/src/Verifier/SAW/Simulator/SBV.hs
@@ -119,6 +119,7 @@ constMap = Map.fromList
   , ("Prelude.generate", Prims.generateOp)
   , ("Prelude.get", getOp)
   , ("Prelude.set", setOp)
+  , ("Prelude.gen", Prims.genOp)
   , ("Prelude.at", Prims.atOp svUnpack svAt (lazyMux muxBVal))
   , ("Prelude.upd", Prims.updOp svUnpack (\x y -> return (svEqual x y)) literalSWord svBitSize (lazyMux muxBVal))
   , ("Prelude.append", Prims.appendOp svUnpack svJoin)