From f5a9b9d9617029776b527889e0947e64a44f4135 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Mon, 4 Jan 2021 12:36:24 -0800 Subject: [PATCH] Make `ap` a defined operation --- lib/Testing.cry | 4 +++- src/Cryptol/Eval/Generic.hs | 13 ------------- 2 files changed, 3 insertions(+), 14 deletions(-) diff --git a/lib/Testing.cry b/lib/Testing.cry index ab6f27364..de8e22588 100644 --- a/lib/Testing.cry +++ b/lib/Testing.cry @@ -12,9 +12,11 @@ primitive runGen : {a} [8] -> [256] -> Gen a -> a primitive return : {a} a -> Gen a primitive (>>=) : {a,b} Gen a -> (a -> Gen b) -> Gen b primitive (<$>) : {a,b} (a -> b) -> Gen a -> Gen b -primitive (<*>) : {a,b} Gen (a -> b) -> Gen a -> Gen b primitive genStream : {a} Gen a -> Gen ([inf]a) +(<*>) : {a,b} Gen (a -> b) -> Gen a -> Gen b +(<*>) mf mx = mf >>= \f -> f <$> mx + primitive withSize : {a} [8] -> Gen a -> Gen a // primitive type RandGen : * diff --git a/src/Cryptol/Eval/Generic.hs b/src/Cryptol/Eval/Generic.hs index 849a58095..61a9aca54 100644 --- a/src/Cryptol/Eval/Generic.hs +++ b/src/Cryptol/Eval/Generic.hs @@ -2366,19 +2366,6 @@ testingPrims sym = Map.fromList $ map (\(n, v) -> (testingPrim n, v)) prims x <- m' sGenLift sym (f' (pure x)) - , "<*>" ~> - PTyPoly \_a -> - PTyPoly \_b -> - PFun \mf -> - PFun \m -> - PPrim - do mf' <- fromVGen <$> mf - m' <- fromVGen <$> m - pure $ VGen do - f <- fromVFun sym <$> mf' - x <- m' - sGenLift sym (f (pure x)) - , ">>=" ~> PTyPoly \_a -> PTyPoly \_b ->