02b6087 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #1743 from jfdm/fix/lift-fixme-todo-1

02b6087Edwin Brady12 years ago

src/IRTS/Compiler.hs+14−13

compare with master

unifiedsplit

@@ -62,7 +62,7 @@ compile codegen f tm

62 -- iputStrLn $ showSep "\n" (map show defs)

63 -- Inlined top level LDecl made here

64 let defsInlined = inlineAll defs

65− let defsUniq = map (allocUnique (addAlist defsInlined emptyContext))

65+ let defsUniq = map (allocUnique (addAlist defsInlined emptyContext))

66 defsInlined

68 let (nexttag, tagged) = addTags 65536 (liftAll defsUniq)

@@ -91,13 +91,13 @@ compile codegen f tm

91 iLOG "Building output"

93 case checked of

94− OK c -> do return $ CodegenInfo f outty triple cpu

94+ OK c -> do return $ CodegenInfo f outty triple cpu

95 hdrs impdirs objs libs flags

96 NONE c (toAlist defuns)

97 tagged

98-- runIO $ case codegen of

99-- ViaC -> codegenC cginfo

100−-- ViaJava -> codegenJava cginfo

100+-- ViaJava -> codegenJava cginfo

101-- ViaJavaScript -> codegenJavaScript cginfo

102-- ViaNode -> codegenNode cginfo

103-- ViaLLVM -> codegenLLVM cginfo

@@ -116,10 +116,10 @@ compile codegen f tm

116 if ex then return f else return h

117

118generate :: Codegen -> FilePath -> CodegenInfo -> IO ()

119−generate codegen mainmod ir

119+generate codegen mainmod ir

120 = case codegen of

121 -- Built-in code generators (FIXME: lift these out!)

122− Via "c" -> codegenC ir

122+ Via "c" -> codegenC ir

123 -- Any external code generator

124 Via cg -> do let cmd = "idris-" ++ cg

125 args = [mainmod, "-o", outputFile ir]

@@ -195,7 +195,7 @@ mkLDecl n (CaseOp ci _ _ _ pats cd)

195 where

196 (args, sc) = cases_runtime cd

197

198− -- Always attempt to inline functions arising from 'case' expressions

198+ -- Always attempt to inline functions arising from 'case' expressions

199 caseName (SN (CaseN _)) = True

200 caseName (SN (WithN _ _)) = True

201 caseName (NS n _) = caseName n

@@ -284,7 +284,7 @@ irTerm vs env tm@(App f a) = case unApply tm of

284 x' <- irTerm vs env x

285 t' <- irTerm vs env t

286 e' <- irTerm vs env e

287− return (LCase Shared x'

287+ return (LCase Shared x'

288 [LConCase 0 (sNS (sUN "False") ["Bool","Prelude"]) [] e'

289 ,LConCase 1 (sNS (sUN "True" ) ["Bool","Prelude"]) [] t'

290 ])

@@ -425,7 +425,7 @@ irTerm vs env (Bind _ _ _) = return $ LNothing

425

426irTerm vs env (Proj t (-1)) = do

427 t' <- irTerm vs env t

428− return $ LOp (LMinus (ATInt ITBig))

428+ return $ LOp (LMinus (ATInt ITBig))

429 [t', LConst (BI 1)]

430

431irTerm vs env (Proj t i) = LProj <$> irTerm vs env t <*> pure i

@@ -458,13 +458,13 @@ doForeign vs env (_ : fgn : args)

458 | fi == txt "FIntT"

459 = mkIntIty (str intTy)

460

461− mkIty' (App (App (P _ (UN ff) _) _) (App (P _ (UN fa) _) (App (P _ (UN io) _) _)))

461+ mkIty' (App (App (P _ (UN ff) _) _) (App (P _ (UN fa) _) (App (P _ (UN io) _) _)))

462 | ff == txt "FFunction"

463 , fa == txt "FAny"

464− , io == txt "IO"

464+ , io == txt "IO"

465 = FFunctionIO

466

467− mkIty' (App (App (P _ (UN ff) _) _) _)

467+ mkIty' (App (App (P _ (UN ff) _) _) _)

468 | ff == txt "FFunction"

469 = FFunction

470

@@ -472,7 +472,8 @@ doForeign vs env (_ : fgn : args)

472

473 -- would be better if these FInt types were evaluated at compile time

474 -- TODO: add %eval directive for such things

475−

475+ -- Issue #1742 on the issue tracker.

476+ -- https://github.com/idris-lang/Idris-dev/issues/1742

476 mkIty "FFloat" = FArith ATFloat

477 mkIty "FFloat" = FArith ATFloat

477 mkIty "FInt" = mkIntIty "ITNative"

478 mkIty "FInt" = mkIntIty "ITNative"

478 mkIty "FChar" = mkIntIty "ITChar"

479 mkIty "FChar" = mkIntIty "ITChar"

@@ -521,7 +522,7 @@ irSC vs (Case up n [ConCase (UN delay) i [_, _, n'] sc])

521 | delay == txt "Delay"

522 | delay == txt "Delay"

522 = do sc' <- irSC vs $ mkForce n' n sc

523 = do sc' <- irSC vs $ mkForce n' n sc

523 return $ LLet n' (LForce (LV (Glob n))) sc'

524 return $ LLet n' (LForce (LV (Glob n))) sc'

524−

525+

525-- There are two transformations in this case:

526-- There are two transformations in this case:

526--

527--

527-- 1. Newtype-case elimination:

528-- 1. Newtype-case elimination:

src/Idris/AbsSyntax.hs+53−45

@@ -114,12 +114,12 @@ addLangExt ErrorReflection = do i <- getIState

114-- Transforms are organised by the function being applied on the lhs of the

115-- transform, to make looking up appropriate transforms quicker

116addTrans :: Name -> (Term, Term) -> Idris ()

117−addTrans basefn t

117+addTrans basefn t

118 = do i <- getIState

119 let t' = case lookupCtxtExact basefn (idris_transforms i) of

120 Just def -> (t : def)

121 Nothing -> [t]

122− putIState $ i { idris_transforms = addDef basefn t'

122+ putIState $ i { idris_transforms = addDef basefn t'

123 (idris_transforms i) }

124

125addErrRev :: (Term, Term) -> Idris ()

@@ -130,8 +130,8 @@ totcheck :: (FC, Name) -> Idris ()

130totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }

131

132defer_totcheck :: (FC, Name) -> Idris ()

133−defer_totcheck n

133+defer_totcheck n

134− = do i <- getIState;

134+ = do i <- getIState;

135 putIState $ i { idris_defertotcheck = nub (idris_defertotcheck i ++ [n]) }

136

137clear_totcheck :: Idris ()

@@ -183,7 +183,7 @@ addToCG n cg

183 putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) }

184

185addTyInferred :: Name -> Idris ()

186−addTyInferred n

186+addTyInferred n

187 = do i <- getIState

188 putIState $ i { idris_tyinfodata =

189 addDef n TIPartial (idris_tyinfodata i) }

@@ -197,7 +197,7 @@ addTyInfConstraints fc ts = do logLvl 2 $ "TI missing: " ++ show ts

197 findMVApps x y

198 = do let (fx, argsx) = unApply x

199 let (fy, argsy) = unApply y

200− if (not (fx == fy))

200+ if (not (fx == fy))

201 then do

202 tryAddMV fx y

203 tryAddMV fy x

@@ -211,17 +211,17 @@ addTyInfConstraints fc ts = do logLvl 2 $ "TI missing: " ++ show ts

211 tryAddMV _ _ = return ()

212

213 addConstraintRule :: Name -> Term -> Idris ()

214− addConstraintRule n t

214+ addConstraintRule n t

215 = do ist <- get

216 logLvl 1 $ "TI constraint: " ++ show (n, t)

217 case lookupCtxt n (idris_tyinfodata ist) of

218− [TISolution ts] ->

218+ [TISolution ts] ->

219 do mapM_ (checkConsistent t) ts

220− let ti' = addDef n (TISolution (t : ts))

220+ let ti' = addDef n (TISolution (t : ts))

221 (idris_tyinfodata ist)

222 put $ ist { idris_tyinfodata = ti' }

223− _ ->

223+ _ ->

224− do let ti' = addDef n (TISolution [t])

224+ do let ti' = addDef n (TISolution [t])

225 (idris_tyinfodata ist)

226 put $ ist { idris_tyinfodata = ti' }

227

@@ -233,14 +233,14 @@ addTyInfConstraints fc ts = do logLvl 2 $ "TI missing: " ++ show ts

233 do let (fx, _) = unApply x

234 let (fy, _) = unApply y

235 case (fx, fy) of

236− (P (TCon _ _) n _, P (TCon _ _) n' _) -> errWhen (n/=n)

236+ (P (TCon _ _) n _, P (TCon _ _) n' _) -> errWhen (n/=n)

237 (P (TCon _ _) n _, Constant _) -> errWhen True

238 (Constant _, P (TCon _ _) n' _) -> errWhen True

239− (P (DCon _ _ _) n _, P (DCon _ _ _) n' _) -> errWhen (n/=n)

239+ (P (DCon _ _ _) n _, P (DCon _ _ _) n' _) -> errWhen (n/=n)

240 _ -> return ()

241

242− where errWhen True

242+ where errWhen True

243− = throwError (At fc

243+ = throwError (At fc

244 (CantUnify False x y (Msg "") [] 0))

245 errWhen False = return ()

246

@@ -310,6 +310,8 @@ getNameHints i n =

310 [ns] -> ns

311 _ -> []

312

313+-- Issue #1737 in the Issue Tracker.

314+-- https://github.com/idris-lang/Idris-dev/issues/1737

313addToCalledG :: Name -> [Name] -> Idris ()

315addToCalledG :: Name -> [Name] -> Idris ()

314addToCalledG n ns = return () -- TODO

316addToCalledG n ns = return () -- TODO

315

317

@@ -333,7 +335,7 @@ addInstance int n i

333 insI i (n : ns) | chaser n = i : n : ns

335 insI i (n : ns) | chaser n = i : n : ns

334 | otherwise = n : insI i ns

336 | otherwise = n : insI i ns

335

337

336− chaser (UN nm)

338+ chaser (UN nm)

337 | ('@':'@':_) <- str nm = True

339 | ('@':'@':_) <- str nm = True

338 chaser (NS n _) = chaser n

340 chaser (NS n _) = chaser n

339 chaser _ = False

341 chaser _ = False

@@ -421,6 +423,9 @@ withContext_ ctx name action = withContext ctx name () action

421runIO :: IO a -> Idris a

423runIO :: IO a -> Idris a

422runIO x = liftIO (tryIOError x) >>= either (throwError . Msg . show) return

424runIO x = liftIO (tryIOError x) >>= either (throwError . Msg . show) return

423-- TODO: create specific Idris exceptions for specific IO errors such as "openFile: does not exist"

425-- TODO: create specific Idris exceptions for specific IO errors such as "openFile: does not exist"

426+--

427+-- Issue #1738 on the issue tracker.

428+-- https://github.com/idris-lang/Idris-dev/issues/1738

424

429

425getName :: Idris Int

430getName :: Idris Int

426getName = do i <- getIState;

431getName = do i <- getIState;

@@ -454,9 +459,9 @@ clearOrigPats = do i <- get

454-- the .ibc, which is all we need after all the analysis is done)

459-- the .ibc, which is all we need after all the analysis is done)

455clearPTypes :: Idris ()

460clearPTypes :: Idris ()

456clearPTypes = do i <- get

461clearPTypes = do i <- get

457− let ctxt = tt_ctxt i

462+ let ctxt = tt_ctxt i

458 put (i { tt_ctxt = mapDefCtxt pErase ctxt })

463 put (i { tt_ctxt = mapDefCtxt pErase ctxt })

459− where pErase (CaseOp c t tys orig tot cds)

464+ where pErase (CaseOp c t tys orig tot cds)

460 = CaseOp c t tys orig [] (pErase' cds)

465 = CaseOp c t tys orig [] (pErase' cds)

461 pErase x = x

466 pErase x = x

462 pErase' (CaseDefs _ (cs, c) _ rs)

467 pErase' (CaseDefs _ (cs, c) _ rs)

@@ -503,7 +508,7 @@ addDeferred' nt ns

503 i <- getIState

508 i <- getIState

504 putIState $ i { idris_metavars = map (\(n, (i, top, _, isTopLevel)) -> (n, (top, i, isTopLevel))) ns ++

509 putIState $ i { idris_metavars = map (\(n, (i, top, _, isTopLevel)) -> (n, (top, i, isTopLevel))) ns ++

505 idris_metavars i }

510 idris_metavars i }

506− where

511+ where

507 -- 'tidyNames' is to generate user accessible names in case they are

512 -- 'tidyNames' is to generate user accessible names in case they are

508 -- needed in tactic scripts

513 -- needed in tactic scripts

509 tidyNames used (Bind (MN i x) b sc)

514 tidyNames used (Bind (MN i x) b sc)

@@ -1075,12 +1080,12 @@ addStatics :: Name -> Term -> PTerm -> Idris ()

1075addStatics n tm ptm =

1080addStatics n tm ptm =

1076 do let (statics, dynamics) = initStatics tm ptm

1081 do let (statics, dynamics) = initStatics tm ptm

1077 ist <- getIState

1082 ist <- getIState

1078− let paramnames

1083+ let paramnames

1079 = nub $ case lookupCtxtExact n (idris_fninfo ist) of

1084 = nub $ case lookupCtxtExact n (idris_fninfo ist) of

1080 Just p -> getNamesFrom 0 (fn_params p) tm ++

1085 Just p -> getNamesFrom 0 (fn_params p) tm ++

1081 concatMap (getParamNames ist) (map snd statics)

1086 concatMap (getParamNames ist) (map snd statics)

1082 _ -> concatMap (getParamNames ist) (map snd statics)

1087 _ -> concatMap (getParamNames ist) (map snd statics)

1083−

1088+

1084 let stnames = nub $ concatMap freeArgNames (map snd statics)

1089 let stnames = nub $ concatMap freeArgNames (map snd statics)

1085 let dnames = (nub $ concatMap freeArgNames (map snd dynamics))

1090 let dnames = (nub $ concatMap freeArgNames (map snd dynamics))

1086 \\ paramnames

1091 \\ paramnames

@@ -1106,7 +1111,7 @@ addStatics n tm ptm =

1106 initStatics (Bind n (Pi ty _) sc) (PPi p n' _ s)

1111 initStatics (Bind n (Pi ty _) sc) (PPi p n' _ s)

1107 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in

1112 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in

1108 if pstatic p == Static then ((n, ty) : static, dynamic)

1113 if pstatic p == Static then ((n, ty) : static, dynamic)

1109− else if (not (searchArg p))

1114+ else if (not (searchArg p))

1110 then (static, (n, ty) : dynamic)

1115 then (static, (n, ty) : dynamic)

1111 else (static, dynamic)

1116 else (static, dynamic)

1112 initStatics t pt = ([], [])

1117 initStatics t pt = ([], [])

@@ -1116,7 +1121,7 @@ addStatics n tm ptm =

1116 Just ti -> getNamePos 0 (param_pos ti) args

1121 Just ti -> getNamePos 0 (param_pos ti) args

1117 Nothing -> []

1122 Nothing -> []

1118 where getNamePos i ps [] = []

1123 where getNamePos i ps [] = []

1119− getNamePos i ps (P _ n _ : as)

1124+ getNamePos i ps (P _ n _ : as)

1120 | i `elem` ps = n : getNamePos (i + 1) ps as

1125 | i `elem` ps = n : getNamePos (i + 1) ps as

1121 getNamePos i ps (_ : as) = getNamePos (i + 1) ps as

1126 getNamePos i ps (_ : as) = getNamePos (i + 1) ps as

1122 getParamNames ist (Bind t (Pi (P _ n _) _) sc)

1127 getParamNames ist (Bind t (Pi (P _ n _) _) sc)

@@ -1128,7 +1133,7 @@ addStatics n tm ptm =

1128 | otherwise = getNamesFrom (i + 1) ps sc

1133 | otherwise = getNamesFrom (i + 1) ps sc

1129 getNamesFrom i ps sc = []

1134 getNamesFrom i ps sc = []

1130

1135

1131− freeArgNames (Bind n (Pi ty _) sc)

1136+ freeArgNames (Bind n (Pi ty _) sc)

1132 = nub $ freeNames ty ++ freeNames sc -- treat '->' as fn here

1137 = nub $ freeNames ty ++ freeNames sc -- treat '->' as fn here

1133 freeArgNames tm = let (_, args) = unApply tm in

1138 freeArgNames tm = let (_, args) = unApply tm in

1134 concatMap freeNames args

1139 concatMap freeNames args

@@ -1199,11 +1204,11 @@ addUsingImpls syn n fc t

1199 let ns = implicitNamesIn (map iname uimpls) ist t

1204 let ns = implicitNamesIn (map iname uimpls) ist t

1200 let badnames = filter (\n -> not (implicitable n) &&

1205 let badnames = filter (\n -> not (implicitable n) &&

1201 n `notElem` (map iname uimpls)) ns

1206 n `notElem` (map iname uimpls)) ns

1202− when (not (null badnames)) $

1207+ when (not (null badnames)) $

1203− throwError (At fc (Elaborating "type of " n

1208+ throwError (At fc (Elaborating "type of " n

1204 (NoSuchVariable (head badnames))))

1209 (NoSuchVariable (head badnames))))

1205− let cs = getArgnames t -- get already bound names

1210+ let cs = getArgnames t -- get already bound names

1206− let addimpls = filter (\n -> iname n `notElem` cs) uimpls

1211+ let addimpls = filter (\n -> iname n `notElem` cs) uimpls

1207 -- if all names in the arguments of addconsts appear in ns,

1212 -- if all names in the arguments of addconsts appear in ns,

1208 -- add the constraint implicitly

1213 -- add the constraint implicitly

1209 return (bindFree ns (doAdd addimpls ns t))

1214 return (bindFree ns (doAdd addimpls ns t))

@@ -1223,9 +1228,9 @@ addUsingImpls syn n fc t

1223

1228

1224 -- bind the free names which weren't in the using block

1229 -- bind the free names which weren't in the using block

1225 bindFree [] tm = tm

1230 bindFree [] tm = tm

1226− bindFree (n:ns) tm

1231+ bindFree (n:ns) tm

1227 | elem n (map iname uimpls) = bindFree ns tm

1232 | elem n (map iname uimpls) = bindFree ns tm

1228− | otherwise

1233+ | otherwise

1229 = PPi (Imp [] Dynamic False) n Placeholder (bindFree ns tm)

1234 = PPi (Imp [] Dynamic False) n Placeholder (bindFree ns tm)

1230

1235

1231 getArgnames (PPi _ n c sc)

1236 getArgnames (PPi _ n c sc)

@@ -1244,15 +1249,15 @@ getUnboundImplicits i t tm = getImps t (collectImps tm)

1244 getImps (Bind n (Pi t _) sc) imps

1249 getImps (Bind n (Pi t _) sc) imps

1245 | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps

1250 | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps

1246 where

1251 where

1247− argInfo n (Imp opt _ _) t'

1252+ argInfo n (Imp opt _ _) t'

1248 = (True, PImp (getPriority i t') True opt n t')

1253 = (True, PImp (getPriority i t') True opt n t')

1249 argInfo n (Exp opt _ _) t'

1254 argInfo n (Exp opt _ _) t'

1250 = (InaccessibleArg `elem` opt,

1255 = (InaccessibleArg `elem` opt,

1251 PExp (getPriority i t') opt n t')

1256 PExp (getPriority i t') opt n t')

1252− argInfo n (Constraint opt _) t'

1257+ argInfo n (Constraint opt _) t'

1253 = (InaccessibleArg `elem` opt,

1258 = (InaccessibleArg `elem` opt,

1254 PConstraint 10 opt n t')

1259 PConstraint 10 opt n t')

1255− argInfo n (TacImp opt _ scr) t'

1260+ argInfo n (TacImp opt _ scr) t'

1256 = (InaccessibleArg `elem` opt,

1261 = (InaccessibleArg `elem` opt,

1257 PTacImplicit 10 opt n scr t')

1262 PTacImplicit 10 opt n scr t')

1258 getImps (Bind n (Pi t _) sc) imps = impBind n t : getImps sc imps

1263 getImps (Bind n (Pi t _) sc) imps = impBind n t : getImps sc imps

@@ -1265,6 +1270,9 @@ getUnboundImplicits i t tm = getImps t (collectImps tm)

1265-- This has become a right mess already. Better redo it some time...

1270-- This has become a right mess already. Better redo it some time...

1266-- TODO: This is obsoleted by the new way of elaborating types, but there's still

1271-- TODO: This is obsoleted by the new way of elaborating types, but there's still

1267-- a couple of places which use it. Clean them up!

1272-- a couple of places which use it. Clean them up!

1273+--

1274+-- Issue 1739 in the issue tracker

1275+-- https://github.com/idris-lang/Idris-dev/issues/1739

1268implicit :: ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm

1276implicit :: ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm

1269implicit info syn n ptm = implicit' info syn [] n ptm

1277implicit info syn n ptm = implicit' info syn [] n ptm

1270

1278

@@ -1283,11 +1291,11 @@ implicit' info syn ignore n ptm

1283 where

1291 where

1284 -- Detect unknown names in default arguments and throw error if found.

1292 -- Detect unknown names in default arguments and throw error if found.

1285 defaultArgCheck :: [Name] -> [PArg] -> Idris ()

1293 defaultArgCheck :: [Name] -> [PArg] -> Idris ()

1286− defaultArgCheck knowns params = foldM_ notFoundInDefault knowns params

1294+ defaultArgCheck knowns params = foldM_ notFoundInDefault knowns params

1287

1295

1288 notFoundInDefault :: [Name] -> PArg -> Idris [Name]

1296 notFoundInDefault :: [Name] -> PArg -> Idris [Name]

1289 notFoundInDefault kns (PTacImplicit _ _ n script _)

1297 notFoundInDefault kns (PTacImplicit _ _ n script _)

1290− = do i <- getIState

1298+ = do i <- getIState

1291 case notFound kns (namesIn [] i script) of

1299 case notFound kns (namesIn [] i script) of

1292 Nothing -> return (n:kns)

1300 Nothing -> return (n:kns)

1293 Just name -> throwError (NoSuchVariable name)

1301 Just name -> throwError (NoSuchVariable name)

@@ -1545,7 +1553,7 @@ aiFn inpat expat qq ist fc f ds as

1545 let nh = filter (\(n, _) -> notHidden n) ns

1553 let nh = filter (\(n, _) -> notHidden n) ns

1546 let ns' = case trimAlts ds nh of

1554 let ns' = case trimAlts ds nh of

1547 [] -> nh

1555 [] -> nh

1548− x -> x

1556+ x -> x

1549 case ns' of

1557 case ns' of

1550 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)

1558 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)

1551 [] -> if f `elem` (map fst (idris_metavars ist))

1559 [] -> if f `elem` (map fst (idris_metavars ist))

@@ -1557,7 +1565,7 @@ aiFn inpat expat qq ist fc f ds as

1557 (insertImpl ns as)) alts

1565 (insertImpl ns as)) alts

1558 where

1566 where

1559 trimAlts [] alts = alts

1567 trimAlts [] alts = alts

1560− trimAlts ns alts

1568+ trimAlts ns alts

1561 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts

1569 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts

1562

1570

1563 nspace (NS _ s) = s

1571 nspace (NS _ s) = s

@@ -1612,6 +1620,8 @@ aiFn inpat expat qq ist fc f ds as

1612 insImpAcc (M.insert n sc pnas) ps given imps

1620 insImpAcc (M.insert n sc pnas) ps given imps

1613 insImpAcc _ expected [] imps = imps -- so that unused implicits give error

1621 insImpAcc _ expected [] imps = imps -- so that unused implicits give error

1614 -- TODO: report here, and prune alternatives

1622 -- TODO: report here, and prune alternatives

1623+ -- Issue #1740 in the Issue Tracker

1624+-- https://github.com/idris-lang/Idris-dev/issues/1740

1615 insImpAcc _ _ given imps = given ++ imps

1625 insImpAcc _ _ given imps = given ++ imps

1616

1626

1617 find n [] acc = Nothing

1627 find n [] acc = Nothing

@@ -1644,7 +1654,7 @@ stripLinear i tm = evalState (sl tm) [] where

1644 return (PPatvar fc f)

1654 return (PPatvar fc f)

1645 sl t@(PAlternative _ (a : as)) = do sl a

1655 sl t@(PAlternative _ (a : as)) = do sl a

1646 return t

1656 return t

1647− sl (PApp fc fn args) = do -- Just the args, fn isn't matchable as a var

1657+ sl (PApp fc fn args) = do -- Just the args, fn isn't matchable as a var

1648 args' <- mapM slA args

1658 args' <- mapM slA args

1649 return $ PApp fc fn args'

1659 return $ PApp fc fn args'

1650 where slA (PImp p m l n t) = do t' <- sl t

1660 where slA (PImp p m l n t) = do t' <- sl t

@@ -1667,11 +1677,11 @@ stripUnmatchable :: IState -> PTerm -> PTerm

1667stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where

1677stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where

1668 su :: PTerm -> PTerm

1678 su :: PTerm -> PTerm

1669 su (PRef fc f)

1679 su (PRef fc f)

1670− | (Bind n (Pi t _) sc :_) <- lookupTy f (tt_ctxt i)

1680+ | (Bind n (Pi t _) sc :_) <- lookupTy f (tt_ctxt i)

1671 = Placeholder

1681 = Placeholder

1672− su (PApp fc fn args)

1682+ su (PApp fc fn args)

1673 = PApp fc fn (fmap (fmap su) args)

1683 = PApp fc fn (fmap (fmap su) args)

1674− su (PAlternative b alts)

1684+ su (PAlternative b alts)

1675 = let alts' = filter (/= Placeholder) (map su alts) in

1685 = let alts' = filter (/= Placeholder) (map su alts) in

1676 if null alts' then Placeholder

1686 if null alts' then Placeholder

1677 else PAlternative b alts'

1687 else PAlternative b alts'

@@ -1766,7 +1776,7 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where

1766 match (PApp _ x []) (PRef f n) = match x (PRef f n)

1776 match (PApp _ x []) (PRef f n) = match x (PRef f n)

1767 match (PRef _ n) tm@(PRef _ n')

1777 match (PRef _ n) tm@(PRef _ n')

1768 | n == n' && not names &&

1778 | n == n' && not names &&

1769− (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))

1779+ (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))

1770 || tm == Placeholder)

1780 || tm == Placeholder)

1771 = return [(n, tm)]

1781 = return [(n, tm)]

1772 -- if one namespace is missing, drop the other

1782 -- if one namespace is missing, drop the other

@@ -1777,7 +1787,7 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where

1777 | not names && (not (isConName n (tt_ctxt i) ||

1787 | not names && (not (isConName n (tt_ctxt i) ||

1778 isFnName n (tt_ctxt i)) || tm == Placeholder)

1788 isFnName n (tt_ctxt i)) || tm == Placeholder)

1779 = return [(n, tm)]

1789 = return [(n, tm)]

1780− match (PEq _ _ _ l r) (PEq _ _ _ l' r')

1790+ match (PEq _ _ _ l r) (PEq _ _ _ l' r')

1781 = do ml <- match' l l'

1791 = do ml <- match' l l'

1782 mr <- match' r r'

1792 mr <- match' r r'

1783 return (ml ++ mr)

1793 return (ml ++ mr)

@@ -2002,5 +2012,3 @@ mkUniqueNames env tm = evalState (mkUniq tm) (S.fromList env) where

2002 mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)

2012 mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)

2003 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)

2013 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)

2004 mkUniq t = return t

2014 mkUniq t = return t

2005−

2006−

src/Idris/Coverage.hs+14−14

@@ -72,7 +72,7 @@ genClauses fc n xs given

72 -- there may be more case splitting that the idris_implicits record

73 -- suggests)

74 let parg = case lookupCtxt n (idris_implicits i) of

75− (p : _) ->

75+ (p : _) ->

76 p ++ repeat (PExp 0 [] (sMN 0 "gcarg") Placeholder)

77 _ -> repeat (pexp Placeholder)

78 let tryclauses = mkClauses parg all_args

@@ -122,7 +122,8 @@ genClauses fc n xs given

122

123-- FIXME: Just look for which one is the deepest, then generate all

124-- possibilities up to that depth.

125−

125+-- This and below issues for this function are tracked as Issue #1741 on the issue tracker.

126+-- https://github.com/idris-lang/Idris-dev/issues/1741

126genAll :: IState -> [PTerm] -> [PTerm]

127genAll :: IState -> [PTerm] -> [PTerm]

127genAll i args

128genAll i args

128 = case filter (/=Placeholder) $ fnub (concatMap otherPats (fnub args)) of

129 = case filter (/=Placeholder) $ fnub (concatMap otherPats (fnub args)) of

@@ -264,13 +265,13 @@ checkAllCovering fc done top n | not (n `elem` done)

264 addIBC (IBCTotCheckErr fc msg)

265 addIBC (IBCTotCheckErr fc msg)

265 [Partial _] ->

266 [Partial _] ->

266 case lookupCtxt n (idris_callgraph i) of

267 case lookupCtxt n (idris_callgraph i) of

267− [cg] -> mapM_ (checkAllCovering fc (n : done) top)

268+ [cg] -> mapM_ (checkAllCovering fc (n : done) top)

268 (map fst (calls cg))

269 (map fst (calls cg))

269 _ -> return ()

270 _ -> return ()

270 x -> return () -- stop if total

271 x -> return () -- stop if total

271checkAllCovering _ _ _ _ = return ()

272checkAllCovering _ _ _ _ = return ()

272

273

273−-- Check if, in a given group of type declarations mut_ns,

274+-- Check if, in a given group of type declarations mut_ns,

274-- the constructor cn : ty is strictly positive,

275-- the constructor cn : ty is strictly positive,

275-- and update the context accordingly

276-- and update the context accordingly

276

277

@@ -290,7 +291,7 @@ checkPositive mut_ns (cn, ty')

290

291

291 cp (Bind n (Pi aty _) sc) = posArg aty && cp sc

292 cp (Bind n (Pi aty _) sc) = posArg aty && cp sc

292 cp t | (P _ n' _, args) <- unApply t,

293 cp t | (P _ n' _, args) <- unApply t,

293− n' `elem` mut_ns = all noRec args

294+ n' `elem` mut_ns = all noRec args

294 cp _ = True

295 cp _ = True

295

296

296 posArg (Bind _ (Pi nty _) sc)

297 posArg (Bind _ (Pi nty _) sc)

@@ -439,7 +440,7 @@ checkDeclTotality (fc, n)

439 i <- getIState

440 i <- getIState

440 let opts = case lookupCtxt n (idris_flags i) of

441 let opts = case lookupCtxt n (idris_flags i) of

441 [fs] -> fs

442 [fs] -> fs

442− _ -> []

443+ _ -> []

443 when (CoveringFn `elem` opts) $ checkAllCovering fc [] n n

444 when (CoveringFn `elem` opts) $ checkAllCovering fc [] n n

444 t <- checkTotality [] fc n

445 t <- checkTotality [] fc n

445 case t of

446 case t of

@@ -507,11 +508,11 @@ buildSCG' ist pats args = nub $ concatMap scgPat pats where

507 | (P _ (UN at) _, [_, _]) <- unApply ap,

508 | (P _ (UN at) _, [_, _]) <- unApply ap,

508 at == txt "assert_total" = []

509 at == txt "assert_total" = []

509 -- under a call to "Delay LazyCodata", don't do any checking of the

510 -- under a call to "Delay LazyCodata", don't do any checking of the

510− -- immediate call, as long as the call is guarded.

511+ -- immediate call, as long as the call is guarded.

511 -- Then check its arguments

512 -- Then check its arguments

512 | (P _ (UN del) _, [_,_,arg]) <- unApply ap,

513 | (P _ (UN del) _, [_,_,arg]) <- unApply ap,

513 Guarded <- guarded,

514 Guarded <- guarded,

514− del == txt "Delay"

515+ del == txt "Delay"

515 = let (capp, args) = unApply arg in

516 = let (capp, args) = unApply arg in

516 concatMap (\x -> findCalls guarded x pvs pargs) args

517 concatMap (\x -> findCalls guarded x pvs pargs) args

517 | (P _ n _, args) <- unApply ap

518 | (P _ n _, args) <- unApply ap

@@ -532,7 +533,7 @@ buildSCG' ist pats args = nub $ concatMap scgPat pats where

532 | not (f `elem` pvs) = [(f, [])]

533 | not (f `elem` pvs) = [(f, [])]

533 findCalls _ _ _ _ = []

534 findCalls _ _ _ _ = []

534

535

535− expandToArity n args

536+ expandToArity n args

536 = case lookupTy n (tt_ctxt ist) of

537 = case lookupTy n (tt_ctxt ist) of

537 [ty] -> expand 0 (normalise (tt_ctxt ist) [] ty) args

538 [ty] -> expand 0 (normalise (tt_ctxt ist) [] ty) args

538 _ -> args

539 _ -> args

@@ -609,7 +610,7 @@ checkSizeChange n = do

609 return (noPartial tot)

610 return (noPartial tot)

610 [] -> do logLvl 5 $ "No paths for " ++ show n

611 [] -> do logLvl 5 $ "No paths for " ++ show n

611 return Unchecked

612 return Unchecked

612− where getArity ist n

613+ where getArity ist n

613 = case lookupTy n (tt_ctxt ist) of

614 = case lookupTy n (tt_ctxt ist) of

614 [ty] -> arity (normalise (tt_ctxt ist) [] ty)

615 [ty] -> arity (normalise (tt_ctxt ist) [] ty)

615 _ -> error "Can't happen: checkSizeChange.getArity"

616 _ -> error "Can't happen: checkSizeChange.getArity"

@@ -674,14 +675,14 @@ checkMP ist i mp = if i > 0

674 Total []

675 Total []

675 else Partial (Mutual (map (fst . fst . fst) path ++ [f]))

676 else Partial (Mutual (map (fst . fst . fst) path ++ [f]))

676 | e `elem` map (fst . fst) path

677 | e `elem` map (fst . fst) path

677− && not (f `elem` map fst es)

678+ && not (f `elem` map fst es)

678 = Partial (Mutual (map (fst . fst . fst) path ++ [f]))

679 = Partial (Mutual (map (fst . fst . fst) path ++ [f]))

679 | [Unchecked] <- lookupTotal f (tt_ctxt ist) =

680 | [Unchecked] <- lookupTotal f (tt_ctxt ist) =

680 let argspos = case collapseNothing (zip nextargs [0..]) of

681 let argspos = case collapseNothing (zip nextargs [0..]) of

681 [] -> [(Nothing, 0)]

682 [] -> [(Nothing, 0)]

682 x -> x

683 x -> x

683-- trace (show (argspos, nextargs, path)) $

684-- trace (show (argspos, nextargs, path)) $

684− pathres =

685+ pathres =

685 do (a, pos) <- argspos

686 do (a, pos) <- argspos

686 case a of

687 case a of

687 Nothing -> -- don't know, but if the

688 Nothing -> -- don't know, but if the

@@ -704,7 +705,7 @@ checkMP ist i mp = if i > 0

704 _ -> trace ("Shouldn't happen " ++ show e) $

705 _ -> trace ("Shouldn't happen " ++ show e) $

705 return (Partial Itself)

706 return (Partial Itself)

706 else return Unchecked in

707 else return Unchecked in

707−-- trace (show (desc, argspos, path, es, pathres)) $

708+-- trace (show (desc, argspos, path, es, pathres)) $

708 collapse' Unchecked pathres

709 collapse' Unchecked pathres

709

710

710 | [Total a] <- lookupTotal f (tt_ctxt ist) = Total a

711 | [Total a] <- lookupTotal f (tt_ctxt ist) = Total a

@@ -734,4 +735,3 @@ collapse' def (Unchecked : xs) = collapse' def xs

734collapse' def (d : xs) = collapse' d xs

735collapse' def (d : xs) = collapse' d xs

735-- collapse' Unchecked [] = Total []

736-- collapse' Unchecked [] = Total []

736collapse' def [] = def

737collapse' def [] = def

737−