Объявить взаимно рекурсивные типы

Question

У меня есть следующие два типа, которые являются взаимно рекурсивными (они имеют указатели, указывающие друг на друга):

vtypedef SimpleTextOutputInterface =
   @{ reset = EfiTextReset
    , output_string = [l:addr] (EfiTextString@l | ptr l)
    }

vtypedef EfiTextString = [n:nat][l1,l2:addr] (SimpleTextOutputInterface@l1, @[uint16][n]@l2 | ptr l1, ptr l2) -> uint64

Я попытался объявить абстрактный тип, как это:

absvt@ype SimpleTextOutputInterface

vtypedef EfiTextString = [n:nat][l1,l2:addr] (SimpleTextOutputInterface@l1, @[uint16][n]@l2 | ptr l1, ptr l2) -> uint64

assume SimpleTextOutputInterface =
   @{ reset = EfiTextReset
    , output_string = [l:addr] (EfiTextString@l | ptr l)
    }

Но у меня возникают ошибки типа, когда я пытаюсь их использовать (как будто где-то теряется вид).

Есть ли способ заставить это работать?Может быть, с предварительной декларацией, если она существует в ATS?

Answer 1

Мой "стандартный" подход заключается во введении фиктивной функции и некоторых связанных с ней функций доказательства:

abst@ype SimpleTextOutputInterface_

prfun encode :
{l:addr} SimpleTextOutputInterface @l -> SimpleTextOutputInterface_@l
prfun decode :
{l:addr} SimpleTextOutputInterface_@l -> SimpleTextOutputInterface @l