How to do viewat-restoration?

[Shea Levy]

Hi all,

With the following code:

dataview partial_buf ( t: t@ype, fill: int, total: int, buf: addr ) =
| { t: t@ype }{ fill, total: nat | fill <= total }{ buf : addr }
partial_buf ( t
, fill
, total
, buf
) of ( @[ t ][ fill ] @ buf
, @[ t? ][ total - fill ] @ ( buf + fill )
)

implement main () = let
var buf = @[byte][10]()
prval empty = array_v_nil{byte}()
prval partial = partial_buf(empty, view@(buf))
prval partial_buf(empty, l) = partial
prval _ = array_v_unnil(empty)
prval _ = view@(buf) := l
in 0 end

I get this error:

/home/shlevy/src/elvysh-main/test2.dats: 593(line=17, offs=13) -- 608(line=17, offs=28): error(3): viewat-restoration cannot be performed: mismatch of bef/aft locations of atviews:
bef: [S2Evar(buf(3864))]
aft: [S2Eapp(S2Ecst(add_addr_int); S2Evar(buf$854(3872)), S2Evar(fill$852(3870)))]
patsopt(TRANS3): there are [1] errors in total.
exit(ATS): uncaught exception: _2home_2hwxi_2research_2Postiats_2git_2src_2pats_error_2esats__FatalErrorExn(1025)

How am I meant to do viewat-restoration?

Thanks,
Shea

[Hongwei Xi]

There are two issues here.

1. Syntax. The following declaration is what you want:

dataview partial_buf ( t: t@ype, int, int, addr ) =

  | { fill, total: nat | fill <= total }{ buf : addr }
      partial_buf ( t
                  , fill
                  , total
                  , buf
                  ) of ( @[ t ][ fill ] @ buf
                       , @[ t? ][ total - fill ] @ ( buf + fill )
                       )

If a parameter is given a name in a dataview declaration, then a universal

quantifier is implicitly introduced for that parameter. So your original declaration

has duplicated quantifiers.

2. Logic.

implement main () = let
  var buf = @[byte][10]()
  prval empty = array_v_nil{byte}()
  prval partial = partial_buf(empty, view@(buf))
  prval partial_buf(empty, l) = partial
  prval _ = array_v_unnil(empty)
  prval _ = view@(buf) := l
in 0 end

>>prval partial_buf(empty, l) = partial

The system does not know that 'empty' is a proof of an empty array-view;

it only knows that 'empty' is a prefix of the given buffer.

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/EC973B28-C1E1-441A-8771-7B60639DD046%40shealevy.com.

[Shea Levy]

On Apr 14, 2015, at 9:33 PM, Hongwei Xi <gmh...@gmail.com> wrote:

There are two issues here.

1. Syntax. The following declaration is what you want:

dataview partial_buf ( t: t@ype, int, int, addr ) =
  | { fill, total: nat | fill <= total }{ buf : addr }
      partial_buf ( t
                  , fill
                  , total
                  , buf
                  ) of ( @[ t ][ fill ] @ buf
                       , @[ t? ][ total - fill ] @ ( buf + fill )
                       )

If a parameter is given a name in a dataview declaration, then a universal

quantifier is implicitly introduced for that parameter. So your original declaration

has duplicated quantifiers.

Ah, OK. Was there a reason you kept the t: t@ype in the declaration but not the buf: addr?

2. Logic.

implement main () = let
  var buf = @[byte][10]()
  prval empty = array_v_nil{byte}()
  prval partial = partial_buf(empty, view@(buf))
  prval partial_buf(empty, l) = partial
  prval _ = array_v_unnil(empty)
  prval _ = view@(buf) := l
in 0 end

>>prval partial_buf(empty, l) = partial

The system does not know that 'empty' is a proof of an empty array-view;

it only knows that 'empty' is a prefix of the given buffer.

Hmm, but the type of partial is partial_buf ( byte, 0, 10, buf ), so empty has to be empty, right?

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLp4bFMpFZ9AiJ0ff%3D%2BAap6fDigSrkvNCU_73_24_HAc8w%40mail.gmail.com.

[gmhwxi]

>>Ah, OK. Was there a reason you kept the t: t@ype in the declaration but not the buf: addr?

I prefer to keep quantifiers over type variables at the front.

>>Hmm, but the type of partial is partial_buf ( byte, 0, 10, buf ), so empty has to be empty, right?

You are right. The following code typechecks:

implement main () = let
  var buf = @[byte][10]()

  prval pfbuf = view@(buf)
  prval pfemp = array_v_nil{byte}{buf}()
  prval partial = partial_buf{byte}{0,10}{..}(pfemp, pfbuf)
  prval partial_buf{..}{fill,total}{buf2}(empty, l) = partial
  prval _ = array_v_unnil(empty)
  prval EQADDR() = eqaddr_make{buf,buf2+fill}()

  prval _ = view@(buf) := l
in 0 end

I really don't know how to explain this. Basically, when you put a proof of some view
into view@(buf), the typechecker expects the view to be of the form T@buf (it is not
okay even if you have the form T@(buf+0)).

[Shea Levy]

On Apr 14, 2015, at 10:30 PM, gmhwxi <gmh...@gmail.com> wrote:

>>Ah, OK. Was there a reason you kept the t: t@ype in the declaration but not the buf: addr?

I prefer to keep quantifiers over type variables at the front.

>>Hmm, but the type of partial is partial_buf ( byte, 0, 10, buf ), so empty has to be empty, right?

You are right. The following code typechecks:

implement main () = let
  var buf = @[byte][10]()
  prval pfbuf = view@(buf)
  prval pfemp = array_v_nil{byte}{buf}()
  prval partial = partial_buf{byte}{0,10}{..}(pfemp, pfbuf)
  prval partial_buf{..}{fill,total}{buf2}(empty, l) = partial
  prval _ = array_v_unnil(empty)
  prval EQADDR() = eqaddr_make{buf,buf2+fill}()
  prval _ = view@(buf) := l
in 0 end


I really don't know how to explain this. Basically, when you put a proof of some view
into view@(buf), the typechecker expects the view to be of the form T@buf (it is not
okay even if you have the form T@(buf+0)).

Ah ha, I think that makes sense. So the eqaddr_make line is forcing the constraint solver to consider whether buf and buf2 + fill are equal, right?

I notice this fails to type check if I replace {0,10} with {..}, why can’t that be inferred?

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/9bb0a533-36a5-4adc-bd25-e11329408ebe%40googlegroups.com.

[gmhwxi]

>>I notice this fails to type check if I replace {0,10} with {..}, why can’t that be inferred?

The typechecker cannot figure out what 'total' should be by simply relying on unification.
Yes, it knows 'total-fill==10' but this constraint cannot be handled by unification.

[Shea Levy]

Ah, right. Thanks!

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/bb963b0b-6812-46e1-a1b0-66622c0dc65c%40googlegroups.com.