@@ -4,11 +4,11 @@ module Idris.TypeSearch (
4 searchByType, searchPred, defaultScoreFunction
4 searchByType, searchPred, defaultScoreFunction
7−import Control.Applicative ((<$>), (<*>), (<|>))
7+import Control.Applicative (Applicative (..), (<$>), (<*>), (<|>))
8−import Control.Arrow (first, second, (&&&))
8+import Control.Arrow (first, second, (&&&), (***))
9−import Control.Monad (forM_, guard)
9+import Control.Monad (guard)
11−import Data.List (find, delete, deleteBy, minimumBy, partition, sortBy, (\\))
11+import Data.List (find, partition, (\\))
12import Data.Map (Map)
12import Data.Map (Map)
13import qualified Data.Map as M
13import qualified Data.Map as M
14import Data.Maybe (catMaybes, fromMaybe, isJust, maybeToList, mapMaybe)
14import Data.Maybe (catMaybes, fromMaybe, isJust, maybeToList, mapMaybe)
@@ -18,11 +18,12 @@ import qualified Data.PriorityQueue.FingerTree as Q
18import Data.Set (Set)
18import Data.Set (Set)
19import qualified Data.Set as S
19import qualified Data.Set as S
20import qualified Data.Text as T (pack, isPrefixOf)
20import qualified Data.Text as T (pack, isPrefixOf)
21+import Data.Traversable (traverse)
22−import Idris.AbsSyntax (addUsingConstraints, addImpl, getContext, getIState, putIState, implicit)
23+import Idris.AbsSyntax (addUsingConstraints, addImpl, getIState, putIState, implicit)
23−import Idris.AbsSyntaxTree (class_instances, ClassInfo, defaultSyntax, Idris,
24+import Idris.AbsSyntaxTree (class_instances, ClassInfo, defaultSyntax, eqTy, Idris,
24 IState (idris_classes, idris_docstrings, tt_ctxt, idris_outputmode),
25 IState (idris_classes, idris_docstrings, tt_ctxt, idris_outputmode),
25− implicitAllowed, OutputMode(..), prettyDocumentedIst, prettyIst, PTerm, toplevel)
26+ implicitAllowed, OutputMode(..), prettyDocumentedIst, PTerm, toplevel)
26import Idris.Core.Evaluate (Context (definitions), Def (Function, TyDecl, CaseOp), normaliseC)
27import Idris.Core.Evaluate (Context (definitions), Def (Function, TyDecl, CaseOp), normaliseC)
27import Idris.Core.TT hiding (score)
28import Idris.Core.TT hiding (score)
28import Idris.Core.Unify (match_unify)
29import Idris.Core.Unify (match_unify)
@@ -31,30 +32,32 @@ import Idris.Docstrings (noDocs, overview)
31import Idris.Elab.Type (elabType)
32import Idris.Elab.Type (elabType)
32import Idris.Output (iRenderOutput, iPrintResult, iRenderResult)
33import Idris.Output (iRenderOutput, iPrintResult, iRenderResult)
35+import Prelude hiding (pred)
34import Util.Pretty (text, char, vsep, (<>), Doc)
37import Util.Pretty (text, char, vsep, (<>), Doc)
36searchByType :: PTerm -> Idris ()
39searchByType :: PTerm -> Idris ()
37searchByType pterm = do
40searchByType pterm = do
38 pterm' <- addUsingConstraints syn emptyFC pterm
41 pterm' <- addUsingConstraints syn emptyFC pterm
39− pterm'' <- implicit toplevel syn n pterm'
42+ pterm'' <- implicit toplevel syn name pterm'
40 i <- getIState
43 i <- getIState
41 let pterm''' = addImpl i pterm''
44 let pterm''' = addImpl i pterm''
42− ty <- elabType toplevel syn (fst noDocs) (snd noDocs) emptyFC [] n pterm'
45+ ty <- elabType toplevel syn (fst noDocs) (snd noDocs) emptyFC [] name pterm'
43 putIState i -- don't actually make any changes
46 putIState i -- don't actually make any changes
44 let names = searchUsing searchPred i ty
47 let names = searchUsing searchPred i ty
45− let names' = take numLimit $ names
48+ let names' = take numLimit names
46 let docs =
49 let docs =
47 [ let docInfo = (n, delabTy i n, fmap (overview . fst) (lookupCtxtExact n (idris_docstrings i))) in
50 [ let docInfo = (n, delabTy i n, fmap (overview . fst) (lookupCtxtExact n (idris_docstrings i))) in
48− displayScore score <> char ' ' <> prettyDocumentedIst i docInfo
51+ displayScore theScore <> char ' ' <> prettyDocumentedIst i docInfo
49− | (n, score) <- names']
52+ | (n, theScore) <- names']
50 case idris_outputmode i of
53 case idris_outputmode i of
51 RawOutput _ -> do mapM_ iRenderOutput docs
54 RawOutput _ -> do mapM_ iRenderOutput docs
52 iPrintResult ""
55 iPrintResult ""
53− IdeSlave n h -> iRenderResult (vsep docs)
56+ IdeSlave _ _ -> iRenderResult (vsep docs)
55 numLimit = 50
58 numLimit = 50
56 syn = defaultSyntax { implicitAllowed = True } -- syntax
59 syn = defaultSyntax { implicitAllowed = True } -- syntax
57− n = sMN 0 "searchType" -- name
60+ name = sMN 0 "searchType" -- name
59-- | Conduct a type-directed search using a given match predicate
62-- | Conduct a type-directed search using a given match predicate
60searchUsing :: (IState -> Type -> [(Name, Type)] -> [(Name, a)])
63searchUsing :: (IState -> Type -> [(Name, Type)] -> [(Name, a)])
@@ -69,7 +72,7 @@ searchUsing pred istate ty = pred istate nty . concat . M.elems $
69 type2 <- typeFromDef x
72 type2 <- typeFromDef x
70 return $ normaliseC ctxt [] type2
73 return $ normaliseC ctxt [] type2
71 special :: Name -> Bool
74 special :: Name -> Bool
72− special (NS n ns) = special n
75+ special (NS n _) = special n
73 special (SN _) = True
76 special (SN _) = True
74 special (UN n) = T.pack "default#" `T.isPrefixOf` n
77 special (UN n) = T.pack "default#" `T.isPrefixOf` n
75 || n `elem` map T.pack ["believe_me", "really_believe_me"]
78 || n `elem` map T.pack ["believe_me", "really_believe_me"]
@@ -85,7 +88,7 @@ searchPred istate ty1 = matcher where
85typeFromDef :: (Def, b, c, d) -> Maybe Type
88typeFromDef :: (Def, b, c, d) -> Maybe Type
86typeFromDef (def, _, _, _) = get def where
89typeFromDef (def, _, _, _) = get def where
87 get :: Def -> Maybe Type
90 get :: Def -> Maybe Type
88− get (Function ty tm) = Just ty
91+ get (Function ty _) = Just ty
89 get (TyDecl _ ty) = Just ty
92 get (TyDecl _ ty) = Just ty
90 -- get (Operator ty _ _) = Just ty
93 -- get (Operator ty _ _) = Just ty
91 get (CaseOp _ ty _ _ _ _) = Just ty
94 get (CaseOp _ ty _ _ _ _) = Just ty
@@ -106,17 +109,17 @@ computeDagP :: Ord n
106 => (TT n -> Bool) -- ^ filter to remove some arguments
109 => (TT n -> Bool) -- ^ filter to remove some arguments
108 -> ([((n, TT n), Set n)], [(n, TT n)], TT n)
111 -> ([((n, TT n), Set n)], [(n, TT n)], TT n)
109−computeDagP removePred t = (reverse (map f args), reverse removedArgs , retTy) where
112+computeDagP removePred t = (reverse (map f arguments), reverse theRemovedArgs , retTy) where
110− f (n, t) = ((n, t), M.keysSet (usedVars t))
113+ f (n, ty) = ((n, ty), M.keysSet (usedVars ty))
112− (numArgs, args, removedArgs, retTy) = go 0 [] [] t
115+ (arguments, theRemovedArgs, retTy) = go [] [] t
114 -- NOTE : args are in reverse order
117 -- NOTE : args are in reverse order
115− go k args removedArgs (Bind n (Pi t _) sc) = let arg = (n, t) in
118+ go args removedArgs (Bind n (Pi ty _) sc) = let arg = (n, ty) in
116− if removePred t
119+ if removePred ty
117− then go k args (arg : removedArgs) sc
120+ then go args (arg : removedArgs) sc
118− else go (succ k) (arg : args) removedArgs sc
121+ else go (arg : args) removedArgs sc
119− go k args removedArgs retTy = (k, args, removedArgs, retTy)
122+ go args removedArgs sc = (args, removedArgs, sc)
121-- | Collect the names and types of all the free variables
124-- | Collect the names and types of all the free variables
122-- The Boolean indicates those variables which are determined due to injectivity
125-- The Boolean indicates those variables which are determined due to injectivity
@@ -130,7 +133,7 @@ usedVars = f True where
130 bind -> f b (binderTy bind)
133 bind -> f b (binderTy bind)
131 f b (App t1 t2) = f b t1 `M.union` f (b && isInjective t1) t2
134 f b (App t1 t2) = f b t1 `M.union` f (b && isInjective t1) t2
132 f b (Proj t _) = f b t
135 f b (Proj t _) = f b t
133− f _ (V j) = error "unexpected! run vToP first"
136+ f _ (V _) = error "unexpected! run vToP first"
134 f _ _ = M.empty
137 f _ _ = M.empty
136-- | Remove a node from a directed acyclic graph
139-- | Remove a node from a directed acyclic graph
@@ -143,73 +146,102 @@ deleteFromDag name (((name2, ty), (ix, set)) : xs) = (if name == name2
143deleteFromArgList :: Ord n => n -> [(n, TT n)] -> [(n, TT n)]
146deleteFromArgList :: Ord n => n -> [(n, TT n)] -> [(n, TT n)]
144deleteFromArgList n = filter ((/= n) . fst)
147deleteFromArgList n = filter ((/= n) . fst)
149+-- | Asymmetric modifications to keep track of
152+ , typeClassApp :: !Int
153+ , typeClassIntro :: !Int
154+ } deriving (Eq, Show)
157+-- | Homogenous tuples
161+ } deriving (Eq, Show)
163+sided :: (a -> a -> b) -> Sided a -> b
164+sided f (Sided l r) = f l r
166+-- | Could be a functor instance, but let's avoid name overloading
167+both :: (a -> b) -> Sided a -> Sided b
168+both f (Sided l r) = Sided (f l) (f r)
146data Score = Score
170data Score = Score
147− { transposition :: !Int
171+ { transposition :: !Int
148− , leftApplied :: !Int
172+ , equalityFlips :: !Int
149− , rightApplied :: !Int
173+ , asymMods :: !(Sided AsymMods)
150− , leftTypeClassApp :: !Int
151− , rightTypeClassApp :: !Int
152− , leftTypeClassIntro :: !Int
153− , rightTypeClassIntro :: !Int } deriving (Eq, Show)
174+ } deriving (Eq, Show)
155displayScore :: Score -> Doc a
176displayScore :: Score -> Doc a
156−displayScore (Score trans lapp rapp lclassapp rclassapp lclassintro rclassintro) = text $ case (lt, gt) of
177+displayScore score = text $ case both noMods (asymMods score) of
157− (True , True ) -> "=" -- types are isomorphic
178+ Sided True True -> "=" -- types are isomorphic
158− (True , False) -> "<" -- found type is more general than searched type
179+ Sided True False -> "<" -- found type is more general than searched type
159− (False, True ) -> ">" -- searched type is more general than found type
180+ Sided False True -> ">" -- searched type is more general than found type
160− (False, False) -> "_"
181+ Sided False False -> "_"
161− where lt = lapp + lclassapp + lclassintro == 0
182+ where
162− gt = rapp + rclassapp + rclassintro == 0
183+ noMods (Mods app tcApp tcIntro) = app + tcApp + tcIntro == 0
165scoreCriterion :: Score -> Bool
185scoreCriterion :: Score -> Bool
166−scoreCriterion (Score a b c d e f g) = not
186+scoreCriterion (Score _ _ amods) = not
167− ( (b > 0 && c > 0) || (b + c) > 4 || any (> 3) [d,e,f,g])
187+ ( sided (&&) (both ((> 0) . argApp) amods)
188+ || sided (+) (both argApp amods) > 4
189+ || sided (||) (both (\(Mods _ tcApp tcIntro) -> tcApp > 3 || tcIntro > 3) amods)
169defaultScoreFunction :: Score -> Int
192defaultScoreFunction :: Score -> Int
170−defaultScoreFunction (Score a b c d e f g) = a + 9*b + 3*c + 12*d + 4*e + 6*f + 2*g + 100*(2*b + d + f)*(2*c + e + g)
193+defaultScoreFunction (Score trans eqFlip amods) =
194+ trans + eqFlip + linearPenalty + upAndDowncastPenalty
196+ -- prefer finding a more general type to a less general type
197+ linearPenalty = (\(Sided l r) -> 3 * l + r)
198+ (both (\(Mods app tcApp tcIntro) -> 3 * app + 4 * tcApp + 2 * tcIntro) amods)
171 -- it's very bad to have *both* upcasting and downcasting
199 -- it's very bad to have *both* upcasting and downcasting
200+ upAndDowncastPenalty = 100 *
201+ sided (*) (both (\(Mods app tcApp tcIntro) -> 2 * app + tcApp + tcIntro) amods)
203+instance Monoid a => Monoid (Sided a) where
204+ mempty = Sided mempty mempty
205+ (Sided l1 r1) `mappend` (Sided l2 r2) = Sided (l1 `mappend` l2) (r1 `mappend` r2)
207+instance Monoid AsymMods where
209+ (Mods a b c) `mappend` (Mods a' b' c') = Mods (a + a') (b + b') (c + c')
173instance Monoid Score where
211instance Monoid Score where
174− mempty = Score 0 0 0 0 0 0 0
212+ mempty = Score 0 0 mempty
175− (Score a b c d e f g) `mappend` (Score a' b' c' d' e' f' g') =
213+ (Score t e mods) `mappend` (Score t' e' mods') = Score (t + t') (e + e') (mods `mappend` mods')
176− Score (a + a') (b + b') (c + c') (d + d') (e + e') (f + f') (g + g')
178-- | A directed acyclic graph representing the arguments to a function
215-- | A directed acyclic graph representing the arguments to a function
179-- The 'Int' represents the position of the argument (1st argument, 2nd, etc.)
216-- The 'Int' represents the position of the argument (1st argument, 2nd, etc.)
180type ArgsDAG = [((Name, Type), (Int, Set Name))]
217type ArgsDAG = [((Name, Type), (Int, Set Name))]
219+-- | A list of typeclass constraints
220+type Classes = [(Name, Type)]
182-- | The state corresponding to an attempted match of two types.
222-- | The state corresponding to an attempted match of two types.
183data State = State
223data State = State
184− { holes :: ![(Name, Type)] -- ^ names which have yet to be resolved
224+ { holes :: ![(Name, Type)] -- ^ names which have yet to be resolved
185− , args1 :: !ArgsDAG -- ^ arguments for the left type which have yet to be resolved
225+ , argsAndClasses :: !(Sided (ArgsDAG, Classes))
186− , args2 :: !ArgsDAG -- ^ arguments for the right type which have yet to be resolved
226+ -- ^ arguments and typeclass constraints for each type which have yet to be resolved
187− , classes1 :: ![(Name, Type)] -- ^ typeclass arguments for the left type which haven't been resolved
188− , classes2 :: ![(Name, Type)] -- ^ typeclass arguments for the right type which haven't been resolved
189 , score :: !Score -- ^ the score so far
227 , score :: !Score -- ^ the score so far
190 , usedNames :: ![Name] -- ^ all names that have been used
228 , usedNames :: ![Name] -- ^ all names that have been used
191 } deriving Show
229 } deriving Show
193−modifyTypes :: (Type -> Type) -> State -> State
231+modifyTypes :: (Type -> Type) -> (ArgsDAG, Classes) -> (ArgsDAG, Classes)
194−modifyTypes f (State h a1 a2 c1 c2 s un) =
232+modifyTypes f = modifyDag *** modifyList
195− State h (modifyDag a1) (modifyDag a2)
196− (modifyList c1) (modifyList c2)
199 modifyDag = map (first (second f))
234 modifyDag = map (first (second f))
200 modifyList = map (second f)
235 modifyList = map (second f)
202findNameInArgsDAG :: Name -> ArgsDAG -> Maybe (Type, Maybe Int)
237findNameInArgsDAG :: Name -> ArgsDAG -> Maybe (Type, Maybe Int)
203−findNameInArgsDAG name xs = fmap ((snd . fst) &&& (Just . fst . snd)) . find ((name ==) . fst . fst) $ xs
238+findNameInArgsDAG name = fmap ((snd . fst) &&& (Just . fst . snd)) . find ((name ==) . fst . fst)
205−findLeft, findRight :: Name -> State -> Maybe (Type, Maybe Int)
206−findLeft n (State _ a1 a2 c1 c2 _ _) = findNameInArgsDAG n a1 <|> ((,) <$> lookup n c1 <*> Nothing)
207−findRight n (State _ a1 a2 c1 c2 _ _) = findNameInArgsDAG n a2 <|> ((,) <$> lookup n c2 <*> Nothing)
209−deleteLeft, deleteRight :: Name -> State -> State
240+findName :: Name -> (ArgsDAG, Classes) -> Maybe (Type, Maybe Int)
210−deleteLeft n state = state { args1 = deleteFromDag n (args1 state) , classes1 = filter ((/= n) . fst) (classes1 state) }
241+findName n (args, classes) = findNameInArgsDAG n args <|> ((,) <$> lookup n classes <*> Nothing)
211−deleteRight n state = state { args2 = deleteFromDag n (args2 state) , classes2 = filter ((/= n) . fst) (classes2 state) }
243+deleteName :: Name -> (ArgsDAG, Classes) -> (ArgsDAG, Classes)
244+deleteName n (args, classes) = (deleteFromDag n args, filter ((/= n) . fst) classes)
214tcToMaybe :: TC' e a -> Maybe a
246tcToMaybe :: TC' e a -> Maybe a
215tcToMaybe (OK x) = Just x
247tcToMaybe (OK x) = Just x
@@ -221,13 +253,13 @@ inArgTys = map . first . second
222typeclassUnify :: Ctxt ClassInfo -> Context -> Type -> Type -> Maybe [(Name, Type)]
254typeclassUnify :: Ctxt ClassInfo -> Context -> Type -> Type -> Maybe [(Name, Type)]
223typeclassUnify classInfo ctxt ty tyTry = do
255typeclassUnify classInfo ctxt ty tyTry = do
224− res <- tcToMaybe $ match_unify ctxt [] ty retTy [] holes []
256+ res <- tcToMaybe $ match_unify ctxt [] ty retTy [] theHoles []
225− guard $ null (holes \\ map fst res)
257+ guard $ null (theHoles \\ map fst res)
226 let argTys' = map (second $ foldr (.) id [ subst n t | (n, t) <- res ]) tcArgs
258 let argTys' = map (second $ foldr (.) id [ subst n t | (n, t) <- res ]) tcArgs
227 return argTys'
259 return argTys'
229 tyTry' = vToP tyTry
261 tyTry' = vToP tyTry
230− holes = map fst nonTcArgs
262+ theHoles = map fst nonTcArgs
231 retTy = getRetTy tyTry'
263 retTy = getRetTy tyTry'
232 (tcArgs, nonTcArgs) = partition (isTypeClassArg classInfo . snd) $ getArgTys tyTry'
264 (tcArgs, nonTcArgs) = partition (isTypeClassArg classInfo . snd) $ getArgTys tyTry'
@@ -247,30 +279,53 @@ subsets [] = [[]]
247subsets (x : xs) = let ss = subsets xs in map (x :) ss ++ ss
279subsets (x : xs) = let ss = subsets xs in map (x :) ss ++ ss
282+-- not recursive (i.e., doesn't flip iterated identities) at the moment
283+-- recalls the number of flips that have been made
284+flipEqualities :: Type -> [(Int, Type)]
285+flipEqualities t = case t of
286+ eq1@(App (App (App (App eq@(P _ eqty _) tyL) tyR) valL) valR) | eqty == eqTy ->
287+ [(0, eq1), (1, App (App (App (App eq tyR) tyL) valR) valL)]
288+ Bind n binder sc -> (\bind' (j, sc') -> (fst (binderTy bind') + j, Bind n (fmap snd bind') sc'))
289+ <$> traverse flipEqualities binder <*> flipEqualities sc
290+ App f x -> (\(i, f') (j, x') -> (i + j, App f' x'))
291+ <$> flipEqualities f <*> flipEqualities x
250--DONT run vToP first!
294--DONT run vToP first!
251-- | Try to match two types together in a unification-like procedure.
295-- | Try to match two types together in a unification-like procedure.
252-- Returns a list of types and their minimum scores, sorted in order
296-- Returns a list of types and their minimum scores, sorted in order
253-- of increasing score.
297-- of increasing score.
254matchTypesBulk :: forall info. IState -> Int -> Type -> [(info, Type)] -> [(info, Score)]
298matchTypesBulk :: forall info. IState -> Int -> Type -> [(info, Type)] -> [(info, Score)]
255matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues where
299matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues where
256− getStartQueue :: (info, Type) -> Maybe (Score, (info, Q.PQueue Score State))
300+ getStartQueues :: (info, Type) -> Maybe (Score, (info, Q.PQueue Score State))
257− getStartQueue nty@(info, type2) = do
301+ getStartQueues nty@(info, type2) = case mapMaybe startStates ty2s of
258− state <- unifyQueue (State startingHoles dag1 dag2
302+ [] -> Nothing
259− typeClassArgs1 typeClassArgs2
303+ xs -> Just (minimum (map fst xs), (info, Q.fromList xs))
260− mempty usedNames) startingTypes
261− let sc = score state
262− return $ (sc, (info, Q.singleton sc state))
305+ ty2s = (\(i, dag) (j, retTy) -> (i + j, dag, retTy))
306+ <$> flipEqualitiesDag dag2 <*> flipEqualities retTy2
307+ flipEqualitiesDag dag = case dag of
309+ ((n, ty), (pos, deps)) : xs ->
310+ (\(i, ty') (j, xs') -> (i + j , ((n, ty'), (pos, deps)) : xs'))
311+ <$> flipEqualities ty <*> flipEqualitiesDag xs
312+ startStates (numEqFlips, sndDag, sndRetTy) = do
313+ state <- unifyQueue (State startingHoles
314+ (Sided (dag1, typeClassArgs1) (sndDag, typeClassArgs2))
315+ (mempty { equalityFlips = numEqFlips }) usedns) [(retTy1, sndRetTy)]
316+ return (score state, state)
264 (dag2, typeClassArgs2, retTy2) = makeDag (uniqueBinders (map fst argNames1) type2)
319 (dag2, typeClassArgs2, retTy2) = makeDag (uniqueBinders (map fst argNames1) type2)
265 argNames2 = map fst dag2
320 argNames2 = map fst dag2
266− usedNames = map fst (argNames1 ++ argNames2)
321+ usedns = map fst startingHoles
267 startingHoles = argNames1 ++ argNames2
322 startingHoles = argNames1 ++ argNames2
269− startingTypes = (retTy1, retTy2) : []
324+ startingTypes = [(retTy1, retTy2)]
272 startQueueOfQueues :: Q.PQueue Score (info, Q.PQueue Score State)
327 startQueueOfQueues :: Q.PQueue Score (info, Q.PQueue Score State)
273− startQueueOfQueues = Q.fromList $ mapMaybe getStartQueue types
328+ startQueueOfQueues = Q.fromList $ mapMaybe getStartQueues types
275 getAllResults :: Q.PQueue Score (info, Q.PQueue Score State) -> [(info, Score)]
330 getAllResults :: Q.PQueue Score (info, Q.PQueue Score State) -> [(info, Score)]
276 getAllResults q = case Q.minViewWithKey q of
331 getAllResults q = case Q.minViewWithKey q of
@@ -282,7 +337,7 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh
282 Just (Left stateQ') -> case Q.minViewWithKey stateQ' of
337 Just (Left stateQ') -> case Q.minViewWithKey stateQ' of
283 Nothing -> getAllResults q'
338 Nothing -> getAllResults q'
284 Just ((newQscore,_), _) -> getAllResults (Q.add newQscore (info, stateQ') q')
339 Just ((newQscore,_), _) -> getAllResults (Q.add newQscore (info, stateQ') q')
285− Just (Right score) -> (info, score) : getAllResults q'
340+ Just (Right theScore) -> (info, theScore) : getAllResults q'
@@ -291,7 +346,7 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh
292 (dag1, typeClassArgs1, retTy1) = makeDag type1
347 (dag1, typeClassArgs1, retTy1) = makeDag type1
293 argNames1 = map fst dag1
348 argNames1 = map fst dag1
294− makeDag :: Type -> (ArgsDAG, [(Name, Type)], Type)
349+ makeDag :: Type -> (ArgsDAG, Classes, Type)
295 makeDag = first3 (zipWith (\i (ty, deps) -> (ty, (i, deps))) [0..] . reverseDag) .
350 makeDag = first3 (zipWith (\i (ty, deps) -> (ty, (i, deps))) [0..] . reverseDag) .
296 computeDagP (isTypeClassArg classInfo) . vToP
351 computeDagP (isTypeClassArg classInfo) . vToP
297 first3 f (a,b,c) = (f a, b, c)
352 first3 f (a,b,c) = (f a, b, c)
@@ -300,44 +355,45 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh
300 resolveUnis :: [(Name, Type)] -> State -> Maybe (State, [(Type, Type)])
355 resolveUnis :: [(Name, Type)] -> State -> Maybe (State, [(Type, Type)])
301 resolveUnis [] state = Just (state, [])
356 resolveUnis [] state = Just (state, [])
302 resolveUnis ((name, term@(P Bound name2 _)) : xs)
357 resolveUnis ((name, term@(P Bound name2 _)) : xs)
303− state@(State holes args1 args2 _ _ _ _) | isJust findArgs = do
358+ state | isJust findArgs = do
304 ((ty1, ix1), (ty2, ix2)) <- findArgs
359 ((ty1, ix1), (ty2, ix2)) <- findArgs
306 (state'', queue) <- resolveUnis xs state'
361 (state'', queue) <- resolveUnis xs state'
307 let transScore = fromMaybe 0 (abs <$> ((-) <$> ix1 <*> ix2))
362 let transScore = fromMaybe 0 (abs <$> ((-) <$> ix1 <*> ix2))
308− return $ (inScore (\s -> s { transposition = transposition s + transScore }) state'', (ty1, ty2) : queue)
363+ return (inScore (\s -> s { transposition = transposition s + transScore }) state'', (ty1, ty2) : queue)
310− mgetType name xs = fmap ((snd . fst) &&& (fst . snd)) . find ((name ==) . fst . fst) $ xs
365+ unresolved = argsAndClasses state
311− inScore f state = state { score = f (score state) }
366+ inScore f stat = stat { score = f (score stat) }
312− findArgs = ((,) <$> findLeft name state <*> findRight name2 state) <|>
367+ findArgs = ((,) <$> findName name (left unresolved) <*> findName name2 (right unresolved)) <|>
313− ((,) <$> findLeft name2 state <*> findRight name state)
368+ ((,) <$> findName name2 (left unresolved) <*> findName name (right unresolved))
314 matchnames = [name, name2]
369 matchnames = [name, name2]
370+ deleteArgs = deleteName name . deleteName name2
315− holes' = filter (not . (`elem` matchnames) . fst) holes
371+ state' = state { holes = filter (not . (`elem` matchnames) . fst) (holes state)
316− deleteArgs = deleteLeft name . deleteLeft name2 . deleteRight name . deleteRight name2
317− state' = modifyTypes (subst name term) $ deleteArgs
372+ , argsAndClasses = both (modifyTypes (subst name term) . deleteArgs) unresolved}
318− (state { holes = holes'})
320 resolveUnis ((name, term) : xs)
374 resolveUnis ((name, term) : xs)
321− state@(State holes args1 args2 _ _ _ _) = case (findLeft name state, findRight name state) of
375+ state@(State hs unresolved _ _) = case both (findName name) unresolved of
322− (Just (_,ix), Nothing) -> first (addScore (mempty { leftApplied = 1, rightApplied = otherApplied})) <$> nextStep
376+ Sided Nothing Nothing -> Nothing
323− (Nothing, Just (_,ix)) -> first (addScore (mempty { rightApplied = 1, leftApplied = otherApplied})) <$> nextStep
324− (Nothing, Nothing) -> nextStep
325− _ -> error ("Idris internal error: TypeSearch.resolveUnis")
377+ Sided (Just _) (Just _) -> error "Idris internal error: TypeSearch.resolveUnis"
378+ oneOfEach -> first (addScore (both scoreFor oneOfEach)) <$> nextStep
380+ scoreFor (Just _) = mempty { argApp = 1 }
381+ scoreFor Nothing = mempty { argApp = otherApplied }
327 -- find variables which are determined uniquely by the type
382 -- find variables which are determined uniquely by the type
328 -- due to injectivity
383 -- due to injectivity
329 matchedVarMap = usedVars term
384 matchedVarMap = usedVars term
330− both f (x, y) = (f x, f y)
385+ bothT f (x, y) = (f x, f y)
331− (injUsedVars, notInjUsedVars) = both M.keys . M.partition id . M.filterWithKey (\k _-> k `elem` map fst holes) $ M.map snd matchedVarMap
386+ (injUsedVars, notInjUsedVars) = bothT M.keys . M.partition id . M.filterWithKey (\k _-> k `elem` map fst hs) $ M.map snd matchedVarMap
332 varsInTy = injUsedVars ++ notInjUsedVars
387 varsInTy = injUsedVars ++ notInjUsedVars
333 toDelete = name : varsInTy
388 toDelete = name : varsInTy
334− deleteMany = foldr (.) id $ [ deleteLeft t . deleteRight t | t <- toDelete ]
389+ deleteMany = foldr (.) id (map deleteName toDelete)
336 otherApplied = length notInjUsedVars
391 otherApplied = length notInjUsedVars
338− addScore additions state = state { score = score state `mappend` additions }
393+ addScore additions theState = theState { score = let s = score theState in
339− state' = modifyTypes (subst name term) . deleteMany $
394+ s { asymMods = asymMods s `mappend` additions } }
340− state { holes = filter (not . (`elem` toDelete) . fst) holes }
395+ state' = state { holes = filter (not . (`elem` toDelete) . fst) hs
396+ , argsAndClasses = both (modifyTypes (subst name term) . deleteMany) (argsAndClasses state) }
341 nextStep = resolveUnis xs state'
397 nextStep = resolveUnis xs state'
@@ -352,13 +408,13 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh
352 unifyQueue state' (queue ++ queueAdditions)
408 unifyQueue state' (queue ++ queueAdditions)
354 possClassInstances :: [Name] -> Type -> [Type]
410 possClassInstances :: [Name] -> Type -> [Type]
355− possClassInstances usedNames ty = do
411+ possClassInstances usedns ty = do
356 className <- getClassName clss
412 className <- getClassName clss
357 classDef <- lookupCtxt className classInfo
413 classDef <- lookupCtxt className classInfo
358 n <- class_instances classDef
414 n <- class_instances classDef
359 def <- lookupCtxt n (definitions ctxt)
415 def <- lookupCtxt n (definitions ctxt)
360− ty <- normaliseC ctxt [] <$> (case typeFromDef def of Just x -> [x]; Nothing -> [])
416+ nty <- normaliseC ctxt [] <$> (case typeFromDef def of Just x -> [x]; Nothing -> [])
361− let ty' = vToP (uniqueBinders usedNames ty)
417+ let ty' = vToP (uniqueBinders usedns nty)
362 return ty'
418 return ty'
364 (clss, _) = unApply ty
420 (clss, _) = unApply ty
@@ -377,7 +433,7 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh
377 else Q.empty in
433 else Q.empty in
378 Just $ Left (Q.union rest additions)
434 Just $ Left (Q.union rest additions)
380− isFinal (State [] [] [] [] [] score _) = True
436+ isFinal (State [] (Sided ([], []) ([], [])) _ _) = True
381 isFinal _ = False
437 isFinal _ = False
383 -- | Find all possible matches starting from a given state.
439 -- | Find all possible matches starting from a given state.
@@ -386,36 +442,40 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh
386 nextSteps :: State -> [State]
442 nextSteps :: State -> [State]
388 -- Stage 3 - match typeclasses
444 -- Stage 3 - match typeclasses
389− nextSteps (State [] [] [] c1 c2 scoreAcc usedNames) =
445+ nextSteps (State [] unresolved@(Sided ([], c1) ([], c2)) scoreAcc usedns) =
390 if null results3 then results4 else results3
446 if null results3 then results4 else results3
392 -- try to match a typeclass argument from the left with a typeclass argument from the right
448 -- try to match a typeclass argument from the left with a typeclass argument from the right
393 results3 =
449 results3 =
394− catMaybes [ unifyQueue (State [] [] []
450+ catMaybes [ unifyQueue (State []
451+ (Sided ([], deleteFromArgList n1 c1)
395− (deleteFromArgList n1 c1) (map (second subst2for1) (deleteFromArgList n2 c2)) scoreAcc usedNames) [(ty1, ty2)]
452+ ([], map (second subst2for1) (deleteFromArgList n2 c2)))
453+ scoreAcc usedns) [(ty1, ty2)]
396 | (n1, ty1) <- c1, (n2, ty2) <- c2, let subst2for1 = psubst n2 (P Bound n1 ty1)]
454 | (n1, ty1) <- c1, (n2, ty2) <- c2, let subst2for1 = psubst n2 (P Bound n1 ty1)]
398 -- try to hunt match a typeclass constraint by replacing it with an instance
456 -- try to hunt match a typeclass constraint by replacing it with an instance
399− results4 = results4A ++ results4B
457+ results4 = [ State [] (both (\(cs, _, _) -> ([], cs)) sds)
458+ (scoreAcc `mappend` Score 0 0 (both (\(_, amods, _) -> amods) sds))
459+ (usedns ++ sided (++) (both (\(_, _, hs) -> hs) sds))
462+ allMods = parallel defMod mods
463+ mods :: Sided [( Classes, AsymMods, [Name] )]
464+ mods = both (instanceMods . snd) unresolved
465+ defMod :: Sided (Classes, AsymMods, [Name])
466+ defMod = both (\(_, cs) -> (cs, mempty , [])) unresolved
467+ parallel :: Sided a -> Sided [a] -> [Sided a]
468+ parallel (Sided l r) (Sided ls rs) = map (flip Sided r) ls ++ map (Sided l) rs
469+ instanceMods :: Classes -> [( Classes , AsymMods, [Name] )]
470+ instanceMods classes = [ ( newClassArgs, mempty { typeClassApp = 1 }, newHoles )
471+ | (_, ty) <- classes
400− typeClassArgs classes = [ ((n, ty), inst) | (n, ty) <- classes, inst <- possClassInstances usedNames ty ]
472+ , inst <- possClassInstances usedns ty
401− results4A = [ State [] [] []
402− (deleteFromArgList n c1 ++ newClassArgs) c2
403− (scoreAcc `mappend` (mempty { leftTypeClassApp = 1 }))
404− (usedNames ++ newHoles)
405− | ((n, ty), inst) <- typeClassArgs c1
406− , newClassArgs <- maybeToList $ typeclassUnify classInfo ctxt ty inst
473+ , newClassArgs <- maybeToList $ typeclassUnify classInfo ctxt ty inst
407− , let newHoles = map fst newClassArgs ]
408− results4B = [ State [] [] []
409− c1 (deleteFromArgList n c2 ++ newClassArgs)
410− (scoreAcc `mappend` (mempty { rightTypeClassApp = 1 }))
411− (usedNames ++ newHoles)
412− | ((n, ty), inst) <- typeClassArgs c2
413− , newClassArgs <- maybeToList $ typeclassUnify classInfo ctxt ty inst
414− , let newHoles = map fst newClassArgs ]
474+ , let newHoles = map fst newClassArgs ]
417 -- Stage 1 - match arguments
477 -- Stage 1 - match arguments
418− nextSteps (State holes dag1 dag2 c1 c2 scoreAcc usedNames) = results where
478+ nextSteps (State hs (Sided (dagL, c1) (dagR, c2)) scoreAcc usedns) = results where
420 results = concatMap takeSomeClasses results1
480 results = concatMap takeSomeClasses results1
@@ -425,18 +485,29 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh
425 canBeFirst = map fst . filter (S.null . snd . snd)
485 canBeFirst = map fst . filter (S.null . snd . snd)
427 -- try to match an argument from the left with an argument from the right
487 -- try to match an argument from the left with an argument from the right
428− results1 = catMaybes [ unifyQueue (State (filter (not . (`elem` [n1,n2]) . fst) holes) (deleteFromDag n1 dag1)
488+ results1 = catMaybes [ unifyQueue (State (filter (not . (`elem` [n1,n2]) . fst) hs)
489+ (Sided (deleteFromDag n1 dagL, c1)
429− ((inArgTys subst2for1) $ deleteFromDag n2 dag2) c1 (map (second subst2for1) c2) scoreAcc usedNames) [(ty1, ty2)]
490+ (inArgTys subst2for1 $ deleteFromDag n2 dagR, map (second subst2for1) c2))
491+ scoreAcc usedns) [(ty1, ty2)]
492+ | (n1, ty1) <- canBeFirst dagL, (n2, ty2) <- canBeFirst dagR
430− | (n1, ty1) <- canBeFirst dag1, (n2, ty2) <- canBeFirst dag2, let subst2for1 = psubst n2 (P Bound n1 ty1)]
493+ , let subst2for1 = psubst n2 (P Bound n1 ty1)]
433− -- Stage 2 - simply introduce a subset of the typeclasses
497+ -- Stage 2 - simply introduce a subset of the typeclasses
434− -- we've finished, so take some classes
498+ -- we've finished, so take some classes
435− takeSomeClasses (State [] [] [] c1 c2 scoreAcc usedNames) =
499+ takeSomeClasses (State [] unresolved@(Sided ([], _) ([], _)) scoreAcc usedns) =
436− let lc1 = length c1; lc2 = length c2 in
500+ map statesFromMods . prod $ both (classMods . snd) unresolved
502+ swap (Sided l r) = Sided r l
503+ statesFromMods :: Sided (Classes, AsymMods) -> State
504+ statesFromMods sides = let classes = both (\(c, _) -> ([], c)) sides
505+ mods = swap (both snd sides) in
437− [ State [] [] [] c1' c2' (scoreAcc `mappend`
506+ State [] classes (scoreAcc `mappend` (mempty { asymMods = mods })) usedns
438− mempty { rightTypeClassIntro = lc1 - length c1',
507+ classMods :: Classes -> [(Classes, AsymMods)]
439− leftTypeClassIntro = lc2 - length c2' }) usedNames
508+ classMods cs = let lcs = length cs in
440− | c1' <- subsets c1, c2' <- subsets c2 ]
509+ [ (cs', mempty { typeClassIntro = lcs - length cs' }) | cs' <- subsets cs ]
510+ prod :: Sided [a] -> [Sided a]
511+ prod (Sided ls rs) = [Sided l r | l <- ls, r <- rs]
441− -- still have arguments to match, so just be the identity
512+ -- still have arguments to match, so just be the identity
442− takeSomeClasses s = [s]
513+ takeSomeClasses s = [s]