d417e41 · Idris-dev · git.iko.soy

41deriving instance NFData SC'

42!-}

43

44−data CaseType = Updatable | Shared

44+data CaseType = Updatable | Shared

45 deriving (Eq, Ord, Show)

46

47type SC = SC' Term

184 fce == txt "Force"

185 = directUse a -- forcing a value counts as a use

186 | (P Ref n _, args) <- unApply fn = [] -- need to know what n does with them

187− | (P (TCon _ _) n _, args) <- unApply fn = [] -- type constructors not used at runtime

187+ | (P (TCon _ _) n _, args) <- unApply fn = [] -- type constructors not used at runtime

188 | otherwise = nub $ directUse f ++ directUse a

189directUse (Proj x i) = nub $ directUse x

190directUse _ = []

258 ns = take numargs args

259 (ns', ps') = order [(n, i `elem` inacc) | (i,n) <- zip [0..] ns] pats

260 (tree, st) = runCaseBuilder erInfo

261− (match ns' ps' (defaultCase cover))

261+ (match ns' ps' (defaultCase cover))

262 ([], numargs, [])

263 t = CaseDef ns (prune proj (depatt ns' tree)) (fstT st) in

264− if proj then return (stripLambdas t)

264+ if proj then return (stripLambdas t)

265 else return t

266-- FIXME: This check is not quite right in some cases, and is breaking

267-- perfectly valid code!

268+--

269+-- Issue #1717 on the issue tracker: https://github.com/idris-lang/Idris-dev/issues/1717

268-- if checkSameTypes (lstT st) tree

270-- if checkSameTypes (lstT st) tree

269-- then return t

271-- then return t

270-- else Error (At fc (Msg "Typecase is not allowed"))

272-- else Error (At fc (Msg "Typecase is not allowed"))

311-- FIXME: All we're actually doing here is checking that we haven't arrived

313-- FIXME: All we're actually doing here is checking that we haven't arrived

312-- at a specific constructor for a polymorphic argument. I *think* this

314-- at a specific constructor for a polymorphic argument. I *think* this

313-- is sufficient, but if it turns out not to be, fix it!

315-- is sufficient, but if it turns out not to be, fix it!

316+--

317+-- Issue #1718 on the issue tracker: https://github.com/idris-lang/Idris-dev/issues/1718

314isType n t | (P (TCon _ _) _ _, _) <- unApply t = True

318isType n t | (P (TCon _ _) _ _, _) <- unApply t = True

315isType n t | (P Ref _ _, _) <- unApply t = True

319isType n t | (P Ref _ _, _) <- unApply t = True

316isType n t = False

320isType n t = False

317

321

318−isConstType (I _) (AType (ATInt ITNative)) = True

322+isConstType (I _) (AType (ATInt ITNative)) = True

319−isConstType (BI _) (AType (ATInt ITBig)) = True

323+isConstType (BI _) (AType (ATInt ITBig)) = True

320−isConstType (Fl _) (AType ATFloat) = True

324+isConstType (Fl _) (AType ATFloat) = True

321−isConstType (Ch _) (AType (ATInt ITChar)) = True

325+isConstType (Ch _) (AType (ATInt ITChar)) = True

322−isConstType (Str _) StrType = True

326+isConstType (Str _) StrType = True

323−isConstType (B8 _) (AType (ATInt _)) = True

327+isConstType (B8 _) (AType (ATInt _)) = True

324−isConstType (B16 _) (AType (ATInt _)) = True

328+isConstType (B16 _) (AType (ATInt _)) = True

325−isConstType (B32 _) (AType (ATInt _)) = True

329+isConstType (B32 _) (AType (ATInt _)) = True

326−isConstType (B64 _) (AType (ATInt _)) = True

330+isConstType (B64 _) (AType (ATInt _)) = True

327−isConstType (B8V _) (AType (ATInt _)) = True

331+isConstType (B8V _) (AType (ATInt _)) = True

328−isConstType (B16V _) (AType (ATInt _)) = True

332+isConstType (B16V _) (AType (ATInt _)) = True

329−isConstType (B32V _) (AType (ATInt _)) = True

333+isConstType (B32V _) (AType (ATInt _)) = True

330−isConstType (B64V _) (AType (ATInt _)) = True

334+isConstType (B64V _) (AType (ATInt _)) = True

331isConstType _ _ = False

335isConstType _ _ = False

332

336

333data Pat = PCon Bool Name Int [Pat]

337data Pat = PCon Bool Name Int [Pat]

430 -- constructor tags between families, and no constructor/constant

434 -- constructor tags between families, and no constructor/constant

431 -- clash, because otherwise we can't reliable make the

435 -- clash, because otherwise we can't reliable make the

432 -- case distinction on evaluation

436 -- case distinction on evaluation

433− (patnames_ord, patnames_rest)

437+ (patnames_ord, patnames_rest)

434 = Data.List.partition (noClash . map snd) patnames

438 = Data.List.partition (noClash . map snd) patnames

435 -- note: sortBy . reverse is not nonsense because sortBy is stable

439 -- note: sortBy . reverse is not nonsense because sortBy is stable

436− pats' = transpose (sortBy moreDistinct (reverse patnames_ord)

440+ pats' = transpose (sortBy moreDistinct (reverse patnames_ord)

437 ++ patnames_rest) in

441 ++ patnames_rest) in

438 (getNOrder pats', zipWith rebuild pats' cs)

442 (getNOrder pats', zipWith rebuild pats' cs)

439 where

443 where

523 altGroups (ConGroup _ (CConst c) args : cs)

527 altGroups (ConGroup _ (CConst c) args : cs)

524 = (:) <$> altConstGroup c args <*> altGroups cs

528 = (:) <$> altConstGroup c args <*> altGroups cs

525

529

526− altGroup n i args

530+ altGroup n i args

527 = do inacc <- inaccessibleArgs n

531 = do inacc <- inaccessibleArgs n

528 (newVars, accVars, inaccVars, nextCs) <- argsToAlt inacc args

532 (newVars, accVars, inaccVars, nextCs) <- argsToAlt inacc args

529 matchCs <- match (accVars ++ vs ++ inaccVars) nextCs err

533 matchCs <- match (accVars ++ vs ++ inaccVars) nextCs err

556 -- Create names for new variables arising from the given patterns.

560 -- Create names for new variables arising from the given patterns.

557 getNewVars :: [Pat] -> CaseBuilder [Name]

561 getNewVars :: [Pat] -> CaseBuilder [Name]

558 getNewVars [] = return []

562 getNewVars [] = return []

559− getNewVars ((PV n t) : ns) = do v <- getVar "e"

563+ getNewVars ((PV n t) : ns) = do v <- getVar "e"

560 nsv <- getNewVars ns

564 nsv <- getNewVars ns

561

565

562 -- Record the type of the variable.

566 -- Record the type of the variable.

666 applyMaps ms t = t

670 applyMaps ms t = t

667

671

668-- FIXME: Do this for SucCase too

672-- FIXME: Do this for SucCase too

673+-- Issue #1719 on the issue tracker: https://github.com/idris-lang/Idris-dev/issues/1719

669prune :: Bool -- ^ Convert single branches to projections (only useful at runtime)

674prune :: Bool -- ^ Convert single branches to projections (only useful at runtime)

670 -> SC -> SC

675 -> SC -> SC

671prune proj (Case up n alts) = case alts' of

676prune proj (Case up n alts) = case alts' of

689 -- with sc

694 -- with sc

690 as@[ConCase cn i args sc]

695 as@[ConCase cn i args sc]

691 | proj -> let sc' = prune proj sc in

696 | proj -> let sc' = prune proj sc in

692− if any (isUsed sc') args

697+ if any (isUsed sc') args

693 then Case up n [ConCase cn i args sc']

698 then Case up n [ConCase cn i args sc']

694− else sc'

699+ else sc'

695

700

696 [SucCase cn sc]

701 [SucCase cn sc]

697 | proj

702 | proj

795 = DefaultCase (mkForceSC n arg rhs)

800 = DefaultCase (mkForceSC n arg rhs)

796

801

797 forceTm n arg t = subst n arg t

802 forceTm n arg t = subst n arg t

798−