{- |
Module      :  ./CASL/Overload.hs
Description :  Overload resolution
Copyright   :  (c) Martin Kuehl, T. Mossakowski, C. Maeder, 2004-2007
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable

Overload resolution (injections are inserted separately)
    Follows Sect. III:3.3 of the CASL Reference Manual.
    The algorthim is from:
      Till Mossakowski, Kolyang, Bernd Krieg-Brueckner:
      Static semantic analysis and theorem proving for CASL.
      12th Workshop on Algebraic Development Techniques, Tarquinia 1997,
      LNCS 1376, p. 333-348
-}

module CASL.Overload
  ( minExpFORMULA
  , minExpFORMULAeq
  , minExpTerm
  , isUnambiguous
  , oneExpTerm
  , mkSorted
  , Min
  , leqF
  , leqP
  , leqSort
  , minimalSupers
  , maximalSubs
  , haveCommonSupersorts
  , haveCommonSubsorts
  , keepMinimals1
  , keepMinimals
  ) where

import CASL.ToDoc (FormExtension)
import CASL.Sign
import CASL.AS_Basic_CASL

import qualified Common.Lib.MapSet as MapSet
import qualified Common.Lib.Rel as Rel
import Common.Lib.State
import Common.Id
import Common.GlobalAnnotations
import Common.DocUtils
import Common.Result
import Common.Partial
import Common.Utils

import Data.List
import Data.Maybe
import qualified Data.Map as Map
import qualified Data.Set as Set

import Control.Monad

-- | the type of the type checking function of extensions
type Min f e = Sign f e -> f -> Result f

mkSorted :: TermExtension f => Sign f e -> TERM f -> SORT -> Range -> TERM f
mkSorted :: Sign f e -> TERM f -> SORT -> Range -> TERM f
mkSorted sign :: Sign f e
sign t :: TERM f
t s :: SORT
s r :: Range
r = let nt :: TERM f
nt = TERM f -> SORT -> Range -> TERM f
forall f. TERM f -> SORT -> Range -> TERM f
Sorted_term TERM f
t SORT
s Range
r in case TERM f -> Maybe SORT
forall f. TermExtension f => f -> Maybe SORT
optTermSort TERM f
t of
  Nothing -> TERM f
nt
  Just srt :: SORT
srt -> if Sign f e -> SORT -> SORT -> Bool
forall f e. Sign f e -> SORT -> SORT -> Bool
leqSort Sign f e
sign SORT
s SORT
srt then TERM f
t else TERM f
nt

{- ----------------------------------------------------------
    - Minimal expansion of a formula -
  Expand a given formula by typing information.
  * For non-atomic formulae, recurse through subsentences.
  * For trival atomic formulae, no expansion is neccessary.
  * For atomic formulae, the following cases are implemented:
    + Predication is handled by the dedicated expansion function
      'minExpFORMULApred'.
    + Existl_equation and Strong_equation are handled by the dedicated
      expansion function 'minExpFORMULAeq'.
    + Definedness is handled by expanding the subterm.
    + Membership is handled like Cast
---------------------------------------------------------- -}
minExpFORMULA
  :: (FormExtension f, TermExtension f)
   => Min f e -> Sign f e -> FORMULA f -> Result (FORMULA f)
minExpFORMULA :: Min f e -> Sign f e -> FORMULA f -> Result (FORMULA f)
minExpFORMULA mef :: Min f e
mef sign :: Sign f e
sign formula :: FORMULA f
formula = let sign0 :: Sign f e
sign0 = Sign f e
sign { envDiags :: [Diagnosis]
envDiags = [] } in
  case FORMULA f
formula of
    Quantification q :: QUANTIFIER
q vars :: [VAR_DECL]
vars f :: FORMULA f
f pos :: Range
pos -> do
        -- add 'vars' to signature
        let sign' :: Sign f e
sign' = State (Sign f e) () -> Sign f e -> Sign f e
forall s a. State s a -> s -> s
execState ((VAR_DECL -> State (Sign f e) ())
-> [VAR_DECL] -> State (Sign f e) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ VAR_DECL -> State (Sign f e) ()
forall f e. VAR_DECL -> State (Sign f e) ()
addVars [VAR_DECL]
vars) Sign f e
sign0
        [Diagnosis] -> Maybe () -> Result ()
forall a. [Diagnosis] -> Maybe a -> Result a
Result (Sign f e -> [Diagnosis]
forall f e. Sign f e -> [Diagnosis]
envDiags Sign f e
sign') (Maybe () -> Result ()) -> Maybe () -> Result ()
forall a b. (a -> b) -> a -> b
$ () -> Maybe ()
forall a. a -> Maybe a
Just ()
        FORMULA f
f' <- Min f e -> Sign f e -> FORMULA f -> Result (FORMULA f)
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> FORMULA f -> Result (FORMULA f)
minExpFORMULA Min f e
mef Sign f e
sign' FORMULA f
f
        FORMULA f -> Result (FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
q [VAR_DECL]
vars FORMULA f
f' Range
pos)
    Junction j :: Junctor
j fs :: [FORMULA f]
fs pos :: Range
pos -> do
        [FORMULA f]
fs' <- (FORMULA f -> Result (FORMULA f))
-> [FORMULA f] -> Result [FORMULA f]
forall a b. (a -> Result b) -> [a] -> Result [b]
mapR (Min f e -> Sign f e -> FORMULA f -> Result (FORMULA f)
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> FORMULA f -> Result (FORMULA f)
minExpFORMULA Min f e
mef Sign f e
sign) [FORMULA f]
fs
        FORMULA f -> Result (FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (Junctor -> [FORMULA f] -> Range -> FORMULA f
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction Junctor
j [FORMULA f]
fs' Range
pos)
    Relation f1 :: FORMULA f
f1 c :: Relation
c f2 :: FORMULA f
f2 pos :: Range
pos ->
        (FORMULA f -> FORMULA f -> FORMULA f)
-> Result (FORMULA f) -> Result (FORMULA f) -> Result (FORMULA f)
forall a b c. (a -> b -> c) -> Result a -> Result b -> Result c
joinResultWith (\ f1' :: FORMULA f
f1' f2' :: FORMULA f
f2' -> FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
Relation FORMULA f
f1' Relation
c FORMULA f
f2' Range
pos)
              (Min f e -> Sign f e -> FORMULA f -> Result (FORMULA f)
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> FORMULA f -> Result (FORMULA f)
minExpFORMULA Min f e
mef Sign f e
sign FORMULA f
f1) (Result (FORMULA f) -> Result (FORMULA f))
-> Result (FORMULA f) -> Result (FORMULA f)
forall a b. (a -> b) -> a -> b
$ Min f e -> Sign f e -> FORMULA f -> Result (FORMULA f)
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> FORMULA f -> Result (FORMULA f)
minExpFORMULA Min f e
mef Sign f e
sign FORMULA f
f2
    Negation f :: FORMULA f
f pos :: Range
pos -> do
        FORMULA f
f' <- Min f e -> Sign f e -> FORMULA f -> Result (FORMULA f)
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> FORMULA f -> Result (FORMULA f)
minExpFORMULA Min f e
mef Sign f e
sign FORMULA f
f
        FORMULA f -> Result (FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA f -> Range -> FORMULA f
forall f. FORMULA f -> Range -> FORMULA f
Negation FORMULA f
f' Range
pos)
    Predication (Pred_name ide :: SORT
ide) terms :: [TERM f]
terms pos :: Range
pos
        -> Min f e
-> Sign f e
-> SORT
-> Maybe PredType
-> [TERM f]
-> Range
-> Result (FORMULA f)
forall f e.
(FormExtension f, TermExtension f) =>
Min f e
-> Sign f e
-> SORT
-> Maybe PredType
-> [TERM f]
-> Range
-> Result (FORMULA f)
minExpFORMULApred Min f e
mef Sign f e
sign SORT
ide Maybe PredType
forall a. Maybe a
Nothing [TERM f]
terms Range
pos
    Predication (Qual_pred_name ide :: SORT
ide ty :: PRED_TYPE
ty pos1 :: Range
pos1) terms :: [TERM f]
terms pos2 :: Range
pos2
        -> Min f e
-> Sign f e
-> SORT
-> Maybe PredType
-> [TERM f]
-> Range
-> Result (FORMULA f)
forall f e.
(FormExtension f, TermExtension f) =>
Min f e
-> Sign f e
-> SORT
-> Maybe PredType
-> [TERM f]
-> Range
-> Result (FORMULA f)
minExpFORMULApred Min f e
mef Sign f e
sign SORT
ide (PredType -> Maybe PredType
forall a. a -> Maybe a
Just (PredType -> Maybe PredType) -> PredType -> Maybe PredType
forall a b. (a -> b) -> a -> b
$ PRED_TYPE -> PredType
toPredType PRED_TYPE
ty)
           [TERM f]
terms (Range
pos1 Range -> Range -> Range
`appRange` Range
pos2)
    Equation term1 :: TERM f
term1 e :: Equality
e term2 :: TERM f
term2 pos :: Range
pos
        -> Min f e
-> Sign f e
-> (TERM f -> TERM f -> Range -> FORMULA f)
-> TERM f
-> TERM f
-> Range
-> Result (FORMULA f)
forall f e.
(FormExtension f, TermExtension f) =>
Min f e
-> Sign f e
-> (TERM f -> TERM f -> Range -> FORMULA f)
-> TERM f
-> TERM f
-> Range
-> Result (FORMULA f)
minExpFORMULAeq Min f e
mef Sign f e
sign (TERM f -> Equality -> TERM f -> Range -> FORMULA f
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
`Equation` Equality
e) TERM f
term1 TERM f
term2 Range
pos
    Definedness term :: TERM f
term pos :: Range
pos -> do
        TERM f
t <- Min f e -> Sign f e -> TERM f -> Result (TERM f)
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> TERM f -> Result (TERM f)
oneExpTerm Min f e
mef Sign f e
sign TERM f
term
        FORMULA f -> Result (FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (TERM f -> Range -> FORMULA f
forall f. TERM f -> Range -> FORMULA f
Definedness TERM f
t Range
pos)
    Membership term :: TERM f
term srt :: SORT
srt pos :: Range
pos -> do
        [[TERM f]]
ts <- Min f e -> Sign f e -> TERM f -> Result [[TERM f]]
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> TERM f -> Result [[TERM f]]
minExpTerm Min f e
mef Sign f e
sign TERM f
term
        let fs :: [[FORMULA f]]
fs = ([TERM f] -> [FORMULA f]) -> [[TERM f]] -> [[FORMULA f]]
forall a b. (a -> b) -> [a] -> [b]
map ((TERM f -> [FORMULA f]) -> [TERM f] -> [FORMULA f]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ( \ t :: TERM f
t ->
                    (SORT -> FORMULA f) -> [SORT] -> [FORMULA f]
forall a b. (a -> b) -> [a] -> [b]
map ( \ c :: SORT
c ->
                        TERM f -> SORT -> Range -> FORMULA f
forall f. TERM f -> SORT -> Range -> FORMULA f
Membership (Sign f e -> TERM f -> SORT -> Range -> TERM f
forall f e.
TermExtension f =>
Sign f e -> TERM f -> SORT -> Range -> TERM f
mkSorted Sign f e
sign TERM f
t SORT
c Range
pos) SORT
srt Range
pos)
                    ([SORT] -> [FORMULA f]) -> [SORT] -> [FORMULA f]
forall a b. (a -> b) -> a -> b
$ [SORT] -> (SORT -> [SORT]) -> Maybe SORT -> [SORT]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [SORT
srt] (Sign f e -> SORT -> SORT -> [SORT]
forall f e. Sign f e -> SORT -> SORT -> [SORT]
minimalSupers Sign f e
sign SORT
srt)
                    (Maybe SORT -> [SORT]) -> Maybe SORT -> [SORT]
forall a b. (a -> b) -> a -> b
$ TERM f -> Maybe SORT
forall f. TermExtension f => f -> Maybe SORT
optTermSort TERM f
t)) [[TERM f]]
ts
            msg :: String
msg = Bool -> Sign f e -> SORT -> [[TERM f]] -> String
forall f e.
TermExtension f =>
Bool -> Sign f e -> SORT -> [[TERM f]] -> String
superSortError Bool
True Sign f e
sign SORT
srt [[TERM f]]
ts
        String
-> GlobalAnnos
-> FORMULA f
-> [[FORMULA f]]
-> Range
-> Result (FORMULA f)
forall f.
Pretty f =>
String -> GlobalAnnos -> f -> [[f]] -> Range -> Result f
isUnambiguous String
msg (Sign f e -> GlobalAnnos
forall f e. Sign f e -> GlobalAnnos
globAnnos Sign f e
sign) FORMULA f
formula [[FORMULA f]]
fs Range
pos
    ExtFORMULA f :: f
f -> (f -> FORMULA f) -> Result f -> Result (FORMULA f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f -> FORMULA f
forall f. f -> FORMULA f
ExtFORMULA (Result f -> Result (FORMULA f)) -> Result f -> Result (FORMULA f)
forall a b. (a -> b) -> a -> b
$ Min f e
mef Sign f e
sign f
f
    QuantOp o :: SORT
o ty :: OP_TYPE
ty f :: FORMULA f
f -> do
        let sign' :: Sign f e
sign' = Sign f e
sign0 { opMap :: OpMap
opMap = SORT -> OpType -> OpMap -> OpMap
addOpTo SORT
o (OP_TYPE -> OpType
toOpType OP_TYPE
ty) (OpMap -> OpMap) -> OpMap -> OpMap
forall a b. (a -> b) -> a -> b
$ Sign f e -> OpMap
forall f e. Sign f e -> OpMap
opMap Sign f e
sign0 }
        [Diagnosis] -> Maybe () -> Result ()
forall a. [Diagnosis] -> Maybe a -> Result a
Result (Sign f e -> [Diagnosis]
forall f e. Sign f e -> [Diagnosis]
envDiags Sign f e
sign') (Maybe () -> Result ()) -> Maybe () -> Result ()
forall a b. (a -> b) -> a -> b
$ () -> Maybe ()
forall a. a -> Maybe a
Just ()
        FORMULA f
f' <- Min f e -> Sign f e -> FORMULA f -> Result (FORMULA f)
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> FORMULA f -> Result (FORMULA f)
minExpFORMULA Min f e
mef Sign f e
sign' FORMULA f
f
        FORMULA f -> Result (FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA f -> Result (FORMULA f))
-> FORMULA f -> Result (FORMULA f)
forall a b. (a -> b) -> a -> b
$ SORT -> OP_TYPE -> FORMULA f -> FORMULA f
forall f. SORT -> OP_TYPE -> FORMULA f -> FORMULA f
QuantOp SORT
o OP_TYPE
ty FORMULA f
f'
    QuantPred p :: SORT
p ty :: PRED_TYPE
ty f :: FORMULA f
f -> do
        let pm :: PredMap
pm = Sign f e -> PredMap
forall f e. Sign f e -> PredMap
predMap Sign f e
sign0
            sign' :: Sign f e
sign' = Sign f e
sign0
              { predMap :: PredMap
predMap = SORT -> PredType -> PredMap -> PredMap
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert SORT
p (PRED_TYPE -> PredType
toPredType PRED_TYPE
ty) PredMap
pm }
        [Diagnosis] -> Maybe () -> Result ()
forall a. [Diagnosis] -> Maybe a -> Result a
Result (Sign f e -> [Diagnosis]
forall f e. Sign f e -> [Diagnosis]
envDiags Sign f e
sign') (Maybe () -> Result ()) -> Maybe () -> Result ()
forall a b. (a -> b) -> a -> b
$ () -> Maybe ()
forall a. a -> Maybe a
Just ()
        FORMULA f
f' <- Min f e -> Sign f e -> FORMULA f -> Result (FORMULA f)
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> FORMULA f -> Result (FORMULA f)
minExpFORMULA Min f e
mef Sign f e
sign' FORMULA f
f
        FORMULA f -> Result (FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA f -> Result (FORMULA f))
-> FORMULA f -> Result (FORMULA f)
forall a b. (a -> b) -> a -> b
$ SORT -> PRED_TYPE -> FORMULA f -> FORMULA f
forall f. SORT -> PRED_TYPE -> FORMULA f -> FORMULA f
QuantPred SORT
p PRED_TYPE
ty FORMULA f
f'
    Mixfix_formula term :: TERM f
term -> do
       TERM f
t <- Min f e -> Sign f e -> TERM f -> Result (TERM f)
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> TERM f -> Result (TERM f)
oneExpTerm Min f e
mef Sign f e
sign TERM f
term
       let Result ds :: [Diagnosis]
ds mt :: Maybe (FORMULA f)
mt = Range -> Result (FORMULA f) -> Result (FORMULA f)
forall a. Range -> Result a -> Result a
adjustPos (TERM f -> Range
forall a. GetRange a => a -> Range
getRangeSpan TERM f
term) (Result (FORMULA f) -> Result (FORMULA f))
-> Result (FORMULA f) -> Result (FORMULA f)
forall a b. (a -> b) -> a -> b
$ TERM f -> Result (FORMULA f)
forall f. TermExtension f => TERM f -> Result (FORMULA f)
termToFormula TERM f
t
       [Diagnosis] -> Result ()
appendDiags [Diagnosis]
ds
       case Maybe (FORMULA f)
mt of
         Nothing -> String -> TERM f -> Result (FORMULA f)
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "not a formula" TERM f
term
         Just f :: FORMULA f
f -> FORMULA f -> Result (FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return FORMULA f
f
    _ -> FORMULA f -> Result (FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return FORMULA f
formula -- do not fail even for unresolved cases

superSortError :: TermExtension f
  => Bool -> Sign f e -> SORT -> [[TERM f]] -> String
superSortError :: Bool -> Sign f e -> SORT -> [[TERM f]] -> String
superSortError super :: Bool
super sign :: Sign f e
sign srt :: SORT
srt ts :: [[TERM f]]
ts = let
  ds :: [SORT]
ds = Sign f e -> (SORT -> SORT) -> [SORT] -> [SORT]
forall f e a. Sign f e -> (a -> SORT) -> [a] -> [a]
keepMinimals Sign f e
sign SORT -> SORT
forall a. a -> a
id ([SORT] -> [SORT]) -> ([TERM f] -> [SORT]) -> [TERM f] -> [SORT]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TERM f -> SORT) -> [TERM f] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map TERM f -> SORT
forall f. TermExtension f => f -> SORT
sortOfTerm ([TERM f] -> [SORT]) -> [TERM f] -> [SORT]
forall a b. (a -> b) -> a -> b
$ [[TERM f]] -> [TERM f]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[TERM f]]
ts
  in "\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [SORT] -> String
showSort [SORT]
ds String -> String -> String
forall a. [a] -> [a] -> [a]
++ "found but\na "
     String -> String -> String
forall a. [a] -> [a] -> [a]
++ (if Bool
super then "super" else "sub") String -> String -> String
forall a. [a] -> [a] -> [a]
++ "sort of '"
              String -> String -> String
forall a. [a] -> [a] -> [a]
++ SORT -> String -> String
forall a. Show a => a -> String -> String
shows SORT
srt "' was expected."

-- | test if a term can be uniquely resolved
oneExpTerm :: (FormExtension f, TermExtension f)
  => Min f e -> Sign f e -> TERM f -> Result (TERM f)
oneExpTerm :: Min f e -> Sign f e -> TERM f -> Result (TERM f)
oneExpTerm minF :: Min f e
minF sign :: Sign f e
sign term :: TERM f
term = do
    [[TERM f]]
ts <- Min f e -> Sign f e -> TERM f -> Result [[TERM f]]
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> TERM f -> Result [[TERM f]]
minExpTerm Min f e
minF Sign f e
sign TERM f
term
    String
-> GlobalAnnos -> TERM f -> [[TERM f]] -> Range -> Result (TERM f)
forall f.
Pretty f =>
String -> GlobalAnnos -> f -> [[f]] -> Range -> Result f
isUnambiguous "" (Sign f e -> GlobalAnnos
forall f e. Sign f e -> GlobalAnnos
globAnnos Sign f e
sign) TERM f
term [[TERM f]]
ts Range
nullRange

{- ----------------------------------------------------------
    - Minimal expansion of an equation formula -
  see minExpTermCond
---------------------------------------------------------- -}
minExpFORMULAeq :: (FormExtension f, TermExtension f)
  => Min f e -> Sign f e -> (TERM f -> TERM f -> Range -> FORMULA f)
    -> TERM f -> TERM f -> Range -> Result (FORMULA f)
minExpFORMULAeq :: Min f e
-> Sign f e
-> (TERM f -> TERM f -> Range -> FORMULA f)
-> TERM f
-> TERM f
-> Range
-> Result (FORMULA f)
minExpFORMULAeq mef :: Min f e
mef sign :: Sign f e
sign eq :: TERM f -> TERM f -> Range -> FORMULA f
eq term1 :: TERM f
term1 term2 :: TERM f
term2 pos :: Range
pos = do
    (ps :: [[FORMULA f]]
ps, msg :: String
msg) <- Min f e
-> Sign f e
-> (TERM f -> TERM f -> FORMULA f)
-> TERM f
-> TERM f
-> Range
-> Result ([[FORMULA f]], String)
forall f e a.
(FormExtension f, TermExtension f) =>
Min f e
-> Sign f e
-> (TERM f -> TERM f -> a)
-> TERM f
-> TERM f
-> Range
-> Result ([[a]], String)
minExpTermCond Min f e
mef Sign f e
sign ( \ t1 :: TERM f
t1 t2 :: TERM f
t2 -> TERM f -> TERM f -> Range -> FORMULA f
eq TERM f
t1 TERM f
t2 Range
pos)
          TERM f
term1 TERM f
term2 Range
pos
    String
-> GlobalAnnos
-> FORMULA f
-> [[FORMULA f]]
-> Range
-> Result (FORMULA f)
forall f.
Pretty f =>
String -> GlobalAnnos -> f -> [[f]] -> Range -> Result f
isUnambiguous String
msg (Sign f e -> GlobalAnnos
forall f e. Sign f e -> GlobalAnnos
globAnnos Sign f e
sign) (TERM f -> TERM f -> Range -> FORMULA f
eq TERM f
term1 TERM f
term2 Range
pos) [[FORMULA f]]
ps Range
pos

-- | check if there is at least one solution
hasSolutions :: Pretty f => String -> GlobalAnnos -> f -> [[f]] -> Range
             -> Result [[f]]
hasSolutions :: String -> GlobalAnnos -> f -> [[f]] -> Range -> Result [[f]]
hasSolutions msg :: String
msg ga :: GlobalAnnos
ga topterm :: f
topterm ts :: [[f]]
ts pos :: Range
pos = let terms :: [[f]]
terms = ([f] -> Bool) -> [[f]] -> [[f]]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> ([f] -> Bool) -> [f] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [f] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [[f]]
ts in
   if [[f]] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[f]]
terms then [Diagnosis] -> Maybe [[f]] -> Result [[f]]
forall a. [Diagnosis] -> Maybe a -> Result a
Result
    [DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
Error ("no typing for: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ GlobalAnnos -> f -> String -> String
forall a. Pretty a => GlobalAnnos -> a -> String -> String
showGlobalDoc GlobalAnnos
ga f
topterm "" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
msg)
          Range
pos] Maybe [[f]]
forall a. Maybe a
Nothing
    else [[f]] -> Result [[f]]
forall (m :: * -> *) a. Monad m => a -> m a
return [[f]]
terms

-- | check if there is a unique equivalence class
isUnambiguous :: Pretty f => String -> GlobalAnnos -> f -> [[f]] -> Range
  -> Result f
isUnambiguous :: String -> GlobalAnnos -> f -> [[f]] -> Range -> Result f
isUnambiguous msg :: String
msg ga :: GlobalAnnos
ga topterm :: f
topterm ts :: [[f]]
ts pos :: Range
pos = do
    [[f]]
terms <- String -> GlobalAnnos -> f -> [[f]] -> Range -> Result [[f]]
forall f.
Pretty f =>
String -> GlobalAnnos -> f -> [[f]] -> Range -> Result [[f]]
hasSolutions String
msg GlobalAnnos
ga f
topterm [[f]]
ts Range
pos
    case [[f]]
terms of
        [ term :: f
term : _ ] -> f -> Result f
forall (m :: * -> *) a. Monad m => a -> m a
return f
term
        _ -> [Diagnosis] -> Maybe f -> Result f
forall a. [Diagnosis] -> Maybe a -> Result a
Result [DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
Error ("ambiguous term\n  " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                (String -> String)
-> (f -> String -> String) -> [f] -> String -> String
forall a.
(String -> String)
-> (a -> String -> String) -> [a] -> String -> String
showSepList (String -> String -> String
showString "\n  ") (GlobalAnnos -> f -> String -> String
forall a. Pretty a => GlobalAnnos -> a -> String -> String
showGlobalDoc GlobalAnnos
ga)
                (Int -> [f] -> [f]
forall a. Int -> [a] -> [a]
take 5 ([f] -> [f]) -> [f] -> [f]
forall a b. (a -> b) -> a -> b
$ ([f] -> f) -> [[f]] -> [f]
forall a b. (a -> b) -> [a] -> [b]
map [f] -> f
forall a. [a] -> a
head [[f]]
terms) "") Range
pos] Maybe f
forall a. Maybe a
Nothing

checkIdAndArgs :: Id -> [a] -> Range -> Result Int
checkIdAndArgs :: SORT -> [a] -> Range -> Result Int
checkIdAndArgs ide :: SORT
ide args :: [a]
args poss :: Range
poss =
    let nargs :: Int
nargs = [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
args
        pargs :: Int
pargs = SORT -> Int
placeCount SORT
ide
    in if SORT -> Bool
isMixfix SORT
ide Bool -> Bool -> Bool
&& Int
pargs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
nargs then
    [Diagnosis] -> Maybe Int -> Result Int
forall a. [Diagnosis] -> Maybe a -> Result a
Result [DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
Error
       ("expected " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String -> String
forall a. Show a => a -> String -> String
shows Int
pargs " argument(s) of mixfix identifier '"
         String -> String -> String
forall a. [a] -> [a] -> [a]
++ SORT -> String -> String
forall a. Pretty a => a -> String -> String
showDoc SORT
ide "' but found " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String -> String
forall a. Show a => a -> String -> String
shows Int
nargs " argument(s)")
       Range
poss] Maybe Int
forall a. Maybe a
Nothing
    else Int -> Result Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
nargs

noOpOrPredDiag :: Pretty t => [a] -> DiagKind -> String -> Maybe t -> Id
  -> Range -> Int -> [Diagnosis]
noOpOrPredDiag :: [a]
-> DiagKind
-> String
-> Maybe t
-> SORT
-> Range
-> Int
-> [Diagnosis]
noOpOrPredDiag ops :: [a]
ops k :: DiagKind
k str :: String
str mty :: Maybe t
mty ide :: SORT
ide pos :: Range
pos nargs :: Int
nargs = case [a]
ops of
  [] -> let
    hd :: String
hd = "no " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
str String -> String -> String
forall a. [a] -> [a] -> [a]
++ " with "
    ft :: String
ft = " found for '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ SORT -> String -> String
forall a. Pretty a => a -> String -> String
showDoc SORT
ide "'"
    in [DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
k (case Maybe t
mty of
      Nothing -> String
hd String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String -> String
forall a. Show a => a -> String -> String
shows Int
nargs " argument"
               String -> String -> String
forall a. [a] -> [a] -> [a]
++ (if Int
nargs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 1 then "" else "s") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ft
      Just ty :: t
ty -> String
hd String -> String -> String
forall a. [a] -> [a] -> [a]
++ "profile '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ t -> String -> String
forall a. Pretty a => a -> String -> String
showDoc t
ty "'" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ft) Range
pos]
  _ -> []

noOpOrPred :: Pretty t => [a] -> String -> Maybe t -> Id -> Range -> Int
  -> Result ()
noOpOrPred :: [a] -> String -> Maybe t -> SORT -> Range -> Int -> Result ()
noOpOrPred ops :: [a]
ops str :: String
str mty :: Maybe t
mty ide :: SORT
ide pos :: Range
pos nargs :: Int
nargs = Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
ops) (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> Maybe () -> Result ()
forall a. [Diagnosis] -> Maybe a -> Result a
Result
      ([a]
-> DiagKind
-> String
-> Maybe t
-> SORT
-> Range
-> Int
-> [Diagnosis]
forall t a.
Pretty t =>
[a]
-> DiagKind
-> String
-> Maybe t
-> SORT
-> Range
-> Int
-> [Diagnosis]
noOpOrPredDiag [a]
ops DiagKind
Error String
str Maybe t
mty SORT
ide Range
pos Int
nargs) Maybe ()
forall a. Maybe a
Nothing

{- ----------------------------------------------------------
    - Minimal expansion of a predication formula -
    see minExpTermAppl
---------------------------------------------------------- -}
minExpFORMULApred :: (FormExtension f, TermExtension f)
  => Min f e -> Sign f e -> Id -> Maybe PredType -> [TERM f] -> Range
    -> Result (FORMULA f)
minExpFORMULApred :: Min f e
-> Sign f e
-> SORT
-> Maybe PredType
-> [TERM f]
-> Range
-> Result (FORMULA f)
minExpFORMULApred mef :: Min f e
mef sign :: Sign f e
sign ide :: SORT
ide mty :: Maybe PredType
mty args :: [TERM f]
args pos :: Range
pos = do
    Int
nargs <- SORT -> [TERM f] -> Range -> Result Int
forall a. SORT -> [a] -> Range -> Result Int
checkIdAndArgs SORT
ide [TERM f]
args Range
pos
    let -- predicates matching that name in the current environment
        preds' :: Set PredType
preds' = (PredType -> Bool) -> Set PredType -> Set PredType
forall a. (a -> Bool) -> Set a -> Set a
Set.filter ((Int
nargs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==) (Int -> Bool) -> (PredType -> Int) -> PredType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SORT] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([SORT] -> Int) -> (PredType -> [SORT]) -> PredType -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredType -> [SORT]
predArgs) (Set PredType -> Set PredType) -> Set PredType -> Set PredType
forall a b. (a -> b) -> a -> b
$
              SORT -> PredMap -> Set PredType
forall a b. Ord a => a -> MapSet a b -> Set b
MapSet.lookup SORT
ide (PredMap -> Set PredType) -> PredMap -> Set PredType
forall a b. (a -> b) -> a -> b
$ Sign f e -> PredMap
forall f e. Sign f e -> PredMap
predMap Sign f e
sign
        preds :: [[PredType]]
preds = case Maybe PredType
mty of
                   Nothing -> ([PredType] -> [PredType]) -> [[PredType]] -> [[PredType]]
forall a b. (a -> b) -> [a] -> [b]
map ((PredType -> [SORT]) -> Sign f e -> [PredType] -> [PredType]
forall a f e. (a -> [SORT]) -> Sign f e -> [a] -> [a]
pSortBy PredType -> [SORT]
predArgs Sign f e
sign)
                              ([[PredType]] -> [[PredType]]) -> [[PredType]] -> [[PredType]]
forall a b. (a -> b) -> a -> b
$ (PredType -> PredType -> Bool) -> Set PredType -> [[PredType]]
forall a. Ord a => (a -> a -> Bool) -> Set a -> [[a]]
Rel.leqClasses (Sign f e -> PredType -> PredType -> Bool
forall f e. Sign f e -> PredType -> PredType -> Bool
leqP' Sign f e
sign) Set PredType
preds'
                   Just ty :: PredType
ty -> [[PredType
ty] | PredType -> Set PredType -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member PredType
ty Set PredType
preds']
        boolAna :: t a -> Result (FORMULA f) -> Result (FORMULA f)
boolAna l :: t a
l cmd :: Result (FORMULA f)
cmd = case Maybe PredType
mty of
          Nothing | t a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null t a
l -> do
            [Diagnosis] -> Result ()
appendDiags ([Diagnosis] -> Result ()) -> [Diagnosis] -> Result ()
forall a b. (a -> b) -> a -> b
$ [[PredType]]
-> DiagKind
-> String
-> Maybe PredType
-> SORT
-> Range
-> Int
-> [Diagnosis]
forall t a.
Pretty t =>
[a]
-> DiagKind
-> String
-> Maybe t
-> SORT
-> Range
-> Int
-> [Diagnosis]
noOpOrPredDiag [[PredType]]
preds DiagKind
Hint
              "matching predicate" Maybe PredType
mty SORT
ide Range
pos Int
nargs
            Min f e -> Sign f e -> FORMULA f -> Result (FORMULA f)
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> FORMULA f -> Result (FORMULA f)
minExpFORMULA Min f e
mef Sign f e
sign (FORMULA f -> Result (FORMULA f))
-> FORMULA f -> Result (FORMULA f)
forall a b. (a -> b) -> a -> b
$ TERM f -> FORMULA f
forall f. TERM f -> FORMULA f
Mixfix_formula
              (TERM f -> FORMULA f) -> TERM f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ OP_SYMB -> [TERM f] -> Range -> TERM f
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application (SORT -> OP_SYMB
Op_name SORT
ide) [TERM f]
args Range
pos
          _ -> Result (FORMULA f)
cmd
    [[PredType]] -> Result (FORMULA f) -> Result (FORMULA f)
forall (t :: * -> *) a.
Foldable t =>
t a -> Result (FORMULA f) -> Result (FORMULA f)
boolAna [[PredType]]
preds (Result (FORMULA f) -> Result (FORMULA f))
-> Result (FORMULA f) -> Result (FORMULA f)
forall a b. (a -> b) -> a -> b
$ do
      [[PredType]]
-> String -> Maybe PredType -> SORT -> Range -> Int -> Result ()
forall t a.
Pretty t =>
[a] -> String -> Maybe t -> SORT -> Range -> Int -> Result ()
noOpOrPred [[PredType]]
preds "predicate" Maybe PredType
mty SORT
ide Range
pos Int
nargs
      [[[TERM f]]]
tts <- (TERM f -> Result [[TERM f]]) -> [TERM f] -> Result [[[TERM f]]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Min f e -> Sign f e -> TERM f -> Result [[TERM f]]
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> TERM f -> Result [[TERM f]]
minExpTerm Min f e
mef Sign f e
sign) [TERM f]
args
      let (goodCombs :: [[(PredType, [TERM f], Maybe Int)]]
goodCombs, msg :: String
msg) = Sign f e
-> Int
-> SORT
-> (PredType -> [SORT])
-> [[PredType]]
-> [[[TERM f]]]
-> ([[(PredType, [TERM f], Maybe Int)]], String)
forall f e a.
TermExtension f =>
Sign f e
-> Int
-> SORT
-> (a -> [SORT])
-> [[a]]
-> [[[TERM f]]]
-> ([[(a, [TERM f], Maybe Int)]], String)
getAllCombs Sign f e
sign Int
nargs SORT
ide PredType -> [SORT]
predArgs [[PredType]]
preds [[[TERM f]]]
tts
          qualForms :: [[FORMULA f]]
qualForms = (SORT -> Range -> (PredType, [TERM f]) -> FORMULA f)
-> SORT
-> Range
-> [[(PredType, [TERM f], Maybe Int)]]
-> [[FORMULA f]]
forall a f b.
(SORT -> Range -> (a, [TERM f]) -> b)
-> SORT -> Range -> [[(a, [TERM f], Maybe Int)]] -> [[b]]
qualifyGFs SORT -> Range -> (PredType, [TERM f]) -> FORMULA f
forall f. SORT -> Range -> (PredType, [TERM f]) -> FORMULA f
qualifyPred SORT
ide Range
pos [[(PredType, [TERM f], Maybe Int)]]
goodCombs
      [[FORMULA f]] -> Result (FORMULA f) -> Result (FORMULA f)
forall (t :: * -> *) a.
Foldable t =>
t a -> Result (FORMULA f) -> Result (FORMULA f)
boolAna [[FORMULA f]]
qualForms
        (Result (FORMULA f) -> Result (FORMULA f))
-> Result (FORMULA f) -> Result (FORMULA f)
forall a b. (a -> b) -> a -> b
$ String
-> GlobalAnnos
-> FORMULA f
-> [[FORMULA f]]
-> Range
-> Result (FORMULA f)
forall f.
Pretty f =>
String -> GlobalAnnos -> f -> [[f]] -> Range -> Result f
isUnambiguous String
msg (Sign f e -> GlobalAnnos
forall f e. Sign f e -> GlobalAnnos
globAnnos Sign f e
sign)
              (PRED_SYMB -> [TERM f] -> Range -> FORMULA f
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication (SORT -> PRED_SYMB
Pred_name SORT
ide) [TERM f]
args Range
pos) [[FORMULA f]]
qualForms Range
pos

showSort :: [SORT] -> String
showSort :: [SORT] -> String
showSort s :: [SORT]
s = case [SORT]
s of
         [ft :: SORT
ft] -> "a term of sort '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ SORT -> String -> String
forall a. Show a => a -> String -> String
shows SORT
ft "' was "
         _ -> "terms of sorts " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [SORT] -> String -> String
forall a. Pretty a => a -> String -> String
showDoc [SORT]
s " were "

missMsg :: Bool -> Int -> Id -> [[SORT]] -> [SORT] -> [SORT] -> String
missMsg :: Bool -> Int -> SORT -> [[SORT]] -> [SORT] -> [SORT] -> String
missMsg singleArg :: Bool
singleArg maxArg :: Int
maxArg ide :: SORT
ide args :: [[SORT]]
args foundTs :: [SORT]
foundTs expectedTs :: [SORT]
expectedTs =
  "\nin the "
  String -> String -> String
forall a. [a] -> [a] -> [a]
++ (if Bool
singleArg then "" else Int -> String
forall a. Show a => a -> String
show (Int
maxArg Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) String -> String -> String
forall a. [a] -> [a] -> [a]
++ ". ")
  String -> String -> String
forall a. [a] -> [a] -> [a]
++ "argument of '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ SORT -> String
forall a. Show a => a -> String
show SORT
ide
  String -> String -> String
forall a. [a] -> [a] -> [a]
++ (if Bool
singleArg then "'\n" else case [[SORT]]
args of
       [arg :: [SORT]
arg] -> " : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PredType -> String -> String
forall a. Pretty a => a -> String -> String
showDoc ([SORT] -> PredType
PredType [SORT]
arg) "'\n"
       _ -> "'\n  with argument sorts " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [PredType] -> String -> String
forall a. Pretty a => a -> String -> String
showDoc (([SORT] -> PredType) -> [[SORT]] -> [PredType]
forall a b. (a -> b) -> [a] -> [b]
map [SORT] -> PredType
PredType [[SORT]]
args) "\n")
  String -> String -> String
forall a. [a] -> [a] -> [a]
++ [SORT] -> String
showSort [SORT]
foundTs String -> String -> String
forall a. [a] -> [a] -> [a]
++ "found but\n"
  String -> String -> String
forall a. [a] -> [a] -> [a]
++ [SORT] -> String
showSort [SORT]
expectedTs String -> String -> String
forall a. [a] -> [a] -> [a]
++ "expected."

getAllCombs :: TermExtension f => Sign f e -> Int -> Id -> (a -> [SORT])
  -> [[a]] -> [[[TERM f]]] -> ([[(a, [TERM f], Maybe Int)]], String)
getAllCombs :: Sign f e
-> Int
-> SORT
-> (a -> [SORT])
-> [[a]]
-> [[[TERM f]]]
-> ([[(a, [TERM f], Maybe Int)]], String)
getAllCombs sign :: Sign f e
sign nargs :: Int
nargs ide :: SORT
ide getArgs :: a -> [SORT]
getArgs fs :: [[a]]
fs expansions :: [[[TERM f]]]
expansions =
      let formCombs :: [[(a, [TERM f], Maybe Int)]]
formCombs = ([[TERM f]] -> [[(a, [TERM f], Maybe Int)]])
-> [[[TERM f]]] -> [[(a, [TERM f], Maybe Int)]]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Sign f e
-> (a -> [SORT])
-> [[a]]
-> [[TERM f]]
-> [[(a, [TERM f], Maybe Int)]]
forall f e a.
TermExtension f =>
Sign f e
-> (a -> [SORT])
-> [[a]]
-> [[TERM f]]
-> [[(a, [TERM f], Maybe Int)]]
getCombs Sign f e
sign a -> [SORT]
getArgs [[a]]
fs ([[TERM f]] -> [[(a, [TERM f], Maybe Int)]])
-> ([[TERM f]] -> [[TERM f]])
-> [[TERM f]]
-> [[(a, [TERM f], Maybe Int)]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[TERM f]] -> [[TERM f]]
forall a. [[a]] -> [[a]]
combine)
            ([[[TERM f]]] -> [[(a, [TERM f], Maybe Int)]])
-> [[[TERM f]]] -> [[(a, [TERM f], Maybe Int)]]
forall a b. (a -> b) -> a -> b
$ [[[TERM f]]] -> [[[TERM f]]]
forall a. [[a]] -> [[a]]
combine [[[TERM f]]]
expansions
          partCombs :: [([(a, [TERM f], Maybe Int)], [(a, [TERM f], Maybe Int)])]
partCombs = ([(a, [TERM f], Maybe Int)]
 -> ([(a, [TERM f], Maybe Int)], [(a, [TERM f], Maybe Int)]))
-> [[(a, [TERM f], Maybe Int)]]
-> [([(a, [TERM f], Maybe Int)], [(a, [TERM f], Maybe Int)])]
forall a b. (a -> b) -> [a] -> [b]
map (((a, [TERM f], Maybe Int) -> Bool)
-> [(a, [TERM f], Maybe Int)]
-> ([(a, [TERM f], Maybe Int)], [(a, [TERM f], Maybe Int)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (((a, [TERM f], Maybe Int) -> Bool)
 -> [(a, [TERM f], Maybe Int)]
 -> ([(a, [TERM f], Maybe Int)], [(a, [TERM f], Maybe Int)]))
-> ((a, [TERM f], Maybe Int) -> Bool)
-> [(a, [TERM f], Maybe Int)]
-> ([(a, [TERM f], Maybe Int)], [(a, [TERM f], Maybe Int)])
forall a b. (a -> b) -> a -> b
$ \ (_, _, m :: Maybe Int
m) -> Maybe Int -> Bool
forall a. Maybe a -> Bool
isNothing Maybe Int
m) [[(a, [TERM f], Maybe Int)]]
formCombs
          (goodCombs :: [[(a, [TERM f], Maybe Int)]]
goodCombs, badCombs :: [[(a, [TERM f], Maybe Int)]]
badCombs) = [([(a, [TERM f], Maybe Int)], [(a, [TERM f], Maybe Int)])]
-> ([[(a, [TERM f], Maybe Int)]], [[(a, [TERM f], Maybe Int)]])
forall a b. [(a, b)] -> ([a], [b])
unzip [([(a, [TERM f], Maybe Int)], [(a, [TERM f], Maybe Int)])]
partCombs
          badCs :: [(a, [TERM f], Maybe Int)]
badCs = [[(a, [TERM f], Maybe Int)]] -> [(a, [TERM f], Maybe Int)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(a, [TERM f], Maybe Int)]]
badCombs
      in if [(a, [TERM f], Maybe Int)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(a, [TERM f], Maybe Int)]
badCs then ([[(a, [TERM f], Maybe Int)]]
goodCombs, "") else let
          maxArg :: Int
maxArg = [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ ((a, [TERM f], Maybe Int) -> Int)
-> [(a, [TERM f], Maybe Int)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (\ (_, _, Just c :: Int
c) -> Int
c) [(a, [TERM f], Maybe Int)]
badCs
          badCs2 :: [(a, [TERM f], Maybe Int)]
badCs2 = ((a, [TERM f], Maybe Int) -> Bool)
-> [(a, [TERM f], Maybe Int)] -> [(a, [TERM f], Maybe Int)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (_, _, Just c :: Int
c) -> Int
maxArg Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
c) [(a, [TERM f], Maybe Int)]
badCs
          args :: [[SORT]]
args = Set [SORT] -> [[SORT]]
forall a. Set a -> [a]
Set.toList (Set [SORT] -> [[SORT]])
-> ([[SORT]] -> Set [SORT]) -> [[SORT]] -> [[SORT]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[SORT]] -> Set [SORT]
forall a. Ord a => [a] -> Set a
Set.fromList
            ([[SORT]] -> [[SORT]]) -> [[SORT]] -> [[SORT]]
forall a b. (a -> b) -> a -> b
$ ((a, [TERM f], Maybe Int) -> [SORT])
-> [(a, [TERM f], Maybe Int)] -> [[SORT]]
forall a b. (a -> b) -> [a] -> [b]
map (\ (a :: a
a, _, _) -> a -> [SORT]
getArgs a
a) [(a, [TERM f], Maybe Int)]
badCs2
          foundTs :: [SORT]
foundTs = Sign f e -> (SORT -> SORT) -> [SORT] -> [SORT]
forall f e a. Sign f e -> (a -> SORT) -> [a] -> [a]
keepMinimals Sign f e
sign SORT -> SORT
forall a. a -> a
id
            ([SORT] -> [SORT]) -> [SORT] -> [SORT]
forall a b. (a -> b) -> a -> b
$ ((a, [TERM f], Maybe Int) -> SORT)
-> [(a, [TERM f], Maybe Int)] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map (\ (_, ts :: [TERM f]
ts, _) -> TERM f -> SORT
forall f. TermExtension f => f -> SORT
sortOfTerm (TERM f -> SORT) -> TERM f -> SORT
forall a b. (a -> b) -> a -> b
$ [TERM f]
ts [TERM f] -> Int -> TERM f
forall a. [a] -> Int -> a
!! Int
maxArg) [(a, [TERM f], Maybe Int)]
badCs2
          expectedTs :: [SORT]
expectedTs = Bool -> Sign f e -> (SORT -> SORT) -> [SORT] -> [SORT]
forall f e a. Bool -> Sign f e -> (a -> SORT) -> [a] -> [a]
keepMinimals1 Bool
False Sign f e
sign SORT -> SORT
forall a. a -> a
id ([SORT] -> [SORT]) -> [SORT] -> [SORT]
forall a b. (a -> b) -> a -> b
$ ([SORT] -> SORT) -> [[SORT]] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map ([SORT] -> Int -> SORT
forall a. [a] -> Int -> a
!! Int
maxArg) [[SORT]]
args
      in ([[(a, [TERM f], Maybe Int)]]
goodCombs, Bool -> Int -> SORT -> [[SORT]] -> [SORT] -> [SORT] -> String
missMsg (Int
nargs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 1) Int
maxArg SORT
ide [[SORT]]
args [SORT]
foundTs [SORT]
expectedTs)

getCombs :: TermExtension f => Sign f e -> (a -> [SORT]) -> [[a]] -> [[TERM f]]
  -> [[(a, [TERM f], Maybe Int)]]
getCombs :: Sign f e
-> (a -> [SORT])
-> [[a]]
-> [[TERM f]]
-> [[(a, [TERM f], Maybe Int)]]
getCombs sign :: Sign f e
sign getArgs :: a -> [SORT]
getArgs = ([[TERM f]] -> [[a]] -> [[(a, [TERM f], Maybe Int)]])
-> [[a]] -> [[TERM f]] -> [[(a, [TERM f], Maybe Int)]]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (([[TERM f]] -> [[a]] -> [[(a, [TERM f], Maybe Int)]])
 -> [[a]] -> [[TERM f]] -> [[(a, [TERM f], Maybe Int)]])
-> ([[TERM f]] -> [[a]] -> [[(a, [TERM f], Maybe Int)]])
-> [[a]]
-> [[TERM f]]
-> [[(a, [TERM f], Maybe Int)]]
forall a b. (a -> b) -> a -> b
$ ([a] -> [(a, [TERM f], Maybe Int)])
-> [[a]] -> [[(a, [TERM f], Maybe Int)]]
forall a b. (a -> b) -> [a] -> [b]
map (([a] -> [(a, [TERM f], Maybe Int)])
 -> [[a]] -> [[(a, [TERM f], Maybe Int)]])
-> ([[TERM f]] -> [a] -> [(a, [TERM f], Maybe Int)])
-> [[TERM f]]
-> [[a]]
-> [[(a, [TERM f], Maybe Int)]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \ cs :: [[TERM f]]
cs fs :: [a]
fs ->
  [ (a
f, [TERM f]
ts, Bool -> [Bool] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
elemIndex Bool
False ([Bool] -> Maybe Int) -> [Bool] -> Maybe Int
forall a b. (a -> b) -> a -> b
$ (SORT -> SORT -> Bool) -> [SORT] -> [SORT] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Sign f e -> SORT -> SORT -> Bool
forall f e. Sign f e -> SORT -> SORT -> Bool
leqSort Sign f e
sign) ((TERM f -> SORT) -> [TERM f] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map TERM f -> SORT
forall f. TermExtension f => f -> SORT
sortOfTerm [TERM f]
ts)
            ([SORT] -> [Bool]) -> [SORT] -> [Bool]
forall a b. (a -> b) -> a -> b
$ a -> [SORT]
getArgs a
f) | a
f <- [a]
fs, [TERM f]
ts <- [[TERM f]]
cs ]

qualifyGFs :: (Id -> Range -> (a, [TERM f]) -> b) -> Id -> Range
  -> [[(a, [TERM f], Maybe Int)]] -> [[b]]
qualifyGFs :: (SORT -> Range -> (a, [TERM f]) -> b)
-> SORT -> Range -> [[(a, [TERM f], Maybe Int)]] -> [[b]]
qualifyGFs f :: SORT -> Range -> (a, [TERM f]) -> b
f ide :: SORT
ide pos :: Range
pos = ([(a, [TERM f], Maybe Int)] -> [b])
-> [[(a, [TERM f], Maybe Int)]] -> [[b]]
forall a b. (a -> b) -> [a] -> [b]
map (([(a, [TERM f], Maybe Int)] -> [b])
 -> [[(a, [TERM f], Maybe Int)]] -> [[b]])
-> ([(a, [TERM f], Maybe Int)] -> [b])
-> [[(a, [TERM f], Maybe Int)]]
-> [[b]]
forall a b. (a -> b) -> a -> b
$ ((a, [TERM f], Maybe Int) -> b)
-> [(a, [TERM f], Maybe Int)] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map (SORT -> Range -> (a, [TERM f]) -> b
f SORT
ide Range
pos ((a, [TERM f]) -> b)
-> ((a, [TERM f], Maybe Int) -> (a, [TERM f]))
-> (a, [TERM f], Maybe Int)
-> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \ (a :: a
a, b :: [TERM f]
b, _) -> (a
a, [TERM f]
b))

-- | qualify a single pred, given by its signature and its arguments
qualifyPred :: Id -> Range -> (PredType, [TERM f]) -> FORMULA f
qualifyPred :: SORT -> Range -> (PredType, [TERM f]) -> FORMULA f
qualifyPred ide :: SORT
ide pos :: Range
pos (pred' :: PredType
pred', terms' :: [TERM f]
terms') =
    PRED_SYMB -> [TERM f] -> Range -> FORMULA f
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication (SORT -> PRED_TYPE -> Range -> PRED_SYMB
Qual_pred_name SORT
ide (PredType -> PRED_TYPE
toPRED_TYPE PredType
pred') Range
pos) [TERM f]
terms' Range
pos

-- | expansions of an equation formula or a conditional
minExpTermEq :: (FormExtension f, TermExtension f)
  => Min f e -> Sign f e -> TERM f -> TERM f -> Result [[(TERM f, TERM f)]]
minExpTermEq :: Min f e
-> Sign f e -> TERM f -> TERM f -> Result [[(TERM f, TERM f)]]
minExpTermEq mef :: Min f e
mef sign :: Sign f e
sign term1 :: TERM f
term1 term2 :: TERM f
term2 = do
    [[TERM f]]
exps1 <- Min f e -> Sign f e -> TERM f -> Result [[TERM f]]
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> TERM f -> Result [[TERM f]]
minExpTerm Min f e
mef Sign f e
sign TERM f
term1
    [[TERM f]]
exps2 <- Min f e -> Sign f e -> TERM f -> Result [[TERM f]]
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> TERM f -> Result [[TERM f]]
minExpTerm Min f e
mef Sign f e
sign TERM f
term2
    [[(TERM f, TERM f)]] -> Result [[(TERM f, TERM f)]]
forall (m :: * -> *) a. Monad m => a -> m a
return ([[(TERM f, TERM f)]] -> Result [[(TERM f, TERM f)]])
-> [[(TERM f, TERM f)]] -> Result [[(TERM f, TERM f)]]
forall a b. (a -> b) -> a -> b
$ ([[TERM f]] -> [(TERM f, TERM f)])
-> [[[TERM f]]] -> [[(TERM f, TERM f)]]
forall a b. (a -> b) -> [a] -> [b]
map (Sign f e -> [(TERM f, TERM f)] -> [(TERM f, TERM f)]
forall f e.
TermExtension f =>
Sign f e -> [(TERM f, TERM f)] -> [(TERM f, TERM f)]
minimizeEq Sign f e
sign ([(TERM f, TERM f)] -> [(TERM f, TERM f)])
-> ([[TERM f]] -> [(TERM f, TERM f)])
-> [[TERM f]]
-> [(TERM f, TERM f)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[TERM f]] -> [(TERM f, TERM f)]
forall f. [[TERM f]] -> [(TERM f, TERM f)]
getPairs) ([[[TERM f]]] -> [[(TERM f, TERM f)]])
-> [[[TERM f]]] -> [[(TERM f, TERM f)]]
forall a b. (a -> b) -> a -> b
$ [[[TERM f]]] -> [[[TERM f]]]
forall a. [[a]] -> [[a]]
combine [[[TERM f]]
exps1, [[TERM f]]
exps2]

getPairs :: [[TERM f]] -> [(TERM f, TERM f)]
getPairs :: [[TERM f]] -> [(TERM f, TERM f)]
getPairs cs :: [[TERM f]]
cs = [ (TERM f
t1, TERM f
t2) | [t1 :: TERM f
t1, t2 :: TERM f
t2] <- [[TERM f]] -> [[TERM f]]
forall a. [[a]] -> [[a]]
combine [[TERM f]]
cs ]

minimizeEq :: TermExtension f => Sign f e -> [(TERM f, TERM f)]
           -> [(TERM f, TERM f)]
minimizeEq :: Sign f e -> [(TERM f, TERM f)] -> [(TERM f, TERM f)]
minimizeEq s :: Sign f e
s = Sign f e
-> ((TERM f, TERM f) -> SORT)
-> [(TERM f, TERM f)]
-> [(TERM f, TERM f)]
forall f e a. Sign f e -> (a -> SORT) -> [a] -> [a]
keepMinimals Sign f e
s (TERM f -> SORT
forall f. TermExtension f => f -> SORT
sortOfTerm (TERM f -> SORT)
-> ((TERM f, TERM f) -> TERM f) -> (TERM f, TERM f) -> SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TERM f, TERM f) -> TERM f
forall a b. (a, b) -> b
snd)
  ([(TERM f, TERM f)] -> [(TERM f, TERM f)])
-> ([(TERM f, TERM f)] -> [(TERM f, TERM f)])
-> [(TERM f, TERM f)]
-> [(TERM f, TERM f)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign f e
-> ((TERM f, TERM f) -> SORT)
-> [(TERM f, TERM f)]
-> [(TERM f, TERM f)]
forall f e a. Sign f e -> (a -> SORT) -> [a] -> [a]
keepMinimals Sign f e
s (TERM f -> SORT
forall f. TermExtension f => f -> SORT
sortOfTerm (TERM f -> SORT)
-> ((TERM f, TERM f) -> TERM f) -> (TERM f, TERM f) -> SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TERM f, TERM f) -> TERM f
forall a b. (a, b) -> a
fst)

{- ----------------------------------------------------------
    - Minimal expansion of a term -
  Expand a given term by typing information.
  * 'Qual_var' terms are handled by 'minExpTerm_var'
  * 'Application' terms are handled by 'minExpTermOp'.
  * 'Conditional' terms are handled by 'minExpTermCond'.
---------------------------------------------------------- -}
minExpTerm :: (FormExtension f, TermExtension f)
  => Min f e -> Sign f e -> TERM f -> Result [[TERM f]]
minExpTerm :: Min f e -> Sign f e -> TERM f -> Result [[TERM f]]
minExpTerm mef :: Min f e
mef sign :: Sign f e
sign top :: TERM f
top = let ga :: GlobalAnnos
ga = Sign f e -> GlobalAnnos
forall f e. Sign f e -> GlobalAnnos
globAnnos Sign f e
sign in case TERM f
top of
    Qual_var var :: VAR
var srt :: SORT
srt _ -> let ts :: [[TERM f]]
ts = Sign f e -> VAR -> Maybe SORT -> [[TERM f]]
forall f e. Sign f e -> VAR -> Maybe SORT -> [[TERM f]]
minExpTermVar Sign f e
sign VAR
var (SORT -> Maybe SORT
forall a. a -> Maybe a
Just SORT
srt) in
        if [[TERM f]] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[TERM f]]
ts then String -> VAR -> Result [[TERM f]]
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "no matching qualified variable found" VAR
var
        else [[TERM f]] -> Result [[TERM f]]
forall (m :: * -> *) a. Monad m => a -> m a
return [[TERM f]]
ts
    Application op :: OP_SYMB
op terms :: [TERM f]
terms pos :: Range
pos -> Min f e
-> Sign f e -> OP_SYMB -> [TERM f] -> Range -> Result [[TERM f]]
forall f e.
(FormExtension f, TermExtension f) =>
Min f e
-> Sign f e -> OP_SYMB -> [TERM f] -> Range -> Result [[TERM f]]
minExpTermOp Min f e
mef Sign f e
sign OP_SYMB
op [TERM f]
terms Range
pos
    Sorted_term term :: TERM f
term srt :: SORT
srt pos :: Range
pos -> do
      [[TERM f]]
expandedTerm <- Min f e -> Sign f e -> TERM f -> Result [[TERM f]]
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> TERM f -> Result [[TERM f]]
minExpTerm Min f e
mef Sign f e
sign TERM f
term
      -- choose expansions that fit the given signature, then qualify
      let validExps :: [[TERM f]]
validExps =
              ([TERM f] -> [TERM f]) -> [[TERM f]] -> [[TERM f]]
forall a b. (a -> b) -> [a] -> [b]
map ((TERM f -> Bool) -> [TERM f] -> [TERM f]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> (SORT -> Bool) -> Maybe SORT -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True ((SORT -> SORT -> Bool) -> SORT -> SORT -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Sign f e -> SORT -> SORT -> Bool
forall f e. Sign f e -> SORT -> SORT -> Bool
leqSort Sign f e
sign) SORT
srt)
                                   (Maybe SORT -> Bool) -> (TERM f -> Maybe SORT) -> TERM f -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TERM f -> Maybe SORT
forall f. TermExtension f => f -> Maybe SORT
optTermSort))
                      [[TERM f]]
expandedTerm
          msg :: String
msg = Bool -> Sign f e -> SORT -> [[TERM f]] -> String
forall f e.
TermExtension f =>
Bool -> Sign f e -> SORT -> [[TERM f]] -> String
superSortError Bool
False Sign f e
sign SORT
srt [[TERM f]]
expandedTerm
      String
-> GlobalAnnos
-> TERM f
-> [[TERM f]]
-> Range
-> Result [[TERM f]]
forall f.
Pretty f =>
String -> GlobalAnnos -> f -> [[f]] -> Range -> Result [[f]]
hasSolutions String
msg GlobalAnnos
ga TERM f
top (([TERM f] -> [TERM f]) -> [[TERM f]] -> [[TERM f]]
forall a b. (a -> b) -> [a] -> [b]
map ((TERM f -> TERM f) -> [TERM f] -> [TERM f]
forall a b. (a -> b) -> [a] -> [b]
map (\ t :: TERM f
t ->
                 TERM f -> SORT -> Range -> TERM f
forall f. TERM f -> SORT -> Range -> TERM f
Sorted_term TERM f
t SORT
srt Range
pos)) [[TERM f]]
validExps) Range
pos
    Cast term :: TERM f
term srt :: SORT
srt pos :: Range
pos -> do
      [[TERM f]]
expandedTerm <- Min f e -> Sign f e -> TERM f -> Result [[TERM f]]
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> TERM f -> Result [[TERM f]]
minExpTerm Min f e
mef Sign f e
sign TERM f
term
      -- find a unique minimal common supersort
      let ts :: [[TERM f]]
ts = ([TERM f] -> [TERM f]) -> [[TERM f]] -> [[TERM f]]
forall a b. (a -> b) -> [a] -> [b]
map ((TERM f -> [TERM f]) -> [TERM f] -> [TERM f]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ t :: TERM f
t ->
                    (SORT -> TERM f) -> [SORT] -> [TERM f]
forall a b. (a -> b) -> [a] -> [b]
map ( \ c :: SORT
c ->
                        TERM f -> SORT -> Range -> TERM f
forall f. TERM f -> SORT -> Range -> TERM f
Cast (Sign f e -> TERM f -> SORT -> Range -> TERM f
forall f e.
TermExtension f =>
Sign f e -> TERM f -> SORT -> Range -> TERM f
mkSorted Sign f e
sign TERM f
t SORT
c Range
pos) SORT
srt Range
pos)
                    ([SORT] -> [TERM f]) -> [SORT] -> [TERM f]
forall a b. (a -> b) -> a -> b
$ [SORT] -> (SORT -> [SORT]) -> Maybe SORT -> [SORT]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [SORT
srt] (Sign f e -> SORT -> SORT -> [SORT]
forall f e. Sign f e -> SORT -> SORT -> [SORT]
minimalSupers Sign f e
sign SORT
srt)
                    (Maybe SORT -> [SORT]) -> Maybe SORT -> [SORT]
forall a b. (a -> b) -> a -> b
$ TERM f -> Maybe SORT
forall f. TermExtension f => f -> Maybe SORT
optTermSort TERM f
t)) [[TERM f]]
expandedTerm
          msg :: String
msg = Bool -> Sign f e -> SORT -> [[TERM f]] -> String
forall f e.
TermExtension f =>
Bool -> Sign f e -> SORT -> [[TERM f]] -> String
superSortError Bool
True Sign f e
sign SORT
srt [[TERM f]]
expandedTerm
      String
-> GlobalAnnos
-> TERM f
-> [[TERM f]]
-> Range
-> Result [[TERM f]]
forall f.
Pretty f =>
String -> GlobalAnnos -> f -> [[f]] -> Range -> Result [[f]]
hasSolutions String
msg GlobalAnnos
ga TERM f
top [[TERM f]]
ts Range
pos
    Conditional term1 :: TERM f
term1 formula :: FORMULA f
formula term2 :: TERM f
term2 pos :: Range
pos -> do
      FORMULA f
f <- Min f e -> Sign f e -> FORMULA f -> Result (FORMULA f)
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> FORMULA f -> Result (FORMULA f)
minExpFORMULA Min f e
mef Sign f e
sign FORMULA f
formula
      (ts :: [[TERM f]]
ts, msg :: String
msg) <- Min f e
-> Sign f e
-> (TERM f -> TERM f -> TERM f)
-> TERM f
-> TERM f
-> Range
-> Result ([[TERM f]], String)
forall f e a.
(FormExtension f, TermExtension f) =>
Min f e
-> Sign f e
-> (TERM f -> TERM f -> a)
-> TERM f
-> TERM f
-> Range
-> Result ([[a]], String)
minExpTermCond Min f e
mef Sign f e
sign ( \ t1 :: TERM f
t1 t2 :: TERM f
t2 -> TERM f -> FORMULA f -> TERM f -> Range -> TERM f
forall f. TERM f -> FORMULA f -> TERM f -> Range -> TERM f
Conditional TERM f
t1 FORMULA f
f TERM f
t2 Range
pos)
            TERM f
term1 TERM f
term2 Range
pos
      String
-> GlobalAnnos
-> TERM f
-> [[TERM f]]
-> Range
-> Result [[TERM f]]
forall f.
Pretty f =>
String -> GlobalAnnos -> f -> [[f]] -> Range -> Result [[f]]
hasSolutions String
msg GlobalAnnos
ga (TERM f -> FORMULA f -> TERM f -> Range -> TERM f
forall f. TERM f -> FORMULA f -> TERM f -> Range -> TERM f
Conditional TERM f
term1 FORMULA f
formula TERM f
term2 Range
pos) [[TERM f]]
ts Range
pos
    ExtTERM t :: f
t -> do
      f
nt <- Min f e
mef Sign f e
sign f
t
      [[TERM f]] -> Result [[TERM f]]
forall (m :: * -> *) a. Monad m => a -> m a
return [[f -> TERM f
forall f. f -> TERM f
ExtTERM f
nt]]
    _ -> String -> TERM f -> Result [[TERM f]]
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "unexpected kind of term" TERM f
top

-- | Minimal expansion of a possibly qualified variable identifier
minExpTermVar :: Sign f e -> Token -> Maybe SORT -> [[TERM f]]
minExpTermVar :: Sign f e -> VAR -> Maybe SORT -> [[TERM f]]
minExpTermVar sign :: Sign f e
sign tok :: VAR
tok ms :: Maybe SORT
ms = case VAR -> Map VAR SORT -> Maybe SORT
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup VAR
tok (Map VAR SORT -> Maybe SORT) -> Map VAR SORT -> Maybe SORT
forall a b. (a -> b) -> a -> b
$ Sign f e -> Map VAR SORT
forall f e. Sign f e -> Map VAR SORT
varMap Sign f e
sign of
    Nothing -> []
    Just s :: SORT
s -> let qv :: [[TERM f]]
qv = [[VAR -> SORT -> Range -> TERM f
forall f. VAR -> SORT -> Range -> TERM f
Qual_var VAR
tok SORT
s Range
nullRange]] in
              case Maybe SORT
ms of
              Nothing -> [[TERM f]]
forall f. [[TERM f]]
qv
              Just s2 :: SORT
s2 -> if SORT
s SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
s2 then [[TERM f]]
forall f. [[TERM f]]
qv else []

-- | minimal expansion of an (possibly qualified) operator application
minExpTermAppl :: (FormExtension f, TermExtension f)
  => Min f e -> Sign f e -> Id -> Maybe OpType -> [TERM f] -> Range
    -> Result [[TERM f]]
minExpTermAppl :: Min f e
-> Sign f e
-> SORT
-> Maybe OpType
-> [TERM f]
-> Range
-> Result [[TERM f]]
minExpTermAppl mef :: Min f e
mef sign :: Sign f e
sign ide :: SORT
ide mty :: Maybe OpType
mty args :: [TERM f]
args pos :: Range
pos = do
    Int
nargs <- SORT -> [TERM f] -> Range -> Result Int
forall a. SORT -> [a] -> Range -> Result Int
checkIdAndArgs SORT
ide [TERM f]
args Range
pos
    let -- functions matching that name in the current environment
        ops' :: Set OpType
ops' = (OpType -> Bool) -> Set OpType -> Set OpType
forall a. (a -> Bool) -> Set a -> Set a
Set.filter ( \ o :: OpType
o -> [SORT] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (OpType -> [SORT]
opArgs OpType
o) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
nargs) (Set OpType -> Set OpType) -> Set OpType -> Set OpType
forall a b. (a -> b) -> a -> b
$
              SORT -> OpMap -> Set OpType
forall a b. Ord a => a -> MapSet a b -> Set b
MapSet.lookup SORT
ide (OpMap -> Set OpType) -> OpMap -> Set OpType
forall a b. (a -> b) -> a -> b
$ Sign f e -> OpMap
forall f e. Sign f e -> OpMap
opMap Sign f e
sign
        ops :: [[OpType]]
ops = case Maybe OpType
mty of
                   Nothing -> ([OpType] -> [OpType]) -> [[OpType]] -> [[OpType]]
forall a b. (a -> b) -> [a] -> [b]
map ((OpType -> [SORT]) -> Sign f e -> [OpType] -> [OpType]
forall a f e. (a -> [SORT]) -> Sign f e -> [a] -> [a]
pSortBy OpType -> [SORT]
opArgs Sign f e
sign)
                              ([[OpType]] -> [[OpType]]) -> [[OpType]] -> [[OpType]]
forall a b. (a -> b) -> a -> b
$ (OpType -> OpType -> Bool) -> Set OpType -> [[OpType]]
forall a. Ord a => (a -> a -> Bool) -> Set a -> [[a]]
Rel.leqClasses (Sign f e -> OpType -> OpType -> Bool
forall f e. Sign f e -> OpType -> OpType -> Bool
leqF' Sign f e
sign) Set OpType
ops'
                   Just ty :: OpType
ty -> [[OpType
ty] | OpType -> Set OpType -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member OpType
ty Set OpType
ops' Bool -> Bool -> Bool
||
                                  -- might be known to be total
                                 OpType -> Set OpType -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (OpType -> OpType
mkTotal OpType
ty) Set OpType
ops' ]
    [[OpType]]
-> String -> Maybe OpType -> SORT -> Range -> Int -> Result ()
forall t a.
Pretty t =>
[a] -> String -> Maybe t -> SORT -> Range -> Int -> Result ()
noOpOrPred [[OpType]]
ops "operation" Maybe OpType
mty SORT
ide Range
pos Int
nargs
    [[[TERM f]]]
expansions <- (TERM f -> Result [[TERM f]]) -> [TERM f] -> Result [[[TERM f]]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Min f e -> Sign f e -> TERM f -> Result [[TERM f]]
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> TERM f -> Result [[TERM f]]
minExpTerm Min f e
mef Sign f e
sign) [TERM f]
args
    let  -- generate profiles as descr. on p. 339 (Step 3)
        (goodCombs :: [[(OpType, [TERM f], Maybe Int)]]
goodCombs, msg :: String
msg) = Sign f e
-> Int
-> SORT
-> (OpType -> [SORT])
-> [[OpType]]
-> [[[TERM f]]]
-> ([[(OpType, [TERM f], Maybe Int)]], String)
forall f e a.
TermExtension f =>
Sign f e
-> Int
-> SORT
-> (a -> [SORT])
-> [[a]]
-> [[[TERM f]]]
-> ([[(a, [TERM f], Maybe Int)]], String)
getAllCombs Sign f e
sign Int
nargs SORT
ide OpType -> [SORT]
opArgs [[OpType]]
ops [[[TERM f]]]
expansions
        qualTerms :: [[TERM f]]
qualTerms = (SORT -> Range -> (OpType, [TERM f]) -> TERM f)
-> SORT -> Range -> [[(OpType, [TERM f], Maybe Int)]] -> [[TERM f]]
forall a f b.
(SORT -> Range -> (a, [TERM f]) -> b)
-> SORT -> Range -> [[(a, [TERM f], Maybe Int)]] -> [[b]]
qualifyGFs SORT -> Range -> (OpType, [TERM f]) -> TERM f
forall f. SORT -> Range -> (OpType, [TERM f]) -> TERM f
qualifyOp SORT
ide Range
pos
                    ([[(OpType, [TERM f], Maybe Int)]] -> [[TERM f]])
-> [[(OpType, [TERM f], Maybe Int)]] -> [[TERM f]]
forall a b. (a -> b) -> a -> b
$ ([(OpType, [TERM f], Maybe Int)]
 -> [(OpType, [TERM f], Maybe Int)])
-> [[(OpType, [TERM f], Maybe Int)]]
-> [[(OpType, [TERM f], Maybe Int)]]
forall a b. (a -> b) -> [a] -> [b]
map (Sign f e
-> [(OpType, [TERM f], Maybe Int)]
-> [(OpType, [TERM f], Maybe Int)]
forall f e a.
Sign f e -> [(OpType, [TERM f], a)] -> [(OpType, [TERM f], a)]
minimizeOp Sign f e
sign) [[(OpType, [TERM f], Maybe Int)]]
goodCombs
    String
-> GlobalAnnos
-> TERM f
-> [[TERM f]]
-> Range
-> Result [[TERM f]]
forall f.
Pretty f =>
String -> GlobalAnnos -> f -> [[f]] -> Range -> Result [[f]]
hasSolutions String
msg (Sign f e -> GlobalAnnos
forall f e. Sign f e -> GlobalAnnos
globAnnos Sign f e
sign)
        (OP_SYMB -> [TERM f] -> Range -> TERM f
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application (SORT -> OP_SYMB
Op_name SORT
ide) [TERM f]
args Range
pos) [[TERM f]]
qualTerms Range
pos

    -- qualify a single op, given by its signature and its arguments
qualifyOp :: Id -> Range -> (OpType, [TERM f]) -> TERM f
qualifyOp :: SORT -> Range -> (OpType, [TERM f]) -> TERM f
qualifyOp ide :: SORT
ide pos :: Range
pos (op' :: OpType
op', terms' :: [TERM f]
terms') =
    OP_SYMB -> [TERM f] -> Range -> TERM f
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application (SORT -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name SORT
ide (OpType -> OP_TYPE
toOP_TYPE OpType
op') Range
pos) [TERM f]
terms' Range
pos

{- ----------------------------------------------------------
    - Minimal expansion of a function application or a variable -
  Expand a function application by typing information.
  1. First expand all argument subterms.
  2. Combine these expansions so we compute the set of tuples
    { (C_1, ..., C_n) | (C_1, ..., C_n) \in
                        minExpTerm(t_1) x ... x minExpTerm(t_n) }
    where t_1, ..., t_n are the given argument terms.
  3. For each element of this set compute the set of possible profiles
    (as described on p. 339).
  4. Define an equivalence relation ~ on these profiles
    (as described on p. 339).
  5. Separate each profile into equivalence classes by the relation ~
    and take the unification of these sets.
  6. Minimize each element of this unified set (as described on p. 339).
  7. Transform each term in the minimized set into a qualified function
    application term.
---------------------------------------------------------- -}
minExpTermOp :: (FormExtension f, TermExtension f)
  => Min f e -> Sign f e -> OP_SYMB -> [TERM f] -> Range -> Result [[TERM f]]
minExpTermOp :: Min f e
-> Sign f e -> OP_SYMB -> [TERM f] -> Range -> Result [[TERM f]]
minExpTermOp mef :: Min f e
mef sign :: Sign f e
sign osym :: OP_SYMB
osym args :: [TERM f]
args pos :: Range
pos = case OP_SYMB
osym of
  Op_name ide :: SORT
ide@(Id ts :: [VAR]
ts _ _) ->
    let res :: Result [[TERM f]]
res = Min f e
-> Sign f e
-> SORT
-> Maybe OpType
-> [TERM f]
-> Range
-> Result [[TERM f]]
forall f e.
(FormExtension f, TermExtension f) =>
Min f e
-> Sign f e
-> SORT
-> Maybe OpType
-> [TERM f]
-> Range
-> Result [[TERM f]]
minExpTermAppl Min f e
mef Sign f e
sign SORT
ide Maybe OpType
forall a. Maybe a
Nothing [TERM f]
args Range
pos in
      if [TERM f] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TERM f]
args Bool -> Bool -> Bool
&& SORT -> Bool
isSimpleId SORT
ide then
          let vars :: [[TERM f]]
vars = Sign f e -> VAR -> Maybe SORT -> [[TERM f]]
forall f e. Sign f e -> VAR -> Maybe SORT -> [[TERM f]]
minExpTermVar Sign f e
sign ([VAR] -> VAR
forall a. [a] -> a
head [VAR]
ts) Maybe SORT
forall a. Maybe a
Nothing
          in if [[TERM f]] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[TERM f]]
vars then Result [[TERM f]]
res else
             case Result [[TERM f]] -> Maybe [[TERM f]]
forall a. Result a -> Maybe a
maybeResult Result [[TERM f]]
res of
             Nothing -> [[TERM f]] -> Result [[TERM f]]
forall (m :: * -> *) a. Monad m => a -> m a
return [[TERM f]]
vars
             Just ops :: [[TERM f]]
ops -> [[TERM f]] -> Result [[TERM f]]
forall (m :: * -> *) a. Monad m => a -> m a
return ([[TERM f]] -> Result [[TERM f]])
-> [[TERM f]] -> Result [[TERM f]]
forall a b. (a -> b) -> a -> b
$ [[TERM f]]
ops [[TERM f]] -> [[TERM f]] -> [[TERM f]]
forall a. [a] -> [a] -> [a]
++ [[TERM f]]
vars
      else Result [[TERM f]]
res
  Qual_op_name ide :: SORT
ide ty :: OP_TYPE
ty pos1 :: Range
pos1 ->
   if [TERM f] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TERM f]
args Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [SORT] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (OP_TYPE -> [SORT]
args_OP_TYPE OP_TYPE
ty) then
      String -> SORT -> Result [[TERM f]]
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "type qualification does not match number of arguments" SORT
ide
   else Min f e
-> Sign f e
-> SORT
-> Maybe OpType
-> [TERM f]
-> Range
-> Result [[TERM f]]
forall f e.
(FormExtension f, TermExtension f) =>
Min f e
-> Sign f e
-> SORT
-> Maybe OpType
-> [TERM f]
-> Range
-> Result [[TERM f]]
minExpTermAppl Min f e
mef Sign f e
sign SORT
ide (OpType -> Maybe OpType
forall a. a -> Maybe a
Just (OpType -> Maybe OpType) -> OpType -> Maybe OpType
forall a b. (a -> b) -> a -> b
$ OP_TYPE -> OpType
toOpType OP_TYPE
ty) [TERM f]
args
        (Range
pos1 Range -> Range -> Range
`appRange` Range
pos)

{- ----------------------------------------------------------
    - Minimal expansion of a conditional -
  Expand a conditional by typing information (see minExpTermEq)
  First expand the subterms and subformula. Then calculate a profile
  P(C_1, C_2) for each (C_1, C_2) \in minExpTerm(t1) x minExpTerm(t_2).
  Separate these profiles into equivalence classes and take the
  unification of all these classes. Minimize each equivalence class.
  Finally transform the eq. classes into lists of
  conditionals with equally sorted terms.
---------------------------------------------------------- -}
minExpTermCond :: (FormExtension f, TermExtension f)
  => Min f e -> Sign f e -> (TERM f -> TERM f -> a) -> TERM f -> TERM f
    -> Range -> Result ([[a]], String)
minExpTermCond :: Min f e
-> Sign f e
-> (TERM f -> TERM f -> a)
-> TERM f
-> TERM f
-> Range
-> Result ([[a]], String)
minExpTermCond mef :: Min f e
mef sign :: Sign f e
sign f :: TERM f -> TERM f -> a
f term1 :: TERM f
term1 term2 :: TERM f
term2 pos :: Range
pos = do
    [[(TERM f, TERM f)]]
pairs <- Min f e
-> Sign f e -> TERM f -> TERM f -> Result [[(TERM f, TERM f)]]
forall f e.
(FormExtension f, TermExtension f) =>
Min f e
-> Sign f e -> TERM f -> TERM f -> Result [[(TERM f, TERM f)]]
minExpTermEq Min f e
mef Sign f e
sign TERM f
term1 TERM f
term2
    let (lhs :: [TERM f]
lhs, rhs :: [TERM f]
rhs) = [(TERM f, TERM f)] -> ([TERM f], [TERM f])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(TERM f, TERM f)] -> ([TERM f], [TERM f]))
-> [(TERM f, TERM f)] -> ([TERM f], [TERM f])
forall a b. (a -> b) -> a -> b
$ [[(TERM f, TERM f)]] -> [(TERM f, TERM f)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(TERM f, TERM f)]]
pairs
        mins :: [TERM f] -> [SORT]
mins = Sign f e -> (SORT -> SORT) -> [SORT] -> [SORT]
forall f e a. Sign f e -> (a -> SORT) -> [a] -> [a]
keepMinimals Sign f e
sign SORT -> SORT
forall a. a -> a
id ([SORT] -> [SORT]) -> ([TERM f] -> [SORT]) -> [TERM f] -> [SORT]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TERM f -> SORT) -> [TERM f] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map TERM f -> SORT
forall f. TermExtension f => f -> SORT
sortOfTerm
        ds :: String
ds = "\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [SORT] -> String
showSort ([TERM f] -> [SORT]
mins [TERM f]
lhs) String -> String -> String
forall a. [a] -> [a] -> [a]
++ "on the lhs but\n"
          String -> String -> String
forall a. [a] -> [a] -> [a]
++ [SORT] -> String
showSort ([TERM f] -> [SORT]
mins [TERM f]
rhs) String -> String -> String
forall a. [a] -> [a] -> [a]
++ "on the rhs."
    ([[a]], String) -> Result ([[a]], String)
forall (m :: * -> *) a. Monad m => a -> m a
return (([(TERM f, TERM f)] -> [a]) -> [[(TERM f, TERM f)]] -> [[a]]
forall a b. (a -> b) -> [a] -> [b]
map (((TERM f, TERM f) -> [a]) -> [(TERM f, TERM f)] -> [a]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ( \ (t1 :: TERM f
t1, t2 :: TERM f
t2) ->
              let s1 :: SORT
s1 = TERM f -> SORT
forall f. TermExtension f => f -> SORT
sortOfTerm TERM f
t1
                  s2 :: SORT
s2 = TERM f -> SORT
forall f. TermExtension f => f -> SORT
sortOfTerm TERM f
t2
              in (SORT -> a) -> [SORT] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map ( \ s :: SORT
s -> TERM f -> TERM f -> a
f (Sign f e -> TERM f -> SORT -> Range -> TERM f
forall f e.
TermExtension f =>
Sign f e -> TERM f -> SORT -> Range -> TERM f
mkSorted Sign f e
sign TERM f
t1 SORT
s Range
pos)
                                (Sign f e -> TERM f -> SORT -> Range -> TERM f
forall f e.
TermExtension f =>
Sign f e -> TERM f -> SORT -> Range -> TERM f
mkSorted Sign f e
sign TERM f
t2 SORT
s Range
pos))
                   ([SORT] -> [a]) -> [SORT] -> [a]
forall a b. (a -> b) -> a -> b
$ Sign f e -> SORT -> SORT -> [SORT]
forall f e. Sign f e -> SORT -> SORT -> [SORT]
minimalSupers Sign f e
sign SORT
s1 SORT
s2)) [[(TERM f, TERM f)]]
pairs, String
ds)

{- ----------------------------------------------------------
    Let P be a set of equivalence classes of qualified terms.
    For each C \in P, let C' choose _one_
    t:s \in C for each s minimal such that t:s \in C.
    That is, discard all terms whose sort is a supersort of
    any other term in the same equivalence class.
---------------------------------------------------------- -}
minimizeOp :: Sign f e -> [(OpType, [TERM f], a)] -> [(OpType, [TERM f], a)]
minimizeOp :: Sign f e -> [(OpType, [TERM f], a)] -> [(OpType, [TERM f], a)]
minimizeOp sign :: Sign f e
sign = Sign f e
-> ((OpType, [TERM f], a) -> SORT)
-> [(OpType, [TERM f], a)]
-> [(OpType, [TERM f], a)]
forall f e a. Sign f e -> (a -> SORT) -> [a] -> [a]
keepMinimals Sign f e
sign (OpType -> SORT
opRes (OpType -> SORT)
-> ((OpType, [TERM f], a) -> OpType)
-> (OpType, [TERM f], a)
-> SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \ (a :: OpType
a, _, _) -> OpType
a)

-- | the (possibly incomplete) list of supersorts common to both sorts
commonSupersorts :: Bool -> Sign f e -> SORT -> SORT -> [SORT]
commonSupersorts :: Bool -> Sign f e -> SORT -> SORT -> [SORT]
commonSupersorts b :: Bool
b sign :: Sign f e
sign s1 :: SORT
s1 s2 :: SORT
s2 =
    if SORT
s1 SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
s2 then [SORT
s1] else
    let l1 :: Set SORT
l1 = SORT -> Sign f e -> Set SORT
forall f e. SORT -> Sign f e -> Set SORT
supersortsOf SORT
s1 Sign f e
sign
        l2 :: Set SORT
l2 = SORT -> Sign f e -> Set SORT
forall f e. SORT -> Sign f e -> Set SORT
supersortsOf SORT
s2 Sign f e
sign in
    if SORT -> Set SORT -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member SORT
s2 Set SORT
l1 then if Bool
b then [SORT
s2] else [SORT
s1] else
    if SORT -> Set SORT -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member SORT
s1 Set SORT
l2 then if Bool
b then [SORT
s1] else [SORT
s2] else
    Set SORT -> [SORT]
forall a. Set a -> [a]
Set.toList (Set SORT -> [SORT]) -> Set SORT -> [SORT]
forall a b. (a -> b) -> a -> b
$ if Bool
b then Set SORT -> Set SORT -> Set SORT
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set SORT
l1 Set SORT
l2
                 else Set SORT -> Set SORT -> Set SORT
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection (SORT -> Sign f e -> Set SORT
forall f e. SORT -> Sign f e -> Set SORT
subsortsOf SORT
s1 Sign f e
sign)
                             (Set SORT -> Set SORT) -> Set SORT -> Set SORT
forall a b. (a -> b) -> a -> b
$ SORT -> Sign f e -> Set SORT
forall f e. SORT -> Sign f e -> Set SORT
subsortsOf SORT
s2 Sign f e
sign

-- | True if both sorts have a common supersort
haveCommonSupersorts :: Bool -> Sign f e -> SORT -> SORT -> Bool
haveCommonSupersorts :: Bool -> Sign f e -> SORT -> SORT -> Bool
haveCommonSupersorts b :: Bool
b s :: Sign f e
s s1 :: SORT
s1 = Bool -> Bool
not (Bool -> Bool) -> (SORT -> Bool) -> SORT -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SORT] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([SORT] -> Bool) -> (SORT -> [SORT]) -> SORT -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Sign f e -> SORT -> SORT -> [SORT]
forall f e. Bool -> Sign f e -> SORT -> SORT -> [SORT]
commonSupersorts Bool
b Sign f e
s SORT
s1

-- True if both sorts have a common subsort
haveCommonSubsorts :: Sign f e -> SORT -> SORT -> Bool
haveCommonSubsorts :: Sign f e -> SORT -> SORT -> Bool
haveCommonSubsorts = Bool -> Sign f e -> SORT -> SORT -> Bool
forall f e. Bool -> Sign f e -> SORT -> SORT -> Bool
haveCommonSupersorts Bool
False

-- | if True test if s1 > s2
geqSort :: Bool -> Sign f e -> SORT -> SORT -> Bool
geqSort :: Bool -> Sign f e -> SORT -> SORT -> Bool
geqSort b :: Bool
b sign :: Sign f e
sign s1 :: SORT
s1 s2 :: SORT
s2 = SORT
s1 SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
s2 Bool -> Bool -> Bool
|| let rel :: Rel SORT
rel = Sign f e -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel Sign f e
sign in
    if Bool
b then SORT -> SORT -> Rel SORT -> Bool
forall a. Ord a => a -> a -> Rel a -> Bool
Rel.member SORT
s2 SORT
s1 Rel SORT
rel else SORT -> SORT -> Rel SORT -> Bool
forall a. Ord a => a -> a -> Rel a -> Bool
Rel.member SORT
s1 SORT
s2 Rel SORT
rel

-- | test if s1 < s2
leqSort :: Sign f e -> SORT -> SORT -> Bool
leqSort :: Sign f e -> SORT -> SORT -> Bool
leqSort = Bool -> Sign f e -> SORT -> SORT -> Bool
forall f e. Bool -> Sign f e -> SORT -> SORT -> Bool
geqSort Bool
False

-- | minimal common supersorts of the two input sorts
minimalSupers :: Sign f e -> SORT -> SORT -> [SORT]
minimalSupers :: Sign f e -> SORT -> SORT -> [SORT]
minimalSupers = Bool -> Sign f e -> SORT -> SORT -> [SORT]
forall f e. Bool -> Sign f e -> SORT -> SORT -> [SORT]
minimalSupers1 Bool
True

minimalSupers1 :: Bool -> Sign f e -> SORT -> SORT -> [SORT]
minimalSupers1 :: Bool -> Sign f e -> SORT -> SORT -> [SORT]
minimalSupers1 b :: Bool
b s :: Sign f e
s s1 :: SORT
s1 = Bool -> Sign f e -> (SORT -> SORT) -> [SORT] -> [SORT]
forall f e a. Bool -> Sign f e -> (a -> SORT) -> [a] -> [a]
keepMinimals1 Bool
b Sign f e
s SORT -> SORT
forall a. a -> a
id ([SORT] -> [SORT]) -> (SORT -> [SORT]) -> SORT -> [SORT]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Sign f e -> SORT -> SORT -> [SORT]
forall f e. Bool -> Sign f e -> SORT -> SORT -> [SORT]
commonSupersorts Bool
b Sign f e
s SORT
s1

-- | maximal common subsorts of the two input sorts
maximalSubs :: Sign f e -> SORT -> SORT -> [SORT]
maximalSubs :: Sign f e -> SORT -> SORT -> [SORT]
maximalSubs = Bool -> Sign f e -> SORT -> SORT -> [SORT]
forall f e. Bool -> Sign f e -> SORT -> SORT -> [SORT]
minimalSupers1 Bool
False

-- | only keep elements with minimal (and different) sorts
keepMinimals :: Sign f e -> (a -> SORT) -> [a] -> [a]
keepMinimals :: Sign f e -> (a -> SORT) -> [a] -> [a]
keepMinimals = Bool -> Sign f e -> (a -> SORT) -> [a] -> [a]
forall f e a. Bool -> Sign f e -> (a -> SORT) -> [a] -> [a]
keepMinimals1 Bool
True

keepMinimals1 :: Bool -> Sign f e -> (a -> SORT) -> [a] -> [a]
keepMinimals1 :: Bool -> Sign f e -> (a -> SORT) -> [a] -> [a]
keepMinimals1 b :: Bool
b s :: Sign f e
s f :: a -> SORT
f = let lt :: a -> a -> Bool
lt x :: a
x y :: a
y = Bool -> Sign f e -> SORT -> SORT -> Bool
forall f e. Bool -> Sign f e -> SORT -> SORT -> Bool
geqSort Bool
b Sign f e
s (a -> SORT
f a
y) (a -> SORT
f a
x) in (a -> a -> Bool) -> [a] -> [a]
forall a. (a -> a -> Bool) -> [a] -> [a]
keepMins a -> a -> Bool
lt

-- | True if both ops are in the overloading relation
leqF :: Sign f e -> OpType -> OpType -> Bool
leqF :: Sign f e -> OpType -> OpType -> Bool
leqF sign :: Sign f e
sign o1 :: OpType
o1 o2 :: OpType
o2 = [SORT] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (OpType -> [SORT]
opArgs OpType
o1) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [SORT] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (OpType -> [SORT]
opArgs OpType
o2) Bool -> Bool -> Bool
&& Sign f e -> OpType -> OpType -> Bool
forall f e. Sign f e -> OpType -> OpType -> Bool
leqF' Sign f e
sign OpType
o1 OpType
o2

leqF' :: Sign f e -> OpType -> OpType -> Bool
leqF' :: Sign f e -> OpType -> OpType -> Bool
leqF' sign :: Sign f e
sign o1 :: OpType
o1 o2 :: OpType
o2 = Bool -> Sign f e -> SORT -> SORT -> Bool
forall f e. Bool -> Sign f e -> SORT -> SORT -> Bool
haveCommonSupersorts Bool
True Sign f e
sign (OpType -> SORT
opRes OpType
o1) (OpType -> SORT
opRes OpType
o2) Bool -> Bool -> Bool
&&
    [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((SORT -> SORT -> Bool) -> [SORT] -> [SORT] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Sign f e -> SORT -> SORT -> Bool
forall f e. Sign f e -> SORT -> SORT -> Bool
haveCommonSubsorts Sign f e
sign) (OpType -> [SORT]
opArgs OpType
o1) (OpType -> [SORT]
opArgs OpType
o2))

-- | True if both preds are in the overloading relation
leqP :: Sign f e -> PredType -> PredType -> Bool
leqP :: Sign f e -> PredType -> PredType -> Bool
leqP sign :: Sign f e
sign p1 :: PredType
p1 p2 :: PredType
p2 = [SORT] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (PredType -> [SORT]
predArgs PredType
p1) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [SORT] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (PredType -> [SORT]
predArgs PredType
p2)
                  Bool -> Bool -> Bool
&& Sign f e -> PredType -> PredType -> Bool
forall f e. Sign f e -> PredType -> PredType -> Bool
leqP' Sign f e
sign PredType
p1 PredType
p2

leqP' :: Sign f e -> PredType -> PredType -> Bool
leqP' :: Sign f e -> PredType -> PredType -> Bool
leqP' sign :: Sign f e
sign p1 :: PredType
p1 =
    [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> (PredType -> [Bool]) -> PredType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SORT -> SORT -> Bool) -> [SORT] -> [SORT] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Sign f e -> SORT -> SORT -> Bool
forall f e. Sign f e -> SORT -> SORT -> Bool
haveCommonSubsorts Sign f e
sign) (PredType -> [SORT]
predArgs PredType
p1) ([SORT] -> [Bool]) -> (PredType -> [SORT]) -> PredType -> [Bool]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredType -> [SORT]
predArgs

cmpSubsort :: Sign f e -> POrder SORT
cmpSubsort :: Sign f e -> POrder SORT
cmpSubsort sign :: Sign f e
sign s1 :: SORT
s1 s2 :: SORT
s2 =
    if SORT
s1 SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
s2 then Ordering -> Maybe Ordering
forall a. a -> Maybe a
Just Ordering
EQ else
    let l1 :: Set SORT
l1 = SORT -> Sign f e -> Set SORT
forall f e. SORT -> Sign f e -> Set SORT
supersortsOf SORT
s1 Sign f e
sign
        l2 :: Set SORT
l2 = SORT -> Sign f e -> Set SORT
forall f e. SORT -> Sign f e -> Set SORT
supersortsOf SORT
s2 Sign f e
sign
        b :: Bool
b = SORT -> Set SORT -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member SORT
s1 Set SORT
l2 in
    if SORT -> Set SORT -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member SORT
s2 Set SORT
l1 then
        Ordering -> Maybe Ordering
forall a. a -> Maybe a
Just (Ordering -> Maybe Ordering) -> Ordering -> Maybe Ordering
forall a b. (a -> b) -> a -> b
$ if Bool
b then Ordering
EQ else Ordering
LT
    else if Bool
b then Ordering -> Maybe Ordering
forall a. a -> Maybe a
Just Ordering
GT else Maybe Ordering
forall a. Maybe a
Nothing

cmpSubsorts :: Sign f e -> POrder [SORT]
cmpSubsorts :: Sign f e -> POrder [SORT]
cmpSubsorts sign :: Sign f e
sign l1 :: [SORT]
l1 l2 :: [SORT]
l2 =
    let l :: [Maybe Ordering]
l = POrder SORT -> [SORT] -> [SORT] -> [Maybe Ordering]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Sign f e -> POrder SORT
forall f e. Sign f e -> POrder SORT
cmpSubsort Sign f e
sign) [SORT]
l1 [SORT]
l2
    in if [Maybe Ordering] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Maybe Ordering]
l then Ordering -> Maybe Ordering
forall a. a -> Maybe a
Just Ordering
EQ else (Maybe Ordering -> Maybe Ordering -> Maybe Ordering)
-> [Maybe Ordering] -> Maybe Ordering
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1
       ( \ c1 :: Maybe Ordering
c1 c2 :: Maybe Ordering
c2 -> if Maybe Ordering
c1 Maybe Ordering -> Maybe Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe Ordering
c2 then Maybe Ordering
c1 else case (Maybe Ordering
c1, Maybe Ordering
c2) of
           (Just EQ, _) -> Maybe Ordering
c2
           (_, Just EQ) -> Maybe Ordering
c1
           _ -> Maybe Ordering
forall a. Maybe a
Nothing) [Maybe Ordering]
l

pSortBy :: (a -> [SORT]) -> Sign f e -> [a] -> [a]
pSortBy :: (a -> [SORT]) -> Sign f e -> [a] -> [a]
pSortBy f :: a -> [SORT]
f sign :: Sign f e
sign = let pOrd :: a -> a -> Maybe Ordering
pOrd a :: a
a b :: a
b = Sign f e -> POrder [SORT]
forall f e. Sign f e -> POrder [SORT]
cmpSubsorts Sign f e
sign (a -> [SORT]
f a
a) (a -> [SORT]
f a
b)
                 in [[a]] -> [a]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[a]] -> [a]) -> ([a] -> [[a]]) -> [a] -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> a -> Maybe Ordering) -> [a] -> [[a]]
forall a. POrder a -> [a] -> [[a]]
rankBy a -> a -> Maybe Ordering
pOrd