Overload.hs revision 32da3d5d6c39683cf1434a18a740717a7c0d7ef4
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher Module : $Header$
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher Copyright : (c) Martin K�hl and Till Mossakowski and Uni Bremen 2003
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher Licence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher Maintainer : hets@tzi.de
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher Stability : provisional
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher Portability : portable
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher Overload resolution
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher-- does anyone ever need anything else from me?
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher overloadResolution -- :: Sign -> [FORMULA] -> Result [FORMULA]
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagherimport CASL.Sign -- Sign, OpType
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagherimport CASL.AS_Basic_CASL -- FORMULA, OP_{NAME,SYMB}, TERM, SORT, VAR
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagherimport qualified Common.Lib.Map as Map
f2c346eaa486431ffa2a3adc05356159de834e2eLukas Slebodnikimport qualified Common.Lib.Set as Set
f2c346eaa486431ffa2a3adc05356159de834e2eLukas Slebodnikimport qualified Common.Id as Id
f2c346eaa486431ffa2a3adc05356159de834e2eLukas Slebodnikimport qualified Common.Named as Named
6ac396bebb4cd3124711d26dce54263f6f9c7c45Simo Sorceimport Data.List ( partition )
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek - global Infos aus Sign berechnen + mit durchreichen
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek (connected compenents, s.u.)
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek - rekursiv in FORMULA absteigen, bis atomare Formel erreicht wird
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek - atomaren Formeln mit minExpTerm behandeln
3412d14d65490c32414e72ac20fe21bad53ceb45Simo Sorce * generalize 'is_unambiguous' (see 'choose') and make it available globally
9579839a00493830c10a856ad1f5e035b6fa3b45Ondrej Kos * replace 'case' statements w/ pattern matching where possible
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher * generalize minExpFORMULA_pred/minExpTerm_op/minExpTerm_cond
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher * utilize Sets instead of Lists
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher * check whether Qual_var expansion works as it is supposed to
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher * generalize expansion for Qual_var and Sorted_term
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher * move structural logic to higher levels, as e.g. in
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher qualifyOps = map (map qualify_op) -- map should go somewhere above
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher * sweep op-like logic from minExpTerm_cond where it is unneeded
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher * generalize zipped_all
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher * generalize qualifyTerms or implement locally - too much structural force
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher * gemeralize minimize_* or implement locally - needed only in one f. each
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher * use more let/in constructs (instead of where) to simulate workflow
51773686d354b82081830444c048706d83d43d65Jakub Hrozek{-----------------------------------------------------------
51773686d354b82081830444c048706d83d43d65Jakub Hrozek Overload Resolution
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher-----------------------------------------------------------}
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub HrozekoverloadResolution :: Sign -> [Named.Named FORMULA]
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher -> Result [Named.Named FORMULA]
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub HrozekoverloadResolution sign = mapM overload
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher overload :: (Named.Named FORMULA) -> Result (Named.Named FORMULA)
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher overload sent = do
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher let sent' = Named.sentence sent
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher --debug 1 ("sent'",sent')
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher exp_sent <- minExpFORMULA sign sent'
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher --debug 2 ("exp_sent",exp_sent)
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher return sent { Named.sentence = exp_sent }
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher{-----------------------------------------------------------
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher Minimal Expansions of a FORMULA
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher-----------------------------------------------------------}
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen GallagherminExpFORMULA :: Sign -> FORMULA -> Result FORMULA
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen GallagherminExpFORMULA sign formula
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher = case formula of
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher -- Trivial Atom -> Return untouched
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher True_atom _ -> return formula -- :: FORMULA
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher False_atom _ -> return formula -- :: FORMULA
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher -- Non-Atomic FORMULA -> Recurse through subFORMULAe
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher Quantification q vars f pos -> do
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek let (_, sign') = runState (mapM_ addVars vars) sign
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek f' <- minExpFORMULA sign' f
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek return $ Quantification q vars f' pos
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek Conjunction fs pos -> do
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek fs' <- mapM (minExpFORMULA sign) fs
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek return $ Conjunction fs' pos
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek Disjunction fs pos -> do
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek fs' <- mapM (minExpFORMULA sign) fs
3412d14d65490c32414e72ac20fe21bad53ceb45Simo Sorce return $ Disjunction fs' pos
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek Implication f1 f2 pos -> do
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek f1' <- minExpFORMULA sign f1
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek f2' <- minExpFORMULA sign f2
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek return $ Implication f1' f2' pos
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek Equivalence f1 f2 pos -> do
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek f1' <- minExpFORMULA sign f1
51773686d354b82081830444c048706d83d43d65Jakub Hrozek f2' <- minExpFORMULA sign f2
51773686d354b82081830444c048706d83d43d65Jakub Hrozek return $ Equivalence f1' f2' pos
b3292840ebaa747a9fd596ff47cc5d18198361d0Michal Zidek Negation f pos -> do
51773686d354b82081830444c048706d83d43d65Jakub Hrozek f' <- minExpFORMULA sign f
51773686d354b82081830444c048706d83d43d65Jakub Hrozek return $ Negation f' pos
51773686d354b82081830444c048706d83d43d65Jakub Hrozek -- Atomic FORMULA -> Check for Ambiguities
51773686d354b82081830444c048706d83d43d65Jakub Hrozek Predication predicate terms pos ->
51773686d354b82081830444c048706d83d43d65Jakub Hrozek minExpFORMULA_pred sign predicate terms pos -- :: FORMULA
51773686d354b82081830444c048706d83d43d65Jakub Hrozek Definedness term pos -> do
51773686d354b82081830444c048706d83d43d65Jakub Hrozek t <- minExpTerm sign term -- :: [[TERM]]
51773686d354b82081830444c048706d83d43d65Jakub Hrozek --debug 4 ("t",t)
51773686d354b82081830444c048706d83d43d65Jakub Hrozek t' <- is_unambiguous t pos -- :: TERM
51773686d354b82081830444c048706d83d43d65Jakub Hrozek return $ Definedness t' pos -- :: FORMULA
51773686d354b82081830444c048706d83d43d65Jakub Hrozek Existl_equation term1 term2 pos ->
51773686d354b82081830444c048706d83d43d65Jakub Hrozek minExpFORMULA_eq sign Existl_equation term1 term2 pos
51773686d354b82081830444c048706d83d43d65Jakub Hrozek Strong_equation term1 term2 pos ->
51773686d354b82081830444c048706d83d43d65Jakub Hrozek minExpFORMULA_eq sign Strong_equation term1 term2 pos
51773686d354b82081830444c048706d83d43d65Jakub Hrozek Membership term sort pos -> do
51773686d354b82081830444c048706d83d43d65Jakub Hrozek t <- minExpTerm sign term -- :: [[TERM]]
51773686d354b82081830444c048706d83d43d65Jakub Hrozek t' <- let leq_term [] = False
51773686d354b82081830444c048706d83d43d65Jakub Hrozek leq_term (t1:_) =
51773686d354b82081830444c048706d83d43d65Jakub Hrozek leq_SORT sign sort $ term_sort t1
51773686d354b82081830444c048706d83d43d65Jakub Hrozek in return $ filter leq_term t -- :: TERM
51773686d354b82081830444c048706d83d43d65Jakub Hrozek t'' <- is_unambiguous t' pos -- :: [[TERM]]
51773686d354b82081830444c048706d83d43d65Jakub Hrozek return $ Membership t'' sort pos -- :: FORMULA
51773686d354b82081830444c048706d83d43d65Jakub Hrozek -- Unparsed FORMULA -> Error in Parser, Bail out!
51773686d354b82081830444c048706d83d43d65Jakub Hrozek Mixfix_formula term -> error
51773686d354b82081830444c048706d83d43d65Jakub Hrozek $ "Parser Error: Unparsed `Mixfix_formula' received: "
51773686d354b82081830444c048706d83d43d65Jakub Hrozek ++ (show term)
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek Unparsed_formula string _ -> error
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek $ "Parser Error: Unparsed `Unparsed_formula' received: "
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek ++ (show string)
3412d14d65490c32414e72ac20fe21bad53ceb45Simo Sorce -- "Other" FORMULA -> Unknown Error, Bail out!
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek $ "Internal Error: Unknown type of FORMULA received: "
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek ++ (show formula)
6ac396bebb4cd3124711d26dce54263f6f9c7c45Simo Sorce is_unambiguous :: [[TERM]] -> [Id.Pos] -> Result TERM
51773686d354b82081830444c048706d83d43d65Jakub Hrozek is_unambiguous term pos = do
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek case term of
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek [] -> pplain_error (Unparsed_term "<error>" [])
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek (ptext "No correct typing for " <+> printText term)
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek -- BEWARE! Oversimplified disambiguation!
c9041cb7addc1a49e0771246d17de101662fbcbcJakub Hrozek (_:_):_ -> return $ head $ head term -- :: TERM
c9041cb7addc1a49e0771246d17de101662fbcbcJakub Hrozek _ -> pplain_error (Unparsed_term "<error>" [])
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek (ptext "Cannot disambiguate1! Possible Expansions: "
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek <+> (printText term)) (Id.headPos pos)
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek{-----------------------------------------------------------
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek Minimal Expansions of a Predicate Application Formula
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek-----------------------------------------------------------}
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub HrozekminExpFORMULA_pred :: Sign -> PRED_SYMB -> [TERM] -> [Id.Pos] -> Result FORMULA
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub HrozekminExpFORMULA_pred sign predicate terms pos = do
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek expansions <- mapM
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek (minExpTerm sign) terms -- :: [[[TERM]]]
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek permuted_exps <- return
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek $ permute expansions -- :: [[[TERM]]]
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek profiles <- return
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek $ map get_profile permuted_exps -- :: [[(PredType, [TERM])]]
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher $ concat -- :: [[(PredType, [TERM])]]
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher $ map (equivalence_Classes pred_eq) -- :: [[[(PredType, [TERM])]]]
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher profiles -- :: [[(PredType, [TERM])]]
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek p' <- choose p -- :: (PredType, [TERM])
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek return $ qualify_pred p'
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher name :: PRED_NAME
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher name = pred_name predicate
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher preds :: [PredType]
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher Set.empty name $ (predMap sign)
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher pred_name :: PRED_SYMB -> PRED_NAME
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher pred_name pred' = case pred' of
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher (Pred_name name') -> name'
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher (Qual_pred_name name' _ _) -> name'
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher choose :: [[(PredType, [TERM])]] -> Result (PredType, [TERM])
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek choose ps = case ps of
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek [] -> pplain_error (PredType [],[])
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek (ptext "No correct typing for " <+> printText ps)
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher -- BEWARE! Oversimplified disambiguation!
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher (_:_):_ -> return $ head $ head ps
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher _ -> pplain_error (PredType [], terms)
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher (ptext "Cannot disambiguate2! Term: "
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek <+> (printText (predicate, terms))
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek $$ ptext "Possible Expansions: "
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher <+> (printText ps)) (Id.headPos pos)
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek qualify_pred :: (PredType, [TERM]) -> FORMULA
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher qualify_pred (pred', terms')
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher = (Predication -- :: FORMULA
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek (Qual_pred_name name (toPRED_TYPE pred') []) -- :: PRED_SYMB
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher terms' -- :: [TERM]
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek pos) -- :: [Pos]
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher get_profile :: [[TERM]] -> [(PredType, [TERM])]
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher get_profile cs
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher = [ (pred', ts) |
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher pred' <- preds, -- :: PredType
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher ts <- (permute cs), -- :: [TERM]
9579839a00493830c10a856ad1f5e035b6fa3b45Ondrej Kos zipped_all (leq_SORT sign) -- :: Bool
3412d14d65490c32414e72ac20fe21bad53ceb45Simo Sorce (map term_sort ts) -- :: [SORT]
3412d14d65490c32414e72ac20fe21bad53ceb45Simo Sorce (predArgs pred') ] -- :: [SORT]
3412d14d65490c32414e72ac20fe21bad53ceb45Simo Sorce pred_eq :: (PredType, [TERM]) -> (PredType, [TERM]) -> Bool
9579839a00493830c10a856ad1f5e035b6fa3b45Ondrej Kos pred_eq (pred1,ts1) (pred2,ts2)
9579839a00493830c10a856ad1f5e035b6fa3b45Ondrej Kos = let w1 = predArgs pred1 -- :: [SORT]
9579839a00493830c10a856ad1f5e035b6fa3b45Ondrej Kos w2 = predArgs pred2 -- :: [SORT]
9579839a00493830c10a856ad1f5e035b6fa3b45Ondrej Kos s1 = map term_sort ts1 -- :: [SORT]
9579839a00493830c10a856ad1f5e035b6fa3b45Ondrej Kos s2 = map term_sort ts2 -- :: [SORT]
9579839a00493830c10a856ad1f5e035b6fa3b45Ondrej Kos b1 = zipped_all (leq_SORT sign) s1 w1 -- :: Bool
3412d14d65490c32414e72ac20fe21bad53ceb45Simo Sorce b2 = zipped_all (leq_SORT sign) s2 w2 -- :: Bool
9579839a00493830c10a856ad1f5e035b6fa3b45Ondrej Kos preds_equal = (pred1 == pred2) -- :: Bool
9579839a00493830c10a856ad1f5e035b6fa3b45Ondrej Kos preds_equiv = leqP sign pred1 pred2 -- :: Bool
9579839a00493830c10a856ad1f5e035b6fa3b45Ondrej Kos types_equal = and ( zipWith (==) ts1 ts2 ) -- :: Bool
9579839a00493830c10a856ad1f5e035b6fa3b45Ondrej Kos in b1 && b2 && (preds_equal || (preds_equiv && types_equal))
9579839a00493830c10a856ad1f5e035b6fa3b45Ondrej Kos{-----------------------------------------------------------
9579839a00493830c10a856ad1f5e035b6fa3b45Ondrej Kos Minimal Expansions of a Strong/Existl. Equation Formula
6ac396bebb4cd3124711d26dce54263f6f9c7c45Simo Sorce-----------------------------------------------------------}
6ac396bebb4cd3124711d26dce54263f6f9c7c45Simo SorceminExpFORMULA_eq :: Sign -> (TERM -> TERM -> [Id.Pos] -> FORMULA)
51773686d354b82081830444c048706d83d43d65Jakub Hrozek -> TERM -> TERM -> [Id.Pos] -> Result FORMULA
4e9631a9f1ae87317eef53145622099c46196b56Jakub HrozekminExpFORMULA_eq sign eq term1 term2 pos = do
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek exps1 <- minExpTerm sign term1 -- :: [[TERM]]
01d048293cba60cf45ca2791585a7d6dc3bf57b2Jakub Hrozek exps2 <- minExpTerm sign term2 -- :: [[TERM]]
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek --debug 1 ("exps1",exps1)
de5dcfd8e6a8aabd2064cbb86e6c2a3f304b1ca5Stephen Gallagher --debug 2 ("exps2",exps2)
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek pairs <- return
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek $ permute [catMaybes (map maybeHead exps1),
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek catMaybes (map maybeHead exps2)] -- :: [[TERM]]
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek --debug 3 ("paris",pairs)
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek candidates <- return
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek $ filter fit pairs -- :: [[TERM]]
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek --debug 3 ("candidates",candidates)
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek case candidates of
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek [] -> pplain_error (eq term1 term2 pos)
01d048293cba60cf45ca2791585a7d6dc3bf57b2Jakub Hrozek (ptext "No correct typing for " <+> printText (eq term1 term2 pos))
01d048293cba60cf45ca2791585a7d6dc3bf57b2Jakub Hrozek -- BEWARE! Oversimplified disambiguation!
01d048293cba60cf45ca2791585a7d6dc3bf57b2Jakub Hrozek ([t1,t2]:_) -> return $ eq t1 t2 pos
01d048293cba60cf45ca2791585a7d6dc3bf57b2Jakub Hrozek _ -> pplain_error (eq term1 term2 pos)
01d048293cba60cf45ca2791585a7d6dc3bf57b2Jakub Hrozek (ptext "Cannot disambiguate3! Possible Expansions: "
c5eb0dc6c5ce2940f329c477aeecb57e2d8ec38dAriel Barria <+> (printText exps1) $$ (printText exps2)) (Id.headPos pos)
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek fit :: [TERM] -> Bool
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek fit = (have_common_supersorts sign) . (map term_sort)
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek maybeHead :: [a] -> Maybe a
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek maybeHead (x:_) = Just x
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek maybeHead _ = Nothing
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek{-----------------------------------------------------------
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek Minimal Expansions of a TERM
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek-----------------------------------------------------------}
4e9631a9f1ae87317eef53145622099c46196b56Jakub HrozekminExpTerm :: Sign -> TERM -> Result [[TERM]]
4e9631a9f1ae87317eef53145622099c46196b56Jakub HrozekminExpTerm sign term'
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek = do -- debug 66 ("term'",term')
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek u <- case term' of
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek Simple_id var
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek -> minExpTerm_simple sign var
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek Qual_var var sort pos
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek -> minExpTerm_qual sign var sort pos
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek Application op terms pos
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek -> minExpTerm_op sign op terms pos
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek Sorted_term term sort pos
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek -> minExpTerm_sorted sign term sort pos
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek Cast term sort pos
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek -> minExpTerm_cast sign term sort pos
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek Conditional term1 formula term2 pos
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek -> minExpTerm_cond sign term1 formula term2 pos
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek Unparsed_term string _
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek -> error $ "minExpTerm: Parser Error - Unparsed `Unparsed_term' "
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek _ -> error $ "minExpTerm: Parser Error - Unparsed `Mixfix' term "
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek ++ (show term')
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek -- debug 6 ("u",u)
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek{-----------------------------------------------------------
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek Minimal Expansions of a Simple_id Term
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek-----------------------------------------------------------}
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub HrozekminExpTerm_simple :: Sign -> Id.SIMPLE_ID -> Result [[TERM]]
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub HrozekminExpTerm_simple sign var = do
6ac396bebb4cd3124711d26dce54263f6f9c7c45Simo Sorce vars <- return
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek Set.empty var (varMap sign)
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek ops' <- return
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek $ (Set.filter is_const_op) -- :: Set.Set OpType
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek Set.empty name (opMap sign)
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek ops <- return
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek $ (map opRes) -- :: [SORT]
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek $ Set.toList -- :: [OpType]
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek ops' -- :: Set.Set OpType
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek cs <- return
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek least <- return
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek -- BEWARE: Restriction to minimal sorts is not correct
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek -- in case of downcasts: here, it may be the
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek -- case that the cast is only correct for non-minimal sorts!
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek $ {-Set.filter (is_least_sort cs)-} cs -- :: Set.Set SORT
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek $ qualifyTerms [] -- :: [[TERM]]
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher $ (equivalence_Classes eq) -- :: [[(TERM, SORT)]]
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher $ map pair_with_id -- :: [(TERM, SORT)]
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher $ Set.toList least -- :: [SORT]
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher is_const_op :: OpType -> Bool
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher is_const_op op = (null . opArgs) op
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher is_least_sort :: Set.Set SORT -> SORT -> Bool
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher is_least_sort ss s
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher = Set.size (Set.intersection ss (subsortsOf s sign)) == 1
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher eq = xeq_TUPLE sign
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher pair_with_id :: SORT -> (TERM, SORT)
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher pair_with_id sort = ((Simple_id var), sort)
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher{-----------------------------------------------------------
f2c346eaa486431ffa2a3adc05356159de834e2eLukas Slebodnik Minimal Expansions of a Qual_var Term
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher-----------------------------------------------------------}
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub HrozekminExpTerm_qual :: Sign -> VAR -> SORT -> [Id.Pos] -> Result [[TERM]]
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen GallagherminExpTerm_qual sign var sort pos = do
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher expandedVar <- minExpTerm_simple sign var -- :: [[TERM]]
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher $ qualifyTerms pos -- :: [[TERM]]
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher $ map selectExpansions expandedVar -- :: [[(TERM, SORT)]]
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher fits :: TERM -> Bool
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek fits term = case term of
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher (Sorted_term (Simple_id var') sort' _)
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher -> (var == var') && (sort == sort')
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher _ -> error "Internal error: minExpTerm: unsorted TERM after expansion"
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher selectExpansions :: [TERM] -> [(TERM, SORT)]
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher selectExpansions c
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher = [ ((Simple_id var), sort) | -- :: (TERM, SORT)
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek sorted <- c, -- :: TERM
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher fits sorted ] -- :: Bool
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher{-----------------------------------------------------------
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek Minimal Expansions of a Sorted_term Term
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek-----------------------------------------------------------}
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub HrozekminExpTerm_sorted :: Sign -> TERM -> SORT -> [Id.Pos] -> Result [[TERM]]
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub HrozekminExpTerm_sorted sign term sort pos = do
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher expandedTerm <- minExpTerm sign term -- :: [[TERM]]
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher --debug 7 ("expandedTerm", expandedTerm)
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher $ qualifyTerms pos -- :: [[TERM]]
3412d14d65490c32414e72ac20fe21bad53ceb45Simo Sorce $ map selectExpansions expandedTerm -- :: [[(TERM, SORT)]]
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher fits :: TERM -> Bool
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher fits term' = case term' of
6ac396bebb4cd3124711d26dce54263f6f9c7c45Simo Sorce (Sorted_term _ sort' _)
51773686d354b82081830444c048706d83d43d65Jakub Hrozek -> sort == sort'
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek _ -> error "Internal error: minExpTerm: unsorted TERM after expansion"
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher selectExpansions :: [TERM] -> [(TERM, SORT)]
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher selectExpansions c
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher = [ (sorted, sort) | -- :: (TERM, SORT)
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek sorted <- c, -- :: TERM
f2c346eaa486431ffa2a3adc05356159de834e2eLukas Slebodnik fits sorted ] -- :: Bool
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher{-----------------------------------------------------------
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher Minimal Expansions of a Function Application Term
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher-----------------------------------------------------------}
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen GallagherminExpTerm_op :: Sign -> OP_SYMB -> [TERM] -> [Id.Pos] -> Result [[TERM]]
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen GallagherminExpTerm_op sign (Op_name (Id.Id [tok] [] _)) [] pos =
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher minExpTerm_simple sign tok
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen GallagherminExpTerm_op sign op terms pos = minExpTerm_op1 sign op terms pos
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen GallagherminExpTerm_op1 :: Sign -> OP_SYMB -> [TERM] -> [Id.Pos] -> Result [[TERM]]
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen GallagherminExpTerm_op1 sign op terms pos = do
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher --debug 3 ("op",op)
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher --debug 3 ("terms",show terms)
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher expansions <- mapM
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher (minExpTerm sign) terms -- :: [[[TERM]]]
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher --debug 3 ("expansions",show expansions)
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher permuted_exps <- return
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher $ permute expansions -- :: [[[TERM]]]
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher --debug 3 ("permuted_exps",show permuted_exps)
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher profiles <- return
21d485184df986e1a123f70c689517386e51a5ceMichal Zidek $ map get_profile permuted_exps -- :: [[(OpType, [TERM])]]
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher $ concat -- :: [[(OpType, [TERM])]]
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos $ map (equivalence_Classes op_eq) -- :: [[[(OpType, [TERM])]]]
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher profiles -- :: [[(OpType, [TERM])]]
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher --debug 3 ("p",show p)
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher $ map (minimize_op sign) p -- :: [[(OpType, [TERM])]]
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher --debug 3 ("p'",show p')
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher --debug 3 (" qualifyOps p'",show $ qualifyOps p')
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher --debug 3 ("qualifyTerms pos $ qualifyOps p'",show $ qualifyTerms pos $ qualifyOps p')
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher $ qualifyTerms pos -- :: [[TERM]]
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher $ qualifyOps p' -- :: [[(TERM, SORT)]]
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher name :: OP_NAME
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher name = op_name op
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher ops :: [OpType]
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher Set.empty name $ (opMap sign)
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher op_name :: OP_SYMB -> OP_NAME
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher op_name op' = case op' of
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher (Op_name name') -> name'
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher (Qual_op_name name' _ _) -> name'
21d485184df986e1a123f70c689517386e51a5ceMichal Zidek qualifyOps :: [[(OpType, [TERM])]] -> [[(TERM, SORT)]]
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher qualifyOps = map (map qualify_op)
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher qualify_op :: (OpType, [TERM]) -> (TERM, SORT)
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher qualify_op (op', terms')
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher = ((Application -- :: TERM
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher (Qual_op_name name (toOP_TYPE op') []) -- :: OP_SYMB
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher terms' -- :: [TERM]
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher []) -- :: [Pos]
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher , (opRes op')) -- :: SORT
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher get_profile :: [[TERM]] -> [(OpType, [TERM])]
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher get_profile cs
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos = [ (op', ts) | -- :: (OpType, [TERM])
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos op' <- ops, -- :: OpType
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos ts <- (permute cs), -- :: [TERM]
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos zipped_all (leq_SORT sign) -- :: Bool
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos (map term_sort ts) -- :: [SORT]
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos (opArgs op') ] -- :: [SORT]
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos op_eq :: (OpType, [TERM]) -> (OpType, [TERM]) -> Bool
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos op_eq (op1,ts1) (op2,ts2)
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos = let w1 = opArgs op1 -- :: [SORT]
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos w2 = opArgs op2 -- :: [SORT]
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos s1 = map term_sort ts1 -- :: [SORT]
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos s2 = map term_sort ts2 -- :: [SORT]
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos b1 = zipped_all (leq_SORT sign) s1 w1 -- :: Bool
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos b2 = zipped_all (leq_SORT sign) s2 w2 -- :: Bool
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos ops_equal = (op1 == op2) -- :: Bool
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos ops_equiv = leqF sign op1 op2 -- :: Bool
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos types_equal = and ( zipWith (==) ts1 ts2 ) -- :: Bool
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos in b1 && b2 && (ops_equal || (ops_equiv && types_equal))
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos{-----------------------------------------------------------
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos Minimal Expansions of a Cast Term
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos-----------------------------------------------------------}
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej KosminExpTerm_cast :: Sign -> TERM -> SORT -> [Id.Pos] -> Result [[TERM]]
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej KosminExpTerm_cast sign term sort pos = do
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos expandedTerm <- minExpTerm sign term -- :: [[TERM]]
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos --debug 1 ("expandedTerm",expandedTerm)
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos validExps <- return
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos $ map (filter (leq_SORT sign sort . term_sort)) -- :: [[TERM]]
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos $ expandedTerm -- :: [[TERM]]
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos --debug 2 ("validExps",validExps)
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos $ qualifyTerms pos -- :: [[TERM]]
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos $ map (map (\ t -> (t, sort))) validExps -- :: [[(TERM, SORT)]]
21d485184df986e1a123f70c689517386e51a5ceMichal Zidek{-----------------------------------------------------------
21d485184df986e1a123f70c689517386e51a5ceMichal Zidek Minimal Expansions of a Conditional Term
21d485184df986e1a123f70c689517386e51a5ceMichal Zidek-----------------------------------------------------------}
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej KosminExpTerm_cond :: Sign -> TERM -> FORMULA -> TERM -> [Id.Pos]
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos -> Result [[TERM]]
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej KosminExpTerm_cond sign term1 formula term2 pos = do
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos <- minExpTerm sign term1 -- :: [[TERM]]
a4bf85ccc902490c3b75b44532010fbb32169801Lukas Slebodnik <- minExpTerm sign term2 -- :: [[TERM]]
a4bf85ccc902490c3b75b44532010fbb32169801Lukas Slebodnik expanded_formula
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos <- minExpFORMULA sign formula -- :: FORMULA
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos permuted_exps <- return
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos $ permute [expansions1, expansions2] -- :: [[[TERM]]]
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos --debug 7 ("permuted_exps",permuted_exps)
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos profiles <- return
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos $ map get_profile permuted_exps -- :: [[([TERM], SORT)]]
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos --debug 7 ("profiles",profiles)
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos $ concat -- :: [[([TERM], SORT)]]
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos $ map -- :: [[[([TERM], SORT)]]]
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos (equivalence_Classes eq)
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos profiles -- :: [[([TERM], SORT)]]
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos --debug 7 ("p",p)
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos p' <- return
6ac396bebb4cd3124711d26dce54263f6f9c7c45Simo Sorce $ map (minimize_cond sign) p -- :: [[([TERM], SORT)]]
51773686d354b82081830444c048706d83d43d65Jakub Hrozek --debug 7 ("p'",p')
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos $ qualifyTerms pos -- :: [[TERM]]
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos $ qualifyConds expanded_formula p' -- :: [[(TERM, SORT)]]
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos have_supersort :: [TERM] -> Bool
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos have_supersort = not . Set.isEmpty . supersorts
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos supersorts :: [TERM] -> Set.Set SORT
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos supersorts = common_supersorts sign . map term_sort
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos eq = xeq_TUPLE sign
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos qualifyConds :: FORMULA -> [[([TERM], SORT)]] -> [[(TERM, SORT)]]
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos qualifyConds f = map $ map (qualify_cond f)
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos qualify_cond :: FORMULA -> ([TERM], SORT) -> (TERM, SORT)
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos qualify_cond f (ts, s) = case ts of
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos [t1, t2] -> (Conditional t1 f t2 [], s)
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos _ -> (Unparsed_term "" [],s) {-error
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos $ "Internal Error: wrong number of TERMs in qualify_cond!"-}
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos get_profile :: [[TERM]] -> [([TERM], SORT)]
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos get_profile cs
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos = [ (c, s) | -- :: ([TERM], SORT)
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher c <- permute cs, -- :: [TERM]
499718cb04a534ba76ee9dfb055c2bfc96fdeeb3Ondrej Kos have_supersort c, -- :: Bool
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher s <- Set.toList $ supersorts c ] -- :: SORT
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher{-----------------------------------------------------------
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher Divide a Set (List) into equivalence classes w.r. to eq
21d485184df986e1a123f70c689517386e51a5ceMichal Zidek-----------------------------------------------------------}
21d485184df986e1a123f70c689517386e51a5ceMichal Zidek-- also look below for Till's SML-version of this
21d485184df986e1a123f70c689517386e51a5ceMichal Zidekequivalence_Classes :: (a -> a -> Bool) -> [a] -> [[a]]
21d485184df986e1a123f70c689517386e51a5ceMichal Zidekequivalence_Classes _ [] = []
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagherequivalence_Classes eq (x:l) = xs':(equivalence_Classes eq ys)
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher (xs, ys) = partition (eq x) l
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek{-----------------------------------------------------------
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher Transform a list [l1,l2, ... ln] to (in sloppy notation)
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher [[x1,x2, ... ,xn] | x1<-l1, x2<-l2, ... xn<-ln]
99dd40a885ed3d42af4bbbde7ee2fc98830544d0Pavel Březina-----------------------------------------------------------}
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagherpermute :: [[a]] -> [[a]]
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagherpermute [] = [[]]
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagherpermute [x] = map (\y -> [y]) x
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagherpermute (x:l) = concat (map (distribute (permute l)) x)
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher distribute perms y = map ((:) y) perms
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher{-----------------------------------------------------------
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher Like 'and (zipWith p as bs)',
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher but must return False if lengths don't match
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagher-----------------------------------------------------------}
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagherzipped_all :: (a -> b -> Bool) -> [a] -> [b] -> Bool
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagherzipped_all _ [] [] = True
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagherzipped_all p (a:as) (b:bs) = (p a b) && (zipped_all p as bs)
2dd3faebcd3cfd00efda38ffd2585d675e696b12Stephen Gallagherzipped_all _ _ _ = False
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen Gallagher{-----------------------------------------------------------
2ce00e0d3896bb42db169d1e79553a81ca837a22Simo Sorce Construct a TERM of type Sorted_term
8c8cbddeabe585377a5fb3d5df09cc9a236b77ddJan Zeleny from each (TERM, SORT) tuple
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen Gallagher-----------------------------------------------------------}
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen GallagherqualifyTerms :: [Id.Pos] -> [[(TERM, SORT)]] -> [[TERM]]
4e9631a9f1ae87317eef53145622099c46196b56Jakub HrozekqualifyTerms pos pairs = map (map qualify_term) pairs
51773686d354b82081830444c048706d83d43d65Jakub Hrozek qualify_term :: (TERM, SORT) -> TERM
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek qualify_term (t, s) = Sorted_term t s pos
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek{-----------------------------------------------------------
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek For each C in P (see above), let C' choose _one_
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek f:s \in C for each s minimal such that f:s \in C
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek-----------------------------------------------------------}
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen Gallagherminimize_op :: Sign -> [(OpType, [TERM])] -> [(OpType, [TERM])]
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen Gallagherminimize_op sign ops_n_terms
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek = concat $ map reduce ops_n_terms
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek results :: Set.Set SORT
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek results = Set.fromList (map (opRes . fst) ops_n_terms)
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek lesserSorts :: SORT -> Set.Set SORT
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek lesserSorts s = Set.intersection results (subsortsOf s sign)
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek leastSort :: SORT -> Bool
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek leastSort s = Set.size (lesserSorts s) == 1
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen Gallagher reduce :: (OpType, [TERM]) -> [(OpType, [TERM])]
21d485184df986e1a123f70c689517386e51a5ceMichal Zidek reduce x@(op,_) = if (leastSort (opRes op)) then [x] else []
21d485184df986e1a123f70c689517386e51a5ceMichal Zidek{-----------------------------------------------------------
21d485184df986e1a123f70c689517386e51a5ceMichal Zidek Workalike for minimize_op, but used inside m_e_t_cond
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen Gallagher-----------------------------------------------------------}
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen Gallagherminimize_cond :: Sign -> [([TERM], SORT)] -> [([TERM], SORT)]
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozekminimize_cond sign terms_n_sort
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek = concat $ map reduce terms_n_sort
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek sorts :: Set.Set SORT
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek sorts = Set.fromList (map snd terms_n_sort)
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek lesserSorts :: SORT -> Set.Set SORT
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek lesserSorts s = Set.intersection sorts (subsortsOf s sign)
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek leastSort :: SORT -> Bool
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek leastSort s = Set.size (lesserSorts s) == 1
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek reduce :: ([TERM], SORT) -> [([TERM], SORT)]
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek reduce x@(_,s) = if (leastSort s) then [x] else []
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozekterm_sort :: TERM -> SORT
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozekterm_sort term' = case term' of
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek (Sorted_term _ sort _ ) -> sort
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen Gallagher _ -> error -- unlikely
8c8cbddeabe585377a5fb3d5df09cc9a236b77ddJan Zeleny "minExpTerm: unsorted TERM after expansion"
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen Gallagher{-----------------------------------------------------------
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen Gallagher Set of SubSORTs common to all given SORTs
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen Gallagher-----------------------------------------------------------}
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen Gallaghercommon_subsorts :: Sign -> [SORT] -> Set.Set SORT
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozekcommon_subsorts sign = let
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek get_subsorts = flip subsortsOf sign
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek in (foldr Set.intersection Set.empty) . (map get_subsorts)
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek{-----------------------------------------------------------
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek Set of SuperSORTs common to all given SORTs
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek-----------------------------------------------------------}
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozekcommon_supersorts :: Sign -> [SORT] -> Set.Set SORT
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozekcommon_supersorts sign [] = Set.empty
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozekcommon_supersorts sign srts = let
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek get_supersorts = flip supersortsOf sign
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek in foldr1 Set.intersection $ map get_supersorts $ srts
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek{-----------------------------------------------------------
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek True if all SORTs have a common subSORT
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek-----------------------------------------------------------}
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozekhave_common_subsorts :: Sign -> [SORT] -> Bool
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozekhave_common_subsorts s = (not . Set.isEmpty . common_subsorts s)
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek{-----------------------------------------------------------
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek True if all SORTs have a common superSORT
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek-----------------------------------------------------------}
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozekhave_common_supersorts :: Sign -> [SORT] -> Bool
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozekhave_common_supersorts s = (not . Set.isEmpty . common_supersorts s)
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek{-----------------------------------------------------------
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek True if s1 <= s2 OR s1 >= s2
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek-----------------------------------------------------------}
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozekxeq_SORT :: Sign -> SORT -> SORT -> Bool
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozekxeq_SORT sign s1 s2 = (leq_SORT sign s1 s2) || (geq_SORT sign s1 s2)
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek{-----------------------------------------------------------
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek True if s1 <= s2 OR s1 >= s2
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek-----------------------------------------------------------}
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozekxeq_TUPLE :: Sign -> (a, SORT) -> (a, SORT) -> Bool
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozekxeq_TUPLE sign (_,s1) (_,s2) = xeq_SORT sign s1 s2
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek{-----------------------------------------------------------
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek True if s1 <= s2
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozek-----------------------------------------------------------}
28d1ff294f7d612f6d37c82ed426b8bf5c34bfafJakub Hrozekleq_SORT :: Sign -> SORT -> SORT -> Bool
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozekleq_SORT sign s1 s2 = Set.member s2 (supersortsOf s1 sign)
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek-- leq_SORT = (flip Set.member) . (flip supersortsOf)
99c0cfdc5f065ba38f1ee91701d1d27f9e4fdb96Simo Sorce{-----------------------------------------------------------
51773686d354b82081830444c048706d83d43d65Jakub Hrozek True if s1 >= s2
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek-----------------------------------------------------------}
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozekgeq_SORT :: Sign -> SORT -> SORT -> Bool
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozekgeq_SORT sign s1 s2 = Set.member s2 (subsortsOf s1 sign)
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen Gallagher-- geq_SORT = (flip Set.member) . (flip subsortsOf)
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek{-----------------------------------------------------------
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek True if o1 ~F o2
4e9631a9f1ae87317eef53145622099c46196b56Jakub Hrozek-----------------------------------------------------------}
4e9631a9f1ae87317eef53145622099c46196b56Jakub HrozekleqF :: Sign -> OpType -> OpType -> Bool
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen GallagherleqF sign o1 o2 = zipped_all are_legal (opArgs o1) (opArgs o2)
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen Gallagher && have_common_supersorts sign [(opRes o1), (opRes o2)]
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen Gallagher where are_legal a b = have_common_subsorts sign [a, b]
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen Gallagher{-----------------------------------------------------------
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen Gallagher True if p1 ~P p2
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen Gallagher-----------------------------------------------------------}
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen GallagherleqP :: Sign -> PredType -> PredType -> Bool
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen GallagherleqP sign p1 p2 = zipped_all are_legal (predArgs p1) (predArgs p2)
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen Gallagher where are_legal a b = have_common_subsorts sign [a, b]
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen GallagherDie alten SML-Funktionen, die hier verwandt wurden.
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen GallagherDen Beschreibungen nach sind das genau die beiden, mit denen eine Menge in
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen GallagherAequivalenzklassen unterteilt wird.
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen GallagherWie die erste davon funktioniert, ist mir nicht offen ersichtlich,
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen Gallagheraber vielleicht brauch ich die eigentlich auch gar nicht?
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen Gallagher(* Compute the connected compenents of a graph which is given
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen Gallagher by a list of nodes and a boolean function indicating whether
2ce00e0d3896bb42db169d1e79553a81ca837a22Simo Sorce there is an egde between two nodes.
8c8cbddeabe585377a5fb3d5df09cc9a236b77ddJan Zeleny For each node, the algorithm splits the connected components
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen Gallagher which have been computed so far into two categories:
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen Gallagher those which are connected to the node and those which are not.
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen Gallagher The former are all linked with @ in order to form a new connected
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen Gallagher component, the latter are left untouched. *)
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen Gallagherfun compute_conn_components (edges:'a*'a->bool) (nodes:'a list):'a list list =
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen Gallagher fun is_connected(node,nil) = false
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen Gallagher | is_connected(node,n::c) =
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen Gallagher edges(node,n) orelse edges(n,node) orelse is_connected(node,c)
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen Gallagher fun split_components(node,nil,acc_comp_of_node,acc_other_comps) =
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen Gallagher (node::acc_comp_of_node)::acc_other_comps
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen Gallagher | split_components(node,current_comp::other_comps,acc_comp_of_node,acc_other_comps) =
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen Gallagher if is_connected(node,current_comp)
4c08db0fb0dda3d27b1184248ca5c800d7ce23f0Michal Zidek then split_components(node,other_comps,current_comp@acc_comp_of_node,acc_other_comps)
4c08db0fb0dda3d27b1184248ca5c800d7ce23f0Michal Zidek else split_components(node,other_comps,acc_comp_of_node,current_comp::acc_other_comps)
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen Gallagher fun add_node (node:'a,components:'a list list):'a list list =
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen Gallagher split_components(node,components,nil,nil)
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen Gallagher foldr add_node (nodes,[])
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen Gallagher(* Compute the equivalence classes of the equivalence closures of leqF and leqP resp.
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen Gallagher and store them in a table indexed by function and predicate names, resp.
8c8cbddeabe585377a5fb3d5df09cc9a236b77ddJan Zeleny This is needed when checking if terms or predications are equivalent, since
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen Gallagher this equivalence is defined in terms of the equivalence closures of leqF and leqP resp. *)
8c8cbddeabe585377a5fb3d5df09cc9a236b77ddJan Zelenyfun get_conn_components (env:local_env) : local_env1 =
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen Gallagher val (srts,vars,funs,preds) = env
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen Gallagher (env,(Symtab_id.map (compute_conn_components (leqF env)) funs ,
b6a8bdebb40a63d2adc50c574fee88229d1e8f3dStephen Gallagher Symtab_id.map (compute_conn_components (leqP env)) preds) )