GMP.GradedML.hs revision 61b020f416f2204caf544da16d97b9955148b53e
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach{-# OPTIONS -fglasgow-exts #-}
08ea5f703d2e034f347a7e30ee3cca8a127d9c0eChristian Maedermodule GradedML where
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachdata GMLrules = GMLR [Int] [Int]
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder-- negative coeff first, positive after
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachdata Coeffs = Coeffs [Int] [Int]
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach deriving (Eq, Ord)
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reillyinstance ModalLogic GML GMLrules where
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly-- orderIns _ = True
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly flagML _ = Ang
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly parseIndex = do n <- natural
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly return $ GML (fromInteger n)
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly matchR r = let (q, w) = eccContent r
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly wrapR (x,y) = GMLR x y
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly in map wrapR (ineqSolver q (2^w))
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly guessClause (GMLR n p) =
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly let zn = zip n [1..]
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly zp = zip p [1+length n..]
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly f l x = let aux = psplit l ((sum.fst.unzip.fst) x)
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly in assoc aux ((snd.unzip.fst) x,(snd.unzip.snd) x)
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly in concat (map (f zp) (split zn))
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly-------------------------------------------------------------------------------
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly{- associate the elements of l with x
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly - @ param l : list of pairs of lists of integers
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly - @ param u : pair of lists of integers
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly - @ return : list of propositional clauses (associated and wrapped lists) -}
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reillyassoc :: [([Int], [Int])] -> ([Int], [Int]) -> [PropClause]
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reillyassoc l u = map ((\x y -> Pimplies ((snd x)++(snd y)) ((fst x)++(fst y))) u) l
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly{- spliting function
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly - @ param l : list to be split
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach - @ return : all pairs of lists which result by spliting l -}
bcd914850de931848b86d7728192a149f9c0108bChristian Maedersplit :: [a] -> [([a], [a])]
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder [] -> [([],[])]
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder h:t -> let x = split t
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder in [(h:(fst q),snd q)|q <- x] ++ [(fst q,h:(snd q))|q <- x]
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly{- splitting function for positive coefficients
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly - @ param l : list to be split
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'Reilly - @ param s : sum of the current to be counted elements (the ones in J)
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder - @ return : all pairs of indexes of positive coefficients which are good -}
bcd914850de931848b86d7728192a149f9c0108bChristian Maederpsplit :: (Num a, Ord a) => [(a, b)] -> a -> [([b], [b])]
d3c9318c22fcf44d9135a3b2c64f880b9a785babChristian Maeder then case l of
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly [] -> [([],[])]
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly h:t -> if (s + (fst h) < 0)
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder then let aux1 = psplit t (s + (fst h))
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly aux2 = psplit t s
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder in [((snd h):(fst q),snd q)|q <- aux1] ++
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder [(fst q,(snd h):(snd q))|q <- aux2]
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder else let aux = psplit t s
f284db6f4dffd7bf60b82319648efb7bcb9378c9Christian Maeder in [(fst q,(snd h):(snd q))|q <- aux]
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder{- compute the size of a number as specified in the paper
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder - @ param i : the given integer
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett - @ return : the size of i -}
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reillysize :: Int -> Int
90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblettsize i = ceiling (logBase 2 (fromIntegral (abs i + 1)) :: Double)
2650e8a56cc2381719bd2390fdf82402e0c696d8Christian Maeder{- extract the content of the contracted clause
2650e8a56cc2381719bd2390fdf82402e0c696d8Christian Maeder - @ param (Mimplies n p) : contracted clause
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder - @ return : the grade of the equivalent modal applications in the input param
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly - and the length of the inequality
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly - left: negative signed grades; right: positive signed grades -}
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian MaedereccContent :: ModClause GML -> (Coeffs, Int)
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaedereccContent (Mimplies n p) =
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly let getGrade x =
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Mapp (Mop (GML i) Angle) _ -> i
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder l1 = map (\x -> - x - 1) (map getGrade n) -- coeff for negative r_i
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder l2 = map getGrade p -- coeff for positive r_i
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder w = 1 + (length l1) + (length l2) + sum (map size l1) + sum (map size l2)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly in (Coeffs l1 l2, w)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly-------------------------------------------------------------------------------
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly{- generate all lists of given length and with elements between 1 and a limit
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder - @ param n : fixed length
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly - @ param lim : upper limit of elements
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder - @ return : a list of all lists described above -}
842ae753ab848a8508c4832ab64296b929167a97Christian MaedernegCands :: Int -> Int -> [[Int]]
842ae753ab848a8508c4832ab64296b929167a97Christian MaedernegCands n lim =
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly _ -> [i:l| i <- [1..lim], l <- negCands (n-1) lim]
67e234eb781dd16dfd269486befd2b5781075079Christian Maeder{- generate all lists of given length with elems between 1 and a limit such
67e234eb781dd16dfd269486befd2b5781075079Christian Maeder - that the side condition of Graded ML rule is satisfied
67e234eb781dd16dfd269486befd2b5781075079Christian Maeder - @ param n : fixed length
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder - @ param lim : upper limit of elements
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder - @ param s : sum (negative) which is previously computed and gets increased
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder - @ param p : positive coefficients
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly - @ return : list of all lists described above -}
842ae753ab848a8508c4832ab64296b929167a97Christian MaederposCands :: Int -> Int -> Int -> [Int] -> [[Int]]
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaederposCands n lim s p =
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder i<-[1..(min lim (floor (fromIntegral (abs s)/fromIntegral (head p)::Double)))],
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly l <- (posCands (n-1) lim (s + i*(head p)) (tail p))]
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly{- gives all solutions in (1,lim) of the inequality with coeff n and p
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly - @ param (Coeff n p) : negative and positive coefficients
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly - @ param lim : limit for solution searching
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly - @ return : solutions of the inequality, each stored as a pair -}
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'ReillyineqSolver :: Coeffs -> Int -> [([Int],[Int])]
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'ReillyineqSolver (Coeffs n p) lim =
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly let x = negCands (length n) lim
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett linComb l1 l2 =
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly if (l1 == [])||(l2==[])
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly else (head l1)*(head l2) + linComb (tail l1) (tail l2)
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett in [(a,b)| a <- x, b <- posCands (length p) lim (linComb a n) p]
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett-------------------------------------------------------------------------------