a7e434a · Idris-dev · git.iko.soy

libs/prelude/Language/Reflection/Elab.idr+8

@@ -74,6 +74,7 @@ data Elab : Type -> Type where

7474

7575 prim__DeclareType : TyDecl -> Elab ()

7676 prim__DefineFunction : FunDefn -> Elab ()

77+ prim__AddInstance : TTName -> TTName -> Elab ()

7778

7879 prim__RecursiveElab : Raw -> Elab () -> Elab (TT, TT)

7980

@@ -204,6 +205,13 @@ declareType decl = prim__DeclareType decl

204205defineFunction : FunDefn -> Elab ()

205206defineFunction defun = prim__DefineFunction defun

206207

208+||| Register a new instance for type class resolution

209+|||

210+||| @ className the name of the class for which an instance is being registered

211+||| @ instName the name of the definition to use in instance search

212+addInstance : (className, instName : TTName) -> Elab ()

213+addInstance className instName = prim__AddInstance className instName

214+

207215debug : Elab a

208216debug = prim__Debug Nothing

209217

src/Idris/AbsSyntax.hs+19−10

@@ -353,24 +353,33 @@ pop_estack = do i <- getIState

353353 where ptail [] = []

354354 ptail (x : xs) = xs

355355

356−-- Add a class instance function. Dodgy hack: Put integer instances first in the

357−-- list so they are resolved by default.

356+-- | Add a class instance function.

357+--

358+-- Precondition: the instance should have the correct type.

359+--

360+-- Dodgy hack 1: Put integer instances first in the list so they are

361+-- resolved by default.

362+--

358363-- Dodgy hack 2: put constraint chasers (@@) last

359−

360−addInstance :: Bool -> Name -> Name -> Idris ()

361−addInstance int n i

364+addInstance :: Bool -- ^ whether the name is an Integer instance

365+ -> Bool -- ^ whether to include the instance in instance search

366+ -> Name -- ^ the name of the class

367+ -> Name -- ^ the name of the instance

368+ -> Idris ()

369+addInstance int res n i

362370 = do ist <- getIState

363371 case lookupCtxt n (idris_classes ist) of

364372 [CI a b c d e ins fds] ->

365373 do let cs = addDef n (CI a b c d e (addI i ins) fds) (idris_classes ist)

366374 putIState $ ist { idris_classes = cs }

367− _ -> do let cs = addDef n (CI (sMN 0 "none") [] [] [] [] [i] []) (idris_classes ist)

375+ _ -> do let cs = addDef n (CI (sMN 0 "none") [] [] [] [] [(i, res)] []) (idris_classes ist)

368376 putIState $ ist { idris_classes = cs }

369− where addI i ins | int = i : ins

370− | chaser n = ins ++ [i]

377+ where addI, insI :: Name -> [(Name, Bool)] -> [(Name, Bool)]

378+ addI i ins | int = (i, res) : ins

379+ | chaser n = ins ++ [(i, res)]

371380 | otherwise = insI i ins

372− insI i [] = [i]

373− insI i (n : ns) | chaser n = i : n : ns

381+ insI i [] = [(i, res)]

382+ insI i (n : ns) | chaser (fst n) = (i, res) : n : ns

374383 | otherwise = n : insI i ns

375384

376385 chaser (UN nm)

src/Idris/AbsSyntaxTree.hs+3−2

@@ -274,7 +274,7 @@ data IBCWrite = IBCFix FixDecl

274274 | IBCImp Name

275275 | IBCStatic Name

276276 | IBCClass Name

277− | IBCInstance Bool Name Name

277+ | IBCInstance Bool Bool Name Name

278278 | IBCDSL Name

279279 | IBCData Name

280280 | IBCOpt Name

@@ -672,6 +672,7 @@ data Directive = DLib Codegen String |

672672-- after a term elaboration when there's been reflected elaboration.

673673data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type

674674 | RClausesInstrs Name [([Name], Term, Term)]

675+ | RAddInstance Name Name

675676

676677-- | For elaborator state

677678data EState = EState {

@@ -1083,7 +1084,7 @@ data ClassInfo = CI { instanceCtorName :: Name,

10831084 class_defaults :: [(Name, (Name, PDecl))], -- method name -> default impl

10841085 class_default_superclasses :: [PDecl],

10851086 class_params :: [Name],

1086− class_instances :: [Name],

1087+ class_instances :: [(Name, Bool)], -- the Bool is whether to include in instance search, so named instances are excluded

10871088 class_determiners :: [Int] }

10881089 deriving Show

10891090{-!

src/Idris/Docs.hs+2−2

@@ -232,7 +232,7 @@ getDocs n w

232232 classNameForInst ist n =

233233 listToMaybe [ cn

234234 | (cn, ci) <- toAlist (idris_classes ist)

235− , n `elem` class_instances ci

235+ , n `elem` map fst (class_instances ci)

236236 ]

237237

238238docData :: Name -> TypeInfo -> Idris Docs

@@ -254,7 +254,7 @@ docClass n ci

254254 instances = map (\inst -> (namedInst inst,

255255 delabTy i inst,

256256 docsForInstance inst))

257− (nub (class_instances ci))

257+ (nub (map fst (class_instances ci)))

258258 (subclasses, instances') = partition (isSubclass . (\(_,tm,_) -> tm)) instances

259259 superclasses = catMaybes $ map getDInst (class_default_superclasses ci)

260260 mdocs <- mapM (docFun . fst) (class_methods ci)

src/Idris/Elab/Class.hs+2−2

@@ -209,8 +209,8 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

209209 let conn' = case lookupCtxtName conn (idris_classes i) of

210210 [(n, _)] -> n

211211 _ -> conn

212− addInstance False conn' cfn

213− addIBC (IBCInstance False conn' cfn)

212+ addInstance False True conn' cfn

213+ addIBC (IBCInstance False True conn' cfn)

214214-- iputStrLn ("Added " ++ show (conn, cfn, ty))

215215 return [PTy emptyDocstring [] syn fc [] cfn NoFC ty,

216216 PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]

src/Idris/Elab/Instance.hs+5−5

@@ -77,9 +77,9 @@ elabInstance info syn doc argDocs what fc cs n nfc ps t expn ds = do

7777 -- and it's not a named instance, then it's overlapping, so report an error

7878 case expn of

7979 Nothing -> do mapM_ (maybe (return ()) overlapping . findOverlapping i (class_determiners ci) (delab i nty))

80− (class_instances ci)

81− addInstance intInst n iname

82− Just _ -> addInstance intInst n iname

80+ (map fst $ class_instances ci)

81+ addInstance intInst True n iname

82+ Just _ -> addInstance intInst False n iname

8383 when (what /= ETypes && (not (null ds && not emptyclass))) $ do

8484 let ips = zip (class_params ci) ps

8585 let ns = case n of

@@ -143,7 +143,7 @@ elabInstance info syn doc argDocs what fc cs n nfc ps t expn ds = do

143143 mapM_ (rec_elabDecl info EAll info) idecls

144144 ist <- getIState

145145 checkInjectiveArgs fc n (class_determiners ci) (lookupTyExact iname (tt_ctxt ist))

146− addIBC (IBCInstance intInst n iname)

146+ addIBC (IBCInstance intInst (isNothing expn) n iname)

147147

148148 where

149149 intInst = case ps of

@@ -186,7 +186,7 @@ elabInstance info syn doc argDocs what fc cs n nfc ps t expn ds = do

186186 ctxt <- getContext

187187 (cty, _) <- recheckC fc id [] tyT

188188 let nty = normalise ctxt [] cty

189− return $ any (isJust . findOverlapping i (class_determiners ci) (delab i nty)) (class_instances ci)

189+ return $ any (isJust . findOverlapping i (class_determiners ci) (delab i nty)) (map fst $ class_instances ci)

190190

191191 findOverlapping i dets t n

192192 | take 2 (show n) == "@@" = Nothing

src/Idris/Elab/Term.hs+22−12

@@ -1431,12 +1431,14 @@ findHighlight n = do ctxt <- get_context

14311431 Nothing -> lift . tfail . InternalMsg $

14321432 "Can't find name" ++ show n

14331433

1434−

1434+-- | Find the names of instances that have been designeated for

1435+-- searching (i.e. non-named instances or instances from Elab scripts)

14351436findInstances :: IState -> Term -> [Name]

14361437findInstances ist t

14371438 | (P _ n _, _) <- unApply (getRetTy t)

14381439 = case lookupCtxt n (idris_classes ist) of

1439− [CI _ _ _ _ _ ins _] -> filter accessible ins

1440+ [CI _ _ _ _ _ ins _] ->

1441+ [n | (n, True) <- ins, accessible n]

14401442 _ -> []

14411443 | otherwise = []

14421444 where accessible n = case lookupDefAccExact n False (tt_ctxt ist) of

@@ -1466,11 +1468,10 @@ proofSearch' ist rec ambigok depth prv top n hints

14661468 proofSearch rec prv ambigok (not prv) depth

14671469 (elab ist toplevel ERHS [] (sMN 0 "tac")) top n hints ist

14681470

1469−-- Resolve type classes. This will only pick up 'normal' instances, never

1470−-- named instances (hence using 'tcname' to check it's a generated instance

1471−-- name).

1471+-- | Resolve type classes. This will only pick up 'normal' instances, never

1472+-- named instances (which is enforced by 'findInstances').

14721473resolveTC :: Bool -- using default Int

1473− -> Bool -- allow metavariables in the goal

1474+ -> Bool -- allow metavariables in the goal

14741475 -> Int -- depth

14751476 -> Term -- top level goal

14761477 -> Name -- top level function name

@@ -1527,9 +1528,6 @@ resTC' tcs defaultOn topholes depth topg fn ist

15271528 | Constant _ <- c = not (n `elem` hs)

15281529 notHole _ _ = True

15291530

1530− elabTC n | n /= fn && tcname n = (resolve n depth, show n)

1531− | otherwise = (fail "Can't resolve", show n)

1532−

15331531 -- HACK! Rather than giving a special name, better to have some kind

15341532 -- of flag in ClassInfo structure

15351533 chaser (UN nm)

@@ -1555,11 +1553,11 @@ resTC' tcs defaultOn topholes depth topg fn ist

15551553 -- ps <- get_probs

15561554 lift $ tfail $ CantResolve False topg

15571555 blunderbuss t d stk (n:ns)

1558− | n /= fn && (n `elem` stk || tcname n)

1559− = tryCatch (resolve n d)

1556+ | n /= fn -- && (n `elem` stk)

1557+ = tryCatch (resolve n d)

15601558 (\e -> case e of

15611559 CantResolve True _ -> lift $ tfail e

1562− _ -> blunderbuss t d stk ns)

1560+ _ -> blunderbuss t d stk ns)

15631561 | otherwise = blunderbuss t d stk ns

15641562

15651563 introImps = do g <- goal

@@ -1888,6 +1886,12 @@ runTactical fc env tm = do tm' <- eval tm

18881886 = do defn <- reifyFunDefn decl

18891887 defineFunction defn

18901888 returnUnit

1889+ | n == tacN "prim__AddInstance", [cls, inst] <- args

1890+ = do className <- reifyTTName cls

1891+ instName <- reifyTTName inst

1892+ updateAux $ \e -> e { new_tyDecls = RAddInstance className instName :

1893+ new_tyDecls e}

1894+ returnUnit

18911895 | n == tacN "prim__RecursiveElab", [goal, script] <- args

18921896 = do goal' <- reifyRaw goal

18931897 ctxt <- get_context

@@ -2266,6 +2270,12 @@ processTacticDecls info steps =

22662270 let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds

22672271 in addDeferred ds'

22682272 _ -> return ()

2273+ RAddInstance className instName ->

2274+ do -- The type class resolution machinery relies on a special

2275+ logLvl 2 $ "Adding elab script instance " ++ show instName ++

2276+ " for " ++ show className

2277+ addInstance False True className instName

2278+ addIBC (IBCInstance False True className instName)

22692279 RClausesInstrs n cs ->

22702280 do logLvl 3 $ "Pattern-matching definition from tactics: " ++ show n

22712281 solveDeferred n

src/Idris/IBC.hs+6−6

@@ -41,7 +41,7 @@ import Codec.Archive.Zip

4141import Util.Zlib (decompressEither)

4242

4343ibcVersion :: Word16

44−ibcVersion = 108

44+ibcVersion = 109

4545

4646data IBCFile = IBCFile { ver :: Word16,

4747 sourcefile :: FilePath,

@@ -52,7 +52,7 @@ data IBCFile = IBCFile { ver :: Word16,

5252 ibc_fixes :: ![FixDecl],

5353 ibc_statics :: ![(Name, [Bool])],

5454 ibc_classes :: ![(Name, ClassInfo)],

55− ibc_instances :: ![(Bool, Name, Name)],

55+ ibc_instances :: ![(Bool, Bool, Name, Name)],

5656 ibc_dsls :: ![(Name, DSL)],

5757 ibc_datatypes :: ![(Name, TypeInfo)],

5858 ibc_optimise :: ![(Name, OptInfo)],

@@ -229,8 +229,8 @@ ibc i (IBCClass n) f

229229 = case lookupCtxtExact n (idris_classes i) of

230230 Just v -> return f { ibc_classes = (n,v): ibc_classes f }

231231 _ -> ifail "IBC write failed"

232−ibc i (IBCInstance int n ins) f

233− = return f { ibc_instances = (int,n,ins): ibc_instances f }

232+ibc i (IBCInstance int res n ins) f

233+ = return f { ibc_instances = (int, res, n, ins) : ibc_instances f }

234234ibc i (IBCDSL n) f

235235 = case lookupCtxtExact n (idris_dsls i) of

236236 Just v -> return f { ibc_dsls = (n,v): ibc_dsls f }

@@ -439,8 +439,8 @@ pClasses cs = mapM_ (\ (n, c) ->

439439 = addDef n c' (idris_classes i) }))

440440 cs

441441

442−pInstances :: [(Bool, Name, Name)] -> Idris ()

443−pInstances cs = mapM_ (\ (i, n, ins) -> addInstance i n ins) cs

442+pInstances :: [(Bool, Bool, Name, Name)] -> Idris ()

443+pInstances cs = mapM_ (\ (i, res, n, ins) -> addInstance i res n ins) cs

444444

445445pDSLs :: [(Name, DSL)] -> Idris ()

446446pDSLs cs = mapM_ (\ (n, c) -> updateIState (\i ->

src/Idris/TypeSearch.hs+1−1

@@ -439,7 +439,7 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh

439439 className <- getClassName clss

440440 classDef <- lookupCtxt className classInfo

441441 n <- class_instances classDef

442− def <- lookupCtxt n (definitions ctxt)

442+ def <- lookupCtxt (fst n) (definitions ctxt)

443443 nty <- normaliseC ctxt [] <$> (case typeFromDef def of Just x -> [x]; Nothing -> [])

444444 let ty' = vToP (uniqueBinders usedns nty)

445445 return ty'