Overload.hs revision d1bde0959b9c4c30eb8d1d38187ae3588bae4abc
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens Elkner Module : $Header$
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder Copyright : (c) Martin K�hl, T. Mossakowski, C. Maeder, Uni Bremen 2004
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder Licence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder Maintainer : hets@tzi.de
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder Stability : provisional
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder Portability : portable
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder Overload resolution
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder Follows Sect. III:3.3 of the CASL Reference Manual.
99b26e2ab8ba89bc9a050c1524137eb6269e2753Christian Maeder The algorthim is from
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maeder Till Mossakowski, Kolyang, Bernd Krieg-Brueckner:
4cc0a3156ac9f0f1e080433f8c4d050712e09d2bmcodescu Static semantic analysis and theorem proving for CASL.
4cc0a3156ac9f0f1e080433f8c4d050712e09d2bmcodescu 12th Workshop on Algebraic Development Techniques, Tarquinia 1997,
4cc0a3156ac9f0f1e080433f8c4d050712e09d2bmcodescu LNCS 1376, p. 333-348
25da71ee832b729e33def344a68f59fe21ce9c07Eugen Kuksaimport CASL.Sign -- Sign, OpType
92ae4d5885ea837ffe3dae9b2de742f871229b94Christian Maederimport CASL.AS_Basic_CASL -- FORMULA, OP_{NAME,SYMB}, TERM, SORT, VAR
ef1c24c8229ade3ac872febebd18c181e32fb9c4Christian Maederimport qualified Common.Lib.Map as Map
8d2321e17a34951fbd52f68e9f9f148f0890e471Christian Maederimport qualified Common.Lib.Set as Set
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maederimport qualified Common.Id as Id
99b26e2ab8ba89bc9a050c1524137eb6269e2753Christian Maederimport qualified Common.AS_Annotation as Named
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder - global Infos aus Sign berechnen + mit durchreichen
18b36f727b1d0be6ce1ec918de15f5c17da7b53fcmaeder (connected compenents, s.u.)
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder - rekursiv in FORMULA absteigen, bis atomare Formel erreicht wird
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder - atomaren Formeln mit minExpTerm behandeln
ef1c24c8229ade3ac872febebd18c181e32fb9c4Christian Maeder * generalize 'is_unambiguous' (see 'choose') and make it available globally
945e82ed7877917f3ab1657f555e71991372546aChristian Maeder * replace 'case' statements w/ pattern matching where possible
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder * generalize minExpFORMULA_pred/minExpTerm_op/minExpTerm_cond
5606c84ebef3de545602e215bbd87931334d48f0mcodescu * utilize Sets instead of Lists
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder * check whether Qual_var expansion works as it is supposed to
ef1c24c8229ade3ac872febebd18c181e32fb9c4Christian Maeder * generalize expansion for Qual_var and Sorted_term
ef1c24c8229ade3ac872febebd18c181e32fb9c4Christian Maeder * move structural logic to higher levels, as e.g. in
7c99a6c982aaf61547de8054296c8055c8d1a13aSimon Ulbricht qualifyOps = map (map qualify_op) -- map should go somewhere above
ef1c24c8229ade3ac872febebd18c181e32fb9c4Christian Maeder * sweep op-like logic from minExpTerm_cond where it is unneeded
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder * generalize zipped_all
d97700a22b2585ece83b05f3fff945fdfd0c44b4Christian Maeder * generalize qualifyTerms or implement locally - too much structural force
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder * gemeralize minimize_* or implement locally - needed only in one f. each
1d65a799298f6b1253d774c22f61029e6eb99cadcmaeder * use more let/in constructs (instead of where) to simulate workflow
ea5ccb1c6e89486a54e1f4bd95840147e96093edChristian Maeder * use common upper bounds for membership and projection
de8eee2014437ec4020be15cd363257f87e79943Christian Maeder then re-include "BEWARE: Restriction to minimal...."
fd94a6f66ccb5cef99aa42069b61e4b8734dbd3fChristian Maeder{-----------------------------------------------------------
f674d7a58db3f991300a708f3799d80c369781f8Eugen Kuksa Overload Resolution
fd94a6f66ccb5cef99aa42069b61e4b8734dbd3fChristian Maeder-----------------------------------------------------------}
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maedertype Min f e = GlobalAnnos -> Sign f e -> f -> Result f
473f5af6e4803fbeecc814065952396f2501039bChristian MaederoverloadResolution :: (Eq f, PrettyPrint f) =>
473f5af6e4803fbeecc814065952396f2501039bChristian Maeder Min f e -> GlobalAnnos -> Sign f e
473f5af6e4803fbeecc814065952396f2501039bChristian Maeder -> [Named.Named (FORMULA f)]
473f5af6e4803fbeecc814065952396f2501039bChristian Maeder -> Result [Named.Named (FORMULA f)]
e42249ec61f50a83525db6e5fc9f5c4dd1b4cf5fcmaederoverloadResolution mef ga sign = mapM overload
473f5af6e4803fbeecc814065952396f2501039bChristian Maeder overload sent = do
20bbcc2b693b3040d7b8cc92ba966580637027d9cmaeder let sent' = Named.sentence sent
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa --debug 1 ("sent'",sent')
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder exp_sent <- minExpFORMULA mef ga sign sent'
e42249ec61f50a83525db6e5fc9f5c4dd1b4cf5fcmaeder --debug 2 ("exp_sent",exp_sent)
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder return sent { Named.sentence = exp_sent }
ea5ccb1c6e89486a54e1f4bd95840147e96093edChristian Maeder{-----------------------------------------------------------
c8afa08a8bda589ef6670068dff0108464be4da7Christian Maeder Minimal Expansions of a FORMULA
c99b0eb6632087d502dd4269599c5aa68a148eebSimon Ulbricht-----------------------------------------------------------}
b99c9606f2faafeabb3fa8c596992143a561c787Simon UlbrichtminExpFORMULA :: (Eq f, PrettyPrint f) => Min f e -> GlobalAnnos ->
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa Sign f e -> (FORMULA f) -> Result (FORMULA f)
df67ddf64192bfcae6ece65255ad796a17cbe532Christian MaederminExpFORMULA mef ga sign formula
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder = case formula of
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder -- Trivial Atom -> Return untouched
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder True_atom _ -> return formula -- :: FORMULA
526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder False_atom _ -> return formula -- :: FORMULA
473f5af6e4803fbeecc814065952396f2501039bChristian Maeder -- Non-Atomic FORMULA -> Recurse through subFORMULAe
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder Quantification q vars f pos -> do
c24f7998fe7dfca4277f83076a119aabfe6186a0mcodescu let (_, sign') = runState (mapM_ addVars vars) sign
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder f' <- minExpFORMULA mef ga sign' f
526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder return $ Quantification q vars f' pos
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa Conjunction fs pos -> do
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa fs' <- mapM (minExpFORMULA mef ga sign) fs
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder return $ Conjunction fs' pos
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maeder Disjunction fs pos -> do
dae8246f1f55b6a85e946fc1bfb6d32d556395f1Simon Ulbricht fs' <- mapM (minExpFORMULA mef ga sign) fs
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder return $ Disjunction fs' pos
64f5f0a8c38d5b2ba33b09e02e92b0e3f812d6d0Eugen Kuksa Implication f1 f2 b pos -> do
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maeder f1' <- minExpFORMULA mef ga sign f1
6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder f2' <- minExpFORMULA mef ga sign f2
f56cdf11927c31495bae642a9eb383212c90ba61Christian Maeder return $ Implication f1' f2' b pos
7710f7c3425e45af11af124ff37bec27229d24f7Christian Maeder Equivalence f1 f2 pos -> do
2e2559f894aaa661b199e4fa00609f522bc5482aSimon Ulbricht f1' <- minExpFORMULA mef ga sign f1
df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder f2' <- minExpFORMULA mef ga sign f2
be1ce1c2b2819ef32743136c13101f1927375311Christian Maeder return $ Equivalence f1' f2' pos
6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder Negation f pos -> do
f674d7a58db3f991300a708f3799d80c369781f8Eugen Kuksa f' <- minExpFORMULA mef ga sign f
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder return $ Negation f' pos
5896f38ba2934056542cb7cb3e6359e88a622547Christian Maeder -- Atomic FORMULA -> Check for Ambiguities
526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder Predication predicate terms pos ->
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder minExpFORMULA_pred mef ga sign predicate terms pos -- :: FORMULA
526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder Definedness term pos -> do
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder t <- minExpTerm mef ga sign term -- :: [[TERM]]
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa --debug 4 ("t", t)
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa t' <- is_unambiguous term t pos -- :: TERM
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder return $ Definedness t' pos -- :: FORMULA
6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder Existl_equation term1 term2 pos ->
6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder minExpFORMULA_eq mef ga sign Existl_equation term1 term2 pos
6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder Strong_equation term1 term2 pos ->
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder minExpFORMULA_eq mef ga sign Strong_equation term1 term2 pos
e98c3d3efab62d97ebdeed52f4109d961f6432aaChristian Maeder Membership term sort pos -> do
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder t <- minExpTerm mef ga sign term -- :: [[TERM]]
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder t' <- let leq_term [] = False
8f9ac967da20be8d7782d2fc0a085dd42f79c0cbEugen Kuksa leq_term (t1:_) =
8f9ac967da20be8d7782d2fc0a085dd42f79c0cbEugen Kuksa leq_SORT sign sort $ term_sort t1
6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder in return $ filter leq_term t -- :: TERM
703004db20b23870f080c4d9640729b19b7c2288Eugen Kuksa t'' <- is_unambiguous term t' pos -- :: [[TERM]]
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder return $ Membership t'' sort pos -- :: FORMULA
26acf851cacd7a31bdc9b25a42af9949942fa7c6Christian Maeder Sort_gen_ax _ _ -> return formula
26acf851cacd7a31bdc9b25a42af9949942fa7c6Christian Maeder ExtFORMULA f -> fmap ExtFORMULA $ mef ga sign f
5896f38ba2934056542cb7cb3e6359e88a622547Christian Maeder _ -> error $ "minExpFORMULA: unexpected type of FORMULA: "
5896f38ba2934056542cb7cb3e6359e88a622547Christian Maeder ++ (show formula)
5fb6343a5a2b4bbc67bc83479c84a92d23d30edfChristian Maederis_unambiguous :: (Eq f, PrettyPrint f) => TERM f -> [[TERM f]]
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder -> [Id.Pos] -> Result (TERM f)
eca54dc24f2c59cc51645115347a89ba2b40de36cmaederis_unambiguous topterm term pos = do
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder case term of
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder [] -> pplain_error (Unparsed_term "<error>" [])
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maeder (ptext "No correct typing for " <+> printText topterm)
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maeder (_:_):_ -> return $ head $ head $ term -- :: TERM
5fb6343a5a2b4bbc67bc83479c84a92d23d30edfChristian Maeder -- BEWARE! Oversimplified disambiguation!
6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder --(_:_):[] -> return head $ head term -- :: TERM
12882fa70d12d9b56cbd850ccb4b724feb3c62d5Christian Maeder _ -> pplain_error (Unparsed_term "<error>" [])
12882fa70d12d9b56cbd850ccb4b724feb3c62d5Christian Maeder (ptext "Cannot disambiguate!\nPossible Expansions: "
12882fa70d12d9b56cbd850ccb4b724feb3c62d5Christian Maeder <+> (printText term)) (Id.headPos pos)
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder{-----------------------------------------------------------
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder Minimal Expansions of a Predicate Application Formula
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder-----------------------------------------------------------}
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian MaederminExpFORMULA_pred :: (Eq f, PrettyPrint f) => Min f e -> GlobalAnnos ->
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder Sign f e -> PRED_SYMB -> [TERM f] -> [Id.Pos]
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder -> Result (FORMULA f)
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian MaederminExpFORMULA_pred mef ga sign predicate terms pos = do
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder expansions <- mapM
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder (minExpTerm mef ga sign) terms -- :: [[[TERM]]]
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder --debug 5 ("expansions", expansions)
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder permuted_exps <- return
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder $ permute expansions -- :: [[[TERM]]]
b87fb5d6d5aba8fc6d3c528f7da0af228ca76b02Eugen Kuksa profiles <- return
dfa31ad230c88a66a9722c2a5ab23fe82c33f014Eugen Kuksa $ map get_profile permuted_exps -- :: [[(PredType, [TERM])]]
b87fb5d6d5aba8fc6d3c528f7da0af228ca76b02Eugen Kuksa --debug 6 ("profiles", profiles)
b87fb5d6d5aba8fc6d3c528f7da0af228ca76b02Eugen Kuksa $ concat -- :: [[(PredType, [TERM])]]
b87fb5d6d5aba8fc6d3c528f7da0af228ca76b02Eugen Kuksa $ map (equivalence_Classes pred_eq) -- :: [[[(PredType, [TERM])]]]
8723ec450f2e7a024230467c0c28a3f154905483cmaeder profiles -- :: [[(PredType, [TERM])]]
8723ec450f2e7a024230467c0c28a3f154905483cmaeder --debug 7 ("p", p)
7b21830970250ca6369b0ae60f34c990f9a5c5bfTill Mossakowski p' <- choose p -- :: (PredType, [TERM])
e99cb5db53054d96bb97c9b8b130bd249802450eTill Mossakowski return $ qualify_pred p'
e99cb5db53054d96bb97c9b8b130bd249802450eTill Mossakowski name :: PRED_NAME
e99cb5db53054d96bb97c9b8b130bd249802450eTill Mossakowski name = pred_name predicate
8723ec450f2e7a024230467c0c28a3f154905483cmaeder preds :: [PredType]
8723ec450f2e7a024230467c0c28a3f154905483cmaeder Set.empty name $ (predMap sign)
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa pred_name :: PRED_SYMB -> PRED_NAME
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa pred_name pred' = case pred' of
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa (Pred_name name') -> name'
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa (Qual_pred_name name' _ _) -> name'
d3d8d20d41aaaa107cf2dfa4dd0434e6a08b22d5Till Mossakowski-- choose :: [[(PredType, [TERM f])]] -> Result (PredType, [TERM f])
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder choose ps = case ps of
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa [] -> pplain_error (PredType [],[])
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa (ptext "No correct typing for"
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa <+> printText (Predication predicate terms pos))
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa -- BEWARE! Oversimplified disambiguation!
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa --(p:_):[] -> return p
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa (_:_):_ -> return $ head $ head ps
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa _ -> pplain_error (PredType [], terms)
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa (ptext "Cannot disambiguate! Term: "
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa <+> (printText (predicate, terms))
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa $$ ptext "Possible Expansions: "
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa <+> (printText ps)) (Id.posOfId name)
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa qualify_pred :: (PredType, [TERM f]) -> FORMULA f
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa qualify_pred (pred', terms')
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa = (Predication -- :: FORMULA
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa (Qual_pred_name name (toPRED_TYPE pred') []) -- :: PRED_SYMB
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa terms' -- :: [TERM]
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa pos) -- :: [Pos]
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa get_profile :: [[TERM f]] -> [(PredType, [TERM f])]
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa get_profile cs
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa = [ (pred', ts) |
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa pred' <- preds, -- :: PredType
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa ts <- (permute cs), -- :: [TERM]
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa zipped_all (leq_SORT sign) -- :: Bool
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa (map term_sort ts) -- :: [SORT]
31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder (predArgs pred') ] -- :: [SORT]
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder pred_eq :: (PredType, [TERM f]) -> (PredType, [TERM f]) -> Bool
1f0483f71bad0707f10293d0b4db4649aa93fb35Christian Maeder neuer Algorithmus:
1f0483f71bad0707f10293d0b4db4649aa93fb35Christian Maeder checken, ob Pr�dikatsymbole und Argument-Terme �quivalent sind.
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder F�r letzteres pro Argument-Position in expansions nachgucken.
c5b8b64377e24bcbf5cc108ca433cfbbd6235ba1Christian Maeder Dto. f�r Operationen.
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder Injektionen: op:w->s(t_i) : s' ----> "_inj":s->s'(op:w->s(t_i)) : s'
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder pred_eq (pred1,ts1) (pred2,ts2)
c5b8b64377e24bcbf5cc108ca433cfbbd6235ba1Christian Maeder = let w1 = predArgs pred1 -- :: [SORT]
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder w2 = predArgs pred2 -- :: [SORT]
c5b8b64377e24bcbf5cc108ca433cfbbd6235ba1Christian Maeder s1 = map term_sort ts1 -- :: [SORT]
26acf851cacd7a31bdc9b25a42af9949942fa7c6Christian Maeder s2 = map term_sort ts2 -- :: [SORT]
293abe6af19382a456dbe612aef45054ef76832fcmaeder b1 = zipped_all (leq_SORT sign) s1 w1 -- :: Bool
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder b2 = zipped_all (leq_SORT sign) s2 w2 -- :: Bool
8723ec450f2e7a024230467c0c28a3f154905483cmaeder preds_equal = (pred1 == pred2) -- :: Bool
7b21830970250ca6369b0ae60f34c990f9a5c5bfTill Mossakowski preds_equiv = leqP sign pred1 pred2 -- :: Bool
e99cb5db53054d96bb97c9b8b130bd249802450eTill Mossakowski types_equal = False -- and (zipWith (==) s1 s2) -- :: Bool
8e3e7896a1818bb0521674cf4f10403e9f9911b3Till Mossakowski in b1 && b2 && (preds_equal
e5f71ad96ddbaafd3bf8ae0820df93e0db4b0527cmaeder || (preds_equiv
8723ec450f2e7a024230467c0c28a3f154905483cmaeder && types_equal))
8723ec450f2e7a024230467c0c28a3f154905483cmaeder{-----------------------------------------------------------
8723ec450f2e7a024230467c0c28a3f154905483cmaeder Minimal Expansions of a Strong/Existl. Equation Formula
5d93620c37abd9c665d3fe532d4852d62dff4233Christian Maeder-----------------------------------------------------------}
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian MaederminExpFORMULA_eq :: (Eq f, PrettyPrint f) => Min f e -> GlobalAnnos ->
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder Sign f e -> (TERM f -> TERM f -> [Id.Pos] -> FORMULA f)
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder -> TERM f -> TERM f -> [Id.Pos] -> Result (FORMULA f)
5d93620c37abd9c665d3fe532d4852d62dff4233Christian MaederminExpFORMULA_eq mef ga sign eq term1 term2 pos = do
5d93620c37abd9c665d3fe532d4852d62dff4233Christian Maeder exps1 <- minExpTerm mef ga sign term1 -- :: [[TERM]]
232c13ff6847a6f2bac7163392f80ab692cd7774Christian Maeder exps2 <- minExpTerm mef ga sign term2 -- :: [[TERM]]
12882fa70d12d9b56cbd850ccb4b724feb3c62d5Christian Maeder --debug 1 ("exps1",exps1)
4bd27a2cb9efd5d8ff00b5cf823487403add724ecmaeder --debug 2 ("exps2",exps2)
5d93620c37abd9c665d3fe532d4852d62dff4233Christian Maeder pairs <- return
99b26e2ab8ba89bc9a050c1524137eb6269e2753Christian Maeder $ permute [catMaybes (map maybeHead exps1),
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder catMaybes (map maybeHead exps2)] -- :: [[TERM]]
26acf851cacd7a31bdc9b25a42af9949942fa7c6Christian Maeder --debug 3 ("pairs",pairs)
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder candidates <- return
c5b8b64377e24bcbf5cc108ca433cfbbd6235ba1Christian Maeder $ filter fit pairs -- :: [[TERM]]
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder --debug 3 ("candidates",candidates)
99b26e2ab8ba89bc9a050c1524137eb6269e2753Christian Maeder case candidates of
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder [] -> pplain_error (eq term1 term2 pos)
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder (ptext "No correct typing for "
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder <+> printText (eq term1 term2 pos))
4937a0e373f619dc520799923acec42db5da5eb3Eugen Kuksa -- BEWARE! Oversimplified disambiguation!
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder ([t1,t2]:_) -> return $ eq t1 t2 pos
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder --([t1,t2]:[]) -> return $ eq t1 t2 pos
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder _ -> pplain_error (eq term1 term2 pos)
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder (ptext "Cannot disambiguate! Possible Expansions: "
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder <+> (printText exps1) $$ (printText exps2)) (Id.headPos pos)
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder fit :: [TERM f] -> Bool
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder fit = (have_common_supersorts sign) . (map term_sort)
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder maybeHead :: [a] -> Maybe a
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder maybeHead (x:_) = Just x
df24d7f0c79862ffd8189698645e201bf07a4d9cEugen Kuksa maybeHead _ = Nothing
feb9227bb5c49d5bea1a112500c3b3eba31abdfbcmaeder{-----------------------------------------------------------
df24d7f0c79862ffd8189698645e201bf07a4d9cEugen Kuksa Minimal Expansions of a TERM
df24d7f0c79862ffd8189698645e201bf07a4d9cEugen Kuksa-----------------------------------------------------------}
df24d7f0c79862ffd8189698645e201bf07a4d9cEugen KuksaminExpTerm :: (Eq f, PrettyPrint f) => Min f e -> GlobalAnnos ->
df24d7f0c79862ffd8189698645e201bf07a4d9cEugen Kuksa Sign f e -> TERM f -> Result [[TERM f]]
feb9227bb5c49d5bea1a112500c3b3eba31abdfbcmaederminExpTerm mef ga sign term'
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder = do -- debug 6 ("term'",term')
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder u <- case term' of
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder Simple_id var
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa -> minExpTerm_simple sign var
dfa31ad230c88a66a9722c2a5ab23fe82c33f014Eugen Kuksa Qual_var var sort pos
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa -> minExpTerm_qual sign var sort pos
64f5f0a8c38d5b2ba33b09e02e92b0e3f812d6d0Eugen Kuksa Application op terms pos
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa -> minExpTerm_op mef ga sign op terms pos
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa Sorted_term term sort pos
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa -> minExpTerm_sorted mef ga sign term sort pos
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa Cast term sort pos
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa -> minExpTerm_cast mef ga sign term sort pos
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa Conditional term1 formula term2 pos
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa -> minExpTerm_cond mef ga sign term1 formula term2 pos
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa _ -> error "minExpTerm"
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa{-----------------------------------------------------------
ab38e2fac740c4336afafbe0584053dc2e67002bEugen Kuksa Minimal Expansions of a Simple_id Term
dfa31ad230c88a66a9722c2a5ab23fe82c33f014Eugen Kuksa-----------------------------------------------------------}
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen KuksaminExpTerm_simple ::
ab38e2fac740c4336afafbe0584053dc2e67002bEugen Kuksa Sign f e -> Id.SIMPLE_ID -> Result [[TERM f]]
ab38e2fac740c4336afafbe0584053dc2e67002bEugen KuksaminExpTerm_simple sign var = do
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa vars <- return
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa Set.empty var (varMap sign)
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa ops' <- return
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa Set.empty name (opMap sign)
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa ops <- return
dfa31ad230c88a66a9722c2a5ab23fe82c33f014Eugen Kuksa $ (map opRes) -- :: [SORT]
e99cb5db53054d96bb97c9b8b130bd249802450eTill Mossakowski $ Set.toList -- :: [OpType]
ab38e2fac740c4336afafbe0584053dc2e67002bEugen Kuksa ops' -- :: Set.Set OpType
ab38e2fac740c4336afafbe0584053dc2e67002bEugen Kuksa cs <- return
d16243f2fd4825f598eee589b68e324e23eb469dEugen Kuksa least <- return
ab38e2fac740c4336afafbe0584053dc2e67002bEugen Kuksa -- BEWARE: Restriction to minimal sorts is not correct
ab38e2fac740c4336afafbe0584053dc2e67002bEugen Kuksa -- in case of downcasts: here, it may be the
ab38e2fac740c4336afafbe0584053dc2e67002bEugen Kuksa -- case that the cast is only correct for non-minimal sorts!
64f5f0a8c38d5b2ba33b09e02e92b0e3f812d6d0Eugen Kuksa $ {-Set.filter (is_least_sort cs)-} cs -- :: Set.Set SORT
64f5f0a8c38d5b2ba33b09e02e92b0e3f812d6d0Eugen Kuksa $ qualifyTerms [] -- :: [[TERM]]
64f5f0a8c38d5b2ba33b09e02e92b0e3f812d6d0Eugen Kuksa $ (equivalence_Classes eq) -- :: [[(TERM, SORT)]]
64f5f0a8c38d5b2ba33b09e02e92b0e3f812d6d0Eugen Kuksa $ map pair_with_id -- :: [(TERM, SORT)]
64f5f0a8c38d5b2ba33b09e02e92b0e3f812d6d0Eugen Kuksa $ Set.toList least -- :: [SORT]
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder is_const_op :: OpType -> Bool
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder is_const_op op = (null . opArgs) op
8723ec450f2e7a024230467c0c28a3f154905483cmaeder is_least_sort :: Set.Set SORT -> SORT -> Bool
8723ec450f2e7a024230467c0c28a3f154905483cmaeder is_least_sort ss s
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder = Set.size (Set.intersection ss (subsortsOf s sign)) == 1
8723ec450f2e7a024230467c0c28a3f154905483cmaeder eq = xeq_TUPLE sign
8723ec450f2e7a024230467c0c28a3f154905483cmaeder pair_with_id :: SORT -> (TERM f, SORT)
0b144823976d79a34bff62f7f9ec032e80b8ce85Simon Ulbricht pair_with_id sort | isVar sort = ((Qual_var var sort []), sort)
12882fa70d12d9b56cbd850ccb4b724feb3c62d5Christian Maeder | otherwise = (Application (Qual_op_name name (Total_op_type [] sort [] )[]) [] [],sort) -- should deal with partial constants as well!!!!
0b144823976d79a34bff62f7f9ec032e80b8ce85Simon Ulbricht isVar :: SORT -> Bool
0b144823976d79a34bff62f7f9ec032e80b8ce85Simon Ulbricht{-----------------------------------------------------------
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa Minimal Expansions of a Qual_var Term
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa-----------------------------------------------------------}
8723ec450f2e7a024230467c0c28a3f154905483cmaederminExpTerm_qual ::
9542b929f3cfabf1491c3f0489acf92ba703968fmcodescu Sign f e -> VAR -> SORT -> [Id.Pos] -> Result [[TERM f]]
9542b929f3cfabf1491c3f0489acf92ba703968fmcodescuminExpTerm_qual sign var sort pos = do
0b144823976d79a34bff62f7f9ec032e80b8ce85Simon Ulbricht expandedVar <- minExpTerm_simple sign var -- :: [[TERM]]
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht $ qualifyTerms pos -- :: [[TERM]]
233754e153e665aa748bf8b45bd8b1938b6c21a7Christian Maeder $ map selectExpansions expandedVar -- :: [[(TERM, SORT)]]
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht fits :: TERM f -> Bool
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht fits term = case term of
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht (Sorted_term (Qual_var var' _ _) sort' _)
8723ec450f2e7a024230467c0c28a3f154905483cmaeder -> (var == var') && (sort == sort')
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht _ -> error "minExpTerm_qual: unsorted TERM after expansion"
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht selectExpansions :: [TERM f] -> [(TERM f, SORT)]
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht selectExpansions c
8723ec450f2e7a024230467c0c28a3f154905483cmaeder = [ ((Qual_var var sort []), sort) | -- :: (TERM, SORT)
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder sorted <- c, -- :: TERM
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht fits sorted ] -- :: Bool
12882fa70d12d9b56cbd850ccb4b724feb3c62d5Christian Maeder{-----------------------------------------------------------
0b144823976d79a34bff62f7f9ec032e80b8ce85Simon Ulbricht Minimal Expansions of a Sorted_term Term
8723ec450f2e7a024230467c0c28a3f154905483cmaeder-----------------------------------------------------------}
8723ec450f2e7a024230467c0c28a3f154905483cmaederminExpTerm_sorted :: (Eq f, PrettyPrint f) => Min f e -> GlobalAnnos ->
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht Sign f e -> TERM f -> SORT -> [Id.Pos] -> Result [[TERM f]]
12882fa70d12d9b56cbd850ccb4b724feb3c62d5Christian MaederminExpTerm_sorted mef ga sign term sort pos = do
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht expandedTerm <- minExpTerm mef ga sign term -- :: [[TERM]]
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht --debug 7 ("expandedTerm", expandedTerm)
8723ec450f2e7a024230467c0c28a3f154905483cmaeder $ qualifyTerms pos -- :: [[TERM]]
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht $ map selectExpansions expandedTerm -- :: [[(TERM, SORT)]]
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht selectExpansions :: [TERM f] -> [(TERM f, SORT)]
8723ec450f2e7a024230467c0c28a3f154905483cmaeder selectExpansions c
de8983abdf4b35af1ed1fdee2de4dff13c2368bacmaeder = [ (sorted, sort) | -- :: (TERM, SORT)
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht sorted <- c, -- :: TERM
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht term_sort sorted == sort ] -- :: Bool
0b144823976d79a34bff62f7f9ec032e80b8ce85Simon Ulbricht{-----------------------------------------------------------
12882fa70d12d9b56cbd850ccb4b724feb3c62d5Christian Maeder Minimal Expansions of a Function Application Term
0b144823976d79a34bff62f7f9ec032e80b8ce85Simon Ulbricht-----------------------------------------------------------}
0b144823976d79a34bff62f7f9ec032e80b8ce85Simon UlbrichtminExpTerm_op :: (Eq f, PrettyPrint f) => Min f e -> GlobalAnnos ->
0b144823976d79a34bff62f7f9ec032e80b8ce85Simon Ulbricht Sign f e -> OP_SYMB -> [TERM f] -> [Id.Pos] -> Result [[TERM f]]
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon UlbrichtminExpTerm_op _ _ sign (Op_name (Id.Id [tok] [] _)) [] _ =
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht minExpTerm_simple sign tok
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon UlbrichtminExpTerm_op mef ga sign op terms pos =
ccd9cf19d129595770d592d3d0d80c6619f7a141Eugen Kuksa minExpTerm_op1 mef ga sign op terms pos
0b144823976d79a34bff62f7f9ec032e80b8ce85Simon UlbrichtminExpTerm_op1 :: (Eq f, PrettyPrint f) => Min f e -> GlobalAnnos ->
0b144823976d79a34bff62f7f9ec032e80b8ce85Simon Ulbricht Sign f e -> OP_SYMB -> [TERM f] -> [Id.Pos] -> Result [[TERM f]]
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon UlbrichtminExpTerm_op1 mef ga sign op terms pos = do
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa --debug 3 ("op",op)
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa --debug 3 ("terms",show terms)
0b144823976d79a34bff62f7f9ec032e80b8ce85Simon Ulbricht expansions <- mapM
4937a0e373f619dc520799923acec42db5da5eb3Eugen Kuksa (minExpTerm mef ga sign) terms -- :: [[[TERM]]]
4937a0e373f619dc520799923acec42db5da5eb3Eugen Kuksa --debug 9 ("expansions", expansions)
4937a0e373f619dc520799923acec42db5da5eb3Eugen Kuksa permuted_exps <- return
4f820114168836fb05b720c429866baa5665690eChristian Maeder $ permute expansions -- :: [[[TERM]]]
60e6795dd310e10194e12bb660575aadf941328bEugen Kuksa profiles <- return
4937a0e373f619dc520799923acec42db5da5eb3Eugen Kuksa $ map get_profile permuted_exps -- :: [[(OpType, [TERM])]]
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht --debug 10 ("profiles", profiles)
4937a0e373f619dc520799923acec42db5da5eb3Eugen Kuksa $ concat -- :: [[(OpType, [TERM])]]
1698621aea64f7a2b04a4084984eed1437e22771Christian Maeder $ map (equivalence_Classes op_eq) -- :: [[[(OpType, [TERM])]]]
6fb590a3747600c145abfd7c3483039fb03af032Christian Maeder profiles -- :: [[(OpType, [TERM])]]
1d65a799298f6b1253d774c22f61029e6eb99cadcmaeder --debug 3 ("p",show p)
6fb590a3747600c145abfd7c3483039fb03af032Christian Maeder $ map (minimize_op sign) p -- :: [[(OpType, [TERM])]]
6fb590a3747600c145abfd7c3483039fb03af032Christian Maeder{- debug 3 ("p'",show p')
6fb590a3747600c145abfd7c3483039fb03af032Christian Maeder debug 3 (" qualifyOps p'",show $ qualifyOps p')
6fb590a3747600c145abfd7c3483039fb03af032Christian Maeder debug 3 ("qualifyTerms pos $ qualifyOps p'",
6fb590a3747600c145abfd7c3483039fb03af032Christian Maeder show $ qualifyTerms pos $ qualifyOps p')
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht $ qualifyTerms pos -- :: [[TERM]]
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder $ qualifyOps p' -- :: [[(TERM, SORT)]]
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder name :: OP_NAME
fcd8dd6d9029180ae5e777e94a973c5e355a55cfcmaeder name = op_name op
fcd8dd6d9029180ae5e777e94a973c5e355a55cfcmaeder result :: SORT
fcd8dd6d9029180ae5e777e94a973c5e355a55cfcmaeder result = opRes $ toOpType $ op_type op
fcd8dd6d9029180ae5e777e94a973c5e355a55cfcmaeder ops :: [OpType]
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa Set.empty name $ (opMap sign)
4937a0e373f619dc520799923acec42db5da5eb3Eugen Kuksa op_name :: OP_SYMB -> OP_NAME
4937a0e373f619dc520799923acec42db5da5eb3Eugen Kuksa op_name op' = case op' of
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa (Op_name name') -> name'
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa (Qual_op_name name' _ _) -> name'
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa op_type :: OP_SYMB -> OP_TYPE
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht op_type (Op_name _) = error "unqualified op"
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht op_type (Qual_op_name _ type' _) = type'
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa qualifyOps :: [[(OpType, [TERM f])]] -> [[(TERM f, SORT)]]
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa qualifyOps = map (map qualify_op)
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa qualify_op :: (OpType, [TERM f]) -> (TERM f, SORT)
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa qualify_op (op', terms')
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa | True -- result == (opRes op')
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa = ((Application -- :: TERM
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa (Qual_op_name name (toOP_TYPE op') []) -- :: OP_SYMB
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa terms' -- :: [TERM]
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa []) -- :: [Pos]
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa , (opRes op')) -- :: SORT
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa = ((Application
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa (Qual_op_name
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa (Total_op_type [(opRes op')] result [Id.nullPos])
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa [(Application
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa (Qual_op_name name (toOP_TYPE op') [])
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa get_profile :: [[TERM f]] -> [(OpType, [TERM f])]
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa get_profile cs
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa = [ (op', ts) | -- :: (OpType, [TERM])
4ded733c298c9fd95db25858b897da482f4ab3e7Eugen Kuksa op' <- ops, -- :: OpType
4ded733c298c9fd95db25858b897da482f4ab3e7Eugen Kuksa ts <- (permute cs), -- :: [TERM]
4ded733c298c9fd95db25858b897da482f4ab3e7Eugen Kuksa zipped_all (leq_SORT sign) -- :: Bool
4ded733c298c9fd95db25858b897da482f4ab3e7Eugen Kuksa (map term_sort ts) -- :: [SORT]
4ded733c298c9fd95db25858b897da482f4ab3e7Eugen Kuksa (opArgs op') ] -- :: [SORT]
4ded733c298c9fd95db25858b897da482f4ab3e7Eugen Kuksa op_eq :: (OpType, [TERM f]) -> (OpType, [TERM f]) -> Bool
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa op_eq (op1,ts1) (op2,ts2)
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa = let w1 = opArgs op1 -- :: [SORT]
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa w2 = opArgs op2 -- :: [SORT]
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa s1 = map term_sort ts1 -- :: [SORT]
4ded733c298c9fd95db25858b897da482f4ab3e7Eugen Kuksa s2 = map term_sort ts2 -- :: [SORT]
4ded733c298c9fd95db25858b897da482f4ab3e7Eugen Kuksa b1 = zipped_all (leq_SORT sign) s1 w1 -- :: Bool
f345dca8aecfdbc7137a28dda45f9a5574d1fd14Eugen Kuksa b2 = zipped_all (leq_SORT sign) s2 w2 -- :: Bool
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa ops_equal = (op1 == op2) -- :: Bool
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa ops_equiv = leqF sign op1 op2 -- :: Bool
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa types_equal = False -- and (zipWith (==) s1 s2) -- :: Bool
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa in b1 && b2 && (ops_equal
f345dca8aecfdbc7137a28dda45f9a5574d1fd14Eugen Kuksa || (ops_equiv
f382d86a384743a770cd5490a641e38ed1069c5cChristian Maeder && types_equal))
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa{-----------------------------------------------------------
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder Minimal Expansions of a Cast Term
4937a0e373f619dc520799923acec42db5da5eb3Eugen Kuksa-----------------------------------------------------------}
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaederminExpTerm_cast :: (Eq f, PrettyPrint f) => Min f e -> GlobalAnnos ->
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht Sign f e -> TERM f -> SORT -> [Id.Pos] -> Result [[TERM f]]
f382d86a384743a770cd5490a641e38ed1069c5cChristian MaederminExpTerm_cast mef ga sign term sort pos = do
4ded733c298c9fd95db25858b897da482f4ab3e7Eugen Kuksa expandedTerm <- minExpTerm mef ga sign term -- :: [[TERM]]
4ded733c298c9fd95db25858b897da482f4ab3e7Eugen Kuksa --debug 1 ("expandedTerm",expandedTerm)
4ded733c298c9fd95db25858b897da482f4ab3e7Eugen Kuksa validExps <- return
4ded733c298c9fd95db25858b897da482f4ab3e7Eugen Kuksa $ map (filter (leq_SORT sign sort . term_sort)) -- :: [[TERM]]
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder $ expandedTerm -- :: [[TERM]]
bf51e183eda8e66f16795b35ce9a62468974b8e3Christian Maeder --debug 2 ("validExps",validExps)
562e30787355109feb0133ffea2ad86b6c143c26Simon Ulbricht $ qualifyTerms pos -- :: [[TERM]]
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaeder $ map (map (\ t -> (t, sort))) validExps -- :: [[(TERM, SORT)]]
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa{-----------------------------------------------------------
c24f7998fe7dfca4277f83076a119aabfe6186a0mcodescu Minimal Expansions of a Conditional Term
8723ec450f2e7a024230467c0c28a3f154905483cmaeder-----------------------------------------------------------}
9542b929f3cfabf1491c3f0489acf92ba703968fmcodescuminExpTerm_cond :: (Eq f, PrettyPrint f) => Min f e -> GlobalAnnos ->
9542b929f3cfabf1491c3f0489acf92ba703968fmcodescu Sign f e -> TERM f -> FORMULA f -> TERM f -> [Id.Pos]
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaeder -> Result [[TERM f]]
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon UlbrichtminExpTerm_cond mef ga sign term1 formula term2 pos = do
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder <- minExpTerm mef ga sign term1 -- :: [[TERM]]
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder expansions2
4bd27a2cb9efd5d8ff00b5cf823487403add724ecmaeder <- minExpTerm mef ga sign term2 -- :: [[TERM]]
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder expanded_formula
4bd27a2cb9efd5d8ff00b5cf823487403add724ecmaeder <- minExpFORMULA mef ga sign formula -- :: FORMULA
2e76bbbed1c936bb0aee1753837e1c50416847a2Simon Ulbricht permuted_exps <- return
8723ec450f2e7a024230467c0c28a3f154905483cmaeder $ permute [expansions1, expansions2] -- :: [[[TERM]]]
8723ec450f2e7a024230467c0c28a3f154905483cmaeder --debug 7 ("permuted_exps",permuted_exps)
8723ec450f2e7a024230467c0c28a3f154905483cmaeder profiles <- return
8723ec450f2e7a024230467c0c28a3f154905483cmaeder $ map get_profile permuted_exps -- :: [[([TERM], SORT)]]
60e6795dd310e10194e12bb660575aadf941328bEugen Kuksa --debug 7 ("profiles",profiles)
60e6795dd310e10194e12bb660575aadf941328bEugen Kuksa $ concat -- :: [[([TERM], SORT)]]
1d65a799298f6b1253d774c22f61029e6eb99cadcmaeder $ map -- :: [[[([TERM], SORT)]]]
90d3a604eeb43972cef8bfd283a0118a4ad6e9e7cmaeder (equivalence_Classes eq)
1d65a799298f6b1253d774c22f61029e6eb99cadcmaeder profiles -- :: [[([TERM], SORT)]]
2e76bbbed1c936bb0aee1753837e1c50416847a2Simon Ulbricht --debug 7 ("p",p)
8723ec450f2e7a024230467c0c28a3f154905483cmaeder p' <- return
7463a1bf64cfa90917e2afb6a5017ec411d2b3dbSimon Ulbricht $ map (minimize_cond sign) p -- :: [[([TERM], SORT)]]
7f150d7930b47c297e184638ecd811b3656b0dadChristian Maeder --debug 7 ("p'",p')
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder $ qualifyTerms pos -- :: [[TERM]]
bf51e183eda8e66f16795b35ce9a62468974b8e3Christian Maeder $ qualifyConds expanded_formula p' -- :: [[(TERM, SORT)]]
f6a562e28240e4f9107c199ba7a8e500ccfbfa55Simon Ulbricht have_supersort :: [TERM f] -> Bool
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder have_supersort = not . Set.isEmpty . supersorts
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder supersorts :: [TERM f] -> Set.Set SORT
f382d86a384743a770cd5490a641e38ed1069c5cChristian Maeder supersorts = common_supersorts sign . map term_sort
f382d86a384743a770cd5490a641e38ed1069c5cChristian Maeder eq = xeq_TUPLE sign
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht qualifyConds :: FORMULA f -> [[([TERM f], SORT)]] -> [[(TERM f, SORT)]]
22bb4a9063684a0f37dd7d0e6b21086adcc1e789Christian Maeder qualifyConds f = map $ map (qualify_cond f)
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht qualify_cond :: FORMULA f -> ([TERM f], SORT) -> (TERM f, SORT)
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht qualify_cond f (ts, s) = case ts of
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht [t1, t2] -> (Conditional t1 f t2 [], s)
f6a562e28240e4f9107c199ba7a8e500ccfbfa55Simon Ulbricht _ -> (Unparsed_term "" [],s) {-error
f6a562e28240e4f9107c199ba7a8e500ccfbfa55Simon Ulbricht $ "Internal Error: wrong number of TERMs in qualify_cond!"-}
22bb4a9063684a0f37dd7d0e6b21086adcc1e789Christian Maeder get_profile :: [[TERM f]] -> [([TERM f], SORT)]
41a3368af0eaad78c660477e7ded53b2ba85a275Christian Maeder get_profile cs
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht = [ (c, s) | -- :: ([TERM], SORT)
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht c <- permute cs, -- :: [TERM]
2e76bbbed1c936bb0aee1753837e1c50416847a2Simon Ulbricht have_supersort c, -- :: Bool
bf51e183eda8e66f16795b35ce9a62468974b8e3Christian Maeder s <- Set.toList $ supersorts c ] -- :: SORT
2e76bbbed1c936bb0aee1753837e1c50416847a2Simon Ulbricht{-----------------------------------------------------------
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder Construct a TERM of type Sorted_term
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder from each (TERM, SORT) tuple
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder-----------------------------------------------------------}
30ccae9374798a92124e1b294404f7b55ffbb412Christian MaederqualifyTerms :: [Id.Pos] -> [[(TERM f, SORT)]] -> [[TERM f]]
30ccae9374798a92124e1b294404f7b55ffbb412Christian MaederqualifyTerms pos pairs =
2e76bbbed1c936bb0aee1753837e1c50416847a2Simon Ulbricht map (map qualify_term) pairs
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder qualify_term :: (TERM f, SORT) -> TERM f
b532acc045cf5e26beb0691acc136d11188cce87Christian Maeder qualify_term (t, s) = Sorted_term t s pos
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder{-----------------------------------------------------------
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaeder For each C in P (see above), let C' choose _one_
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaeder f:s \in C for each s minimal such that f:s \in C
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaeder-----------------------------------------------------------}
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaederminimize_op ::
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaeder Sign f e -> [(OpType, [TERM f])] -> [(OpType, [TERM f])]
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaederminimize_op sign ops_n_terms
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaeder = concat $ map reduce ops_n_terms
c24f7998fe7dfca4277f83076a119aabfe6186a0mcodescu results :: Set.Set SORT
cbd64ad1d663565751cb9442f78a40ff96c6bed6Eugen Kuksa results = Set.fromList (map (opRes . fst) ops_n_terms)
f382d86a384743a770cd5490a641e38ed1069c5cChristian Maeder lesserSorts :: SORT -> Set.Set SORT
f382d86a384743a770cd5490a641e38ed1069c5cChristian Maeder lesserSorts s = Set.intersection results (subsortsOf s sign)
22bb4a9063684a0f37dd7d0e6b21086adcc1e789Christian Maeder leastSort :: SORT -> Bool
22bb4a9063684a0f37dd7d0e6b21086adcc1e789Christian Maeder leastSort s = Set.size (lesserSorts s) == 1
22bb4a9063684a0f37dd7d0e6b21086adcc1e789Christian Maeder reduce :: (OpType, [TERM f]) -> [(OpType, [TERM f])]
22bb4a9063684a0f37dd7d0e6b21086adcc1e789Christian Maeder reduce x@(op,_) = if (leastSort (opRes op)) then [x] else []
22bb4a9063684a0f37dd7d0e6b21086adcc1e789Christian Maeder{-----------------------------------------------------------
e24da6268aa5791c7efd44571cafc0e36bf568dbChristian Maeder Workalike for minimize_op, but used inside m_e_t_cond
e24da6268aa5791c7efd44571cafc0e36bf568dbChristian Maeder-----------------------------------------------------------}
e24da6268aa5791c7efd44571cafc0e36bf568dbChristian Maederminimize_cond ::
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa Sign f e -> [([TERM f], SORT)] -> [([TERM f], SORT)]
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksaminimize_cond sign terms_n_sort
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa = concat $ map reduce terms_n_sort
fdae29fce51a3b43f17e1cad0deb0f5381b9d3f6Christian Maeder sorts = Set.fromList (map snd terms_n_sort)
dab141168df1b5ae84852d862b3aefc8782cfc7emcodescu lesserSorts :: SORT -> Set.Set SORT
5606c84ebef3de545602e215bbd87931334d48f0mcodescu lesserSorts s = Set.intersection sorts (subsortsOf s sign)
5606c84ebef3de545602e215bbd87931334d48f0mcodescu leastSort :: SORT -> Bool
c24f7998fe7dfca4277f83076a119aabfe6186a0mcodescu leastSort s = Set.size (lesserSorts s) == 1
c24f7998fe7dfca4277f83076a119aabfe6186a0mcodescu reduce :: ([TERM f], SORT) -> [([TERM f], SORT)]
dab141168df1b5ae84852d862b3aefc8782cfc7emcodescu reduce x@(_,s) = if (leastSort s) then [x] else []
c24f7998fe7dfca4277f83076a119aabfe6186a0mcodescuterm_sort :: TERM f -> SORT
c24f7998fe7dfca4277f83076a119aabfe6186a0mcodescuterm_sort term' = case term' of
dab141168df1b5ae84852d862b3aefc8782cfc7emcodescu (Sorted_term _ sort _ ) -> sort
c24f7998fe7dfca4277f83076a119aabfe6186a0mcodescu _ -> error -- unlikely
c24f7998fe7dfca4277f83076a119aabfe6186a0mcodescu "term_sort: unsorted TERM after expansion"
c24f7998fe7dfca4277f83076a119aabfe6186a0mcodescu{-----------------------------------------------------------
dab141168df1b5ae84852d862b3aefc8782cfc7emcodescu Set of SubSORTs common to all given SORTs
c24f7998fe7dfca4277f83076a119aabfe6186a0mcodescu-----------------------------------------------------------}
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbrichtcommon_subsorts ::
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht Sign f e -> [SORT] -> Set.Set SORT
2e2559f894aaa661b199e4fa00609f522bc5482aSimon Ulbrichtcommon_subsorts sign srts = let
2e2559f894aaa661b199e4fa00609f522bc5482aSimon Ulbricht get_subsorts = flip subsortsOf sign
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder in foldr1 Set.intersection $ map get_subsorts $ srts
05c714be15ce094d83f1b989cdf5236be78419bfSimon Ulbricht -- in (foldr Set.intersection Set.empty) . (map get_subsorts)
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder{-----------------------------------------------------------
05c714be15ce094d83f1b989cdf5236be78419bfSimon Ulbricht Set of SuperSORTs common to all given SORTs
bf51e183eda8e66f16795b35ce9a62468974b8e3Christian Maeder-----------------------------------------------------------}
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbrichtcommon_supersorts ::
05c714be15ce094d83f1b989cdf5236be78419bfSimon Ulbricht Sign f e -> [SORT] -> Set.Set SORT
986888e7f4d8ed681272a79c63f329ce8037063dcmaedercommon_supersorts _ [] = Set.empty
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaedercommon_supersorts sign srts = let
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder get_supersorts = flip supersortsOf sign
f6a562e28240e4f9107c199ba7a8e500ccfbfa55Simon Ulbricht in foldr1 Set.intersection $ map get_supersorts $ srts
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa{-----------------------------------------------------------
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa True if all SORTs have a common subSORT
f382d86a384743a770cd5490a641e38ed1069c5cChristian Maeder-----------------------------------------------------------}
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maederhave_common_subsorts ::
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder Sign f e -> [SORT] -> Bool
fdae29fce51a3b43f17e1cad0deb0f5381b9d3f6Christian Maederhave_common_subsorts s = (not . Set.isEmpty . common_subsorts s)
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder{-----------------------------------------------------------
fdae29fce51a3b43f17e1cad0deb0f5381b9d3f6Christian Maeder True if all SORTs have a common superSORT
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder-----------------------------------------------------------}
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maederhave_common_supersorts ::
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa Sign f e -> [SORT] -> Bool
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maederhave_common_supersorts s = (not . Set.isEmpty . common_supersorts s)
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder{-----------------------------------------------------------
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder True if s1 <= s2 OR s1 >= s2
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder-----------------------------------------------------------}
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht Sign f e -> SORT -> SORT -> Bool
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbrichtxeq_SORT sign s1 s2 = (leq_SORT sign s1 s2) || (geq_SORT sign s1 s2)
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder{-----------------------------------------------------------
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder True if s1 <= s2 OR s1 >= s2
b532acc045cf5e26beb0691acc136d11188cce87Christian Maeder-----------------------------------------------------------}
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder Sign f e -> (a, SORT) -> (a, SORT) -> Bool
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maederxeq_TUPLE sign (_,s1) (_,s2) = xeq_SORT sign s1 s2
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder{-----------------------------------------------------------
05c714be15ce094d83f1b989cdf5236be78419bfSimon Ulbricht True if s1 <= s2
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht-----------------------------------------------------------}
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht Sign f e -> SORT -> SORT -> Bool
de8983abdf4b35af1ed1fdee2de4dff13c2368bacmaederleq_SORT sign s1 s2 = Set.member s2 (supersortsOf s1 sign)
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht-- leq_SORT = (flip Set.member) . (flip supersortsOf)
ccd9cf19d129595770d592d3d0d80c6619f7a141Eugen Kuksa{-----------------------------------------------------------
f07364021546acc2fa5da55501bd6207b040f7bfEugen Kuksa True if s1 >= s2
f07364021546acc2fa5da55501bd6207b040f7bfEugen Kuksa-----------------------------------------------------------}
8723ec450f2e7a024230467c0c28a3f154905483cmaeder Sign f e -> SORT -> SORT -> Bool
8723ec450f2e7a024230467c0c28a3f154905483cmaedergeq_SORT sign s1 s2 = Set.member s2 (subsortsOf s1 sign)
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder-- geq_SORT = (flip Set.member) . (flip subsortsOf)
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maeder{-----------------------------------------------------------
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maeder True if o1 ~F o2
e4a035578fa9d1911eee097e2ed9a998c90c7805Christian Maeder-----------------------------------------------------------}
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maeder Sign f e -> OpType -> OpType -> Bool
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian MaederleqF sign o1 o2 = zipped_all are_legal (opArgs o1) (opArgs o2)
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maeder && have_common_supersorts sign [(opRes o1), (opRes o2)]
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maeder where are_legal a b = have_common_subsorts sign [a, b]
00d671cc654fe8d1571fa594bbebc9a2906ea880cmaeder{-----------------------------------------------------------
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder True if p1 ~P p2
8723ec450f2e7a024230467c0c28a3f154905483cmaeder-----------------------------------------------------------}
fb9ec1e4dd1877781ec2b491fb0a6bcd38a7b04dcmaeder Sign f e -> PredType -> PredType -> Bool
8723ec450f2e7a024230467c0c28a3f154905483cmaederleqP sign p1 p2 = zipped_all are_legal (predArgs p1) (predArgs p2)
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder where are_legal a b = have_common_subsorts sign [a, b]
1698621aea64f7a2b04a4084984eed1437e22771Christian MaederDie alten SML-Funktionen, die hier verwandt wurden.
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian MaederDen Beschreibungen nach sind das genau die beiden, mit denen eine Menge in
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian MaederAequivalenzklassen unterteilt wird.
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian MaederWie die erste davon funktioniert, ist mir nicht offen ersichtlich,
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maederaber vielleicht brauch ich die eigentlich auch gar nicht?
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maeder(* Compute the connected compenents of a graph which is given
69ad4a5f0c84ae5d0cdd7518c3698c36342a47d9cmaeder by a list of nodes and a boolean function indicating whether
69ad4a5f0c84ae5d0cdd7518c3698c36342a47d9cmaeder there is an egde between two nodes.
69ad4a5f0c84ae5d0cdd7518c3698c36342a47d9cmaeder For each node, the algorithm splits the connected components
69ad4a5f0c84ae5d0cdd7518c3698c36342a47d9cmaeder which have been computed so far into two categories:
69ad4a5f0c84ae5d0cdd7518c3698c36342a47d9cmaeder those which are connected to the node and those which are not.
4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder The former are all linked with @ in order to form a new connected
4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder component, the latter are left untouched. *)
60e6795dd310e10194e12bb660575aadf941328bEugen Kuksafun compute_conn_components (edges:'a*'a->bool) (nodes:'a list):'a list list =
ad5671edfa2ed767ec4fdc2f3099603d6fe8b97ecmaeder fun is_connected(node,nil) = false
8d2321e17a34951fbd52f68e9f9f148f0890e471Christian Maeder | is_connected(node,n::c) =
8d2321e17a34951fbd52f68e9f9f148f0890e471Christian Maeder edges(node,n) orelse edges(n,node) orelse is_connected(node,c)
8d2321e17a34951fbd52f68e9f9f148f0890e471Christian Maeder fun split_components(node,nil,acc_comp_of_node,acc_other_comps) =
8d2321e17a34951fbd52f68e9f9f148f0890e471Christian Maeder (node::acc_comp_of_node)::acc_other_comps
4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder | split_components(node,current_comp::
4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder other_comps,acc_comp_of_node,acc_other_comps) =
69ad4a5f0c84ae5d0cdd7518c3698c36342a47d9cmaeder if is_connected(node,current_comp)
69ad4a5f0c84ae5d0cdd7518c3698c36342a47d9cmaeder then split_components(node,other_comps,
69ad4a5f0c84ae5d0cdd7518c3698c36342a47d9cmaeder current_comp@acc_comp_of_node,acc_other_comps)
69ad4a5f0c84ae5d0cdd7518c3698c36342a47d9cmaeder else split_components(node,other_comps,acc_comp_of_node,
69ad4a5f0c84ae5d0cdd7518c3698c36342a47d9cmaeder current_comp::acc_other_comps)
4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder fun add_node (node:'a,components:'a list list):'a list list =
69ad4a5f0c84ae5d0cdd7518c3698c36342a47d9cmaeder split_components(node,components,nil,nil)
69ad4a5f0c84ae5d0cdd7518c3698c36342a47d9cmaeder foldr add_node (nodes,[])
69ad4a5f0c84ae5d0cdd7518c3698c36342a47d9cmaeder(* Compute the equivalence classes of the equivalence closures of leqF
116efc752fbf094a464c4f4940d9a450ab41c6c9Simon Ulbricht and leqP resp. and store them in a table indexed by function and
8723ec450f2e7a024230467c0c28a3f154905483cmaeder predicate names, resp. This is needed when checking if terms or
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder predications are equivalent, since this equivalence is defined in
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder terms of the equivalence closures of leqF and leqP resp. *)
00d671cc654fe8d1571fa594bbebc9a2906ea880cmaederfun get_conn_components (env:local_env) : local_env1 =
00d671cc654fe8d1571fa594bbebc9a2906ea880cmaeder val (srts,vars,funs,preds) = env
00d671cc654fe8d1571fa594bbebc9a2906ea880cmaeder (env,(Symtab_id.map (compute_conn_components (leqF env)) funs ,
00d671cc654fe8d1571fa594bbebc9a2906ea880cmaeder Symtab_id.map (compute_conn_components (leqP env)) preds) )