@@ -9,26 +9,28 @@ import Control.Monad (forM_, guard)
9import Data.Function (on)
9import Data.Function (on)
10import Data.List (find, sortBy, (\\))
10import Data.List (find, sortBy, (\\))
11import qualified Data.Map as M
11import qualified Data.Map as M
12−import Data.Maybe (catMaybes)
12+import Data.Maybe (catMaybes, fromMaybe, isJust)
13import Data.Monoid (Monoid (mempty, mappend))
13import Data.Monoid (Monoid (mempty, mappend))
14import Data.Set (Set)
14import Data.Set (Set)
15import qualified Data.Set as S
15import qualified Data.Set as S
17import Idris.AbsSyntax (addUsingConstraints, addImpl, getContext, getIState, putIState, implicit)
17import Idris.AbsSyntax (addUsingConstraints, addImpl, getContext, getIState, putIState, implicit)
18+import Idris.AbsSyntaxTree (class_instances, defaultSyntax, Idris,
19+ IState (idris_classes, tt_ctxt),
18−import Idris.AbsSyntaxTree (defaultSyntax, Idris, implicitAllowed, prettyIst, PTerm, toplevel)
20+ implicitAllowed, prettyIst, PTerm, toplevel)
19import Idris.Core.Evaluate (Context (definitions), Def (Function, TyDecl, CaseOp), normaliseC)
21import Idris.Core.Evaluate (Context (definitions), Def (Function, TyDecl, CaseOp), normaliseC)
20import Idris.Core.TT
22import Idris.Core.TT
21−import Idris.Core.Unify (unify)
23+import Idris.Core.Unify (match_unify)
22−import Idris.Delaborate (delabTy)
24+import Idris.Delaborate (delab, delabTy)
23import Idris.Docstrings (noDocs)
25import Idris.Docstrings (noDocs)
24import Idris.ElabDecls (elabType')
26import Idris.ElabDecls (elabType')
25−import Idris.Output (ihRenderResult, ihPrintResult)
27+import Idris.Output (ihRenderResult, ihPrintResult, ihPrintFunTypes)
27import System.IO (Handle)
29import System.IO (Handle)
30−searchByType :: (Ord a, Show a) => Handle -> (Context -> Type -> Type -> Maybe a) -> PTerm -> Idris ()
32+searchByType :: (Ord a, Show a) => Handle -> (IState -> Type -> Type -> Maybe a) -> a -> PTerm -> Idris ()
31−searchByType h pred pterm = do
33+searchByType h pred scoreLimit pterm = do
32 pterm' <- addUsingConstraints syn emptyFC pterm
34 pterm' <- addUsingConstraints syn emptyFC pterm
33 pterm'' <- implicit toplevel syn n pterm'
35 pterm'' <- implicit toplevel syn n pterm'
34 i <- getIState
36 i <- getIState
@@ -36,26 +38,29 @@ searchByType h pred pterm = do
36 ty <- elabType' False toplevel syn (fst noDocs) (snd noDocs) emptyFC [] n pterm'
38 ty <- elabType' False toplevel syn (fst noDocs) (snd noDocs) emptyFC [] n pterm'
37 putIState i -- don't actually make any changes
39 putIState i -- don't actually make any changes
38 ihRenderResult h (prettyIst i pterm)
40 ihRenderResult h (prettyIst i pterm)
40− let names = searchUsing pred ctxt ty
41+ let names = searchUsing pred i ty
42+ let names' = take numLimit . takeWhile ((< scoreLimit) . snd . snd) $
41− let names' = sortBy (compare `on` (snd . snd)) names
43+ sortBy (compare `on` (snd . snd)) names
42 forM_ names' $ \(name, (typ, val)) -> do
44 forM_ names' $ \(name, (typ, val)) -> do
45+ ihPrintFunTypes h [] name [(name, delabTy i name)]
43− ihPrintResult h ("Score: " ++ show val ++ "\t" ++ show name)
46+ ihPrintResult h ("\tScore: " ++ show val ++ "\n")
44− ihRenderResult h (prettyIst i (delabTy i name))
46 syn = defaultSyntax { implicitAllowed = True } -- syntax
49 syn = defaultSyntax { implicitAllowed = True } -- syntax
47 n = sMN 0 "searchType" -- name
50 n = sMN 0 "searchType" -- name
50−searchUsing :: (Context -> Type -> Type -> Maybe a) -> Context -> Type -> [(Name, (Type, a))]
53+searchUsing :: (IState -> Type -> Type -> Maybe a) -> IState -> Type -> [(Name, (Type, a))]
51−searchUsing pred ctxt ty =
54+searchUsing pred istate ty =
52 concat . M.elems $ M.mapWithKey (\key -> M.toAscList . M.mapMaybe (f key)) (definitions ctxt)
55 concat . M.elems $ M.mapWithKey (\key -> M.toAscList . M.mapMaybe (f key)) (definitions ctxt)
57+ ctxt = tt_ctxt istate
54 f k x = do
58 f k x = do
59+ guard $ not (special k)
55 y <- get (fst4 x)
60 y <- get (fst4 x)
56 let ny = normaliseC ctxt [] y
61 let ny = normaliseC ctxt [] y
57 -- traceShow k False `seq` return ()
62 -- traceShow k False `seq` return ()
58− val <- pred ctxt nty ny
63+ val <- pred istate nty ny
59 return (y, val)
64 return (y, val)
60 nty = normaliseC ctxt [] ty
65 nty = normaliseC ctxt [] ty
61 fst4 :: (a,b,c,d) -> a
66 fst4 :: (a,b,c,d) -> a
@@ -66,6 +71,9 @@ searchUsing pred ctxt ty =
66 -- get (Operator ty _ _) = Just ty
71 -- get (Operator ty _ _) = Just ty
67 get (CaseOp _ ty _ _ _ _) = Just ty
72 get (CaseOp _ ty _ _ _ _) = Just ty
68 get _ = Nothing
73 get _ = Nothing
74+ special :: Name -> Bool
75+ special (SN _) = True
71tcToMaybe :: TC' e a -> Maybe a
79tcToMaybe :: TC' e a -> Maybe a
@@ -74,12 +82,12 @@ tcToMaybe (Error _) = Nothing
77−searchPred :: (Score -> Int) -> Context -> Type -> Type -> Maybe Int
85+searchPred :: (Score -> Int) -> IState -> Type -> Type -> Maybe Int
78−searchPred scoref ctxt ty1 = \ty2 -> case matcher ty2 of
86+searchPred scoref istate ty1 = \ty2 -> case matcher ty2 of
79 Nothing -> Nothing
87 Nothing -> Nothing
80 Just xs -> guard (not (null xs)) >> return (minimum (map scoref xs))
88 Just xs -> guard (not (null xs)) >> return (minimum (map scoref xs))
82− matcher = unifyWithHoles True ctxt ty1
90+ matcher = unifyWithHoles True istate ty1
@@ -124,20 +132,22 @@ deleteFromDag name (((name2, ty), (ix, set)) : xs) = (if name == name2
124data Score = Score
132data Score = Score
125 { transposition :: Int
133 { transposition :: Int
126 , leftApplied :: Int
134 , leftApplied :: Int
127− , rightApplied :: Int } deriving (Eq, Show)
135+ , rightApplied :: Int
136+ , leftTypeClass :: Int
137+ , rightTypeClass :: Int } deriving (Eq, Show)
130scoreCriterion :: Score -> Bool
140scoreCriterion :: Score -> Bool
131−scoreCriterion (Score a b c) = True {- not
141+scoreCriterion (Score a b c d e) = True {- not
132 ( (b > 0 && c > 0) || (b + c) > 2 ) -}
142 ( (b > 0 && c > 0) || (b + c) > 2 ) -}
134defaultScoreFunction :: Score -> Int
144defaultScoreFunction :: Score -> Int
135−defaultScoreFunction (Score a b c) = a + 10*b + 10*c + 100*b*c
145+defaultScoreFunction (Score a b c d e) = a + 9*b + 3*c + 12*d + 4*e + 100*(2*b + d)*(2*c + e)
136 -- it's very bad to have *both* upcasting and downcasting
146 -- it's very bad to have *both* upcasting and downcasting
138instance Monoid Score where
148instance Monoid Score where
139− mempty = Score 0 0 0
149+ mempty = Score 0 0 0 0 0
140− (Score a b c) `mappend` (Score d e f) = Score (a + d) (b + e) (c + f)
150+ (Score a b c d e) `mappend` (Score a' b' c' d' e') = Score (a + a') (b + b') (c + c') (d + d') (e + e')
143type ArgsDAG = [((Name, Type), (Int, Set Name))]
153type ArgsDAG = [((Name, Type), (Int, Set Name))]
@@ -152,9 +162,9 @@ data State = State
154--DONT run vToP first!
164--DONT run vToP first!
155−unifyWithHoles :: Bool -> Context -> Type -> Type -> Maybe [Score]
165+unifyWithHoles :: Bool -> IState -> Type -> Type -> Maybe [Score]
156−unifyWithHoles debugParam ctxt type1 = \type2 -> let
166+unifyWithHoles debugParam istate type1 = \type2 -> let
157− (dag2, retTy2) = makeDag (uniqueBinders' argNames1 type2)
167+ (dag2, retTy2) = makeDag (uniqueBinders argNames1 type2)
158 argNames2 = map (fst . fst) dag2
168 argNames2 = map (fst . fst) dag2
159 startingHoles = argNames1 ++ argNames2
169 startingHoles = argNames1 ++ argNames2
@@ -163,6 +173,8 @@ unifyWithHoles debugParam ctxt type1 = \type2 -> let
163 state <- go (State startingHoles dag1 dag2 mempty) startingTypes
173 state <- go (State startingHoles dag1 dag2 mempty) startingTypes
164 return $ processDags state
174 return $ processDags state
176+ ctxt = tt_ctxt istate
177+ classInfo = idris_classes istate
166 (dag1, retTy1) = makeDag type1
178 (dag1, retTy1) = makeDag type1
167 argNames1 = map (fst . fst) dag1
179 argNames1 = map (fst . fst) dag1
168 makeDag = first (zipWith (\i (ty, deps) -> (ty, (i, deps))) [0..] . reverseDag) . computeDagP . vToP
180 makeDag = first (zipWith (\i (ty, deps) -> (ty, (i, deps))) [0..] . reverseDag) . computeDagP . vToP
@@ -174,15 +186,15 @@ unifyWithHoles debugParam ctxt type1 = \type2 -> let
174 -- update our state with the unification resolutions
186 -- update our state with the unification resolutions
175 updateDags :: [(Name, Type)] -> ResType -> Maybe (ResType, [(Type, Type)], Score)
187 updateDags :: [(Name, Type)] -> ResType -> Maybe (ResType, [(Type, Type)], Score)
176 updateDags [] res = Just (res, [], mempty)
188 updateDags [] res = Just (res, [], mempty)
177− updateDags ((name, term@(P Bound name2 _)) : xs) (holes, args1, args2) = do
189+ updateDags ((name, term@(P Bound name2 _)) : xs) (holes, args1, args2) | isJust findArgs = do
178− ((ty1, ix1), (ty2, ix2)) <-
190+ ((ty1, ix1), (ty2, ix2)) <- findArgs
179− ((,) <$> mgetType name args1 <*> mgetType name2 args2) <|>
180− ((,) <$> mgetType name2 args1 <*> mgetType name args2)
182 (res, queue, score) <- updateDags xs (holes', args1'', args2'')
192 (res, queue, score) <- updateDags xs (holes', args1'', args2'')
183 --traceShow (ty1, ty2) False `seq` return ()
193 --traceShow (ty1, ty2) False `seq` return ()
184 return $ (res, (ty1, ty2) : queue , score { transposition = transposition score + abs (ix2 - ix1) })
194 return $ (res, (ty1, ty2) : queue , score { transposition = transposition score + abs (ix2 - ix1) })
196+ findArgs = ((,) <$> mgetType name args1 <*> mgetType name2 args2) <|>
197+ ((,) <$> mgetType name2 args1 <*> mgetType name args2)
186 matchnames = [name, name2]
198 matchnames = [name, name2]
187 holes' = holes \\ matchnames
199 holes' = holes \\ matchnames
188 substf = deleteFromDag name . deleteFromDag name2
200 substf = deleteFromDag name . deleteFromDag name2
@@ -208,12 +220,12 @@ unifyWithHoles debugParam ctxt type1 = \type2 -> let
210 go :: State -> [(Type, Type)] -> Maybe State
222 go :: State -> [(Type, Type)] -> Maybe State
211−-- go (State holes args1 args2 score) queue | trace ("go\n\t" ++ show holes ++ "\n\t" ++ show args1 ++ "\n\t" ++ show args2 ++ "\n\t" ++ show queue) False = undefined
223+ --go (State holes args1 args2 score) queue | trace ("go\n\t" ++ show holes ++ "\n\t" ++ show args1 ++ "\n\t" ++ show args2 ++ "\n\t" ++ show queue) False = undefined
212 go state [] = return state
224 go state [] = return state
213 go (State holes args1 args2 score) ((ty1, ty2) : queue) = do
225 go (State holes args1 args2 score) ((ty1, ty2) : queue) = do
214− (res, errors) <- tcToMaybe $ unify ctxt [] ty1 ty2 [] holes []
226+ res <- tcToMaybe $ match_unify ctxt [] ty1 ty2 [] holes []
215 --trace ("UnifyResult: " ++ show (ty1, ty2, res, errors)) False `seq` return ()
227 --trace ("UnifyResult: " ++ show (ty1, ty2, res, errors)) False `seq` return ()
216− guard (null errors)
228+ --guard (null errors)
217 ((holes', args1', args2'), queueAdditions, scoreAdditions) <- updateDags res (holes, args1, args2)
229 ((holes', args1', args2'), queueAdditions, scoreAdditions) <- updateDags res (holes, args1, args2)
218 let newScore = score `mappend` scoreAdditions
230 let newScore = score `mappend` scoreAdditions
219 guard $ scoreCriterion newScore
231 guard $ scoreCriterion newScore
@@ -222,14 +234,35 @@ unifyWithHoles debugParam ctxt type1 = \type2 -> let
223 processDags :: State -> [Score]
235 processDags :: State -> [Score]
224 processDags (State [] [] [] scoreAcc) = [scoreAcc]
236 processDags (State [] [] [] scoreAcc) = [scoreAcc]
225− processDags (State holes (_:_) [] scoreAcc) = []
237+ --processDags (State holes (_:_) [] scoreAcc) = []
226− processDags (State holes [] (_:_) scoreAcc) = []
238+ --processDags (State holes [] (_:_) scoreAcc) = []
227− processDags (State holes dag1 dag2 scoreAcc) = concat [ processDags state | state <- results ] where
239+ processDags (State holes dag1 dag2 scoreAcc) = concat [ processDags state | state <- allResults ] where
229 results = catMaybes [ go (State (holes \\ (map nameOf [ty1, ty2])) (deleteFromDag (nameOf ty1) dag1)
241 results = catMaybes [ go (State (holes \\ (map nameOf [ty1, ty2])) (deleteFromDag (nameOf ty1) dag1)
230 (inArgTys (psubst (nameOf ty2) (P Bound (nameOf ty1) (typeOf ty1))) $ deleteFromDag (nameOf ty2) dag2) scoreAcc) [(typeOf ty1, typeOf ty2)]
242 (inArgTys (psubst (nameOf ty2) (P Bound (nameOf ty1) (typeOf ty1))) $ deleteFromDag (nameOf ty2) dag2) scoreAcc) [(typeOf ty1, typeOf ty2)]
231 | ty1 <- canBeFirst dag1, ty2 <- canBeFirst dag2 {-, exactTypeEquality ctxt (typeOf ty1) (typeOf ty2) -} ]
243 | ty1 <- canBeFirst dag1, ty2 <- canBeFirst dag2 {-, exactTypeEquality ctxt (typeOf ty1) (typeOf ty2) -} ]
245+ results2 = [ State (holes \\ [nameOf ty])
246+ (deleteFromDag (nameOf ty) dag1) dag2
247+ (scoreAcc `mappend` (mempty { leftTypeClass = 1 }))
248+ | ty <- typeClassArgs1 ]
250+ typeClassArgs1 = filter (isSaturatedClass . typeOf) dag1
251+ typeClassArgs2 = filter (isSaturatedClass . typeOf) dag2
254+ results3 = [ State (holes \\ [nameOf ty])
255+ dag1 (deleteFromDag (nameOf ty) dag2)
256+ (scoreAcc `mappend` (mempty { rightTypeClass = 1 }))
257+ | ty <- typeClassArgs2 ]
259+ allResults :: [State]
260+ allResults = {- (if not (null typeClasses) then (traceShow typeClasses False `seq` id) else id ) -}
261+ (results ++ results2 ++ results3)
263+ typeClasses = filter (isSaturatedClass . typeOf) (dag1 ++ dag2)
233 -- check if the canBeFirst thing is losing any possibilities
266 -- check if the canBeFirst thing is losing any possibilities
@@ -244,13 +277,14 @@ unifyWithHoles debugParam ctxt type1 = \type2 -> let
244 deleteIdx _ [] = []
277 deleteIdx _ [] = []
245 deleteIdx idx l@(x@(i,_,_) : xs) = if i == idx then xs else x : deleteIdx idx xs
278 deleteIdx idx l@(x@(i,_,_) : xs) = if i == idx then xs else x : deleteIdx idx xs
280+ isSaturatedClass :: Type -> Bool
281+ isSaturatedClass ty = fromMaybe False $ do
282+ className <- getClassName clss
283+ let possInstances = concatMap class_instances $ lookupCtxt className classInfo
284+ return $ (SN (sInstanceN className (map argToName args))) `elem` possInstances
286+ (clss, args) = unApply ty
287+ getClassName (P (TCon _ _) className _) = Just className
288+ getClassName _ = Nothing
289+ argToName arg = show (delab istate arg)
250−uniqueBinders' :: [Name] -> TT Name -> TT Name
251−uniqueBinders' ns (Bind n b sc)
252− = let n' = uniqueName n ns
254− Bind n' (fmap (uniqueBinders' ns') b) (uniqueBinders' ns' sc)
255−uniqueBinders' ns (App f a) = App (uniqueBinders' ns f) (uniqueBinders' ns a)
256−uniqueBinders' ns t = t