swh:1:snp:aeaf3dbb58f5be84b565e73b5ade1503ee8cb6d6
Tip revision: b6407e0f026cf5491ca5ed0a35ea5cf316ebe8ca authored by Anish Tondwalkar on 21 May 2021, 03:15:25 UTC
formatted for submission
formatted for submission
Tip revision: b6407e0
shillSet.hs
-- The Shill example from the BRTs paper
-- Ulitmately this should be written with a map of sets, but let's do it
-- with just sets first and see how that goes.
-- | The API
-- Caps: lst, lookup (do we need this?), contents, read, create, write
-- Monad interface: pure, bind, thenn
measure mNil :: List [] -> Bool
measure mCons :: List [] -> Bool
measure mLength :: List [] -> Int
empty as rforall a. x:(List <a) -> {v: Bool | v == mNil x}
empty = (0)
nil as rforall a. {v: List <a | (mNil v) /\ (mLength v = 0)}
nil = (0)
cons as rforall a. x:a -> xs:(List <a) -> {v: List <a | (mCons v) /\ (mLength v = mLength xs + 1)}
cons = (0)
write as lstSet:(Set >Int) ~> lookupSet:(Set >Int) ~> contentsSet:(Set >Int) ~> readSet:(Set >Int) ~> createSet:(Set >Int) ~> writeSet:(Set >Int) ~>
f:{v:Int | v ∈ writeSet} -> (String) ->
Shill
<{v:Set >Int | v == lstSet} <{v:Set >Int | v == lookupSet} <{v:Set >Int | v == contentsSet} <{v:Set >Int | v == readSet} <{v:Set >Int | v == createSet} <{v:Set >Int | v == writeSet}
>{v:Set >Int | v == lstSet} >{v:Set >Int | v == lookupSet} >{v:Set >Int | v == contentsSet} >{v:Set >Int | v == readSet} >{v:Set >Int | v == createSet} >{v:Set >Int | v == writeSet}
>Unit
write = 0
read as lstSet:(Set >Int) ~> lookupSet:(Set >Int) ~> contentsSet:(Set >Int) ~> readSet:(Set >Int) ~> createSet:(Set >Int) ~> writeSet:(Set >Int) ~>
f:{v:Int | v ∈ readSet} ->
Shill
<{v:Set >Int | v == lstSet} <{v:Set >Int | v == lookupSet} <{v:Set >Int | v == contentsSet} <{v:Set >Int | v == readSet} <{v:Set >Int | v == createSet} <{v:Set >Int | v == writeSet}
>{v:Set >Int | v == lstSet} >{v:Set >Int | v == lookupSet} >{v:Set >Int | v == contentsSet} >{v:Set >Int | v == readSet} >{v:Set >Int | v == createSet} >{v:Set >Int | v == writeSet}
>String
read = 0
-- Does this rforall correctly capture the fact that we inherit permissions?
-- lst as rforall a. lstSet:(Set >Int) ~> lookupSet:(Set >Int) ~> contentsSet:(Set >Int) ~> readSet:(Set >Int) ~> createSet:(Set >Int) ~> writeSet:(Set >Int) ~>
-- d:{v:a | v ∈ lstSet} ->
-- Shill
-- <{v:Set >Int | v == lstSet} <{v:Set >Int | v == lookupSet} <{v:Set >Int | v == contentsSet} <{v:Set >Int | v == readSet} <{v:Set >Int | v == createSet} <{v:Set >Int | v == writeSet}
-- >{v:Set >Int | v == lstSet} >{v:Set >Int | v == lookupSet} >{v:Set >Int | v == contentsSet} >{v:Set >Int | v == readSet} >{v:Set >Int | v == createSet} >{v:Set >Int | v == writeSet}
-- >(List >a)
-- lst = 0
-- this is what is called createWO
create as rforall a. lstSet:(Set >Int) ~> lookupSet:(Set >Int) ~> contentsSet:(Set >Int) ~> readSet:(Set >Int) ~> createSet:(Set >Int) ~> writeSet:(Set >Int) ~>
d:{v:a | v ∈ createSet} ->
Shill
<{v:Set >Int | v == lstSet} <{v:Set >Int | v == lookupSet} <{v:Set >Int | v == contentsSet} <{v:Set >Int | v == readSet} <{v:Set >Int | v == createSet} <{v:Set >Int | v == writeSet}
>{v:Set >Int | v == lstSet} >{v:Set >Int | v == lookupSet} >{v:Set >Int | v == contentsSet} >{v:Set >Int | v == readSet} >{v:Set >Int | v == createSet} >{v:Set >Int | v == setPlus writeSet d}
>a
create = 0
pure as rforall a. lstSet:(Set >Int) ~> lookupSet:(Set >Int) ~> contentsSet:(Set >Int) ~> readSet:(Set >Int) ~> createSet:(Set >Int) ~> writeSet:(Set >Int) ~>
x:a ->
Shill
<{v:Set >Int | v == lstSet} <{v:Set >Int | v == lookupSet} <{v:Set >Int | v == contentsSet} <{v:Set >Int | v == readSet} <{v:Set >Int | v == createSet} <{v:Set >Int | v == writeSet}
>{v:Set >Int | v == lstSet} >{v:Set >Int | v == lookupSet} >{v:Set >Int | v == contentsSet} >{v:Set >Int | v == readSet} >{v:Set >Int | v == createSet} >{v:Set >Int | v == writeSet}
>a
pure = 0
bind as rforall a, b .
lstSet1:(Set >Int) ~> lookupSet1:(Set >Int) ~> contentsSet1:(Set >Int) ~> readSet1:(Set >Int) ~> createSet1:(Set >Int) ~> writeSet1:(Set >Int) ~>
lstSet2:(Set >Int) ~> lookupSet2:(Set >Int) ~> contentsSet2:(Set >Int) ~> readSet2:(Set >Int) ~> createSet2:(Set >Int) ~> writeSet2:(Set >Int) ~>
lstSet3:(Set >Int) ~> lookupSet3:(Set >Int) ~> contentsSet3:(Set >Int) ~> readSet3:(Set >Int) ~> createSet3:(Set >Int) ~> writeSet3:(Set >Int) ~>
(Shill
<{v:Set >Int | v == lstSet1} <{v:Set >Int | v == lookupSet1} <{v:Set >Int | v == contentsSet1} <{v:Set >Int | v == readSet1} <{v:Set >Int | v == createSet1} <{v:Set >Int | v == writeSet1}
>{v:Set >Int | v == lstSet2} >{v:Set >Int | v == lookupSet2} >{v:Set >Int | v == contentsSet2} >{v:Set >Int | v == readSet2} >{v:Set >Int | v == createSet2} >{v:Set >Int | v == writeSet2}
>a) ->
(x:a -> Shill
<{v:Set >Int | v == lstSet2} <{v:Set >Int | v == lookupSet2} <{v:Set >Int | v == contentsSet2} <{v:Set >Int | v == readSet2} <{v:Set >Int | v == createSet2} <{v:Set >Int | v == writeSet2}
>{v:Set >Int | v == lstSet3} >{v:Set >Int | v == lookupSet3} >{v:Set >Int | v == contentsSet3} >{v:Set >Int | v == readSet3} >{v:Set >Int | v == createSet3} >{v:Set >Int | v == writeSet3}
>b) ->
Shill
<{v:Set >Int | v == lstSet1} <{v:Set >Int | v == lookupSet1} <{v:Set >Int | v == contentsSet1} <{v:Set >Int | v == readSet1} <{v:Set >Int | v == createSet1} <{v:Set >Int | v == writeSet1}
>{v:Set >Int | v == lstSet3} >{v:Set >Int | v == lookupSet3} >{v:Set >Int | v == contentsSet3} >{v:Set >Int | v == readSet3} >{v:Set >Int | v == createSet3} >{v:Set >Int | v == writeSet3}
>b
bind = 0
thenn as rforall a, b .
lstSet1:(Set >Int) ~> lookupSet1:(Set >Int) ~> contentsSet1:(Set >Int) ~> readSet1:(Set >Int) ~> createSet1:(Set >Int) ~> writeSet1:(Set >Int) ~>
lstSet2:(Set >Int) ~> lookupSet2:(Set >Int) ~> contentsSet2:(Set >Int) ~> readSet2:(Set >Int) ~> createSet2:(Set >Int) ~> writeSet2:(Set >Int) ~>
lstSet3:(Set >Int) ~> lookupSet3:(Set >Int) ~> contentsSet3:(Set >Int) ~> readSet3:(Set >Int) ~> createSet3:(Set >Int) ~> writeSet3:(Set >Int) ~>
(Shill
<{v:Set >Int | v == lstSet1} <{v:Set >Int | v == lookupSet1} <{v:Set >Int | v == contentsSet1} <{v:Set >Int | v == readSet1} <{v:Set >Int | v == createSet1} <{v:Set >Int | v == writeSet1}
>{v:Set >Int | v == lstSet2} >{v:Set >Int | v == lookupSet2} >{v:Set >Int | v == contentsSet2} >{v:Set >Int | v == readSet2} >{v:Set >Int | v == createSet2} >{v:Set >Int | v == writeSet2}
>a) ->
(Shill
<{v:Set >Int | v == lstSet2} <{v:Set >Int | v == lookupSet2} <{v:Set >Int | v == contentsSet2} <{v:Set >Int | v == readSet2} <{v:Set >Int | v == createSet2} <{v:Set >Int | v == writeSet2}
>{v:Set >Int | v == lstSet3} >{v:Set >Int | v == lookupSet3} >{v:Set >Int | v == contentsSet3} >{v:Set >Int | v == readSet3} >{v:Set >Int | v == createSet3} >{v:Set >Int | v == writeSet3}
>b) ->
Shill
<{v:Set >Int | v == lstSet1} <{v:Set >Int | v == lookupSet1} <{v:Set >Int | v == contentsSet1} <{v:Set >Int | v == readSet1} <{v:Set >Int | v == createSet1} <{v:Set >Int | v == writeSet1}
>{v:Set >Int | v == lstSet3} >{v:Set >Int | v == lookupSet3} >{v:Set >Int | v == contentsSet3} >{v:Set >Int | v == readSet3} >{v:Set >Int | v == createSet3} >{v:Set >Int | v == writeSet3}
>b
thenn = 0
-- should be in the monad
isFile as f:Int -> Bool
isFile = 0
isDir as f:Int -> Bool
isDir = 0
-- NEXT: forShill
-- Hmm, I think forShill needs to enforece that @f@ is monotonic and return
-- a monotonically larger world in order to account for creation, but the
-- BRTs example simply returns a world over which all the same predicates
-- hold, so let's try that first
--
-- Actually, this doesn't seem to work, so let's do it with subsets, but
-- let's do the inside of that loop first
forShill as rforall a, b, c, d, e, f, g, h.
lstSet:(Set >Int) ~> lookupSet:(Set >Int) ~> contentsSet:(Set >Int) ~> readSet:(Set >Int) ~> createSet:(Set >Int) ~> writeSet:(Set >Int) ~>
(lstSet2:{v: Set >Int | setSubset lstSet v} ~> lookupSet2:{v: Set >Int | setSubset lookupSet v} ~> contentsSet2:{v: Set >Int | setSubset contentsSet v} ~> readSet2:{v: Set >Int | setSubset readSet v} ~> createSet2:{v: Set >Int | setSubset createSet v} ~> writeSet2:{v: Set >Int | setSubset writeSet v} ~>
x:a ->
Shill
<{v:Set >Int | v == lstSet2} <{v:Set >Int | v == lookupSet2} <{v:Set >Int | v == contentsSet2} <{v:Set >Int | v == readSet2} <{v:Set >Int | v == createSet2} <{v:Set >Int | v == writeSet2}
>{v:Set >Int | setSubset lstSet2 v} >{v:Set >Int | setSubset lookupSet2 v} >{v:Set >Int | setSubset contentsSet2 v} >{v:Set >Int | setSubset readSet2 v} >{v:Set >Int | setSubset createSet2 v} >{v:Set >Int | setSubset writeSet2 v}
>h) ->
List >a ->
Shill
<{v:Set >Int | v == lstSet} <{v:Set >Int | v == lookupSet} <{v:Set >Int | v == contentsSet} <{v:Set >Int | v == readSet} <{v:Set >Int | v == createSet} <{v:Set >Int | v == writeSet}
>{v:Set >Int | setSubset lstSet v} >{v:Set >Int | setSubset lookupSet v} >{v:Set >Int | setSubset contentsSet v} >{v:Set >Int | setSubset readSet v} >{v:Set >Int | setSubset createSet v} >{v:Set >Int | setSubset writeSet v}
>h
-- We can implement forShill using Lists (see append.hs)
forShill = 0
undefined as rforall a . a
undefined = 0
-- why does this fail? do we not encode bools properly?
and as a:Bool -> b:Bool -> {v:Bool | v == a /\ b}
and = \a -> \b -> if a == True then (if b == True then True else False) else False
-- The "Client"
-- copyRec :: lstSet:(Set >Int) ~> lookupSet:(Set >Int) ~> contentsSet:(Set >Int) ~> readSet:(Set >Int) ~> createSet:(Set >Int) ~> writeSet:(Set >Int) ~>
-- f:{v:Int | v ∈ lstSet /\ v ∈ lookupSet /\ v ∈ readSet} ->
-- t:{v:Int | v ∈ createSet /\ v ∈ writeSet} ->
-- Shill
-- <{v:(Set >Int) | v == lstSet} <{v:(Set >Int) | v == lookupSet} <{v:(Set >Int) | v == contentsSet} <{v:(Set >Int) | v == readSet} <{v:(Set >Int) | v == createSet} <{v:(Set >Int) | v == writeSet}
-- >{v:(Set >Int) | setSubset lstSet v} >{v:(Set >Int) | setSubset lookupSet v} >{v:(Set >Int) | setSubset contentsSet v} >{v:(Set >Int) | setSubset readSet v} >{v:(Set >Int) | setSubset createSet v} >{v:(Set >Int) | setSubset writeSet v}
-- >Unit -- This should return a Unit, but we don't have a value-level unit terms
-- copyRec = \f -> \t -> bind (read f) (write t)
-- doesn't work:
-- copyRec = \f -> \t -> bind (lst f) (\x -> (forShill x (\y -> pure 0)))
-- works:
-- copyRec = \f -> \t -> bind (lst f) (\x -> pure 0)
-- oops, copyRec is a BRTs invention. Let's do `find` from the shill papers
-- find :: lstSet:(Set >Int) ~> lookupSet:(Set >Int) ~> contentsSet:(Set >Int) ~> readSet:(Set >Int) ~> createSet:(Set >Int) ~> writeSet:(Set >Int) ~>
-- ({v:Int | v ∈ lstSet /\ v ∈ lookupSet /\ v ∈ readSet} -> Bool) ->
-- cur:{v:Int | v ∈ lstSet /\ v ∈ lookupSet /\ v ∈ readSet} ->
-- Shill
-- <{v:Set >Int | v == lstSet} <{v:Set >Int | v == lookupSet} <{v:Set >Int | v == contentsSet} <{v:Set >Int | v == readSet} <{v:Set >Int | v == createSet} <{v:Set >Int | v == writeSet}
-- >{v:Set >Int | setSubset lstSet v} >{v:Set >Int | setSubset lookupSet v} >{v:Set >Int | setSubset contentsSet v} >{v:Set >Int | setSubset readSet v} >{v:Set >Int | setSubset createSet v} >{v:Set >Int | setSubset writeSet v}
-- >Int -- This should return a Unit, but we don't have a value-level unit terms
-- find = \lstSet ~> \lookupSet ~> \filter -> \f -> if and (isFile f) (filter f)
-- then pure f
-- else (if (isDir f)
-- then (bind (lst f)
-- (let finder :: lstSetAnn:(Set >Int) ~> lookupSetAnn:(Set >Int) ~> contentsSetAnn:(Set >Int) ~> readSetAnn:(Set >Int) ~> createSetAnn:(Set >Int) ~> writeSetAnn:(Set >Int) ~>
-- cur:{v:Int | v ∈ lstSetAnn /\ v ∈ lookupSetAnn /\ v ∈ readSetAnn} ->
-- Shill <{v:Set >Int | v == lstSetAnn} <{v:Set >Int | v == lookupSetAnn} <{v:Set >Int | v == contentsSetAnn} <{v:Set >Int | v == readSetAnn} <{v:Set >Int | v == createSetAnn} <{v:Set >Int | v == writeSetAnn}
-- >{v:Set >Int | setSubset lstSetAnn v} >{v:Set >Int | setSubset lookupSetAnn v} >{v:Set >Int | setSubset contentsSetAnn v} >{v:Set >Int | setSubset readSetAnn v} >{v:Set >Int | setSubset createSetAnn v} >{v:Set >Int | setSubset writeSetAnn v}
-- >Int
-- = (find filter) in forShill finder))
-- else (pure 0))
-- find
-- :: lstSet:(Set >Int) ~> lookupSet:(Set >Int) ~> contentsSet:(Set >Int) ~> readSet:(Set >Int) ~> createSet:(Set >Int) ~> writeSet:(Set >Int)
-- ~> (Int -> Bool)
-- -> cur:{v:Int | v ∈ lstSet /\ v ∈ lookupSet /\ v ∈ readSet}
-- -> Shill <{v:Set >Int | v == lstSet} <{v:Set >Int | v == lookupSet} <{v:Set >Int | v == contentsSet} <{v:Set >Int | v == readSet} <{v:Set >Int | v == createSet} <{v:Set >Int | v == writeSet}
-- >{v:Set >Int | setSubset lstSet v} >{v:Set >Int | setSubset lookupSet v} >{v:Set >Int | setSubset contentsSet v} >{v:Set >Int | setSubset readSet v} >{v:Set >Int | setSubset createSet v} >{v:Set >Int | setSubset writeSet v}
-- >Int
-- find = \lstSet ~> \lookupSet ~> \contentsSet ~> \readSet ~> \createSet ~> \writeSet ~>
-- \filter -> \f ->
-- if and (isFile f) (filter f)
-- then pure f
-- else (if (isDir f)
-- then (let finder
-- :: lstSetAnn:{v: Set >Int | setSubset lstSet v} ~> lookupSetAnn:{v: Set >Int | setSubset lookupSet v} ~> contentsSetAnn:{v: Set >Int | setSubset contentsSet v} ~> readSetAnn:{v: Set >Int | setSubset readSet v} ~> createSetAnn:{v: Set >Int | setSubset createSet v} ~> writeSetAnn:{v: Set >Int | setSubset writeSet v}
-- ~> cur:{v:Int | v ∈ lstSetAnn /\ v ∈ lookupSetAnn /\ v ∈ readSetAnn}
-- -> Shill
-- <{v:Set >Int | v == lstSetAnn} <{v:Set >Int | v == lookupSetAnn} <{v:Set >Int | v == contentsSetAnn} <{v:Set >Int | v == readSetAnn} <{v:Set >Int | v == createSetAnn} <{v:Set >Int | v == writeSetAnn}
-- >{v:Set >Int | setSubset lstSetAnn v} >{v:Set >Int | setSubset lookupSetAnn v} >{v:Set >Int | setSubset contentsSetAnn v} >{v:Set >Int | setSubset readSetAnn v} >{v:Set >Int | setSubset createSetAnn v} >{v:Set >Int | setSubset writeSetAnn v}
-- >Int
-- = (find filter) in forShill finder empty)
-- else pure 0)
lst
as lstSet:(Set >Int) ~> lookupSet:(Set >Int) ~> contentsSet:(Set >Int) ~> readSet:(Set >Int) ~> createSet:(Set >Int) ~> writeSet:(Set >Int)
~> lstSetOut:{v: Set >Int | setSubset lstSet v} ~> lookupSetOut:{v: Set >Int | setSubset lookupSet v} ~> contentsSetOut:{v: Set >Int | setSubset contentsSet v} ~> readSetOut:{v: Set >Int | setSubset readSet v} ~> createSetOut:{v: Set >Int | setSubset createSet v} ~> writeSetOut:{v: Set >Int | setSubset writeSet v}
~> dir:{v:Int | v ∈ lstSet}
-> Shill
<{v:Set >Int | v == lstSet} <{v:Set >Int | v == lookupSet} <{v:Set >Int | v == contentsSet} <{v:Set >Int | v == readSet} <{v:Set >Int | v == createSet} <{v:Set >Int | v == writeSet}
>{v:Set >Int | v == lstSetOut} >{v:Set >Int | v == lookupSetOut} >{v:Set >Int | v == contentsSetOut} >{v:Set >Int | v == readSetOut} >{v:Set >Int | v == createSetOut} >{v:Set >Int | v == writeSetOut}
>{v: Int | ((dir ∈ lstSet) => (v ∈ lstSetOut)) /\ ((dir ∈ lookupSet) => (v ∈ lookupSetOut)) /\ ((dir ∈ contentsSet) => (v ∈ contentsSetOut)) /\ ((dir ∈ readSet) => (v ∈ readSetOut)) /\ ((dir ∈ createSet) => (v ∈ createSetOut)) /\ ((dir ∈ writeSet) => (v ∈ writeSetOut))}
lst = 0
find
:: (Int -> Bool)
-> lstSet:(Set >Int) ~> lookupSet:(Set >Int) ~> contentsSet:(Set >Int) ~> readSet:(Set >Int) ~> createSet:(Set >Int) ~> writeSet:(Set >Int)
~> f:{v:Int | v ∈ lstSet /\ v ∈ lookupSet /\ v ∈ readSet}
-> Shill
<{v:Set >Int | v == lstSet} <{v:Set >Int | v == lookupSet} <{v:Set >Int | v == contentsSet} <{v:Set >Int | v == readSet} <{v:Set >Int | v == createSet} <{v:Set >Int | v == writeSet}
>{v:Set >Int | setSubset lstSet v} >{v:Set >Int | setSubset lookupSet v} >{v:Set >Int | setSubset contentsSet v} >{v:Set >Int | setSubset readSet v} >{v:Set >Int | setSubset createSet v} >{v:Set >Int | setSubset writeSet v}
>Int
find =
\filter -> \f ->
if and (isFile f) (filter f)
then pure f
else (if (isDir f)
then bind (lst f) (find filter)
else pure 0)
-- CURRENT ATTEMPT
--------------------------------------------------------------------------------
-- lst
-- as lstSet:(Set >Int) ~> lookupSet:(Set >Int) ~> contentsSet:(Set >Int) ~> readSet:(Set >Int) ~> createSet:(Set >Int) ~> writeSet:(Set >Int)
-- ~> lstSetOut:{v: Set >Int | setSubset lstSet v} ~> lookupSetOut:{v: Set >Int | setSubset lookupSet v} ~> contentsSetOut:{v: Set >Int | setSubset contentsSet v} ~> readSetOut:{v: Set >Int | setSubset readSet v} ~> createSetOut:{v: Set >Int | setSubset createSet v} ~> writeSetOut:{v: Set >Int | setSubset writeSet v}
-- ~> dir:{v:Int | v ∈ lstSet}
-- -> Shill
-- <{v:Set >Int | v == lstSet} <{v:Set >Int | v == lookupSet} <{v:Set >Int | v == contentsSet} <{v:Set >Int | v == readSet} <{v:Set >Int | v == createSet} <{v:Set >Int | v == writeSet}
-- >{v:Set >Int | v == lstSetOut} >{v:Set >Int | v == lookupSetOut} >{v:Set >Int | v == contentsSetOut} >{v:Set >Int | v == readSetOut} >{v:Set >Int | v == createSetOut} >{v:Set >Int | v == writeSetOut}
-- >(List >{v: Int | ((dir ∈ lstSet) => (v ∈ lstSetOut)) /\ ((dir ∈ lookupSet) => (v ∈ lookupSetOut)) /\ ((dir ∈ contentsSet) => (v ∈ contentsSetOut)) /\ ((dir ∈ readSet) => (v ∈ readSetOut)) /\ ((dir ∈ createSet) => (v ∈ createSetOut)) /\ ((dir ∈ writeSet) => (v ∈ writeSetOut))})
-- lst = 0
-- find
-- :: (Int -> Bool)
-- -> lstSet:(Set >Int) ~> lookupSet:(Set >Int) ~> contentsSet:(Set >Int) ~> readSet:(Set >Int) ~> createSet:(Set >Int) ~> writeSet:(Set >Int)
-- ~> f:{v:Int | v ∈ lstSet /\ v ∈ lookupSet /\ v ∈ readSet}
-- -> Shill
-- <{v:Set >Int | v == lstSet} <{v:Set >Int | v == lookupSet} <{v:Set >Int | v == contentsSet} <{v:Set >Int | v == readSet} <{v:Set >Int | v == createSet} <{v:Set >Int | v == writeSet}
-- >{v:Set >Int | setSubset lstSet v} >{v:Set >Int | setSubset lookupSet v} >{v:Set >Int | setSubset contentsSet v} >{v:Set >Int | setSubset readSet v} >{v:Set >Int | setSubset createSet v} >{v:Set >Int | setSubset writeSet v}
-- >Int
-- find =
-- \filter -> \f ->
-- if and (isFile f) (filter f)
-- then pure f
-- else (if (isDir f)
-- then bind (lst f) (forShill (find filter))
-- else pure 0)