diff --git a/idris.cabal b/idris.cabal index 15264bcd4..66621c485 100644 --- a/idris.cabal +++ b/idris.cabal @@ -151,7 +151,7 @@ Library , Idris.Elab.Clause , Idris.Elab.Data , Idris.Elab.Record - , Idris.Elab.Class + , Idris.Elab.Interface , Idris.Elab.Instance , Idris.Elab.Provider , Idris.Elab.RunElab diff --git a/libs/contrib/Classes/Verified.idr b/libs/contrib/Interfaces/Verified.idr similarity index 99% rename from libs/contrib/Classes/Verified.idr rename to libs/contrib/Interfaces/Verified.idr index b60741f7c..4ff7829b9 100644 --- a/libs/contrib/Classes/Verified.idr +++ b/libs/contrib/Interfaces/Verified.idr @@ -1,4 +1,4 @@ -module Classes.Verified +module Interfaces.Verified import Control.Algebra import Control.Algebra.Lattice diff --git a/libs/contrib/contrib.ipkg b/libs/contrib/contrib.ipkg index ffed203cb..781af8e97 100644 --- a/libs/contrib/contrib.ipkg +++ b/libs/contrib/contrib.ipkg @@ -9,7 +9,7 @@ modules = CFFI, CFFI.Types, CFFI.Memory, Control.Isomorphism.Primitives, Control.Partial, - Classes.Verified, + Interfaces.Verified, Data.Fun, Data.Rel, Data.Hash, diff --git a/libs/oldeffects/Effect/Default.idr b/libs/oldeffects/Effect/Default.idr index 0f94acbbe..1ccc775b6 100644 --- a/libs/oldeffects/Effect/Default.idr +++ b/libs/oldeffects/Effect/Default.idr @@ -1,6 +1,6 @@ module Default -class Default a where +interface Default a where default : a instance Default Int where diff --git a/libs/oldeffects/Effects.idr b/libs/oldeffects/Effects.idr index 3895891fc..b8fa85a7e 100644 --- a/libs/oldeffects/Effects.idr +++ b/libs/oldeffects/Effects.idr @@ -26,7 +26,7 @@ data EFFECT : Type where ||| Handler classes describe how an effect `e` is translated to the ||| underlying computation context `m` for execution. -class Handler (e : Effect) (m : Type -> Type) where +interface Handler (e : Effect) (m : Type -> Type) where ||| How to handle the effect. ||| ||| @ r The resource being handled. diff --git a/src/IRTS/Compiler.hs b/src/IRTS/Compiler.hs index ff339bda4..99fca943c 100644 --- a/src/IRTS/Compiler.hs +++ b/src/IRTS/Compiler.hs @@ -628,7 +628,7 @@ irAlt top vs _ (ConCase n t args sc) = do LConCase (-1) n usedArgs <$> irSC top (methodVars `M.union` vs) sc where methodVars = case n of - SN (InstanceCtorN className) + SN (InstanceCtorN interfaceName) -> M.fromList [(v, VI { viMethod = Just $ mkFieldName n i }) | (v,i) <- zip args [0..]] diff --git a/src/Idris/ASTUtils.hs b/src/Idris/ASTUtils.hs index 48bed8cfc..1b021e80f 100644 --- a/src/Idris/ASTUtils.hs +++ b/src/Idris/ASTUtils.hs @@ -40,7 +40,7 @@ f = do module Idris.ASTUtils( Field(), cg_usedpos, ctxt_lookup, fgetState, fmodifyState , fputState, idris_fixities, ist_callgraph, ist_optimisation - , known_classes, known_terms, opt_detaggable, opt_inaccessible + , known_interfaces, known_terms, opt_detaggable, opt_inaccessible , opts_idrisCmdline, repl_definitions ) where @@ -148,8 +148,8 @@ known_terms :: Field IState (Ctxt (Def, Injectivity, Accessibility, Totality, Me known_terms = Field (definitions . tt_ctxt) (\v state -> state {tt_ctxt = (tt_ctxt state) {definitions = v}}) -known_classes :: Field IState (Ctxt ClassInfo) -known_classes = Field idris_classes (\v state -> state {idris_classes = idris_classes state}) +known_interfaces :: Field IState (Ctxt InterfaceInfo) +known_interfaces = Field idris_interfaces (\v state -> state {idris_interfaces = idris_interfaces state}) -- | Names defined at the repl diff --git a/src/Idris/AbsSyntax.hs b/src/Idris/AbsSyntax.hs index 99c8e3e32..b332eb645 100644 --- a/src/Idris/AbsSyntax.hs +++ b/src/Idris/AbsSyntax.hs @@ -449,12 +449,12 @@ addInstance :: Bool -- ^ whether the name is an Integer instance -> Idris () addInstance int res n i = do ist <- getIState - case lookupCtxt n (idris_classes ist) of + case lookupCtxt n (idris_interfaces ist) of [CI a b c d e ins fds] -> - do let cs = addDef n (CI a b c d e (addI i ins) fds) (idris_classes ist) - putIState $ ist { idris_classes = cs } - _ -> do let cs = addDef n (CI (sMN 0 "none") [] [] [] [] [(i, res)] []) (idris_classes ist) - putIState $ ist { idris_classes = cs } + do let cs = addDef n (CI a b c d e (addI i ins) fds) (idris_interfaces ist) + putIState $ ist { idris_interfaces = cs } + _ -> do let cs = addDef n (CI (sMN 0 "none") [] [] [] [] [(i, res)] []) (idris_interfaces ist) + putIState $ ist { idris_interfaces = cs } where addI, insI :: Name -> [(Name, Bool)] -> [(Name, Bool)] addI i ins | int = (i, res) : ins | chaser n = ins ++ [(i, res)] @@ -493,13 +493,13 @@ getOpenImpl :: Idris [Name] getOpenImpl = do ist <- getIState return (idris_openimpls ist) -addClass :: Name -> ClassInfo -> Idris () -addClass n i +addInterface :: Name -> InterfaceInfo -> Idris () +addInterface n i = do ist <- getIState - let i' = case lookupCtxt n (idris_classes ist) of - [c] -> c { class_instances = class_instances i } + let i' = case lookupCtxt n (idris_interfaces ist) of + [c] -> c { interface_instances = interface_instances i } _ -> i - putIState $ ist { idris_classes = addDef n i' (idris_classes ist) } + putIState $ ist { idris_interfaces = addDef n i' (idris_interfaces ist) } addRecord :: Name -> RecordInfo -> Idris () addRecord n ri = do ist <- getIState @@ -1353,8 +1353,8 @@ expandParamsD rhs ist dec ps ns (PParams f params pds) -- (map (expandParamsD ist dec ps ns) pds) expandParamsD rhs ist dec ps ns (PMutual f pds) = PMutual f (map (expandParamsD rhs ist dec ps ns) pds) -expandParamsD rhs ist dec ps ns (PClass doc info f cs n nfc params pDocs fds decls cn cd) - = PClass doc info f +expandParamsD rhs ist dec ps ns (PInterface doc info f cs n nfc params pDocs fds decls cn cd) + = PInterface doc info f (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs) n nfc (map (\(n, fc, t) -> (n, fc, expandParams dec ps ns [] t)) params) diff --git a/src/Idris/AbsSyntaxTree.hs b/src/Idris/AbsSyntaxTree.hs index 637b73a3c..2cd97951d 100644 --- a/src/Idris/AbsSyntaxTree.hs +++ b/src/Idris/AbsSyntaxTree.hs @@ -216,7 +216,7 @@ data IState = IState { , idris_infixes :: [FixDecl] -- ^ Currently defined infix operators , idris_implicits :: Ctxt [PArg] , idris_statics :: Ctxt [Bool] - , idris_classes :: Ctxt ClassInfo + , idris_interfaces :: Ctxt InterfaceInfo , idris_openimpls :: [Name] -- ^ Privileged implementations, will resolve immediately , idris_records :: Ctxt RecordInfo , idris_dsls :: Ctxt DSL @@ -347,7 +347,7 @@ primDefs = [ sUN "unsafePerformPrimIO" data IBCWrite = IBCFix FixDecl | IBCImp Name | IBCStatic Name - | IBCClass Name + | IBCInterface Name | IBCRecord Name | IBCInstance Bool Bool Name Name | IBCDSL Name @@ -719,7 +719,7 @@ data PDecl' t -- | Type class: arguments are documentation, syntax info, source -- location, constraints, class name, class name location, -- parameters, method declarations, optional constructor name - | PClass (Docstring (Either Err t)) SyntaxInfo FC + | PInterface (Docstring (Either Err t)) SyntaxInfo FC [(Name, t)] -- constraints Name -- class name FC -- accurate location of class name @@ -912,8 +912,8 @@ mapPDeclFC f g (PRecord doc syn fc opts n nfc params paramdocs fields ctor ctorD (fmap (\(ctorN, ctorNFC) -> (ctorN, g ctorNFC)) ctor) ctorDoc syn' -mapPDeclFC f g (PClass doc syn fc constrs n nfc params paramDocs det body ctor ctorDoc) = - PClass doc syn (f fc) +mapPDeclFC f g (PInterface doc syn fc constrs n nfc params paramDocs det body ctor ctorDoc) = + PInterface doc syn (f fc) (map (\(constrn, constr) -> (constrn, mapPTermFC f g constr)) constrs) n (g nfc) (map (\(n, nfc, pty) -> (n, g nfc, mapPTermFC f g pty)) params) paramDocs (map (\(dn, dnfc) -> (dn, g dnfc)) det) @@ -964,7 +964,7 @@ declared (PParams _ _ ds) = concatMap declared ds declared (POpenInterfaces _ _ ds) = concatMap declared ds declared (PNamespace _ _ ds) = concatMap declared ds declared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn) -declared (PClass _ _ _ _ n _ _ _ _ ms cn cd) = n : (map fst (maybeToList cn) ++ concatMap declared ms) +declared (PInterface _ _ _ _ n _ _ _ _ ms cn cd) = n : (map fst (maybeToList cn) ++ concatMap declared ms) declared (PInstance _ _ _ _ _ _ _ _ _ _ _ _ _ mn _) = case mn of Nothing -> [] @@ -988,7 +988,7 @@ tldeclared (PParams _ _ ds) = [] tldeclared (POpenInterfaces _ _ ds) = concatMap tldeclared ds tldeclared (PMutual _ ds) = concatMap tldeclared ds tldeclared (PNamespace _ _ ds) = concatMap tldeclared ds -tldeclared (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap tldeclared ms) +tldeclared (PInterface _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap tldeclared ms) tldeclared (PInstance _ _ _ _ _ _ _ _ _ _ _ _ _ mn _) = case mn of Nothing -> [] @@ -1008,7 +1008,7 @@ defined (PParams _ _ ds) = concatMap defined ds defined (POpenInterfaces _ _ ds) = concatMap defined ds defined (PNamespace _ _ ds) = concatMap defined ds defined (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn) -defined (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap defined ms) +defined (PInterface _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap defined ms) defined (PInstance _ _ _ _ _ _ _ _ _ _ _ _ _ mn _) = case mn of Nothing -> [] @@ -1412,18 +1412,18 @@ highestFC (PAppImpl t _) = highestFC t -- Type class data -data ClassInfo = CI { - instanceCtorName :: Name - , class_methods :: [(Name, (Bool, FnOpts, PTerm))] -- ^ flag whether it's a "data" method - , class_defaults :: [(Name, (Name, PDecl))] -- ^ method name -> default impl - , class_default_superclasses :: [PDecl] - , class_params :: [Name] - , class_instances :: [(Name, Bool)] -- ^ the Bool is whether to include in instance search, so named instances are excluded - , class_determiners :: [Int] +data InterfaceInfo = CI { + instanceCtorName :: Name + , interface_methods :: [(Name, (Bool, FnOpts, PTerm))] -- ^ flag whether it's a "data" method + , interface_defaults :: [(Name, (Name, PDecl))] -- ^ method name -> default impl + , interface_default_super_interfaces :: [PDecl] + , interface_params :: [Name] + , interface_instances :: [(Name, Bool)] -- ^ the Bool is whether to include in instance search, so named instances are excluded + , interface_determiners :: [Int] } deriving (Show, Generic) {-! -deriving instance Binary ClassInfo -deriving instance NFData ClassInfo +deriving instance Binary InterfaceInfo +deriving instance NFData InterfaceInfo !-} -- Record data @@ -2241,7 +2241,7 @@ showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) < showDeclImp o (POpenInterfaces _ ns ps) = text "open" <+> braces (text (show ns) <> line <> showDecls o ps <> line) showDeclImp o (PNamespace n fc ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line) showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn) -showDeclImp o (PClass _ _ _ cs n _ ps _ _ ds _ _) +showDeclImp o (PInterface _ _ _ cs n _ ps _ _ ds _ _) = text "interface" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds showDeclImp o (PInstance _ _ _ _ cs _ acc _ n _ _ _ t _ ds) = text "implementation" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds diff --git a/src/Idris/CaseSplit.hs b/src/Idris/CaseSplit.hs index 053296f84..65fd2092d 100644 --- a/src/Idris/CaseSplit.hs +++ b/src/Idris/CaseSplit.hs @@ -401,8 +401,8 @@ getClause :: Int -- ^ line number that the type is declared on -> Idris String getClause l fn un fp = do i <- getIState - case lookupCtxt un (idris_classes i) of - [c] -> return (mkClassBodies i (class_methods c)) + case lookupCtxt un (idris_interfaces i) of + [c] -> return (mkInterfaceBodies i (interface_methods c)) _ -> do ty_in <- getInternalApp fp l let ty = case ty_in of PTyped n t -> t @@ -436,8 +436,8 @@ getClause l fn un fp sUN "z"]) used -- write method declarations, indent with 4 spaces - mkClassBodies :: IState -> [(Name, (Bool, FnOpts, PTerm))] -> String - mkClassBodies i ns + mkInterfaceBodies :: IState -> [(Name, (Bool, FnOpts, PTerm))] -> String + mkInterfaceBodies i ns = showSep "\n" (zipWith (\(n, (_, _, ty)) m -> " " ++ def (show (nsroot n)) ++ " " diff --git a/src/Idris/DeepSeq.hs b/src/Idris/DeepSeq.hs index ce9f664b2..32d692791 100644 --- a/src/Idris/DeepSeq.hs +++ b/src/Idris/DeepSeq.hs @@ -91,7 +91,7 @@ instance NFData PAltType instance (NFData t) => NFData (PTactic' t) instance (NFData t) => NFData (PDo' t) instance (NFData t) => NFData (PArg' t) -instance NFData ClassInfo +instance NFData InterfaceInfo instance NFData RecordInfo instance NFData OptInfo instance NFData TypeInfo diff --git a/src/Idris/Docs.hs b/src/Idris/Docs.hs index e88db0214..1d785e8aa 100644 --- a/src/Idris/Docs.hs +++ b/src/Idris/Docs.hs @@ -45,7 +45,7 @@ type FunDoc = FunDoc' (Docstring DocTerm) data Docs' d = FunDoc (FunDoc' d) | DataDoc (FunDoc' d) -- type constructor docs [FunDoc' d] -- data constructor docs - | ClassDoc Name d -- class docs + | InterfaceDoc Name d -- class docs [FunDoc' d] -- method docs [(Name, Maybe d)] -- parameters and their docstrings [(Maybe Name, PTerm, (d, [(Name, d)]))] -- instances: name for named instances, the constraint term, the docs @@ -139,7 +139,7 @@ pprintDocs ist (DataDoc t args) if null args then text "No constructors." else nest 4 (text "Constructors:" <> line <> vsep (map (pprintFDWithoutTotality ist False) args)) -pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses ctor) +pprintDocs ist (InterfaceDoc n doc meths params instances sub_interfaces super_interfaces ctor) = nest 4 (text "Interface" <+> prettyName True (ppopt_impl ppo) [] n <> if nullDocstring doc then empty @@ -164,13 +164,13 @@ pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses ct else line <$> nest 4 (text "Named implementations:" <$> vsep (map pprintInstance namedInstances))) <> - (if null subclasses then empty + (if null sub_interfaces then empty else line <$> nest 4 (text "Child interfaces:" <$> - vsep (map (dumpInstance . prettifySubclasses) subclasses))) + vsep (map (dumpInstance . prettifySubInterfaces) sub_interfaces))) <> - (if null superclasses then empty + (if null super_interfaces then empty else line <$> nest 4 (text "Default parent implementations:" <$> - vsep (map dumpInstance superclasses))) + vsep (map dumpInstance super_interfaces))) where params' = zip pNames (repeat False) @@ -213,10 +213,10 @@ pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses ct dumpInstance :: PTerm -> Doc OutputAnnotation dumpInstance = pprintPTerm ppo params' [] infixes - prettifySubclasses (PPi (Constraint _ _) _ _ tm _) = prettifySubclasses tm - prettifySubclasses (PPi plcity nm fc t1 t2) = PPi plcity (safeHead nm pNames) NoFC (prettifySubclasses t1) (prettifySubclasses t2) - prettifySubclasses (PApp fc ref args) = PApp fc ref $ updateArgs pNames args - prettifySubclasses tm = tm + prettifySubInterfaces (PPi (Constraint _ _) _ _ tm _) = prettifySubInterfaces tm + prettifySubInterfaces (PPi plcity nm fc t1 t2) = PPi plcity (safeHead nm pNames) NoFC (prettifySubInterfaces t1) (prettifySubInterfaces t2) + prettifySubInterfaces (PApp fc ref args) = PApp fc ref $ updateArgs pNames args + prettifySubInterfaces tm = tm safeHead _ (y:_) = y safeHead x [] = x @@ -228,9 +228,9 @@ pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses ct updateRef nm (PRef fc _ _) = PRef fc [] nm updateRef _ pt = pt - isSubclass (PPi (Constraint _ _) _ _ (PApp _ _ args) (PApp _ (PRef _ _ nm) args')) = nm == n && map getTm args == map getTm args' - isSubclass (PPi _ _ _ _ pt) = isSubclass pt - isSubclass _ = False + isSubInterface (PPi (Constraint _ _) _ _ (PApp _ _ args) (PApp _ (PRef _ _ nm) args')) = nm == n && map getTm args == map getTm args' + isSubInterface (PPi _ _ _ _ pt) = isSubInterface pt + isSubInterface _ = False prettyParameters = if any (isJust . snd) params @@ -287,24 +287,24 @@ getDocs n@(NS n' ns) w | n' == modDocName " do not exist! This shouldn't have happened and is a bug." getDocs n w = do i <- getIState - docs <- if | Just ci <- lookupCtxtExact n (idris_classes i) - -> docClass n ci + docs <- if | Just ci <- lookupCtxtExact n (idris_interfaces i) + -> docInterface n ci | Just ri <- lookupCtxtExact n (idris_records i) -> docRecord n ri | Just ti <- lookupCtxtExact n (idris_datatypes i) -> docData n ti - | Just class_ <- classNameForInst i n + | Just interface_ <- interfaceNameForInst i n -> do fd <- docFun n - return $ NamedInstanceDoc class_ fd + return $ NamedInstanceDoc interface_ fd | otherwise -> do fd <- docFun n return (FunDoc fd) return $ fmap (howMuch w) docs - where classNameForInst :: IState -> Name -> Maybe Name - classNameForInst ist n = + where interfaceNameForInst :: IState -> Name -> Maybe Name + interfaceNameForInst ist n = listToMaybe [ cn - | (cn, ci) <- toAlist (idris_classes ist) - , n `elem` map fst (class_instances ci) + | (cn, ci) <- toAlist (idris_interfaces ist) + , n `elem` map fst (interface_instances ci) ] docData :: Name -> TypeInfo -> Idris Docs @@ -313,30 +313,30 @@ docData n ti cdocs <- mapM docFun (con_names ti) return (DataDoc tdoc cdocs) -docClass :: Name -> ClassInfo -> Idris Docs -docClass n ci +docInterface :: Name -> InterfaceInfo -> Idris Docs +docInterface n ci = do i <- getIState let docStrings = listToMaybe $ lookupCtxt n $ idris_docstrings i docstr = maybe emptyDocstring fst docStrings params = map (\pn -> (pn, docStrings >>= (lookup pn . snd))) - (class_params ci) + (interface_params ci) docsForInstance inst = fromMaybe (emptyDocstring, []) . flip lookupCtxtExact (idris_docstrings i) $ inst instances = map (\inst -> (namedInst inst, delabTy i inst, docsForInstance inst)) - (nub (map fst (class_instances ci))) - (subclasses, instances') = partition (isSubclass . (\(_,tm,_) -> tm)) instances - superclasses = catMaybes $ map getDInst (class_default_superclasses ci) - mdocs <- mapM (docFun . fst) (class_methods ci) + (nub (map fst (interface_instances ci))) + (sub_interfaces, instances') = partition (isSubInterface . (\(_,tm,_) -> tm)) instances + super_interfaces = catMaybes $ map getDInst (interface_default_super_interfaces ci) + mdocs <- mapM (docFun . fst) (interface_methods ci) let ctorN = instanceCtorName ci ctorDocs <- case basename ctorN of SN _ -> return Nothing _ -> fmap Just $ docFun ctorN - return $ ClassDoc + return $ InterfaceDoc n docstr mdocs params - instances' (map (\(_,tm,_) -> tm) subclasses) superclasses + instances' (map (\(_,tm,_) -> tm) sub_interfaces) super_interfaces ctorDocs where namedInst (NS n ns) = fmap (flip NS ns) (namedInst n) @@ -346,11 +346,11 @@ docClass n ci getDInst (PInstance _ _ _ _ _ _ _ _ _ _ _ _ t _ _) = Just t getDInst _ = Nothing - isSubclass (PPi (Constraint _ _) _ _ (PApp _ _ args) (PApp _ (PRef _ _ nm) args')) + isSubInterface (PPi (Constraint _ _) _ _ (PApp _ _ args) (PApp _ (PRef _ _ nm) args')) = nm == n && map getTm args == map getTm args' - isSubclass (PPi _ _ _ _ pt) - = isSubclass pt - isSubclass _ + isSubInterface (PPi _ _ _ _ pt) + = isSubInterface pt + isSubInterface _ = False docRecord :: Name -> RecordInfo -> Idris Docs diff --git a/src/Idris/Elab/Clause.hs b/src/Idris/Elab/Clause.hs index 986d8b9a9..c45a7f715 100644 --- a/src/Idris/Elab/Clause.hs +++ b/src/Idris/Elab/Clause.hs @@ -1100,7 +1100,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock) addResolvesArgs fc (Bind n (Pi _ ty _) sc) (a : args) | (P _ cn _, _) <- unApply ty, getTm a == Placeholder - = case lookupCtxtExact cn (idris_classes ist) of + = case lookupCtxtExact cn (idris_interfaces ist) of Just _ -> a { getTm = PResolveTC fc } : addResolvesArgs fc sc args Nothing -> a : addResolvesArgs fc sc args addResolvesArgs fc (Bind n (Pi _ ty _) sc) (a : args) diff --git a/src/Idris/Elab/Instance.hs b/src/Idris/Elab/Instance.hs index d563efc9c..cdc3429f4 100644 --- a/src/Idris/Elab/Instance.hs +++ b/src/Idris/Elab/Instance.hs @@ -77,7 +77,7 @@ elabInstance :: ElabInfo -> Idris () elabInstance info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t expn ds = do ist <- getIState - (n, ci) <- case lookupCtxtName n (idris_classes ist) of + (n, ci) <- case lookupCtxtName n (idris_interfaces ist) of [c] -> return c [] -> ifail $ show fc ++ ":" ++ show n ++ " is not an interface" cs -> tclift $ tfail $ At fc @@ -89,22 +89,22 @@ elabInstance info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t let totopts = Dictionary : Inlinable : opts - let emptyclass = null (class_methods ci) + let emptyinterface = null (interface_methods ci) when (what /= EDefns) $ do nty <- elabType' True info syn doc argDocs fc totopts iname NoFC (piBindp expl_param pextra t) -- if the instance type matches any of the instances we have already, -- and it's not a named instance, then it's overlapping, so report an error case expn of - Nothing -> do mapM_ (maybe (return ()) overlapping . findOverlapping ist (class_determiners ci) (delab ist nty)) - (map fst $ class_instances ci) + Nothing -> do mapM_ (maybe (return ()) overlapping . findOverlapping ist (interface_determiners ci) (delab ist nty)) + (map fst $ interface_instances ci) addInstance intInst True n iname Just _ -> addInstance intInst False n iname - when (what /= ETypes && (not (null ds && not emptyclass))) $ do + when (what /= ETypes && (not (null ds && not emptyinterface))) $ do -- Add the parent implementation names to the privileged set oldOpen <- addOpenImpl parents - let ips = zip (class_params ci) ps + let ips = zip (interface_params ci) ps let ns = case n of NS n ns' -> ns' _ -> [] @@ -118,9 +118,9 @@ elabInstance info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t let pnames = nub $ map pname (concat (nub wparams)) ++ concatMap (namesIn [] ist) ps - let superclassInstances = map (substInstance ips pnames) (class_default_superclasses ci) - undefinedSuperclassInstances <- filterM (fmap not . isOverlapping ist) superclassInstances - mapM_ (rec_elabDecl info EAll info) undefinedSuperclassInstances + let superInterfaceInstances = map (substInstance ips pnames) (interface_default_super_interfaces ci) + undefinedSuperInterfaceInstances <- filterM (fmap not . isOverlapping ist) superInterfaceInstances + mapM_ (rec_elabDecl info EAll info) undefinedSuperInterfaceInstances ist <- getIState -- Bring variables in instance head into scope when building the @@ -132,7 +132,7 @@ elabInstance info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t _ -> (zip headVars (repeat Placeholder), Erased) logElab 3 $ "Head var types " ++ show headVarTypes ++ " from " ++ show ty - let all_meths = map (nsroot . fst) (class_methods ci) + let all_meths = map (nsroot . fst) (interface_methods ci) let mtys = map (\ (n, (inj, op, t)) -> let t_in = substMatchesShadow ips pnames t mnamemap = @@ -142,16 +142,16 @@ elabInstance info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t t' = substMatchesShadow mnamemap pnames t_in in (decorate ns iname n, op, coninsert cs pextra t', t')) - (class_methods ci) + (interface_methods ci) logElab 3 (show (mtys, ips)) - logElab 5 ("Before defaults: " ++ show ds ++ "\n" ++ show (map fst (class_methods ci))) - let ds_defs = insertDefaults ist iname (class_defaults ci) ns ds + logElab 5 ("Before defaults: " ++ show ds ++ "\n" ++ show (map fst (interface_methods ci))) + let ds_defs = insertDefaults ist iname (interface_defaults ci) ns ds logElab 3 ("After defaults: " ++ show ds_defs ++ "\n") - let ds' = reorderDefs (map fst (class_methods ci)) ds_defs + let ds' = reorderDefs (map fst (interface_methods ci)) ds_defs logElab 1 ("Reordered: " ++ show ds' ++ "\n") - mapM_ (warnMissing ds' ns iname) (map fst (class_methods ci)) - mapM_ (checkInClass (map fst (class_methods ci))) (concatMap defined ds') + mapM_ (warnMissing ds' ns iname) (map fst (interface_methods ci)) + mapM_ (checkInInterface (map fst (interface_methods ci))) (concatMap defined ds') let wbTys = map mkTyDecl mtys let wbVals_orig = map (decorateid (decorate ns iname)) ds' ist <- getIState @@ -199,14 +199,14 @@ elabInstance info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t mapM_ (rec_elabDecl info EAll info) wbVals' - mapM_ (checkInjectiveDef fc (class_methods ci)) (zip ds' wbVals') + mapM_ (checkInjectiveDef fc (interface_methods ci)) (zip ds' wbVals') pop_estack setOpenImpl oldOpen -- totalityCheckBlock - checkInjectiveArgs fc n (class_determiners ci) (lookupTyExact iname (tt_ctxt ist)) + checkInjectiveArgs fc n (interface_determiners ci) (lookupTyExact iname (tt_ctxt ist)) addIBC (IBCInstance intInst (isNothing expn) n iname) where @@ -228,7 +228,7 @@ elabInstance info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t (substMatchesShadow ips pnames t) expn ds isOverlapping i (PInstance doc argDocs syn _ _ _ _ _ n nfc ps pextra t expn _) - = case lookupCtxtName n (idris_classes i) of + = case lookupCtxtName n (idris_interfaces i) of [(n, ci)] -> let iname = (mkiname n (namespace info) ps expn) in case lookupTy iname (tt_ctxt i) of [] -> elabFindOverlapping i ci iname syn t @@ -255,7 +255,7 @@ elabInstance info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t ctxt <- getContext (cty, _) <- recheckC (constraintNS info) fc id [] tyT let nty = normalise ctxt [] cty - return $ any (isJust . findOverlapping i (class_determiners ci) (delab i nty)) (map fst $ class_instances ci) + return $ any (isJust . findOverlapping i (interface_determiners ci) (delab i nty)) (map fst $ interface_instances ci) findOverlapping i dets t n | SN (ParentN _ _) <- n = Nothing @@ -375,7 +375,7 @@ elabInstance info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t = iWarn fc . text $ "method " ++ show meth ++ " not defined" | otherwise = return () - checkInClass ns meth + checkInInterface ns meth | any (eqRoot meth) ns = return () | otherwise = tclift $ tfail (At fc (Msg $ show meth ++ " not a method of class " ++ show n)) diff --git a/src/Idris/Elab/Class.hs b/src/Idris/Elab/Interface.hs similarity index 95% rename from src/Idris/Elab/Class.hs rename to src/Idris/Elab/Interface.hs index 3cd4b862e..0c7d362f1 100644 --- a/src/Idris/Elab/Class.hs +++ b/src/Idris/Elab/Interface.hs @@ -7,7 +7,7 @@ Maintainer : The Idris Community. -} {-# LANGUAGE PatternGuards #-} {-# OPTIONS_GHC -fwarn-missing-signatures #-} -module Idris.Elab.Class(elabClass) where +module Idris.Elab.Interface(elabInterface) where import Idris.AbsSyntax import Idris.ASTUtils @@ -61,7 +61,7 @@ import Util.Pretty(pretty, text) data MArgTy = IA Name | EA Name | CA deriving Show -elabClass :: ElabInfo +elabInterface :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) -> FC @@ -75,7 +75,7 @@ elabClass :: ElabInfo -> Maybe (Name, FC) -- ^ instance ctor name and location -> Docstring (Either Err PTerm) -- ^ instance ctor docs -> Idris () -elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd +elabInterface info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd = do let cn = fromMaybe (SN (InstanceCtorN tn)) (fst <$> mcn) let tty = pibind (map (\(n, _, ty) -> (n, ty)) ps) (PType fc) let constraint = PApp fc (PRef fc [] tn) @@ -89,7 +89,7 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd -- build data declaration let mdecls = filter tydecl ds -- method declarations let idecls = filter instdecl ds -- default superclass instance declarations - mapM_ checkDefaultSuperclassInstance idecls + mapM_ checkDefaultSuperInterfaceInstance idecls let mnames = map getMName mdecls ist <- getIState let constraintNames = nub $ @@ -119,7 +119,7 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd elabData info (syn { no_imp = no_imp syn ++ mnames, imp_methods = mnames }) doc pDocs fc [] ddecl dets <- findDets cn (map fst fds) - addClass tn (CI cn (map nodoc imethods) defaults idecls (map (\(n, _, _) -> n) ps) [] dets) + addInterface tn (CI cn (map nodoc imethods) defaults idecls (map (\(n, _, _) -> n) ps) [] dets) -- for each constraint, build a top level function to chase it cfns <- mapM (cfun cn constraint syn (map fst imethods)) constraints @@ -139,7 +139,7 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd -- add the default definitions mapM_ (rec_elabDecl info EAll info) (concatMap (snd.snd) defs) - addIBC (IBCClass tn) + addIBC (IBCInterface tn) sendHighlighting $ [(tnfc, AnnName tn Nothing Nothing Nothing)] ++ @@ -161,8 +161,8 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd chkUniq _ t = t -- TODO: probably should normalise - checkDefaultSuperclassInstance :: PDecl -> Idris () - checkDefaultSuperclassInstance (PInstance _ _ _ fc cs _ _ _ n _ ps _ _ _ _) + checkDefaultSuperInterfaceInstance :: PDecl -> Idris () + checkDefaultSuperInterfaceInstance (PInstance _ _ _ fc cs _ _ _ n _ ps _ _ _ _) = do when (not $ null cs) . tclift $ tfail (At fc (Msg "Default superclass instances can't have constraints.")) i <- getIState @@ -249,7 +249,7 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd let conn = case con of PRef _ _ n -> n PApp _ (PRef _ _ n) _ -> n - let conn' = case lookupCtxtName conn (idris_classes i) of + let conn' = case lookupCtxtName conn (idris_interfaces i) of [(n, _)] -> n _ -> conn addInstance False True conn' cfn @@ -341,7 +341,7 @@ memberDocs (PTy d _ _ _ _ n _ _) = Just (basename n, d) memberDocs (PPostulate _ d _ _ _ _ n _) = Just (basename n, d) memberDocs (PData d _ _ _ _ pdata) = Just (basename $ d_name pdata, d) memberDocs (PRecord d _ _ _ n _ _ _ _ _ _ _ ) = Just (basename n, d) -memberDocs (PClass d _ _ _ n _ _ _ _ _ _ _) = Just (basename n, d) +memberDocs (PInterface d _ _ _ n _ _ _ _ _ _ _) = Just (basename n, d) memberDocs _ = Nothing diff --git a/src/Idris/Elab/Term.hs b/src/Idris/Elab/Term.hs index 98806a8c9..2a8e1e368 100644 --- a/src/Idris/Elab/Term.hs +++ b/src/Idris/Elab/Term.hs @@ -868,7 +868,7 @@ elab ist info emode opts fn tm let isinf = f == inferCon || tcname f -- if f is a type class, we need to know its arguments so that -- we can unify with them - case lookupCtxt f (idris_classes ist) of + case lookupCtxt f (idris_interfaces ist) of [] -> return () _ -> do mapM_ setInjective (map getTm args) -- maybe more things are solvable now @@ -961,10 +961,10 @@ elab ist info emode opts fn tm Just b -> case unApply (normalise (tt_ctxt ist) env (binderTy b)) of (P _ c _, args) -> - case lookupCtxtExact c (idris_classes ist) of + case lookupCtxtExact c (idris_interfaces ist) of Nothing -> return () Just ci -> -- type class, set as injective - do mapM_ setinjArg (getDets 0 (class_determiners ci) args) + do mapM_ setinjArg (getDets 0 (interface_determiners ci) args) -- maybe we can solve more things now... ulog <- getUnifyLog probs <- get_probs @@ -1137,7 +1137,7 @@ elab ist info emode opts fn tm _ -> return (n, False) tcName tm | (P _ n _, _) <- unApply tm - = case lookupCtxt n (idris_classes ist) of + = case lookupCtxt n (idris_interfaces ist) of [_] -> True _ -> False tcName _ = False @@ -1745,18 +1745,18 @@ pruneByType _ t _ _ as = as -- to it later - just returns 'var' for now. EB) isPlausible :: IState -> Bool -> Env -> Name -> Type -> Bool isPlausible ist var env n ty - = let (hvar, classes) = collectConstraints [] [] ty in + = let (hvar, interfaces) = collectConstraints [] [] ty in case hvar of Nothing -> True - Just rth -> var -- trace (show (rth, classes)) var + Just rth -> var -- trace (show (rth, interfaces)) var where collectConstraints :: [Name] -> [(Term, [Name])] -> Type -> (Maybe Name, [(Term, [Name])]) collectConstraints env tcs (Bind n (Pi _ ty _) sc) = let tcs' = case unApply ty of (P _ c _, _) -> - case lookupCtxtExact c (idris_classes ist) of - Just tc -> ((ty, map fst (class_instances tc)) + case lookupCtxtExact c (idris_interfaces ist) of + Just tc -> ((ty, map fst (interface_instances tc)) : tcs) Nothing -> tcs _ -> tcs @@ -2321,15 +2321,15 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm returnUnit | n == tacN "Prim__AddInstance" = do ~[cls, inst] <- tacTmArgs 2 tac args - className <- reifyTTName cls + interfaceName <- reifyTTName cls instName <- reifyTTName inst - updateAux $ \e -> e { new_tyDecls = RAddInstance className instName : + updateAux $ \e -> e { new_tyDecls = RAddInstance interfaceName instName : new_tyDecls e } returnUnit | n == tacN "Prim__IsTCName" = do ~[n] <- tacTmArgs 1 tac args n' <- reifyTTName n - case lookupCtxtExact n' (idris_classes ist) of + case lookupCtxtExact n' (idris_interfaces ist) of Just _ -> fmap fst . checkClosed $ Var (sNS (sUN "True") ["Bool", "Prelude"]) Nothing -> fmap fst . checkClosed $ Var (sNS (sUN "False") ["Bool", "Prelude"]) | n == tacN "Prim__ResolveTC" @@ -2819,12 +2819,12 @@ processTacticDecls info steps = _ -> return () -- TODO: inaccessible - RAddInstance className instName -> + RAddInstance interfaceName instName -> do -- The type class resolution machinery relies on a special logElab 2 $ "Adding elab script instance " ++ show instName ++ - " for " ++ show className - addInstance False True className instName - addIBC (IBCInstance False True className instName) + " for " ++ show interfaceName + addInstance False True interfaceName instName + addIBC (IBCInstance False True interfaceName instName) RClausesInstrs n cs -> do logElab 3 $ "Pattern-matching definition from tactics: " ++ show n solveDeferred emptyFC n diff --git a/src/Idris/Elab/Utils.hs b/src/Idris/Elab/Utils.hs index c0e58a92d..6095a7f8f 100644 --- a/src/Idris/Elab/Utils.hs +++ b/src/Idris/Elab/Utils.hs @@ -191,7 +191,7 @@ pbinds i (Bind n (PVar t) sc) = do attack; patbind n env <- get_env case unApply (normalise (tt_ctxt i) env t) of - (P _ c _, args) -> case lookupCtxt c (idris_classes i) of + (P _ c _, args) -> case lookupCtxt c (idris_interfaces i) of [] -> return () _ -> -- type class, set as injective mapM_ setinjArg args @@ -270,7 +270,7 @@ getTCinj i ap@(App _ f a) isTCName n = mapMaybe getInjName args | otherwise = [] where - isTCName n = case lookupCtxtExact n (idris_classes i) of + isTCName n = case lookupCtxtExact n (idris_interfaces i) of Just _ -> True _ -> False getInjName t | (P _ x _, _) <- unApply t = Just x diff --git a/src/Idris/ElabDecls.hs b/src/Idris/ElabDecls.hs index 03922a567..7ee7b082a 100644 --- a/src/Idris/ElabDecls.hs +++ b/src/Idris/ElabDecls.hs @@ -34,7 +34,7 @@ import Idris.Elab.Type import Idris.Elab.Clause import Idris.Elab.Data import Idris.Elab.Record -import Idris.Elab.Class +import Idris.Elab.Interface import Idris.Elab.Instance import Idris.Elab.Provider import Idris.Elab.RunElab @@ -271,10 +271,10 @@ elabDecl' what info (PNamespace n nfc ps) = newNS = n : namespace info ninfo = info { namespace = newNS } -elabDecl' what info (PClass doc s f cs n nfc ps pdocs fds ds cn cd) +elabDecl' what info (PInterface doc s f cs n nfc ps pdocs fds ds cn cd) | what /= EDefns = do logElab 1 $ "Elaborating class " ++ show n - elabClass info (s { syn_params = [] }) doc f cs n nfc ps pdocs fds ds cn cd + elabInterface info (s { syn_params = [] }) doc f cs n nfc ps pdocs fds ds cn cd elabDecl' what info (PInstance doc argDocs s f cs pnames acc fnopts n nfc ps pextra t expn ds) = do logElab 1 $ "Elaborating instance " ++ show n elabInstance info s doc argDocs what f cs pnames acc fnopts n nfc ps pextra t expn ds diff --git a/src/Idris/Erasure.hs b/src/Idris/Erasure.hs index 2410f6195..420769e8f 100644 --- a/src/Idris/Erasure.hs +++ b/src/Idris/Erasure.hs @@ -79,7 +79,7 @@ performUsageAnalysis startNames = do case startNames of [] -> return [] -- no main -> not compiling -> reachability irrelevant main -> do - ci <- idris_classes <$> getIState + ci <- idris_interfaces <$> getIState cg <- idris_callgraph <$> getIState opt <- idris_optimisation <$> getIState used <- idris_erasureUsed <$> getIState @@ -170,7 +170,7 @@ forwardChain deps -- | Build the dependency graph, starting the depth-first search from -- a list of Names. -buildDepMap :: Ctxt ClassInfo -> [(Name, Int)] -> [(Name, Int)] -> +buildDepMap :: Ctxt InterfaceInfo -> [(Name, Int)] -> [(Name, Int)] -> Context -> [Name] -> Deps buildDepMap ci used externs ctx startNames = addPostulates used $ dfs S.empty M.empty startNames @@ -252,7 +252,7 @@ buildDepMap ci used externs ctx startNames -- get Deps for a Name getDeps :: Name -> Deps - getDeps (SN (WhereN i (SN (InstanceCtorN classN)) (MN i' field))) + getDeps (SN (WhereN i (SN (InstanceCtorN interfaceN)) (MN i' field))) = M.empty -- these deps are created when applying instance ctors getDeps n = case lookupDefExact n ctx of Just def -> getDepsDef n def @@ -338,7 +338,7 @@ buildDepMap ci used externs ctx startNames -- generate metamethod names, "n" is the instance ctor meth :: Int -> Maybe Name - meth | SN (InstanceCtorN className) <- n = \j -> Just (mkFieldName n j) + meth | SN (InstanceCtorN interfaceName) <- n = \j -> Just (mkFieldName n j) | otherwise = \j -> Nothing -- Named variables -> DeBruijn variables -> Conds/guards -> Term -> Deps @@ -381,7 +381,7 @@ buildDepMap ci used externs ctx startNames getDepsTerm vs bs cd app@(App _ _ _) | (fun, args) <- unApply app = case fun of -- instance constructors -> create metamethod deps - P (DCon _ _ _) ctorName@(SN (InstanceCtorN className)) _ + P (DCon _ _ _) ctorName@(SN (InstanceCtorN interfaceName)) _ -> conditionalDeps ctorName args -- regular data ctor stuff `union` unionMap (methodDeps ctorName) (zip [0..] args) -- method-specific stuff diff --git a/src/Idris/IBC.hs b/src/Idris/IBC.hs index 9a743b180..5d35d4b1d 100644 --- a/src/Idris/IBC.hs +++ b/src/Idris/IBC.hs @@ -67,7 +67,7 @@ data IBCFile = IBCFile { , ibc_implicits :: ![(Name, [PArg])] , ibc_fixes :: ![FixDecl] , ibc_statics :: ![(Name, [Bool])] - , ibc_classes :: ![(Name, ClassInfo)] + , ibc_classes :: ![(Name, InterfaceInfo)] , ibc_records :: ![(Name, RecordInfo)] , ibc_instances :: ![(Bool, Bool, Name, Name)] , ibc_dsls :: ![(Name, DSL)] @@ -268,8 +268,8 @@ ibc i (IBCStatic n) f = case lookupCtxtExact n (idris_statics i) of Just v -> return f { ibc_statics = (n,v): ibc_statics f } _ -> ifail "IBC write failed" -ibc i (IBCClass n) f - = case lookupCtxtExact n (idris_classes i) of +ibc i (IBCInterface n) f + = case lookupCtxtExact n (idris_interfaces i) of Just v -> return f { ibc_classes = (n,v): ibc_classes f } _ -> ifail "IBC write failed" ibc i (IBCRecord n) f @@ -390,7 +390,7 @@ process reexp phase archive fn = do processImplicits archive processInfix archive processStatics archive - processClasses archive + processInterfaces archive processRecords archive processInstances archive processDSLs archive @@ -545,18 +545,18 @@ processStatics ar = do mapM_ (\ (n, s) -> updateIState (\i -> i { idris_statics = addDef n s (idris_statics i) })) ss -processClasses :: Archive -> Idris () -processClasses ar = do +processInterfaces :: Archive -> Idris () +processInterfaces ar = do cs <- getEntry [] "ibc_classes" ar mapM_ (\ (n, c) -> do i <- getIState -- Don't lose instances from previous IBCs, which -- could have loaded in any order - let is = case lookupCtxtExact n (idris_classes i) of + let is = case lookupCtxtExact n (idris_interfaces i) of Just (CI _ _ _ _ _ ins _) -> ins _ -> [] - let c' = c { class_instances = class_instances c ++ is } - putIState (i { idris_classes = addDef n c' (idris_classes i) })) cs + let c' = c { interface_instances = interface_instances c ++ is } + putIState (i { idris_interfaces = addDef n c' (idris_interfaces i) })) cs processRecords :: Archive -> Idris () processRecords ar = do @@ -1408,7 +1408,7 @@ instance (Binary t) => Binary (PDecl' t) where put x10 put x11 put x12 - PClass x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 + PInterface x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 -> do putWord8 7 put x1 put x2 @@ -1545,7 +1545,7 @@ instance (Binary t) => Binary (PDecl' t) where x10 <- get x11 <- get x12 <- get - return (PClass x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) + return (PInterface x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) 8 -> do x1 <- get x2 <- get x3 <- get @@ -2355,7 +2355,7 @@ instance (Binary t) => Binary (PArg' t) where _ -> error "Corrupted binary data for PArg'" -instance Binary ClassInfo where +instance Binary InterfaceInfo where put (CI x1 x2 x3 x4 x5 _ x6) = do put x1 put x2 diff --git a/src/Idris/IdrisDoc.hs b/src/Idris/IdrisDoc.hs index 05768b199..f8c74638c 100644 --- a/src/Idris/IdrisDoc.hs +++ b/src/Idris/IdrisDoc.hs @@ -173,9 +173,9 @@ removeOrphans list = let children = S.fromList $ concatMap (names . (\(_, d, _) -> d)) list in filter ((flip S.notMember children) . (\(n, _, _) -> n)) list - where names (Just (DataDoc _ fds)) = map (\(FD n _ _ _ _) -> n) fds - names (Just (ClassDoc _ _ fds _ _ _ _ c)) = map (\(FD n _ _ _ _) -> n) fds ++ map (\(FD n _ _ _ _) -> n) (maybeToList c) - names _ = [] + where names (Just (DataDoc _ fds)) = map (\(FD n _ _ _ _) -> n) fds + names (Just (InterfaceDoc _ _ fds _ _ _ _ c)) = map (\(FD n _ _ _ _) -> n) fds ++ map (\(FD n _ _ _ _) -> n) (maybeToList c) + names _ = [] -- | Whether a Name names something which should be documented filterName :: Name -- ^ Name to check @@ -222,14 +222,14 @@ referredNss (n, Just d, _) = names = concatMap (extractPTermNames) ts in S.map getNs $ S.fromList names - where getFunDocs (FunDoc f) = [f] - getFunDocs (DataDoc f fs) = f:fs - getFunDocs (ClassDoc _ _ fs _ _ _ _ _) = fs - getFunDocs (RecordDoc _ _ f fs _) = f:fs - getFunDocs (NamedInstanceDoc _ fd) = [fd] - getFunDocs (ModDoc _ _) = [] - types (FD _ _ args t _) = t:(map second args) - second (_, x, _, _) = x + where getFunDocs (FunDoc f) = [f] + getFunDocs (DataDoc f fs) = f:fs + getFunDocs (InterfaceDoc _ _ fs _ _ _ _ _) = fs + getFunDocs (RecordDoc _ _ f fs _) = f:fs + getFunDocs (NamedInstanceDoc _ fd) = [fd] + getFunDocs (ModDoc _ _) = [] + types (FD _ _ args t _) = t:(map second args) + second (_, x, _, _) = x -- | Returns an NsDict of containing all known namespaces and their contents @@ -583,7 +583,7 @@ createOtherDoc :: IState -- ^ Needed to determine the types of names -> H.Html -- ^ Resulting HTML createOtherDoc ist (FunDoc fd) = createFunDoc ist fd -createOtherDoc ist (ClassDoc n docstring fds _ _ _ _ c) = do +createOtherDoc ist (InterfaceDoc n docstring fds _ _ _ _ c) = do H.dt ! (A.id $ toValue $ show n) $ do H.span ! class_ "word" $ do "interface"; nbsp H.span ! class_ "name type" diff --git a/src/Idris/Interactive.hs b/src/Idris/Interactive.hs index 386d4881d..6b1e3752c 100644 --- a/src/Idris/Interactive.hs +++ b/src/Idris/Interactive.hs @@ -349,10 +349,10 @@ makeLemma fn updatefile l n if (not isProv) then do let skip = guessImps i (tt_ctxt i) mty let impty = stripMNBind skip margs (delab i mty) - let classes = guessClasses i (tt_ctxt i) [] (allNamesIn impty) mty + let interfaces = guessInterfaces i (tt_ctxt i) [] (allNamesIn impty) mty let lem = show n ++ " : " ++ - constraints i classes mty ++ + constraints i interfaces mty ++ showTmOpts (defaultPPOption { ppopt_pinames = True }) impty let lem_app = guessBrackets False tyline (show n) (show n ++ appArgs skip margs mty) @@ -434,7 +434,7 @@ makeLemma fn updatefile l n guessImps ist ctxt (Bind n (Pi _ ty _) sc) | guarded ctxt n (substV (P Bound n Erased) sc) = n : guessImps ist ctxt sc - | isClass ist ty + | isInterface ist ty = n : guessImps ist ctxt sc | paramty ty = n : guessImps ist ctxt sc | ignoreName n = n : guessImps ist ctxt sc @@ -450,13 +450,13 @@ makeLemma fn updatefile l n "_aX" -> True _ -> False - guessClasses :: IState -> Context -> [Name] -> [Name] -> Term -> [Name] - guessClasses ist ctxt binders usednames (Bind n (Pi _ ty _) sc) - | isParamClass ist ty && any (\x -> elem x usednames) - (paramNames binders ty) - = n : guessClasses ist ctxt (n : binders) usednames sc - | otherwise = guessClasses ist ctxt (n : binders) usednames sc - guessClasses ist ctxt _ _ _ = [] + guessInterfaces :: IState -> Context -> [Name] -> [Name] -> Term -> [Name] + guessInterfaces ist ctxt binders usednames (Bind n (Pi _ ty _) sc) + | isParamInterface ist ty && any (\x -> elem x usednames) + (paramNames binders ty) + = n : guessInterfaces ist ctxt (n : binders) usednames sc + | otherwise = guessInterfaces ist ctxt (n : binders) usednames sc + guessInterfaces ist ctxt _ _ _ = [] paramNames bs ty | (P _ _ _, args) <- unApply ty = vnames args @@ -464,16 +464,16 @@ makeLemma fn updatefile l n vnames (V i : xs) | i < length bs = bs !! i : vnames xs vnames (_ : xs) = vnames xs - isClass ist t + isInterface ist t | (P _ n _, args) <- unApply t - = case lookupCtxtExact n (idris_classes ist) of + = case lookupCtxtExact n (idris_interfaces ist) of Just _ -> True _ -> False | otherwise = False - isParamClass ist t + isParamInterface ist t | (P _ n _, args) <- unApply t - = case lookupCtxtExact n (idris_classes ist) of + = case lookupCtxtExact n (idris_interfaces ist) of Just _ -> any isV args _ -> False | otherwise = False diff --git a/src/Idris/Parser.hs b/src/Idris/Parser.hs index 102716f2f..ca3a0711c 100644 --- a/src/Idris/Parser.hs +++ b/src/Idris/Parser.hs @@ -226,7 +226,7 @@ internalDecl syn <|> params syn <|> mutual syn <|> namespace syn - <|> class_ syn + <|> interface_ syn <|> do d <- dsl syn; return [d] <|> directive syn <|> provider syn @@ -340,8 +340,8 @@ declExtension syn ns rules = (updateRecCon ns cname) cdoc s - updateNs ns (PClass docs s fc cs cn fc' ps pdocs pdets ds cname cdocs) - = PClass docs s fc cs (updateB ns cn) fc' ps pdocs pdets + updateNs ns (PInterface docs s fc cs cn fc' ps pdocs pdets ds cname cdocs) + = PInterface docs s fc cs (updateB ns cn) fc' ps pdocs pdets (map (updateNs ns) ds) (updateRecCon ns cname) cdocs @@ -859,23 +859,23 @@ ClassBlock ::= ; @ -} -classBlock :: SyntaxInfo -> IdrisParser (Maybe (Name, FC), Docstring (Either Err PTerm), [PDecl]) -classBlock syn = do reservedHL "where" - openBlock - (cn, cd) <- option (Nothing, emptyDocstring) $ - try (do (doc, _) <- option noDocs docComment - n <- constructor - return (Just n, doc)) - ist <- get - let cd' = annotate syn ist cd +interfaceBlock :: SyntaxInfo -> IdrisParser (Maybe (Name, FC), Docstring (Either Err PTerm), [PDecl]) +interfaceBlock syn = do reservedHL "where" + openBlock + (cn, cd) <- option (Nothing, emptyDocstring) $ + try (do (doc, _) <- option noDocs docComment + n <- constructor + return (Just n, doc)) + ist <- get + let cd' = annotate syn ist cd - ds <- many (notEndBlock >> try (instance_ True syn) - <|> do x <- data_ syn - return [x] - <|> fnDecl syn) - closeBlock - return (cn, cd', concat ds) - "class block" + ds <- many (notEndBlock >> try (instance_ True syn) + <|> do x <- data_ syn + return [x] + <|> fnDecl syn) + closeBlock + return (cn, cd', concat ds) + "class block" where constructor :: IdrisParser (Name, FC) @@ -899,29 +899,29 @@ Class ::= ; @ -} -class_ :: SyntaxInfo -> IdrisParser [PDecl] -class_ syn = do (doc, argDocs, acc) - <- try (do (doc, argDocs) <- docstring syn - acc <- accessibility - classKeyword - return (doc, argDocs, acc)) - fc <- getFC - cons <- constraintList syn - let cons' = [(c, ty) | (c, _, ty) <- cons] - (n_in, nfc) <- fnName - let n = expandNS syn n_in - cs <- many carg - fds <- option [(cn, NoFC) | (cn, _, _) <- cs] fundeps - (cn, cd, ds) <- option (Nothing, fst noDocs, []) (classBlock syn) - accData acc n (concatMap declared ds) - return [PClass doc syn fc cons' n nfc cs argDocs fds ds cn cd] - "type-class declaration" +interface_ :: SyntaxInfo -> IdrisParser [PDecl] +interface_ syn = do (doc, argDocs, acc) + <- try (do (doc, argDocs) <- docstring syn + acc <- accessibility + interfaceKeyword + return (doc, argDocs, acc)) + fc <- getFC + cons <- constraintList syn + let cons' = [(c, ty) | (c, _, ty) <- cons] + (n_in, nfc) <- fnName + let n = expandNS syn n_in + cs <- many carg + fds <- option [(cn, NoFC) | (cn, _, _) <- cs] fundeps + (cn, cd, ds) <- option (Nothing, fst noDocs, []) (interfaceBlock syn) + accData acc n (concatMap declared ds) + return [PInterface doc syn fc cons' n nfc cs argDocs fds ds cn cd] + "type-class declaration" where fundeps :: IdrisParser [(Name, FC)] fundeps = do lchar '|'; sepBy name (lchar ',') - classKeyword :: IdrisParser () - classKeyword = reservedHL "interface" + interfaceKeyword :: IdrisParser () + interfaceKeyword = reservedHL "interface" <|> do reservedHL "class" fc <- getFC parserWarning fc Nothing (Msg "The 'class' keyword is deprecated. Use 'interface' instead.") @@ -1864,7 +1864,7 @@ loadSource lidr f toline toMutual x = let r = PMutual (fileFC "single mutual") [x] in case x of PClauses{} -> r - PClass{} -> r + PInterface{} -> r PData{} -> r PInstance{} -> r _ -> x diff --git a/src/Idris/Parser/Helpers.hs b/src/Idris/Parser/Helpers.hs index 13a7d17cb..6d423b2ca 100644 --- a/src/Idris/Parser/Helpers.hs +++ b/src/Idris/Parser/Helpers.hs @@ -713,8 +713,8 @@ collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds collect (POpenInterfaces f ns ps : ds) = POpenInterfaces f ns (collect ps) : collect ds collect (PMutual f ms : ds) = PMutual f (collect ms) : collect ds collect (PNamespace ns fc ps : ds) = PNamespace ns fc (collect ps) : collect ds -collect (PClass doc f s cs n nfc ps pdocs fds ds cn cd : ds') - = PClass doc f s cs n nfc ps pdocs fds (collect ds) cn cd : collect ds' +collect (PInterface doc f s cs n nfc ps pdocs fds ds cn cd : ds') + = PInterface doc f s cs n nfc ps pdocs fds (collect ds) cn cd : collect ds' collect (PInstance doc argDocs f s cs pnames acc opts n nfc ps pextra t en ds : ds') = PInstance doc argDocs f s cs pnames acc opts n nfc ps pextra t en (collect ds) : collect ds' collect (d : ds) = d : collect ds diff --git a/src/Idris/PartialEval.hs b/src/Idris/PartialEval.hs index a5c9f455a..99967dbfe 100644 --- a/src/Idris/PartialEval.hs +++ b/src/Idris/PartialEval.hs @@ -141,8 +141,8 @@ mkPE_TyDecl ist args ty = mkty args ty mkty ((ExplicitD, v) : xs) (Bind n (Pi _ t k) sc) = PPi expl n NoFC (delab ist (generaliseIn t)) (mkty xs sc) mkty ((ImplicitD, v) : xs) (Bind n (Pi _ t k) sc) - | concreteClass ist t = mkty xs sc - | classConstraint ist t + | concreteInterface ist t = mkty xs sc + | interfaceConstraint ist t = PPi constraint n NoFC (delab ist (generaliseIn t)) (mkty xs sc) | otherwise = PPi impl n NoFC (delab ist (generaliseIn t)) (mkty xs sc) @@ -161,18 +161,18 @@ mkPE_TyDecl ist args ty = mkty args ty gen tm = return tm -- | Checks if a given argument is a type class constraint argument -classConstraint :: Idris.AbsSyntax.IState -> TT Name -> Bool -classConstraint ist v - | (P _ c _, args) <- unApply v = case lookupCtxt c (idris_classes ist) of +interfaceConstraint :: Idris.AbsSyntax.IState -> TT Name -> Bool +interfaceConstraint ist v + | (P _ c _, args) <- unApply v = case lookupCtxt c (idris_interfaces ist) of [_] -> True _ -> False | otherwise = False -- | Checks if the given arguments of a type class constraint are all either constants -- or references (i.e. that it doesn't contain any complex terms). -concreteClass :: IState -> TT Name -> Bool -concreteClass ist v - | not (classConstraint ist v) = False +concreteInterface :: IState -> TT Name -> Bool +concreteInterface ist v + | not (interfaceConstraint ist v) = False | (P _ c _, args) <- unApply v = all concrete args | otherwise = False where concrete (Constant _) = True diff --git a/src/Idris/ProofSearch.hs b/src/Idris/ProofSearch.hs index 9632c3e74..236130112 100644 --- a/src/Idris/ProofSearch.hs +++ b/src/Idris/ProofSearch.hs @@ -101,7 +101,7 @@ trivialTCs ok elab ist tcArg env ty | (P _ n _, args) <- unApply (getRetTy (normalise (tt_ctxt ist) env ty)) - = case lookupCtxtExact n (idris_classes ist) of + = case lookupCtxtExact n (idris_interfaces ist) of Just _ -> True _ -> False | otherwise = False @@ -412,13 +412,13 @@ resTC' tcs defaultOn openOK topholes depth topg fn elab ist -- returns Just hs if okay, where hs are holes which are okay in the -- goal, or Nothing if not okay to proceed - tcArgsOK ty hs | (P _ nc _, as) <- unApply (getRetTy ty), nc == numclass && defaultOn + tcArgsOK ty hs | (P _ nc _, as) <- unApply (getRetTy ty), nc == numinterface && defaultOn = Just [] tcArgsOK ty hs -- if any determining arguments are metavariables, postpone = let (f, as) = unApply (getRetTy ty) in case f of - P _ cn _ -> case lookupCtxtExact cn (idris_classes ist) of - Just ci -> tcDetArgsOK 0 (class_determiners ci) hs as + P _ cn _ -> case lookupCtxtExact cn (idris_interfaces ist) of + Just ci -> tcDetArgsOK 0 (interface_determiners ci) hs as Nothing -> if any (isMeta hs) as then Nothing else Just [] @@ -451,9 +451,9 @@ resTC' tcs defaultOn openOK topholes depth topg fn elab ist | Constant _ <- c = not (n `elem` hs) notHole _ _ = True - numclass = sNS (sUN "Num") ["Interfaces","Prelude"] + numinterface = sNS (sUN "Num") ["Interfaces","Prelude"] - addDefault t num@(P _ nc _) [P Bound a _] | nc == numclass && defaultOn + addDefault t num@(P _ nc _) [P Bound a _] | nc == numinterface && defaultOn = do focus a fill (RConstant (AType (ATInt ITBig))) -- default Integer solve @@ -525,7 +525,7 @@ resTC' tcs defaultOn openOK topholes depth topg fn elab ist findInstances :: IState -> Term -> [Name] findInstances ist t | (P _ n _, _) <- unApply (getRetTy t) - = case lookupCtxt n (idris_classes ist) of + = case lookupCtxt n (idris_interfaces ist) of [CI _ _ _ _ _ ins _] -> [n | (n, True) <- ins, accessible n] _ -> [] diff --git a/src/Idris/REPL.hs b/src/Idris/REPL.hs index 354feaefa..3c91058f1 100644 --- a/src/Idris/REPL.hs +++ b/src/Idris/REPL.hs @@ -868,7 +868,7 @@ process fn (NewDefn decls) = do getName (PTy docs argdocs syn fc opts name _ ty) = Just name getName (PClauses fc opts name (clause:clauses)) = Just (getClauseName clause) getName (PData doc argdocs syn fc opts dataDecl) = Just (d_name dataDecl) - getName (PClass doc syn fc constraints name nfc parms parmdocs fds decls _ _) = Just name + getName (PInterface doc syn fc constraints name nfc parms parmdocs fds decls _ _) = Just name getName _ = Nothing -- getClauseName is partial and I am not sure it's used safely! -- trillioneyes getClauseName (PClause fc name whole with rhs whereBlock) = name @@ -943,7 +943,7 @@ process fn (Undefine names) = undefine names undefOne n = do fputState (ctxt_lookup n . known_terms) Nothing -- for now just assume it's a class. Eventually we'll want some kind of -- smart detection of exactly what kind of name we're undefining. - fputState (ctxt_lookup n . known_classes) Nothing + fputState (ctxt_lookup n . known_interfaces) Nothing fmodifyState repl_definitions (delete n) undefClosure n = do replDefs <- idris_repl_defs `fmap` get diff --git a/src/Idris/TypeSearch.hs b/src/Idris/TypeSearch.hs index 09867fcdc..0451d8ce7 100644 --- a/src/Idris/TypeSearch.hs +++ b/src/Idris/TypeSearch.hs @@ -30,8 +30,8 @@ import qualified Data.Text as T (pack, isPrefixOf) import Data.Traversable (traverse) import Idris.AbsSyntax (addUsingConstraints, addImpl, getIState, putIState, implicit, logLvl) -import Idris.AbsSyntaxTree (class_instances, ClassInfo, defaultSyntax, eqTy, Idris - , IState (idris_classes, idris_docstrings, tt_ctxt, idris_outputmode), +import Idris.AbsSyntaxTree (interface_instances, InterfaceInfo, defaultSyntax, eqTy, Idris + , IState (idris_interfaces, idris_docstrings, tt_ctxt, idris_outputmode), implicitAllowed, OutputMode(..), PTerm, toplevel) import Idris.Core.Evaluate (Context (definitions), Def (Function, TyDecl, CaseOp), normaliseC) import Idris.Core.TT hiding (score) @@ -173,8 +173,8 @@ deleteFromArgList n = filter ((/= n) . fst) -- | Asymmetric modifications to keep track of data AsymMods = Mods { argApp :: !Int - , typeClassApp :: !Int - , typeClassIntro :: !Int + , interfaceApp :: !Int + , interfaceIntro :: !Int } deriving (Eq, Show) @@ -253,18 +253,18 @@ instance Monoid Score where type ArgsDAG = [((Name, Type), (Int, Set Name))] -- | A list of typeclass constraints -type Classes = [(Name, Type)] +type Interfaces = [(Name, Type)] -- | The state corresponding to an attempted match of two types. data State = State { holes :: ![(Name, Type)] -- ^ names which have yet to be resolved - , argsAndClasses :: !(Sided (ArgsDAG, Classes)) + , argsAndInterfaces :: !(Sided (ArgsDAG, Interfaces)) -- ^ arguments and typeclass constraints for each type which have yet to be resolved , score :: !Score -- ^ the score so far , usedNames :: ![Name] -- ^ all names that have been used } deriving Show -modifyTypes :: (Type -> Type) -> (ArgsDAG, Classes) -> (ArgsDAG, Classes) +modifyTypes :: (Type -> Type) -> (ArgsDAG, Interfaces) -> (ArgsDAG, Interfaces) modifyTypes f = modifyDag *** modifyList where modifyDag = map (first (second f)) @@ -273,11 +273,11 @@ modifyTypes f = modifyDag *** modifyList findNameInArgsDAG :: Name -> ArgsDAG -> Maybe (Type, Maybe Int) findNameInArgsDAG name = fmap ((snd . fst) &&& (Just . fst . snd)) . find ((name ==) . fst . fst) -findName :: Name -> (ArgsDAG, Classes) -> Maybe (Type, Maybe Int) -findName n (args, classes) = findNameInArgsDAG n args <|> ((,) <$> lookup n classes <*> Nothing) +findName :: Name -> (ArgsDAG, Interfaces) -> Maybe (Type, Maybe Int) +findName n (args, interfaces) = findNameInArgsDAG n args <|> ((,) <$> lookup n interfaces <*> Nothing) -deleteName :: Name -> (ArgsDAG, Classes) -> (ArgsDAG, Classes) -deleteName n (args, classes) = (deleteFromDag n args, filter ((/= n) . fst) classes) +deleteName :: Name -> (ArgsDAG, Interfaces) -> (ArgsDAG, Interfaces) +deleteName n (args, interfaces) = (deleteFromDag n args, filter ((/= n) . fst) interfaces) tcToMaybe :: TC a -> Maybe a tcToMaybe (OK x) = Just x @@ -287,8 +287,8 @@ inArgTys :: (Type -> Type) -> ArgsDAG -> ArgsDAG inArgTys = map . first . second -typeclassUnify :: Ctxt ClassInfo -> Context -> Type -> Type -> Maybe [(Name, Type)] -typeclassUnify classInfo ctxt ty tyTry = do +interfaceUnify :: Ctxt InterfaceInfo -> Context -> Type -> Type -> Maybe [(Name, Type)] +interfaceUnify interfaceInfo ctxt ty tyTry = do res <- tcToMaybe $ match_unify ctxt [] (ty, Nothing) (retTy, Nothing) [] theHoles [] guard $ null (theHoles \\ map fst res) let argTys' = map (second $ foldr (.) id [ subst n t | (n, t) <- res ]) tcArgs @@ -297,13 +297,13 @@ typeclassUnify classInfo ctxt ty tyTry = do tyTry' = vToP tyTry theHoles = map fst nonTcArgs retTy = getRetTy tyTry' - (tcArgs, nonTcArgs) = partition (isTypeClassArg classInfo . snd) $ getArgTys tyTry' + (tcArgs, nonTcArgs) = partition (isInterfaceArg interfaceInfo . snd) $ getArgTys tyTry' -isTypeClassArg :: Ctxt ClassInfo -> Type -> Bool -isTypeClassArg classInfo ty = not (null (getClassName clss >>= flip lookupCtxt classInfo)) where +isInterfaceArg :: Ctxt InterfaceInfo -> Type -> Bool +isInterfaceArg interfaceInfo ty = not (null (getInterfaceName clss >>= flip lookupCtxt interfaceInfo)) where (clss, args) = unApply ty - getClassName (P (TCon _ _) className _) = [className] - getClassName _ = [] + getInterfaceName (P (TCon _ _) interfaceName _) = [interfaceName] + getInterfaceName _ = [] -- | Compute the power set @@ -345,12 +345,12 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh <$> flipEqualities ty <*> flipEqualitiesDag xs startStates (numEqFlips, sndDag, sndRetTy) = do state <- unifyQueue (State startingHoles - (Sided (dag1, typeClassArgs1) (sndDag, typeClassArgs2)) + (Sided (dag1, interfaceArgs1) (sndDag, interfaceArgs2)) (mempty { equalityFlips = numEqFlips }) usedns) [(retTy1, sndRetTy)] return (score state, state) - (dag2, typeClassArgs2, retTy2) = makeDag (uniqueBinders (map fst argNames1) type2) + (dag2, interfaceArgs2, retTy2) = makeDag (uniqueBinders (map fst argNames1) type2) argNames2 = map fst dag2 usedns = map fst startingHoles startingHoles = argNames1 ++ argNames2 @@ -376,13 +376,13 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh ctxt = tt_ctxt istate - classInfo = idris_classes istate + interfaceInfo = idris_interfaces istate - (dag1, typeClassArgs1, retTy1) = makeDag type1 + (dag1, interfaceArgs1, retTy1) = makeDag type1 argNames1 = map fst dag1 - makeDag :: Type -> (ArgsDAG, Classes, Type) + makeDag :: Type -> (ArgsDAG, Interfaces, Type) makeDag = first3 (zipWith (\i (ty, deps) -> (ty, (i, deps))) [0..] . reverseDag) . - computeDagP (isTypeClassArg classInfo) . vToP . unLazy + computeDagP (isInterfaceArg interfaceInfo) . vToP . unLazy first3 f (a,b,c) = (f a, b, c) -- update our state with the unification resolutions @@ -396,14 +396,14 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh let transScore = fromMaybe 0 (abs <$> ((-) <$> ix1 <*> ix2)) return (inScore (\s -> s { transposition = transposition s + transScore }) state'', (ty1, ty2) : queue) where - unresolved = argsAndClasses state + unresolved = argsAndInterfaces state inScore f stat = stat { score = f (score stat) } findArgs = ((,) <$> findName name (left unresolved) <*> findName name2 (right unresolved)) <|> ((,) <$> findName name2 (left unresolved) <*> findName name (right unresolved)) matchnames = [name, name2] deleteArgs = deleteName name . deleteName name2 state' = state { holes = filter (not . (`elem` matchnames) . fst) (holes state) - , argsAndClasses = both (modifyTypes (subst name term) . deleteArgs) unresolved} + , argsAndInterfaces = both (modifyTypes (subst name term) . deleteArgs) unresolved} resolveUnis ((name, term) : xs) state@(State hs unresolved _ _) = case both (findName name) unresolved of @@ -427,7 +427,7 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh addScore additions theState = theState { score = let s = score theState in s { asymMods = asymMods s `mappend` additions } } state' = state { holes = filter (not . (`elem` toDelete) . fst) hs - , argsAndClasses = both (modifyTypes (subst name term) . deleteMany) (argsAndClasses state) } + , argsAndInterfaces = both (modifyTypes (subst name term) . deleteMany) (argsAndInterfaces state) } nextStep = resolveUnis xs state' @@ -443,19 +443,19 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh guard $ scoreCriterion (score state') unifyQueue state' (queue ++ queueAdditions) - possClassInstances :: [Name] -> Type -> [Type] - possClassInstances usedns ty = do - className <- getClassName clss - classDef <- lookupCtxt className classInfo - n <- class_instances classDef + possInterfaceInstances :: [Name] -> Type -> [Type] + possInterfaceInstances usedns ty = do + interfaceName <- getInterfaceName clss + interfaceDef <- lookupCtxt interfaceName interfaceInfo + n <- interface_instances interfaceDef def <- lookupCtxt (fst n) (definitions ctxt) nty <- normaliseC ctxt [] <$> (case typeFromDef def of Just x -> [x]; Nothing -> []) let ty' = vToP (uniqueBinders usedns nty) return ty' where (clss, _) = unApply ty - getClassName (P (TCon _ _) className _) = [className] - getClassName _ = [] + getInterfaceName (P (TCon _ _) interfaceName _) = [interfaceName] + getInterfaceName _ = [] -- 'Just' if the computation hasn't totally failed yet, 'Nothing' if it has -- '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 | sds <- allMods ] where allMods = parallel defMod mods - mods :: Sided [( Classes, AsymMods, [Name] )] + mods :: Sided [( Interfaces, AsymMods, [Name] )] mods = both (instanceMods . snd) unresolved - defMod :: Sided (Classes, AsymMods, [Name]) + defMod :: Sided (Interfaces, AsymMods, [Name]) defMod = both (\(_, cs) -> (cs, mempty , [])) unresolved parallel :: Sided a -> Sided [a] -> [Sided a] parallel (Sided l r) (Sided ls rs) = map (flip Sided r) ls ++ map (Sided l) rs - instanceMods :: Classes -> [( Classes , AsymMods, [Name] )] - instanceMods classes = [ ( newClassArgs, mempty { typeClassApp = 1 }, newHoles ) - | (_, ty) <- classes - , inst <- possClassInstances usedns ty - , newClassArgs <- maybeToList $ typeclassUnify classInfo ctxt ty inst - , let newHoles = map fst newClassArgs ] + instanceMods :: Interfaces -> [( Interfaces , AsymMods, [Name] )] + instanceMods interfaces = [ ( newInterfaceArgs, mempty { interfaceApp = 1 }, newHoles ) + | (_, ty) <- interfaces + , inst <- possInterfaceInstances usedns ty + , newInterfaceArgs <- maybeToList $ interfaceUnify interfaceInfo ctxt ty inst + , let newHoles = map fst newInterfaceArgs ] -- Stage 1 - match arguments nextSteps (State hs (Sided (dagL, c1) (dagR, c2)) scoreAcc usedns) = results where - results = concatMap takeSomeClasses results1 + results = concatMap takeSomeInterfaces results1 -- we only try to match arguments whose names don't appear in the types -- of any other arguments @@ -532,18 +532,18 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh -- Stage 2 - simply introduce a subset of the typeclasses -- we've finished, so take some classes - takeSomeClasses (State [] unresolved@(Sided ([], _) ([], _)) scoreAcc usedns) = - map statesFromMods . prod $ both (classMods . snd) unresolved + takeSomeInterfaces (State [] unresolved@(Sided ([], _) ([], _)) scoreAcc usedns) = + map statesFromMods . prod $ both (interfaceMods . snd) unresolved where swap (Sided l r) = Sided r l - statesFromMods :: Sided (Classes, AsymMods) -> State - statesFromMods sides = let classes = both (\(c, _) -> ([], c)) sides + statesFromMods :: Sided (Interfaces, AsymMods) -> State + statesFromMods sides = let interfaces = both (\(c, _) -> ([], c)) sides mods = swap (both snd sides) in - State [] classes (scoreAcc `mappend` (mempty { asymMods = mods })) usedns - classMods :: Classes -> [(Classes, AsymMods)] - classMods cs = let lcs = length cs in - [ (cs', mempty { typeClassIntro = lcs - length cs' }) | cs' <- subsets cs ] + State [] interfaces (scoreAcc `mappend` (mempty { asymMods = mods })) usedns + interfaceMods :: Interfaces -> [(Interfaces, AsymMods)] + interfaceMods cs = let lcs = length cs in + [ (cs', mempty { interfaceIntro = lcs - length cs' }) | cs' <- subsets cs ] prod :: Sided [a] -> [Sided a] prod (Sided ls rs) = [Sided l r | l <- ls, r <- rs] -- still have arguments to match, so just be the identity - takeSomeClasses s = [s] + takeSomeInterfaces s = [s] diff --git a/test/idrisdoc004/TestTypeclasses.idr b/test/idrisdoc004/TestInterfaces.idr similarity index 83% rename from test/idrisdoc004/TestTypeclasses.idr rename to test/idrisdoc004/TestInterfaces.idr index b7b1da837..891a5d3bf 100644 --- a/test/idrisdoc004/TestTypeclasses.idr +++ b/test/idrisdoc004/TestInterfaces.idr @@ -1,4 +1,4 @@ -module TestTypeclasses +module TestInterfaces ||| This is a test ||| diff --git a/test/idrisdoc004/expected b/test/idrisdoc004/expected index f976fc187..8318d0fa1 100644 --- a/test/idrisdoc004/expected +++ b/test/idrisdoc004/expected @@ -1 +1 @@ -Typeclasses are documented +Interfaces are documented diff --git a/test/idrisdoc004/run b/test/idrisdoc004/run index 42e85787c..98b7a9f04 100755 --- a/test/idrisdoc004/run +++ b/test/idrisdoc004/run @@ -1,5 +1,5 @@ #!/usr/bin/env bash -# Tests that documentation is generated for typeclasses -${IDRIS:-idris} $@ --mkdoc test_typeclasses.ipkg -[ -d test_typeclasses_doc ] && echo "Typeclasses are documented" +# Tests that documentation is generated for interfaces +${IDRIS:-idris} $@ --mkdoc test_interfaces.ipkg +[ -d test_interfaces_doc ] && echo "Interfaces are documented" rm -rf *.ibc *_doc diff --git a/test/idrisdoc004/test_interfaces.ipkg b/test/idrisdoc004/test_interfaces.ipkg new file mode 100644 index 000000000..a0cf6de1e --- /dev/null +++ b/test/idrisdoc004/test_interfaces.ipkg @@ -0,0 +1,6 @@ +package test_interfaces + +opts = "--quiet" + +modules = TestInterfaces + diff --git a/test/idrisdoc004/test_typeclasses.ipkg b/test/idrisdoc004/test_typeclasses.ipkg deleted file mode 100644 index de8e693dd..000000000 --- a/test/idrisdoc004/test_typeclasses.ipkg +++ /dev/null @@ -1,6 +0,0 @@ -package test_typeclasses - -opts = "--quiet" - -modules = TestTypeclasses - diff --git a/test/interfaces001/ClassName.idr b/test/interfaces001/InterfaceName.idr similarity index 92% rename from test/interfaces001/ClassName.idr rename to test/interfaces001/InterfaceName.idr index 0e44ad5f0..f0e3dfddb 100644 --- a/test/interfaces001/ClassName.idr +++ b/test/interfaces001/InterfaceName.idr @@ -1,4 +1,4 @@ -module ClassName +module InterfaceName ||| A fancy shower with a constructor ||| @ a the thing to be shown @@ -21,7 +21,7 @@ badShow = MkMyShow (const "hej") test1 : twiceAString 2 = "22" test1 = Refl -test2 : twiceAString @{ClassName.badShow} 2 = "hejhej" +test2 : twiceAString @{InterfaceName.badShow} 2 = "hejhej" test2 = Refl diff --git a/test/interfaces001/run b/test/interfaces001/run index c1b4f929b..aa7f4fb11 100755 --- a/test/interfaces001/run +++ b/test/interfaces001/run @@ -1,3 +1,3 @@ #!/usr/bin/env bash -${IDRIS:-idris} $@ --quiet --nocolour --consolewidth 70 ClassName.idr < input +${IDRIS:-idris} $@ --quiet --nocolour --consolewidth 70 InterfaceName.idr < input rm -f *.ibc diff --git a/test/regression001/reg065.idr b/test/regression001/reg065.idr index 8c89debd9..771e7a886 100644 --- a/test/regression001/reg065.idr +++ b/test/regression001/reg065.idr @@ -2,7 +2,7 @@ ||| ||| Fixes a regression where previous methods used in a later method's ||| type would lead to "can't find interface" errors -module TypeClassDep +module InterfaceDep import Data.Vect