Skip to content

Commit

Permalink
Make ap a defined operation
Browse files Browse the repository at this point in the history
  • Loading branch information
robdockins committed Jan 4, 2021
1 parent dfe522a commit f5a9b9d
Show file tree
Hide file tree
Showing 2 changed files with 3 additions and 14 deletions.
4 changes: 3 additions & 1 deletion lib/Testing.cry
Original file line number Diff line number Diff line change
Expand Up @@ -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 : *
Expand Down
13 changes: 0 additions & 13 deletions src/Cryptol/Eval/Generic.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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 ->
Expand Down

0 comments on commit f5a9b9d

Please sign in to comment.