Declare mutually recursive types

Question

I have the following two types that are mutually recursive (they have pointers pointing to each other):

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

I tried declaring an abstract type, like this:

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)
    }

But I have type errors when I try to use them (as though an at-view is lost somewhere).

Is there a way to make this work? Maybe with a forward declaration if that exists in ATS?

Answer 1

My "standard" approach is to introduce a dummy and some related proof functions:

abst@ype SimpleTextOutputInterface_

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