@@ -30,8 +30,8 @@ import qualified Data.Text as T (pack, isPrefixOf)
3030import Data.Traversable (traverse)
3131
3232import Idris.AbsSyntax (addUsingConstraints, addImpl, getIState, putIState, implicit, logLvl)
33−import Idris.AbsSyntaxTree (class_instances, ClassInfo, defaultSyntax, eqTy, Idris
34− , IState (idris_classes, idris_docstrings, tt_ctxt, idris_outputmode),
33+import Idris.AbsSyntaxTree (interface_instances, InterfaceInfo, defaultSyntax, eqTy, Idris
34+ , IState (idris_interfaces, idris_docstrings, tt_ctxt, idris_outputmode),
3535 implicitAllowed, OutputMode(..), PTerm, toplevel)
3636import Idris.Core.Evaluate (Context (definitions), Def (Function, TyDecl, CaseOp), normaliseC)
3737import Idris.Core.TT hiding (score)
@@ -173,8 +173,8 @@ deleteFromArgList n = filter ((/= n) . fst)
173173-- | Asymmetric modifications to keep track of
174174data AsymMods = Mods
175175 { argApp :: !Int
176− , typeClassApp :: !Int
177− , typeClassIntro :: !Int
176+ , interfaceApp :: !Int
177+ , interfaceIntro :: !Int
178178 } deriving (Eq, Show)
179179
180180
@@ -253,18 +253,18 @@ instance Monoid Score where
253253type ArgsDAG = [((Name, Type), (Int, Set Name))]
254254
255255-- | A list of typeclass constraints
256−type Classes = [(Name, Type)]
256+type Interfaces = [(Name, Type)]
257257
258258-- | The state corresponding to an attempted match of two types.
259259data State = State
260260 { holes :: ![(Name, Type)] -- ^ names which have yet to be resolved
261− , argsAndClasses :: !(Sided (ArgsDAG, Classes))
261+ , argsAndInterfaces :: !(Sided (ArgsDAG, Interfaces))
262262 -- ^ arguments and typeclass constraints for each type which have yet to be resolved
263263 , score :: !Score -- ^ the score so far
264264 , usedNames :: ![Name] -- ^ all names that have been used
265265 } deriving Show
266266
267−modifyTypes :: (Type -> Type) -> (ArgsDAG, Classes) -> (ArgsDAG, Classes)
267+modifyTypes :: (Type -> Type) -> (ArgsDAG, Interfaces) -> (ArgsDAG, Interfaces)
268268modifyTypes f = modifyDag *** modifyList
269269 where
270270 modifyDag = map (first (second f))
@@ -273,11 +273,11 @@ modifyTypes f = modifyDag *** modifyList
273273findNameInArgsDAG :: Name -> ArgsDAG -> Maybe (Type, Maybe Int)
274274findNameInArgsDAG name = fmap ((snd . fst) &&& (Just . fst . snd)) . find ((name ==) . fst . fst)
275275
276−findName :: Name -> (ArgsDAG, Classes) -> Maybe (Type, Maybe Int)
277−findName n (args, classes) = findNameInArgsDAG n args <|> ((,) <$> lookup n classes <*> Nothing)
276+findName :: Name -> (ArgsDAG, Interfaces) -> Maybe (Type, Maybe Int)
277+findName n (args, interfaces) = findNameInArgsDAG n args <|> ((,) <$> lookup n interfaces <*> Nothing)
278278
279−deleteName :: Name -> (ArgsDAG, Classes) -> (ArgsDAG, Classes)
280−deleteName n (args, classes) = (deleteFromDag n args, filter ((/= n) . fst) classes)
279+deleteName :: Name -> (ArgsDAG, Interfaces) -> (ArgsDAG, Interfaces)
280+deleteName n (args, interfaces) = (deleteFromDag n args, filter ((/= n) . fst) interfaces)
281281
282282tcToMaybe :: TC a -> Maybe a
283283tcToMaybe (OK x) = Just x
@@ -287,8 +287,8 @@ inArgTys :: (Type -> Type) -> ArgsDAG -> ArgsDAG
287287inArgTys = map . first . second
288288
289289
290−typeclassUnify :: Ctxt ClassInfo -> Context -> Type -> Type -> Maybe [(Name, Type)]
291−typeclassUnify classInfo ctxt ty tyTry = do
290+interfaceUnify :: Ctxt InterfaceInfo -> Context -> Type -> Type -> Maybe [(Name, Type)]
291+interfaceUnify interfaceInfo ctxt ty tyTry = do
292292 res <- tcToMaybe $ match_unify ctxt [] (ty, Nothing) (retTy, Nothing) [] theHoles []
293293 guard $ null (theHoles \\ map fst res)
294294 let argTys' = map (second $ foldr (.) id [ subst n t | (n, t) <- res ]) tcArgs
@@ -297,13 +297,13 @@ typeclassUnify classInfo ctxt ty tyTry = do
297297 tyTry' = vToP tyTry
298298 theHoles = map fst nonTcArgs
299299 retTy = getRetTy tyTry'
300− (tcArgs, nonTcArgs) = partition (isTypeClassArg classInfo . snd) $ getArgTys tyTry'
300+ (tcArgs, nonTcArgs) = partition (isInterfaceArg interfaceInfo . snd) $ getArgTys tyTry'
301301
302−isTypeClassArg :: Ctxt ClassInfo -> Type -> Bool
303−isTypeClassArg classInfo ty = not (null (getClassName clss >>= flip lookupCtxt classInfo)) where
302+isInterfaceArg :: Ctxt InterfaceInfo -> Type -> Bool
303+isInterfaceArg interfaceInfo ty = not (null (getInterfaceName clss >>= flip lookupCtxt interfaceInfo)) where
304304 (clss, args) = unApply ty
305− getClassName (P (TCon _ _) className _) = [className]
306− getClassName _ = []
305+ getInterfaceName (P (TCon _ _) interfaceName _) = [interfaceName]
306+ getInterfaceName _ = []
307307
308308
309309-- | Compute the power set
@@ -345,12 +345,12 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh
345345 <$> flipEqualities ty <*> flipEqualitiesDag xs
346346 startStates (numEqFlips, sndDag, sndRetTy) = do
347347 state <- unifyQueue (State startingHoles
348− (Sided (dag1, typeClassArgs1) (sndDag, typeClassArgs2))
348+ (Sided (dag1, interfaceArgs1) (sndDag, interfaceArgs2))
349349 (mempty { equalityFlips = numEqFlips }) usedns) [(retTy1, sndRetTy)]
350350 return (score state, state)
351351
352352
353− (dag2, typeClassArgs2, retTy2) = makeDag (uniqueBinders (map fst argNames1) type2)
353+ (dag2, interfaceArgs2, retTy2) = makeDag (uniqueBinders (map fst argNames1) type2)
354354 argNames2 = map fst dag2
355355 usedns = map fst startingHoles
356356 startingHoles = argNames1 ++ argNames2
@@ -376,13 +376,13 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh
376376
377377
378378 ctxt = tt_ctxt istate
379− classInfo = idris_classes istate
379+ interfaceInfo = idris_interfaces istate
380380
381− (dag1, typeClassArgs1, retTy1) = makeDag type1
381+ (dag1, interfaceArgs1, retTy1) = makeDag type1
382382 argNames1 = map fst dag1
383− makeDag :: Type -> (ArgsDAG, Classes, Type)
383+ makeDag :: Type -> (ArgsDAG, Interfaces, Type)
384384 makeDag = first3 (zipWith (\i (ty, deps) -> (ty, (i, deps))) [0..] . reverseDag) .
385− computeDagP (isTypeClassArg classInfo) . vToP . unLazy
385+ computeDagP (isInterfaceArg interfaceInfo) . vToP . unLazy
386386 first3 f (a,b,c) = (f a, b, c)
387387
388388 -- update our state with the unification resolutions
@@ -396,14 +396,14 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh
396396 let transScore = fromMaybe 0 (abs <$> ((-) <$> ix1 <*> ix2))
397397 return (inScore (\s -> s { transposition = transposition s + transScore }) state'', (ty1, ty2) : queue)
398398 where
399− unresolved = argsAndClasses state
399+ unresolved = argsAndInterfaces state
400400 inScore f stat = stat { score = f (score stat) }
401401 findArgs = ((,) <$> findName name (left unresolved) <*> findName name2 (right unresolved)) <|>
402402 ((,) <$> findName name2 (left unresolved) <*> findName name (right unresolved))
403403 matchnames = [name, name2]
404404 deleteArgs = deleteName name . deleteName name2
405405 state' = state { holes = filter (not . (`elem` matchnames) . fst) (holes state)
406− , argsAndClasses = both (modifyTypes (subst name term) . deleteArgs) unresolved}
406+ , argsAndInterfaces = both (modifyTypes (subst name term) . deleteArgs) unresolved}
407407
408408 resolveUnis ((name, term) : xs)
409409 state@(State hs unresolved _ _) = case both (findName name) unresolved of
@@ -427,7 +427,7 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh
427427 addScore additions theState = theState { score = let s = score theState in
428428 s { asymMods = asymMods s `mappend` additions } }
429429 state' = state { holes = filter (not . (`elem` toDelete) . fst) hs
430− , argsAndClasses = both (modifyTypes (subst name term) . deleteMany) (argsAndClasses state) }
430+ , argsAndInterfaces = both (modifyTypes (subst name term) . deleteMany) (argsAndInterfaces state) }
431431 nextStep = resolveUnis xs state'
432432
433433
@@ -443,19 +443,19 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh
443443 guard $ scoreCriterion (score state')
444444 unifyQueue state' (queue ++ queueAdditions)
445445
446− possClassInstances :: [Name] -> Type -> [Type]
447− possClassInstances usedns ty = do
448− className <- getClassName clss
449− classDef <- lookupCtxt className classInfo
450− n <- class_instances classDef
446+ possInterfaceInstances :: [Name] -> Type -> [Type]
447+ possInterfaceInstances usedns ty = do
448+ interfaceName <- getInterfaceName clss
449+ interfaceDef <- lookupCtxt interfaceName interfaceInfo
450+ n <- interface_instances interfaceDef
451451 def <- lookupCtxt (fst n) (definitions ctxt)
452452 nty <- normaliseC ctxt [] <$> (case typeFromDef def of Just x -> [x]; Nothing -> [])
453453 let ty' = vToP (uniqueBinders usedns nty)
454454 return ty'
455455 where
456456 (clss, _) = unApply ty
457− getClassName (P (TCon _ _) className _) = [className]
458− getClassName _ = []
457+ getInterfaceName (P (TCon _ _) interfaceName _) = [interfaceName]
458+ getInterfaceName _ = []
459459
460460 -- 'Just' if the computation hasn't totally failed yet, 'Nothing' if it has
461461 -- 'Left' if we haven't found a terminal state, 'Right' if we have
@@ -496,24 +496,24 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh
496496 | sds <- allMods ]
497497 where
498498 allMods = parallel defMod mods
499− mods :: Sided [( Classes, AsymMods, [Name] )]
499+ mods :: Sided [( Interfaces, AsymMods, [Name] )]
500500 mods = both (instanceMods . snd) unresolved
501− defMod :: Sided (Classes, AsymMods, [Name])
501+ defMod :: Sided (Interfaces, AsymMods, [Name])
502502 defMod = both (\(_, cs) -> (cs, mempty , [])) unresolved
503503 parallel :: Sided a -> Sided [a] -> [Sided a]
504504 parallel (Sided l r) (Sided ls rs) = map (flip Sided r) ls ++ map (Sided l) rs
505− instanceMods :: Classes -> [( Classes , AsymMods, [Name] )]
506− instanceMods classes = [ ( newClassArgs, mempty { typeClassApp = 1 }, newHoles )
507− | (_, ty) <- classes
508− , inst <- possClassInstances usedns ty
509− , newClassArgs <- maybeToList $ typeclassUnify classInfo ctxt ty inst
510− , let newHoles = map fst newClassArgs ]
505+ instanceMods :: Interfaces -> [( Interfaces , AsymMods, [Name] )]
506+ instanceMods interfaces = [ ( newInterfaceArgs, mempty { interfaceApp = 1 }, newHoles )
507+ | (_, ty) <- interfaces
508+ , inst <- possInterfaceInstances usedns ty
509+ , newInterfaceArgs <- maybeToList $ interfaceUnify interfaceInfo ctxt ty inst
510+ , let newHoles = map fst newInterfaceArgs ]
511511
512512
513513 -- Stage 1 - match arguments
514514 nextSteps (State hs (Sided (dagL, c1) (dagR, c2)) scoreAcc usedns) = results where
515515
516− results = concatMap takeSomeClasses results1
516+ results = concatMap takeSomeInterfaces results1
517517
518518 -- we only try to match arguments whose names don't appear in the types
519519 -- of any other arguments
@@ -532,18 +532,18 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh
532532
533533 -- Stage 2 - simply introduce a subset of the typeclasses
534534 -- we've finished, so take some classes
535− takeSomeClasses (State [] unresolved@(Sided ([], _) ([], _)) scoreAcc usedns) =
536− map statesFromMods . prod $ both (classMods . snd) unresolved
535+ takeSomeInterfaces (State [] unresolved@(Sided ([], _) ([], _)) scoreAcc usedns) =
536+ map statesFromMods . prod $ both (interfaceMods . snd) unresolved
537537 where
538538 swap (Sided l r) = Sided r l
539− statesFromMods :: Sided (Classes, AsymMods) -> State
540− statesFromMods sides = let classes = both (\(c, _) -> ([], c)) sides
539+ statesFromMods :: Sided (Interfaces, AsymMods) -> State
540+ statesFromMods sides = let interfaces = both (\(c, _) -> ([], c)) sides
541541 mods = swap (both snd sides) in
542− State [] classes (scoreAcc `mappend` (mempty { asymMods = mods })) usedns
543− classMods :: Classes -> [(Classes, AsymMods)]
544− classMods cs = let lcs = length cs in
545− [ (cs', mempty { typeClassIntro = lcs - length cs' }) | cs' <- subsets cs ]
542+ State [] interfaces (scoreAcc `mappend` (mempty { asymMods = mods })) usedns
543+ interfaceMods :: Interfaces -> [(Interfaces, AsymMods)]
544+ interfaceMods cs = let lcs = length cs in
545+ [ (cs', mempty { interfaceIntro = lcs - length cs' }) | cs' <- subsets cs ]
546546 prod :: Sided [a] -> [Sided a]
547547 prod (Sided ls rs) = [Sided l r | l <- ls, r <- rs]
548548 -- still have arguments to match, so just be the identity
549− takeSomeClasses s = [s]
549+ takeSomeInterfaces s = [s]