@@ -9,26 +9,28 @@ import Control.Monad (forM_, guard)
99import Data.Function (on)
1010import Data.List (find, sortBy, (\\))
1111import qualified Data.Map as M
12−import Data.Maybe (catMaybes)
12+import Data.Maybe (catMaybes, fromMaybe, isJust)
1313import Data.Monoid (Monoid (mempty, mappend))
1414import Data.Set (Set)
1515import qualified Data.Set as S
1616
1717import Idris.AbsSyntax (addUsingConstraints, addImpl, getContext, getIState, putIState, implicit)
18−import Idris.AbsSyntaxTree (defaultSyntax, Idris, implicitAllowed, prettyIst, PTerm, toplevel)
18+import Idris.AbsSyntaxTree (class_instances, defaultSyntax, Idris,
19+ IState (idris_classes, tt_ctxt),
20+ implicitAllowed, prettyIst, PTerm, toplevel)
1921import Idris.Core.Evaluate (Context (definitions), Def (Function, TyDecl, CaseOp), normaliseC)
2022import Idris.Core.TT
21−import Idris.Core.Unify (unify)
22−import Idris.Delaborate (delabTy)
23+import Idris.Core.Unify (match_unify)
24+import Idris.Delaborate (delab, delabTy)
2325import Idris.Docstrings (noDocs)
2426import Idris.ElabDecls (elabType')
25−import Idris.Output (ihRenderResult, ihPrintResult)
27+import Idris.Output (ihRenderResult, ihPrintResult, ihPrintFunTypes)
2628
2729import System.IO (Handle)
2830
2931
30−searchByType :: (Ord a, Show a) => Handle -> (Context -> Type -> Type -> Maybe a) -> PTerm -> Idris ()
31−searchByType h pred pterm = do
32+searchByType :: (Ord a, Show a) => Handle -> (IState -> Type -> Type -> Maybe a) -> a -> PTerm -> Idris ()
33+searchByType h pred scoreLimit pterm = do
3234 pterm' <- addUsingConstraints syn emptyFC pterm
3335 pterm'' <- implicit toplevel syn n pterm'
3436 i <- getIState
@@ -36,26 +38,29 @@ searchByType h pred pterm = do
3638 ty <- elabType' False toplevel syn (fst noDocs) (snd noDocs) emptyFC [] n pterm'
3739 putIState i -- don't actually make any changes
3840 ihRenderResult h (prettyIst i pterm)
39− ctxt <- getContext
40− let names = searchUsing pred ctxt ty
41− let names' = sortBy (compare `on` (snd . snd)) names
41+ let names = searchUsing pred i ty
42+ let names' = take numLimit . takeWhile ((< scoreLimit) . snd . snd) $
43+ sortBy (compare `on` (snd . snd)) names
4244 forM_ names' $ \(name, (typ, val)) -> do
43− ihPrintResult h ("Score: " ++ show val ++ "\t" ++ show name)
44− ihRenderResult h (prettyIst i (delabTy i name))
45+ ihPrintFunTypes h [] name [(name, delabTy i name)]
46+ ihPrintResult h ("\tScore: " ++ show val ++ "\n")
4547 where
48+ numLimit = 50
4649 syn = defaultSyntax { implicitAllowed = True } -- syntax
4750 n = sMN 0 "searchType" -- name
4851
4952
50−searchUsing :: (Context -> Type -> Type -> Maybe a) -> Context -> Type -> [(Name, (Type, a))]
51−searchUsing pred ctxt ty =
53+searchUsing :: (IState -> Type -> Type -> Maybe a) -> IState -> Type -> [(Name, (Type, a))]
54+searchUsing pred istate ty =
5255 concat . M.elems $ M.mapWithKey (\key -> M.toAscList . M.mapMaybe (f key)) (definitions ctxt)
5356 where
57+ ctxt = tt_ctxt istate
5458 f k x = do
59+ guard $ not (special k)
5560 y <- get (fst4 x)
5661 let ny = normaliseC ctxt [] y
5762 -- traceShow k False `seq` return ()
58− val <- pred ctxt nty ny
63+ val <- pred istate nty ny
5964 return (y, val)
6065 nty = normaliseC ctxt [] ty
6166 fst4 :: (a,b,c,d) -> a
@@ -66,6 +71,9 @@ searchUsing pred ctxt ty =
6671 -- get (Operator ty _ _) = Just ty
6772 get (CaseOp _ ty _ _ _ _) = Just ty
6873 get _ = Nothing
74+ special :: Name -> Bool
75+ special (SN _) = True
76+ special _ = False
6977
7078
7179tcToMaybe :: TC' e a -> Maybe a
@@ -74,12 +82,12 @@ tcToMaybe (Error _) = Nothing
7482
7583
7684
77−searchPred :: (Score -> Int) -> Context -> Type -> Type -> Maybe Int
78−searchPred scoref ctxt ty1 = \ty2 -> case matcher ty2 of
85+searchPred :: (Score -> Int) -> IState -> Type -> Type -> Maybe Int
86+searchPred scoref istate ty1 = \ty2 -> case matcher ty2 of
7987 Nothing -> Nothing
8088 Just xs -> guard (not (null xs)) >> return (minimum (map scoref xs))
8189 where
82− matcher = unifyWithHoles True ctxt ty1
90+ matcher = unifyWithHoles True istate ty1
8391
8492
8593
@@ -124,20 +132,22 @@ deleteFromDag name (((name2, ty), (ix, set)) : xs) = (if name == name2
124132data Score = Score
125133 { transposition :: Int
126134 , leftApplied :: Int
127− , rightApplied :: Int } deriving (Eq, Show)
135+ , rightApplied :: Int
136+ , leftTypeClass :: Int
137+ , rightTypeClass :: Int } deriving (Eq, Show)
128138
129139
130140scoreCriterion :: Score -> Bool
131−scoreCriterion (Score a b c) = True {- not
141+scoreCriterion (Score a b c d e) = True {- not
132142 ( (b > 0 && c > 0) || (b + c) > 2 ) -}
133143
134144defaultScoreFunction :: 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)
136146 -- it's very bad to have *both* upcasting and downcasting
137147
138148instance Monoid Score where
139− mempty = Score 0 0 0
140− (Score a b c) `mappend` (Score d e f) = Score (a + d) (b + e) (c + f)
149+ mempty = Score 0 0 0 0 0
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')
141151
142152
143153type ArgsDAG = [((Name, Type), (Int, Set Name))]
@@ -152,9 +162,9 @@ data State = State
152162
153163
154164--DONT run vToP first!
155−unifyWithHoles :: Bool -> Context -> Type -> Type -> Maybe [Score]
156−unifyWithHoles debugParam ctxt type1 = \type2 -> let
157− (dag2, retTy2) = makeDag (uniqueBinders' argNames1 type2)
165+unifyWithHoles :: Bool -> IState -> Type -> Type -> Maybe [Score]
166+unifyWithHoles debugParam istate type1 = \type2 -> let
167+ (dag2, retTy2) = makeDag (uniqueBinders argNames1 type2)
158168 argNames2 = map (fst . fst) dag2
159169 startingHoles = argNames1 ++ argNames2
160170
@@ -163,6 +173,8 @@ unifyWithHoles debugParam ctxt type1 = \type2 -> let
163173 state <- go (State startingHoles dag1 dag2 mempty) startingTypes
164174 return $ processDags state
165175 where
176+ ctxt = tt_ctxt istate
177+ classInfo = idris_classes istate
166178 (dag1, retTy1) = makeDag type1
167179 argNames1 = map (fst . fst) dag1
168180 makeDag = first (zipWith (\i (ty, deps) -> (ty, (i, deps))) [0..] . reverseDag) . computeDagP . vToP
@@ -174,15 +186,15 @@ unifyWithHoles debugParam ctxt type1 = \type2 -> let
174186 -- update our state with the unification resolutions
175187 updateDags :: [(Name, Type)] -> ResType -> Maybe (ResType, [(Type, Type)], Score)
176188 updateDags [] res = Just (res, [], mempty)
177− updateDags ((name, term@(P Bound name2 _)) : xs) (holes, args1, args2) = do
178− ((ty1, ix1), (ty2, ix2)) <-
179− ((,) <$> mgetType name args1 <*> mgetType name2 args2) <|>
180− ((,) <$> mgetType name2 args1 <*> mgetType name args2)
189+ updateDags ((name, term@(P Bound name2 _)) : xs) (holes, args1, args2) | isJust findArgs = do
190+ ((ty1, ix1), (ty2, ix2)) <- findArgs
181191
182192 (res, queue, score) <- updateDags xs (holes', args1'', args2'')
183193 --traceShow (ty1, ty2) False `seq` return ()
184194 return $ (res, (ty1, ty2) : queue , score { transposition = transposition score + abs (ix2 - ix1) })
185195 where
196+ findArgs = ((,) <$> mgetType name args1 <*> mgetType name2 args2) <|>
197+ ((,) <$> mgetType name2 args1 <*> mgetType name args2)
186198 matchnames = [name, name2]
187199 holes' = holes \\ matchnames
188200 substf = deleteFromDag name . deleteFromDag name2
@@ -208,12 +220,12 @@ unifyWithHoles debugParam ctxt type1 = \type2 -> let
208220
209221
210222 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
212224 go state [] = return state
213225 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 []
215227 --trace ("UnifyResult: " ++ show (ty1, ty2, res, errors)) False `seq` return ()
216− guard (null errors)
228+ --guard (null errors)
217229 ((holes', args1', args2'), queueAdditions, scoreAdditions) <- updateDags res (holes, args1, args2)
218230 let newScore = score `mappend` scoreAdditions
219231 guard $ scoreCriterion newScore
@@ -222,14 +234,35 @@ unifyWithHoles debugParam ctxt type1 = \type2 -> let
222234
223235 processDags :: State -> [Score]
224236 processDags (State [] [] [] scoreAcc) = [scoreAcc]
225− processDags (State holes (_:_) [] scoreAcc) = []
226− processDags (State holes [] (_:_) scoreAcc) = []
227− processDags (State holes dag1 dag2 scoreAcc) = concat [ processDags state | state <- results ] where
237+ --processDags (State holes (_:_) [] scoreAcc) = []
238+ --processDags (State holes [] (_:_) scoreAcc) = []
239+ processDags (State holes dag1 dag2 scoreAcc) = concat [ processDags state | state <- allResults ] where
228240
229241 results = catMaybes [ go (State (holes \\ (map nameOf [ty1, ty2])) (deleteFromDag (nameOf ty1) dag1)
230242 (inArgTys (psubst (nameOf ty2) (P Bound (nameOf ty1) (typeOf ty1))) $ deleteFromDag (nameOf ty2) dag2) scoreAcc) [(typeOf ty1, typeOf ty2)]
231243 | ty1 <- canBeFirst dag1, ty2 <- canBeFirst dag2 {-, exactTypeEquality ctxt (typeOf ty1) (typeOf ty2) -} ]
232244
245+ results2 = [ State (holes \\ [nameOf ty])
246+ (deleteFromDag (nameOf ty) dag1) dag2
247+ (scoreAcc `mappend` (mempty { leftTypeClass = 1 }))
248+ | ty <- typeClassArgs1 ]
249+
250+ typeClassArgs1 = filter (isSaturatedClass . typeOf) dag1
251+ typeClassArgs2 = filter (isSaturatedClass . typeOf) dag2
252+
253+
254+ results3 = [ State (holes \\ [nameOf ty])
255+ dag1 (deleteFromDag (nameOf ty) dag2)
256+ (scoreAcc `mappend` (mempty { rightTypeClass = 1 }))
257+ | ty <- typeClassArgs2 ]
258+
259+ allResults :: [State]
260+ allResults = {- (if not (null typeClasses) then (traceShow typeClasses False `seq` id) else id ) -}
261+ (results ++ results2 ++ results3)
262+ where
263+ typeClasses = filter (isSaturatedClass . typeOf) (dag1 ++ dag2)
264+
265+
233266 -- check if the canBeFirst thing is losing any possibilities
234267
235268
@@ -244,13 +277,14 @@ unifyWithHoles debugParam ctxt type1 = \type2 -> let
244277 deleteIdx _ [] = []
245278 deleteIdx idx l@(x@(i,_,_) : xs) = if i == idx then xs else x : deleteIdx idx xs
246279
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
285+ where
286+ (clss, args) = unApply ty
287+ getClassName (P (TCon _ _) className _) = Just className
288+ getClassName _ = Nothing
289+ argToName arg = show (delab istate arg)
247290
248−
249−
250−uniqueBinders' :: [Name] -> TT Name -> TT Name
251−uniqueBinders' ns (Bind n b sc)
252− = let n' = uniqueName n ns
253− ns' = n' : ns in
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