@@ -333,16 +333,6 @@ checkTotality path fc n
333333 setTotality n t'
334334 addIBC (IBCTotal n t')
335335 return t'
336− -- if it's not total, it can't reduce, to keep
337− -- typechecking decidable
338−-- case t' of
339−-- p@(Partial _) ->
340−-- do setAccessibility n Frozen
341−-- addIBC (IBCAccess n Frozen)
342−-- logLvl 5 $ "HIDDEN: "
343−-- ++ show n ++ show p
344−-- _ -> return ()
345−-- return t'
346336 _ -> return $ Total []
347337 x -> return x
348338 case t' of
@@ -498,103 +488,12 @@ buildSCG' ist pats args = nub $ concatMap scgPat pats where
498488 nty == nty' && not co
499489 isInductive _ _ = False
500490
501−-- getTypeFam t | (P _ n _, _) <- unApply t
502−
503491 dePat (Bind x (PVar ty) sc) = dePat (instantiate (P Bound x ty) sc)
504492 dePat t = t
505493
506494 patvars (Bind x (PVar _) sc) = x : patvars sc
507495 patvars _ = []
508496
509−{-
510−buildSCG' :: IState -> SC -> [Name] -> [SCGEntry]
511−buildSCG' ist sc args = -- trace ("Building SCG for " ++ show sc) $
512− nub $ scg sc (zip args args)
513− (zip args (zip args (repeat Same)))
514− where
515− scg :: SC -> [(Name, Name)] -> -- local var, originating top level var
516− [(Name, (Name, SizeChange))] -> -- orig to new, and relationship
517− [SCGEntry]
518− scg (Case x alts) vars szs
519− = let x' = findTL x vars in
520− concatMap (scgAlt x' vars szs) alts
521− where
522− findTL x vars
523− | Just x' <- lookup x vars
524− = if x' `elem` args then x'
525− else findTL x' vars
526− | otherwise = x
527−
528− scg (STerm tm) vars szs = scgTerm tm vars szs
529− scg _ _ _ = []
530−
531− -- how the arguments relate - either Smaller or Unknown
532− argRels :: Name -> [(Name, SizeChange)]
533− argRels n = let ctxt = tt_ctxt ist
534− [ty] = lookupTy n ctxt -- must exist!
535− P _ nty _ = fst (unApply (getRetTy ty))
536− co = case lookupCtxt nty (idris_datatypes ist) of
537− [TI _ x _ _] -> x
538− _ -> False
539− args = map snd (getArgTys ty) in
540− map (getRel co nty) (map (fst . unApply . getRetTy) args)
541− where
542− getRel True _ _ = (n, Unknown) -- coinductive
543− getRel _ ty (P _ n' _) | n' == ty = (n, Smaller)
544− getRel _ ty t = (n, Unknown)
545−
546− scgAlt x vars szs (ConCase n _ args sc)
547− -- all args smaller than top variable of x in sc
548− -- (as long as they are in the same type family, and it's
549− -- not coinductive)
550− | Just tvar <- lookup x vars
551− = let arel = argRels n
552− szs' = zipWith (\arg (_,t) -> (arg, (x, t))) args arel
553− ++ szs
554− vars' = nub (zip args (repeat tvar) ++ vars) in
555− scg sc vars' szs'
556− | otherwise = scg sc vars szs
557− scgAlt x vars szs (ConstCase _ sc) = scg sc vars szs
558− scgAlt x vars szs (DefaultCase sc) = scg sc vars szs
559−
560− scgTerm f@(App _ _) vars szs
561− | (P _ (UN "lazy") _, [_, arg]) <- unApply f
562− = scgTerm arg vars szs
563− | (P _ fn _, args) <- unApply f
564− = let rest = concatMap (\x -> scgTerm x vars szs) args in
565− case lookup fn vars of
566− Just _ -> rest
567− Nothing -> nub $ (fn, map (mkChange szs) args) : rest
568− scgTerm (App f a) vars szs
569− = scgTerm f vars szs ++ scgTerm a vars szs
570− scgTerm (Bind n (Let t v) e) vars szs
571− = scgTerm v vars szs ++ scgTerm e vars szs
572− scgTerm (Bind n _ e) vars szs
573− = scgTerm e (nub ((n, n) : vars)) szs
574− scgTerm (P _ fn _) vars szs
575− = case lookup fn vars of
576− Just _ -> []
577− Nothing -> [(fn, [])]
578− scgTerm _ _ _ = []
579−
580− mkChange :: [(Name, (Name, SizeChange))] -> Term
581− -> Maybe (Int, SizeChange)
582− mkChange szs tm
583− | (P _ (UN "lazy") _, [_, arg]) <- unApply tm = mkChange szs arg
584− | (P _ n ty, _) <- unApply tm -- get higher order args too
585− = do sc <- lookup n szs
586− case sc of
587− (_, Unknown) -> Nothing
588− (o, sc) -> do i <- getArgPos 0 o args
589− return (i, sc)
590− mkChange _ _ = Nothing
591−
592− getArgPos :: Int -> Name -> [Name] -> Maybe Int
593− getArgPos i n [] = Nothing
594− getArgPos i n (x : xs) | n == x = Just i
595− | otherwise = getArgPos (i + 1) n xs
596−-}
597−
598497checkSizeChange :: Name -> Idris Totality
599498checkSizeChange n = do
600499 ist <- getIState