Overload.hs revision 37283855efed5d385435b4f70ff4eeef60b914a0
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek Module : $Header$
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek Copyright : (c) Martin K�hl and Till Mossakowski and Uni Bremen 2003
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek Licence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek Maintainer : hets@tzi.de
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek Stability : provisional
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek Portability : portable
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek Overload resolution
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek-- does anyone ever need anything else from here??
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek overloadResolution -- :: Sign -> [FORMULA] -> Result [FORMULA]
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozekimport CASL.Sign -- Sign, OpType
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozekimport CASL.AS_Basic_CASL -- FORMULA, OP_{NAME,SYMB}, TERM, SORT, VAR
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozekimport Common.Result -- Result
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozekimport qualified Common.Lib.Map as Map
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozekimport qualified Common.Lib.Set as Set
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek--import qualified Common.Lib.Rel as Rel -- not used directly
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozekimport qualified Common.Id as Id
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozekimport Data.List ( partition )
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek - global Infos aus Sign berechnen + mit durchreichen
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek (connected compenents, s.u.)
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek - rekursiv in FORMULA absteigen, bis atomare Formel erreicht wird
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek - atomaren Formeln mit minExpTerm behandeln
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek{-----------------------------------------------------------
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek Overload Resolution
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek-----------------------------------------------------------}
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek{- expand all formulae to be fully qualified, then return them if there is no
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek ambiguity -}
64ea4127f463798410a2c20e0261c6b15f60257fJakub HrozekoverloadResolution :: Sign -> [FORMULA] -> Result [FORMULA]
64ea4127f463798410a2c20e0261c6b15f60257fJakub HrozekoverloadResolution sign
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek = mapM (minExpFORMULA sign)
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek{-----------------------------------------------------------
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek Minimal Expansions of a FORMULA
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek-----------------------------------------------------------}
64ea4127f463798410a2c20e0261c6b15f60257fJakub HrozekminExpFORMULA :: Sign -> FORMULA -> Result FORMULA
64ea4127f463798410a2c20e0261c6b15f60257fJakub HrozekminExpFORMULA sign formula
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek = case formula of
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek -- Trivial Atom -> Return untouched
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek True_atom _ -> return formula -- :: FORMULA
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek False_atom _ -> return formula -- :: FORMULA
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek -- Atomic FORMULA -> Check for Ambiguities
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek Predication predicate terms _ ->
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek minExpFORMULA_pred sign predicate terms -- :: FORMULA
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek Definedness term pos -> do
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek t <- minExpTerm sign term -- :: [[TERM]]
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek t' <- is_unambiguous t -- :: TERM
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek return $ Definedness t' pos -- :: FORMULA
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek Existl_equation term1 term2 pos -> do
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek t1 <- minExpTerm sign term1 -- :: [[TERM]]
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek t2 <- minExpTerm sign term2 -- :: [[TERM]]
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek -- find common supersort for each combination of equivs
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek return $ Existl_equation term1 term2 pos -- :: FORMULA
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek -- FIXME: check whether sorts of terms match
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek Strong_equation term1 term2 pos -> do
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek t1 <- minExpTerm sign term1 -- :: [[TERM]]
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek t2 <- minExpTerm sign term2 -- :: [[TERM]]
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek -- find common supersort for each combination of equivs
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek return $ Strong_equation term1 term2 pos -- :: FORMULA
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek -- FIXME: check whether sorts of terms match
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek Membership term sort pos -> do
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek t <- minExpTerm sign term -- :: [[TERM]]
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek t' <- return
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek $ filter ( -- :: [[TERM]]
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek (geq_SORT sign sort) -- :: Bool
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek . term_sort -- :: SORT
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek . head) t -- :: TERM
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek t'' <- is_unambiguous t' -- :: [[TERM]]
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek return $ Membership t'' sort pos -- :: FORMULA
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek -- Unparsed FORMULA -> Error in Parser, Bail out!
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek Mixfix_formula term -> error
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek $ "Parser Error: Unparsed `Mixfix_formula' received: "
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek ++ (show term)
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek Unparsed_formula string _ -> error
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek $ "Parser Error: Unparsed `Unparsed_formula' received: "
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek ++ (show string)
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek -- "Other" FORMULA -> Unknown Error, Bail out!
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek $ "Internal Error: Unknown type of FORMULA received: "
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek ++ (show formula)
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek is_unambiguous :: [[TERM]] -> Result TERM
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek is_unambiguous term = do
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek case term of
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek [_] -> return $ head $ head term -- :: TERM
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek $ "Cannot disambiguate! Possible Expansions: "
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek ++ (show term)
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek{-----------------------------------------------------------
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek Minimal Expansions of a Predicate Application Term
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek-----------------------------------------------------------}
05d935cc9d04f03522d0bb44598d22d99b085926Jakub HrozekminExpFORMULA_pred :: Sign -> PRED_SYMB -> [TERM] -> Result FORMULA
05d935cc9d04f03522d0bb44598d22d99b085926Jakub HrozekminExpFORMULA_pred sign predicate terms = do
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek expansions <- mapM
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek (minExpTerm sign) terms -- :: [[[TERM]]]
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek permuted_exps <- return
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek $ permute expansions -- :: [[[TERM]]]
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek profiles <- return
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek $ map get_profile permuted_exps -- :: [[(PredType, [TERM])]]
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek $ concat -- :: [[(PredType, [TERM])]]
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek $ map (equivalence_Classes pred_eq) -- :: [[[(PredType, [TERM])]]]
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek profiles -- :: [[(PredType, [TERM])]]
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek p' <- return $ choose p -- :: (PredType, [TERM])
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek return $ qualify_pred p'
05d935cc9d04f03522d0bb44598d22d99b085926Jakub Hrozek name :: PRED_NAME
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek name = pred_name predicate
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek preds :: [PredType]
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek $ Map.find name $ (predMap sign)
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek pred_name :: PRED_SYMB -> PRED_NAME
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek pred_name pred' = case pred' of
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek (Pred_name name') -> name'
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek (Qual_pred_name name' _ _) -> name'
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek choose :: [[(PredType, [TERM])]] -> (PredType, [TERM])
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek choose ps = case ps of
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek [_] -> head $ head ps
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek $ "Cannot disambiguate! Term: " ++ (show (predicate, terms))
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek ++ "\n Possible Expansions: " ++ (show ps)
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek qualify_pred :: (PredType, [TERM]) -> FORMULA
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek qualify_pred (pred', terms')
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek = (Predication -- :: FORMULA
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek (Qual_pred_name name (toPRED_TYPE pred') []) -- :: PRED_SYMB
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek terms' -- :: [TERM]
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek []) -- :: [Pos]
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek get_profile :: [[TERM]] -> [(PredType, [TERM])]
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek get_profile cs
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek = [ (pred', ts) |
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek pred' <- preds, -- :: OpType
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek ts <- (permute cs), -- :: [TERM]
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek zipped_all (leq_SORT sign) -- :: Bool
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek (map term_sort ts) -- :: [SORT]
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek (predArgs pred') ] -- :: [SORT]
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek pred_eq :: (PredType, [TERM]) -> (PredType, [TERM]) -> Bool
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek pred_eq (pred1,ts1) (pred2,ts2)
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek = let w1 = predArgs pred1 -- :: [SORT]
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek w2 = predArgs pred2 -- :: [SORT]
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek s1 = map term_sort ts1 -- :: [SORT]
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek s2 = map term_sort ts2 -- :: [SORT]
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek b1 = zipped_all (leq_SORT sign) s1 w1 -- :: Bool
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek b2 = zipped_all (leq_SORT sign) s2 w2 -- :: Bool
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek preds_equal = (pred1 == pred2) -- :: Bool
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek preds_equiv = pred1 `leqP` pred2 -- :: Bool
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek types_equal = and ( zipWith (==) ts1 ts2 ) -- :: Bool
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek in b1 && b2 && (preds_equal || (preds_equiv && types_equal))
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek{-----------------------------------------------------------
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek Minimal Expansions of a Term
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek-----------------------------------------------------------}
d2c552edde275e6c0de904760147afb2992796e9Jakub HrozekminExpTerm :: Sign -> TERM -> Result [[TERM]]
d2c552edde275e6c0de904760147afb2992796e9Jakub HrozekminExpTerm sign term'
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek = case term' of
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek Simple_id var
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek -> minExpTerm_simple sign var
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek Qual_var var sort _
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek -> minExpTerm_qual sign var sort
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek Application op terms _
cc4caf88344210ea9777d618f0f71935ca5e7f8bSumit Bose -> minExpTerm_op sign op terms
cc4caf88344210ea9777d618f0f71935ca5e7f8bSumit Bose Sorted_term term sort _
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek -> minExpTerm_sorted sign term sort
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek Cast term sort _
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek -> minExpTerm_cast sign term sort
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek Conditional term1 formula term2 _
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek -> error $ "not implemented ... yet" -- conditional ?
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek -- FIXME: implement conditionals
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek Unparsed_term string _
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek -> error $ "minExpTerm: Parser Error - Unparsed `Unparsed_term' "
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek _ -> error $ "minExpTerm: Parser Error - Unparsed `Mixfix' term "
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek ++ (show term')
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek{-----------------------------------------------------------
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek Minimal Expansions of a Simple_id Term
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek-----------------------------------------------------------}
64ea4127f463798410a2c20e0261c6b15f60257fJakub HrozekminExpTerm_simple :: Sign -> Id.SIMPLE_ID -> Result [[TERM]]
27e89b6925334565c73c407a9ae2809358789c81Jakub HrozekminExpTerm_simple sign var = do
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek vars <- return
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek Set.empty var (varMap sign)
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek ops' <- return
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek Set.empty name (opMap sign)
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek ops <- return
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek $ (map opRes) -- :: [SORT]
de2bad8ae08f09964834bda0f88db9de39f47c5cJakub Hrozek $ Set.toList -- :: [SORT]
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek ops' -- :: Set.Set SORT
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek cs <- return
de2bad8ae08f09964834bda0f88db9de39f47c5cJakub Hrozek least <- return
de2bad8ae08f09964834bda0f88db9de39f47c5cJakub Hrozek $ Set.filter (is_least_sort cs) cs -- :: Set.Set SORT
d2c552edde275e6c0de904760147afb2992796e9Jakub Hrozek $ qualifyTerms -- :: [[TERM]]
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek $ (equivalence_Classes leqF) -- :: [[(TERM, SORT)]]
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek $ map pair_with_id -- :: [(TERM, SORT)]
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek $ Set.toList least -- :: [SORT]
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek is_const_op :: OpType -> Bool
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek is_const_op op = (null . opArgs) op
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek is_least_sort :: Set.Set SORT -> SORT -> Bool
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek is_least_sort ss s
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek = Set.size (Set.intersection ss (subsortsOf s sign)) == 1
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek pair_with_id :: SORT -> (TERM, SORT)
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek pair_with_id sort = ((Simple_id var), sort)
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek{-----------------------------------------------------------
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek Minimal Expansions of a Qual_var Term
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek-----------------------------------------------------------}
27e89b6925334565c73c407a9ae2809358789c81Jakub HrozekminExpTerm_qual :: Sign -> VAR -> SORT -> Result [[TERM]]
27e89b6925334565c73c407a9ae2809358789c81Jakub HrozekminExpTerm_qual sign var sort = do
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek expandedVar <- minExpTerm_simple sign var -- :: [[TERM]]
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek $ qualifyTerms -- :: [[TERM]]
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek $ map selectExpansions expandedVar -- :: [[(TERM, SORT)]]
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek fits :: TERM -> Bool
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek fits term = case term of
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek (Sorted_term (Simple_id var') sort' _)
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek -> (var == var') && (sort == sort')
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek _ -> error "minExpTerm: unsorted TERM after expansion"
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek selectExpansions :: [TERM] -> [(TERM, SORT)]
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek selectExpansions c
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek = [ ((Simple_id var), sort) | -- :: (TERM, SORT)
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek sorted <- c, -- :: TERM
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek fits sorted ] -- :: Bool
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek{-----------------------------------------------------------
149174acae677d1e72a0da431bf0850d55f2ccb4Sumit Bose Minimal Expansions of a Sorted_term Term
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek-----------------------------------------------------------}
27e89b6925334565c73c407a9ae2809358789c81Jakub HrozekminExpTerm_sorted :: Sign -> TERM -> SORT -> Result [[TERM]]
27e89b6925334565c73c407a9ae2809358789c81Jakub HrozekminExpTerm_sorted sign term sort = do
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek expandedTerm <- minExpTerm sign term -- :: [[TERM]]
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek $ qualifyTerms -- :: [[TERM]]
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek $ map selectExpansions expandedTerm -- :: [[(TERM, SORT)]]
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek fits :: TERM -> Bool
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek fits term' = case term' of
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek (Sorted_term term'' sort' _)
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek -> (term == term'') && (sort == sort')
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek _ -> error "minExpTerm: unsorted TERM after expansion"
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek selectExpansions :: [TERM] -> [(TERM, SORT)]
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek selectExpansions c
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek = [ (term, sort) | -- :: (TERM, SORT)
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek sorted <- c, -- :: TERM
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek fits sorted ] -- :: Bool
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek{-----------------------------------------------------------
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek Minimal Expansions of a Function Application Term
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek-----------------------------------------------------------}
27e89b6925334565c73c407a9ae2809358789c81Jakub HrozekminExpTerm_op :: Sign -> OP_SYMB -> [TERM] -> Result [[TERM]]
27e89b6925334565c73c407a9ae2809358789c81Jakub HrozekminExpTerm_op sign op terms = do
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek expansions <- mapM
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek (minExpTerm sign) terms -- :: [[[TERM]]]
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek permuted_exps <- return
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek $ permute expansions -- :: [[[TERM]]]
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek profiles <- return
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek $ map get_profile permuted_exps -- :: [[(OpType, [TERM])]]
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek $ concat -- :: [[(OpType, [TERM])]]
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek $ map (equivalence_Classes op_eq) -- :: [[[(OpType, [TERM])]]]
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek profiles -- :: [[(OpType, [TERM])]]
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek p' <- return
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek $ map (minimize sign) p -- :: [[(OpType, [TERM])]]
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek $ qualifyTerms -- :: [[TERM]]
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek $ qualifyOps p' -- :: [[(TERM, SORT)]]
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek name :: OP_NAME
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek name = op_name op
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek ops :: [OpType]
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek $ Map.find name $ (opMap sign)
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek op_name :: OP_SYMB -> OP_NAME
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek op_name op' = case op' of
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek (Op_name name') -> name'
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek (Qual_op_name name' _ _) -> name'
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek qualifyOps :: [[(OpType, [TERM])]] -> [[(TERM, SORT)]]
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek qualifyOps = map (map qualify_op)
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek qualify_op :: (OpType, [TERM]) -> (TERM, SORT)
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek qualify_op (op', terms')
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek = ((Application -- :: TERM
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek (Qual_op_name name (toOP_TYPE op') []) -- :: OP_SYMB
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek terms' -- :: [TERM]
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek []) -- :: [Pos]
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek , (opRes op')) -- :: SORT
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek get_profile :: [[TERM]] -> [(OpType, [TERM])]
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek get_profile cs
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek = [ (op', ts) |
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek op' <- ops, -- :: OpType
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek ts <- (permute cs), -- :: [TERM]
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek zipped_all (leq_SORT sign) -- :: Bool
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek (map term_sort ts) -- :: [SORT]
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek (opArgs op') ] -- :: [SORT]
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek op_eq :: (OpType, [TERM]) -> (OpType, [TERM]) -> Bool
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek op_eq (op1,ts1) (op2,ts2)
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek = let w1 = opArgs op1 -- :: [SORT]
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek w2 = opArgs op2 -- :: [SORT]
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek s1 = map term_sort ts1 -- :: [SORT]
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek s2 = map term_sort ts2 -- :: [SORT]
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek b1 = zipped_all (leq_SORT sign) s1 w1 -- :: Bool
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek b2 = zipped_all (leq_SORT sign) s2 w2 -- :: Bool
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek ops_equal = (op1 == op2) -- :: Bool
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek ops_equiv = op1 `leqF` op2 -- :: Bool
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek types_equal = and ( zipWith (==) ts1 ts2 ) -- :: Bool
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek in b1 && b2 && (ops_equal || (ops_equiv && types_equal))
27e89b6925334565c73c407a9ae2809358789c81Jakub Hrozek{-----------------------------------------------------------
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek Minimal Expansions of a Cast Term
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek-----------------------------------------------------------}
64ea4127f463798410a2c20e0261c6b15f60257fJakub HrozekminExpTerm_cast :: Sign -> TERM -> SORT -> Result [[TERM]]
64ea4127f463798410a2c20e0261c6b15f60257fJakub HrozekminExpTerm_cast sign term sort = do
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek expandedTerm <- minExpTerm sign term -- :: [[TERM]]
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek validExps <- return
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek $ filter (leq_SORT sign sort . term_sort) -- :: [TERM]
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek $ map head expandedTerm -- :: [TERM]
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek $ qualifyTerms -- :: [[TERM]]
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek $ [map (\ t -> (t, sort)) validExps] -- :: [[(TERM, SORT)]]
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek{-----------------------------------------------------------
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek Divide a Set (list) into equivalence classes w.r. to eq
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek-----------------------------------------------------------}
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek-- also look below for Till's SML-version of this
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozekequivalence_Classes :: (a -> a -> Bool) -> [a] -> [[a]]
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozekequivalence_Classes _ [] = []
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozekequivalence_Classes eq (x:l) = xs':(equivalence_Classes eq ys)
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek (xs, ys) = partition (eq x) l
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek xs' = (x:xs)
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek{-----------------------------------------------------------
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek Transform a list [l1,l2, ... ln] to (in sloppy notation)
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek [[x1,x2, ... ,xn] | x1<-l1, x2<-l2, ... xn<-ln]
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek-----------------------------------------------------------}
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozekpermute :: [[a]] -> [[a]]
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozekpermute [] = [[]]
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozekpermute [x] = map (\y -> [y]) x
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozekpermute (x:l) = concat (map (distribute (permute l)) x)
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek distribute perms y = map ((:) y) perms
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek{-----------------------------------------------------------
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek Like 'and (zipWith p as bs)',
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek but must return False if lengths don't match
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek-----------------------------------------------------------}
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozekzipped_all :: (a -> b -> Bool) -> [a] -> [b] -> Bool
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozekzipped_all _ [] [] = True
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozekzipped_all p (a:as) (b:bs) = (p a b) && (zipped_all p as bs)
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozekzipped_all _ _ _ = False
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek{-----------------------------------------------------------
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek Construct a TERM of type Sorted_term
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek from each (TERM, SORT) tuple
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek-----------------------------------------------------------}
64ea4127f463798410a2c20e0261c6b15f60257fJakub HrozekqualifyTerms :: [[(TERM, SORT)]] -> [[TERM]]
64ea4127f463798410a2c20e0261c6b15f60257fJakub HrozekqualifyTerms = map (map qualify_term)
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek qualify_term :: (TERM, SORT) -> TERM
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek qualify_term (t, s) = Sorted_term t s []
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek{-----------------------------------------------------------
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek For each C in P (see above), let C' choose _one_
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek f:s \in C for each s minimal such that f:s \in C
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek-----------------------------------------------------------}
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozekminimize :: Sign -> [(OpType, [TERM])] -> [(OpType, [TERM])]
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozekminimize sign ops_n_terms
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek = concat $ map reduce ops_n_terms
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek results :: Set.Set SORT
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek results = Set.fromList (map (opRes . fst) ops_n_terms)
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek lesserSorts :: SORT -> Set.Set SORT
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek lesserSorts s = Set.intersection results (subsortsOf s sign)
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek leastSort :: SORT -> Bool
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek leastSort s = Set.size (lesserSorts s) == 1
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek reduce :: (OpType, [TERM]) -> [(OpType, [TERM])]
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek reduce x@(op,_) = if (leastSort (opRes op)) then [x] else []
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozekterm_sort :: TERM -> SORT
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozekterm_sort term' = case term' of
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek (Sorted_term _ sort _ ) -> sort
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek _ -> error -- unlikely
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek "minExpTerm: unsorted TERM after expansion"
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek{-----------------------------------------------------------
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek Return True if s1 <= s2
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek-----------------------------------------------------------}
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozekleq_SORT :: Sign -> SORT -> SORT -> Bool
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozekleq_SORT sign s1 s2 = Set.member s2 (supersortsOf s1 sign)
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek-- leq_SORT = (flip Set.member) . (flip supersortsOf)
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek{-----------------------------------------------------------
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek Return True if s1 >= s2
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek-----------------------------------------------------------}
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozekgeq_SORT :: Sign -> SORT -> SORT -> Bool
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozekgeq_SORT sign s1 s2 = Set.member s2 (subsortsOf s1 sign)
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek-- geq_SORT = (flip Set.member) . (flip subsortsOf)
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek{- Die hier fehlen noch - sind aber essentiell :) -}
64ea4127f463798410a2c20e0261c6b15f60257fJakub HrozekleqF :: a -> a -> Bool -- Funktionsgleichheit
64ea4127f463798410a2c20e0261c6b15f60257fJakub HrozekleqF _ _ = True
64ea4127f463798410a2c20e0261c6b15f60257fJakub HrozekleqP :: a -> a -> Bool -- Praedikatsgleichheit
64ea4127f463798410a2c20e0261c6b15f60257fJakub HrozekleqP _ _ = True
64ea4127f463798410a2c20e0261c6b15f60257fJakub HrozekDie alten SML-Funktionen, die hier verwandt wurden.
64ea4127f463798410a2c20e0261c6b15f60257fJakub HrozekDen Beschreibungen nach sind das genau die beiden, mit denen eine Menge in
64ea4127f463798410a2c20e0261c6b15f60257fJakub HrozekAequivalenzklassen unterteilt wird.
64ea4127f463798410a2c20e0261c6b15f60257fJakub HrozekWie die erste davon funktioniert, ist mir nicht offen ersichtlich,
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozekaber vielleicht brauch ich die eigentlich auch gar nicht?
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek(* Compute the connected compenents of a graph which is given
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek by a list of nodes and a boolean function indicating whether
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek there is an egde between two nodes.
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek For each node, the algorithm splits the connected components
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek which have been computed so far into two categories:
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek those which are connected to the node and those which are not.
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek The former are all linked with @ in order to form a new connected
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek component, the latter are left untouched. *)
db5f9ab3feb85aa444eab20428ca2b98801b6783Jakub Hrozekfun compute_conn_components (edges:'a*'a->bool) (nodes:'a list):'a list list =
db5f9ab3feb85aa444eab20428ca2b98801b6783Jakub Hrozek fun is_connected(node,nil) = false
db5f9ab3feb85aa444eab20428ca2b98801b6783Jakub Hrozek | is_connected(node,n::c) =
db5f9ab3feb85aa444eab20428ca2b98801b6783Jakub Hrozek edges(node,n) orelse edges(n,node) orelse is_connected(node,c)
db5f9ab3feb85aa444eab20428ca2b98801b6783Jakub Hrozek fun split_components(node,nil,acc_comp_of_node,acc_other_comps) =
db5f9ab3feb85aa444eab20428ca2b98801b6783Jakub Hrozek (node::acc_comp_of_node)::acc_other_comps
db5f9ab3feb85aa444eab20428ca2b98801b6783Jakub Hrozek | split_components(node,current_comp::other_comps,acc_comp_of_node,acc_other_comps) =
db5f9ab3feb85aa444eab20428ca2b98801b6783Jakub Hrozek if is_connected(node,current_comp)
db5f9ab3feb85aa444eab20428ca2b98801b6783Jakub Hrozek then split_components(node,other_comps,current_comp@acc_comp_of_node,acc_other_comps)
db5f9ab3feb85aa444eab20428ca2b98801b6783Jakub Hrozek else split_components(node,other_comps,acc_comp_of_node,current_comp::acc_other_comps)
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek fun add_node (node:'a,components:'a list list):'a list list =
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek split_components(node,components,nil,nil)
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek foldr add_node (nodes,[])
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek(* Compute the equivalence classes of the equivalence closures of leqF and leqP resp.
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek and store them in a table indexed by function and predicate names, resp.
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek This is needed when checking if terms or predications are equivalent, since
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek this equivalence is defined in terms of the equivalence closures of leqF and leqP resp. *)
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozekfun get_conn_components (env:local_env) : local_env1 =
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek val (srts,vars,funs,preds) = env
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek (env,(Symtab_id.map (compute_conn_components (leqF env)) funs ,
64ea4127f463798410a2c20e0261c6b15f60257fJakub Hrozek Symtab_id.map (compute_conn_components (leqP env)) preds) )