Overload.hs revision eb4c721139bd2e372939de781aafc2c859f70bc3
97a9a944b5887e91042b019776c41d5dd74557aferikabele Module : $Header$
97a9a944b5887e91042b019776c41d5dd74557aferikabele Copyright : (c) Martin Kuehl, T. Mossakowski, C. Maeder, Uni Bremen 2004-2005
a945f35eff8b6a88009ce73de6d4c862ce58de3cslive License : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
a945f35eff8b6a88009ce73de6d4c862ce58de3cslive Maintainer : maeder@tzi.de
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Stability : provisional
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Portability : portable
fe64b2ba25510d8c9dba5560a2d537763566cf40ndOverload resolution (injections are inserted separately)
d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowen Follows Sect. III:3.3 of the CASL Reference Manual.
d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowen The algorthim is from:
d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowen Till Mossakowski, Kolyang, Bernd Krieg-Brueckner:
d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowen Static semantic analysis and theorem proving for CASL.
fe64b2ba25510d8c9dba5560a2d537763566cf40nd 12th Workshop on Algebraic Development Techniques, Tarquinia 1997,
fe64b2ba25510d8c9dba5560a2d537763566cf40nd LNCS 1376, p. 333-348
3f08db06526d6901aa08c110b5bc7dde6bc39905ndmodule CASL.Overload(minExpFORMULA, oneExpTerm, Min, combine,
fe64b2ba25510d8c9dba5560a2d537763566cf40nd is_unambiguous, term_sort, leqF, leqP, leq_SORT,
fe64b2ba25510d8c9dba5560a2d537763566cf40nd minimalSupers, maximalSubs, keepMinimals) where
3b3b7fc78d1f5bfc2769903375050048ff41ff26ndimport qualified Common.Lib.Rel as Rel
ad74a0524a06bfe11b7de9e3b4ce7233ab3bd3f7ndimport qualified Common.Lib.Map as Map
4aa805f8500255bc52a4c03259fe46df10a1d07cyoshikiimport qualified Common.Lib.Set as Set
fe64b2ba25510d8c9dba5560a2d537763566cf40nd-- | the type of the type checking function of extensions
fe64b2ba25510d8c9dba5560a2d537763566cf40ndtype Min f e = Sign f e -> f -> Result f
fe64b2ba25510d8c9dba5560a2d537763566cf40nd{-----------------------------------------------------------
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna - Minimal expansion of a formula -
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Expand a given formula by typing information.
117c1f888a14e73cdd821dc6c23eb0411144a41cnd * For non-atomic formulae, recurse through subsentences.
117c1f888a14e73cdd821dc6c23eb0411144a41cnd * For trival atomic formulae, no expansion is neccessary.
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd * For atomic formulae, the following cases are implemented:
117c1f888a14e73cdd821dc6c23eb0411144a41cnd + Predication is handled by the dedicated expansion function
bed3c2e56e8f3328e780200466b9d009093db468sf 'minExpFORMULA_pred'.
117c1f888a14e73cdd821dc6c23eb0411144a41cnd + Existl_equation and Strong_equation are handled by the dedicated
117c1f888a14e73cdd821dc6c23eb0411144a41cnd expansion function 'minExpFORMULA_eq'.
9464a57d17bd3db87268f8eed322ceb65cfec818jim + Definedness is handled by expanding the subterm.
117c1f888a14e73cdd821dc6c23eb0411144a41cnd + Membership is handled like Cast
9597f440430d8c876dd64f5f78066804650a18ecnoodl-----------------------------------------------------------}
117c1f888a14e73cdd821dc6c23eb0411144a41cndminExpFORMULA :: PrettyPrint f => Min f e -> Sign f e -> FORMULA f
117c1f888a14e73cdd821dc6c23eb0411144a41cnd -> Result (FORMULA f)
117c1f888a14e73cdd821dc6c23eb0411144a41cndminExpFORMULA mef sign formula = case formula of
8559a67073808d84d85bb5dd552d4247caafe709sf Quantification q vars f pos -> do
8559a67073808d84d85bb5dd552d4247caafe709sf -- add 'vars' to signature
117c1f888a14e73cdd821dc6c23eb0411144a41cnd let (_, sign') = runState (mapM_ addVars vars) sign
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejesh -- expand subformula
dce2bc31f4940687c7ffabb80570bc37ea7296d8trawick f' <- minExpFORMULA mef sign' f
117c1f888a14e73cdd821dc6c23eb0411144a41cnd return (Quantification q vars f' pos)
117c1f888a14e73cdd821dc6c23eb0411144a41cnd Conjunction fs pos -> do
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf fs' <- mapR (minExpFORMULA mef sign) fs
e797af4d7b0cada1278d72d6c8ac77210ef78632minfrin return (Conjunction fs' pos)
117c1f888a14e73cdd821dc6c23eb0411144a41cnd Disjunction fs pos -> do
117c1f888a14e73cdd821dc6c23eb0411144a41cnd fs' <- mapR (minExpFORMULA mef sign) fs
117c1f888a14e73cdd821dc6c23eb0411144a41cnd return (Disjunction fs' pos)
117c1f888a14e73cdd821dc6c23eb0411144a41cnd Implication f1 f2 b pos ->
c3e2e664a67b1adb9b6a6b91ff161f4f562cecf6covener joinResultWith (\ f1' f2' -> Implication f1' f2' b pos)
117c1f888a14e73cdd821dc6c23eb0411144a41cnd (minExpFORMULA mef sign f1) $ minExpFORMULA mef sign f2
3cc4ff86e6cc4cfd7d4ccfc58dedff599091444bnoodl Equivalence f1 f2 pos ->
117c1f888a14e73cdd821dc6c23eb0411144a41cnd joinResultWith (\ f1' f2' -> Equivalence f1' f2' pos)
117c1f888a14e73cdd821dc6c23eb0411144a41cnd (minExpFORMULA mef sign f1) $ minExpFORMULA mef sign f2
117c1f888a14e73cdd821dc6c23eb0411144a41cnd Negation f pos -> do
0193f13df922db31ff281e3e5ce9632fe42bac87sf f' <- minExpFORMULA mef sign f
117c1f888a14e73cdd821dc6c23eb0411144a41cnd return (Negation f' pos)
117c1f888a14e73cdd821dc6c23eb0411144a41cnd Predication (Pred_name ide) terms pos
117c1f888a14e73cdd821dc6c23eb0411144a41cnd -> minExpFORMULA_pred mef sign ide Nothing terms pos
117c1f888a14e73cdd821dc6c23eb0411144a41cnd Predication (Qual_pred_name ide ty pos1) terms pos2
6c45910d5394acbc3f20ab3f2615d9ed2b4e6533nd -> minExpFORMULA_pred mef sign ide (Just $ toPredType ty)
117c1f888a14e73cdd821dc6c23eb0411144a41cnd terms (pos1 `appRange` pos2)
117c1f888a14e73cdd821dc6c23eb0411144a41cnd Existl_equation term1 term2 pos
117c1f888a14e73cdd821dc6c23eb0411144a41cnd -> minExpFORMULA_eq mef sign Existl_equation term1 term2 pos
117c1f888a14e73cdd821dc6c23eb0411144a41cnd Strong_equation term1 term2 pos
117c1f888a14e73cdd821dc6c23eb0411144a41cnd -> minExpFORMULA_eq mef sign Strong_equation term1 term2 pos
117c1f888a14e73cdd821dc6c23eb0411144a41cnd Definedness term pos -> do
117c1f888a14e73cdd821dc6c23eb0411144a41cnd t <- oneExpTerm mef sign term
117c1f888a14e73cdd821dc6c23eb0411144a41cnd return (Definedness t pos)
e83cd73f10044371dd9dfa5f46b6d7d5c585fe54sf Membership term sort pos -> do
117c1f888a14e73cdd821dc6c23eb0411144a41cnd ts <- minExpTerm mef sign term
2b6565aedca9e9c10691b12fd2f3689bf4c85bc7jim let fs = map (concatMap ( \ t ->
2b6565aedca9e9c10691b12fd2f3689bf4c85bc7jim let s = term_sort t in
6beba165aeced2ca77a6f1593ee08c47a32099efcovener if leq_SORT sign sort s then
709e3a21ba73b8433462959cd56c773454b34441trawick [Membership t sort pos] else
117c1f888a14e73cdd821dc6c23eb0411144a41cnd map ( \ c ->
117c1f888a14e73cdd821dc6c23eb0411144a41cnd Membership (Sorted_term t c pos) sort pos)
9f19223e8fb7b99f5f1cc02c8c3c2c6567793262rbowen $ minimalSupers sign s sort)) ts
17f88acd0b3fba7eddb6fd974927edf8f5dbe41dsf is_unambiguous (globAnnos sign) formula fs pos
117c1f888a14e73cdd821dc6c23eb0411144a41cnd ExtFORMULA f -> fmap ExtFORMULA $ mef sign f
117c1f888a14e73cdd821dc6c23eb0411144a41cnd _ -> return formula -- do not fail even for unresolved cases
117c1f888a14e73cdd821dc6c23eb0411144a41cnd-- | test if a term can be uniquely resolved
e797af4d7b0cada1278d72d6c8ac77210ef78632minfrinoneExpTerm :: PrettyPrint f => Min f e -> Sign f e
117c1f888a14e73cdd821dc6c23eb0411144a41cnd -> TERM f -> Result (TERM f)
117c1f888a14e73cdd821dc6c23eb0411144a41cndoneExpTerm minF sign term = do
117c1f888a14e73cdd821dc6c23eb0411144a41cnd ts <- minExpTerm minF sign term
117c1f888a14e73cdd821dc6c23eb0411144a41cnd is_unambiguous (globAnnos sign) term ts nullRange
117c1f888a14e73cdd821dc6c23eb0411144a41cnd{-----------------------------------------------------------
117c1f888a14e73cdd821dc6c23eb0411144a41cnd - Minimal expansion of an equation formula -
117c1f888a14e73cdd821dc6c23eb0411144a41cnd see minExpTerm_cond
117c1f888a14e73cdd821dc6c23eb0411144a41cnd-----------------------------------------------------------}
117c1f888a14e73cdd821dc6c23eb0411144a41cndminExpFORMULA_eq :: PrettyPrint f => Min f e -> Sign f e
117c1f888a14e73cdd821dc6c23eb0411144a41cnd -> (TERM f -> TERM f -> Range -> FORMULA f)
b00fe3c3354db01001b8eddfd9b88441380f837dwrowe -> TERM f -> TERM f -> Range -> Result (FORMULA f)
e797af4d7b0cada1278d72d6c8ac77210ef78632minfrinminExpFORMULA_eq mef sign eq term1 term2 pos = do
117c1f888a14e73cdd821dc6c23eb0411144a41cnd ps <- minExpTerm_cond mef sign ( \ t1 t2 -> eq t1 t2 pos)
a38b5f73e7f0f3b8726fb47d27b145f37036ead0jim term1 term2 pos
117c1f888a14e73cdd821dc6c23eb0411144a41cnd is_unambiguous (globAnnos sign) (eq term1 term2 pos) ps pos
fe64b2ba25510d8c9dba5560a2d537763566cf40nd-- | check if there is at least one solution
30471a4650391f57975f60bbb6e4a90be7b284bfhumbedoohhasSolutions :: PrettyPrint f => GlobalAnnos -> f -> [[f]] -> Range
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -> Result [[f]]
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquernahasSolutions ga topterm ts pos = let terms = filter (not . null) ts in
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna if null terms then Result
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna [Diag Error ("no typing for: " ++ show (printText0 ga topterm))
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna pos] Nothing
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna else return terms
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna-- | check if there is a unique equivalence class
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquernais_unambiguous :: PrettyPrint f => GlobalAnnos -> f -> [[f]] -> Range
b09fcdfc59ada4712150e7bcc7b502bb9e4601d8rjung -> Result f
b09fcdfc59ada4712150e7bcc7b502bb9e4601d8rjungis_unambiguous ga topterm ts pos = do
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna terms <- hasSolutions ga topterm ts pos
d972e4a0688f66b1402473dd9dacfecefa2132a8rbowen case terms of
173e5f4d5ec46b5febb74ce860d753bb1faaba0fsf [ term : _ ] -> return term
d972e4a0688f66b1402473dd9dacfecefa2132a8rbowen _ -> Result [Diag Error ("ambiguous term\n " ++
d972e4a0688f66b1402473dd9dacfecefa2132a8rbowen showSepList (showString "\n ") (shows . printText0 ga)
d972e4a0688f66b1402473dd9dacfecefa2132a8rbowen (take 5 $ map head terms) "") pos] Nothing
5ae609a8a09239d20f48a4a95c4f21b713995babwrowecheckIdAndArgs :: Id -> [a] -> Range -> Result Int
5ae609a8a09239d20f48a4a95c4f21b713995babwrowecheckIdAndArgs ide args poss =
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe let nargs = length args
031bbbc0d1189b07330e38d0c126820a9ab7795egryzor pargs = placeCount ide
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe in if isMixfix ide && pargs /= nargs then
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe Result [Diag Error
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen ("expected " ++ shows pargs " argument(s) of mixfix identifier '"
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen ++ showPretty ide "' but found " ++ shows nargs " argument(s)")
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen poss] Nothing
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen else return nargs
6fad623c3cc52b4a84d4d36538f6eed886f49f98covenernoOpOrPred :: PrettyPrint t => [a] -> String -> Maybe t -> Id -> Range
6fad623c3cc52b4a84d4d36538f6eed886f49f98covener -> Int -> Result ()
6fad623c3cc52b4a84d4d36538f6eed886f49f98covenernoOpOrPred ops str mty ide pos nargs =
6fad623c3cc52b4a84d4d36538f6eed886f49f98covener if null ops then case mty of
6fad623c3cc52b4a84d4d36538f6eed886f49f98covener Nothing -> Result [Diag Error
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna ("no " ++ str ++ " with " ++ shows nargs " argument"
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen ++ (if nargs == 1 then "" else "s") ++ " found for '"
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen ++ showPretty ide "'") pos] Nothing
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen Just ty -> Result [Diag Error
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen ("no " ++ str ++ " with profile '"
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen ++ showPretty ty "' found for '"
031bbbc0d1189b07330e38d0c126820a9ab7795egryzor ++ showPretty ide "'") pos] Nothing
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna else return ()
031bbbc0d1189b07330e38d0c126820a9ab7795egryzor{-----------------------------------------------------------
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna - Minimal expansion of a predication formula -
031bbbc0d1189b07330e38d0c126820a9ab7795egryzor see minExpTerm_appl
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna-----------------------------------------------------------}
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquernaminExpFORMULA_pred :: PrettyPrint f => Min f e -> Sign f e -> Id
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna -> Maybe PredType -> [TERM f] -> Range
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna -> Result (FORMULA f)
51b60896224b408a35684bd6ec0fafe5e4abe322rbowenminExpFORMULA_pred mef sign ide mty args pos = do
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen nargs <- checkIdAndArgs ide args pos
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen let -- predicates matching that name in the current environment
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen preds' = Set.filter ( \ p -> length (predArgs p) == nargs) $
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna preds = case mty of
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna Nothing -> map (pSortBy predArgs sign)
031bbbc0d1189b07330e38d0c126820a9ab7795egryzor $ leqClasses (leqP' sign) preds'
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna Just ty -> if Set.member ty preds'
031bbbc0d1189b07330e38d0c126820a9ab7795egryzor then [[ty]] else []
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna noOpOrPred preds "predicate" mty ide pos nargs
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna expansions <- mapM (minExpTerm mef sign) args
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna let get_profiles :: [[TERM f]] -> [[(PredType, [TERM f])]]
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe get_profiles cs = map (get_profile cs) preds
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen get_profile :: [[TERM f]] -> [PredType] -> [(PredType, [TERM f])]
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen get_profile cs ps = [ (pred', ts) |
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen pred' <- ps,
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen and $ zipWith (leq_SORT sign)
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe (map term_sort ts)
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe (predArgs pred') ]
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe qualForms = qualifyPreds ide pos
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe $ concatMap (get_profiles . combine)
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe $ combine expansions
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe is_unambiguous (globAnnos sign)
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe (Predication (Pred_name ide) args pos) qualForms pos
5ae609a8a09239d20f48a4a95c4f21b713995babwrowequalifyPreds :: Id -> Range -> [[(PredType, [TERM f])]] -> [[FORMULA f]]
5ae609a8a09239d20f48a4a95c4f21b713995babwrowequalifyPreds ide pos = map $ map $ qualify_pred ide pos
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe-- | qualify a single pred, given by its signature and its arguments
d972e4a0688f66b1402473dd9dacfecefa2132a8rbowenqualify_pred :: Id -> Range -> (PredType, [TERM f]) -> FORMULA f
5ae609a8a09239d20f48a4a95c4f21b713995babwrowequalify_pred ide pos (pred', terms') =
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe Predication (Qual_pred_name ide (toPRED_TYPE pred') pos) terms' pos
031bbbc0d1189b07330e38d0c126820a9ab7795egryzor-- | expansions of an equation formula or a conditional
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquernaminExpTerm_eq :: PrettyPrint f => Min f e -> Sign f e -> TERM f -> TERM f
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna -> Result [[(TERM f, TERM f)]]
9f19223e8fb7b99f5f1cc02c8c3c2c6567793262rbowenminExpTerm_eq mef sign term1 term2 = do
9f19223e8fb7b99f5f1cc02c8c3c2c6567793262rbowen exps1 <- minExpTerm mef sign term1
c3c006c28c5b03892ccaef6e4d2cbb15a13a2072rbowen exps2 <- minExpTerm mef sign term2
9f19223e8fb7b99f5f1cc02c8c3c2c6567793262rbowen return $ map (minimize_eq sign)
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna $ map getPairs $ combine [exps1, exps2]
fe64b2ba25510d8c9dba5560a2d537763566cf40ndgetPairs :: [[TERM f]] -> [(TERM f, TERM f)]
fe64b2ba25510d8c9dba5560a2d537763566cf40ndgetPairs cs = [ (t1, t2) | [t1,t2] <- combine cs ]
fe64b2ba25510d8c9dba5560a2d537763566cf40ndminimize_eq :: Sign f e -> [(TERM f, TERM f)] -> [(TERM f, TERM f)]
fe64b2ba25510d8c9dba5560a2d537763566cf40ndminimize_eq s l = keepMinimals s (term_sort . snd) $
fe64b2ba25510d8c9dba5560a2d537763566cf40nd keepMinimals s (term_sort . fst) l
fe64b2ba25510d8c9dba5560a2d537763566cf40nd{-----------------------------------------------------------
fe64b2ba25510d8c9dba5560a2d537763566cf40nd - Minimal expansion of a term -
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Expand a given term by typing information.
06ba4a61654b3763ad65f52283832ebf058fdf1cslive * 'Simple_id' do not exist!
06ba4a61654b3763ad65f52283832ebf058fdf1cslive * 'Qual_var' terms are handled by 'minExpTerm_var'
06ba4a61654b3763ad65f52283832ebf058fdf1cslive * 'Application' terms are handled by 'minExpTerm_op'.
06ba4a61654b3763ad65f52283832ebf058fdf1cslive * 'Conditional' terms are handled by 'minExpTerm_cond'.
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-----------------------------------------------------------}
fb77c505254b6e9c925e23e734463e87574f8f40kessminExpTerm :: PrettyPrint f => Min f e -> Sign f e -> TERM f
fb77c505254b6e9c925e23e734463e87574f8f40kess -> Result [[TERM f]]
06ba4a61654b3763ad65f52283832ebf058fdf1csliveminExpTerm mef sign top = let ga = globAnnos sign in case top of
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Qual_var var sort _ -> let ts = minExpTerm_var sign var (Just sort) in
06ba4a61654b3763ad65f52283832ebf058fdf1cslive if null ts then mkError "no matching qualified variable found" var
06ba4a61654b3763ad65f52283832ebf058fdf1cslive else return ts
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Application op terms pos -> minExpTerm_op mef sign op terms pos
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Sorted_term term sort pos -> do
fb77c505254b6e9c925e23e734463e87574f8f40kess expandedTerm <- minExpTerm mef sign term
06ba4a61654b3763ad65f52283832ebf058fdf1cslive -- choose expansions that fit the given signature, then qualify
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let validExps = map (filter $ \ t -> leq_SORT sign (term_sort t) sort)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive expandedTerm
06ba4a61654b3763ad65f52283832ebf058fdf1cslive hasSolutions ga top (map (map (\ t ->
fb77c505254b6e9c925e23e734463e87574f8f40kess Sorted_term t sort pos)) validExps) pos
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Cast term sort pos -> do
06ba4a61654b3763ad65f52283832ebf058fdf1cslive expandedTerm <- minExpTerm mef sign term
06ba4a61654b3763ad65f52283832ebf058fdf1cslive -- find a unique minimal common supersort
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let ts = map (concatMap (\ t -> let s = term_sort t in
06ba4a61654b3763ad65f52283832ebf058fdf1cslive if leq_SORT sign sort s then
fb77c505254b6e9c925e23e734463e87574f8f40kess if leq_SORT sign s sort then [t] else
06ba4a61654b3763ad65f52283832ebf058fdf1cslive [Cast t sort pos] else
06ba4a61654b3763ad65f52283832ebf058fdf1cslive map ( \ c ->
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Cast (Sorted_term t c pos) sort pos)
fb77c505254b6e9c925e23e734463e87574f8f40kess $ minimalSupers sign s sort)) expandedTerm
fb77c505254b6e9c925e23e734463e87574f8f40kess hasSolutions ga top ts pos
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Conditional term1 formula term2 pos -> do
fb77c505254b6e9c925e23e734463e87574f8f40kess f <- minExpFORMULA mef sign formula
bc4b55ec8f31569d606d5680d50189a355bcd7a6rbowen ts <- minExpTerm_cond mef sign ( \ t1 t2 -> Conditional t1 f t2 pos)
fb77c505254b6e9c925e23e734463e87574f8f40kess term1 term2 pos
06ba4a61654b3763ad65f52283832ebf058fdf1cslive hasSolutions ga (Conditional term1 formula term2 pos) ts pos
06ba4a61654b3763ad65f52283832ebf058fdf1cslive _ -> error "minExpTerm"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-- | Minimal expansion of a possibly qualified variable identifier
fb77c505254b6e9c925e23e734463e87574f8f40kessminExpTerm_var :: Sign f e -> Token -> Maybe SORT -> [[TERM f]]
fb77c505254b6e9c925e23e734463e87574f8f40kessminExpTerm_var sign tok ms = case Map.lookup tok $ varMap sign of
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Nothing -> []
fb77c505254b6e9c925e23e734463e87574f8f40kess Just s -> let qv = [[Qual_var tok s nullRange]] in
fb77c505254b6e9c925e23e734463e87574f8f40kess case ms of
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Nothing -> qv
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd Just s2 -> if s == s2 then qv else []
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen-- | minimal expansion of an (possibly qualified) operator application
51b60896224b408a35684bd6ec0fafe5e4abe322rbowenminExpTerm_appl :: PrettyPrint f => Min f e -> Sign f e -> Id
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen -> Maybe OpType -> [TERM f] -> Range -> Result [[TERM f]]
51b60896224b408a35684bd6ec0fafe5e4abe322rbowenminExpTerm_appl mef sign ide mty args pos = do
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen nargs <- checkIdAndArgs ide args pos
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen let -- functions matching that name in the current environment
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen ops' = Set.filter ( \ o -> length (opArgs o) == nargs) $
fe64b2ba25510d8c9dba5560a2d537763566cf40nd ops = case mty of
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Nothing -> map (pSortBy opArgs sign)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd $ leqClasses (leqF' sign) ops'
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Just ty -> if Set.member ty ops' ||
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -- might be known to be total
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Set.member ty {opKind = Total} ops'
fe64b2ba25510d8c9dba5560a2d537763566cf40nd then [[ty]] else []
fe64b2ba25510d8c9dba5560a2d537763566cf40nd noOpOrPred ops "operation" mty ide pos nargs
fe64b2ba25510d8c9dba5560a2d537763566cf40nd expansions <- mapM (minExpTerm mef sign) args
fe64b2ba25510d8c9dba5560a2d537763566cf40nd let -- generate profiles as descr. on p. 339 (Step 3)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd get_profiles cs = map (get_profile cs) ops
fe64b2ba25510d8c9dba5560a2d537763566cf40nd get_profile cs os = [ (op', ts) |
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess op' <- os,
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslive and $ zipWith (leq_SORT sign)
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess (map term_sort ts)
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess (opArgs op') ]
06ba4a61654b3763ad65f52283832ebf058fdf1cslive qualTerms = qualifyOps ide pos
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen $ map (minimize_op sign)
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen $ concatMap (get_profiles . combine)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive $ combine expansions
06ba4a61654b3763ad65f52283832ebf058fdf1cslive hasSolutions (globAnnos sign)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (Application (Op_name ide) args pos) qualTerms pos
06ba4a61654b3763ad65f52283832ebf058fdf1cslivequalifyOps :: Id -> Range -> [[(OpType, [TERM f])]] -> [[TERM f]]
06ba4a61654b3763ad65f52283832ebf058fdf1cslivequalifyOps ide pos = map $ map $ qualify_op ide pos
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen -- qualify a single op, given by its signature and its arguments
51b60896224b408a35684bd6ec0fafe5e4abe322rbowenqualify_op :: Id -> Range -> (OpType, [TERM f]) -> TERM f
51b60896224b408a35684bd6ec0fafe5e4abe322rbowenqualify_op ide pos (op', terms') =
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen Application (Qual_op_name ide (toOP_TYPE op') pos) terms' pos
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen{-----------------------------------------------------------
fe64b2ba25510d8c9dba5560a2d537763566cf40nd - Minimal expansion of a function application or a variable -
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Expand a function application by typing information.
fe64b2ba25510d8c9dba5560a2d537763566cf40nd 1. First expand all argument subterms.
fe64b2ba25510d8c9dba5560a2d537763566cf40nd 2. Combine these expansions so we compute the set of tuples
fe64b2ba25510d8c9dba5560a2d537763566cf40nd { (C_1, ..., C_n) | (C_1, ..., C_n) \in
fe64b2ba25510d8c9dba5560a2d537763566cf40nd minExpTerm(t_1) x ... x minExpTerm(t_n) }
fe64b2ba25510d8c9dba5560a2d537763566cf40nd where t_1, ..., t_n are the given argument terms.
fe64b2ba25510d8c9dba5560a2d537763566cf40nd 3. For each element of this set compute the set of possible profiles
fe64b2ba25510d8c9dba5560a2d537763566cf40nd (as described on p. 339).
fe64b2ba25510d8c9dba5560a2d537763566cf40nd 4. Define an equivalence relation ~ on these profiles
fe64b2ba25510d8c9dba5560a2d537763566cf40nd (as described on p. 339).
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd 5. Separate each profile into equivalence classes by the relation ~
627c978514c54179736d152923478be7c8707f9bnd and take the unification of these sets.
fe64b2ba25510d8c9dba5560a2d537763566cf40nd 6. Minimize each element of this unified set (as described on p. 339).
fe64b2ba25510d8c9dba5560a2d537763566cf40nd 7. Transform each term in the minimized set into a qualified function
fe64b2ba25510d8c9dba5560a2d537763566cf40nd application term.
fe64b2ba25510d8c9dba5560a2d537763566cf40nd-----------------------------------------------------------}
fe64b2ba25510d8c9dba5560a2d537763566cf40ndminExpTerm_op :: PrettyPrint f => Min f e -> Sign f e -> OP_SYMB -> [TERM f]
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -> Range -> Result [[TERM f]]
fe64b2ba25510d8c9dba5560a2d537763566cf40ndminExpTerm_op mef sign (Op_name ide@(Id (tok:_) _ _)) args pos =
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd let res = minExpTerm_appl mef sign ide Nothing args pos in
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd if null args && isSimpleId ide then
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd let vars = minExpTerm_var sign tok Nothing
888b616027180cc8aaa4d2bee5ecc6acec175bc5nd in if null vars then res else
b95ae799514ad86a15610ad75808d7065e9847c9kess case maybeResult res of
888b616027180cc8aaa4d2bee5ecc6acec175bc5nd Nothing -> return vars
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd Just ops -> return (ops ++ vars)
5224ff8eae5156a05f676f1dad8add2e2f2efe1dndminExpTerm_op mef sign (Qual_op_name ide ty pos1) args pos2 =
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd if length args /= length (args_OP_TYPE ty) then
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd mkError "type qualification does not match number of arguments" ide
604c89126c27104f659d7a51b0113e3bd435faf8fielding else minExpTerm_appl mef sign ide (Just $ toOpType ty) args
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd (pos1 `appRange` pos2)
06ba4a61654b3763ad65f52283832ebf058fdf1csliveminExpTerm_op _ _ _ _ _ = error "minExpTerm_op"
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen{-----------------------------------------------------------
fe64b2ba25510d8c9dba5560a2d537763566cf40nd - Minimal expansion of a conditional -
888b616027180cc8aaa4d2bee5ecc6acec175bc5nd Expand a conditional by typing information (see minExpTerm_eq)
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd First expand the subterms and subformula. Then calculate a profile
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd P(C_1, C_2) for each (C_1, C_2) \in minExpTerm(t1) x minExpTerm(t_2).
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd Separate these profiles into equivalence classes and take the
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd unification of all these classes. Minimize each equivalence class.
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd Finally transform the eq. classes into lists of
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd conditionals with equally sorted terms.
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd-----------------------------------------------------------}
5224ff8eae5156a05f676f1dad8add2e2f2efe1dndminExpTerm_cond :: PrettyPrint f => Min f e -> Sign f e
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd -> (TERM f -> TERM f -> a) -> TERM f -> TERM f -> Range
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd -> Result [[a]]
5224ff8eae5156a05f676f1dad8add2e2f2efe1dndminExpTerm_cond mef sign f term1 term2 pos = do
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd pairs <- minExpTerm_eq mef sign term1 term2
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd return $ map (concatMap ( \ (t1, t2) ->
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd let s1 = term_sort t1
fe64b2ba25510d8c9dba5560a2d537763566cf40nd s2 = term_sort t2
fe64b2ba25510d8c9dba5560a2d537763566cf40nd in if s1 == s2 then [f t1 t2]
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd else if leq_SORT sign s2 s1 then
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd [f t1 (Sorted_term t2 s1 pos)]
9583adab6bc4b3758e41963c905d9dad9f067131nd else if leq_SORT sign s1 s2 then
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd [f (Sorted_term t1 s2 pos) t2]
2509f1cd3be884abbe4852e15b8da00bebaad5b1poirier else map ( \ s -> f (Sorted_term t1 s pos)
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd (Sorted_term t2 s pos))
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd $ minimalSupers sign s1 s2)) pairs
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd{-----------------------------------------------------------
b09fcdfc59ada4712150e7bcc7b502bb9e4601d8rjung Let P be a set of equivalence classes of qualified terms.
2509f1cd3be884abbe4852e15b8da00bebaad5b1poirier For each C \in P, let C' choose _one_
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd t:s \in C for each s minimal such that t:s \in C.
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd That is, discard all terms whose sort is a supersort of
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd any other term in the same equivalence class.
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd-----------------------------------------------------------}
2509f1cd3be884abbe4852e15b8da00bebaad5b1poirierminimize_op :: Sign f e -> [(OpType, [TERM f])] -> [(OpType, [TERM f])]
2509f1cd3be884abbe4852e15b8da00bebaad5b1poirierminimize_op sign = keepMinimals sign (opRes . fst)
2509f1cd3be884abbe4852e15b8da00bebaad5b1poirier-- | Extract the sort from an analysed term
2509f1cd3be884abbe4852e15b8da00bebaad5b1poirierterm_sort :: TERM f -> SORT
2509f1cd3be884abbe4852e15b8da00bebaad5b1poirierterm_sort term' = case term' of
2509f1cd3be884abbe4852e15b8da00bebaad5b1poirier Sorted_term _ sort _ -> sort
2509f1cd3be884abbe4852e15b8da00bebaad5b1poirier Qual_var _ sort _ -> sort
2509f1cd3be884abbe4852e15b8da00bebaad5b1poirier Cast _ sort _ -> sort
2509f1cd3be884abbe4852e15b8da00bebaad5b1poirier Application (Qual_op_name _ ty _) _ _ -> res_OP_TYPE ty
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd Conditional t1 _ _ _ -> term_sort t1
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd _ -> error "term_sort: unsorted TERM after expansion"
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd-- | the (possibly incomplete) list of supersorts common to both sorts
4335f1cbf345c91bb996eec540c11ba8ce5d4268ndcommon_supersorts :: Bool -> Sign f e -> SORT -> SORT -> [SORT]
2509f1cd3be884abbe4852e15b8da00bebaad5b1poiriercommon_supersorts b sign s1 s2 =
2509f1cd3be884abbe4852e15b8da00bebaad5b1poirier if s1 == s2 then [s1] else
2509f1cd3be884abbe4852e15b8da00bebaad5b1poirier let l1 = supersortsOf s1 sign
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd l2 = supersortsOf s2 sign in
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd if Set.member s2 l1 then if b then [s2] else [s1] else
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd if Set.member s1 l2 then if b then [s1] else [s2] else
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd else Set.intersection (subsortsOf s1 sign)
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd $ subsortsOf s2 sign
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd-- | True if both sorts have a common supersort
fe64b2ba25510d8c9dba5560a2d537763566cf40ndhave_common_supersorts :: Bool -> Sign f e -> SORT -> SORT -> Bool
fe64b2ba25510d8c9dba5560a2d537763566cf40ndhave_common_supersorts b s s1 s2 = not $ null $ common_supersorts b s s1 s2
627c978514c54179736d152923478be7c8707f9bnd-- True if both sorts have a common subsort
fb77c505254b6e9c925e23e734463e87574f8f40kesshave_common_subsorts :: Sign f e -> SORT -> SORT -> Bool
fe64b2ba25510d8c9dba5560a2d537763566cf40ndhave_common_subsorts = have_common_supersorts False
fe64b2ba25510d8c9dba5560a2d537763566cf40nd-- | if True test if s1 > s2
fe64b2ba25510d8c9dba5560a2d537763566cf40ndgeq_SORT :: Bool -> Sign f e -> SORT -> SORT -> Bool
fe64b2ba25510d8c9dba5560a2d537763566cf40ndgeq_SORT b sign s1 s2 = let rel = sortRel sign in
fb77c505254b6e9c925e23e734463e87574f8f40kess-- | if True test if s1 < s2
fb77c505254b6e9c925e23e734463e87574f8f40kessleq_SORT :: Sign f e -> SORT -> SORT -> Bool
6b64034fa2a644ba291c484c0c01c7df5b8d982ckessleq_SORT sign s1 s2 = s1 == s2 || Set.member s2 (supersortsOf s1 sign)
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess-- | minimal common supersorts of the two input sorts
10673857794a4b3d9568ca2d983722a87ed352f1rbowenminimalSupers :: Sign f e -> SORT -> SORT -> [SORT]
fb77c505254b6e9c925e23e734463e87574f8f40kessminimalSupers = minimalSupers1 True
ed0dae472b518c553c923a86fb4322d4c50d86a6ndminimalSupers1 :: Bool -> Sign f e -> SORT -> SORT -> [SORT]
10673857794a4b3d9568ca2d983722a87ed352f1rbowenminimalSupers1 b s s1 s2 =
10673857794a4b3d9568ca2d983722a87ed352f1rbowen keepMinimals1 b s id $ common_supersorts b s s1 s2
bed3c2e56e8f3328e780200466b9d009093db468sf-- | maximal common subsorts of the two input sorts
bed3c2e56e8f3328e780200466b9d009093db468sfmaximalSubs :: Sign f e -> SORT -> SORT -> [SORT]
bed3c2e56e8f3328e780200466b9d009093db468sfmaximalSubs = minimalSupers1 False
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-- | only keep elements with minimal (and different) sorts
06ba4a61654b3763ad65f52283832ebf058fdf1cslivekeepMinimals :: Sign f e -> (a -> SORT) -> [a] -> [a]
fb77c505254b6e9c925e23e734463e87574f8f40kesskeepMinimals = keepMinimals1 True
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cndkeepMinimals1 :: Bool -> Sign f e -> (a -> SORT) -> [a] -> [a]
06ba4a61654b3763ad65f52283832ebf058fdf1cslivekeepMinimals1 b s f l = case l of
06ba4a61654b3763ad65f52283832ebf058fdf1cslive x : r1 -> let v = f x
06ba4a61654b3763ad65f52283832ebf058fdf1cslive r2 = filter (\ y -> let w = f y in
06ba4a61654b3763ad65f52283832ebf058fdf1cslive not (geq_SORT b s w v) && v /= w) r1
06ba4a61654b3763ad65f52283832ebf058fdf1cslive m = keepMinimals1 b s f r2
06ba4a61654b3763ad65f52283832ebf058fdf1cslive in if any (geq_SORT b s v . f) r2 then m
cb3a1082aec4b3b4f4ed238c93c3cc54933a7f0end-- | True if both ops are in the overloading relation
9335f6d807d76d60e54af4ededdebebddb3e3d13noodlleqF :: Sign f e -> OpType -> OpType -> Bool
9335f6d807d76d60e54af4ededdebebddb3e3d13noodlleqF sign o1 o2 = length (opArgs o1) == length (opArgs o2) && leqF' sign o1 o2
06ba4a61654b3763ad65f52283832ebf058fdf1csliveleqF' :: Sign f e -> OpType -> OpType -> Bool
06ba4a61654b3763ad65f52283832ebf058fdf1csliveleqF' sign o1 o2 = have_common_supersorts True sign (opRes o1) (opRes o2) &&
06ba4a61654b3763ad65f52283832ebf058fdf1cslive and (zipWith (have_common_subsorts sign) (opArgs o1) (opArgs o2))
604c89126c27104f659d7a51b0113e3bd435faf8fielding-- | True if both preds are in the overloading relation
604c89126c27104f659d7a51b0113e3bd435faf8fieldingleqP :: Sign f e -> PredType -> PredType -> Bool
604c89126c27104f659d7a51b0113e3bd435faf8fieldingleqP sign p1 p2 = length (predArgs p1) == length (predArgs p2)
604c89126c27104f659d7a51b0113e3bd435faf8fielding && leqP' sign p1 p2
604c89126c27104f659d7a51b0113e3bd435faf8fieldingleqP' :: Sign f e -> PredType -> PredType -> Bool
604c89126c27104f659d7a51b0113e3bd435faf8fieldingleqP' sign p1 p2 =
604c89126c27104f659d7a51b0113e3bd435faf8fielding and $ zipWith (have_common_subsorts sign) (predArgs p1) $ predArgs p2
e6342815b6b2be821ab51f5e867e210b47203429humbedooh-- | Divide a Set (List) into equivalence classes w.r.t. eq
909ce17e2bd0faef7b1c294f2307f009793fd493ndleqClasses :: Ord a => (a -> a -> Bool) -> Set.Set a -> [[a]]
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-- | Transform a list [l1,l2, ... ln] to (in sloppy notation)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-- [[x1,x2, ... ,xn] | x1<-l1, x2<-l2, ... xn<-ln]
06ba4a61654b3763ad65f52283832ebf058fdf1cslivecombine :: [[a]] -> [[a]]
06ba4a61654b3763ad65f52283832ebf058fdf1cslivecombine [] = [[]]
06ba4a61654b3763ad65f52283832ebf058fdf1cslivecombine (x:l) = concatMap ((`map` combine l) . (:)) x
97a9a944b5887e91042b019776c41d5dd74557aferikabele-- a better name would be "combine"
97a9a944b5887e91042b019776c41d5dd74557aferikabelecmpSubsort :: Sign f e -> POrder SORT
e56276e30ac0c3830f6ee0b0799eadc49e7338cbrbowencmpSubsort sign s1 s2 =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive if s1 == s2 then Just EQ else
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let l1 = supersortsOf s1 sign
06ba4a61654b3763ad65f52283832ebf058fdf1cslive l2 = supersortsOf s2 sign
06ba4a61654b3763ad65f52283832ebf058fdf1cslive b = Set.member s1 l2 in
06ba4a61654b3763ad65f52283832ebf058fdf1cslive if Set.member s2 l1 then
897b9432efe6e6effa0939f700b1ccc50b29698crbowen if b then Just EQ
06ba4a61654b3763ad65f52283832ebf058fdf1cslive else Just LT
173e5f4d5ec46b5febb74ce860d753bb1faaba0fsf else if b then Just GT else Nothing
173e5f4d5ec46b5febb74ce860d753bb1faaba0fsfcmpSubsorts :: Sign f e -> POrder [SORT]
d1636bdc2e674b84ee46f534b51be18ecac6bef5rbowencmpSubsorts sign l1 l2 =
a84592bb632899fd65753b227741b5ebe6b3b471jim let l = zipWith (cmpSubsort sign) l1 l2
a84592bb632899fd65753b227741b5ebe6b3b471jim in if null l then Just EQ else foldr1
d1636bdc2e674b84ee46f534b51be18ecac6bef5rbowen ( \ c1 c2 -> if c1 == c2 then c1 else case (c1, c2) of
d1636bdc2e674b84ee46f534b51be18ecac6bef5rbowen (Nothing, _) -> Nothing
d1636bdc2e674b84ee46f534b51be18ecac6bef5rbowen (_, Nothing) -> Nothing
d1636bdc2e674b84ee46f534b51be18ecac6bef5rbowen (Just EQ, _) -> c2
d1636bdc2e674b84ee46f534b51be18ecac6bef5rbowen (_, Just EQ) -> c1
d1636bdc2e674b84ee46f534b51be18ecac6bef5rbowen _ -> Nothing) l
d1636bdc2e674b84ee46f534b51be18ecac6bef5rbowenpSortBy :: (a -> [SORT]) -> Sign f e -> [a] -> [a]
d1636bdc2e674b84ee46f534b51be18ecac6bef5rbowenpSortBy f sign = let pOrd a b = cmpSubsorts sign (f a) (f b)
d1636bdc2e674b84ee46f534b51be18ecac6bef5rbowen in concat . rankBy pOrd
d1636bdc2e674b84ee46f534b51be18ecac6bef5rbowen-- * stolen from Keith Wansbrough 2000, Partial.lhs
d1636bdc2e674b84ee46f534b51be18ecac6bef5rbowen-- | the partial order relation type
2e1ba74a0ed02fe61c93492e3958934e750f0b0endtype POrder a = a -> a -> Maybe Ordering
d1636bdc2e674b84ee46f534b51be18ecac6bef5rbowen-- | split a set into the minimal elements and the remaining elements
d1636bdc2e674b84ee46f534b51be18ecac6bef5rbowenminimalBy :: POrder a -> [a] -> ([a],[a])
d1636bdc2e674b84ee46f534b51be18ecac6bef5rbowenminimalBy order es = go es [] []
d1636bdc2e674b84ee46f534b51be18ecac6bef5rbowen where go (x:xs) ms rs = if any (\ e -> order x e == Just GT) es
a84592bb632899fd65753b227741b5ebe6b3b471jim then go xs ms (x:rs)
8e31885fc494b603e0650113dde9e29d1b1d2602maczniak else go xs (x:ms) rs
06ba4a61654b3763ad65f52283832ebf058fdf1cslive go [] ms rs = (ms,rs)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-- | split a set into ranks of elements, minimal first
97a9a944b5887e91042b019776c41d5dd74557aferikabelerankBy :: POrder a -> [a] -> [[a]]
8e31885fc494b603e0650113dde9e29d1b1d2602maczniakrankBy order l = go l
8e31885fc494b603e0650113dde9e29d1b1d2602maczniak where go [] = []
a011221d1a3bfb6ec07a3596c6dc962c58041ee6covener go es@(_:_) = let (xs,ys) = minimalBy order es