Overload.hs revision dfb729454186ec087df4860a568d7cb946d458be
97a9a944b5887e91042b019776c41d5dd74557aferikabele Module : $Header$
a945f35eff8b6a88009ce73de6d4c862ce58de3cslive Copyright : (c) Martin Kuehl, T. Mossakowski, C. Maeder, Uni Bremen 2004
a945f35eff8b6a88009ce73de6d4c862ce58de3cslive Licence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Maintainer : hets@tzi.de
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Stability : provisional
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Portability : portable
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Overload resolution
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Follows Sect. III:3.3 of the CASL Reference Manual.
fe64b2ba25510d8c9dba5560a2d537763566cf40nd The algorthim is from:
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Till Mossakowski, Kolyang, Bernd Krieg-Brueckner:
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Static semantic analysis and theorem proving for CASL.
52fff662005b1866a3ff09bb6c902800c5cc6dedjerenkrantz 12th Workshop on Algebraic Development Techniques, Tarquinia 1997,
fe64b2ba25510d8c9dba5560a2d537763566cf40nd LNCS 1376, p. 333-348
4aa805f8500255bc52a4c03259fe46df10a1d07cyoshikiimport qualified Common.Lib.Map as Map
dfb59c684345700bf9186b8d44936f8b1ba082ffgryzorimport qualified Common.Lib.Set as Set
fe64b2ba25510d8c9dba5560a2d537763566cf40ndimport qualified Common.AS_Annotation as Named
fe64b2ba25510d8c9dba5560a2d537763566cf40ndimport qualified Common.Id as Id
117c1f888a14e73cdd821dc6c23eb0411144a41cnd{- Outline:
58699879a562774640b95e9eedfd891f336e38c2nd - calculate global information from signature and pass it through
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd - recurse through sentences until atomic sentences are reached
117c1f888a14e73cdd821dc6c23eb0411144a41cnd - calculate expansions of atomic sentences
117c1f888a14e73cdd821dc6c23eb0411144a41cnd{- TODO-List:
9597f440430d8c876dd64f5f78066804650a18ecnoodl * generalize 'is_unambiguous' (see 'choose') and make it available globally
117c1f888a14e73cdd821dc6c23eb0411144a41cnd * replace 'case' statements w/ pattern matching where possible
117c1f888a14e73cdd821dc6c23eb0411144a41cnd * generalize minExpFORMULA_pred/minExpTerm_op/minExpTerm_cond
117c1f888a14e73cdd821dc6c23eb0411144a41cnd * utilize Sets instead of Lists
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejesh * generalize expansion for Qual_var and Sorted_term
117c1f888a14e73cdd821dc6c23eb0411144a41cnd * move structural logic to higher levels, as e.g. in
117c1f888a14e73cdd821dc6c23eb0411144a41cnd qualifyOps = map (map qualify_op) -- map should go somewhere above
117c1f888a14e73cdd821dc6c23eb0411144a41cnd * sweep op-like logic from minExpTerm_cond where it is unneeded
117c1f888a14e73cdd821dc6c23eb0411144a41cnd * generalize zipped_all
117c1f888a14e73cdd821dc6c23eb0411144a41cnd * generalize qualifyTerms or implement locally - too much structural force
117c1f888a14e73cdd821dc6c23eb0411144a41cnd * gemeralize minimize_* or implement locally - needed only in one f. each
117c1f888a14e73cdd821dc6c23eb0411144a41cnd * use more let/in constructs (instead of where) to simulate workflow
117c1f888a14e73cdd821dc6c23eb0411144a41cnd To find more items or pitfalls, search this file for:
117c1f888a14e73cdd821dc6c23eb0411144a41cnd-- TODO: this ain't mine, somebody might need to explain it
117c1f888a14e73cdd821dc6c23eb0411144a41cndtype Min f e = GlobalAnnos -> Sign f e -> f -> Result f
117c1f888a14e73cdd821dc6c23eb0411144a41cnd{-----------------------------------------------------------
117c1f888a14e73cdd821dc6c23eb0411144a41cnd - Overload Resolution -
117c1f888a14e73cdd821dc6c23eb0411144a41cnd Apply the algorithm for overload resolution described in
117c1f888a14e73cdd821dc6c23eb0411144a41cnd Till Mossakowski, Kolyang, Bernd Krieg-Brueckner:
117c1f888a14e73cdd821dc6c23eb0411144a41cnd Static semantic analysis and theorem proving for CASL.
709e3a21ba73b8433462959cd56c773454b34441trawick 12th Workshop on Algebraic Development Techniques, Tarquinia 1997,
117c1f888a14e73cdd821dc6c23eb0411144a41cnd LNCS 1376, p. 333-348
117c1f888a14e73cdd821dc6c23eb0411144a41cnd to all given formulae/sentences w.r.t. the given annotations and
117c1f888a14e73cdd821dc6c23eb0411144a41cnd signature. All real work is done by 'minExpFORMULA', which is
117c1f888a14e73cdd821dc6c23eb0411144a41cnd applied to any given formula in turn.
117c1f888a14e73cdd821dc6c23eb0411144a41cnd-----------------------------------------------------------}
117c1f888a14e73cdd821dc6c23eb0411144a41cndoverloadResolution :: (Eq f, PrettyPrint f) =>
117c1f888a14e73cdd821dc6c23eb0411144a41cnd Min f e ->
117c1f888a14e73cdd821dc6c23eb0411144a41cnd GlobalAnnos ->
117c1f888a14e73cdd821dc6c23eb0411144a41cnd Sign f e ->
117c1f888a14e73cdd821dc6c23eb0411144a41cnd [Named.Named (FORMULA f)] ->
117c1f888a14e73cdd821dc6c23eb0411144a41cnd Result [Named.Named (FORMULA f)]
117c1f888a14e73cdd821dc6c23eb0411144a41cnd -- neat type signature, eh?
117c1f888a14e73cdd821dc6c23eb0411144a41cndoverloadResolution mef ga sign = mapM overload
117c1f888a14e73cdd821dc6c23eb0411144a41cnd where overload sent = do sent' <- return $ Named.sentence sent
117c1f888a14e73cdd821dc6c23eb0411144a41cnd exp_sent <- minExpFORMULA mef ga sign sent'
117c1f888a14e73cdd821dc6c23eb0411144a41cnd return sent { Named.sentence = exp_sent }
117c1f888a14e73cdd821dc6c23eb0411144a41cnd{-----------------------------------------------------------
a38b5f73e7f0f3b8726fb47d27b145f37036ead0jim - Minimal expansion of a formula -
117c1f888a14e73cdd821dc6c23eb0411144a41cnd Expand a given formula by typing information.
fe64b2ba25510d8c9dba5560a2d537763566cf40nd * For non-atomic formulae, recurse through subsentences.
fe64b2ba25510d8c9dba5560a2d537763566cf40nd * For trival atomic formulae, no expansion is neccessary.
fe64b2ba25510d8c9dba5560a2d537763566cf40nd * For atomic formulae, the following cases are implemented:
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna + Predication is handled by the dedicated expansion function
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna 'minExpFORMULA_pred'.
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna + Existl_equation and Strong_equation are handled by the dedicated
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna expansion function 'minExpFORMULA_eq'.
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna + Definedness is handled by expanding the subterm.
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna + Membership is handled by expanding the subterm, followed by
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna checking the found expansions' appropriateness to the stated
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna Membership.
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe + TODO: I don't know about 'Sort_gen_ax' and 'ExtFORMULA'.
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe-----------------------------------------------------------}
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquernaminExpFORMULA :: (Eq f, PrettyPrint f) =>
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna GlobalAnnos ->
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna Sign f e ->
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna (FORMULA f) ->
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna Result (FORMULA f)
5ae609a8a09239d20f48a4a95c4f21b713995babwroweminExpFORMULA mef ga sign formula = case formula of
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe --- Trivial atomic formula -> return sentence unmodified
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe True_atom _ -> return formula
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe False_atom _ -> return formula
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe Sort_gen_ax _ _ -> return formula
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe --- Non-atomic formula -> recurse through subsentences
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe Quantification q vars f pos -> do
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe -- add 'vars' to signature
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna (_, sign') <- return $ runState (mapM_ addVars vars) sign
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna -- expand subformula
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna f' <- minExpFORMULA mef ga sign' f
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna -- wrap 'Quantification' around expanded sentence
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna return (Quantification q vars f' pos)
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna Conjunction fs pos -> do
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna -- expand all subformulae
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna fs' <- mapM (minExpFORMULA mef ga sign) fs
90efa9f1730742d874edb5a7803adce11c9f08eanoodl -- wrap 'Conjunction' around expanded sentences
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna return (Conjunction fs' pos)
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna Disjunction fs pos -> do
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna -- expand all subformulae
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna fs' <- mapM (minExpFORMULA mef ga sign) fs
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna -- wrap 'Disjunction' around expanded sentences
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna return $ Disjunction fs' pos
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna -- TODO: reminds of 'Conjunction'...
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna Implication f1 f2 b pos -> do
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna -- expand all subformulae
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna f1' <- minExpFORMULA mef ga sign f1
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna f2' <- minExpFORMULA mef ga sign f2
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna -- wrap 'Implication' around expanded sentences
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna return (Implication f1' f2' b pos)
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna Equivalence f1 f2 pos -> do
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna -- expand all subformulae
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna f1' <- minExpFORMULA mef ga sign f1
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna f2' <- minExpFORMULA mef ga sign f2
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna -- wrap 'Equivalence' around expanded sentences
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna return (Equivalence f1' f2' pos)
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe -- TODO: reminds of 'Implication'...
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe Negation f pos -> do
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe -- expand subformula
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe f' <- minExpFORMULA mef ga sign f
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe -- wrap 'Negation' around expanded sentence
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe return (Negation f' pos)
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe -- TODO: reminds of ... all of the above
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe --- Atomic formula -> expand and check for ambiguities
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe Predication predicate terms pos
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe -- pass information to dedicated helper function
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe -> minExpFORMULA_pred mef ga sign predicate terms pos
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe Existl_equation term1 term2 pos
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe -- pass information to dedicated helper function
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe -> minExpFORMULA_eq mef ga sign Existl_equation term1 term2 pos
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe Strong_equation term1 term2 pos
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe -- pass information to dedicated helper function
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe -> minExpFORMULA_eq mef ga sign Strong_equation term1 term2 pos
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe Definedness term pos -> do
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe -- expand subterm
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe t <- minExpTerm mef ga sign term
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe -- check expansions for ambiguity
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe t' <- is_unambiguous term t pos
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna -- wrap 'Definedness' around expanded term
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna return (Definedness t' pos)
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna Membership term sort pos -> do
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -- expand subterm
fe64b2ba25510d8c9dba5560a2d537763566cf40nd t <- minExpTerm mef ga sign term
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -- choose expansions that fulfill 'Membership' to the given 'sort'
fe64b2ba25510d8c9dba5560a2d537763566cf40nd t' <- let leq_term [] = False
fe64b2ba25510d8c9dba5560a2d537763566cf40nd leq_term (t1:_) = leq_SORT sign sort $ term_sort t1
fe64b2ba25510d8c9dba5560a2d537763566cf40nd in return $ filter leq_term t
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -- check chosen expansions for ambiguity
fe64b2ba25510d8c9dba5560a2d537763566cf40nd t'' <- is_unambiguous term t' pos
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -- wrap 'Membership' around expanded term
fe64b2ba25510d8c9dba5560a2d537763566cf40nd return (Membership t'' sort pos)
c985aca104389df30d6ec0a637ce0ccaac904362nd ExtFORMULA f -> fmap ExtFORMULA $ mef ga sign f
fe64b2ba25510d8c9dba5560a2d537763566cf40nd --- unknown formula -> signal error
06ba4a61654b3763ad65f52283832ebf058fdf1cslive _ -> error $ "minExpFORMULA: unexpected type of FORMULA: "
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ++ (show formula)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive -- TODO: is there a nicer kind of error I can signal here?
fb77c505254b6e9c925e23e734463e87574f8f40kess{-----------------------------------------------------------
fb77c505254b6e9c925e23e734463e87574f8f40kess - Check expanded terms for ambiguity -
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Check, whether the given expansions contain ambiguity.
06ba4a61654b3763ad65f52283832ebf058fdf1cslive If so, return any of the equivalent expansions, otherwise, or in
06ba4a61654b3763ad65f52283832ebf058fdf1cslive case no correct expansions were found, signal an error.
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-----------------------------------------------------------}
06ba4a61654b3763ad65f52283832ebf058fdf1csliveis_unambiguous :: (Eq f, PrettyPrint f) =>
fb77c505254b6e9c925e23e734463e87574f8f40kess [[TERM f]] ->
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Result (TERM f)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive--- unambiguous expansion found -> return first expansion
06ba4a61654b3763ad65f52283832ebf058fdf1csliveis_unambiguous _ ((term:_):_) _ = return term
fb77c505254b6e9c925e23e734463e87574f8f40kess-- TODO: pattern should read '((term:_):[])' to really filter ambiguities
06ba4a61654b3763ad65f52283832ebf058fdf1cslive--- no expansions found -> signal error
06ba4a61654b3763ad65f52283832ebf058fdf1csliveis_unambiguous topterm [] pos
06ba4a61654b3763ad65f52283832ebf058fdf1cslive = pplain_error (Unparsed_term "<error>" [])
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (ptext "No correct typing for " <+> (printText topterm))
fb77c505254b6e9c925e23e734463e87574f8f40kess--- ambiguous expansions found -> signal error
06ba4a61654b3763ad65f52283832ebf058fdf1csliveis_unambiguous _ term pos
06ba4a61654b3763ad65f52283832ebf058fdf1cslive = pplain_error (Unparsed_term "<error>" [])
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (ptext "Cannot disambiguate!\nPossible Expansions: "
fb77c505254b6e9c925e23e734463e87574f8f40kess <+> (printText term))
bc4b55ec8f31569d606d5680d50189a355bcd7a6rbowen{-----------------------------------------------------------
fb77c505254b6e9c925e23e734463e87574f8f40kess - Minimal expansion of a predication formula -
06ba4a61654b3763ad65f52283832ebf058fdf1cslive 'minExpFORMULA_pred' erweitert eine Praedikatenanwendung um
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Sorteninformationen. Sie geht dabei entsprechend dem Algorithmus (TODO:
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Seitenzahl aus dem CASL-Reference-Manual herausfinden) vor.
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Zuerst werden die Erweiterungen der Argument-Terme erzeugt. Fuer jede
fb77c505254b6e9c925e23e734463e87574f8f40kess moegliche Argumentenliste aus diesen Erweiterungen wird dann ein sog.
fb77c505254b6e9c925e23e734463e87574f8f40kess 'Profil' erzeugt, welches zusaetzlich zu der Argumentenliste auch dazu
06ba4a61654b3763ad65f52283832ebf058fdf1cslive passende Typinformationen des Praedikates enthaelt. Zusaetzlich werden die
fb77c505254b6e9c925e23e734463e87574f8f40kess Argumente noch in Injektionen verpackt, damit sie genau auf die Signatur
fb77c505254b6e9c925e23e734463e87574f8f40kess des Profils passen. Diese Profile werden in Aequivalenzklassen aufgeteilt,
06ba4a61654b3763ad65f52283832ebf058fdf1cslive damit entschieden werden kann, ob die Erweiterungen eindeutig sind. In
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd diesem Fall wird eine der aequivalenten eindeutigen Erweiterungen gewaehlt
130d299c4b2b15be45532a176604c71fdc7bea5bnd und zurueckgegeben.
130d299c4b2b15be45532a176604c71fdc7bea5bnd This process is analogous to expanding a function application (s. below),
130d299c4b2b15be45532a176604c71fdc7bea5bnd just with the minimization step being left out.
130d299c4b2b15be45532a176604c71fdc7bea5bnd TODO: Documentation!
130d299c4b2b15be45532a176604c71fdc7bea5bnd-----------------------------------------------------------}
ef8e89e090461194ecadd31e8796a2c51e0531a2kessminExpFORMULA_pred :: (Eq f, PrettyPrint f) =>
130d299c4b2b15be45532a176604c71fdc7bea5bnd Min f e ->
130d299c4b2b15be45532a176604c71fdc7bea5bnd GlobalAnnos ->
130d299c4b2b15be45532a176604c71fdc7bea5bnd Sign f e ->
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd PRED_SYMB ->
fe64b2ba25510d8c9dba5560a2d537763566cf40nd [TERM f] ->
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Result (FORMULA f)
fe64b2ba25510d8c9dba5560a2d537763566cf40ndminExpFORMULA_pred mef ga sign predicate terms pos = do
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -- expand argument subterms
fe64b2ba25510d8c9dba5560a2d537763566cf40nd expansions <- mapM (minExpTerm mef ga sign) terms
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -- permute expansions to get a list of argument-lists to the predicate
fe64b2ba25510d8c9dba5560a2d537763566cf40nd permuted_exps <- return (permute expansions)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -- convert each permutation to a profile (as descr. on p. XXX)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -- then inject arguments that don't match the predicate's expected type
fe64b2ba25510d8c9dba5560a2d537763566cf40nd profiles <- return $ map (map insert_injections)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd $ map get_profile
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess permuted_exps
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslive -- collect generated profiles into equivalence classes
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslive p <- return $ concat
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess $ map (equivalence_Classes pred_eq)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive -- choose profile if unambiguous, otherwise signal error
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd p' <- choose p
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd -- transform chosen profile into a qualified predicate application
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd return (qualify_pred p')
06ba4a61654b3763ad65f52283832ebf058fdf1cslive where -- the predicate's name
06ba4a61654b3763ad65f52283832ebf058fdf1cslive name :: PRED_NAME
06ba4a61654b3763ad65f52283832ebf058fdf1cslive name = pred_name predicate
06ba4a61654b3763ad65f52283832ebf058fdf1cslive -- predicates matching that name in the current environment
06ba4a61654b3763ad65f52283832ebf058fdf1cslive preds :: [PredType]
130d299c4b2b15be45532a176604c71fdc7bea5bnd -- extract a predicate's name from its definition
130d299c4b2b15be45532a176604c71fdc7bea5bnd pred_name :: PRED_SYMB -> PRED_NAME
130d299c4b2b15be45532a176604c71fdc7bea5bnd pred_name (Pred_name name') = name'
130d299c4b2b15be45532a176604c71fdc7bea5bnd pred_name (Qual_pred_name name' _ _) = name'
130d299c4b2b15be45532a176604c71fdc7bea5bnd -- if an unambiguous class of expansions is found, choose its head
130d299c4b2b15be45532a176604c71fdc7bea5bnd -- otherwise signal an error
130d299c4b2b15be45532a176604c71fdc7bea5bnd --choose :: [[(PredType, [TERM f])]] -> Result (PredType, [TERM f])
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -- TODO: Signature throws an Error that I don't understand...
fe64b2ba25510d8c9dba5560a2d537763566cf40nd choose ps = case ps of
fe64b2ba25510d8c9dba5560a2d537763566cf40nd (_:_):_ -> return $ head $ head ps
fe64b2ba25510d8c9dba5560a2d537763566cf40nd [] -> pplain_error (PredType [],[])
fe64b2ba25510d8c9dba5560a2d537763566cf40nd (ptext "No correct typing for "
fe64b2ba25510d8c9dba5560a2d537763566cf40nd <+> (printText ps))
fe64b2ba25510d8c9dba5560a2d537763566cf40nd _ -> pplain_error (PredType [], terms)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd (ptext "Cannot disambiguate! Term: "
fe64b2ba25510d8c9dba5560a2d537763566cf40nd <+> (printText (predicate, terms))
fe64b2ba25510d8c9dba5560a2d537763566cf40nd $$ ptext "Possible Expansions: "
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd <+> (printText ps))
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -- wrap qualified predication around predicate and its argument terms
fe64b2ba25510d8c9dba5560a2d537763566cf40nd qualify_pred :: (PredType, [TERM f]) -> FORMULA f
fe64b2ba25510d8c9dba5560a2d537763566cf40nd qualify_pred (pred', terms')
fe64b2ba25510d8c9dba5560a2d537763566cf40nd = (Predication (Qual_pred_name name (toPRED_TYPE pred') [])
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -- generate profiles as descr. on p. XXX
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd get_profile :: [[TERM f]] -> [(PredType, [TERM f])]
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd get_profile cs = [ (pred', ts) |
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd pred' <- preds,
888b616027180cc8aaa4d2bee5ecc6acec175bc5nd ts <- (permute cs),
b95ae799514ad86a15610ad75808d7065e9847c9kess zipped_all (leq_SORT sign)
888b616027180cc8aaa4d2bee5ecc6acec175bc5nd (map term_sort ts)
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd (predArgs pred') ]
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd -- insert injections for all argument terms where neccessary
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd insert_injections :: (PredType, [TERM f]) -> (PredType, [TERM f])
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd insert_injections (pred', args)
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd = (pred', (zipWith inject args (predArgs pred')))
604c89126c27104f659d7a51b0113e3bd435faf8fielding -- the equivalence relation for predicates as descr. on p. XXX
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd pred_eq :: (PredType, [TERM f]) -> (PredType, [TERM f]) -> Bool
06ba4a61654b3763ad65f52283832ebf058fdf1cslive -- * TODO: Documentation!
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd -- * neuer Algorithmus:
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd -- checken, ob Praedikatsymbole und Argument-Terme Aequivalent sind.
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd -- Fuer letzteres pro Argument-Position in expansions nachgucken.
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -- Ditto. fuer Operationen!
888b616027180cc8aaa4d2bee5ecc6acec175bc5nd pred_eq (pred1,ts1) (pred2,ts2)
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd = let w1 = predArgs pred1
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd w2 = predArgs pred2
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd s1 = map term_sort ts1
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd s2 = map term_sort ts2
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd b1 = zipped_all (leq_SORT sign) s1 w1
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd b2 = zipped_all (leq_SORT sign) s2 w2
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd preds_equal = (pred1 == pred2)
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd preds_equiv = leqP sign pred1 pred2
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd types_equal = False -- and (zipWith (==) s1 s2)
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd -- TODO: check whether argtypes are equal
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd in b1 && b2 && (preds_equal
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd || (preds_equiv
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd && types_equal))
fe64b2ba25510d8c9dba5560a2d537763566cf40nd-- Handy shortcut for the type signature of 'Existl_equation' et al.
fe64b2ba25510d8c9dba5560a2d537763566cf40ndtype Eq_constructor f = TERM f -> TERM f -> [Id.Pos] -> FORMULA f
604c89126c27104f659d7a51b0113e3bd435faf8fielding{-----------------------------------------------------------
fb77c505254b6e9c925e23e734463e87574f8f40kess - Minimal expansion of an equation formula -
604c89126c27104f659d7a51b0113e3bd435faf8fielding Expand an equation formula by typing information.
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Expand all subterms w.r.t. the given environment, then find pairs of
fe64b2ba25510d8c9dba5560a2d537763566cf40nd expansions that belong to a common supersort. Check these pairs for
fe64b2ba25510d8c9dba5560a2d537763566cf40nd ambiguity and, if none is found, wrap them into an equation formula
fe64b2ba25510d8c9dba5560a2d537763566cf40nd specified by the given 'Eq_constructor'. If no correct expansions
6fe26506780e73be2a412d758af77fafdf03291and are found or the found expansions are ambiguous, signal an error.
fe64b2ba25510d8c9dba5560a2d537763566cf40nd-----------------------------------------------------------}
58699879a562774640b95e9eedfd891f336e38c2ndminExpFORMULA_eq :: (Eq f, PrettyPrint f) =>
6fe26506780e73be2a412d758af77fafdf03291and GlobalAnnos ->
6fe26506780e73be2a412d758af77fafdf03291and Sign f e ->
58699879a562774640b95e9eedfd891f336e38c2nd Eq_constructor f ->
fb77c505254b6e9c925e23e734463e87574f8f40kess Result (FORMULA f)
fb77c505254b6e9c925e23e734463e87574f8f40kessminExpFORMULA_eq mef ga sign eq term1 term2 pos = do
58699879a562774640b95e9eedfd891f336e38c2nd -- expand subterms
58699879a562774640b95e9eedfd891f336e38c2nd exps1 <- minExpTerm mef ga sign term1
58699879a562774640b95e9eedfd891f336e38c2nd exps2 <- minExpTerm mef ga sign term2
58699879a562774640b95e9eedfd891f336e38c2nd -- choose head of any generated equivalence class, wrap into pairs
58699879a562774640b95e9eedfd891f336e38c2nd pairs <- return (permute [catMaybes (map maybeHead exps1),
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess catMaybes (map maybeHead exps2)])
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess -- choose pairs that belong to a common supersort
58699879a562774640b95e9eedfd891f336e38c2nd candidates <- return (filter fit pairs)
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess -- check candidate pairs for ambiguity
58699879a562774640b95e9eedfd891f336e38c2nd case candidates of
58699879a562774640b95e9eedfd891f336e38c2nd -- unambiguous expansion found -> wrap 'eq' around expansions
fb77c505254b6e9c925e23e734463e87574f8f40kess ([t1,t2]:_) -> return (eq t1 t2 pos)
fb77c505254b6e9c925e23e734463e87574f8f40kess -- no expansions found -> signal error
fb77c505254b6e9c925e23e734463e87574f8f40kess [] -> pplain_error (eq term1 term2 pos)
58699879a562774640b95e9eedfd891f336e38c2nd (ptext "No correct typing for "
58699879a562774640b95e9eedfd891f336e38c2nd <+> printText (eq term1 term2 pos))
58699879a562774640b95e9eedfd891f336e38c2nd -- ambiguous expansions found -> signal error
58699879a562774640b95e9eedfd891f336e38c2nd _ -> pplain_error (eq term1 term2 pos)
58699879a562774640b95e9eedfd891f336e38c2nd (ptext "Cannot disambiguate! Possible Expansions: "
58699879a562774640b95e9eedfd891f336e38c2nd <+> (printText exps1) $$ (printText exps2))
58699879a562774640b95e9eedfd891f336e38c2nd where -- True if the sorts of all given terms have a common supersort
58699879a562774640b95e9eedfd891f336e38c2nd fit :: [TERM f] -> Bool
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess fit = (have_common_supersorts sign) . (map term_sort)
4a7affccb2f1f5b94cab395e1bf3825aed715ebcnd -- 'Just . head' if there is a head, 'Nothing' else
9b5e2c5e769dc678a1aca06df75c32022b2f1492trawick maybeHead :: [a] -> Maybe a
604c89126c27104f659d7a51b0113e3bd435faf8fielding maybeHead (x:_) = Just x
604c89126c27104f659d7a51b0113e3bd435faf8fielding maybeHead _ = Nothing
4a7affccb2f1f5b94cab395e1bf3825aed715ebcnd{-----------------------------------------------------------
4a7affccb2f1f5b94cab395e1bf3825aed715ebcnd - Minimal expansion of a term -
4a7affccb2f1f5b94cab395e1bf3825aed715ebcnd Expand a given term by typing information.
58699879a562774640b95e9eedfd891f336e38c2nd * 'Simple_id' terms are handled by 'minExpTerm_simple'.
fe64b2ba25510d8c9dba5560a2d537763566cf40nd * 'Qual_var' terms are handled by 'minExpTerm_qual'.
fe64b2ba25510d8c9dba5560a2d537763566cf40nd * 'Application' terms are handled by 'minExpTerm_op'.
fe64b2ba25510d8c9dba5560a2d537763566cf40nd * 'Sorted_term' terms are handled by 'minExpTerm_sorted'.
fe64b2ba25510d8c9dba5560a2d537763566cf40nd * 'Cast' terms are handled by 'minExpTerm_cast'.
fe64b2ba25510d8c9dba5560a2d537763566cf40nd * 'Conditional' terms are handled by 'minExpTerm_cond'.
fe64b2ba25510d8c9dba5560a2d537763566cf40nd-----------------------------------------------------------}
fe64b2ba25510d8c9dba5560a2d537763566cf40ndminExpTerm :: (Eq f, PrettyPrint f) =>
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Min f e ->
fe64b2ba25510d8c9dba5560a2d537763566cf40nd GlobalAnnos ->
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd Sign f e ->
9583adab6bc4b3758e41963c905d9dad9f067131nd Result [[TERM f]]
4335f1cbf345c91bb996eec540c11ba8ce5d4268ndminExpTerm mef ga sign (Simple_id var)
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd = minExpTerm_simple sign var
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd -- TODO: what about 'mef' and 'ga'?
4335f1cbf345c91bb996eec540c11ba8ce5d4268ndminExpTerm mef ga sign (Qual_var var sort pos)
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd = minExpTerm_qual sign var sort pos
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd -- TODO: what about 'mef' and 'ga'?
4335f1cbf345c91bb996eec540c11ba8ce5d4268ndminExpTerm mef ga sign (Application op terms pos)
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd = minExpTerm_op mef ga sign op terms pos
4335f1cbf345c91bb996eec540c11ba8ce5d4268ndminExpTerm mef ga sign (Sorted_term term sort pos)
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd = minExpTerm_sorted mef ga sign term sort pos
4335f1cbf345c91bb996eec540c11ba8ce5d4268ndminExpTerm mef ga sign (Cast term sort pos)
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd = minExpTerm_cast mef ga sign term sort pos
4335f1cbf345c91bb996eec540c11ba8ce5d4268ndminExpTerm mef ga sign (Conditional term1 formula term2 pos)
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd = minExpTerm_cond mef ga sign term1 formula term2 pos
4335f1cbf345c91bb996eec540c11ba8ce5d4268ndminExpTerm mef ga sign _
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd = error "minExpTerm"
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd -- TODO: is there a nicer kind of error I can signal here?
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd{-----------------------------------------------------------
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd - Minimal expansion of a simple identifier -
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd Expand a simple identifier by typing information.
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd Look up the given identifier in the given environment (as a variable
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd or a constant). Sort the found definitions into equivalence
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd classes, then construct a qualified term from each.
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd-----------------------------------------------------------}
4335f1cbf345c91bb996eec540c11ba8ce5d4268ndminExpTerm_simple :: Sign f e ->
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd Result [[TERM f]]
fe64b2ba25510d8c9dba5560a2d537763566cf40ndminExpTerm_simple sign var = do
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -- look up identifier as variable in environment
fe64b2ba25510d8c9dba5560a2d537763566cf40nd vars <- return (Map.findWithDefault Set.empty var (varMap sign))
627c978514c54179736d152923478be7c8707f9bnd -- get name of identifier
fb77c505254b6e9c925e23e734463e87574f8f40kess name <- return (Id.simpleIdToId var)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -- look up constant matching name in environment
fe64b2ba25510d8c9dba5560a2d537763566cf40nd ops' <- return $ Set.filter is_const_op
fe64b2ba25510d8c9dba5560a2d537763566cf40nd ops <- return (Set.image opRes ops')
fe64b2ba25510d8c9dba5560a2d537763566cf40nd cs <- return (Set.union vars ops)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd least <- return
fb77c505254b6e9c925e23e734463e87574f8f40kess -- BEWARE: Restriction to minimal sorts is not correct
fb77c505254b6e9c925e23e734463e87574f8f40kess -- in case of downcasts: here, it may be the
fb77c505254b6e9c925e23e734463e87574f8f40kess -- case that the cast is only correct for non-minimal sorts!
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess $ {-Set.filter (is_least_sort cs)-} cs -- :: Set.Set SORT
06ba4a61654b3763ad65f52283832ebf058fdf1cslive return $ qualifyTerms []
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess $ (equivalence_Classes eq)
10673857794a4b3d9568ca2d983722a87ed352f1rbowen $ map pair_with_id
ed0dae472b518c553c923a86fb4322d4c50d86a6nd -- FIXME: Christian states that the result must be an
ed0dae472b518c553c923a86fb4322d4c50d86a6nd -- 'Application' if var is indeed a constant!
10673857794a4b3d9568ca2d983722a87ed352f1rbowen where -- True if operation takes no arguments (i.e. op is a constant)
10673857794a4b3d9568ca2d983722a87ed352f1rbowen is_const_op :: OpType -> Bool
06ba4a61654b3763ad65f52283832ebf058fdf1cslive is_const_op = null . opArgs
fb77c505254b6e9c925e23e734463e87574f8f40kess -- True if given set of sorts contains no subsort of the given sort
fb77c505254b6e9c925e23e734463e87574f8f40kess is_least_sort :: Set.Set SORT -> SORT -> Bool
fb77c505254b6e9c925e23e734463e87574f8f40kess is_least_sort ss s
06ba4a61654b3763ad65f52283832ebf058fdf1cslive = Set.size (Set.intersection ss (subsortsOf s sign)) == 1
06ba4a61654b3763ad65f52283832ebf058fdf1cslive -- True if of the given sorts is a supersort of the other
06ba4a61654b3763ad65f52283832ebf058fdf1cslive eq = xeq_TUPLE sign
fb77c505254b6e9c925e23e734463e87574f8f40kess -- wrap 'Qual_var' and the current identifier around the given sort
06ba4a61654b3763ad65f52283832ebf058fdf1cslive pair_with_id :: SORT -> (TERM f, SORT)
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd pair_with_id sort = ((Qual_var var sort []), sort)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive{-----------------------------------------------------------
06ba4a61654b3763ad65f52283832ebf058fdf1cslive - Minimal expansion of a qualified variable -
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Expand a qualified identifier by typing information.
06ba4a61654b3763ad65f52283832ebf058fdf1cslive First expand the identifier, disregarding the given qualification.
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Then choose only expansions that satisfy that qualification, and
1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantz wrap the typing information around them.
1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantz-----------------------------------------------------------}
cb3a1082aec4b3b4f4ed238c93c3cc54933a7f0endminExpTerm_qual :: Sign f e ->
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Result [[TERM f]]
06ba4a61654b3763ad65f52283832ebf058fdf1csliveminExpTerm_qual sign var sort pos = do
06ba4a61654b3763ad65f52283832ebf058fdf1cslive -- expand subterm
604c89126c27104f659d7a51b0113e3bd435faf8fielding expandedVar <- minExpTerm_simple sign var
604c89126c27104f659d7a51b0113e3bd435faf8fielding -- choose expansions that fit the given signature, then qualify
604c89126c27104f659d7a51b0113e3bd435faf8fielding return $ qualifyTerms pos
604c89126c27104f659d7a51b0113e3bd435faf8fielding $ map selectExpansions expandedVar
604c89126c27104f659d7a51b0113e3bd435faf8fielding where -- True if identifier and sort match the current signature
604c89126c27104f659d7a51b0113e3bd435faf8fielding fits :: TERM f -> Bool
604c89126c27104f659d7a51b0113e3bd435faf8fielding fits term = case term of
604c89126c27104f659d7a51b0113e3bd435faf8fielding (Sorted_term (Qual_var var' _ _) sort' _)
604c89126c27104f659d7a51b0113e3bd435faf8fielding -> (var == var') && (sort == sort')
909ce17e2bd0faef7b1c294f2307f009793fd493nd _ -> error "minExpTerm_qual: unsorted TERM after expansion"
909ce17e2bd0faef7b1c294f2307f009793fd493nd -- TODO: this type-checking might be too restrictive, see 'term_sort'
909ce17e2bd0faef7b1c294f2307f009793fd493nd -- choose all given terms that satisfy 'fits'
909ce17e2bd0faef7b1c294f2307f009793fd493nd selectExpansions :: [TERM f] -> [(TERM f, SORT)]
06ba4a61654b3763ad65f52283832ebf058fdf1cslive selectExpansions c = [ ((Qual_var var sort []), sort) |
06ba4a61654b3763ad65f52283832ebf058fdf1cslive sorted <- c,
06ba4a61654b3763ad65f52283832ebf058fdf1cslive fits sorted ]
06ba4a61654b3763ad65f52283832ebf058fdf1cslive -- TODO: this looks very wrong, doesn't it?
97a9a944b5887e91042b019776c41d5dd74557aferikabele{-----------------------------------------------------------
97a9a944b5887e91042b019776c41d5dd74557aferikabele - Minimal expansion of a sorted term -
97a9a944b5887e91042b019776c41d5dd74557aferikabele Expand a sorted term by typing information.
06ba4a61654b3763ad65f52283832ebf058fdf1cslive First expand the subterm, disregarding the given qualification.
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Then choose only expansions that satisfy that qualification, and
06ba4a61654b3763ad65f52283832ebf058fdf1cslive wrap the typing information around them.
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-----------------------------------------------------------}
06ba4a61654b3763ad65f52283832ebf058fdf1csliveminExpTerm_sorted :: (Eq f, PrettyPrint f) =>
cb3a1082aec4b3b4f4ed238c93c3cc54933a7f0end Min f e ->
06ba4a61654b3763ad65f52283832ebf058fdf1cslive GlobalAnnos ->
8e31885fc494b603e0650113dde9e29d1b1d2602maczniak Sign f e ->
97a9a944b5887e91042b019776c41d5dd74557aferikabele Result [[TERM f]]
8e31885fc494b603e0650113dde9e29d1b1d2602maczniakminExpTerm_sorted mef ga sign term sort pos = do
8e31885fc494b603e0650113dde9e29d1b1d2602maczniak -- expand subterm
f23fb63b05f89f47d7a3099491f2c68dcce432e9kess expandedTerm <- minExpTerm mef ga sign term
06ba4a61654b3763ad65f52283832ebf058fdf1cslive -- choose expansions that fit the given signature, then qualify
06ba4a61654b3763ad65f52283832ebf058fdf1cslive return $ qualifyTerms pos
06ba4a61654b3763ad65f52283832ebf058fdf1cslive $ map selectExpansions expandedTerm
06ba4a61654b3763ad65f52283832ebf058fdf1cslive where -- choose all given terms that match the current sort
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd selectExpansions :: [TERM f] -> [(TERM f, SORT)]
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd selectExpansions c = [ (sorted, sort) |
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd sorted <- c,
fe64b2ba25510d8c9dba5560a2d537763566cf40nd term_sort sorted == sort ]
ed0dae472b518c553c923a86fb4322d4c50d86a6nd{-----------------------------------------------------------
ed0dae472b518c553c923a86fb4322d4c50d86a6nd - Minimal expansion of a function application -
da637bcae7b6e150470e701af29da5604a34a17erbowen Expand a function application by typing information.
da637bcae7b6e150470e701af29da5604a34a17erbowen-----------------------------------------------------------}
da637bcae7b6e150470e701af29da5604a34a17erbowenminExpTerm_op :: (Eq f, PrettyPrint f) =>
da637bcae7b6e150470e701af29da5604a34a17erbowen GlobalAnnos ->
da637bcae7b6e150470e701af29da5604a34a17erbowen Sign f e ->
da637bcae7b6e150470e701af29da5604a34a17erbowen [TERM f] ->
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Result [[TERM f]]
fe64b2ba25510d8c9dba5560a2d537763566cf40nd-- If the op is indeed a constant, expand it as a simple identifier
fe64b2ba25510d8c9dba5560a2d537763566cf40ndminExpTerm_op _ _ sign (Op_name (Id.Id [tok] [] _)) [] _
fe64b2ba25510d8c9dba5560a2d537763566cf40nd = minExpTerm_simple sign tok
fe64b2ba25510d8c9dba5560a2d537763566cf40nd-- FIXME: Christian states that the above is too restrictive.
fe64b2ba25510d8c9dba5560a2d537763566cf40nd-- It should probably expand into an application again...
fe64b2ba25510d8c9dba5560a2d537763566cf40ndminExpTerm_op mef ga sign op terms pos = do
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -- expand argument subterms
fe64b2ba25510d8c9dba5560a2d537763566cf40nd expansions <- mapM (minExpTerm mef ga sign) terms
fb77c505254b6e9c925e23e734463e87574f8f40kess -- permute expansions to get a list of argument-lists to the function
fe64b2ba25510d8c9dba5560a2d537763566cf40nd permuted_exps <- return (permute expansions)
fb77c505254b6e9c925e23e734463e87574f8f40kess -- convert each permutation to a profile (as descr. on p. XXX)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -- then inject arguments that don't match the function's expected type
fe64b2ba25510d8c9dba5560a2d537763566cf40nd profiles <- return $ map (map insert_injections)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd $ map get_profile permuted_exps
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -- collect generated profiles into equivalence classes
c985aca104389df30d6ec0a637ce0ccaac904362nd p <- return $ concat
fe64b2ba25510d8c9dba5560a2d537763566cf40nd $ map (equivalence_Classes op_eq)
fb77c505254b6e9c925e23e734463e87574f8f40kess -- minimize generated equivalence classes (as descr. on p. XXX)
fb77c505254b6e9c925e23e734463e87574f8f40kess p' <- return (map (minimize_op sign) p)
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess -- transform minimized eq.classes into qualified function application terms
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess return $ qualifyTerms pos
fe64b2ba25510d8c9dba5560a2d537763566cf40nd $ qualifyOps p'
fe64b2ba25510d8c9dba5560a2d537763566cf40nd where -- the function's name
fe64b2ba25510d8c9dba5560a2d537763566cf40nd name :: OP_NAME
fe64b2ba25510d8c9dba5560a2d537763566cf40nd name = op_name op
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -- functions matching that name in the current environment
627c978514c54179736d152923478be7c8707f9bnd ops :: [OpType]
fe64b2ba25510d8c9dba5560a2d537763566cf40nd ops = Set.toList $ Map.findWithDefault Set.empty name $ (opMap sign)
fb77c505254b6e9c925e23e734463e87574f8f40kess -- extract a function's name from its definition
fb77c505254b6e9c925e23e734463e87574f8f40kess op_name :: OP_SYMB -> OP_NAME
fe64b2ba25510d8c9dba5560a2d537763566cf40nd op_name (Op_name name') = name'
fe64b2ba25510d8c9dba5560a2d537763566cf40nd op_name (Qual_op_name name' _ _) = name'
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -- extract a function's signature from its definition
fe64b2ba25510d8c9dba5560a2d537763566cf40nd op_type :: OP_SYMB -> OP_TYPE
fe64b2ba25510d8c9dba5560a2d537763566cf40nd op_type (Op_name _) = error "unqualified op"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive -- TODO: is there a nicer kind of error I can signal here?
06ba4a61654b3763ad65f52283832ebf058fdf1cslive op_type (Qual_op_name _ type' _) = type'
5bb5fba250bf526bc51d13b25378d54acb93c1cbnoodl -- qualify all ops in a list of eq.classes of ops
06ba4a61654b3763ad65f52283832ebf058fdf1cslive qualifyOps :: [[(OpType, [TERM f])]] -> [[(TERM f, SORT)]]
06ba4a61654b3763ad65f52283832ebf058fdf1cslive qualifyOps = map (map qualify_op)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive -- qualify a single op, given by its signature and its arguments
06ba4a61654b3763ad65f52283832ebf058fdf1cslive qualify_op :: (OpType, [TERM f]) -> (TERM f, SORT)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive qualify_op (op', terms')
06ba4a61654b3763ad65f52283832ebf058fdf1cslive = ((Application (Qual_op_name name (toOP_TYPE op') [])
06ba4a61654b3763ad65f52283832ebf058fdf1cslive , (opRes op'))
06ba4a61654b3763ad65f52283832ebf058fdf1cslive -- generate profiles as descr. on p. XXX
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd get_profile :: [[TERM f]] -> [(OpType, [TERM f])]
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd get_profile cs = [ (op', ts) |
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd op' <- ops,
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd ts <- (permute cs),
06ba4a61654b3763ad65f52283832ebf058fdf1cslive zipped_all (leq_SORT sign)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (map term_sort ts)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (opArgs op') ]
06ba4a61654b3763ad65f52283832ebf058fdf1cslive -- insert injections for all argument terms where neccessary
06ba4a61654b3763ad65f52283832ebf058fdf1cslive insert_injections :: (OpType, [TERM f]) -> (OpType, [TERM f])
06ba4a61654b3763ad65f52283832ebf058fdf1cslive insert_injections (op', args)
fb77c505254b6e9c925e23e734463e87574f8f40kess = (op', (zipWith inject args (opArgs op')))
fb77c505254b6e9c925e23e734463e87574f8f40kess -- the equivalence relation for functions as descr. on p. XXX
fb77c505254b6e9c925e23e734463e87574f8f40kess op_eq :: (OpType, [TERM f]) -> (OpType, [TERM f]) -> Bool
fe64b2ba25510d8c9dba5560a2d537763566cf40nd op_eq (op1,ts1) (op2,ts2)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd = let w1 = opArgs op1
fe64b2ba25510d8c9dba5560a2d537763566cf40nd w2 = opArgs op2
fe64b2ba25510d8c9dba5560a2d537763566cf40nd s1 = map term_sort ts1
fe64b2ba25510d8c9dba5560a2d537763566cf40nd s2 = map term_sort ts2
604c89126c27104f659d7a51b0113e3bd435faf8fielding b1 = zipped_all (leq_SORT sign) s1 w1
604c89126c27104f659d7a51b0113e3bd435faf8fielding b2 = zipped_all (leq_SORT sign) s2 w2
604c89126c27104f659d7a51b0113e3bd435faf8fielding ops_equal = (op1 == op2)
604c89126c27104f659d7a51b0113e3bd435faf8fielding ops_equiv = leqF sign op1 op2
604c89126c27104f659d7a51b0113e3bd435faf8fielding types_equal = False -- and (zipWith (==) s1 s2)
604c89126c27104f659d7a51b0113e3bd435faf8fielding -- TODO: check whether arg.types are equal
604c89126c27104f659d7a51b0113e3bd435faf8fielding in b1 && b2 && (ops_equal
fe64b2ba25510d8c9dba5560a2d537763566cf40nd || (ops_equiv
fe64b2ba25510d8c9dba5560a2d537763566cf40nd && types_equal))
604c89126c27104f659d7a51b0113e3bd435faf8fielding{-----------------------------------------------------------
fe64b2ba25510d8c9dba5560a2d537763566cf40nd - Minimal expansion of a type-cast -
604c89126c27104f659d7a51b0113e3bd435faf8fielding Expand a type-cast by typing information.
604c89126c27104f659d7a51b0113e3bd435faf8fielding First expand the contained subterm. Of the generated expansions,
604c89126c27104f659d7a51b0113e3bd435faf8fielding choose those that are of a subsort of the given target sort.
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Qualify the chosen expansions as terms of the target sort.
22265f1724519886e2a2b5e0ebd61477506b7379noodl-----------------------------------------------------------}
22265f1724519886e2a2b5e0ebd61477506b7379noodlminExpTerm_cast :: (Eq f, PrettyPrint f) =>
22265f1724519886e2a2b5e0ebd61477506b7379noodl GlobalAnnos ->
604c89126c27104f659d7a51b0113e3bd435faf8fielding Sign f e ->
604c89126c27104f659d7a51b0113e3bd435faf8fielding Result [[TERM f]]
604c89126c27104f659d7a51b0113e3bd435faf8fieldingminExpTerm_cast mef ga sign term sort pos = do
604c89126c27104f659d7a51b0113e3bd435faf8fielding -- expand subterm
604c89126c27104f659d7a51b0113e3bd435faf8fielding expandedTerm <- minExpTerm mef ga sign term
604c89126c27104f659d7a51b0113e3bd435faf8fielding -- choose only expansions that are subsorts of the given sort
604c89126c27104f659d7a51b0113e3bd435faf8fielding validExps <- return $ map (filter (leq_SORT sign sort . term_sort))
fe64b2ba25510d8c9dba5560a2d537763566cf40nd expandedTerm
9597f440430d8c876dd64f5f78066804650a18ecnoodl -- pair expansions w/ the given sort, then wrap qualification around
9597f440430d8c876dd64f5f78066804650a18ecnoodl return $ qualifyTerms pos
9597f440430d8c876dd64f5f78066804650a18ecnoodl $ map (map (\ t -> (t, sort))) validExps
9597f440430d8c876dd64f5f78066804650a18ecnoodl{-----------------------------------------------------------
9597f440430d8c876dd64f5f78066804650a18ecnoodl - Minimal expansion of a conditional -
9597f440430d8c876dd64f5f78066804650a18ecnoodl Expand a conditional by typing information.
9597f440430d8c876dd64f5f78066804650a18ecnoodl-----------------------------------------------------------}
9597f440430d8c876dd64f5f78066804650a18ecnoodlminExpTerm_cond :: (Eq f, PrettyPrint f) =>
9597f440430d8c876dd64f5f78066804650a18ecnoodl GlobalAnnos ->
9597f440430d8c876dd64f5f78066804650a18ecnoodl Sign f e ->
fe64b2ba25510d8c9dba5560a2d537763566cf40nd FORMULA f ->
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Result [[TERM f]]
fe64b2ba25510d8c9dba5560a2d537763566cf40ndminExpTerm_cond mef ga sign term1 formula term2 pos = do
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -- expand both subterms and the subsentence
fe64b2ba25510d8c9dba5560a2d537763566cf40nd expansions1 <- minExpTerm mef ga sign term1
fe64b2ba25510d8c9dba5560a2d537763566cf40nd expansions2 <- minExpTerm mef ga sign term2
fe64b2ba25510d8c9dba5560a2d537763566cf40nd expanded_formula <- minExpFORMULA mef ga sign formula
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -- permute stuff
fe64b2ba25510d8c9dba5560a2d537763566cf40nd permuted_exps <- return (permute [expansions1, expansions2])
fe64b2ba25510d8c9dba5560a2d537763566cf40nd profiles <- return (map get_profile permuted_exps)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive p <- return (concat (map (equivalence_Classes eq) profiles))
06ba4a61654b3763ad65f52283832ebf058fdf1cslive p' <- return (map (minimize_cond sign) p)
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslive return $ qualifyTerms pos
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslive $ qualifyConds expanded_formula p'
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd where -- TODO
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslive have_supersort :: [TERM f] -> Bool
fb77c505254b6e9c925e23e734463e87574f8f40kess have_supersort = not . Set.isEmpty . supersorts
fb77c505254b6e9c925e23e734463e87574f8f40kess supersorts :: [TERM f] -> Set.Set SORT
fb77c505254b6e9c925e23e734463e87574f8f40kess supersorts = common_supersorts sign . map term_sort
fb77c505254b6e9c925e23e734463e87574f8f40kess eq = xeq_TUPLE sign
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslive qualifyConds :: FORMULA f ->
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslive [[([TERM f], SORT)]] ->
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslive [[(TERM f, SORT)]]
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd qualifyConds f = map $ map (qualify_cond f)
130d299c4b2b15be45532a176604c71fdc7bea5bnd qualify_cond :: FORMULA f ->
130d299c4b2b15be45532a176604c71fdc7bea5bnd ([TERM f], SORT) ->
130d299c4b2b15be45532a176604c71fdc7bea5bnd (TERM f, SORT)
130d299c4b2b15be45532a176604c71fdc7bea5bnd qualify_cond f (ts, s) = case ts of
130d299c4b2b15be45532a176604c71fdc7bea5bnd [t1, t2] -> (Conditional t1 f t2 [], s)
130d299c4b2b15be45532a176604c71fdc7bea5bnd _ -> (Unparsed_term "" [],s)
130d299c4b2b15be45532a176604c71fdc7bea5bnd get_profile :: [[TERM f]] -> [([TERM f], SORT)]
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd get_profile cs = [ (c, s) |
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd c <- permute cs,
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd have_supersort c,
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd s <- Set.toList (supersorts c) ]
fb77c505254b6e9c925e23e734463e87574f8f40kess{-----------------------------------------------------------
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd Construct a TERM of type Sorted_term from each (TERM, SORT) tuple
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd TODO: 'Sorted_term' does _not_ fit in all cases!
b06660a3ed3d885e15d99c0209a46c4657df33fbrbowen-----------------------------------------------------------}
d1348237b33bc1755b9f1165eea52317465a7671ndqualifyTerms :: [Id.Pos] -> [[(TERM f, SORT)]] -> [[TERM f]]
d1348237b33bc1755b9f1165eea52317465a7671ndqualifyTerms pos pairs = map (map qualify_term) pairs
06ba4a61654b3763ad65f52283832ebf058fdf1cslive where qualify_term :: (TERM f, SORT) -> TERM f
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd qualify_term (t, s) = Sorted_term t s pos
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd{-----------------------------------------------------------
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd Construct explicit Injection to 'result_type'
fb77c505254b6e9c925e23e734463e87574f8f40kess if SORT of 'argument' does not match 'result_type'
fb77c505254b6e9c925e23e734463e87574f8f40kess-----------------------------------------------------------}
06ba4a61654b3763ad65f52283832ebf058fdf1csliveinject :: TERM f -> SORT -> TERM f
6b64034fa2a644ba291c484c0c01c7df5b8d982ckessinject argument result_type
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess | argument_type == result_type
06ba4a61654b3763ad65f52283832ebf058fdf1cslive | otherwise
06ba4a61654b3763ad65f52283832ebf058fdf1cslive = (Application (injOpSymb argument_type result_type) [argument] [])
06ba4a61654b3763ad65f52283832ebf058fdf1cslive where argument_type = term_sort argument
130d299c4b2b15be45532a176604c71fdc7bea5bndinjOpSymb :: SORT -> SORT -> OP_SYMB
130d299c4b2b15be45532a176604c71fdc7bea5bndinjOpSymb s1 s2 =
130d299c4b2b15be45532a176604c71fdc7bea5bnd Qual_op_name injName
130d299c4b2b15be45532a176604c71fdc7bea5bnd (Total_op_type [s1] s2 [Id.nullPos])
130d299c4b2b15be45532a176604c71fdc7bea5bnd{-----------------------------------------------------------
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd For each C in P (see above), let C' choose _one_
06ba4a61654b3763ad65f52283832ebf058fdf1cslive f:s \in C for each s minimal such that f:s \in C.
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-----------------------------------------------------------}
06ba4a61654b3763ad65f52283832ebf058fdf1csliveminimize_op :: Sign f e -> [(OpType, [TERM f])] -> [(OpType, [TERM f])]
06ba4a61654b3763ad65f52283832ebf058fdf1csliveminimize_op sign ops_n_terms = concat $ map reduce ops_n_terms
06ba4a61654b3763ad65f52283832ebf058fdf1cslive where results :: Set.Set SORT
06ba4a61654b3763ad65f52283832ebf058fdf1cslive results = Set.fromList (map (opRes . fst) ops_n_terms)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive lesserSorts :: SORT -> Set.Set SORT
06ba4a61654b3763ad65f52283832ebf058fdf1cslive lesserSorts s = Set.intersection results (subsortsOf s sign)
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess leastSort :: SORT -> Bool
06ba4a61654b3763ad65f52283832ebf058fdf1cslive leastSort s = Set.size (lesserSorts s) == 1
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess reduce :: (OpType, [TERM f]) -> [(OpType, [TERM f])]
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess reduce x@(op,_) = if (leastSort (opRes op)) then [x] else []
06ba4a61654b3763ad65f52283832ebf058fdf1cslive{-----------------------------------------------------------
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Workalike for minimize_op, but used inside m_e_t_cond.
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-----------------------------------------------------------}
06ba4a61654b3763ad65f52283832ebf058fdf1csliveminimize_cond :: Sign f e -> [([TERM f], SORT)] -> [([TERM f], SORT)]
06ba4a61654b3763ad65f52283832ebf058fdf1csliveminimize_cond sign terms_n_sort = concat $ map reduce terms_n_sort
06ba4a61654b3763ad65f52283832ebf058fdf1cslive where sorts :: Set.Set SORT
130d299c4b2b15be45532a176604c71fdc7bea5bnd sorts = Set.fromList (map snd terms_n_sort)
130d299c4b2b15be45532a176604c71fdc7bea5bnd lesserSorts :: SORT -> Set.Set SORT
130d299c4b2b15be45532a176604c71fdc7bea5bnd lesserSorts s = Set.intersection sorts (subsortsOf s sign)
130d299c4b2b15be45532a176604c71fdc7bea5bnd leastSort :: SORT -> Bool
130d299c4b2b15be45532a176604c71fdc7bea5bnd leastSort s = Set.size (lesserSorts s) == 1
130d299c4b2b15be45532a176604c71fdc7bea5bnd reduce :: ([TERM f], SORT) -> [([TERM f], SORT)]
130d299c4b2b15be45532a176604c71fdc7bea5bnd reduce x@(_,s) = if (leastSort s) then [x] else []
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess{-----------------------------------------------------------
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess - Extract the sort from a given term -
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess If the given term contains information about its sort, return that,
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess otherwise signal an error.
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess-----------------------------------------------------------}
06ba4a61654b3763ad65f52283832ebf058fdf1csliveterm_sort :: TERM f -> SORT
06ba4a61654b3763ad65f52283832ebf058fdf1csliveterm_sort term' = case term' of
fb77c505254b6e9c925e23e734463e87574f8f40kess (Sorted_term _ sort _) -> sort
fb77c505254b6e9c925e23e734463e87574f8f40kess (Qual_var _ sort _) -> sort
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (Cast _ sort _) -> sort
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (Application (Qual_op_name _ ty _) _ _) -> res_OP_TYPE ty
06ba4a61654b3763ad65f52283832ebf058fdf1cslive _ -> error "term_sort: unsorted TERM after expansion"
130d299c4b2b15be45532a176604c71fdc7bea5bnd -- TODO: is there a nicer kind of error I can signal here?
130d299c4b2b15be45532a176604c71fdc7bea5bnd{-----------------------------------------------------------
130d299c4b2b15be45532a176604c71fdc7bea5bnd - Return the set of subsorts common to all given sorts -
130d299c4b2b15be45532a176604c71fdc7bea5bnd-----------------------------------------------------------}
130d299c4b2b15be45532a176604c71fdc7bea5bndcommon_subsorts :: Sign f e -> [SORT] -> Set.Set SORT
130d299c4b2b15be45532a176604c71fdc7bea5bndcommon_subsorts sign srts = let get_subsorts = flip subsortsOf sign
06ba4a61654b3763ad65f52283832ebf058fdf1cslive $ map get_subsorts $ srts
06ba4a61654b3763ad65f52283832ebf058fdf1cslive{-----------------------------------------------------------
fb77c505254b6e9c925e23e734463e87574f8f40kess - Return the set of supersorts common to all given sorts -
fb77c505254b6e9c925e23e734463e87574f8f40kess-----------------------------------------------------------}
97a9a944b5887e91042b019776c41d5dd74557aferikabelecommon_supersorts :: Sign f e -> [SORT] -> Set.Set SORT
fe64b2ba25510d8c9dba5560a2d537763566cf40ndcommon_supersorts _ [] = Set.empty
fe64b2ba25510d8c9dba5560a2d537763566cf40ndcommon_supersorts sign srts = let get_supersorts = flip supersortsOf sign
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess $ map get_supersorts $ srts
fe64b2ba25510d8c9dba5560a2d537763566cf40nd{-----------------------------------------------------------
fe64b2ba25510d8c9dba5560a2d537763566cf40nd - True if all sorts have a common subsort -
fe64b2ba25510d8c9dba5560a2d537763566cf40nd-----------------------------------------------------------}
fe64b2ba25510d8c9dba5560a2d537763566cf40ndhave_common_subsorts :: Sign f e -> [SORT] -> Bool
fe64b2ba25510d8c9dba5560a2d537763566cf40ndhave_common_subsorts s = (not . Set.isEmpty . common_subsorts s)
15ba1801088da1aad6d20609cf3f7b0b1eefce8aslive{-----------------------------------------------------------
fe64b2ba25510d8c9dba5560a2d537763566cf40nd - True if all sorts have a common supersort -
fe64b2ba25510d8c9dba5560a2d537763566cf40nd-----------------------------------------------------------}
fe64b2ba25510d8c9dba5560a2d537763566cf40ndhave_common_supersorts :: Sign f e -> [SORT] -> Bool
fe64b2ba25510d8c9dba5560a2d537763566cf40ndhave_common_supersorts s = (not . Set.isEmpty . common_supersorts s)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd{-----------------------------------------------------------
06ba4a61654b3763ad65f52283832ebf058fdf1cslive - True if s1 <= s2 OR s1 >= s2 -
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-----------------------------------------------------------}
06ba4a61654b3763ad65f52283832ebf058fdf1cslivexeq_SORT :: Sign f e -> SORT -> SORT -> Bool
97a9a944b5887e91042b019776c41d5dd74557aferikabelexeq_SORT sign s1 s2 = (leq_SORT sign s1 s2) || (geq_SORT sign s1 s2)
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd{-----------------------------------------------------------
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd - True if s1 <= s2 OR s1 >= s2 -
6954edc623ca2c179eb5b33e97e4304d06fd649frbowen-----------------------------------------------------------}
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cndxeq_TUPLE :: Sign f e -> (a, SORT) -> (a, SORT) -> Bool
06ba4a61654b3763ad65f52283832ebf058fdf1cslivexeq_TUPLE sign (_,s1) (_,s2) = xeq_SORT sign s1 s2
fe64b2ba25510d8c9dba5560a2d537763566cf40nd{-----------------------------------------------------------
fe64b2ba25510d8c9dba5560a2d537763566cf40nd - True if s1 <= s2 -
fe64b2ba25510d8c9dba5560a2d537763566cf40nd-----------------------------------------------------------}
fe64b2ba25510d8c9dba5560a2d537763566cf40ndleq_SORT :: Sign f e -> SORT -> SORT -> Bool
06ba4a61654b3763ad65f52283832ebf058fdf1csliveleq_SORT sign s1 s2 = Set.member s2 (supersortsOf s1 sign)
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess{-----------------------------------------------------------
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess - True if s1 >= s2 -
fe64b2ba25510d8c9dba5560a2d537763566cf40nd-----------------------------------------------------------}
fe64b2ba25510d8c9dba5560a2d537763566cf40ndgeq_SORT :: Sign f e -> SORT -> SORT -> Bool
fe64b2ba25510d8c9dba5560a2d537763566cf40ndgeq_SORT sign s1 s2 = Set.member s2 (subsortsOf s1 sign)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd{-----------------------------------------------------------
fe64b2ba25510d8c9dba5560a2d537763566cf40nd - True if o1 ~F o2 -
fe64b2ba25510d8c9dba5560a2d537763566cf40nd-----------------------------------------------------------}
fe64b2ba25510d8c9dba5560a2d537763566cf40ndleqF :: Sign f e -> OpType -> OpType -> Bool
fe64b2ba25510d8c9dba5560a2d537763566cf40ndleqF sign o1 o2 = zipped_all are_legal (opArgs o1) (opArgs o2)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd && have_common_supersorts sign [(opRes o1), (opRes o2)]
fe64b2ba25510d8c9dba5560a2d537763566cf40nd where are_legal a b = have_common_subsorts sign [a, b]
fb77c505254b6e9c925e23e734463e87574f8f40kess{-----------------------------------------------------------
fb77c505254b6e9c925e23e734463e87574f8f40kess - True if p1 ~P p2 -
fb77c505254b6e9c925e23e734463e87574f8f40kess-----------------------------------------------------------}
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cndleqP :: Sign f e -> PredType -> PredType -> Bool
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cndleqP sign p1 p2 = zipped_all are_legal (predArgs p1) (predArgs p2)
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd where are_legal a b = have_common_subsorts sign [a, b]