a7e434a · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Allow Elab scripts to register type class instances

a7e434aDavid Raymond Christiansen11 years ago

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

compare with master

unifiedsplit

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

75 prim__DeclareType : TyDecl -> Elab ()

76 prim__DefineFunction : FunDefn -> Elab ()

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

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

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

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

204defineFunction : FunDefn -> Elab ()

205defineFunction : FunDefn -> Elab ()

205defineFunction defun = prim__DefineFunction defun

206defineFunction defun = prim__DefineFunction defun

206

207

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+

207debug : Elab a

215debug : Elab a

208debug = prim__Debug Nothing

216debug = prim__Debug Nothing

209

217

src/Idris/AbsSyntax.hs+19−10

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

353 where ptail [] = []

354 ptail (x : xs) = xs

355

356+-- | Add a class instance function.

357+--

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

359+--

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

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

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

361+-- resolved by default.

362+--

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

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

359−

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

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

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 ()

361−addInstance int n i

369+addInstance int res n i

362 = do ist <- getIState

370 = do ist <- getIState

363 case lookupCtxt n (idris_classes ist) of

371 case lookupCtxt n (idris_classes ist) of

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

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

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

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

366 putIState $ ist { idris_classes = cs }

374 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)

368 putIState $ ist { idris_classes = cs }

376 putIState $ ist { idris_classes = cs }

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

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

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

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

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

371 | otherwise = insI i ins

380 | otherwise = insI i ins

372− insI i [] = [i]

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

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

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

374 | otherwise = n : insI i ns

383 | otherwise = n : insI i ns

375

384

376 chaser (UN nm)

385 chaser (UN nm)

src/Idris/AbsSyntaxTree.hs+3−2

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

274 | IBCImp Name

275 | IBCStatic Name

276 | IBCClass Name

277− | IBCInstance Bool Name Name

277+ | IBCInstance Bool Bool Name Name

278 | IBCDSL Name

279 | IBCData Name

280 | IBCOpt Name

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

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

673data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type

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

675+ | RAddInstance Name Name

675

676

676-- | For elaborator state

677-- | For elaborator state

677data EState = EState {

678data EState = EState {

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

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

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

1084 class_default_superclasses :: [PDecl],

1085 class_default_superclasses :: [PDecl],

1085 class_params :: [Name],

1086 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

1087 class_determiners :: [Int] }

1088 class_determiners :: [Int] }

1088 deriving Show

1089 deriving Show

1089{-!

1090{-!

src/Idris/Docs.hs+2−2

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

232 classNameForInst ist n =

233 listToMaybe [ cn

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

235− , n `elem` class_instances ci

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

236 ]

237

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

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

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

255 delabTy i inst,

256 docsForInstance inst))

257− (nub (class_instances ci))

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

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

259 superclasses = catMaybes $ map getDInst (class_default_superclasses ci)

260 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

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

210 [(n, _)] -> n

211 _ -> conn

212− addInstance False conn' cfn

212+ addInstance False True conn' cfn

213− addIBC (IBCInstance False conn' cfn)

213+ addIBC (IBCInstance False True conn' cfn)

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

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

216 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

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

78 case expn of

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

80− (class_instances ci)

80+ (map fst $ class_instances ci)

81− addInstance intInst n iname

81+ addInstance intInst True n iname

82− Just _ -> addInstance intInst n iname

82+ Just _ -> addInstance intInst False n iname

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

84 let ips = zip (class_params ci) ps

85 let ns = case n of

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

143 mapM_ (rec_elabDecl info EAll info) idecls

144 ist <- getIState

145 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)

147

148 where

149 intInst = case ps of

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

186 ctxt <- getContext

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

188 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)

190

191 findOverlapping i dets t n

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

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

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

1431 Nothing -> lift . tfail . InternalMsg $

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

1433

1434−

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

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

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

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

1436findInstances ist t

1437findInstances ist t

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

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

1438 = case lookupCtxt n (idris_classes ist) of

1439 = case lookupCtxt n (idris_classes ist) of

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

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

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

1440 _ -> []

1442 _ -> []

1441 | otherwise = []

1443 | otherwise = []

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

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

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

1466 proofSearch rec prv ambigok (not prv) depth

1468 proofSearch rec prv ambigok (not prv) depth

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

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

1468

1470

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

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

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

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

1471−-- name).

1472resolveTC :: Bool -- using default Int

1473resolveTC :: Bool -- using default Int

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

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

1474 -> Int -- depth

1475 -> Int -- depth

1475 -> Term -- top level goal

1476 -> Term -- top level goal

1476 -> Name -- top level function name

1477 -> Name -- top level function name

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

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

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

1528 notHole _ _ = True

1529 notHole _ _ = True

1529

1530

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

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

1532−

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

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

1534 -- of flag in ClassInfo structure

1532 -- of flag in ClassInfo structure

1535 chaser (UN nm)

1533 chaser (UN nm)

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

1555 -- ps <- get_probs

1553 -- ps <- get_probs

1556 lift $ tfail $ CantResolve False topg

1554 lift $ tfail $ CantResolve False topg

1557 blunderbuss t d stk (n:ns)

1555 blunderbuss t d stk (n:ns)

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

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

1559− = tryCatch (resolve n d)

1557+ = tryCatch (resolve n d)

1560 (\e -> case e of

1558 (\e -> case e of

1561 CantResolve True _ -> lift $ tfail e

1559 CantResolve True _ -> lift $ tfail e

1562− _ -> blunderbuss t d stk ns)

1560+ _ -> blunderbuss t d stk ns)

1563 | otherwise = blunderbuss t d stk ns

1561 | otherwise = blunderbuss t d stk ns

1564

1562

1565 introImps = do g <- goal

1563 introImps = do g <- goal

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

1888 = do defn <- reifyFunDefn decl

1886 = do defn <- reifyFunDefn decl

1889 defineFunction defn

1887 defineFunction defn

1890 returnUnit

1888 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

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

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

1892 = do goal' <- reifyRaw goal

1896 = do goal' <- reifyRaw goal

1893 ctxt <- get_context

1897 ctxt <- get_context

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

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

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

2267 in addDeferred ds'

2271 in addDeferred ds'

2268 _ -> return ()

2272 _ -> 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)

2269 RClausesInstrs n cs ->

2279 RClausesInstrs n cs ->

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

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

2271 solveDeferred n

2281 solveDeferred n

src/Idris/IBC.hs+6−6

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

41import Util.Zlib (decompressEither)

43ibcVersion :: Word16

44−ibcVersion = 108

44+ibcVersion = 109

46data IBCFile = IBCFile { ver :: Word16,

47 sourcefile :: FilePath,

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

52 ibc_fixes :: ![FixDecl],

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

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

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

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

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

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

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

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

229 = case lookupCtxtExact n (idris_classes i) of

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

231 _ -> ifail "IBC write failed"

232−ibc i (IBCInstance int n ins) f

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

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

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

234ibc i (IBCDSL n) f

235 = case lookupCtxtExact n (idris_dsls i) of

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

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

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

440 cs

441

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

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

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

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

444

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

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

src/Idris/TypeSearch.hs+1−1

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

439 className <- getClassName clss

440 classDef <- lookupCtxt className classInfo

441 n <- class_instances classDef

442− def <- lookupCtxt n (definitions ctxt)

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

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

444 let ty' = vToP (uniqueBinders usedns nty)

445 return ty'