72b9e95 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #1618 from jfdm/tidyup/lift-todos-3

72b9e95Edwin Brady12 years ago

src/Idris/Elab/Clause.hs+37−37

compare with master

unifiedsplit

@@ -90,7 +90,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

90 Nothing -> transformPats ist pats_in

91 _ -> pats_in

93− let pats = map (simple_lhs (tt_ctxt ist)) $

93+ let pats = map (simple_lhs (tt_ctxt ist)) $

94 doPartialEval ist tpats

96 -- logLvl 3 (showSep "\n" (map (\ (l,r) ->

@@ -257,7 +257,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

257

258 getLHS (_, l, _) = l

259

260− simple_lhs ctxt (Right (x, y)) = Right (normalise ctxt [] x,

260+ simple_lhs ctxt (Right (x, y)) = Right (normalise ctxt [] x,

261 force (normalisePats ctxt [] y))

262 simple_lhs ctxt t = t

263

@@ -265,10 +265,10 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

265 (rt_simplify ctxt [] y)))

266

267 -- this is so pattern types are in the right form for erasure

268− normalisePats ctxt env (Bind n (PVar t) sc)

268+ normalisePats ctxt env (Bind n (PVar t) sc)

269 = let t' = normalise ctxt env t in

270 Bind n (PVar t') (normalisePats ctxt ((n, PVar t') : env) sc)

271− normalisePats ctxt env (Bind n (PVTy t) sc)

271+ normalisePats ctxt env (Bind n (PVTy t) sc)

272 = let t' = normalise ctxt env t in

273 Bind n (PVTy t') (normalisePats ctxt ((n, PVar t') : env) sc)

274 normalisePats ctxt env t = t

@@ -284,7 +284,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

284 else tfail (At fc (Msg "Clauses have differing numbers of arguments "))

285 sameLength [] = return 0

286

287− -- Partially evaluate, if the definition is marked as specialisable

287+ -- Partially evaluate, if the definition is marked as specialisable

288 doPartialEval ist pats =

289 case specNames opts of

290 Nothing -> pats

@@ -296,14 +296,14 @@ elabPE info fc caller r =

296 do ist <- getIState

297 let sa = getSpecApps ist [] r

298 mapM_ (mkSpecialised ist) sa

299− where

299+ where

300− -- Make a specialised version of the application, and

300+ -- Make a specialised version of the application, and

301− -- add a PTerm level transformation rule, which is basically the

301+ -- add a PTerm level transformation rule, which is basically the

302− -- new definition in reverse (before specialising it).

302+ -- new definition in reverse (before specialising it).

303− -- RHS => LHS where implicit arguments are left blank in the

303+ -- RHS => LHS where implicit arguments are left blank in the

304 -- transformation.

305

306− -- Transformation rules are applied after every PClause elaboration

306+ -- Transformation rules are applied after every PClause elaboration

307

308 mkSpecialised ist specapp_in = do

309 let (specTy, specapp) = getSpecTy ist specapp_in

@@ -315,7 +315,7 @@ elabPE info fc caller r =

315 idrisCatch

316 (when (undef && all (concreteArg ist) (snd specapp)) $ do

317 cgns <- getAllNames n

318− let opts = [Specialise (map (\x -> (x, Nothing)) cgns ++

318+ let opts = [Specialise (map (\x -> (x, Nothing)) cgns ++

319 mapMaybe specName (snd specapp))]

320 logLvl 3 $ "Specialising application: " ++ show specapp

321 ++ " with " ++ show cgns

@@ -323,25 +323,25 @@ elabPE info fc caller r =

323 logLvl 3 $ "PE definition type : " ++ (show specTy)

324 ++ "\n" ++ show opts

325 logLvl 3 $ "PE definition " ++ show newnm ++ ":\n" ++

326−-- showSep "\n"

326+-- showSep "\n"

327-- (map (\ (lhs, rhs) ->

328− (showTmImpls lhs ++ " = " ++

328+ (showTmImpls lhs ++ " = " ++

329 showTmImpls rhs) -- pats)

330

331 logLvl 2 $ show n ++ " transformation rule: " ++

332 show rhs ++ " ==> " ++ show lhs

333

334 elabType info defaultSyntax emptyDocstring [] fc opts newnm specTy

335− let def = -- map (\ (lhs, rhs) ->

335+ let def = -- map (\ (lhs, rhs) ->

336 [PClause fc newnm lhs [] rhs []] --) pats

337 elabTransform info fc False rhs lhs

338 elabClauses info fc opts newnm def)

339 -- if it doesn't work, just don't specialise. Could happen for lots

340 -- of valid reasons (e.g. local variables in scope which can't be

341 -- lifted out).

342− (\e -> logLvl 4 $ "Couldn't specialise: " ++ (pshow ist e))

342+ (\e -> logLvl 4 $ "Couldn't specialise: " ++ (pshow ist e))

343

344− specName (ImplicitS, tm)

344+ specName (ImplicitS, tm)

345 | (P Ref n _, _) <- unApply tm = Just (n, Just 1)

346 specName (ExplicitS, tm)

347 | (P Ref n _, _) <- unApply tm = Just (n, Just 1)

@@ -370,8 +370,8 @@ elabPE info fc caller r =

370

371 -- get the clause of a specialised application

372 getSpecClause ist (n, args)

373− = let newnm = sUN ("PE_"++show (nsroot n) ++ "_" ++

373+ = let newnm = sUN ("PE_"++show (nsroot n) ++ "_" ++

374− qhash 0 (showSep "_" (map showArg args))) in

374+ qhash 0 (showSep "_" (map showArg args))) in

375 -- UN (show n ++ show (map snd args)) in

376 (n, newnm, mkPE_TermDecl ist newnm n args)

377 where showArg (ExplicitS, n) = show n

@@ -413,8 +413,8 @@ checkPossible info fc tcgen fname lhs_in

413 validCase ctxt (Elaborating _ _ e) = validCase ctxt e

414 validCase ctxt (ElaboratingArg _ _ _ e) = validCase ctxt e

415 validCase ctxt _ = True

416−

416+

417− recoverable ctxt (CantUnify r topx topy e _ _)

417+ recoverable ctxt (CantUnify r topx topy e _ _)

418 = let topx' = normalise ctxt [] topx

419 topy' = normalise ctxt [] topy in

420 checkRec topx' topy'

@@ -423,7 +423,7 @@ checkPossible info fc tcgen fname lhs_in

423 recoverable ctxt (ElaboratingArg _ _ _ e) = recoverable ctxt e

424 recoverable _ _ = False

425

426− sameFam topx topy

426+ sameFam topx topy

427 = case (unApply topx, unApply topy) of

428 ((P _ x _, _), (P _ y _, _)) -> x == y

429 _ -> False

@@ -434,11 +434,11 @@ checkPossible info fc tcgen fname lhs_in

434

435 checkRec (App f a) p@(P _ _ _) = checkRec f p

436 checkRec p@(P _ _ _) (App f a) = checkRec p f

437− checkRec fa@(App _ _) fa'@(App _ _)

437+ checkRec fa@(App _ _) fa'@(App _ _)

438 | (f, as) <- unApply fa,

439 (f', as') <- unApply fa'

440− = if (length as /= length as')

440+ = if (length as /= length as')

441− then checkRec f f'

441+ then checkRec f f'

442 else checkRec f f' && and (zipWith checkRec as as')

443 checkRec (P xt x _) (P yt y _) = x == y || ntRec xt yt

444 checkRec _ _ = False

@@ -488,7 +488,7 @@ elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])

488 let lhs = addImpl i lhs_in

489 b <- checkPossible info fc tcgen fname lhs_in

490 case b of

491− True -> tclift $ tfail (At fc

491+ True -> tclift $ tfail (At fc

492 (Msg $ show lhs_in ++ " is a valid case"))

493 False -> do ptm <- mkPatTm lhs_in

494 return (Left ptm, lhs)

@@ -541,9 +541,11 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

541 -- These are the names we're not allowed to use on the RHS, because

542 -- they're UniqueTypes and borrowed from another function.

543 -- FIXME: There is surely a nicer way than this...

544+ -- Issue #1615 on the Issue Tracker.

545+ -- https://github.com/idris-lang/Idris-dev/issues/1615

544 when (not (null borrowed)) $

546 when (not (null borrowed)) $

545 logLvl 5 ("Borrowed names on LHS: " ++ show borrowed)

547 logLvl 5 ("Borrowed names on LHS: " ++ show borrowed)

546−

548+

547 logLvl 3 ("Normalised LHS: " ++ showTmImpls (delabMV i clhs))

549 logLvl 3 ("Normalised LHS: " ++ showTmImpls (delabMV i clhs))

548

550

549 rep <- useREPL

551 rep <- useREPL

@@ -587,7 +589,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

587 tclift $ elaborate ctxt (sMN 0 "patRHS") clhsty []

589 tclift $ elaborate ctxt (sMN 0 "patRHS") clhsty []

588 (do pbinds ist lhs_tm

590 (do pbinds ist lhs_tm

589 mapM_ setinj (nub (params ++ inj))

591 mapM_ setinj (nub (params ++ inj))

590− setNextName

592+ setNextName

591 (_, _, is) <- errAt "right hand side of " fname

593 (_, _, is) <- errAt "right hand side of " fname

592 (erun fc (build i winfo ERHS opts fname rhs))

594 (erun fc (build i winfo ERHS opts fname rhs))

593 errAt "right hand side of " fname

595 errAt "right hand side of " fname

@@ -604,7 +606,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

604

606

605 logLvl 5 "DONE CHECK"

607 logLvl 5 "DONE CHECK"

606 logLvl 2 $ "---> " ++ show rhs'

608 logLvl 2 $ "---> " ++ show rhs'

607− when (not (null defer)) $ iLOG $ "DEFERRED " ++

609+ when (not (null defer)) $ iLOG $ "DEFERRED " ++

608 show (map (\ (n, (_,_,t)) -> (n, t)) defer)

610 show (map (\ (n, (_,_,t)) -> (n, t)) defer)

609 def' <- checkDef fc defer

611 def' <- checkDef fc defer

610 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'

612 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'

@@ -624,7 +626,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

624 logLvl 5 $ "Rechecking"

626 logLvl 5 $ "Rechecking"

625 logLvl 6 $ " ==> " ++ show (forget rhs')

627 logLvl 6 $ " ==> " ++ show (forget rhs')

626

628

627− (crhs, crhsty) <- if not inf

629+ (crhs, crhsty) <- if not inf

628 then recheckC_borrowing True borrowed fc [] rhs'

630 then recheckC_borrowing True borrowed fc [] rhs'

629 else return (rhs', clhsty)

631 else return (rhs', clhsty)

630 logLvl 6 $ " ==> " ++ show crhsty ++ " against " ++ show clhsty

632 logLvl 6 $ " ==> " ++ show crhsty ++ " against " ++ show clhsty

@@ -637,16 +639,16 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

637 -- then we'll try running it in reverse to improve error messages

639 -- then we'll try running it in reverse to improve error messages

638 let (ret_fam, _) = unApply (getRetTy crhsty)

640 let (ret_fam, _) = unApply (getRetTy crhsty)

639 rev <- case ret_fam of

641 rev <- case ret_fam of

640− P _ rfamn _ ->

642+ P _ rfamn _ ->

641 case lookupCtxt rfamn (idris_datatypes i) of

643 case lookupCtxt rfamn (idris_datatypes i) of

642− [TI _ _ dopts _ _] ->

644+ [TI _ _ dopts _ _] ->

643 return (DataErrRev `elem` dopts)

645 return (DataErrRev `elem` dopts)

644 _ -> return False

646 _ -> return False

645 _ -> return False

647 _ -> return False

646

648

647 when (rev || ErrorReverse `elem` opts) $ do

649 when (rev || ErrorReverse `elem` opts) $ do

648 addIBC (IBCErrRev (crhs, clhs))

650 addIBC (IBCErrRev (crhs, clhs))

649− addErrRev (crhs, clhs)

651+ addErrRev (crhs, clhs)

650 return $ (Right (clhs, crhs), lhs)

652 return $ (Right (clhs, crhs), lhs)

651 where

653 where

652 pinfo :: ElabInfo -> [(Name, PTerm)] -> [Name] -> Int -> ElabInfo

654 pinfo :: ElabInfo -> [(Name, PTerm)] -> [Name] -> Int -> ElabInfo

@@ -666,7 +668,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

666 -- we know they can't be used on the RHS

668 -- we know they can't be used on the RHS

667 borrowedNames :: [Name] -> Term -> [Name]

669 borrowedNames :: [Name] -> Term -> [Name]

668 borrowedNames env (App (App (P _ (NS (UN lend) [owner]) _) _) arg)

670 borrowedNames env (App (App (P _ (NS (UN lend) [owner]) _) _) arg)

669− | owner == txt "Ownership" &&

671+ | owner == txt "Ownership" &&

670 (lend == txt "lend" || lend == txt "Read") = getVs arg

672 (lend == txt "lend" || lend == txt "Read") = getVs arg

671 where

673 where

672 getVs (V i) = [env!!i]

674 getVs (V i) = [env!!i]

@@ -714,7 +716,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

714 isArg :: Name -> PDecl -> Bool

716 isArg :: Name -> PDecl -> Bool

715 isArg n (PClauses _ _ _ cs) = any isArg' cs

717 isArg n (PClauses _ _ _ cs) = any isArg' cs

716 where

718 where

717− isArg' (PClause _ _ (PApp _ _ args) _ _ _)

719+ isArg' (PClause _ _ (PApp _ _ args) _ _ _)

718 = any (\x -> case x of

720 = any (\x -> case x of

719 PRef _ n' -> n == n'

721 PRef _ n' -> n == n'

720 _ -> False) (map getTm args)

722 _ -> False) (map getTm args)

@@ -892,5 +894,3 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

892 split deps [] pre = (reverse pre, [])

894 split deps [] pre = (reverse pre, [])

893

895

894 abstract wn wv wty (n, argty) = (n, substTerm wv (P Bound wn wty) argty)

896 abstract wn wv wty (n, argty) = (n, substTerm wv (P Bound wn wty) argty)

895−

896−

src/Idris/Elab/Data.hs+7−10

@@ -124,7 +124,7 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

124 [oi] -> putIState ist{ idris_optimisation = addDef n oi{ detaggable = True } opt }

125 _ -> putIState ist{ idris_optimisation = addDef n (Optimise [] True) opt }

126

127− checkDefinedAs fc n t ctxt

127+ checkDefinedAs fc n t ctxt

128 = case lookupDef n ctxt of

129 [] -> return ()

130 [TyDecl _ ty] ->

@@ -204,14 +204,9 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

204 liftname = id -- Is this appropriate?

205 }

206

207−-- FIXME: 'forcenames' is an almighty hack! Need a better way of

208−-- erasing non-forceable things

209−-- ^^^

210−-- TODO: the above is a comment from the past;

211−-- forcenames is probably no longer needed

212elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->

207elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->

213 Type -> -- for kind checking

208 Type -> -- for kind checking

214− (Docstring (Maybe PTerm), [(Name, Docstring (Maybe PTerm))], Name, PTerm, FC, [Name]) ->

209+ (Docstring (Maybe PTerm), [(Name, Docstring (Maybe PTerm))], Name, PTerm, FC, [Name]) ->

215 Idris (Name, Type)

210 Idris (Name, Type)

216elabCon info syn tn codata expkind (doc, argDocs, n, t_in, fc, forcenames)

211elabCon info syn tn codata expkind (doc, argDocs, n, t_in, fc, forcenames)

217 = do checkUndefined fc n

212 = do checkUndefined fc n

@@ -244,7 +239,7 @@ elabCon info syn tn codata expkind (doc, argDocs, n, t_in, fc, forcenames)

244 else return ()

239 else return ()

245 tyIs con t = tclift $ tfail (At fc (Elaborating "constructor " con (Msg (show t ++ " is not " ++ show tn))))

240 tyIs con t = tclift $ tfail (At fc (Elaborating "constructor " con (Msg (show t ++ " is not " ++ show tn))))

246

241

247− mkLazy (PPi pl n ty sc)

242+ mkLazy (PPi pl n ty sc)

248 = let ty' = if getTyName ty

243 = let ty' = if getTyName ty

249 then PApp fc (PRef fc (sUN "Lazy'"))

244 then PApp fc (PRef fc (sUN "Lazy'"))

250 [pexp (PRef fc (sUN "LazyCodata")),

245 [pexp (PRef fc (sUN "LazyCodata")),

@@ -277,6 +272,9 @@ elabCon info syn tn codata expkind (doc, argDocs, n, t_in, fc, forcenames)

277

272

278type EliminatorState = StateT (Map.Map String Int) Idris

273type EliminatorState = StateT (Map.Map String Int) Idris

279

274

275+-- -- Issue #1616 in the issue tracker.

276+-- https://github.com/idris-lang/Idris-dev/issues/1616

277+--

280-- TODO: Rewrite everything to use idris_implicits instead of manual splitting (or in TT)

278-- TODO: Rewrite everything to use idris_implicits instead of manual splitting (or in TT)

281-- FIXME: Many things have name starting with elim internally since this was the only purpose in the first edition of the function

279-- FIXME: Many things have name starting with elim internally since this was the only purpose in the first edition of the function

282-- rename to caseFun to match updated intend

280-- rename to caseFun to match updated intend

@@ -417,7 +415,7 @@ elabCaseFun ind paramPos n ty cons info = do

417 case findIndex (== n) oldParams of

415 case findIndex (== n) oldParams of

418 Nothing -> (PPi pl n (removeParamPis oldParams params tyb) (removeParamPis oldParams params tyr))

416 Nothing -> (PPi pl n (removeParamPis oldParams params tyb) (removeParamPis oldParams params tyr))

419 Just i -> (removeParamPis oldParams params tyr)

417 Just i -> (removeParamPis oldParams params tyr)

420− removeParamPis oldParams params (PRef _ n) =

418+ removeParamPis oldParams params (PRef _ n) =

421 case findIndex (== n) oldParams of

419 case findIndex (== n) oldParams of

422 Nothing -> (PRef elimFC n)

420 Nothing -> (PRef elimFC n)

423 Just i -> let (newname,_,_) = params !! i in (PRef elimFC (newname))

421 Just i -> let (newname,_,_) = params !! i in (PRef elimFC (newname))

@@ -518,4 +516,3 @@ elabCaseFun ind paramPos n ty cons info = do

518 where applyRecElim :: (Name, Plicity, PTerm) -> PArg

516 where applyRecElim :: (Name, Plicity, PTerm) -> PArg

519 applyRecElim (constr@(recCnm,_,recTy)) = pexp $ PApp elimFC (PRef elimFC elimDeclName) (generalArgs ++ map pexp idxs ++ [pexp $ PRef elimFC recCnm])

517 applyRecElim (constr@(recCnm,_,recTy)) = pexp $ PApp elimFC (PRef elimFC elimDeclName) (generalArgs ++ map pexp idxs ++ [pexp $ PRef elimFC recCnm])

520 where (_, idxs) = splitArgPms recTy

518 where (_, idxs) = splitArgPms recTy

521−

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

@@ -63,7 +63,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

63 (n, ci) <- case lookupCtxtName n (idris_classes i) of

64 [c] -> return c

65 [] -> ifail $ show fc ++ ":" ++ show n ++ " is not a type class"

66− cs -> tclift $ tfail $ At fc

66+ cs -> tclift $ tfail $ At fc

67 (CantResolveAlts (map fst cs))

68 let constraint = PApp fc (PRef fc n) (map pexp ps)

69 let iname = mkiname n ps expn

@@ -77,7 +77,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

77 (class_instances ci)

78 addInstance intInst n iname

79 Just _ -> addInstance intInst n iname

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

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

81 let ips = zip (class_params ci) ps

82 let ns = case n of

83 NS n ns' -> ns'

@@ -93,7 +93,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

93 mapM_ (rec_elabDecl info EAll info) undefinedSuperclassInstances

94 let all_meths = map (nsroot . fst) (class_methods ci)

95 let mtys = map (\ (n, (op, t)) ->

96− let t_in = substMatchesShadow ips pnames t

96+ let t_in = substMatchesShadow ips pnames t

97 mnamemap = map (\n -> (n, PRef fc (decorate ns iname n)))

98 all_meths

99 t' = substMatchesShadow mnamemap pnames t_in in

@@ -115,7 +115,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

115 -- Bring variables in instance head into scope

116 ist <- getIState

117 let headVars = nub $ mapMaybe (\p -> case p of

118− PRef _ n ->

118+ PRef _ n ->

119 case lookupTy n (tt_ctxt ist) of

120 [] -> Just n

121 _ -> Nothing

@@ -157,6 +157,8 @@ elabInstance info syn what fc cs n ps t expn ds = do

157 _ -> return False -- couldn't find class, just let elabInstance fail later

158

159 -- TODO: largely based upon elabType' - should try to abstract

160+ -- Issue #1614 in the issue tracker:

161+ -- https://github.com/idris-lang/Idris-dev/issues/1614

160 elabFindOverlapping i ci iname syn t

162 elabFindOverlapping i ci iname syn t

161 = do ty' <- addUsingConstraints syn fc t

163 = do ty' <- addUsingConstraints syn fc t

162 -- TODO think: something more in info?

164 -- TODO think: something more in info?

@@ -256,5 +258,3 @@ elabInstance info syn what fc cs n ps t expn ds = do

256 clauseFor m iname ns (PClauses _ _ m' _)

258 clauseFor m iname ns (PClauses _ _ m' _)

257 = decorate ns iname m == decorate ns iname m'

259 = decorate ns iname m == decorate ns iname m'

258 clauseFor m iname ns _ = False

260 clauseFor m iname ns _ = False

259−

260−

src/Idris/IdeSlave.hs+2−2

@@ -145,7 +145,7 @@ instance SExpable OutputAnnotation where

145 ItalicText -> "italic"

146 UnderlineText -> "underline"

147 toSExp (AnnTerm bnd tm) = toSExp [(SymbolAtom "tt-term", StringAtom (encodeTerm bnd tm))]

148− toSExp (AnnSearchResult ordr) = toSExp [(SymbolAtom "doc-overview",

148+ toSExp (AnnSearchResult ordr) = toSExp [(SymbolAtom "doc-overview",

149 StringAtom ("Result type is " ++ descr))]

150 where descr = case ordr of

151 EQ -> "isomorphic"

@@ -251,7 +251,7 @@ sexpToCommand (SexpList [SymbolAtom "apropos", StringAtom search])

251sexpToCommand (SymbolAtom "get-options") = Just GetOpts

252sexpToCommand (SexpList [SymbolAtom "set-option", SymbolAtom s, BoolAtom b])

253 | Just opt <- lookup s opts = Just (SetOpt opt b)

254− where opts = [("show-implicits", ShowImpl), ("error-context", ErrContext)] --TODO support more

254+ where opts = [("show-implicits", ShowImpl), ("error-context", ErrContext)] --TODO support more options. Issue #1611 in the Issue tracker. https://github.com/idris-lang/Idris-dev/issues/1611

255sexpToCommand (SexpList [SymbolAtom "metavariables", IntegerAtom cols]) = Just (Metavariables (fromIntegral cols))

256sexpToCommand (SexpList [SymbolAtom "who-calls", StringAtom name]) = Just (WhoCalls name)

257sexpToCommand (SexpList [SymbolAtom "calls-who", StringAtom name]) = Just (CallsWho name)

src/Idris/Primitives.hs+3

@@ -262,6 +262,9 @@ vecCmps ity =

262 , iCmp ity "gt" True (bCmp ity (>)) LGt total

263 ]

264

265+-- The TODOs in this function are documented as Issue #1617 on the issue tracker.

266+--

267+-- https://github.com/idris-lang/Idris-dev/issues/1617

265vecOps :: IntTy -> [Prim]

268vecOps :: IntTy -> [Prim]

266vecOps ity@(ITVec elem count) =

269vecOps ity@(ITVec elem count) =

267 [ Prim (sUN $ "prim__mk" ++ intTyName ity)

270 [ Prim (sUN $ "prim__mk" ++ intTyName ity)