Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Prototype.hs
import Data.List
import Control.Monad
type Subst = [(String, Formula)]
(|->) :: String -> Formula -> Subst
v |-> f = [(v,f)]
data Formula = Var String
| FTrue | FFalse
| FAnd [Formula]
| FOr [Formula]
| FEquiv [Formula]
| Formula :=> Formula
| Formula :<= Formula
| Formula := Formula
| Not Formula
deriving (Eq,Ord)
match :: (MonadPlus m) => Formula -> Formula -> [(Formula,m Subst)]
match (Var p) f = [(f, return (p |-> f))]
match FFalse FFalse = [(FFalse, mzero)]
match FFalse _ = []
match FTrue FTrue = [(FTrue,mzero)]
match FTrue _ = []
match (Not f) (Not g) = map (prod Not id) $ match f g
match (FAnd fs1) (FAnd fs2) = [ matchList FAnd fs1 l | l <- permutations fs2 ]
match (FOr fs1) (FOr fs2) = [ matchList FOr fs1 l | l <- permutations fs2 ]
match (FEquiv fs1) (FEquiv fs2) = [ matchList FEquiv fs1 l | l <- permutations fs2 ]
matchList :: (MonadPlus m) => ([Formula] -> Formula ) -> [Formula] -> [Formula] -> (Formula,m Subst)
matchList cons fs1 fs2 = prod cons msum $ unzip.concat $ zipWith match fs1 fs2
prod f g (a,b) = (f a, g b)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.