@@ -106,7 +106,7 @@ computeDagP :: Ord n
107 -> ([((n, TT n), Set n)], [(n, TT n)], TT n)
107 -> ([((n, TT n), Set n)], [(n, TT n)], TT n)
108computeDagP removePred t = (reverse (map f args), reverse removedArgs , retTy) where
108computeDagP removePred t = (reverse (map f args), reverse removedArgs , retTy) where
109− f (n, t) = ((n, t), M.keysSet (usedVars False t))
109+ f (n, t) = ((n, t), M.keysSet (usedVars t))
111 (numArgs, args, removedArgs, retTy) = go 0 [] [] t
111 (numArgs, args, removedArgs, retTy) = go 0 [] [] t
@@ -118,19 +118,19 @@ computeDagP removePred t = (reverse (map f args), reverse removedArgs , retTy) w
118 go k args removedArgs retTy = (k, args, removedArgs, retTy)
118 go k args removedArgs retTy = (k, args, removedArgs, retTy)
120-- | Collect the names and types of all the free variables
120-- | Collect the names and types of all the free variables
122− => Bool -- ^ only collect variables which must be determined due to injectivity
121+-- The Boolean indicates those variables which are determined due to injectivity
122+-- I have not given nearly enough thought to know whether this is correct
123− -> TT n -> Map n (TT n)
123+usedVars :: Ord n => TT n -> Map n (TT n, Bool)
124−usedVars inj = f where
124+usedVars = f True where
125− f (P Bound n t) = M.singleton n t `M.union` f t
125+ f b (P Bound n t) = M.singleton n (t, b) `M.union` f b t
126− f (Bind n binder t2) = (M.delete n (f t2) `M.union`) $ case binder of
126+ f b (Bind n binder t2) = (M.delete n (f b t2) `M.union`) $ case binder of
127− Let t v -> f t `M.union` f v
127+ Let t v -> f b t `M.union` f b v
128− Guess t v -> f t `M.union` f v
128+ Guess t v -> f b t `M.union` f b v
129− b -> f (binderTy b)
129+ bind -> f b (binderTy bind)
130− f (App t1 t2) = f t1 `M.union` (if not inj || isInjective t1 then f t2 else M.empty)
130+ f b (App t1 t2) = f b t1 `M.union` f (b && isInjective t1) t2
131− f (Proj t _) = f t
131+ f b (Proj t _) = f b t
132− f (V j) = error "unexpected! run vToP first"
132+ f _ (V j) = error "unexpected! run vToP first"
133− f _ = M.empty
133+ f _ _ = M.empty
135-- | Remove a node from a directed acyclic graph
135-- | Remove a node from a directed acyclic graph
136deleteFromDag :: Ord n => n -> [((n, TT n), (a, Set n))] -> [((n, TT n), (a, Set n))]
136deleteFromDag :: Ord n => n -> [((n, TT n), (a, Set n))] -> [((n, TT n), (a, Set n))]
@@ -318,18 +318,23 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh
319 resolveUnis ((name, term) : xs)
319 resolveUnis ((name, term) : xs)
320 state@(State holes args1 args2 _ _ _ _) = case (findLeft name state, findRight name state) of
320 state@(State holes args1 args2 _ _ _ _) = case (findLeft name state, findRight name state) of
321− (Just (_,ix), Nothing) -> first (inScore (\score -> score { leftApplied = succ (leftApplied score) })) <$> nextStep
321+ (Just (_,ix), Nothing) -> first (addScore (mempty { leftApplied = 1, rightApplied = otherApplied})) <$> nextStep
322− (Nothing, Just (_, ix)) -> first (inScore (\score -> score { rightApplied = succ (rightApplied score) })) <$> nextStep
322+ (Nothing, Just (_,ix)) -> first (addScore (mempty { rightApplied = 1, leftApplied = otherApplied})) <$> nextStep
323 (Nothing, Nothing) -> nextStep
323 (Nothing, Nothing) -> nextStep
324 _ -> error ("Idris internal error: TypeSearch.resolveUnis")
324 _ -> error ("Idris internal error: TypeSearch.resolveUnis")
326 -- find variables which are determined uniquely by the type
326 -- find variables which are determined uniquely by the type
327 -- due to injectivity
327 -- due to injectivity
328− varsInTy = M.keys $ usedVars True term
328+ matchedVarMap = usedVars term
329+ both f (x, y) = (f x, f y)
330+ (injUsedVars, notInjUsedVars) = both M.keys . M.partition id . M.filterWithKey (\k _-> k `elem` map fst holes) $ M.map snd matchedVarMap
331+ varsInTy = injUsedVars ++ notInjUsedVars
329 toDelete = name : varsInTy
332 toDelete = name : varsInTy
330 deleteMany = foldr (.) id $ [ deleteLeft t . deleteRight t | t <- toDelete ]
333 deleteMany = foldr (.) id $ [ deleteLeft t . deleteRight t | t <- toDelete ]
335+ otherApplied = length notInjUsedVars
332− inScore f state = state { score = f (score state) }
337+ addScore additions state = state { score = score state `mappend` additions }
333 state' = modifyTypes (subst name term) . deleteMany $
338 state' = modifyTypes (subst name term) . deleteMany $
334 state { holes = filter (not . (`elem` toDelete) . fst) holes }
339 state { holes = filter (not . (`elem` toDelete) . fst) holes }
335 nextStep = resolveUnis xs state'
340 nextStep = resolveUnis xs state'