I am working on a haskell program that includes these data type definitions as part of this:
data Term t (deriving Eq) where Con :: a -> Term a And :: Term Bool -> Term Bool -> Term Bool Or :: Term Bool -> Term Bool -> Term Bool Smaller :: Term Int -> Term Int -> Term Bool Plus :: Term Int -> Term Int -> Term Int
And the data is Formula ts, where
data Formula ts where Body :: Term Bool -> Formula () Forall :: Show a => [a] -> (Term a -> Formula as) -> Formula (a, as)
as well as an eval function that evaluates each Term t as:
eval :: Term t -> t eval (Con i) =i eval (And pq)=eval p && eval q eval (Or pq)=eval p || eval q eval(Smaller nm)=eval n < eval m eval (Plus nm) = eval n + eval m
And the following function, which checks whether the Formula is satisfactory for any possible substitution of values:
satisfiable :: Formula ts -> Bool satisfiable (Body( sth ))=eval sth satisfiable (Forall xs f) = any (satisfiable . f . Con) xs
Now I was asked to write a solution function that solves this Formula:
solutions :: Formula ts -> [ts]
In addition, I have the following Formulas as test examples that expect my solution to behave as follows:
ex1 :: Formula () ex1 = Body (Con True) ex2 :: Formula (Int, ()) ex2 = Forall [1..10] $ \n -> Body $ n `Smaller` (n `Plus` Con 1) ex3 :: Formula (Bool, (Int, ())) ex3 = Forall [False, True] $ \p -> Forall [0..2] $ \n -> Body $ p `Or` (Con 0 `Smaller` n)
the solution function should be returned:
*Solver>solutions ex1 [()] *Solver> solutions ex2 [(1,()),(2,()),(3,()),(4,()),(5,()),(6,()),(7,()),(8,()),(9,()),(10,())] *Solver> solutions ex3 [(False,(1,())),(False,(2,())),(True,(0,())),(True,(1,())),(True,(2,()))]
My code for this function so far:
solutions :: Formula ts -> [ts] solutions(Body(sth))|satisfiable (Body( sth ))=[()] |otherwise=[] solutions(Forall [a] f)|(satisfiable (Forall [a] f))=[(a,(helper $(f.Con) a) )] |otherwise=[] solutions(Forall (a:as) f)=solutions(Forall [a] f)++ solutions(Forall as f)
and auxiliary function:
helper :: Formula ts -> ts helper (Body(sth))|satisfiable (Body( sth ))=() helper (Forall [a] f)|(satisfiable (Forall [a] f))=(a,((helper.f.Con) a) )
Finally, here is my question: with this solution function, I can solve formulas that are either ex1 or ex2 without any problems, but the problem is that I cannot solve ex3. assuming my function does not work with formulas that include nested "Forall" s. Any help with how I can do this would be appreciated, thanks in advance.