{-# 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 (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.Monoid (Monoid(mappend, mempty))
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)
import Data.Traversable (traverse)
searchByType :: [PkgName] -> PTerm -> Idris ()
searchByType :: [PkgName] -> PTerm -> Idris ()
searchByType pkgs :: [PkgName]
pkgs pterm :: PTerm
pterm = do
IState
i <- Idris IState
getIState
Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not ([PkgName] -> 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
$ "Searching packages: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
showSep ", " ((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 (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 ' ' 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
| (n :: Name
n, theScore :: Score
theScore) <- [(Name, Score)]
names']
if (Bool -> Bool
not ([Doc OutputAnnotation] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Doc OutputAnnotation]
docs))
then case IState -> OutputMode
idris_outputmode IState
i of
RawOutput _ -> 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 ""
IdeMode _ _ -> 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 "No results found"
IState -> Idris ()
putIState IState
i
where
numLimit :: Int
numLimit = 50
syn :: SyntaxInfo
syn = SyntaxInfo
defaultSyntax { implicitAllowed :: Bool
implicitAllowed = Bool
True }
name :: Name
name = Int -> String -> Name
sMN 0 "searchType"
searchUsing :: (IState -> Type -> [(Name, Type)] -> [(Name, a)])
-> IState -> Type -> [(Name, a)]
searchUsing :: (IState -> Type -> [(Name, Type)] -> [(Name, a)])
-> IState -> Type -> [(Name, a)]
searchUsing pred :: IState -> Type -> [(Name, Type)] -> [(Name, a)]
pred istate :: IState
istate ty :: 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 (\key :: 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 k :: Name
k x :: (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 (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 n :: Name
n _) = Name -> Bool
special Name
n
special (SN _) = Bool
True
special (UN n :: Text
n) = String -> Text
T.pack "default#" Text -> Text -> Bool
`T.isPrefixOf` Text
n
Bool -> Bool -> Bool
|| Text
n Text -> [Text] -> 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 ["believe_me", "really_believe_me"]
special _ = Bool
False
searchPred :: IState -> Type -> [(Name, Type)] -> [(Name, Score)]
searchPred :: IState -> Type -> [(Name, Type)] -> [(Name, Score)]
searchPred istate :: IState
istate ty1 :: Type
ty1 = [(Name, Type)] -> [(Name, Score)]
forall info. [(info, Type)] -> [(info, Score)]
matcher where
maxScore :: Int
maxScore = 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 :: (Def, r, i, b, c, d) -> Maybe Type
typeFromDef (def :: Def
def, _, _, _, _, _) = Def -> Maybe Type
get Def
def where
get :: Def -> Maybe Type
get :: Def -> Maybe Type
get (Function ty :: Type
ty _) = Type -> Maybe Type
forall a. a -> Maybe a
Just Type
ty
get (TyDecl _ ty :: Type
ty) = Type -> Maybe Type
forall a. a -> Maybe a
Just Type
ty
get (CaseOp _ ty :: Type
ty _ _ _ _) = Type -> Maybe Type
forall a. a -> Maybe a
Just Type
ty
get _ = Maybe Type
forall a. Maybe a
Nothing
unLazy :: Type -> Type
unLazy :: Type -> Type
unLazy typ :: Type
typ = case Type
typ of
App _ (App _ (P _ lazy :: Name
lazy _) _) ty :: Type
ty | Name
lazy Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN "Delayed" -> Type -> Type
unLazy Type
ty
Bind name :: Name
name binder :: Binder Type
binder ty :: 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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Type -> Type
unLazy Binder Type
binder) (Type -> Type
unLazy Type
ty)
App s :: AppStatus Name
s t1 :: Type
t1 t2 :: 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 ty :: Type
ty i :: Int
i -> Type -> Int -> Type
forall n. TT n -> Int -> TT n
Proj (Type -> Type
unLazy Type
ty) Int
i
_ -> Type
typ
reverseDag :: Ord k => [((k, a), Set k)] -> [((k, a), Set k)]
reverseDag :: [((k, a), Set k)] -> [((k, a), Set k)]
reverseDag xs :: [((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
k, v :: b
v), _) = ((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)
computeDagP :: Ord n
=> (TT n -> Bool)
-> TT n
-> ([((n, TT n), Set n)], [(n, TT n)], TT n)
computeDagP :: (TT n -> Bool) -> TT n -> ([((n, TT n), Set n)], [(n, TT n)], TT n)
computeDagP removePred :: TT n -> Bool
removePred t :: 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 (n :: a
n, ty :: 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))
(arguments :: [(n, TT n)]
arguments, theRemovedArgs :: [(n, TT n)]
theRemovedArgs, retTy :: TT n
retTy) = [(n, TT n)]
-> [(n, TT n)] -> TT n -> ([(n, TT n)], [(n, TT n)], TT n)
go [] [] TT n
t
go :: [(n, TT n)]
-> [(n, TT n)] -> TT n -> ([(n, TT n)], [(n, TT n)], TT n)
go args :: [(n, TT n)]
args removedArgs :: [(n, TT n)]
removedArgs (Bind n :: n
n (Pi _ _ ty :: TT n
ty _) sc :: 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 args :: [(n, TT n)]
args removedArgs :: [(n, TT n)]
removedArgs sc :: TT n
sc = ([(n, TT n)]
args, [(n, TT n)]
removedArgs, TT n
sc)
usedVars :: Ord n => TT n -> Map n (TT n, Bool)
usedVars :: 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 b :: Bool
b (P Bound n :: n
n t :: 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 b :: Bool
b (Bind n :: n
n binder :: Binder (TT n)
binder t2 :: 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 rig :: RigCount
rig t :: TT n
t v :: 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 t :: TT n
t v :: 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
bind :: 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 b :: Bool
b (App _ t1 :: TT n
t1 t2 :: 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 b :: Bool
b (Proj t :: TT n
t _) = Bool -> TT n -> Map n (TT n, Bool)
f Bool
b TT n
t
f _ (V _) = String -> Map n (TT n, Bool)
forall a. HasCallStack => String -> a
error "unexpected! run vToP first"
f _ _ = Map n (TT n, Bool)
forall k a. Map k a
M.empty
deleteFromDag :: Ord n => n -> [((n, TT n), (a, Set n))] -> [((n, TT n), (a, Set n))]
deleteFromDag :: n -> [((n, TT n), (a, Set n))] -> [((n, TT n), (a, Set n))]
deleteFromDag name :: n
name [] = []
deleteFromDag name :: n
name (((name2 :: n
name2, ty :: TT n
ty), (ix :: a
ix, set :: Set n
set)) : xs :: [((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 :: n -> [(n, TT n)] -> [(n, TT n)]
deleteFromArgList n :: 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)
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
/= :: AsymMods -> AsymMods -> Bool
$c/= :: AsymMods -> AsymMods -> Bool
== :: AsymMods -> AsymMods -> Bool
$c== :: 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
showList :: [AsymMods] -> String -> String
$cshowList :: [AsymMods] -> String -> String
show :: AsymMods -> String
$cshow :: AsymMods -> String
showsPrec :: Int -> AsymMods -> String -> String
$cshowsPrec :: Int -> AsymMods -> String -> String
Show)
data Sided a = Sided
{ Sided a -> a
left :: !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
/= :: 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 -> 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
showList :: [Sided a] -> String -> String
$cshowList :: forall a. Show a => [Sided a] -> String -> String
show :: Sided a -> String
$cshow :: forall a. Show a => Sided a -> String
showsPrec :: Int -> Sided a -> String -> String
$cshowsPrec :: forall a. Show a => Int -> Sided a -> String -> String
Show)
sided :: (a -> a -> b) -> Sided a -> b
sided :: (a -> a -> b) -> Sided a -> b
sided f :: a -> a -> b
f (Sided l :: a
l r :: a
r) = a -> a -> b
f a
l a
r
both :: (a -> b) -> Sided a -> Sided b
both :: (a -> b) -> Sided a -> Sided b
both f :: a -> b
f (Sided l :: a
l r :: a
r) = b -> b -> Sided b
forall a. a -> a -> Sided a
Sided (a -> b
f a
l) (a -> b
f a
r)
data Score = Score
{ Score -> Int
transposition :: !Int
, Score -> Int
equalityFlips :: !Int
, Score -> Sided AsymMods
asymMods :: !(Sided AsymMods)
} deriving (Score -> Score -> Bool
(Score -> Score -> Bool) -> (Score -> Score -> Bool) -> Eq Score
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 -> 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
showList :: [Score] -> String -> String
$cshowList :: [Score] -> String -> String
show :: Score -> String
$cshow :: Score -> String
showsPrec :: Int -> Score -> String -> String
$cshowsPrec :: Int -> Score -> String -> String
Show)
displayScore :: Score -> Doc OutputAnnotation
displayScore :: Score -> Doc OutputAnnotation
displayScore score :: 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 True True -> Ordering -> String -> Doc OutputAnnotation
annotated Ordering
EQ "="
Sided True False -> Ordering -> String -> Doc OutputAnnotation
annotated Ordering
LT "<"
Sided False True -> Ordering -> String -> Doc OutputAnnotation
annotated Ordering
GT ">"
Sided False False -> String -> Doc OutputAnnotation
forall a. String -> Doc a
text "_"
where
annotated :: Ordering -> String -> Doc OutputAnnotation
annotated ordr :: 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 app :: Int
app tcApp :: Int
tcApp tcIntro :: 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
== 0
scoreCriterion :: Score -> Bool
scoreCriterion :: Score -> Bool
scoreCriterion (Score _ _ amods :: 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
> 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
> 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 _ tcApp :: Int
tcApp tcIntro :: Int
tcIntro) -> Int
tcApp Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 3 Bool -> Bool -> Bool
|| Int
tcIntro Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 3) Sided AsymMods
amods)
)
defaultScoreFunction :: Score -> Int
defaultScoreFunction :: Score -> Int
defaultScoreFunction (Score trans :: Int
trans eqFlip :: Int
eqFlip amods :: 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
linearPenalty :: Int
linearPenalty = (\(Sided l :: Int
l r :: Int
r) -> 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 app :: Int
app tcApp :: Int
tcApp tcIntro :: Int
tcIntro) -> 3 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
app Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 4 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
tcApp Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
tcIntro) Sided AsymMods
amods)
upAndDowncastPenalty :: Int
upAndDowncastPenalty = 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 app :: Int
app tcApp :: Int
tcApp tcIntro :: Int
tcIntro) -> 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 l1 :: a
l1 r1 :: a
r1) <> :: Sided a -> Sided a -> Sided a
<> (Sided l2 :: a
l2 r2 :: 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 l1 :: a
l1 r1 :: a
r1) mappend :: Sided a -> Sided a -> Sided a
`mappend` (Sided l2 :: a
l2 r2 :: 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 0 0 0
(Mods a :: Int
a b :: Int
b c :: Int
c) mappend :: AsymMods -> AsymMods -> AsymMods
`mappend` (Mods a' :: Int
a' b' :: Int
b' c' :: 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 0 0 Sided AsymMods
forall a. Monoid a => a
mempty
(Score t :: Int
t e :: Int
e mods :: Sided AsymMods
mods) mappend :: Score -> Score -> Score
`mappend` (Score t' :: Int
t' e' :: Int
e' mods' :: 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')
type ArgsDAG = [((Name, Type), (Int, Set Name))]
type Interfaces = [(Name, Type)]
data State = State
{ State -> [(Name, Type)]
holes :: ![(Name, Type)]
, State -> Sided (ArgsDAG, [(Name, Type)])
argsAndInterfaces :: !(Sided (ArgsDAG, Interfaces))
, State -> Score
score :: !Score
, State -> [Name]
usedNames :: ![Name]
} 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
showList :: [State] -> String -> String
$cshowList :: [State] -> String -> String
show :: State -> String
$cshow :: State -> String
showsPrec :: Int -> State -> String -> String
$cshowsPrec :: Int -> State -> String -> String
Show
modifyTypes :: (Type -> Type) -> (ArgsDAG, Interfaces) -> (ArgsDAG, Interfaces)
modifyTypes :: (Type -> Type)
-> (ArgsDAG, [(Name, Type)]) -> (ArgsDAG, [(Name, Type)])
modifyTypes f :: 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 (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 (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first ((Type -> Type) -> (d, Type) -> (d, Type)
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 (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 = (((Name, Type), (Int, Set Name)) -> (Type, Maybe Int))
-> Maybe ((Name, Type), (Int, Set Name)) -> Maybe (Type, Maybe Int)
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 (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 n :: Name
n (args :: ArgsDAG
args, interfaces :: [(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 (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 (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 n :: Name
n (args :: ArgsDAG
args, interfaces :: [(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 :: TC a -> Maybe a
tcToMaybe (OK x :: a
x) = a -> Maybe a
forall a. a -> Maybe a
Just a
x
tcToMaybe (Error _) = 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 (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 (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 interfaceInfo :: Ctxt InterfaceInfo
interfaceInfo ctxt :: Context
ctxt ty :: Type
ty tyTry :: 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 (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 (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 (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 | (n :: Name
n, t :: Type
t) <- [(Name, Type)]
res ]) [(Name, Type)]
tcArgs
[(Name, Type)] -> Maybe [(Name, Type)]
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'
(tcArgs :: [(Name, Type)]
tcArgs, nonTcArgs :: [(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 interfaceInfo :: Ctxt InterfaceInfo
interfaceInfo ty :: Type
ty = Bool -> Bool
not ([InterfaceInfo] -> 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 (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
(clss :: Type
clss, _) = Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
ty
getInterfaceName :: TT a -> [a]
getInterfaceName (P (TCon _ _) interfaceName :: a
interfaceName _) = [a
interfaceName]
getInterfaceName _ = []
subsets :: [a] -> [[a]]
subsets :: [a] -> [[a]]
subsets [] = [[]]
subsets (x :: a
x : xs :: [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
flipEqualities :: Type -> [(Int, Type)]
flipEqualities :: Type -> [(Int, Type)]
flipEqualities t :: Type
t = case Type
t of
eq1 :: Type
eq1@(App _ (App _ (App _ (App _ eq :: Type
eq@(P _ eqty :: Name
eqty _) tyL :: Type
tyL) tyR :: Type
tyR) valL :: Type
valL) valR :: Type
valR) | Name
eqty Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
eqTy ->
[(0, Type
eq1), (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 n :: Name
n binder :: Binder Type
binder sc :: Type
sc -> (\bind' :: Binder (Int, Type)
bind' (j :: Int
j, sc' :: 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 (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)
traverse Type -> [(Int, Type)]
flipEqualities Binder Type
binder [(Int, Type) -> (Int, Type)] -> [(Int, Type)] -> [(Int, Type)]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> [(Int, Type)]
flipEqualities Type
sc
App _ f :: Type
f x :: Type
x -> (\(i :: Int
i, f' :: Type
f') (j :: Int
j, x' :: 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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> [(Int, Type)]
flipEqualities Type
x
t' :: Type
t' -> [(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
matchTypesBulk :: forall info. IState -> Int -> Type -> [(info, Type)] -> [(info, Score)]
matchTypesBulk :: IState -> Int -> Type -> [(info, Type)] -> [(info, Score)]
matchTypesBulk istate :: IState
istate maxScore :: Int
maxScore type1 :: Type
type1 types :: [(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
info, type2 :: 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
xs :: [(Score, State)]
xs -> (Score, (info, PQueue Score State))
-> Maybe (Score, (info, PQueue Score State))
forall a. a -> Maybe a
Just ([Score] -> Score
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 = (\(i :: Int
i, dag :: ArgsDAG
dag) (j :: Int
j, retTy :: 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 (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 dag :: [((a, Type), (a, b))]
dag = case [((a, Type), (a, b))]
dag of
[] -> [(0, [])]
((n :: a
n, ty :: Type
ty), (pos :: a
pos, deps :: b
deps)) : xs :: [((a, Type), (a, b))]
xs ->
(\(i :: Int
i, ty' :: Type
ty') (j :: Int
j, xs' :: [((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 (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 (numEqFlips :: Int
numEqFlips, sndDag :: ArgsDAG
sndDag, sndRetTy :: 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 :: Int
equalityFlips = Int
numEqFlips }) [Name]
usedns) [(Type
retTy1, Type
sndRetTy)]
(Score, State) -> Maybe (Score, State)
forall (m :: * -> *) a. Monad m => a -> m a
return (State -> Score
score State
state, State
state)
(dag2 :: ArgsDAG
dag2, interfaceArgs2 :: [(Name, Type)]
interfaceArgs2, retTy2 :: 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 q :: 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
Nothing -> []
Just ((nextScore :: Score
nextScore, (info :: info
info, stateQ :: PQueue Score State
stateQ)), q' :: 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
Nothing -> PQueue Score (info, PQueue Score State) -> [(info, Score)]
getAllResults PQueue Score (info, PQueue Score State)
q'
Just (Left stateQ' :: 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
Nothing -> PQueue Score (info, PQueue Score State) -> [(info, Score)]
getAllResults PQueue Score (info, PQueue Score State)
q'
Just ((newQscore :: Score
newQscore,_), _) -> 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 theScore :: 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
(dag1 :: ArgsDAG
dag1, interfaceArgs1 :: [(Name, Type)]
interfaceArgs1, retTy1 :: 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 (\i :: Int
i (ty :: (Name, Type)
ty, deps :: Set Name
deps) -> ((Name, Type)
ty, (Int
i, Set Name
deps))) [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 f :: t -> a
f (a :: t
a,b :: b
b,c :: c
c) = (t -> a
f t
a, b
b, c
c)
resolveUnis :: [(Name, Type)] -> State -> Maybe (State, [(Type, Type)])
resolveUnis :: [(Name, Type)] -> State -> Maybe (State, [(Type, Type)])
resolveUnis [] state :: State
state = (State, [(Type, Type)]) -> Maybe (State, [(Type, Type)])
forall a. a -> Maybe a
Just (State
state, [])
resolveUnis ((name :: Name
name, term :: Type
term@(P Bound name2 :: Name
name2 _)) : xs :: [(Name, Type)]
xs)
state :: 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
((ty1 :: Type
ty1, ix1 :: Maybe Int
ix1), (ty2 :: Type
ty2, ix2 :: Maybe Int
ix2)) <- Maybe ((Type, Maybe Int), (Type, Maybe Int))
findArgs
(state'' :: State
state'', queue :: [(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 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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe Int
ix2))
(State, [(Type, Type)]) -> Maybe (State, [(Type, Type)])
forall (m :: * -> *) a. Monad m => a -> m a
return ((Score -> Score) -> State -> State
inScore (\s :: Score
s -> Score
s { transposition :: Int
transposition = Score -> Int
transposition Score
s Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
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 f :: Score -> Score
f stat :: State
stat = State
stat { score :: Score
score = Score -> Score
f (State -> Score
score State
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 (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 (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 (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 :: [(Name, Type)]
holes = ((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 (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
matchnames) (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) (State -> [(Name, Type)]
holes State
state)
, argsAndInterfaces :: Sided (ArgsDAG, [(Name, Type)])
argsAndInterfaces = ((ArgsDAG, [(Name, Type)]) -> (ArgsDAG, [(Name, Type)]))
-> Sided (ArgsDAG, [(Name, Type)])
-> Sided (ArgsDAG, [(Name, Type)])
forall a b. (a -> b) -> Sided a -> Sided b
both ((Type -> Type)
-> (ArgsDAG, [(Name, Type)]) -> (ArgsDAG, [(Name, Type)])
modifyTypes (Name -> Type -> Type -> Type
forall n. Eq n => n -> TT n -> TT n -> TT n
subst Name
name Type
term) ((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)])
deleteArgs) Sided (ArgsDAG, [(Name, Type)])
unresolved}
resolveUnis ((name :: Name
name, term :: Type
term) : xs :: [(Name, Type)]
xs)
state :: State
state@(State hs :: [(Name, Type)]
hs unresolved :: Sided (ArgsDAG, [(Name, Type)])
unresolved _ _) = 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 Nothing Nothing -> Maybe (State, [(Type, Type)])
forall a. Maybe a
Nothing
Sided (Just _) (Just _) -> String -> Maybe (State, [(Type, Type)])
forall a. HasCallStack => String -> a
error "Idris internal error: TypeSearch.resolveUnis"
oneOfEach :: Sided (Maybe (Type, Maybe Int))
oneOfEach -> (State -> State)
-> (State, [(Type, Type)]) -> (State, [(Type, Type)])
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 _) = AsymMods
forall a. Monoid a => a
mempty { argApp :: Int
argApp = 1 }
scoreFor Nothing = AsymMods
forall a. Monoid a => a
mempty { argApp :: Int
argApp = Int
otherApplied }
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 f :: t -> b
f (x :: t
x, y :: t
y) = (t -> b
f t
x, t -> b
f t
y)
(injUsedVars :: [Name]
injUsedVars, notInjUsedVars :: [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 (\k :: Name
k _-> Name
k Name -> [Name] -> 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 (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 (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
notInjUsedVars
addScore :: Sided AsymMods -> State -> State
addScore additions :: Sided AsymMods
additions theState :: 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 Sided AsymMods -> Sided AsymMods -> Sided AsymMods
forall a. Monoid a => a -> a -> a
`mappend` Sided AsymMods
additions } }
state' :: State
state' = State
state { holes :: [(Name, Type)]
holes = ((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 (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
toDelete) (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
, argsAndInterfaces :: Sided (ArgsDAG, [(Name, Type)])
argsAndInterfaces = ((ArgsDAG, [(Name, Type)]) -> (ArgsDAG, [(Name, Type)]))
-> Sided (ArgsDAG, [(Name, Type)])
-> Sided (ArgsDAG, [(Name, Type)])
forall a b. (a -> b) -> Sided a -> Sided b
both ((Type -> Type)
-> (ArgsDAG, [(Name, Type)]) -> (ArgsDAG, [(Name, Type)])
modifyTypes (Name -> Type -> Type -> Type
forall n. Eq n => n -> TT n -> TT n -> TT n
subst Name
name Type
term) ((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)])
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'
unifyQueue :: State -> [(Type, Type)] -> Maybe State
unifyQueue :: State -> [(Type, Type)] -> Maybe State
unifyQueue state :: State
state [] = State -> Maybe State
forall (m :: * -> *) a. Monad m => a -> m a
return State
state
unifyQueue state :: State
state ((ty1 :: Type
ty1, ty2 :: Type
ty2) : queue :: [(Type, Type)]
queue) = 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 [ (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 [] 0))) | (n :: Name
n, ty :: 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
state', queueAdditions :: [(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 usedns :: [Name]
usedns ty :: 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 x :: Type
x -> [Type
x]; 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 (m :: * -> *) a. Monad m => a -> m a
return Type
ty'
where
(clss :: Type
clss, _) = Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
ty
getInterfaceName :: TT a -> [a]
getInterfaceName (P (TCon _ _) interfaceName :: a
interfaceName _) = [a
interfaceName]
getInterfaceName _ = []
nextStepsQueue :: Q.PQueue Score State -> Maybe (Either (Q.PQueue Score State) Score)
nextStepsQueue :: PQueue Score State -> Maybe (Either (PQueue Score State) Score)
nextStepsQueue queue :: PQueue Score State
queue = do
((nextScore :: Score
nextScore, next :: State
next), rest :: 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 ([], []) ([], [])) _ _) = Bool
True
isFinal _ = Bool
False
nextSteps :: State -> [State]
nextSteps :: State -> [State]
nextSteps (State [] unresolved :: Sided (ArgsDAG, [(Name, Type)])
unresolved@(Sided ([], c1 :: [(Name, Type)]
c1) ([], c2 :: [(Name, Type)]
c2)) scoreAcc :: Score
scoreAcc usedns :: [Name]
usedns) =
if [State] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [State]
results3 then [State]
results4 else [State]
results3
where
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 (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)]
| (n1 :: Name
n1, ty1 :: Type
ty1) <- [(Name, Type)]
c1, (n2 :: Name
n2, ty2 :: 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)]
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 (\(cs :: [(Name, Type)]
cs, _, _) -> ([], [(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 0 0 ((([(Name, Type)], AsymMods, [Name]) -> AsymMods)
-> Sided ([(Name, Type)], AsymMods, [Name]) -> Sided AsymMods
forall a b. (a -> b) -> Sided a -> Sided b
both (\(_, amods :: AsymMods
amods, _) -> 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 (\(_, _, hs :: [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 (\(_, cs :: [(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 :: Sided a -> Sided [a] -> [Sided a]
parallel (Sided l :: a
l r :: a
r) (Sided ls :: [a]
ls rs :: [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 interfaces :: [(Name, Type)]
interfaces = [ ( [(Name, Type)]
newInterfaceArgs, AsymMods
forall a. Monoid a => a
mempty { interfaceApp :: Int
interfaceApp = 1 }, [Name]
newHoles )
| (_, ty :: 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 ]
nextSteps (State hs :: [(Name, Type)]
hs (Sided (dagL :: ArgsDAG
dagL, c1 :: [(Name, Type)]
c1) (dagR :: ArgsDAG
dagR, c2 :: [(Name, Type)]
c2)) scoreAcc :: Score
scoreAcc usedns :: [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
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)
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 (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 (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)]
| (n1 :: Name
n1, ty1 :: Type
ty1) <- ArgsDAG -> [(Name, Type)]
canBeFirst ArgsDAG
dagL, (n2 :: Name
n2, ty2 :: 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)]
takeSomeInterfaces :: State -> [State]
takeSomeInterfaces (State [] unresolved :: Sided (ArgsDAG, [(Name, Type)])
unresolved@(Sided ([], _) ([], _)) scoreAcc :: Score
scoreAcc usedns :: [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 l :: a
l r :: 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 sides :: 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 (\(c :: [(Name, Type)]
c, _) -> ([], [(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 :: Sided AsymMods
asymMods = Sided AsymMods
mods })) [Name]
usedns
interfaceMods :: Interfaces -> [(Interfaces, AsymMods)]
interfaceMods :: [(Name, Type)] -> [([(Name, Type)], AsymMods)]
interfaceMods cs :: [(Name, Type)]
cs = let lcs :: Int
lcs = [(Name, Type)] -> 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 :: Int
interfaceIntro = Int
lcs Int -> Int -> Int
forall a. Num a => a -> a -> a
- [(Name, Type)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Name, Type)]
cs' }) | [(Name, Type)]
cs' <- [(Name, Type)] -> [[(Name, Type)]]
forall a. [a] -> [[a]]
subsets [(Name, Type)]
cs ]
prod :: Sided [a] -> [Sided a]
prod :: Sided [a] -> [Sided a]
prod (Sided ls :: [a]
ls rs :: [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]
takeSomeInterfaces s :: State
s = [State
s]