{-|
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
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PkgName]
pkgs)) forall a b. (a -> b) -> a -> b
$
     String -> Idris ()
iputStrLn forall a b. (a -> b) -> a -> b
$ String
"Searching packages: " forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
showSep String
", " (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [PkgName]
pkgs)

  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 (forall a b. (a, b) -> a
fst forall a. (Docstring a, [(Name, Docstring a)])
noDocs) (forall a b. (a, b) -> b
snd forall a. (Docstring a, [(Name, Docstring a)])
noDocs) FC
emptyFC [] Name
name FC
NoFC PTerm
pterm'
  let names :: [(Name, Score)]
names = 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' = 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, forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. Docstring a -> Docstring a
overview forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) (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 forall a. Doc a -> Doc a -> Doc a
<> forall a. Char -> Doc a
char Char
' ' 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 (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Doc OutputAnnotation]
docs))
     then case IState -> OutputMode
idris_outputmode IState
i of
               RawOutput Handle
_  -> do 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 (forall a. [Doc a] -> Doc a
vsep [Doc OutputAnnotation]
docs)
     else Doc OutputAnnotation -> Idris ()
iRenderError forall a b. (a -> b) -> a -> b
$ 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 :: Bool
implicitAllowed = Bool
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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [a]
M.elems forall a b. (a -> b) -> a -> b
$
  forall k a b. (k -> a -> b) -> Map k a -> Map k b
M.mapWithKey (\Name
key -> forall k a. Map k a -> [(k, a)]
M.toAscList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b k. (a -> Maybe b) -> Map k a -> Map k b
M.mapMaybe (forall {r} {i} {b} {c} {d}.
Name -> (Def, r, i, b, c, d) -> Maybe Type
f Name
key)) (Context
-> Ctxt
     (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
    forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Name -> Bool
special Name
k)
    Type
type2 <- forall r i b c d. (Def, r, i, b, c, d) -> Maybe Type
typeFromDef (Def, r, i, b, c, d)
x
    forall (m :: * -> *) a. Monad m => a -> m a
return 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 forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` 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 = forall {info}. [(info, Type)] -> [(info, Score)]
matcher where
  maxScore :: Int
maxScore = Int
100
  matcher :: [(info, Type)] -> [(info, Score)]
matcher = 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
_) = forall a. a -> Maybe a
Just Type
ty
  get (TyDecl NameType
_ Type
ty) = 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
_)  = forall a. a -> Maybe a
Just Type
ty
  get Def
_ = 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 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 -> forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
name (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 -> 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 -> 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 = forall a b. (a -> b) -> [a] -> [b]
map 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), forall a. Ord a => [a] -> Set a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Ord a => a -> Set a -> Bool
S.member k
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = (forall a. [a] -> [a]
reverse (forall a b. (a -> b) -> [a] -> [b]
map forall {k} {a}. Ord k => (a, TT k) -> ((a, TT k), Set k)
f [(n, TT n)]
arguments), 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), forall k a. Map k a -> Set k
M.keysSet (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 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 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 = 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) = forall k a. k -> a -> Map k a
M.singleton n
n (TT n
t, Bool
b) 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) = (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) forall k a. Ord k => Map k a -> Map k a -> Map k a
`M.union`) 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 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 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 (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 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
&& 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
_) = forall a. HasCallStack => String -> a
error String
"unexpected! run vToP first"
  f Bool
_ TT n
_ = 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 forall a. Eq a => a -> a -> Bool
== n
name2
  then forall a. a -> a
id
  else (((n
name2, TT n
ty) , (a
ix, forall a. Ord a => a -> Set a -> Set a
S.delete n
name Set n
set)) forall a. a -> [a] -> [a]
:) ) (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 = forall a. (a -> Bool) -> [a] -> [a]
filter ((forall a. Eq a => a -> a -> Bool
/= n
n) forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: AsymMods -> AsymMods -> Bool
$c/= :: AsymMods -> AsymMods -> Bool
== :: AsymMods -> AsymMods -> Bool
$c== :: AsymMods -> AsymMods -> Bool
Eq, Int -> AsymMods -> ShowS
[AsymMods] -> ShowS
AsymMods -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [AsymMods] -> ShowS
$cshowList :: [AsymMods] -> ShowS
show :: AsymMods -> String
$cshow :: AsymMods -> String
showsPrec :: Int -> AsymMods -> ShowS
$cshowsPrec :: Int -> AsymMods -> ShowS
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
forall a. Eq a => Sided a -> Sided a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Sided a -> Sided a -> Bool
$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
Eq, Int -> Sided a -> ShowS
forall a. Show a => Int -> Sided a -> ShowS
forall a. Show a => [Sided a] -> ShowS
forall a. Show a => Sided a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Sided a] -> ShowS
$cshowList :: forall a. Show a => [Sided a] -> ShowS
show :: Sided a -> String
$cshow :: forall a. Show a => Sided a -> String
showsPrec :: Int -> Sided a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Sided a -> ShowS
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) = 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
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Score -> Score -> Bool
$c/= :: Score -> Score -> Bool
== :: Score -> Score -> Bool
$c== :: Score -> Score -> Bool
Eq, Int -> Score -> ShowS
[Score] -> ShowS
Score -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Score] -> ShowS
$cshowList :: [Score] -> ShowS
show :: Score -> String
$cshow :: Score -> String
showsPrec :: Int -> Score -> ShowS
$cshowsPrec :: Int -> Score -> ShowS
Show)

displayScore :: Score -> Doc OutputAnnotation
displayScore :: Score -> Doc OutputAnnotation
displayScore Score
score = case 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 -> forall a. String -> Doc a
text String
"_"
  where
  annotated :: Ordering -> String -> Doc OutputAnnotation
annotated Ordering
ordr = forall a. a -> Doc a -> Doc a
annotate (Ordering -> OutputAnnotation
AnnSearchResult Ordering
ordr) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. String -> Doc a
text
  noMods :: AsymMods -> Bool
noMods (Mods Int
app Int
tcApp Int
tcIntro) = Int
app forall a. Num a => a -> a -> a
+ Int
tcApp forall a. Num a => a -> a -> a
+ Int
tcIntro 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
  (  forall a b. (a -> a -> b) -> Sided a -> b
sided Bool -> Bool -> Bool
(&&) (forall a b. (a -> b) -> Sided a -> Sided b
both ((forall a. Ord a => a -> a -> Bool
> Int
0) forall b c a. (b -> c) -> (a -> b) -> a -> c
. AsymMods -> Int
argApp) Sided AsymMods
amods)
  Bool -> Bool -> Bool
|| forall a b. (a -> a -> b) -> Sided a -> b
sided forall a. Num a => a -> a -> a
(+) (forall a b. (a -> b) -> Sided a -> Sided b
both AsymMods -> Int
argApp Sided AsymMods
amods) forall a. Ord a => a -> a -> Bool
> Int
4
  Bool -> Bool -> Bool
|| forall a b. (a -> a -> b) -> Sided a -> b
sided Bool -> Bool -> Bool
(||) (forall a b. (a -> b) -> Sided a -> Sided b
both (\(Mods Int
_ Int
tcApp Int
tcIntro) -> Int
tcApp forall a. Ord a => a -> a -> Bool
> Int
3 Bool -> Bool -> Bool
|| Int
tcIntro 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 forall a. Num a => a -> a -> a
+ Int
eqFlip forall a. Num a => a -> a -> a
+ Int
linearPenalty 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 forall a. Num a => a -> a -> a
* Int
l forall a. Num a => a -> a -> a
+ Int
r)
    (forall a b. (a -> b) -> Sided a -> Sided b
both (\(Mods Int
app Int
tcApp Int
tcIntro) -> Int
3 forall a. Num a => a -> a -> a
* Int
app forall a. Num a => a -> a -> a
+ Int
4 forall a. Num a => a -> a -> a
* Int
tcApp forall a. Num a => a -> a -> a
+ Int
2 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 forall a. Num a => a -> a -> a
*
    forall a b. (a -> a -> b) -> Sided a -> b
sided forall a. Num a => a -> a -> a
(*) (forall a b. (a -> b) -> Sided a -> Sided b
both (\(Mods Int
app Int
tcApp Int
tcIntro) -> Int
2 forall a. Num a => a -> a -> a
* Int
app forall a. Num a => a -> a -> a
+ Int
tcApp forall a. Num a => a -> a -> a
+ Int
tcIntro) Sided AsymMods
amods)

instance Ord Score where
  compare :: Score -> Score -> Ordering
compare = 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) = forall a. a -> a -> Sided a
Sided (a
l1 forall a. Semigroup a => a -> a -> a
S.<> a
l2) (a
r1 forall a. Semigroup a => a -> a -> a
S.<> a
r2)

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

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

instance Monoid a => Monoid (Sided a) where
  mempty :: Sided a
mempty = forall a. a -> a -> Sided a
Sided forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty
  (Sided a
l1 a
r1) mappend :: Sided a -> Sided a -> Sided a
`mappend` (Sided a
l2 a
r2) = forall a. a -> a -> Sided a
Sided (a
l1 forall a. Monoid a => a -> a -> a
`mappend` a
l2) (a
r1 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 forall a. Num a => a -> a -> a
+ Int
a') (Int
b forall a. Num a => a -> a -> a
+ Int
b') (Int
c 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 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 forall a. Num a => a -> a -> a
+ Int
t') (Int
e forall a. Num a => a -> a -> a
+ Int
e') (Sided AsymMods
mods 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 -> ShowS
[State] -> ShowS
State -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [State] -> ShowS
$cshowList :: [State] -> ShowS
show :: State -> String
$cshow :: State -> String
showsPrec :: Int -> State -> ShowS
$cshowsPrec :: Int -> State -> ShowS
Show

modifyTypes :: (Type -> Type) -> (ArgsDAG, Interfaces) -> (ArgsDAG, Interfaces)
modifyTypes :: (Type -> Type)
-> (ArgsDAG, [(Name, Type)]) -> (ArgsDAG, [(Name, Type)])
modifyTypes Type -> Type
f = forall {d} {d}. [((d, Type), d)] -> [((d, Type), d)]
modifyDag forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** forall {d}. [(d, Type)] -> [(d, Type)]
modifyList
  where
  modifyDag :: [((d, Type), d)] -> [((d, Type), d)]
modifyDag = forall a b. (a -> b) -> [a] -> [b]
map (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (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 = forall a b. (a -> b) -> [a] -> [b]
map (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 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& (forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((Name
name forall a. Eq a => a -> a -> Bool
==) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ((,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, Type)]
interfaces forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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) = (forall n a.
Ord n =>
n -> [((n, TT n), (a, Set n))] -> [((n, TT n), (a, Set n))]
deleteFromDag Name
n ArgsDAG
args, forall a. (a -> Bool) -> [a] -> [a]
filter ((forall a. Eq a => a -> a -> Bool
/= Name
n) forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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) = forall a. a -> Maybe a
Just a
x
tcToMaybe (Error Err
_) = forall a. Maybe a
Nothing

inArgTys :: (Type -> Type) -> ArgsDAG -> ArgsDAG
inArgTys :: (Type -> Type) -> ArgsDAG -> ArgsDAG
inArgTys = forall a b. (a -> b) -> [a] -> [b]
map forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first forall b c a. (b -> c) -> (a -> b) -> a -> 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 <- forall a. TC a -> Maybe a
tcToMaybe 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, forall a. Maybe a
Nothing) (Type
retTy, forall a. Maybe a
Nothing) [] [Name]
theHoles []
  forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Name]
theHoles forall a. Eq a => [a] -> [a] -> [a]
\\ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, Type)]
res)
  let argTys' :: [(Name, Type)]
argTys' = forall a b. (a -> b) -> [a] -> [b]
map (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) forall a. a -> a
id [ 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
  forall (m :: * -> *) a. Monad m => a -> m a
return [(Name, Type)]
argTys'
  where
  tyTry' :: Type
tyTry' = forall n. TT n -> TT n
vToP Type
tyTry
  theHoles :: [Name]
theHoles = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, Type)]
nonTcArgs
  retTy :: Type
retTy = forall n. TT n -> TT n
getRetTy Type
tyTry'
  ([(Name, Type)]
tcArgs, [(Name, Type)]
nonTcArgs) = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Ctxt InterfaceInfo -> Type -> Bool
isInterfaceArg Ctxt InterfaceInfo
interfaceInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) forall a b. (a -> b) -> a -> b
$ 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 (forall (t :: * -> *) a. Foldable t => t a -> Bool
null (forall {a}. TT a -> [a]
getInterfaceName Type
clss forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a. Name -> Ctxt a -> [a]
lookupCtxt Ctxt InterfaceInfo
interfaceInfo)) where
  (Type
clss, [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 = forall a. [a] -> [[a]]
subsets [a]
xs in forall a b. (a -> b) -> [a] -> [b]
map (a
x forall a. a -> [a] -> [a]
:) [[a]]
ss 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 forall a. Eq a => a -> a -> Bool
== Name
eqTy ->
    [(Int
0, Type
eq1), (Int
1, forall {n}. TT n -> TT n -> TT n
app (forall {n}. TT n -> TT n -> TT n
app (forall {n}. TT n -> TT n -> TT n
app (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') -> (forall a b. (a, b) -> a
fst (forall b. Binder b -> b
binderTy Binder (Int, Type)
bind') forall a. Num a => a -> a -> a
+ Int
j, forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> b
snd Binder (Int, Type)
bind') Type
sc'))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Type -> [(Int, Type)]
flipEqualities Binder Type
binder 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 forall a. Num a => a -> a -> a
+ Int
j, forall {n}. TT n -> TT n -> TT n
app Type
f' Type
x'))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> [(Int, Type)]
flipEqualities Type
f 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 = forall n. AppStatus n -> TT n -> TT n -> TT n
App 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 forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Int, ArgsDAG, Type) -> Maybe (Score, State)
startStates [(Int, ArgsDAG, Type)]
ty2s of
    [] -> forall a. Maybe a
Nothing
    [(Score, State)]
xs -> forall a. a -> Maybe a
Just (forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Score, State)]
xs), (info
info, 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 forall a. Num a => a -> a -> a
+ Int
j, ArgsDAG
dag, Type
retTy))
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {a} {a} {b}.
[((a, Type), (a, b))] -> [(Int, [((a, Type), (a, b))])]
flipEqualitiesDag ArgsDAG
dag2 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 forall a. Num a => a -> a -> a
+ Int
j , ((a
n, Type
ty'), (a
pos, b
deps)) forall a. a -> [a] -> [a]
: [((a, Type), (a, b))]
xs'))
           forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> [(Int, Type)]
flipEqualities Type
ty 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
                (forall a. a -> a -> Sided a
Sided (ArgsDAG
dag1, [(Name, Type)]
interfaceArgs1) (ArgsDAG
sndDag, [(Name, Type)]
interfaceArgs2))
                (forall a. Monoid a => a
mempty { equalityFlips :: Int
equalityFlips = Int
numEqFlips }) [Name]
usedns) [(Type
retTy1, Type
sndRetTy)]
      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 (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, Type)]
argNames1) Type
type2)
    argNames2 :: [(Name, Type)]
argNames2 = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst ArgsDAG
dag2
    usedns :: [Name]
usedns = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, Type)]
startingHoles
    startingHoles :: [(Name, Type)]
startingHoles = [(Name, Type)]
argNames1 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 = forall k v. Ord k => [(k, v)] -> PQueue k v
Q.fromList forall a b. (a -> b) -> a -> b
$ 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 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 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 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 (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) 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 = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst ArgsDAG
dag1
  makeDag :: Type -> (ArgsDAG, Interfaces, Type)
  makeDag :: Type -> (ArgsDAG, [(Name, Type)], Type)
makeDag = forall {t} {a} {b} {c}. (t -> a) -> (t, b, c) -> (a, b, c)
first3 (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..] forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Ord k => [((k, a), Set k)] -> [((k, a), Set k)]
reverseDag) forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    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) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n. TT n -> TT n
vToP 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 = 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 | 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 = forall a. a -> Maybe a -> a
fromMaybe Int
0 (forall a. Num a => a -> a
abs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((-) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Int
ix1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe Int
ix2))
    forall (m :: * -> *) a. Monad m => a -> m a
return ((Score -> Score) -> State -> State
inScore (\Score
s -> Score
s { transposition :: Int
transposition = Score -> Int
transposition Score
s forall a. Num a => a -> a -> a
+ Int
transScore }) State
state'', (Type
ty1, Type
ty2) 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 :: Score
score = Score -> Score
f (State -> Score
score State
stat) }
    findArgs :: Maybe ((Type, Maybe Int), (Type, Maybe Int))
findArgs = ((,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> (ArgsDAG, [(Name, Type)]) -> Maybe (Type, Maybe Int)
findName Name
name  (forall a. Sided a -> a
left Sided (ArgsDAG, [(Name, Type)])
unresolved) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Name -> (ArgsDAG, [(Name, Type)]) -> Maybe (Type, Maybe Int)
findName Name
name2 (forall a. Sided a -> a
right Sided (ArgsDAG, [(Name, Type)])
unresolved)) forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
               ((,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> (ArgsDAG, [(Name, Type)]) -> Maybe (Type, Maybe Int)
findName Name
name2 (forall a. Sided a -> a
left Sided (ArgsDAG, [(Name, Type)])
unresolved) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Name -> (ArgsDAG, [(Name, Type)]) -> Maybe (Type, Maybe Int)
findName Name
name  (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 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 :: [(Name, Type)]
holes = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
matchnames) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) (State -> [(Name, Type)]
holes State
state)
                   , argsAndInterfaces :: Sided (ArgsDAG, [(Name, Type)])
argsAndInterfaces = forall a b. (a -> b) -> Sided a -> Sided b
both ((Type -> Type)
-> (ArgsDAG, [(Name, Type)]) -> (ArgsDAG, [(Name, Type)])
modifyTypes (forall n. Eq n => n -> TT n -> TT n -> TT n
subst Name
name Type
term) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ArgsDAG, [(Name, Type)]) -> (ArgsDAG, [(Name, Type)])
deleteArgs) Sided (ArgsDAG, [(Name, Type)])
unresolved}

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

    otherApplied :: Int
otherApplied = 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 :: Score
score = let s :: Score
s = State -> Score
score State
theState in
      Score
s { asymMods :: Sided AsymMods
asymMods = Score -> Sided AsymMods
asymMods Score
s forall a. Monoid a => a -> a -> a
`mappend` Sided AsymMods
additions } }
    state' :: State
state' = State
state { holes :: [(Name, Type)]
holes = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
toDelete) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(Name, Type)]
hs
                   , argsAndInterfaces :: Sided (ArgsDAG, [(Name, Type)])
argsAndInterfaces = forall a b. (a -> b) -> Sided a -> Sided b
both ((Type -> Type)
-> (ArgsDAG, [(Name, Type)]) -> (ArgsDAG, [(Name, Type)])
modifyTypes (forall n. Eq n => n -> TT n -> TT n -> TT n
subst Name
name Type
term) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ArgsDAG, [(Name, Type)]) -> (ArgsDAG, [(Name, Type)])
deleteMany) (State -> Sided (ArgsDAG, [(Name, Type)])
argsAndInterfaces State
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 [] = 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 <- forall a. TC a -> Maybe a
tcToMaybe 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, forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
RigW forall a. Maybe a
Nothing Type
ty (forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] Int
0))) | (Name
n, Type
ty) <- State -> [(Name, Type)]
holes State
state]
                                   (Type
ty1, forall a. Maybe a
Nothing)
                                   (Type
ty2, forall a. Maybe a
Nothing) [] (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst 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
    forall (f :: * -> *). Alternative f => Bool -> f ()
guard 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 forall a. [a] -> [a] -> [a]
++ [(Type, Type)]
queueAdditions)

  possInterfaceImplementations :: [Name] -> Type -> [Type]
  possInterfaceImplementations :: [Name] -> Type -> [Type]
possInterfaceImplementations [Name]
usedns Type
ty = do
    Name
interfaceName <- forall {a}. TT a -> [a]
getInterfaceName Type
clss
    InterfaceInfo
interfaceDef <- 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 <- forall a. Name -> Ctxt a -> [a]
lookupCtxt (forall a b. (a, b) -> a
fst (Name, Bool)
n) (Context
-> Ctxt
     (Def, RigCount, Bool, Accessibility, Totality, MetaInformation)
definitions Context
ctxt)
    Type
nty <- Context -> Env -> Type -> Type
normaliseC Context
ctxt [] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (case 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' = forall n. TT n -> TT n
vToP ([Name] -> Type -> Type
uniqueBinders [Name]
usedns Type
nty)
    forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty'
    where
    (Type
clss, [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) <- forall k v. Ord k => PQueue k v -> Maybe ((k, v), PQueue k v)
Q.minViewWithKey PQueue Score State
queue
    forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ if State -> Bool
isFinal State
next
      then forall a b. b -> Either a b
Right Score
nextScore
      else let additions :: PQueue Score State
additions = if Score -> Bool
scoreCriterion Score
nextScore
                 then 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 forall k v. Ord k => PQueue k v
Q.empty in
           forall a b. a -> Either a b
Left (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 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 =
         forall a. [Maybe a] -> [a]
catMaybes [ State -> [(Type, Type)] -> Maybe State
unifyQueue ([(Name, Type)]
-> Sided (ArgsDAG, [(Name, Type)]) -> Score -> [Name] -> State
State []
         (forall a. a -> a -> Sided a
Sided ([], forall n. Ord n => n -> [(n, TT n)] -> [(n, TT n)]
deleteFromArgList Name
n1 [(Name, Type)]
c1)
                ([], forall a b. (a -> b) -> [a] -> [b]
map (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second Type -> Type
subst2for1) (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 = forall n. Eq n => n -> TT n -> TT n -> TT n
psubst Name
n2 (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 [] (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 forall a. Monoid a => a -> a -> a
`mappend` Int -> Int -> Sided AsymMods -> Score
Score Int
0 Int
0 (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 forall a. [a] -> [a] -> [a]
++ forall a b. (a -> a -> b) -> Sided a -> b
sided forall a. [a] -> [a] -> [a]
(++) (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 = 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 = forall a b. (a -> b) -> Sided a -> Sided b
both ([(Name, Type)] -> [([(Name, Type)], AsymMods, [Name])]
implementationMods forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) Sided (ArgsDAG, [(Name, Type)])
unresolved
      defMod :: Sided (Interfaces, AsymMods, [Name])
      defMod :: Sided ([(Name, Type)], AsymMods, [Name])
defMod = forall a b. (a -> b) -> Sided a -> Sided b
both (\(ArgsDAG
_, [(Name, Type)]
cs) -> ([(Name, Type)]
cs, 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) = forall a b. (a -> b) -> [a] -> [b]
map (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a. a -> a -> Sided a
Sided a
r) [a]
ls forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (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, forall a. Monoid a => a
mempty { interfaceApp :: Int
interfaceApp = Int
1 }, [Name]
newHoles )
                                      | (Name
_, Type
ty) <- [(Name, Type)]
interfaces
                                      , Type
impl <- [Name] -> Type -> [Type]
possInterfaceImplementations [Name]
usedns Type
ty
                                      , [(Name, Type)]
newInterfaceArgs <- forall a. Maybe a -> [a]
maybeToList 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 = forall a b. (a -> b) -> [a] -> [b]
map 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 = 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 = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Set a -> Bool
S.null forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd)

    -- try to match an argument from the left with an argument from the right
    results1 :: [State]
results1 = forall a. [Maybe a] -> [a]
catMaybes [ State -> [(Type, Type)] -> Maybe State
unifyQueue ([(Name, Type)]
-> Sided (ArgsDAG, [(Name, Type)]) -> Score -> [Name] -> State
State (forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name
n1,Name
n2]) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(Name, Type)]
hs)
         (forall a. a -> a -> Sided a
Sided (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 forall a b. (a -> b) -> a -> b
$ forall n a.
Ord n =>
n -> [((n, TT n), (a, Set n))] -> [((n, TT n), (a, Set n))]
deleteFromDag Name
n2 ArgsDAG
dagR, forall a b. (a -> b) -> [a] -> [b]
map (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 = forall n. Eq n => n -> TT n -> TT n -> TT n
psubst Name
n2 (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) =
    forall a b. (a -> b) -> [a] -> [b]
map Sided ([(Name, Type)], AsymMods) -> State
statesFromMods forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Sided [a] -> [Sided a]
prod forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> Sided a -> Sided b
both ([(Name, Type)] -> [([(Name, Type)], AsymMods)]
interfaceMods forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) Sided (ArgsDAG, [(Name, Type)])
unresolved
    where
    swap :: Sided a -> Sided a
swap (Sided a
l a
r) = 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 = 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    = forall {a}. Sided a -> Sided a
swap (forall a b. (a -> b) -> Sided a -> Sided b
both forall a b. (a, b) -> b
snd Sided ([(Name, Type)], AsymMods)
sides) in
      [(Name, Type)]
-> Sided (ArgsDAG, [(Name, Type)]) -> Score -> [Name] -> State
State [] forall {a}. Sided ([a], [(Name, Type)])
interfaces (Score
scoreAcc forall a. Monoid a => a -> a -> a
`mappend` (forall a. Monoid a => a
mempty { asymMods :: Sided AsymMods
asymMods = Sided AsymMods
mods })) [Name]
usedns
    interfaceMods :: Interfaces -> [(Interfaces, AsymMods)]
    interfaceMods :: [(Name, Type)] -> [([(Name, Type)], AsymMods)]
interfaceMods [(Name, Type)]
cs = let lcs :: Int
lcs = forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Name, Type)]
cs in
      [ ([(Name, Type)]
cs', forall a. Monoid a => a
mempty { interfaceIntro :: Int
interfaceIntro = Int
lcs forall a. Num a => a -> a -> a
- forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Name, Type)]
cs' }) | [(Name, Type)]
cs' <- 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) = [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]