mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-10-26 18:02:24 +03:00
replace code level class symbol with inferface
This commit is contained in:
parent
06cc10a5e0
commit
c3f0755519
@ -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
|
||||
|
@ -1,4 +1,4 @@
|
||||
module Classes.Verified
|
||||
module Interfaces.Verified
|
||||
|
||||
import Control.Algebra
|
||||
import Control.Algebra.Lattice
|
@ -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,
|
||||
|
@ -1,6 +1,6 @@
|
||||
module Default
|
||||
|
||||
class Default a where
|
||||
interface Default a where
|
||||
default : a
|
||||
|
||||
instance Default Int where
|
||||
|
@ -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.
|
||||
|
@ -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..]]
|
||||
|
@ -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
|
||||
|
@ -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)
|
||||
|
@ -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
|
||||
|
@ -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)) ++ " "
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
@ -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)
|
||||
|
@ -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))
|
||||
|
@ -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
|
||||
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
||||
|
@ -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
|
||||
|
@ -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"
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
@ -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]
|
||||
_ -> []
|
||||
|
@ -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
|
||||
|
@ -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]
|
||||
|
@ -1,4 +1,4 @@
|
||||
module TestTypeclasses
|
||||
module TestInterfaces
|
||||
|
||||
||| This is a test
|
||||
|||
|
@ -1 +1 @@
|
||||
Typeclasses are documented
|
||||
Interfaces are documented
|
||||
|
@ -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
|
||||
|
6
test/idrisdoc004/test_interfaces.ipkg
Normal file
6
test/idrisdoc004/test_interfaces.ipkg
Normal file
@ -0,0 +1,6 @@
|
||||
package test_interfaces
|
||||
|
||||
opts = "--quiet"
|
||||
|
||||
modules = TestInterfaces
|
||||
|
@ -1,6 +0,0 @@
|
||||
package test_typeclasses
|
||||
|
||||
opts = "--quiet"
|
||||
|
||||
modules = TestTypeclasses
|
||||
|
@ -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
|
||||
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user