A prototype implementation of generating set functions as presented in Synthesizing Set Functions.
Execute cypm install
(due to a bug in KiCS2, only PAKCS is currently supported). This installs the executable synsetfun
in the bin directory of CPM.
For an existing Curry Module Examples.curry
module Examples where
anyOf :: [Int] -> Int
:xs) = x ? anyOf xs anyOf (x
the command
synsetfun Examples -f anyOf
generates the output
instance NF t0 => NF (STList t0) where
=
nf v9 case v9 of
STNil -> Val STNil
STCons v10 v11 ->
case nfST v10 of
Choice v12 v13 v14 -> Choice v12 (nf (STCons v13 v11)) (nf (STCons v14 v11))
Fail -> Fail
->
v15 case nfST v11 of
Choice v16 v17 v18 -> Choice v16 (nf (STCons v15 v17)) (nf (STCons v15 v18))
Fail -> Fail
-> Val (STCons v15 v19)
v19
data STList t0 = STNil | STCons (ST t0) (ST (STList t0))
choiceP :: IDSupply -> ST t0 -> ST t0 -> ST t0
= Choice v1 v_1 v_2 where v1 = uniqueID v2
choiceP v2 v_1 v_2
anyOfP :: IDSupply -> ST (STList Int) -> ST Int
= applyST
anyOfP v6 v_1 -> case v0 of
(\v0 STCons v_2 v_3 -> choiceP v5 v_2 (anyOfP v4 v_3)
STNil -> Fail
)
v_1where
= rightSupply v6
v5 = leftSupply v6
v7 = rightSupply v7
v4
toValST_List_STList :: (t0 -> ST t1) -> [t0] -> STList t1
= STNil
toValST_List_STList v20 [] : v23) =
toValST_List_STList v21 (v22 STCons (v21 v22) (toST_List_STList v21 v23)
fromValST_List_STList :: (t0 -> t1) -> STList t0 -> [t1]
STNil = []
fromValST_List_STList v24 STCons (Val v26) (Val v27)) =
fromValST_List_STList v25 (: fromValST_List_STList v25 v27
v25 v26
toST_List_STList :: (t0 -> ST t1) -> [t0] -> ST (STList t1)
= Uneval . toValST_List_STList v28
toST_List_STList v28
fromST_List_STList :: NF t0 => (t0 -> t1) -> ST (STList t0) -> Values [t1]
= map (fromValST_List_STList v29) . stValues
fromST_List_STList v29
toValST_Int_Int :: Int -> Int
= id
toValST_Int_Int
fromValST_Int_Int :: Int -> Int
= id
fromValST_Int_Int
toST_Int_Int :: Int -> ST Int
= Uneval . toValST_Int_Int
toST_Int_Int
fromST_Int_Int :: ST Int -> Values Int
= map fromValST_Int_Int . stValues
fromST_Int_Int
anyOfS :: [Int] -> Values Int
=
anyOfS v30 fromST_Int_Int (anyOfP initSupply (toST_List_STList toST_Int_Int v30))
Adding the output to the original file and importing the ST
library should yield the synthesized set function.
Not supported (yet): * Sharing and nested set functions * Polymorphic set functions * Higher-order functions * Type synonyms * External functions * Record types * Everything else that doesn’t work 🙂