@@ -18,9 +18,10 @@ import qualified Data.PriorityQueue.FingerTree as Q
1818import Data.Set (Set)
1919import qualified Data.Set as S
2020import qualified Data.Text as T (pack, isPrefixOf)
21+import Data.Traversable (traverse)
2122
2223import 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,
2425 IState (idris_classes, idris_docstrings, tt_ctxt, idris_outputmode),
2526 implicitAllowed, OutputMode(..), prettyDocumentedIst, PTerm, toplevel)
2627import Idris.Core.Evaluate (Context (definitions), Def (Function, TyDecl, CaseOp), normaliseC)
@@ -168,11 +169,12 @@ both f (Sided l r) = Sided (f l) (f r)
168169
169170data Score = Score
170171 { transposition :: !Int
172+ , equalityFlips :: !Int
171173 , asymMods :: !(Sided AsymMods)
172174 } deriving (Eq, Show)
173175
174176displayScore :: Score -> Doc a
175−displayScore (Score trans amods) = text $ case both noMods amods of
177+displayScore score = text $ case both noMods (asymMods score) of
176178 Sided True True -> "=" -- types are isomorphic
177179 Sided True False -> "<" -- found type is more general than searched type
178180 Sided False True -> ">" -- searched type is more general than found type
@@ -181,15 +183,15 @@ displayScore (Score trans amods) = text $ case both noMods amods of
181183 noMods (Mods app tcApp tcIntro) = app + tcApp + tcIntro == 0
182184
183185scoreCriterion :: Score -> Bool
184−scoreCriterion (Score _ amods) = not
186+scoreCriterion (Score _ _ amods) = not
185187 ( sided (&&) (both ((> 0) . argApp) amods)
186188 || sided (+) (both argApp amods) > 4
187189 || sided (||) (both (\(Mods _ tcApp tcIntro) -> tcApp > 3 || tcIntro > 3) amods)
188190 )
189191
190192defaultScoreFunction :: Score -> Int
191−defaultScoreFunction (Score trans amods) =
192− trans + linearPenalty + upAndDowncastPenalty
193+defaultScoreFunction (Score trans eqFlip amods) =
194+ trans + eqFlip + linearPenalty + upAndDowncastPenalty
193195 where
194196 -- prefer finding a more general type to a less general type
195197 linearPenalty = (\(Sided l r) -> 3 * l + r)
@@ -207,8 +209,8 @@ instance Monoid AsymMods where
207209 (Mods a b c) `mappend` (Mods a' b' c') = Mods (a + a') (b + b') (c + c')
208210
209211instance Monoid Score where
210− mempty = Score 0 mempty
211− (Score t mods) `mappend` (Score t' mods') = Score (t + t') (mods `mappend` mods')
212+ mempty = Score 0 0 mempty
213+ (Score t e mods) `mappend` (Score t' e' mods') = Score (t + t') (e + e') (mods `mappend` mods')
212214
213215-- | A directed acyclic graph representing the arguments to a function
214216-- The 'Int' represents the position of the argument (1st argument, 2nd, etc.)
@@ -277,20 +279,43 @@ subsets [] = [[]]
277279subsets (x : xs) = let ss = subsets xs in map (x :) ss ++ ss
278280
279281
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
292+ t' -> [(0, t')]
293+
280294--DONT run vToP first!
281295-- | Try to match two types together in a unification-like procedure.
282296-- Returns a list of types and their minimum scores, sorted in order
283297-- of increasing score.
284298matchTypesBulk :: forall info. IState -> Int -> Type -> [(info, Type)] -> [(info, Score)]
285299matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues where
286− getStartQueue :: (info, Type) -> Maybe (Score, (info, Q.PQueue Score State))
287− getStartQueue nty@(info, type2) = do
288− state <- unifyQueue (State startingHoles
289− (Sided (dag1, typeClassArgs1) (dag2, typeClassArgs2))
290− mempty usedns) startingTypes
291− let sc = score state
292− return (sc, (info, Q.singleton sc state))
300+ getStartQueues :: (info, Type) -> Maybe (Score, (info, Q.PQueue Score State))
301+ getStartQueues nty@(info, type2) = case mapMaybe startStates ty2s of
302+ [] -> Nothing
303+ xs -> Just (minimum (map fst xs), (info, Q.fromList xs))
293304 where
305+ ty2s = (\(i, dag) (j, retTy) -> (i + j, dag, retTy))
306+ <$> flipEqualitiesDag dag2 <*> flipEqualities retTy2
307+ flipEqualitiesDag dag = case dag of
308+ [] -> [(0, [])]
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)
317+
318+
294319 (dag2, typeClassArgs2, retTy2) = makeDag (uniqueBinders (map fst argNames1) type2)
295320 argNames2 = map fst dag2
296321 usedns = map fst startingHoles
@@ -300,7 +325,7 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh
300325
301326
302327 startQueueOfQueues :: Q.PQueue Score (info, Q.PQueue Score State)
303− startQueueOfQueues = Q.fromList $ mapMaybe getStartQueue types
328+ startQueueOfQueues = Q.fromList $ mapMaybe getStartQueues types
304329
305330 getAllResults :: Q.PQueue Score (info, Q.PQueue Score State) -> [(info, Score)]
306331 getAllResults q = case Q.minViewWithKey q of
@@ -365,8 +390,8 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh
365390
366391 otherApplied = length notInjUsedVars
367392
368− addScore additions theState = theState { score = let (Score t mods) = score theState in
369− Score t (mods `mappend` additions) }
393+ addScore additions theState = theState { score = let s = score theState in
394+ s { asymMods = asymMods s `mappend` additions } }
370395 state' = state { holes = filter (not . (`elem` toDelete) . fst) hs
371396 , argsAndClasses = both (modifyTypes (subst name term) . deleteMany) (argsAndClasses state) }
372397 nextStep = resolveUnis xs state'
@@ -430,7 +455,7 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh
430455
431456 -- try to hunt match a typeclass constraint by replacing it with an instance
432457 results4 = [ State [] (both (\(cs, _, _) -> ([], cs)) sds)
433− (scoreAcc `mappend` Score 0 (both (\(_, amods, _) -> amods) sds))
458+ (scoreAcc `mappend` Score 0 0 (both (\(_, amods, _) -> amods) sds))
434459 (usedns ++ sided (++) (both (\(_, _, hs) -> hs) sds))
435460 | sds <- allMods ]
436461 where
@@ -478,7 +503,7 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh
478503 statesFromMods :: Sided (Classes, AsymMods) -> State
479504 statesFromMods sides = let classes = both (\(c, _) -> ([], c)) sides
480505 mods = swap (both snd sides) in
481− State [] classes (scoreAcc `mappend` Score 0 mods) usedns
506+ State [] classes (scoreAcc `mappend` (mempty { asymMods = mods })) usedns
482507 classMods :: Classes -> [(Classes, AsymMods)]
483508 classMods cs = let lcs = length cs in
484509 [ (cs', mempty { typeClassIntro = lcs - length cs' }) | cs' <- subsets cs ]