Идрис - стирание индексов не удается - PullRequest
Новая
       51

Идрис - стирание индексов не удается

0 голосов
/ 11 октября 2018

В настоящее время я пытаюсь стереть все неиспользуемые индексы из моей программы Idris - однако в одном случае компилятор Idris считает индексы достижимыми.Я попытался воспроизвести поведение в следующем минимальном примере: 

module Main

%access public export

-- CUSTOM VECTOR TYPES
data VectA : Nat -> Type -> Type where
    VNilA  : VectA Z a
    VConsA : a -> VectA len a -> VectA (S len) a

data VectB : Nat -> Type -> Type where
    VNilB  : VectB Z a
    VConsB : a -> VectB len a -> VectB (S len) a

-- THE FOLLOWING FUNCTIONS ARE USED TO CREATE A
-- CUSTOM VECTOR WHERE THE SIZE IS UNKNOWN
fromList : (l : List a) -> VectA (length l) a
fromList []      = VNilA
fromList (x::xs) = VConsA x (fromList xs)

createList : String -> List Int
createList "42" = [42, 42, 42]
createList _    = [1, 2, 3, 4]

-- SOME NESTED TRANSFORMATION FUNCTIONS ON VECT
transformVectA : VectA n a -> Maybe (VectB n a)
transformVectA VNilA         = Just VNilB
transformVectA (VConsA v vs) = 
    case transformVectA vs of
       Just vs' => Just $ VConsB v vs'
       Nothing  => Nothing

transformVectB : VectA m a -> VectB n a -> Maybe (VectB n a)
transformVectB VNilA ws = Just ws
transformVectB (VConsA v vs) ws = transformVectB vs ws 

transformVect : VectA n a -> VectA m a -> Maybe (VectB n a)
transformVect VNilA         VNilB = Nothing
transformVect VNilA         VNilA = Nothing
transformVect vs            VNilA = Nothing
transformVect (VConsA v vs) xs    = 
    case transformVectA (VConsA v vs) of
        Nothing  => Nothing
        Just vs' => transformVectB xs vs'

main : IO ()
main = do
    (testArg :: _) <- getArgs
    ls <- pure $ createList testArg
    va <- pure $ fromList ls
    vb <- pure $ transformVect va va

    putStrLn "OK"

Когда это скомпилировано с помощью команды:

idris Erasure.idr -o Erasure --warnreach

... отображаются следующие предупреждения: 

Main.transformVect: inaccessible arguments reachable:
n (no more information available)
m (no more information available)

У меня также возникают проблемы при чтении дамп-регистров при компиляции с дополнительной опцией:

- дамп-кейсыcase.txt

Почему появляются эти предупреждения?Есть ли какая-либо информация о том, как Idris обрабатывает удаление, кроме главы «Анализ с помощью стирания» в Учебном пособии?

...