В прелюдии имеем:
Smaller x y = size x `LT` size y
instance Sized (List a) where size = length
sizeAccessible : Sized a => (x : a) -> Accessible Smaller x
accRec : (step : (x : a) -> ((y : a) -> rel y x -> b) -> b) ->
(z : a) -> Accessible rel z -> b
accRec
позволяет вам использовать «нестандартные шаблоны рекурсии» таким образом, что компилятор может понимать как total
. Это в основном fix : ((a -> b) -> (a -> b)) -> (a -> b)
, за исключением того, что открытая рекурсивная функция обязана передавать дополнительный термин доказательства, чтобы доказать, что рекурсивный аргумент как-то "меньше" Аргумент Accessible
определяет то, что используется шаблон рекурсии; здесь это простой «уменьшающийся Nat
размер» паттен. Предпочтительно, мы бы использовали sizeRec
вместо accRec
+ sizeAccessible
, но я не могу заставить его работать. Не стесняйтесь редактировать это «правильным» способом.
На каждой итерации вашей функции вы можете удалить имя, если найдете его.
delFirst : DecEq a => (x : a) -> (xs : List a)
-> Maybe (ys : List a ** length xs = S (length ys))
delFirst _ [] = Nothing
delFirst x (y :: xs) with (decEq x y)
delFirst x (x :: xs) | Yes Refl = Just (xs ** Refl)
delFirst x (y :: xs) | No _ with (delFirst x xs)
| Nothing = Nothing
| Just (ys ** prf) = Just (x :: ys ** cong prf)
Теперь вы можете использовать открытую, обоснованную рекурсию в pickName
:
pickName : String -> Ctx -> (String, Ctx)
pickName s ctx = let new = go s (bindings ctx) Z
in (new, addCtx new ctx)
where mkName : Nat -> String -> String
mkName Z name = name
mkName n name = name ++ show n
ltFromRefl : n = S m -> LT m n
ltFromRefl Refl = lteRefl
go : String -> List String -> Nat -> String
go name binds = accRec (\binds, rec, n =>
let name' = mkName n name
in case delFirst name' binds of
Nothing => name'
Just (binds' ** prf) => rec binds' (ltFromRefl prf) (S n)
) binds (sizeAccessible binds)
A Nat -> a
- это то же самое, что и Stream a
, поэтому, IMO, это несколько лучше:
findNew : DecEq a => (olds : List a) -> (news : Stream a) -> a
findNew olds = accRec (\olds, rec, (new :: news) =>
case delFirst new olds of
Nothing => new
Just (olds' ** prf) => rec olds' (ltFromRefl prf) news
) olds (sizeAccessible olds)
where ltFromRefl : n = S m -> LT m n
ltFromRefl Refl = lteRefl
pickName : String -> Ctx -> (String, Ctx)
pickName name ctx = let new = findNew (bindings ctx)
(name :: map ((name ++) . show) (iterate S 1))
in (new, addCtx new ctx)
Что, я думаю, отражает интуицию, лежащую в основе идеи, что если у вас есть бесконечный запас имен, но есть только конечное число старых, у вас наверняка будет бесконечно много новых.
(Кроме того, логика в вашем коде кажется неправильной. Вы перевернули ветви if
?)