{-|
Module      : Idris.TypeSearch
Description : A Hoogle for Idris.

License     : BSD3
Maintainer  : The Idris Community.
-}
{-# LANGUAGE CPP, ScopedTypeVariables #-}

module Idris.TypeSearch (
    searchByType
  , searchPred
  , defaultScoreFunction
  ) where

import Idris.AbsSyntax (addUsingConstraints, getIState, implicit, putIState)
import Idris.AbsSyntaxTree (IState(idris_docstrings, idris_interfaces, idris_outputmode, tt_ctxt),
                            Idris, InterfaceInfo, OutputMode(..), PTerm,
                            defaultSyntax, eqTy, implicitAllowed,
                            interface_implementations, toplevel)
import Idris.Core.Evaluate (Context(definitions), Def(CaseOp, Function, TyDecl),
                            normaliseC)
import Idris.Core.TT hiding (score)
import Idris.Core.Unify (match_unify)
import Idris.Delaborate (delabTy)
import Idris.Docstrings (noDocs, overview)
import Idris.Elab.Type (elabType)
import Idris.IBC
import Idris.Imports (PkgName)
import Idris.Output (iPrintResult, iRenderError, iRenderOutput, iRenderResult,
                     iputStrLn, prettyDocumentedIst)

import Util.Pretty (Doc, annotate, char, text, vsep, (<>))

#if (MIN_VERSION_base(4,11,0))
import Prelude hiding (Semigroup(..), pred)
import qualified Prelude as S (Semigroup(..))
#else
import Prelude hiding (pred)
#endif
import Control.Applicative ((<|>))
import Control.Arrow (first, second, (&&&), (***))
import Control.Monad (guard, when)
import Data.List (find, partition, (\\))
import Data.Map (Map)
import qualified Data.Map as M
import Data.Maybe (catMaybes, fromMaybe, isJust, mapMaybe, maybeToList)
import Data.Ord (comparing)
import qualified Data.PriorityQueue.FingerTree as Q
import Data.Set (Set)
import qualified Data.Set as S
import qualified Data.Text as T (isPrefixOf, pack)

searchByType :: [PkgName] -> PTerm -> Idris ()
searchByType :: [PkgName] -> PTerm -> Idris ()
searchByType [PkgName]
pkgs PTerm
pterm = do
  IState
i <- Idris IState
getIState -- save original
  Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not ([PkgName] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PkgName]
pkgs)) (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$
     String -> Idris ()
iputStrLn (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Searching packages: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
showSep String
", " ((PkgName -> String) -> [PkgName] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map PkgName -> String
forall a. Show a => a -> String
show [PkgName]
pkgs)

  (PkgName -> Idris ()) -> [PkgName] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ PkgName -> Idris ()
loadPkgIndex [PkgName]
pkgs
  PTerm
pterm' <- SyntaxInfo -> FC -> PTerm -> Idris PTerm
addUsingConstraints SyntaxInfo
syn FC
emptyFC PTerm
pterm
  PTerm
pterm'' <- ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm
implicit ElabInfo
toplevel SyntaxInfo
syn Name
name PTerm
pterm'
  Type
ty <- ElabInfo
-> SyntaxInfo
-> Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> FC
-> FnOpts
-> Name
-> FC
-> PTerm
-> Idris Type
elabType ElabInfo
toplevel SyntaxInfo
syn ((Docstring (Either Err PTerm),
 [(Name, Docstring (Either Err PTerm))])
-> Docstring (Either Err PTerm)
forall a b. (a, b) -> a
fst (Docstring (Either Err PTerm),
 [(Name, Docstring (Either Err PTerm))])
forall a. (Docstring a, [(Name, Docstring a)])
noDocs) ((Docstring (Either Err PTerm),
 [(Name, Docstring (Either Err PTerm))])
-> [(Name, Docstring (Either Err PTerm))]
forall a b. (a, b) -> b
snd (Docstring (Either Err PTerm),
 [(Name, Docstring (Either Err PTerm))])
forall a. (Docstring a, [(Name, Docstring a)])
noDocs) FC
emptyFC [] Name
name FC
NoFC PTerm
pterm'
  let names :: [(Name, Score)]
names = (IState -> Type -> [(Name, Type)] -> [(Name, Score)])
-> IState -> Type -> [(Name, Score)]
forall a.
(IState -> Type -> [(Name, Type)] -> [(Name, a)])
-> IState -> Type -> [(Name, a)]
searchUsing IState -> Type -> [(Name, Type)] -> [(Name, Score)]
searchPred IState
i Type
ty
  let names' :: [(Name, Score)]
names' = Int -> [(Name, Score)] -> [(Name, Score)]
forall a. Int -> [a] -> [a]
take Int
numLimit [(Name, Score)]
names
  let docs :: [Doc OutputAnnotation]
docs =
       [ let docInfo :: (Name, PTerm, Maybe (Docstring DocTerm))
docInfo = (Name
n, IState -> Name -> PTerm
delabTy IState
i Name
n, ((Docstring DocTerm, [(Name, Docstring DocTerm)])
 -> Docstring DocTerm)
-> Maybe (Docstring DocTerm, [(Name, Docstring DocTerm)])
-> Maybe (Docstring DocTerm)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Docstring DocTerm -> Docstring DocTerm
forall a. Docstring a -> Docstring a
overview (Docstring DocTerm -> Docstring DocTerm)
-> ((Docstring DocTerm, [(Name, Docstring DocTerm)])
    -> Docstring DocTerm)
-> (Docstring DocTerm, [(Name, Docstring DocTerm)])
-> Docstring DocTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Docstring DocTerm, [(Name, Docstring DocTerm)])
-> Docstring DocTerm
forall a b. (a, b) -> a
fst) (Name
-> Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
-> Maybe (Docstring DocTerm, [(Name, Docstring DocTerm)])
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
idris_docstrings IState
i))) in
         Score -> Doc OutputAnnotation
displayScore Score
theScore Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Char -> Doc OutputAnnotation
forall a. Char -> Doc a
char Char
' ' Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> IState
-> (Name, PTerm, Maybe (Docstring DocTerm)) -> Doc OutputAnnotation
prettyDocumentedIst IState
i (Name, PTerm, Maybe (Docstring DocTerm))
docInfo
                | (Name
n, Score
theScore) <- [(Name, Score)]
names']
  if (Bool -> Bool
not ([Doc OutputAnnotation] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Doc OutputAnnotation]
docs))
     then case IState -> OutputMode
idris_outputmode IState
i of
               RawOutput Handle
_  -> do (Doc OutputAnnotation -> Idris ())
-> [Doc OutputAnnotation] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Doc OutputAnnotation -> Idris ()
iRenderOutput [Doc OutputAnnotation]
docs
                                  String -> Idris ()
iPrintResult String
""
               IdeMode Integer
_ Handle
_ -> Doc OutputAnnotation -> Idris ()
iRenderResult ([Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep [Doc OutputAnnotation]
docs)
     else Doc OutputAnnotation -> Idris ()
iRenderError (Doc OutputAnnotation -> Idris ())
-> Doc OutputAnnotation -> Idris ()
forall a b. (a -> b) -> a -> b
$ String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"No results found"
  IState -> Idris ()
putIState IState
i -- don't actually make any changes
  where
    numLimit :: Int
numLimit = Int
50
    syn :: SyntaxInfo
syn = SyntaxInfo
defaultSyntax { implicitAllowed = True } -- syntax
    name :: Name
name = Int -> String -> Name
sMN Int
0 String
"searchType" -- name

-- | Conduct a type-directed search using a given match predicate
searchUsing :: (IState -> Type -> [(Name, Type)] -> [(Name, a)])
  -> IState -> Type -> [(Name, a)]
searchUsing :: forall a.
(IState -> Type -> [(Name, Type)] -> [(Name, a)])
-> IState -> Type -> [(Name, a)]
searchUsing IState -> Type -> [(Name, Type)] -> [(Name, a)]
pred IState
istate Type
ty = IState -> Type -> [(Name, Type)] -> [(Name, a)]
pred IState
istate Type
nty ([(Name, Type)] -> [(Name, a)])
-> (Map Name [(Name, Type)] -> [(Name, Type)])
-> Map Name [(Name, Type)]
-> [(Name, a)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[(Name, Type)]] -> [(Name, Type)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(Name, Type)]] -> [(Name, Type)])
-> (Map Name [(Name, Type)] -> [[(Name, Type)]])
-> Map Name [(Name, Type)]
-> [(Name, Type)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Name [(Name, Type)] -> [[(Name, Type)]]
forall k a. Map k a -> [a]
M.elems (Map Name [(Name, Type)] -> [(Name, a)])
-> Map Name [(Name, Type)] -> [(Name, a)]
forall a b. (a -> b) -> a -> b
$
  (Name
 -> Map
      Name
      (Def, RigCount, Bool, Accessibility, Totality, MetaInformation)
 -> [(Name, Type)])
-> Map
     Name
     (Map
        Name
        (Def, RigCount, Bool, Accessibility, Totality, MetaInformation))
-> Map Name [(Name, Type)]
forall k a b. (k -> a -> b) -> Map k a -> Map k b
M.mapWithKey (\Name
key -> Map Name Type -> [(Name, Type)]
forall k a. Map k a -> [(k, a)]
M.toAscList (Map Name Type -> [(Name, Type)])
-> (Map
      Name
      (Def, RigCount, Bool, Accessibility, Totality, MetaInformation)
    -> Map Name Type)
-> Map
     Name
     (Def, RigCount, Bool, Accessibility, Totality, MetaInformation)
-> [(Name, Type)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Def, RigCount, Bool, Accessibility, Totality, MetaInformation)
 -> Maybe Type)
-> Map
     Name
     (Def, RigCount, Bool, Accessibility, Totality, MetaInformation)
-> Map Name Type
forall a b k. (a -> Maybe b) -> Map k a -> Map k b
M.mapMaybe (Name
-> (Def, RigCount, Bool, Accessibility, Totality, MetaInformation)
-> Maybe Type
forall {r} {i} {b} {c} {d}.
Name -> (Def, r, i, b, c, d) -> Maybe Type
f Name
key)) (Context
-> Map
     Name
     (Map
        Name
        (Def, RigCount, Bool, Accessibility, Totality, MetaInformation))
definitions Context
ctxt)
  where
  nty :: Type
nty = Context -> Env -> Type -> Type
normaliseC Context
ctxt [] Type
ty
  ctxt :: Context
ctxt = IState -> Context
tt_ctxt IState
istate
  f :: Name -> (Def, r, i, b, c, d) -> Maybe Type
f Name
k (Def, r, i, b, c, d)
x = do
    Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Name -> Bool
special Name
k)
    Type
type2 <- (Def, r, i, b, c, d) -> Maybe Type
forall r i b c d. (Def, r, i, b, c, d) -> Maybe Type
typeFromDef (Def, r, i, b, c, d)
x
    Type -> Maybe Type
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Type -> Type
normaliseC Context
ctxt [] Type
type2
  special :: Name -> Bool
  special :: Name -> Bool
special (NS Name
n [Text]
_) = Name -> Bool
special Name
n
  special (SN SpecialName
_) = Bool
True
  special (UN Text
n) =    String -> Text
T.pack String
"default#" Text -> Text -> Bool
`T.isPrefixOf` Text
n
                   Bool -> Bool -> Bool
|| Text
n Text -> [Text] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (String -> Text) -> [String] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map String -> Text
T.pack [String
"believe_me", String
"really_believe_me"]
  special Name
_ = Bool
False

-- | Our default search predicate.
searchPred :: IState -> Type -> [(Name, Type)] -> [(Name, Score)]
searchPred :: IState -> Type -> [(Name, Type)] -> [(Name, Score)]
searchPred IState
istate Type
ty1 = [(Name, Type)] -> [(Name, Score)]
forall {info}. [(info, Type)] -> [(info, Score)]
matcher where
  maxScore :: Int
maxScore = Int
100
  matcher :: [(info, Type)] -> [(info, Score)]
matcher = IState -> Int -> Type -> [(info, Type)] -> [(info, Score)]
forall info.
IState -> Int -> Type -> [(info, Type)] -> [(info, Score)]
matchTypesBulk IState
istate Int
maxScore Type
ty1


typeFromDef :: (Def, r, i, b, c, d) -> Maybe Type
typeFromDef :: forall r i b c d. (Def, r, i, b, c, d) -> Maybe Type
typeFromDef (Def
def, r
_, i
_, b
_, c
_, d
_) = Def -> Maybe Type
get Def
def where
  get :: Def -> Maybe Type
  get :: Def -> Maybe Type
get (Function Type
ty Type
_) = Type -> Maybe Type
forall a. a -> Maybe a
Just Type
ty
  get (TyDecl NameType
_ Type
ty) = Type -> Maybe Type
forall a. a -> Maybe a
Just Type
ty
 -- get (Operator ty _ _) = Just ty
  get (CaseOp CaseInfo
_ Type
ty [(Type, Bool)]
_ [Either Type (Type, Type)]
_ [([Name], Type, Type)]
_ CaseDefs
_)  = Type -> Maybe Type
forall a. a -> Maybe a
Just Type
ty
  get Def
_ = Maybe Type
forall a. Maybe a
Nothing

-- Replace all occurences of `Delayed s t` with `t` in a type
unLazy :: Type -> Type
unLazy :: Type -> Type
unLazy Type
typ = case Type
typ of
  App AppStatus Name
_ (App AppStatus Name
_ (P NameType
_ Name
lazy Type
_) Type
_) Type
ty | Name
lazy Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"Delayed" -> Type -> Type
unLazy Type
ty
  Bind Name
name Binder Type
binder Type
ty -> Name -> Binder Type -> Type -> Type
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
name ((Type -> Type) -> Binder Type -> Binder Type
forall a b. (a -> b) -> Binder a -> Binder b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Type -> Type
unLazy Binder Type
binder) (Type -> Type
unLazy Type
ty)
  App AppStatus Name
s Type
t1 Type
t2 -> AppStatus Name -> Type -> Type -> Type
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
s (Type -> Type
unLazy Type
t1) (Type -> Type
unLazy Type
t2)
  Proj Type
ty Int
i -> Type -> Int -> Type
forall n. TT n -> Int -> TT n
Proj (Type -> Type
unLazy Type
ty) Int
i
  Type
_ -> Type
typ

-- | reverse the edges for a directed acyclic graph
reverseDag :: Ord k => [((k, a), Set k)] -> [((k, a), Set k)]
reverseDag :: forall k a. Ord k => [((k, a), Set k)] -> [((k, a), Set k)]
reverseDag [((k, a), Set k)]
xs = (((k, a), Set k) -> ((k, a), Set k))
-> [((k, a), Set k)] -> [((k, a), Set k)]
forall a b. (a -> b) -> [a] -> [b]
map ((k, a), Set k) -> ((k, a), Set k)
forall {b} {b}. ((k, b), b) -> ((k, b), Set k)
f [((k, a), Set k)]
xs where
  f :: ((k, b), b) -> ((k, b), Set k)
f ((k
k, b
v), b
_) = ((k
k, b
v), [k] -> Set k
forall a. Ord a => [a] -> Set a
S.fromList ([k] -> Set k)
-> ([((k, a), Set k)] -> [k]) -> [((k, a), Set k)] -> Set k
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (((k, a), Set k) -> k) -> [((k, a), Set k)] -> [k]
forall a b. (a -> b) -> [a] -> [b]
map ((k, a) -> k
forall a b. (a, b) -> a
fst ((k, a) -> k)
-> (((k, a), Set k) -> (k, a)) -> ((k, a), Set k) -> k
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((k, a), Set k) -> (k, a)
forall a b. (a, b) -> a
fst) ([((k, a), Set k)] -> Set k) -> [((k, a), Set k)] -> Set k
forall a b. (a -> b) -> a -> b
$ (((k, a), Set k) -> Bool) -> [((k, a), Set k)] -> [((k, a), Set k)]
forall a. (a -> Bool) -> [a] -> [a]
filter (k -> Set k -> Bool
forall a. Ord a => a -> Set a -> Bool
S.member k
k (Set k -> Bool)
-> (((k, a), Set k) -> Set k) -> ((k, a), Set k) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((k, a), Set k) -> Set k
forall a b. (a, b) -> b
snd) [((k, a), Set k)]
xs)

-- run vToP first!
-- | Compute a directed acyclic graph corresponding to the
-- arguments of a function.
-- returns [(the name and type of the bound variable
--          the names in the type of the bound variable)]
computeDagP :: Ord n
  => (TT n -> Bool) -- ^ filter to remove some arguments
  -> TT n
  -> ([((n, TT n), Set n)], [(n, TT n)], TT n)
computeDagP :: forall n.
Ord n =>
(TT n -> Bool) -> TT n -> ([((n, TT n), Set n)], [(n, TT n)], TT n)
computeDagP TT n -> Bool
removePred TT n
t = ([((n, TT n), Set n)] -> [((n, TT n), Set n)]
forall a. [a] -> [a]
reverse (((n, TT n) -> ((n, TT n), Set n))
-> [(n, TT n)] -> [((n, TT n), Set n)]
forall a b. (a -> b) -> [a] -> [b]
map (n, TT n) -> ((n, TT n), Set n)
forall {k} {a}. Ord k => (a, TT k) -> ((a, TT k), Set k)
f [(n, TT n)]
arguments), [(n, TT n)] -> [(n, TT n)]
forall a. [a] -> [a]
reverse [(n, TT n)]
theRemovedArgs , TT n
retTy) where
  f :: (a, TT k) -> ((a, TT k), Set k)
f (a
n, TT k
ty) = ((a
n, TT k
ty), Map k (TT k, Bool) -> Set k
forall k a. Map k a -> Set k
M.keysSet (TT k -> Map k (TT k, Bool)
forall n. Ord n => TT n -> Map n (TT n, Bool)
usedVars TT k
ty))

  ([(n, TT n)]
arguments, [(n, TT n)]
theRemovedArgs, TT n
retTy) = [(n, TT n)]
-> [(n, TT n)] -> TT n -> ([(n, TT n)], [(n, TT n)], TT n)
go [] [] TT n
t

  -- NOTE : args are in reverse order
  go :: [(n, TT n)]
-> [(n, TT n)] -> TT n -> ([(n, TT n)], [(n, TT n)], TT n)
go [(n, TT n)]
args [(n, TT n)]
removedArgs (Bind n
n (Pi RigCount
_ Maybe ImplicitInfo
_ TT n
ty TT n
_) TT n
sc) = let arg :: (n, TT n)
arg = (n
n, TT n
ty) in
    if TT n -> Bool
removePred TT n
ty
      then [(n, TT n)]
-> [(n, TT n)] -> TT n -> ([(n, TT n)], [(n, TT n)], TT n)
go [(n, TT n)]
args ((n, TT n)
arg (n, TT n) -> [(n, TT n)] -> [(n, TT n)]
forall a. a -> [a] -> [a]
: [(n, TT n)]
removedArgs) TT n
sc
      else [(n, TT n)]
-> [(n, TT n)] -> TT n -> ([(n, TT n)], [(n, TT n)], TT n)
go ((n, TT n)
arg (n, TT n) -> [(n, TT n)] -> [(n, TT n)]
forall a. a -> [a] -> [a]
: [(n, TT n)]
args) [(n, TT n)]
removedArgs TT n
sc
  go [(n, TT n)]
args [(n, TT n)]
removedArgs TT n
sc = ([(n, TT n)]
args, [(n, TT n)]
removedArgs, TT n
sc)

-- | Collect the names and types of all the free variables
-- The Boolean indicates those variables which are determined due to injectivity
-- I have not given nearly enough thought to know whether this is correct
usedVars :: Ord n => TT n -> Map n (TT n, Bool)
usedVars :: forall n. Ord n => TT n -> Map n (TT n, Bool)
usedVars = Bool -> TT n -> Map n (TT n, Bool)
forall {n}. Ord n => Bool -> TT n -> Map n (TT n, Bool)
f Bool
True where
  f :: Bool -> TT n -> Map n (TT n, Bool)
f Bool
b (P NameType
Bound n
n TT n
t) = n -> (TT n, Bool) -> Map n (TT n, Bool)
forall k a. k -> a -> Map k a
M.singleton n
n (TT n
t, Bool
b) Map n (TT n, Bool) -> Map n (TT n, Bool) -> Map n (TT n, Bool)
forall k a. Ord k => Map k a -> Map k a -> Map k a
`M.union` Bool -> TT n -> Map n (TT n, Bool)
f Bool
b TT n
t
  f Bool
b (Bind n
n Binder (TT n)
binder TT n
t2) = (n -> Map n (TT n, Bool) -> Map n (TT n, Bool)
forall k a. Ord k => k -> Map k a -> Map k a
M.delete n
n (Bool -> TT n -> Map n (TT n, Bool)
f Bool
b TT n
t2) Map n (TT n, Bool) -> Map n (TT n, Bool) -> Map n (TT n, Bool)
forall k a. Ord k => Map k a -> Map k a -> Map k a
`M.union`) (Map n (TT n, Bool) -> Map n (TT n, Bool))
-> Map n (TT n, Bool) -> Map n (TT n, Bool)
forall a b. (a -> b) -> a -> b
$ case Binder (TT n)
binder of
    Let RigCount
rig TT n
t TT n
v -> Bool -> TT n -> Map n (TT n, Bool)
f Bool
b TT n
t Map n (TT n, Bool) -> Map n (TT n, Bool) -> Map n (TT n, Bool)
forall k a. Ord k => Map k a -> Map k a -> Map k a
`M.union` Bool -> TT n -> Map n (TT n, Bool)
f Bool
b TT n
v
    Guess TT n
t TT n
v -> Bool -> TT n -> Map n (TT n, Bool)
f Bool
b TT n
t Map n (TT n, Bool) -> Map n (TT n, Bool) -> Map n (TT n, Bool)
forall k a. Ord k => Map k a -> Map k a -> Map k a
`M.union` Bool -> TT n -> Map n (TT n, Bool)
f Bool
b TT n
v
    Binder (TT n)
bind -> Bool -> TT n -> Map n (TT n, Bool)
f Bool
b (Binder (TT n) -> TT n
forall b. Binder b -> b
binderTy Binder (TT n)
bind)
  f Bool
b (App AppStatus n
_ TT n
t1 TT n
t2) = Bool -> TT n -> Map n (TT n, Bool)
f Bool
b TT n
t1 Map n (TT n, Bool) -> Map n (TT n, Bool) -> Map n (TT n, Bool)
forall k a. Ord k => Map k a -> Map k a -> Map k a
`M.union` Bool -> TT n -> Map n (TT n, Bool)
f (Bool
b Bool -> Bool -> Bool
&& TT n -> Bool
forall n. TT n -> Bool
isInjective TT n
t1) TT n
t2
  f Bool
b (Proj TT n
t Int
_) = Bool -> TT n -> Map n (TT n, Bool)
f Bool
b TT n
t
  f Bool
_ (V Int
_) = String -> Map n (TT n, Bool)
forall a. HasCallStack => String -> a
error String
"unexpected! run vToP first"
  f Bool
_ TT n
_ = Map n (TT n, Bool)
forall k a. Map k a
M.empty

-- | Remove a node from a directed acyclic graph
deleteFromDag :: Ord n => n -> [((n, TT n), (a, Set n))] -> [((n, TT n), (a, Set n))]
deleteFromDag :: forall n a.
Ord n =>
n -> [((n, TT n), (a, Set n))] -> [((n, TT n), (a, Set n))]
deleteFromDag n
name [] = []
deleteFromDag n
name (((n
name2, TT n
ty), (a
ix, Set n
set)) : [((n, TT n), (a, Set n))]
xs) = (if n
name n -> n -> Bool
forall a. Eq a => a -> a -> Bool
== n
name2
  then [((n, TT n), (a, Set n))] -> [((n, TT n), (a, Set n))]
forall a. a -> a
id
  else (((n
name2, TT n
ty) , (a
ix, n -> Set n -> Set n
forall a. Ord a => a -> Set a -> Set a
S.delete n
name Set n
set)) ((n, TT n), (a, Set n))
-> [((n, TT n), (a, Set n))] -> [((n, TT n), (a, Set n))]
forall a. a -> [a] -> [a]
:) ) (n -> [((n, TT n), (a, Set n))] -> [((n, TT n), (a, Set n))]
forall n a.
Ord n =>
n -> [((n, TT n), (a, Set n))] -> [((n, TT n), (a, Set n))]
deleteFromDag n
name [((n, TT n), (a, Set n))]
xs)

deleteFromArgList :: Ord n => n -> [(n, TT n)] -> [(n, TT n)]
deleteFromArgList :: forall n. Ord n => n -> [(n, TT n)] -> [(n, TT n)]
deleteFromArgList n
n = ((n, TT n) -> Bool) -> [(n, TT n)] -> [(n, TT n)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((n -> n -> Bool
forall a. Eq a => a -> a -> Bool
/= n
n) (n -> Bool) -> ((n, TT n) -> n) -> (n, TT n) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (n, TT n) -> n
forall a b. (a, b) -> a
fst)

-- | Asymmetric modifications to keep track of
data AsymMods = Mods
  { AsymMods -> Int
argApp         :: !Int
  , AsymMods -> Int
interfaceApp   :: !Int
  , AsymMods -> Int
interfaceIntro :: !Int
  } deriving (AsymMods -> AsymMods -> Bool
(AsymMods -> AsymMods -> Bool)
-> (AsymMods -> AsymMods -> Bool) -> Eq AsymMods
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: AsymMods -> AsymMods -> Bool
== :: AsymMods -> AsymMods -> Bool
$c/= :: AsymMods -> AsymMods -> Bool
/= :: AsymMods -> AsymMods -> Bool
Eq, Int -> AsymMods -> String -> String
[AsymMods] -> String -> String
AsymMods -> String
(Int -> AsymMods -> String -> String)
-> (AsymMods -> String)
-> ([AsymMods] -> String -> String)
-> Show AsymMods
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> AsymMods -> String -> String
showsPrec :: Int -> AsymMods -> String -> String
$cshow :: AsymMods -> String
show :: AsymMods -> String
$cshowList :: [AsymMods] -> String -> String
showList :: [AsymMods] -> String -> String
Show)


-- | Homogenous tuples
data Sided a = Sided
  { forall a. Sided a -> a
left  :: !a
  , forall a. Sided a -> a
right :: !a
  } deriving (Sided a -> Sided a -> Bool
(Sided a -> Sided a -> Bool)
-> (Sided a -> Sided a -> Bool) -> Eq (Sided a)
forall a. Eq a => Sided a -> Sided a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => Sided a -> Sided a -> Bool
== :: Sided a -> Sided a -> Bool
$c/= :: forall a. Eq a => Sided a -> Sided a -> Bool
/= :: Sided a -> Sided a -> Bool
Eq, Int -> Sided a -> String -> String
[Sided a] -> String -> String
Sided a -> String
(Int -> Sided a -> String -> String)
-> (Sided a -> String)
-> ([Sided a] -> String -> String)
-> Show (Sided a)
forall a. Show a => Int -> Sided a -> String -> String
forall a. Show a => [Sided a] -> String -> String
forall a. Show a => Sided a -> String
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Sided a -> String -> String
showsPrec :: Int -> Sided a -> String -> String
$cshow :: forall a. Show a => Sided a -> String
show :: Sided a -> String
$cshowList :: forall a. Show a => [Sided a] -> String -> String
showList :: [Sided a] -> String -> String
Show)

sided :: (a -> a -> b) -> Sided a -> b
sided :: forall a b. (a -> a -> b) -> Sided a -> b
sided a -> a -> b
f (Sided a
l a
r) = a -> a -> b
f a
l a
r

-- | Could be a functor instance, but let's avoid name overloading
both :: (a -> b) -> Sided a -> Sided b
both :: forall a b. (a -> b) -> Sided a -> Sided b
both a -> b
f (Sided a
l a
r) = b -> b -> Sided b
forall a. a -> a -> Sided a
Sided (a -> b
f a
l) (a -> b
f a
r)

-- | Keeps a record of the modifications made to match one type
-- signature with another
data Score = Score
  { Score -> Int
transposition :: !Int -- ^ transposition of arguments
  , Score -> Int
equalityFlips :: !Int -- ^ application of symmetry of equality
  , Score -> Sided AsymMods
asymMods      :: !(Sided AsymMods) -- ^ "directional" modifications
  } deriving (Score -> Score -> Bool
(Score -> Score -> Bool) -> (Score -> Score -> Bool) -> Eq Score
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Score -> Score -> Bool
== :: Score -> Score -> Bool
$c/= :: Score -> Score -> Bool
/= :: Score -> Score -> Bool
Eq, Int -> Score -> String -> String
[Score] -> String -> String
Score -> String
(Int -> Score -> String -> String)
-> (Score -> String) -> ([Score] -> String -> String) -> Show Score
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> Score -> String -> String
showsPrec :: Int -> Score -> String -> String
$cshow :: Score -> String
show :: Score -> String
$cshowList :: [Score] -> String -> String
showList :: [Score] -> String -> String
Show)

displayScore :: Score -> Doc OutputAnnotation
displayScore :: Score -> Doc OutputAnnotation
displayScore Score
score = case (AsymMods -> Bool) -> Sided AsymMods -> Sided Bool
forall a b. (a -> b) -> Sided a -> Sided b
both AsymMods -> Bool
noMods (Score -> Sided AsymMods
asymMods Score
score) of
  Sided Bool
True  Bool
True  -> Ordering -> String -> Doc OutputAnnotation
annotated Ordering
EQ String
"=" -- types are isomorphic
  Sided Bool
True  Bool
False -> Ordering -> String -> Doc OutputAnnotation
annotated Ordering
LT String
"<" -- found type is more general than searched type
  Sided Bool
False Bool
True  -> Ordering -> String -> Doc OutputAnnotation
annotated Ordering
GT String
">" -- searched type is more general than found type
  Sided Bool
False Bool
False -> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"_"
  where
  annotated :: Ordering -> String -> Doc OutputAnnotation
annotated Ordering
ordr = OutputAnnotation -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. a -> Doc a -> Doc a
annotate (Ordering -> OutputAnnotation
AnnSearchResult Ordering
ordr) (Doc OutputAnnotation -> Doc OutputAnnotation)
-> (String -> Doc OutputAnnotation)
-> String
-> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Doc OutputAnnotation
forall a. String -> Doc a
text
  noMods :: AsymMods -> Bool
noMods (Mods Int
app Int
tcApp Int
tcIntro) = Int
app Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
tcApp Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
tcIntro Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0

-- | This allows the search to stop expanding on a certain state if its
-- score is already too high. Returns 'True' if the algorithm should keep
-- exploring from this state, and 'False' otherwise.
scoreCriterion :: Score -> Bool
scoreCriterion :: Score -> Bool
scoreCriterion (Score Int
_ Int
_ Sided AsymMods
amods) = Bool -> Bool
not
  (  (Bool -> Bool -> Bool) -> Sided Bool -> Bool
forall a b. (a -> a -> b) -> Sided a -> b
sided Bool -> Bool -> Bool
(&&) ((AsymMods -> Bool) -> Sided AsymMods -> Sided Bool
forall a b. (a -> b) -> Sided a -> Sided b
both ((Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (Int -> Bool) -> (AsymMods -> Int) -> AsymMods -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AsymMods -> Int
argApp) Sided AsymMods
amods)
  Bool -> Bool -> Bool
|| (Int -> Int -> Int) -> Sided Int -> Int
forall a b. (a -> a -> b) -> Sided a -> b
sided Int -> Int -> Int
forall a. Num a => a -> a -> a
(+) ((AsymMods -> Int) -> Sided AsymMods -> Sided Int
forall a b. (a -> b) -> Sided a -> Sided b
both AsymMods -> Int
argApp Sided AsymMods
amods) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
4
  Bool -> Bool -> Bool
|| (Bool -> Bool -> Bool) -> Sided Bool -> Bool
forall a b. (a -> a -> b) -> Sided a -> b
sided Bool -> Bool -> Bool
(||) ((AsymMods -> Bool) -> Sided AsymMods -> Sided Bool
forall a b. (a -> b) -> Sided a -> Sided b
both (\(Mods Int
_ Int
tcApp Int
tcIntro) -> Int
tcApp Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
3 Bool -> Bool -> Bool
|| Int
tcIntro Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
3) Sided AsymMods
amods)
  )

-- | Convert a 'Score' to an 'Int' to provide an order for search results.
-- Lower scores are better.
defaultScoreFunction :: Score -> Int
defaultScoreFunction :: Score -> Int
defaultScoreFunction (Score Int
trans Int
eqFlip Sided AsymMods
amods) =
  Int
trans Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
eqFlip Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
linearPenalty Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
upAndDowncastPenalty
  where
  -- prefer finding a more general type to a less general type
  linearPenalty :: Int
linearPenalty = (\(Sided Int
l Int
r) -> Int
3 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
l Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
r)
    ((AsymMods -> Int) -> Sided AsymMods -> Sided Int
forall a b. (a -> b) -> Sided a -> Sided b
both (\(Mods Int
app Int
tcApp Int
tcIntro) -> Int
3 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
app Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
4 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
tcApp Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
tcIntro) Sided AsymMods
amods)
  -- it's very bad to have *both* upcasting and downcasting
  upAndDowncastPenalty :: Int
upAndDowncastPenalty = Int
100 Int -> Int -> Int
forall a. Num a => a -> a -> a
*
    (Int -> Int -> Int) -> Sided Int -> Int
forall a b. (a -> a -> b) -> Sided a -> b
sided Int -> Int -> Int
forall a. Num a => a -> a -> a
(*) ((AsymMods -> Int) -> Sided AsymMods -> Sided Int
forall a b. (a -> b) -> Sided a -> Sided b
both (\(Mods Int
app Int
tcApp Int
tcIntro) -> Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
app Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
tcApp Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
tcIntro) Sided AsymMods
amods)

instance Ord Score where
  compare :: Score -> Score -> Ordering
compare = (Score -> Int) -> Score -> Score -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing Score -> Int
defaultScoreFunction


#if (MIN_VERSION_base(4,11,0))
instance S.Semigroup a => S.Semigroup (Sided a) where
    (Sided a
l1 a
r1) <> :: Sided a -> Sided a -> Sided a
<> (Sided a
l2 a
r2) = a -> a -> Sided a
forall a. a -> a -> Sided a
Sided (a
l1 a -> a -> a
forall a. Semigroup a => a -> a -> a
S.<> a
l2) (a
r1 a -> a -> a
forall a. Semigroup a => a -> a -> a
S.<> a
r2)

instance S.Semigroup AsymMods where
    <> :: AsymMods -> AsymMods -> AsymMods
(<>) = AsymMods -> AsymMods -> AsymMods
forall a. Monoid a => a -> a -> a
mappend

instance S.Semigroup Score where
    <> :: Score -> Score -> Score
(<>) = Score -> Score -> Score
forall a. Monoid a => a -> a -> a
mappend
#endif

instance Monoid a => Monoid (Sided a) where
  mempty :: Sided a
mempty = a -> a -> Sided a
forall a. a -> a -> Sided a
Sided a
forall a. Monoid a => a
mempty a
forall a. Monoid a => a
mempty
  (Sided a
l1 a
r1) mappend :: Sided a -> Sided a -> Sided a
`mappend` (Sided a
l2 a
r2) = a -> a -> Sided a
forall a. a -> a -> Sided a
Sided (a
l1 a -> a -> a
forall a. Monoid a => a -> a -> a
`mappend` a
l2) (a
r1 a -> a -> a
forall a. Monoid a => a -> a -> a
`mappend` a
r2)

instance Monoid AsymMods where
  mempty :: AsymMods
mempty = Int -> Int -> Int -> AsymMods
Mods Int
0 Int
0 Int
0
  (Mods Int
a Int
b Int
c) mappend :: AsymMods -> AsymMods -> AsymMods
`mappend` (Mods Int
a' Int
b' Int
c') = Int -> Int -> Int -> AsymMods
Mods (Int
a Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
a') (Int
b Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
b') (Int
c Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
c')

instance Monoid Score where
  mempty :: Score
mempty = Int -> Int -> Sided AsymMods -> Score
Score Int
0 Int
0 Sided AsymMods
forall a. Monoid a => a
mempty
  (Score Int
t Int
e Sided AsymMods
mods) mappend :: Score -> Score -> Score
`mappend` (Score Int
t' Int
e' Sided AsymMods
mods') = Int -> Int -> Sided AsymMods -> Score
Score (Int
t Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
t') (Int
e Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
e') (Sided AsymMods
mods Sided AsymMods -> Sided AsymMods -> Sided AsymMods
forall a. Monoid a => a -> a -> a
`mappend` Sided AsymMods
mods')

-- | A directed acyclic graph representing the arguments to a function
-- The 'Int' represents the position of the argument (1st argument, 2nd, etc.)
type ArgsDAG = [((Name, Type), (Int, Set Name))]

-- | A list of interface constraints
type Interfaces = [(Name, Type)]

-- | The state corresponding to an attempted match of two types.
data State = State
  { State -> [(Name, Type)]
holes             :: ![(Name, Type)] -- ^ names which have yet to be resolved
  , State -> Sided (ArgsDAG, [(Name, Type)])
argsAndInterfaces :: !(Sided (ArgsDAG, Interfaces))
     -- ^ arguments and interface constraints for each type which have yet to be resolved
  , State -> Score
score             :: !Score -- ^ the score so far
  , State -> [Name]
usedNames         :: ![Name] -- ^ all names that have been used
  } deriving Int -> State -> String -> String
[State] -> String -> String
State -> String
(Int -> State -> String -> String)
-> (State -> String) -> ([State] -> String -> String) -> Show State
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> State -> String -> String
showsPrec :: Int -> State -> String -> String
$cshow :: State -> String
show :: State -> String
$cshowList :: [State] -> String -> String
showList :: [State] -> String -> String
Show

modifyTypes :: (Type -> Type) -> (ArgsDAG, Interfaces) -> (ArgsDAG, Interfaces)
modifyTypes :: (Type -> Type)
-> (ArgsDAG, [(Name, Type)]) -> (ArgsDAG, [(Name, Type)])
modifyTypes Type -> Type
f = ArgsDAG -> ArgsDAG
forall {d} {d}. [((d, Type), d)] -> [((d, Type), d)]
modifyDag (ArgsDAG -> ArgsDAG)
-> ([(Name, Type)] -> [(Name, Type)])
-> (ArgsDAG, [(Name, Type)])
-> (ArgsDAG, [(Name, Type)])
forall b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** [(Name, Type)] -> [(Name, Type)]
forall {d}. [(d, Type)] -> [(d, Type)]
modifyList
  where
  modifyDag :: [((d, Type), d)] -> [((d, Type), d)]
modifyDag = (((d, Type), d) -> ((d, Type), d))
-> [((d, Type), d)] -> [((d, Type), d)]
forall a b. (a -> b) -> [a] -> [b]
map (((d, Type) -> (d, Type)) -> ((d, Type), d) -> ((d, Type), d)
forall b c d. (b -> c) -> (b, d) -> (c, d)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first ((Type -> Type) -> (d, Type) -> (d, Type)
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second Type -> Type
f))
  modifyList :: [(d, Type)] -> [(d, Type)]
modifyList = ((d, Type) -> (d, Type)) -> [(d, Type)] -> [(d, Type)]
forall a b. (a -> b) -> [a] -> [b]
map ((Type -> Type) -> (d, Type) -> (d, Type)
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second Type -> Type
f)

findNameInArgsDAG :: Name -> ArgsDAG -> Maybe (Type, Maybe Int)
findNameInArgsDAG :: Name -> ArgsDAG -> Maybe (Type, Maybe Int)
findNameInArgsDAG Name
name = (((Name, Type), (Int, Set Name)) -> (Type, Maybe Int))
-> Maybe ((Name, Type), (Int, Set Name)) -> Maybe (Type, Maybe Int)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (((Name, Type) -> Type
forall a b. (a, b) -> b
snd ((Name, Type) -> Type)
-> (((Name, Type), (Int, Set Name)) -> (Name, Type))
-> ((Name, Type), (Int, Set Name))
-> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Name, Type), (Int, Set Name)) -> (Name, Type)
forall a b. (a, b) -> a
fst) (((Name, Type), (Int, Set Name)) -> Type)
-> (((Name, Type), (Int, Set Name)) -> Maybe Int)
-> ((Name, Type), (Int, Set Name))
-> (Type, Maybe Int)
forall b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& (Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int)
-> (((Name, Type), (Int, Set Name)) -> Int)
-> ((Name, Type), (Int, Set Name))
-> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, Set Name) -> Int
forall a b. (a, b) -> a
fst ((Int, Set Name) -> Int)
-> (((Name, Type), (Int, Set Name)) -> (Int, Set Name))
-> ((Name, Type), (Int, Set Name))
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Name, Type), (Int, Set Name)) -> (Int, Set Name)
forall a b. (a, b) -> b
snd)) (Maybe ((Name, Type), (Int, Set Name)) -> Maybe (Type, Maybe Int))
-> (ArgsDAG -> Maybe ((Name, Type), (Int, Set Name)))
-> ArgsDAG
-> Maybe (Type, Maybe Int)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (((Name, Type), (Int, Set Name)) -> Bool)
-> ArgsDAG -> Maybe ((Name, Type), (Int, Set Name))
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((Name
name Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
==) (Name -> Bool)
-> (((Name, Type), (Int, Set Name)) -> Name)
-> ((Name, Type), (Int, Set Name))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, Type) -> Name
forall a b. (a, b) -> a
fst ((Name, Type) -> Name)
-> (((Name, Type), (Int, Set Name)) -> (Name, Type))
-> ((Name, Type), (Int, Set Name))
-> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Name, Type), (Int, Set Name)) -> (Name, Type)
forall a b. (a, b) -> a
fst)

findName :: Name -> (ArgsDAG, Interfaces) -> Maybe (Type, Maybe Int)
findName :: Name -> (ArgsDAG, [(Name, Type)]) -> Maybe (Type, Maybe Int)
findName Name
n (ArgsDAG
args, [(Name, Type)]
interfaces) = Name -> ArgsDAG -> Maybe (Type, Maybe Int)
findNameInArgsDAG Name
n ArgsDAG
args Maybe (Type, Maybe Int)
-> Maybe (Type, Maybe Int) -> Maybe (Type, Maybe Int)
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ((,) (Type -> Maybe Int -> (Type, Maybe Int))
-> Maybe Type -> Maybe (Maybe Int -> (Type, Maybe Int))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> [(Name, Type)] -> Maybe Type
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, Type)]
interfaces Maybe (Maybe Int -> (Type, Maybe Int))
-> Maybe (Maybe Int) -> Maybe (Type, Maybe Int)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe (Maybe Int)
forall a. Maybe a
Nothing)

deleteName :: Name -> (ArgsDAG, Interfaces) -> (ArgsDAG, Interfaces)
deleteName :: Name -> (ArgsDAG, [(Name, Type)]) -> (ArgsDAG, [(Name, Type)])
deleteName Name
n (ArgsDAG
args, [(Name, Type)]
interfaces) = (Name -> ArgsDAG -> ArgsDAG
forall n a.
Ord n =>
n -> [((n, TT n), (a, Set n))] -> [((n, TT n), (a, Set n))]
deleteFromDag Name
n ArgsDAG
args, ((Name, Type) -> Bool) -> [(Name, Type)] -> [(Name, Type)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/= Name
n) (Name -> Bool) -> ((Name, Type) -> Name) -> (Name, Type) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, Type) -> Name
forall a b. (a, b) -> a
fst) [(Name, Type)]
interfaces)

tcToMaybe :: TC a -> Maybe a
tcToMaybe :: forall a. TC a -> Maybe a
tcToMaybe (OK a
x) = a -> Maybe a
forall a. a -> Maybe a
Just a
x
tcToMaybe (Error Err
_) = Maybe a
forall a. Maybe a
Nothing

inArgTys :: (Type -> Type) -> ArgsDAG -> ArgsDAG
inArgTys :: (Type -> Type) -> ArgsDAG -> ArgsDAG
inArgTys = (((Name, Type), (Int, Set Name))
 -> ((Name, Type), (Int, Set Name)))
-> ArgsDAG -> ArgsDAG
forall a b. (a -> b) -> [a] -> [b]
map ((((Name, Type), (Int, Set Name))
  -> ((Name, Type), (Int, Set Name)))
 -> ArgsDAG -> ArgsDAG)
-> ((Type -> Type)
    -> ((Name, Type), (Int, Set Name))
    -> ((Name, Type), (Int, Set Name)))
-> (Type -> Type)
-> ArgsDAG
-> ArgsDAG
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Name, Type) -> (Name, Type))
-> ((Name, Type), (Int, Set Name))
-> ((Name, Type), (Int, Set Name))
forall b c d. (b -> c) -> (b, d) -> (c, d)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (((Name, Type) -> (Name, Type))
 -> ((Name, Type), (Int, Set Name))
 -> ((Name, Type), (Int, Set Name)))
-> ((Type -> Type) -> (Name, Type) -> (Name, Type))
-> (Type -> Type)
-> ((Name, Type), (Int, Set Name))
-> ((Name, Type), (Int, Set Name))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type -> Type) -> (Name, Type) -> (Name, Type)
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second


interfaceUnify :: Ctxt InterfaceInfo -> Context -> Type -> Type -> Maybe [(Name, Type)]
interfaceUnify :: Ctxt InterfaceInfo
-> Context -> Type -> Type -> Maybe [(Name, Type)]
interfaceUnify Ctxt InterfaceInfo
interfaceInfo Context
ctxt Type
ty Type
tyTry = do
  [(Name, Type)]
res <- TC [(Name, Type)] -> Maybe [(Name, Type)]
forall a. TC a -> Maybe a
tcToMaybe (TC [(Name, Type)] -> Maybe [(Name, Type)])
-> TC [(Name, Type)] -> Maybe [(Name, Type)]
forall a b. (a -> b) -> a -> b
$ Context
-> Env
-> (Type, Maybe Provenance)
-> (Type, Maybe Provenance)
-> [Name]
-> [Name]
-> [FailContext]
-> TC [(Name, Type)]
match_unify Context
ctxt [] (Type
ty, Maybe Provenance
forall a. Maybe a
Nothing) (Type
retTy, Maybe Provenance
forall a. Maybe a
Nothing) [] [Name]
theHoles []
  Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ [Name] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Name]
theHoles [Name] -> [Name] -> [Name]
forall a. Eq a => [a] -> [a] -> [a]
\\ ((Name, Type) -> Name) -> [(Name, Type)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Type) -> Name
forall a b. (a, b) -> a
fst [(Name, Type)]
res)
  let argTys' :: [(Name, Type)]
argTys' = ((Name, Type) -> (Name, Type)) -> [(Name, Type)] -> [(Name, Type)]
forall a b. (a -> b) -> [a] -> [b]
map ((Type -> Type) -> (Name, Type) -> (Name, Type)
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second ((Type -> Type) -> (Name, Type) -> (Name, Type))
-> (Type -> Type) -> (Name, Type) -> (Name, Type)
forall a b. (a -> b) -> a -> b
$ ((Type -> Type) -> (Type -> Type) -> Type -> Type)
-> (Type -> Type) -> [Type -> Type] -> Type -> Type
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Type -> Type) -> (Type -> Type) -> Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) Type -> Type
forall a. a -> a
id [ Name -> Type -> Type -> Type
forall n. Eq n => n -> TT n -> TT n -> TT n
subst Name
n Type
t | (Name
n, Type
t) <- [(Name, Type)]
res ]) [(Name, Type)]
tcArgs
  [(Name, Type)] -> Maybe [(Name, Type)]
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return [(Name, Type)]
argTys'
  where
  tyTry' :: Type
tyTry' = Type -> Type
forall n. TT n -> TT n
vToP Type
tyTry
  theHoles :: [Name]
theHoles = ((Name, Type) -> Name) -> [(Name, Type)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Type) -> Name
forall a b. (a, b) -> a
fst [(Name, Type)]
nonTcArgs
  retTy :: Type
retTy = Type -> Type
forall n. TT n -> TT n
getRetTy Type
tyTry'
  ([(Name, Type)]
tcArgs, [(Name, Type)]
nonTcArgs) = ((Name, Type) -> Bool)
-> [(Name, Type)] -> ([(Name, Type)], [(Name, Type)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Ctxt InterfaceInfo -> Type -> Bool
isInterfaceArg Ctxt InterfaceInfo
interfaceInfo (Type -> Bool) -> ((Name, Type) -> Type) -> (Name, Type) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, Type) -> Type
forall a b. (a, b) -> b
snd) ([(Name, Type)] -> ([(Name, Type)], [(Name, Type)]))
-> [(Name, Type)] -> ([(Name, Type)], [(Name, Type)])
forall a b. (a -> b) -> a -> b
$ Type -> [(Name, Type)]
forall n. TT n -> [(n, TT n)]
getArgTys Type
tyTry'

isInterfaceArg :: Ctxt InterfaceInfo -> Type -> Bool
isInterfaceArg :: Ctxt InterfaceInfo -> Type -> Bool
isInterfaceArg Ctxt InterfaceInfo
interfaceInfo Type
ty = Bool -> Bool
not ([InterfaceInfo] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Type -> [Name]
forall {a}. TT a -> [a]
getInterfaceName Type
clss [Name] -> (Name -> [InterfaceInfo]) -> [InterfaceInfo]
forall a b. [a] -> (a -> [b]) -> [b]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Name -> Ctxt InterfaceInfo -> [InterfaceInfo])
-> Ctxt InterfaceInfo -> Name -> [InterfaceInfo]
forall a b c. (a -> b -> c) -> b -> a -> c
flip Name -> Ctxt InterfaceInfo -> [InterfaceInfo]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Ctxt InterfaceInfo
interfaceInfo)) where
  (Type
clss, [Type]
_) = Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
ty
  getInterfaceName :: TT a -> [a]
getInterfaceName (P (TCon Int
_ Int
_) a
interfaceName TT a
_) = [a
interfaceName]
  getInterfaceName TT a
_ = []


-- | Compute the power set
subsets :: [a] -> [[a]]
subsets :: forall a. [a] -> [[a]]
subsets [] = [[]]
subsets (a
x : [a]
xs) = let ss :: [[a]]
ss = [a] -> [[a]]
forall a. [a] -> [[a]]
subsets [a]
xs in ([a] -> [a]) -> [[a]] -> [[a]]
forall a b. (a -> b) -> [a] -> [b]
map (a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
:) [[a]]
ss [[a]] -> [[a]] -> [[a]]
forall a. [a] -> [a] -> [a]
++ [[a]]
ss


-- not recursive (i.e., doesn't flip iterated identities) at the moment
-- recalls the number of flips that have been made
flipEqualities :: Type -> [(Int, Type)]
flipEqualities :: Type -> [(Int, Type)]
flipEqualities Type
t = case Type
t of
  eq1 :: Type
eq1@(App AppStatus Name
_ (App AppStatus Name
_ (App AppStatus Name
_ (App AppStatus Name
_ eq :: Type
eq@(P NameType
_ Name
eqty Type
_) Type
tyL) Type
tyR) Type
valL) Type
valR) | Name
eqty Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
eqTy ->
    [(Int
0, Type
eq1), (Int
1, Type -> Type -> Type
forall {n}. TT n -> TT n -> TT n
app (Type -> Type -> Type
forall {n}. TT n -> TT n -> TT n
app (Type -> Type -> Type
forall {n}. TT n -> TT n -> TT n
app (Type -> Type -> Type
forall {n}. TT n -> TT n -> TT n
app Type
eq Type
tyR) Type
tyL) Type
valR) Type
valL)]
  Bind Name
n Binder Type
binder Type
sc -> (\Binder (Int, Type)
bind' (Int
j, Type
sc') -> ((Int, Type) -> Int
forall a b. (a, b) -> a
fst (Binder (Int, Type) -> (Int, Type)
forall b. Binder b -> b
binderTy Binder (Int, Type)
bind') Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
j, Name -> Binder Type -> Type -> Type
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (((Int, Type) -> Type) -> Binder (Int, Type) -> Binder Type
forall a b. (a -> b) -> Binder a -> Binder b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int, Type) -> Type
forall a b. (a, b) -> b
snd Binder (Int, Type)
bind') Type
sc'))
    (Binder (Int, Type) -> (Int, Type) -> (Int, Type))
-> [Binder (Int, Type)] -> [(Int, Type) -> (Int, Type)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type -> [(Int, Type)]) -> Binder Type -> [Binder (Int, Type)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Binder a -> f (Binder b)
traverse Type -> [(Int, Type)]
flipEqualities Binder Type
binder [(Int, Type) -> (Int, Type)] -> [(Int, Type)] -> [(Int, Type)]
forall a b. [a -> b] -> [a] -> [b]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> [(Int, Type)]
flipEqualities Type
sc
  App AppStatus Name
_ Type
f Type
x -> (\(Int
i, Type
f') (Int
j, Type
x') -> (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
j, Type -> Type -> Type
forall {n}. TT n -> TT n -> TT n
app Type
f' Type
x'))
    ((Int, Type) -> (Int, Type) -> (Int, Type))
-> [(Int, Type)] -> [(Int, Type) -> (Int, Type)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> [(Int, Type)]
flipEqualities Type
f [(Int, Type) -> (Int, Type)] -> [(Int, Type)] -> [(Int, Type)]
forall a b. [a -> b] -> [a] -> [b]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> [(Int, Type)]
flipEqualities Type
x
  Type
t' -> [(Int
0, Type
t')]
 where app :: TT n -> TT n -> TT n
app = AppStatus n -> TT n -> TT n -> TT n
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus n
forall n. AppStatus n
Complete

--DONT run vToP first!
-- | Try to match two types together in a unification-like procedure.
-- Returns a list of types and their minimum scores, sorted in order
-- of increasing score.
matchTypesBulk :: forall info. IState -> Int -> Type -> [(info, Type)] -> [(info, Score)]
matchTypesBulk :: forall info.
IState -> Int -> Type -> [(info, Type)] -> [(info, Score)]
matchTypesBulk IState
istate Int
maxScore Type
type1 [(info, Type)]
types = PQueue Score (info, PQueue Score State) -> [(info, Score)]
getAllResults PQueue Score (info, PQueue Score State)
startQueueOfQueues where
  getStartQueues :: (info, Type) -> Maybe (Score, (info, Q.PQueue Score State))
  getStartQueues :: (info, Type) -> Maybe (Score, (info, PQueue Score State))
getStartQueues nty :: (info, Type)
nty@(info
info, Type
type2) = case ((Int, ArgsDAG, Type) -> Maybe (Score, State))
-> [(Int, ArgsDAG, Type)] -> [(Score, State)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Int, ArgsDAG, Type) -> Maybe (Score, State)
startStates [(Int, ArgsDAG, Type)]
ty2s of
    [] -> Maybe (Score, (info, PQueue Score State))
forall a. Maybe a
Nothing
    [(Score, State)]
xs -> (Score, (info, PQueue Score State))
-> Maybe (Score, (info, PQueue Score State))
forall a. a -> Maybe a
Just ([Score] -> Score
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum (((Score, State) -> Score) -> [(Score, State)] -> [Score]
forall a b. (a -> b) -> [a] -> [b]
map (Score, State) -> Score
forall a b. (a, b) -> a
fst [(Score, State)]
xs), (info
info, [(Score, State)] -> PQueue Score State
forall k v. Ord k => [(k, v)] -> PQueue k v
Q.fromList [(Score, State)]
xs))
    where
    ty2s :: [(Int, ArgsDAG, Type)]
ty2s = (\(Int
i, ArgsDAG
dag) (Int
j, Type
retTy) -> (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
j, ArgsDAG
dag, Type
retTy))
      ((Int, ArgsDAG) -> (Int, Type) -> (Int, ArgsDAG, Type))
-> [(Int, ArgsDAG)] -> [(Int, Type) -> (Int, ArgsDAG, Type)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ArgsDAG -> [(Int, ArgsDAG)]
forall {a} {a} {b}.
[((a, Type), (a, b))] -> [(Int, [((a, Type), (a, b))])]
flipEqualitiesDag ArgsDAG
dag2 [(Int, Type) -> (Int, ArgsDAG, Type)]
-> [(Int, Type)] -> [(Int, ArgsDAG, Type)]
forall a b. [a -> b] -> [a] -> [b]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> [(Int, Type)]
flipEqualities Type
retTy2
    flipEqualitiesDag :: [((a, Type), (a, b))] -> [(Int, [((a, Type), (a, b))])]
flipEqualitiesDag [((a, Type), (a, b))]
dag = case [((a, Type), (a, b))]
dag of
      [] -> [(Int
0, [])]
      ((a
n, Type
ty), (a
pos, b
deps)) : [((a, Type), (a, b))]
xs ->
         (\(Int
i, Type
ty') (Int
j, [((a, Type), (a, b))]
xs') -> (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
j , ((a
n, Type
ty'), (a
pos, b
deps)) ((a, Type), (a, b))
-> [((a, Type), (a, b))] -> [((a, Type), (a, b))]
forall a. a -> [a] -> [a]
: [((a, Type), (a, b))]
xs'))
           ((Int, Type)
 -> (Int, [((a, Type), (a, b))]) -> (Int, [((a, Type), (a, b))]))
-> [(Int, Type)]
-> [(Int, [((a, Type), (a, b))]) -> (Int, [((a, Type), (a, b))])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> [(Int, Type)]
flipEqualities Type
ty [(Int, [((a, Type), (a, b))]) -> (Int, [((a, Type), (a, b))])]
-> [(Int, [((a, Type), (a, b))])] -> [(Int, [((a, Type), (a, b))])]
forall a b. [a -> b] -> [a] -> [b]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [((a, Type), (a, b))] -> [(Int, [((a, Type), (a, b))])]
flipEqualitiesDag [((a, Type), (a, b))]
xs
    startStates :: (Int, ArgsDAG, Type) -> Maybe (Score, State)
startStates (Int
numEqFlips, ArgsDAG
sndDag, Type
sndRetTy) = do
      State
state <- State -> [(Type, Type)] -> Maybe State
unifyQueue ([(Name, Type)]
-> Sided (ArgsDAG, [(Name, Type)]) -> Score -> [Name] -> State
State [(Name, Type)]
startingHoles
                ((ArgsDAG, [(Name, Type)])
-> (ArgsDAG, [(Name, Type)]) -> Sided (ArgsDAG, [(Name, Type)])
forall a. a -> a -> Sided a
Sided (ArgsDAG
dag1, [(Name, Type)]
interfaceArgs1) (ArgsDAG
sndDag, [(Name, Type)]
interfaceArgs2))
                (Score
forall a. Monoid a => a
mempty { equalityFlips = numEqFlips }) [Name]
usedns) [(Type
retTy1, Type
sndRetTy)]
      (Score, State) -> Maybe (Score, State)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (State -> Score
score State
state, State
state)


    (ArgsDAG
dag2, [(Name, Type)]
interfaceArgs2, Type
retTy2) = Type -> (ArgsDAG, [(Name, Type)], Type)
makeDag ([Name] -> Type -> Type
uniqueBinders (((Name, Type) -> Name) -> [(Name, Type)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Type) -> Name
forall a b. (a, b) -> a
fst [(Name, Type)]
argNames1) Type
type2)
    argNames2 :: [(Name, Type)]
argNames2 = (((Name, Type), (Int, Set Name)) -> (Name, Type))
-> ArgsDAG -> [(Name, Type)]
forall a b. (a -> b) -> [a] -> [b]
map ((Name, Type), (Int, Set Name)) -> (Name, Type)
forall a b. (a, b) -> a
fst ArgsDAG
dag2
    usedns :: [Name]
usedns = ((Name, Type) -> Name) -> [(Name, Type)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Type) -> Name
forall a b. (a, b) -> a
fst [(Name, Type)]
startingHoles
    startingHoles :: [(Name, Type)]
startingHoles = [(Name, Type)]
argNames1 [(Name, Type)] -> [(Name, Type)] -> [(Name, Type)]
forall a. [a] -> [a] -> [a]
++ [(Name, Type)]
argNames2


  startQueueOfQueues :: Q.PQueue Score (info, Q.PQueue Score State)
  startQueueOfQueues :: PQueue Score (info, PQueue Score State)
startQueueOfQueues = [(Score, (info, PQueue Score State))]
-> PQueue Score (info, PQueue Score State)
forall k v. Ord k => [(k, v)] -> PQueue k v
Q.fromList ([(Score, (info, PQueue Score State))]
 -> PQueue Score (info, PQueue Score State))
-> [(Score, (info, PQueue Score State))]
-> PQueue Score (info, PQueue Score State)
forall a b. (a -> b) -> a -> b
$ ((info, Type) -> Maybe (Score, (info, PQueue Score State)))
-> [(info, Type)] -> [(Score, (info, PQueue Score State))]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (info, Type) -> Maybe (Score, (info, PQueue Score State))
getStartQueues [(info, Type)]
types

  getAllResults :: Q.PQueue Score (info, Q.PQueue Score State) -> [(info, Score)]
  getAllResults :: PQueue Score (info, PQueue Score State) -> [(info, Score)]
getAllResults PQueue Score (info, PQueue Score State)
q = case PQueue Score (info, PQueue Score State)
-> Maybe
     ((Score, (info, PQueue Score State)),
      PQueue Score (info, PQueue Score State))
forall k v. Ord k => PQueue k v -> Maybe ((k, v), PQueue k v)
Q.minViewWithKey PQueue Score (info, PQueue Score State)
q of
    Maybe
  ((Score, (info, PQueue Score State)),
   PQueue Score (info, PQueue Score State))
Nothing -> []
    Just ((Score
nextScore, (info
info, PQueue Score State
stateQ)), PQueue Score (info, PQueue Score State)
q') ->
      if Score -> Int
defaultScoreFunction Score
nextScore Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
maxScore
        then case PQueue Score State -> Maybe (Either (PQueue Score State) Score)
nextStepsQueue PQueue Score State
stateQ of
          Maybe (Either (PQueue Score State) Score)
Nothing -> PQueue Score (info, PQueue Score State) -> [(info, Score)]
getAllResults PQueue Score (info, PQueue Score State)
q'
          Just (Left PQueue Score State
stateQ') -> case PQueue Score State -> Maybe ((Score, State), PQueue Score State)
forall k v. Ord k => PQueue k v -> Maybe ((k, v), PQueue k v)
Q.minViewWithKey PQueue Score State
stateQ' of
             Maybe ((Score, State), PQueue Score State)
Nothing -> PQueue Score (info, PQueue Score State) -> [(info, Score)]
getAllResults PQueue Score (info, PQueue Score State)
q'
             Just ((Score
newQscore,State
_), PQueue Score State
_) -> PQueue Score (info, PQueue Score State) -> [(info, Score)]
getAllResults (Score
-> (info, PQueue Score State)
-> PQueue Score (info, PQueue Score State)
-> PQueue Score (info, PQueue Score State)
forall k v. Ord k => k -> v -> PQueue k v -> PQueue k v
Q.add Score
newQscore (info
info, PQueue Score State
stateQ') PQueue Score (info, PQueue Score State)
q')
          Just (Right Score
theScore) -> (info
info, Score
theScore) (info, Score) -> [(info, Score)] -> [(info, Score)]
forall a. a -> [a] -> [a]
: PQueue Score (info, PQueue Score State) -> [(info, Score)]
getAllResults PQueue Score (info, PQueue Score State)
q'
        else []


  ctxt :: Context
ctxt = IState -> Context
tt_ctxt IState
istate
  interfaceInfo :: Ctxt InterfaceInfo
interfaceInfo = IState -> Ctxt InterfaceInfo
idris_interfaces IState
istate

  (ArgsDAG
dag1, [(Name, Type)]
interfaceArgs1, Type
retTy1) = Type -> (ArgsDAG, [(Name, Type)], Type)
makeDag Type
type1
  argNames1 :: [(Name, Type)]
argNames1 = (((Name, Type), (Int, Set Name)) -> (Name, Type))
-> ArgsDAG -> [(Name, Type)]
forall a b. (a -> b) -> [a] -> [b]
map ((Name, Type), (Int, Set Name)) -> (Name, Type)
forall a b. (a, b) -> a
fst ArgsDAG
dag1
  makeDag :: Type -> (ArgsDAG, Interfaces, Type)
  makeDag :: Type -> (ArgsDAG, [(Name, Type)], Type)
makeDag = ([((Name, Type), Set Name)] -> ArgsDAG)
-> ([((Name, Type), Set Name)], [(Name, Type)], Type)
-> (ArgsDAG, [(Name, Type)], Type)
forall {t} {a} {b} {c}. (t -> a) -> (t, b, c) -> (a, b, c)
first3 ((Int
 -> ((Name, Type), Set Name) -> ((Name, Type), (Int, Set Name)))
-> [Int] -> [((Name, Type), Set Name)] -> ArgsDAG
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Int
i ((Name, Type)
ty, Set Name
deps) -> ((Name, Type)
ty, (Int
i, Set Name
deps))) [Int
0..] ([((Name, Type), Set Name)] -> ArgsDAG)
-> ([((Name, Type), Set Name)] -> [((Name, Type), Set Name)])
-> [((Name, Type), Set Name)]
-> ArgsDAG
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [((Name, Type), Set Name)] -> [((Name, Type), Set Name)]
forall k a. Ord k => [((k, a), Set k)] -> [((k, a), Set k)]
reverseDag) (([((Name, Type), Set Name)], [(Name, Type)], Type)
 -> (ArgsDAG, [(Name, Type)], Type))
-> (Type -> ([((Name, Type), Set Name)], [(Name, Type)], Type))
-> Type
-> (ArgsDAG, [(Name, Type)], Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    (Type -> Bool)
-> Type -> ([((Name, Type), Set Name)], [(Name, Type)], Type)
forall n.
Ord n =>
(TT n -> Bool) -> TT n -> ([((n, TT n), Set n)], [(n, TT n)], TT n)
computeDagP (Ctxt InterfaceInfo -> Type -> Bool
isInterfaceArg Ctxt InterfaceInfo
interfaceInfo) (Type -> ([((Name, Type), Set Name)], [(Name, Type)], Type))
-> (Type -> Type)
-> Type
-> ([((Name, Type), Set Name)], [(Name, Type)], Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type
forall n. TT n -> TT n
vToP (Type -> Type) -> (Type -> Type) -> Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type
unLazy
  first3 :: (t -> a) -> (t, b, c) -> (a, b, c)
first3 t -> a
f (t
a,b
b,c
c) = (t -> a
f t
a, b
b, c
c)

  -- update our state with the unification resolutions
  resolveUnis :: [(Name, Type)] -> State -> Maybe (State, [(Type, Type)])
  resolveUnis :: [(Name, Type)] -> State -> Maybe (State, [(Type, Type)])
resolveUnis [] State
state = (State, [(Type, Type)]) -> Maybe (State, [(Type, Type)])
forall a. a -> Maybe a
Just (State
state, [])
  resolveUnis ((Name
name, term :: Type
term@(P NameType
Bound Name
name2 Type
_)) : [(Name, Type)]
xs)
    State
state | Maybe ((Type, Maybe Int), (Type, Maybe Int)) -> Bool
forall a. Maybe a -> Bool
isJust Maybe ((Type, Maybe Int), (Type, Maybe Int))
findArgs = do
    ((Type
ty1, Maybe Int
ix1), (Type
ty2, Maybe Int
ix2)) <- Maybe ((Type, Maybe Int), (Type, Maybe Int))
findArgs

    (State
state'', [(Type, Type)]
queue) <- [(Name, Type)] -> State -> Maybe (State, [(Type, Type)])
resolveUnis [(Name, Type)]
xs State
state'
    let transScore :: Int
transScore = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
0 (Int -> Int
forall a. Num a => a -> a
abs (Int -> Int) -> Maybe Int -> Maybe Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((-) (Int -> Int -> Int) -> Maybe Int -> Maybe (Int -> Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Int
ix1 Maybe (Int -> Int) -> Maybe Int -> Maybe Int
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe Int
ix2))
    (State, [(Type, Type)]) -> Maybe (State, [(Type, Type)])
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Score -> Score) -> State -> State
inScore (\Score
s -> Score
s { transposition = transposition s + transScore }) State
state'', (Type
ty1, Type
ty2) (Type, Type) -> [(Type, Type)] -> [(Type, Type)]
forall a. a -> [a] -> [a]
: [(Type, Type)]
queue)
    where
    unresolved :: Sided (ArgsDAG, [(Name, Type)])
unresolved = State -> Sided (ArgsDAG, [(Name, Type)])
argsAndInterfaces State
state
    inScore :: (Score -> Score) -> State -> State
inScore Score -> Score
f State
stat = State
stat { score = f (score stat) }
    findArgs :: Maybe ((Type, Maybe Int), (Type, Maybe Int))
findArgs = ((,) ((Type, Maybe Int)
 -> (Type, Maybe Int) -> ((Type, Maybe Int), (Type, Maybe Int)))
-> Maybe (Type, Maybe Int)
-> Maybe
     ((Type, Maybe Int) -> ((Type, Maybe Int), (Type, Maybe Int)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> (ArgsDAG, [(Name, Type)]) -> Maybe (Type, Maybe Int)
findName Name
name  (Sided (ArgsDAG, [(Name, Type)]) -> (ArgsDAG, [(Name, Type)])
forall a. Sided a -> a
left Sided (ArgsDAG, [(Name, Type)])
unresolved) Maybe ((Type, Maybe Int) -> ((Type, Maybe Int), (Type, Maybe Int)))
-> Maybe (Type, Maybe Int)
-> Maybe ((Type, Maybe Int), (Type, Maybe Int))
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Name -> (ArgsDAG, [(Name, Type)]) -> Maybe (Type, Maybe Int)
findName Name
name2 (Sided (ArgsDAG, [(Name, Type)]) -> (ArgsDAG, [(Name, Type)])
forall a. Sided a -> a
right Sided (ArgsDAG, [(Name, Type)])
unresolved)) Maybe ((Type, Maybe Int), (Type, Maybe Int))
-> Maybe ((Type, Maybe Int), (Type, Maybe Int))
-> Maybe ((Type, Maybe Int), (Type, Maybe Int))
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
               ((,) ((Type, Maybe Int)
 -> (Type, Maybe Int) -> ((Type, Maybe Int), (Type, Maybe Int)))
-> Maybe (Type, Maybe Int)
-> Maybe
     ((Type, Maybe Int) -> ((Type, Maybe Int), (Type, Maybe Int)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> (ArgsDAG, [(Name, Type)]) -> Maybe (Type, Maybe Int)
findName Name
name2 (Sided (ArgsDAG, [(Name, Type)]) -> (ArgsDAG, [(Name, Type)])
forall a. Sided a -> a
left Sided (ArgsDAG, [(Name, Type)])
unresolved) Maybe ((Type, Maybe Int) -> ((Type, Maybe Int), (Type, Maybe Int)))
-> Maybe (Type, Maybe Int)
-> Maybe ((Type, Maybe Int), (Type, Maybe Int))
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Name -> (ArgsDAG, [(Name, Type)]) -> Maybe (Type, Maybe Int)
findName Name
name  (Sided (ArgsDAG, [(Name, Type)]) -> (ArgsDAG, [(Name, Type)])
forall a. Sided a -> a
right Sided (ArgsDAG, [(Name, Type)])
unresolved))
    matchnames :: [Name]
matchnames = [Name
name, Name
name2]
    deleteArgs :: (ArgsDAG, [(Name, Type)]) -> (ArgsDAG, [(Name, Type)])
deleteArgs = Name -> (ArgsDAG, [(Name, Type)]) -> (ArgsDAG, [(Name, Type)])
deleteName Name
name ((ArgsDAG, [(Name, Type)]) -> (ArgsDAG, [(Name, Type)]))
-> ((ArgsDAG, [(Name, Type)]) -> (ArgsDAG, [(Name, Type)]))
-> (ArgsDAG, [(Name, Type)])
-> (ArgsDAG, [(Name, Type)])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> (ArgsDAG, [(Name, Type)]) -> (ArgsDAG, [(Name, Type)])
deleteName Name
name2
    state' :: State
state' = State
state { holes = filter (not . (`elem` matchnames) . fst) (holes state)
                   , argsAndInterfaces = both (modifyTypes (subst name term) . deleteArgs) unresolved}

  resolveUnis ((Name
name, Type
term) : [(Name, Type)]
xs)
    state :: State
state@(State [(Name, Type)]
hs Sided (ArgsDAG, [(Name, Type)])
unresolved Score
_ [Name]
_) = case ((ArgsDAG, [(Name, Type)]) -> Maybe (Type, Maybe Int))
-> Sided (ArgsDAG, [(Name, Type)])
-> Sided (Maybe (Type, Maybe Int))
forall a b. (a -> b) -> Sided a -> Sided b
both (Name -> (ArgsDAG, [(Name, Type)]) -> Maybe (Type, Maybe Int)
findName Name
name) Sided (ArgsDAG, [(Name, Type)])
unresolved of
      Sided Maybe (Type, Maybe Int)
Nothing  Maybe (Type, Maybe Int)
Nothing  -> Maybe (State, [(Type, Type)])
forall a. Maybe a
Nothing
      Sided (Just (Type, Maybe Int)
_) (Just (Type, Maybe Int)
_) -> String -> Maybe (State, [(Type, Type)])
forall a. HasCallStack => String -> a
error String
"Idris internal error: TypeSearch.resolveUnis"
      Sided (Maybe (Type, Maybe Int))
oneOfEach -> (State -> State)
-> (State, [(Type, Type)]) -> (State, [(Type, Type)])
forall b c d. (b -> c) -> (b, d) -> (c, d)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (Sided AsymMods -> State -> State
addScore ((Maybe (Type, Maybe Int) -> AsymMods)
-> Sided (Maybe (Type, Maybe Int)) -> Sided AsymMods
forall a b. (a -> b) -> Sided a -> Sided b
both Maybe (Type, Maybe Int) -> AsymMods
forall {a}. Maybe a -> AsymMods
scoreFor Sided (Maybe (Type, Maybe Int))
oneOfEach)) ((State, [(Type, Type)]) -> (State, [(Type, Type)]))
-> Maybe (State, [(Type, Type)]) -> Maybe (State, [(Type, Type)])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (State, [(Type, Type)])
nextStep
    where
    scoreFor :: Maybe a -> AsymMods
scoreFor (Just a
_) = AsymMods
forall a. Monoid a => a
mempty { argApp = 1 }
    scoreFor Maybe a
Nothing  = AsymMods
forall a. Monoid a => a
mempty { argApp = otherApplied }
    -- find variables which are determined uniquely by the type
    -- due to injectivity
    matchedVarMap :: Map Name (Type, Bool)
matchedVarMap = Type -> Map Name (Type, Bool)
forall n. Ord n => TT n -> Map n (TT n, Bool)
usedVars Type
term
    bothT :: (t -> b) -> (t, t) -> (b, b)
bothT t -> b
f (t
x, t
y) = (t -> b
f t
x, t -> b
f t
y)
    ([Name]
injUsedVars, [Name]
notInjUsedVars) = (Map Name Bool -> [Name])
-> (Map Name Bool, Map Name Bool) -> ([Name], [Name])
forall {t} {b}. (t -> b) -> (t, t) -> (b, b)
bothT Map Name Bool -> [Name]
forall k a. Map k a -> [k]
M.keys ((Map Name Bool, Map Name Bool) -> ([Name], [Name]))
-> (Map Name Bool -> (Map Name Bool, Map Name Bool))
-> Map Name Bool
-> ([Name], [Name])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool -> Bool) -> Map Name Bool -> (Map Name Bool, Map Name Bool)
forall a k. (a -> Bool) -> Map k a -> (Map k a, Map k a)
M.partition Bool -> Bool
forall a. a -> a
id (Map Name Bool -> (Map Name Bool, Map Name Bool))
-> (Map Name Bool -> Map Name Bool)
-> Map Name Bool
-> (Map Name Bool, Map Name Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name -> Bool -> Bool) -> Map Name Bool -> Map Name Bool
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
M.filterWithKey (\Name
k Bool
_-> Name
k Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ((Name, Type) -> Name) -> [(Name, Type)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Type) -> Name
forall a b. (a, b) -> a
fst [(Name, Type)]
hs) (Map Name Bool -> ([Name], [Name]))
-> Map Name Bool -> ([Name], [Name])
forall a b. (a -> b) -> a -> b
$ ((Type, Bool) -> Bool) -> Map Name (Type, Bool) -> Map Name Bool
forall a b k. (a -> b) -> Map k a -> Map k b
M.map (Type, Bool) -> Bool
forall a b. (a, b) -> b
snd Map Name (Type, Bool)
matchedVarMap
    varsInTy :: [Name]
varsInTy = [Name]
injUsedVars [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
notInjUsedVars
    toDelete :: [Name]
toDelete = Name
name Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
varsInTy
    deleteMany :: (ArgsDAG, [(Name, Type)]) -> (ArgsDAG, [(Name, Type)])
deleteMany = (((ArgsDAG, [(Name, Type)]) -> (ArgsDAG, [(Name, Type)]))
 -> ((ArgsDAG, [(Name, Type)]) -> (ArgsDAG, [(Name, Type)]))
 -> (ArgsDAG, [(Name, Type)])
 -> (ArgsDAG, [(Name, Type)]))
-> ((ArgsDAG, [(Name, Type)]) -> (ArgsDAG, [(Name, Type)]))
-> [(ArgsDAG, [(Name, Type)]) -> (ArgsDAG, [(Name, Type)])]
-> (ArgsDAG, [(Name, Type)])
-> (ArgsDAG, [(Name, Type)])
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((ArgsDAG, [(Name, Type)]) -> (ArgsDAG, [(Name, Type)]))
-> ((ArgsDAG, [(Name, Type)]) -> (ArgsDAG, [(Name, Type)]))
-> (ArgsDAG, [(Name, Type)])
-> (ArgsDAG, [(Name, Type)])
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) (ArgsDAG, [(Name, Type)]) -> (ArgsDAG, [(Name, Type)])
forall a. a -> a
id ((Name -> (ArgsDAG, [(Name, Type)]) -> (ArgsDAG, [(Name, Type)]))
-> [Name]
-> [(ArgsDAG, [(Name, Type)]) -> (ArgsDAG, [(Name, Type)])]
forall a b. (a -> b) -> [a] -> [b]
map Name -> (ArgsDAG, [(Name, Type)]) -> (ArgsDAG, [(Name, Type)])
deleteName [Name]
toDelete)

    otherApplied :: Int
otherApplied = [Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
notInjUsedVars

    addScore :: Sided AsymMods -> State -> State
addScore Sided AsymMods
additions State
theState = State
theState { score = let s = State -> Score
score State
theState in
      s { asymMods = asymMods s `mappend` additions } }
    state' :: State
state' = State
state { holes = filter (not . (`elem` toDelete) . fst) hs
                   , argsAndInterfaces = both (modifyTypes (subst name term) . deleteMany) (argsAndInterfaces state) }
    nextStep :: Maybe (State, [(Type, Type)])
nextStep = [(Name, Type)] -> State -> Maybe (State, [(Type, Type)])
resolveUnis [(Name, Type)]
xs State
state'


  -- | resolve a queue of unification constraints
  unifyQueue :: State -> [(Type, Type)] -> Maybe State
  unifyQueue :: State -> [(Type, Type)] -> Maybe State
unifyQueue State
state [] = State -> Maybe State
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return State
state
  unifyQueue State
state ((Type
ty1, Type
ty2) : [(Type, Type)]
queue) = do
    --trace ("go: \n" ++ show state) True `seq` return ()
    [(Name, Type)]
res <- TC [(Name, Type)] -> Maybe [(Name, Type)]
forall a. TC a -> Maybe a
tcToMaybe (TC [(Name, Type)] -> Maybe [(Name, Type)])
-> TC [(Name, Type)] -> Maybe [(Name, Type)]
forall a b. (a -> b) -> a -> b
$ Context
-> Env
-> (Type, Maybe Provenance)
-> (Type, Maybe Provenance)
-> [Name]
-> [Name]
-> [FailContext]
-> TC [(Name, Type)]
match_unify Context
ctxt [ (Name
n, RigCount
RigW, RigCount -> Maybe ImplicitInfo -> Type -> Type -> Binder Type
forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
RigW Maybe ImplicitInfo
forall a. Maybe a
Nothing Type
ty (UExp -> Type
forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] Int
0))) | (Name
n, Type
ty) <- State -> [(Name, Type)]
holes State
state]
                                   (Type
ty1, Maybe Provenance
forall a. Maybe a
Nothing)
                                   (Type
ty2, Maybe Provenance
forall a. Maybe a
Nothing) [] (((Name, Type) -> Name) -> [(Name, Type)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Type) -> Name
forall a b. (a, b) -> a
fst ([(Name, Type)] -> [Name]) -> [(Name, Type)] -> [Name]
forall a b. (a -> b) -> a -> b
$ State -> [(Name, Type)]
holes State
state) []
    (State
state', [(Type, Type)]
queueAdditions) <- [(Name, Type)] -> State -> Maybe (State, [(Type, Type)])
resolveUnis [(Name, Type)]
res State
state
    Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ Score -> Bool
scoreCriterion (State -> Score
score State
state')
    State -> [(Type, Type)] -> Maybe State
unifyQueue State
state' ([(Type, Type)]
queue [(Type, Type)] -> [(Type, Type)] -> [(Type, Type)]
forall a. [a] -> [a] -> [a]
++ [(Type, Type)]
queueAdditions)

  possInterfaceImplementations :: [Name] -> Type -> [Type]
  possInterfaceImplementations :: [Name] -> Type -> [Type]
possInterfaceImplementations [Name]
usedns Type
ty = do
    Name
interfaceName <- Type -> [Name]
forall {a}. TT a -> [a]
getInterfaceName Type
clss
    InterfaceInfo
interfaceDef <- Name -> Ctxt InterfaceInfo -> [InterfaceInfo]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
interfaceName Ctxt InterfaceInfo
interfaceInfo
    (Name, Bool)
n <- InterfaceInfo -> [(Name, Bool)]
interface_implementations InterfaceInfo
interfaceDef
    (Def, RigCount, Bool, Accessibility, Totality, MetaInformation)
def <- Name
-> Map
     Name
     (Map
        Name
        (Def, RigCount, Bool, Accessibility, Totality, MetaInformation))
-> [(Def, RigCount, Bool, Accessibility, Totality,
     MetaInformation)]
forall a. Name -> Ctxt a -> [a]
lookupCtxt ((Name, Bool) -> Name
forall a b. (a, b) -> a
fst (Name, Bool)
n) (Context
-> Map
     Name
     (Map
        Name
        (Def, RigCount, Bool, Accessibility, Totality, MetaInformation))
definitions Context
ctxt)
    Type
nty <- Context -> Env -> Type -> Type
normaliseC Context
ctxt [] (Type -> Type) -> [Type] -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (case (Def, RigCount, Bool, Accessibility, Totality, MetaInformation)
-> Maybe Type
forall r i b c d. (Def, r, i, b, c, d) -> Maybe Type
typeFromDef (Def, RigCount, Bool, Accessibility, Totality, MetaInformation)
def of Just Type
x -> [Type
x]; Maybe Type
Nothing -> [])
    let ty' :: Type
ty' = Type -> Type
forall n. TT n -> TT n
vToP ([Name] -> Type -> Type
uniqueBinders [Name]
usedns Type
nty)
    Type -> [Type]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty'
    where
    (Type
clss, [Type]
_) = Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
ty
    getInterfaceName :: TT a -> [a]
getInterfaceName (P (TCon Int
_ Int
_) a
interfaceName TT a
_) = [a
interfaceName]
    getInterfaceName TT a
_ = []

  -- 'Just' if the computation hasn't totally failed yet, 'Nothing' if it has
  -- 'Left' if we haven't found a terminal state, 'Right' if we have
  nextStepsQueue :: Q.PQueue Score State -> Maybe (Either (Q.PQueue Score State) Score)
  nextStepsQueue :: PQueue Score State -> Maybe (Either (PQueue Score State) Score)
nextStepsQueue PQueue Score State
queue = do
    ((Score
nextScore, State
next), PQueue Score State
rest) <- PQueue Score State -> Maybe ((Score, State), PQueue Score State)
forall k v. Ord k => PQueue k v -> Maybe ((k, v), PQueue k v)
Q.minViewWithKey PQueue Score State
queue
    Either (PQueue Score State) Score
-> Maybe (Either (PQueue Score State) Score)
forall a. a -> Maybe a
Just (Either (PQueue Score State) Score
 -> Maybe (Either (PQueue Score State) Score))
-> Either (PQueue Score State) Score
-> Maybe (Either (PQueue Score State) Score)
forall a b. (a -> b) -> a -> b
$ if State -> Bool
isFinal State
next
      then Score -> Either (PQueue Score State) Score
forall a b. b -> Either a b
Right Score
nextScore
      else let additions :: PQueue Score State
additions = if Score -> Bool
scoreCriterion Score
nextScore
                 then [(Score, State)] -> PQueue Score State
forall k v. Ord k => [(k, v)] -> PQueue k v
Q.fromList [ (State -> Score
score State
state, State
state) | State
state <- State -> [State]
nextSteps State
next ]
                 else PQueue Score State
forall k v. Ord k => PQueue k v
Q.empty in
           PQueue Score State -> Either (PQueue Score State) Score
forall a b. a -> Either a b
Left (PQueue Score State -> PQueue Score State -> PQueue Score State
forall k v. Ord k => PQueue k v -> PQueue k v -> PQueue k v
Q.union PQueue Score State
rest PQueue Score State
additions)
    where
    isFinal :: State -> Bool
isFinal (State [] (Sided ([], []) ([], [])) Score
_ [Name]
_) = Bool
True
    isFinal State
_ = Bool
False

  -- | Find all possible matches starting from a given state.
  -- We go in stages rather than concatenating all three results in hopes of narrowing
  -- the search tree. Once we advance in a phase, there should be no going back.
  nextSteps :: State -> [State]

  -- Stage 3 - match interfaces
  nextSteps :: State -> [State]
nextSteps (State [] unresolved :: Sided (ArgsDAG, [(Name, Type)])
unresolved@(Sided ([], [(Name, Type)]
c1) ([], [(Name, Type)]
c2)) Score
scoreAcc [Name]
usedns) =
    if [State] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [State]
results3 then [State]
results4 else [State]
results3
    where
    -- try to match an interface argument from the left with an interface argument from the right
    results3 :: [State]
results3 =
         [Maybe State] -> [State]
forall a. [Maybe a] -> [a]
catMaybes [ State -> [(Type, Type)] -> Maybe State
unifyQueue ([(Name, Type)]
-> Sided (ArgsDAG, [(Name, Type)]) -> Score -> [Name] -> State
State []
         ((ArgsDAG, [(Name, Type)])
-> (ArgsDAG, [(Name, Type)]) -> Sided (ArgsDAG, [(Name, Type)])
forall a. a -> a -> Sided a
Sided ([], Name -> [(Name, Type)] -> [(Name, Type)]
forall n. Ord n => n -> [(n, TT n)] -> [(n, TT n)]
deleteFromArgList Name
n1 [(Name, Type)]
c1)
                ([], ((Name, Type) -> (Name, Type)) -> [(Name, Type)] -> [(Name, Type)]
forall a b. (a -> b) -> [a] -> [b]
map ((Type -> Type) -> (Name, Type) -> (Name, Type)
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second Type -> Type
subst2for1) (Name -> [(Name, Type)] -> [(Name, Type)]
forall n. Ord n => n -> [(n, TT n)] -> [(n, TT n)]
deleteFromArgList Name
n2 [(Name, Type)]
c2)))
         Score
scoreAcc [Name]
usedns) [(Type
ty1, Type
ty2)]
     | (Name
n1, Type
ty1) <- [(Name, Type)]
c1, (Name
n2, Type
ty2) <- [(Name, Type)]
c2, let subst2for1 :: Type -> Type
subst2for1 = Name -> Type -> Type -> Type
forall n. Eq n => n -> TT n -> TT n -> TT n
psubst Name
n2 (NameType -> Name -> Type -> Type
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n1 Type
ty1)]

    -- try to hunt match an interface constraint by replacing it with an implementation
    results4 :: [State]
results4 = [ [(Name, Type)]
-> Sided (ArgsDAG, [(Name, Type)]) -> Score -> [Name] -> State
State [] ((([(Name, Type)], AsymMods, [Name]) -> (ArgsDAG, [(Name, Type)]))
-> Sided ([(Name, Type)], AsymMods, [Name])
-> Sided (ArgsDAG, [(Name, Type)])
forall a b. (a -> b) -> Sided a -> Sided b
both (\([(Name, Type)]
cs, AsymMods
_, [Name]
_) -> ([], [(Name, Type)]
cs)) Sided ([(Name, Type)], AsymMods, [Name])
sds)
               (Score
scoreAcc Score -> Score -> Score
forall a. Monoid a => a -> a -> a
`mappend` Int -> Int -> Sided AsymMods -> Score
Score Int
0 Int
0 ((([(Name, Type)], AsymMods, [Name]) -> AsymMods)
-> Sided ([(Name, Type)], AsymMods, [Name]) -> Sided AsymMods
forall a b. (a -> b) -> Sided a -> Sided b
both (\([(Name, Type)]
_, AsymMods
amods, [Name]
_) -> AsymMods
amods) Sided ([(Name, Type)], AsymMods, [Name])
sds))
               ([Name]
usedns [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ ([Name] -> [Name] -> [Name]) -> Sided [Name] -> [Name]
forall a b. (a -> a -> b) -> Sided a -> b
sided [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
(++) ((([(Name, Type)], AsymMods, [Name]) -> [Name])
-> Sided ([(Name, Type)], AsymMods, [Name]) -> Sided [Name]
forall a b. (a -> b) -> Sided a -> Sided b
both (\([(Name, Type)]
_, AsymMods
_, [Name]
hs) -> [Name]
hs) Sided ([(Name, Type)], AsymMods, [Name])
sds))
               | Sided ([(Name, Type)], AsymMods, [Name])
sds <- [Sided ([(Name, Type)], AsymMods, [Name])]
allMods ]
      where
      allMods :: [Sided ([(Name, Type)], AsymMods, [Name])]
allMods = Sided ([(Name, Type)], AsymMods, [Name])
-> Sided [([(Name, Type)], AsymMods, [Name])]
-> [Sided ([(Name, Type)], AsymMods, [Name])]
forall a. Sided a -> Sided [a] -> [Sided a]
parallel Sided ([(Name, Type)], AsymMods, [Name])
defMod Sided [([(Name, Type)], AsymMods, [Name])]
mods
      mods :: Sided [( Interfaces, AsymMods, [Name] )]
      mods :: Sided [([(Name, Type)], AsymMods, [Name])]
mods = ((ArgsDAG, [(Name, Type)]) -> [([(Name, Type)], AsymMods, [Name])])
-> Sided (ArgsDAG, [(Name, Type)])
-> Sided [([(Name, Type)], AsymMods, [Name])]
forall a b. (a -> b) -> Sided a -> Sided b
both ([(Name, Type)] -> [([(Name, Type)], AsymMods, [Name])]
implementationMods ([(Name, Type)] -> [([(Name, Type)], AsymMods, [Name])])
-> ((ArgsDAG, [(Name, Type)]) -> [(Name, Type)])
-> (ArgsDAG, [(Name, Type)])
-> [([(Name, Type)], AsymMods, [Name])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ArgsDAG, [(Name, Type)]) -> [(Name, Type)]
forall a b. (a, b) -> b
snd) Sided (ArgsDAG, [(Name, Type)])
unresolved
      defMod :: Sided (Interfaces, AsymMods, [Name])
      defMod :: Sided ([(Name, Type)], AsymMods, [Name])
defMod = ((ArgsDAG, [(Name, Type)]) -> ([(Name, Type)], AsymMods, [Name]))
-> Sided (ArgsDAG, [(Name, Type)])
-> Sided ([(Name, Type)], AsymMods, [Name])
forall a b. (a -> b) -> Sided a -> Sided b
both (\(ArgsDAG
_, [(Name, Type)]
cs) -> ([(Name, Type)]
cs, AsymMods
forall a. Monoid a => a
mempty , [])) Sided (ArgsDAG, [(Name, Type)])
unresolved
      parallel :: Sided a -> Sided [a] -> [Sided a]
      parallel :: forall a. Sided a -> Sided [a] -> [Sided a]
parallel (Sided a
l a
r) (Sided [a]
ls [a]
rs) = (a -> Sided a) -> [a] -> [Sided a]
forall a b. (a -> b) -> [a] -> [b]
map ((a -> a -> Sided a) -> a -> a -> Sided a
forall a b c. (a -> b -> c) -> b -> a -> c
flip a -> a -> Sided a
forall a. a -> a -> Sided a
Sided a
r) [a]
ls [Sided a] -> [Sided a] -> [Sided a]
forall a. [a] -> [a] -> [a]
++ (a -> Sided a) -> [a] -> [Sided a]
forall a b. (a -> b) -> [a] -> [b]
map (a -> a -> Sided a
forall a. a -> a -> Sided a
Sided a
l) [a]
rs
      implementationMods :: Interfaces -> [( Interfaces , AsymMods, [Name] )]
      implementationMods :: [(Name, Type)] -> [([(Name, Type)], AsymMods, [Name])]
implementationMods [(Name, Type)]
interfaces = [ ( [(Name, Type)]
newInterfaceArgs, AsymMods
forall a. Monoid a => a
mempty { interfaceApp = 1 }, [Name]
newHoles )
                                      | (Name
_, Type
ty) <- [(Name, Type)]
interfaces
                                      , Type
impl <- [Name] -> Type -> [Type]
possInterfaceImplementations [Name]
usedns Type
ty
                                      , [(Name, Type)]
newInterfaceArgs <- Maybe [(Name, Type)] -> [[(Name, Type)]]
forall a. Maybe a -> [a]
maybeToList (Maybe [(Name, Type)] -> [[(Name, Type)]])
-> Maybe [(Name, Type)] -> [[(Name, Type)]]
forall a b. (a -> b) -> a -> b
$ Ctxt InterfaceInfo
-> Context -> Type -> Type -> Maybe [(Name, Type)]
interfaceUnify Ctxt InterfaceInfo
interfaceInfo Context
ctxt Type
ty Type
impl
                                      , let newHoles :: [Name]
newHoles = ((Name, Type) -> Name) -> [(Name, Type)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Type) -> Name
forall a b. (a, b) -> a
fst [(Name, Type)]
newInterfaceArgs ]


  -- Stage 1 - match arguments
  nextSteps (State [(Name, Type)]
hs (Sided (ArgsDAG
dagL, [(Name, Type)]
c1) (ArgsDAG
dagR, [(Name, Type)]
c2)) Score
scoreAcc [Name]
usedns) = [State]
results where

    results :: [State]
results = (State -> [State]) -> [State] -> [State]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap State -> [State]
takeSomeInterfaces [State]
results1

    -- we only try to match arguments whose names don't appear in the types
    -- of any other arguments
    canBeFirst :: ArgsDAG -> [(Name, Type)]
    canBeFirst :: ArgsDAG -> [(Name, Type)]
canBeFirst = (((Name, Type), (Int, Set Name)) -> (Name, Type))
-> ArgsDAG -> [(Name, Type)]
forall a b. (a -> b) -> [a] -> [b]
map ((Name, Type), (Int, Set Name)) -> (Name, Type)
forall a b. (a, b) -> a
fst (ArgsDAG -> [(Name, Type)])
-> (ArgsDAG -> ArgsDAG) -> ArgsDAG -> [(Name, Type)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (((Name, Type), (Int, Set Name)) -> Bool) -> ArgsDAG -> ArgsDAG
forall a. (a -> Bool) -> [a] -> [a]
filter (Set Name -> Bool
forall a. Set a -> Bool
S.null (Set Name -> Bool)
-> (((Name, Type), (Int, Set Name)) -> Set Name)
-> ((Name, Type), (Int, Set Name))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, Set Name) -> Set Name
forall a b. (a, b) -> b
snd ((Int, Set Name) -> Set Name)
-> (((Name, Type), (Int, Set Name)) -> (Int, Set Name))
-> ((Name, Type), (Int, Set Name))
-> Set Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Name, Type), (Int, Set Name)) -> (Int, Set Name)
forall a b. (a, b) -> b
snd)

    -- try to match an argument from the left with an argument from the right
    results1 :: [State]
results1 = [Maybe State] -> [State]
forall a. [Maybe a] -> [a]
catMaybes [ State -> [(Type, Type)] -> Maybe State
unifyQueue ([(Name, Type)]
-> Sided (ArgsDAG, [(Name, Type)]) -> Score -> [Name] -> State
State (((Name, Type) -> Bool) -> [(Name, Type)] -> [(Name, Type)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> ((Name, Type) -> Bool) -> (Name, Type) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name
n1,Name
n2]) (Name -> Bool) -> ((Name, Type) -> Name) -> (Name, Type) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, Type) -> Name
forall a b. (a, b) -> a
fst) [(Name, Type)]
hs)
         ((ArgsDAG, [(Name, Type)])
-> (ArgsDAG, [(Name, Type)]) -> Sided (ArgsDAG, [(Name, Type)])
forall a. a -> a -> Sided a
Sided (Name -> ArgsDAG -> ArgsDAG
forall n a.
Ord n =>
n -> [((n, TT n), (a, Set n))] -> [((n, TT n), (a, Set n))]
deleteFromDag Name
n1 ArgsDAG
dagL, [(Name, Type)]
c1)
                ((Type -> Type) -> ArgsDAG -> ArgsDAG
inArgTys Type -> Type
subst2for1 (ArgsDAG -> ArgsDAG) -> ArgsDAG -> ArgsDAG
forall a b. (a -> b) -> a -> b
$ Name -> ArgsDAG -> ArgsDAG
forall n a.
Ord n =>
n -> [((n, TT n), (a, Set n))] -> [((n, TT n), (a, Set n))]
deleteFromDag Name
n2 ArgsDAG
dagR, ((Name, Type) -> (Name, Type)) -> [(Name, Type)] -> [(Name, Type)]
forall a b. (a -> b) -> [a] -> [b]
map ((Type -> Type) -> (Name, Type) -> (Name, Type)
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second Type -> Type
subst2for1) [(Name, Type)]
c2))
          Score
scoreAcc [Name]
usedns) [(Type
ty1, Type
ty2)]
     | (Name
n1, Type
ty1) <- ArgsDAG -> [(Name, Type)]
canBeFirst ArgsDAG
dagL, (Name
n2, Type
ty2) <- ArgsDAG -> [(Name, Type)]
canBeFirst ArgsDAG
dagR
     , let subst2for1 :: Type -> Type
subst2for1 = Name -> Type -> Type -> Type
forall n. Eq n => n -> TT n -> TT n -> TT n
psubst Name
n2 (NameType -> Name -> Type -> Type
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n1 Type
ty1)]



  -- Stage 2 - simply introduce a subset of the interfaces
  -- we've finished, so take some interfaces
  takeSomeInterfaces :: State -> [State]
takeSomeInterfaces (State [] unresolved :: Sided (ArgsDAG, [(Name, Type)])
unresolved@(Sided ([], [(Name, Type)]
_) ([], [(Name, Type)]
_)) Score
scoreAcc [Name]
usedns) =
    (Sided ([(Name, Type)], AsymMods) -> State)
-> [Sided ([(Name, Type)], AsymMods)] -> [State]
forall a b. (a -> b) -> [a] -> [b]
map Sided ([(Name, Type)], AsymMods) -> State
statesFromMods ([Sided ([(Name, Type)], AsymMods)] -> [State])
-> (Sided [([(Name, Type)], AsymMods)]
    -> [Sided ([(Name, Type)], AsymMods)])
-> Sided [([(Name, Type)], AsymMods)]
-> [State]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sided [([(Name, Type)], AsymMods)]
-> [Sided ([(Name, Type)], AsymMods)]
forall a. Sided [a] -> [Sided a]
prod (Sided [([(Name, Type)], AsymMods)] -> [State])
-> Sided [([(Name, Type)], AsymMods)] -> [State]
forall a b. (a -> b) -> a -> b
$ ((ArgsDAG, [(Name, Type)]) -> [([(Name, Type)], AsymMods)])
-> Sided (ArgsDAG, [(Name, Type)])
-> Sided [([(Name, Type)], AsymMods)]
forall a b. (a -> b) -> Sided a -> Sided b
both ([(Name, Type)] -> [([(Name, Type)], AsymMods)]
interfaceMods ([(Name, Type)] -> [([(Name, Type)], AsymMods)])
-> ((ArgsDAG, [(Name, Type)]) -> [(Name, Type)])
-> (ArgsDAG, [(Name, Type)])
-> [([(Name, Type)], AsymMods)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ArgsDAG, [(Name, Type)]) -> [(Name, Type)]
forall a b. (a, b) -> b
snd) Sided (ArgsDAG, [(Name, Type)])
unresolved
    where
    swap :: Sided a -> Sided a
swap (Sided a
l a
r) = a -> a -> Sided a
forall a. a -> a -> Sided a
Sided a
r a
l
    statesFromMods :: Sided (Interfaces, AsymMods) -> State
    statesFromMods :: Sided ([(Name, Type)], AsymMods) -> State
statesFromMods Sided ([(Name, Type)], AsymMods)
sides = let interfaces :: Sided ([a], [(Name, Type)])
interfaces = (([(Name, Type)], AsymMods) -> ([a], [(Name, Type)]))
-> Sided ([(Name, Type)], AsymMods) -> Sided ([a], [(Name, Type)])
forall a b. (a -> b) -> Sided a -> Sided b
both (\([(Name, Type)]
c, AsymMods
_) -> ([], [(Name, Type)]
c)) Sided ([(Name, Type)], AsymMods)
sides
                               mods :: Sided AsymMods
mods    = Sided AsymMods -> Sided AsymMods
forall {a}. Sided a -> Sided a
swap ((([(Name, Type)], AsymMods) -> AsymMods)
-> Sided ([(Name, Type)], AsymMods) -> Sided AsymMods
forall a b. (a -> b) -> Sided a -> Sided b
both ([(Name, Type)], AsymMods) -> AsymMods
forall a b. (a, b) -> b
snd Sided ([(Name, Type)], AsymMods)
sides) in
      [(Name, Type)]
-> Sided (ArgsDAG, [(Name, Type)]) -> Score -> [Name] -> State
State [] Sided (ArgsDAG, [(Name, Type)])
forall {a}. Sided ([a], [(Name, Type)])
interfaces (Score
scoreAcc Score -> Score -> Score
forall a. Monoid a => a -> a -> a
`mappend` (Score
forall a. Monoid a => a
mempty { asymMods = mods })) [Name]
usedns
    interfaceMods :: Interfaces -> [(Interfaces, AsymMods)]
    interfaceMods :: [(Name, Type)] -> [([(Name, Type)], AsymMods)]
interfaceMods [(Name, Type)]
cs = let lcs :: Int
lcs = [(Name, Type)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Name, Type)]
cs in
      [ ([(Name, Type)]
cs', AsymMods
forall a. Monoid a => a
mempty { interfaceIntro = lcs - length cs' }) | [(Name, Type)]
cs' <- [(Name, Type)] -> [[(Name, Type)]]
forall a. [a] -> [[a]]
subsets [(Name, Type)]
cs ]
    prod :: Sided [a] -> [Sided a]
    prod :: forall a. Sided [a] -> [Sided a]
prod (Sided [a]
ls [a]
rs) = [a -> a -> Sided a
forall a. a -> a -> Sided a
Sided a
l a
r | a
l <- [a]
ls, a
r <- [a]
rs]
  -- still have arguments to match, so just be the identity
  takeSomeInterfaces State
s = [State
s]